src/HOL/Decision_Procs/MIR.thy
changeset 41836 c9d788ff7940
parent 41807 ab5d2d81f9fb
child 41839 421a795cee05
     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Wed Feb 23 17:40:28 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Feb 24 17:38:05 2011 +0100
     1.3 @@ -37,18 +37,6 @@
     1.4    with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
     1.5  qed
     1.6  
     1.7 -  (* generate a list from i to j*)
     1.8 -consts iupt :: "int \<times> int \<Rightarrow> int list"
     1.9 -recdef iupt "measure (\<lambda> (i,j). nat (j-i +1))" 
    1.10 -  "iupt (i,j) = (if j <i then [] else (i# iupt(i+1, j)))"
    1.11 -
    1.12 -lemma iupt_set: "set (iupt(i,j)) = {i .. j}"
    1.13 -proof(induct rule: iupt.induct)
    1.14 -  case (1 a b)
    1.15 -  show ?case
    1.16 -    using 1 by (simp add: simp_from_to)
    1.17 -qed
    1.18 -
    1.19  lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
    1.20  using Nat.gr0_conv_Suc
    1.21  by clarsimp
    1.22 @@ -3538,7 +3526,7 @@
    1.23    "rsplit0 (Neg a) = map (\<lambda> (p,n,s). (p,-n,Neg s)) (rsplit0 a)"
    1.24    "rsplit0 (Floor a) = foldl (op @) [] (map 
    1.25        (\<lambda> (p,n,s). if n=0 then [(p,0,Floor s)]
    1.26 -          else (map (\<lambda> j. (fp p n s j, 0, Add (Floor s) (C j))) (if n > 0 then iupt (0,n) else iupt(n,0))))
    1.27 +          else (map (\<lambda> j. (fp p n s j, 0, Add (Floor s) (C j))) (if n > 0 then [0 .. n] else [n .. 0])))
    1.28         (rsplit0 a))"
    1.29    "rsplit0 (CN 0 c a) = map (\<lambda> (p,n,s). (p,n+c,s)) (rsplit0 a)"
    1.30    "rsplit0 (CN m c a) = map (\<lambda> (p,n,s). (p,n,CN m c s)) (rsplit0 a)"
    1.31 @@ -3562,26 +3550,26 @@
    1.32    case (5 a) 
    1.33    let ?p = "\<lambda> (p,n,s) j. fp p n s j"
    1.34    let ?f = "(\<lambda> (p,n,s) j. (?p (p,n,s) j, (0::int),Add (Floor s) (C j)))"
    1.35 -  let ?J = "\<lambda> n. if n>0 then iupt (0,n) else iupt (n,0)"
    1.36 +  let ?J = "\<lambda> n. if n>0 then [0..n] else [n..0]"
    1.37    let ?ff=" (\<lambda> (p,n,s). if n= 0 then [(p,0,Floor s)] else map (?f (p,n,s)) (?J n))"
    1.38    have int_cases: "\<forall> (i::int). i= 0 \<or> i < 0 \<or> i > 0" by arith
    1.39    have U1: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = 
    1.40      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)]))" by auto
    1.41    have U2': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0}. 
    1.42 -    ?ff (p,n,s) = map (?f(p,n,s)) (iupt(0,n))" by auto
    1.43 +    ?ff (p,n,s) = map (?f(p,n,s)) [0..n]" by auto
    1.44    hence U2: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = 
    1.45      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). 
    1.46 -    set (map (?f(p,n,s)) (iupt(0,n)))))"
    1.47 +    set (map (?f(p,n,s)) [0..n])))"
    1.48    proof-
    1.49      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
    1.50      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
    1.51      thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
    1.52        by (auto simp add: split_def)
    1.53    qed
    1.54 -  have U3': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0}. ?ff (p,n,s) = map (?f(p,n,s)) (iupt(n,0))"
    1.55 +  have U3': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0}. ?ff (p,n,s) = map (?f(p,n,s)) [n..0]"
    1.56      by auto
    1.57    hence U3: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = 
    1.58 -    (UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n<0} (\<lambda>(p,n,s). set (map (?f(p,n,s)) (iupt(n,0)))))"
    1.59 +    (UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n<0} (\<lambda>(p,n,s). set (map (?f(p,n,s)) [n..0])))"
    1.60        proof-
    1.61      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
    1.62      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
    1.63 @@ -3589,7 +3577,7 @@
    1.64        by (auto simp add: split_def)
    1.65    qed
    1.66    have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
    1.67 -    by (auto simp add: foldl_conv_concat simp del: iupt.simps)
    1.68 +    by (auto simp add: foldl_conv_concat)
    1.69    also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
    1.70    also have "\<dots> = 
    1.71      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un 
    1.72 @@ -3598,14 +3586,14 @@
    1.73      using int_cases[rule_format] by blast
    1.74    also have "\<dots> =  
    1.75      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un 
    1.76 -   (UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n>0} (\<lambda>(p,n,s). set(map(?f(p,n,s)) (iupt(0,n))))) Un 
    1.77 +   (UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n>0} (\<lambda>(p,n,s). set(map(?f(p,n,s)) [0..n]))) Un 
    1.78     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). 
    1.79 -    set (map (?f(p,n,s)) (iupt(n,0))))))" by (simp only: U1 U2 U3)
    1.80 +    set (map (?f(p,n,s)) [n..0]))))" by (simp only: U1 U2 U3)
    1.81    also have "\<dots> =  
    1.82      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
    1.83      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un 
    1.84      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {n .. 0})))"
    1.85 -    by (simp only: set_map iupt_set set.simps)
    1.86 +    by (simp only: set_map set_upto set.simps)
    1.87    also have "\<dots> =   
    1.88      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
    1.89      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un 
    1.90 @@ -3723,22 +3711,22 @@
    1.91    case (5 a) 
    1.92    let ?p = "\<lambda> (p,n,s) j. fp p n s j"
    1.93    let ?f = "(\<lambda> (p,n,s) j. (?p (p,n,s) j, (0::int),(Add (Floor s) (C j))))"
    1.94 -  let ?J = "\<lambda> n. if n>0 then iupt (0,n) else iupt (n,0)"
    1.95 +  let ?J = "\<lambda> n. if n>0 then [0..n] else [n..0]"
    1.96    let ?ff=" (\<lambda> (p,n,s). if n= 0 then [(p,0,Floor s)] else map (?f (p,n,s)) (?J n))"
    1.97    have int_cases: "\<forall> (i::int). i= 0 \<or> i < 0 \<or> i > 0" by arith
    1.98    have U1: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)]))" by auto
    1.99 -  have U2': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0}. ?ff (p,n,s) = map (?f(p,n,s)) (iupt(0,n))"
   1.100 +  have U2': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0}. ?ff (p,n,s) = map (?f(p,n,s)) [0..n]"
   1.101      by auto
   1.102 -  hence U2: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) (iupt(0,n)))))"
   1.103 +  hence U2: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) [0..n])))"
   1.104    proof-
   1.105      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
   1.106      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
   1.107      thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
   1.108        by (auto simp add: split_def)
   1.109    qed
   1.110 -  have U3': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0}. ?ff (p,n,s) = map (?f(p,n,s)) (iupt(n,0))"
   1.111 +  have U3': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0}. ?ff (p,n,s) = map (?f(p,n,s)) [n..0]"
   1.112      by auto
   1.113 -  hence U3: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) (iupt(n,0)))))"
   1.114 +  hence U3: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) = (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) [n..0])))"
   1.115    proof-
   1.116      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
   1.117      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
   1.118 @@ -3746,7 +3734,7 @@
   1.119        by (auto simp add: split_def)
   1.120    qed
   1.121  
   1.122 -  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat simp del: iupt.simps) 
   1.123 +  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat) 
   1.124    also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
   1.125    also have "\<dots> = 
   1.126      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un 
   1.127 @@ -3755,13 +3743,13 @@
   1.128      using int_cases[rule_format] by blast
   1.129    also have "\<dots> =  
   1.130      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un 
   1.131 -    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) (iupt(0,n))))) Un 
   1.132 -    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) (iupt(n,0))))))" by (simp only: U1 U2 U3)
   1.133 +    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) [0..n]))) Un 
   1.134 +    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) [n..0]))))" by (simp only: U1 U2 U3)
   1.135    also have "\<dots> =  
   1.136      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
   1.137      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {0 .. n})) Un 
   1.138      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). (?f(p,n,s)) ` {n .. 0})))"
   1.139 -    by (simp only: set_map iupt_set set.simps)
   1.140 +    by (simp only: set_map set_upto set.simps)
   1.141    also have "\<dots> =   
   1.142      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un 
   1.143      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un 
   1.144 @@ -4023,12 +4011,12 @@
   1.145  definition
   1.146    DVDJ:: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm"
   1.147  where
   1.148 -  DVDJ_def: "DVDJ i n s = (foldr disj (map (\<lambda> j. conj (Eq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) F)"
   1.149 +  DVDJ_def: "DVDJ i n s = (foldr disj (map (\<lambda> j. conj (Eq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))) [0..n - 1]) F)"
   1.150  
   1.151  definition
   1.152    NDVDJ:: "int \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm"
   1.153  where
   1.154 -  NDVDJ_def: "NDVDJ i n s = (foldr conj (map (\<lambda> j. disj (NEq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor (Neg s))))) (iupt(0,n - 1))) T)"
   1.155 +  NDVDJ_def: "NDVDJ i n s = (foldr conj (map (\<lambda> j. disj (NEq (CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor (Neg s))))) [0..n - 1]) T)"
   1.156  
   1.157  lemma DVDJ_DVD: 
   1.158    assumes xp:"x\<ge> 0" and x1: "x < 1" and np:"real n > 0"
   1.159 @@ -4036,9 +4024,9 @@
   1.160  proof-
   1.161    let ?f = "\<lambda> j. conj (Eq(CN 0 n (Add s (Sub(Floor (Neg s)) (C j))))) (Dvd i (Sub (C j) (Floor (Neg s))))"
   1.162    let ?s= "Inum (x#bs) s"
   1.163 -  from foldr_disj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
   1.164 +  from foldr_disj_map[where xs="[0..n - 1]" and bs="x#bs" and f="?f"]
   1.165    have "Ifm (x#bs) (DVDJ i n s) = (\<exists> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" 
   1.166 -    by (simp add: iupt_set np DVDJ_def del: iupt.simps)
   1.167 +    by (simp add: np DVDJ_def)
   1.168    also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: algebra_simps diff_minus[symmetric])
   1.169    also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] 
   1.170    have "\<dots> = (real i rdvd real n * x - (-?s))" by simp
   1.171 @@ -4051,9 +4039,9 @@
   1.172  proof-
   1.173    let ?f = "\<lambda> j. disj(NEq(CN 0 n (Add s (Sub (Floor (Neg s)) (C j))))) (NDvd i (Sub (C j) (Floor(Neg s))))"
   1.174    let ?s= "Inum (x#bs) s"
   1.175 -  from foldr_conj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
   1.176 +  from foldr_conj_map[where xs="[0..n - 1]" and bs="x#bs" and f="?f"]
   1.177    have "Ifm (x#bs) (NDVDJ i n s) = (\<forall> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))" 
   1.178 -    by (simp add: iupt_set np NDVDJ_def del: iupt.simps)
   1.179 +    by (simp add: np NDVDJ_def)
   1.180    also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: algebra_simps diff_minus[symmetric])
   1.181    also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"] 
   1.182    have "\<dots> = (\<not> (real i rdvd real n * x - (-?s)))" by simp
   1.183 @@ -5422,7 +5410,7 @@
   1.184  
   1.185  definition cooper :: "fm \<Rightarrow> fm" where
   1.186    "cooper p \<equiv> 
   1.187 -  (let (q,B,d) = unit p; js = iupt (1,d);
   1.188 +  (let (q,B,d) = unit p; js = [1..d];
   1.189         mq = simpfm (minusinf q);
   1.190         md = evaldjf (\<lambda> j. simpfm (subst0 (C j) mq)) js
   1.191     in if md = T then T else
   1.192 @@ -5439,7 +5427,7 @@
   1.193    let ?q = "fst (unit p)"
   1.194    let ?B = "fst (snd(unit p))"
   1.195    let ?d = "snd (snd (unit p))"
   1.196 -  let ?js = "iupt (1,?d)"
   1.197 +  let ?js = "[1..?d]"
   1.198    let ?mq = "minusinf ?q"
   1.199    let ?smq = "simpfm ?mq"
   1.200    let ?md = "evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js"
   1.201 @@ -5476,7 +5464,7 @@
   1.202    have mdqdb: "bound0 (disj ?md ?qd)" by (simp only: disj_def, cases "?md=T \<or> ?qd=T", simp_all)
   1.203    from trans [OF pq_ex cp_thm'[OF lq uq dd dp]] B
   1.204    have "?lhs = (\<exists> j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists> b\<in> ?N ` set ?B. Ifm ((b+ real j)#bs) ?q))" by auto
   1.205 -  also have "\<dots> = ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> (b,j) \<in> (?N ` set ?B \<times> set ?js). Ifm ((b+ real j)#bs) ?q))" apply (simp only: iupt_set simpfm) by auto
   1.206 +  also have "\<dots> = ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> (b,j) \<in> (?N ` set ?B \<times> set ?js). Ifm ((b+ real j)#bs) ?q))" by auto
   1.207    also have "\<dots>= ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> t \<in> (\<lambda> (b,j). ?N (Add b (C j))) ` set ?bjs. Ifm (t #bs) ?q))" by simp
   1.208    also have "\<dots>= ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> t \<in> (\<lambda> (b,j). ?N (simpnum (Add b (C j)))) ` set ?bjs. Ifm (t #bs) ?q))" by (simp only: simpnum_ci)
   1.209    also  have "\<dots>= ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> t \<in> set ?sbjs. Ifm (?N t #bs) ?q))" 
   1.210 @@ -5625,16 +5613,16 @@
   1.211  qed
   1.212  
   1.213  definition stage :: "fm \<Rightarrow> int \<Rightarrow> (num \<times> int) \<Rightarrow> fm" where
   1.214 -  "stage p d \<equiv> (\<lambda> (e,c). evaldjf (\<lambda> j. simpfm (\<sigma> p c (Add e (C j)))) (iupt (1,c*d)))"
   1.215 +  "stage p d \<equiv> (\<lambda> (e,c). evaldjf (\<lambda> j. simpfm (\<sigma> p c (Add e (C j)))) [1..c*d])"
   1.216  lemma stage:
   1.217    shows "Ifm bs (stage p d (e,c)) = (\<exists> j\<in>{1 .. c*d}. Ifm bs (\<sigma> p c (Add e (C j))))"
   1.218 -  by (unfold stage_def split_def ,simp only: evaldjf_ex iupt_set simpfm) simp
   1.219 +  by (unfold stage_def split_def ,simp only: evaldjf_ex simpfm) simp
   1.220  
   1.221  lemma stage_nb: assumes lp: "iszlfm p (a#bs)" and cp: "c >0" and nb:"numbound0 e"
   1.222    shows "bound0 (stage p d (e,c))"
   1.223  proof-
   1.224    let ?f = "\<lambda> j. simpfm (\<sigma> p c (Add e (C j)))"
   1.225 -  have th: "\<forall> j\<in> set (iupt(1,c*d)). bound0 (?f j)"
   1.226 +  have th: "\<forall> j\<in> set [1..c*d]. bound0 (?f j)"
   1.227    proof
   1.228      fix j
   1.229      from nb have nb':"numbound0 (Add e (C j))" by simp
   1.230 @@ -5648,7 +5636,7 @@
   1.231    "redlove p \<equiv> 
   1.232    (let (q,B,d) = chooset p;
   1.233         mq = simpfm (minusinf q);
   1.234 -       md = evaldjf (\<lambda> j. simpfm (subst0 (C j) mq)) (iupt (1,d))
   1.235 +       md = evaldjf (\<lambda> j. simpfm (subst0 (C j) mq)) [1..d]
   1.236     in if md = T then T else
   1.237      (let qd = evaldjf (stage q d) B
   1.238       in decr (disj md qd)))"
   1.239 @@ -5662,7 +5650,7 @@
   1.240    let ?q = "fst (chooset p)"
   1.241    let ?B = "fst (snd(chooset p))"
   1.242    let ?d = "snd (snd (chooset p))"
   1.243 -  let ?js = "iupt (1,?d)"
   1.244 +  let ?js = "[1..?d]"
   1.245    let ?mq = "minusinf ?q"
   1.246    let ?smq = "simpfm ?mq"
   1.247    let ?md = "evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js"
   1.248 @@ -5692,7 +5680,7 @@
   1.249      by (simp add: simpfm stage split_def)
   1.250    also have "\<dots> = ((\<exists> j\<in> {1 .. ?d}. ?I i (subst0 (C j) ?smq))  \<or> ?I i ?qd)"
   1.251      by (simp add: evaldjf_ex subst0_I[OF qfmq])
   1.252 -  finally have mdqd:"?lhs = (?I i ?md \<or> ?I i ?qd)" by (simp only: evaldjf_ex iupt_set simpfm) 
   1.253 +  finally have mdqd:"?lhs = (?I i ?md \<or> ?I i ?qd)" by (simp only: evaldjf_ex set_upto simpfm) 
   1.254    also have "\<dots> = (?I i (disj ?md ?qd))" by (simp add: disj)
   1.255    also have "\<dots> = (Ifm bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb]) 
   1.256    finally have mdqd2: "?lhs = (Ifm bs (decr (disj ?md ?qd)))" .