如何从归纳式声明中给出它的结论的假设？

下面是一个简单的语言的定义：如何从归纳式声明中给出它的结论的假设？

theory SimpleLang 
    imports Main 
begin 

type_synonym vname = "string" 
datatype exp = BConst bool | IConst int | Let vname exp exp | Var vname | And exp exp 

datatype type = BType | IType 
type_synonym tenv = "vname ⇒ type option" 

inductive typing :: "tenv ⇒ exp ⇒ type ⇒ bool" 
    ("(1_/ ⊢/ (_ :/ _))" [50,0,50] 50) where 
BConstTyping: "Γ ⊢ BConst c : BType" | 
IConstTyping: "Γ ⊢ IConst c : IType" | 
LetTyping: "⟦Γ ⊢ init : t1; Γ(var ↦ t1) ⊢ body : t⟧ ⟹ Γ ⊢ Let var init body : t" | 
VarTyping: "Γ var = Some t ⟹ Γ ⊢ Var var : t" | 
AndTyping: "⟦Γ ⊢ a : BType; Γ ⊢ b : BType⟧ ⟹ Γ ⊢ And a b : BType" 

lemma AndTypingRev: 
    "Γ ⊢ And a b : BType ⟹ Γ ⊢ a : BType ∧ Γ ⊢ b : BType" 

end

我的表达式定义一个打字的功能。我试图证明，如果And-expression有一个Bool Type，那么它的两个参数都有Bool Type。这是从理论上回归AndTyping规则。

你能否建议如何证明这个引理？ Isar没有证明吗？

来源

2017-07-07 Denis

inductive对于这类事情证明了一个叫做typing.cases的消除规则。这可以让你做'规则反转'。专家工作组的办法是做这样的：

lemma AndTypingRev: 
    assumes "Γ ⊢ And a b : BType" 
    shows "Γ ⊢ a : BType ∧ Γ ⊢ b : BType" 
    using assms by (cases rule: typing.cases) auto

因为这是涉及typing大小写区别的默认规则，你也可以只写by cases auto。在任何情况下，如果你使用cases对于这一点，你应该假设链涉及typing与using，from等

你也可以做到这一点，而无需使用例如链erule：

lemma AndTypingRev: 
    "Γ ⊢ And a b : BType ⟹ Γ ⊢ a : BType ∧ Γ ⊢ b : BType" 
    by (erule typing.cases) auto

还有另一种方法：你可以使用inductive_cases命令来自动生成规则反转合适的引理（本质上，它是typing.cases规则的专用版本）：

inductive_cases AndTypingRev: "Γ ⊢ And a b : BType"

你可以使它更加一般：

inductive_cases AndTypingRev: "Γ ⊢ And a b : t"

这给你一个消除规则AndTypingRev您可以使用erule,elim或cases：

?Γ ⊢ And ?a ?b : ?t ⟹ 
    (?t = BType ⟹ ?Γ ⊢ ?a : BType ⟹ ?Γ ⊢ ?b : BType ⟹ ?P) ⟹ 
    ?P

来源

2017-07-07 11:29:58

如何从归纳式声明中给出它的结论的假设？

回答

相关问题