src/HOL/Decision_Procs/MIR.thy
changeset 66809 f6a30d48aab0
parent 66515 85c505c98332
child 67118 ccab07d1196c
     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -84,23 +84,32 @@
     1.4    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
     1.5    (*********************************************************************************)
     1.6  
     1.7 -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
     1.8 -  | Mul int num | Floor num| CF int num num
     1.9 -
    1.10 -  (* A size for num to make inductive proofs simpler*)
    1.11 -primrec num_size :: "num \<Rightarrow> nat" where
    1.12 - "num_size (C c) = 1"
    1.13 -| "num_size (Bound n) = 1"
    1.14 -| "num_size (Neg a) = 1 + num_size a"
    1.15 -| "num_size (Add a b) = 1 + num_size a + num_size b"
    1.16 -| "num_size (Sub a b) = 3 + num_size a + num_size b"
    1.17 -| "num_size (CN n c a) = 4 + num_size a "
    1.18 -| "num_size (CF c a b) = 4 + num_size a + num_size b"
    1.19 -| "num_size (Mul c a) = 1 + num_size a"
    1.20 -| "num_size (Floor a) = 1 + num_size a"
    1.21 +datatype (plugins del: size) num = C int | Bound nat | CN nat int num
    1.22 +  | Neg num | Add num num | Sub num num
    1.23 +  | Mul int num | Floor num | CF int num num
    1.24 +
    1.25 +instantiation num :: size
    1.26 +begin
    1.27 +
    1.28 +primrec size_num :: "num \<Rightarrow> nat"
    1.29 +where
    1.30 +  "size_num (C c) = 1"
    1.31 +| "size_num (Bound n) = 1"
    1.32 +| "size_num (Neg a) = 1 + size_num a"
    1.33 +| "size_num (Add a b) = 1 + size_num a + size_num b"
    1.34 +| "size_num (Sub a b) = 3 + size_num a + size_num b"
    1.35 +| "size_num (CN n c a) = 4 + size_num a "
    1.36 +| "size_num (CF c a b) = 4 + size_num a + size_num b"
    1.37 +| "size_num (Mul c a) = 1 + size_num a"
    1.38 +| "size_num (Floor a) = 1 + size_num a"
    1.39 +
    1.40 +instance ..
    1.41 +
    1.42 +end
    1.43  
    1.44    (* Semantics of numeral terms (num) *)
    1.45 -primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real" where
    1.46 +primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real"
    1.47 +where
    1.48    "Inum bs (C c) = (real_of_int c)"
    1.49  | "Inum bs (Bound n) = bs!n"
    1.50  | "Inum bs (CN n c a) = (real_of_int c) * (bs!n) + (Inum bs a)"
    1.51 @@ -169,48 +178,64 @@
    1.52  
    1.53  
    1.54      (* FORMULAE *)
    1.55 -datatype fm  =
    1.56 -  T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
    1.57 -  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
    1.58 -
    1.59 -
    1.60 -  (* A size for fm *)
    1.61 -fun fmsize :: "fm \<Rightarrow> nat" where
    1.62 - "fmsize (NOT p) = 1 + fmsize p"
    1.63 -| "fmsize (And p q) = 1 + fmsize p + fmsize q"
    1.64 -| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    1.65 -| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
    1.66 -| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
    1.67 -| "fmsize (E p) = 1 + fmsize p"
    1.68 -| "fmsize (A p) = 4+ fmsize p"
    1.69 -| "fmsize (Dvd i t) = 2"
    1.70 -| "fmsize (NDvd i t) = 2"
    1.71 -| "fmsize p = 1"
    1.72 -  (* several lemmas about fmsize *)
    1.73 -lemma fmsize_pos: "fmsize p > 0"
    1.74 -  by (induct p rule: fmsize.induct) simp_all
    1.75 +datatype (plugins del: size) fm =
    1.76 +  T | F | Lt num | Le num | Gt num | Ge num | Eq num | NEq num |
    1.77 +  Dvd int num | NDvd int num |
    1.78 +  NOT fm | And fm fm |  Or fm fm | Imp fm fm | Iff fm fm | E fm | A fm
    1.79 +
    1.80 +instantiation fm :: size
    1.81 +begin
    1.82 +
    1.83 +primrec size_fm :: "fm \<Rightarrow> nat"
    1.84 +where
    1.85 +  "size_fm (NOT p) = 1 + size_fm p"
    1.86 +| "size_fm (And p q) = 1 + size_fm p + size_fm q"
    1.87 +| "size_fm (Or p q) = 1 + size_fm p + size_fm q"
    1.88 +| "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
    1.89 +| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
    1.90 +| "size_fm (E p) = 1 + size_fm p"
    1.91 +| "size_fm (A p) = 4 + size_fm p"
    1.92 +| "size_fm (Dvd i t) = 2"
    1.93 +| "size_fm (NDvd i t) = 2"
    1.94 +| "size_fm T = 1"
    1.95 +| "size_fm F = 1"
    1.96 +| "size_fm (Lt _) = 1"
    1.97 +| "size_fm (Le _) = 1"
    1.98 +| "size_fm (Gt _) = 1"
    1.99 +| "size_fm (Ge _) = 1"
   1.100 +| "size_fm (Eq _) = 1"
   1.101 +| "size_fm (NEq _) = 1"
   1.102 +
   1.103 +instance ..
   1.104 +
   1.105 +end
   1.106 +
   1.107 +lemma size_fm_pos [simp]: "size p > 0" for p :: fm
   1.108 +  by (induct p) simp_all
   1.109  
   1.110    (* Semantics of formulae (fm) *)
   1.111 -primrec Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool" where
   1.112 -  "Ifm bs T = True"
   1.113 -| "Ifm bs F = False"
   1.114 -| "Ifm bs (Lt a) = (Inum bs a < 0)"
   1.115 -| "Ifm bs (Gt a) = (Inum bs a > 0)"
   1.116 -| "Ifm bs (Le a) = (Inum bs a \<le> 0)"
   1.117 -| "Ifm bs (Ge a) = (Inum bs a \<ge> 0)"
   1.118 -| "Ifm bs (Eq a) = (Inum bs a = 0)"
   1.119 -| "Ifm bs (NEq a) = (Inum bs a \<noteq> 0)"
   1.120 -| "Ifm bs (Dvd i b) = (real_of_int i rdvd Inum bs b)"
   1.121 -| "Ifm bs (NDvd i b) = (\<not>(real_of_int i rdvd Inum bs b))"
   1.122 -| "Ifm bs (NOT p) = (\<not> (Ifm bs p))"
   1.123 -| "Ifm bs (And p q) = (Ifm bs p \<and> Ifm bs q)"
   1.124 -| "Ifm bs (Or p q) = (Ifm bs p \<or> Ifm bs q)"
   1.125 -| "Ifm bs (Imp p q) = ((Ifm bs p) \<longrightarrow> (Ifm bs q))"
   1.126 -| "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)"
   1.127 -| "Ifm bs (E p) = (\<exists> x. Ifm (x#bs) p)"
   1.128 -| "Ifm bs (A p) = (\<forall> x. Ifm (x#bs) p)"
   1.129 -
   1.130 -function (sequential) prep :: "fm \<Rightarrow> fm" where
   1.131 +primrec Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool"
   1.132 +where
   1.133 +  "Ifm bs T \<longleftrightarrow> True"
   1.134 +| "Ifm bs F \<longleftrightarrow> False"
   1.135 +| "Ifm bs (Lt a) \<longleftrightarrow> Inum bs a < 0"
   1.136 +| "Ifm bs (Gt a) \<longleftrightarrow> Inum bs a > 0"
   1.137 +| "Ifm bs (Le a) \<longleftrightarrow> Inum bs a \<le> 0"
   1.138 +| "Ifm bs (Ge a) \<longleftrightarrow> Inum bs a \<ge> 0"
   1.139 +| "Ifm bs (Eq a) \<longleftrightarrow> Inum bs a = 0"
   1.140 +| "Ifm bs (NEq a) \<longleftrightarrow> Inum bs a \<noteq> 0"
   1.141 +| "Ifm bs (Dvd i b) \<longleftrightarrow> real_of_int i rdvd Inum bs b"
   1.142 +| "Ifm bs (NDvd i b) \<longleftrightarrow> \<not> (real_of_int i rdvd Inum bs b)"
   1.143 +| "Ifm bs (NOT p) \<longleftrightarrow> \<not> (Ifm bs p)"
   1.144 +| "Ifm bs (And p q) \<longleftrightarrow> Ifm bs p \<and> Ifm bs q"
   1.145 +| "Ifm bs (Or p q) \<longleftrightarrow> Ifm bs p \<or> Ifm bs q"
   1.146 +| "Ifm bs (Imp p q) \<longleftrightarrow> (Ifm bs p \<longrightarrow> Ifm bs q)"
   1.147 +| "Ifm bs (Iff p q) \<longleftrightarrow> (Ifm bs p \<longleftrightarrow> Ifm bs q)"
   1.148 +| "Ifm bs (E p) \<longleftrightarrow> (\<exists>x. Ifm (x # bs) p)"
   1.149 +| "Ifm bs (A p) \<longleftrightarrow> (\<forall>x. Ifm (x # bs) p)"
   1.150 +
   1.151 +fun prep :: "fm \<Rightarrow> fm"
   1.152 +where
   1.153    "prep (E T) = T"
   1.154  | "prep (E F) = F"
   1.155  | "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
   1.156 @@ -234,35 +259,35 @@
   1.157  | "prep (Imp p q) = prep (Or (NOT p) q)"
   1.158  | "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   1.159  | "prep p = p"
   1.160 -  by pat_completeness simp_all
   1.161 -termination by (relation "measure fmsize") (simp_all add: fmsize_pos)
   1.162  
   1.163  lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
   1.164    by (induct p rule: prep.induct) auto
   1.165  
   1.166  
   1.167    (* Quantifier freeness *)
   1.168 -fun qfree:: "fm \<Rightarrow> bool" where
   1.169 +fun qfree:: "fm \<Rightarrow> bool"
   1.170 +where
   1.171    "qfree (E p) = False"
   1.172 -  | "qfree (A p) = False"
   1.173 -  | "qfree (NOT p) = qfree p"
   1.174 -  | "qfree (And p q) = (qfree p \<and> qfree q)"
   1.175 -  | "qfree (Or  p q) = (qfree p \<and> qfree q)"
   1.176 -  | "qfree (Imp p q) = (qfree p \<and> qfree q)"
   1.177 -  | "qfree (Iff p q) = (qfree p \<and> qfree q)"
   1.178 -  | "qfree p = True"
   1.179 +| "qfree (A p) = False"
   1.180 +| "qfree (NOT p) = qfree p"
   1.181 +| "qfree (And p q) = (qfree p \<and> qfree q)"
   1.182 +| "qfree (Or  p q) = (qfree p \<and> qfree q)"
   1.183 +| "qfree (Imp p q) = (qfree p \<and> qfree q)"
   1.184 +| "qfree (Iff p q) = (qfree p \<and> qfree q)"
   1.185 +| "qfree p = True"
   1.186  
   1.187    (* Boundedness and substitution *)
   1.188 -primrec numbound0 :: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) where
   1.189 +primrec numbound0 :: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)
   1.190 +where
   1.191    "numbound0 (C c) = True"
   1.192 -  | "numbound0 (Bound n) = (n>0)"
   1.193 -  | "numbound0 (CN n i a) = (n > 0 \<and> numbound0 a)"
   1.194 -  | "numbound0 (Neg a) = numbound0 a"
   1.195 -  | "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
   1.196 -  | "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
   1.197 -  | "numbound0 (Mul i a) = numbound0 a"
   1.198 -  | "numbound0 (Floor a) = numbound0 a"
   1.199 -  | "numbound0 (CF c a b) = (numbound0 a \<and> numbound0 b)"
   1.200 +| "numbound0 (Bound n) = (n>0)"
   1.201 +| "numbound0 (CN n i a) = (n > 0 \<and> numbound0 a)"
   1.202 +| "numbound0 (Neg a) = numbound0 a"
   1.203 +| "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
   1.204 +| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
   1.205 +| "numbound0 (Mul i a) = numbound0 a"
   1.206 +| "numbound0 (Floor a) = numbound0 a"
   1.207 +| "numbound0 (CF c a b) = (numbound0 a \<and> numbound0 b)"
   1.208  
   1.209  lemma numbound0_I:
   1.210    assumes nb: "numbound0 a"
   1.211 @@ -280,24 +305,25 @@
   1.212      by (simp add: isint_def)
   1.213  qed
   1.214  
   1.215 -primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
   1.216 +primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
   1.217 +where
   1.218    "bound0 T = True"
   1.219 -  | "bound0 F = True"
   1.220 -  | "bound0 (Lt a) = numbound0 a"
   1.221 -  | "bound0 (Le a) = numbound0 a"
   1.222 -  | "bound0 (Gt a) = numbound0 a"
   1.223 -  | "bound0 (Ge a) = numbound0 a"
   1.224 -  | "bound0 (Eq a) = numbound0 a"
   1.225 -  | "bound0 (NEq a) = numbound0 a"
   1.226 -  | "bound0 (Dvd i a) = numbound0 a"
   1.227 -  | "bound0 (NDvd i a) = numbound0 a"
   1.228 -  | "bound0 (NOT p) = bound0 p"
   1.229 -  | "bound0 (And p q) = (bound0 p \<and> bound0 q)"
   1.230 -  | "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
   1.231 -  | "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
   1.232 -  | "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
   1.233 -  | "bound0 (E p) = False"
   1.234 -  | "bound0 (A p) = False"
   1.235 +| "bound0 F = True"
   1.236 +| "bound0 (Lt a) = numbound0 a"
   1.237 +| "bound0 (Le a) = numbound0 a"
   1.238 +| "bound0 (Gt a) = numbound0 a"
   1.239 +| "bound0 (Ge a) = numbound0 a"
   1.240 +| "bound0 (Eq a) = numbound0 a"
   1.241 +| "bound0 (NEq a) = numbound0 a"
   1.242 +| "bound0 (Dvd i a) = numbound0 a"
   1.243 +| "bound0 (NDvd i a) = numbound0 a"
   1.244 +| "bound0 (NOT p) = bound0 p"
   1.245 +| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
   1.246 +| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
   1.247 +| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
   1.248 +| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
   1.249 +| "bound0 (E p) = False"
   1.250 +| "bound0 (A p) = False"
   1.251  
   1.252  lemma bound0_I:
   1.253    assumes bp: "bound0 p"
   1.254 @@ -305,44 +331,47 @@
   1.255    using bp numbound0_I [where b="b" and bs="bs" and b'="b'"]
   1.256    by (induct p) auto
   1.257  
   1.258 -primrec numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *) where
   1.259 +primrec numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *)
   1.260 +where
   1.261    "numsubst0 t (C c) = (C c)"
   1.262 -  | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   1.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))"
   1.264 -  | "numsubst0 t (CF i a b) = CF i (numsubst0 t a) (numsubst0 t b)"
   1.265 -  | "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
   1.266 -  | "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
   1.267 -  | "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)"
   1.268 -  | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
   1.269 -  | "numsubst0 t (Floor a) = Floor (numsubst0 t a)"
   1.270 +| "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   1.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))"
   1.272 +| "numsubst0 t (CF i a b) = CF i (numsubst0 t a) (numsubst0 t b)"
   1.273 +| "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
   1.274 +| "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
   1.275 +| "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)"
   1.276 +| "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
   1.277 +| "numsubst0 t (Floor a) = Floor (numsubst0 t a)"
   1.278  
   1.279  lemma numsubst0_I:
   1.280    shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
   1.281    by (induct t) simp_all
   1.282  
   1.283 -primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
   1.284 +primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *)
   1.285 +where
   1.286    "subst0 t T = T"
   1.287 -  | "subst0 t F = F"
   1.288 -  | "subst0 t (Lt a) = Lt (numsubst0 t a)"
   1.289 -  | "subst0 t (Le a) = Le (numsubst0 t a)"
   1.290 -  | "subst0 t (Gt a) = Gt (numsubst0 t a)"
   1.291 -  | "subst0 t (Ge a) = Ge (numsubst0 t a)"
   1.292 -  | "subst0 t (Eq a) = Eq (numsubst0 t a)"
   1.293 -  | "subst0 t (NEq a) = NEq (numsubst0 t a)"
   1.294 -  | "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
   1.295 -  | "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
   1.296 -  | "subst0 t (NOT p) = NOT (subst0 t p)"
   1.297 -  | "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   1.298 -  | "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   1.299 -  | "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
   1.300 -  | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   1.301 +| "subst0 t F = F"
   1.302 +| "subst0 t (Lt a) = Lt (numsubst0 t a)"
   1.303 +| "subst0 t (Le a) = Le (numsubst0 t a)"
   1.304 +| "subst0 t (Gt a) = Gt (numsubst0 t a)"
   1.305 +| "subst0 t (Ge a) = Ge (numsubst0 t a)"
   1.306 +| "subst0 t (Eq a) = Eq (numsubst0 t a)"
   1.307 +| "subst0 t (NEq a) = NEq (numsubst0 t a)"
   1.308 +| "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
   1.309 +| "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
   1.310 +| "subst0 t (NOT p) = NOT (subst0 t p)"
   1.311 +| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   1.312 +| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   1.313 +| "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
   1.314 +| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   1.315  
   1.316  lemma subst0_I: assumes qfp: "qfree p"
   1.317    shows "Ifm (b#bs) (subst0 a p) = Ifm ((Inum (b#bs) a)#bs) p"
   1.318    using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
   1.319    by (induct p) simp_all
   1.320  
   1.321 -fun decrnum:: "num \<Rightarrow> num" where
   1.322 +fun decrnum:: "num \<Rightarrow> num"
   1.323 +where
   1.324    "decrnum (Bound n) = Bound (n - 1)"
   1.325  | "decrnum (Neg a) = Neg (decrnum a)"
   1.326  | "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
   1.327 @@ -353,7 +382,8 @@
   1.328  | "decrnum (CF c a b) = CF c (decrnum a) (decrnum b)"
   1.329  | "decrnum a = a"
   1.330  
   1.331 -fun decr :: "fm \<Rightarrow> fm" where
   1.332 +fun decr :: "fm \<Rightarrow> fm"
   1.333 +where
   1.334    "decr (Lt a) = Lt (decrnum a)"
   1.335  | "decr (Le a) = Le (decrnum a)"
   1.336  | "decr (Gt a) = Gt (decrnum a)"
   1.337 @@ -380,7 +410,8 @@
   1.338  lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
   1.339    by (induct p) simp_all
   1.340  
   1.341 -fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where
   1.342 +fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
   1.343 +where
   1.344    "isatom T = True"
   1.345  | "isatom F = True"
   1.346  | "isatom (Lt a) = True"
   1.347 @@ -441,12 +472,14 @@
   1.348    apply auto
   1.349    done
   1.350  
   1.351 -fun disjuncts :: "fm \<Rightarrow> fm list" where
   1.352 +fun disjuncts :: "fm \<Rightarrow> fm list"
   1.353 +where
   1.354    "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
   1.355  | "disjuncts F = []"
   1.356  | "disjuncts p = [p]"
   1.357  
   1.358 -fun conjuncts :: "fm \<Rightarrow> fm list" where
   1.359 +fun conjuncts :: "fm \<Rightarrow> fm list"
   1.360 +where
   1.361    "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)"
   1.362  | "conjuncts T = []"
   1.363  | "conjuncts p = [p]"
   1.364 @@ -511,7 +544,8 @@
   1.365    (* Simplification *)
   1.366  
   1.367    (* Algebraic simplifications for nums *)
   1.368 -fun bnds:: "num \<Rightarrow> nat list" where
   1.369 +fun bnds:: "num \<Rightarrow> nat list"
   1.370 +where
   1.371    "bnds (Bound n) = [n]"
   1.372  | "bnds (CN n c a) = n#(bnds a)"
   1.373  | "bnds (Neg a) = bnds a"
   1.374 @@ -521,14 +555,17 @@
   1.375  | "bnds (Floor a) = bnds a"
   1.376  | "bnds (CF c a b) = (bnds a)@(bnds b)"
   1.377  | "bnds a = []"
   1.378 -fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool" where
   1.379 +
   1.380 +fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool"
   1.381 +where
   1.382    "lex_ns [] ms = True"
   1.383  | "lex_ns ns [] = False"
   1.384  | "lex_ns (n#ns) (m#ms) = (n<m \<or> ((n = m) \<and> lex_ns ns ms)) "
   1.385  definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool" where
   1.386    "lex_bnd t s \<equiv> lex_ns (bnds t) (bnds s)"
   1.387  
   1.388 -fun maxcoeff:: "num \<Rightarrow> int" where
   1.389 +fun maxcoeff:: "num \<Rightarrow> int"
   1.390 +where
   1.391    "maxcoeff (C i) = \<bar>i\<bar>"
   1.392  | "maxcoeff (CN n c t) = max \<bar>c\<bar> (maxcoeff t)"
   1.393  | "maxcoeff (CF c t s) = max \<bar>c\<bar> (maxcoeff s)"
   1.394 @@ -537,7 +574,8 @@
   1.395  lemma maxcoeff_pos: "maxcoeff t \<ge> 0"
   1.396    by (induct t rule: maxcoeff.induct) auto
   1.397  
   1.398 -fun numgcdh:: "num \<Rightarrow> int \<Rightarrow> int" where
   1.399 +fun numgcdh:: "num \<Rightarrow> int \<Rightarrow> int"
   1.400 +where
   1.401    "numgcdh (C i) = (\<lambda>g. gcd i g)"
   1.402  | "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"
   1.403  | "numgcdh (CF c s t) = (\<lambda>g. gcd c (numgcdh t g))"
   1.404 @@ -546,7 +584,8 @@
   1.405  definition numgcd :: "num \<Rightarrow> int"
   1.406    where "numgcd t = numgcdh t (maxcoeff t)"
   1.407  
   1.408 -fun reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num" where
   1.409 +fun reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num"
   1.410 +where
   1.411    "reducecoeffh (C i) = (\<lambda> g. C (i div g))"
   1.412  | "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))"
   1.413  | "reducecoeffh (CF c s t) = (\<lambda> g. CF (c div g)  s (reducecoeffh t g))"
   1.414 @@ -558,7 +597,8 @@
   1.415      (let g = numgcd t in
   1.416       if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)"
   1.417  
   1.418 -fun dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
   1.419 +fun dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
   1.420 +where
   1.421    "dvdnumcoeff (C i) = (\<lambda> g. g dvd i)"
   1.422  | "dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"
   1.423  | "dvdnumcoeff (CF c s t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"
   1.424 @@ -602,7 +642,8 @@
   1.425    from assms 3 show ?case by (simp add: real_of_int_div[OF gd] algebra_simps)
   1.426  qed (auto simp add: numgcd_def gp)
   1.427  
   1.428 -fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
   1.429 +fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
   1.430 +where
   1.431    "ismaxcoeff (C i) = (\<lambda> x. \<bar>i\<bar> \<le> x)"
   1.432  | "ismaxcoeff (CN n c t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> (ismaxcoeff t x))"
   1.433  | "ismaxcoeff (CF c s t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> (ismaxcoeff t x))"
   1.434 @@ -711,7 +752,7 @@
   1.435    using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)
   1.436  
   1.437  consts numadd:: "num \<times> num \<Rightarrow> num"
   1.438 -recdef numadd "measure (\<lambda> (t,s). size t + size s)"
   1.439 +recdef numadd "measure (\<lambda>(t, s). size t + size s)"
   1.440    "numadd (CN n1 c1 r1,CN n2 c2 r2) =
   1.441    (if n1=n2 then
   1.442    (let c = c1 + c2
   1.443 @@ -730,22 +771,14 @@
   1.444    "numadd (C b1, C b2) = C (b1+b2)"
   1.445    "numadd (a,b) = Add a b"
   1.446  
   1.447 -lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
   1.448 -apply (induct t s rule: numadd.induct, simp_all add: Let_def)
   1.449 - apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
   1.450 -  apply (case_tac "n1 = n2", simp_all add: algebra_simps)
   1.451 -  apply (simp only: distrib_right[symmetric])
   1.452 - apply simp
   1.453 -apply (case_tac "lex_bnd t1 t2", simp_all)
   1.454 - apply (case_tac "c1+c2 = 0")
   1.455 -  apply (case_tac "t1 = t2")
   1.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)
   1.457 -  done
   1.458 -
   1.459 -lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
   1.460 -  by (induct t s rule: numadd.induct) (auto simp add: Let_def)
   1.461 -
   1.462 -fun nummul:: "num \<Rightarrow> int \<Rightarrow> num" where
   1.463 +lemma numadd [simp]: "Inum bs (numadd (t, s)) = Inum bs (Add t s)"
   1.464 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff)
   1.465 +
   1.466 +lemma numadd_nb [simp]: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"
   1.467 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def)
   1.468 +
   1.469 +fun nummul:: "num \<Rightarrow> int \<Rightarrow> num"
   1.470 +where
   1.471    "nummul (C j) = (\<lambda> i. C (i*j))"
   1.472  | "nummul (CN n c t) = (\<lambda> i. CN n (c*i) (nummul t i))"
   1.473  | "nummul (CF c t s) = (\<lambda> i. CF (c*i) t (nummul s i))"
   1.474 @@ -785,7 +818,8 @@
   1.475    finally show ?thesis .
   1.476  qed
   1.477  
   1.478 -fun split_int:: "num \<Rightarrow> num \<times> num" where
   1.479 +fun split_int:: "num \<Rightarrow> num \<times> num"
   1.480 +where
   1.481    "split_int (C c) = (C 0, C c)"
   1.482  | "split_int (CN n c b) =
   1.483       (let (bv,bi) = split_int b
   1.484 @@ -853,7 +887,8 @@
   1.485    using split_int_nb[where t="t"]
   1.486    by (cases "fst (split_int t)") (auto simp add: numfloor_def Let_def split_def)
   1.487  
   1.488 -function simpnum:: "num \<Rightarrow> num" where
   1.489 +fun simpnum:: "num \<Rightarrow> num"
   1.490 +where
   1.491    "simpnum (C j) = C j"
   1.492  | "simpnum (Bound n) = CN n 1 (C 0)"
   1.493  | "simpnum (Neg t) = numneg (simpnum t)"
   1.494 @@ -863,8 +898,6 @@
   1.495  | "simpnum (Floor t) = numfloor (simpnum t)"
   1.496  | "simpnum (CN n c t) = (if c=0 then simpnum t else CN n c (simpnum t))"
   1.497  | "simpnum (CF c t s) = simpnum(Add (Mul c (Floor t)) s)"
   1.498 -by pat_completeness auto
   1.499 -termination by (relation "measure num_size") auto
   1.500  
   1.501  lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t"
   1.502    by (induct t rule: simpnum.induct) auto
   1.503 @@ -872,7 +905,8 @@
   1.504  lemma simpnum_numbound0[simp]: "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
   1.505    by (induct t rule: simpnum.induct) auto
   1.506  
   1.507 -fun nozerocoeff:: "num \<Rightarrow> bool" where
   1.508 +fun nozerocoeff:: "num \<Rightarrow> bool"
   1.509 +where
   1.510    "nozerocoeff (C c) = True"
   1.511  | "nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff t)"
   1.512  | "nozerocoeff (CF c s t) = (c \<noteq> 0 \<and> nozerocoeff t)"
   1.513 @@ -1001,7 +1035,8 @@
   1.514    ultimately show ?thesis by blast
   1.515  qed
   1.516  
   1.517 -fun not:: "fm \<Rightarrow> fm" where
   1.518 +fun not:: "fm \<Rightarrow> fm"
   1.519 +where
   1.520    "not (NOT p) = p"
   1.521  | "not T = F"
   1.522  | "not F = T"
   1.523 @@ -1059,12 +1094,13 @@
   1.524    Iff p q)"
   1.525  
   1.526  lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)"
   1.527 -  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp)  (cases "not p= q", auto simp add:not)
   1.528 +  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp)  (cases "not p= q", auto)
   1.529  
   1.530  lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
   1.531    by (unfold iff_def,cases "p=q", auto)
   1.532  
   1.533 -fun check_int:: "num \<Rightarrow> bool" where
   1.534 +fun check_int:: "num \<Rightarrow> bool"
   1.535 +where
   1.536    "check_int (C i) = True"
   1.537  | "check_int (Floor t) = True"
   1.538  | "check_int (Mul i t) = check_int t"
   1.539 @@ -1139,14 +1175,15 @@
   1.540    ultimately show ?thesis by blast
   1.541  qed
   1.542  
   1.543 -function (sequential) simpfm :: "fm \<Rightarrow> fm" where
   1.544 +fun simpfm :: "fm \<Rightarrow> fm"
   1.545 +where
   1.546    "simpfm (And p q) = conj (simpfm p) (simpfm q)"
   1.547  | "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   1.548  | "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
   1.549  | "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
   1.550  | "simpfm (NOT p) = not (simpfm p)"
   1.551  | "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F
   1.552 -  | _ \<Rightarrow> Lt (reducecoeff a'))"
   1.553 +    | _ \<Rightarrow> Lt (reducecoeff a'))"
   1.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'))"
   1.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'))"
   1.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'))"
   1.557 @@ -1159,8 +1196,6 @@
   1.558               else if (\<bar>i\<bar> = 1) \<and> check_int a then F
   1.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))"
   1.560  | "simpfm p = p"
   1.561 -by pat_completeness auto
   1.562 -termination by (relation "measure fmsize") auto
   1.563  
   1.564  lemma simpfm[simp]: "Ifm bs (simpfm p) = Ifm bs p"
   1.565  proof(induct p rule: simpfm.induct)
   1.566 @@ -1414,7 +1449,8 @@
   1.567    with qf show "qfree (CJNB qe p) \<and> Ifm bs (CJNB qe p) = Ifm bs (E p)" by blast
   1.568  qed
   1.569  
   1.570 -function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" where
   1.571 +fun qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   1.572 +where
   1.573    "qelim (E p) = (\<lambda> qe. DJ (CJNB qe) (qelim p qe))"
   1.574  | "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
   1.575  | "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
   1.576 @@ -1423,8 +1459,6 @@
   1.577  | "qelim (Imp p q) = (\<lambda> qe. disj (qelim (NOT p) qe) (qelim q qe))"
   1.578  | "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
   1.579  | "qelim p = (\<lambda> y. simpfm p)"
   1.580 -by pat_completeness auto
   1.581 -termination by (relation "measure fmsize") auto
   1.582  
   1.583  lemma qelim_ci:
   1.584    assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"
   1.585 @@ -1436,7 +1470,8 @@
   1.586  text \<open>The \<open>\<int>\<close> Part\<close>
   1.587  text\<open>Linearity for fm where Bound 0 ranges over \<open>\<int>\<close>\<close>
   1.588  
   1.589 -function zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*) where
   1.590 +fun zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*)
   1.591 +where
   1.592    "zsplit0 (C c) = (0,C c)"
   1.593  | "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"
   1.594  | "zsplit0 (CN n c a) = zsplit0 (Add (Mul c (Bound n)) a)"
   1.595 @@ -1450,8 +1485,6 @@
   1.596                              in (ia-ib, Sub a' b'))"
   1.597  | "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"
   1.598  | "zsplit0 (Floor a) = (let (i',a') =  zsplit0 a in (i',Floor a'))"
   1.599 -by pat_completeness auto
   1.600 -termination by (relation "measure num_size") auto
   1.601  
   1.602  lemma zsplit0_I:
   1.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"
   1.604 @@ -1533,23 +1566,21 @@
   1.605    with na show ?case by simp
   1.606  qed
   1.607  
   1.608 -consts
   1.609 -  iszlfm :: "fm \<Rightarrow> real list \<Rightarrow> bool"   (* Linearity test for fm *)
   1.610 -  zlfm :: "fm \<Rightarrow> fm"       (* Linearity transformation for fm *)
   1.611 -recdef iszlfm "measure size"
   1.612 +fun iszlfm :: "fm \<Rightarrow> real list \<Rightarrow> bool"   (* Linearity test for fm *)
   1.613 +where
   1.614    "iszlfm (And p q) = (\<lambda> bs. iszlfm p bs \<and> iszlfm q bs)"
   1.615 -  "iszlfm (Or p q) = (\<lambda> bs. iszlfm p bs \<and> iszlfm q bs)"
   1.616 -  "iszlfm (Eq  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.617 -  "iszlfm (NEq (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.618 -  "iszlfm (Lt  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.619 -  "iszlfm (Le  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.620 -  "iszlfm (Gt  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.621 -  "iszlfm (Ge  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.622 -  "iszlfm (Dvd i (CN 0 c e)) =
   1.623 +| "iszlfm (Or p q) = (\<lambda> bs. iszlfm p bs \<and> iszlfm q bs)"
   1.624 +| "iszlfm (Eq  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.625 +| "iszlfm (NEq (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.626 +| "iszlfm (Lt  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.627 +| "iszlfm (Le  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.628 +| "iszlfm (Gt  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.629 +| "iszlfm (Ge  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"
   1.630 +| "iszlfm (Dvd i (CN 0 c e)) =
   1.631                   (\<lambda> bs. c>0 \<and> i>0 \<and> numbound0 e \<and> isint e bs)"
   1.632 -  "iszlfm (NDvd i (CN 0 c e))=
   1.633 +| "iszlfm (NDvd i (CN 0 c e))=
   1.634                   (\<lambda> bs. c>0 \<and> i>0 \<and> numbound0 e \<and> isint e bs)"
   1.635 -  "iszlfm p = (\<lambda> bs. isatom p \<and> (bound0 p))"
   1.636 +| "iszlfm p = (\<lambda> bs. isatom p \<and> (bound0 p))"
   1.637  
   1.638  lemma zlin_qfree: "iszlfm p bs \<Longrightarrow> qfree p"
   1.639    by (induct p rule: iszlfm.induct) auto
   1.640 @@ -1569,61 +1600,62 @@
   1.641  lemma disj_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm q bs \<Longrightarrow> iszlfm (disj p q) bs"
   1.642    using disj_def by (cases p,auto)
   1.643  
   1.644 -recdef zlfm "measure fmsize"
   1.645 +fun zlfm :: "fm \<Rightarrow> fm"       (* Linearity transformation for fm *)
   1.646 +where
   1.647    "zlfm (And p q) = conj (zlfm p) (zlfm q)"
   1.648 -  "zlfm (Or p q) = disj (zlfm p) (zlfm q)"
   1.649 -  "zlfm (Imp p q) = disj (zlfm (NOT p)) (zlfm q)"
   1.650 -  "zlfm (Iff p q) = disj (conj (zlfm p) (zlfm q)) (conj (zlfm (NOT p)) (zlfm (NOT q)))"
   1.651 -  "zlfm (Lt a) = (let (c,r) = zsplit0 a in
   1.652 +| "zlfm (Or p q) = disj (zlfm p) (zlfm q)"
   1.653 +| "zlfm (Imp p q) = disj (zlfm (NOT p)) (zlfm q)"
   1.654 +| "zlfm (Iff p q) = disj (conj (zlfm p) (zlfm q)) (conj (zlfm (NOT p)) (zlfm (NOT q)))"
   1.655 +| "zlfm (Lt a) = (let (c,r) = zsplit0 a in
   1.656       if c=0 then Lt r else
   1.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)))
   1.658       else Or (Gt (CN 0 (-c) (Floor(Neg r)))) (And (Eq(CN 0 (-c) (Floor(Neg r)))) (Lt (Add (Floor (Neg r)) r))))"
   1.659 -  "zlfm (Le a) = (let (c,r) = zsplit0 a in
   1.660 +| "zlfm (Le a) = (let (c,r) = zsplit0 a in
   1.661       if c=0 then Le r else
   1.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)))
   1.663       else Or (Ge (CN 0 (-c) (Floor(Neg r)))) (And (Eq(CN 0 (-c) (Floor(Neg r)))) (Lt (Add (Floor (Neg r)) r))))"
   1.664 -  "zlfm (Gt a) = (let (c,r) = zsplit0 a in
   1.665 +| "zlfm (Gt a) = (let (c,r) = zsplit0 a in
   1.666       if c=0 then Gt r else
   1.667       if c>0 then Or (Gt (CN 0 c (Floor r))) (And (Eq (CN 0 c (Floor r))) (Lt (Sub (Floor r) r)))
   1.668       else Or (Lt (CN 0 (-c) (Neg (Floor r)))) (And (Eq(CN 0 (-c) (Neg (Floor r)))) (Lt (Sub (Floor r) r))))"
   1.669 -  "zlfm (Ge a) = (let (c,r) = zsplit0 a in
   1.670 +| "zlfm (Ge a) = (let (c,r) = zsplit0 a in
   1.671       if c=0 then Ge r else
   1.672       if c>0 then Or (Ge (CN 0 c (Floor r))) (And (Eq (CN 0 c (Floor r))) (Lt (Sub (Floor r) r)))
   1.673       else Or (Le (CN 0 (-c) (Neg (Floor r)))) (And (Eq(CN 0 (-c) (Neg (Floor r)))) (Lt (Sub (Floor r) r))))"
   1.674 -  "zlfm (Eq a) = (let (c,r) = zsplit0 a in
   1.675 +| "zlfm (Eq a) = (let (c,r) = zsplit0 a in
   1.676                if c=0 then Eq r else
   1.677        if c>0 then (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Eq (Add (Floor (Neg r)) r)))
   1.678        else (And (Eq (CN 0 (-c) (Floor (Neg r)))) (Eq (Add (Floor (Neg r)) r))))"
   1.679 -  "zlfm (NEq a) = (let (c,r) = zsplit0 a in
   1.680 +| "zlfm (NEq a) = (let (c,r) = zsplit0 a in
   1.681                if c=0 then NEq r else
   1.682        if c>0 then (Or (NEq (CN 0 c (Neg (Floor (Neg r))))) (NEq (Add (Floor (Neg r)) r)))
   1.683        else (Or (NEq (CN 0 (-c) (Floor (Neg r)))) (NEq (Add (Floor (Neg r)) r))))"
   1.684 -  "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
   1.685 +| "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
   1.686    else (let (c,r) = zsplit0 a in
   1.687                if c=0 then Dvd \<bar>i\<bar> r else
   1.688        if c>0 then And (Eq (Sub (Floor r) r)) (Dvd \<bar>i\<bar> (CN 0 c (Floor r)))
   1.689        else And (Eq (Sub (Floor r) r)) (Dvd \<bar>i\<bar> (CN 0 (-c) (Neg (Floor r))))))"
   1.690 -  "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
   1.691 +| "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
   1.692    else (let (c,r) = zsplit0 a in
   1.693                if c=0 then NDvd \<bar>i\<bar> r else
   1.694        if c>0 then Or (NEq (Sub (Floor r) r)) (NDvd \<bar>i\<bar> (CN 0 c (Floor r)))
   1.695        else Or (NEq (Sub (Floor r) r)) (NDvd \<bar>i\<bar> (CN 0 (-c) (Neg (Floor r))))))"
   1.696 -  "zlfm (NOT (And p q)) = disj (zlfm (NOT p)) (zlfm (NOT q))"
   1.697 -  "zlfm (NOT (Or p q)) = conj (zlfm (NOT p)) (zlfm (NOT q))"
   1.698 -  "zlfm (NOT (Imp p q)) = conj (zlfm p) (zlfm (NOT q))"
   1.699 -  "zlfm (NOT (Iff p q)) = disj (conj(zlfm p) (zlfm(NOT q))) (conj (zlfm(NOT p)) (zlfm q))"
   1.700 -  "zlfm (NOT (NOT p)) = zlfm p"
   1.701 -  "zlfm (NOT T) = F"
   1.702 -  "zlfm (NOT F) = T"
   1.703 -  "zlfm (NOT (Lt a)) = zlfm (Ge a)"
   1.704 -  "zlfm (NOT (Le a)) = zlfm (Gt a)"
   1.705 -  "zlfm (NOT (Gt a)) = zlfm (Le a)"
   1.706 -  "zlfm (NOT (Ge a)) = zlfm (Lt a)"
   1.707 -  "zlfm (NOT (Eq a)) = zlfm (NEq a)"
   1.708 -  "zlfm (NOT (NEq a)) = zlfm (Eq a)"
   1.709 -  "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
   1.710 -  "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
   1.711 -  "zlfm p = p" (hints simp add: fmsize_pos)
   1.712 +| "zlfm (NOT (And p q)) = disj (zlfm (NOT p)) (zlfm (NOT q))"
   1.713 +| "zlfm (NOT (Or p q)) = conj (zlfm (NOT p)) (zlfm (NOT q))"
   1.714 +| "zlfm (NOT (Imp p q)) = conj (zlfm p) (zlfm (NOT q))"
   1.715 +| "zlfm (NOT (Iff p q)) = disj (conj(zlfm p) (zlfm(NOT q))) (conj (zlfm(NOT p)) (zlfm q))"
   1.716 +| "zlfm (NOT (NOT p)) = zlfm p"
   1.717 +| "zlfm (NOT T) = F"
   1.718 +| "zlfm (NOT F) = T"
   1.719 +| "zlfm (NOT (Lt a)) = zlfm (Ge a)"
   1.720 +| "zlfm (NOT (Le a)) = zlfm (Gt a)"
   1.721 +| "zlfm (NOT (Gt a)) = zlfm (Le a)"
   1.722 +| "zlfm (NOT (Ge a)) = zlfm (Lt a)"
   1.723 +| "zlfm (NOT (Eq a)) = zlfm (NEq a)"
   1.724 +| "zlfm (NOT (NEq a)) = zlfm (Eq a)"
   1.725 +| "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
   1.726 +| "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
   1.727 +| "zlfm p = p"
   1.728  
   1.729  lemma split_int_less_real:
   1.730    "(real_of_int (a::int) < b) = (a < \<lfloor>b\<rfloor> \<or> (a = \<lfloor>b\<rfloor> \<and> real_of_int \<lfloor>b\<rfloor> < b))"
   1.731 @@ -1944,7 +1976,8 @@
   1.732         \<open>\<delta>\<close> Compute lcm \<open>d| Dvd d  c*x+t \<in> p\<close>
   1.733         \<open>d_\<delta>\<close> checks if a given l divides all the ds above\<close>
   1.734  
   1.735 -fun minusinf:: "fm \<Rightarrow> fm" where
   1.736 +fun minusinf:: "fm \<Rightarrow> fm"
   1.737 +where
   1.738    "minusinf (And p q) = conj (minusinf p) (minusinf q)"
   1.739  | "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
   1.740  | "minusinf (Eq  (CN 0 c e)) = F"
   1.741 @@ -1958,7 +1991,8 @@
   1.742  lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
   1.743    by (induct p rule: minusinf.induct, auto)
   1.744  
   1.745 -fun plusinf:: "fm \<Rightarrow> fm" where
   1.746 +fun plusinf:: "fm \<Rightarrow> fm"
   1.747 +where
   1.748    "plusinf (And p q) = conj (plusinf p) (plusinf q)"
   1.749  | "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
   1.750  | "plusinf (Eq  (CN 0 c e)) = F"
   1.751 @@ -1969,14 +2003,16 @@
   1.752  | "plusinf (Ge  (CN 0 c e)) = T"
   1.753  | "plusinf p = p"
   1.754  
   1.755 -fun \<delta> :: "fm \<Rightarrow> int" where
   1.756 +fun \<delta> :: "fm \<Rightarrow> int"
   1.757 +where
   1.758    "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)"
   1.759  | "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)"
   1.760  | "\<delta> (Dvd i (CN 0 c e)) = i"
   1.761  | "\<delta> (NDvd i (CN 0 c e)) = i"
   1.762  | "\<delta> p = 1"
   1.763  
   1.764 -fun d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where
   1.765 +fun d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"
   1.766 +where
   1.767    "d_\<delta> (And p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)"
   1.768  | "d_\<delta> (Or p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)"
   1.769  | "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
   1.770 @@ -2237,88 +2273,88 @@
   1.771    from periodic_finite_ex[OF dpos th1] show ?thesis by blast
   1.772  qed
   1.773  
   1.774 -lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto
   1.775 -
   1.776 -consts
   1.777 -  a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coefficients of a formula *)
   1.778 -  d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
   1.779 -  \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
   1.780 -  \<beta> :: "fm \<Rightarrow> num list"
   1.781 -  \<alpha> :: "fm \<Rightarrow> num list"
   1.782 -
   1.783 -recdef a_\<beta> "measure size"
   1.784 +lemma dvd1_eq1: "x > 0 \<Longrightarrow> is_unit x \<longleftrightarrow> x = 1" for x :: int
   1.785 +  by simp
   1.786 +
   1.787 +fun a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coefficients of a formula *)
   1.788 +where
   1.789    "a_\<beta> (And p q) = (\<lambda> k. And (a_\<beta> p k) (a_\<beta> q k))"
   1.790 -  "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))"
   1.791 -  "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
   1.792 -  "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
   1.793 -  "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
   1.794 -  "a_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
   1.795 -  "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
   1.796 -  "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
   1.797 -  "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
   1.798 -  "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
   1.799 -  "a_\<beta> p = (\<lambda> k. p)"
   1.800 -
   1.801 -recdef d_\<beta> "measure size"
   1.802 +| "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))"
   1.803 +| "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
   1.804 +| "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
   1.805 +| "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
   1.806 +| "a_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
   1.807 +| "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
   1.808 +| "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
   1.809 +| "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
   1.810 +| "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
   1.811 +| "a_\<beta> p = (\<lambda> k. p)"
   1.812 +
   1.813 +fun d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
   1.814 +where
   1.815    "d_\<beta> (And p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
   1.816 -  "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
   1.817 -  "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.818 -  "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.819 -  "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.820 -  "d_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.821 -  "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.822 -  "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.823 -  "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
   1.824 -  "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
   1.825 -  "d_\<beta> p = (\<lambda> k. True)"
   1.826 -
   1.827 -recdef \<zeta> "measure size"
   1.828 +| "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
   1.829 +| "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.830 +| "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.831 +| "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.832 +| "d_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.833 +| "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.834 +| "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
   1.835 +| "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
   1.836 +| "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
   1.837 +| "d_\<beta> p = (\<lambda> k. True)"
   1.838 +
   1.839 +fun \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
   1.840 +where
   1.841    "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
   1.842 -  "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
   1.843 -  "\<zeta> (Eq  (CN 0 c e)) = c"
   1.844 -  "\<zeta> (NEq (CN 0 c e)) = c"
   1.845 -  "\<zeta> (Lt  (CN 0 c e)) = c"
   1.846 -  "\<zeta> (Le  (CN 0 c e)) = c"
   1.847 -  "\<zeta> (Gt  (CN 0 c e)) = c"
   1.848 -  "\<zeta> (Ge  (CN 0 c e)) = c"
   1.849 -  "\<zeta> (Dvd i (CN 0 c e)) = c"
   1.850 -  "\<zeta> (NDvd i (CN 0 c e))= c"
   1.851 -  "\<zeta> p = 1"
   1.852 -
   1.853 -recdef \<beta> "measure size"
   1.854 +| "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
   1.855 +| "\<zeta> (Eq  (CN 0 c e)) = c"
   1.856 +| "\<zeta> (NEq (CN 0 c e)) = c"
   1.857 +| "\<zeta> (Lt  (CN 0 c e)) = c"
   1.858 +| "\<zeta> (Le  (CN 0 c e)) = c"
   1.859 +| "\<zeta> (Gt  (CN 0 c e)) = c"
   1.860 +| "\<zeta> (Ge  (CN 0 c e)) = c"
   1.861 +| "\<zeta> (Dvd i (CN 0 c e)) = c"
   1.862 +| "\<zeta> (NDvd i (CN 0 c e))= c"
   1.863 +| "\<zeta> p = 1"
   1.864 +
   1.865 +fun \<beta> :: "fm \<Rightarrow> num list"
   1.866 +where
   1.867    "\<beta> (And p q) = (\<beta> p @ \<beta> q)"
   1.868 -  "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
   1.869 -  "\<beta> (Eq  (CN 0 c e)) = [Sub (C (- 1)) e]"
   1.870 -  "\<beta> (NEq (CN 0 c e)) = [Neg e]"
   1.871 -  "\<beta> (Lt  (CN 0 c e)) = []"
   1.872 -  "\<beta> (Le  (CN 0 c e)) = []"
   1.873 -  "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
   1.874 -  "\<beta> (Ge  (CN 0 c e)) = [Sub (C (- 1)) e]"
   1.875 -  "\<beta> p = []"
   1.876 -
   1.877 -recdef \<alpha> "measure size"
   1.878 +| "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
   1.879 +| "\<beta> (Eq  (CN 0 c e)) = [Sub (C (- 1)) e]"
   1.880 +| "\<beta> (NEq (CN 0 c e)) = [Neg e]"
   1.881 +| "\<beta> (Lt  (CN 0 c e)) = []"
   1.882 +| "\<beta> (Le  (CN 0 c e)) = []"
   1.883 +| "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
   1.884 +| "\<beta> (Ge  (CN 0 c e)) = [Sub (C (- 1)) e]"
   1.885 +| "\<beta> p = []"
   1.886 +
   1.887 +fun \<alpha> :: "fm \<Rightarrow> num list"
   1.888 +where
   1.889    "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)"
   1.890 -  "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)"
   1.891 -  "\<alpha> (Eq  (CN 0 c e)) = [Add (C (- 1)) e]"
   1.892 -  "\<alpha> (NEq (CN 0 c e)) = [e]"
   1.893 -  "\<alpha> (Lt  (CN 0 c e)) = [e]"
   1.894 -  "\<alpha> (Le  (CN 0 c e)) = [Add (C (- 1)) e]"
   1.895 -  "\<alpha> (Gt  (CN 0 c e)) = []"
   1.896 -  "\<alpha> (Ge  (CN 0 c e)) = []"
   1.897 -  "\<alpha> p = []"
   1.898 -consts mirror :: "fm \<Rightarrow> fm"
   1.899 -recdef mirror "measure size"
   1.900 +| "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)"
   1.901 +| "\<alpha> (Eq  (CN 0 c e)) = [Add (C (- 1)) e]"
   1.902 +| "\<alpha> (NEq (CN 0 c e)) = [e]"
   1.903 +| "\<alpha> (Lt  (CN 0 c e)) = [e]"
   1.904 +| "\<alpha> (Le  (CN 0 c e)) = [Add (C (- 1)) e]"
   1.905 +| "\<alpha> (Gt  (CN 0 c e)) = []"
   1.906 +| "\<alpha> (Ge  (CN 0 c e)) = []"
   1.907 +| "\<alpha> p = []"
   1.908 +
   1.909 +fun mirror :: "fm \<Rightarrow> fm"
   1.910 +where
   1.911    "mirror (And p q) = And (mirror p) (mirror q)"
   1.912 -  "mirror (Or p q) = Or (mirror p) (mirror q)"
   1.913 -  "mirror (Eq  (CN 0 c e)) = Eq (CN 0 c (Neg e))"
   1.914 -  "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
   1.915 -  "mirror (Lt  (CN 0 c e)) = Gt (CN 0 c (Neg e))"
   1.916 -  "mirror (Le  (CN 0 c e)) = Ge (CN 0 c (Neg e))"
   1.917 -  "mirror (Gt  (CN 0 c e)) = Lt (CN 0 c (Neg e))"
   1.918 -  "mirror (Ge  (CN 0 c e)) = Le (CN 0 c (Neg e))"
   1.919 -  "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
   1.920 -  "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
   1.921 -  "mirror p = p"
   1.922 +| "mirror (Or p q) = Or (mirror p) (mirror q)"
   1.923 +| "mirror (Eq  (CN 0 c e)) = Eq (CN 0 c (Neg e))"
   1.924 +| "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
   1.925 +| "mirror (Lt  (CN 0 c e)) = Gt (CN 0 c (Neg e))"
   1.926 +| "mirror (Le  (CN 0 c e)) = Ge (CN 0 c (Neg e))"
   1.927 +| "mirror (Gt  (CN 0 c e)) = Lt (CN 0 c (Neg e))"
   1.928 +| "mirror (Ge  (CN 0 c e)) = Le (CN 0 c (Neg e))"
   1.929 +| "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
   1.930 +| "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
   1.931 +| "mirror p = p"
   1.932  
   1.933  lemma mirror_\<alpha>_\<beta>:
   1.934    assumes lp: "iszlfm p (a#bs)"
   1.935 @@ -2770,51 +2806,49 @@
   1.936      (* Reddy and Loveland *)
   1.937  
   1.938  
   1.939 -consts
   1.940 -  \<rho> :: "fm \<Rightarrow> (num \<times> int) list" (* Compute the Reddy and Loveland Bset*)
   1.941 -  \<sigma>_\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
   1.942 -  \<alpha>_\<rho> :: "fm \<Rightarrow> (num\<times>int) list"
   1.943 -  a_\<rho> :: "fm \<Rightarrow> int \<Rightarrow> fm"
   1.944 -recdef \<rho> "measure size"
   1.945 +fun \<rho> :: "fm \<Rightarrow> (num \<times> int) list" (* Compute the Reddy and Loveland Bset*)
   1.946 +  where
   1.947    "\<rho> (And p q) = (\<rho> p @ \<rho> q)"
   1.948 -  "\<rho> (Or p q) = (\<rho> p @ \<rho> q)"
   1.949 -  "\<rho> (Eq  (CN 0 c e)) = [(Sub (C (- 1)) e,c)]"
   1.950 -  "\<rho> (NEq (CN 0 c e)) = [(Neg e,c)]"
   1.951 -  "\<rho> (Lt  (CN 0 c e)) = []"
   1.952 -  "\<rho> (Le  (CN 0 c e)) = []"
   1.953 -  "\<rho> (Gt  (CN 0 c e)) = [(Neg e, c)]"
   1.954 -  "\<rho> (Ge  (CN 0 c e)) = [(Sub (C (-1)) e, c)]"
   1.955 -  "\<rho> p = []"
   1.956 -
   1.957 -recdef \<sigma>_\<rho> "measure size"
   1.958 +| "\<rho> (Or p q) = (\<rho> p @ \<rho> q)"
   1.959 +| "\<rho> (Eq  (CN 0 c e)) = [(Sub (C (- 1)) e,c)]"
   1.960 +| "\<rho> (NEq (CN 0 c e)) = [(Neg e,c)]"
   1.961 +| "\<rho> (Lt  (CN 0 c e)) = []"
   1.962 +| "\<rho> (Le  (CN 0 c e)) = []"
   1.963 +| "\<rho> (Gt  (CN 0 c e)) = [(Neg e, c)]"
   1.964 +| "\<rho> (Ge  (CN 0 c e)) = [(Sub (C (-1)) e, c)]"
   1.965 +| "\<rho> p = []"
   1.966 +
   1.967 +fun \<sigma>_\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
   1.968 +where
   1.969    "\<sigma>_\<rho> (And p q) = (\<lambda> (t,k). And (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
   1.970 -  "\<sigma>_\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
   1.971 -  "\<sigma>_\<rho> (Eq  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e))
   1.972 +| "\<sigma>_\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
   1.973 +| "\<sigma>_\<rho> (Eq  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e))
   1.974                                              else (Eq (Add (Mul c t) (Mul k e))))"
   1.975 -  "\<sigma>_\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e))
   1.976 +| "\<sigma>_\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e))
   1.977                                              else (NEq (Add (Mul c t) (Mul k e))))"
   1.978 -  "\<sigma>_\<rho> (Lt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e))
   1.979 +| "\<sigma>_\<rho> (Lt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e))
   1.980                                              else (Lt (Add (Mul c t) (Mul k e))))"
   1.981 -  "\<sigma>_\<rho> (Le  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e))
   1.982 +| "\<sigma>_\<rho> (Le  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e))
   1.983                                              else (Le (Add (Mul c t) (Mul k e))))"
   1.984 -  "\<sigma>_\<rho> (Gt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e))
   1.985 +| "\<sigma>_\<rho> (Gt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e))
   1.986                                              else (Gt (Add (Mul c t) (Mul k e))))"
   1.987 -  "\<sigma>_\<rho> (Ge  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e))
   1.988 +| "\<sigma>_\<rho> (Ge  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e))
   1.989                                              else (Ge (Add (Mul c t) (Mul k e))))"
   1.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))
   1.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))
   1.992                                              else (Dvd (i*k) (Add (Mul c t) (Mul k e))))"
   1.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))
   1.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))
   1.995                                              else (NDvd (i*k) (Add (Mul c t) (Mul k e))))"
   1.996 -  "\<sigma>_\<rho> p = (\<lambda> (t,k). p)"
   1.997 -
   1.998 -recdef \<alpha>_\<rho> "measure size"
   1.999 +| "\<sigma>_\<rho> p = (\<lambda> (t,k). p)"
  1.1000 +
  1.1001 +fun \<alpha>_\<rho> :: "fm \<Rightarrow> (num \<times> int) list"
  1.1002 +where
  1.1003    "\<alpha>_\<rho> (And p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
  1.1004 -  "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
  1.1005 -  "\<alpha>_\<rho> (Eq  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
  1.1006 -  "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
  1.1007 -  "\<alpha>_\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
  1.1008 -  "\<alpha>_\<rho> (Le  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
  1.1009 -  "\<alpha>_\<rho> p = []"
  1.1010 +| "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
  1.1011 +| "\<alpha>_\<rho> (Eq  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
  1.1012 +| "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
  1.1013 +| "\<alpha>_\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
  1.1014 +| "\<alpha>_\<rho> (Le  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
  1.1015 +| "\<alpha>_\<rho> p = []"
  1.1016  
  1.1017      (* Simulates normal substituion by modifying the formula see correctness theorem *)
  1.1018  
  1.1019 @@ -3277,18 +3311,17 @@
  1.1020  text \<open>The \<open>\<real>\<close> part\<close>
  1.1021  
  1.1022  text\<open>Linearity for fm where Bound 0 ranges over \<open>\<real>\<close>\<close>
  1.1023 -consts
  1.1024 -  isrlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
  1.1025 -recdef isrlfm "measure size"
  1.1026 +fun isrlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
  1.1027 +where
  1.1028    "isrlfm (And p q) = (isrlfm p \<and> isrlfm q)"
  1.1029 -  "isrlfm (Or p q) = (isrlfm p \<and> isrlfm q)"
  1.1030 -  "isrlfm (Eq  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1031 -  "isrlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1032 -  "isrlfm (Lt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1033 -  "isrlfm (Le  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1034 -  "isrlfm (Gt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1035 -  "isrlfm (Ge  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1036 -  "isrlfm p = (isatom p \<and> (bound0 p))"
  1.1037 +| "isrlfm (Or p q) = (isrlfm p \<and> isrlfm q)"
  1.1038 +| "isrlfm (Eq  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1039 +| "isrlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1040 +| "isrlfm (Lt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1041 +| "isrlfm (Le  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1042 +| "isrlfm (Gt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1043 +| "isrlfm (Ge  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1044 +| "isrlfm p = (isatom p \<and> (bound0 p))"
  1.1045  
  1.1046  definition fp :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> int \<Rightarrow> fm" where
  1.1047    "fp p n s j \<equiv> (if n > 0 then
  1.1048 @@ -3299,7 +3332,8 @@
  1.1049                          (Gt (CN 0 (-n) (Add (Neg s) (Add (Floor s) (C (j + 1)))))))))"
  1.1050  
  1.1051    (* splits the bounded from the unbounded part*)
  1.1052 -function (sequential) rsplit0 :: "num \<Rightarrow> (fm \<times> int \<times> num) list" where
  1.1053 +fun rsplit0 :: "num \<Rightarrow> (fm \<times> int \<times> num) list"
  1.1054 +where
  1.1055    "rsplit0 (Bound 0) = [(T,1,C 0)]"
  1.1056  | "rsplit0 (Add a b) = (let acs = rsplit0 a ; bcs = rsplit0 b
  1.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])"
  1.1058 @@ -3314,8 +3348,6 @@
  1.1059  | "rsplit0 (CF c t s) = rsplit0 (Add (Mul c (Floor t)) s)"
  1.1060  | "rsplit0 (Mul c a) = map (\<lambda> (p,n,s). (p,c*n,Mul c s)) (rsplit0 a)"
  1.1061  | "rsplit0 t = [(T,0,t)]"
  1.1062 -by pat_completeness auto
  1.1063 -termination by (relation "measure num_size") auto
  1.1064  
  1.1065  lemma conj_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)"
  1.1066    using conj_def by (cases p, auto)
  1.1067 @@ -3914,36 +3946,36 @@
  1.1068    by (rule rsplit_l[where f="NDVD i" and a="a"], auto simp add: NDVD_def neq_def NDVDJ_l)
  1.1069  (case_tac s, simp_all, rename_tac nat a b, case_tac "nat", simp_all)
  1.1070  
  1.1071 -consts rlfm :: "fm \<Rightarrow> fm"
  1.1072 -recdef rlfm "measure fmsize"
  1.1073 +fun rlfm :: "fm \<Rightarrow> fm"
  1.1074 +where
  1.1075    "rlfm (And p q) = conj (rlfm p) (rlfm q)"
  1.1076 -  "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
  1.1077 -  "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
  1.1078 -  "rlfm (Iff p q) = disj (conj(rlfm p) (rlfm q)) (conj(rlfm (NOT p)) (rlfm (NOT q)))"
  1.1079 -  "rlfm (Lt a) = rsplit lt a"
  1.1080 -  "rlfm (Le a) = rsplit le a"
  1.1081 -  "rlfm (Gt a) = rsplit gt a"
  1.1082 -  "rlfm (Ge a) = rsplit ge a"
  1.1083 -  "rlfm (Eq a) = rsplit eq a"
  1.1084 -  "rlfm (NEq a) = rsplit neq a"
  1.1085 -  "rlfm (Dvd i a) = rsplit (\<lambda> t. DVD i t) a"
  1.1086 -  "rlfm (NDvd i a) = rsplit (\<lambda> t. NDVD i t) a"
  1.1087 -  "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
  1.1088 -  "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
  1.1089 -  "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
  1.1090 -  "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
  1.1091 -  "rlfm (NOT (NOT p)) = rlfm p"
  1.1092 -  "rlfm (NOT T) = F"
  1.1093 -  "rlfm (NOT F) = T"
  1.1094 -  "rlfm (NOT (Lt a)) = simpfm (rlfm (Ge a))"
  1.1095 -  "rlfm (NOT (Le a)) = simpfm (rlfm (Gt a))"
  1.1096 -  "rlfm (NOT (Gt a)) = simpfm (rlfm (Le a))"
  1.1097 -  "rlfm (NOT (Ge a)) = simpfm (rlfm (Lt a))"
  1.1098 -  "rlfm (NOT (Eq a)) = simpfm (rlfm (NEq a))"
  1.1099 -  "rlfm (NOT (NEq a)) = simpfm (rlfm (Eq a))"
  1.1100 -  "rlfm (NOT (Dvd i a)) = simpfm (rlfm (NDvd i a))"
  1.1101 -  "rlfm (NOT (NDvd i a)) = simpfm (rlfm (Dvd i a))"
  1.1102 -  "rlfm p = p" (hints simp add: fmsize_pos)
  1.1103 +| "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
  1.1104 +| "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
  1.1105 +| "rlfm (Iff p q) = disj (conj(rlfm p) (rlfm q)) (conj(rlfm (NOT p)) (rlfm (NOT q)))"
  1.1106 +| "rlfm (Lt a) = rsplit lt a"
  1.1107 +| "rlfm (Le a) = rsplit le a"
  1.1108 +| "rlfm (Gt a) = rsplit gt a"
  1.1109 +| "rlfm (Ge a) = rsplit ge a"
  1.1110 +| "rlfm (Eq a) = rsplit eq a"
  1.1111 +| "rlfm (NEq a) = rsplit neq a"
  1.1112 +| "rlfm (Dvd i a) = rsplit (\<lambda> t. DVD i t) a"
  1.1113 +| "rlfm (NDvd i a) = rsplit (\<lambda> t. NDVD i t) a"
  1.1114 +| "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
  1.1115 +| "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
  1.1116 +| "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
  1.1117 +| "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
  1.1118 +| "rlfm (NOT (NOT p)) = rlfm p"
  1.1119 +| "rlfm (NOT T) = F"
  1.1120 +| "rlfm (NOT F) = T"
  1.1121 +| "rlfm (NOT (Lt a)) = simpfm (rlfm (Ge a))"
  1.1122 +| "rlfm (NOT (Le a)) = simpfm (rlfm (Gt a))"
  1.1123 +| "rlfm (NOT (Gt a)) = simpfm (rlfm (Le a))"
  1.1124 +| "rlfm (NOT (Ge a)) = simpfm (rlfm (Lt a))"
  1.1125 +| "rlfm (NOT (Eq a)) = simpfm (rlfm (NEq a))"
  1.1126 +| "rlfm (NOT (NEq a)) = simpfm (rlfm (Eq a))"
  1.1127 +| "rlfm (NOT (Dvd i a)) = simpfm (rlfm (NDvd i a))"
  1.1128 +| "rlfm (NOT (NDvd i a)) = simpfm (rlfm (Dvd i a))"
  1.1129 +| "rlfm p = p"
  1.1130  
  1.1131  lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
  1.1132    by (induct p rule: isrlfm.induct, auto)
  1.1133 @@ -4377,30 +4409,29 @@
  1.1134    ultimately show ?thesis using z_def by auto
  1.1135  qed
  1.1136  
  1.1137 -consts
  1.1138 -  \<Upsilon>:: "fm \<Rightarrow> (num \<times> int) list"
  1.1139 -  \<upsilon> :: "fm \<Rightarrow> (num \<times> int) \<Rightarrow> fm "
  1.1140 -recdef \<Upsilon> "measure size"
  1.1141 +fun \<Upsilon>:: "fm \<Rightarrow> (num \<times> int) list"
  1.1142 +where
  1.1143    "\<Upsilon> (And p q) = (\<Upsilon> p @ \<Upsilon> q)"
  1.1144 -  "\<Upsilon> (Or p q) = (\<Upsilon> p @ \<Upsilon> q)"
  1.1145 -  "\<Upsilon> (Eq  (CN 0 c e)) = [(Neg e,c)]"
  1.1146 -  "\<Upsilon> (NEq (CN 0 c e)) = [(Neg e,c)]"
  1.1147 -  "\<Upsilon> (Lt  (CN 0 c e)) = [(Neg e,c)]"
  1.1148 -  "\<Upsilon> (Le  (CN 0 c e)) = [(Neg e,c)]"
  1.1149 -  "\<Upsilon> (Gt  (CN 0 c e)) = [(Neg e,c)]"
  1.1150 -  "\<Upsilon> (Ge  (CN 0 c e)) = [(Neg e,c)]"
  1.1151 -  "\<Upsilon> p = []"
  1.1152 -
  1.1153 -recdef \<upsilon> "measure size"
  1.1154 +| "\<Upsilon> (Or p q) = (\<Upsilon> p @ \<Upsilon> q)"
  1.1155 +| "\<Upsilon> (Eq  (CN 0 c e)) = [(Neg e,c)]"
  1.1156 +| "\<Upsilon> (NEq (CN 0 c e)) = [(Neg e,c)]"
  1.1157 +| "\<Upsilon> (Lt  (CN 0 c e)) = [(Neg e,c)]"
  1.1158 +| "\<Upsilon> (Le  (CN 0 c e)) = [(Neg e,c)]"
  1.1159 +| "\<Upsilon> (Gt  (CN 0 c e)) = [(Neg e,c)]"
  1.1160 +| "\<Upsilon> (Ge  (CN 0 c e)) = [(Neg e,c)]"
  1.1161 +| "\<Upsilon> p = []"
  1.1162 +
  1.1163 +fun \<upsilon> :: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm"
  1.1164 +where
  1.1165    "\<upsilon> (And p q) = (\<lambda> (t,n). And (\<upsilon> p (t,n)) (\<upsilon> q (t,n)))"
  1.1166 -  "\<upsilon> (Or p q) = (\<lambda> (t,n). Or (\<upsilon> p (t,n)) (\<upsilon> q (t,n)))"
  1.1167 -  "\<upsilon> (Eq (CN 0 c e)) = (\<lambda> (t,n). Eq (Add (Mul c t) (Mul n e)))"
  1.1168 -  "\<upsilon> (NEq (CN 0 c e)) = (\<lambda> (t,n). NEq (Add (Mul c t) (Mul n e)))"
  1.1169 -  "\<upsilon> (Lt (CN 0 c e)) = (\<lambda> (t,n). Lt (Add (Mul c t) (Mul n e)))"
  1.1170 -  "\<upsilon> (Le (CN 0 c e)) = (\<lambda> (t,n). Le (Add (Mul c t) (Mul n e)))"
  1.1171 -  "\<upsilon> (Gt (CN 0 c e)) = (\<lambda> (t,n). Gt (Add (Mul c t) (Mul n e)))"
  1.1172 -  "\<upsilon> (Ge (CN 0 c e)) = (\<lambda> (t,n). Ge (Add (Mul c t) (Mul n e)))"
  1.1173 -  "\<upsilon> p = (\<lambda> (t,n). p)"
  1.1174 +| "\<upsilon> (Or p q) = (\<lambda> (t,n). Or (\<upsilon> p (t,n)) (\<upsilon> q (t,n)))"
  1.1175 +| "\<upsilon> (Eq (CN 0 c e)) = (\<lambda> (t,n). Eq (Add (Mul c t) (Mul n e)))"
  1.1176 +| "\<upsilon> (NEq (CN 0 c e)) = (\<lambda> (t,n). NEq (Add (Mul c t) (Mul n e)))"
  1.1177 +| "\<upsilon> (Lt (CN 0 c e)) = (\<lambda> (t,n). Lt (Add (Mul c t) (Mul n e)))"
  1.1178 +| "\<upsilon> (Le (CN 0 c e)) = (\<lambda> (t,n). Le (Add (Mul c t) (Mul n e)))"
  1.1179 +| "\<upsilon> (Gt (CN 0 c e)) = (\<lambda> (t,n). Gt (Add (Mul c t) (Mul n e)))"
  1.1180 +| "\<upsilon> (Ge (CN 0 c e)) = (\<lambda> (t,n). Ge (Add (Mul c t) (Mul n e)))"
  1.1181 +| "\<upsilon> p = (\<lambda> (t,n). p)"
  1.1182  
  1.1183  lemma \<upsilon>_I: assumes lp: "isrlfm p"
  1.1184    and np: "real_of_int n > 0" and nbt: "numbound0 t"
  1.1185 @@ -4765,7 +4796,8 @@
  1.1186    ultimately show "(\<exists> (i::int) (u::real). 0\<le> u \<and> u< 1 \<and> P (real_of_int i + u))" by blast
  1.1187  qed
  1.1188  
  1.1189 -fun exsplitnum :: "num \<Rightarrow> num" where
  1.1190 +fun exsplitnum :: "num \<Rightarrow> num"
  1.1191 +where
  1.1192    "exsplitnum (C c) = (C c)"
  1.1193  | "exsplitnum (Bound 0) = Add (Bound 0) (Bound 1)"
  1.1194  | "exsplitnum (Bound n) = Bound (n+1)"
  1.1195 @@ -4778,7 +4810,8 @@
  1.1196  | "exsplitnum (CN n c a) = CN (n+1) c (exsplitnum a)"
  1.1197  | "exsplitnum (CF c s t) = CF c (exsplitnum s) (exsplitnum t)"
  1.1198  
  1.1199 -fun exsplit :: "fm \<Rightarrow> fm" where
  1.1200 +fun exsplit :: "fm \<Rightarrow> fm"
  1.1201 +where
  1.1202    "exsplit (Lt a) = Lt (exsplitnum a)"
  1.1203  | "exsplit (Le a) = Le (exsplitnum a)"
  1.1204  | "exsplit (Gt a) = Gt (exsplitnum a)"