[isabelle-dev] Remaining uses of defer_recdef?
Larry Paulson
lp15 at cam.ac.uk
Sat Jun 6 20:44:15 CEST 2015
> On 6 Jun 2015, at 19:37, Tobias Nipkow <nipkow at 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
More information about the isabelle-dev
mailing list