src/HOL/Decision_Procs/MIR.thy
 changeset 41464 cb2e3e651893 parent 41413 64cd30d6b0b8 child 41807 ab5d2d81f9fb
```     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Fri Jan 07 18:10:35 2011 +0100
1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Jan 07 18:10:42 2011 +0100
1.3 @@ -3585,9 +3585,9 @@
1.4      thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
1.5        by (auto simp add: split_def)
1.6    qed
1.7 -  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
1.8 -    by (auto simp add: foldl_conv_concat)
1.9 -  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by auto
1.10 +  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
1.11 +    by (auto simp add: foldl_conv_concat simp del: iupt.simps)
1.12 +  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
1.13    also have "\<dots> =
1.14      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
1.15      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
1.16 @@ -3743,8 +3743,8 @@
1.17        by (auto simp add: split_def)
1.18    qed
1.19
1.20 -  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat)
1.21 -  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by auto
1.22 +  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat simp del: iupt.simps)
1.23 +  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
1.24    also have "\<dots> =
1.25      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
1.26      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
```