Re: [isabelle] beginner proof question

	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.


Attachment: Test.thy
Description: Binary data

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>

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