*To*: Dorka Tronix <dorkatronix at gmail.com>*Subject*: Re: [isabelle] beginner proof question*From*: Simon Winwood <sjw at cse.unsw.edu.au>*Date*: Thu, 16 Jun 2011 18:22:12 +1000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <BANLkTinE0vTHFgtrrg1Sp10RZVBA7Vgwug@mail.gmail.com>*References*: <BANLkTinE0vTHFgtrrg1Sp10RZVBA7Vgwug@mail.gmail.com>

Hi, it looks like you are using the wrong induction rule for your proof --- you are using List.induct, rather than fse.induct. I had a go at the proof, attached, and found it a bit annoying. Given a slightly more compact version of fse (my fse2) it goes away by induct, auto. Simon

**Attachment:
Test.thy**

On 16/06/2011, at 1:27 PM, Dorka Tronix wrote: > Hi, > I'm a beginner with proof assistants. Apologies if this is the wrong mailing > list; I wasn't sure where to ask beginner questions. I'm trying to learn > Isabelle with some small examples of my own. I'm having problems with what > I thought would be a simple proof, and think I must be missing something > obvious. > > I have a very simple recursive data type: > datatype "S" = Assert bool > | Assign bool > | Ite bool "S list" "S list" (* if then else statement *) > > and a simple function: > > fun "fse" :: "S list \<Rightarrow> bool \<Rightarrow> bool" where > "fse [] b = b" | > "fse (x#xs) b = (case x of > (Assert e) \<Rightarrow> fse xs (b \<and> e ) > | (Assign e) \<Rightarrow> fse xs (b \<and> e) > | (Ite e s1 s2) \<Rightarrow> (fse xs (fse (s1) (b \<and> e))) > \<or> (fse xs (fse (s2) (b \<and> (\<not> e)))))" > > This function should be doing something like forward symbolic execution of a > program. I'd like to prove the law of excluded miracle: > lemma law_of_excluded_miracle [simp] : "\<forall> s. \<not> (fse s False)" > > My handwritten proof is via induction on the structure of an S list. The > empty list, Assert e, and Assign e cases are trivial. In my handwritten > proof I'm also applying the IH to ITE. Ite is causing the problem in > Isabelle. This case is recursively calling fse on the first branch s1 to > get a predicate, and then processing the rest of the list. Similar with the > second branch. > > I can't seem to get past the ITE case. At first I thought I just needed a > size function so that isabelle knew that the list sizes were decreasing so > the IH would apply. That didn't work. > > My ultimate goal is to prove: > lemma swap : "\<forall> s. \<forall> p. \<forall> q. (fse s p) \<and> q = > (fse s q) \<and> p" > > This fails as well (I'm hoping that the law_of_excluded_miracle proof will > give insight into the swap proof). > > I've attached the .thy file. Any help would be appreciated....I've spent > several days on both. > > thanks! > <simple-fse-lst-question.thy>

**References**:**[isabelle] beginner proof question***From:*Dorka Tronix

- Previous by Date: [isabelle] beginner proof question
- Next by Date: [isabelle] How to apply a fix to Isabelle?
- Previous by Thread: [isabelle] beginner proof question
- Next by Thread: [isabelle] How to apply a fix to Isabelle?
- Cl-isabelle-users June 2011 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