src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 66809 f6a30d48aab0
parent 66453 cc19f7ca2ed6
child 67123 3fe40ff1b921
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -10,24 +10,29 @@
     1.4    Dense_Linear_Order
     1.5    DP_Library
     1.6    "HOL-Library.Code_Target_Numeral"
     1.7 -  "HOL-Library.Old_Recdef"
     1.8  begin
     1.9  
    1.10  subsection \<open>Terms\<close>
    1.11  
    1.12 -datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
    1.13 +datatype (plugins del: size) tm = CP poly | Bound nat | Add tm tm | Mul poly tm
    1.14    | Neg tm | Sub tm tm | CNP nat poly tm
    1.15  
    1.16 -text \<open>A size for poly to make inductive proofs simpler.\<close>
    1.17 -primrec tmsize :: "tm \<Rightarrow> nat"
    1.18 +instantiation tm :: size
    1.19 +begin
    1.20 +
    1.21 +primrec size_tm :: "tm \<Rightarrow> nat"
    1.22  where
    1.23 -  "tmsize (CP c) = polysize c"
    1.24 -| "tmsize (Bound n) = 1"
    1.25 -| "tmsize (Neg a) = 1 + tmsize a"
    1.26 -| "tmsize (Add a b) = 1 + tmsize a + tmsize b"
    1.27 -| "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
    1.28 -| "tmsize (Mul c a) = 1 + polysize c + tmsize a"
    1.29 -| "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
    1.30 +  "size_tm (CP c) = polysize c"
    1.31 +| "size_tm (Bound n) = 1"
    1.32 +| "size_tm (Neg a) = 1 + size_tm a"
    1.33 +| "size_tm (Add a b) = 1 + size_tm a + size_tm b"
    1.34 +| "size_tm (Sub a b) = 3 + size_tm a + size_tm b"
    1.35 +| "size_tm (Mul c a) = 1 + polysize c + size_tm a"
    1.36 +| "size_tm (CNP n c a) = 3 + polysize c + size_tm a "
    1.37 +
    1.38 +instance ..
    1.39 +
    1.40 +end
    1.41  
    1.42  text \<open>Semantics of terms tm.\<close>
    1.43  primrec Itm :: "'a::{field_char_0,field} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
    1.44 @@ -258,42 +263,42 @@
    1.45  
    1.46  text \<open>Simplification.\<close>
    1.47  
    1.48 -consts tmadd:: "tm \<times> tm \<Rightarrow> tm"
    1.49 -recdef tmadd "measure (\<lambda>(t,s). size t + size s)"
    1.50 -  "tmadd (CNP n1 c1 r1,CNP n2 c2 r2) =
    1.51 +fun tmadd:: "tm \<Rightarrow> tm \<Rightarrow> tm"
    1.52 +where
    1.53 +  "tmadd (CNP n1 c1 r1) (CNP n2 c2 r2) =
    1.54      (if n1 = n2 then
    1.55        let c = c1 +\<^sub>p c2
    1.56 -      in if c = 0\<^sub>p then tmadd(r1,r2) else CNP n1 c (tmadd (r1, r2))
    1.57 -    else if n1 \<le> n2 then (CNP n1 c1 (tmadd (r1,CNP n2 c2 r2)))
    1.58 -    else (CNP n2 c2 (tmadd (CNP n1 c1 r1, r2))))"
    1.59 -  "tmadd (CNP n1 c1 r1, t) = CNP n1 c1 (tmadd (r1, t))"
    1.60 -  "tmadd (t, CNP n2 c2 r2) = CNP n2 c2 (tmadd (t, r2))"
    1.61 -  "tmadd (CP b1, CP b2) = CP (b1 +\<^sub>p b2)"
    1.62 -  "tmadd (a, b) = Add a b"
    1.63 -
    1.64 -lemma tmadd[simp]: "Itm vs bs (tmadd (t, s)) = Itm vs bs (Add t s)"
    1.65 +      in if c = 0\<^sub>p then tmadd r1 r2 else CNP n1 c (tmadd r1 r2)
    1.66 +    else if n1 \<le> n2 then (CNP n1 c1 (tmadd r1 (CNP n2 c2 r2)))
    1.67 +    else (CNP n2 c2 (tmadd (CNP n1 c1 r1) r2)))"
    1.68 +| "tmadd (CNP n1 c1 r1) t = CNP n1 c1 (tmadd r1 t)"
    1.69 +| "tmadd t (CNP n2 c2 r2) = CNP n2 c2 (tmadd t r2)"
    1.70 +| "tmadd (CP b1) (CP b2) = CP (b1 +\<^sub>p b2)"
    1.71 +| "tmadd a b = Add a b"
    1.72 +
    1.73 +lemma tmadd [simp]: "Itm vs bs (tmadd t s) = Itm vs bs (Add t s)"
    1.74    apply (induct t s rule: tmadd.induct)
    1.75    apply (simp_all add: Let_def)
    1.76    apply (case_tac "c1 +\<^sub>p c2 = 0\<^sub>p")
    1.77    apply (case_tac "n1 \<le> n2")
    1.78    apply simp_all
    1.79    apply (case_tac "n1 = n2")
    1.80 -  apply (simp_all add: field_simps)
    1.81 -  apply (simp only: distrib_left[symmetric])
    1.82 -  apply (auto simp del: polyadd simp add: polyadd[symmetric])
    1.83 +  apply (simp_all add: algebra_simps)
    1.84 +  apply (simp only: distrib_left [symmetric] polyadd [symmetric])
    1.85 +  apply simp
    1.86    done
    1.87  
    1.88 -lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd (t, s))"
    1.89 +lemma tmadd_nb0[simp]: "tmbound0 t \<Longrightarrow> tmbound0 s \<Longrightarrow> tmbound0 (tmadd t s)"
    1.90    by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
    1.91  
    1.92 -lemma tmadd_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmadd (t, s))"
    1.93 +lemma tmadd_nb[simp]: "tmbound n t \<Longrightarrow> tmbound n s \<Longrightarrow> tmbound n (tmadd t s)"
    1.94    by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
    1.95  
    1.96 -lemma tmadd_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmadd (t, s))"
    1.97 +lemma tmadd_blt[simp]: "tmboundslt n t \<Longrightarrow> tmboundslt n s \<Longrightarrow> tmboundslt n (tmadd t s)"
    1.98    by (induct t s rule: tmadd.induct) (auto simp add: Let_def)
    1.99  
   1.100  lemma tmadd_allpolys_npoly[simp]:
   1.101 -  "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd(t, s))"
   1.102 +  "allpolys isnpoly t \<Longrightarrow> allpolys isnpoly s \<Longrightarrow> allpolys isnpoly (tmadd t s)"
   1.103    by (induct t s rule: tmadd.induct) (simp_all add: Let_def polyadd_norm)
   1.104  
   1.105  fun tmmul:: "tm \<Rightarrow> poly \<Rightarrow> tm"
   1.106 @@ -323,7 +328,7 @@
   1.107    where "tmneg t \<equiv> tmmul t (C (- 1,1))"
   1.108  
   1.109  definition tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   1.110 -  where "tmsub s t \<equiv> (if s = t then CP 0\<^sub>p else tmadd (s, tmneg t))"
   1.111 +  where "tmsub s t \<equiv> (if s = t then CP 0\<^sub>p else tmadd s (tmneg t))"
   1.112  
   1.113  lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)"
   1.114    using tmneg_def[of t] by simp
   1.115 @@ -367,12 +372,12 @@
   1.116    "simptm (CP j) = CP (polynate j)"
   1.117  | "simptm (Bound n) = CNP n (1)\<^sub>p (CP 0\<^sub>p)"
   1.118  | "simptm (Neg t) = tmneg (simptm t)"
   1.119 -| "simptm (Add t s) = tmadd (simptm t,simptm s)"
   1.120 +| "simptm (Add t s) = tmadd (simptm t) (simptm s)"
   1.121  | "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
   1.122  | "simptm (Mul i t) =
   1.123      (let i' = polynate i in if i' = 0\<^sub>p then CP 0\<^sub>p else tmmul (simptm t) i')"
   1.124  | "simptm (CNP n c t) =
   1.125 -    (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p ), simptm t))"
   1.126 +    (let c' = polynate c in if c' = 0\<^sub>p then simptm t else tmadd (CNP n c' (CP 0\<^sub>p)) (simptm t))"
   1.127  
   1.128  lemma polynate_stupid:
   1.129    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   1.130 @@ -497,24 +502,34 @@
   1.131  
   1.132  subsection \<open>Formulae\<close>
   1.133  
   1.134 -datatype fm  =  T| F| Le tm | Lt tm | Eq tm | NEq tm|
   1.135 -  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
   1.136 -
   1.137 -
   1.138 -text \<open>A size for fm.\<close>
   1.139 -fun fmsize :: "fm \<Rightarrow> nat"
   1.140 +datatype (plugins del: size) fm = T | F | Le tm | Lt tm | Eq tm | NEq tm |
   1.141 +  NOT fm | And fm fm | Or fm fm | Imp fm fm | Iff fm fm | E fm | A fm
   1.142 +
   1.143 +instantiation fm :: size
   1.144 +begin
   1.145 +
   1.146 +primrec size_fm :: "fm \<Rightarrow> nat"
   1.147  where
   1.148 -  "fmsize (NOT p) = 1 + fmsize p"
   1.149 -| "fmsize (And p q) = 1 + fmsize p + fmsize q"
   1.150 -| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
   1.151 -| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
   1.152 -| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
   1.153 -| "fmsize (E p) = 1 + fmsize p"
   1.154 -| "fmsize (A p) = 4+ fmsize p"
   1.155 -| "fmsize p = 1"
   1.156 -
   1.157 -lemma fmsize_pos[termination_simp]: "fmsize p > 0"
   1.158 -  by (induct p rule: fmsize.induct) simp_all
   1.159 +  "size_fm (NOT p) = 1 + size_fm p"
   1.160 +| "size_fm (And p q) = 1 + size_fm p + size_fm q"
   1.161 +| "size_fm (Or p q) = 1 + size_fm p + size_fm q"
   1.162 +| "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
   1.163 +| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
   1.164 +| "size_fm (E p) = 1 + size_fm p"
   1.165 +| "size_fm (A p) = 4 + size_fm p"
   1.166 +| "size_fm T = 1"
   1.167 +| "size_fm F = 1"
   1.168 +| "size_fm (Le _) = 1"
   1.169 +| "size_fm (Lt _) = 1"
   1.170 +| "size_fm (Eq _) = 1"
   1.171 +| "size_fm (NEq _) = 1"
   1.172 +
   1.173 +instance ..
   1.174 +
   1.175 +end
   1.176 +
   1.177 +lemma fmsize_pos [simp]: "size p > 0" for p :: fm
   1.178 +  by (induct p) simp_all
   1.179  
   1.180  text \<open>Semantics of formulae (fm).\<close>
   1.181  primrec Ifm ::"'a::linordered_field list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
   1.182 @@ -1507,30 +1522,30 @@
   1.183      by blast
   1.184  qed
   1.185  
   1.186 -consts simpfm :: "fm \<Rightarrow> fm"
   1.187 -recdef simpfm "measure fmsize"
   1.188 +fun simpfm :: "fm \<Rightarrow> fm"
   1.189 +where
   1.190    "simpfm (Lt t) = simplt (simptm t)"
   1.191 -  "simpfm (Le t) = simple (simptm t)"
   1.192 -  "simpfm (Eq t) = simpeq(simptm t)"
   1.193 -  "simpfm (NEq t) = simpneq(simptm t)"
   1.194 -  "simpfm (And p q) = conj (simpfm p) (simpfm q)"
   1.195 -  "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   1.196 -  "simpfm (Imp p q) = disj (simpfm (NOT p)) (simpfm q)"
   1.197 -  "simpfm (Iff p q) =
   1.198 +| "simpfm (Le t) = simple (simptm t)"
   1.199 +| "simpfm (Eq t) = simpeq(simptm t)"
   1.200 +| "simpfm (NEq t) = simpneq(simptm t)"
   1.201 +| "simpfm (And p q) = conj (simpfm p) (simpfm q)"
   1.202 +| "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   1.203 +| "simpfm (Imp p q) = disj (simpfm (NOT p)) (simpfm q)"
   1.204 +| "simpfm (Iff p q) =
   1.205      disj (conj (simpfm p) (simpfm q)) (conj (simpfm (NOT p)) (simpfm (NOT q)))"
   1.206 -  "simpfm (NOT (And p q)) = disj (simpfm (NOT p)) (simpfm (NOT q))"
   1.207 -  "simpfm (NOT (Or p q)) = conj (simpfm (NOT p)) (simpfm (NOT q))"
   1.208 -  "simpfm (NOT (Imp p q)) = conj (simpfm p) (simpfm (NOT q))"
   1.209 -  "simpfm (NOT (Iff p q)) =
   1.210 +| "simpfm (NOT (And p q)) = disj (simpfm (NOT p)) (simpfm (NOT q))"
   1.211 +| "simpfm (NOT (Or p q)) = conj (simpfm (NOT p)) (simpfm (NOT q))"
   1.212 +| "simpfm (NOT (Imp p q)) = conj (simpfm p) (simpfm (NOT q))"
   1.213 +| "simpfm (NOT (Iff p q)) =
   1.214      disj (conj (simpfm p) (simpfm (NOT q))) (conj (simpfm (NOT p)) (simpfm q))"
   1.215 -  "simpfm (NOT (Eq t)) = simpneq t"
   1.216 -  "simpfm (NOT (NEq t)) = simpeq t"
   1.217 -  "simpfm (NOT (Le t)) = simplt (Neg t)"
   1.218 -  "simpfm (NOT (Lt t)) = simple (Neg t)"
   1.219 -  "simpfm (NOT (NOT p)) = simpfm p"
   1.220 -  "simpfm (NOT T) = F"
   1.221 -  "simpfm (NOT F) = T"
   1.222 -  "simpfm p = p"
   1.223 +| "simpfm (NOT (Eq t)) = simpneq t"
   1.224 +| "simpfm (NOT (NEq t)) = simpeq t"
   1.225 +| "simpfm (NOT (Le t)) = simplt (Neg t)"
   1.226 +| "simpfm (NOT (Lt t)) = simple (Neg t)"
   1.227 +| "simpfm (NOT (NOT p)) = simpfm p"
   1.228 +| "simpfm (NOT T) = F"
   1.229 +| "simpfm (NOT F) = T"
   1.230 +| "simpfm p = p"
   1.231  
   1.232  lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p"
   1.233    by (induct p arbitrary: bs rule: simpfm.induct) auto
   1.234 @@ -1589,39 +1604,38 @@
   1.235    shows "qfree p \<Longrightarrow> islin (simpfm p)"
   1.236    by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin)
   1.237  
   1.238 -consts prep :: "fm \<Rightarrow> fm"
   1.239 -recdef prep "measure fmsize"
   1.240 +fun prep :: "fm \<Rightarrow> fm"
   1.241 +where
   1.242    "prep (E T) = T"
   1.243 -  "prep (E F) = F"
   1.244 -  "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
   1.245 -  "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
   1.246 -  "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
   1.247 -  "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
   1.248 -  "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
   1.249 -  "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
   1.250 -  "prep (E p) = E (prep p)"
   1.251 -  "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
   1.252 -  "prep (A p) = prep (NOT (E (NOT p)))"
   1.253 -  "prep (NOT (NOT p)) = prep p"
   1.254 -  "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
   1.255 -  "prep (NOT (A p)) = prep (E (NOT p))"
   1.256 -  "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
   1.257 -  "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
   1.258 -  "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
   1.259 -  "prep (NOT p) = not (prep p)"
   1.260 -  "prep (Or p q) = disj (prep p) (prep q)"
   1.261 -  "prep (And p q) = conj (prep p) (prep q)"
   1.262 -  "prep (Imp p q) = prep (Or (NOT p) q)"
   1.263 -  "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   1.264 -  "prep p = p"
   1.265 -  (hints simp add: fmsize_pos)
   1.266 +| "prep (E F) = F"
   1.267 +| "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
   1.268 +| "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
   1.269 +| "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
   1.270 +| "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
   1.271 +| "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
   1.272 +| "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
   1.273 +| "prep (E p) = E (prep p)"
   1.274 +| "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
   1.275 +| "prep (A p) = prep (NOT (E (NOT p)))"
   1.276 +| "prep (NOT (NOT p)) = prep p"
   1.277 +| "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
   1.278 +| "prep (NOT (A p)) = prep (E (NOT p))"
   1.279 +| "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
   1.280 +| "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
   1.281 +| "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
   1.282 +| "prep (NOT p) = not (prep p)"
   1.283 +| "prep (Or p q) = disj (prep p) (prep q)"
   1.284 +| "prep (And p q) = conj (prep p) (prep q)"
   1.285 +| "prep (Imp p q) = prep (Or (NOT p) q)"
   1.286 +| "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   1.287 +| "prep p = p"
   1.288  
   1.289  lemma prep: "Ifm vs bs (prep p) = Ifm vs bs p"
   1.290    by (induct p arbitrary: bs rule: prep.induct) auto
   1.291  
   1.292  
   1.293  text \<open>Generic quantifier elimination.\<close>
   1.294 -function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   1.295 +fun qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   1.296  where
   1.297    "qelim (E p) = (\<lambda>qe. DJ (CJNB qe) (qelim p qe))"
   1.298  | "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
   1.299 @@ -1631,8 +1645,6 @@
   1.300  | "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
   1.301  | "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
   1.302  | "qelim p = (\<lambda>y. simpfm p)"
   1.303 -  by pat_completeness simp_all
   1.304 -termination by (relation "measure fmsize") auto
   1.305  
   1.306  lemma qelim:
   1.307    assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))"
   1.308 @@ -2667,7 +2679,7 @@
   1.309      also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (-?s / (2*?d)) + ?r) = 0"
   1.310        using cd(2) mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
   1.311      also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2 * ?d * ?r= 0"
   1.312 -      by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left)
   1.313 +      by (simp add: field_simps distrib_left [of "2*?d"])
   1.314      also have "\<dots> \<longleftrightarrow> - (?a * ?s) + 2*?d*?r = 0"
   1.315        using cd(2) by simp
   1.316      finally show ?thesis
   1.317 @@ -2684,7 +2696,7 @@
   1.318      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (-?t / (2 * ?c)) + ?r) = 0"
   1.319        using cd(1) mult_cancel_left[of "2 * ?c" "(?a * (-?t / (2 * ?c)) + ?r)" 0] by simp
   1.320      also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2 * ?c) / (2 * ?c) + 2 * ?c * ?r= 0"
   1.321 -      by (simp add: field_simps distrib_left[of "2 * ?c"] del: distrib_left)
   1.322 +      by (simp add: field_simps distrib_left [of "2 * ?c"])
   1.323      also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0"
   1.324        using cd(1) by simp
   1.325      finally show ?thesis using cd