src/HOL/Order_Relation.thy
 author huffman Mon Jan 12 12:09:54 2009 -0800 (2009-01-12) changeset 29460 ad87e5d1488b parent 28952 15a4b2cf8c34 permissions -rw-r--r--
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
```     1 (*  ID          : \$Id\$
```
```     2     Author      : Tobias Nipkow
```
```     3 *)
```
```     4
```
```     5 header {* Orders as Relations *}
```
```     6
```
```     7 theory Order_Relation
```
```     8 imports Plain "~~/src/HOL/Hilbert_Choice" "~~/src/HOL/ATP_Linkup"
```
```     9 begin
```
```    10
```
```    11 text{* This prelude could be moved to theory Relation: *}
```
```    12
```
```    13 definition "irrefl r \<equiv> \<forall>x. (x,x) \<notin> r"
```
```    14
```
```    15 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"
```
```    16
```
```    17 abbreviation "total \<equiv> total_on UNIV"
```
```    18
```
```    19
```
```    20 lemma total_on_empty[simp]: "total_on {} r"
```
```    21 by(simp add:total_on_def)
```
```    22
```
```    23 lemma refl_on_converse[simp]: "refl A (r^-1) = refl A r"
```
```    24 by(auto simp add:refl_def)
```
```    25
```
```    26 lemma total_on_converse[simp]: "total_on A (r^-1) = total_on A r"
```
```    27 by (auto simp: total_on_def)
```
```    28
```
```    29 lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
```
```    30 by(simp add:irrefl_def)
```
```    31
```
```    32 declare [[simp_depth_limit = 2]]
```
```    33 lemma trans_diff_Id: " trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r-Id)"
```
```    34 by(simp add: antisym_def trans_def) blast
```
```    35 declare [[simp_depth_limit = 50]]
```
```    36
```
```    37 lemma total_on_diff_Id[simp]: "total_on A (r-Id) = total_on A r"
```
```    38 by(simp add: total_on_def)
```
```    39
```
```    40
```
```    41 subsection{* Orders on a set *}
```
```    42
```
```    43 definition "preorder_on A r \<equiv> refl A r \<and> trans r"
```
```    44
```
```    45 definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
```
```    46
```
```    47 definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"
```
```    48
```
```    49 definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"
```
```    50
```
```    51 definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)"
```
```    52
```
```    53 lemmas order_on_defs =
```
```    54   preorder_on_def partial_order_on_def linear_order_on_def
```
```    55   strict_linear_order_on_def well_order_on_def
```
```    56
```
```    57
```
```    58 lemma preorder_on_empty[simp]: "preorder_on {} {}"
```
```    59 by(simp add:preorder_on_def trans_def)
```
```    60
```
```    61 lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
```
```    62 by(simp add:partial_order_on_def)
```
```    63
```
```    64 lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
```
```    65 by(simp add:linear_order_on_def)
```
```    66
```
```    67 lemma well_order_on_empty[simp]: "well_order_on {} {}"
```
```    68 by(simp add:well_order_on_def)
```
```    69
```
```    70
```
```    71 lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
```
```    72 by (simp add:preorder_on_def)
```
```    73
```
```    74 lemma partial_order_on_converse[simp]:
```
```    75   "partial_order_on A (r^-1) = partial_order_on A r"
```
```    76 by (simp add: partial_order_on_def)
```
```    77
```
```    78 lemma linear_order_on_converse[simp]:
```
```    79   "linear_order_on A (r^-1) = linear_order_on A r"
```
```    80 by (simp add: linear_order_on_def)
```
```    81
```
```    82
```
```    83 lemma strict_linear_order_on_diff_Id:
```
```    84   "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
```
```    85 by(simp add: order_on_defs trans_diff_Id)
```
```    86
```
```    87
```
```    88 subsection{* Orders on the field *}
```
```    89
```
```    90 abbreviation "Refl r \<equiv> refl (Field r) r"
```
```    91
```
```    92 abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
```
```    93
```
```    94 abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
```
```    95
```
```    96 abbreviation "Total r \<equiv> total_on (Field r) r"
```
```    97
```
```    98 abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
```
```    99
```
```   100 abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
```
```   101
```
```   102
```
```   103 lemma subset_Image_Image_iff:
```
```   104   "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
```
```   105    r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
```
```   106 apply(auto simp add: subset_eq preorder_on_def refl_def Image_def)
```
```   107 apply metis
```
```   108 by(metis trans_def)
```
```   109
```
```   110 lemma subset_Image1_Image1_iff:
```
```   111   "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
```
```   112 by(simp add:subset_Image_Image_iff)
```
```   113
```
```   114 lemma Refl_antisym_eq_Image1_Image1_iff:
```
```   115   "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
```
```   116 by(simp add: expand_set_eq antisym_def refl_def) metis
```
```   117
```
```   118 lemma Partial_order_eq_Image1_Image1_iff:
```
```   119   "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
```
```   120 by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
```
```   121
```
```   122
```
```   123 subsection{* Orders on a type *}
```
```   124
```
```   125 abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
```
```   126
```
```   127 abbreviation "linear_order \<equiv> linear_order_on UNIV"
```
```   128
```
```   129 abbreviation "well_order r \<equiv> well_order_on UNIV"
```
```   130
```
```   131 end
```