src/HOL/BNF_Comp.thy
changeset 56166 9a241bc276cd
parent 56016 8875cdcfc85b
child 57698 afef6616cbae
     1.1 --- a/src/HOL/BNF_Comp.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/BNF_Comp.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4      fset_bd: "\<And>x. |fset x| \<le>o fbd" and
     1.5      gset_bd: "\<And>x. |gset x| \<le>o gbd"
     1.6    shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
     1.7 -apply (subst sym[OF SUP_def])
     1.8 +apply simp
     1.9  apply (rule ordLeq_transitive)
    1.10  apply (rule card_of_UNION_Sigma)
    1.11  apply (subst SIGMA_CSUM)
    1.12 @@ -69,7 +69,7 @@
    1.13  by blast
    1.14  
    1.15  lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
    1.16 -by (unfold comp_apply collect_def SUP_def)
    1.17 +by (unfold comp_apply collect_def) simp
    1.18  
    1.19  lemma wpull_cong:
    1.20  "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"