CODEWITHSUNDEEP
isabelle
Denis
Denis

Reputation: 1271

How to prove an assumption given its conclusion from inductive declaration?

Here is a definition of a simple language:

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

I defined a typing function for expressions. And I'm trying to prove that if And-expression has a Bool Type then both of its arguments have Bool Type too. It's a reversion of AndTyping rule from the theory.

Could you suggest how to prove this lemma? Could it be proved without Isar?

Upvotes: 0

Views: 64

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8298

inductive proves an elimination rule called typing.cases for this sort of thing. That allows you to do ‘rule inversion’. The Isar way is to do it like this:

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

Since this is the default rule for case distinctions involving typing, you can also just write by cases auto. In any case, if you use cases for this, you should chain in the assumption involving typing with using, from, etc.

You can also do it without chaining using e.g. erule:

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

There is another way: You can use the inductive_cases command to automatically generate a suitable lemma for rule inversion (essentially, it's a specialised version of the typing.cases rule):

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

You can make it even more general:

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

That gives you an elimination rule AndTypingRev that you can use with erule, elim, or cases:

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

Upvotes: 1

Related Questions