如何取代存在量化變量？

下面是一個簡單類型系統：如何取代存在量化變量？

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

如何取代存在量化變量？

回答

相關問題