# HG changeset patch # User haftmann # Date 1507494501 -7200 # Node ID f6a30d48aab014edeaa38b6e18dca4821103d4fb # Parent 1907167b60383c049804ec3b7f8069b4142a8990 replaced recdef were easy to replace diff -r 1907167b6038 -r f6a30d48aab0 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Sun Oct 08 22:28:21 2017 +0200 +++ b/src/HOL/Bali/Basis.thy Sun Oct 08 22:28:21 2017 +0200 @@ -4,7 +4,7 @@ subsection \Definitions extending HOL as logical basis of Bali\ theory Basis -imports Main "HOL-Library.Old_Recdef" +imports Main begin subsubsection "misc" diff -r 1907167b6038 -r f6a30d48aab0 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Sun Oct 08 22:28:21 2017 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Sun Oct 08 22:28:21 2017 +0200 @@ -6,7 +6,6 @@ imports Complex_Main "HOL-Library.Code_Target_Numeral" - "HOL-Library.Old_Recdef" begin (* Periodicity of dvd *) @@ -15,50 +14,74 @@ (**** SHADOW SYNTAX AND SEMANTICS ****) (*********************************************************************************) -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num +datatype (plugins del: size) num = C int | Bound nat | CN nat int num + | Neg num | Add num num | Sub num num | Mul int num -primrec num_size :: "num \ nat" \ \A size for num to make inductive proofs simpler\ +instantiation num :: size +begin + +primrec size_num :: "num \ nat" where - "num_size (C c) = 1" -| "num_size (Bound n) = 1" -| "num_size (Neg a) = 1 + num_size a" -| "num_size (Add a b) = 1 + num_size a + num_size b" -| "num_size (Sub a b) = 3 + num_size a + num_size b" -| "num_size (CN n c a) = 4 + num_size a" -| "num_size (Mul c a) = 1 + num_size a" + "size_num (C c) = 1" +| "size_num (Bound n) = 1" +| "size_num (Neg a) = 1 + size_num a" +| "size_num (Add a b) = 1 + size_num a + size_num b" +| "size_num (Sub a b) = 3 + size_num a + size_num b" +| "size_num (CN n c a) = 4 + size_num a" +| "size_num (Mul c a) = 1 + size_num a" + +instance .. + +end primrec Inum :: "int list \ num \ int" where "Inum bs (C c) = c" -| "Inum bs (Bound n) = bs!n" -| "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)" -| "Inum bs (Neg a) = -(Inum bs a)" +| "Inum bs (Bound n) = bs ! n" +| "Inum bs (CN n c a) = c * (bs ! n) + Inum bs a" +| "Inum bs (Neg a) = - Inum bs a" | "Inum bs (Add a b) = Inum bs a + Inum bs b" | "Inum bs (Sub a b) = Inum bs a - Inum bs b" -| "Inum bs (Mul c a) = c* Inum bs a" +| "Inum bs (Mul c a) = c * Inum bs a" -datatype fm = - T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num| - NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm - | Closed nat | NClosed nat +datatype (plugins del: size) fm = T | F + | Lt num | Le num | Gt num | Ge num | Eq num | NEq num + | Dvd int num | NDvd int num + | NOT fm | And fm fm | Or fm fm | Imp fm fm | Iff fm fm + | E fm | A fm | Closed nat | NClosed nat +instantiation fm :: size +begin -fun fmsize :: "fm \ nat" \ \A size for fm\ +primrec size_fm :: "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" + "size_fm (NOT p) = 1 + size_fm p" +| "size_fm (And p q) = 1 + size_fm p + size_fm q" +| "size_fm (Or p q) = 1 + size_fm p + size_fm q" +| "size_fm (Imp p q) = 3 + size_fm p + size_fm q" +| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)" +| "size_fm (E p) = 1 + size_fm p" +| "size_fm (A p) = 4 + size_fm p" +| "size_fm (Dvd i t) = 2" +| "size_fm (NDvd i t) = 2" +| "size_fm T = 1" +| "size_fm F = 1" +| "size_fm (Lt _) = 1" +| "size_fm (Le _) = 1" +| "size_fm (Gt _) = 1" +| "size_fm (Ge _) = 1" +| "size_fm (Eq _) = 1" +| "size_fm (NEq _) = 1" +| "size_fm (Closed _) = 1" +| "size_fm (NClosed _) = 1" -lemma fmsize_pos: "fmsize p > 0" - by (induct p rule: fmsize.induct) simp_all +instance .. + +end + +lemma fmsize_pos [simp]: "size p > 0" for p :: fm + by (induct p) simp_all primrec Ifm :: "bool list \ int list \ fm \ bool" \ \Semantics of formulae (fm)\ where @@ -79,10 +102,10 @@ | "Ifm bbs bs (Iff p q) \ Ifm bbs bs p = Ifm bbs bs q" | "Ifm bbs bs (E p) \ (\x. Ifm bbs (x # bs) p)" | "Ifm bbs bs (A p) \ (\x. Ifm bbs (x # bs) p)" -| "Ifm bbs bs (Closed n) \ bbs!n" -| "Ifm bbs bs (NClosed n) \ \ bbs!n" +| "Ifm bbs bs (Closed n) \ bbs ! n" +| "Ifm bbs bs (NClosed n) \ \ bbs ! n" -function (sequential) prep :: "fm \ fm" +fun prep :: "fm \ fm" where "prep (E T) = T" | "prep (E F) = F" @@ -107,10 +130,6 @@ | "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 auto - -termination - by (relation "measure fmsize") (simp_all add: fmsize_pos) lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p" by (induct p arbitrary: bs rule: prep.induct) auto @@ -424,34 +443,24 @@ definition lex_bnd :: "num \ num \ bool" where "lex_bnd t s = lex_ns (bnds t) (bnds s)" -consts numadd:: "num \ num \ num" -recdef numadd "measure (\(t, s). num_size t + num_size s)" - "numadd (CN n1 c1 r1, CN n2 c2 r2) = +fun numadd:: "num \ num \ num" +where + "numadd (CN n1 c1 r1) (CN n2 c2 r2) = (if n1 = n2 then let c = c1 + c2 - in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2)) - else if n1 \ n2 then CN n1 c1 (numadd (r1, Add (Mul c2 (Bound n2)) r2)) - else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))" - "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))" - "numadd (t, CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))" - "numadd (C b1, C b2) = C (b1 + b2)" - "numadd (a, b) = Add a b" + in if c = 0 then numadd r1 r2 else CN n1 c (numadd r1 r2) + else if n1 \ n2 then CN n1 c1 (numadd r1 (Add (Mul c2 (Bound n2)) r2)) + else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1) r2))" +| "numadd (CN n1 c1 r1) t = CN n1 c1 (numadd r1 t)" +| "numadd t (CN n2 c2 r2) = CN n2 c2 (numadd t r2)" +| "numadd (C b1) (C b2) = C (b1 + b2)" +| "numadd a b = Add a b" -lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" - apply (induct t s rule: numadd.induct) - apply (simp_all add: Let_def) - subgoal for n1 c1 r1 n2 c2 r2 - apply (cases "c1 + c2 = 0") - apply (cases "n1 \ n2") - apply simp_all - apply (cases "n1 = n2") - apply (simp_all add: algebra_simps) - apply (simp add: distrib_right[symmetric]) - done - done +lemma numadd: "Inum bs (numadd t s) = Inum bs (Add t s)" + by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff) -lemma numadd_nb: "numbound0 t \ numbound0 s \ numbound0 (numadd (t, s))" - by (induct t s rule: numadd.induct) (auto simp add: Let_def) +lemma numadd_nb: "numbound0 t \ numbound0 s \ numbound0 (numadd t s)" + by (induct t s rule: numadd.induct) (simp_all add: Let_def) fun nummul :: "int \ num \ num" where @@ -460,16 +469,16 @@ | "nummul i t = Mul i t" lemma nummul: "Inum bs (nummul i t) = Inum bs (Mul i t)" - by (induct t arbitrary: i rule: nummul.induct) (auto simp add: algebra_simps numadd) + by (induct t arbitrary: i rule: nummul.induct) (simp_all add: algebra_simps) lemma nummul_nb: "numbound0 t \ numbound0 (nummul i t)" - by (induct t arbitrary: i rule: nummul.induct) (auto simp add: numadd_nb) + by (induct t arbitrary: i rule: nummul.induct) (simp_all add: numadd_nb) definition numneg :: "num \ num" where "numneg t = nummul (- 1) t" definition numsub :: "num \ num \ num" - where "numsub s t = (if s = t then C 0 else numadd (s, numneg t))" + where "numsub s t = (if s = t then C 0 else numadd s (numneg t))" lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)" using numneg_def nummul by simp @@ -488,7 +497,7 @@ "simpnum (C j) = C j" | "simpnum (Bound n) = CN n 1 (C 0)" | "simpnum (Neg t) = numneg (simpnum t)" -| "simpnum (Add t s) = numadd (simpnum t, simpnum s)" +| "simpnum (Add t s) = numadd (simpnum t) (simpnum s)" | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)" | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))" | "simpnum t = t" @@ -587,7 +596,7 @@ lemma iff_nb: "bound0 p \ bound0 q \ bound0 (iff p q)" using iff_def by (unfold iff_def, cases "p = q", auto simp add: not_bn) -function (sequential) simpfm :: "fm \ fm" +fun simpfm :: "fm \ fm" where "simpfm (And p q) = conj (simpfm p) (simpfm q)" | "simpfm (Or p q) = disj (simpfm p) (simpfm q)" @@ -609,8 +618,6 @@ else if \i\ = 1 then F else let a' = simpnum a in case a' of C v \ if \( i dvd v) then T else F | _ \ NDvd i a')" | "simpfm p = p" - by pat_completeness auto -termination by (relation "measure fmsize") auto lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p" proof (induct p rule: simpfm.induct) @@ -819,7 +826,7 @@ done text \Generic quantifier elimination\ -function (sequential) qelim :: "fm \ (fm \ fm) \ fm" +fun 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))))" @@ -829,8 +836,6 @@ | "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") auto lemma qelim_ci: assumes qe_inv: "\bs p. qfree p \ qfree (qe p) \ Ifm bbs bs (qe p) = Ifm bbs bs (E p)" @@ -990,7 +995,7 @@ lemma zlin_qfree: "iszlfm p \ qfree p" by (induct p rule: iszlfm.induct) auto -function (sequential) zlfm :: "fm \ fm" \ \Linearity transformation for fm\ +fun zlfm :: "fm \ fm" \ \Linearity transformation for fm\ where "zlfm (And p q) = And (zlfm p) (zlfm q)" | "zlfm (Or p q) = Or (zlfm p) (zlfm q)" @@ -1058,10 +1063,6 @@ | "zlfm (NOT (Closed P)) = NClosed P" | "zlfm (NOT (NClosed P)) = Closed P" | "zlfm p = p" - by pat_completeness auto - -termination - by (relation "measure fmsize") (simp_all add: fmsize_pos) lemma zlfm_I: assumes qfp: "qfree p" diff -r 1907167b6038 -r f6a30d48aab0 src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Sun Oct 08 22:28:21 2017 +0200 +++ b/src/HOL/Decision_Procs/Ferrack.thy Sun Oct 08 22:28:21 2017 +0200 @@ -4,7 +4,7 @@ theory Ferrack imports Complex_Main Dense_Linear_Order DP_Library - "HOL-Library.Code_Target_Numeral" "HOL-Library.Old_Recdef" + "HOL-Library.Code_Target_Numeral" begin section \Quantifier elimination for \\ (0, 1, +, <)\\ @@ -13,19 +13,25 @@ (**** SHADOW SYNTAX AND SEMANTICS ****) (*********************************************************************************) -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num +datatype (plugins del: size) num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num | Mul int num - (* A size for num to make inductive proofs simpler*) -primrec num_size :: "num \ nat" +instantiation num :: size +begin + +primrec size_num :: "num \ nat" where - "num_size (C c) = 1" -| "num_size (Bound n) = 1" -| "num_size (Neg a) = 1 + num_size a" -| "num_size (Add a b) = 1 + num_size a + num_size b" -| "num_size (Sub a b) = 3 + num_size a + num_size b" -| "num_size (Mul c a) = 1 + num_size a" -| "num_size (CN n c a) = 3 + num_size a " + "size_num (C c) = 1" +| "size_num (Bound n) = 1" +| "size_num (Neg a) = 1 + size_num a" +| "size_num (Add a b) = 1 + size_num a + size_num b" +| "size_num (Sub a b) = 3 + size_num a + size_num b" +| "size_num (Mul c a) = 1 + size_num a" +| "size_num (CN n c a) = 3 + size_num a " + +instance .. + +end (* Semantics of numeral terms (num) *) primrec Inum :: "real list \ num \ real" @@ -38,26 +44,37 @@ | "Inum bs (Sub a b) = Inum bs a - Inum bs b" | "Inum bs (Mul c a) = (real_of_int c) * Inum bs a" (* FORMULAE *) -datatype fm = +datatype (plugins del: size) fm = T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm +instantiation fm :: size +begin - (* A size for fm *) -fun fmsize :: "fm \ nat" +primrec size_fm :: "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 p = 1" - (* several lemmas about fmsize *) + "size_fm (NOT p) = 1 + size_fm p" +| "size_fm (And p q) = 1 + size_fm p + size_fm q" +| "size_fm (Or p q) = 1 + size_fm p + size_fm q" +| "size_fm (Imp p q) = 3 + size_fm p + size_fm q" +| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)" +| "size_fm (E p) = 1 + size_fm p" +| "size_fm (A p) = 4 + size_fm p" +| "size_fm T = 1" +| "size_fm F = 1" +| "size_fm (Lt _) = 1" +| "size_fm (Le _) = 1" +| "size_fm (Gt _) = 1" +| "size_fm (Ge _) = 1" +| "size_fm (Eq _) = 1" +| "size_fm (NEq _) = 1" -lemma fmsize_pos: "fmsize p > 0" - by (induct p rule: fmsize.induct) simp_all +instance .. + +end + +lemma size_fm_pos [simp]: "size p > 0" for p :: fm + by (induct p) simp_all (* Semantics of formulae (fm) *) primrec Ifm ::"real list \ fm \ bool" @@ -646,33 +663,24 @@ lemma reducecoeff_numbound0: "numbound0 t \ numbound0 (reducecoeff t)" using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def) -consts numadd:: "num \ num \ num" -recdef numadd "measure (\(t,s). size t + size s)" - "numadd (CN n1 c1 r1,CN n2 c2 r2) = +fun numadd:: "num \ num \ num" +where + "numadd (CN n1 c1 r1) (CN n2 c2 r2) = (if n1 = n2 then (let c = c1 + c2 - in (if c = 0 then numadd(r1,r2) else CN n1 c (numadd (r1, r2)))) - else if n1 \ n2 then (CN n1 c1 (numadd (r1,CN n2 c2 r2))) - else (CN n2 c2 (numadd (CN n1 c1 r1, r2))))" - "numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))" - "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))" - "numadd (C b1, C b2) = C (b1 + b2)" - "numadd (a,b) = Add a b" + in (if c = 0 then numadd r1 r2 else CN n1 c (numadd r1 r2))) + else if n1 \ n2 then (CN n1 c1 (numadd r1 (CN n2 c2 r2))) + else (CN n2 c2 (numadd (CN n1 c1 r1) r2)))" +| "numadd (CN n1 c1 r1) t = CN n1 c1 (numadd r1 t)" +| "numadd t (CN n2 c2 r2) = CN n2 c2 (numadd t r2)" +| "numadd (C b1) (C b2) = C (b1 + b2)" +| "numadd a b = Add a b" -lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" - apply (induct t s rule: numadd.induct) - apply (simp_all add: Let_def) - apply (case_tac "c1 + c2 = 0") - apply (case_tac "n1 \ n2") - apply simp_all - apply (case_tac "n1 = n2") - apply (simp_all add: algebra_simps) - apply (simp only: distrib_right[symmetric]) - apply simp - done +lemma numadd [simp]: "Inum bs (numadd t s) = Inum bs (Add t s)" + by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff) -lemma numadd_nb[simp]: "\ numbound0 t ; numbound0 s\ \ numbound0 (numadd (t,s))" - by (induct t s rule: numadd.induct) (auto simp add: Let_def) +lemma numadd_nb [simp]: "numbound0 t \ numbound0 s \ numbound0 (numadd t s)" + by (induct t s rule: numadd.induct) (simp_all add: Let_def) fun nummul:: "num \ int \ num" where @@ -690,7 +698,7 @@ where "numneg t = nummul t (- 1)" definition numsub :: "num \ num \ num" - where "numsub s t = (if s = t then C 0 else numadd (s, numneg t))" + where "numsub s t = (if s = t then C 0 else numadd s (numneg t))" lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)" using numneg_def by simp @@ -709,10 +717,10 @@ "simpnum (C j) = C j" | "simpnum (Bound n) = CN n 1 (C 0)" | "simpnum (Neg t) = numneg (simpnum t)" -| "simpnum (Add t s) = numadd (simpnum t,simpnum s)" +| "simpnum (Add t s) = numadd (simpnum t) (simpnum s)" | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)" | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul (simpnum t) i)" -| "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0), simpnum t))" +| "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0)) (simpnum t))" lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t" by (induct t) simp_all @@ -726,8 +734,8 @@ | "nozerocoeff (CN n c t) = (c \ 0 \ nozerocoeff t)" | "nozerocoeff t = True" -lemma numadd_nz : "nozerocoeff a \ nozerocoeff b \ nozerocoeff (numadd (a,b))" - by (induct a b rule: numadd.induct) (auto simp add: Let_def) +lemma numadd_nz : "nozerocoeff a \ nozerocoeff b \ nozerocoeff (numadd a b)" + by (induct a b rule: numadd.induct) (simp_all add: Let_def) lemma nummul_nz : "\i. i\0 \ nozerocoeff a \ nozerocoeff (nummul a i)" by (induct a rule: nummul.induct) (auto simp add: Let_def numadd_nz) @@ -856,7 +864,7 @@ proof (cases "?g > 1") case False then show ?thesis - using assms by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0) + using assms by (auto simp add: Let_def simp_num_pair_def) next case g1: True then have g0: "?g > 0" by simp @@ -868,7 +876,7 @@ proof cases case 1 then show ?thesis - using assms g1 by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0) + using assms g1 by (auto simp add: Let_def simp_num_pair_def) next case g'1: 2 have gpdg: "?g' dvd ?g" by simp @@ -879,7 +887,7 @@ by simp then show ?thesis using assms g1 g'1 - by (auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0) + by (auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0) qed qed qed @@ -985,7 +993,7 @@ case 2 then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def) qed -qed (induct p rule: simpfm.induct, simp_all add: conj disj imp iff not) +qed (induct p rule: simpfm.induct, simp_all) lemma simpfm_bound0: "bound0 p \ bound0 (simpfm p)" @@ -1019,7 +1027,7 @@ then have nb: "numbound0 a" by simp then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) then show ?case by (cases "simpnum a") (auto simp add: Let_def) -qed (auto simp add: disj_def imp_def iff_def conj_def not_bn) +qed (auto simp add: disj_def imp_def iff_def conj_def) lemma simpfm_qf: "qfree p \ qfree (simpfm p)" apply (induct p rule: simpfm.induct) @@ -1027,38 +1035,37 @@ apply (case_tac "simpnum a", auto)+ done -consts prep :: "fm \ fm" -recdef prep "measure fmsize" +fun prep :: "fm \ fm" +where "prep (E T) = T" - "prep (E F) = F" - "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))" - "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))" - "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" - "prep (E (NOT (And p q))) = disj (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))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))" - "prep (E p) = E (prep p)" - "prep (A (And p q)) = conj (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)) = disj (prep (NOT p)) (prep (NOT q))" - "prep (NOT (A p)) = prep (E (NOT p))" - "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))" - "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))" - "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))" - "prep (NOT p) = not (prep p)" - "prep (Or p q) = disj (prep p) (prep q)" - "prep (And p q) = conj (prep p) (prep q)" - "prep (Imp p q) = prep (Or (NOT p) q)" - "prep (Iff p q) = disj (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)) = disj (prep (E p)) (prep (E q))" +| "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))" +| "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" +| "prep (E (NOT (And p q))) = disj (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))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))" +| "prep (E p) = E (prep p)" +| "prep (A (And p q)) = conj (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)) = disj (prep (NOT p)) (prep (NOT q))" +| "prep (NOT (A p)) = prep (E (NOT p))" +| "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))" +| "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))" +| "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))" +| "prep (NOT p) = not (prep p)" +| "prep (Or p q) = disj (prep p) (prep q)" +| "prep (And p q) = conj (prep p) (prep q)" +| "prep (Imp p q) = prep (Or (NOT p) q)" +| "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))" +| "prep p = p" lemma prep: "\bs. Ifm bs (prep p) = Ifm bs p" by (induct p rule: prep.induct) auto (* Generic quantifier elimination *) -function (sequential) qelim :: "fm \ (fm \ fm) \ fm" +fun 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))))" @@ -1068,16 +1075,13 @@ | "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 qelim by (relation "measure fmsize") simp_all lemma qelim_ci: assumes qe_inv: "\bs p. qfree p \ qfree (qe p) \ (Ifm bs (qe p) = Ifm bs (E p))" shows "\bs. qfree (qelim p qe) \ (Ifm bs (qelim p qe) = Ifm bs p)" using qe_inv DJ_qe[OF qe_inv] by (induct p rule: qelim.induct) - (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf - simpfm simpfm_qf simp del: simpfm.simps) + (auto simp add: simpfm simpfm_qf simp del: simpfm.simps) fun minusinf:: "fm \ fm" (* Virtual substitution of -\*) where @@ -1116,7 +1120,7 @@ | "isrlfm p = (isatom p \ (bound0 p))" (* splits the bounded from the unbounded part*) -function (sequential) rsplit0 :: "num \ int \ num" +fun rsplit0 :: "num \ int \ num" where "rsplit0 (Bound 0) = (1,C 0)" | "rsplit0 (Add a b) = (let (ca,ta) = rsplit0 a; (cb,tb) = rsplit0 b in (ca + cb, Add ta tb))" @@ -1126,8 +1130,6 @@ | "rsplit0 (CN 0 c a) = (let (ca,ta) = rsplit0 a in (c + ca, ta))" | "rsplit0 (CN n c a) = (let (ca,ta) = rsplit0 a in (ca, CN n c ta))" | "rsplit0 t = (0,t)" - by pat_completeness auto -termination rsplit0 by (relation "measure num_size") simp_all lemma rsplit0: "Inum bs ((case_prod (CN 0)) (rsplit0 t)) = Inum bs t \ numbound0 (snd (rsplit0 t))" proof (induct t rule: rsplit0.induct) @@ -1222,39 +1224,38 @@ lemma disj_lin: "isrlfm p \ isrlfm q \ isrlfm (disj p q)" by (auto simp add: disj_def) -consts rlfm :: "fm \ fm" -recdef rlfm "measure fmsize" +fun rlfm :: "fm \ fm" +where "rlfm (And p q) = conj (rlfm p) (rlfm q)" - "rlfm (Or p q) = disj (rlfm p) (rlfm q)" - "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)" - "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))" - "rlfm (Lt a) = case_prod lt (rsplit0 a)" - "rlfm (Le a) = case_prod le (rsplit0 a)" - "rlfm (Gt a) = case_prod gt (rsplit0 a)" - "rlfm (Ge a) = case_prod ge (rsplit0 a)" - "rlfm (Eq a) = case_prod eq (rsplit0 a)" - "rlfm (NEq a) = case_prod neq (rsplit0 a)" - "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))" - "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))" - "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))" - "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))" - "rlfm (NOT (NOT p)) = rlfm p" - "rlfm (NOT T) = F" - "rlfm (NOT F) = T" - "rlfm (NOT (Lt a)) = rlfm (Ge a)" - "rlfm (NOT (Le a)) = rlfm (Gt a)" - "rlfm (NOT (Gt a)) = rlfm (Le a)" - "rlfm (NOT (Ge a)) = rlfm (Lt a)" - "rlfm (NOT (Eq a)) = rlfm (NEq a)" - "rlfm (NOT (NEq a)) = rlfm (Eq a)" - "rlfm p = p" - (hints simp add: fmsize_pos) +| "rlfm (Or p q) = disj (rlfm p) (rlfm q)" +| "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)" +| "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))" +| "rlfm (Lt a) = case_prod lt (rsplit0 a)" +| "rlfm (Le a) = case_prod le (rsplit0 a)" +| "rlfm (Gt a) = case_prod gt (rsplit0 a)" +| "rlfm (Ge a) = case_prod ge (rsplit0 a)" +| "rlfm (Eq a) = case_prod eq (rsplit0 a)" +| "rlfm (NEq a) = case_prod neq (rsplit0 a)" +| "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))" +| "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))" +| "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))" +| "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))" +| "rlfm (NOT (NOT p)) = rlfm p" +| "rlfm (NOT T) = F" +| "rlfm (NOT F) = T" +| "rlfm (NOT (Lt a)) = rlfm (Ge a)" +| "rlfm (NOT (Le a)) = rlfm (Gt a)" +| "rlfm (NOT (Gt a)) = rlfm (Le a)" +| "rlfm (NOT (Ge a)) = rlfm (Lt a)" +| "rlfm (NOT (Eq a)) = rlfm (NEq a)" +| "rlfm (NOT (NEq a)) = rlfm (Eq a)" +| "rlfm p = p" lemma rlfm_I: assumes qfp: "qfree p" shows "(Ifm bs (rlfm p) = Ifm bs p) \ isrlfm (rlfm p)" using qfp - by (induct p rule: rlfm.induct) (auto simp add: lt le gt ge eq neq conj disj conj_lin disj_lin) + by (induct p rule: rlfm.induct) (auto simp add: lt le gt ge eq neq conj_lin disj_lin) (* Operations needed for Ferrante and Rackoff *) lemma rminusinf_inf: @@ -1555,29 +1556,29 @@ ultimately show ?thesis using z_def by auto qed -consts - uset:: "fm \ (num \ int) list" - usubst :: "fm \ (num \ int) \ fm " -recdef uset "measure size" +fun uset :: "fm \ (num \ int) list" +where "uset (And p q) = (uset p @ uset q)" - "uset (Or p q) = (uset p @ uset q)" - "uset (Eq (CN 0 c e)) = [(Neg e,c)]" - "uset (NEq (CN 0 c e)) = [(Neg e,c)]" - "uset (Lt (CN 0 c e)) = [(Neg e,c)]" - "uset (Le (CN 0 c e)) = [(Neg e,c)]" - "uset (Gt (CN 0 c e)) = [(Neg e,c)]" - "uset (Ge (CN 0 c e)) = [(Neg e,c)]" - "uset p = []" -recdef usubst "measure size" +| "uset (Or p q) = (uset p @ uset q)" +| "uset (Eq (CN 0 c e)) = [(Neg e,c)]" +| "uset (NEq (CN 0 c e)) = [(Neg e,c)]" +| "uset (Lt (CN 0 c e)) = [(Neg e,c)]" +| "uset (Le (CN 0 c e)) = [(Neg e,c)]" +| "uset (Gt (CN 0 c e)) = [(Neg e,c)]" +| "uset (Ge (CN 0 c e)) = [(Neg e,c)]" +| "uset p = []" + +fun usubst :: "fm \ num \ int \ fm" +where "usubst (And p q) = (\(t,n). And (usubst p (t,n)) (usubst q (t,n)))" - "usubst (Or p q) = (\(t,n). Or (usubst p (t,n)) (usubst q (t,n)))" - "usubst (Eq (CN 0 c e)) = (\(t,n). Eq (Add (Mul c t) (Mul n e)))" - "usubst (NEq (CN 0 c e)) = (\(t,n). NEq (Add (Mul c t) (Mul n e)))" - "usubst (Lt (CN 0 c e)) = (\(t,n). Lt (Add (Mul c t) (Mul n e)))" - "usubst (Le (CN 0 c e)) = (\(t,n). Le (Add (Mul c t) (Mul n e)))" - "usubst (Gt (CN 0 c e)) = (\(t,n). Gt (Add (Mul c t) (Mul n e)))" - "usubst (Ge (CN 0 c e)) = (\(t,n). Ge (Add (Mul c t) (Mul n e)))" - "usubst p = (\(t, n). p)" +| "usubst (Or p q) = (\(t,n). Or (usubst p (t,n)) (usubst q (t,n)))" +| "usubst (Eq (CN 0 c e)) = (\(t,n). Eq (Add (Mul c t) (Mul n e)))" +| "usubst (NEq (CN 0 c e)) = (\(t,n). NEq (Add (Mul c t) (Mul n e)))" +| "usubst (Lt (CN 0 c e)) = (\(t,n). Lt (Add (Mul c t) (Mul n e)))" +| "usubst (Le (CN 0 c e)) = (\(t,n). Le (Add (Mul c t) (Mul n e)))" +| "usubst (Gt (CN 0 c e)) = (\(t,n). Gt (Add (Mul c t) (Mul n e)))" +| "usubst (Ge (CN 0 c e)) = (\(t,n). Ge (Add (Mul c t) (Mul n e)))" +| "usubst p = (\(t, n). p)" lemma usubst_I: assumes lp: "isrlfm p" diff -r 1907167b6038 -r f6a30d48aab0 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Sun Oct 08 22:28:21 2017 +0200 +++ b/src/HOL/Decision_Procs/MIR.thy Sun Oct 08 22:28:21 2017 +0200 @@ -84,23 +84,32 @@ (**** SHADOW SYNTAX AND SEMANTICS ****) (*********************************************************************************) -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num - | Mul int num | Floor num| CF int num num - - (* A size for num to make inductive proofs simpler*) -primrec num_size :: "num \ nat" where - "num_size (C c) = 1" -| "num_size (Bound n) = 1" -| "num_size (Neg a) = 1 + num_size a" -| "num_size (Add a b) = 1 + num_size a + num_size b" -| "num_size (Sub a b) = 3 + num_size a + num_size b" -| "num_size (CN n c a) = 4 + num_size a " -| "num_size (CF c a b) = 4 + num_size a + num_size b" -| "num_size (Mul c a) = 1 + num_size a" -| "num_size (Floor a) = 1 + num_size a" +datatype (plugins del: size) num = C int | Bound nat | CN nat int num + | Neg num | Add num num | Sub num num + | Mul int num | Floor num | CF int num num + +instantiation num :: size +begin + +primrec size_num :: "num \ nat" +where + "size_num (C c) = 1" +| "size_num (Bound n) = 1" +| "size_num (Neg a) = 1 + size_num a" +| "size_num (Add a b) = 1 + size_num a + size_num b" +| "size_num (Sub a b) = 3 + size_num a + size_num b" +| "size_num (CN n c a) = 4 + size_num a " +| "size_num (CF c a b) = 4 + size_num a + size_num b" +| "size_num (Mul c a) = 1 + size_num a" +| "size_num (Floor a) = 1 + size_num a" + +instance .. + +end (* Semantics of numeral terms (num) *) -primrec Inum :: "real list \ num \ real" where +primrec Inum :: "real list \ num \ real" +where "Inum bs (C c) = (real_of_int c)" | "Inum bs (Bound n) = bs!n" | "Inum bs (CN n c a) = (real_of_int c) * (bs!n) + (Inum bs a)" @@ -169,48 +178,64 @@ (* FORMULAE *) -datatype fm = - T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num| - NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm - - - (* A size for fm *) -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" - (* several lemmas about fmsize *) -lemma fmsize_pos: "fmsize p > 0" - by (induct p rule: fmsize.induct) simp_all +datatype (plugins del: size) fm = + T | F | Lt num | Le num | Gt num | Ge num | Eq num | NEq num | + Dvd int num | NDvd int num | + NOT fm | And fm fm | Or fm fm | Imp fm fm | Iff fm fm | E fm | A fm + +instantiation fm :: size +begin + +primrec size_fm :: "fm \ nat" +where + "size_fm (NOT p) = 1 + size_fm p" +| "size_fm (And p q) = 1 + size_fm p + size_fm q" +| "size_fm (Or p q) = 1 + size_fm p + size_fm q" +| "size_fm (Imp p q) = 3 + size_fm p + size_fm q" +| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)" +| "size_fm (E p) = 1 + size_fm p" +| "size_fm (A p) = 4 + size_fm p" +| "size_fm (Dvd i t) = 2" +| "size_fm (NDvd i t) = 2" +| "size_fm T = 1" +| "size_fm F = 1" +| "size_fm (Lt _) = 1" +| "size_fm (Le _) = 1" +| "size_fm (Gt _) = 1" +| "size_fm (Ge _) = 1" +| "size_fm (Eq _) = 1" +| "size_fm (NEq _) = 1" + +instance .. + +end + +lemma size_fm_pos [simp]: "size p > 0" for p :: fm + by (induct p) simp_all (* Semantics of formulae (fm) *) -primrec Ifm ::"real list \ fm \ bool" where - "Ifm bs T = True" -| "Ifm bs F = False" -| "Ifm bs (Lt a) = (Inum bs a < 0)" -| "Ifm bs (Gt a) = (Inum bs a > 0)" -| "Ifm bs (Le a) = (Inum bs a \ 0)" -| "Ifm bs (Ge a) = (Inum bs a \ 0)" -| "Ifm bs (Eq a) = (Inum bs a = 0)" -| "Ifm bs (NEq a) = (Inum bs a \ 0)" -| "Ifm bs (Dvd i b) = (real_of_int i rdvd Inum bs b)" -| "Ifm bs (NDvd i b) = (\(real_of_int i rdvd Inum bs b))" -| "Ifm bs (NOT p) = (\ (Ifm bs p))" -| "Ifm bs (And p q) = (Ifm bs p \ Ifm bs q)" -| "Ifm bs (Or p q) = (Ifm bs p \ Ifm bs q)" -| "Ifm bs (Imp p q) = ((Ifm bs p) \ (Ifm bs q))" -| "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)" -| "Ifm bs (E p) = (\ x. Ifm (x#bs) p)" -| "Ifm bs (A p) = (\ x. Ifm (x#bs) p)" - -function (sequential) prep :: "fm \ fm" where +primrec Ifm ::"real list \ fm \ bool" +where + "Ifm bs T \ True" +| "Ifm bs F \ False" +| "Ifm bs (Lt a) \ Inum bs a < 0" +| "Ifm bs (Gt a) \ Inum bs a > 0" +| "Ifm bs (Le a) \ Inum bs a \ 0" +| "Ifm bs (Ge a) \ Inum bs a \ 0" +| "Ifm bs (Eq a) \ Inum bs a = 0" +| "Ifm bs (NEq a) \ Inum bs a \ 0" +| "Ifm bs (Dvd i b) \ real_of_int i rdvd Inum bs b" +| "Ifm bs (NDvd i b) \ \ (real_of_int i rdvd Inum bs b)" +| "Ifm bs (NOT p) \ \ (Ifm bs p)" +| "Ifm bs (And p q) \ Ifm bs p \ Ifm bs q" +| "Ifm bs (Or p q) \ Ifm bs p \ Ifm bs q" +| "Ifm bs (Imp p q) \ (Ifm bs p \ Ifm bs q)" +| "Ifm bs (Iff p q) \ (Ifm bs p \ Ifm bs q)" +| "Ifm bs (E p) \ (\x. Ifm (x # bs) p)" +| "Ifm bs (A p) \ (\x. Ifm (x # bs) p)" + +fun prep :: "fm \ fm" +where "prep (E T) = T" | "prep (E F) = F" | "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))" @@ -234,35 +259,35 @@ | "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: "\ bs. Ifm bs (prep p) = Ifm bs p" by (induct p rule: prep.induct) auto (* Quantifier freeness *) -fun qfree:: "fm \ bool" where +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 *) -primrec numbound0 :: "num \ bool" (* a num is INDEPENDENT of Bound 0 *) where +primrec numbound0 :: "num \ bool" (* a num is INDEPENDENT of Bound 0 *) +where "numbound0 (C c) = True" - | "numbound0 (Bound n) = (n>0)" - | "numbound0 (CN n i a) = (n > 0 \ numbound0 a)" - | "numbound0 (Neg a) = numbound0 a" - | "numbound0 (Add a b) = (numbound0 a \ numbound0 b)" - | "numbound0 (Sub a b) = (numbound0 a \ numbound0 b)" - | "numbound0 (Mul i a) = numbound0 a" - | "numbound0 (Floor a) = numbound0 a" - | "numbound0 (CF c a b) = (numbound0 a \ numbound0 b)" +| "numbound0 (Bound n) = (n>0)" +| "numbound0 (CN n i a) = (n > 0 \ numbound0 a)" +| "numbound0 (Neg a) = numbound0 a" +| "numbound0 (Add a b) = (numbound0 a \ numbound0 b)" +| "numbound0 (Sub a b) = (numbound0 a \ numbound0 b)" +| "numbound0 (Mul i a) = numbound0 a" +| "numbound0 (Floor a) = numbound0 a" +| "numbound0 (CF c a b) = (numbound0 a \ numbound0 b)" lemma numbound0_I: assumes nb: "numbound0 a" @@ -280,24 +305,25 @@ by (simp add: isint_def) qed -primrec bound0:: "fm \ bool" (* A Formula is independent of Bound 0 *) where +primrec bound0:: "fm \ bool" (* A Formula is independent of Bound 0 *) +where "bound0 T = True" - | "bound0 F = True" - | "bound0 (Lt a) = numbound0 a" - | "bound0 (Le a) = numbound0 a" - | "bound0 (Gt a) = numbound0 a" - | "bound0 (Ge a) = numbound0 a" - | "bound0 (Eq a) = numbound0 a" - | "bound0 (NEq a) = numbound0 a" - | "bound0 (Dvd i a) = numbound0 a" - | "bound0 (NDvd i a) = numbound0 a" - | "bound0 (NOT p) = bound0 p" - | "bound0 (And p q) = (bound0 p \ bound0 q)" - | "bound0 (Or p q) = (bound0 p \ bound0 q)" - | "bound0 (Imp p q) = ((bound0 p) \ (bound0 q))" - | "bound0 (Iff p q) = (bound0 p \ bound0 q)" - | "bound0 (E p) = False" - | "bound0 (A p) = False" +| "bound0 F = True" +| "bound0 (Lt a) = numbound0 a" +| "bound0 (Le a) = numbound0 a" +| "bound0 (Gt a) = numbound0 a" +| "bound0 (Ge a) = numbound0 a" +| "bound0 (Eq a) = numbound0 a" +| "bound0 (NEq a) = numbound0 a" +| "bound0 (Dvd i a) = numbound0 a" +| "bound0 (NDvd i a) = numbound0 a" +| "bound0 (NOT p) = bound0 p" +| "bound0 (And p q) = (bound0 p \ bound0 q)" +| "bound0 (Or p q) = (bound0 p \ bound0 q)" +| "bound0 (Imp p q) = ((bound0 p) \ (bound0 q))" +| "bound0 (Iff p q) = (bound0 p \ bound0 q)" +| "bound0 (E p) = False" +| "bound0 (A p) = False" lemma bound0_I: assumes bp: "bound0 p" @@ -305,44 +331,47 @@ using bp numbound0_I [where b="b" and bs="bs" and b'="b'"] by (induct p) auto -primrec numsubst0:: "num \ num \ num" (* substitute a num into a num for Bound 0 *) where +primrec numsubst0:: "num \ num \ num" (* substitute a num into a num for Bound 0 *) +where "numsubst0 t (C c) = (C c)" - | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)" - | "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))" - | "numsubst0 t (CF i a b) = CF i (numsubst0 t a) (numsubst0 t b)" - | "numsubst0 t (Neg a) = Neg (numsubst0 t a)" - | "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)" - | "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" - | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)" - | "numsubst0 t (Floor a) = Floor (numsubst0 t a)" +| "numsubst0 t (Bound n) = (if n=0 then t else Bound n)" +| "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))" +| "numsubst0 t (CF i a b) = CF i (numsubst0 t a) (numsubst0 t b)" +| "numsubst0 t (Neg a) = Neg (numsubst0 t a)" +| "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)" +| "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" +| "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)" +| "numsubst0 t (Floor a) = Floor (numsubst0 t a)" lemma numsubst0_I: shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t" by (induct t) simp_all -primrec subst0:: "num \ fm \ fm" (* substitue a num into a formula for Bound 0 *) where +primrec subst0:: "num \ fm \ fm" (* substitue a num into a formula for Bound 0 *) +where "subst0 t T = T" - | "subst0 t F = F" - | "subst0 t (Lt a) = Lt (numsubst0 t a)" - | "subst0 t (Le a) = Le (numsubst0 t a)" - | "subst0 t (Gt a) = Gt (numsubst0 t a)" - | "subst0 t (Ge a) = Ge (numsubst0 t a)" - | "subst0 t (Eq a) = Eq (numsubst0 t a)" - | "subst0 t (NEq a) = NEq (numsubst0 t a)" - | "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)" - | "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)" - | "subst0 t (NOT p) = NOT (subst0 t p)" - | "subst0 t (And p q) = And (subst0 t p) (subst0 t q)" - | "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)" - | "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)" - | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)" +| "subst0 t F = F" +| "subst0 t (Lt a) = Lt (numsubst0 t a)" +| "subst0 t (Le a) = Le (numsubst0 t a)" +| "subst0 t (Gt a) = Gt (numsubst0 t a)" +| "subst0 t (Ge a) = Ge (numsubst0 t a)" +| "subst0 t (Eq a) = Eq (numsubst0 t a)" +| "subst0 t (NEq a) = NEq (numsubst0 t a)" +| "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)" +| "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)" +| "subst0 t (NOT p) = NOT (subst0 t p)" +| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)" +| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)" +| "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)" +| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)" lemma subst0_I: assumes qfp: "qfree p" shows "Ifm (b#bs) (subst0 a p) = Ifm ((Inum (b#bs) a)#bs) p" using qfp numsubst0_I[where b="b" and bs="bs" and a="a"] by (induct p) simp_all -fun decrnum:: "num \ num" where +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)" @@ -353,7 +382,8 @@ | "decrnum (CF c a b) = CF c (decrnum a) (decrnum b)" | "decrnum a = a" -fun decr :: "fm \ fm" where +fun decr :: "fm \ fm" +where "decr (Lt a) = Lt (decrnum a)" | "decr (Le a) = Le (decrnum a)" | "decr (Gt a) = Gt (decrnum a)" @@ -380,7 +410,8 @@ lemma decr_qf: "bound0 p \ qfree (decr p)" by (induct p) simp_all -fun isatom :: "fm \ bool" (* test for atomicity *) where +fun isatom :: "fm \ bool" (* test for atomicity *) +where "isatom T = True" | "isatom F = True" | "isatom (Lt a) = True" @@ -441,12 +472,14 @@ apply auto done -fun disjuncts :: "fm \ fm list" where +fun disjuncts :: "fm \ fm list" +where "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)" | "disjuncts F = []" | "disjuncts p = [p]" -fun conjuncts :: "fm \ fm list" where +fun conjuncts :: "fm \ fm list" +where "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)" | "conjuncts T = []" | "conjuncts p = [p]" @@ -511,7 +544,8 @@ (* Simplification *) (* Algebraic simplifications for nums *) -fun bnds:: "num \ nat list" where +fun bnds:: "num \ nat list" +where "bnds (Bound n) = [n]" | "bnds (CN n c a) = n#(bnds a)" | "bnds (Neg a) = bnds a" @@ -521,14 +555,17 @@ | "bnds (Floor a) = bnds a" | "bnds (CF c a b) = (bnds a)@(bnds b)" | "bnds a = []" -fun lex_ns:: "nat list \ nat list \ bool" where + +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)" -fun maxcoeff:: "num \ int" where +fun maxcoeff:: "num \ int" +where "maxcoeff (C i) = \i\" | "maxcoeff (CN n c t) = max \c\ (maxcoeff t)" | "maxcoeff (CF c t s) = max \c\ (maxcoeff s)" @@ -537,7 +574,8 @@ lemma maxcoeff_pos: "maxcoeff t \ 0" by (induct t rule: maxcoeff.induct) auto -fun numgcdh:: "num \ int \ int" where +fun numgcdh:: "num \ int \ int" +where "numgcdh (C i) = (\g. gcd i g)" | "numgcdh (CN n c t) = (\g. gcd c (numgcdh t g))" | "numgcdh (CF c s t) = (\g. gcd c (numgcdh t g))" @@ -546,7 +584,8 @@ definition numgcd :: "num \ int" where "numgcd t = numgcdh t (maxcoeff t)" -fun reducecoeffh:: "num \ int \ num" where +fun reducecoeffh:: "num \ int \ num" +where "reducecoeffh (C i) = (\ g. C (i div g))" | "reducecoeffh (CN n c t) = (\ g. CN n (c div g) (reducecoeffh t g))" | "reducecoeffh (CF c s t) = (\ g. CF (c div g) s (reducecoeffh t g))" @@ -558,7 +597,8 @@ (let g = numgcd t in if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)" -fun dvdnumcoeff:: "num \ int \ bool" where +fun dvdnumcoeff:: "num \ int \ bool" +where "dvdnumcoeff (C i) = (\ g. g dvd i)" | "dvdnumcoeff (CN n c t) = (\ g. g dvd c \ (dvdnumcoeff t g))" | "dvdnumcoeff (CF c s t) = (\ g. g dvd c \ (dvdnumcoeff t g))" @@ -602,7 +642,8 @@ from assms 3 show ?case by (simp add: real_of_int_div[OF gd] algebra_simps) qed (auto simp add: numgcd_def gp) -fun ismaxcoeff:: "num \ int \ bool" where +fun ismaxcoeff:: "num \ int \ bool" +where "ismaxcoeff (C i) = (\ x. \i\ \ x)" | "ismaxcoeff (CN n c t) = (\x. \c\ \ x \ (ismaxcoeff t x))" | "ismaxcoeff (CF c s t) = (\x. \c\ \ x \ (ismaxcoeff t x))" @@ -711,7 +752,7 @@ using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def) consts numadd:: "num \ num \ num" -recdef numadd "measure (\ (t,s). size t + size s)" +recdef numadd "measure (\(t, s). size t + size s)" "numadd (CN n1 c1 r1,CN n2 c2 r2) = (if n1=n2 then (let c = c1 + c2 @@ -730,22 +771,14 @@ "numadd (C b1, C b2) = C (b1+b2)" "numadd (a,b) = Add a b" -lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)" -apply (induct t s rule: numadd.induct, simp_all add: Let_def) - apply (case_tac "c1+c2 = 0",case_tac "n1 \ n2", simp_all) - apply (case_tac "n1 = n2", simp_all add: algebra_simps) - apply (simp only: distrib_right[symmetric]) - apply simp -apply (case_tac "lex_bnd t1 t2", simp_all) - apply (case_tac "c1+c2 = 0") - apply (case_tac "t1 = t2") - apply (simp_all add: algebra_simps distrib_right[symmetric] of_int_mult[symmetric] of_int_add[symmetric]del: of_int_mult of_int_add distrib_right) - done - -lemma numadd_nb[simp]: "\ numbound0 t ; numbound0 s\ \ numbound0 (numadd (t,s))" - by (induct t s rule: numadd.induct) (auto simp add: Let_def) - -fun nummul:: "num \ int \ num" where +lemma numadd [simp]: "Inum bs (numadd (t, s)) = Inum bs (Add t s)" + by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff) + +lemma numadd_nb [simp]: "numbound0 t \ numbound0 s \ numbound0 (numadd (t, s))" + by (induct t s rule: numadd.induct) (simp_all add: Let_def) + +fun nummul:: "num \ int \ num" +where "nummul (C j) = (\ i. C (i*j))" | "nummul (CN n c t) = (\ i. CN n (c*i) (nummul t i))" | "nummul (CF c t s) = (\ i. CF (c*i) t (nummul s i))" @@ -785,7 +818,8 @@ finally show ?thesis . qed -fun split_int:: "num \ num \ num" where +fun split_int:: "num \ num \ num" +where "split_int (C c) = (C 0, C c)" | "split_int (CN n c b) = (let (bv,bi) = split_int b @@ -853,7 +887,8 @@ using split_int_nb[where t="t"] by (cases "fst (split_int t)") (auto simp add: numfloor_def Let_def split_def) -function simpnum:: "num \ num" where +fun simpnum:: "num \ num" +where "simpnum (C j) = C j" | "simpnum (Bound n) = CN n 1 (C 0)" | "simpnum (Neg t) = numneg (simpnum t)" @@ -863,8 +898,6 @@ | "simpnum (Floor t) = numfloor (simpnum t)" | "simpnum (CN n c t) = (if c=0 then simpnum t else CN n c (simpnum t))" | "simpnum (CF c t s) = simpnum(Add (Mul c (Floor t)) s)" -by pat_completeness auto -termination by (relation "measure num_size") auto lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t" by (induct t rule: simpnum.induct) auto @@ -872,7 +905,8 @@ lemma simpnum_numbound0[simp]: "numbound0 t \ numbound0 (simpnum t)" by (induct t rule: simpnum.induct) auto -fun nozerocoeff:: "num \ bool" where +fun nozerocoeff:: "num \ bool" +where "nozerocoeff (C c) = True" | "nozerocoeff (CN n c t) = (c\0 \ nozerocoeff t)" | "nozerocoeff (CF c s t) = (c \ 0 \ nozerocoeff t)" @@ -1001,7 +1035,8 @@ ultimately show ?thesis by blast qed -fun not:: "fm \ fm" where +fun not:: "fm \ fm" +where "not (NOT p) = p" | "not T = F" | "not F = T" @@ -1059,12 +1094,13 @@ Iff p q)" lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)" - by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp) (cases "not p= q", auto simp add:not) + by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp) (cases "not p= q", auto) lemma iff_qf[simp]: "\qfree p ; qfree q\ \ qfree (iff p q)" by (unfold iff_def,cases "p=q", auto) -fun check_int:: "num \ bool" where +fun check_int:: "num \ bool" +where "check_int (C i) = True" | "check_int (Floor t) = True" | "check_int (Mul i t) = check_int t" @@ -1139,14 +1175,15 @@ ultimately show ?thesis by blast qed -function (sequential) simpfm :: "fm \ fm" where +fun simpfm :: "fm \ fm" +where "simpfm (And p q) = conj (simpfm p) (simpfm q)" | "simpfm (Or p q) = disj (simpfm p) (simpfm q)" | "simpfm (Imp p q) = imp (simpfm p) (simpfm q)" | "simpfm (Iff p q) = iff (simpfm p) (simpfm q)" | "simpfm (NOT p) = not (simpfm p)" | "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \ if (v < 0) then T else F - | _ \ Lt (reducecoeff a'))" + | _ \ Lt (reducecoeff a'))" | "simpfm (Le a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ Le (reducecoeff a'))" | "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \ if (v > 0) then T else F | _ \ Gt (reducecoeff a'))" | "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \