src/HOL/Library/Order_Relation.thy
author nipkow
Fri Mar 14 19:58:01 2008 +0100 (2008-03-14)
changeset 26273 6c4d534af98d
child 26295 afc43168ed85
permissions -rw-r--r--
Orders as relations
nipkow@26273
     1
(*  ID          : $Id$
nipkow@26273
     2
    Author      : Tobias Nipkow
nipkow@26273
     3
nipkow@26273
     4
Orders as relations with implicit base set, their Field
nipkow@26273
     5
*)
nipkow@26273
     6
nipkow@26273
     7
header {* Orders as Relations *}
nipkow@26273
     8
nipkow@26273
     9
theory Order_Relation
nipkow@26273
    10
imports ATP_Linkup Hilbert_Choice
nipkow@26273
    11
begin
nipkow@26273
    12
nipkow@26273
    13
definition "Refl r \<equiv> \<forall>x \<in> Field r. (x,x) \<in> r"
nipkow@26273
    14
definition "Preorder r \<equiv> Refl r \<and> trans r"
nipkow@26273
    15
definition "Partial_order r \<equiv> Preorder r \<and> antisym r"
nipkow@26273
    16
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"
nipkow@26273
    17
definition "Linear_order r \<equiv> Partial_order r \<and> Total r"
nipkow@26273
    18
definition "Well_order r \<equiv> Linear_order r \<and> wf(r - Id)"
nipkow@26273
    19
nipkow@26273
    20
lemmas Order_defs =
nipkow@26273
    21
  Preorder_def Partial_order_def Linear_order_def Well_order_def
nipkow@26273
    22
nipkow@26273
    23
lemma Refl_empty[simp]: "Refl {}"
nipkow@26273
    24
by(simp add:Refl_def)
nipkow@26273
    25
nipkow@26273
    26
lemma Preorder_empty[simp]: "Preorder {}"
nipkow@26273
    27
by(simp add:Preorder_def trans_def)
nipkow@26273
    28
nipkow@26273
    29
lemma Partial_order_empty[simp]: "Partial_order {}"
nipkow@26273
    30
by(simp add:Partial_order_def)
nipkow@26273
    31
nipkow@26273
    32
lemma Total_empty[simp]: "Total {}"
nipkow@26273
    33
by(simp add:Total_def)
nipkow@26273
    34
nipkow@26273
    35
lemma Linear_order_empty[simp]: "Linear_order {}"
nipkow@26273
    36
by(simp add:Linear_order_def)
nipkow@26273
    37
nipkow@26273
    38
lemma Well_order_empty[simp]: "Well_order {}"
nipkow@26273
    39
by(simp add:Well_order_def)
nipkow@26273
    40
nipkow@26273
    41
lemma Refl_converse[simp]: "Refl(r^-1) = Refl r"
nipkow@26273
    42
by(simp add:Refl_def)
nipkow@26273
    43
nipkow@26273
    44
lemma Preorder_converse[simp]: "Preorder (r^-1) = Preorder r"
nipkow@26273
    45
by (simp add:Preorder_def)
nipkow@26273
    46
nipkow@26273
    47
lemma Partial_order_converse[simp]: "Partial_order (r^-1) = Partial_order r"
nipkow@26273
    48
by (simp add: Partial_order_def)
nipkow@26273
    49
nipkow@26273
    50
lemma Total_converse[simp]: "Total (r^-1) = Total r"
nipkow@26273
    51
by (auto simp: Total_def)
nipkow@26273
    52
nipkow@26273
    53
lemma Linear_order_converse[simp]: "Linear_order (r^-1) = Linear_order r"
nipkow@26273
    54
by (simp add: Linear_order_def)
nipkow@26273
    55
nipkow@26273
    56
lemma subset_Image_Image_iff:
nipkow@26273
    57
  "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
nipkow@26273
    58
   r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
nipkow@26273
    59
apply(auto simp add:subset_def Preorder_def Refl_def Image_def)
nipkow@26273
    60
apply metis
nipkow@26273
    61
by(metis trans_def)
nipkow@26273
    62
nipkow@26273
    63
lemma subset_Image1_Image1_iff:
nipkow@26273
    64
  "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
nipkow@26273
    65
by(simp add:subset_Image_Image_iff)
nipkow@26273
    66
nipkow@26273
    67
lemma Refl_antisym_eq_Image1_Image1_iff:
nipkow@26273
    68
  "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
nipkow@26273
    69
by(simp add:Preorder_def expand_set_eq Partial_order_def antisym_def Refl_def)
nipkow@26273
    70
  metis
nipkow@26273
    71
nipkow@26273
    72
lemma Partial_order_eq_Image1_Image1_iff:
nipkow@26273
    73
  "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
nipkow@26273
    74
by(auto simp:Preorder_def Partial_order_def Refl_antisym_eq_Image1_Image1_iff)
nipkow@26273
    75
nipkow@26273
    76
end