# HG changeset patch
# User nipkow
# Date 1205750566 -3600
# Node ID afc43168ed8586f940203d8ca08dda500c4e7015
# Parent  c5fe289de63421d95085e6755a0351a6722fbfe9
More defns and thms

diff -r c5fe289de634 -r afc43168ed85 src/HOL/Library/Order_Relation.thy
--- a/src/HOL/Library/Order_Relation.thy	Mon Mar 17 07:15:40 2008 +0100
+++ b/src/HOL/Library/Order_Relation.thy	Mon Mar 17 11:42:46 2008 +0100
@@ -1,7 +1,5 @@
 (*  ID          : $Id$
     Author      : Tobias Nipkow
-
-Orders as relations with implicit base set, their Field
 *)
 
 header {* Orders as Relations *}
@@ -10,53 +8,106 @@
 imports ATP_Linkup Hilbert_Choice
 begin
 
-definition "Refl r \<equiv> \<forall>x \<in> Field r. (x,x) \<in> r"
-definition "Preorder r \<equiv> Refl r \<and> trans r"
-definition "Partial_order r \<equiv> Preorder r \<and> antisym r"
-definition "Total r \<equiv> \<forall>x\<in>Field r.\<forall>y\<in>Field r. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r"
-definition "Linear_order r \<equiv> Partial_order r \<and> Total r"
-definition "Well_order r \<equiv> Linear_order r \<and> wf(r - Id)"
+(* FIXME to Relation *)
+
+definition "refl_on A r \<equiv> \<forall>x\<in>A. (x,x) \<in> r"
+
+definition "irrefl r \<equiv> \<forall>x. (x,x) \<notin> r"
+
+definition "total_on A r \<equiv> \<forall>x\<in>A.\<forall>y\<in>A. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r"
+
+abbreviation "total \<equiv> total_on UNIV"
+
+
+lemma refl_on_empty[simp]: "refl_on {} r"
+by(simp add:refl_on_def)
+
+lemma total_on_empty[simp]: "total_on {} r"
+by(simp add:total_on_def)
+
+lemma refl_on_converse[simp]: "refl_on A (r^-1) = refl_on A r"
+by(simp add:refl_on_def)
+
+lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r"
+by (auto simp: total_on_def)
 
-lemmas Order_defs =
-  Preorder_def Partial_order_def Linear_order_def Well_order_def
+lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
+by(simp add:irrefl_def)
 
-lemma Refl_empty[simp]: "Refl {}"
-by(simp add:Refl_def)
+declare [[simp_depth_limit = 2]]
+lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
+by(simp add: antisym_def trans_def) blast
+declare [[simp_depth_limit = 50]]
+
+lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
+by(simp add: total_on_def)
 
-lemma Preorder_empty[simp]: "Preorder {}"
-by(simp add:Preorder_def trans_def)
+subsection{* Orders on a set *}
+
+definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
+
+definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
 
-lemma Partial_order_empty[simp]: "Partial_order {}"
-by(simp add:Partial_order_def)
+definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"
+
+definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"
+
+definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)"
 
-lemma Total_empty[simp]: "Total {}"
-by(simp add:Total_def)
+lemmas order_on_defs =
+  preorder_on_def partial_order_on_def linear_order_on_def
+  strict_linear_order_on_def well_order_on_def
+
 
-lemma Linear_order_empty[simp]: "Linear_order {}"
-by(simp add:Linear_order_def)
+lemma preorder_on_empty[simp]: "preorder_on {} {}"
+by(simp add:preorder_on_def trans_def)
+
+lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
+by(simp add:partial_order_on_def)
 
-lemma Well_order_empty[simp]: "Well_order {}"
-by(simp add:Well_order_def)
+lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
+by(simp add:linear_order_on_def)
+
+lemma well_order_on_empty[simp]: "well_order_on {} {}"
+by(simp add:well_order_on_def)
+
 
-lemma Refl_converse[simp]: "Refl(r^-1) = Refl r"
-by(simp add:Refl_def)
+lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
+by (simp add:preorder_on_def)
+
+lemma partial_order_on_converse[simp]:
+  "partial_order_on A (r^-1) = partial_order_on A r"
+by (simp add: partial_order_on_def)
 
-lemma Preorder_converse[simp]: "Preorder (r^-1) = Preorder r"
-by (simp add:Preorder_def)
+lemma linear_order_on_converse[simp]:
+  "linear_order_on A (r^-1) = linear_order_on A r"
+by (simp add: linear_order_on_def)
+
 
-lemma Partial_order_converse[simp]: "Partial_order (r^-1) = Partial_order r"
-by (simp add: Partial_order_def)
+lemma strict_linear_order_on_diff_Id:
+  "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
+by(simp add: order_on_defs trans_diff_Id)
+
+
+subsection{* Orders on the field *}
 
-lemma Total_converse[simp]: "Total (r^-1) = Total r"
-by (auto simp: Total_def)
+abbreviation "Refl r \<equiv> refl_on (Field r) r"
+
+abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
+
+abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
 
-lemma Linear_order_converse[simp]: "Linear_order (r^-1) = Linear_order r"
-by (simp add: Linear_order_def)
+abbreviation "Total r \<equiv> total_on (Field r) r"
+
+abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
+
+abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
+
 
 lemma subset_Image_Image_iff:
   "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
    r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
-apply(auto simp add:subset_def Preorder_def Refl_def Image_def)
+apply(auto simp add:subset_def preorder_on_def refl_on_def Image_def)
 apply metis
 by(metis trans_def)
 
@@ -66,11 +117,19 @@
 
 lemma Refl_antisym_eq_Image1_Image1_iff:
   "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
-by(simp add:Preorder_def expand_set_eq Partial_order_def antisym_def Refl_def)
-  metis
+by(simp add: expand_set_eq antisym_def refl_on_def) metis
 
 lemma Partial_order_eq_Image1_Image1_iff:
   "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
-by(auto simp:Preorder_def Partial_order_def Refl_antisym_eq_Image1_Image1_iff)
+by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
+
+
+subsection{* Orders on a type *}
+
+abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
+
+abbreviation "linear_order \<equiv> linear_order_on UNIV"
+
+abbreviation "well_order r \<equiv> well_order_on UNIV"
 
 end
diff -r c5fe289de634 -r afc43168ed85 src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Mon Mar 17 07:15:40 2008 +0100
+++ b/src/HOL/Library/Zorn.thy	Mon Mar 17 11:42:46 2008 +0100
@@ -279,7 +279,7 @@
 assumes po: "Partial_order r" and u: "\<forall>C\<in>Chain r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a,u):r"
 shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m,a):r \<longrightarrow> a=m"
 proof-
-  have "Preorder r" using po by(simp add:Partial_order_def)
+  have "Preorder r" using po by(simp add:partial_order_on_def)
 --{* Mirror r in the set of subsets below (wrt r) elements of A*}
   let ?B = "%x. r^-1 `` {x}" let ?S = "?B ` Field r"
   have "\<forall>C \<in> chain ?S. EX U:?S. ALL A:C. A\<subseteq>U"
@@ -301,7 +301,7 @@
       fix a B assume aB: "B:C" "a:B"
       with 1 obtain x where "x:Field r" "B = r^-1 `` {x}" by auto
       thus "(a,u) : r" using uA aB `Preorder r`
-	by (auto simp add: Preorder_def Refl_def) (metis transD)
+	by (auto simp add: preorder_on_def refl_on_def) (metis transD)
     qed
     thus "EX u:Field r. ?P u" using `u:Field r` by blast
   qed
@@ -358,18 +358,18 @@
 lemma chain_subset_Total_Union:
 assumes "chain\<^bsub>\<subseteq>\<^esub> R" "\<forall>r\<in>R. Total r"
 shows "Total (\<Union>R)"
-proof (simp add: Total_def Ball_def, auto del:disjCI)
+proof (simp add: total_on_def Ball_def, auto del:disjCI)
   fix r s a b assume A: "r:R" "s:R" "a:Field r" "b:Field s" "a\<noteq>b"
   from `chain\<^bsub>\<subseteq>\<^esub> R` `r:R` `s:R` have "r\<subseteq>s \<or> s\<subseteq>r"
     by(simp add:chain_subset_def)
   thus "(\<exists>r\<in>R. (a,b) \<in> r) \<or> (\<exists>r\<in>R. (b,a) \<in> r)"
   proof
     assume "r\<subseteq>s" hence "(a,b):s \<or> (b,a):s" using assms(2) A
-      by(simp add:Total_def)(metis mono_Field subsetD)
+      by(simp add:total_on_def)(metis mono_Field subsetD)
     thus ?thesis using `s:R` by blast
   next
     assume "s\<subseteq>r" hence "(a,b):r \<or> (b,a):r" using assms(2) A
-      by(simp add:Total_def)(metis mono_Field subsetD)
+      by(simp add:total_on_def)(metis mono_Field subsetD)
     thus ?thesis using `r:R` by blast
   qed
 qed
@@ -414,7 +414,7 @@
     by(simp add:Chain_def I_def) blast
   have FI: "Field I = ?WO" by(auto simp add:I_def init_seg_of_def Field_def)
   hence 0: "Partial_order I"
-    by(auto simp add: Partial_order_def Preorder_def antisym_def antisym_init_seg_of Refl_def trans_def I_def)(metis trans_init_seg_of)
+    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)
 -- {*I-chains have upper bounds in ?WO wrt I: their Union*}
   { fix R assume "R \<in> Chain I"
     hence Ris: "R \<in> Chain init_seg_of" using mono_Chain[OF I_init] by blast
@@ -422,8 +422,8 @@
       by(auto simp:init_seg_of_def chain_subset_def Chain_def)
     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"
          "\<forall>r\<in>R. wf(r-Id)"
-      using Chain_wo[OF `R \<in> Chain I`] by(simp_all add:Order_defs)
-    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:Refl_def)
+      using Chain_wo[OF `R \<in> Chain I`] by(simp_all add:order_on_defs)
+    have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:refl_on_def)
     moreover have "trans (\<Union>R)"
       by(rule chain_subset_trans_Union[OF subch `\<forall>r\<in>R. trans r`])
     moreover have "antisym(\<Union>R)"
@@ -436,7 +436,7 @@
       with `\<forall>r\<in>R. wf(r-Id)` wf_Union_wf_init_segs[OF Chain_inits_DiffI[OF Ris]]
       show ?thesis by (simp (no_asm_simp)) blast
     qed
-    ultimately have "Well_order (\<Union>R)" by(simp add:Order_defs)
+    ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs)
     moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris
       by(simp add: Chain_init_seg_of_Union)
     ultimately have "\<Union>R : ?WO \<and> (\<forall>r\<in>R. (r,\<Union>R) : I)"
@@ -455,26 +455,27 @@
     proof
       assume "m={}"
       moreover have "Well_order {(x,x)}"
-	by(simp add:Order_defs Refl_def trans_def antisym_def Total_def Field_def Domain_def Range_def)
+	by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def)
       ultimately show False using max
 	by (auto simp:I_def init_seg_of_def simp del:Field_insert)
     qed
     hence "Field m \<noteq> {}" by(auto simp:Field_def)
-    moreover have "wf(m-Id)" using `Well_order m` by(simp add:Well_order_def)
+    moreover have "wf(m-Id)" using `Well_order m`
+      by(simp add:well_order_on_def)
 --{*The extension of m by x:*}
     let ?s = "{(a,x)|a. a : Field m}" let ?m = "insert (x,x) m Un ?s"
     have Fm: "Field ?m = insert x (Field m)"
       apply(simp add:Field_insert Field_Un)
       unfolding Field_def by auto
     have "Refl m" "trans m" "antisym m" "Total m" "wf(m-Id)"
-      using `Well_order m` by(simp_all add:Order_defs)
+      using `Well_order m` by(simp_all add:order_on_defs)
 --{*We show that the extension is a well-order*}
-    have "Refl ?m" using `Refl m` Fm by(auto simp:Refl_def)
+    have "Refl ?m" using `Refl m` Fm by(auto simp:refl_on_def)
     moreover have "trans ?m" using `trans m` `x \<notin> Field m`
       unfolding trans_def Field_def Domain_def Range_def by blast
     moreover have "antisym ?m" using `antisym m` `x \<notin> Field m`
       unfolding antisym_def Field_def Domain_def Range_def by blast
-    moreover have "Total ?m" using `Total m` Fm by(auto simp: Total_def)
+    moreover have "Total ?m" using `Total m` Fm by(auto simp: total_on_def)
     moreover have "wf(?m-Id)"
     proof-
       have "wf ?s" using `x \<notin> Field m`
@@ -483,7 +484,7 @@
 	wf_subset[OF `wf ?s` Diff_subset]
 	by (fastsimp intro!: wf_Un simp add: Un_Diff Field_def)
     qed
-    ultimately have "Well_order ?m" by(simp add:Order_defs)
+    ultimately have "Well_order ?m" by(simp add:order_on_defs)
 --{*We show that the extension is above m*}
     moreover hence "(m,?m) : I" using `Well_order m` `x \<notin> Field m`
       by(fastsimp simp:I_def init_seg_of_def Field_def Domain_def Range_def)
@@ -496,24 +497,24 @@
   ultimately show ?thesis by blast
 qed
 
-corollary well_ordering_set: "\<exists>r::('a*'a)set. Well_order r \<and> Field r = A"
+corollary well_order_on: "\<exists>r::('a*'a)set. well_order_on A r"
 proof -
   obtain r::"('a*'a)set" where wo: "Well_order r" and univ: "Field r = UNIV"
     using well_ordering[where 'a = "'a"] by blast
   let ?r = "{(x,y). x:A & y:A & (x,y):r}"
   have 1: "Field ?r = A" using wo univ
-    by(fastsimp simp: Field_def Domain_def Range_def Order_defs Refl_def)
+    by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_on_def)
   have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)"
-    using `Well_order r` by(simp_all add:Order_defs)
-  have "Refl ?r" using `Refl r` by(auto simp:Refl_def 1 univ)
+    using `Well_order r` by(simp_all add:order_on_defs)
+  have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ)
   moreover have "trans ?r" using `trans r`
     unfolding trans_def by blast
   moreover have "antisym ?r" using `antisym r`
     unfolding antisym_def by blast
-  moreover have "Total ?r" using `Total r` by(simp add:Total_def 1 univ)
+  moreover have "Total ?r" using `Total r` by(simp add:total_on_def 1 univ)
   moreover have "wf(?r - Id)" by(rule wf_subset[OF `wf(r-Id)`]) blast
-  ultimately have "Well_order ?r" by(simp add:Order_defs)
-  with 1 show ?thesis by blast
+  ultimately have "Well_order ?r" by(simp add:order_on_defs)
+  with 1 show ?thesis by metis
 qed
 
 end