# HG changeset patch
# User nipkow
# Date 1187601498 -7200
# Node ID fff40259f3366b3c0fc76dab10bf56ce56b9e6bb
# Parent  21b4350cf5ec3098e26f7961b6a40896387a4571
removed allpairs

diff -r 21b4350cf5ec -r fff40259f336 src/HOL/Complex/ex/MIR.thy
--- a/src/HOL/Complex/ex/MIR.thy	Mon Aug 20 11:18:07 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy	Mon Aug 20 11:18:18 2007 +0200
@@ -11,11 +11,6 @@
 
 declare real_of_int_floor_cancel [simp del]
 
-  (* All pairs from two lists *)
-
-lemma allpairs_set: "set (allpairs Pair xs ys) = {(x,y). x\<in> set xs \<and> y \<in> set ys}"
-by (induct xs) auto
-
 fun alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where 
   "alluopairs [] = []"
 | "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
@@ -3536,7 +3531,7 @@
 recdef rsplit0 "measure num_size"
   "rsplit0 (Bound 0) = [(T,1,C 0)]"
   "rsplit0 (Add a b) = (let acs = rsplit0 a ; bcs = rsplit0 b 
-              in map (\<lambda> ((p,n,t),(q,m,s)). (And p q, n+m, Add t s)) (allpairs Pair acs bcs))"
+              in map (\<lambda> ((p,n,t),(q,m,s)). (And p q, n+m, Add t s)) [(a,b). a\<leftarrow>acs,b\<leftarrow>bcs])"
   "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))"
   "rsplit0 (Neg a) = map (\<lambda> (p,n,s). (p,-n,Neg s)) (rsplit0 a)"
   "rsplit0 (Floor a) = foldl (op @) [] (map 
@@ -3692,8 +3687,8 @@
       ultimately show ?ths by auto
     qed
 next
-  case (3 a b) thus ?case by auto 
-qed (auto simp add: Let_def allpairs_set split_def ring_simps conj_rl)
+  case (3 a b) thus ?case by auto
+qed (auto simp add: Let_def split_def ring_simps conj_rl)
 
 lemma real_in_int_intervals: 
   assumes xb: "real m \<le> x \<and> x < real ((n::int) + 1)"
@@ -3710,8 +3705,8 @@
   then obtain "pa" "na" "sa" where pa: "(pa,na,sa)\<in> ?SS a \<and> ?I pa" by blast
   from prems have "\<exists> (pb,nb,sb) \<in> ?SS b. ?I pb" by auto
   then obtain "pb" "nb" "sb" where pb: "(pb,nb,sb)\<in> ?SS b \<and> ?I pb" by blast
-  from pa pb have th: "((pa,na,sa),(pb,nb,sb)) \<in> set (allpairs Pair (rsplit0 a) (rsplit0 b))"
-    by (auto simp add: allpairs_set)
+  from pa pb have th: "((pa,na,sa),(pb,nb,sb)) \<in> set[(x,y). x\<leftarrow>rsplit0 a, y\<leftarrow>rsplit0 b]"
+    by (auto)
   let ?f="(\<lambda> ((p,n,t),(q,m,s)). (And p q, n+m, Add t s))"
   from imageI[OF th, where f="?f"] have "?f ((pa,na,sa),(pb,nb,sb)) \<in> ?SS (Add a b)"
     by (simp add: Let_def)
@@ -5415,7 +5410,7 @@
    in if md = T then T else
     (let qd = evaldjf (\<lambda> t. simpfm (subst0 t q)) 
                                (remdups (map (\<lambda> (b,j). simpnum (Add b (C j))) 
-                                            (allpairs Pair B js)))
+                                            [(b,j). b\<leftarrow>B,j\<leftarrow>js]))
      in decr (disj md qd)))"
 lemma cooper: assumes qf: "qfree p"
   shows "((\<exists> (x::int). Ifm (real x#bs) p) = (Ifm bs (cooper p))) \<and> qfree (cooper p)" 
@@ -5431,8 +5426,8 @@
   let ?smq = "simpfm ?mq"
   let ?md = "evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js"
   let ?N = "\<lambda> t. Inum (real (i::int)#bs) t"
-  let ?bjs = "allpairs Pair ?B ?js"
-  let ?sbjs = "map (\<lambda> (b,j). simpnum (Add b (C j))) (allpairs Pair ?B ?js)"
+  let ?bjs = "[(b,j). b\<leftarrow>?B,j\<leftarrow>?js]"
+  let ?sbjs = "map (\<lambda> (b,j). simpnum (Add b (C j))) ?bjs"
   let ?qd = "evaldjf (\<lambda> t. simpfm (subst0 t ?q)) (remdups ?sbjs)"
   have qbf:"unit p = (?q,?B,?d)" by simp
   from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and 
@@ -5448,10 +5443,10 @@
   hence th: "\<forall> j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
     by (auto simp add: simpfm_bound0)
   from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp 
-  from Bn jsnb have "\<forall> (b,j) \<in> set (allpairs Pair ?B ?js). numbound0 (Add b (C j))"
-    by (simp add: allpairs_set)
-  hence "\<forall> (b,j) \<in> set (allpairs Pair ?B ?js). numbound0 (simpnum (Add b (C j)))"
-    using simpnum_numbound0 by blast 
+  from Bn jsnb have "\<forall> (b,j) \<in> set ?bjs. numbound0 (Add b (C j))"
+    by simp
+  hence "\<forall> (b,j) \<in> set ?bjs. numbound0 (simpnum (Add b (C j)))"
+    using simpnum_numbound0 by blast
   hence "\<forall> t \<in> set ?sbjs. numbound0 t" by simp
   hence "\<forall> t \<in> set (remdups ?sbjs). bound0 (subst0 t ?q)"
     using subst0_bound0[OF qfq] by auto 
@@ -5463,8 +5458,8 @@
   from trans [OF pq_ex cp_thm'[OF lq uq dd dp]] B
   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
   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
-  also have "\<dots>= ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> t \<in> (\<lambda> (b,j). ?N (Add b (C j))) ` set (allpairs Pair ?B ?js). Ifm (t #bs) ?q))" by (simp only: allpairs_set) simp
-  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 (allpairs Pair ?B ?js). Ifm (t #bs) ?q))" by (simp only: simpnum_ci)
+  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
+  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)
   also  have "\<dots>= ((\<exists> j\<in> set ?js. ?I j ?smq) \<or> (\<exists> t \<in> set ?sbjs. Ifm (?N t #bs) ?q))" 
     by (auto simp add: split_def) 
   also have "\<dots> = ((\<exists> j\<in> set ?js. (\<lambda> j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or> (\<exists> t \<in> set (remdups ?sbjs). (\<lambda> t. ?I i (simpfm (subst0 t ?q))) t))" by (simp only: simpfm subst0_I[OF qfq] simpfm Inum.simps subst0_I[OF qfmq] set_remdups)
diff -r 21b4350cf5ec -r fff40259f336 src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 20 11:18:07 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 20 11:18:18 2007 +0200
@@ -1766,13 +1766,6 @@
   ultimately show "?E" by blast
 qed
 
-consts allpairs:: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list"
-primrec
-  "allpairs [] ys = []"
-  "allpairs (x#xs) ys = (map (Pair x) ys)@(allpairs xs ys)"
-
-lemma allpairs_set: "set (allpairs xs ys) = {(x,y). x\<in> set xs \<and> y \<in> set ys}"
-by (induct xs) auto
 
     (* Implement the right hand side of Ferrante and Rackoff's Theorem. *)
 constdefs ferrack:: "fm \<Rightarrow> fm"
diff -r 21b4350cf5ec -r fff40259f336 src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Mon Aug 20 11:18:07 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Aug 20 11:18:18 2007 +0200
@@ -1850,7 +1850,7 @@
        md = evaldjf (\<lambda> j. simpfm (subst0 (C j) mq)) js
    in if md = T then T else
     (let qd = evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) q)) 
-                               (allpairs Pair B js)
+                               [(b,j). b\<leftarrow>B,j\<leftarrow>js]
      in decr (disj md qd)))"
 lemma cooper: assumes qf: "qfree p"
   shows "((\<exists> x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \<and> qfree (cooper p)" 
@@ -1866,7 +1866,8 @@
   let ?smq = "simpfm ?mq"
   let ?md = "evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js"
   let ?N = "\<lambda> t. Inum (i#bs) t"
-  let ?qd = "evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) (allpairs Pair ?B ?js)"
+  let ?Bjs = "[(b,j). b\<leftarrow>?B,j\<leftarrow>?js]"
+  let ?qd = "evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs"
   have qbf:"unit p = (?q,?B,?d)" by simp
   from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and 
     B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and 
@@ -1881,13 +1882,13 @@
   hence th: "\<forall> j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
     by (auto simp add: simpfm_bound0)
   from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp 
-  from Bn jsnb have "\<forall> (b,j) \<in> set (allpairs Pair ?B ?js). numbound0 (Add b (C j))"
+  from Bn jsnb have "\<forall> (b,j) \<in> set ?Bjs. numbound0 (Add b (C j))"
     by simp
-  hence "\<forall> (b,j) \<in> set (allpairs Pair ?B ?js). bound0 (subst0 (Add b (C j)) ?q)"
+  hence "\<forall> (b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)"
     using subst0_bound0[OF qfq] by blast
-  hence "\<forall> (b,j) \<in> set (allpairs Pair ?B ?js). bound0 (simpfm (subst0 (Add b (C j)) ?q))"
+  hence "\<forall> (b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))"
     using simpfm_bound0  by blast
-  hence th': "\<forall> x \<in> set (allpairs Pair ?B ?js). bound0 ((\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
+  hence th': "\<forall> x \<in> set ?Bjs. bound0 ((\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
     by auto 
   from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp
   from mdb qdb 
@@ -1901,10 +1902,10 @@
     by (simp only: simpfm subst0_I[OF qfmq] iupt_set) auto
   also have "\<dots> = (?I i (evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js) \<or> (\<exists> j\<in> set ?js. \<exists> b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q)))" 
    by (simp only: evaldjf_ex subst0_I[OF qfq])
- also have "\<dots>= (?I i ?md \<or> (\<exists> (b,j) \<in> set (allpairs Pair ?B ?js). (\<lambda> (b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j)))"
-   by (simp only: simpfm set_allpairs) blast
- also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) (allpairs Pair ?B ?js))))"
-   by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="allpairs Pair ?B ?js"]) (auto simp add: split_def)
+ also have "\<dots>= (?I i ?md \<or> (\<exists> (b,j) \<in> set ?Bjs. (\<lambda> (b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j)))"
+   by (simp only: simpfm set_concat set_map UN_simps) blast
+ also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))"
+   by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"]) (auto simp add: split_def)
  finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)" by simp  
   also have "\<dots> = (?I i (disj ?md ?qd))" by (simp add: disj)
   also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb])