23 section "Orders"; |
23 section "Orders"; |
24 |
24 |
25 AddIffs [order_refl]; |
25 AddIffs [order_refl]; |
26 |
26 |
27 (*This form is useful with the classical reasoner*) |
27 (*This form is useful with the classical reasoner*) |
28 goal Ord.thy "!!x::'a::order. x = y ==> x <= y"; |
28 Goal "!!x::'a::order. x = y ==> x <= y"; |
29 by (etac ssubst 1); |
29 by (etac ssubst 1); |
30 by (rtac order_refl 1); |
30 by (rtac order_refl 1); |
31 qed "order_eq_refl"; |
31 qed "order_eq_refl"; |
32 |
32 |
33 goal Ord.thy "~ x < (x::'a::order)"; |
33 Goal "~ x < (x::'a::order)"; |
34 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
34 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
35 qed "order_less_irrefl"; |
35 qed "order_less_irrefl"; |
36 AddIffs [order_less_irrefl]; |
36 AddIffs [order_less_irrefl]; |
37 |
37 |
38 goal thy "(x::'a::order) <= y = (x < y | x = y)"; |
38 Goal "(x::'a::order) <= y = (x < y | x = y)"; |
39 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
39 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
40 by (Blast_tac 1); |
40 by (Blast_tac 1); |
41 qed "order_le_less"; |
41 qed "order_le_less"; |
42 |
42 |
43 (** min **) |
43 (** min **) |
44 |
44 |
45 goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least"; |
45 Goalw [min_def] "!!least. (!!x. least <= x) ==> min least x = least"; |
46 by (Asm_simp_tac 1); |
46 by (Asm_simp_tac 1); |
47 qed "min_leastL"; |
47 qed "min_leastL"; |
48 |
48 |
49 val prems = goalw thy [min_def] |
49 val prems = goalw thy [min_def] |
50 "(!!x::'a::order. least <= x) ==> min x least = least"; |
50 "(!!x::'a::order. least <= x) ==> min x least = least"; |
54 qed "min_leastR"; |
54 qed "min_leastR"; |
55 |
55 |
56 |
56 |
57 section "Linear/Total Orders"; |
57 section "Linear/Total Orders"; |
58 |
58 |
59 goal thy "!!x::'a::linorder. x<y | x=y | y<x"; |
59 Goal "!!x::'a::linorder. x<y | x=y | y<x"; |
60 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
60 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
61 by(cut_facts_tac [linorder_linear] 1); |
61 by(cut_facts_tac [linorder_linear] 1); |
62 by (Blast_tac 1); |
62 by (Blast_tac 1); |
63 qed "linorder_less_linear"; |
63 qed "linorder_less_linear"; |
64 |
64 |
65 goalw thy [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"; |
65 Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"; |
66 by (Simp_tac 1); |
66 by (Simp_tac 1); |
67 by(cut_facts_tac [linorder_linear] 1); |
67 by(cut_facts_tac [linorder_linear] 1); |
68 by (blast_tac (claset() addIs [order_trans]) 1); |
68 by (blast_tac (claset() addIs [order_trans]) 1); |
69 qed "le_max_iff_disj"; |
69 qed "le_max_iff_disj"; |
70 |
70 |
71 goalw thy [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"; |
71 Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"; |
72 by (Simp_tac 1); |
72 by (Simp_tac 1); |
73 by(cut_facts_tac [linorder_linear] 1); |
73 by(cut_facts_tac [linorder_linear] 1); |
74 by (blast_tac (claset() addIs [order_trans]) 1); |
74 by (blast_tac (claset() addIs [order_trans]) 1); |
75 qed "max_le_iff_conj"; |
75 qed "max_le_iff_conj"; |
76 |
76 |
77 goalw thy [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"; |
77 Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"; |
78 by (Simp_tac 1); |
78 by (Simp_tac 1); |
79 by(cut_facts_tac [linorder_linear] 1); |
79 by(cut_facts_tac [linorder_linear] 1); |
80 by (blast_tac (claset() addIs [order_trans]) 1); |
80 by (blast_tac (claset() addIs [order_trans]) 1); |
81 qed "le_min_iff_conj"; |
81 qed "le_min_iff_conj"; |
82 |
82 |
83 goalw thy [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"; |
83 Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"; |
84 by (Simp_tac 1); |
84 by (Simp_tac 1); |
85 by(cut_facts_tac [linorder_linear] 1); |
85 by(cut_facts_tac [linorder_linear] 1); |
86 by (blast_tac (claset() addIs [order_trans]) 1); |
86 by (blast_tac (claset() addIs [order_trans]) 1); |
87 qed "min_le_iff_disj"; |
87 qed "min_le_iff_disj"; |
88 |
88 |