src/HOL/Library/Zorn.thy
changeset 46752 e9e7209eb375
parent 46008 c296c75f4cf4
child 46980 6bc213e90401
     1.1 --- a/src/HOL/Library/Zorn.thy	Thu Mar 01 17:13:54 2012 +0000
     1.2 +++ b/src/HOL/Library/Zorn.thy	Thu Mar 01 19:34:52 2012 +0100
     1.3 @@ -453,7 +453,7 @@
     1.4      proof
     1.5        assume "m={}"
     1.6        moreover have "Well_order {(x,x)}"
     1.7 -        by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
     1.8 +        by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_unfold Domain_converse [symmetric])
     1.9        ultimately show False using max
    1.10          by (auto simp:I_def init_seg_of_def simp del:Field_insert)
    1.11      qed
    1.12 @@ -470,14 +470,14 @@
    1.13  --{*We show that the extension is a well-order*}
    1.14      have "Refl ?m" using `Refl m` Fm by(auto simp:refl_on_def)
    1.15      moreover have "trans ?m" using `trans m` `x \<notin> Field m`
    1.16 -      unfolding trans_def Field_def Domain_def Range_def by blast
    1.17 +      unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast
    1.18      moreover have "antisym ?m" using `antisym m` `x \<notin> Field m`
    1.19 -      unfolding antisym_def Field_def Domain_def Range_def by blast
    1.20 +      unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast
    1.21      moreover have "Total ?m" using `Total m` Fm by(auto simp: total_on_def)
    1.22      moreover have "wf(?m-Id)"
    1.23      proof-
    1.24        have "wf ?s" using `x \<notin> Field m`
    1.25 -        by(auto simp add:wf_eq_minimal Field_def Domain_def Range_def) metis
    1.26 +        by(auto simp add:wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis
    1.27        thus ?thesis using `wf(m-Id)` `x \<notin> Field m`
    1.28          wf_subset[OF `wf ?s` Diff_subset]
    1.29          by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)
    1.30 @@ -485,7 +485,7 @@
    1.31      ultimately have "Well_order ?m" by(simp add:order_on_defs)
    1.32  --{*We show that the extension is above m*}
    1.33      moreover hence "(m,?m) : I" using `Well_order m` `x \<notin> Field m`
    1.34 -      by(fastforce simp:I_def init_seg_of_def Field_def Domain_def Range_def)
    1.35 +      by(fastforce simp:I_def init_seg_of_def Field_def Domain_unfold Domain_converse [symmetric])
    1.36      ultimately
    1.37  --{*This contradicts maximality of m:*}
    1.38      have False using max `x \<notin> Field m` unfolding Field_def by blast
    1.39 @@ -501,7 +501,7 @@
    1.40      using well_ordering[where 'a = "'a"] by blast
    1.41    let ?r = "{(x,y). x:A & y:A & (x,y):r}"
    1.42    have 1: "Field ?r = A" using wo univ
    1.43 -    by(fastforce simp: Field_def Domain_def Range_def order_on_defs refl_on_def)
    1.44 +    by(fastforce simp: Field_def Domain_unfold Domain_converse [symmetric] order_on_defs refl_on_def)
    1.45    have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)"
    1.46      using `Well_order r` by(simp_all add:order_on_defs)
    1.47    have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ)