--- 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