open three ; bind_st_thm ("threes", "[| $X |- $Y; $X |- @ $Y; $X |- *@* $Y |] ==> $X |- *@* @ $Y", [asm_rl, md1 blob, md1 sbs] MRS threea RS md2 blob RS md2 sbs) ; (* to prove axiom .3 from rule .3 *) val ax3 = prove_goal thy "$I |- wdm A & wdm B -> wdm (A & wdm B) v wdm (B & wdm A) v wdm (A & B)" (fn _ => [ rtac imps 1, rtac mla 1, rtac anda 1, rtac ors 1, d_b_tac "-l" (rtac ors) 1, disp_tac "-lr" 1, rtac cS 1, disp_tac "|rlr" 1, rtac (md2 aS) 1, rtac (md1 pSe) 1, rtac (md2 aS) 1, d_b_tac "-r" (rtac (md2 aS)) 1, rtac (md2 aS) 1, rtac wdma 1, disp_tac "|*@*" 1, rtac sbsdists 1, d_b_tac "-r" (rtac wdmS) 1, d_b_tac "-r" (rtac andS) 1, rtac mls 1, rtac idf 1, disp_tac "-l*@*" 1, d_b_tac "-l" (rtac (md1 pSe)) 1, rtac (md1 aS) 1, disp_tac "-l*" 1, rtac wdma 1, disp_tac "|*@" 1, glob_tac (tfpr pr_dd) 1, rtac bldista 1, d_b_tac "|r" (rtac bldista) 1, d_b_tac "|rl" (rtac bldista) 1, disp_tac "|r" 1, rtac (md2 dcp) 1, glob_tac (tfpr pr_dd) 1, d_b_tac "-l" (rtac wdmS) 1, d_b_tac "-rl" (rtac wdmS) 1, d_b_tac "-rr" (rtac wdmS) 1, d_b_tac "|r@*@" (rtac (md2 ssS)) 1, d_b_tac "|r" (rtac threea) 1, d_b_tac "|r*" (rtac mls) 1, rtac mrs 1, glob_tac (tfpr pr_dbl) 1, rtac ands 1, rtac idf 1, rtac idf 1, d_b_tac "|r@*" (rtac mrs) 1, disp_tac "|l" 1, (rtac mls) 1, rtac wdmS 1, rtac idf 1, glob_tac (tfpr pr_dbl) 1, d_b_tac "|r*@" (rtac mls) 1, rtac mls 1, rtac mrs 1, rtac ands 1, rtac wdms 2, rtac idf 1, rtac idf 1]) ; (* axiom .3 as structural rule *) val ax3sr = prove_goal three.thy "[| (*@* ($P,*@* $Q) |- $Z) ; (*@* ($Q,*@* $P) |- $Z) ; *@* ($P,$Q) |- $Z |] \ \ ==> *@* $P, *@* $Q |- $Z " (fn [p1, p2, p3] => [ rtac cS 1, disp_tac "|r" 1, rtac (md2 aS) 1, disp_tac "|uuu" 1, bup_tac (tfpr pr_bdd) 1, disp_tac "-luuulu" 1, rtac bldista 1, disp_tac "|l" 1, glob_tac (tfpr pr_dbl) 1, rtac threea 1, rtac mra 1, disp_tac "-ruuu" 1, glob_tac (tfpr pr_dbl) 1, rtac p3 1, rtac mrs 1, disp_tac "|ul" 1, disp_tac "-ruuu" 1, d_b_tac "|uuu" (rtac pA) 1, rtac p2 1, d_b_tac "|uuu" (rtac mra) 1, disp_tac "-ruuu" 1, glob_tac (tfpr pr_dbl) 1, rtac p1 1]) ; (* alternative proof of axiom.3 *) val ax3 = prove_goal thy "$I |- wdm A & wdm B -> wdm (A & wdm B) v wdm (B & wdm A) v wdm (A & B)" (fn _ => [ glob_tac (tfpr pr_intr) 1, disp_tac "-lu" 1, rep_glob_tac (tfpr pr_simp) 1, rtac ax3sr 1, keep_tac ["|", "-ll"] 1, keep_tac ["|", "-lr"] 2, keep_tac ["|", "-r"] 3, ALLGOALS (rtac wdms THEN' glob_tac (tfpr pr_intr)), ALLGOALS (weak_tac), ALLGOALS (rtac mla THEN' rtac wdms THEN' rtac idf)]) ; (* now prove axiom threea from ax3sr *) val threea_alt = prove_goal three.thy "[| $X |- $Y ; (@ $X) |- $Y ; *@* $X |- $Y |] ==> @*@* $X |- $Y" (fn prems => [ rtac (md2 ssS) 1, disp_tac "|u" 1, rtac ils 1, disp_tac "-l" 1, rtac ax3sr 1, ALLGOALS (d_t_name "Y" THEN' bup_tac (tfpr pr_simp) THEN' resolve_tac prems)]) ; (* val ax3a = prove_goal thy "$I |- wbx (wbx A -> wbx B) v wbx (wbx B -> wbx A)" (fn _ => [ *)