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