open mint ; (* consequences of psh - note all this assumes that we have the boolean negation operator, which is I think not so *) val pshS = idf RS pshA RS md2 blob RSN (2, cut) ; val [pshbdm, pshwbx] = map s2l [idf RS pshA, idf RS pshA RS md2 blob] ; val pshwdm = prove_goal thy "wdm A |- A" (fn _ => [(glob_tac (tfpr pr_intr) 1), (rtac (md1 sA) 1), tau_tac 1, rtac pshwbx 1]) ; val pshbbx = prove_goal thy "A |- bbx A" (fn _ => [(glob_tac (tfpr pr_intr) 1), (rtac (md1 sS) 1), tau_tac 1, rtac pshbdm 1]) ; (* supposedly a rule separate from psh, see p22 of Gore, TR-ARP-1-95 *) val prhA = l2s pshwdm RS cut ; (* to prove the intuitionistic logic axioms given in Belnap, Display Logic, pp 405-6, using the axiomatisation given in Gore, TR-ARP-1-95 (roughly - changed to define ->h and ~h in terms of related logical connectives *) val hdefs = [noth_def, imph_def] ; val tacIs = [ (glob_tac (tfpr pr_intr) 1), (ALLGOALS (EVERY' [ (rtac (nA RS md2 blob)), (rtac (mra RS md1 ca2)), (TRY o rtac (pshA RS md2 blob)), weak_tac]))] ; fun mkIs str tacs = prove_goalw thy hdefs str (fn _ => tacs) ; val I1 = mkIs "$I |- A ->h (B ->h A)" tacIs ; val I3 = mkIs "$I |- (A & B) ->h A" tacIs ; val I4 = mkIs "$I |- (A & B) ->h B" tacIs ; val I5 = mkIs "$I |- A ->h B ->h (A & B)" tacIs ; val I6 = mkIs "$I |- A ->h (A v B)" tacIs ; val I7 = mkIs "$I |- B ->h (A v B)" tacIs ; val I8 = prove_goalw thy hdefs "$I |- (A ->h C) ->h (B ->h C) ->h (A v B ->h C)" (fn _ => [(glob_tac (tfpr pr_intr) 1), (ALLGOALS (rtac (nA RS md2 blob))), (rtac mls 2), (rtac (nA RS md2 blob) 2), (ALLGOALS (rtac (mra RS md1 ca2))), (rtac (pshA RS md2 blob) 1), (rtac mls 1), (ALLGOALS (EVERY' [rtac wbxa, (glob_tac (tfpr pr_intr))])), (ALLGOALS weak_tac)]) ; val pr_wbt = make_prt ([wbxa RS TS], []) ; val tacs29 = [(glob_tac (tfpr pr_intr) 1), (rtac (nA RS md2 blob) 1), (rtac (mra RS md1 ca2) 1), (rtac (pshA RS md2 blob) 1), (disp_tac "-ru" 1), (glob_tac (tfpr pr_bdd) 1), (glob_tac (tfpr (pr_append (pr_wbt, pr_intr))) 1), ALLGOALS weak_tac] ; val I2 = mkIs "$I |- (A ->h B) ->h (A ->h B ->h C) ->h (A ->h C)" tacs29 ; val I9 = mkIs "$I |- (A ->h B) ->h (A ->h ~h B) ->h ~h A" tacs29 ; val I10 = prove_goalw thy hdefs "$I |- A ->h (~h A ->h B)" (fn _ => [(glob_tac (tfpr pr_intr) 1), (rtac (nA RS md2 blob) 1), (rtac (mra RS md1 ca2) 1), (rtac (md2 blob) 1), rtac mrs 1, rtac pshA 1, (rtac (md1 sS) 1), rtac TS 1, rtac wbxa 1, rtac nota 1, weak_tac 1]) ; val imp_rev = prove_goal thy "A -> B |- *A, B" (fn _ => [ (rtac impa 1), ALLGOALS weak_tac]) ; (* modus ponens *) val mp = prove_goalw thy hdefs "[| $I |- A ; $I |- A ->h B |] ==> $I |- B" (fn [pa, pab] => let val pab1 = [pab, axT'] MRS cut ; val pab2 = [pab1, imp_rev] MRS cut ; in [ (rtac (pa RS cut) 1), (rtac ila 1), (rtac (md2 ca1) 1), (rtac pS 1), (rtac pab2 1)] end) ; (* proofs using lax logic axioms for bdm, ie ax4_bdm', axT_bdm', bdm_mono *) val ext_bdm = [bdm_mono, ax4_bdm'] MRS cut ; (* but note, although bdm_mono and ext_bdm are like monadic mapo and ext, we can't prove "A --> B |- bdm A --> bdm B" or "A --> bdm B |- bdm A --> bdm B" *)