[isabelle] beginner proof question



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!

Attachment: simple-fse-lst-question.thy
Description: Binary data



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