src/HOL/Orderings.thy
changeset 15780 6744bba5561d
parent 15622 4723248c982b
child 15791 446ec11266be
     1.1 --- a/src/HOL/Orderings.thy	Wed Apr 20 16:03:17 2005 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Wed Apr 20 17:19:18 2005 +0200
     1.3 @@ -93,8 +93,8 @@
     1.4  
     1.5  text{* Connection to locale: *}
     1.6  
     1.7 -lemma partial_order_order:
     1.8 - "partial_order (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
     1.9 +interpretation order[rule del]:
    1.10 +  partial_order["op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool"]
    1.11  apply(rule partial_order.intro)
    1.12  apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
    1.13  done
    1.14 @@ -226,6 +226,16 @@
    1.15  axclass linorder < order
    1.16    linorder_linear: "x <= y | y <= x"
    1.17  
    1.18 +(* Could (should?) follow automatically from the interpretation of
    1.19 +   partial_order by class order. rule del is needed because two copies
    1.20 +   of refl with classes order and linorder confuse blast (and are pointless)*)
    1.21 +interpretation order[rule del]:
    1.22 +  partial_order["op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool"]
    1.23 +apply(rule partial_order.intro)
    1.24 +apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
    1.25 +done
    1.26 +
    1.27 +
    1.28  lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
    1.29    apply (simp add: order_less_le)
    1.30    apply (insert linorder_linear, blast)
    1.31 @@ -388,39 +398,30 @@
    1.32  
    1.33  text{* Instantiate locales: *}
    1.34  
    1.35 -lemma lower_semilattice_lin_min:
    1.36 -  "lower_semilattice(op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.37 -apply(rule lower_semilattice.intro)
    1.38 -apply(rule partial_order_order)
    1.39 +interpretation min_max [rule del]:
    1.40 +  lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
    1.41 +apply -
    1.42  apply(rule lower_semilattice_axioms.intro)
    1.43  apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.44  apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.45  apply(simp add:min_def linorder_not_le order_less_imp_le)
    1.46  done
    1.47  
    1.48 -lemma upper_semilattice_lin_max:
    1.49 -  "upper_semilattice(op \<le>) (max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
    1.50 -apply(rule upper_semilattice.intro)
    1.51 -apply(rule partial_order_order)
    1.52 +interpretation min_max [rule del]:
    1.53 +  upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
    1.54 +apply -
    1.55  apply(rule upper_semilattice_axioms.intro)
    1.56  apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.57  apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.58  apply(simp add: max_def linorder_not_le order_less_imp_le)
    1.59  done
    1.60  
    1.61 -lemma lattice_min_max: "lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
    1.62 -apply(rule lattice.intro)
    1.63 -apply(rule partial_order_order)
    1.64 -apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
    1.65 -apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
    1.66 -done
    1.67 +interpretation min_max [rule del]:
    1.68 +  lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
    1.69 +.
    1.70  
    1.71 -lemma distrib_lattice_min_max:
    1.72 - "distrib_lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
    1.73 -apply(rule distrib_lattice.intro)
    1.74 -apply(rule partial_order_order)
    1.75 -apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
    1.76 -apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
    1.77 +interpretation min_max [rule del]:
    1.78 +  distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
    1.79  apply(rule distrib_lattice_axioms.intro)
    1.80  apply(rule_tac x=x and y=y in linorder_le_cases)
    1.81  apply(rule_tac x=x and y=z in linorder_le_cases)
    1.82 @@ -445,12 +446,8 @@
    1.83    apply (blast intro: order_trans)
    1.84    done
    1.85  
    1.86 -lemma le_maxI1: "(x::'a::linorder) <= max x y"
    1.87 -by(rule upper_semilattice.sup_ge1[OF upper_semilattice_lin_max])
    1.88 -
    1.89 -lemma le_maxI2: "(y::'a::linorder) <= max x y"
    1.90 -    -- {* CANNOT use with @{text "[intro!]"} because blast will give PROOF FAILED. *}
    1.91 -by(rule upper_semilattice.sup_ge2[OF upper_semilattice_lin_max])
    1.92 +lemmas le_maxI1 = min_max.sup_ge1
    1.93 +lemmas le_maxI2 = min_max.sup_ge2
    1.94  
    1.95  lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"
    1.96    apply (simp add: max_def order_le_less)
    1.97 @@ -458,22 +455,18 @@
    1.98    apply (blast intro: order_less_trans)
    1.99    done
   1.100  
   1.101 -lemma max_le_iff_conj [simp]:
   1.102 -    "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"
   1.103 -by (rule upper_semilattice.above_sup_conv[OF upper_semilattice_lin_max])
   1.104 -
   1.105  lemma max_less_iff_conj [simp]:
   1.106      "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"
   1.107    apply (simp add: order_le_less max_def)
   1.108    apply (insert linorder_less_linear)
   1.109    apply (blast intro: order_less_trans)
   1.110    done
   1.111 -
   1.112 +(*
   1.113  lemma le_min_iff_conj [simp]:
   1.114      "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"
   1.115      -- {* @{text "[iff]"} screws up a @{text blast} in MiniML *}
   1.116  by (rule lower_semilattice.below_inf_conv[OF lower_semilattice_lin_min])
   1.117 -
   1.118 +*)
   1.119  lemma min_less_iff_conj [simp]:
   1.120      "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
   1.121    apply (simp add: order_le_less min_def)
   1.122 @@ -492,24 +485,24 @@
   1.123    apply (insert linorder_less_linear)
   1.124    apply (blast intro: order_less_trans)
   1.125    done
   1.126 -
   1.127 +(*
   1.128  lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
   1.129  by (rule upper_semilattice.sup_assoc[OF upper_semilattice_lin_max])
   1.130  
   1.131  lemma max_commute: "!!x::'a::linorder. max x y = max y x"
   1.132  by (rule upper_semilattice.sup_commute[OF upper_semilattice_lin_max])
   1.133 -
   1.134 -lemmas max_ac = max_assoc max_commute
   1.135 -                mk_left_commute[of max,OF max_assoc max_commute]
   1.136 -
   1.137 +*)
   1.138 +lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   1.139 +               mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
   1.140 +(*
   1.141  lemma min_assoc: "!!x::'a::linorder. min (min x y) z = min x (min y z)"
   1.142  by (rule lower_semilattice.inf_assoc[OF lower_semilattice_lin_min])
   1.143  
   1.144  lemma min_commute: "!!x::'a::linorder. min x y = min y x"
   1.145  by (rule lower_semilattice.inf_commute[OF lower_semilattice_lin_min])
   1.146 -
   1.147 -lemmas min_ac = min_assoc min_commute
   1.148 -                mk_left_commute[of min,OF min_assoc min_commute]
   1.149 +*)
   1.150 +lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   1.151 +               mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
   1.152  
   1.153  lemma split_min:
   1.154      "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"