# HG changeset patch # User krauss # Date 1298566476 -3600 # Node ID 6fc224dc54731f1bd9e9949c49c01e01013217c2 # Parent c9d788ff7940e5cc991e102dda4a053df82b529b recdef -> fun(ction); tuned diff -r c9d788ff7940 -r 6fc224dc5473 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Thu Feb 24 17:38:05 2011 +0100 +++ b/src/HOL/Decision_Procs/Cooper.thy Thu Feb 24 17:54:36 2011 +0100 @@ -42,18 +42,17 @@ (* A size for fm *) -consts fmsize :: "fm \ nat" -recdef fmsize "measure size" +fun fmsize :: "fm \ nat" where "fmsize (NOT p) = 1 + fmsize p" - "fmsize (And p q) = 1 + fmsize p + fmsize q" - "fmsize (Or p q) = 1 + fmsize p + fmsize q" - "fmsize (Imp p q) = 3 + fmsize p + fmsize q" - "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)" - "fmsize (E p) = 1 + fmsize p" - "fmsize (A p) = 4+ fmsize p" - "fmsize (Dvd i t) = 2" - "fmsize (NDvd i t) = 2" - "fmsize p = 1" +| "fmsize (And p q) = 1 + fmsize p + fmsize q" +| "fmsize (Or p q) = 1 + fmsize p + fmsize q" +| "fmsize (Imp p q) = 3 + fmsize p + fmsize q" +| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)" +| "fmsize (E p) = 1 + fmsize p" +| "fmsize (A p) = 4+ fmsize p" +| "fmsize (Dvd i t) = 2" +| "fmsize (NDvd i t) = 2" +| "fmsize p = 1" (* several lemmas about fmsize *) lemma fmsize_pos: "fmsize p > 0" by (induct p rule: fmsize.induct) simp_all @@ -111,16 +110,15 @@ (* Quantifier freeness *) -consts qfree:: "fm \ bool" -recdef qfree "measure size" +fun qfree:: "fm \ bool" where "qfree (E p) = False" - "qfree (A p) = False" - "qfree (NOT p) = qfree p" - "qfree (And p q) = (qfree p \ qfree q)" - "qfree (Or p q) = (qfree p \ qfree q)" - "qfree (Imp p q) = (qfree p \ qfree q)" - "qfree (Iff p q) = (qfree p \ qfree q)" - "qfree p = True" +| "qfree (A p) = False" +| "qfree (NOT p) = qfree p" +| "qfree (And p q) = (qfree p \ qfree q)" +| "qfree (Or p q) = (qfree p \ qfree q)" +| "qfree (Imp p q) = (qfree p \ qfree q)" +| "qfree (Iff p q) = (qfree p \ qfree q)" +| "qfree p = True" (* Boundedness and substitution *) @@ -207,35 +205,30 @@ using qfp numsubst0_I[where b="b" and bs="bs" and a="a"] by (induct p) (simp_all add: gr0_conv_Suc) - -consts - decrnum:: "num \ num" - decr :: "fm \ fm" - -recdef decrnum "measure size" +fun decrnum:: "num \ num" where "decrnum (Bound n) = Bound (n - 1)" - "decrnum (Neg a) = Neg (decrnum a)" - "decrnum (Add a b) = Add (decrnum a) (decrnum b)" - "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)" - "decrnum (Mul c a) = Mul c (decrnum a)" - "decrnum (CN n i a) = (CN (n - 1) i (decrnum a))" - "decrnum a = a" +| "decrnum (Neg a) = Neg (decrnum a)" +| "decrnum (Add a b) = Add (decrnum a) (decrnum b)" +| "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)" +| "decrnum (Mul c a) = Mul c (decrnum a)" +| "decrnum (CN n i a) = (CN (n - 1) i (decrnum a))" +| "decrnum a = a" -recdef decr "measure size" +fun decr :: "fm \ fm" where "decr (Lt a) = Lt (decrnum a)" - "decr (Le a) = Le (decrnum a)" - "decr (Gt a) = Gt (decrnum a)" - "decr (Ge a) = Ge (decrnum a)" - "decr (Eq a) = Eq (decrnum a)" - "decr (NEq a) = NEq (decrnum a)" - "decr (Dvd i a) = Dvd i (decrnum a)" - "decr (NDvd i a) = NDvd i (decrnum a)" - "decr (NOT p) = NOT (decr p)" - "decr (And p q) = And (decr p) (decr q)" - "decr (Or p q) = Or (decr p) (decr q)" - "decr (Imp p q) = Imp (decr p) (decr q)" - "decr (Iff p q) = Iff (decr p) (decr q)" - "decr p = p" +| "decr (Le a) = Le (decrnum a)" +| "decr (Gt a) = Gt (decrnum a)" +| "decr (Ge a) = Ge (decrnum a)" +| "decr (Eq a) = Eq (decrnum a)" +| "decr (NEq a) = NEq (decrnum a)" +| "decr (Dvd i a) = Dvd i (decrnum a)" +| "decr (NDvd i a) = NDvd i (decrnum a)" +| "decr (NOT p) = NOT (decr p)" +| "decr (And p q) = And (decr p) (decr q)" +| "decr (Or p q) = Or (decr p) (decr q)" +| "decr (Imp p q) = Imp (decr p) (decr q)" +| "decr (Iff p q) = Iff (decr p) (decr q)" +| "decr p = p" lemma decrnum: assumes nb: "numbound0 t" shows "Inum (x#bs) t = Inum bs (decrnum t)" @@ -249,22 +242,20 @@ lemma decr_qf: "bound0 p \ qfree (decr p)" by (induct p, simp_all) -consts - isatom :: "fm \ bool" (* test for atomicity *) -recdef isatom "measure size" +fun isatom :: "fm \ bool" (* test for atomicity *) where "isatom T = True" - "isatom F = True" - "isatom (Lt a) = True" - "isatom (Le a) = True" - "isatom (Gt a) = True" - "isatom (Ge a) = True" - "isatom (Eq a) = True" - "isatom (NEq a) = True" - "isatom (Dvd i b) = True" - "isatom (NDvd i b) = True" - "isatom (Closed P) = True" - "isatom (NClosed P) = True" - "isatom p = False" +| "isatom F = True" +| "isatom (Lt a) = True" +| "isatom (Le a) = True" +| "isatom (Gt a) = True" +| "isatom (Ge a) = True" +| "isatom (Eq a) = True" +| "isatom (NEq a) = True" +| "isatom (Dvd i b) = True" +| "isatom (NDvd i b) = True" +| "isatom (Closed P) = True" +| "isatom (NClosed P) = True" +| "isatom p = False" lemma numsubst0_numbound0: assumes nb: "numbound0 t" shows "numbound0 (numsubst0 t a)" @@ -304,11 +295,10 @@ shows "qfree (evaldjf f xs)" using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) -consts disjuncts :: "fm \ fm list" -recdef disjuncts "measure size" +fun disjuncts :: "fm \ fm list" where "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)" - "disjuncts F = []" - "disjuncts p = [p]" +| "disjuncts F = []" +| "disjuncts p = [p]" lemma disjuncts: "(\ q\ set (disjuncts p). Ifm bbs bs q) = Ifm bbs bs p" by(induct p rule: disjuncts.induct, auto) @@ -369,22 +359,22 @@ (* Simplification *) (* Algebraic simplifications for nums *) -consts bnds:: "num \ nat list" - lex_ns:: "nat list \ nat list \ bool" -recdef bnds "measure size" + +fun bnds:: "num \ nat list" where "bnds (Bound n) = [n]" - "bnds (CN n c a) = n#(bnds a)" - "bnds (Neg a) = bnds a" - "bnds (Add a b) = (bnds a)@(bnds b)" - "bnds (Sub a b) = (bnds a)@(bnds b)" - "bnds (Mul i a) = bnds a" - "bnds a = []" -recdef lex_ns "measure (\ (xs,ys). length xs + length ys)" - "lex_ns ([], ms) = True" - "lex_ns (ns, []) = False" - "lex_ns (n#ns, m#ms) = (n ((n = m) \ lex_ns (ns,ms))) " +| "bnds (CN n c a) = n#(bnds a)" +| "bnds (Neg a) = bnds a" +| "bnds (Add a b) = (bnds a)@(bnds b)" +| "bnds (Sub a b) = (bnds a)@(bnds b)" +| "bnds (Mul i a) = bnds a" +| "bnds a = []" + +fun lex_ns:: "nat list \ nat list \ bool" where + "lex_ns [] ms = True" +| "lex_ns ns [] = False" +| "lex_ns (n#ns) (m#ms) = (n ((n = m) \ lex_ns ns ms)) " definition lex_bnd :: "num \ num \ bool" where - "lex_bnd t s \ lex_ns (bnds t, bnds s)" + "lex_bnd t s \ lex_ns (bnds t) (bnds s)" consts numadd:: "num \ num \ num" @@ -430,12 +420,10 @@ lemma numadd_nb: "\ numbound0 t ; numbound0 s\ \ numbound0 (numadd (t,s))" by (induct t s rule: numadd.induct, auto simp add: Let_def) -fun - nummul :: "int \ num \ num" -where +fun nummul :: "int \ num \ num" where "nummul i (C j) = C (i * j)" - | "nummul i (CN n c t) = CN n (c*i) (nummul i t)" - | "nummul i t = Mul i t" +| "nummul i (CN n c t) = CN n (c*i) (nummul i t)" +| "nummul i t = Mul i t" lemma nummul: "\ i. Inum bs (nummul i t) = Inum bs (Mul i t)" by (induct t rule: nummul.induct, auto simp add: algebra_simps numadd) @@ -683,30 +671,17 @@ (case_tac "simpnum a",auto)+ (* Generic quantifier elimination *) -consts qelim :: "fm \ (fm \ fm) \ fm" -recdef qelim "measure fmsize" +function (sequential) qelim :: "fm \ (fm \ fm) \ fm" where "qelim (E p) = (\ qe. DJ qe (qelim p qe))" - "qelim (A p) = (\ qe. not (qe ((qelim (NOT p) qe))))" - "qelim (NOT p) = (\ qe. not (qelim p qe))" - "qelim (And p q) = (\ qe. conj (qelim p qe) (qelim q qe))" - "qelim (Or p q) = (\ qe. disj (qelim p qe) (qelim q qe))" - "qelim (Imp p q) = (\ qe. imp (qelim p qe) (qelim q qe))" - "qelim (Iff p q) = (\ qe. iff (qelim p qe) (qelim q qe))" - "qelim p = (\ y. simpfm p)" - -(*function (sequential) - qelim :: "(fm \ fm) \ fm \ fm" -where - "qelim qe (E p) = DJ qe (qelim qe p)" - | "qelim qe (A p) = not (qe ((qelim qe (NOT p))))" - | "qelim qe (NOT p) = not (qelim qe p)" - | "qelim qe (And p q) = conj (qelim qe p) (qelim qe q)" - | "qelim qe (Or p q) = disj (qelim qe p) (qelim qe q)" - | "qelim qe (Imp p q) = imp (qelim qe p) (qelim qe q)" - | "qelim qe (Iff p q) = iff (qelim qe p) (qelim qe q)" - | "qelim qe p = simpfm p" +| "qelim (A p) = (\ qe. not (qe ((qelim (NOT p) qe))))" +| "qelim (NOT p) = (\ qe. not (qelim p qe))" +| "qelim (And p q) = (\ qe. conj (qelim p qe) (qelim q qe))" +| "qelim (Or p q) = (\ qe. disj (qelim p qe) (qelim q qe))" +| "qelim (Imp p q) = (\ qe. imp (qelim p qe) (qelim q qe))" +| "qelim (Iff p q) = (\ qe. iff (qelim p qe) (qelim q qe))" +| "qelim p = (\ y. simpfm p)" by pat_completeness auto -termination by (relation "measure (fmsize o snd)") auto*) +termination by (relation "measure fmsize") auto lemma qelim_ci: assumes qe_inv: "\ bs p. qfree p \ qfree (qe p) \ (Ifm bbs bs (qe p) = Ifm bbs bs (E p))" @@ -717,8 +692,7 @@ simpfm simpfm_qf simp del: simpfm.simps) (* Linearity for fm where Bound 0 ranges over \ *) -fun - zsplit0 :: "num \ int \ num" (* splits the bounded from the unbounded part*) +fun zsplit0 :: "num \ int \ num" (* splits the bounded from the unbounded part*) where "zsplit0 (C c) = (0,C c)" | "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"