# HG changeset patch
# User haftmann
# Date 1497938516 -7200
# Node ID 7f00885715766d30e4c08006fdc2c81caf6c9381
# Parent  6e4904863d2a9068a51320a211e298d8559503b8
replaced recdef by fun

diff -r 6e4904863d2a -r 7f0088571576 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Tue Jun 20 08:01:56 2017 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Tue Jun 20 08:01:56 2017 +0200
@@ -210,32 +210,33 @@
 | "Ifm bs (E p) = (\<exists> x. Ifm (x#bs) p)"
 | "Ifm bs (A p) = (\<forall> x. Ifm (x#bs) p)"
 
-consts prep :: "fm \<Rightarrow> fm"
-recdef prep "measure fmsize"
+function (sequential) prep :: "fm \<Rightarrow> fm" where
   "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)
+| "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"
+  by pat_completeness simp_all
+termination by (relation "measure fmsize") (simp_all add: fmsize_pos)
+
 lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
   by (induct p rule: prep.induct) auto