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
  intros
    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))"
  proof
    show "TrueB -e-> True" ..
    show "NotB FalseB -e-> (~ False)"
    proof
      show "FalseB -e-> False" ..
    qed
  qed
  also have "(True & (~ False)) = True" by simp
  finally show ?thesis .
qed


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:

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

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"
  proof
    assume "b : I"
    then show False
    proof cases
      assume "b = a"
      then show ?thesis by simp
    qed
  qed

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.


	Makarius





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