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.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.126
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.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.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.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.178
1.179  lemma nummul_nz : "\<And>i. i\<noteq>0 \<Longrightarrow> nozerocoeff a \<Longrightarrow> nozerocoeff (nummul a i)"
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"
```