2102 by (rule subsetD) |
2106 by (rule subsetD) |
2103 |
2107 |
2104 lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B" |
2108 lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B" |
2105 by (rule subsetD) |
2109 by (rule subsetD) |
2106 |
2110 |
2107 lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c" |
|
2108 by (rule subst) |
|
2109 |
|
2110 lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c" |
|
2111 by (rule ssubst) |
|
2112 |
|
2113 lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c" |
|
2114 by (rule subst) |
|
2115 |
|
2116 lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c" |
|
2117 by (rule ssubst) |
|
2118 |
|
2119 lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==> |
|
2120 (!!x y. x < y ==> f x < f y) ==> f a < c" |
|
2121 proof - |
|
2122 assume r: "!!x y. x < y ==> f x < f y" |
|
2123 assume "a < b" hence "f a < f b" by (rule r) |
|
2124 also assume "f b < c" |
|
2125 finally (order_less_trans) show ?thesis . |
|
2126 qed |
|
2127 |
|
2128 lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==> |
|
2129 (!!x y. x < y ==> f x < f y) ==> a < f c" |
|
2130 proof - |
|
2131 assume r: "!!x y. x < y ==> f x < f y" |
|
2132 assume "a < f b" |
|
2133 also assume "b < c" hence "f b < f c" by (rule r) |
|
2134 finally (order_less_trans) show ?thesis . |
|
2135 qed |
|
2136 |
|
2137 lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==> |
|
2138 (!!x y. x <= y ==> f x <= f y) ==> f a < c" |
|
2139 proof - |
|
2140 assume r: "!!x y. x <= y ==> f x <= f y" |
|
2141 assume "a <= b" hence "f a <= f b" by (rule r) |
|
2142 also assume "f b < c" |
|
2143 finally (order_le_less_trans) show ?thesis . |
|
2144 qed |
|
2145 |
|
2146 lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==> |
|
2147 (!!x y. x < y ==> f x < f y) ==> a < f c" |
|
2148 proof - |
|
2149 assume r: "!!x y. x < y ==> f x < f y" |
|
2150 assume "a <= f b" |
|
2151 also assume "b < c" hence "f b < f c" by (rule r) |
|
2152 finally (order_le_less_trans) show ?thesis . |
|
2153 qed |
|
2154 |
|
2155 lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==> |
|
2156 (!!x y. x < y ==> f x < f y) ==> f a < c" |
|
2157 proof - |
|
2158 assume r: "!!x y. x < y ==> f x < f y" |
|
2159 assume "a < b" hence "f a < f b" by (rule r) |
|
2160 also assume "f b <= c" |
|
2161 finally (order_less_le_trans) show ?thesis . |
|
2162 qed |
|
2163 |
|
2164 lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==> |
|
2165 (!!x y. x <= y ==> f x <= f y) ==> a < f c" |
|
2166 proof - |
|
2167 assume r: "!!x y. x <= y ==> f x <= f y" |
|
2168 assume "a < f b" |
|
2169 also assume "b <= c" hence "f b <= f c" by (rule r) |
|
2170 finally (order_less_le_trans) show ?thesis . |
|
2171 qed |
|
2172 |
|
2173 lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==> |
|
2174 (!!x y. x <= y ==> f x <= f y) ==> a <= f c" |
|
2175 proof - |
|
2176 assume r: "!!x y. x <= y ==> f x <= f y" |
|
2177 assume "a <= f b" |
|
2178 also assume "b <= c" hence "f b <= f c" by (rule r) |
|
2179 finally (order_trans) show ?thesis . |
|
2180 qed |
|
2181 |
|
2182 lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==> |
|
2183 (!!x y. x <= y ==> f x <= f y) ==> f a <= c" |
|
2184 proof - |
|
2185 assume r: "!!x y. x <= y ==> f x <= f y" |
|
2186 assume "a <= b" hence "f a <= f b" by (rule r) |
|
2187 also assume "f b <= c" |
|
2188 finally (order_trans) show ?thesis . |
|
2189 qed |
|
2190 |
|
2191 lemma ord_le_eq_subst: "a <= b ==> f b = c ==> |
|
2192 (!!x y. x <= y ==> f x <= f y) ==> f a <= c" |
|
2193 proof - |
|
2194 assume r: "!!x y. x <= y ==> f x <= f y" |
|
2195 assume "a <= b" hence "f a <= f b" by (rule r) |
|
2196 also assume "f b = c" |
|
2197 finally (ord_le_eq_trans) show ?thesis . |
|
2198 qed |
|
2199 |
|
2200 lemma ord_eq_le_subst: "a = f b ==> b <= c ==> |
|
2201 (!!x y. x <= y ==> f x <= f y) ==> a <= f c" |
|
2202 proof - |
|
2203 assume r: "!!x y. x <= y ==> f x <= f y" |
|
2204 assume "a = f b" |
|
2205 also assume "b <= c" hence "f b <= f c" by (rule r) |
|
2206 finally (ord_eq_le_trans) show ?thesis . |
|
2207 qed |
|
2208 |
|
2209 lemma ord_less_eq_subst: "a < b ==> f b = c ==> |
|
2210 (!!x y. x < y ==> f x < f y) ==> f a < c" |
|
2211 proof - |
|
2212 assume r: "!!x y. x < y ==> f x < f y" |
|
2213 assume "a < b" hence "f a < f b" by (rule r) |
|
2214 also assume "f b = c" |
|
2215 finally (ord_less_eq_trans) show ?thesis . |
|
2216 qed |
|
2217 |
|
2218 lemma ord_eq_less_subst: "a = f b ==> b < c ==> |
|
2219 (!!x y. x < y ==> f x < f y) ==> a < f c" |
|
2220 proof - |
|
2221 assume r: "!!x y. x < y ==> f x < f y" |
|
2222 assume "a = f b" |
|
2223 also assume "b < c" hence "f b < f c" by (rule r) |
|
2224 finally (ord_eq_less_trans) show ?thesis . |
|
2225 qed |
|
2226 |
|
2227 instance set :: (type) order |
|
2228 by (intro_classes, |
|
2229 (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+) |
|
2230 |
|
2231 text {* |
|
2232 Note that this list of rules is in reverse order of priorities. |
|
2233 *} |
|
2234 |
|
2235 lemmas basic_trans_rules [trans] = |
2111 lemmas basic_trans_rules [trans] = |
2236 order_less_subst2 |
2112 order_trans_rules set_rev_mp set_mp |
2237 order_less_subst1 |
|
2238 order_le_less_subst2 |
|
2239 order_le_less_subst1 |
|
2240 order_less_le_subst2 |
|
2241 order_less_le_subst1 |
|
2242 order_subst2 |
|
2243 order_subst1 |
|
2244 ord_le_eq_subst |
|
2245 ord_eq_le_subst |
|
2246 ord_less_eq_subst |
|
2247 ord_eq_less_subst |
|
2248 forw_subst |
|
2249 back_subst |
|
2250 rev_mp |
|
2251 mp |
|
2252 set_rev_mp |
|
2253 set_mp |
|
2254 order_neq_le_trans |
|
2255 order_le_neq_trans |
|
2256 order_less_trans |
|
2257 order_less_asym' |
|
2258 order_le_less_trans |
|
2259 order_less_le_trans |
|
2260 order_trans |
|
2261 order_antisym |
|
2262 ord_le_eq_trans |
|
2263 ord_eq_le_trans |
|
2264 ord_less_eq_trans |
|
2265 ord_eq_less_trans |
|
2266 trans |
|
2267 |
2113 |
2268 end |
2114 end |