# 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

```

• References:

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