recdef -> fun(ction)
authorkrauss
Thu Feb 24 21:54:28 2011 +0100 (2011-02-24)
changeset 41839421a795cee05
parent 41838 c845adaecf98
child 41840 f69045fdc836
recdef -> fun(ction)
src/HOL/Decision_Procs/MIR.thy
     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Feb 24 20:52:05 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Feb 24 21:54:28 2011 +0100
     1.3 @@ -415,36 +415,32 @@
     1.4    using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
     1.5    by (induct p) (simp_all add: nth_pos2 )
     1.6  
     1.7 -consts
     1.8 -  decrnum:: "num \<Rightarrow> num" 
     1.9 -  decr :: "fm \<Rightarrow> fm"
    1.10 -
    1.11 -recdef decrnum "measure size"
    1.12 +fun decrnum:: "num \<Rightarrow> num" where
    1.13    "decrnum (Bound n) = Bound (n - 1)"
    1.14 -  "decrnum (Neg a) = Neg (decrnum a)"
    1.15 -  "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
    1.16 -  "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
    1.17 -  "decrnum (Mul c a) = Mul c (decrnum a)"
    1.18 -  "decrnum (Floor a) = Floor (decrnum a)"
    1.19 -  "decrnum (CN n c a) = CN (n - 1) c (decrnum a)"
    1.20 -  "decrnum (CF c a b) = CF c (decrnum a) (decrnum b)"
    1.21 -  "decrnum a = a"
    1.22 -
    1.23 -recdef decr "measure size"
    1.24 +| "decrnum (Neg a) = Neg (decrnum a)"
    1.25 +| "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
    1.26 +| "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
    1.27 +| "decrnum (Mul c a) = Mul c (decrnum a)"
    1.28 +| "decrnum (Floor a) = Floor (decrnum a)"
    1.29 +| "decrnum (CN n c a) = CN (n - 1) c (decrnum a)"
    1.30 +| "decrnum (CF c a b) = CF c (decrnum a) (decrnum b)"
    1.31 +| "decrnum a = a"
    1.32 +
    1.33 +fun decr :: "fm \<Rightarrow> fm" where
    1.34    "decr (Lt a) = Lt (decrnum a)"
    1.35 -  "decr (Le a) = Le (decrnum a)"
    1.36 -  "decr (Gt a) = Gt (decrnum a)"
    1.37 -  "decr (Ge a) = Ge (decrnum a)"
    1.38 -  "decr (Eq a) = Eq (decrnum a)"
    1.39 -  "decr (NEq a) = NEq (decrnum a)"
    1.40 -  "decr (Dvd i a) = Dvd i (decrnum a)"
    1.41 -  "decr (NDvd i a) = NDvd i (decrnum a)"
    1.42 -  "decr (NOT p) = NOT (decr p)" 
    1.43 -  "decr (And p q) = And (decr p) (decr q)"
    1.44 -  "decr (Or p q) = Or (decr p) (decr q)"
    1.45 -  "decr (Imp p q) = Imp (decr p) (decr q)"
    1.46 -  "decr (Iff p q) = Iff (decr p) (decr q)"
    1.47 -  "decr p = p"
    1.48 +| "decr (Le a) = Le (decrnum a)"
    1.49 +| "decr (Gt a) = Gt (decrnum a)"
    1.50 +| "decr (Ge a) = Ge (decrnum a)"
    1.51 +| "decr (Eq a) = Eq (decrnum a)"
    1.52 +| "decr (NEq a) = NEq (decrnum a)"
    1.53 +| "decr (Dvd i a) = Dvd i (decrnum a)"
    1.54 +| "decr (NDvd i a) = NDvd i (decrnum a)"
    1.55 +| "decr (NOT p) = NOT (decr p)" 
    1.56 +| "decr (And p q) = And (decr p) (decr q)"
    1.57 +| "decr (Or p q) = Or (decr p) (decr q)"
    1.58 +| "decr (Imp p q) = Imp (decr p) (decr q)"
    1.59 +| "decr (Iff p q) = Iff (decr p) (decr q)"
    1.60 +| "decr p = p"
    1.61  
    1.62  lemma decrnum: assumes nb: "numbound0 t"
    1.63    shows "Inum (x#bs) t = Inum bs (decrnum t)"
    1.64 @@ -458,20 +454,18 @@
    1.65  lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
    1.66  by (induct p, simp_all)
    1.67  
    1.68 -consts 
    1.69 -  isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
    1.70 -recdef isatom "measure size"
    1.71 +fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where
    1.72    "isatom T = True"
    1.73 -  "isatom F = True"
    1.74 -  "isatom (Lt a) = True"
    1.75 -  "isatom (Le a) = True"
    1.76 -  "isatom (Gt a) = True"
    1.77 -  "isatom (Ge a) = True"
    1.78 -  "isatom (Eq a) = True"
    1.79 -  "isatom (NEq a) = True"
    1.80 -  "isatom (Dvd i b) = True"
    1.81 -  "isatom (NDvd i b) = True"
    1.82 -  "isatom p = False"
    1.83 +| "isatom F = True"
    1.84 +| "isatom (Lt a) = True"
    1.85 +| "isatom (Le a) = True"
    1.86 +| "isatom (Gt a) = True"
    1.87 +| "isatom (Ge a) = True"
    1.88 +| "isatom (Eq a) = True"
    1.89 +| "isatom (NEq a) = True"
    1.90 +| "isatom (Dvd i b) = True"
    1.91 +| "isatom (NDvd i b) = True"
    1.92 +| "isatom p = False"
    1.93  
    1.94  lemma numsubst0_numbound0: assumes nb: "numbound0 t"
    1.95    shows "numbound0 (numsubst0 t a)"
    1.96 @@ -509,18 +503,16 @@
    1.97    shows "qfree (evaldjf f xs)"
    1.98    using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
    1.99  
   1.100 -consts 
   1.101 -  disjuncts :: "fm \<Rightarrow> fm list" 
   1.102 -  conjuncts :: "fm \<Rightarrow> fm list"
   1.103 -recdef disjuncts "measure size"
   1.104 +fun disjuncts :: "fm \<Rightarrow> fm list" where
   1.105    "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
   1.106 -  "disjuncts F = []"
   1.107 -  "disjuncts p = [p]"
   1.108 -
   1.109 -recdef conjuncts "measure size"
   1.110 +| "disjuncts F = []"
   1.111 +| "disjuncts p = [p]"
   1.112 +
   1.113 +fun conjuncts :: "fm \<Rightarrow> fm list" where
   1.114    "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)"
   1.115 -  "conjuncts T = []"
   1.116 -  "conjuncts p = [p]"
   1.117 +| "conjuncts T = []"
   1.118 +| "conjuncts p = [p]"
   1.119 +
   1.120  lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bs q) = Ifm bs p"
   1.121  by(induct p rule: disjuncts.induct, auto)
   1.122  lemma conjuncts: "(\<forall> q\<in> set (conjuncts p). Ifm bs q) = Ifm bs p"
   1.123 @@ -595,56 +587,49 @@
   1.124    (* Simplification *)
   1.125  
   1.126    (* Algebraic simplifications for nums *)
   1.127 -consts bnds:: "num \<Rightarrow> nat list"
   1.128 -  lex_ns:: "nat list \<times> nat list \<Rightarrow> bool"
   1.129 -recdef bnds "measure size"
   1.130 +fun bnds:: "num \<Rightarrow> nat list" where
   1.131    "bnds (Bound n) = [n]"
   1.132 -  "bnds (CN n c a) = n#(bnds a)"
   1.133 -  "bnds (Neg a) = bnds a"
   1.134 -  "bnds (Add a b) = (bnds a)@(bnds b)"
   1.135 -  "bnds (Sub a b) = (bnds a)@(bnds b)"
   1.136 -  "bnds (Mul i a) = bnds a"
   1.137 -  "bnds (Floor a) = bnds a"
   1.138 -  "bnds (CF c a b) = (bnds a)@(bnds b)"
   1.139 -  "bnds a = []"
   1.140 -recdef lex_ns "measure (\<lambda> (xs,ys). length xs + length ys)"
   1.141 -  "lex_ns ([], ms) = True"
   1.142 -  "lex_ns (ns, []) = False"
   1.143 -  "lex_ns (n#ns, m#ms) = (n<m \<or> ((n = m) \<and> lex_ns (ns,ms))) "
   1.144 +| "bnds (CN n c a) = n#(bnds a)"
   1.145 +| "bnds (Neg a) = bnds a"
   1.146 +| "bnds (Add a b) = (bnds a)@(bnds b)"
   1.147 +| "bnds (Sub a b) = (bnds a)@(bnds b)"
   1.148 +| "bnds (Mul i a) = bnds a"
   1.149 +| "bnds (Floor a) = bnds a"
   1.150 +| "bnds (CF c a b) = (bnds a)@(bnds b)"
   1.151 +| "bnds a = []"
   1.152 +fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool" where
   1.153 +  "lex_ns [] ms = True"
   1.154 +| "lex_ns ns [] = False"
   1.155 +| "lex_ns (n#ns) (m#ms) = (n<m \<or> ((n = m) \<and> lex_ns ns ms)) "
   1.156  definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool" where
   1.157 -  "lex_bnd t s \<equiv> lex_ns (bnds t, bnds s)"
   1.158 -
   1.159 -consts 
   1.160 -  numgcdh:: "num \<Rightarrow> int \<Rightarrow> int"
   1.161 -  reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num"
   1.162 -  dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
   1.163 -consts maxcoeff:: "num \<Rightarrow> int"
   1.164 -recdef maxcoeff "measure size"
   1.165 +  "lex_bnd t s \<equiv> lex_ns (bnds t) (bnds s)"
   1.166 +
   1.167 +fun maxcoeff:: "num \<Rightarrow> int" where
   1.168    "maxcoeff (C i) = abs i"
   1.169 -  "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)"
   1.170 -  "maxcoeff (CF c t s) = max (abs c) (maxcoeff s)"
   1.171 -  "maxcoeff t = 1"
   1.172 +| "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)"
   1.173 +| "maxcoeff (CF c t s) = max (abs c) (maxcoeff s)"
   1.174 +| "maxcoeff t = 1"
   1.175  
   1.176  lemma maxcoeff_pos: "maxcoeff t \<ge> 0"
   1.177    apply (induct t rule: maxcoeff.induct, auto) 
   1.178    done
   1.179  
   1.180 -recdef numgcdh "measure size"
   1.181 +fun numgcdh:: "num \<Rightarrow> int \<Rightarrow> int" where
   1.182    "numgcdh (C i) = (\<lambda>g. gcd i g)"
   1.183 -  "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"
   1.184 -  "numgcdh (CF c s t) = (\<lambda>g. gcd c (numgcdh t g))"
   1.185 -  "numgcdh t = (\<lambda>g. 1)"
   1.186 +| "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"
   1.187 +| "numgcdh (CF c s t) = (\<lambda>g. gcd c (numgcdh t g))"
   1.188 +| "numgcdh t = (\<lambda>g. 1)"
   1.189  
   1.190  definition
   1.191    numgcd :: "num \<Rightarrow> int"
   1.192  where
   1.193    numgcd_def: "numgcd t = numgcdh t (maxcoeff t)"
   1.194  
   1.195 -recdef reducecoeffh "measure size"
   1.196 +fun reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num" where
   1.197    "reducecoeffh (C i) = (\<lambda> g. C (i div g))"
   1.198 -  "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))"
   1.199 -  "reducecoeffh (CF c s t) = (\<lambda> g. CF (c div g)  s (reducecoeffh t g))"
   1.200 -  "reducecoeffh t = (\<lambda>g. t)"
   1.201 +| "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))"
   1.202 +| "reducecoeffh (CF c s t) = (\<lambda> g. CF (c div g)  s (reducecoeffh t g))"
   1.203 +| "reducecoeffh t = (\<lambda>g. t)"
   1.204  
   1.205  definition
   1.206    reducecoeff :: "num \<Rightarrow> num"
   1.207 @@ -653,11 +638,11 @@
   1.208    (let g = numgcd t in 
   1.209    if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)"
   1.210  
   1.211 -recdef dvdnumcoeff "measure size"
   1.212 +fun dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
   1.213    "dvdnumcoeff (C i) = (\<lambda> g. g dvd i)"
   1.214 -  "dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"
   1.215 -  "dvdnumcoeff (CF c s t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"
   1.216 -  "dvdnumcoeff t = (\<lambda>g. False)"
   1.217 +| "dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"
   1.218 +| "dvdnumcoeff (CF c s t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"
   1.219 +| "dvdnumcoeff t = (\<lambda>g. False)"
   1.220  
   1.221  lemma dvdnumcoeff_trans: 
   1.222    assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'"
   1.223 @@ -704,12 +689,11 @@
   1.224    from assms 3 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) 
   1.225  qed (auto simp add: numgcd_def gp)
   1.226  
   1.227 -consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
   1.228 -recdef ismaxcoeff "measure size"
   1.229 +fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
   1.230    "ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)"
   1.231 -  "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"
   1.232 -  "ismaxcoeff (CF c s t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"
   1.233 -  "ismaxcoeff t = (\<lambda>x. True)"
   1.234 +| "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"
   1.235 +| "ismaxcoeff (CF c s t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"
   1.236 +| "ismaxcoeff t = (\<lambda>x. True)"
   1.237  
   1.238  lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'"
   1.239  by (induct t rule: ismaxcoeff.induct, auto)
   1.240 @@ -813,9 +797,7 @@
   1.241  using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)
   1.242  
   1.243  consts
   1.244 -  simpnum:: "num \<Rightarrow> num"
   1.245    numadd:: "num \<times> num \<Rightarrow> num"
   1.246 -  nummul:: "num \<Rightarrow> int \<Rightarrow> num"
   1.247  
   1.248  recdef numadd "measure (\<lambda> (t,s). size t + size s)"
   1.249    "numadd (CN n1 c1 r1,CN n2 c2 r2) =
   1.250 @@ -849,12 +831,12 @@
   1.251  lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
   1.252  by (induct t s rule: numadd.induct, auto simp add: Let_def)
   1.253  
   1.254 -recdef nummul "measure size"
   1.255 +fun nummul:: "num \<Rightarrow> int \<Rightarrow> num" where
   1.256    "nummul (C j) = (\<lambda> i. C (i*j))"
   1.257 -  "nummul (CN n c t) = (\<lambda> i. CN n (c*i) (nummul t i))"
   1.258 -  "nummul (CF c t s) = (\<lambda> i. CF (c*i) t (nummul s i))"
   1.259 -  "nummul (Mul c t) = (\<lambda> i. nummul t (i*c))"
   1.260 -  "nummul t = (\<lambda> i. Mul i t)"
   1.261 +| "nummul (CN n c t) = (\<lambda> i. CN n (c*i) (nummul t i))"
   1.262 +| "nummul (CF c t s) = (\<lambda> i. CF (c*i) t (nummul s i))"
   1.263 +| "nummul (Mul c t) = (\<lambda> i. nummul t (i*c))"
   1.264 +| "nummul t = (\<lambda> i. Mul i t)"
   1.265  
   1.266  lemma nummul[simp]: "\<And> i. Inum bs (nummul t i) = Inum bs (Mul i t)"
   1.267  by (induct t rule: nummul.induct, auto simp add: algebra_simps)
   1.268 @@ -889,16 +871,15 @@
   1.269    finally show ?thesis .
   1.270  qed
   1.271  
   1.272 -consts split_int:: "num \<Rightarrow> num\<times>num"
   1.273 -recdef split_int "measure num_size"
   1.274 +fun split_int:: "num \<Rightarrow> num \<times> num" where
   1.275    "split_int (C c) = (C 0, C c)"
   1.276 -  "split_int (CN n c b) = 
   1.277 +| "split_int (CN n c b) = 
   1.278       (let (bv,bi) = split_int b 
   1.279         in (CN n c bv, bi))"
   1.280 -  "split_int (CF c a b) = 
   1.281 +| "split_int (CF c a b) = 
   1.282       (let (bv,bi) = split_int b 
   1.283         in (bv, CF c a bi))"
   1.284 -  "split_int a = (a,C 0)"
   1.285 +| "split_int a = (a,C 0)"
   1.286  
   1.287  lemma split_int: "\<And>tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti bs"
   1.288  proof (induct t rule: split_int.induct)
   1.289 @@ -958,16 +939,18 @@
   1.290    using split_int_nb[where t="t"]
   1.291    by (cases "fst(split_int t)" , auto simp add: numfloor_def Let_def split_def  numadd_nb)
   1.292  
   1.293 -recdef simpnum "measure num_size"
   1.294 +function simpnum:: "num \<Rightarrow> num" where
   1.295    "simpnum (C j) = C j"
   1.296 -  "simpnum (Bound n) = CN n 1 (C 0)"
   1.297 -  "simpnum (Neg t) = numneg (simpnum t)"
   1.298 -  "simpnum (Add t s) = numadd (simpnum t,simpnum s)"
   1.299 -  "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
   1.300 -  "simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum t) i)"
   1.301 -  "simpnum (Floor t) = numfloor (simpnum t)"
   1.302 -  "simpnum (CN n c t) = (if c=0 then simpnum t else CN n c (simpnum t))"
   1.303 -  "simpnum (CF c t s) = simpnum(Add (Mul c (Floor t)) s)"
   1.304 +| "simpnum (Bound n) = CN n 1 (C 0)"
   1.305 +| "simpnum (Neg t) = numneg (simpnum t)"
   1.306 +| "simpnum (Add t s) = numadd (simpnum t,simpnum s)"
   1.307 +| "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
   1.308 +| "simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum t) i)"
   1.309 +| "simpnum (Floor t) = numfloor (simpnum t)"
   1.310 +| "simpnum (CN n c t) = (if c=0 then simpnum t else CN n c (simpnum t))"
   1.311 +| "simpnum (CF c t s) = simpnum(Add (Mul c (Floor t)) s)"
   1.312 +by pat_completeness auto
   1.313 +termination by (relation "measure num_size") auto
   1.314  
   1.315  lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t"
   1.316  by (induct t rule: simpnum.induct, auto)
   1.317 @@ -976,13 +959,12 @@
   1.318    "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
   1.319  by (induct t rule: simpnum.induct, auto)
   1.320  
   1.321 -consts nozerocoeff:: "num \<Rightarrow> bool"
   1.322 -recdef nozerocoeff "measure size"
   1.323 +fun nozerocoeff:: "num \<Rightarrow> bool" where
   1.324    "nozerocoeff (C c) = True"
   1.325 -  "nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff t)"
   1.326 -  "nozerocoeff (CF c s t) = (c \<noteq> 0 \<and> nozerocoeff t)"
   1.327 -  "nozerocoeff (Mul c t) = (c\<noteq>0 \<and> nozerocoeff t)"
   1.328 -  "nozerocoeff t = True"
   1.329 +| "nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff t)"
   1.330 +| "nozerocoeff (CF c s t) = (c \<noteq> 0 \<and> nozerocoeff t)"
   1.331 +| "nozerocoeff (Mul c t) = (c\<noteq>0 \<and> nozerocoeff t)"
   1.332 +| "nozerocoeff t = True"
   1.333  
   1.334  lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd (a,b))"
   1.335  by (induct a b rule: numadd.induct,auto simp add: Let_def)
   1.336 @@ -1105,22 +1087,21 @@
   1.337    ultimately show ?thesis by blast
   1.338  qed
   1.339  
   1.340 -consts not:: "fm \<Rightarrow> fm"
   1.341 -recdef not "measure size"
   1.342 +fun not:: "fm \<Rightarrow> fm" where
   1.343    "not (NOT p) = p"
   1.344 -  "not T = F"
   1.345 -  "not F = T"
   1.346 -  "not (Lt t) = Ge t"
   1.347 -  "not (Le t) = Gt t"
   1.348 -  "not (Gt t) = Le t"
   1.349 -  "not (Ge t) = Lt t"
   1.350 -  "not (Eq t) = NEq t"
   1.351 -  "not (NEq t) = Eq t"
   1.352 -  "not (Dvd i t) = NDvd i t"
   1.353 -  "not (NDvd i t) = Dvd i t"
   1.354 -  "not (And p q) = Or (not p) (not q)"
   1.355 -  "not (Or p q) = And (not p) (not q)"
   1.356 -  "not p = NOT p"
   1.357 +| "not T = F"
   1.358 +| "not F = T"
   1.359 +| "not (Lt t) = Ge t"
   1.360 +| "not (Le t) = Gt t"
   1.361 +| "not (Gt t) = Le t"
   1.362 +| "not (Ge t) = Lt t"
   1.363 +| "not (Eq t) = NEq t"
   1.364 +| "not (NEq t) = Eq t"
   1.365 +| "not (Dvd i t) = NDvd i t"
   1.366 +| "not (NDvd i t) = Dvd i t"
   1.367 +| "not (And p q) = Or (not p) (not q)"
   1.368 +| "not (Or p q) = And (not p) (not q)"
   1.369 +| "not p = NOT p"
   1.370  lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)"
   1.371    by (induct p) auto
   1.372  lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
   1.373 @@ -1172,15 +1153,14 @@
   1.374  lemma iff_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
   1.375  using iff_def by (unfold iff_def,cases "p=q", auto)
   1.376  
   1.377 -consts check_int:: "num \<Rightarrow> bool"
   1.378 -recdef check_int "measure size"
   1.379 +fun check_int:: "num \<Rightarrow> bool" where
   1.380    "check_int (C i) = True"
   1.381 -  "check_int (Floor t) = True"
   1.382 -  "check_int (Mul i t) = check_int t"
   1.383 -  "check_int (Add t s) = (check_int t \<and> check_int s)"
   1.384 -  "check_int (Neg t) = check_int t"
   1.385 -  "check_int (CF c t s) = check_int s"
   1.386 -  "check_int t = False"
   1.387 +| "check_int (Floor t) = True"
   1.388 +| "check_int (Mul i t) = check_int t"
   1.389 +| "check_int (Add t s) = (check_int t \<and> check_int s)"
   1.390 +| "check_int (Neg t) = check_int t"
   1.391 +| "check_int (CF c t s) = check_int s"
   1.392 +| "check_int t = False"
   1.393  lemma check_int: "check_int t \<Longrightarrow> isint t bs"
   1.394  by (induct t, auto simp add: isint_add isint_Floor isint_Mul isint_neg isint_c isint_CF)
   1.395  
   1.396 @@ -1248,27 +1228,28 @@
   1.397    ultimately show ?thesis by blast
   1.398  qed
   1.399  
   1.400 -consts simpfm :: "fm \<Rightarrow> fm"
   1.401 -recdef simpfm "measure fmsize"
   1.402 +function (sequential) simpfm :: "fm \<Rightarrow> fm" where
   1.403    "simpfm (And p q) = conj (simpfm p) (simpfm q)"
   1.404 -  "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   1.405 -  "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
   1.406 -  "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
   1.407 -  "simpfm (NOT p) = not (simpfm p)"
   1.408 -  "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F 
   1.409 +| "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   1.410 +| "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
   1.411 +| "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
   1.412 +| "simpfm (NOT p) = not (simpfm p)"
   1.413 +| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F 
   1.414    | _ \<Rightarrow> Lt (reducecoeff a'))"
   1.415 -  "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.416 -  "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.417 -  "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.418 -  "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq (reducecoeff a'))"
   1.419 -  "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0)  then T else F | _ \<Rightarrow> NEq (reducecoeff a'))"
   1.420 -  "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a)
   1.421 +| "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.422 +| "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.423 +| "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.424 +| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq (reducecoeff a'))"
   1.425 +| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0)  then T else F | _ \<Rightarrow> NEq (reducecoeff a'))"
   1.426 +| "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a)
   1.427               else if (abs i = 1) \<and> check_int a then T
   1.428               else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v)  then T else F | _ \<Rightarrow> (let (d,t) = simpdvd i a' in Dvd d t))"
   1.429 -  "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a) 
   1.430 +| "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a) 
   1.431               else if (abs i = 1) \<and> check_int a then F
   1.432               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.433 -  "simpfm p = p"
   1.434 +| "simpfm p = p"
   1.435 +by pat_completeness auto
   1.436 +termination by (relation "measure fmsize") auto
   1.437  
   1.438  lemma simpfm[simp]: "Ifm bs (simpfm p) = Ifm bs p"
   1.439  proof(induct p rule: simpfm.induct)
   1.440 @@ -1522,16 +1503,17 @@
   1.441    with qf show "qfree (CJNB qe p) \<and> Ifm bs (CJNB qe p) = Ifm bs (E p)" by blast
   1.442  qed
   1.443  
   1.444 -consts qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   1.445 -recdef qelim "measure fmsize"
   1.446 +function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" where
   1.447    "qelim (E p) = (\<lambda> qe. DJ (CJNB qe) (qelim p qe))"
   1.448 -  "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
   1.449 -  "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
   1.450 -  "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))" 
   1.451 -  "qelim (Or  p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))" 
   1.452 -  "qelim (Imp p q) = (\<lambda> qe. disj (qelim (NOT p) qe) (qelim q qe))"
   1.453 -  "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
   1.454 -  "qelim p = (\<lambda> y. simpfm p)"
   1.455 +| "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
   1.456 +| "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
   1.457 +| "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))" 
   1.458 +| "qelim (Or  p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))" 
   1.459 +| "qelim (Imp p q) = (\<lambda> qe. disj (qelim (NOT p) qe) (qelim q qe))"
   1.460 +| "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
   1.461 +| "qelim p = (\<lambda> y. simpfm p)"
   1.462 +by pat_completeness auto
   1.463 +termination by (relation "measure fmsize") auto
   1.464  
   1.465  lemma qelim_ci:
   1.466    assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"
   1.467 @@ -1542,23 +1524,23 @@
   1.468  
   1.469  text {* The @{text "\<int>"} Part *}
   1.470  text{* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}
   1.471 -consts
   1.472 -  zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*)
   1.473 -recdef zsplit0 "measure num_size"
   1.474 +
   1.475 +function zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*) where
   1.476    "zsplit0 (C c) = (0,C c)"
   1.477 -  "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"
   1.478 -  "zsplit0 (CN n c a) = zsplit0 (Add (Mul c (Bound n)) a)"
   1.479 -  "zsplit0 (CF c a b) = zsplit0 (Add (Mul c (Floor a)) b)"
   1.480 -  "zsplit0 (Neg a) = (let (i',a') =  zsplit0 a in (-i', Neg a'))"
   1.481 -  "zsplit0 (Add a b) = (let (ia,a') =  zsplit0 a ; 
   1.482 +| "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"
   1.483 +| "zsplit0 (CN n c a) = zsplit0 (Add (Mul c (Bound n)) a)"
   1.484 +| "zsplit0 (CF c a b) = zsplit0 (Add (Mul c (Floor a)) b)"
   1.485 +| "zsplit0 (Neg a) = (let (i',a') =  zsplit0 a in (-i', Neg a'))"
   1.486 +| "zsplit0 (Add a b) = (let (ia,a') =  zsplit0 a ; 
   1.487                              (ib,b') =  zsplit0 b 
   1.488                              in (ia+ib, Add a' b'))"
   1.489 -  "zsplit0 (Sub a b) = (let (ia,a') =  zsplit0 a ; 
   1.490 +| "zsplit0 (Sub a b) = (let (ia,a') =  zsplit0 a ; 
   1.491                              (ib,b') =  zsplit0 b 
   1.492                              in (ia-ib, Sub a' b'))"
   1.493 -  "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"
   1.494 -  "zsplit0 (Floor a) = (let (i',a') =  zsplit0 a in (i',Floor a'))"
   1.495 -(hints simp add: Let_def)
   1.496 +| "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"
   1.497 +| "zsplit0 (Floor a) = (let (i',a') =  zsplit0 a in (i',Floor a'))"
   1.498 +by pat_completeness auto
   1.499 +termination by (relation "measure num_size") auto
   1.500  
   1.501  lemma zsplit0_I:
   1.502    shows "\<And> n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((real (x::int)) #bs) (CN 0 n a) = Inum (real x #bs) t) \<and> numbound0 a"
   1.503 @@ -1590,7 +1572,7 @@
   1.504    ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using prems 
   1.505      by (simp add: Let_def split_def)
   1.506    from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
   1.507 -  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \<and> numbound0 xb)" by simp
   1.508 +  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \<and> numbound0 xb)" by blast (*FIXME*)
   1.509    with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   1.510    from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
   1.511    from th3[simplified] th2[simplified] th[simplified] show ?case 
   1.512 @@ -1606,7 +1588,7 @@
   1.513    ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using prems 
   1.514      by (simp add: Let_def split_def)
   1.515    from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
   1.516 -  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \<and> numbound0 xb)" by simp
   1.517 +  from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \<and> numbound0 xb)" by blast (*FIXME*)
   1.518    with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   1.519    from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
   1.520    from th3[simplified] th2[simplified] th[simplified] show ?case 
   1.521 @@ -2052,50 +2034,44 @@
   1.522         @{text "\<delta>"} Compute lcm @{text "d| Dvd d  c*x+t \<in> p"}
   1.523         @{text "d\<delta>"} checks if a given l divides all the ds above*}
   1.524  
   1.525 -consts 
   1.526 -  plusinf:: "fm \<Rightarrow> fm" 
   1.527 -  minusinf:: "fm \<Rightarrow> fm"
   1.528 -  \<delta> :: "fm \<Rightarrow> int" 
   1.529 -  d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"
   1.530 -
   1.531 -recdef minusinf "measure size"
   1.532 +fun minusinf:: "fm \<Rightarrow> fm" where
   1.533    "minusinf (And p q) = conj (minusinf p) (minusinf q)" 
   1.534 -  "minusinf (Or p q) = disj (minusinf p) (minusinf q)" 
   1.535 -  "minusinf (Eq  (CN 0 c e)) = F"
   1.536 -  "minusinf (NEq (CN 0 c e)) = T"
   1.537 -  "minusinf (Lt  (CN 0 c e)) = T"
   1.538 -  "minusinf (Le  (CN 0 c e)) = T"
   1.539 -  "minusinf (Gt  (CN 0 c e)) = F"
   1.540 -  "minusinf (Ge  (CN 0 c e)) = F"
   1.541 -  "minusinf p = p"
   1.542 +| "minusinf (Or p q) = disj (minusinf p) (minusinf q)" 
   1.543 +| "minusinf (Eq  (CN 0 c e)) = F"
   1.544 +| "minusinf (NEq (CN 0 c e)) = T"
   1.545 +| "minusinf (Lt  (CN 0 c e)) = T"
   1.546 +| "minusinf (Le  (CN 0 c e)) = T"
   1.547 +| "minusinf (Gt  (CN 0 c e)) = F"
   1.548 +| "minusinf (Ge  (CN 0 c e)) = F"
   1.549 +| "minusinf p = p"
   1.550  
   1.551  lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
   1.552    by (induct p rule: minusinf.induct, auto)
   1.553  
   1.554 -recdef plusinf "measure size"
   1.555 +fun plusinf:: "fm \<Rightarrow> fm" where
   1.556    "plusinf (And p q) = conj (plusinf p) (plusinf q)" 
   1.557 -  "plusinf (Or p q) = disj (plusinf p) (plusinf q)" 
   1.558 -  "plusinf (Eq  (CN 0 c e)) = F"
   1.559 -  "plusinf (NEq (CN 0 c e)) = T"
   1.560 -  "plusinf (Lt  (CN 0 c e)) = F"
   1.561 -  "plusinf (Le  (CN 0 c e)) = F"
   1.562 -  "plusinf (Gt  (CN 0 c e)) = T"
   1.563 -  "plusinf (Ge  (CN 0 c e)) = T"
   1.564 -  "plusinf p = p"
   1.565 -
   1.566 -recdef \<delta> "measure size"
   1.567 +| "plusinf (Or p q) = disj (plusinf p) (plusinf q)" 
   1.568 +| "plusinf (Eq  (CN 0 c e)) = F"
   1.569 +| "plusinf (NEq (CN 0 c e)) = T"
   1.570 +| "plusinf (Lt  (CN 0 c e)) = F"
   1.571 +| "plusinf (Le  (CN 0 c e)) = F"
   1.572 +| "plusinf (Gt  (CN 0 c e)) = T"
   1.573 +| "plusinf (Ge  (CN 0 c e)) = T"
   1.574 +| "plusinf p = p"
   1.575 +
   1.576 +fun \<delta> :: "fm \<Rightarrow> int" where
   1.577    "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)" 
   1.578 -  "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)" 
   1.579 -  "\<delta> (Dvd i (CN 0 c e)) = i"
   1.580 -  "\<delta> (NDvd i (CN 0 c e)) = i"
   1.581 -  "\<delta> p = 1"
   1.582 -
   1.583 -recdef d\<delta> "measure size"
   1.584 +| "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)" 
   1.585 +| "\<delta> (Dvd i (CN 0 c e)) = i"
   1.586 +| "\<delta> (NDvd i (CN 0 c e)) = i"
   1.587 +| "\<delta> p = 1"
   1.588 +
   1.589 +fun d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where
   1.590    "d\<delta> (And p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 
   1.591 -  "d\<delta> (Or p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 
   1.592 -  "d\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
   1.593 -  "d\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
   1.594 -  "d\<delta> p = (\<lambda> d. True)"
   1.595 +| "d\<delta> (Or p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 
   1.596 +| "d\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
   1.597 +| "d\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
   1.598 +| "d\<delta> p = (\<lambda> d. True)"
   1.599  
   1.600  lemma delta_mono: 
   1.601    assumes lin: "iszlfm p bs"
   1.602 @@ -3517,22 +3493,23 @@
   1.603                          (Gt (CN 0 (-n) (Add (Neg s) (Add (Floor s) (C (j + 1)))))))))"
   1.604  
   1.605    (* splits the bounded from the unbounded part*)
   1.606 -consts rsplit0 :: "num \<Rightarrow> (fm \<times> int \<times> num) list" 
   1.607 -recdef rsplit0 "measure num_size"
   1.608 +function (sequential) rsplit0 :: "num \<Rightarrow> (fm \<times> int \<times> num) list" where
   1.609    "rsplit0 (Bound 0) = [(T,1,C 0)]"
   1.610 -  "rsplit0 (Add a b) = (let acs = rsplit0 a ; bcs = rsplit0 b 
   1.611 +| "rsplit0 (Add a b) = (let acs = rsplit0 a ; bcs = rsplit0 b 
   1.612                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.613 -  "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))"
   1.614 -  "rsplit0 (Neg a) = map (\<lambda> (p,n,s). (p,-n,Neg s)) (rsplit0 a)"
   1.615 -  "rsplit0 (Floor a) = foldl (op @) [] (map 
   1.616 +| "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))"
   1.617 +| "rsplit0 (Neg a) = map (\<lambda> (p,n,s). (p,-n,Neg s)) (rsplit0 a)"
   1.618 +| "rsplit0 (Floor a) = foldl (op @) [] (map 
   1.619        (\<lambda> (p,n,s). if n=0 then [(p,0,Floor s)]
   1.620            else (map (\<lambda> j. (fp p n s j, 0, Add (Floor s) (C j))) (if n > 0 then [0 .. n] else [n .. 0])))
   1.621         (rsplit0 a))"
   1.622 -  "rsplit0 (CN 0 c a) = map (\<lambda> (p,n,s). (p,n+c,s)) (rsplit0 a)"
   1.623 -  "rsplit0 (CN m c a) = map (\<lambda> (p,n,s). (p,n,CN m c s)) (rsplit0 a)"
   1.624 -  "rsplit0 (CF c t s) = rsplit0 (Add (Mul c (Floor t)) s)"
   1.625 -  "rsplit0 (Mul c a) = map (\<lambda> (p,n,s). (p,c*n,Mul c s)) (rsplit0 a)"
   1.626 -  "rsplit0 t = [(T,0,t)]"
   1.627 +| "rsplit0 (CN 0 c a) = map (\<lambda> (p,n,s). (p,n+c,s)) (rsplit0 a)"
   1.628 +| "rsplit0 (CN m c a) = map (\<lambda> (p,n,s). (p,n,CN m c s)) (rsplit0 a)"
   1.629 +| "rsplit0 (CF c t s) = rsplit0 (Add (Mul c (Floor t)) s)"
   1.630 +| "rsplit0 (Mul c a) = map (\<lambda> (p,n,s). (p,c*n,Mul c s)) (rsplit0 a)"
   1.631 +| "rsplit0 t = [(T,0,t)]"
   1.632 +by pat_completeness auto
   1.633 +termination by (relation "measure num_size") auto
   1.634  
   1.635  lemma not_rl[simp]: "isrlfm p \<Longrightarrow> isrlfm (not p)"
   1.636    by (induct p rule: isrlfm.induct, auto)
   1.637 @@ -3697,7 +3674,7 @@
   1.638    case (2 a b) 
   1.639    from prems have "\<exists> (pa,na,sa) \<in> ?SS a. ?I pa" by auto
   1.640    then obtain "pa" "na" "sa" where pa: "(pa,na,sa)\<in> ?SS a \<and> ?I pa" by blast
   1.641 -  from prems have "\<exists> (pb,nb,sb) \<in> ?SS b. ?I pb" by auto
   1.642 +  from prems have "\<exists> (pb,nb,sb) \<in> ?SS b. ?I pb" by blast
   1.643    then obtain "pb" "nb" "sb" where pb: "(pb,nb,sb)\<in> ?SS b \<and> ?I pb" by blast
   1.644    from pa pb have th: "((pa,na,sa),(pb,nb,sb)) \<in> set[(x,y). x\<leftarrow>rsplit0 a, y\<leftarrow>rsplit0 b]"
   1.645      by (auto)
   1.646 @@ -5038,36 +5015,34 @@
   1.647    ultimately show "(\<exists> (i::int) (u::real). 0\<le> u \<and> u< 1 \<and> P (real i + u))" by blast
   1.648  qed
   1.649  
   1.650 -consts exsplitnum :: "num \<Rightarrow> num"
   1.651 -  exsplit :: "fm \<Rightarrow> fm"
   1.652 -recdef exsplitnum "measure size"
   1.653 +fun exsplitnum :: "num \<Rightarrow> num" where
   1.654    "exsplitnum (C c) = (C c)"
   1.655 -  "exsplitnum (Bound 0) = Add (Bound 0) (Bound 1)"
   1.656 -  "exsplitnum (Bound n) = Bound (n+1)"
   1.657 -  "exsplitnum (Neg a) = Neg (exsplitnum a)"
   1.658 -  "exsplitnum (Add a b) = Add (exsplitnum a) (exsplitnum b) "
   1.659 -  "exsplitnum (Sub a b) = Sub (exsplitnum a) (exsplitnum b) "
   1.660 -  "exsplitnum (Mul c a) = Mul c (exsplitnum a)"
   1.661 -  "exsplitnum (Floor a) = Floor (exsplitnum a)"
   1.662 -  "exsplitnum (CN 0 c a) = CN 0 c (Add (Mul c (Bound 1)) (exsplitnum a))"
   1.663 -  "exsplitnum (CN n c a) = CN (n+1) c (exsplitnum a)"
   1.664 -  "exsplitnum (CF c s t) = CF c (exsplitnum s) (exsplitnum t)"
   1.665 -
   1.666 -recdef exsplit "measure size"
   1.667 +| "exsplitnum (Bound 0) = Add (Bound 0) (Bound 1)"
   1.668 +| "exsplitnum (Bound n) = Bound (n+1)"
   1.669 +| "exsplitnum (Neg a) = Neg (exsplitnum a)"
   1.670 +| "exsplitnum (Add a b) = Add (exsplitnum a) (exsplitnum b) "
   1.671 +| "exsplitnum (Sub a b) = Sub (exsplitnum a) (exsplitnum b) "
   1.672 +| "exsplitnum (Mul c a) = Mul c (exsplitnum a)"
   1.673 +| "exsplitnum (Floor a) = Floor (exsplitnum a)"
   1.674 +| "exsplitnum (CN 0 c a) = CN 0 c (Add (Mul c (Bound 1)) (exsplitnum a))"
   1.675 +| "exsplitnum (CN n c a) = CN (n+1) c (exsplitnum a)"
   1.676 +| "exsplitnum (CF c s t) = CF c (exsplitnum s) (exsplitnum t)"
   1.677 +
   1.678 +fun exsplit :: "fm \<Rightarrow> fm" where
   1.679    "exsplit (Lt a) = Lt (exsplitnum a)"
   1.680 -  "exsplit (Le a) = Le (exsplitnum a)"
   1.681 -  "exsplit (Gt a) = Gt (exsplitnum a)"
   1.682 -  "exsplit (Ge a) = Ge (exsplitnum a)"
   1.683 -  "exsplit (Eq a) = Eq (exsplitnum a)"
   1.684 -  "exsplit (NEq a) = NEq (exsplitnum a)"
   1.685 -  "exsplit (Dvd i a) = Dvd i (exsplitnum a)"
   1.686 -  "exsplit (NDvd i a) = NDvd i (exsplitnum a)"
   1.687 -  "exsplit (And p q) = And (exsplit p) (exsplit q)"
   1.688 -  "exsplit (Or p q) = Or (exsplit p) (exsplit q)"
   1.689 -  "exsplit (Imp p q) = Imp (exsplit p) (exsplit q)"
   1.690 -  "exsplit (Iff p q) = Iff (exsplit p) (exsplit q)"
   1.691 -  "exsplit (NOT p) = NOT (exsplit p)"
   1.692 -  "exsplit p = p"
   1.693 +| "exsplit (Le a) = Le (exsplitnum a)"
   1.694 +| "exsplit (Gt a) = Gt (exsplitnum a)"
   1.695 +| "exsplit (Ge a) = Ge (exsplitnum a)"
   1.696 +| "exsplit (Eq a) = Eq (exsplitnum a)"
   1.697 +| "exsplit (NEq a) = NEq (exsplitnum a)"
   1.698 +| "exsplit (Dvd i a) = Dvd i (exsplitnum a)"
   1.699 +| "exsplit (NDvd i a) = NDvd i (exsplitnum a)"
   1.700 +| "exsplit (And p q) = And (exsplit p) (exsplit q)"
   1.701 +| "exsplit (Or p q) = Or (exsplit p) (exsplit q)"
   1.702 +| "exsplit (Imp p q) = Imp (exsplit p) (exsplit q)"
   1.703 +| "exsplit (Iff p q) = Iff (exsplit p) (exsplit q)"
   1.704 +| "exsplit (NOT p) = NOT (exsplit p)"
   1.705 +| "exsplit p = p"
   1.706  
   1.707  lemma exsplitnum: 
   1.708    "Inum (x#y#bs) (exsplitnum t) = Inum ((x+y) #bs) t"