> On 6 Jun 2015, at 19:37, Tobias Nipkow <nip...@in.tum.de> wrote: > > You can always turn all patterns of the lhs into cases on the rhs and derive > the individual equations as lemmas. You also need to derive an induction > principle. I would rather keep recdef than do all that by hand.
Are we talking about this definition? recdef prep "measure fmsize" "prep (E T) = T" "prep (E F) = F" "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))" "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))" "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))" "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))" "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))" "prep (E p) = E (prep p)" "prep (A (And p q)) = And (prep (A p)) (prep (A q))" "prep (A p) = prep (NOT (E (NOT p)))" "prep (NOT (NOT p)) = prep p" "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))" "prep (NOT (A p)) = prep (E (NOT p))" "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))" "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))" "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))" "prep (NOT p) = NOT (prep p)" "prep (Or p q) = Or (prep p) (prep q)" "prep (And p q) = And (prep p) (prep q)" "prep (Imp p q) = prep (Or (NOT p) q)" "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))" "prep p = p" (hints simp add: fmsize_pos) So what is recdef doing right that fun is doing wrong? Larry _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
