src/HOL/Orderings.thy
changeset 22206 8cc04341de38
parent 22068 00bed5ac9884
child 22295 5f8a2898668c
     1.1 --- a/src/HOL/Orderings.thy	Mon Jan 29 19:58:14 2007 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Tue Jan 30 08:21:13 2007 +0100
     1.3 @@ -293,7 +293,7 @@
     1.4  axclass linorder < order
     1.5    linorder_linear: "x <= y | y <= x"
     1.6  
     1.7 -interpretation linorder:
     1.8 +interpretation order:
     1.9    linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool"]
    1.10    by unfold_locales (rule linorder_linear)
    1.11  
    1.12 @@ -320,20 +320,20 @@
    1.13  lemmas order_neq_le_trans [where 'b = "?'a::order"] = order.neq_le_trans
    1.14  lemmas order_le_neq_trans [where 'b = "?'a::order"] = order.le_neq_trans
    1.15  lemmas order_less_asym' [where 'b = "?'a::order"] = order.less_asym'
    1.16 -lemmas linorder_less_linear [where 'b = "?'a::linorder"] = linorder.less_linear
    1.17 -lemmas linorder_le_less_linear [where 'b = "?'a::linorder"] = linorder.le_less_linear
    1.18 -lemmas linorder_le_cases [where 'b = "?'a::linorder"] = linorder.le_cases
    1.19 -lemmas linorder_cases [where 'b = "?'a::linorder"] = linorder.cases
    1.20 -lemmas linorder_not_less [where 'b = "?'a::linorder"] = linorder.not_less
    1.21 -lemmas linorder_not_le [where 'b = "?'a::linorder"] = linorder.not_le
    1.22 -lemmas linorder_neq_iff [where 'b = "?'a::linorder"] = linorder.neq_iff
    1.23 -lemmas linorder_neqE [where 'b = "?'a::linorder"] = linorder.neqE
    1.24 -lemmas linorder_antisym_conv1 [where 'b = "?'a::linorder"] = linorder.antisym_conv1
    1.25 -lemmas linorder_antisym_conv2 [where 'b = "?'a::linorder"] = linorder.antisym_conv2
    1.26 -lemmas linorder_antisym_conv3 [where 'b = "?'a::linorder"] = linorder.antisym_conv3
    1.27 -lemmas leI [where 'b = "?'a::linorder"] = linorder.leI
    1.28 -lemmas leD [where 'b = "?'a::linorder"] = linorder.leD
    1.29 -lemmas not_leE [where 'b = "?'a::linorder"] = linorder.not_leE
    1.30 +lemmas linorder_less_linear [where 'b = "?'a::linorder"] = order.less_linear
    1.31 +lemmas linorder_le_less_linear [where 'b = "?'a::linorder"] = order.le_less_linear
    1.32 +lemmas linorder_le_cases [where 'b = "?'a::linorder"] = order.le_cases
    1.33 +lemmas linorder_cases [where 'b = "?'a::linorder"] = order.cases
    1.34 +lemmas linorder_not_less [where 'b = "?'a::linorder"] = order.not_less
    1.35 +lemmas linorder_not_le [where 'b = "?'a::linorder"] = order.not_le
    1.36 +lemmas linorder_neq_iff [where 'b = "?'a::linorder"] = order.neq_iff
    1.37 +lemmas linorder_neqE [where 'b = "?'a::linorder"] = order.neqE
    1.38 +lemmas linorder_antisym_conv1 [where 'b = "?'a::linorder"] = order.antisym_conv1
    1.39 +lemmas linorder_antisym_conv2 [where 'b = "?'a::linorder"] = order.antisym_conv2
    1.40 +lemmas linorder_antisym_conv3 [where 'b = "?'a::linorder"] = order.antisym_conv3
    1.41 +lemmas leI [where 'b = "?'a::linorder"] = order.leI
    1.42 +lemmas leD [where 'b = "?'a::linorder"] = order.leD
    1.43 +lemmas not_leE [where 'b = "?'a::linorder"] = order.not_leE
    1.44  
    1.45  
    1.46  subsection {* Reasoning tools setup *}
    1.47 @@ -866,24 +866,24 @@
    1.48    max :: "['a::ord, 'a] => 'a"
    1.49    "max a b == (if a <= b then b else a)"
    1.50  
    1.51 -hide const linorder.less_eq_less.max linorder.less_eq_less.min  (* FIXME !? *)
    1.52 +hide const order.less_eq_less.max order.less_eq_less.min  (* FIXME !? *)
    1.53  
    1.54  lemma min_linorder:
    1.55    "linorder.min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = min"
    1.56 -  by (rule+) (simp add: min_def linorder.min_def)
    1.57 +  by (rule+) (simp add: min_def order.min_def)
    1.58  
    1.59  lemma max_linorder:
    1.60    "linorder.max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = max"
    1.61 -  by (rule+) (simp add: max_def linorder.max_def)
    1.62 +  by (rule+) (simp add: max_def order.max_def)
    1.63  
    1.64 -lemmas min_le_iff_disj = linorder.min_le_iff_disj [where 'b = "?'a::linorder", simplified min_linorder]
    1.65 -lemmas le_max_iff_disj = linorder.le_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder]
    1.66 -lemmas min_less_iff_disj = linorder.min_less_iff_disj [where 'b = "?'a::linorder", simplified min_linorder]
    1.67 -lemmas less_max_iff_disj = linorder.less_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder]
    1.68 -lemmas min_less_iff_conj [simp] = linorder.min_less_iff_conj [where 'b = "?'a::linorder", simplified min_linorder]
    1.69 -lemmas max_less_iff_conj [simp] = linorder.max_less_iff_conj [where 'b = "?'a::linorder", simplified max_linorder]
    1.70 -lemmas split_min = linorder.split_min [where 'b = "?'a::linorder", simplified min_linorder]
    1.71 -lemmas split_max = linorder.split_max [where 'b = "?'a::linorder", simplified max_linorder]
    1.72 +lemmas min_le_iff_disj = order.min_le_iff_disj [where 'b = "?'a::linorder", simplified min_linorder]
    1.73 +lemmas le_max_iff_disj = order.le_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder]
    1.74 +lemmas min_less_iff_disj = order.min_less_iff_disj [where 'b = "?'a::linorder", simplified min_linorder]
    1.75 +lemmas less_max_iff_disj = order.less_max_iff_disj [where 'b = "?'a::linorder", simplified max_linorder]
    1.76 +lemmas min_less_iff_conj [simp] = order.min_less_iff_conj [where 'b = "?'a::linorder", simplified min_linorder]
    1.77 +lemmas max_less_iff_conj [simp] = order.max_less_iff_conj [where 'b = "?'a::linorder", simplified max_linorder]
    1.78 +lemmas split_min = order.split_min [where 'b = "?'a::linorder", simplified min_linorder]
    1.79 +lemmas split_max = order.split_max [where 'b = "?'a::linorder", simplified max_linorder]
    1.80  
    1.81  lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
    1.82    by (simp add: min_def)