如何取代存在量化变量？

下面是一个简单类型系统：如何取代存在量化变量？

datatype type = 
    VoidType 
| IntegerType 
| RealType 
| StringType 

datatype val = 
    VoidVal 
| IntegerVal int 
| RealVal real 
| StringVal string 

fun type_of :: "val ⇒ type" where 
    "type_of (VoidVal) = VoidType" 
| "type_of (IntegerVal _) = IntegerType" 
| "type_of (RealVal _) = RealType" 
| "type_of (StringVal _) = StringType"

与类型一致性关系：

inductive less_type :: "type ⇒ type ⇒ bool" (infix "<" 65) where 
    "IntegerType < RealType"

整型值可强制转换为对应的真实值：

inductive cast :: "val ⇒ val ⇒ bool" where 
    "cast (IntegerVal x) (RealVal x)"

我想证明以下引理。如果变量x的类型符合RealType，则存在具有类型RealType的值y，并且x可以被铸造为y。

lemma is_castable_to_real: 
    "type_of x < RealType ⟹ ∃y. type_of y = RealType ∧ cast x y" 
    apply (rule exI[of _ "RealVal v"])

我可以证明使用cases战术通用引理：

lemma is_castable: 
    "type_of x < τ ⟹ ∃y. type_of y = τ ∧ cast x y" 
    by (cases x; cases τ; auto simp add: less_type.simps cast.simps)

但我想了解如何在引理治疗存在量词。所以我想为y提供一个具体的例子RealVal v：

type_of x < RealType ⟹ ∃v. type_of (RealVal v) = RealType ∧ cast x (RealVal v)

的问题是，我得到下面的命题，而不是：

type_of x < RealType ⟹ type_of (RealVal v) = RealType ∧ cast x (RealVal v)

又是什么样的变量v的？它是普遍量化的变量吗？如何使它存在量化？

来源

2017-09-02 Denis

是其他公式的'P'和'Q'占位符吗？否则，引理是不可证明的。如果是这样，那么发布具体公式可能会有所帮助。特别是：'y'从哪里来？它出现在'P'还是'Q'？ – peq

@peq我已经添加了一个更具体的例子。 – Denis

为了证明存在，你可以举一个具体的例子。在你的情况下，这个例子可以从引理假设推导出来。

lemma is_castable_to_real: 
assumes subtype_of_real: "type_of x < RealType" 
shows "∃y. type_of y = RealType ∧ cast x y" 
proof - 
    have "type_of x = IntegerType" 
    using subtype_of_real less_type.cases by blast 

    from this obtain i where x_def: "x = IntegerVal i" 
    by (cases x, auto) 

    (* prove it for concrete example (RealVal i) *) 
    have "type_of (RealVal i) = RealType ∧ cast x (RealVal i)" 
    by (auto simp add: x_def cast.intros) 

    (* From the concrete example, the existential statement follows: *) 
    thus "∃y. type_of y = RealType ∧ cast x y" .. 
qed

如果你只是获得或以某种方式定义之前使用v，该值将类似于undefined。它有正确的类型，但你不知道任何事情。

如果你没有破折号（-）开始proof伊莎贝尔将使用默认策略，你会得到子目标type_of ?y = RealType ∧ cast x ?y。这里?y是一个原理图变量，你可以在以后提供任何已经可用的值，然后开始证明。也许这是你得到v的那种变量，但是如何到达问题的最后一行仍然不清楚。

来源

2017-09-04 13:02:58 peq

如何取代存在量化变量？

回答

相关问题