replaced recdef were easy to replace
authorhaftmann
Sun Oct 08 22:28:21 2017 +0200 (19 months ago)
changeset 66809f6a30d48aab0
parent 66808 1907167b6038
child 66810 cc2b490f9dc4
replaced recdef were easy to replace
src/HOL/Bali/Basis.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  subsection \<open>Definitions extending HOL as logical basis of Bali\<close>
     1.5  
     1.6  theory Basis
     1.7 -imports Main "HOL-Library.Old_Recdef"
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  subsubsection "misc"
     2.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sun Oct 08 22:28:21 2017 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Oct 08 22:28:21 2017 +0200
     2.3 @@ -6,7 +6,6 @@
     2.4  imports
     2.5    Complex_Main
     2.6    "HOL-Library.Code_Target_Numeral"
     2.7 -  "HOL-Library.Old_Recdef"
     2.8  begin
     2.9  
    2.10  (* Periodicity of dvd *)
    2.11 @@ -15,50 +14,74 @@
    2.12  (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    2.13  (*********************************************************************************)
    2.14  
    2.15 -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
    2.16 +datatype (plugins del: size) num = C int | Bound nat | CN nat int num
    2.17 +  | Neg num | Add num num | Sub num num
    2.18    | Mul int num
    2.19  
    2.20 -primrec num_size :: "num \<Rightarrow> nat" \<comment> \<open>A size for num to make inductive proofs simpler\<close>
    2.21 +instantiation num :: size
    2.22 +begin
    2.23 +
    2.24 +primrec size_num :: "num \<Rightarrow> nat"
    2.25  where
    2.26 -  "num_size (C c) = 1"
    2.27 -| "num_size (Bound n) = 1"
    2.28 -| "num_size (Neg a) = 1 + num_size a"
    2.29 -| "num_size (Add a b) = 1 + num_size a + num_size b"
    2.30 -| "num_size (Sub a b) = 3 + num_size a + num_size b"
    2.31 -| "num_size (CN n c a) = 4 + num_size a"
    2.32 -| "num_size (Mul c a) = 1 + num_size a"
    2.33 +  "size_num (C c) = 1"
    2.34 +| "size_num (Bound n) = 1"
    2.35 +| "size_num (Neg a) = 1 + size_num a"
    2.36 +| "size_num (Add a b) = 1 + size_num a + size_num b"
    2.37 +| "size_num (Sub a b) = 3 + size_num a + size_num b"
    2.38 +| "size_num (CN n c a) = 4 + size_num a"
    2.39 +| "size_num (Mul c a) = 1 + size_num a"
    2.40 +
    2.41 +instance ..
    2.42 +
    2.43 +end
    2.44  
    2.45  primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int"
    2.46  where
    2.47    "Inum bs (C c) = c"
    2.48 -| "Inum bs (Bound n) = bs!n"
    2.49 -| "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
    2.50 -| "Inum bs (Neg a) = -(Inum bs a)"
    2.51 +| "Inum bs (Bound n) = bs ! n"
    2.52 +| "Inum bs (CN n c a) = c * (bs ! n) + Inum bs a"
    2.53 +| "Inum bs (Neg a) = - Inum bs a"
    2.54  | "Inum bs (Add a b) = Inum bs a + Inum bs b"
    2.55  | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
    2.56 -| "Inum bs (Mul c a) = c* Inum bs a"
    2.57 +| "Inum bs (Mul c a) = c * Inum bs a"
    2.58  
    2.59 -datatype fm  =
    2.60 -  T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
    2.61 -  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
    2.62 -  | Closed nat | NClosed nat
    2.63 +datatype (plugins del: size) fm = T | F
    2.64 +  | Lt num | Le num | Gt num | Ge num | Eq num | NEq num
    2.65 +  | Dvd int num | NDvd int num
    2.66 +  | NOT fm | And fm fm | Or fm fm | Imp fm fm | Iff fm fm
    2.67 +  | E fm | A fm | Closed nat | NClosed nat
    2.68  
    2.69 +instantiation fm :: size
    2.70 +begin
    2.71  
    2.72 -fun fmsize :: "fm \<Rightarrow> nat"  \<comment> \<open>A size for fm\<close>
    2.73 +primrec size_fm :: "fm \<Rightarrow> nat"
    2.74  where
    2.75 -  "fmsize (NOT p) = 1 + fmsize p"
    2.76 -| "fmsize (And p q) = 1 + fmsize p + fmsize q"
    2.77 -| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    2.78 -| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
    2.79 -| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
    2.80 -| "fmsize (E p) = 1 + fmsize p"
    2.81 -| "fmsize (A p) = 4+ fmsize p"
    2.82 -| "fmsize (Dvd i t) = 2"
    2.83 -| "fmsize (NDvd i t) = 2"
    2.84 -| "fmsize p = 1"
    2.85 +  "size_fm (NOT p) = 1 + size_fm p"
    2.86 +| "size_fm (And p q) = 1 + size_fm p + size_fm q"
    2.87 +| "size_fm (Or p q) = 1 + size_fm p + size_fm q"
    2.88 +| "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
    2.89 +| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
    2.90 +| "size_fm (E p) = 1 + size_fm p"
    2.91 +| "size_fm (A p) = 4 + size_fm p"
    2.92 +| "size_fm (Dvd i t) = 2"
    2.93 +| "size_fm (NDvd i t) = 2"
    2.94 +| "size_fm T = 1" 
    2.95 +| "size_fm F = 1"
    2.96 +| "size_fm (Lt _) = 1" 
    2.97 +| "size_fm (Le _) = 1" 
    2.98 +| "size_fm (Gt _) = 1" 
    2.99 +| "size_fm (Ge _) = 1" 
   2.100 +| "size_fm (Eq _) = 1" 
   2.101 +| "size_fm (NEq _) = 1" 
   2.102 +| "size_fm (Closed _) = 1" 
   2.103 +| "size_fm (NClosed _) = 1"
   2.104  
   2.105 -lemma fmsize_pos: "fmsize p > 0"
   2.106 -  by (induct p rule: fmsize.induct) simp_all
   2.107 +instance ..
   2.108 +
   2.109 +end
   2.110 +
   2.111 +lemma fmsize_pos [simp]: "size p > 0" for p :: fm
   2.112 +  by (induct p) simp_all
   2.113  
   2.114  primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  \<comment> \<open>Semantics of formulae (fm)\<close>
   2.115  where
   2.116 @@ -79,10 +102,10 @@
   2.117  | "Ifm bbs bs (Iff p q) \<longleftrightarrow> Ifm bbs bs p = Ifm bbs bs q"
   2.118  | "Ifm bbs bs (E p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) p)"
   2.119  | "Ifm bbs bs (A p) \<longleftrightarrow> (\<forall>x. Ifm bbs (x # bs) p)"
   2.120 -| "Ifm bbs bs (Closed n) \<longleftrightarrow> bbs!n"
   2.121 -| "Ifm bbs bs (NClosed n) \<longleftrightarrow> \<not> bbs!n"
   2.122 +| "Ifm bbs bs (Closed n) \<longleftrightarrow> bbs ! n"
   2.123 +| "Ifm bbs bs (NClosed n) \<longleftrightarrow> \<not> bbs ! n"
   2.124  
   2.125 -function (sequential) prep :: "fm \<Rightarrow> fm"
   2.126 +fun prep :: "fm \<Rightarrow> fm"
   2.127  where
   2.128    "prep (E T) = T"
   2.129  | "prep (E F) = F"
   2.130 @@ -107,10 +130,6 @@
   2.131  | "prep (Imp p q) = prep (Or (NOT p) q)"
   2.132  | "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   2.133  | "prep p = p"
   2.134 -  by pat_completeness auto
   2.135 -
   2.136 -termination
   2.137 -  by (relation "measure fmsize") (simp_all add: fmsize_pos)
   2.138  
   2.139  lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
   2.140    by (induct p arbitrary: bs rule: prep.induct) auto
   2.141 @@ -424,34 +443,24 @@
   2.142  definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool"
   2.143    where "lex_bnd t s = lex_ns (bnds t) (bnds s)"
   2.144  
   2.145 -consts numadd:: "num \<times> num \<Rightarrow> num"
   2.146 -recdef numadd "measure (\<lambda>(t, s). num_size t + num_size s)"
   2.147 -  "numadd (CN n1 c1 r1, CN n2 c2 r2) =
   2.148 +fun numadd:: "num \<Rightarrow> num \<Rightarrow> num"
   2.149 +where
   2.150 +  "numadd (CN n1 c1 r1) (CN n2 c2 r2) =
   2.151      (if n1 = n2 then
   2.152         let c = c1 + c2
   2.153 -       in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2))
   2.154 -     else if n1 \<le> n2 then CN n1 c1 (numadd (r1, Add (Mul c2 (Bound n2)) r2))
   2.155 -     else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))"
   2.156 -  "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"
   2.157 -  "numadd (t, CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))"
   2.158 -  "numadd (C b1, C b2) = C (b1 + b2)"
   2.159 -  "numadd (a, b) = Add a b"
   2.160 +       in if c = 0 then numadd r1 r2 else CN n1 c (numadd r1 r2)
   2.161 +     else if n1 \<le> n2 then CN n1 c1 (numadd r1 (Add (Mul c2 (Bound n2)) r2))
   2.162 +     else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1) r2))"
   2.163 +| "numadd (CN n1 c1 r1) t = CN n1 c1 (numadd r1 t)"
   2.164 +| "numadd t (CN n2 c2 r2) = CN n2 c2 (numadd t r2)"
   2.165 +| "numadd (C b1) (C b2) = C (b1 + b2)"
   2.166 +| "numadd a b = Add a b"
   2.167  
   2.168 -lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
   2.169 -  apply (induct t s rule: numadd.induct)
   2.170 -  apply (simp_all add: Let_def)
   2.171 -  subgoal for n1 c1 r1 n2 c2 r2
   2.172 -    apply (cases "c1 + c2 = 0")
   2.173 -    apply (cases "n1 \<le> n2")
   2.174 -    apply simp_all
   2.175 -     apply (cases "n1 = n2")
   2.176 -      apply (simp_all add: algebra_simps)
   2.177 -    apply (simp add: distrib_right[symmetric])
   2.178 -    done
   2.179 -  done
   2.180 +lemma numadd: "Inum bs (numadd t s) = Inum bs (Add t s)"
   2.181 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff)
   2.182  
   2.183 -lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"
   2.184 -  by (induct t s rule: numadd.induct) (auto simp add: Let_def)
   2.185 +lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd t s)"
   2.186 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def)
   2.187  
   2.188  fun nummul :: "int \<Rightarrow> num \<Rightarrow> num"
   2.189  where
   2.190 @@ -460,16 +469,16 @@
   2.191  | "nummul i t = Mul i t"
   2.192  
   2.193  lemma nummul: "Inum bs (nummul i t) = Inum bs (Mul i t)"
   2.194 -  by (induct t arbitrary: i rule: nummul.induct) (auto simp add: algebra_simps numadd)
   2.195 +  by (induct t arbitrary: i rule: nummul.induct) (simp_all add: algebra_simps)
   2.196  
   2.197  lemma nummul_nb: "numbound0 t \<Longrightarrow> numbound0 (nummul i t)"
   2.198 -  by (induct t arbitrary: i rule: nummul.induct) (auto simp add: numadd_nb)
   2.199 +  by (induct t arbitrary: i rule: nummul.induct) (simp_all add: numadd_nb)
   2.200  
   2.201  definition numneg :: "num \<Rightarrow> num"
   2.202    where "numneg t = nummul (- 1) t"
   2.203  
   2.204  definition numsub :: "num \<Rightarrow> num \<Rightarrow> num"
   2.205 -  where "numsub s t = (if s = t then C 0 else numadd (s, numneg t))"
   2.206 +  where "numsub s t = (if s = t then C 0 else numadd s (numneg t))"
   2.207  
   2.208  lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)"
   2.209    using numneg_def nummul by simp
   2.210 @@ -488,7 +497,7 @@
   2.211    "simpnum (C j) = C j"
   2.212  | "simpnum (Bound n) = CN n 1 (C 0)"
   2.213  | "simpnum (Neg t) = numneg (simpnum t)"
   2.214 -| "simpnum (Add t s) = numadd (simpnum t, simpnum s)"
   2.215 +| "simpnum (Add t s) = numadd (simpnum t) (simpnum s)"
   2.216  | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
   2.217  | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))"
   2.218  | "simpnum t = t"
   2.219 @@ -587,7 +596,7 @@
   2.220  lemma iff_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (iff p q)"
   2.221    using iff_def by (unfold iff_def, cases "p = q", auto simp add: not_bn)
   2.222  
   2.223 -function (sequential) simpfm :: "fm \<Rightarrow> fm"
   2.224 +fun simpfm :: "fm \<Rightarrow> fm"
   2.225  where
   2.226    "simpfm (And p q) = conj (simpfm p) (simpfm q)"
   2.227  | "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   2.228 @@ -609,8 +618,6 @@
   2.229       else if \<bar>i\<bar> = 1 then F
   2.230       else let a' = simpnum a in case a' of C v \<Rightarrow> if \<not>( i dvd v) then T else F | _ \<Rightarrow> NDvd i a')"
   2.231  | "simpfm p = p"
   2.232 -  by pat_completeness auto
   2.233 -termination by (relation "measure fmsize") auto
   2.234  
   2.235  lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"
   2.236  proof (induct p rule: simpfm.induct)
   2.237 @@ -819,7 +826,7 @@
   2.238    done
   2.239  
   2.240  text \<open>Generic quantifier elimination\<close>
   2.241 -function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   2.242 +fun qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   2.243  where
   2.244    "qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))"
   2.245  | "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
   2.246 @@ -829,8 +836,6 @@
   2.247  | "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
   2.248  | "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
   2.249  | "qelim p = (\<lambda>y. simpfm p)"
   2.250 -  by pat_completeness auto
   2.251 -termination by (relation "measure fmsize") auto
   2.252  
   2.253  lemma qelim_ci:
   2.254    assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
   2.255 @@ -990,7 +995,7 @@
   2.256  lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
   2.257    by (induct p rule: iszlfm.induct) auto
   2.258  
   2.259 -function (sequential) zlfm :: "fm \<Rightarrow> fm"  \<comment> \<open>Linearity transformation for fm\<close>
   2.260 +fun zlfm :: "fm \<Rightarrow> fm"  \<comment> \<open>Linearity transformation for fm\<close>
   2.261  where
   2.262    "zlfm (And p q) = And (zlfm p) (zlfm q)"
   2.263  | "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
   2.264 @@ -1058,10 +1063,6 @@
   2.265  | "zlfm (NOT (Closed P)) = NClosed P"
   2.266  | "zlfm (NOT (NClosed P)) = Closed P"
   2.267  | "zlfm p = p"
   2.268 -  by pat_completeness auto
   2.269 -
   2.270 -termination
   2.271 -  by (relation "measure fmsize") (simp_all add: fmsize_pos)
   2.272  
   2.273  lemma zlfm_I:
   2.274    assumes qfp: "qfree p"
     3.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Sun Oct 08 22:28:21 2017 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Sun Oct 08 22:28:21 2017 +0200
     3.3 @@ -4,7 +4,7 @@
     3.4  
     3.5  theory Ferrack
     3.6  imports Complex_Main Dense_Linear_Order DP_Library
     3.7 -  "HOL-Library.Code_Target_Numeral" "HOL-Library.Old_Recdef"
     3.8 +  "HOL-Library.Code_Target_Numeral"
     3.9  begin
    3.10  
    3.11  section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, <)\<close>\<close>
    3.12 @@ -13,19 +13,25 @@
    3.13    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    3.14    (*********************************************************************************)
    3.15  
    3.16 -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
    3.17 +datatype (plugins del: size) num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
    3.18    | Mul int num
    3.19  
    3.20 -  (* A size for num to make inductive proofs simpler*)
    3.21 -primrec num_size :: "num \<Rightarrow> nat"
    3.22 +instantiation num :: size
    3.23 +begin
    3.24 +
    3.25 +primrec size_num :: "num \<Rightarrow> nat"
    3.26  where
    3.27 -  "num_size (C c) = 1"
    3.28 -| "num_size (Bound n) = 1"
    3.29 -| "num_size (Neg a) = 1 + num_size a"
    3.30 -| "num_size (Add a b) = 1 + num_size a + num_size b"
    3.31 -| "num_size (Sub a b) = 3 + num_size a + num_size b"
    3.32 -| "num_size (Mul c a) = 1 + num_size a"
    3.33 -| "num_size (CN n c a) = 3 + num_size a "
    3.34 +  "size_num (C c) = 1"
    3.35 +| "size_num (Bound n) = 1"
    3.36 +| "size_num (Neg a) = 1 + size_num a"
    3.37 +| "size_num (Add a b) = 1 + size_num a + size_num b"
    3.38 +| "size_num (Sub a b) = 3 + size_num a + size_num b"
    3.39 +| "size_num (Mul c a) = 1 + size_num a"
    3.40 +| "size_num (CN n c a) = 3 + size_num a "
    3.41 +
    3.42 +instance ..
    3.43 +
    3.44 +end
    3.45  
    3.46    (* Semantics of numeral terms (num) *)
    3.47  primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real"
    3.48 @@ -38,26 +44,37 @@
    3.49  | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
    3.50  | "Inum bs (Mul c a) = (real_of_int c) * Inum bs a"
    3.51      (* FORMULAE *)
    3.52 -datatype fm  =
    3.53 +datatype (plugins del: size) fm  =
    3.54    T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num|
    3.55    NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
    3.56  
    3.57 +instantiation fm :: size
    3.58 +begin
    3.59  
    3.60 -  (* A size for fm *)
    3.61 -fun fmsize :: "fm \<Rightarrow> nat"
    3.62 +primrec size_fm :: "fm \<Rightarrow> nat"
    3.63  where
    3.64 -  "fmsize (NOT p) = 1 + fmsize p"
    3.65 -| "fmsize (And p q) = 1 + fmsize p + fmsize q"
    3.66 -| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    3.67 -| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
    3.68 -| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
    3.69 -| "fmsize (E p) = 1 + fmsize p"
    3.70 -| "fmsize (A p) = 4+ fmsize p"
    3.71 -| "fmsize p = 1"
    3.72 -  (* several lemmas about fmsize *)
    3.73 +  "size_fm (NOT p) = 1 + size_fm p"
    3.74 +| "size_fm (And p q) = 1 + size_fm p + size_fm q"
    3.75 +| "size_fm (Or p q) = 1 + size_fm p + size_fm q"
    3.76 +| "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
    3.77 +| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
    3.78 +| "size_fm (E p) = 1 + size_fm p"
    3.79 +| "size_fm (A p) = 4 + size_fm p"
    3.80 +| "size_fm T = 1"
    3.81 +| "size_fm F = 1"
    3.82 +| "size_fm (Lt _) = 1"
    3.83 +| "size_fm (Le _) = 1"
    3.84 +| "size_fm (Gt _) = 1"
    3.85 +| "size_fm (Ge _) = 1"
    3.86 +| "size_fm (Eq _) = 1"
    3.87 +| "size_fm (NEq _) = 1"
    3.88  
    3.89 -lemma fmsize_pos: "fmsize p > 0"
    3.90 -  by (induct p rule: fmsize.induct) simp_all
    3.91 +instance ..
    3.92 +
    3.93 +end
    3.94 +
    3.95 +lemma size_fm_pos [simp]: "size p > 0" for p :: fm
    3.96 +  by (induct p) simp_all
    3.97  
    3.98    (* Semantics of formulae (fm) *)
    3.99  primrec Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool"
   3.100 @@ -646,33 +663,24 @@
   3.101  lemma reducecoeff_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeff t)"
   3.102    using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)
   3.103  
   3.104 -consts numadd:: "num \<times> num \<Rightarrow> num"
   3.105 -recdef numadd "measure (\<lambda>(t,s). size t + size s)"
   3.106 -  "numadd (CN n1 c1 r1,CN n2 c2 r2) =
   3.107 +fun numadd:: "num \<Rightarrow> num \<Rightarrow> num"
   3.108 +where
   3.109 +  "numadd (CN n1 c1 r1) (CN n2 c2 r2) =
   3.110     (if n1 = n2 then
   3.111      (let c = c1 + c2
   3.112 -     in (if c = 0 then numadd(r1,r2) else CN n1 c (numadd (r1, r2))))
   3.113 -    else if n1 \<le> n2 then (CN n1 c1 (numadd (r1,CN n2 c2 r2)))
   3.114 -    else (CN n2 c2 (numadd (CN n1 c1 r1, r2))))"
   3.115 -  "numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))"
   3.116 -  "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))"
   3.117 -  "numadd (C b1, C b2) = C (b1 + b2)"
   3.118 -  "numadd (a,b) = Add a b"
   3.119 +     in (if c = 0 then numadd r1 r2 else CN n1 c (numadd r1 r2)))
   3.120 +    else if n1 \<le> n2 then (CN n1 c1 (numadd r1 (CN n2 c2 r2)))
   3.121 +    else (CN n2 c2 (numadd (CN n1 c1 r1) r2)))"
   3.122 +| "numadd (CN n1 c1 r1) t = CN n1 c1 (numadd r1 t)"
   3.123 +| "numadd t (CN n2 c2 r2) = CN n2 c2 (numadd t r2)"
   3.124 +| "numadd (C b1) (C b2) = C (b1 + b2)"
   3.125 +| "numadd a b = Add a b"
   3.126  
   3.127 -lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
   3.128 -  apply (induct t s rule: numadd.induct)
   3.129 -  apply (simp_all add: Let_def)
   3.130 -  apply (case_tac "c1 + c2 = 0")
   3.131 -  apply (case_tac "n1 \<le> n2")
   3.132 -  apply simp_all
   3.133 -  apply (case_tac "n1 = n2")
   3.134 -  apply (simp_all add: algebra_simps)
   3.135 -  apply (simp only: distrib_right[symmetric])
   3.136 -  apply simp
   3.137 -  done
   3.138 +lemma numadd [simp]: "Inum bs (numadd t s) = Inum bs (Add t s)"
   3.139 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff)
   3.140  
   3.141 -lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
   3.142 -  by (induct t s rule: numadd.induct) (auto simp add: Let_def)
   3.143 +lemma numadd_nb [simp]: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd t s)"
   3.144 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def)
   3.145  
   3.146  fun nummul:: "num \<Rightarrow> int \<Rightarrow> num"
   3.147  where
   3.148 @@ -690,7 +698,7 @@
   3.149    where "numneg t = nummul t (- 1)"
   3.150  
   3.151  definition numsub :: "num \<Rightarrow> num \<Rightarrow> num"
   3.152 -  where "numsub s t = (if s = t then C 0 else numadd (s, numneg t))"
   3.153 +  where "numsub s t = (if s = t then C 0 else numadd s (numneg t))"
   3.154  
   3.155  lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)"
   3.156    using numneg_def by simp
   3.157 @@ -709,10 +717,10 @@
   3.158    "simpnum (C j) = C j"
   3.159  | "simpnum (Bound n) = CN n 1 (C 0)"
   3.160  | "simpnum (Neg t) = numneg (simpnum t)"
   3.161 -| "simpnum (Add t s) = numadd (simpnum t,simpnum s)"
   3.162 +| "simpnum (Add t s) = numadd (simpnum t) (simpnum s)"
   3.163  | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
   3.164  | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul (simpnum t) i)"
   3.165 -| "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0), simpnum t))"
   3.166 +| "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0)) (simpnum t))"
   3.167  
   3.168  lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t"
   3.169    by (induct t) simp_all
   3.170 @@ -726,8 +734,8 @@
   3.171  | "nozerocoeff (CN n c t) = (c \<noteq> 0 \<and> nozerocoeff t)"
   3.172  | "nozerocoeff t = True"
   3.173  
   3.174 -lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd (a,b))"
   3.175 -  by (induct a b rule: numadd.induct) (auto simp add: Let_def)
   3.176 +lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd a b)"
   3.177 +  by (induct a b rule: numadd.induct) (simp_all add: Let_def)
   3.178  
   3.179  lemma nummul_nz : "\<And>i. i\<noteq>0 \<Longrightarrow> nozerocoeff a \<Longrightarrow> nozerocoeff (nummul a i)"
   3.180    by (induct a rule: nummul.induct) (auto simp add: Let_def numadd_nz)
   3.181 @@ -856,7 +864,7 @@
   3.182      proof (cases "?g > 1")
   3.183        case False
   3.184        then show ?thesis
   3.185 -        using assms by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)
   3.186 +        using assms by (auto simp add: Let_def simp_num_pair_def)
   3.187      next
   3.188        case g1: True
   3.189        then have g0: "?g > 0" by simp
   3.190 @@ -868,7 +876,7 @@
   3.191        proof cases
   3.192          case 1
   3.193          then show ?thesis
   3.194 -          using assms g1 by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)
   3.195 +          using assms g1 by (auto simp add: Let_def simp_num_pair_def)
   3.196        next
   3.197          case g'1: 2
   3.198          have gpdg: "?g' dvd ?g" by simp
   3.199 @@ -879,7 +887,7 @@
   3.200            by simp
   3.201          then show ?thesis
   3.202            using assms g1 g'1
   3.203 -          by (auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0)
   3.204 +          by (auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)
   3.205        qed
   3.206      qed
   3.207    qed
   3.208 @@ -985,7 +993,7 @@
   3.209      case 2
   3.210      then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
   3.211    qed
   3.212 -qed (induct p rule: simpfm.induct, simp_all add: conj disj imp iff not)
   3.213 +qed (induct p rule: simpfm.induct, simp_all)
   3.214  
   3.215  
   3.216  lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"
   3.217 @@ -1019,7 +1027,7 @@
   3.218    then have nb: "numbound0 a" by simp
   3.219    then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   3.220    then show ?case by (cases "simpnum a") (auto simp add: Let_def)
   3.221 -qed (auto simp add: disj_def imp_def iff_def conj_def not_bn)
   3.222 +qed (auto simp add: disj_def imp_def iff_def conj_def)
   3.223  
   3.224  lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
   3.225    apply (induct p rule: simpfm.induct)
   3.226 @@ -1027,38 +1035,37 @@
   3.227    apply (case_tac "simpnum a", auto)+
   3.228    done
   3.229  
   3.230 -consts prep :: "fm \<Rightarrow> fm"
   3.231 -recdef prep "measure fmsize"
   3.232 +fun prep :: "fm \<Rightarrow> fm"
   3.233 +where
   3.234    "prep (E T) = T"
   3.235 -  "prep (E F) = F"
   3.236 -  "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
   3.237 -  "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
   3.238 -  "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
   3.239 -  "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
   3.240 -  "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
   3.241 -  "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
   3.242 -  "prep (E p) = E (prep p)"
   3.243 -  "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
   3.244 -  "prep (A p) = prep (NOT (E (NOT p)))"
   3.245 -  "prep (NOT (NOT p)) = prep p"
   3.246 -  "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
   3.247 -  "prep (NOT (A p)) = prep (E (NOT p))"
   3.248 -  "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
   3.249 -  "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
   3.250 -  "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
   3.251 -  "prep (NOT p) = not (prep p)"
   3.252 -  "prep (Or p q) = disj (prep p) (prep q)"
   3.253 -  "prep (And p q) = conj (prep p) (prep q)"
   3.254 -  "prep (Imp p q) = prep (Or (NOT p) q)"
   3.255 -  "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   3.256 -  "prep p = p"
   3.257 -  (hints simp add: fmsize_pos)
   3.258 +| "prep (E F) = F"
   3.259 +| "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
   3.260 +| "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
   3.261 +| "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
   3.262 +| "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
   3.263 +| "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
   3.264 +| "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
   3.265 +| "prep (E p) = E (prep p)"
   3.266 +| "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
   3.267 +| "prep (A p) = prep (NOT (E (NOT p)))"
   3.268 +| "prep (NOT (NOT p)) = prep p"
   3.269 +| "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
   3.270 +| "prep (NOT (A p)) = prep (E (NOT p))"
   3.271 +| "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
   3.272 +| "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
   3.273 +| "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
   3.274 +| "prep (NOT p) = not (prep p)"
   3.275 +| "prep (Or p q) = disj (prep p) (prep q)"
   3.276 +| "prep (And p q) = conj (prep p) (prep q)"
   3.277 +| "prep (Imp p q) = prep (Or (NOT p) q)"
   3.278 +| "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   3.279 +| "prep p = p"
   3.280  
   3.281  lemma prep: "\<And>bs. Ifm bs (prep p) = Ifm bs p"
   3.282    by (induct p rule: prep.induct) auto
   3.283  
   3.284    (* Generic quantifier elimination *)
   3.285 -function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   3.286 +fun qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   3.287  where
   3.288    "qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))"
   3.289  | "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
   3.290 @@ -1068,16 +1075,13 @@
   3.291  | "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
   3.292  | "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
   3.293  | "qelim p = (\<lambda>y. simpfm p)"
   3.294 -  by pat_completeness auto
   3.295 -termination qelim by (relation "measure fmsize") simp_all
   3.296  
   3.297  lemma qelim_ci:
   3.298    assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"
   3.299    shows "\<And>bs. qfree (qelim p qe) \<and> (Ifm bs (qelim p qe) = Ifm bs p)"
   3.300    using qe_inv DJ_qe[OF qe_inv]
   3.301    by (induct p rule: qelim.induct)
   3.302 -    (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
   3.303 -      simpfm simpfm_qf simp del: simpfm.simps)
   3.304 +    (auto simp add: simpfm simpfm_qf simp del: simpfm.simps)
   3.305  
   3.306  fun minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
   3.307  where
   3.308 @@ -1116,7 +1120,7 @@
   3.309  | "isrlfm p = (isatom p \<and> (bound0 p))"
   3.310  
   3.311    (* splits the bounded from the unbounded part*)
   3.312 -function (sequential) rsplit0 :: "num \<Rightarrow> int \<times> num"
   3.313 +fun rsplit0 :: "num \<Rightarrow> int \<times> num"
   3.314  where
   3.315    "rsplit0 (Bound 0) = (1,C 0)"
   3.316  | "rsplit0 (Add a b) = (let (ca,ta) = rsplit0 a; (cb,tb) = rsplit0 b in (ca + cb, Add ta tb))"
   3.317 @@ -1126,8 +1130,6 @@
   3.318  | "rsplit0 (CN 0 c a) = (let (ca,ta) = rsplit0 a in (c + ca, ta))"
   3.319  | "rsplit0 (CN n c a) = (let (ca,ta) = rsplit0 a in (ca, CN n c ta))"
   3.320  | "rsplit0 t = (0,t)"
   3.321 -  by pat_completeness auto
   3.322 -termination rsplit0 by (relation "measure num_size") simp_all
   3.323  
   3.324  lemma rsplit0: "Inum bs ((case_prod (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))"
   3.325  proof (induct t rule: rsplit0.induct)
   3.326 @@ -1222,39 +1224,38 @@
   3.327  lemma disj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (disj p q)"
   3.328    by (auto simp add: disj_def)
   3.329  
   3.330 -consts rlfm :: "fm \<Rightarrow> fm"
   3.331 -recdef rlfm "measure fmsize"
   3.332 +fun rlfm :: "fm \<Rightarrow> fm"
   3.333 +where
   3.334    "rlfm (And p q) = conj (rlfm p) (rlfm q)"
   3.335 -  "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
   3.336 -  "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
   3.337 -  "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))"
   3.338 -  "rlfm (Lt a) = case_prod lt (rsplit0 a)"
   3.339 -  "rlfm (Le a) = case_prod le (rsplit0 a)"
   3.340 -  "rlfm (Gt a) = case_prod gt (rsplit0 a)"
   3.341 -  "rlfm (Ge a) = case_prod ge (rsplit0 a)"
   3.342 -  "rlfm (Eq a) = case_prod eq (rsplit0 a)"
   3.343 -  "rlfm (NEq a) = case_prod neq (rsplit0 a)"
   3.344 -  "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
   3.345 -  "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
   3.346 -  "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
   3.347 -  "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
   3.348 -  "rlfm (NOT (NOT p)) = rlfm p"
   3.349 -  "rlfm (NOT T) = F"
   3.350 -  "rlfm (NOT F) = T"
   3.351 -  "rlfm (NOT (Lt a)) = rlfm (Ge a)"
   3.352 -  "rlfm (NOT (Le a)) = rlfm (Gt a)"
   3.353 -  "rlfm (NOT (Gt a)) = rlfm (Le a)"
   3.354 -  "rlfm (NOT (Ge a)) = rlfm (Lt a)"
   3.355 -  "rlfm (NOT (Eq a)) = rlfm (NEq a)"
   3.356 -  "rlfm (NOT (NEq a)) = rlfm (Eq a)"
   3.357 -  "rlfm p = p"
   3.358 -  (hints simp add: fmsize_pos)
   3.359 +| "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
   3.360 +| "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
   3.361 +| "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))"
   3.362 +| "rlfm (Lt a) = case_prod lt (rsplit0 a)"
   3.363 +| "rlfm (Le a) = case_prod le (rsplit0 a)"
   3.364 +| "rlfm (Gt a) = case_prod gt (rsplit0 a)"
   3.365 +| "rlfm (Ge a) = case_prod ge (rsplit0 a)"
   3.366 +| "rlfm (Eq a) = case_prod eq (rsplit0 a)"
   3.367 +| "rlfm (NEq a) = case_prod neq (rsplit0 a)"
   3.368 +| "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
   3.369 +| "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
   3.370 +| "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
   3.371 +| "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
   3.372 +| "rlfm (NOT (NOT p)) = rlfm p"
   3.373 +| "rlfm (NOT T) = F"
   3.374 +| "rlfm (NOT F) = T"
   3.375 +| "rlfm (NOT (Lt a)) = rlfm (Ge a)"
   3.376 +| "rlfm (NOT (Le a)) = rlfm (Gt a)"
   3.377 +| "rlfm (NOT (Gt a)) = rlfm (Le a)"
   3.378 +| "rlfm (NOT (Ge a)) = rlfm (Lt a)"
   3.379 +| "rlfm (NOT (Eq a)) = rlfm (NEq a)"
   3.380 +| "rlfm (NOT (NEq a)) = rlfm (Eq a)"
   3.381 +| "rlfm p = p"
   3.382  
   3.383  lemma rlfm_I:
   3.384    assumes qfp: "qfree p"
   3.385    shows "(Ifm bs (rlfm p) = Ifm bs p) \<and> isrlfm (rlfm p)"
   3.386    using qfp
   3.387 -  by (induct p rule: rlfm.induct) (auto simp add: lt le gt ge eq neq conj disj conj_lin disj_lin)
   3.388 +  by (induct p rule: rlfm.induct) (auto simp add: lt le gt ge eq neq conj_lin disj_lin)
   3.389  
   3.390      (* Operations needed for Ferrante and Rackoff *)
   3.391  lemma rminusinf_inf:
   3.392 @@ -1555,29 +1556,29 @@
   3.393    ultimately show ?thesis using z_def by auto
   3.394  qed
   3.395  
   3.396 -consts
   3.397 -  uset:: "fm \<Rightarrow> (num \<times> int) list"
   3.398 -  usubst :: "fm \<Rightarrow> (num \<times> int) \<Rightarrow> fm "
   3.399 -recdef uset "measure size"
   3.400 +fun uset :: "fm \<Rightarrow> (num \<times> int) list"
   3.401 +where
   3.402    "uset (And p q) = (uset p @ uset q)"
   3.403 -  "uset (Or p q) = (uset p @ uset q)"
   3.404 -  "uset (Eq  (CN 0 c e)) = [(Neg e,c)]"
   3.405 -  "uset (NEq (CN 0 c e)) = [(Neg e,c)]"
   3.406 -  "uset (Lt  (CN 0 c e)) = [(Neg e,c)]"
   3.407 -  "uset (Le  (CN 0 c e)) = [(Neg e,c)]"
   3.408 -  "uset (Gt  (CN 0 c e)) = [(Neg e,c)]"
   3.409 -  "uset (Ge  (CN 0 c e)) = [(Neg e,c)]"
   3.410 -  "uset p = []"
   3.411 -recdef usubst "measure size"
   3.412 +| "uset (Or p q) = (uset p @ uset q)"
   3.413 +| "uset (Eq  (CN 0 c e)) = [(Neg e,c)]"
   3.414 +| "uset (NEq (CN 0 c e)) = [(Neg e,c)]"
   3.415 +| "uset (Lt  (CN 0 c e)) = [(Neg e,c)]"
   3.416 +| "uset (Le  (CN 0 c e)) = [(Neg e,c)]"
   3.417 +| "uset (Gt  (CN 0 c e)) = [(Neg e,c)]"
   3.418 +| "uset (Ge  (CN 0 c e)) = [(Neg e,c)]"
   3.419 +| "uset p = []"
   3.420 +
   3.421 +fun usubst :: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm"
   3.422 +where
   3.423    "usubst (And p q) = (\<lambda>(t,n). And (usubst p (t,n)) (usubst q (t,n)))"
   3.424 -  "usubst (Or p q) = (\<lambda>(t,n). Or (usubst p (t,n)) (usubst q (t,n)))"
   3.425 -  "usubst (Eq (CN 0 c e)) = (\<lambda>(t,n). Eq (Add (Mul c t) (Mul n e)))"
   3.426 -  "usubst (NEq (CN 0 c e)) = (\<lambda>(t,n). NEq (Add (Mul c t) (Mul n e)))"
   3.427 -  "usubst (Lt (CN 0 c e)) = (\<lambda>(t,n). Lt (Add (Mul c t) (Mul n e)))"
   3.428 -  "usubst (Le (CN 0 c e)) = (\<lambda>(t,n). Le (Add (Mul c t) (Mul n e)))"
   3.429 -  "usubst (Gt (CN 0 c e)) = (\<lambda>(t,n). Gt (Add (Mul c t) (Mul n e)))"
   3.430 -  "usubst (Ge (CN 0 c e)) = (\<lambda>(t,n). Ge (Add (Mul c t) (Mul n e)))"
   3.431 -  "usubst p = (\<lambda>(t, n). p)"
   3.432 +| "usubst (Or p q) = (\<lambda>(t,n). Or (usubst p (t,n)) (usubst q (t,n)))"
   3.433 +| "usubst (Eq (CN 0 c e)) = (\<lambda>(t,n). Eq (Add (Mul c t) (Mul n e)))"
   3.434 +| "usubst (NEq (CN 0 c e)) = (\<lambda>(t,n). NEq (Add (Mul c t) (Mul n e)))"
   3.435 +| "usubst (Lt (CN 0 c e)) = (\<lambda>(t,n). Lt (Add (Mul c t) (Mul n e)))"
   3.436 +| "usubst (Le (CN 0 c e)) = (\<lambda>(t,n). Le (Add (Mul c t) (Mul n e)))"
   3.437 +| "usubst (Gt (CN 0 c e)) = (\<lambda>(t,n). Gt (Add (Mul c t) (Mul n e)))"
   3.438 +| "usubst (Ge (CN 0 c e)) = (\<lambda>(t,n). Ge (Add (Mul c t) (Mul n e)))"
   3.439 +| "usubst p = (\<lambda>(t, n). p)"
   3.440  
   3.441  lemma usubst_I:
   3.442    assumes lp: "isrlfm p"
     4.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun Oct 08 22:28:21 2017 +0200
     4.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun Oct 08 22:28:21 2017 +0200
     4.3 @@ -84,23 +84,32 @@
     4.4    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
     4.5    (*********************************************************************************)
     4.6  
     4.7 -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
     4.8 -  | Mul int num | Floor num| CF int num num
     4.9 -
    4.10 -  (* A size for num to make inductive proofs simpler*)
    4.11 -primrec num_size :: "num \<Rightarrow> nat" where
    4.12 - "num_size (C c) = 1"
    4.13 -| "num_size (Bound n) = 1"
    4.14 -| "num_size (Neg a) = 1 + num_size a"
    4.15 -| "num_size (Add a b) = 1 + num_size a + num_size b"
    4.16 -| "num_size (Sub a b) = 3 + num_size a + num_size b"
    4.17 -| "num_size (CN n c a) = 4 + num_size a "
    4.18 -| "num_size (CF c a b) = 4 + num_size a + num_size b"
    4.19 -| "num_size (Mul c a) = 1 + num_size a"
    4.20 -| "num_size (Floor a) = 1 + num_size a"
    4.21 +datatype (plugins del: size) num = C int | Bound nat | CN nat int num
    4.22 +  | Neg num | Add num num | Sub num num
    4.23 +  | Mul int num | Floor num | CF int num num
    4.24 +
    4.25 +instantiation num :: size
    4.26 +begin
    4.27 +
    4.28 +primrec size_num :: "num \<Rightarrow> nat"
    4.29 +where
    4.30 +  "size_num (C c) = 1"
    4.31 +| "size_num (Bound n) = 1"
    4.32 +| "size_num (Neg a) = 1 + size_num a"
    4.33 +| "size_num (Add a b) = 1 + size_num a + size_num b"
    4.34 +| "size_num (Sub a b) = 3 + size_num a + size_num b"
    4.35 +| "size_num (CN n c a) = 4 + size_num a "
    4.36 +| "size_num (CF c a b) = 4 + size_num a + size_num b"
    4.37 +| "size_num (Mul c a) = 1 + size_num a"
    4.38 +| "size_num (Floor a) = 1 + size_num a"
    4.39 +
    4.40 +instance ..
    4.41 +
    4.42 +end
    4.43  
    4.44    (* Semantics of numeral terms (num) *)
    4.45 -primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real" where
    4.46 +primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real"
    4.47 +where
    4.48    "Inum bs (C c) = (real_of_int c)"
    4.49  | "Inum bs (Bound n) = bs!n"
    4.50  | "Inum bs (CN n c a) = (real_of_int c) * (bs!n) + (Inum bs a)"
    4.51 @@ -169,48 +178,64 @@
    4.52  
    4.53  
    4.54      (* FORMULAE *)
    4.55 -datatype fm  =
    4.56 -  T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
    4.57 -  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
    4.58 -
    4.59 -
    4.60 -  (* A size for fm *)
    4.61 -fun fmsize :: "fm \<Rightarrow> nat" where
    4.62 - "fmsize (NOT p) = 1 + fmsize p"
    4.63 -| "fmsize (And p q) = 1 + fmsize p + fmsize q"
    4.64 -| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    4.65 -| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
    4.66 -| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
    4.67 -| "fmsize (E p) = 1 + fmsize p"
    4.68 -| "fmsize (A p) = 4+ fmsize p"
    4.69 -| "fmsize (Dvd i t) = 2"
    4.70 -| "fmsize (NDvd i t) = 2"
    4.71 -| "fmsize p = 1"
    4.72 -  (* several lemmas about fmsize *)
    4.73 -lemma fmsize_pos: "fmsize p > 0"
    4.74 -  by (induct p rule: fmsize.induct) simp_all
    4.75 +datatype (plugins del: size) fm =
    4.76 +  T | F | Lt num | Le num | Gt num | Ge num | Eq num | NEq num |
    4.77 +  Dvd int num | NDvd int num |
    4.78 +  NOT fm | And fm fm |  Or fm fm | Imp fm fm | Iff fm fm | E fm | A fm
    4.79 +
    4.80 +instantiation fm :: size
    4.81 +begin
    4.82 +
    4.83 +primrec size_fm :: "fm \<Rightarrow> nat"
    4.84 +where
    4.85 +  "size_fm (NOT p) = 1 + size_fm p"
    4.86 +| "size_fm (And p q) = 1 + size_fm p + size_fm q"
    4.87 +| "size_fm (Or p q) = 1 + size_fm p + size_fm q"
    4.88 +| "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
    4.89 +| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
    4.90 +| "size_fm (E p) = 1 + size_fm p"
    4.91 +| "size_fm (A p) = 4 + size_fm p"
    4.92 +| "size_fm (Dvd i t) = 2"
    4.93 +| "size_fm (NDvd i t) = 2"
    4.94 +| "size_fm T = 1"
    4.95 +| "size_fm F = 1"
    4.96 +| "size_fm (Lt _) = 1"
    4.97 +| "size_fm (Le _) = 1"
    4.98 +| "size_fm (Gt _) = 1"
    4.99 +| "size_fm (Ge _) = 1"
   4.100 +| "size_fm (Eq _) = 1"
   4.101 +| "size_fm (NEq _) = 1"
   4.102 +
   4.103 +instance ..
   4.104 +
   4.105 +end
   4.106 +
   4.107 +lemma size_fm_pos [simp]: "size p > 0" for p :: fm
   4.108 +  by (induct p) simp_all
   4.109  
   4.110    (* Semantics of formulae (fm) *)
   4.111 -primrec Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool" where
   4.112 -  "Ifm bs T = True"
   4.113 -| "Ifm bs F = False"
   4.114 -| "Ifm bs (Lt a) = (Inum bs a < 0)"
   4.115 -| "Ifm bs (Gt a) = (Inum bs a > 0)"
   4.116 -| "Ifm bs (Le a) = (Inum bs a \<le> 0)"
   4.117 -| "Ifm bs (Ge a) = (Inum bs a \<ge> 0)"
   4.118 -| "Ifm bs (Eq a) = (Inum bs a = 0)"
   4.119 -| "Ifm bs (NEq a) = (Inum bs a \<noteq> 0)"
   4.120 -| "Ifm bs (Dvd i b) = (real_of_int i rdvd Inum bs b)"
   4.121 -| "Ifm bs (NDvd i b) = (\<not>(real_of_int i rdvd Inum bs b))"
   4.122 -| "Ifm bs (NOT p) = (\<not> (Ifm bs p))"
   4.123 -| "Ifm bs (And p q) = (Ifm bs p \<and> Ifm bs q)"
   4.124 -| "Ifm bs (Or p q) = (Ifm bs p \<or> Ifm bs q)"
   4.125 -| "Ifm bs (Imp p q) = ((Ifm bs p) \<longrightarrow> (Ifm bs q))"
   4.126 -| "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)"
   4.127 -| "Ifm bs (E p) = (\<exists> x. Ifm (x#bs) p)"
   4.128 -| "Ifm bs (A p) = (\<forall> x. Ifm (x#bs) p)"
   4.129 -
   4.130 -function (sequential) prep :: "fm \<Rightarrow> fm" where
   4.131 +primrec Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool"
   4.132 +where
   4.133 +  "Ifm bs T \<longleftrightarrow> True"
   4.134 +| "Ifm bs F \<longleftrightarrow> False"
   4.135 +| "Ifm bs (Lt a) \<longleftrightarrow> Inum bs a < 0"
   4.136 +| "Ifm bs (Gt a) \<longleftrightarrow> Inum bs a > 0"
   4.137 +| "Ifm bs (Le a) \<longleftrightarrow> Inum bs a \<le> 0"
   4.138 +| "Ifm bs (Ge a) \<longleftrightarrow> Inum bs a \<ge> 0"
   4.139 +| "Ifm bs (Eq a) \<longleftrightarrow> Inum bs a = 0"
   4.140 +| "Ifm bs (NEq a) \<longleftrightarrow> Inum bs a \<noteq> 0"
   4.141 +| "Ifm bs (Dvd i b) \<longleftrightarrow> real_of_int i rdvd Inum bs b"
   4.142 +| "Ifm bs (NDvd i b) \<longleftrightarrow> \<not> (real_of_int i rdvd Inum bs b)"
   4.143 +| "Ifm bs (NOT p) \<longleftrightarrow> \<not> (Ifm bs p)"
   4.144 +| "Ifm bs (And p q) \<longleftrightarrow> Ifm bs p \<and> Ifm bs q"
   4.145 +| "Ifm bs (Or p q) \<longleftrightarrow> Ifm bs p \<or> Ifm bs q"
   4.146 +| "Ifm bs (Imp p q) \<longleftrightarrow> (Ifm bs p \<longrightarrow> Ifm bs q)"
   4.147 +| "Ifm bs (Iff p q) \<longleftrightarrow> (Ifm bs p \<longleftrightarrow> Ifm bs q)"
   4.148 +| "Ifm bs (E p) \<longleftrightarrow> (\<exists>x. Ifm (x # bs) p)"
   4.149 +| "Ifm bs (A p) \<longleftrightarrow> (\<forall>x. Ifm (x # bs) p)"
   4.150 +
   4.151 +fun prep :: "fm \<Rightarrow> fm"
   4.152 +where
   4.153    "prep (E T) = T"
   4.154  | "prep (E F) = F"
   4.155  | "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
   4.156 @@ -234,35 +259,35 @@
   4.157  | "prep (Imp p q) = prep (Or (NOT p) q)"
   4.158  | "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   4.159  | "prep p = p"
   4.160 -  by pat_completeness simp_all
   4.161 -termination by (relation "measure fmsize") (simp_all add: fmsize_pos)
   4.162  
   4.163  lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
   4.164    by (induct p rule: prep.induct) auto
   4.165  
   4.166  
   4.167    (* Quantifier freeness *)
   4.168 -fun qfree:: "fm \<Rightarrow> bool" where
   4.169 +fun qfree:: "fm \<Rightarrow> bool"
   4.170 +where
   4.171    "qfree (E p) = False"
   4.172 -  | "qfree (A p) = False"
   4.173 -  | "qfree (NOT p) = qfree p"
   4.174 -  | "qfree (And p q) = (qfree p \<and> qfree q)"
   4.175 -  | "qfree (Or  p q) = (qfree p \<and> qfree q)"
   4.176 -  | "qfree (Imp p q) = (qfree p \<and> qfree q)"
   4.177 -  | "qfree (Iff p q) = (qfree p \<and> qfree q)"
   4.178 -  | "qfree p = True"
   4.179 +| "qfree (A p) = False"
   4.180 +| "qfree (NOT p) = qfree p"
   4.181 +| "qfree (And p q) = (qfree p \<and> qfree q)"
   4.182 +| "qfree (Or  p q) = (qfree p \<and> qfree q)"
   4.183 +| "qfree (Imp p q) = (qfree p \<and> qfree q)"
   4.184 +| "qfree (Iff p q) = (qfree p \<and> qfree q)"
   4.185 +| "qfree p = True"
   4.186  
   4.187    (* Boundedness and substitution *)
   4.188 -primrec numbound0 :: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) where
   4.189 +primrec numbound0 :: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)
   4.190 +where
   4.191    "numbound0 (C c) = True"
   4.192 -  | "numbound0 (Bound n) = (n>0)"
   4.193 -  | "numbound0 (CN n i a) = (n > 0 \<and> numbound0 a)"
   4.194 -  | "numbound0 (Neg a) = numbound0 a"
   4.195 -  | "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
   4.196 -  | "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
   4.197 -  | "numbound0 (Mul i a) = numbound0 a"
   4.198 -  | "numbound0 (Floor a) = numbound0 a"
   4.199 -  | "numbound0 (CF c a b) = (numbound0 a \<and> numbound0 b)"
   4.200 +| "numbound0 (Bound n) = (n>0)"
   4.201 +| "numbound0 (CN n i a) = (n > 0 \<and> numbound0 a)"
   4.202 +| "numbound0 (Neg a) = numbound0 a"
   4.203 +| "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
   4.204 +| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
   4.205 +| "numbound0 (Mul i a) = numbound0 a"
   4.206 +| "numbound0 (Floor a) = numbound0 a"
   4.207 +| "numbound0 (CF c a b) = (numbound0 a \<and> numbound0 b)"
   4.208  
   4.209  lemma numbound0_I:
   4.210    assumes nb: "numbound0 a"
   4.211 @@ -280,24 +305,25 @@
   4.212      by (simp add: isint_def)
   4.213  qed
   4.214  
   4.215 -primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
   4.216 +primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
   4.217 +where
   4.218    "bound0 T = True"
   4.219 -  | "bound0 F = True"
   4.220 -  | "bound0 (Lt a) = numbound0 a"
   4.221 -  | "bound0 (Le a) = numbound0 a"
   4.222 -  | "bound0 (Gt a) = numbound0 a"
   4.223 -  | "bound0 (Ge a) = numbound0 a"
   4.224 -  | "bound0 (Eq a) = numbound0 a"
   4.225 -  | "bound0 (NEq a) = numbound0 a"
   4.226 -  | "bound0 (Dvd i a) = numbound0 a"
   4.227 -  | "bound0 (NDvd i a) = numbound0 a"
   4.228 -  | "bound0 (NOT p) = bound0 p"
   4.229 -  | "bound0 (And p q) = (bound0 p \<and> bound0 q)"
   4.230 -  | "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
   4.231 -  | "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
   4.232 -  | "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
   4.233 -  | "bound0 (E p) = False"
   4.234 -  | "bound0 (A p) = False"
   4.235 +| "bound0 F = True"
   4.236 +| "bound0 (Lt a) = numbound0 a"
   4.237 +| "bound0 (Le a) = numbound0 a"
   4.238 +| "bound0 (Gt a) = numbound0 a"
   4.239 +| "bound0 (Ge a) = numbound0 a"
   4.240 +| "bound0 (Eq a) = numbound0 a"
   4.241 +| "bound0 (NEq a) = numbound0 a"
   4.242 +| "bound0 (Dvd i a) = numbound0 a"
   4.243 +| "bound0 (NDvd i a) = numbound0 a"
   4.244 +| "bound0 (NOT p) = bound0 p"
   4.245 +| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
   4.246 +| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
   4.247 +| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
   4.248 +| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
   4.249 +| "bound0 (E p) = False"
   4.250 +| "bound0 (A p) = False"
   4.251  
   4.252  lemma bound0_I:
   4.253    assumes bp: "bound0 p"
   4.254 @@ -305,44 +331,47 @@
   4.255    using bp numbound0_I [where b="b" and bs="bs" and b'="b'"]
   4.256    by (induct p) auto
   4.257  
   4.258 -primrec numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *) where
   4.259 +primrec numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *)
   4.260 +where
   4.261    "numsubst0 t (C c) = (C c)"
   4.262 -  | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   4.263 -  | "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))"
   4.264 -  | "numsubst0 t (CF i a b) = CF i (numsubst0 t a) (numsubst0 t b)"
   4.265 -  | "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
   4.266 -  | "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
   4.267 -  | "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)"
   4.268 -  | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
   4.269 -  | "numsubst0 t (Floor a) = Floor (numsubst0 t a)"
   4.270 +| "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   4.271 +| "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))"
   4.272 +| "numsubst0 t (CF i a b) = CF i (numsubst0 t a) (numsubst0 t b)"
   4.273 +| "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
   4.274 +| "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
   4.275 +| "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)"
   4.276 +| "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
   4.277 +| "numsubst0 t (Floor a) = Floor (numsubst0 t a)"
   4.278  
   4.279  lemma numsubst0_I:
   4.280    shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
   4.281    by (induct t) simp_all
   4.282  
   4.283 -primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
   4.284 +primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *)
   4.285 +where
   4.286    "subst0 t T = T"
   4.287 -  | "subst0 t F = F"
   4.288 -  | "subst0 t (Lt a) = Lt (numsubst0 t a)"
   4.289 -  | "subst0 t (Le a) = Le (numsubst0 t a)"
   4.290 -  | "subst0 t (Gt a) = Gt (numsubst0 t a)"
   4.291 -  | "subst0 t (Ge a) = Ge (numsubst0 t a)"
   4.292 -  | "subst0 t (Eq a) = Eq (numsubst0 t a)"
   4.293 -  | "subst0 t (NEq a) = NEq (numsubst0 t a)"
   4.294 -  | "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
   4.295 -  | "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
   4.296 -  | "subst0 t (NOT p) = NOT (subst0 t p)"
   4.297 -  | "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   4.298 -  | "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   4.299 -  | "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
   4.300 -  | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   4.301 +| "subst0 t F = F"
   4.302 +| "subst0 t (Lt a) = Lt (numsubst0 t a)"
   4.303 +| "subst0 t (Le a) = Le (numsubst0 t a)"
   4.304 +| "subst0 t (Gt a) = Gt (numsubst0 t a)"
   4.305 +| "subst0 t (Ge a) = Ge (numsubst0 t a)"
   4.306 +| "subst0 t (Eq a) = Eq (numsubst0 t a)"
   4.307 +| "subst0 t (NEq a) = NEq (numsubst0 t a)"
   4.308 +| "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
   4.309 +| "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
   4.310 +| "subst0 t (NOT p) = NOT (subst0 t p)"
   4.311 +| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   4.312 +| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   4.313 +| "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
   4.314 +| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   4.315  
   4.316  lemma subst0_I: assumes qfp: "qfree p"
   4.317    shows "Ifm (b#bs) (subst0 a p) = Ifm ((Inum (b#bs) a)#bs) p"
   4.318    using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
   4.319    by (induct p) simp_all
   4.320  
   4.321 -fun decrnum:: "num \<Rightarrow> num" where
   4.322 +fun decrnum:: "num \<Rightarrow> num"
   4.323 +where
   4.324    "decrnum (Bound n) = Bound (n - 1)"
   4.325  | "decrnum (Neg a) = Neg (decrnum a)"
   4.326  | "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
   4.327 @@ -353,7 +382,8 @@
   4.328  | "decrnum (CF c a b) = CF c (decrnum a) (decrnum b)"
   4.329  | "decrnum a = a"
   4.330  
   4.331 -fun decr :: "fm \<Rightarrow> fm" where
   4.332 +fun decr :: "fm \<Rightarrow> fm"
   4.333 +where
   4.334    "decr (Lt a) = Lt (decrnum a)"
   4.335  | "decr (Le a) = Le (decrnum a)"
   4.336  | "decr (Gt a) = Gt (decrnum a)"
   4.337 @@ -380,7 +410,8 @@
   4.338  lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
   4.339    by (induct p) simp_all
   4.340  
   4.341 -fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where
   4.342 +fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
   4.343 +where
   4.344    "isatom T = True"
   4.345  | "isatom F = True"
   4.346  | "isatom (Lt a) = True"
   4.347 @@ -441,12 +472,14 @@
   4.348    apply auto
   4.349    done
   4.350  
   4.351 -fun disjuncts :: "fm \<Rightarrow> fm list" where
   4.352 +fun disjuncts :: "fm \<Rightarrow> fm list"
   4.353 +where
   4.354    "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
   4.355  | "disjuncts F = []"
   4.356  | "disjuncts p = [p]"
   4.357  
   4.358 -fun conjuncts :: "fm \<Rightarrow> fm list" where
   4.359 +fun conjuncts :: "fm \<Rightarrow> fm list"
   4.360 +where
   4.361    "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)"
   4.362  | "conjuncts T = []"
   4.363  | "conjuncts p = [p]"
   4.364 @@ -511,7 +544,8 @@
   4.365    (* Simplification *)
   4.366  
   4.367    (* Algebraic simplifications for nums *)
   4.368 -fun bnds:: "num \<Rightarrow> nat list" where
   4.369 +fun bnds:: "num \<Rightarrow> nat list"
   4.370 +where
   4.371    "bnds (Bound n) = [n]"
   4.372  | "bnds (CN n c a) = n#(bnds a)"
   4.373  | "bnds (Neg a) = bnds a"
   4.374 @@ -521,14 +555,17 @@
   4.375  | "bnds (Floor a) = bnds a"
   4.376  | "bnds (CF c a b) = (bnds a)@(bnds b)"
   4.377  | "bnds a = []"
   4.378 -fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool" where
   4.379 +
   4.380 +fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool"
   4.381 +where
   4.382    "lex_ns [] ms = True"
   4.383  | "lex_ns ns [] = False"
   4.384  | "lex_ns (n#ns) (m#ms) = (n<m \<or> ((n = m) \<and> lex_ns ns ms)) "
   4.385  definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool" where
   4.386    "lex_bnd t s \<equiv> lex_ns (bnds t) (bnds s)"
   4.387  
   4.388 -fun maxcoeff:: "num \<Rightarrow> int" where
   4.389 +fun maxcoeff:: "num \<Rightarrow> int"
   4.390 +where
   4.391    "maxcoeff (C i) = \<bar>i\<bar>"
   4.392  | "maxcoeff (CN n c t) = max \<bar>c\<bar> (maxcoeff t)"
   4.393  | "maxcoeff (CF c t s) = max \<bar>c\<bar> (maxcoeff s)"
   4.394 @@ -537,7 +574,8 @@
   4.395  lemma maxcoeff_pos: "maxcoeff t \<ge> 0"
   4.396    by (induct t rule: maxcoeff.induct) auto
   4.397  
   4.398 -fun numgcdh:: "num \<Rightarrow> int \<Rightarrow> int" where
   4.399 +fun numgcdh:: "num \<Rightarrow> int \<Rightarrow> int"
   4.400 +where
   4.401    "numgcdh (C i) = (\<lambda>g. gcd i g)"
   4.402  | "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"
   4.403  | "numgcdh (CF c s t) = (\<lambda>g. gcd c (numgcdh t g))"
   4.404 @@ -546,7 +584,8 @@
   4.405  definition numgcd :: "num \<Rightarrow> int"
   4.406    where "numgcd t = numgcdh t (maxcoeff t)"
   4.407  
   4.408 -fun reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num" where
   4.409 +fun reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num"
   4.410 +where
   4.411    "reducecoeffh (C i) = (\<lambda> g. C (i div g))"
   4.412  | "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))"
   4.413  | "reducecoeffh (CF c s t) = (\<lambda> g. CF (c div g)  s (reducecoeffh t g))"
   4.414 @@ -558,7 +597,8 @@
   4.415      (let g = numgcd t in
   4.416       if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)"
   4.417  
   4.418 -fun dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
   4.419 +fun dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
   4.420 +where
   4.421    "dvdnumcoeff (C i) = (\<lambda> g. g dvd i)"
   4.422  | "dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"
   4.423  | "dvdnumcoeff (CF c s t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"
   4.424 @@ -602,7 +642,8 @@
   4.425    from assms 3 show ?case by (simp add: real_of_int_div[OF gd] algebra_simps)
   4.426  qed (auto simp add: numgcd_def gp)
   4.427  
   4.428 -fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
   4.429 +fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
   4.430 +where
   4.431    "ismaxcoeff (C i) = (\<lambda> x. \<bar>i\<bar> \<le> x)"
   4.432  | "ismaxcoeff (CN n c t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> (ismaxcoeff t x))"
   4.433  | "ismaxcoeff (CF c s t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> (ismaxcoeff t x))"
   4.434 @@ -711,7 +752,7 @@
   4.435    using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)
   4.436  
   4.437  consts numadd:: "num \<times> num \<Rightarrow> num"
   4.438 -recdef numadd "measure (\<lambda> (t,s). size t + size s)"
   4.439 +recdef numadd "measure (\<lambda>(t, s). size t + size s)"
   4.440    "numadd (CN n1 c1 r1,CN n2 c2 r2) =
   4.441    (if n1=n2 then
   4.442    (let c = c1 + c2
   4.443 @@ -730,22 +771,14 @@
   4.444    "numadd (C b1, C b2) = C (b1+b2)"
   4.445    "numadd (a,b) = Add a b"
   4.446  
   4.447 -lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
   4.448 -apply (induct t s rule: numadd.induct, simp_all add: Let_def)
   4.449 - apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
   4.450 -  apply (case_tac "n1 = n2", simp_all add: algebra_simps)
   4.451 -  apply (simp only: distrib_right[symmetric])
   4.452 - apply simp
   4.453 -apply (case_tac "lex_bnd t1 t2", simp_all)
   4.454 - apply (case_tac "c1+c2 = 0")
   4.455 -  apply (case_tac "t1 = t2")
   4.456 -   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)
   4.457 -  done
   4.458 -
   4.459 -lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
   4.460 -  by (induct t s rule: numadd.induct) (auto simp add: Let_def)
   4.461 -
   4.462 -fun nummul:: "num \<Rightarrow> int \<Rightarrow> num" where
   4.463 +lemma numadd [simp]: "Inum bs (numadd (t, s)) = Inum bs (Add t s)"
   4.464 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff)
   4.465 +
   4.466 +lemma numadd_nb [simp]: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"
   4.467 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def)
   4.468 +
   4.469 +fun nummul:: "num \<Rightarrow> int \<Rightarrow> num"
   4.470 +where
   4.471    "nummul (C j) = (\<lambda> i. C (i*j))"
   4.472  | "nummul (CN n c t) = (\<lambda> i. CN n (c*i) (nummul t i))"
   4.473  | "nummul (CF c t s) = (\<lambda> i. CF (c*i) t (nummul s i))"
   4.474 @@ -785,7 +818,8 @@
   4.475    finally show ?thesis .
   4.476  qed
   4.477  
   4.478 -fun split_int:: "num \<Rightarrow> num \<times> num" where
   4.479 +fun split_int:: "num \<Rightarrow> num \<times> num"
   4.480 +where
   4.481    "split_int (C c) = (C 0, C c)"
   4.482  | "split_int (CN n c b) =
   4.483       (let (bv,bi) = split_int b
   4.484 @@ -853,7 +887,8 @@
   4.485    using split_int_nb[where t="t"]
   4.486    by (cases "fst (split_int t)") (auto simp add: numfloor_def Let_def split_def)
   4.487  
   4.488 -function simpnum:: "num \<Rightarrow> num" where
   4.489 +fun simpnum:: "num \<Rightarrow> num"
   4.490 +where
   4.491    "simpnum (C j) = C j"
   4.492  | "simpnum (Bound n) = CN n 1 (C 0)"
   4.493  | "simpnum (Neg t) = numneg (simpnum t)"
   4.494 @@ -863,8 +898,6 @@
   4.495  | "simpnum (Floor t) = numfloor (simpnum t)"
   4.496  | "simpnum (CN n c t) = (if c=0 then simpnum t else CN n c (simpnum t))"
   4.497  | "simpnum (CF c t s) = simpnum(Add (Mul c (Floor t)) s)"
   4.498 -by pat_completeness auto
   4.499 -termination by (relation "measure num_size") auto
   4.500  
   4.501  lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t"
   4.502    by (induct t rule: simpnum.induct) auto
   4.503 @@ -872,7 +905,8 @@
   4.504  lemma simpnum_numbound0[simp]: "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
   4.505    by (induct t rule: simpnum.induct) auto
   4.506  
   4.507 -fun nozerocoeff:: "num \<Rightarrow> bool" where
   4.508 +fun nozerocoeff:: "num \<Rightarrow> bool"
   4.509 +where
   4.510    "nozerocoeff (C c) = True"
   4.511  | "nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff t)"
   4.512  | "nozerocoeff (CF c s t) = (c \<noteq> 0 \<and> nozerocoeff t)"
   4.513 @@ -1001,7 +1035,8 @@
   4.514    ultimately show ?thesis by blast
   4.515  qed
   4.516  
   4.517 -fun not:: "fm \<Rightarrow> fm" where
   4.518 +fun not:: "fm \<Rightarrow> fm"
   4.519 +where
   4.520    "not (NOT p) = p"
   4.521  | "not T = F"
   4.522  | "not F = T"
   4.523 @@ -1059,12 +1094,13 @@
   4.524    Iff p q)"
   4.525  
   4.526  lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)"
   4.527 -  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp)  (cases "not p= q", auto simp add:not)
   4.528 +  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp)  (cases "not p= q", auto)
   4.529  
   4.530  lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
   4.531    by (unfold iff_def,cases "p=q", auto)
   4.532  
   4.533 -fun check_int:: "num \<Rightarrow> bool" where
   4.534 +fun check_int:: "num \<Rightarrow> bool"
   4.535 +where
   4.536    "check_int (C i) = True"
   4.537  | "check_int (Floor t) = True"
   4.538  | "check_int (Mul i t) = check_int t"
   4.539 @@ -1139,14 +1175,15 @@
   4.540    ultimately show ?thesis by blast
   4.541  qed
   4.542  
   4.543 -function (sequential) simpfm :: "fm \<Rightarrow> fm" where
   4.544 +fun simpfm :: "fm \<Rightarrow> fm"
   4.545 +where
   4.546    "simpfm (And p q) = conj (simpfm p) (simpfm q)"
   4.547  | "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   4.548  | "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
   4.549  | "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
   4.550  | "simpfm (NOT p) = not (simpfm p)"
   4.551  | "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F
   4.552 -  | _ \<Rightarrow> Lt (reducecoeff a'))"
   4.553 +    | _ \<Rightarrow> Lt (reducecoeff a'))"
   4.554  | "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0)  then T else F | _ \<Rightarrow> Le (reducecoeff a'))"
   4.555  | "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0)  then T else F | _ \<Rightarrow> Gt (reducecoeff a'))"
   4.556  | "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0)  then T else F | _ \<Rightarrow> Ge (reducecoeff a'))"
   4.557 @@ -1159,8 +1196,6 @@
   4.558               else if (\<bar>i\<bar> = 1) \<and> check_int a then F
   4.559               else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> (let (d,t) = simpdvd i a' in NDvd d t))"
   4.560  | "simpfm p = p"
   4.561 -by pat_completeness auto
   4.562 -termination by (relation "measure fmsize") auto
   4.563  
   4.564  lemma simpfm[simp]: "Ifm bs (simpfm p) = Ifm bs p"
   4.565  proof(induct p rule: simpfm.induct)
   4.566 @@ -1414,7 +1449,8 @@
   4.567    with qf show "qfree (CJNB qe p) \<and> Ifm bs (CJNB qe p) = Ifm bs (E p)" by blast
   4.568  qed
   4.569  
   4.570 -function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" where
   4.571 +fun qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   4.572 +where
   4.573    "qelim (E p) = (\<lambda> qe. DJ (CJNB qe) (qelim p qe))"
   4.574  | "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
   4.575  | "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
   4.576 @@ -1423,8 +1459,6 @@
   4.577  | "qelim (Imp p q) = (\<lambda> qe. disj (qelim (NOT p) qe) (qelim q qe))"
   4.578  | "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
   4.579  | "qelim p = (\<lambda> y. simpfm p)"
   4.580 -by pat_completeness auto
   4.581 -termination by (relation "measure fmsize") auto
   4.582  
   4.583  lemma qelim_ci:
   4.584    assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"
   4.585 @@ -1436,7 +1470,8 @@
   4.586  text \<open>The \<open>\<int>\<close> Part\<close>
   4.587  text\<open>Linearity for fm where Bound 0 ranges over \<open>\<int>\<close>\<close>
   4.588  
   4.589 -function zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*) where
   4.590 +fun zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*)
   4.591 +where
   4.592    "zsplit0 (C c) = (0,C c)"
   4.593  | "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"
   4.594  | "zsplit0 (CN n c a) = zsplit0 (Add (Mul c (Bound n)) a)"
   4.595 @@ -1450,8 +1485,6 @@
   4.596                              in (ia-ib, Sub a' b'))"
   4.597  | "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"
   4.598  | "zsplit0 (Floor a) = (let (i',a') =  zsplit0 a in (i',Floor a'))"
   4.599 -by pat_completeness auto
   4.600 -termination by (relation "measure num_size") auto
   4.601  
   4.602  lemma zsplit0_I:
   4.603    shows "\<And> n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((real_of_int (x::int)) #bs) (CN 0 n a) = Inum (real_of_int x #bs) t) \<and> numbound0 a"
   4.604 @@ -1533,23 +1566,21 @@
   4.605    with na show ?case by simp
   4.606  qed
   4.607  
   4.608 -consts
   4.609 -  iszlfm :: "fm \<Rightarrow> real list \<Rightarrow> bool"   (* Linearity test for fm *)
   4.610 -  zlfm :: "fm \<Rightarrow> fm"       (* Linearity transformation for fm *)
   4.611 -recdef iszlfm "measure size"
   4.612 +fun iszlfm :: "fm \<Rightarrow> real list \<Rightarrow> bool"   (* Linearity test for fm *)
   4.613 +where
   4.614    "iszlfm (And p q) = (\<lambda> bs. iszlfm p bs \<and> iszlfm q bs)"
   4.615 -  "iszlfm (Or p q) = (\<lambda> bs. iszlfm p bs \<and> iszlfm q bs)"
   4.616 -  "iszlfm (Eq  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.617 -  "iszlfm (NEq (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.618 -  "iszlfm (Lt  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.619 -  "iszlfm (Le  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.620 -  "iszlfm (Gt  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.621 -  "iszlfm (Ge  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.622 -  "iszlfm (Dvd i (CN 0 c e)) =
   4.623 +| "iszlfm (Or p q) = (\<lambda> bs. iszlfm p bs \<and> iszlfm q bs)"
   4.624 +| "iszlfm (Eq  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.625 +| "iszlfm (NEq (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.626 +| "iszlfm (Lt  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.627 +| "iszlfm (Le  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.628 +| "iszlfm (Gt  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.629 +| "iszlfm (Ge  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   4.630 +| "iszlfm (Dvd i (CN 0 c e)) =
   4.631                   (\<lambda> bs. c>0 \<and> i>0 \<and> numbound0 e \<and> isint e bs)"
   4.632 -  "iszlfm (NDvd i (CN 0 c e))=
   4.633 +| "iszlfm (NDvd i (CN 0 c e))=
   4.634                   (\<lambda> bs. c>0 \<and> i>0 \<and> numbound0 e \<and> isint e bs)"
   4.635 -  "iszlfm p = (\<lambda> bs. isatom p \<and> (bound0 p))"
   4.636 +| "iszlfm p = (\<lambda> bs. isatom p \<and> (bound0 p))"
   4.637  
   4.638  lemma zlin_qfree: "iszlfm p bs \<Longrightarrow> qfree p"
   4.639    by (induct p rule: iszlfm.induct) auto
   4.640 @@ -1569,61 +1600,62 @@
   4.641  lemma disj_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm q bs \<Longrightarrow> iszlfm (disj p q) bs"
   4.642    using disj_def by (cases p,auto)
   4.643  
   4.644 -recdef zlfm "measure fmsize"
   4.645 +fun zlfm :: "fm \<Rightarrow> fm"       (* Linearity transformation for fm *)
   4.646 +where
   4.647    "zlfm (And p q) = conj (zlfm p) (zlfm q)"
   4.648 -  "zlfm (Or p q) = disj (zlfm p) (zlfm q)"
   4.649 -  "zlfm (Imp p q) = disj (zlfm (NOT p)) (zlfm q)"
   4.650 -  "zlfm (Iff p q) = disj (conj (zlfm p) (zlfm q)) (conj (zlfm (NOT p)) (zlfm (NOT q)))"
   4.651 -  "zlfm (Lt a) = (let (c,r) = zsplit0 a in
   4.652 +| "zlfm (Or p q) = disj (zlfm p) (zlfm q)"
   4.653 +| "zlfm (Imp p q) = disj (zlfm (NOT p)) (zlfm q)"
   4.654 +| "zlfm (Iff p q) = disj (conj (zlfm p) (zlfm q)) (conj (zlfm (NOT p)) (zlfm (NOT q)))"
   4.655 +| "zlfm (Lt a) = (let (c,r) = zsplit0 a in
   4.656       if c=0 then Lt r else
   4.657       if c>0 then Or (Lt (CN 0 c (Neg (Floor (Neg r))))) (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Lt (Add (Floor (Neg r)) r)))
   4.658       else Or (Gt (CN 0 (-c) (Floor(Neg r)))) (And (Eq(CN 0 (-c) (Floor(Neg r)))) (Lt (Add (Floor (Neg r)) r))))"
   4.659 -  "zlfm (Le a) = (let (c,r) = zsplit0 a in
   4.660 +| "zlfm (Le a) = (let (c,r) = zsplit0 a in
   4.661       if c=0 then Le r else
   4.662       if c>0 then Or (Le (CN 0 c (Neg (Floor (Neg r))))) (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Lt (Add (Floor (Neg r)) r)))
   4.663       else Or (Ge (CN 0 (-c) (Floor(Neg r)))) (And (Eq(CN 0 (-c) (Floor(Neg r)))) (Lt (Add (Floor (Neg r)) r))))"
   4.664 -  "zlfm (Gt a) = (let (c,r) = zsplit0 a in
   4.665 +| "zlfm (Gt a) = (let (c,r) = zsplit0 a in
   4.666       if c=0 then Gt r else
   4.667       if c>0 then Or (Gt (CN 0 c (Floor r))) (And (Eq (CN 0 c (Floor r))) (Lt (Sub (Floor r) r)))
   4.668       else Or (Lt (CN 0 (-c) (Neg (Floor r)))) (And (Eq(CN 0 (-c) (Neg (Floor r)))) (Lt (Sub (Floor r) r))))"
   4.669 -  "zlfm (Ge a) = (let (c,r) = zsplit0 a in
   4.670 +| "zlfm (Ge a) = (let (c,r) = zsplit0 a in
   4.671       if c=0 then Ge r else
   4.672       if c>0 then Or (Ge (CN 0 c (Floor r))) (And (Eq (CN 0 c (Floor r))) (Lt (Sub (Floor r) r)))
   4.673       else Or (Le (CN 0 (-c) (Neg (Floor r)))) (And (Eq(CN 0 (-c) (Neg (Floor r)))) (Lt (Sub (Floor r) r))))"
   4.674 -  "zlfm (Eq a) = (let (c,r) = zsplit0 a in
   4.675 +| "zlfm (Eq a) = (let (c,r) = zsplit0 a in
   4.676                if c=0 then Eq r else
   4.677        if c>0 then (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Eq (Add (Floor (Neg r)) r)))
   4.678        else (And (Eq (CN 0 (-c) (Floor (Neg r)))) (Eq (Add (Floor (Neg r)) r))))"
   4.679 -  "zlfm (NEq a) = (let (c,r) = zsplit0 a in
   4.680 +| "zlfm (NEq a) = (let (c,r) = zsplit0 a in
   4.681                if c=0 then NEq r else
   4.682        if c>0 then (Or (NEq (CN 0 c (Neg (Floor (Neg r))))) (NEq (Add (Floor (Neg r)) r)))
   4.683        else (Or (NEq (CN 0 (-c) (Floor (Neg r)))) (NEq (Add (Floor (Neg r)) r))))"
   4.684 -  "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
   4.685 +| "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
   4.686    else (let (c,r) = zsplit0 a in
   4.687                if c=0 then Dvd \<bar>i\<bar> r else
   4.688        if c>0 then And (Eq (Sub (Floor r) r)) (Dvd \<bar>i\<bar> (CN 0 c (Floor r)))
   4.689        else And (Eq (Sub (Floor r) r)) (Dvd \<bar>i\<bar> (CN 0 (-c) (Neg (Floor r))))))"
   4.690 -  "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
   4.691 +| "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
   4.692    else (let (c,r) = zsplit0 a in
   4.693                if c=0 then NDvd \<bar>i\<bar> r else
   4.694        if c>0 then Or (NEq (Sub (Floor r) r)) (NDvd \<bar>i\<bar> (CN 0 c (Floor r)))
   4.695        else Or (NEq (Sub (Floor r) r)) (NDvd \<bar>i\<bar> (CN 0 (-c) (Neg (Floor r))))))"
   4.696 -  "zlfm (NOT (And p q)) = disj (zlfm (NOT p)) (zlfm (NOT q))"
   4.697 -  "zlfm (NOT (Or p q)) = conj (zlfm (NOT p)) (zlfm (NOT q))"
   4.698 -  "zlfm (NOT (Imp p q)) = conj (zlfm p) (zlfm (NOT q))"
   4.699 -  "zlfm (NOT (Iff p q)) = disj (conj(zlfm p) (zlfm(NOT q))) (conj (zlfm(NOT p)) (zlfm q))"
   4.700 -  "zlfm (NOT (NOT p)) = zlfm p"
   4.701 -  "zlfm (NOT T) = F"
   4.702 -  "zlfm (NOT F) = T"
   4.703 -  "zlfm (NOT (Lt a)) = zlfm (Ge a)"
   4.704 -  "zlfm (NOT (Le a)) = zlfm (Gt a)"
   4.705 -  "zlfm (NOT (Gt a)) = zlfm (Le a)"
   4.706 -  "zlfm (NOT (Ge a)) = zlfm (Lt a)"
   4.707 -  "zlfm (NOT (Eq a)) = zlfm (NEq a)"
   4.708 -  "zlfm (NOT (NEq a)) = zlfm (Eq a)"
   4.709 -  "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
   4.710 -  "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
   4.711 -  "zlfm p = p" (hints simp add: fmsize_pos)
   4.712 +| "zlfm (NOT (And p q)) = disj (zlfm (NOT p)) (zlfm (NOT q))"
   4.713 +| "zlfm (NOT (Or p q)) = conj (zlfm (NOT p)) (zlfm (NOT q))"
   4.714 +| "zlfm (NOT (Imp p q)) = conj (zlfm p) (zlfm (NOT q))"
   4.715 +| "zlfm (NOT (Iff p q)) = disj (conj(zlfm p) (zlfm(NOT q))) (conj (zlfm(NOT p)) (zlfm q))"
   4.716 +| "zlfm (NOT (NOT p)) = zlfm p"
   4.717 +| "zlfm (NOT T) = F"
   4.718 +| "zlfm (NOT F) = T"
   4.719 +| "zlfm (NOT (Lt a)) = zlfm (Ge a)"
   4.720 +| "zlfm (NOT (Le a)) = zlfm (Gt a)"
   4.721 +| "zlfm (NOT (Gt a)) = zlfm (Le a)"
   4.722 +| "zlfm (NOT (Ge a)) = zlfm (Lt a)"
   4.723 +| "zlfm (NOT (Eq a)) = zlfm (NEq a)"
   4.724 +| "zlfm (NOT (NEq a)) = zlfm (Eq a)"
   4.725 +| "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
   4.726 +| "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
   4.727 +| "zlfm p = p"
   4.728  
   4.729  lemma split_int_less_real:
   4.730    "(real_of_int (a::int) < b) = (a < \<lfloor>b\<rfloor> \<or> (a = \<lfloor>b\<rfloor> \<and> real_of_int \<lfloor>b\<rfloor> < b))"
   4.731 @@ -1944,7 +1976,8 @@
   4.732         \<open>\<delta>\<close> Compute lcm \<open>d| Dvd d  c*x+t \<in> p\<close>
   4.733         \<open>d_\<delta>\<close> checks if a given l divides all the ds above\<close>
   4.734  
   4.735 -fun minusinf:: "fm \<Rightarrow> fm" where
   4.736 +fun minusinf:: "fm \<Rightarrow> fm"
   4.737 +where
   4.738    "minusinf (And p q) = conj (minusinf p) (minusinf q)"
   4.739  | "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
   4.740  | "minusinf (Eq  (CN 0 c e)) = F"
   4.741 @@ -1958,7 +1991,8 @@
   4.742  lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
   4.743    by (induct p rule: minusinf.induct, auto)
   4.744  
   4.745 -fun plusinf:: "fm \<Rightarrow> fm" where
   4.746 +fun plusinf:: "fm \<Rightarrow> fm"
   4.747 +where
   4.748    "plusinf (And p q) = conj (plusinf p) (plusinf q)"
   4.749  | "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
   4.750  | "plusinf (Eq  (CN 0 c e)) = F"
   4.751 @@ -1969,14 +2003,16 @@
   4.752  | "plusinf (Ge  (CN 0 c e)) = T"
   4.753  | "plusinf p = p"
   4.754  
   4.755 -fun \<delta> :: "fm \<Rightarrow> int" where
   4.756 +fun \<delta> :: "fm \<Rightarrow> int"
   4.757 +where
   4.758    "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)"
   4.759  | "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)"
   4.760  | "\<delta> (Dvd i (CN 0 c e)) = i"
   4.761  | "\<delta> (NDvd i (CN 0 c e)) = i"
   4.762  | "\<delta> p = 1"
   4.763  
   4.764 -fun d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where
   4.765 +fun d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"
   4.766 +where
   4.767    "d_\<delta> (And p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)"
   4.768  | "d_\<delta> (Or p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)"
   4.769  | "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
   4.770 @@ -2237,88 +2273,88 @@
   4.771    from periodic_finite_ex[OF dpos th1] show ?thesis by blast
   4.772  qed
   4.773  
   4.774 -lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto
   4.775 -
   4.776 -consts
   4.777 -  a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coefficients of a formula *)
   4.778 -  d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
   4.779 -  \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
   4.780 -  \<beta> :: "fm \<Rightarrow> num list"
   4.781 -  \<alpha> :: "fm \<Rightarrow> num list"
   4.782 -
   4.783 -recdef a_\<beta> "measure size"
   4.784 +lemma dvd1_eq1: "x > 0 \<Longrightarrow> is_unit x \<longleftrightarrow> x = 1" for x :: int
   4.785 +  by simp
   4.786 +
   4.787 +fun a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coefficients of a formula *)
   4.788 +where
   4.789    "a_\<beta> (And p q) = (\<lambda> k. And (a_\<beta> p k) (a_\<beta> q k))"
   4.790 -  "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))"
   4.791 -  "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
   4.792 -  "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
   4.793 -  "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
   4.794 -  "a_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
   4.795 -  "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
   4.796 -  "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
   4.797 -  "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
   4.798 -  "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
   4.799 -  "a_\<beta> p = (\<lambda> k. p)"
   4.800 -
   4.801 -recdef d_\<beta> "measure size"
   4.802 +| "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))"
   4.803 +| "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
   4.804 +| "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
   4.805 +| "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
   4.806 +| "a_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
   4.807 +| "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
   4.808 +| "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
   4.809 +| "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
   4.810 +| "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
   4.811 +| "a_\<beta> p = (\<lambda> k. p)"
   4.812 +
   4.813 +fun d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
   4.814 +where
   4.815    "d_\<beta> (And p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
   4.816 -  "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
   4.817 -  "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.818 -  "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.819 -  "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.820 -  "d_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.821 -  "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.822 -  "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.823 -  "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
   4.824 -  "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
   4.825 -  "d_\<beta> p = (\<lambda> k. True)"
   4.826 -
   4.827 -recdef \<zeta> "measure size"
   4.828 +| "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
   4.829 +| "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.830 +| "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.831 +| "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.832 +| "d_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.833 +| "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.834 +| "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   4.835 +| "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
   4.836 +| "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
   4.837 +| "d_\<beta> p = (\<lambda> k. True)"
   4.838 +
   4.839 +fun \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
   4.840 +where
   4.841    "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
   4.842 -  "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
   4.843 -  "\<zeta> (Eq  (CN 0 c e)) = c"
   4.844 -  "\<zeta> (NEq (CN 0 c e)) = c"
   4.845 -  "\<zeta> (Lt  (CN 0 c e)) = c"
   4.846 -  "\<zeta> (Le  (CN 0 c e)) = c"
   4.847 -  "\<zeta> (Gt  (CN 0 c e)) = c"
   4.848 -  "\<zeta> (Ge  (CN 0 c e)) = c"
   4.849 -  "\<zeta> (Dvd i (CN 0 c e)) = c"
   4.850 -  "\<zeta> (NDvd i (CN 0 c e))= c"
   4.851 -  "\<zeta> p = 1"
   4.852 -
   4.853 -recdef \<beta> "measure size"
   4.854 +| "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
   4.855 +| "\<zeta> (Eq  (CN 0 c e)) = c"
   4.856 +| "\<zeta> (NEq (CN 0 c e)) = c"
   4.857 +| "\<zeta> (Lt  (CN 0 c e)) = c"
   4.858 +| "\<zeta> (Le  (CN 0 c e)) = c"
   4.859 +| "\<zeta> (Gt  (CN 0 c e)) = c"
   4.860 +| "\<zeta> (Ge  (CN 0 c e)) = c"
   4.861 +| "\<zeta> (Dvd i (CN 0 c e)) = c"
   4.862 +| "\<zeta> (NDvd i (CN 0 c e))= c"
   4.863 +| "\<zeta> p = 1"
   4.864 +
   4.865 +fun \<beta> :: "fm \<Rightarrow> num list"
   4.866 +where
   4.867    "\<beta> (And p q) = (\<beta> p @ \<beta> q)"
   4.868 -  "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
   4.869 -  "\<beta> (Eq  (CN 0 c e)) = [Sub (C (- 1)) e]"
   4.870 -  "\<beta> (NEq (CN 0 c e)) = [Neg e]"
   4.871 -  "\<beta> (Lt  (CN 0 c e)) = []"
   4.872 -  "\<beta> (Le  (CN 0 c e)) = []"
   4.873 -  "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
   4.874 -  "\<beta> (Ge  (CN 0 c e)) = [Sub (C (- 1)) e]"
   4.875 -  "\<beta> p = []"
   4.876 -
   4.877 -recdef \<alpha> "measure size"
   4.878 +| "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
   4.879 +| "\<beta> (Eq  (CN 0 c e)) = [Sub (C (- 1)) e]"
   4.880 +| "\<beta> (NEq (CN 0 c e)) = [Neg e]"
   4.881 +| "\<beta> (Lt  (CN 0 c e)) = []"
   4.882 +| "\<beta> (Le  (CN 0 c e)) = []"
   4.883 +| "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
   4.884 +| "\<beta> (Ge  (CN 0 c e)) = [Sub (C (- 1)) e]"
   4.885 +| "\<beta> p = []"
   4.886 +
   4.887 +fun \<alpha> :: "fm \<Rightarrow> num list"
   4.888 +where
   4.889    "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)"
   4.890 -  "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)"
   4.891 -  "\<alpha> (Eq  (CN 0 c e)) = [Add (C (- 1)) e]"
   4.892 -  "\<alpha> (NEq (CN 0 c e)) = [e]"
   4.893 -  "\<alpha> (Lt  (CN 0 c e)) = [e]"
   4.894 -  "\<alpha> (Le  (CN 0 c e)) = [Add (C (- 1)) e]"
   4.895 -  "\<alpha> (Gt  (CN 0 c e)) = []"
   4.896 -  "\<alpha> (Ge  (CN 0 c e)) = []"
   4.897 -  "\<alpha> p = []"
   4.898 -consts mirror :: "fm \<Rightarrow> fm"
   4.899 -recdef mirror "measure size"
   4.900 +| "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)"
   4.901 +| "\<alpha> (Eq  (CN 0 c e)) = [Add (C (- 1)) e]"
   4.902 +| "\<alpha> (NEq (CN 0 c e)) = [e]"
   4.903 +| "\<alpha> (Lt  (CN 0 c e)) = [e]"
   4.904 +| "\<alpha> (Le  (CN 0 c e)) = [Add (C (- 1)) e]"
   4.905 +| "\<alpha> (Gt  (CN 0 c e)) = []"
   4.906 +| "\<alpha> (Ge  (CN 0 c e)) = []"
   4.907 +| "\<alpha> p = []"
   4.908 +
   4.909 +fun mirror :: "fm \<Rightarrow> fm"
   4.910 +where
   4.911    "mirror (And p q) = And (mirror p) (mirror q)"
   4.912 -  "mirror (Or p q) = Or (mirror p) (mirror q)"
   4.913 -  "mirror (Eq  (CN 0 c e)) = Eq (CN 0 c (Neg e))"
   4.914 -  "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
   4.915 -  "mirror (Lt  (CN 0 c e)) = Gt (CN 0 c (Neg e))"
   4.916 -  "mirror (Le  (CN 0 c e)) = Ge (CN 0 c (Neg e))"
   4.917 -  "mirror (Gt  (CN 0 c e)) = Lt (CN 0 c (Neg e))"
   4.918 -  "mirror (Ge  (CN 0 c e)) = Le (CN 0 c (Neg e))"
   4.919 -  "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
   4.920 -  "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
   4.921 -  "mirror p = p"
   4.922 +| "mirror (Or p q) = Or (mirror p) (mirror q)"
   4.923 +| "mirror (Eq  (CN 0 c e)) = Eq (CN 0 c (Neg e))"
   4.924 +| "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
   4.925 +| "mirror (Lt  (CN 0 c e)) = Gt (CN 0 c (Neg e))"
   4.926 +| "mirror (Le  (CN 0 c e)) = Ge (CN 0 c (Neg e))"
   4.927 +| "mirror (Gt  (CN 0 c e)) = Lt (CN 0 c (Neg e))"
   4.928 +| "mirror (Ge  (CN 0 c e)) = Le (CN 0 c (Neg e))"
   4.929 +| "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
   4.930 +| "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
   4.931 +| "mirror p = p"
   4.932  
   4.933  lemma mirror_\<alpha>_\<beta>:
   4.934    assumes lp: "iszlfm p (a#bs)"
   4.935 @@ -2770,51 +2806,49 @@
   4.936      (* Reddy and Loveland *)
   4.937  
   4.938  
   4.939 -consts
   4.940 -  \<rho> :: "fm \<Rightarrow> (num \<times> int) list" (* Compute the Reddy and Loveland Bset*)
   4.941 -  \<sigma>_\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
   4.942 -  \<alpha>_\<rho> :: "fm \<Rightarrow> (num\<times>int) list"
   4.943 -  a_\<rho> :: "fm \<Rightarrow> int \<Rightarrow> fm"
   4.944 -recdef \<rho> "measure size"
   4.945 +fun \<rho> :: "fm \<Rightarrow> (num \<times> int) list" (* Compute the Reddy and Loveland Bset*)
   4.946 +  where
   4.947    "\<rho> (And p q) = (\<rho> p @ \<rho> q)"
   4.948 -  "\<rho> (Or p q) = (\<rho> p @ \<rho> q)"
   4.949 -  "\<rho> (Eq  (CN 0 c e)) = [(Sub (C (- 1)) e,c)]"
   4.950 -  "\<rho> (NEq (CN 0 c e)) = [(Neg e,c)]"
   4.951 -  "\<rho> (Lt  (CN 0 c e)) = []"
   4.952 -  "\<rho> (Le  (CN 0 c e)) = []"
   4.953 -  "\<rho> (Gt  (CN 0 c e)) = [(Neg e, c)]"
   4.954 -  "\<rho> (Ge  (CN 0 c e)) = [(Sub (C (-1)) e, c)]"
   4.955 -  "\<rho> p = []"
   4.956 -
   4.957 -recdef \<sigma>_\<rho> "measure size"
   4.958 +| "\<rho> (Or p q) = (\<rho> p @ \<rho> q)"
   4.959 +| "\<rho> (Eq  (CN 0 c e)) = [(Sub (C (- 1)) e,c)]"
   4.960 +| "\<rho> (NEq (CN 0 c e)) = [(Neg e,c)]"
   4.961 +| "\<rho> (Lt  (CN 0 c e)) = []"
   4.962 +| "\<rho> (Le  (CN 0 c e)) = []"
   4.963 +| "\<rho> (Gt  (CN 0 c e)) = [(Neg e, c)]"
   4.964 +| "\<rho> (Ge  (CN 0 c e)) = [(Sub (C (-1)) e, c)]"
   4.965 +| "\<rho> p = []"
   4.966 +
   4.967 +fun \<sigma>_\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
   4.968 +where
   4.969    "\<sigma>_\<rho> (And p q) = (\<lambda> (t,k). And (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
   4.970 -  "\<sigma>_\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
   4.971 -  "\<sigma>_\<rho> (Eq  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e))
   4.972 +| "\<sigma>_\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
   4.973 +| "\<sigma>_\<rho> (Eq  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e))
   4.974                                              else (Eq (Add (Mul c t) (Mul k e))))"
   4.975 -  "\<sigma>_\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e))
   4.976 +| "\<sigma>_\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e))
   4.977                                              else (NEq (Add (Mul c t) (Mul k e))))"
   4.978 -  "\<sigma>_\<rho> (Lt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e))
   4.979 +| "\<sigma>_\<rho> (Lt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e))
   4.980                                              else (Lt (Add (Mul c t) (Mul k e))))"
   4.981 -  "\<sigma>_\<rho> (Le  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e))
   4.982 +| "\<sigma>_\<rho> (Le  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e))
   4.983                                              else (Le (Add (Mul c t) (Mul k e))))"
   4.984 -  "\<sigma>_\<rho> (Gt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e))
   4.985 +| "\<sigma>_\<rho> (Gt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e))
   4.986                                              else (Gt (Add (Mul c t) (Mul k e))))"
   4.987 -  "\<sigma>_\<rho> (Ge  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e))
   4.988 +| "\<sigma>_\<rho> (Ge  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e))
   4.989                                              else (Ge (Add (Mul c t) (Mul k e))))"
   4.990 -  "\<sigma>_\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e))
   4.991 +| "\<sigma>_\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e))
   4.992                                              else (Dvd (i*k) (Add (Mul c t) (Mul k e))))"
   4.993 -  "\<sigma>_\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e))
   4.994 +| "\<sigma>_\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e))
   4.995                                              else (NDvd (i*k) (Add (Mul c t) (Mul k e))))"
   4.996 -  "\<sigma>_\<rho> p = (\<lambda> (t,k). p)"
   4.997 -
   4.998 -recdef \<alpha>_\<rho> "measure size"
   4.999 +| "\<sigma>_\<rho> p = (\<lambda> (t,k). p)"
  4.1000 +
  4.1001 +fun \<alpha>_\<rho> :: "fm \<Rightarrow> (num \<times> int) list"
  4.1002 +where
  4.1003    "\<alpha>_\<rho> (And p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
  4.1004 -  "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
  4.1005 -  "\<alpha>_\<rho> (Eq  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
  4.1006 -  "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
  4.1007 -  "\<alpha>_\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
  4.1008 -  "\<alpha>_\<rho> (Le  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
  4.1009 -  "\<alpha>_\<rho> p = []"
  4.1010 +| "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
  4.1011 +| "\<alpha>_\<rho> (Eq  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
  4.1012 +| "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
  4.1013 +| "\<alpha>_\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
  4.1014 +| "\<alpha>_\<rho> (Le  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
  4.1015 +| "\<alpha>_\<rho> p = []"
  4.1016  
  4.1017      (* Simulates normal substituion by modifying the formula see correctness theorem *)
  4.1018  
  4.1019 @@ -3277,18 +3311,17 @@
  4.1020  text \<open>The \<open>\<real>\<close> part\<close>
  4.1021  
  4.1022  text\<open>Linearity for fm where Bound 0 ranges over \<open>\<real>\<close>\<close>
  4.1023 -consts
  4.1024 -  isrlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
  4.1025 -recdef isrlfm "measure size"
  4.1026 +fun isrlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
  4.1027 +where
  4.1028    "isrlfm (And p q) = (isrlfm p \<and> isrlfm q)"
  4.1029 -  "isrlfm (Or p q) = (isrlfm p \<and> isrlfm q)"
  4.1030 -  "isrlfm (Eq  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1031 -  "isrlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1032 -  "isrlfm (Lt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1033 -  "isrlfm (Le  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1034 -  "isrlfm (Gt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1035 -  "isrlfm (Ge  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1036 -  "isrlfm p = (isatom p \<and> (bound0 p))"
  4.1037 +| "isrlfm (Or p q) = (isrlfm p \<and> isrlfm q)"
  4.1038 +| "isrlfm (Eq  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1039 +| "isrlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1040 +| "isrlfm (Lt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1041 +| "isrlfm (Le  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1042 +| "isrlfm (Gt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1043 +| "isrlfm (Ge  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  4.1044 +| "isrlfm p = (isatom p \<and> (bound0 p))"
  4.1045  
  4.1046  definition fp :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> int \<Rightarrow> fm" where
  4.1047    "fp p n s j \<equiv> (if n > 0 then
  4.1048 @@ -3299,7 +3332,8 @@
  4.1049                          (Gt (CN 0 (-n) (Add (Neg s) (Add (Floor s) (C (j + 1)))))))))"
  4.1050  
  4.1051    (* splits the bounded from the unbounded part*)
  4.1052 -function (sequential) rsplit0 :: "num \<Rightarrow> (fm \<times> int \<times> num) list" where
  4.1053 +fun rsplit0 :: "num \<Rightarrow> (fm \<times> int \<times> num) list"
  4.1054 +where
  4.1055    "rsplit0 (Bound 0) = [(T,1,C 0)]"
  4.1056  | "rsplit0 (Add a b) = (let acs = rsplit0 a ; bcs = rsplit0 b
  4.1057                in map (\<lambda> ((p,n,t),(q,m,s)). (And p q, n+m, Add t s)) [(a,b). a\<leftarrow>acs,b\<leftarrow>bcs])"
  4.1058 @@ -3314,8 +3348,6 @@
  4.1059  | "rsplit0 (CF c t s) = rsplit0 (Add (Mul c (Floor t)) s)"
  4.1060  | "rsplit0 (Mul c a) = map (\<lambda> (p,n,s). (p,c*n,Mul c s)) (rsplit0 a)"
  4.1061  | "rsplit0 t = [(T,0,t)]"
  4.1062 -by pat_completeness auto
  4.1063 -termination by (relation "measure num_size") auto
  4.1064  
  4.1065  lemma conj_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)"
  4.1066    using conj_def by (cases p, auto)
  4.1067 @@ -3914,36 +3946,36 @@
  4.1068    by (rule rsplit_l[where f="NDVD i" and a="a"], auto simp add: NDVD_def neq_def NDVDJ_l)
  4.1069  (case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
  4.1070  
  4.1071 -consts rlfm :: "fm \<Rightarrow> fm"
  4.1072 -recdef rlfm "measure fmsize"
  4.1073 +fun rlfm :: "fm \<Rightarrow> fm"
  4.1074 +where
  4.1075    "rlfm (And p q) = conj (rlfm p) (rlfm q)"
  4.1076 -  "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
  4.1077 -  "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
  4.1078 -  "rlfm (Iff p q) = disj (conj(rlfm p) (rlfm q)) (conj(rlfm (NOT p)) (rlfm (NOT q)))"
  4.1079 -  "rlfm (Lt a) = rsplit lt a"
  4.1080 -  "rlfm (Le a) = rsplit le a"
  4.1081 -  "rlfm (Gt a) = rsplit gt a"
  4.1082 -  "rlfm (Ge a) = rsplit ge a"
  4.1083 -  "rlfm (Eq a) = rsplit eq a"
  4.1084 -  "rlfm (NEq a) = rsplit neq a"
  4.1085 -  "rlfm (Dvd i a) = rsplit (\<lambda> t. DVD i t) a"
  4.1086 -  "rlfm (NDvd i a) = rsplit (\<lambda> t. NDVD i t) a"
  4.1087 -  "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
  4.1088 -  "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
  4.1089 -  "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
  4.1090 -  "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
  4.1091 -  "rlfm (NOT (NOT p)) = rlfm p"
  4.1092 -  "rlfm (NOT T) = F"
  4.1093 -  "rlfm (NOT F) = T"
  4.1094 -  "rlfm (NOT (Lt a)) = simpfm (rlfm (Ge a))"
  4.1095 -  "rlfm (NOT (Le a)) = simpfm (rlfm (Gt a))"
  4.1096 -  "rlfm (NOT (Gt a)) = simpfm (rlfm (Le a))"
  4.1097 -  "rlfm (NOT (Ge a)) = simpfm (rlfm (Lt a))"
  4.1098 -  "rlfm (NOT (Eq a)) = simpfm (rlfm (NEq a))"
  4.1099 -  "rlfm (NOT (NEq a)) = simpfm (rlfm (Eq a))"
  4.1100 -  "rlfm (NOT (Dvd i a)) = simpfm (rlfm (NDvd i a))"
  4.1101 -  "rlfm (NOT (NDvd i a)) = simpfm (rlfm (Dvd i a))"
  4.1102 -  "rlfm p = p" (hints simp add: fmsize_pos)
  4.1103 +| "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
  4.1104 +| "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
  4.1105 +| "rlfm (Iff p q) = disj (conj(rlfm p) (rlfm q)) (conj(rlfm (NOT p)) (rlfm (NOT q)))"
  4.1106 +| "rlfm (Lt a) = rsplit lt a"
  4.1107 +| "rlfm (Le a) = rsplit le a"
  4.1108 +| "rlfm (Gt a) = rsplit gt a"
  4.1109 +| "rlfm (Ge a) = rsplit ge a"
  4.1110 +| "rlfm (Eq a) = rsplit eq a"
  4.1111 +| "rlfm (NEq a) = rsplit neq a"
  4.1112 +| "rlfm (Dvd i a) = rsplit (\<lambda> t. DVD i t) a"
  4.1113 +| "rlfm (NDvd i a) = rsplit (\<lambda> t. NDVD i t) a"
  4.1114 +| "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
  4.1115 +| "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
  4.1116 +| "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
  4.1117 +| "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
  4.1118 +| "rlfm (NOT (NOT p)) = rlfm p"
  4.1119 +| "rlfm (NOT T) = F"
  4.1120 +| "rlfm (NOT F) = T"
  4.1121 +| "rlfm (NOT (Lt a)) = simpfm (rlfm (Ge a))"
  4.1122 +| "rlfm (NOT (Le a)) = simpfm (rlfm (Gt a))"
  4.1123 +| "rlfm (NOT (Gt a)) = simpfm (rlfm (Le a))"
  4.1124 +| "rlfm (NOT (Ge a)) = simpfm (rlfm (Lt a))"
  4.1125 +| "rlfm (NOT (Eq a)) = simpfm (rlfm (NEq a))"
  4.1126 +| "rlfm (NOT (NEq a)) = simpfm (rlfm (Eq a))"
  4.1127 +| "rlfm (NOT (Dvd i a)) = simpfm (rlfm (NDvd i a))"
  4.1128 +| "rlfm (NOT (NDvd i a)) = simpfm (rlfm (Dvd i a))"
  4.1129 +| "rlfm p = p"
  4.1130  
  4.1131  lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
  4.1132    by (induct p rule: isrlfm.induct, auto)
  4.1133 @@ -4377,30 +4409,29 @@
  4.1134    ultimately show ?thesis using z_def by auto
  4.1135  qed
  4.1136  
  4.1137 -consts
  4.1138 -  \<Upsilon>:: "fm \<Rightarrow> (num \<times> int) list"
  4.1139 -  \<upsilon> :: "fm \<Rightarrow> (num \<times> int) \<Rightarrow> fm "
  4.1140 -recdef \<Upsilon> "measure size"
  4.1141 +fun \<Upsilon>:: "fm \<Rightarrow> (num \<times> int) list"
  4.1142 +where
  4.1143    "\<Upsilon> (And p q) = (\<Upsilon> p @ \<Upsilon> q)"
  4.1144 -  "\<Upsilon> (Or p q) = (\<Upsilon> p @ \<Upsilon> q)"
  4.1145 -  "\<Upsilon> (Eq  (CN 0 c e)) = [(Neg e,c)]"
  4.1146 -  "\<Upsilon> (NEq (CN 0 c e)) = [(Neg e,c)]"
  4.1147 -  "\<Upsilon> (Lt  (CN 0 c e)) = [(Neg e,c)]"
  4.1148 -  "\<Upsilon> (Le  (CN 0 c e)) = [(Neg e,c)]"
  4.1149 -  "\<Upsilon> (Gt  (CN 0 c e)) = [(Neg e,c)]"
  4.1150 -  "\<Upsilon> (Ge  (CN 0 c e)) = [(Neg e,c)]"
  4.1151 -  "\<Upsilon> p = []"
  4.1152 -
  4.1153 -recdef \<upsilon> "measure size"
  4.1154 +| "\<Upsilon> (Or p q) = (\<Upsilon> p @ \<Upsilon> q)"
  4.1155 +| "\<Upsilon> (Eq  (CN 0 c e)) = [(Neg e,c)]"
  4.1156 +| "\<Upsilon> (NEq (CN 0 c e)) = [(Neg e,c)]"
  4.1157 +| "\<Upsilon> (Lt  (CN 0 c e)) = [(Neg e,c)]"
  4.1158 +| "\<Upsilon> (Le  (CN 0 c e)) = [(Neg e,c)]"
  4.1159 +| "\<Upsilon> (Gt  (CN 0 c e)) = [(Neg e,c)]"
  4.1160 +| "\<Upsilon> (Ge  (CN 0 c e)) = [(Neg e,c)]"
  4.1161 +| "\<Upsilon> p = []"
  4.1162 +
  4.1163 +fun \<upsilon> :: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm"
  4.1164 +where
  4.1165    "\<upsilon> (And p q) = (\<lambda> (t,n). And (\<upsilon> p (t,n)) (\<upsilon> q (t,n)))"
  4.1166 -  "\<upsilon> (Or p q) = (\<lambda> (t,n). Or (\<upsilon> p (t,n)) (\<upsilon> q (t,n)))"
  4.1167 -  "\<upsilon> (Eq (CN 0 c e)) = (\<lambda> (t,n). Eq (Add (Mul c t) (Mul n e)))"
  4.1168 -  "\<upsilon> (NEq (CN 0 c e)) = (\<lambda> (t,n). NEq (Add (Mul c t) (Mul n e)))"
  4.1169 -  "\<upsilon> (Lt (CN 0 c e)) = (\<lambda> (t,n). Lt (Add (Mul c t) (Mul n e)))"
  4.1170 -  "\<upsilon> (Le (CN 0 c e)) = (\<lambda> (t,n). Le (Add (Mul c t) (Mul n e)))"
  4.1171 -  "\<upsilon> (Gt (CN 0 c e)) = (\<lambda> (t,n). Gt (Add (Mul c t) (Mul n e)))"
  4.1172 -  "\<upsilon> (Ge (CN 0 c e)) = (\<lambda> (t,n). Ge (Add (Mul c t) (Mul n e)))"
  4.1173 -  "\<upsilon> p = (\<lambda> (t,n). p)"
  4.1174 +| "\<upsilon> (Or p q) = (\<lambda> (t,n). Or (\<upsilon> p (t,n)) (\<upsilon> q (t,n)))"
  4.1175 +| "\<upsilon> (Eq (CN 0 c e)) = (\<lambda> (t,n). Eq (Add (Mul c t) (Mul n e)))"
  4.1176 +| "\<upsilon> (NEq (CN 0 c e)) = (\<lambda> (t,n). NEq (Add (Mul c t) (Mul n e)))"
  4.1177 +| "\<upsilon> (Lt (CN 0 c e)) = (\<lambda> (t,n). Lt (Add (Mul c t) (Mul n e)))"
  4.1178 +| "\<upsilon> (Le (CN 0 c e)) = (\<lambda> (t,n). Le (Add (Mul c t) (Mul n e)))"
  4.1179 +| "\<upsilon> (Gt (CN 0 c e)) = (\<lambda> (t,n). Gt (Add (Mul c t) (Mul n e)))"
  4.1180 +| "\<upsilon> (Ge (CN 0 c e)) = (\<lambda> (t,n). Ge (Add (Mul c t) (Mul n e)))"
  4.1181 +| "\<upsilon> p = (\<lambda> (t,n). p)"
  4.1182  
  4.1183  lemma \<upsilon>_I: assumes lp: "isrlfm p"
  4.1184    and np: "real_of_int n > 0" and nbt: "numbound0 t"
  4.1185 @@ -4765,7 +4796,8 @@
  4.1186    ultimately show "(\<exists> (i::int) (u::real). 0\<le> u \<and> u< 1 \<and> P (real_of_int i + u))" by blast
  4.1187  qed
  4.1188  
  4.1189 -fun exsplitnum :: "num \<Rightarrow> num" where
  4.1190 +fun exsplitnum :: "num \<Rightarrow> num"
  4.1191 +where
  4.1192    "exsplitnum (C c) = (C c)"
  4.1193  | "exsplitnum (Bound 0) = Add (Bound 0) (Bound 1)"
  4.1194  | "exsplitnum (Bound n) = Bound (n+1)"
  4.1195 @@ -4778,7 +4810,8 @@
  4.1196  | "exsplitnum (CN n c a) = CN (n+1) c (exsplitnum a)"
  4.1197  | "exsplitnum (CF c s t) = CF c (exsplitnum s) (exsplitnum t)"
  4.1198  
  4.1199 -fun exsplit :: "fm \<Rightarrow> fm" where
  4.1200 +fun exsplit :: "fm \<Rightarrow> fm"
  4.1201 +where
  4.1202    "exsplit (Lt a) = Lt (exsplitnum a)"
  4.1203  | "exsplit (Le a) = Le (exsplitnum a)"
  4.1204  | "exsplit (Gt a) = Gt (exsplitnum a)"
     5.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Oct 08 22:28:21 2017 +0200
     5.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Oct 08 22:28:21 2017 +0200
     5.3 @@ -10,24 +10,29 @@
     5.4    Dense_Linear_Order
     5.5    DP_Library
     5.6    "HOL-Library.Code_Target_Numeral"
     5.7 -  "HOL-Library.Old_Recdef"
     5.8  begin
     5.9  
    5.10  subsection \<open>Terms\<close>
    5.11  
    5.12 -datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
    5.13 +datatype (plugins del: size) tm = CP poly | Bound nat | Add tm tm | Mul poly tm
    5.14    | Neg tm | Sub tm tm | CNP nat poly tm
    5.15  
    5.16 -text \<open>A size for poly to make inductive proofs simpler.\<close>
    5.17 -primrec tmsize :: "tm \<Rightarrow> nat"
    5.18 +instantiation tm :: size
    5.19 +begin
    5.20 +
    5.21 +primrec size_tm :: "tm \<Rightarrow> nat"
    5.22  where
    5.23 -  "tmsize (CP c) = polysize c"
    5.24 -| "tmsize (Bound n) = 1"
    5.25 -| "tmsize (Neg a) = 1 + tmsize a"
    5.26 -| "tmsize (Add a b) = 1 + tmsize a + tmsize b"
    5.27 -| "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
    5.28 -| "tmsize (Mul c a) = 1 + polysize c + tmsize a"
    5.29 -| "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
    5.30 +  "size_tm (CP c) = polysize c"
    5.31 +| "size_tm (Bound n) = 1"
    5.32 +| "size_tm (Neg a) = 1 + size_tm a"
    5.33 +| "size_tm (Add a b) = 1 + size_tm a + size_tm b"
    5.34 +| "size_tm (Sub a b) = 3 + size_tm a + size_tm b"
    5.35 +| "size_tm (Mul c a) = 1 + polysize c + size_tm a"
    5.36 +| "size_tm (CNP n c a) = 3 + polysize c + size_tm a "
    5.37 +
    5.38 +instance ..
    5.39 +
    5.40 +end
    5.41  
    5.42  text \<open>Semantics of terms tm.\<close>
    5.43  primrec Itm :: "'a::{field_char_0,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
    5.44 @@ -258,42 +263,42 @@
    5.45  
    5.46  text \<open>Simplification.\<close>
    5.47  
    5.48 -consts tmadd:: "tm \<times> tm \<Rightarrow> tm"
    5.49 -recdef tmadd "measure (\<lambda>(t,s). size t + size s)"
    5.50 -  "tmadd (CNP n1 c1 r1,CNP n2 c2 r2) =
    5.51 +fun tmadd:: "tm \<Rightarrow> tm \<Rightarrow> tm"
    5.52 +where
    5.53 +  "tmadd (CNP n1 c1 r1) (CNP n2 c2 r2) =
    5.54      (if n1 = n2 then
    5.55        let c = c1 +\<^sub>p c2
    5.56 -      in if c = 0\<^sub>p then tmadd(r1,r2) else CNP n1 c (tmadd (r1, r2))
    5.57 -    else if n1 \<le> n2 then (CNP n1 c1 (tmadd (r1,CNP n2 c2 r2)))
    5.58 -    else (CNP n2 c2 (tmadd (CNP n1 c1 r1, r2))))"
    5.59 -  "tmadd (CNP n1 c1 r1, t) = CNP n1 c1 (tmadd (r1, t))"
    5.60 -  "tmadd (t, CNP n2 c2 r2) = CNP n2 c2 (tmadd (t, r2))"
    5.61 -  "tmadd (CP b1, CP b2) = CP (b1 +\<^sub>p b2)"
    5.62 -  "tmadd (a, b) = Add a b"
    5.63 -
    5.64 -lemma tmadd[simp]: "Itm vs bs (tmadd (t, s)) = Itm vs bs (Add t s)"
    5.65 +      in if c = 0\<^sub>p then tmadd r1 r2 else CNP n1 c (tmadd r1 r2)
    5.66 +    else if n1 \<le> n2 then (CNP n1 c1 (tmadd r1 (CNP n2 c2 r2)))
    5.67 +    else (CNP n2 c2 (tmadd (CNP n1 c1 r1) r2)))"
    5.68 +| "tmadd (CNP n1 c1 r1) t = CNP n1 c1 (tmadd r1 t)"
    5.69 +| "tmadd t (CNP n2 c2 r2) = CNP n2 c2 (tmadd t r2)"
    5.70 +| "tmadd (CP b1) (CP b2) = CP (b1 +\<^sub>p b2)"
    5.71 +| "tmadd a b = Add a b"
    5.72 +
    5.73 +lemma tmadd [simp]: "Itm vs bs (tmadd t s) = Itm vs bs (Add t s)"
    5.74    apply (induct t s rule: tmadd.induct)
    5.75    apply (simp_all add: Let_def)
    5.76    apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p")
    5.77    apply (case_tac "n1 \<le> n2")
    5.78    apply simp_all
    5.79    apply (case_tac "n1 = n2")
    5.80 -  apply (simp_all add: field_simps)
    5.81 -  apply (simp only: distrib_left[symmetric])
    5.82 -  apply (auto simp del: polyadd simp add: polyadd[symmetric])
    5.83 +  apply (simp_all add: algebra_simps)
    5.84 +  apply (simp only: distrib_left [symmetric] polyadd [symmetric])
    5.85 +  apply simp
    5.86    done
    5.87  
    5.88 -lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd (t, s))"
    5.89 +lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd t s)"
    5.90    by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
    5.91  
    5.92 -lemma tmadd_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmadd (t, s))"
    5.93 +lemma tmadd_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmadd t s)"
    5.94    by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
    5.95  
    5.96 -lemma tmadd_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmadd (t, s))"
    5.97 +lemma tmadd_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmadd t s)"
    5.98    by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
    5.99  
   5.100  lemma tmadd_allpolys_npoly[simp]:
   5.101 -  "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd(t, s))"
   5.102 +  "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd t s)"
   5.103    by (induct t s rule: tmadd.induct) (simp_all add: Let_def polyadd_norm)
   5.104  
   5.105  fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm"
   5.106 @@ -323,7 +328,7 @@
   5.107    where "tmneg t \<equiv> tmmul t (C (- 1,1))"
   5.108  
   5.109  definition tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   5.110 -  where "tmsub s t \<equiv> (if s = t then CP 0\<^sub>p else tmadd (s, tmneg t))"
   5.111 +  where "tmsub s t \<equiv> (if s = t then CP 0\<^sub>p else tmadd s (tmneg t))"
   5.112  
   5.113  lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)"
   5.114    using tmneg_def[of t] by simp
   5.115 @@ -367,12 +372,12 @@
   5.116    "simptm (CP j) = CP (polynate j)"
   5.117  | "simptm (Bound n) = CNP n (1)\<^sub>p (CP 0\<^sub>p)"
   5.118  | "simptm (Neg t) = tmneg (simptm t)"
   5.119 -| "simptm (Add t s) = tmadd (simptm t,simptm s)"
   5.120 +| "simptm (Add t s) = tmadd (simptm t) (simptm s)"
   5.121  | "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
   5.122  | "simptm (Mul i t) =
   5.123      (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
   5.124  | "simptm (CNP n c t) =
   5.125 -    (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"
   5.126 +    (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p)) (simptm t))"
   5.127  
   5.128  lemma polynate_stupid:
   5.129    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   5.130 @@ -497,24 +502,34 @@
   5.131  
   5.132  subsection \<open>Formulae\<close>
   5.133  
   5.134 -datatype fm  =  T| F| Le tm | Lt tm | Eq tm | NEq tm|
   5.135 -  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
   5.136 -
   5.137 -
   5.138 -text \<open>A size for fm.\<close>
   5.139 -fun fmsize :: "fm \<Rightarrow> nat"
   5.140 +datatype (plugins del: size) fm = T | F | Le tm | Lt tm | Eq tm | NEq tm |
   5.141 +  NOT fm | And fm fm | Or fm fm | Imp fm fm | Iff fm fm | E fm | A fm
   5.142 +
   5.143 +instantiation fm :: size
   5.144 +begin
   5.145 +
   5.146 +primrec size_fm :: "fm \<Rightarrow> nat"
   5.147  where
   5.148 -  "fmsize (NOT p) = 1 + fmsize p"
   5.149 -| "fmsize (And p q) = 1 + fmsize p + fmsize q"
   5.150 -| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
   5.151 -| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
   5.152 -| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
   5.153 -| "fmsize (E p) = 1 + fmsize p"
   5.154 -| "fmsize (A p) = 4+ fmsize p"
   5.155 -| "fmsize p = 1"
   5.156 -
   5.157 -lemma fmsize_pos[termination_simp]: "fmsize p > 0"
   5.158 -  by (induct p rule: fmsize.induct) simp_all
   5.159 +  "size_fm (NOT p) = 1 + size_fm p"
   5.160 +| "size_fm (And p q) = 1 + size_fm p + size_fm q"
   5.161 +| "size_fm (Or p q) = 1 + size_fm p + size_fm q"
   5.162 +| "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
   5.163 +| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
   5.164 +| "size_fm (E p) = 1 + size_fm p"
   5.165 +| "size_fm (A p) = 4 + size_fm p"
   5.166 +| "size_fm T = 1"
   5.167 +| "size_fm F = 1"
   5.168 +| "size_fm (Le _) = 1"
   5.169 +| "size_fm (Lt _) = 1"
   5.170 +| "size_fm (Eq _) = 1"
   5.171 +| "size_fm (NEq _) = 1"
   5.172 +
   5.173 +instance ..
   5.174 +
   5.175 +end
   5.176 +
   5.177 +lemma fmsize_pos [simp]: "size p > 0" for p :: fm
   5.178 +  by (induct p) simp_all
   5.179  
   5.180  text \<open>Semantics of formulae (fm).\<close>
   5.181  primrec Ifm ::"'a::linordered_field list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
   5.182 @@ -1507,30 +1522,30 @@
   5.183      by blast
   5.184  qed
   5.185  
   5.186 -consts simpfm :: "fm \<Rightarrow> fm"
   5.187 -recdef simpfm "measure fmsize"
   5.188 +fun simpfm :: "fm \<Rightarrow> fm"
   5.189 +where
   5.190    "simpfm (Lt t) = simplt (simptm t)"
   5.191 -  "simpfm (Le t) = simple (simptm t)"
   5.192 -  "simpfm (Eq t) = simpeq(simptm t)"
   5.193 -  "simpfm (NEq t) = simpneq(simptm t)"
   5.194 -  "simpfm (And p q) = conj (simpfm p) (simpfm q)"
   5.195 -  "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   5.196 -  "simpfm (Imp p q) = disj (simpfm (NOT p)) (simpfm q)"
   5.197 -  "simpfm (Iff p q) =
   5.198 +| "simpfm (Le t) = simple (simptm t)"
   5.199 +| "simpfm (Eq t) = simpeq(simptm t)"
   5.200 +| "simpfm (NEq t) = simpneq(simptm t)"
   5.201 +| "simpfm (And p q) = conj (simpfm p) (simpfm q)"
   5.202 +| "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   5.203 +| "simpfm (Imp p q) = disj (simpfm (NOT p)) (simpfm q)"
   5.204 +| "simpfm (Iff p q) =
   5.205      disj (conj (simpfm p) (simpfm q)) (conj (simpfm (NOT p)) (simpfm (NOT q)))"
   5.206 -  "simpfm (NOT (And p q)) = disj (simpfm (NOT p)) (simpfm (NOT q))"
   5.207 -  "simpfm (NOT (Or p q)) = conj (simpfm (NOT p)) (simpfm (NOT q))"
   5.208 -  "simpfm (NOT (Imp p q)) = conj (simpfm p) (simpfm (NOT q))"
   5.209 -  "simpfm (NOT (Iff p q)) =
   5.210 +| "simpfm (NOT (And p q)) = disj (simpfm (NOT p)) (simpfm (NOT q))"
   5.211 +| "simpfm (NOT (Or p q)) = conj (simpfm (NOT p)) (simpfm (NOT q))"
   5.212 +| "simpfm (NOT (Imp p q)) = conj (simpfm p) (simpfm (NOT q))"
   5.213 +| "simpfm (NOT (Iff p q)) =
   5.214      disj (conj (simpfm p) (simpfm (NOT q))) (conj (simpfm (NOT p)) (simpfm q))"
   5.215 -  "simpfm (NOT (Eq t)) = simpneq t"
   5.216 -  "simpfm (NOT (NEq t)) = simpeq t"
   5.217 -  "simpfm (NOT (Le t)) = simplt (Neg t)"
   5.218 -  "simpfm (NOT (Lt t)) = simple (Neg t)"
   5.219 -  "simpfm (NOT (NOT p)) = simpfm p"
   5.220 -  "simpfm (NOT T) = F"
   5.221 -  "simpfm (NOT F) = T"
   5.222 -  "simpfm p = p"
   5.223 +| "simpfm (NOT (Eq t)) = simpneq t"
   5.224 +| "simpfm (NOT (NEq t)) = simpeq t"
   5.225 +| "simpfm (NOT (Le t)) = simplt (Neg t)"
   5.226 +| "simpfm (NOT (Lt t)) = simple (Neg t)"
   5.227 +| "simpfm (NOT (NOT p)) = simpfm p"
   5.228 +| "simpfm (NOT T) = F"
   5.229 +| "simpfm (NOT F) = T"
   5.230 +| "simpfm p = p"
   5.231  
   5.232  lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p"
   5.233    by (induct p arbitrary: bs rule: simpfm.induct) auto
   5.234 @@ -1589,39 +1604,38 @@
   5.235    shows "qfree p \<Longrightarrow> islin (simpfm p)"
   5.236    by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)
   5.237  
   5.238 -consts prep :: "fm \<Rightarrow> fm"
   5.239 -recdef prep "measure fmsize"
   5.240 +fun prep :: "fm \<Rightarrow> fm"
   5.241 +where
   5.242    "prep (E T) = T"
   5.243 -  "prep (E F) = F"
   5.244 -  "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
   5.245 -  "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
   5.246 -  "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
   5.247 -  "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
   5.248 -  "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
   5.249 -  "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
   5.250 -  "prep (E p) = E (prep p)"
   5.251 -  "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
   5.252 -  "prep (A p) = prep (NOT (E (NOT p)))"
   5.253 -  "prep (NOT (NOT p)) = prep p"
   5.254 -  "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
   5.255 -  "prep (NOT (A p)) = prep (E (NOT p))"
   5.256 -  "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
   5.257 -  "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
   5.258 -  "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
   5.259 -  "prep (NOT p) = not (prep p)"
   5.260 -  "prep (Or p q) = disj (prep p) (prep q)"
   5.261 -  "prep (And p q) = conj (prep p) (prep q)"
   5.262 -  "prep (Imp p q) = prep (Or (NOT p) q)"
   5.263 -  "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   5.264 -  "prep p = p"
   5.265 -  (hints simp add: fmsize_pos)
   5.266 +| "prep (E F) = F"
   5.267 +| "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
   5.268 +| "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
   5.269 +| "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
   5.270 +| "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
   5.271 +| "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
   5.272 +| "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
   5.273 +| "prep (E p) = E (prep p)"
   5.274 +| "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
   5.275 +| "prep (A p) = prep (NOT (E (NOT p)))"
   5.276 +| "prep (NOT (NOT p)) = prep p"
   5.277 +| "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
   5.278 +| "prep (NOT (A p)) = prep (E (NOT p))"
   5.279 +| "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
   5.280 +| "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
   5.281 +| "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
   5.282 +| "prep (NOT p) = not (prep p)"
   5.283 +| "prep (Or p q) = disj (prep p) (prep q)"
   5.284 +| "prep (And p q) = conj (prep p) (prep q)"
   5.285 +| "prep (Imp p q) = prep (Or (NOT p) q)"
   5.286 +| "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   5.287 +| "prep p = p"
   5.288  
   5.289  lemma prep: "Ifm vs bs (prep p) = Ifm vs bs p"
   5.290    by (induct p arbitrary: bs rule: prep.induct) auto
   5.291  
   5.292  
   5.293  text \<open>Generic quantifier elimination.\<close>
   5.294 -function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   5.295 +fun qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   5.296  where
   5.297    "qelim (E p) = (\<lambda>qe. DJ (CJNB qe) (qelim p qe))"
   5.298  | "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
   5.299 @@ -1631,8 +1645,6 @@
   5.300  | "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
   5.301  | "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
   5.302  | "qelim p = (\<lambda>y. simpfm p)"
   5.303 -  by pat_completeness simp_all
   5.304 -termination by (relation "measure fmsize") auto
   5.305  
   5.306  lemma qelim:
   5.307    assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))"
   5.308 @@ -2667,7 +2679,7 @@
   5.309      also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (-?s / (2*?d)) + ?r) = 0"
   5.310        using cd(2) mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
   5.311      also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2 * ?d * ?r= 0"
   5.312 -      by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
   5.313 +      by (simp add: field_simps distrib_left [of "2*?d"])
   5.314      also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r = 0"
   5.315        using cd(2) by simp
   5.316      finally show ?thesis
   5.317 @@ -2684,7 +2696,7 @@
   5.318      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (-?t / (2 * ?c)) + ?r) = 0"
   5.319        using cd(1) mult_cancel_left[of "2 * ?c" "(?a * (-?t / (2 * ?c)) + ?r)" 0] by simp
   5.320      also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2 * ?c) / (2 * ?c) + 2 * ?c * ?r= 0"
   5.321 -      by (simp add: field_simps distrib_left[of "2 * ?c"] del: distrib_left)
   5.322 +      by (simp add: field_simps distrib_left [of "2 * ?c"])
   5.323      also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0"
   5.324        using cd(1) by simp
   5.325      finally show ?thesis using cd