moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
authorblanchet
Thu Nov 21 21:33:34 2013 +0100 (2013-11-21)
changeset 545525d57cbec0f0f
parent 54551 4cd6deb430c3
child 54553 2b0da4c1dd40
moving 'Order_Relation' to 'HOL' (since it's a BNF dependency)
src/HOL/Cardinals/Order_Relation_More.thy
src/HOL/Cardinals/Order_Relation_More_FP.thy
src/HOL/Library/Order_Relation.thy
src/HOL/Library/Zorn.thy
src/HOL/Main.thy
src/HOL/Order_Relation.thy
     1.1 --- a/src/HOL/Cardinals/Order_Relation_More.thy	Thu Nov 21 21:33:34 2013 +0100
     1.2 +++ b/src/HOL/Cardinals/Order_Relation_More.thy	Thu Nov 21 21:33:34 2013 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Basics on Order-Like Relations *}
     1.5  
     1.6  theory Order_Relation_More
     1.7 -imports Order_Relation_More_FP
     1.8 +imports Order_Relation_More_FP Main
     1.9  begin
    1.10  
    1.11  
     2.1 --- a/src/HOL/Cardinals/Order_Relation_More_FP.thy	Thu Nov 21 21:33:34 2013 +0100
     2.2 +++ b/src/HOL/Cardinals/Order_Relation_More_FP.thy	Thu Nov 21 21:33:34 2013 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Basics on Order-Like Relations (FP) *}
     2.5  
     2.6  theory Order_Relation_More_FP
     2.7 -imports "~~/src/HOL/Library/Order_Relation"
     2.8 +imports Order_Relation
     2.9  begin
    2.10  
    2.11  
     3.1 --- a/src/HOL/Library/Order_Relation.thy	Thu Nov 21 21:33:34 2013 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,116 +0,0 @@
     3.4 -(* Author: Tobias Nipkow *)
     3.5 -
     3.6 -header {* Orders as Relations *}
     3.7 -
     3.8 -theory Order_Relation
     3.9 -imports Main
    3.10 -begin
    3.11 -
    3.12 -subsection{* Orders on a set *}
    3.13 -
    3.14 -definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
    3.15 -
    3.16 -definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
    3.17 -
    3.18 -definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"
    3.19 -
    3.20 -definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"
    3.21 -
    3.22 -definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)"
    3.23 -
    3.24 -lemmas order_on_defs =
    3.25 -  preorder_on_def partial_order_on_def linear_order_on_def
    3.26 -  strict_linear_order_on_def well_order_on_def
    3.27 -
    3.28 -
    3.29 -lemma preorder_on_empty[simp]: "preorder_on {} {}"
    3.30 -by(simp add:preorder_on_def trans_def)
    3.31 -
    3.32 -lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
    3.33 -by(simp add:partial_order_on_def)
    3.34 -
    3.35 -lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
    3.36 -by(simp add:linear_order_on_def)
    3.37 -
    3.38 -lemma well_order_on_empty[simp]: "well_order_on {} {}"
    3.39 -by(simp add:well_order_on_def)
    3.40 -
    3.41 -
    3.42 -lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
    3.43 -by (simp add:preorder_on_def)
    3.44 -
    3.45 -lemma partial_order_on_converse[simp]:
    3.46 -  "partial_order_on A (r^-1) = partial_order_on A r"
    3.47 -by (simp add: partial_order_on_def)
    3.48 -
    3.49 -lemma linear_order_on_converse[simp]:
    3.50 -  "linear_order_on A (r^-1) = linear_order_on A r"
    3.51 -by (simp add: linear_order_on_def)
    3.52 -
    3.53 -
    3.54 -lemma strict_linear_order_on_diff_Id:
    3.55 -  "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
    3.56 -by(simp add: order_on_defs trans_diff_Id)
    3.57 -
    3.58 -
    3.59 -subsection{* Orders on the field *}
    3.60 -
    3.61 -abbreviation "Refl r \<equiv> refl_on (Field r) r"
    3.62 -
    3.63 -abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
    3.64 -
    3.65 -abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
    3.66 -
    3.67 -abbreviation "Total r \<equiv> total_on (Field r) r"
    3.68 -
    3.69 -abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
    3.70 -
    3.71 -abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
    3.72 -
    3.73 -
    3.74 -lemma subset_Image_Image_iff:
    3.75 -  "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
    3.76 -   r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
    3.77 -unfolding preorder_on_def refl_on_def Image_def
    3.78 -apply (simp add: subset_eq)
    3.79 -unfolding trans_def by fast
    3.80 -
    3.81 -lemma subset_Image1_Image1_iff:
    3.82 -  "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
    3.83 -by(simp add:subset_Image_Image_iff)
    3.84 -
    3.85 -lemma Refl_antisym_eq_Image1_Image1_iff:
    3.86 -  "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
    3.87 -by(simp add: set_eq_iff antisym_def refl_on_def) metis
    3.88 -
    3.89 -lemma Partial_order_eq_Image1_Image1_iff:
    3.90 -  "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
    3.91 -by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
    3.92 -
    3.93 -lemma Total_Id_Field:
    3.94 -assumes TOT: "Total r" and NID: "\<not> (r <= Id)"
    3.95 -shows "Field r = Field(r - Id)"
    3.96 -using mono_Field[of "r - Id" r] Diff_subset[of r Id]
    3.97 -proof(auto)
    3.98 -  have "r \<noteq> {}" using NID by fast
    3.99 -  then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto
   3.100 -  hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def)
   3.101 -  (*  *)
   3.102 -  fix a assume *: "a \<in> Field r"
   3.103 -  obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"
   3.104 -  using * 1 by auto
   3.105 -  hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
   3.106 -  by (simp add: total_on_def)
   3.107 -  thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast
   3.108 -qed
   3.109 -
   3.110 -
   3.111 -subsection{* Orders on a type *}
   3.112 -
   3.113 -abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
   3.114 -
   3.115 -abbreviation "linear_order \<equiv> linear_order_on UNIV"
   3.116 -
   3.117 -abbreviation "well_order \<equiv> well_order_on UNIV"
   3.118 -
   3.119 -end
     4.1 --- a/src/HOL/Library/Zorn.thy	Thu Nov 21 21:33:34 2013 +0100
     4.2 +++ b/src/HOL/Library/Zorn.thy	Thu Nov 21 21:33:34 2013 +0100
     4.3 @@ -10,7 +10,7 @@
     4.4  header {* Zorn's Lemma *}
     4.5  
     4.6  theory Zorn
     4.7 -imports Order_Relation
     4.8 +imports Main
     4.9  begin
    4.10  
    4.11  subsection {* Zorn's Lemma for the Subset Relation *}
     5.1 --- a/src/HOL/Main.thy	Thu Nov 21 21:33:34 2013 +0100
     5.2 +++ b/src/HOL/Main.thy	Thu Nov 21 21:33:34 2013 +0100
     5.3 @@ -1,7 +1,7 @@
     5.4  header {* Main HOL *}
     5.5  
     5.6  theory Main
     5.7 -imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction
     5.8 +imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction Order_Relation
     5.9  begin
    5.10  
    5.11  text {*
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Order_Relation.thy	Thu Nov 21 21:33:34 2013 +0100
     6.3 @@ -0,0 +1,125 @@
     6.4 +(*  Title:      HOL/Order_Relation.thy
     6.5 +    Author:     Tobias Nipkow
     6.6 +*)
     6.7 +
     6.8 +header {* Orders as Relations *}
     6.9 +
    6.10 +theory Order_Relation
    6.11 +imports Wellfounded
    6.12 +begin
    6.13 +
    6.14 +subsection{* Orders on a set *}
    6.15 +
    6.16 +definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
    6.17 +
    6.18 +definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
    6.19 +
    6.20 +definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"
    6.21 +
    6.22 +definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"
    6.23 +
    6.24 +definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)"
    6.25 +
    6.26 +lemmas order_on_defs =
    6.27 +  preorder_on_def partial_order_on_def linear_order_on_def
    6.28 +  strict_linear_order_on_def well_order_on_def
    6.29 +
    6.30 +
    6.31 +lemma preorder_on_empty[simp]: "preorder_on {} {}"
    6.32 +by(simp add:preorder_on_def trans_def)
    6.33 +
    6.34 +lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
    6.35 +by(simp add:partial_order_on_def)
    6.36 +
    6.37 +lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
    6.38 +by(simp add:linear_order_on_def)
    6.39 +
    6.40 +lemma well_order_on_empty[simp]: "well_order_on {} {}"
    6.41 +by(simp add:well_order_on_def)
    6.42 +
    6.43 +
    6.44 +lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
    6.45 +by (simp add:preorder_on_def)
    6.46 +
    6.47 +lemma partial_order_on_converse[simp]:
    6.48 +  "partial_order_on A (r^-1) = partial_order_on A r"
    6.49 +by (simp add: partial_order_on_def)
    6.50 +
    6.51 +lemma linear_order_on_converse[simp]:
    6.52 +  "linear_order_on A (r^-1) = linear_order_on A r"
    6.53 +by (simp add: linear_order_on_def)
    6.54 +
    6.55 +
    6.56 +lemma strict_linear_order_on_diff_Id:
    6.57 +  "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
    6.58 +by(simp add: order_on_defs trans_diff_Id)
    6.59 +
    6.60 +
    6.61 +subsection{* Orders on the field *}
    6.62 +
    6.63 +abbreviation "Refl r \<equiv> refl_on (Field r) r"
    6.64 +
    6.65 +abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
    6.66 +
    6.67 +abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
    6.68 +
    6.69 +abbreviation "Total r \<equiv> total_on (Field r) r"
    6.70 +
    6.71 +abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
    6.72 +
    6.73 +abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
    6.74 +
    6.75 +
    6.76 +lemma subset_Image_Image_iff:
    6.77 +  "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
    6.78 +   r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
    6.79 +unfolding preorder_on_def refl_on_def Image_def
    6.80 +apply (simp add: subset_eq)
    6.81 +unfolding trans_def by fast
    6.82 +
    6.83 +lemma subset_Image1_Image1_iff:
    6.84 +  "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
    6.85 +by(simp add:subset_Image_Image_iff)
    6.86 +
    6.87 +lemma Refl_antisym_eq_Image1_Image1_iff:
    6.88 +  assumes r: "Refl r" and as: "antisym r" and abf: "a \<in> Field r" "b \<in> Field r"
    6.89 +  shows "r `` {a} = r `` {b} \<longleftrightarrow> a = b"
    6.90 +proof
    6.91 +  assume "r `` {a} = r `` {b}"
    6.92 +  hence e: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r" by (simp add: set_eq_iff)
    6.93 +  have "(a, a) \<in> r" "(b, b) \<in> r" using r abf by (simp_all add: refl_on_def)
    6.94 +  hence "(a, b) \<in> r" "(b, a) \<in> r" using e[of a] e[of b] by simp_all
    6.95 +  thus "a = b" using as[unfolded antisym_def] by blast
    6.96 +qed fast
    6.97 +
    6.98 +lemma Partial_order_eq_Image1_Image1_iff:
    6.99 +  "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
   6.100 +by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
   6.101 +
   6.102 +lemma Total_Id_Field:
   6.103 +assumes TOT: "Total r" and NID: "\<not> (r <= Id)"
   6.104 +shows "Field r = Field(r - Id)"
   6.105 +using mono_Field[of "r - Id" r] Diff_subset[of r Id]
   6.106 +proof(auto)
   6.107 +  have "r \<noteq> {}" using NID by fast
   6.108 +  then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto
   6.109 +  hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def)
   6.110 +
   6.111 +  fix a assume *: "a \<in> Field r"
   6.112 +  obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"
   6.113 +  using * 1 by auto
   6.114 +  hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
   6.115 +  by (simp add: total_on_def)
   6.116 +  thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast
   6.117 +qed
   6.118 +
   6.119 +
   6.120 +subsection{* Orders on a type *}
   6.121 +
   6.122 +abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
   6.123 +
   6.124 +abbreviation "linear_order \<equiv> linear_order_on UNIV"
   6.125 +
   6.126 +abbreviation "well_order \<equiv> well_order_on UNIV"
   6.127 +
   6.128 +end