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 -lemmas
1.92 - [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.93 - less_irrefl [THEN notE]
1.94 -lemmas
1.95 - [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.96 - order_refl
1.97 -lemmas
1.98 - [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.99 - less_imp_le
1.100 -lemmas
1.101 - [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.102 - not_less [THEN iffD2]
1.103 -lemmas
1.104 - [order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.105 - not_le [THEN iffD2]
1.106 -lemmas
1.107 - [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.108 - not_less [THEN iffD1]
1.109 -lemmas
1.110 - [order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.111 - not_le [THEN iffD1]
1.112 -lemmas
1.113 - [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.114 - antisym
1.115 -lemmas
1.116 - [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.117 - eq_refl
1.118 -lemmas
1.119 - [order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.120 - sym [THEN eq_refl]
1.121 -lemmas
1.122 - [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.123 - less_trans
1.124 -lemmas
1.125 - [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.126 - less_le_trans
1.127 -lemmas
1.128 - [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.129 - le_less_trans
1.130 -lemmas
1.131 - [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.132 - order_trans
1.133 -lemmas
1.134 - [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.135 - le_neq_trans
1.136 -lemmas
1.137 - [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.138 - neq_le_trans
1.139 -lemmas
1.140 - [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.141 - less_imp_neq
1.142 -lemmas
1.143 - [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.144 - eq_neq_eq_imp_neq
1.145 -lemmas
1.146 - [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
1.147 - not_sym
1.148 +declare less_irrefl [THEN notE, order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
1.149 +
1.150 +declare order_refl [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
1.151 +
1.152 +declare less_imp_le [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
1.153 +
1.154 +declare not_less [THEN iffD2, order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
1.155 +
1.156 +declare not_le [THEN iffD2, order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
1.157 +
1.158 +declare not_less [THEN iffD1, order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
1.159 +
1.160 +declare not_le [THEN iffD1, order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
1.161 +
1.162 +declare antisym [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
1.163 +
1.164 +declare eq_refl [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
1.165 +
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