recdef -> fun
authorkrauss
Wed Feb 23 11:15:06 2011 +0100 (2011-02-23)
changeset 4182227afef7d6c37
parent 41821 c118ae98dfbf
child 41823 81d64ec48427
recdef -> fun
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
     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"