equal
deleted
inserted
replaced
103 |
103 |
104 (*Used in individual datatype definitions*) |
104 (*Used in individual datatype definitions*) |
105 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, |
105 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, |
106 ex_mono, Collect_mono, in_mono]; |
106 ex_mono, Collect_mono, in_mono]; |
107 |
107 |
|
108 (* Courtesy of Stefan Merz *) |
|
109 Goalw [Least_def,mono_def] |
|
110 "[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \ |
|
111 \ ==> (LEAST y. y : f``S) = f(LEAST x. x : S)"; |
|
112 by (etac bexE 1); |
|
113 by (rtac selectI2 1); |
|
114 by (Force_tac 1); |
|
115 by (rtac select_equality 1); |
|
116 by (Force_tac 1); |
|
117 by (force_tac (claset() addSIs [order_antisym], simpset()) 1); |
|
118 qed "Least_mono"; |