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!
Description: Binary data