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