(* Belnap.ML *) val () = qed_goal_spec_mp "frb_cut" GDT.thy "rule : rules --> frb rules (Der seq rule dtl)" (fn _ => [Simp_tac 1]) ; local val lemtac = let fun tacf i = EVERY [rtac allDT_and_mono i, (eatac noCutfrb 1 (i+2)), atac i, atac i] ; val cs = claset () addSafter ("tacf", tacf) ; in [ (full_simp_tac (init_ss addsimps (thms "allNextDTs.simps" @ thms "allDT_allDTs.simps")) 1), Simp_tac 1, Safe_tac, (res_inst_tac [("x", "a'")] exI 1), (fast_tac cs 1), (res_inst_tac [("x", "b'")] exI 1), (fast_tac cs 1)] end ; val lem1 = ( meta_std ( prove_goalw Belnap.thy [derLP_def, der_def, IsDerivableR_def] "cutIsLP M dt & allNextDTs (cutOnFmls {}) dt & \ \ allDT wfb dt & allDT (frb rules) dt & dt = Der ($X |- $Y) cutr dtl --> \ \ derLP rules ($X |- M) & der rules (M |- $Y)" (fn _ => [ Clarify_tac 1, (ftac (allDT_Der RS iffD1 RS conjunct1) 1), (ftac lrwfc 1), Clarify_tac 1, (fatac cutLPonFmls' 1 1), (datac (refl RS cutPrems) 1 1), (dtac cutIsLP_D 1), EVERY lemtac]))) ; val lem1R = ( meta_std ( prove_goalw Belnap.thy [derRP_def, der_def, IsDerivableR_def] "cutIsRP M dt & allNextDTs (cutOnFmls {}) dt & \ \ allDT wfb dt & allDT (frb rules) dt & dt = Der ($X |- $Y) cutr dtl --> \ \ der rules ($X |- M) & derRP rules (M |- $Y)" (fn _ => [ Clarify_tac 1, (ftac (allDT_Der RS iffD1 RS conjunct1) 1), (ftac lrwfc 1), Clarify_tac 1, (ftac (cutRPonFmls) 1), (datac (refl RS cutPrems) 1 1), (dtac cutIsRP_D 1), EVERY lemtac]))) ; val lem1LR = ( meta_std ( prove_goal Belnap.thy "cutIsLP M dt & cutIsRP M dt & allNextDTs (cutOnFmls {}) dt & \ \ allDT wfb dt & allDT (frb rules) dt & dt = Der ($X |- $Y) cutr dtl --> \ \ derLP rules ($X |- M) & derRP rules (M |- $Y)" (fn _ => [fast_tac (claset () addSIs [lem1 RS conjunct1, lem1R RS conjunct2]) 1]))) ; val lem2 = ( meta_std ( prove_goalw Belnap.thy [der_def, IsDerivableR_def] "cutOnFmls {M} dt & allNextDTs (cutOnFmls {}) dt & \ \ allDT wfb dt & allDT (frb rules) dt & dt = Der ($X |- $Y) cutr dtl --> \ \ der rules ($X |- M) & der rules (M |- $Y)" (fn _ => [ Clarify_tac 1, (ftac (allDT_Der RS iffD1 RS conjunct1) 1), (ftac lrwfc 1), Clarify_tac 1, (datac (refl RS cutPrems) 1 1), EVERY lemtac]))) ; val tacs1 = [ (full_simp_tac (esimps [der_def, derLP_def, derRP_def, IsDerivableR_def]) 1), Safe_tac, (eres_inst_tac [("x", "Der ($X |- $Y) cutr [dtr, dtra]")] allE 1), (etac impE 1), (etac ex_match 2), Asm_simp_tac 2, (rtac ([noCut_equiv, conj_commute] MRS trans RS iffD1 RS conjunct1) 2), (Fast_tac 2), (asm_simp_tac (HOL_ss addsimps (thms "allNextDTs.simps" @ thms "premsDT_premsDTs.simps" @ thms "allDT_allDTs.simps")) 1), (fast_tac (claset () addSIs [noCut_equiv RS iffD2 RS conjunct1, frb_cut, conjI RS (exI RS (cut_wfb RS iffD2)), cutIsLP_I, cutIsRP_I, cutOnFmls_I] addSEs [Diff_subset RSN (2,allfrb_mono)]) 1)] ; val tacs2 = [ (case_tac "dt" 1), hyp_subst_tac 2, Full_simp_tac 2, (case_tac "x = cutr" 1), (res_inst_tac [("x", "dt")] exI 2), (fast_tac (claset () addSEs [allDT_Next'] addSss (simpset ())) 2), (case_tac "seq" 1), hyp_subst_tac 1] ; val tacs3 = [ (rtac refl 1), (REPEAT (etac allE 1)), (eatac impE 1 1), (rotate_tac ~1 1), (REPEAT (chop_tac 1 (etac thin_rl 1))), (full_simp_tac (esimps [der_def, IsDerivableR_def]) 1), (etac ex_match 1), Asm_simp_tac 1, Safe_tac, (etac allfrb_mono 2), Fast_tac 2, (dtac (allPremsNil RS iffD2) 1), (etac allDT_and_mono 1), (chop_tac 1 (atac 1)), (case_tac "s" 1), hyp_subst_tac 1, (etac frbNoCut 1), Fast_tac 1, Asm_full_simp_tac 1] ; in val cELP = prove_goalw Belnap.thy [canElim_def, valid_def] "cutr : rules --> (ALL M. canElim rules (cutIsLP M) = (ALL X Y. \ \ derLP rules ($X |- M) & der rules (M |- $Y) --> der rules ($X |- $Y)))" (fn _ => [Safe_tac, EVERY tacs1, EVERY tacs2, (datac lem1 3 1), EVERY tacs3]) RS mp ; val cEder = prove_goalw Belnap.thy [canElim_def, valid_def] "cutr : rules --> (ALL M. canElim rules (cutOnFmls {M}) = (ALL X Y. \ \ der rules ($X |- M) & der rules (M |- $Y) --> der rules ($X |- $Y)))" (fn _ => [Safe_tac, EVERY tacs1, EVERY tacs2, (datac lem2 3 1), EVERY tacs3]) RS mp ; val cELRP = prove_goalw Belnap.thy [cutIsLRP_def, canElim_def, valid_def] "cutr : rules --> (ALL M. canElim rules (cutIsLRP M) = (ALL X Y. \ \ derLP rules ($X |- M) & derRP rules (M |- $Y) --> der rules ($X |- $Y)))" (fn _ => [Safe_tac, EVERY tacs1, EVERY tacs2, (datac lem1LR 4 1), EVERY tacs3]) RS mp ; end ; (* stage3 - (H3a) is derLP ($X |- M) (H3b) is derRP (M |- $Y) (concl) is der ($X |- $Y) so, by cELRP, (H3a) & (H3b) --> concl is canElim (cutIsLRP M) ; (H3c) is (ALL M'. (M', M) : psubfml --> (ALL X Y. der ($X |- M) & der (M |- $Y) --> der ($X |- $Y))), or, by cEder, (ALL M'. (M', M) : psubfml --> canElim (cutOnFmls {M'})) *) val stage3 = prove_goalw GElim.thy [psubfml_def] "C8 rules --> \ \ (ALL M'. (M', M) : psubfml --> canElim rules (cutOnFmls {M'})) --> \ \ canElim rules (cutIsLRP M)" (fn _ => [ (strip_tac 1), (etac allch 1), (rtac elimFmls 1), (asm_simp_tac (esimps [child_fmls_def]) 1), (rtac allElim 1), Force_tac 1]) RS mp ; val stage3' = prove_goal Belnap.thy "cutr : rules --> C8 rules --> ?P" (fn _ => [ Safe_tac, (dtac stage3 1), (safe_asm_full_simp_tac (esimps [cEder, cELRP]) 1), (etac thin_rl 1), atac 1]) RS mp RS mp RS mp ; (** Belnap's proof using stages 1, 2, 3, as on top of pg 394 **) (* Note: see Belnap's proof, in which he derives step 12 from steps 2-11. Steps 2-11 give (ALL X Y. step 2 & step 3 --> step 11), so he is saying that "(ER) admissible for M" (step 12) is the same as (ALL X Y. der ($X |- ?M) & der (?M |- $Y) --> der ($X |- $Y)), which, by cEder, is equivalent to canElim (cutOnFmls {?M}) *) val th146 = simplify (esimps [cELRP]) (transfer Belnap.thy stage3) ; (* 1 & 4 & 5 --> 6 *) val th13 = meta_std (prove_goal GElim.thy (* (1 --> 12) --> 13 *) "(ALL M'. (ALL M''. (M'', M') : psubfml --> \ \ canElim rules (cutOnFmls {M''})) --> \ \ canElim rules (cutOnFmls {M'})) --> \ \ (ALL M. canElim rules (cutOnFmls {M}))" (fn _ => [ (rtac (wf_def RS meta_eq_to_obj_eq RS iffD1 RS spec) 1), (simp_tac (esimps [psubfml_def]) 1), (rtac wf_trancl 1), (rtac wf_ipsubfml 1)])) ; val fitch = meta_std (prove_goal Belnap.thy "cutr : rules --> C8 rules --> \ \ (ALL M'. stage1 rules M') & (ALL M'. stage2 rules M') --> \ \ canElim rules (cutOnFmls {M})" (fn _ => [ Safe_tac, rtac th13 1, Safe_tac, (asm_simp_tac (esimps [cEder]) 1), (* goal is 12 *) Safe_tac, (* goal is 11 *) (rewtac stage1_def), (etac allE 1), (REPEAT (chop_tac 2 (etac allE 1))), (etac mp 1), Safe_tac, atac 1, (* goal is 9 *) (rewtac stage2_def), (etac allE 1), (REPEAT (chop_tac 1 (etac allE 1))), (etac mp 1), Safe_tac, atac 1, atac 2, (* goal is 7 *) (dtac stage3 1), mp_tac 1, (asm_full_simp_tac (esimps [cELRP]) 1)])) ; (** alternatives to stage1 and stage2 **) (* for some reason parser won't accept (M |- M) *) fun tacf _ = ([ (rtac impI 1), (res_inst_tac [("x", "Der (Sequent (Structform M) (Structform M)) idf []")] exI 1), (asm_full_simp_tac (esimps [idf, cut]) 1), (rtac rulefs_find 1), (simp_tac (esimps [Rule_def]) 1), (rtac fFind_match 1)]) ; val derLPid = prove_goalw Belnap.thy [derLP_def] "idf : rules --> derLP rules (Sequent (Structform M) (Structform M))" tacf RS mp ; val derRPid = prove_goalw Belnap.thy [derRP_def] "idf : rules --> derRP rules (Sequent (Structform M) (Structform M))" tacf RS mp ; fun tac'' _ = [ strip_tac 1, (REPEAT (etac conjE 1)), (chop_tac 1 (ftac spec 1)), (dresolve_tac ([derLPid, derRPid] RLN (2, [mp])) 1), atac 1, Fast_tac 1] ; val stg1'' = prove_goalw Belnap.thy [stage1_def, stage1''_def] "idf : rules --> stage1'' rules M --> stage1 rules M" tac'' RS mp RS mp ; val stg1r = prove_goalw Belnap.thy [stage1_def, stage1''_def] "stage1 rules M --> stage1'' rules M" (fn _ => [Fast_tac 1]) RS mp ; val stg1eq = prove_goal Belnap.thy "idf : rules --> stage1'' rules M = stage1 rules M" (fn _ => [ Safe_tac, (eatac stg1'' 1 1), (etac stg1r 1)]) RS mp ; val stg2'' = prove_goalw Belnap.thy [stage2_def, stage2''_def] "idf : rules --> stage2'' rules M --> stage2 rules M" tac'' RS mp RS mp ; (* note - although stg2'' holds, "stage2' M --> stage2 M" does not *) val stg2r = prove_goalw Belnap.thy [stage2_def, stage2''_def] "stage2 rules M --> stage2'' rules M" (fn _ => [Fast_tac 1]) RS mp ; val stg2eq = prove_goal Belnap.thy "idf : rules --> stage2'' rules M = stage2 rules M" (fn _ => [ Safe_tac, (eatac stg2'' 1 1), (etac stg2r 1)]) RS mp ; val () = qed_goalw_spec_mp "cEst1'" Belnap.thy [stage1'_def] "cutr : rules --> \ \ (canElim rules (cutIsLP M) --> canElim rules (cutOnFmls {M})) = \ \ stage1' rules M" (fn _ => [ (rtac impI 1), (ftac cELP 1), (dtac cEder 1), (Fast_tac 1)]) ; val () = qed_goalw_spec_mp "cEst2'" Belnap.thy [stage2'_def] "cutr : rules --> \ \ (canElim rules (cutIsLRP M) --> canElim rules (cutIsLP M)) \ \ = stage2' rules M" (fn _ => [ (rtac impI 1), (ftac cELP 1), (dtac cELRP 1), (Fast_tac 1)]) ; (* Belnap's stage 1 implies stage1', which is more similar to the result canElim (cutIsLP M) ==> canElim (cutOnFmls {M}) *) val stg1 = meta_std (prove_goalw Belnap.thy [stage1_def, stage1'_def] "cutr : rules --> stage1 rules M --> stage1' rules M" (fn _ => [ Fast_tac 1])) ; (* Belnap's stage 2 implies stage2', which is more similar to the result canElim (cutIsLRP M) ==> canElim (cutIsLP M) *) val stg2 = meta_std (prove_goalw Belnap.thy [stage2_def, stage2'_def] "cutr : rules --> stage2 rules M --> stage2' rules M" (fn _ => [ Fast_tac 1])) ; (* comments: our results makeCutLP, allLP, allLP' could be changed to refer solely to cuts whose conclusion has a fixed succedent $Y, and then these would give the result equivalent to stage1'' ?M instead of stage1' ?M ; however we still would have to do the transition from canElimAll to canElim; this step is incorporated in Belnap's proof of stage1 *)