equal
deleted
inserted
replaced
154 (* ------------------------------------------------------------------------ *) |
154 (* ------------------------------------------------------------------------ *) |
155 (* first 5 ugly lemmas *) |
155 (* first 5 ugly lemmas *) |
156 (* ------------------------------------------------------------------------ *) |
156 (* ------------------------------------------------------------------------ *) |
157 |
157 |
158 qed_goal "ssum_lemma9" Ssum3.thy |
158 qed_goal "ssum_lemma9" Ssum3.thy |
159 "[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)" |
159 "[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)" |
160 (fn prems => |
160 (fn prems => |
161 [ |
161 [ |
162 (cut_facts_tac prems 1), |
162 (cut_facts_tac prems 1), |
163 (strip_tac 1), |
163 (strip_tac 1), |
164 (res_inst_tac [("p","Y(i)")] IssumE 1), |
164 (res_inst_tac [("p","Y(i)")] IssumE 1), |
172 (etac is_ub_thelub 1) |
172 (etac is_ub_thelub 1) |
173 ]); |
173 ]); |
174 |
174 |
175 |
175 |
176 qed_goal "ssum_lemma10" Ssum3.thy |
176 qed_goal "ssum_lemma10" Ssum3.thy |
177 "[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)" |
177 "[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)" |
178 (fn prems => |
178 (fn prems => |
179 [ |
179 [ |
180 (cut_facts_tac prems 1), |
180 (cut_facts_tac prems 1), |
181 (strip_tac 1), |
181 (strip_tac 1), |
182 (res_inst_tac [("p","Y(i)")] IssumE 1), |
182 (res_inst_tac [("p","Y(i)")] IssumE 1), |
191 (etac subst 1), |
191 (etac subst 1), |
192 (etac is_ub_thelub 1) |
192 (etac is_ub_thelub 1) |
193 ]); |
193 ]); |
194 |
194 |
195 qed_goal "ssum_lemma11" Ssum3.thy |
195 qed_goal "ssum_lemma11" Ssum3.thy |
196 "[| is_chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\ |
196 "[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\ |
197 \ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
197 \ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
198 (fn prems => |
198 (fn prems => |
199 [ |
199 [ |
200 (cut_facts_tac prems 1), |
200 (cut_facts_tac prems 1), |
201 (asm_simp_tac Ssum0_ss 1), |
201 (asm_simp_tac Ssum0_ss 1), |
208 (etac (inst_ssum_pcpo RS ssubst) 1), |
208 (etac (inst_ssum_pcpo RS ssubst) 1), |
209 (asm_simp_tac Ssum0_ss 1) |
209 (asm_simp_tac Ssum0_ss 1) |
210 ]); |
210 ]); |
211 |
211 |
212 qed_goal "ssum_lemma12" Ssum3.thy |
212 qed_goal "ssum_lemma12" Ssum3.thy |
213 "[| is_chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\ |
213 "[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\ |
214 \ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
214 \ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
215 (fn prems => |
215 (fn prems => |
216 [ |
216 [ |
217 (cut_facts_tac prems 1), |
217 (cut_facts_tac prems 1), |
218 (asm_simp_tac Ssum0_ss 1), |
218 (asm_simp_tac Ssum0_ss 1), |
267 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1) |
267 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1) |
268 ]); |
268 ]); |
269 |
269 |
270 |
270 |
271 qed_goal "ssum_lemma13" Ssum3.thy |
271 qed_goal "ssum_lemma13" Ssum3.thy |
272 "[| is_chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\ |
272 "[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\ |
273 \ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
273 \ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
274 (fn prems => |
274 (fn prems => |
275 [ |
275 [ |
276 (cut_facts_tac prems 1), |
276 (cut_facts_tac prems 1), |
277 (asm_simp_tac Ssum0_ss 1), |
277 (asm_simp_tac Ssum0_ss 1), |
577 tac, |
577 tac, |
578 (rtac less_ssum3d 1) |
578 (rtac less_ssum3d 1) |
579 ]); |
579 ]); |
580 |
580 |
581 qed_goalw "ssum_chainE" Ssum3.thy [sinl_def,sinr_def] |
581 qed_goalw "ssum_chainE" Ssum3.thy [sinl_def,sinr_def] |
582 "is_chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)" |
582 "chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)" |
583 (fn prems => |
583 (fn prems => |
584 [ |
584 [ |
585 (cut_facts_tac prems 1), |
585 (cut_facts_tac prems 1), |
586 (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1), |
586 (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1), |
587 (etac ssum_lemma4 1) |
587 (etac ssum_lemma4 1) |
588 ]); |
588 ]); |
589 |
589 |
590 |
590 |
591 qed_goalw "thelub_ssum2a" Ssum3.thy [sinl_def,sinr_def,sswhen_def] |
591 qed_goalw "thelub_ssum2a" Ssum3.thy [sinl_def,sinr_def,sswhen_def] |
592 "[| is_chain(Y); !i.? x. Y(i) = sinl`x |] ==>\ |
592 "[| chain(Y); !i.? x. Y(i) = sinl`x |] ==>\ |
593 \ lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))" |
593 \ lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))" |
594 (fn prems => |
594 (fn prems => |
595 [ |
595 [ |
596 (cut_facts_tac prems 1), |
596 (cut_facts_tac prems 1), |
597 (stac beta_cfun 1), |
597 (stac beta_cfun 1), |
612 (rtac refl 1), |
612 (rtac refl 1), |
613 (asm_simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1) |
613 (asm_simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1) |
614 ]); |
614 ]); |
615 |
615 |
616 qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def] |
616 qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def] |
617 "[| is_chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ |
617 "[| chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ |
618 \ lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))" |
618 \ lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))" |
619 (fn prems => |
619 (fn prems => |
620 [ |
620 [ |
621 (cut_facts_tac prems 1), |
621 (cut_facts_tac prems 1), |
622 (stac beta_cfun 1), |
622 (stac beta_cfun 1), |
639 [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
639 [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
640 cont_Iwhen3]) 1) |
640 cont_Iwhen3]) 1) |
641 ]); |
641 ]); |
642 |
642 |
643 qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def] |
643 qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def] |
644 "[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x" |
644 "[| chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x" |
645 (fn prems => |
645 (fn prems => |
646 [ |
646 [ |
647 (cut_facts_tac prems 1), |
647 (cut_facts_tac prems 1), |
648 (asm_simp_tac (Ssum0_ss addsimps |
648 (asm_simp_tac (Ssum0_ss addsimps |
649 [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
649 [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
653 [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
653 [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
654 cont_Iwhen3]) 1) |
654 cont_Iwhen3]) 1) |
655 ]); |
655 ]); |
656 |
656 |
657 qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def] |
657 qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def] |
658 "[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x" |
658 "[| chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x" |
659 (fn prems => |
659 (fn prems => |
660 [ |
660 [ |
661 (cut_facts_tac prems 1), |
661 (cut_facts_tac prems 1), |
662 (asm_simp_tac (Ssum0_ss addsimps |
662 (asm_simp_tac (Ssum0_ss addsimps |
663 [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
663 [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
667 [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
667 [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
668 cont_Iwhen3]) 1) |
668 cont_Iwhen3]) 1) |
669 ]); |
669 ]); |
670 |
670 |
671 qed_goal "thelub_ssum3" Ssum3.thy |
671 qed_goal "thelub_ssum3" Ssum3.thy |
672 "is_chain(Y) ==>\ |
672 "chain(Y) ==>\ |
673 \ lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))\ |
673 \ lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))\ |
674 \ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))" |
674 \ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))" |
675 (fn prems => |
675 (fn prems => |
676 [ |
676 [ |
677 (cut_facts_tac prems 1), |
677 (cut_facts_tac prems 1), |