src/HOL/Decision_Procs/MIR.thy
 changeset 69313 b021008c5397 parent 69266 7cc2d66a92a6 child 69325 4b6ddc5989fc
```     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun Nov 18 09:51:41 2018 +0100
1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun Nov 18 18:07:51 2018 +0000
1.3 @@ -3377,22 +3377,23 @@
1.4    proof-
1.5      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
1.6      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
1.7 -    thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
1.8 +    thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
1.9        by (auto simp add: split_def)
1.10    qed
1.11    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.12      by auto
1.13 -  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.14 -    (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.15 -      proof-
1.16 +  hence U3: "(\<Union> ((\<lambda>(p,n,s). set (?ff (p,n,s))) ` {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0})) =
1.17 +    (\<Union> ((\<lambda>(p,n,s). set (map (?f(p,n,s)) [n..0])) ` {(p,n,s). (p,n,s)\<in> ?SS a\<and>n<0}))"
1.18 +  proof -
1.19      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
1.20      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
1.21 -    thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
1.22 +    thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
1.23        by (auto simp add: split_def)
1.24    qed
1.25 -  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
1.26 +  have "?SS (Floor a) = \<Union> ((\<lambda>x. set (?ff x)) ` ?SS a)"
1.27      by auto
1.28 -  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
1.29 +  also have "\<dots> = \<Union> ((\<lambda> (p,n,s). set (?ff (p,n,s))) ` ?SS a)"
1.30 +    by blast
1.31    also have "\<dots> =
1.32      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
1.33      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
1.34 @@ -3535,7 +3536,7 @@
1.35    proof-
1.36      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
1.37      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
1.38 -    thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
1.39 +    thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
1.40        by (auto simp add: split_def)
1.41    qed
1.42    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.43 @@ -3544,12 +3545,12 @@
1.44    proof-
1.45      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
1.46      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
1.47 -    thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
1.48 +    thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
1.49        by (auto simp add: split_def)
1.50    qed
1.51
1.52 -  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by auto
1.53 -  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
1.54 +  have "?SS (Floor a) = \<Union> ((\<lambda>x. set (?ff x)) ` ?SS a)" by auto
1.55 +  also have "\<dots> = \<Union> ((\<lambda> (p,n,s). set (?ff (p,n,s))) ` ?SS a)" by blast
1.56    also have "\<dots> =
1.57      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
1.58      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
```