Wie kann man eine Annahme beweisen, wenn man von einer induktiven Deklaration ausgeht?

Question

Hier ist eine Definition einer einfachen Sprache:

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 

ich für Ausdrücke eine Eingabe-Funktion definiert. Und ich versuche zu beweisen, dass, wenn And-Ausdruck einen Bool-Typ hat, beide Argumente auch Bool-Typ haben. Es ist eine Umkehrung der AndTyping-Regel aus der Theorie.

Können Sie vorschlagen, wie Sie dieses Lemma beweisen? Kann es ohne Isar bewiesen werden?

Answer 1

inductive beweist eine Eliminierungsregel namens typing.cases für diese Art von Sache. Dadurch können Sie eine "Inversionsregelung" durchführen. Die Isar Art und Weise ist es, wie dies zu tun:

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

Da es sich um die Standardregel für Fallunterscheidungen beteiligt typing, können Sie auch nur by cases auto schreiben. Auf jeden Fall, wenn Sie cases dafür verwenden, sollten Sie Kette in der Annahme, typing mit using beteiligt, from usw.

können Sie es auch tun, ohne Verkettungs zum Beispiel unter Verwendung von erule:

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

Es gibt eine andere Art und Weise ist: Sie können den inductive_cases Befehl automatisch eine passende Lemma für Regelumkehr erzeugen (im Wesentlichen ist es eine spezielle Version der typing.cases Regel):

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

Sie kann es allgemeinere machen auch:

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

das gibt Ihnen eine Eliminationsregel AndTypingRev

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

: dass Sie mit erule, elim oder cases verwenden