equal
deleted
inserted
replaced
27 |
27 |
28 (*A convenient way of finding a closed form for inv h*) |
28 (*A convenient way of finding a closed form for inv h*) |
29 val [surj,prem] = Goalw [inv_def] |
29 val [surj,prem] = Goalw [inv_def] |
30 "[| surj h; !! x y. g (h(x,y)) = x |] ==> fst (inv h z) = g z"; |
30 "[| surj h; !! x y. g (h(x,y)) = x |] ==> fst (inv h z) = g z"; |
31 by (res_inst_tac [("y1", "z")] (surj RS surjD RS exE) 1); |
31 by (res_inst_tac [("y1", "z")] (surj RS surjD RS exE) 1); |
32 br selectI2 1; |
32 by (rtac selectI2 1); |
33 by (dres_inst_tac [("f", "g")] arg_cong 2); |
33 by (dres_inst_tac [("f", "g")] arg_cong 2); |
34 by (auto_tac (claset(), simpset() addsimps [prem])); |
34 by (auto_tac (claset(), simpset() addsimps [prem])); |
35 qed "fst_inv_equalityI"; |
35 qed "fst_inv_equalityI"; |
36 |
36 |
37 |
37 |
198 by (Force_tac 1); |
198 by (Force_tac 1); |
199 qed "project_act_Id"; |
199 qed "project_act_Id"; |
200 |
200 |
201 Goalw [project_set_def, project_act_def] |
201 Goalw [project_set_def, project_act_def] |
202 "Domain (project_act h act) = project_set h (Domain act)"; |
202 "Domain (project_act h act) = project_set h (Domain act)"; |
203 auto(); |
203 by Auto_tac; |
204 by (res_inst_tac [("y1", "ya")] (surj_h RS surjD RS exE) 1); |
204 by (res_inst_tac [("y1", "ya")] (surj_h RS surjD RS exE) 1); |
205 auto(); |
205 by Auto_tac; |
206 qed "Domain_project_act"; |
206 qed "Domain_project_act"; |
207 |
207 |
208 Addsimps [extend_act_Id, project_act_Id]; |
208 Addsimps [extend_act_Id, project_act_Id]; |
209 |
209 |
210 Goal "Id : extend_act h `` Acts F"; |
210 Goal "Id : extend_act h `` Acts F"; |
560 (*** progress for (project h F) ***) |
560 (*** progress for (project h F) ***) |
561 |
561 |
562 Goal "F : transient (extend_set h A) ==> project h F : transient A"; |
562 Goal "F : transient (extend_set h A) ==> project h F : transient A"; |
563 by (auto_tac (claset(), |
563 by (auto_tac (claset(), |
564 simpset() addsimps [transient_def, Domain_project_act])); |
564 simpset() addsimps [transient_def, Domain_project_act])); |
565 br bexI 1; |
565 by (rtac bexI 1); |
566 ba 2; |
566 by (assume_tac 2); |
567 by (full_simp_tac (simpset() addsimps [extend_set_def, project_set_def, |
567 by (full_simp_tac (simpset() addsimps [extend_set_def, project_set_def, |
568 project_act_def]) 1); |
568 project_act_def]) 1); |
569 by (Blast_tac 1); |
569 by (Blast_tac 1); |
570 qed "transient_extend_set_imp_project_transient"; |
570 qed "transient_extend_set_imp_project_transient"; |
571 |
571 |
575 \ ALL act: Acts F. extend_set h (project_set h (Domain act)) <= \ |
575 \ ALL act: Acts F. extend_set h (project_set h (Domain act)) <= \ |
576 \ Domain act |] \ |
576 \ Domain act |] \ |
577 \ ==> F : transient (extend_set h A)"; |
577 \ ==> F : transient (extend_set h A)"; |
578 by (auto_tac (claset(), |
578 by (auto_tac (claset(), |
579 simpset() addsimps [transient_def, Domain_project_act])); |
579 simpset() addsimps [transient_def, Domain_project_act])); |
580 br bexI 1; |
580 by (rtac bexI 1); |
581 ba 2; |
581 by (assume_tac 2); |
582 by Auto_tac; |
582 by Auto_tac; |
583 by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1); |
583 by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1); |
584 by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1); |
584 by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1); |
585 by (thin_tac "ALL act:?AA. ?P (act)" 1); |
585 by (thin_tac "ALL act:?AA. ?P (act)" 1); |
586 by (force_tac (claset() addDs [project_act_I], simpset()) 1); |
586 by (force_tac (claset() addDs [project_act_I], simpset()) 1); |