52 by (cut_facts_tac prems 1); |
52 by (cut_facts_tac prems 1); |
53 by (split_tac [expand_if] 1); |
53 by (split_tac [expand_if] 1); |
54 by (Asm_simp_tac 1); |
54 by (Asm_simp_tac 1); |
55 by (blast_tac (claset() addIs [order_antisym]) 1); |
55 by (blast_tac (claset() addIs [order_antisym]) 1); |
56 qed "min_leastR"; |
56 qed "min_leastR"; |
|
57 |
|
58 |
|
59 section "Linear/Total Orders"; |
|
60 |
|
61 goal thy "!!x::'a::linorder. x<y | x=y | y<x"; |
|
62 by (simp_tac (simpset() addsimps [order_less_le]) 1); |
|
63 by(cut_facts_tac [linorder_linear] 1); |
|
64 by (Blast_tac 1); |
|
65 qed "linorder_less_linear"; |
|
66 |
|
67 goalw thy [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"; |
|
68 by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1); |
|
69 by(cut_facts_tac [linorder_linear] 1); |
|
70 by (blast_tac (claset() addIs [order_trans]) 1); |
|
71 qed "le_max_iff_disj"; |
|
72 |
|
73 goalw thy [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"; |
|
74 by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1); |
|
75 by(cut_facts_tac [linorder_linear] 1); |
|
76 by (blast_tac (claset() addIs [order_trans]) 1); |
|
77 qed "max_le_iff_conj"; |
|
78 |
|
79 goalw thy [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"; |
|
80 by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1); |
|
81 by(cut_facts_tac [linorder_linear] 1); |
|
82 by (blast_tac (claset() addIs [order_trans]) 1); |
|
83 qed "le_min_iff_conj"; |
|
84 |
|
85 goalw thy [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"; |
|
86 by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1); |
|
87 by(cut_facts_tac [linorder_linear] 1); |
|
88 by (blast_tac (claset() addIs [order_trans]) 1); |
|
89 qed "min_le_iff_disj"; |
|
90 |
|
91 |