equal
deleted
inserted
replaced
102 qed "Int_Collect_mono"; |
102 qed "Int_Collect_mono"; |
103 |
103 |
104 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, |
104 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, |
105 ex_mono, Collect_mono, in_mono]; |
105 ex_mono, Collect_mono, in_mono]; |
106 |
106 |
107 (* Courtesy of Stephan Merz *) |
|
108 Goalw [Least_def] |
|
109 "[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \ |
|
110 \ ==> (LEAST y. y : f`S) = f(LEAST x. x : S)"; |
|
111 by (Clarify_tac 1); |
|
112 by (eres_inst_tac [("P","%x. x : S")] LeastMI2 1); |
|
113 by (Fast_tac 1); |
|
114 by (rtac LeastMI2 1); |
|
115 by (auto_tac (claset() addEs [monoD] addSIs [thm "order_antisym"], simpset())); |
|
116 qed "Least_mono"; |
|
117 |
|
118 Goal "[| a = b; c = d; b --> d |] ==> a --> c"; |
107 Goal "[| a = b; c = d; b --> d |] ==> a --> c"; |
119 by (Fast_tac 1); |
108 by (Fast_tac 1); |
120 qed "eq_to_mono"; |
109 qed "eq_to_mono"; |
121 |
110 |
122 Goal "[| a = b; c = d; ~ b --> ~ d |] ==> ~ a --> ~ c"; |
111 Goal "[| a = b; c = d; ~ b --> ~ d |] ==> ~ a --> ~ c"; |