--- a/src/HOL/Complex/ex/MIR.thy Wed Aug 29 13:58:00 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Wed Aug 29 14:21:19 2007 +0200
@@ -3586,8 +3586,8 @@
thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
by (auto simp add: split_def)
qed
- from foldl_append_map_Nil_set[where xs="rsplit0 a" and f="?ff"]
- have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by auto
+ have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
+ by (auto simp add: foldl_conv_concat)
also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by auto
also have "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
@@ -3739,8 +3739,8 @@
thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
by (auto simp add: split_def)
qed
- from foldl_append_map_Nil_set[where xs="rsplit0 a" and f="?ff"]
- have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by auto
+
+ have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat)
also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by auto
also have "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
@@ -5810,6 +5810,10 @@
apply mir
done
+(*
+lemma "ALL x y. \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
+by mir
+*)
ML "reset Toplevel.timing"
end