author krauss Wed Feb 23 11:15:06 2011 +0100 (2011-02-23) changeset 41822 27afef7d6c37 parent 41821 c118ae98dfbf child 41823 81d64ec48427
recdef -> fun
```     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 23 10:48:57 2011 +0100
1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 23 11:15:06 2011 +0100
1.3 @@ -335,16 +335,19 @@
1.4    shows "allpolys isnpoly (simptm p)"
1.5    by (induct p rule: simptm.induct, auto simp add: Let_def)
1.6
1.7 -consts split0 :: "tm \<Rightarrow> (poly \<times> tm)"
1.8 -recdef split0 "measure tmsize"
1.9 +declare let_cong[fundef_cong del]
1.10 +
1.11 +fun split0 :: "tm \<Rightarrow> (poly \<times> tm)" where
1.12    "split0 (Bound 0) = (1\<^sub>p, CP 0\<^sub>p)"
1.13 -  "split0 (CNP 0 c t) = (let (c',t') = split0 t in (c +\<^sub>p c',t'))"
1.14 -  "split0 (Neg t) = (let (c,t') = split0 t in (~\<^sub>p c,Neg t'))"
1.15 -  "split0 (CNP n c t) = (let (c',t') = split0 t in (c',CNP n c t'))"
1.16 -  "split0 (Add s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 +\<^sub>p c2, Add s' t'))"
1.17 -  "split0 (Sub s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 -\<^sub>p c2, Sub s' t'))"
1.18 -  "split0 (Mul c t) = (let (c',t') = split0 t in (c *\<^sub>p c', Mul c t'))"
1.19 -  "split0 t = (0\<^sub>p, t)"
1.20 +| "split0 (CNP 0 c t) = (let (c',t') = split0 t in (c +\<^sub>p c',t'))"
1.21 +| "split0 (Neg t) = (let (c,t') = split0 t in (~\<^sub>p c,Neg t'))"
1.22 +| "split0 (CNP n c t) = (let (c',t') = split0 t in (c',CNP n c t'))"
1.23 +| "split0 (Add s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 +\<^sub>p c2, Add s' t'))"
1.24 +| "split0 (Sub s t) = (let (c1,s') = split0 s ; (c2,t') = split0 t in (c1 -\<^sub>p c2, Sub s' t'))"
1.25 +| "split0 (Mul c t) = (let (c',t') = split0 t in (c *\<^sub>p c', Mul c t'))"
1.26 +| "split0 t = (0\<^sub>p, t)"
1.27 +
1.28 +declare let_cong[fundef_cong]
1.29
1.30  lemma split0_stupid[simp]: "\<exists>x y. (x,y) = split0 p"
1.31    apply (rule exI[where x="fst (split0 p)"])
1.32 @@ -418,18 +421,17 @@
1.33
1.34
1.35    (* A size for fm *)
1.36 -consts fmsize :: "fm \<Rightarrow> nat"
1.37 -recdef fmsize "measure size"
1.38 +fun fmsize :: "fm \<Rightarrow> nat" where
1.39    "fmsize (NOT p) = 1 + fmsize p"
1.40 -  "fmsize (And p q) = 1 + fmsize p + fmsize q"
1.41 -  "fmsize (Or p q) = 1 + fmsize p + fmsize q"
1.42 -  "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
1.43 -  "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
1.44 -  "fmsize (E p) = 1 + fmsize p"
1.45 -  "fmsize (A p) = 4+ fmsize p"
1.46 -  "fmsize p = 1"
1.47 +| "fmsize (And p q) = 1 + fmsize p + fmsize q"
1.48 +| "fmsize (Or p q) = 1 + fmsize p + fmsize q"
1.49 +| "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
1.50 +| "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
1.51 +| "fmsize (E p) = 1 + fmsize p"
1.52 +| "fmsize (A p) = 4+ fmsize p"
1.53 +| "fmsize p = 1"
1.54    (* several lemmas about fmsize *)
1.55 -lemma fmsize_pos: "fmsize p > 0"
1.56 +lemma fmsize_pos[termination_simp]: "fmsize p > 0"
1.57  by (induct p rule: fmsize.induct) simp_all
1.58
1.59    (* Semantics of formulae (fm) *)
1.60 @@ -448,17 +450,16 @@
1.61  | "Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)"
1.62  | "Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)"
1.63
1.64 -consts not:: "fm \<Rightarrow> fm"
1.65 -recdef not "measure size"
1.66 +fun not:: "fm \<Rightarrow> fm" where
1.67    "not (NOT (NOT p)) = not p"
1.68 -  "not (NOT p) = p"
1.69 -  "not T = F"
1.70 -  "not F = T"
1.71 -  "not (Lt t) = Le (tmneg t)"
1.72 -  "not (Le t) = Lt (tmneg t)"
1.73 -  "not (Eq t) = NEq t"
1.74 -  "not (NEq t) = Eq t"
1.75 -  "not p = NOT p"
1.76 +| "not (NOT p) = p"
1.77 +| "not T = F"
1.78 +| "not F = T"
1.79 +| "not (Lt t) = Le (tmneg t)"
1.80 +| "not (Le t) = Lt (tmneg t)"
1.81 +| "not (Eq t) = NEq t"
1.82 +| "not (NEq t) = Eq t"
1.83 +| "not p = NOT p"
1.84  lemma not[simp]: "Ifm vs bs (not p) = Ifm vs bs (NOT p)"
1.85  by (induct p rule: not.induct) auto
1.86
1.87 @@ -487,17 +488,17 @@
1.88    Iff p q)"
1.89  lemma iff[simp]: "Ifm vs bs (iff p q) = Ifm vs bs (Iff p q)"
1.90    by (unfold iff_def,cases "p=q", simp,cases "p=NOT q", simp) (cases "NOT p= q", auto)
1.91 +
1.92    (* Quantifier freeness *)
1.93 -consts qfree:: "fm \<Rightarrow> bool"
1.94 -recdef qfree "measure size"
1.95 +fun qfree:: "fm \<Rightarrow> bool" where
1.96    "qfree (E p) = False"
1.97 -  "qfree (A p) = False"
1.98 -  "qfree (NOT p) = qfree p"
1.99 -  "qfree (And p q) = (qfree p \<and> qfree q)"
1.100 -  "qfree (Or  p q) = (qfree p \<and> qfree q)"
1.101 -  "qfree (Imp p q) = (qfree p \<and> qfree q)"
1.102 -  "qfree (Iff p q) = (qfree p \<and> qfree q)"
1.103 -  "qfree p = True"
1.104 +| "qfree (A p) = False"
1.105 +| "qfree (NOT p) = qfree p"
1.106 +| "qfree (And p q) = (qfree p \<and> qfree q)"
1.107 +| "qfree (Or  p q) = (qfree p \<and> qfree q)"
1.108 +| "qfree (Imp p q) = (qfree p \<and> qfree q)"
1.109 +| "qfree (Iff p q) = (qfree p \<and> qfree q)"
1.110 +| "qfree p = True"
1.111
1.112    (* Boundedness and substitution *)
1.113
1.114 @@ -516,22 +517,19 @@
1.115  | "boundslt n (E p) = boundslt (Suc n) p"
1.116  | "boundslt n (A p) = boundslt (Suc n) p"
1.117
1.118 -consts
1.119 -  bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
1.120 -  decr0 :: "fm \<Rightarrow> fm"
1.121 -recdef bound0 "measure size"
1.122 +fun bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
1.123    "bound0 T = True"
1.124 -  "bound0 F = True"
1.125 -  "bound0 (Lt a) = tmbound0 a"
1.126 -  "bound0 (Le a) = tmbound0 a"
1.127 -  "bound0 (Eq a) = tmbound0 a"
1.128 -  "bound0 (NEq a) = tmbound0 a"
1.129 -  "bound0 (NOT p) = bound0 p"
1.130 -  "bound0 (And p q) = (bound0 p \<and> bound0 q)"
1.131 -  "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
1.132 -  "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
1.133 -  "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
1.134 -  "bound0 p = False"
1.135 +| "bound0 F = True"
1.136 +| "bound0 (Lt a) = tmbound0 a"
1.137 +| "bound0 (Le a) = tmbound0 a"
1.138 +| "bound0 (Eq a) = tmbound0 a"
1.139 +| "bound0 (NEq a) = tmbound0 a"
1.140 +| "bound0 (NOT p) = bound0 p"
1.141 +| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
1.142 +| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
1.143 +| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
1.144 +| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
1.145 +| "bound0 p = False"
1.146  lemma bound0_I:
1.147    assumes bp: "bound0 p"
1.148    shows "Ifm vs (b#bs) p = Ifm vs (b'#bs) p"
1.149 @@ -572,17 +570,17 @@
1.150    thus ?case by simp
1.151  qed auto
1.152
1.153 -recdef decr0 "measure size"
1.154 +fun decr0 :: "fm \<Rightarrow> fm" where
1.155    "decr0 (Lt a) = Lt (decrtm0 a)"
1.156 -  "decr0 (Le a) = Le (decrtm0 a)"
1.157 -  "decr0 (Eq a) = Eq (decrtm0 a)"
1.158 -  "decr0 (NEq a) = NEq (decrtm0 a)"
1.159 -  "decr0 (NOT p) = NOT (decr0 p)"
1.160 -  "decr0 (And p q) = conj (decr0 p) (decr0 q)"
1.161 -  "decr0 (Or p q) = disj (decr0 p) (decr0 q)"
1.162 -  "decr0 (Imp p q) = imp (decr0 p) (decr0 q)"
1.163 -  "decr0 (Iff p q) = iff (decr0 p) (decr0 q)"
1.164 -  "decr0 p = p"
1.165 +| "decr0 (Le a) = Le (decrtm0 a)"
1.166 +| "decr0 (Eq a) = Eq (decrtm0 a)"
1.167 +| "decr0 (NEq a) = NEq (decrtm0 a)"
1.168 +| "decr0 (NOT p) = NOT (decr0 p)"
1.169 +| "decr0 (And p q) = conj (decr0 p) (decr0 q)"
1.170 +| "decr0 (Or p q) = disj (decr0 p) (decr0 q)"
1.171 +| "decr0 (Imp p q) = imp (decr0 p) (decr0 q)"
1.172 +| "decr0 (Iff p q) = iff (decr0 p) (decr0 q)"
1.173 +| "decr0 p = p"
1.174
1.175  lemma decr0: assumes nb: "bound0 p"
1.176    shows "Ifm vs (x#bs) p = Ifm vs bs (decr0 p)"
1.177 @@ -740,16 +738,14 @@
1.178  lemma decr0_qf: "bound0 p \<Longrightarrow> qfree (decr0 p)"
1.179  by (induct p, simp_all)
1.180
1.181 -consts
1.182 -  isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
1.183 -recdef isatom "measure size"
1.184 +fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where
1.185    "isatom T = True"
1.186 -  "isatom F = True"
1.187 -  "isatom (Lt a) = True"
1.188 -  "isatom (Le a) = True"
1.189 -  "isatom (Eq a) = True"
1.190 -  "isatom (NEq a) = True"
1.191 -  "isatom p = False"
1.192 +| "isatom F = True"
1.193 +| "isatom (Lt a) = True"
1.194 +| "isatom (Le a) = True"
1.195 +| "isatom (Eq a) = True"
1.196 +| "isatom (NEq a) = True"
1.197 +| "isatom p = False"
1.198
1.199  lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
1.200  by (induct p, simp_all)
1.201 @@ -777,11 +773,10 @@
1.202    shows "qfree (evaldjf f xs)"
1.203    using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
1.204
1.205 -consts disjuncts :: "fm \<Rightarrow> fm list"
1.206 -recdef disjuncts "measure size"
1.207 +fun disjuncts :: "fm \<Rightarrow> fm list" where
1.208    "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
1.209 -  "disjuncts F = []"
1.210 -  "disjuncts p = [p]"
1.211 +| "disjuncts F = []"
1.212 +| "disjuncts p = [p]"
1.213
1.214  lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm vs bs q) = Ifm vs bs p"
1.215  by(induct p rule: disjuncts.induct, auto)
1.216 @@ -840,12 +835,10 @@
1.217    finally show "qfree (DJ qe p) \<and> Ifm vs bs (DJ qe p) = Ifm vs bs (E p)" using qfth by blast
1.218  qed
1.219
1.220 -consts conjuncts :: "fm \<Rightarrow> fm list"
1.221 -
1.222 -recdef conjuncts "measure size"
1.223 +fun conjuncts :: "fm \<Rightarrow> fm list" where
1.224    "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)"
1.225 -  "conjuncts T = []"
1.226 -  "conjuncts p = [p]"
1.227 +| "conjuncts T = []"
1.228 +| "conjuncts p = [p]"
1.229
1.230  definition list_conj :: "fm list \<Rightarrow> fm" where
1.231    "list_conj ps \<equiv> foldr conj ps T"
1.232 @@ -1129,11 +1122,10 @@
1.233         fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simpneq_def Let_def split_def neq_nb)
1.234  qed
1.235
1.236 -consts conjs   :: "fm \<Rightarrow> fm list"
1.237 -recdef conjs "measure size"
1.238 +fun conjs   :: "fm \<Rightarrow> fm list" where
1.239    "conjs (And p q) = (conjs p)@(conjs q)"
1.240 -  "conjs T = []"
1.241 -  "conjs p = [p]"
1.242 +| "conjs T = []"
1.243 +| "conjs p = [p]"
1.244  lemma conjs_ci: "(\<forall> q \<in> set (conjs p). Ifm vs bs q) = Ifm vs bs p"
1.245  by (induct p rule: conjs.induct, auto)
1.246  definition list_disj :: "fm list \<Rightarrow> fm" where
1.247 @@ -1312,17 +1304,17 @@
1.248
1.249
1.250    (* Generic quantifier elimination *)
1.251 -consts qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
1.252 -recdef qelim "measure fmsize"
1.253 +function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" where
1.254    "qelim (E p) = (\<lambda> qe. DJ (CJNB qe) (qelim p qe))"
1.255 -  "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
1.256 -  "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
1.257 -  "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))"
1.258 -  "qelim (Or  p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))"
1.259 -  "qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))"
1.260 -  "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
1.261 -  "qelim p = (\<lambda> y. simpfm p)"
1.262 -
1.263 +| "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
1.264 +| "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
1.265 +| "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))"
1.266 +| "qelim (Or  p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))"
1.267 +| "qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))"
1.268 +| "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
1.269 +| "qelim p = (\<lambda> y. simpfm p)"
1.270 +by pat_completeness simp_all
1.271 +termination by (relation "measure fmsize") auto
1.272
1.273  lemma qelim:
1.274    assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm vs bs (qe p) = Ifm vs bs (E p))"
1.275 @@ -1332,26 +1324,23 @@
1.276
1.277  subsection{* Core Procedure *}
1.278
1.279 -consts
1.280 -  plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
1.281 -  minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
1.282 -recdef minusinf "measure size"
1.283 +fun minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*) where
1.284    "minusinf (And p q) = conj (minusinf p) (minusinf q)"
1.285 -  "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
1.286 -  "minusinf (Eq  (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
1.287 -  "minusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
1.288 -  "minusinf (Lt  (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP (~\<^sub>p c)))"
1.289 -  "minusinf (Le  (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP (~\<^sub>p c)))"
1.290 -  "minusinf p = p"
1.291 +| "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
1.292 +| "minusinf (Eq  (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
1.293 +| "minusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
1.294 +| "minusinf (Lt  (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP (~\<^sub>p c)))"
1.295 +| "minusinf (Le  (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP (~\<^sub>p c)))"
1.296 +| "minusinf p = p"
1.297
1.298 -recdef plusinf "measure size"
1.299 +fun plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*) where
1.300    "plusinf (And p q) = conj (plusinf p) (plusinf q)"
1.301 -  "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
1.302 -  "plusinf (Eq  (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
1.303 -  "plusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
1.304 -  "plusinf (Lt  (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP c))"
1.305 -  "plusinf (Le  (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP c))"
1.306 -  "plusinf p = p"
1.307 +| "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
1.308 +| "plusinf (Eq  (CNP 0 c e)) = conj (eq (CP c)) (eq e)"
1.309 +| "plusinf (NEq (CNP 0 c e)) = disj (not (eq e)) (not (eq (CP c)))"
1.310 +| "plusinf (Lt  (CNP 0 c e)) = disj (conj (eq (CP c)) (lt e)) (lt (CP c))"
1.311 +| "plusinf (Le  (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP c))"
1.312 +| "plusinf p = p"
1.313
1.314  lemma minusinf_inf: assumes lp:"islin p"
1.315    shows "\<exists>z. \<forall>x < z. Ifm vs (x#bs) (minusinf p) \<longleftrightarrow> Ifm vs (x#bs) p"
```