summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Tue, 20 Jun 2017 08:01:56 +0200 | |

changeset 66124 | 7f0088571576 |

parent 66123 | 6e4904863d2a |

child 66125 | 28e782dd0278 |

replaced recdef by fun

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