src/HOL/Decision_Procs/Ferrack.thy
changeset 66809 f6a30d48aab0
parent 66453 cc19f7ca2ed6
child 67118 ccab07d1196c
     1.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  theory Ferrack
     1.6  imports Complex_Main Dense_Linear_Order DP_Library
     1.7 -  "HOL-Library.Code_Target_Numeral" "HOL-Library.Old_Recdef"
     1.8 +  "HOL-Library.Code_Target_Numeral"
     1.9  begin
    1.10  
    1.11  section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, <)\<close>\<close>
    1.12 @@ -13,19 +13,25 @@
    1.13    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    1.14    (*********************************************************************************)
    1.15  
    1.16 -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
    1.17 +datatype (plugins del: size) num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
    1.18    | Mul int num
    1.19  
    1.20 -  (* A size for num to make inductive proofs simpler*)
    1.21 -primrec num_size :: "num \<Rightarrow> nat"
    1.22 +instantiation num :: size
    1.23 +begin
    1.24 +
    1.25 +primrec size_num :: "num \<Rightarrow> nat"
    1.26  where
    1.27 -  "num_size (C c) = 1"
    1.28 -| "num_size (Bound n) = 1"
    1.29 -| "num_size (Neg a) = 1 + num_size a"
    1.30 -| "num_size (Add a b) = 1 + num_size a + num_size b"
    1.31 -| "num_size (Sub a b) = 3 + num_size a + num_size b"
    1.32 -| "num_size (Mul c a) = 1 + num_size a"
    1.33 -| "num_size (CN n c a) = 3 + num_size a "
    1.34 +  "size_num (C c) = 1"
    1.35 +| "size_num (Bound n) = 1"
    1.36 +| "size_num (Neg a) = 1 + size_num a"
    1.37 +| "size_num (Add a b) = 1 + size_num a + size_num b"
    1.38 +| "size_num (Sub a b) = 3 + size_num a + size_num b"
    1.39 +| "size_num (Mul c a) = 1 + size_num a"
    1.40 +| "size_num (CN n c a) = 3 + size_num a "
    1.41 +
    1.42 +instance ..
    1.43 +
    1.44 +end
    1.45  
    1.46    (* Semantics of numeral terms (num) *)
    1.47  primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real"
    1.48 @@ -38,26 +44,37 @@
    1.49  | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
    1.50  | "Inum bs (Mul c a) = (real_of_int c) * Inum bs a"
    1.51      (* FORMULAE *)
    1.52 -datatype fm  =
    1.53 +datatype (plugins del: size) fm  =
    1.54    T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num|
    1.55    NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
    1.56  
    1.57 +instantiation fm :: size
    1.58 +begin
    1.59  
    1.60 -  (* A size for fm *)
    1.61 -fun fmsize :: "fm \<Rightarrow> nat"
    1.62 +primrec size_fm :: "fm \<Rightarrow> nat"
    1.63  where
    1.64 -  "fmsize (NOT p) = 1 + fmsize p"
    1.65 -| "fmsize (And p q) = 1 + fmsize p + fmsize q"
    1.66 -| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    1.67 -| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
    1.68 -| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
    1.69 -| "fmsize (E p) = 1 + fmsize p"
    1.70 -| "fmsize (A p) = 4+ fmsize p"
    1.71 -| "fmsize p = 1"
    1.72 -  (* several lemmas about fmsize *)
    1.73 +  "size_fm (NOT p) = 1 + size_fm p"
    1.74 +| "size_fm (And p q) = 1 + size_fm p + size_fm q"
    1.75 +| "size_fm (Or p q) = 1 + size_fm p + size_fm q"
    1.76 +| "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
    1.77 +| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
    1.78 +| "size_fm (E p) = 1 + size_fm p"
    1.79 +| "size_fm (A p) = 4 + size_fm p"
    1.80 +| "size_fm T = 1"
    1.81 +| "size_fm F = 1"
    1.82 +| "size_fm (Lt _) = 1"
    1.83 +| "size_fm (Le _) = 1"
    1.84 +| "size_fm (Gt _) = 1"
    1.85 +| "size_fm (Ge _) = 1"
    1.86 +| "size_fm (Eq _) = 1"
    1.87 +| "size_fm (NEq _) = 1"
    1.88  
    1.89 -lemma fmsize_pos: "fmsize p > 0"
    1.90 -  by (induct p rule: fmsize.induct) simp_all
    1.91 +instance ..
    1.92 +
    1.93 +end
    1.94 +
    1.95 +lemma size_fm_pos [simp]: "size p > 0" for p :: fm
    1.96 +  by (induct p) simp_all
    1.97  
    1.98    (* Semantics of formulae (fm) *)
    1.99  primrec Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool"
   1.100 @@ -646,33 +663,24 @@
   1.101  lemma reducecoeff_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeff t)"
   1.102    using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)
   1.103  
   1.104 -consts numadd:: "num \<times> num \<Rightarrow> num"
   1.105 -recdef numadd "measure (\<lambda>(t,s). size t + size s)"
   1.106 -  "numadd (CN n1 c1 r1,CN n2 c2 r2) =
   1.107 +fun numadd:: "num \<Rightarrow> num \<Rightarrow> num"
   1.108 +where
   1.109 +  "numadd (CN n1 c1 r1) (CN n2 c2 r2) =
   1.110     (if n1 = n2 then
   1.111      (let c = c1 + c2
   1.112 -     in (if c = 0 then numadd(r1,r2) else CN n1 c (numadd (r1, r2))))
   1.113 -    else if n1 \<le> n2 then (CN n1 c1 (numadd (r1,CN n2 c2 r2)))
   1.114 -    else (CN n2 c2 (numadd (CN n1 c1 r1, r2))))"
   1.115 -  "numadd (CN n1 c1 r1,t) = CN n1 c1 (numadd (r1, t))"
   1.116 -  "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))"
   1.117 -  "numadd (C b1, C b2) = C (b1 + b2)"
   1.118 -  "numadd (a,b) = Add a b"
   1.119 +     in (if c = 0 then numadd r1 r2 else CN n1 c (numadd r1 r2)))
   1.120 +    else if n1 \<le> n2 then (CN n1 c1 (numadd r1 (CN n2 c2 r2)))
   1.121 +    else (CN n2 c2 (numadd (CN n1 c1 r1) r2)))"
   1.122 +| "numadd (CN n1 c1 r1) t = CN n1 c1 (numadd r1 t)"
   1.123 +| "numadd t (CN n2 c2 r2) = CN n2 c2 (numadd t r2)"
   1.124 +| "numadd (C b1) (C b2) = C (b1 + b2)"
   1.125 +| "numadd a b = Add a b"
   1.126  
   1.127 -lemma numadd[simp]: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
   1.128 -  apply (induct t s rule: numadd.induct)
   1.129 -  apply (simp_all add: Let_def)
   1.130 -  apply (case_tac "c1 + c2 = 0")
   1.131 -  apply (case_tac "n1 \<le> n2")
   1.132 -  apply simp_all
   1.133 -  apply (case_tac "n1 = n2")
   1.134 -  apply (simp_all add: algebra_simps)
   1.135 -  apply (simp only: distrib_right[symmetric])
   1.136 -  apply simp
   1.137 -  done
   1.138 +lemma numadd [simp]: "Inum bs (numadd t s) = Inum bs (Add t s)"
   1.139 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff)
   1.140  
   1.141 -lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
   1.142 -  by (induct t s rule: numadd.induct) (auto simp add: Let_def)
   1.143 +lemma numadd_nb [simp]: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd t s)"
   1.144 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def)
   1.145  
   1.146  fun nummul:: "num \<Rightarrow> int \<Rightarrow> num"
   1.147  where
   1.148 @@ -690,7 +698,7 @@
   1.149    where "numneg t = nummul t (- 1)"
   1.150  
   1.151  definition numsub :: "num \<Rightarrow> num \<Rightarrow> num"
   1.152 -  where "numsub s t = (if s = t then C 0 else numadd (s, numneg t))"
   1.153 +  where "numsub s t = (if s = t then C 0 else numadd s (numneg t))"
   1.154  
   1.155  lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)"
   1.156    using numneg_def by simp
   1.157 @@ -709,10 +717,10 @@
   1.158    "simpnum (C j) = C j"
   1.159  | "simpnum (Bound n) = CN n 1 (C 0)"
   1.160  | "simpnum (Neg t) = numneg (simpnum t)"
   1.161 -| "simpnum (Add t s) = numadd (simpnum t,simpnum s)"
   1.162 +| "simpnum (Add t s) = numadd (simpnum t) (simpnum s)"
   1.163  | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
   1.164  | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul (simpnum t) i)"
   1.165 -| "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0), simpnum t))"
   1.166 +| "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0)) (simpnum t))"
   1.167  
   1.168  lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t"
   1.169    by (induct t) simp_all
   1.170 @@ -726,8 +734,8 @@
   1.171  | "nozerocoeff (CN n c t) = (c \<noteq> 0 \<and> nozerocoeff t)"
   1.172  | "nozerocoeff t = True"
   1.173  
   1.174 -lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd (a,b))"
   1.175 -  by (induct a b rule: numadd.induct) (auto simp add: Let_def)
   1.176 +lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd a b)"
   1.177 +  by (induct a b rule: numadd.induct) (simp_all add: Let_def)
   1.178  
   1.179  lemma nummul_nz : "\<And>i. i\<noteq>0 \<Longrightarrow> nozerocoeff a \<Longrightarrow> nozerocoeff (nummul a i)"
   1.180    by (induct a rule: nummul.induct) (auto simp add: Let_def numadd_nz)
   1.181 @@ -856,7 +864,7 @@
   1.182      proof (cases "?g > 1")
   1.183        case False
   1.184        then show ?thesis
   1.185 -        using assms by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)
   1.186 +        using assms by (auto simp add: Let_def simp_num_pair_def)
   1.187      next
   1.188        case g1: True
   1.189        then have g0: "?g > 0" by simp
   1.190 @@ -868,7 +876,7 @@
   1.191        proof cases
   1.192          case 1
   1.193          then show ?thesis
   1.194 -          using assms g1 by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)
   1.195 +          using assms g1 by (auto simp add: Let_def simp_num_pair_def)
   1.196        next
   1.197          case g'1: 2
   1.198          have gpdg: "?g' dvd ?g" by simp
   1.199 @@ -879,7 +887,7 @@
   1.200            by simp
   1.201          then show ?thesis
   1.202            using assms g1 g'1
   1.203 -          by (auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0 simpnum_numbound0)
   1.204 +          by (auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)
   1.205        qed
   1.206      qed
   1.207    qed
   1.208 @@ -985,7 +993,7 @@
   1.209      case 2
   1.210      then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
   1.211    qed
   1.212 -qed (induct p rule: simpfm.induct, simp_all add: conj disj imp iff not)
   1.213 +qed (induct p rule: simpfm.induct, simp_all)
   1.214  
   1.215  
   1.216  lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"
   1.217 @@ -1019,7 +1027,7 @@
   1.218    then have nb: "numbound0 a" by simp
   1.219    then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   1.220    then show ?case by (cases "simpnum a") (auto simp add: Let_def)
   1.221 -qed (auto simp add: disj_def imp_def iff_def conj_def not_bn)
   1.222 +qed (auto simp add: disj_def imp_def iff_def conj_def)
   1.223  
   1.224  lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
   1.225    apply (induct p rule: simpfm.induct)
   1.226 @@ -1027,38 +1035,37 @@
   1.227    apply (case_tac "simpnum a", auto)+
   1.228    done
   1.229  
   1.230 -consts prep :: "fm \<Rightarrow> fm"
   1.231 -recdef prep "measure fmsize"
   1.232 +fun prep :: "fm \<Rightarrow> fm"
   1.233 +where
   1.234    "prep (E T) = T"
   1.235 -  "prep (E F) = F"
   1.236 -  "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
   1.237 -  "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
   1.238 -  "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
   1.239 -  "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
   1.240 -  "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
   1.241 -  "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
   1.242 -  "prep (E p) = E (prep p)"
   1.243 -  "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
   1.244 -  "prep (A p) = prep (NOT (E (NOT p)))"
   1.245 -  "prep (NOT (NOT p)) = prep p"
   1.246 -  "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
   1.247 -  "prep (NOT (A p)) = prep (E (NOT p))"
   1.248 -  "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
   1.249 -  "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
   1.250 -  "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
   1.251 -  "prep (NOT p) = not (prep p)"
   1.252 -  "prep (Or p q) = disj (prep p) (prep q)"
   1.253 -  "prep (And p q) = conj (prep p) (prep q)"
   1.254 -  "prep (Imp p q) = prep (Or (NOT p) q)"
   1.255 -  "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   1.256 -  "prep p = p"
   1.257 -  (hints simp add: fmsize_pos)
   1.258 +| "prep (E F) = F"
   1.259 +| "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
   1.260 +| "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
   1.261 +| "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
   1.262 +| "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
   1.263 +| "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
   1.264 +| "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
   1.265 +| "prep (E p) = E (prep p)"
   1.266 +| "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
   1.267 +| "prep (A p) = prep (NOT (E (NOT p)))"
   1.268 +| "prep (NOT (NOT p)) = prep p"
   1.269 +| "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
   1.270 +| "prep (NOT (A p)) = prep (E (NOT p))"
   1.271 +| "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
   1.272 +| "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
   1.273 +| "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
   1.274 +| "prep (NOT p) = not (prep p)"
   1.275 +| "prep (Or p q) = disj (prep p) (prep q)"
   1.276 +| "prep (And p q) = conj (prep p) (prep q)"
   1.277 +| "prep (Imp p q) = prep (Or (NOT p) q)"
   1.278 +| "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   1.279 +| "prep p = p"
   1.280  
   1.281  lemma prep: "\<And>bs. Ifm bs (prep p) = Ifm bs p"
   1.282    by (induct p rule: prep.induct) auto
   1.283  
   1.284    (* Generic quantifier elimination *)
   1.285 -function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   1.286 +fun qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   1.287  where
   1.288    "qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))"
   1.289  | "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
   1.290 @@ -1068,16 +1075,13 @@
   1.291  | "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
   1.292  | "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
   1.293  | "qelim p = (\<lambda>y. simpfm p)"
   1.294 -  by pat_completeness auto
   1.295 -termination qelim by (relation "measure fmsize") simp_all
   1.296  
   1.297  lemma qelim_ci:
   1.298    assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"
   1.299    shows "\<And>bs. qfree (qelim p qe) \<and> (Ifm bs (qelim p qe) = Ifm bs p)"
   1.300    using qe_inv DJ_qe[OF qe_inv]
   1.301    by (induct p rule: qelim.induct)
   1.302 -    (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
   1.303 -      simpfm simpfm_qf simp del: simpfm.simps)
   1.304 +    (auto simp add: simpfm simpfm_qf simp del: simpfm.simps)
   1.305  
   1.306  fun minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
   1.307  where
   1.308 @@ -1116,7 +1120,7 @@
   1.309  | "isrlfm p = (isatom p \<and> (bound0 p))"
   1.310  
   1.311    (* splits the bounded from the unbounded part*)
   1.312 -function (sequential) rsplit0 :: "num \<Rightarrow> int \<times> num"
   1.313 +fun rsplit0 :: "num \<Rightarrow> int \<times> num"
   1.314  where
   1.315    "rsplit0 (Bound 0) = (1,C 0)"
   1.316  | "rsplit0 (Add a b) = (let (ca,ta) = rsplit0 a; (cb,tb) = rsplit0 b in (ca + cb, Add ta tb))"
   1.317 @@ -1126,8 +1130,6 @@
   1.318  | "rsplit0 (CN 0 c a) = (let (ca,ta) = rsplit0 a in (c + ca, ta))"
   1.319  | "rsplit0 (CN n c a) = (let (ca,ta) = rsplit0 a in (ca, CN n c ta))"
   1.320  | "rsplit0 t = (0,t)"
   1.321 -  by pat_completeness auto
   1.322 -termination rsplit0 by (relation "measure num_size") simp_all
   1.323  
   1.324  lemma rsplit0: "Inum bs ((case_prod (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))"
   1.325  proof (induct t rule: rsplit0.induct)
   1.326 @@ -1222,39 +1224,38 @@
   1.327  lemma disj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (disj p q)"
   1.328    by (auto simp add: disj_def)
   1.329  
   1.330 -consts rlfm :: "fm \<Rightarrow> fm"
   1.331 -recdef rlfm "measure fmsize"
   1.332 +fun rlfm :: "fm \<Rightarrow> fm"
   1.333 +where
   1.334    "rlfm (And p q) = conj (rlfm p) (rlfm q)"
   1.335 -  "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
   1.336 -  "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
   1.337 -  "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))"
   1.338 -  "rlfm (Lt a) = case_prod lt (rsplit0 a)"
   1.339 -  "rlfm (Le a) = case_prod le (rsplit0 a)"
   1.340 -  "rlfm (Gt a) = case_prod gt (rsplit0 a)"
   1.341 -  "rlfm (Ge a) = case_prod ge (rsplit0 a)"
   1.342 -  "rlfm (Eq a) = case_prod eq (rsplit0 a)"
   1.343 -  "rlfm (NEq a) = case_prod neq (rsplit0 a)"
   1.344 -  "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
   1.345 -  "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
   1.346 -  "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
   1.347 -  "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
   1.348 -  "rlfm (NOT (NOT p)) = rlfm p"
   1.349 -  "rlfm (NOT T) = F"
   1.350 -  "rlfm (NOT F) = T"
   1.351 -  "rlfm (NOT (Lt a)) = rlfm (Ge a)"
   1.352 -  "rlfm (NOT (Le a)) = rlfm (Gt a)"
   1.353 -  "rlfm (NOT (Gt a)) = rlfm (Le a)"
   1.354 -  "rlfm (NOT (Ge a)) = rlfm (Lt a)"
   1.355 -  "rlfm (NOT (Eq a)) = rlfm (NEq a)"
   1.356 -  "rlfm (NOT (NEq a)) = rlfm (Eq a)"
   1.357 -  "rlfm p = p"
   1.358 -  (hints simp add: fmsize_pos)
   1.359 +| "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
   1.360 +| "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
   1.361 +| "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))"
   1.362 +| "rlfm (Lt a) = case_prod lt (rsplit0 a)"
   1.363 +| "rlfm (Le a) = case_prod le (rsplit0 a)"
   1.364 +| "rlfm (Gt a) = case_prod gt (rsplit0 a)"
   1.365 +| "rlfm (Ge a) = case_prod ge (rsplit0 a)"
   1.366 +| "rlfm (Eq a) = case_prod eq (rsplit0 a)"
   1.367 +| "rlfm (NEq a) = case_prod neq (rsplit0 a)"
   1.368 +| "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
   1.369 +| "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
   1.370 +| "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
   1.371 +| "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
   1.372 +| "rlfm (NOT (NOT p)) = rlfm p"
   1.373 +| "rlfm (NOT T) = F"
   1.374 +| "rlfm (NOT F) = T"
   1.375 +| "rlfm (NOT (Lt a)) = rlfm (Ge a)"
   1.376 +| "rlfm (NOT (Le a)) = rlfm (Gt a)"
   1.377 +| "rlfm (NOT (Gt a)) = rlfm (Le a)"
   1.378 +| "rlfm (NOT (Ge a)) = rlfm (Lt a)"
   1.379 +| "rlfm (NOT (Eq a)) = rlfm (NEq a)"
   1.380 +| "rlfm (NOT (NEq a)) = rlfm (Eq a)"
   1.381 +| "rlfm p = p"
   1.382  
   1.383  lemma rlfm_I:
   1.384    assumes qfp: "qfree p"
   1.385    shows "(Ifm bs (rlfm p) = Ifm bs p) \<and> isrlfm (rlfm p)"
   1.386    using qfp
   1.387 -  by (induct p rule: rlfm.induct) (auto simp add: lt le gt ge eq neq conj disj conj_lin disj_lin)
   1.388 +  by (induct p rule: rlfm.induct) (auto simp add: lt le gt ge eq neq conj_lin disj_lin)
   1.389  
   1.390      (* Operations needed for Ferrante and Rackoff *)
   1.391  lemma rminusinf_inf:
   1.392 @@ -1555,29 +1556,29 @@
   1.393    ultimately show ?thesis using z_def by auto
   1.394  qed
   1.395  
   1.396 -consts
   1.397 -  uset:: "fm \<Rightarrow> (num \<times> int) list"
   1.398 -  usubst :: "fm \<Rightarrow> (num \<times> int) \<Rightarrow> fm "
   1.399 -recdef uset "measure size"
   1.400 +fun uset :: "fm \<Rightarrow> (num \<times> int) list"
   1.401 +where
   1.402    "uset (And p q) = (uset p @ uset q)"
   1.403 -  "uset (Or p q) = (uset p @ uset q)"
   1.404 -  "uset (Eq  (CN 0 c e)) = [(Neg e,c)]"
   1.405 -  "uset (NEq (CN 0 c e)) = [(Neg e,c)]"
   1.406 -  "uset (Lt  (CN 0 c e)) = [(Neg e,c)]"
   1.407 -  "uset (Le  (CN 0 c e)) = [(Neg e,c)]"
   1.408 -  "uset (Gt  (CN 0 c e)) = [(Neg e,c)]"
   1.409 -  "uset (Ge  (CN 0 c e)) = [(Neg e,c)]"
   1.410 -  "uset p = []"
   1.411 -recdef usubst "measure size"
   1.412 +| "uset (Or p q) = (uset p @ uset q)"
   1.413 +| "uset (Eq  (CN 0 c e)) = [(Neg e,c)]"
   1.414 +| "uset (NEq (CN 0 c e)) = [(Neg e,c)]"
   1.415 +| "uset (Lt  (CN 0 c e)) = [(Neg e,c)]"
   1.416 +| "uset (Le  (CN 0 c e)) = [(Neg e,c)]"
   1.417 +| "uset (Gt  (CN 0 c e)) = [(Neg e,c)]"
   1.418 +| "uset (Ge  (CN 0 c e)) = [(Neg e,c)]"
   1.419 +| "uset p = []"
   1.420 +
   1.421 +fun usubst :: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm"
   1.422 +where
   1.423    "usubst (And p q) = (\<lambda>(t,n). And (usubst p (t,n)) (usubst q (t,n)))"
   1.424 -  "usubst (Or p q) = (\<lambda>(t,n). Or (usubst p (t,n)) (usubst q (t,n)))"
   1.425 -  "usubst (Eq (CN 0 c e)) = (\<lambda>(t,n). Eq (Add (Mul c t) (Mul n e)))"
   1.426 -  "usubst (NEq (CN 0 c e)) = (\<lambda>(t,n). NEq (Add (Mul c t) (Mul n e)))"
   1.427 -  "usubst (Lt (CN 0 c e)) = (\<lambda>(t,n). Lt (Add (Mul c t) (Mul n e)))"
   1.428 -  "usubst (Le (CN 0 c e)) = (\<lambda>(t,n). Le (Add (Mul c t) (Mul n e)))"
   1.429 -  "usubst (Gt (CN 0 c e)) = (\<lambda>(t,n). Gt (Add (Mul c t) (Mul n e)))"
   1.430 -  "usubst (Ge (CN 0 c e)) = (\<lambda>(t,n). Ge (Add (Mul c t) (Mul n e)))"
   1.431 -  "usubst p = (\<lambda>(t, n). p)"
   1.432 +| "usubst (Or p q) = (\<lambda>(t,n). Or (usubst p (t,n)) (usubst q (t,n)))"
   1.433 +| "usubst (Eq (CN 0 c e)) = (\<lambda>(t,n). Eq (Add (Mul c t) (Mul n e)))"
   1.434 +| "usubst (NEq (CN 0 c e)) = (\<lambda>(t,n). NEq (Add (Mul c t) (Mul n e)))"
   1.435 +| "usubst (Lt (CN 0 c e)) = (\<lambda>(t,n). Lt (Add (Mul c t) (Mul n e)))"
   1.436 +| "usubst (Le (CN 0 c e)) = (\<lambda>(t,n). Le (Add (Mul c t) (Mul n e)))"
   1.437 +| "usubst (Gt (CN 0 c e)) = (\<lambda>(t,n). Gt (Add (Mul c t) (Mul n e)))"
   1.438 +| "usubst (Ge (CN 0 c e)) = (\<lambda>(t,n). Ge (Add (Mul c t) (Mul n e)))"
   1.439 +| "usubst p = (\<lambda>(t, n). p)"
   1.440  
   1.441  lemma usubst_I:
   1.442    assumes lp: "isrlfm p"