src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 39246 9e58f0499f57
parent 38864 4abe644fcea5
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Sep 08 13:25:22 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Sep 08 19:21:46 2010 +0200
     1.3 @@ -16,26 +16,24 @@
     1.4    | Neg tm | Sub tm tm | CNP nat poly tm
     1.5    (* A size for poly to make inductive proofs simpler*)
     1.6  
     1.7 -consts tmsize :: "tm \<Rightarrow> nat"
     1.8 -primrec 
     1.9 +primrec tmsize :: "tm \<Rightarrow> nat" where
    1.10    "tmsize (CP c) = polysize c"
    1.11 -  "tmsize (Bound n) = 1"
    1.12 -  "tmsize (Neg a) = 1 + tmsize a"
    1.13 -  "tmsize (Add a b) = 1 + tmsize a + tmsize b"
    1.14 -  "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
    1.15 -  "tmsize (Mul c a) = 1 + polysize c + tmsize a"
    1.16 -  "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
    1.17 +| "tmsize (Bound n) = 1"
    1.18 +| "tmsize (Neg a) = 1 + tmsize a"
    1.19 +| "tmsize (Add a b) = 1 + tmsize a + tmsize b"
    1.20 +| "tmsize (Sub a b) = 3 + tmsize a + tmsize b"
    1.21 +| "tmsize (Mul c a) = 1 + polysize c + tmsize a"
    1.22 +| "tmsize (CNP n c a) = 3 + polysize c + tmsize a "
    1.23  
    1.24    (* Semantics of terms tm *)
    1.25 -consts Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a"
    1.26 -primrec
    1.27 +primrec Itm :: "'a::{field_char_0, field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> tm \<Rightarrow> 'a" where
    1.28    "Itm vs bs (CP c) = (Ipoly vs c)"
    1.29 -  "Itm vs bs (Bound n) = bs!n"
    1.30 -  "Itm vs bs (Neg a) = -(Itm vs bs a)"
    1.31 -  "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
    1.32 -  "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
    1.33 -  "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
    1.34 -  "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"   
    1.35 +| "Itm vs bs (Bound n) = bs!n"
    1.36 +| "Itm vs bs (Neg a) = -(Itm vs bs a)"
    1.37 +| "Itm vs bs (Add a b) = Itm vs bs a + Itm vs bs b"
    1.38 +| "Itm vs bs (Sub a b) = Itm vs bs a - Itm vs bs b"
    1.39 +| "Itm vs bs (Mul c a) = (Ipoly vs c) * Itm vs bs a"
    1.40 +| "Itm vs bs (CNP n c t) = (Ipoly vs c)*(bs!n) + Itm vs bs t"   
    1.41  
    1.42  
    1.43  fun allpolys:: "(poly \<Rightarrow> bool) \<Rightarrow> tm \<Rightarrow> bool"  where
    1.44 @@ -47,51 +45,48 @@
    1.45  | "allpolys P (Sub p q) = (allpolys P p \<and> allpolys P q)"
    1.46  | "allpolys P p = True"
    1.47  
    1.48 -consts 
    1.49 -  tmboundslt:: "nat \<Rightarrow> tm \<Rightarrow> bool"
    1.50 -  tmbound0:: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *)
    1.51 -  tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *)
    1.52 -  incrtm0:: "tm \<Rightarrow> tm"
    1.53 -  incrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm"
    1.54 -  decrtm0:: "tm \<Rightarrow> tm" 
    1.55 -  decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" 
    1.56 -primrec
    1.57 +primrec tmboundslt:: "nat \<Rightarrow> tm \<Rightarrow> bool" where
    1.58    "tmboundslt n (CP c) = True"
    1.59 -  "tmboundslt n (Bound m) = (m < n)"
    1.60 -  "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)"
    1.61 -  "tmboundslt n (Neg a) = tmboundslt n a"
    1.62 -  "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"
    1.63 -  "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)" 
    1.64 -  "tmboundslt n (Mul i a) = tmboundslt n a"
    1.65 -primrec
    1.66 +| "tmboundslt n (Bound m) = (m < n)"
    1.67 +| "tmboundslt n (CNP m c a) = (m < n \<and> tmboundslt n a)"
    1.68 +| "tmboundslt n (Neg a) = tmboundslt n a"
    1.69 +| "tmboundslt n (Add a b) = (tmboundslt n a \<and> tmboundslt n b)"
    1.70 +| "tmboundslt n (Sub a b) = (tmboundslt n a \<and> tmboundslt n b)" 
    1.71 +| "tmboundslt n (Mul i a) = tmboundslt n a"
    1.72 +
    1.73 +primrec tmbound0:: "tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound 0 *) where
    1.74    "tmbound0 (CP c) = True"
    1.75 -  "tmbound0 (Bound n) = (n>0)"
    1.76 -  "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"
    1.77 -  "tmbound0 (Neg a) = tmbound0 a"
    1.78 -  "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)"
    1.79 -  "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)" 
    1.80 -  "tmbound0 (Mul i a) = tmbound0 a"
    1.81 +| "tmbound0 (Bound n) = (n>0)"
    1.82 +| "tmbound0 (CNP n c a) = (n\<noteq>0 \<and> tmbound0 a)"
    1.83 +| "tmbound0 (Neg a) = tmbound0 a"
    1.84 +| "tmbound0 (Add a b) = (tmbound0 a \<and> tmbound0 b)"
    1.85 +| "tmbound0 (Sub a b) = (tmbound0 a \<and> tmbound0 b)" 
    1.86 +| "tmbound0 (Mul i a) = tmbound0 a"
    1.87  lemma tmbound0_I:
    1.88    assumes nb: "tmbound0 a"
    1.89    shows "Itm vs (b#bs) a = Itm vs (b'#bs) a"
    1.90  using nb
    1.91 -by (induct a rule: tmbound0.induct,auto simp add: nth_pos2)
    1.92 +by (induct a rule: tm.induct,auto simp add: nth_pos2)
    1.93  
    1.94 -primrec
    1.95 +primrec tmbound:: "nat \<Rightarrow> tm \<Rightarrow> bool" (* a tm is INDEPENDENT of Bound n *) where
    1.96    "tmbound n (CP c) = True"
    1.97 -  "tmbound n (Bound m) = (n \<noteq> m)"
    1.98 -  "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"
    1.99 -  "tmbound n (Neg a) = tmbound n a"
   1.100 -  "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)"
   1.101 -  "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)" 
   1.102 -  "tmbound n (Mul i a) = tmbound n a"
   1.103 +| "tmbound n (Bound m) = (n \<noteq> m)"
   1.104 +| "tmbound n (CNP m c a) = (n\<noteq>m \<and> tmbound n a)"
   1.105 +| "tmbound n (Neg a) = tmbound n a"
   1.106 +| "tmbound n (Add a b) = (tmbound n a \<and> tmbound n b)"
   1.107 +| "tmbound n (Sub a b) = (tmbound n a \<and> tmbound n b)" 
   1.108 +| "tmbound n (Mul i a) = tmbound n a"
   1.109  lemma tmbound0_tmbound_iff: "tmbound 0 t = tmbound0 t" by (induct t, auto)
   1.110  
   1.111  lemma tmbound_I: 
   1.112    assumes bnd: "tmboundslt (length bs) t" and nb: "tmbound n t" and le: "n \<le> length bs"
   1.113    shows "Itm vs (bs[n:=x]) t = Itm vs bs t"
   1.114    using nb le bnd
   1.115 -  by (induct t rule: tmbound.induct , auto)
   1.116 +  by (induct t rule: tm.induct , auto)
   1.117 +
   1.118 +consts 
   1.119 +  incrtm0:: "tm \<Rightarrow> tm"
   1.120 +  decrtm0:: "tm \<Rightarrow> tm" 
   1.121  
   1.122  recdef decrtm0 "measure size"
   1.123    "decrtm0 (Bound n) = Bound (n - 1)"
   1.124 @@ -101,6 +96,7 @@
   1.125    "decrtm0 (Mul c a) = Mul c (decrtm0 a)"
   1.126    "decrtm0 (CNP n c a) = CNP (n - 1) c (decrtm0 a)"
   1.127    "decrtm0 a = a"
   1.128 +
   1.129  recdef incrtm0 "measure size"
   1.130    "incrtm0 (Bound n) = Bound (n + 1)"
   1.131    "incrtm0 (Neg a) = Neg (incrtm0 a)"
   1.132 @@ -109,25 +105,26 @@
   1.133    "incrtm0 (Mul c a) = Mul c (incrtm0 a)"
   1.134    "incrtm0 (CNP n c a) = CNP (n + 1) c (incrtm0 a)"
   1.135    "incrtm0 a = a"
   1.136 +
   1.137  lemma decrtm0: assumes nb: "tmbound0 t"
   1.138    shows "Itm vs (x#bs) t = Itm vs bs (decrtm0 t)"
   1.139    using nb by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
   1.140 +
   1.141  lemma incrtm0: "Itm vs (x#bs) (incrtm0 t) = Itm vs bs t"
   1.142    by (induct t rule: decrtm0.induct, simp_all add: nth_pos2)
   1.143  
   1.144 -primrec
   1.145 +primrec decrtm:: "nat \<Rightarrow> tm \<Rightarrow> tm" where
   1.146    "decrtm m (CP c) = (CP c)"
   1.147 -  "decrtm m (Bound n) = (if n < m then Bound n else Bound (n - 1))"
   1.148 -  "decrtm m (Neg a) = Neg (decrtm m a)"
   1.149 -  "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)"
   1.150 -  "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)"
   1.151 -  "decrtm m (Mul c a) = Mul c (decrtm m a)"
   1.152 -  "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n - 1) c (decrtm m a))"
   1.153 +| "decrtm m (Bound n) = (if n < m then Bound n else Bound (n - 1))"
   1.154 +| "decrtm m (Neg a) = Neg (decrtm m a)"
   1.155 +| "decrtm m (Add a b) = Add (decrtm m a) (decrtm m b)"
   1.156 +| "decrtm m (Sub a b) = Sub (decrtm m a) (decrtm m b)"
   1.157 +| "decrtm m (Mul c a) = Mul c (decrtm m a)"
   1.158 +| "decrtm m (CNP n c a) = (if n < m then CNP n c (decrtm m a) else CNP (n - 1) c (decrtm m a))"
   1.159  
   1.160 -consts removen:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
   1.161 -primrec
   1.162 +primrec removen:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.163    "removen n [] = []"
   1.164 -  "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"
   1.165 +| "removen n (x#xs) = (if n=0 then xs else (x#(removen (n - 1) xs)))"
   1.166  
   1.167  lemma removen_same: "n \<ge> length xs \<Longrightarrow> removen n xs = xs"
   1.168    by (induct xs arbitrary: n, auto)
   1.169 @@ -172,50 +169,47 @@
   1.170    and nle: "m \<le> length bs" 
   1.171    shows "Itm vs (removen m bs) (decrtm m t) = Itm vs bs t"
   1.172    using bnd nb nle
   1.173 -  by (induct t rule: decrtm.induct, auto simp add: removen_nth)
   1.174 +  by (induct t rule: tm.induct, auto simp add: removen_nth)
   1.175  
   1.176 -consts tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm"
   1.177 -primrec
   1.178 +primrec tmsubst0:: "tm \<Rightarrow> tm \<Rightarrow> tm" where
   1.179    "tmsubst0 t (CP c) = CP c"
   1.180 -  "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   1.181 -  "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))"
   1.182 -  "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
   1.183 -  "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
   1.184 -  "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)" 
   1.185 -  "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
   1.186 +| "tmsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   1.187 +| "tmsubst0 t (CNP n c a) = (if n=0 then Add (Mul c t) (tmsubst0 t a) else CNP n c (tmsubst0 t a))"
   1.188 +| "tmsubst0 t (Neg a) = Neg (tmsubst0 t a)"
   1.189 +| "tmsubst0 t (Add a b) = Add (tmsubst0 t a) (tmsubst0 t b)"
   1.190 +| "tmsubst0 t (Sub a b) = Sub (tmsubst0 t a) (tmsubst0 t b)" 
   1.191 +| "tmsubst0 t (Mul i a) = Mul i (tmsubst0 t a)"
   1.192  lemma tmsubst0:
   1.193    shows "Itm vs (x#bs) (tmsubst0 t a) = Itm vs ((Itm vs (x#bs) t)#bs) a"
   1.194 -by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
   1.195 +by (induct a rule: tm.induct,auto simp add: nth_pos2)
   1.196  
   1.197  lemma tmsubst0_nb: "tmbound0 t \<Longrightarrow> tmbound0 (tmsubst0 t a)"
   1.198 -by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
   1.199 +by (induct a rule: tm.induct,auto simp add: nth_pos2)
   1.200  
   1.201 -consts tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" 
   1.202 -
   1.203 -primrec
   1.204 +primrec tmsubst:: "nat \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" where
   1.205    "tmsubst n t (CP c) = CP c"
   1.206 -  "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
   1.207 -  "tmsubst n t (CNP m c a) = (if n=m then Add (Mul c t) (tmsubst n t a) 
   1.208 +| "tmsubst n t (Bound m) = (if n=m then t else Bound m)"
   1.209 +| "tmsubst n t (CNP m c a) = (if n=m then Add (Mul c t) (tmsubst n t a) 
   1.210               else CNP m c (tmsubst n t a))"
   1.211 -  "tmsubst n t (Neg a) = Neg (tmsubst n t a)"
   1.212 -  "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)"
   1.213 -  "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)" 
   1.214 -  "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)"
   1.215 +| "tmsubst n t (Neg a) = Neg (tmsubst n t a)"
   1.216 +| "tmsubst n t (Add a b) = Add (tmsubst n t a) (tmsubst n t b)"
   1.217 +| "tmsubst n t (Sub a b) = Sub (tmsubst n t a) (tmsubst n t b)" 
   1.218 +| "tmsubst n t (Mul i a) = Mul i (tmsubst n t a)"
   1.219  
   1.220  lemma tmsubst: assumes nb: "tmboundslt (length bs) a" and nlt: "n \<le> length bs"
   1.221    shows "Itm vs bs (tmsubst n t a) = Itm vs (bs[n:= Itm vs bs t]) a"
   1.222  using nb nlt
   1.223 -by (induct a rule: tmsubst0.induct,auto simp add: nth_pos2)
   1.224 +by (induct a rule: tm.induct,auto simp add: nth_pos2)
   1.225  
   1.226  lemma tmsubst_nb0: assumes tnb: "tmbound0 t"
   1.227  shows "tmbound0 (tmsubst 0 t a)"
   1.228  using tnb
   1.229 -by (induct a rule: tmsubst.induct, auto)
   1.230 +by (induct a rule: tm.induct, auto)
   1.231  
   1.232  lemma tmsubst_nb: assumes tnb: "tmbound m t"
   1.233  shows "tmbound m (tmsubst m t a)"
   1.234  using tnb
   1.235 -by (induct a rule: tmsubst.induct, auto)
   1.236 +by (induct a rule: tm.induct, auto)
   1.237  lemma incrtm0_tmbound: "tmbound n t \<Longrightarrow> tmbound (Suc n) (incrtm0 t)"
   1.238    by (induct t, auto)
   1.239    (* Simplification *)
   1.240 @@ -447,21 +441,20 @@
   1.241  by (induct p rule: fmsize.induct) simp_all
   1.242  
   1.243    (* Semantics of formulae (fm) *)
   1.244 -consts Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
   1.245 -primrec
   1.246 +primrec Ifm ::"'a::{linordered_field_inverse_zero} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool" where
   1.247    "Ifm vs bs T = True"
   1.248 -  "Ifm vs bs F = False"
   1.249 -  "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
   1.250 -  "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)"
   1.251 -  "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"
   1.252 -  "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)"
   1.253 -  "Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))"
   1.254 -  "Ifm vs bs (And p q) = (Ifm vs bs p \<and> Ifm vs bs q)"
   1.255 -  "Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)"
   1.256 -  "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))"
   1.257 -  "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)"
   1.258 -  "Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)"
   1.259 -  "Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)"
   1.260 +| "Ifm vs bs F = False"
   1.261 +| "Ifm vs bs (Lt a) = (Itm vs bs a < 0)"
   1.262 +| "Ifm vs bs (Le a) = (Itm vs bs a \<le> 0)"
   1.263 +| "Ifm vs bs (Eq a) = (Itm vs bs a = 0)"
   1.264 +| "Ifm vs bs (NEq a) = (Itm vs bs a \<noteq> 0)"
   1.265 +| "Ifm vs bs (NOT p) = (\<not> (Ifm vs bs p))"
   1.266 +| "Ifm vs bs (And p q) = (Ifm vs bs p \<and> Ifm vs bs q)"
   1.267 +| "Ifm vs bs (Or p q) = (Ifm vs bs p \<or> Ifm vs bs q)"
   1.268 +| "Ifm vs bs (Imp p q) = ((Ifm vs bs p) \<longrightarrow> (Ifm vs bs q))"
   1.269 +| "Ifm vs bs (Iff p q) = (Ifm vs bs p = Ifm vs bs q)"
   1.270 +| "Ifm vs bs (E p) = (\<exists> x. Ifm vs (x#bs) p)"
   1.271 +| "Ifm vs bs (A p) = (\<forall> x. Ifm vs (x#bs) p)"
   1.272  
   1.273  consts not:: "fm \<Rightarrow> fm"
   1.274  recdef not "measure size"
   1.275 @@ -516,27 +509,24 @@
   1.276  
   1.277    (* Boundedness and substitution *)
   1.278  
   1.279 -consts boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool"
   1.280 -primrec
   1.281 +primrec boundslt :: "nat \<Rightarrow> fm \<Rightarrow> bool" where
   1.282    "boundslt n T = True"
   1.283 -  "boundslt n F = True"
   1.284 -  "boundslt n (Lt t) = (tmboundslt n t)"
   1.285 -  "boundslt n (Le t) = (tmboundslt n t)"
   1.286 -  "boundslt n (Eq t) = (tmboundslt n t)"
   1.287 -  "boundslt n (NEq t) = (tmboundslt n t)"
   1.288 -  "boundslt n (NOT p) = boundslt n p"
   1.289 -  "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)"
   1.290 -  "boundslt n (Or p q) = (boundslt n p \<and> boundslt n q)"
   1.291 -  "boundslt n (Imp p q) = ((boundslt n p) \<and> (boundslt n q))"
   1.292 -  "boundslt n (Iff p q) = (boundslt n p \<and> boundslt n q)"
   1.293 -  "boundslt n (E p) = boundslt (Suc n) p"
   1.294 -  "boundslt n (A p) = boundslt (Suc n) p"
   1.295 +| "boundslt n F = True"
   1.296 +| "boundslt n (Lt t) = (tmboundslt n t)"
   1.297 +| "boundslt n (Le t) = (tmboundslt n t)"
   1.298 +| "boundslt n (Eq t) = (tmboundslt n t)"
   1.299 +| "boundslt n (NEq t) = (tmboundslt n t)"
   1.300 +| "boundslt n (NOT p) = boundslt n p"
   1.301 +| "boundslt n (And p q) = (boundslt n p \<and> boundslt n q)"
   1.302 +| "boundslt n (Or p q) = (boundslt n p \<and> boundslt n q)"
   1.303 +| "boundslt n (Imp p q) = ((boundslt n p) \<and> (boundslt n q))"
   1.304 +| "boundslt n (Iff p q) = (boundslt n p \<and> boundslt n q)"
   1.305 +| "boundslt n (E p) = boundslt (Suc n) p"
   1.306 +| "boundslt n (A p) = boundslt (Suc n) p"
   1.307  
   1.308  consts 
   1.309    bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
   1.310 -  bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *)
   1.311    decr0 :: "fm \<Rightarrow> fm"
   1.312 -  decr :: "nat \<Rightarrow> fm \<Rightarrow> fm"
   1.313  recdef bound0 "measure size"
   1.314    "bound0 T = True"
   1.315    "bound0 F = True"
   1.316 @@ -556,26 +546,26 @@
   1.317  using bp tmbound0_I[where b="b" and bs="bs" and b'="b'"]
   1.318  by (induct p rule: bound0.induct,auto simp add: nth_pos2)
   1.319  
   1.320 -primrec
   1.321 +primrec bound:: "nat \<Rightarrow> fm \<Rightarrow> bool" (* A Formula is independent of Bound n *) where
   1.322    "bound m T = True"
   1.323 -  "bound m F = True"
   1.324 -  "bound m (Lt t) = tmbound m t"
   1.325 -  "bound m (Le t) = tmbound m t"
   1.326 -  "bound m (Eq t) = tmbound m t"
   1.327 -  "bound m (NEq t) = tmbound m t"
   1.328 -  "bound m (NOT p) = bound m p"
   1.329 -  "bound m (And p q) = (bound m p \<and> bound m q)"
   1.330 -  "bound m (Or p q) = (bound m p \<and> bound m q)"
   1.331 -  "bound m (Imp p q) = ((bound m p) \<and> (bound m q))"
   1.332 -  "bound m (Iff p q) = (bound m p \<and> bound m q)"
   1.333 -  "bound m (E p) = bound (Suc m) p"
   1.334 -  "bound m (A p) = bound (Suc m) p"
   1.335 +| "bound m F = True"
   1.336 +| "bound m (Lt t) = tmbound m t"
   1.337 +| "bound m (Le t) = tmbound m t"
   1.338 +| "bound m (Eq t) = tmbound m t"
   1.339 +| "bound m (NEq t) = tmbound m t"
   1.340 +| "bound m (NOT p) = bound m p"
   1.341 +| "bound m (And p q) = (bound m p \<and> bound m q)"
   1.342 +| "bound m (Or p q) = (bound m p \<and> bound m q)"
   1.343 +| "bound m (Imp p q) = ((bound m p) \<and> (bound m q))"
   1.344 +| "bound m (Iff p q) = (bound m p \<and> bound m q)"
   1.345 +| "bound m (E p) = bound (Suc m) p"
   1.346 +| "bound m (A p) = bound (Suc m) p"
   1.347  
   1.348  lemma bound_I:
   1.349    assumes bnd: "boundslt (length bs) p" and nb: "bound n p" and le: "n \<le> length bs"
   1.350    shows "Ifm vs (bs[n:=x]) p = Ifm vs bs p"
   1.351    using bnd nb le tmbound_I[where bs=bs and vs = vs]
   1.352 -proof(induct p arbitrary: bs n rule: bound.induct)
   1.353 +proof(induct p arbitrary: bs n rule: fm.induct)
   1.354    case (E p bs n) 
   1.355    {fix y
   1.356      from prems have bnd: "boundslt (length (y#bs)) p" 
   1.357 @@ -607,26 +597,26 @@
   1.358    using nb 
   1.359    by (induct p rule: decr0.induct, simp_all add: decrtm0)
   1.360  
   1.361 -primrec
   1.362 +primrec decr :: "nat \<Rightarrow> fm \<Rightarrow> fm" where
   1.363    "decr m T = T"
   1.364 -  "decr m F = F"
   1.365 -  "decr m (Lt t) = (Lt (decrtm m t))"
   1.366 -  "decr m (Le t) = (Le (decrtm m t))"
   1.367 -  "decr m (Eq t) = (Eq (decrtm m t))"
   1.368 -  "decr m (NEq t) = (NEq (decrtm m t))"
   1.369 -  "decr m (NOT p) = NOT (decr m p)" 
   1.370 -  "decr m (And p q) = conj (decr m p) (decr m q)"
   1.371 -  "decr m (Or p q) = disj (decr m p) (decr m q)"
   1.372 -  "decr m (Imp p q) = imp (decr m p) (decr m q)"
   1.373 -  "decr m (Iff p q) = iff (decr m p) (decr m q)"
   1.374 -  "decr m (E p) = E (decr (Suc m) p)"
   1.375 -  "decr m (A p) = A (decr (Suc m) p)"
   1.376 +| "decr m F = F"
   1.377 +| "decr m (Lt t) = (Lt (decrtm m t))"
   1.378 +| "decr m (Le t) = (Le (decrtm m t))"
   1.379 +| "decr m (Eq t) = (Eq (decrtm m t))"
   1.380 +| "decr m (NEq t) = (NEq (decrtm m t))"
   1.381 +| "decr m (NOT p) = NOT (decr m p)" 
   1.382 +| "decr m (And p q) = conj (decr m p) (decr m q)"
   1.383 +| "decr m (Or p q) = disj (decr m p) (decr m q)"
   1.384 +| "decr m (Imp p q) = imp (decr m p) (decr m q)"
   1.385 +| "decr m (Iff p q) = iff (decr m p) (decr m q)"
   1.386 +| "decr m (E p) = E (decr (Suc m) p)"
   1.387 +| "decr m (A p) = A (decr (Suc m) p)"
   1.388  
   1.389  lemma decr: assumes  bnd: "boundslt (length bs) p" and nb: "bound m p" 
   1.390    and nle: "m < length bs" 
   1.391    shows "Ifm vs (removen m bs) (decr m p) = Ifm vs bs p"
   1.392    using bnd nb nle
   1.393 -proof(induct p arbitrary: bs m rule: decr.induct)
   1.394 +proof(induct p arbitrary: bs m rule: fm.induct)
   1.395    case (E p bs m) 
   1.396    {fix x
   1.397      from prems have bnd: "boundslt (length (x#bs)) p" and nb: "bound (Suc m) p" 
   1.398 @@ -642,55 +632,51 @@
   1.399    } thus ?case by auto
   1.400  qed (auto simp add: decrtm removen_nth)
   1.401  
   1.402 -consts
   1.403 -  subst0:: "tm \<Rightarrow> fm \<Rightarrow> fm"
   1.404 -
   1.405 -primrec
   1.406 +primrec subst0:: "tm \<Rightarrow> fm \<Rightarrow> fm" where
   1.407    "subst0 t T = T"
   1.408 -  "subst0 t F = F"
   1.409 -  "subst0 t (Lt a) = Lt (tmsubst0 t a)"
   1.410 -  "subst0 t (Le a) = Le (tmsubst0 t a)"
   1.411 -  "subst0 t (Eq a) = Eq (tmsubst0 t a)"
   1.412 -  "subst0 t (NEq a) = NEq (tmsubst0 t a)"
   1.413 -  "subst0 t (NOT p) = NOT (subst0 t p)"
   1.414 -  "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   1.415 -  "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   1.416 -  "subst0 t (Imp p q) = Imp (subst0 t p)  (subst0 t q)"
   1.417 -  "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   1.418 -  "subst0 t (E p) = E p"
   1.419 -  "subst0 t (A p) = A p"
   1.420 +| "subst0 t F = F"
   1.421 +| "subst0 t (Lt a) = Lt (tmsubst0 t a)"
   1.422 +| "subst0 t (Le a) = Le (tmsubst0 t a)"
   1.423 +| "subst0 t (Eq a) = Eq (tmsubst0 t a)"
   1.424 +| "subst0 t (NEq a) = NEq (tmsubst0 t a)"
   1.425 +| "subst0 t (NOT p) = NOT (subst0 t p)"
   1.426 +| "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   1.427 +| "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   1.428 +| "subst0 t (Imp p q) = Imp (subst0 t p)  (subst0 t q)"
   1.429 +| "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   1.430 +| "subst0 t (E p) = E p"
   1.431 +| "subst0 t (A p) = A p"
   1.432  
   1.433  lemma subst0: assumes qf: "qfree p"
   1.434    shows "Ifm vs (x#bs) (subst0 t p) = Ifm vs ((Itm vs (x#bs) t)#bs) p"
   1.435  using qf tmsubst0[where x="x" and bs="bs" and t="t"]
   1.436 -by (induct p rule: subst0.induct, auto)
   1.437 +by (induct p rule: fm.induct, auto)
   1.438  
   1.439  lemma subst0_nb:
   1.440    assumes bp: "tmbound0 t" and qf: "qfree p"
   1.441    shows "bound0 (subst0 t p)"
   1.442  using qf tmsubst0_nb[OF bp] bp
   1.443 -by (induct p rule: subst0.induct, auto)
   1.444 +by (induct p rule: fm.induct, auto)
   1.445  
   1.446 -consts   subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm" 
   1.447 -primrec
   1.448 +primrec subst:: "nat \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm" where
   1.449    "subst n t T = T"
   1.450 -  "subst n t F = F"
   1.451 -  "subst n t (Lt a) = Lt (tmsubst n t a)"
   1.452 -  "subst n t (Le a) = Le (tmsubst n t a)"
   1.453 -  "subst n t (Eq a) = Eq (tmsubst n t a)"
   1.454 -  "subst n t (NEq a) = NEq (tmsubst n t a)"
   1.455 -  "subst n t (NOT p) = NOT (subst n t p)"
   1.456 -  "subst n t (And p q) = And (subst n t p) (subst n t q)"
   1.457 -  "subst n t (Or p q) = Or (subst n t p) (subst n t q)"
   1.458 -  "subst n t (Imp p q) = Imp (subst n t p)  (subst n t q)"
   1.459 -  "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)"
   1.460 -  "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)"
   1.461 -  "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)"
   1.462 +| "subst n t F = F"
   1.463 +| "subst n t (Lt a) = Lt (tmsubst n t a)"
   1.464 +| "subst n t (Le a) = Le (tmsubst n t a)"
   1.465 +| "subst n t (Eq a) = Eq (tmsubst n t a)"
   1.466 +| "subst n t (NEq a) = NEq (tmsubst n t a)"
   1.467 +| "subst n t (NOT p) = NOT (subst n t p)"
   1.468 +| "subst n t (And p q) = And (subst n t p) (subst n t q)"
   1.469 +| "subst n t (Or p q) = Or (subst n t p) (subst n t q)"
   1.470 +| "subst n t (Imp p q) = Imp (subst n t p)  (subst n t q)"
   1.471 +| "subst n t (Iff p q) = Iff (subst n t p) (subst n t q)"
   1.472 +| "subst n t (E p) = E (subst (Suc n) (incrtm0 t) p)"
   1.473 +| "subst n t (A p) = A (subst (Suc n) (incrtm0 t) p)"
   1.474  
   1.475  lemma subst: assumes nb: "boundslt (length bs) p" and nlm: "n \<le> length bs"
   1.476    shows "Ifm vs bs (subst n t p) = Ifm vs (bs[n:= Itm vs bs t]) p"
   1.477    using nb nlm
   1.478 -proof (induct p arbitrary: bs n t rule: subst0.induct)
   1.479 +proof (induct p arbitrary: bs n t rule: fm.induct)
   1.480    case (E p bs n) 
   1.481    {fix x 
   1.482      from prems have bn: "boundslt (length (x#bs)) p" by simp 
   1.483 @@ -713,7 +699,7 @@
   1.484  lemma subst_nb: assumes tnb: "tmbound m t"
   1.485  shows "bound m (subst m t p)"
   1.486  using tnb tmsubst_nb incrtm0_tmbound
   1.487 -by (induct p arbitrary: m t rule: subst.induct, auto)
   1.488 +by (induct p arbitrary: m t rule: fm.induct, auto)
   1.489  
   1.490  lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
   1.491  by (induct p rule: not.induct, auto)
   1.492 @@ -2475,10 +2461,9 @@
   1.493  
   1.494  text {* Rest of the implementation *}
   1.495  
   1.496 -consts alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list"
   1.497 -primrec
   1.498 +primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where
   1.499    "alluopairs [] = []"
   1.500 -  "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
   1.501 +| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
   1.502  
   1.503  lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
   1.504  by (induct xs, auto)