如何替换存在量化变量？

Question

这是一个简单的类型系统：

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？它是普遍量化的变量吗？如何使它成为存在量化的？

Answer 1

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

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 获得的那种变量，但仍然不清楚您是如何到达问题的最后一行的。

如何替换存在量化变量？

How to replace existentially quantified variable?

isabelle