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)))" .
```