src/HOL/Orderings.thy
changeset 51487 f4bfdee99304
parent 51329 4a3c453f99a1
child 51546 2e26df807dc7
     1.1 --- a/src/HOL/Orderings.thy	Sat Mar 23 07:30:53 2013 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Sat Mar 23 17:11:06 2013 +0100
     1.3 @@ -12,6 +12,79 @@
     1.4  ML_file "~~/src/Provers/order.ML"
     1.5  ML_file "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
     1.6  
     1.7 +subsection {* Abstract ordering *}
     1.8 +
     1.9 +locale ordering =
    1.10 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
    1.11 +   and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
    1.12 +  assumes strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    1.13 +  assumes refl: "a \<preceq> a" -- {* not @{text iff}: makes problems due to multiple (dual) interpretations *}
    1.14 +    and antisym: "a \<preceq> b \<Longrightarrow> b \<preceq> a \<Longrightarrow> a = b"
    1.15 +    and trans: "a \<preceq> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<preceq> c"
    1.16 +begin
    1.17 +
    1.18 +lemma strict_implies_order:
    1.19 +  "a \<prec> b \<Longrightarrow> a \<preceq> b"
    1.20 +  by (simp add: strict_iff_order)
    1.21 +
    1.22 +lemma strict_implies_not_eq:
    1.23 +  "a \<prec> b \<Longrightarrow> a \<noteq> b"
    1.24 +  by (simp add: strict_iff_order)
    1.25 +
    1.26 +lemma not_eq_order_implies_strict:
    1.27 +  "a \<noteq> b \<Longrightarrow> a \<preceq> b \<Longrightarrow> a \<prec> b"
    1.28 +  by (simp add: strict_iff_order)
    1.29 +
    1.30 +lemma order_iff_strict:
    1.31 +  "a \<preceq> b \<longleftrightarrow> a \<prec> b \<or> a = b"
    1.32 +  by (auto simp add: strict_iff_order refl)
    1.33 +
    1.34 +lemma irrefl: -- {* not @{text iff}: makes problems due to multiple (dual) interpretations *}
    1.35 +  "\<not> a \<prec> a"
    1.36 +  by (simp add: strict_iff_order)
    1.37 +
    1.38 +lemma asym:
    1.39 +  "a \<prec> b \<Longrightarrow> b \<prec> a \<Longrightarrow> False"
    1.40 +  by (auto simp add: strict_iff_order intro: antisym)
    1.41 +
    1.42 +lemma strict_trans1:
    1.43 +  "a \<preceq> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
    1.44 +  by (auto simp add: strict_iff_order intro: trans antisym)
    1.45 +
    1.46 +lemma strict_trans2:
    1.47 +  "a \<prec> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<prec> c"
    1.48 +  by (auto simp add: strict_iff_order intro: trans antisym)
    1.49 +
    1.50 +lemma strict_trans:
    1.51 +  "a \<prec> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
    1.52 +  by (auto intro: strict_trans1 strict_implies_order)
    1.53 +
    1.54 +end
    1.55 +
    1.56 +locale ordering_top = ordering +
    1.57 +  fixes top :: "'a"
    1.58 +  assumes extremum [simp]: "a \<preceq> top"
    1.59 +begin
    1.60 +
    1.61 +lemma extremum_uniqueI:
    1.62 +  "top \<preceq> a \<Longrightarrow> a = top"
    1.63 +  by (rule antisym) auto
    1.64 +
    1.65 +lemma extremum_unique:
    1.66 +  "top \<preceq> a \<longleftrightarrow> a = top"
    1.67 +  by (auto intro: antisym)
    1.68 +
    1.69 +lemma extremum_strict [simp]:
    1.70 +  "\<not> (top \<prec> a)"
    1.71 +  using extremum [of a] by (auto simp add: order_iff_strict intro: asym irrefl)
    1.72 +
    1.73 +lemma not_eq_extremum:
    1.74 +  "a \<noteq> top \<longleftrightarrow> a \<prec> top"
    1.75 +  by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum)
    1.76 +
    1.77 +end  
    1.78 +
    1.79 +
    1.80  subsection {* Syntactic orders *}
    1.81  
    1.82  class ord =
    1.83 @@ -119,10 +192,21 @@
    1.84    assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
    1.85  begin
    1.86  
    1.87 -text {* Reflexivity. *}
    1.88 +lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
    1.89 +  by (auto simp add: less_le_not_le intro: antisym)
    1.90 +
    1.91 +end
    1.92 +
    1.93 +sublocale order < order!: ordering less_eq less
    1.94 +  by default (auto intro: antisym order_trans simp add: less_le)
    1.95  
    1.96 -lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
    1.97 -by (auto simp add: less_le_not_le intro: antisym)
    1.98 +sublocale order < dual_order!: ordering greater_eq greater
    1.99 +  by default (auto intro: antisym order_trans simp add: less_le)
   1.100 +
   1.101 +context order
   1.102 +begin
   1.103 +
   1.104 +text {* Reflexivity. *}
   1.105  
   1.106  lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
   1.107      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
   1.108 @@ -1089,46 +1173,59 @@
   1.109  
   1.110  class bot = order +
   1.111    fixes bot :: 'a ("\<bottom>")
   1.112 -  assumes bot_least [simp]: "\<bottom> \<le> a"
   1.113 +  assumes bot_least: "\<bottom> \<le> a"
   1.114 +
   1.115 +sublocale bot < bot!: ordering_top greater_eq greater bot
   1.116 +proof
   1.117 +qed (fact bot_least)
   1.118 +
   1.119 +context bot
   1.120  begin
   1.121  
   1.122  lemma le_bot:
   1.123    "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
   1.124 -  by (auto intro: antisym)
   1.125 +  by (fact bot.extremum_uniqueI)
   1.126  
   1.127  lemma bot_unique:
   1.128    "a \<le> \<bottom> \<longleftrightarrow> a = \<bottom>"
   1.129 -  by (auto intro: antisym)
   1.130 +  by (fact bot.extremum_unique)
   1.131  
   1.132 -lemma not_less_bot [simp]:
   1.133 -  "\<not> (a < \<bottom>)"
   1.134 -  using bot_least [of a] by (auto simp: le_less)
   1.135 +lemma not_less_bot:
   1.136 +  "\<not> a < \<bottom>"
   1.137 +  by (fact bot.extremum_strict)
   1.138  
   1.139  lemma bot_less:
   1.140    "a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a"
   1.141 -  by (auto simp add: less_le_not_le intro!: antisym)
   1.142 +  by (fact bot.not_eq_extremum)
   1.143  
   1.144  end
   1.145  
   1.146  class top = order +
   1.147    fixes top :: 'a ("\<top>")
   1.148 -  assumes top_greatest [simp]: "a \<le> \<top>"
   1.149 +  assumes top_greatest: "a \<le> \<top>"
   1.150 +
   1.151 +sublocale top < top!: ordering_top less_eq less top
   1.152 +proof
   1.153 +qed (fact top_greatest)
   1.154 +
   1.155 +context top
   1.156  begin
   1.157  
   1.158  lemma top_le:
   1.159    "\<top> \<le> a \<Longrightarrow> a = \<top>"
   1.160 -  by (rule antisym) auto
   1.161 +  by (fact top.extremum_uniqueI)
   1.162  
   1.163  lemma top_unique:
   1.164    "\<top> \<le> a \<longleftrightarrow> a = \<top>"
   1.165 -  by (auto intro: antisym)
   1.166 +  by (fact top.extremum_unique)
   1.167  
   1.168 -lemma not_top_less [simp]: "\<not> (\<top> < a)"
   1.169 -  using top_greatest [of a] by (auto simp: le_less)
   1.170 +lemma not_top_less:
   1.171 +  "\<not> \<top> < a"
   1.172 +  by (fact top.extremum_strict)
   1.173  
   1.174  lemma less_top:
   1.175    "a \<noteq> \<top> \<longleftrightarrow> a < \<top>"
   1.176 -  by (auto simp add: less_le_not_le intro!: antisym)
   1.177 +  by (fact top.not_eq_extremum)
   1.178  
   1.179  end
   1.180  
   1.181 @@ -1489,3 +1586,4 @@
   1.182  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
   1.183  
   1.184  end
   1.185 +