reorganization
authornipkow
Mon Mar 17 16:47:45 2008 +0100 (2008-03-17)
changeset 2629853e382ccf71f
parent 26297 74012d599204
child 26299 2f387f5c0f52
reorganization
src/HOL/Library/Order_Relation.thy
src/HOL/Library/Zorn.thy
     1.1 --- a/src/HOL/Library/Order_Relation.thy	Mon Mar 17 16:47:24 2008 +0100
     1.2 +++ b/src/HOL/Library/Order_Relation.thy	Mon Mar 17 16:47:45 2008 +0100
     1.3 @@ -8,9 +8,7 @@
     1.4  imports ATP_Linkup Hilbert_Choice
     1.5  begin
     1.6  
     1.7 -(* FIXME to Relation *)
     1.8 -
     1.9 -definition "refl_on A r \<equiv> \<forall>x\<in>A. (x,x) \<in> r"
    1.10 +text{* This prelude could be moved to theory Relation: *}
    1.11  
    1.12  definition "irrefl r \<equiv> \<forall>x. (x,x) \<notin> r"
    1.13  
    1.14 @@ -19,14 +17,11 @@
    1.15  abbreviation "total \<equiv> total_on UNIV"
    1.16  
    1.17  
    1.18 -lemma refl_on_empty[simp]: "refl_on {} r"
    1.19 -by(simp add:refl_on_def)
    1.20 -
    1.21  lemma total_on_empty[simp]: "total_on {} r"
    1.22  by(simp add:total_on_def)
    1.23  
    1.24 -lemma refl_on_converse[simp]: "refl_on A (r^-1) = refl_on A r"
    1.25 -by(simp add:refl_on_def)
    1.26 +lemma refl_on_converse[simp]: "refl A (r^-1) = refl A r"
    1.27 +by(auto simp add:refl_def)
    1.28  
    1.29  lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r"
    1.30  by (auto simp: total_on_def)
    1.31 @@ -42,9 +37,10 @@
    1.32  lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
    1.33  by(simp add: total_on_def)
    1.34  
    1.35 +
    1.36  subsection{* Orders on a set *}
    1.37  
    1.38 -definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
    1.39 +definition "preorder_on A r \<equiv> refl A r \<and> trans r"
    1.40  
    1.41  definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
    1.42  
    1.43 @@ -91,7 +87,7 @@
    1.44  
    1.45  subsection{* Orders on the field *}
    1.46  
    1.47 -abbreviation "Refl r \<equiv> refl_on (Field r) r"
    1.48 +abbreviation "Refl r \<equiv> refl (Field r) r"
    1.49  
    1.50  abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
    1.51  
    1.52 @@ -107,7 +103,7 @@
    1.53  lemma subset_Image_Image_iff:
    1.54    "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
    1.55     r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
    1.56 -apply(auto simp add:subset_def preorder_on_def refl_on_def Image_def)
    1.57 +apply(auto simp add:subset_def preorder_on_def refl_def Image_def)
    1.58  apply metis
    1.59  by(metis trans_def)
    1.60  
    1.61 @@ -117,7 +113,7 @@
    1.62  
    1.63  lemma Refl_antisym_eq_Image1_Image1_iff:
    1.64    "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
    1.65 -by(simp add: expand_set_eq antisym_def refl_on_def) metis
    1.66 +by(simp add: expand_set_eq antisym_def refl_def) metis
    1.67  
    1.68  lemma Partial_order_eq_Image1_Image1_iff:
    1.69    "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
     2.1 --- a/src/HOL/Library/Zorn.thy	Mon Mar 17 16:47:24 2008 +0100
     2.2 +++ b/src/HOL/Library/Zorn.thy	Mon Mar 17 16:47:45 2008 +0100
     2.3 @@ -301,7 +301,7 @@
     2.4        fix a B assume aB: "B:C" "a:B"
     2.5        with 1 obtain x where "x:Field r" "B = r^-1 `` {x}" by auto
     2.6        thus "(a,u) : r" using uA aB `Preorder r`
     2.7 -	by (auto simp add: preorder_on_def refl_on_def) (metis transD)
     2.8 +	by (auto simp add: preorder_on_def refl_def) (metis transD)
     2.9      qed
    2.10      thus "EX u:Field r. ?P u" using `u:Field r` by blast
    2.11    qed
    2.12 @@ -414,7 +414,7 @@
    2.13      by(simp add:Chain_def I_def) blast
    2.14    have FI: "Field I = ?WO" by(auto simp add:I_def init_seg_of_def Field_def)
    2.15    hence 0: "Partial_order I"
    2.16 -    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)
    2.17 +    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)
    2.18  -- {*I-chains have upper bounds in ?WO wrt I: their Union*}
    2.19    { fix R assume "R \<in> Chain I"
    2.20      hence Ris: "R \<in> Chain init_seg_of" using mono_Chain[OF I_init] by blast
    2.21 @@ -423,7 +423,7 @@
    2.22      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"
    2.23           "\<forall>r\<in>R. wf(r-Id)"
    2.24        using Chain_wo[OF `R \<in> Chain I`] by(simp_all add:order_on_defs)
    2.25 -    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:refl_on_def)
    2.26 +    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:refl_def)
    2.27      moreover have "trans (\<Union>R)"
    2.28        by(rule chain_subset_trans_Union[OF subch `\<forall>r\<in>R. trans r`])
    2.29      moreover have "antisym(\<Union>R)"
    2.30 @@ -455,7 +455,7 @@
    2.31      proof
    2.32        assume "m={}"
    2.33        moreover have "Well_order {(x,x)}"
    2.34 -	by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
    2.35 +	by(simp add:order_on_defs refl_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
    2.36        ultimately show False using max
    2.37  	by (auto simp:I_def init_seg_of_def simp del:Field_insert)
    2.38      qed
    2.39 @@ -470,7 +470,7 @@
    2.40      have "Refl m" "trans m" "antisym m" "Total m" "wf(m-Id)"
    2.41        using `Well_order m` by(simp_all add:order_on_defs)
    2.42  --{*We show that the extension is a well-order*}
    2.43 -    have "Refl ?m" using `Refl m` Fm by(auto simp:refl_on_def)
    2.44 +    have "Refl ?m" using `Refl m` Fm by(auto simp:refl_def)
    2.45      moreover have "trans ?m" using `trans m` `x \<notin> Field m`
    2.46        unfolding trans_def Field_def Domain_def Range_def by blast
    2.47      moreover have "antisym ?m" using `antisym m` `x \<notin> Field m`
    2.48 @@ -503,10 +503,10 @@
    2.49      using well_ordering[where 'a = "'a"] by blast
    2.50    let ?r = "{(x,y). x:A & y:A & (x,y):r}"
    2.51    have 1: "Field ?r = A" using wo univ
    2.52 -    by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_on_def)
    2.53 +    by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_def)
    2.54    have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)"
    2.55      using `Well_order r` by(simp_all add:order_on_defs)
    2.56 -  have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ)
    2.57 +  have "Refl ?r" using `Refl r` by(auto simp:refl_def 1 univ)
    2.58    moreover have "trans ?r" using `trans r`
    2.59      unfolding trans_def by blast
    2.60    moreover have "antisym ?r" using `antisym r`