src/HOL/Orderings.thy
changeset 22316 f662831459de
parent 22295 5f8a2898668c
child 22344 eddeabf16b5d
     1.1 --- a/src/HOL/Orderings.thy	Tue Feb 13 18:26:48 2007 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Wed Feb 14 10:06:12 2007 +0100
     1.3 @@ -71,10 +71,10 @@
     1.4  
     1.5  subsection {* Quasiorders (preorders) *}
     1.6  
     1.7 -locale preorder = ord +
     1.8 -  assumes refl [iff]: "x \<sqsubseteq> x"
     1.9 +class preorder = ord +
    1.10 +  assumes less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
    1.11 +  and refl [iff]: "x \<sqsubseteq> x"
    1.12    and trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
    1.13 -  and less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
    1.14  begin
    1.15  
    1.16  text {* Reflexivity. *}
    1.17 @@ -122,7 +122,7 @@
    1.18  
    1.19  subsection {* Partial orderings *}
    1.20  
    1.21 -locale order = preorder + 
    1.22 +class order = preorder + 
    1.23    assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
    1.24  
    1.25  context order
    1.26 @@ -174,25 +174,10 @@
    1.27  
    1.28  end
    1.29  
    1.30 -axclass order < ord
    1.31 -  order_refl [iff]: "x <= x"
    1.32 -  order_trans: "x <= y ==> y <= z ==> x <= z"
    1.33 -  order_antisym: "x <= y ==> y <= x ==> x = y"
    1.34 -  order_less_le: "(x < y) = (x <= y & x ~= y)"
    1.35 -
    1.36 -interpretation order:
    1.37 -  order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"]
    1.38 -apply unfold_locales
    1.39 -apply (rule order_refl)
    1.40 -apply (erule (1) order_trans)
    1.41 -apply (rule order_less_le)
    1.42 -apply (erule (1) order_antisym)
    1.43 -done
    1.44 -
    1.45  
    1.46  subsection {* Linear (total) orders *}
    1.47  
    1.48 -locale linorder = order +
    1.49 +class linorder = order +
    1.50    assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
    1.51  begin
    1.52  
    1.53 @@ -290,50 +275,50 @@
    1.54  
    1.55  end
    1.56  
    1.57 -axclass linorder < order
    1.58 -  linorder_linear: "x <= y | y <= x"
    1.59 -
    1.60 -interpretation order:
    1.61 -  linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool"]
    1.62 -  by unfold_locales (rule linorder_linear)
    1.63 -
    1.64  
    1.65  subsection {* Name duplicates *}
    1.66  
    1.67 -lemmas order_eq_refl [where 'b = "?'a::order"] = order.eq_refl
    1.68 -lemmas order_less_irrefl [where 'b = "?'a::order"] = order.less_irrefl
    1.69 -lemmas order_le_less [where 'b = "?'a::order"] = order.le_less
    1.70 -lemmas order_le_imp_less_or_eq [where 'b = "?'a::order"] = order.le_imp_less_or_eq
    1.71 -lemmas order_less_imp_le [where 'b = "?'a::order"] = order.less_imp_le
    1.72 -lemmas order_less_not_sym [where 'b = "?'a::order"] = order.less_not_sym
    1.73 -lemmas order_less_asym [where 'b = "?'a::order"] = order.less_asym
    1.74 -lemmas order_eq_iff [where 'b = "?'a::order"] = order.eq_iff
    1.75 -lemmas order_antisym_conv [where 'b = "?'a::order"] = order.antisym_conv
    1.76 -lemmas less_imp_neq [where 'b = "?'a::order"] = order.less_imp_neq
    1.77 -lemmas order_less_trans [where 'b = "?'a::order"] = order.less_trans
    1.78 -lemmas order_le_less_trans [where 'b = "?'a::order"] = order.le_less_trans
    1.79 -lemmas order_less_le_trans [where 'b = "?'a::order"] = order.less_le_trans
    1.80 -lemmas order_less_imp_not_less [where 'b = "?'a::order"] = order.less_imp_not_less
    1.81 -lemmas order_less_imp_triv [where 'b = "?'a::order"] = order.less_imp_triv
    1.82 -lemmas order_less_imp_not_eq [where 'b = "?'a::order"] = order.less_imp_not_eq
    1.83 -lemmas order_less_imp_not_eq2 [where 'b = "?'a::order"] = order.less_imp_not_eq2
    1.84 -lemmas order_neq_le_trans [where 'b = "?'a::order"] = order.neq_le_trans
    1.85 -lemmas order_le_neq_trans [where 'b = "?'a::order"] = order.le_neq_trans
    1.86 -lemmas order_less_asym' [where 'b = "?'a::order"] = order.less_asym'
    1.87 -lemmas linorder_less_linear [where 'b = "?'a::linorder"] = order.less_linear
    1.88 -lemmas linorder_le_less_linear [where 'b = "?'a::linorder"] = order.le_less_linear
    1.89 -lemmas linorder_le_cases [where 'b = "?'a::linorder"] = order.le_cases
    1.90 -lemmas linorder_cases [where 'b = "?'a::linorder"] = order.cases
    1.91 -lemmas linorder_not_less [where 'b = "?'a::linorder"] = order.not_less
    1.92 -lemmas linorder_not_le [where 'b = "?'a::linorder"] = order.not_le
    1.93 -lemmas linorder_neq_iff [where 'b = "?'a::linorder"] = order.neq_iff
    1.94 -lemmas linorder_neqE [where 'b = "?'a::linorder"] = order.neqE
    1.95 -lemmas linorder_antisym_conv1 [where 'b = "?'a::linorder"] = order.antisym_conv1
    1.96 -lemmas linorder_antisym_conv2 [where 'b = "?'a::linorder"] = order.antisym_conv2
    1.97 -lemmas linorder_antisym_conv3 [where 'b = "?'a::linorder"] = order.antisym_conv3
    1.98 -lemmas leI [where 'b = "?'a::linorder"] = order.leI
    1.99 -lemmas leD [where 'b = "?'a::linorder"] = order.leD
   1.100 -lemmas not_leE [where 'b = "?'a::linorder"] = order.not_leE
   1.101 +lemmas order_refl [iff] = preorder_class.refl
   1.102 +lemmas order_trans = preorder_class.trans
   1.103 +lemmas order_less_le = preorder_class.less_le
   1.104 +lemmas order_eq_refl = preorder_class.eq_refl
   1.105 +lemmas order_less_irrefl = preorder_class.less_irrefl
   1.106 +lemmas order_le_less = preorder_class.le_less
   1.107 +lemmas order_le_imp_less_or_eq = preorder_class.le_imp_less_or_eq
   1.108 +lemmas order_less_imp_le = preorder_class.less_imp_le
   1.109 +lemmas order_less_imp_not_eq = preorder_class.less_imp_not_eq
   1.110 +lemmas order_less_imp_not_eq2 = preorder_class.less_imp_not_eq2
   1.111 +lemmas order_neq_le_trans = preorder_class.neq_le_trans
   1.112 +lemmas order_le_neq_trans = preorder_class.le_neq_trans
   1.113 +
   1.114 +lemmas order_antisym = order_class.antisym
   1.115 +lemmas order_less_not_sym = order_class.less_not_sym
   1.116 +lemmas order_less_asym = order_class.less_asym
   1.117 +lemmas order_eq_iff = order_class.eq_iff
   1.118 +lemmas order_antisym_conv = order_class.antisym_conv
   1.119 +lemmas less_imp_neq = order_class.less_imp_neq
   1.120 +lemmas order_less_trans = order_class.less_trans
   1.121 +lemmas order_le_less_trans = order_class.le_less_trans
   1.122 +lemmas order_less_le_trans = order_class.less_le_trans
   1.123 +lemmas order_less_imp_not_less = order_class.less_imp_not_less
   1.124 +lemmas order_less_imp_triv = order_class.less_imp_triv
   1.125 +lemmas order_less_asym' = order_class.less_asym'
   1.126 +
   1.127 +lemmas linorder_linear = linorder_class.linear
   1.128 +lemmas linorder_less_linear = linorder_class.less_linear
   1.129 +lemmas linorder_le_less_linear = linorder_class.le_less_linear
   1.130 +lemmas linorder_le_cases = linorder_class.le_cases
   1.131 +lemmas linorder_cases = linorder_class.cases
   1.132 +lemmas linorder_not_less = linorder_class.not_less
   1.133 +lemmas linorder_not_le = linorder_class.not_le
   1.134 +lemmas linorder_neq_iff = linorder_class.neq_iff
   1.135 +lemmas linorder_neqE = linorder_class.neqE
   1.136 +lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
   1.137 +lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
   1.138 +lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
   1.139 +lemmas leI = linorder_class.leI
   1.140 +lemmas leD = linorder_class.leD
   1.141 +lemmas not_leE = linorder_class.not_leE
   1.142  
   1.143  
   1.144  subsection {* Reasoning tools setup *}
   1.145 @@ -866,24 +851,22 @@
   1.146    max :: "['a::ord, 'a] => 'a"
   1.147    "max a b == (if a <= b then b else a)"
   1.148  
   1.149 -hide const order.less_eq_less.max order.less_eq_less.min  (* FIXME !? *)
   1.150 -
   1.151  lemma min_linorder:
   1.152    "linorder.min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = min"
   1.153 -  by (rule+) (simp add: min_def order.min_def)
   1.154 +  by rule+ (simp add: min_def linorder_class.min_def)
   1.155  
   1.156  lemma max_linorder:
   1.157    "linorder.max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = max"
   1.158 -  by (rule+) (simp add: max_def order.max_def)
   1.159 +  by rule+ (simp add: max_def linorder_class.max_def)
   1.160  
   1.161 -lemmas min_le_iff_disj = order.min_le_iff_disj [where 'b = "?'a::linorder", unfolded min_linorder]
   1.162 -lemmas le_max_iff_disj = order.le_max_iff_disj [where 'b = "?'a::linorder", unfolded max_linorder]
   1.163 -lemmas min_less_iff_disj = order.min_less_iff_disj [where 'b = "?'a::linorder", unfolded min_linorder]
   1.164 -lemmas less_max_iff_disj = order.less_max_iff_disj [where 'b = "?'a::linorder", unfolded max_linorder]
   1.165 -lemmas min_less_iff_conj [simp] = order.min_less_iff_conj [where 'b = "?'a::linorder", unfolded min_linorder]
   1.166 -lemmas max_less_iff_conj [simp] = order.max_less_iff_conj [where 'b = "?'a::linorder", unfolded max_linorder]
   1.167 -lemmas split_min = order.split_min [where 'b = "?'a::linorder", unfolded min_linorder]
   1.168 -lemmas split_max = order.split_max [where 'b = "?'a::linorder", unfolded max_linorder]
   1.169 +lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded min_linorder]
   1.170 +lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded max_linorder]
   1.171 +lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded min_linorder]
   1.172 +lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [unfolded max_linorder]
   1.173 +lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [unfolded min_linorder]
   1.174 +lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [unfolded max_linorder]
   1.175 +lemmas split_min = linorder_class.split_min [unfolded min_linorder]
   1.176 +lemmas split_max = linorder_class.split_max [unfolded max_linorder]
   1.177  
   1.178  lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
   1.179    by (simp add: min_def)