equal
deleted
inserted
replaced
133 (stac lub 1), |
133 (stac lub 1), |
134 (etac selectI 1), |
134 (etac selectI 1), |
135 (atac 1) |
135 (atac 1) |
136 ]); |
136 ]); |
137 |
137 |
|
138 |
|
139 goal thy "lub{x} = x"; |
|
140 br thelubI 1; |
|
141 by(simp_tac (!simpset addsimps [is_lub,is_ub]) 1); |
|
142 qed "lub_singleton"; |
|
143 Addsimps [lub_singleton]; |
138 |
144 |
139 (* ------------------------------------------------------------------------ *) |
145 (* ------------------------------------------------------------------------ *) |
140 (* access to some definition as inference rule *) |
146 (* access to some definition as inference rule *) |
141 (* ------------------------------------------------------------------------ *) |
147 (* ------------------------------------------------------------------------ *) |
142 |
148 |
242 (cut_facts_tac prems 1), |
248 (cut_facts_tac prems 1), |
243 (rtac is_chainI 1), |
249 (rtac is_chainI 1), |
244 (rtac allI 1), |
250 (rtac allI 1), |
245 (nat_ind_tac "i" 1), |
251 (nat_ind_tac "i" 1), |
246 (Asm_simp_tac 1), |
252 (Asm_simp_tac 1), |
247 (Asm_simp_tac 1), |
253 (Asm_simp_tac 1) |
248 (rtac refl_less 1) |
|
249 ]); |
254 ]); |
250 |
255 |
251 qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def] |
256 qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def] |
252 "x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)" |
257 "x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)" |
253 (fn prems => |
258 (fn prems => |