Re: [isabelle] simple proof over inductively defined relation (operational semantics)

On Sat, 21 Jan 2006, Patrice Chalin wrote:

> I managed to find ways to avoid having to write intermediate lemmas which I
> will illustrate on a slightly more complex B expression:
>    *lemma *"AndB TrueB (NotB FalseB) -e-> True"
>      apply(insert TrueB)
>      apply(drule AndB)
>      apply(insert FalseB)
>      apply(drule NotB)
>      apply simp+
>    *done*
>    *lemma *"AndB TrueB (NotB FalseB) -e-> True"
>      apply(subgoal_tac "True = (True & True)", erule ssubst)
>      apply(rule AndB, auto)
>      apply(subgoal_tac "True = (Not False)", erule ssubst)
>      apply(rule NotB, auto)
>    *done*

Note that your second proof does not really scale up to larger examples, 
due to subgoal_tac, ssubst, and auto.  Any of these have certain features 
that require some experience to employ them in a stable fashion.

> Is this the way to handle it or is there a simpler way?

Maybe you want to try actual structured proofs, using the full Isar proof 
language (apart from apply/done).  E.g. like this:

datatype B = TrueB | FalseB | NotB B | AndB B B

consts eval :: "(B * bool) set"
syntax "_eval" :: "B => bool => bool" (infixl "-e->" 50)
translations  "b -e-> b'" => "(b, b') : eval"

inductive eval
    TrueB [intro]: "TrueB -e-> True"
    FalseB [intro]: "FalseB -e-> False"
    NotB [intro]: "b -e-> b' ==> NotB b -e-> (~ b')"
    AndB [intro]: "a -e-> a' ==> b -e-> b' ==> AndB a b -e-> (a' & b')"

lemma "AndB TrueB (NotB FalseB) -e-> True"
proof -
  have "AndB TrueB (NotB FalseB) -e-> (True & (~ False))"
    show "TrueB -e-> True" ..
    show "NotB FalseB -e-> (~ False)"
      show "FalseB -e-> False" ..
  also have "(True & (~ False)) = True" by simp
  finally show ?thesis .

Since the inductive intro rules have been declared as [intro], the 
subsequence 'proof' and '..' steps ('..' abbreviates 'proof qed') are all 
canonical, i.e. determined by the goal expressions.  The substitution is 
done by calculation, using 'also' and 'finally' -- watch out for the 
strong binding of "=" vs. logical connectives in the equivalence
"(True & (~ False)) = True".

This kind of structured proof uses only minimal means -- no magical 
automation so far.

>    datatype X = a | b
>    consts I :: "X set"
>    inductive I
>    intros
>      aintro: "a : I"

> How would one prove that b is not in I:
>    lemma "b ~: I"
> so that eventually one can prove that x : I ==> x = a.

We can prove the latter directly as follows:

    assumes x: "x : I"
    shows "x = a"
    using x
  proof induct
    show "a = a" ..

Here we have started with a structured statement in the first place -- 
assumes/shows instead of raw formulae.  The 'using' step tells the 
subsequent induct method to eliminate that fact inductively, which means 
we wish to do induction over the judgment "x : I" (as opposed to induction 
over the datatype, for example).

Here is your other example, without induction this time:

  lemma "b ~: I"
    assume "b : I"
    then show False
    proof cases
      assume "b = a"
      then show ?thesis by simp

The first step is canonical introduction; the inner step, involving 
'then', performs a case-split over the fact "b : I": there is only one 
case, which happens to be contradictory.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.