*To*: Patrice Chalin <chalin at cs.concordia.ca>*Subject*: Re: [isabelle] simple proof over inductively defined relation (operational semantics)*From*: Makarius <makarius at sketis.net>*Date*: Sun, 22 Jan 2006 18:32:23 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <43D293CD.7010502@cs.concordia.ca>*References*: <43D185CE.4010109@cs.concordia.ca> <20060121092022.2511639B29@atbroy30> <43D293CD.7010502@cs.concordia.ca>

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**:**[isabelle] simple proof over inductively defined relation (operational semantics)***From:*Patrice Chalin

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

**Re: [isabelle] simple proof over inductively defined relation (operational semantics)***From:*Patrice Chalin

- Previous by Date: Re: [isabelle] proving that a value is outside of an inductivelydefined set
- Next by Date: Re: [isabelle] proving that a value is outside of an inductively defined set
- Previous by Thread: Re: [isabelle] simple proof over inductively defined relation (operational semantics)
- Next by Thread: Re: [isabelle] simple proof over inductively defined relation (operational semantics)
- Cl-isabelle-users January 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list