src/HOL/Library/Zorn.thy
changeset 30198 922f944f03b2
parent 28952 15a4b2cf8c34
child 30663 0b6aff7451b2
     1.1 --- a/src/HOL/Library/Zorn.thy	Mon Mar 02 08:26:03 2009 +0100
     1.2 +++ b/src/HOL/Library/Zorn.thy	Mon Mar 02 16:53:55 2009 +0100
     1.3 @@ -297,7 +297,7 @@
     1.4        fix a B assume aB: "B:C" "a:B"
     1.5        with 1 obtain x where "x:Field r" "B = r^-1 `` {x}" by auto
     1.6        thus "(a,u) : r" using uA aB `Preorder r`
     1.7 -	by (auto simp add: preorder_on_def refl_def) (metis transD)
     1.8 +	by (auto simp add: preorder_on_def refl_on_def) (metis transD)
     1.9      qed
    1.10      thus "EX u:Field r. ?P u" using `u:Field r` by blast
    1.11    qed
    1.12 @@ -322,7 +322,7 @@
    1.13               (infix "initial'_segment'_of" 55) where
    1.14  "r initial_segment_of s == (r,s):init_seg_of"
    1.15  
    1.16 -lemma refl_init_seg_of[simp]: "r initial_segment_of r"
    1.17 +lemma refl_on_init_seg_of[simp]: "r initial_segment_of r"
    1.18  by(simp add:init_seg_of_def)
    1.19  
    1.20  lemma trans_init_seg_of:
    1.21 @@ -411,7 +411,7 @@
    1.22      by(simp add:Chain_def I_def) blast
    1.23    have FI: "Field I = ?WO" by(auto simp add:I_def init_seg_of_def Field_def)
    1.24    hence 0: "Partial_order I"
    1.25 -    by(auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_def trans_def I_def elim!: trans_init_seg_of)
    1.26 +    by(auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def trans_def I_def elim!: trans_init_seg_of)
    1.27  -- {*I-chains have upper bounds in ?WO wrt I: their Union*}
    1.28    { fix R assume "R \<in> Chain I"
    1.29      hence Ris: "R \<in> Chain init_seg_of" using mono_Chain[OF I_init] by blast
    1.30 @@ -420,7 +420,7 @@
    1.31      have "\<forall>r\<in>R. Refl r" "\<forall>r\<in>R. trans r" "\<forall>r\<in>R. antisym r" "\<forall>r\<in>R. Total r"
    1.32           "\<forall>r\<in>R. wf(r-Id)"
    1.33        using Chain_wo[OF `R \<in> Chain I`] by(simp_all add:order_on_defs)
    1.34 -    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:refl_def)
    1.35 +    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:refl_on_def)
    1.36      moreover have "trans (\<Union>R)"
    1.37        by(rule chain_subset_trans_Union[OF subch `\<forall>r\<in>R. trans r`])
    1.38      moreover have "antisym(\<Union>R)"
    1.39 @@ -452,7 +452,7 @@
    1.40      proof
    1.41        assume "m={}"
    1.42        moreover have "Well_order {(x,x)}"
    1.43 -	by(simp add:order_on_defs refl_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
    1.44 +	by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
    1.45        ultimately show False using max
    1.46  	by (auto simp:I_def init_seg_of_def simp del:Field_insert)
    1.47      qed
    1.48 @@ -467,7 +467,7 @@
    1.49      have "Refl m" "trans m" "antisym m" "Total m" "wf(m-Id)"
    1.50        using `Well_order m` by(simp_all add:order_on_defs)
    1.51  --{*We show that the extension is a well-order*}
    1.52 -    have "Refl ?m" using `Refl m` Fm by(auto simp:refl_def)
    1.53 +    have "Refl ?m" using `Refl m` Fm by(auto simp:refl_on_def)
    1.54      moreover have "trans ?m" using `trans m` `x \<notin> Field m`
    1.55        unfolding trans_def Field_def Domain_def Range_def by blast
    1.56      moreover have "antisym ?m" using `antisym m` `x \<notin> Field m`
    1.57 @@ -500,10 +500,10 @@
    1.58      using well_ordering[where 'a = "'a"] by blast
    1.59    let ?r = "{(x,y). x:A & y:A & (x,y):r}"
    1.60    have 1: "Field ?r = A" using wo univ
    1.61 -    by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_def)
    1.62 +    by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_on_def)
    1.63    have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)"
    1.64      using `Well_order r` by(simp_all add:order_on_defs)
    1.65 -  have "Refl ?r" using `Refl r` by(auto simp:refl_def 1 univ)
    1.66 +  have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ)
    1.67    moreover have "trans ?r" using `trans r`
    1.68      unfolding trans_def by blast
    1.69    moreover have "antisym ?r" using `antisym r`