src/HOL/Decision_Procs/Cooper.thy
changeset 66809 f6a30d48aab0
parent 66453 cc19f7ca2ed6
child 67123 3fe40ff1b921
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  imports
     1.5    Complex_Main
     1.6    "HOL-Library.Code_Target_Numeral"
     1.7 -  "HOL-Library.Old_Recdef"
     1.8  begin
     1.9  
    1.10  (* Periodicity of dvd *)
    1.11 @@ -15,50 +14,74 @@
    1.12  (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    1.13  (*********************************************************************************)
    1.14  
    1.15 -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
    1.16 +datatype (plugins del: size) num = C int | Bound nat | CN nat int num
    1.17 +  | Neg num | Add num num | Sub num num
    1.18    | Mul int num
    1.19  
    1.20 -primrec num_size :: "num \<Rightarrow> nat" \<comment> \<open>A size for num to make inductive proofs simpler\<close>
    1.21 +instantiation num :: size
    1.22 +begin
    1.23 +
    1.24 +primrec size_num :: "num \<Rightarrow> nat"
    1.25  where
    1.26 -  "num_size (C c) = 1"
    1.27 -| "num_size (Bound n) = 1"
    1.28 -| "num_size (Neg a) = 1 + num_size a"
    1.29 -| "num_size (Add a b) = 1 + num_size a + num_size b"
    1.30 -| "num_size (Sub a b) = 3 + num_size a + num_size b"
    1.31 -| "num_size (CN n c a) = 4 + num_size a"
    1.32 -| "num_size (Mul c a) = 1 + num_size a"
    1.33 +  "size_num (C c) = 1"
    1.34 +| "size_num (Bound n) = 1"
    1.35 +| "size_num (Neg a) = 1 + size_num a"
    1.36 +| "size_num (Add a b) = 1 + size_num a + size_num b"
    1.37 +| "size_num (Sub a b) = 3 + size_num a + size_num b"
    1.38 +| "size_num (CN n c a) = 4 + size_num a"
    1.39 +| "size_num (Mul c a) = 1 + size_num a"
    1.40 +
    1.41 +instance ..
    1.42 +
    1.43 +end
    1.44  
    1.45  primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int"
    1.46  where
    1.47    "Inum bs (C c) = c"
    1.48 -| "Inum bs (Bound n) = bs!n"
    1.49 -| "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
    1.50 -| "Inum bs (Neg a) = -(Inum bs a)"
    1.51 +| "Inum bs (Bound n) = bs ! n"
    1.52 +| "Inum bs (CN n c a) = c * (bs ! n) + Inum bs a"
    1.53 +| "Inum bs (Neg a) = - Inum bs a"
    1.54  | "Inum bs (Add a b) = Inum bs a + Inum bs b"
    1.55  | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
    1.56 -| "Inum bs (Mul c a) = c* Inum bs a"
    1.57 +| "Inum bs (Mul c a) = c * Inum bs a"
    1.58  
    1.59 -datatype fm  =
    1.60 -  T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
    1.61 -  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
    1.62 -  | Closed nat | NClosed nat
    1.63 +datatype (plugins del: size) fm = T | F
    1.64 +  | Lt num | Le num | Gt num | Ge num | Eq num | NEq num
    1.65 +  | Dvd int num | NDvd int num
    1.66 +  | NOT fm | And fm fm | Or fm fm | Imp fm fm | Iff fm fm
    1.67 +  | E fm | A fm | Closed nat | NClosed nat
    1.68  
    1.69 +instantiation fm :: size
    1.70 +begin
    1.71  
    1.72 -fun fmsize :: "fm \<Rightarrow> nat"  \<comment> \<open>A size for fm\<close>
    1.73 +primrec size_fm :: "fm \<Rightarrow> nat"
    1.74  where
    1.75 -  "fmsize (NOT p) = 1 + fmsize p"
    1.76 -| "fmsize (And p q) = 1 + fmsize p + fmsize q"
    1.77 -| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    1.78 -| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
    1.79 -| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
    1.80 -| "fmsize (E p) = 1 + fmsize p"
    1.81 -| "fmsize (A p) = 4+ fmsize p"
    1.82 -| "fmsize (Dvd i t) = 2"
    1.83 -| "fmsize (NDvd i t) = 2"
    1.84 -| "fmsize p = 1"
    1.85 +  "size_fm (NOT p) = 1 + size_fm p"
    1.86 +| "size_fm (And p q) = 1 + size_fm p + size_fm q"
    1.87 +| "size_fm (Or p q) = 1 + size_fm p + size_fm q"
    1.88 +| "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
    1.89 +| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
    1.90 +| "size_fm (E p) = 1 + size_fm p"
    1.91 +| "size_fm (A p) = 4 + size_fm p"
    1.92 +| "size_fm (Dvd i t) = 2"
    1.93 +| "size_fm (NDvd i t) = 2"
    1.94 +| "size_fm T = 1" 
    1.95 +| "size_fm F = 1"
    1.96 +| "size_fm (Lt _) = 1" 
    1.97 +| "size_fm (Le _) = 1" 
    1.98 +| "size_fm (Gt _) = 1" 
    1.99 +| "size_fm (Ge _) = 1" 
   1.100 +| "size_fm (Eq _) = 1" 
   1.101 +| "size_fm (NEq _) = 1" 
   1.102 +| "size_fm (Closed _) = 1" 
   1.103 +| "size_fm (NClosed _) = 1"
   1.104  
   1.105 -lemma fmsize_pos: "fmsize p > 0"
   1.106 -  by (induct p rule: fmsize.induct) simp_all
   1.107 +instance ..
   1.108 +
   1.109 +end
   1.110 +
   1.111 +lemma fmsize_pos [simp]: "size p > 0" for p :: fm
   1.112 +  by (induct p) simp_all
   1.113  
   1.114  primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  \<comment> \<open>Semantics of formulae (fm)\<close>
   1.115  where
   1.116 @@ -79,10 +102,10 @@
   1.117  | "Ifm bbs bs (Iff p q) \<longleftrightarrow> Ifm bbs bs p = Ifm bbs bs q"
   1.118  | "Ifm bbs bs (E p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) p)"
   1.119  | "Ifm bbs bs (A p) \<longleftrightarrow> (\<forall>x. Ifm bbs (x # bs) p)"
   1.120 -| "Ifm bbs bs (Closed n) \<longleftrightarrow> bbs!n"
   1.121 -| "Ifm bbs bs (NClosed n) \<longleftrightarrow> \<not> bbs!n"
   1.122 +| "Ifm bbs bs (Closed n) \<longleftrightarrow> bbs ! n"
   1.123 +| "Ifm bbs bs (NClosed n) \<longleftrightarrow> \<not> bbs ! n"
   1.124  
   1.125 -function (sequential) prep :: "fm \<Rightarrow> fm"
   1.126 +fun prep :: "fm \<Rightarrow> fm"
   1.127  where
   1.128    "prep (E T) = T"
   1.129  | "prep (E F) = F"
   1.130 @@ -107,10 +130,6 @@
   1.131  | "prep (Imp p q) = prep (Or (NOT p) q)"
   1.132  | "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   1.133  | "prep p = p"
   1.134 -  by pat_completeness auto
   1.135 -
   1.136 -termination
   1.137 -  by (relation "measure fmsize") (simp_all add: fmsize_pos)
   1.138  
   1.139  lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
   1.140    by (induct p arbitrary: bs rule: prep.induct) auto
   1.141 @@ -424,34 +443,24 @@
   1.142  definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool"
   1.143    where "lex_bnd t s = lex_ns (bnds t) (bnds s)"
   1.144  
   1.145 -consts numadd:: "num \<times> num \<Rightarrow> num"
   1.146 -recdef numadd "measure (\<lambda>(t, s). num_size t + num_size s)"
   1.147 -  "numadd (CN n1 c1 r1, CN n2 c2 r2) =
   1.148 +fun numadd:: "num \<Rightarrow> num \<Rightarrow> num"
   1.149 +where
   1.150 +  "numadd (CN n1 c1 r1) (CN n2 c2 r2) =
   1.151      (if n1 = n2 then
   1.152         let c = c1 + c2
   1.153 -       in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2))
   1.154 -     else if n1 \<le> n2 then CN n1 c1 (numadd (r1, Add (Mul c2 (Bound n2)) r2))
   1.155 -     else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))"
   1.156 -  "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"
   1.157 -  "numadd (t, CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))"
   1.158 -  "numadd (C b1, C b2) = C (b1 + b2)"
   1.159 -  "numadd (a, b) = Add a b"
   1.160 +       in if c = 0 then numadd r1 r2 else CN n1 c (numadd r1 r2)
   1.161 +     else if n1 \<le> n2 then CN n1 c1 (numadd r1 (Add (Mul c2 (Bound n2)) r2))
   1.162 +     else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1) r2))"
   1.163 +| "numadd (CN n1 c1 r1) t = CN n1 c1 (numadd r1 t)"
   1.164 +| "numadd t (CN n2 c2 r2) = CN n2 c2 (numadd t r2)"
   1.165 +| "numadd (C b1) (C b2) = C (b1 + b2)"
   1.166 +| "numadd a b = Add a b"
   1.167  
   1.168 -lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
   1.169 -  apply (induct t s rule: numadd.induct)
   1.170 -  apply (simp_all add: Let_def)
   1.171 -  subgoal for n1 c1 r1 n2 c2 r2
   1.172 -    apply (cases "c1 + c2 = 0")
   1.173 -    apply (cases "n1 \<le> n2")
   1.174 -    apply simp_all
   1.175 -     apply (cases "n1 = n2")
   1.176 -      apply (simp_all add: algebra_simps)
   1.177 -    apply (simp add: distrib_right[symmetric])
   1.178 -    done
   1.179 -  done
   1.180 +lemma numadd: "Inum bs (numadd t s) = Inum bs (Add t s)"
   1.181 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff)
   1.182  
   1.183 -lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"
   1.184 -  by (induct t s rule: numadd.induct) (auto simp add: Let_def)
   1.185 +lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd t s)"
   1.186 +  by (induct t s rule: numadd.induct) (simp_all add: Let_def)
   1.187  
   1.188  fun nummul :: "int \<Rightarrow> num \<Rightarrow> num"
   1.189  where
   1.190 @@ -460,16 +469,16 @@
   1.191  | "nummul i t = Mul i t"
   1.192  
   1.193  lemma nummul: "Inum bs (nummul i t) = Inum bs (Mul i t)"
   1.194 -  by (induct t arbitrary: i rule: nummul.induct) (auto simp add: algebra_simps numadd)
   1.195 +  by (induct t arbitrary: i rule: nummul.induct) (simp_all add: algebra_simps)
   1.196  
   1.197  lemma nummul_nb: "numbound0 t \<Longrightarrow> numbound0 (nummul i t)"
   1.198 -  by (induct t arbitrary: i rule: nummul.induct) (auto simp add: numadd_nb)
   1.199 +  by (induct t arbitrary: i rule: nummul.induct) (simp_all add: numadd_nb)
   1.200  
   1.201  definition numneg :: "num \<Rightarrow> num"
   1.202    where "numneg t = nummul (- 1) t"
   1.203  
   1.204  definition numsub :: "num \<Rightarrow> num \<Rightarrow> num"
   1.205 -  where "numsub s t = (if s = t then C 0 else numadd (s, numneg t))"
   1.206 +  where "numsub s t = (if s = t then C 0 else numadd s (numneg t))"
   1.207  
   1.208  lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)"
   1.209    using numneg_def nummul by simp
   1.210 @@ -488,7 +497,7 @@
   1.211    "simpnum (C j) = C j"
   1.212  | "simpnum (Bound n) = CN n 1 (C 0)"
   1.213  | "simpnum (Neg t) = numneg (simpnum t)"
   1.214 -| "simpnum (Add t s) = numadd (simpnum t, simpnum s)"
   1.215 +| "simpnum (Add t s) = numadd (simpnum t) (simpnum s)"
   1.216  | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
   1.217  | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))"
   1.218  | "simpnum t = t"
   1.219 @@ -587,7 +596,7 @@
   1.220  lemma iff_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (iff p q)"
   1.221    using iff_def by (unfold iff_def, cases "p = q", auto simp add: not_bn)
   1.222  
   1.223 -function (sequential) simpfm :: "fm \<Rightarrow> fm"
   1.224 +fun simpfm :: "fm \<Rightarrow> fm"
   1.225  where
   1.226    "simpfm (And p q) = conj (simpfm p) (simpfm q)"
   1.227  | "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   1.228 @@ -609,8 +618,6 @@
   1.229       else if \<bar>i\<bar> = 1 then F
   1.230       else let a' = simpnum a in case a' of C v \<Rightarrow> if \<not>( i dvd v) then T else F | _ \<Rightarrow> NDvd i a')"
   1.231  | "simpfm p = p"
   1.232 -  by pat_completeness auto
   1.233 -termination by (relation "measure fmsize") auto
   1.234  
   1.235  lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"
   1.236  proof (induct p rule: simpfm.induct)
   1.237 @@ -819,7 +826,7 @@
   1.238    done
   1.239  
   1.240  text \<open>Generic quantifier elimination\<close>
   1.241 -function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   1.242 +fun qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   1.243  where
   1.244    "qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))"
   1.245  | "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
   1.246 @@ -829,8 +836,6 @@
   1.247  | "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
   1.248  | "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
   1.249  | "qelim p = (\<lambda>y. simpfm p)"
   1.250 -  by pat_completeness auto
   1.251 -termination by (relation "measure fmsize") auto
   1.252  
   1.253  lemma qelim_ci:
   1.254    assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
   1.255 @@ -990,7 +995,7 @@
   1.256  lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
   1.257    by (induct p rule: iszlfm.induct) auto
   1.258  
   1.259 -function (sequential) zlfm :: "fm \<Rightarrow> fm"  \<comment> \<open>Linearity transformation for fm\<close>
   1.260 +fun zlfm :: "fm \<Rightarrow> fm"  \<comment> \<open>Linearity transformation for fm\<close>
   1.261  where
   1.262    "zlfm (And p q) = And (zlfm p) (zlfm q)"
   1.263  | "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
   1.264 @@ -1058,10 +1063,6 @@
   1.265  | "zlfm (NOT (Closed P)) = NClosed P"
   1.266  | "zlfm (NOT (NClosed P)) = Closed P"
   1.267  | "zlfm p = p"
   1.268 -  by pat_completeness auto
   1.269 -
   1.270 -termination
   1.271 -  by (relation "measure fmsize") (simp_all add: fmsize_pos)
   1.272  
   1.273  lemma zlfm_I:
   1.274    assumes qfp: "qfree p"