Comment prouver une hypothèse compte tenu de sa conclusion de la déclaration inductive?

Question

Voici une définition d'un langage simple:

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 

J'ai défini une fonction de saisie des expressions. Et j'essaie de prouver que si And-expression a un type booléen, alors ses deux arguments ont aussi un type booléen. C'est une réversion de la règle AndTyping de la théorie.

Pouvez-vous suggérer comment prouver ce lemme? Pourrait-il être prouvé sans Isar?

Answer 1

inductive prouve une règle d'élimination appelée typing.cases pour ce genre de chose. Cela vous permet de faire 'l'inversion des règles'. La façon est de le faire comme Isar ceci:

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

Depuis c'est la règle par défaut pour les distinctions de cas impliquant typing, vous pouvez simplement écrire by cases auto. Dans tous les cas, si vous utilisez cases pour cela, vous devez chaîne dans l'hypothèse impliquant typing avec using, from, etc.

Vous pouvez aussi le faire sans enchaînant par exemple en utilisant erule:

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

Il y a une autre façon: Vous pouvez utiliser la commande inductive_cases pour générer automatiquement un lemme approprié pour l'inversion de la règle (essentiellement, il est une version spécialisée de la règle typing.cases):

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

Vous peut rendre encore plus générale:

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

cela vous donne une règle d'élimination AndTypingRev que vous pouvez utiliser avec erule, elim ou cases:

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