56 |
56 |
57 section "Linear/Total Orders"; |
57 section "Linear/Total Orders"; |
58 |
58 |
59 Goal "!!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 [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 [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 [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 [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 |
89 |
89 |