src/HOL/Orderings.thy
changeset 27689 268a7d02cf7a
parent 27682 25aceefd4786
child 27823 52971512d1a2
     1.1 --- a/src/HOL/Orderings.thy	Mon Jul 28 20:49:07 2008 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Tue Jul 29 08:15:38 2008 +0200
     1.3 @@ -403,117 +403,80 @@
     1.4  (* The type constraint on @{term op =} below is necessary since the operation
     1.5     is not a parameter of the locale. *)
     1.6  
     1.7 -lemmas
     1.8 -  [order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"] =
     1.9 -  less_irrefl [THEN notE]
    1.10 -lemmas
    1.11 -  [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.12 -  order_refl
    1.13 -lemmas
    1.14 -  [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.15 -  less_imp_le
    1.16 -lemmas
    1.17 -  [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.18 -  antisym
    1.19 -lemmas
    1.20 -  [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.21 -  eq_refl
    1.22 -lemmas
    1.23 -  [order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.24 -  sym [THEN eq_refl]
    1.25 -lemmas
    1.26 -  [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.27 -  less_trans
    1.28 -lemmas
    1.29 -  [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.30 -  less_le_trans
    1.31 -lemmas
    1.32 -  [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.33 -  le_less_trans
    1.34 -lemmas
    1.35 -  [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.36 -  order_trans
    1.37 -lemmas
    1.38 -  [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.39 -  le_neq_trans
    1.40 -lemmas
    1.41 -  [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.42 -  neq_le_trans
    1.43 -lemmas
    1.44 -  [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.45 -  less_imp_neq
    1.46 -lemmas
    1.47 -  [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.48 -   eq_neq_eq_imp_neq
    1.49 -lemmas
    1.50 -  [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    1.51 -  not_sym
    1.52 +declare less_irrefl [THEN notE, order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"]
    1.53 +  
    1.54 +declare order_refl  [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.55 +  
    1.56 +declare less_imp_le [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.57 +  
    1.58 +declare antisym [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.59 +
    1.60 +declare eq_refl [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.61 +
    1.62 +declare sym [THEN eq_refl, order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.63 +
    1.64 +declare less_trans [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.65 +  
    1.66 +declare less_le_trans [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.67 +  
    1.68 +declare le_less_trans [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.69 +
    1.70 +declare order_trans [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.71 +
    1.72 +declare le_neq_trans [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.73 +
    1.74 +declare neq_le_trans [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.75 +
    1.76 +declare less_imp_neq [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.77 +
    1.78 +declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.79 +
    1.80 +declare not_sym [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.81  
    1.82  end
    1.83  
    1.84  context linorder
    1.85  begin
    1.86  
    1.87 -lemmas
    1.88 -  [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _
    1.89 +declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]]
    1.90 +
    1.91 +declare less_irrefl [THEN notE, order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.92 +
    1.93 +declare order_refl [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.94 +
    1.95 +declare less_imp_le [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.96 +
    1.97 +declare not_less [THEN iffD2, order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
    1.98 +
    1.99 +declare not_le [THEN iffD2, order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.100 +
   1.101 +declare not_less [THEN iffD1, order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.102 +
   1.103 +declare not_le [THEN iffD1, order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.104 +
   1.105 +declare antisym [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.106 +
   1.107 +declare eq_refl [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.108  
   1.109 -lemmas
   1.110 -  [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.111 -  less_irrefl [THEN notE]
   1.112 -lemmas
   1.113 -  [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.114 -  order_refl
   1.115 -lemmas
   1.116 -  [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.117 -  less_imp_le
   1.118 -lemmas
   1.119 -  [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.120 -  not_less [THEN iffD2]
   1.121 -lemmas
   1.122 -  [order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.123 -  not_le [THEN iffD2]
   1.124 -lemmas
   1.125 -  [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.126 -  not_less [THEN iffD1]
   1.127 -lemmas
   1.128 -  [order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.129 -  not_le [THEN iffD1]
   1.130 -lemmas
   1.131 -  [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.132 -  antisym
   1.133 -lemmas
   1.134 -  [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.135 -  eq_refl
   1.136 -lemmas
   1.137 -  [order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.138 -  sym [THEN eq_refl]
   1.139 -lemmas
   1.140 -  [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.141 -  less_trans
   1.142 -lemmas
   1.143 -  [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.144 -  less_le_trans
   1.145 -lemmas
   1.146 -  [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.147 -  le_less_trans
   1.148 -lemmas
   1.149 -  [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.150 -  order_trans
   1.151 -lemmas
   1.152 -  [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.153 -  le_neq_trans
   1.154 -lemmas
   1.155 -  [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.156 -  neq_le_trans
   1.157 -lemmas
   1.158 -  [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.159 -  less_imp_neq
   1.160 -lemmas
   1.161 -  [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.162 -  eq_neq_eq_imp_neq
   1.163 -lemmas
   1.164 -  [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   1.165 -  not_sym
   1.166 +declare sym [THEN eq_refl, order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.167 +
   1.168 +declare less_trans [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.169 +
   1.170 +declare less_le_trans [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.171 +
   1.172 +declare le_less_trans [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.173 +
   1.174 +declare order_trans [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.175 +
   1.176 +declare le_neq_trans [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.177 +
   1.178 +declare neq_le_trans [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.179 +
   1.180 +declare less_imp_neq [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.181 +
   1.182 +declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.183 +
   1.184 +declare not_sym [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
   1.185  
   1.186  end
   1.187