(* Belnap.ML *) val gb = goal Belnap.thy ; val gwb = goalw Belnap.thy ; val thC8Es'' = map (fn th => elimFmls RS th) thC8Es' ; val () = qed_goalw "frb_cut" Belnap.thy [rls] "frb rls (Der seq cutr dtl)" (fn _ => [simp_tac (esimps [ruleInOrInv_def]) 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 () addSEs [noPremsI] 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 rls) dt & dt = Der ($X |- $Y) cutr dtl --> \ \ derLP ($X |- M) & der (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 rls) dt & dt = Der ($X |- $Y) cutr dtl --> \ \ der ($X |- M) & derRP (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 rls) dt & dt = Der ($X |- $Y) cutr dtl --> \ \ derLP ($X |- M) & derRP (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 rls) dt & dt = Der ($X |- $Y) cutr dtl --> \ \ der ($X |- M) & der (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) 2), (Fast_tac 2), (asm_simp_tac (HOL_ss addsimps (thms "allNextDTs.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 = [ (exhaust_tac "dt" 1), hyp_subst_tac 2, Full_simp_tac 2, (case_tac "rule = cutr" 1), (res_inst_tac [("x", "dt")] exI 2), (fast_tac (claset () addSEs [allDT_Next'] addSss (simpset ())) 2), (exhaust_tac "sequent" 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)), (exhaust_tac "dt" 1), hyp_subst_tac 1, (etac frbNoCut 1), Fast_tac 1, Asm_full_simp_tac 1] ; in val () = qed_goalw "cELP" Belnap.thy [canElim_def] "canElim (cutIsLP M) = \ \ (ALL X Y. derLP ($X |- M) & der (M |- $Y) --> der ($X |- $Y))" (fn _ => [Safe_tac, EVERY tacs1, EVERY tacs2, (datac lem1 3 1), EVERY tacs3]) ; val () = qed_goalw "cEder" Belnap.thy [canElim_def] "canElim (cutOnFmls {M}) = \ \ (ALL X Y. der ($X |- M) & der (M |- $Y) --> der ($X |- $Y))" (fn _ => [Safe_tac, EVERY tacs1, EVERY tacs2, (datac lem2 3 1), EVERY tacs3]) ; val () = qed_goalw "cELRP" Belnap.thy [cutIsLRP_def, canElim_def] "canElim (cutIsLRP M) = \ \ (ALL X Y. derLP ($X |- M) & derRP (M |- $Y) --> der ($X |- $Y))" (fn _ => [Safe_tac, EVERY tacs1, EVERY tacs2, (datac lem1LR 4 1), EVERY tacs3]) ; 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 Belnap.thy [psubfml_def] "(ALL M'. (M', M) : psubfml --> canElim (cutOnFmls {M'})) --> \ \ canElim (cutIsLRP M)" (fn _ => [ (rtac impI 1), (exhaust_tac "M" 1), ALLGOALS (EVERY' [hyp_subst_tac, resolve_tac thC8Es'', TRY o resolve_tac [twoElim, trivElim] THEN_ALL_NEW fast_tac (claset () addSIs (r_into_trancl :: ipsubfml.intrs))])]) RS mp ; val stage3' = full_simplify (HOL_ss addsimps [cEder, cELRP]) stage3 ; val () = qed_goalw "wf_ipsubfml" Belnap.thy [wf_def] "wf ipsubfml" (fn _ => [ Safe_tac, rtac formula.induct 1, (ALLGOALS (EVERY' [etac allE, etac mp, strip_tac, etac ipsubfml.elim THEN_ALL_NEW Full_simp_tac])), (ALLGOALS Fast_tac)]) ; (** 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]) stage3 ; (* 1 & 4 & 5 --> 6 *) val th13 = meta_std (prove_goal Belnap.thy (* (1 --> 12) --> 13 *) "(ALL M'. (ALL M''. (M'', M') : psubfml --> canElim (cutOnFmls {M''})) --> \ \ canElim (cutOnFmls {M'})) --> (ALL M. canElim (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 "(ALL M'. stage1 M') & (ALL M'. stage2 M') --> canElim (cutOnFmls {M})" (fn _ => [ Safe_tac, rtac th13 1, Safe_tac, (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 th146 1), Fast_tac 1])) ; (** alternatives to stage1 and stage2 **) fun tacf _ = ([ (res_inst_tac [("x", "Der (M |- M) idf []")] exI 1), (simp_tac (esimps [ruleInOrInv_def, rls, idf, cut, ruleMatches_def]) 1), (res_inst_tac [("x", "Rule [] (M |- M)")] exI 1), (Simp_tac 1), (rtac exI 1), (rtac fFind_match 1)]) ; val derLPid = prove_goalw Belnap.thy [derLP_def] "derLP (M |- M)" tacf ; val derRPid = prove_goalw Belnap.thy [derRP_def] "derRP (M |- M)" tacf ; fun tac'' _ = [ strip_tac 1, (REPEAT (etac conjE 1)), (chop_tac 1 (ftac spec 1)), (dresolve_tac ([derLPid, derRPid] RLN (2, [mp])) 1), Fast_tac 1] ; fun tac' _ = [ strip_tac 1, (REPEAT (etac conjE 1)), (ftac spec 1), (dresolve_tac ([derLPid, derRPid] RLN (2, [mp])) 1), Fast_tac 1] ; val stg1'' = prove_goalw Belnap.thy [stage1_def, stage1''_def] "stage1'' M --> stage1 M" tac'' RS mp ; val stg1r = prove_goalw Belnap.thy [stage1_def, stage1''_def] "stage1 M --> stage1'' M" (fn _ => [Fast_tac 1]) RS mp ; val stg1eq = tacthm (etac stg1r 1 THEN etac stg1'' 1) iffI ; val stg2'' = prove_goalw Belnap.thy [stage2_def, stage2''_def] "stage2'' M --> stage2 M" tac'' RS mp ; (* note - although stg2'' holds, "stage2' M --> stage2 M" does not *) val stg2r = prove_goalw Belnap.thy [stage2_def, stage2''_def] "stage2 M --> stage2'' M" (fn _ => [Fast_tac 1]) RS mp ; val stg2eq = tacthm (etac stg2r 1 THEN etac stg2'' 1) iffI ; val () = qed_goalw "cEst1'" Belnap.thy (stage1'_def :: (map mk_eq [cELP, cEder])) "(canElim (cutIsLP M) --> canElim (cutOnFmls {M})) = stage1' M" (fn _ => [rtac refl 1]) ; val () = qed_goalw "cEst2'" Belnap.thy (stage2'_def :: (map mk_eq [cELP, cELRP])) "(canElim (cutIsLRP M) --> canElim (cutIsLP M)) = stage2' M" (fn _ => [rtac refl 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] "stage1 M --> stage1' 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] "stage2 M --> stage2' 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 *)