(* link between category semantics and deep nested system *) (* have shown that things provable in deep nested system are provable in shallow nested system and vice versa (sn_dn_equiv) and that that things provable in shallow nested system are provable in display calculus, and vv, (dc_sn_equiv, tr_der_snb_dc, tr_der_dc_snb) and that things provable in display calculus are valid in the categorical semantics, and vv, (dc_cat_equiv) This last uses the calculi containing cut, but we also have cut-admissibility for the display calculus (biill_cut); thus we don't need to show that the rules of the deep nested system are valid in the category, except that we _do_ want to show this for the subsystems for FILL only, not all of BiILL *) fun solve_ipsf_rtc sg st = (rtac rtrancl_refl ORELSE' EVERY' [rtac tct.rsr, resolve_tac ipsubfml.intrs o incr, solve_ipsf_rtc]) sg st ; val imp_forwardp = tacthm (atac 3) imp_forward2 ; val excl_ex_fwd_rt_tacs = [ etac ex_forward, etac conj_forward, atac o incr, etac tct.rrr, solve_ipsf_rtc] ; val excl_ex_rt_tacs = [rtac exI, rtac conjI, atac o incr, etac tct.rrr, solve_ipsf_rtc] ; (* Lemma 25, hollow nested sequents *) val dff = derl_trans_prems [dor_idRI, dor_mono] dfcut ; val dtt = derl_trans_prems_rev [dand_idRD, dand_mono] dfcut ; val dtf = derl_trans_prems [dlolli_idI, dlolli_mono] dfcut ; val dft = derl_trans_prems_rev [dexcl_idD, dexcl_mono] dfcut ; val dttr = derl_trans_prems [dand_idRI, dand_mono] dfcut ; val dffr = derl_trans_prems_rev [dor_idRD, dor_mono] dfcut ; val dtfr = derl_trans_prems_rev [dlolli_idD, dlolli_mono] dfcut ; val dftr = derl_trans_prems [dexcl_idI, dexcl_mono] dfcut ; val _ = qed_goal_spec_mp "biill_hollows_rev" N_Cat.thy "V : hollows --> (ntau True V |- F) : derrec (rulefs biill_cat_rules) ps & \ \ (T |- ntau False V) : derrec (rulefs biill_cat_rules) ps" (fn _ => [ (rtac impI 1), (etac hollows.induct 1), Safe_tac, ALLGOALS Clarsimp_tac, TRYALL (rtac der_idf), (TRYALL (rtac derl_derrec_trans THEN' resolve_tac [dftr, dtfr, dttr, dffr])), (TRYALL (resolve_tac singleton_sub_bcr_thms)), (TRYALL Force_tac) ]) ; val [biill_hollows_revT, biill_hollows_revF] = msc biill_hollows_rev ; (* could also do the same as biill_hollows_rev for fill *) val _ = qed_goal_spec_mp "biill_hollows_der" N_Cat.thy "V : hollows --> (F |- ntau True V) : derrec (rulefs biill_cat_rules) ps & \ \ (ntau False V |- T) : derrec (rulefs biill_cat_rules) ps" (fn _ => [ (rtac impI 1), (etac hollows.induct 1), Safe_tac, ALLGOALS Clarsimp_tac, TRYALL (rtac der_idf), (TRYALL (rtac derl_derrec_trans THEN' resolve_tac [dft, dtf, dtt, dff])), (TRYALL (resolve_tac singleton_sub_bcr_thms)), (TRYALL Force_tac) ]) ; val [biill_hollows_derT, biill_hollows_derF] = msc biill_hollows_der ; val _ = qed_goal_spec_mp "fill_hollows_der" N_Cat.thy "V : hollows --> (no_excl_sf (ntau True V) --> \ \ (F |- ntau True V) : derrec (rulefs fill_cat_rules) ps) & \ \ (no_excl_sf (ntau False V) --> \ \ (ntau False V |- T) : derrec (rulefs fill_cat_rules) ps)" (fn _ => [ (rtac impI 1), (etac hollows.induct 1), (TRYALL (rtac conjI)), ALLGOALS Clarsimp_tac, TRYALL (rtac der_idf), (TRYALL (rtac derl_derrec_trans THEN' resolve_tac [dft, dtf, dtt, dff])), (TRYALL (resolve_tac singleton_sub_fcr_thms)), ALLGOALS Clarsimp_tac ]) ; val [fill_hollows_derT, fill_hollows_derF] = map zero_var_indexes (msc fill_hollows_der) ; (* Lemma 26, merged sequents *) val dme = derl_trans_prems_rev [and_excls, dexcl_mono] dfcut ; val dml = derl_trans_prems [or_lollis, dlolli_mono] dfcut ; val dmo = derl_trans_prems_rev [dor_mono, dor_4] dfcut ; val dma = derl_trans_prems [dand_mono, dand_4] dfcut ; val dxl = derl_trans_prems [and_lollis, dlolli_mono] dfcut ; val dxl' = derl_trans_prems [and_lollis_or, dlolli_mono] dfcut ; val dxe = derl_trans_prems_rev [or_excls, dexcl_mono] dfcut ; val dxe' = derl_trans_prems_rev [or_excls_and, dexcl_mono] dfcut ; val dxo = derl_trans_prems [dwk_dist2, dor_mono] dfcut ; val dxo' = derl_trans_prems [dwk_dist2_alt, dor_mono] dfcut ; val dxa = derl_trans_prems_rev [dwk_dist2s, dand_mono] dfcut ; val dxa' = derl_trans_prems_rev [dwk_dist2s_alt, dand_mono] dfcut ; val _ = qed_goal_spec_mp "biill_rmerge_der" N_Cat.thy "(Ta, Tb, Tc) : rmerge --> \ \ (ntau True Ta +++ ntau True Tb |- ntau True Tc) : \ \ derrec (rulefs biill_cat_rules) prems & \ \ (ntau False Tc |- ntau False Ta &&& ntau False Tb) : \ \ derrec (rulefs biill_cat_rules) prems" (fn _ => [ rtac impI 1, etac rmerge.induct 1, (TRYALL (rtac conjI)), ALLGOALS Clarsimp_tac, (TRYALL (resolve_tac der_ids)), (TRYALL (rtac derl_derrec_trans THEN' resolve_tac [dme, dml, dma, dmo])), (TRYALL (resolve_tac singleton_sub_bcr_thms)), TRYALL Force_tac ]) ; val [biill_rmerge_derT, biill_rmerge_derF] = msc biill_rmerge_der ; val conj_forward2s = tacthm (atac 3) conj_forward ; val subtacs = [ hyp_subst_tac, mp_tac, etac ex_forward, etac conj_forward2s, etac tct.rsr, resolve_tac ipsubfml.intrs ] ; val _ = qed_goalw_spec_mp "rmerge_subfml" N_Cat.thy [mk_eq all_bool_eq] "(Ta, Tb, Tc) : rmerge --> P : excl_fmls --> \ \ (ALL b. (P, ntau b Ta) : ipsubfml^* | (P, ntau b Tb) : ipsubfml^* --> \ \ (EX Q. (Q, ntau b Tc) : ipsubfml^* & Q : excl_fmls))" (fn _ => [ (rtac impI 1), (etac rmerge.induct 1), (safe_tac csp), ALLGOALS Clarsimp_tac, (TRYALL (EVERY' [rtac exI, eatac conjI 1])), (TRYALL (EVERY' [ (etac rtranclE), (etac excl_fmls.elim), (MSSG Clarsimp_tac), (eresolve_tac ipsubfml_0_cases) ])), TRYALL atac, (REPEAT1 (LASTGOAL (EVERY' [rtac exI, rtac conjI, rtac rtrancl_refl, rtac excl_fmls.I ]))), (TRYALL (EVERY' [etac rtranclE, etac excl_fmls.elim, MSSG Clarsimp_tac, (eresolve_tac ipsubfml_2_cases), EVERY' subtacs, EVERY' subtacs ])) ]) ; val _ = qed_goal_spec_mp "fill_rmerge_der" N_Cat.thy "(Ta, Tb, Tc) : rmerge --> (no_excl_sf (ntau True Tc) --> \ \ (ntau True Ta +++ ntau True Tb |- ntau True Tc) : \ \ derrec (rulefs fill_cat_rules) prems) & \ \ (no_excl_sf (ntau False Tc) --> \ \ (ntau False Tc |- ntau False Ta &&& ntau False Tb) : \ \ derrec (rulefs fill_cat_rules) prems)" (fn _ => [ rtac impI 1, etac rmerge.induct 1, (TRYALL (rtac conjI)), ALLGOALS Clarsimp_tac, (TRYALL (resolve_tac der_ids)), (TRYALL (resolve_tac singleton_sub_fcr_thms)), (TRYALL (rtac derl_derrec_trans THEN' resolve_tac [dme, dml, dma, dmo])), (TRYALL (resolve_tac singleton_sub_fcr_thms)), (ALLGOALS Clarsimp_tac) ]) ; val [fill_rmerge_derT, fill_rmerge_derF] = map zero_var_indexes (msc fill_rmerge_der) ; (* following two - thought these what we want for Lemma 27, but not so *) val _ = qed_goal_spec_mp "biill_rmerge1_der" N_Cat.thy "(Ta, Tb, Tc) : rmerge1 (A, B, C) --> \ \ prems = {(ntau True A +++ ntau True B |- ntau True C), \ \ (ntau False C |- ntau False A &&& ntau False B)} --> \ \ (ntau True Ta +++ ntau True Tb |- ntau True Tc) : \ \ derrec (rulefs biill_cat_rules) prems & \ \ (ntau False Tc |- ntau False Ta &&& ntau False Tb) : \ \ derrec (rulefs biill_cat_rules) prems" (fn _ => [ rtac impI 1, rtac impI 1, etac rmerge1_induct 1, ALLGOALS Clarsimp_tac, (TRYALL (rtac conjI)), (TRYALL (rtac drs.dpI THEN' solve_in)), (TRYALL (rtac derl_derrec_trans THEN' resolve_tac [dme, dml, dma, dmo])), (TRYALL (resolve_tac singleton_sub_bcr_thms)), (ALLGOALS Clarsimp_tac), (TRYALL (eresolve_tac [biill_rmerge_derT, biill_rmerge_derF])) ]) ; val [biill_rmerge1_derT, biill_rmerge1_derF] = msc biill_rmerge1_der ; val _ = qed_goal_spec_mp "fill_rmerge1_der" N_Cat.thy "(Ta, Tb, Tc) : rmerge1 (A, B, C) --> \ \ prems = {(ntau True A +++ ntau True B |- ntau True C), \ \ (ntau False C |- ntau False A &&& ntau False B)} --> \ \ (no_excl_sf (ntau True Tc) --> \ \ (ntau True Ta +++ ntau True Tb |- ntau True Tc) : \ \ derrec (rulefs fill_cat_rules) prems) & \ \ (no_excl_sf (ntau False Tc) --> \ \ (ntau False Tc |- ntau False Ta &&& ntau False Tb) : \ \ derrec (rulefs fill_cat_rules) prems)" (fn _ => [ rtac impI 1, rtac impI 1, etac rmerge1_induct 1, ALLGOALS Clarsimp_tac, (TRYALL (rtac conjI)), ALLGOALS Clarify_tac, (TRYALL (rtac drs.dpI THEN' solve_in)), (TRYALL (rtac derl_derrec_trans THEN' resolve_tac [dme, dml, dma, dmo])), (TRYALL (resolve_tac singleton_sub_fcr_thms)), (ALLGOALS Clarsimp_tac), (TRYALL (eresolve_tac [fill_rmerge_derT, fill_rmerge_derF])), TRYALL atac]) ; val [fill_rmerge1_derT, fill_rmerge1_derF] = msc fill_rmerge1_der ; (* inductive portion of Lemma 27 *) val _ = qed_goal_spec_mp "biill_rmerge1_der_alt" N_Cat.thy "(Ta, Tb, Tc) : rmerge1 (A, B, C) --> \ \ prems = {(ntau True A &&& ntau True B |- ntau True C), \ \ (ntau False C |- ntau False A +++ ntau False B)} --> \ \ (ntau True Ta &&& ntau True Tb |- ntau True Tc) : \ \ derrec (rulefs biill_cat_rules) prems & \ \ (ntau False Tc |- ntau False Ta +++ ntau False Tb) : \ \ derrec (rulefs biill_cat_rules) prems" (fn _ => [ rtac impI 1, rtac impI 1, etac rmerge1_induct 1, ALLGOALS Clarsimp_tac, (TRYALL (rtac conjI)), (TRYALL (rtac drs.dpI THEN' solve_in)), (rtac derl_derrec_trans 8), (rtac dxe 8), (rtac derl_derrec_trans 7), (rtac dxl' 7), (rtac derl_derrec_trans 6), (rtac dxe' 6), (rtac derl_derrec_trans 5), (rtac dxl 5), (rtac derl_derrec_trans 4), (rtac dxa' 4), (rtac derl_derrec_trans 3), (rtac dxo 3), (rtac derl_derrec_trans 2), (rtac dxa 2), (rtac derl_derrec_trans 1), (rtac dxo' 1), (TRYALL (resolve_tac singleton_sub_bcr_thms)), (ALLGOALS Clarsimp_tac), (TRYALL (rtac conjI)), (TRYALL (eresolve_tac [mp, biill_rmerge_derT, biill_rmerge_derF])) ]) ; val [biill_rmerge1_der_altT, biill_rmerge1_der_altF] = msc biill_rmerge1_der_alt ; val _ = qed_goal_spec_mp "fill_rmerge1_der_alt" N_Cat.thy "(Ta, Tb, Tc) : rmerge1 (A, B, C) --> \ \ prems = {(ntau True A &&& ntau True B |- ntau True C), \ \ (ntau False C |- ntau False A +++ ntau False B)} --> \ \ (no_excl_sf (ntau True Tc) --> \ \ (ntau True Ta &&& ntau True Tb |- ntau True Tc) : \ \ derrec (rulefs fill_cat_rules) prems) & \ \ (no_excl_sf (ntau False Tc) --> \ \ (ntau False Tc |- ntau False Ta +++ ntau False Tb) : \ \ derrec (rulefs fill_cat_rules) prems)" (fn _ => [ rtac impI 1, rtac impI 1, etac rmerge1_induct 1, ALLGOALS Clarsimp_tac, (TRYALL (rtac conjI)), ALLGOALS Clarify_tac, (TRYALL (rtac drs.dpI THEN' solve_in)), (rtac derl_derrec_trans 6), (rtac dxl' 6), (rtac derl_derrec_trans 5), (rtac dxl 5), (rtac derl_derrec_trans 4), (rtac dxa' 4), (rtac derl_derrec_trans 3), (rtac dxo 3), (rtac derl_derrec_trans 2), (rtac dxa 2), (rtac derl_derrec_trans 1), (rtac dxo' 1), (TRYALL (resolve_tac singleton_sub_fcr_thms)), (ALLGOALS Clarsimp_tac), (TRYALL (eresolve_tac [fill_rmerge_derT, fill_rmerge_derF])), (TRYALL atac) ]) ; val [fill_rmerge1_der_altT, fill_rmerge1_der_altF] = msc fill_rmerge1_der_alt ; val _ = qed_goal_spec_mp "TF_nes" N_Cat.thy "~ no_excl_sf (ntau True C) --> ~ no_excl_sf (ntau False C)" (fn _ => [ (induct_tac "C" 1), ALLGOALS Clarsimp_tac ]) ; val _ = qed_goal_spec_mp "TF_excl" N_Cat.thy "(W, ntau True C) : ipsubfml^* --> W : excl_fmls --> \ \ (EX U. (U, ntau False C) : ipsubfml^* & U : excl_fmls)" (fn _ => [ (induct_tac "C" 1), ALLGOALS Clarsimp_tac, Fast_tac 4, (TRYALL (etac rtranclE)), (TRYALL (MSSG (clarsimp_tac (ces (excl_fmls.elim :: ipsubfml_0_cases), esimps [])))), (TRYALL (eresolve_tac ipsubfml_2_cases)), ALLGOALS Clarify_tac, (TRYALL (EVERY' [rtac exI, etac rev_conjI, etac tct.rsr, resolve_tac ipsubfml.intrs ])) ]) ; val _ = qed_goal_spec_mp "rmerge1_excl_lemF" N_Cat.thy "(a, b, c) : rmerge1 (A, B, C) --> ~ no_excl_sf (ntau False C) --> \ \ ~ no_excl_sf (ntau False c)" (fn _ => [ strip_tac 1, etac rmerge1_induct 1, ALLGOALS Clarsimp_tac ]) ; val _ = qed_goal_spec_mp "rmerge1_excl_lemT" N_Cat.thy "(a, b, c) : rmerge1 (A, B, C) --> ~ no_excl_sf (ntau True C) --> \ \ ~ no_excl_sf (ntau True c)" (fn _ => [ strip_tac 1, etac rmerge1_induct 1, ALLGOALS Clarsimp_tac, (dtac TF_nes 1 THEN contr_tac 1) ]) ; (* lines involving exclusions are a complicated way of saying that Tc already contains a => (or a --< in which case the theorem is vacuous) *) val _ = qed_goal_spec_mp "fill_rmerge1_der_nseq" N_Cat.thy "(Ta, Tb, Tc) : rmerge1 (A, B, C) --> \ \ prems = {ntau True A &&& ntau True B |- ntau True C} --> \ \ ~ no_excl_sf (ntau False C) --> no_excl_sf (ntau True Tc) --> \ \ (ntau True Ta &&& ntau True Tb |- ntau True Tc) : \ \ derrec (rulefs fill_cat_rules) prems" (fn _ => [ rtac impI 1, rtac impI 1, etac rmerge1_induct 1, ALLGOALS Clarsimp_tac, (TRYALL (rtac conjI)), (TRYALL (rtac drs.dpI THEN' solve_in)), (* subgoal 4 - not in fill *) (datac rmerge1_excl_lemF 1 4), Clarify_tac 4, (rtac derl_derrec_trans 3), (rtac dxl 3), (rtac derl_derrec_trans 2), (rtac dxo 2), (rtac derl_derrec_trans 1), (rtac dxo' 1), (TRYALL (resolve_tac singleton_sub_fcr_thms)), (ALLGOALS Clarsimp_tac), (TRYALL (eresolve_tac [fill_rmerge_derT, fill_rmerge_derF])), TRYALL atac ]) ; val _ = qed_goal_spec_mp "dn_ands_fcr" N_Cat.thy "(A, B, C) : dn_ands --> \ \ no_excl_sf (ntau True C) --> \ \ (ntau True A &&& ntau True B |- ntau True C) : \ \ derrec (rulefs fill_cat_rules) {}" (fn _ => [ (safe_tac (ces dn_ands.elims)), ALLGOALS Clarsimp_tac, (rtac derl_derrec_trans 1), (rtac dxl 1), (TRYALL (resolve_tac singleton_sub_fcr_thms)), Clarsimp_tac 1, rtac conjI 1, (etac fill_rmerge_derF 1), (rtac derl_derrec_trans 2), (rtac dxo 2), (TRYALL (resolve_tac singleton_sub_fcr_thms)), Clarsimp_tac 2, rtac conjI 2, (etac fill_rmerge_derT 3), rtac der_idf 2, (resolve_tac singleton_sub_fcr_thms 2), TRYALL atac ]) ; val _ = qed_goal_spec_mp "dn_ora_fcr" N_Cat.thy "(A, B, C) : dn_ora --> \ \ no_excl_sf (ntau True C) --> \ \ (ntau True A &&& ntau True B |- ntau True C) : \ \ derrec (rulefs fill_cat_rules) {}" (fn _ => [ (safe_tac (ces dn_ora.elims)), ALLGOALS Clarsimp_tac, (rtac derl_derrec_trans 1), (rtac dxl' 1), (TRYALL (resolve_tac singleton_sub_fcr_thms)), Clarsimp_tac 1, rtac conjI 1, (etac fill_rmerge_derT 2), (rtac derl_derrec_trans 1), (rtac dxa 1), (TRYALL (resolve_tac singleton_sub_fcr_thms)), Clarsimp_tac 1, rtac conjI 1, (etac fill_rmerge_derF 1), rtac der_idf 2, (resolve_tac singleton_sub_fcr_thms 2), TRYALL atac ]) ; val dlh1 = tdfc [tni [dlolli_export, dand_monoR], drl.asmI, dlolli_import] ; val dlh2 = tdfc [dand_assocR, tni [dlolli_trans, dand_monoR], dand_comm, dwk_dist, tni [dlolliD, dor_monoL], dor_comm, drl.asmI] ; val dlh3 = tni [dlh2, and_to_lolli] ; val _ = qed_goal_spec_mp "dn_lollia_fcr" N_Cat.thy "(A, B, C) : dn_lollia --> \ \ no_excl_sf (ntau True C) --> \ \ (ntau True A &&& ntau True B |- ntau True C) : \ \ derrec (rulefs fill_cat_rules) {}" (fn _ => [ (safe_tac (ces dn_lollia.elims)), ALLGOALS Clarsimp_tac, (rtac derl_derrec_trans 1), (rtac dlh1 1), (TRYALL (resolve_tac singleton_sub_fcr_thms)), Clarsimp_tac 1, (rtac derl_derrec_trans 1), (rtac dxl 1), (TRYALL (resolve_tac singleton_sub_fcr_thms)), Clarsimp_tac 1, rtac conjI 1, (etac fill_rmerge_derF 1), (rtac derl_derrec_trans 2), (rtac dlh3 2), (TRYALL (resolve_tac singleton_sub_fcr_thms)), Clarsimp_tac 2, (etac fill_rmerge_derT 2), TRYALL atac ]) ; (* inductive part of Lemma 27 (all parts) *) val l27i = [singleton_subsetI, refl RSN (2, fill_rmerge1_der_nseq)] MRS derrec_trans ; val dn_fcrs = [dn_ands_fcr, dn_ora_fcr, dn_lollia_fcr] ; val dn_fcrs_ths' = dn_fcrs RL [l27i] ; fun mkpp th = tacsthm [rtac th 2, atac 3, etac thin_rl 2] contrapos_pp ; fun mkpp th = tacsthm [rtac th 2, LASTGOAL atac, TRYALL (etac thin_rl)] contrapos_pp ; (* to simplify all of these *) val dn_fcr_str = "(A, B, C) : ?dn_lr --> (Ta, Tb, Tc) : rmerge1 (A, B, C) --> \ \ no_excl_sf (ntau True Tc) --> \ \ (ntau True Ta &&& ntau True Tb |- ntau True Tc) : \ \ derrec (rulefs fill_cat_rules) {}" ; fun mk_dn_fcr_th dn_fcr_th' = prove_goal N_Cat.thy dn_fcr_str (fn _ => [ Clarify_tac 1, (rtac dn_fcr_th' 1), TRYALL atac, (eatac (mkpp rmerge1_excl_lemT) 1 1), (eresolve_tac [dn_ands.elim, dn_ora.elim, dn_lollia.elim] 1), Clarsimp_tac 1 ]) ; val _ = bind_thms ("lem27s", map (meta_std o mk_dn_fcr_th) dn_fcrs_ths') ; (* Lemma 24 *) val _ = qed_goal_spec_mp "biill_ctxt_cat'" N_Cat.thy "(XSs, XU) : ctxt {([S], U)} --> \ \ prems = {ntau True S |- ntau True U, ntau False U |- ntau False S} --> \ \ (ALL XS. XSs = [XS] --> \ \ (ntau True XS |- ntau True XU) : derrec (rulefs biill_cat_rules) prems & \ \ (ntau False XU |- ntau False XS) : derrec (rulefs biill_cat_rules) prems)" (fn _ => [ (rtac impI 1), (rtac impI 1), hyp_subst_tac 1, (etac pair_ctxt_induct 1), ALLGOALS Clarsimp_tac, (TRYALL (rtac conjI)), (fast_tac (cis [drs.sdp RS subsetD]) 1), (fast_tac (cis [drs.sdp RS subsetD]) 1), (TRYALL (rtac derl_derrec_trans THEN' resolve_tac cat_dmono1s)), (TRYALL (resolve_tac singleton_sub_bcr_thms)), ALLGOALS Clarsimp_tac ]) ; val biill_ctxt_cat = [asm_rl, refl, refl] MRS biill_ctxt_cat' ; val [biill_ctxt_catT, biill_ctxt_catF] = msc biill_ctxt_cat ; val _ = qed_goal_spec_mp "fill_ctxt_cat'" N_Cat.thy "(XSs, XU) : ctxt {([S], U)} --> \ \ prems = {ntau True S |- ntau True U, ntau False U |- ntau False S} --> \ \ (ALL XS. XSs = [XS] --> \ \ (no_excl_sf (ntau True XU) --> \ \ (ntau True XS |- ntau True XU) : derrec (rulefs fill_cat_rules) prems) & \ \ (no_excl_sf (ntau False XU) --> \ \ (ntau False XU |- ntau False XS) : derrec (rulefs fill_cat_rules) prems))" (fn _ => [ (rtac impI 1), (rtac impI 1), hyp_subst_tac 1, (etac pair_ctxt_induct 1), ALLGOALS Clarsimp_tac, (TRYALL (rtac conjI)), (fast_tac (cis [drs.sdp RS subsetD]) 1), (fast_tac (cis [drs.sdp RS subsetD]) 1), (ALLGOALS Clarify_tac), (TRYALL (rtac derl_derrec_trans THEN' resolve_tac cat_dmono1s)), (TRYALL (resolve_tac singleton_sub_fcr_thms)), ALLGOALS Clarsimp_tac ]) ; val fill_ctxt_cat = [asm_rl, refl, refl] MRS fill_ctxt_cat' ; val [fill_ctxt_catT, fill_ctxt_catF] = msc fill_ctxt_cat ; val _ = qed_goal_spec_mp "ctxt_excl_lemF'" N_Cat.thy "(XSs, XU) : ctxt {([S], U)} --> ~ no_excl_sf (ntau False U) --> \ \ (ALL XS. XSs = [XS] --> ~ no_excl_sf (ntau False XU))" (fn _ => [ (REPEAT (rtac impI 1)), (etac pair_ctxt_induct 1), ALLGOALS Clarsimp_tac ]) ; val _ = qed_goal_spec_mp "ctxt_excl_lemT'" N_Cat.thy "(XSs, XU) : ctxt {([S], U)} --> ~ no_excl_sf (ntau True U) --> \ \ (ALL XS. XSs = [XS] --> ~ no_excl_sf (ntau True XU))" (fn _ => [ (REPEAT (rtac impI 1)), (etac pair_ctxt_induct 1), ALLGOALS Clarsimp_tac, (dtac TF_nes 1 THEN contr_tac 1) ]) ; val ctxt_excl_lemF = [asm_rl, asm_rl, refl] MRS ctxt_excl_lemF' ; val ctxt_excl_lemT = [asm_rl, asm_rl, refl] MRS ctxt_excl_lemT' ; (* this is what we want for Lemma 24 (?), as conditions imply positive context *) val _ = qed_goal_spec_mp "fill_ctxt_cat_nseq'" N_Cat.thy "(XSs, XU) : ctxt {([S], U)} --> prems = {ntau True S |- ntau True U} --> \ \ ~ no_excl_sf (ntau False U) --> \ \ (ALL XS. XSs = [XS] --> no_excl_sf (ntau True XU) --> \ \ (ntau True XS |- ntau True XU) : derrec (rulefs fill_cat_rules) prems)" (fn _ => [ (REPEAT (rtac impI 1)), hyp_subst_tac 1, (etac pair_ctxt_induct 1), ALLGOALS Clarsimp_tac, (fast_tac (cis [drs.sdp RS subsetD]) 1), (datac ctxt_excl_lemF 1 4), Clarify_tac 4, (TRYALL (rtac derl_derrec_trans THEN' resolve_tac [dand_monoL, dand_monoR, dor_monoL, dor_monoR, dlolli_monoL, dlolli_monoR, dexcl_monoL, dexcl_monoR])), (TRYALL (resolve_tac singleton_sub_fcr_thms)), ALLGOALS Clarsimp_tac ]) ; val fill_ctxt_cat_nseq = [asm_rl, refl, asm_rl, refl] MRS fill_ctxt_cat_nseq' ; val ivtacs = [ Safe_tac, (ALLGOALS (dtac ctxt_op_ex1)), (safe_tac (ces nrulefs.elims)), (TRYALL (rtac derrec_trans)), (TRYALL (rtac fill_ctxt_cat_nseq THEN' atac)), TRYALL atac, (TRYALL (rtac rtrancl_refl)) ] ; val _ = qed_goal_spec_mp "dn_splrs_valid" N_Cat.thy "([p], c) : ctxt (nrulefs dn_splrs) --> no_excl_sf (ntau True c) --> \ \ (ntau True p |- ntau True c) : derrec (rulefs fill_cat_rules) {}" (fn _ => [ EVERY ivtacs, (rewtac dn_splrs), Safe_tac, (ALLGOALS (clarsimp_tac (cesimps sn_rule_defs))), (TRYALL (rtac der_idf)), (TRYALL (resolve_tac singleton_sub_fcr_thms)), (rewtac drr_empty), (rtac (tni [dor_idRI, dlolli_monoR]) 2), (rtac (tni [dand_idRD, dlolli_monoL]) 1), (TRYALL (resolve_tac singleton_sub_fcr_thms)) ]) ; val dnf_splrs_valid = mk_mono' (transfer N_Cat.thy dnf_splrs_sub RS cnr_mono) RS dn_splrs_valid ; val _ = qed_goal_spec_mp "dn_pl1_pr2_valid" N_Cat.thy "([p], c) : ctxt (nrulefs {dn_pl1, dn_pr2}) --> \ \ no_excl_sf (ntau True c) --> \ \ (ntau True p |- ntau True c) : derrec (rulefs fill_cat_rules) {}" (fn _ => [ EVERY ivtacs, (ALLGOALS (clarsimp_tac (cesimps dn_plr_defs))), (rewtac drr_empty), (rtac dpr2 2), (rtac dpl1 1), (TRYALL (resolve_tac singleton_sub_fcr_thms)) ]) ; val _ = qed_goal_spec_mp "dn_ac0_valid" N_Cat.thy "([p], c) : ctxt (nrulefs dn_ac0) --> no_excl_sf (ntau True c) --> \ \ (ntau True p |- ntau True c) : derrec (rulefs fill_cat_rules) {}" (fn _ => [ Safe_tac, (ALLGOALS (dtac ctxt_op_ex1)), (safe_tac (ces nrulefs.elims)), (TRYALL (rtac derrec_trans)), (rtac fill_ctxt_catT THEN' atac) 2, atac 2, rewtac dn_ac0, Safe_tac, (ALLGOALS (clarsimp_tac (cesimps dn_ac0_defs))), (TRYALL (resolve_tac der_ids)), rewtac drr_empty, (TRYALL (resolve_tac [dor_assocL, dor_assocR, dor_comm, dand_assocL, dand_assocR, dand_comm])), (TRYALL (resolve_tac singleton_sub_fcr_thms)) ]) ; val [cut_b] = singleton_sub_bcr_thms RL [gfcut] ; val [cut_f] = singleton_sub_fcr_thms RL [gfcut] ; val _ = qed_goal_spec_mp "biill_hctxt_cat" N_Cat.thy "Y : hctxt {X} --> \ \ prems = {T |- ntau True X, ntau False X |- F} --> \ \ (T |- ntau True Y) : derrec (rulefs biill_cat_rules) prems & \ \ (ntau False Y |- F) : derrec (rulefs biill_cat_rules) prems" (fn _ => [ (rtac impI 1), (rtac impI 1), (etac hctxt.induct 1), ALLGOALS Clarsimp_tac, (TRYALL (rtac conjI)), (REPEAT (rtac (drs.sdp RS subsetD) 1 THEN solve_in 1)), (ALLGOALS (rtac (cut_b RS drs.derI))), ALLGOALS Clarsimp_tac, Safe_tac, (TRYALL (rtac derl_derrec_trans THEN' resolve_tac cat_dmonos)), (TRYALL (resolve_tac singleton_sub_bcr_thms)), ALLGOALS Clarsimp_tac, TRYALL (rtac conjI), TRYALL atac, (TRYALL (eresolve_tac [biill_hollows_derT, biill_hollows_derF])), (TRYALL (rtac drr_np THEN' resolve_tac cat_ids)), (TRYALL (resolve_tac singleton_sub_bcr_thms)), (ALLGOALS (EVERY' [rtac derl_derrec_trans, resolve_tac [seq_to_Fexcl, seq_to_Tlolli] ])), (TRYALL (resolve_tac singleton_sub_bcr_thms)), ALLGOALS Clarsimp_tac, ALLGOALS (rtac der_idf), (TRYALL (resolve_tac singleton_sub_bcr_thms)) ]) ; val [biill_hctxt_catT, biill_hctxt_catF] = msc (refl RSN (2, biill_hctxt_cat)) ; val _ = qed_goal_spec_mp "fill_hctxt_cat" N_Cat.thy "Y : hctxt {X} --> \ \ prems = {T |- ntau True X, ntau False X |- F} --> \ \ (no_excl_sf (ntau True Y) --> \ \ (T |- ntau True Y) : derrec (rulefs fill_cat_rules) prems) & \ \ (no_excl_sf (ntau False Y) --> \ \ (ntau False Y |- F) : derrec (rulefs fill_cat_rules) prems)" (fn _ => [ (rtac impI 1), (rtac impI 1), (etac hctxt.induct 1), (TRYALL (rtac conjI)), ALLGOALS Clarsimp_tac, (REPEAT (rtac (drs.sdp RS subsetD) 1 THEN solve_in 1)), (ALLGOALS (rtac (cut_f RS drs.derI))), ALLGOALS Clarsimp_tac, Safe_tac, (TRYALL (rtac derl_derrec_trans THEN' resolve_tac cat_dmonos)), (TRYALL (resolve_tac singleton_sub_fcr_thms)), ALLGOALS Clarsimp_tac, TRYALL (rtac conjI), TRYALL atac, (TRYALL (eresolve_tac [fill_hollows_derT, fill_hollows_derF])), (TRYALL (rtac drr_np THEN' resolve_tac cat_ids)), (TRYALL (ares_tac singleton_sub_fcr_thms)), (ALLGOALS (EVERY' [rtac derl_derrec_trans, resolve_tac [seq_to_Fexcl, seq_to_Tlolli] ])), (TRYALL (resolve_tac singleton_sub_fcr_thms)), ALLGOALS Clarsimp_tac, ALLGOALS (rtac der_idf), (TRYALL (resolve_tac singleton_sub_fcr_thms)) ]) ; val [fill_hctxt_catT, fill_hctxt_catF] = msc (refl RSN (2, fill_hctxt_cat)) ; val _ = qed_goal_spec_mp "hctxt_excl_lemF" N_Cat.thy "Y : hctxt {X} --> (W, ntau False X) : ipsubfml^* --> W : excl_fmls --> \ \ (EX U. (U, ntau False Y) : ipsubfml^* & U : excl_fmls)" (fn _ => [ (REPEAT (rtac impI 1)), (etac hctxt.induct 1), ALLGOALS Clarsimp_tac, Fast_tac 1, (TRYALL (EVERY' [rtac exI, rtac conjI, etac tct.rsr, resolve_tac ipsubfml.intrs, atac])), (EVERY' [rtac exI, rtac conjI, rtac rtrancl_refl, rtac excl_fmls.I] 1) ]) ; val _ = qed_goal_spec_mp "hctxt_excl_lemF" N_Cat.thy "Y : hctxt {X} --> ~ no_excl_sf (ntau False X) --> \ \ ~ no_excl_sf (ntau False Y)" (fn _ => [ (REPEAT (rtac impI 1)), (etac hctxt.induct 1), ALLGOALS Clarsimp_tac ]) ; val _ = qed_goal_spec_mp "hctxt_excl_lemT" N_Cat.thy "Y : hctxt {X} --> (W, ntau True X) : ipsubfml^* --> W : excl_fmls --> \ \ (EX U. (U, ntau True Y) : ipsubfml^* & U : excl_fmls)" (fn _ => [ (REPEAT (rtac impI 1)), (etac hctxt.induct 1), ALLGOALS Clarsimp_tac, Fast_tac 1, (TRYALL (EVERY' [rtac exI, rtac conjI, etac tct.rsr, resolve_tac ipsubfml.intrs, atac])), (chop_last (datac TF_excl 1 1)), (EVERY' [ etac ex_forward, etac conj_forward2s, etac tct.rsr, resolve_tac ipsubfml.intrs] 1) ]) ; val _ = qed_goal_spec_mp "hctxt_excl_lemT" N_Cat.thy "Y : hctxt {X} --> ~ no_excl_sf (ntau True X) --> \ \ ~ no_excl_sf (ntau True Y)" (fn _ => [ (REPEAT (rtac impI 1)), (etac hctxt.induct 1), ALLGOALS Clarsimp_tac, (dtac TF_nes 1 THEN contr_tac 1) ]) ; val _ = qed_goal_spec_mp "fill_hctxt_cat_nseq" N_Cat.thy "Y : hctxt {X} --> \ \ ~ no_excl_sf (ntau False X) --> no_excl_sf (ntau True Y) --> \ \ (T |- ntau True Y) : derrec (rulefs fill_cat_rules) {T |- ntau True X}" (fn _ => [ (rtac impI 1), (rtac impI 1), (etac hctxt.induct 1), ALLGOALS Clarsimp_tac, (rtac (drs.sdp RS subsetD) 1 THEN solve_in 1), (datac hctxt_excl_lemF 1 4), Clarify_tac 4, (ALLGOALS (rtac (cut_f RS drs.derI))), ALLGOALS Clarsimp_tac, Safe_tac, (TRYALL (rtac derl_derrec_trans THEN' resolve_tac cat_dmonos)), (TRYALL (resolve_tac singleton_sub_fcr_thms)), ALLGOALS Clarsimp_tac, TRYALL (rtac conjI), TRYALL atac, (TRYALL (eresolve_tac [fill_hollows_derT, fill_hollows_derF])), (TRYALL (rtac drr_np THEN' resolve_tac cat_ids)), (TRYALL (ares_tac singleton_sub_fcr_thms)) ]) ; val _ = qed_goal_spec_mp "dn_ax_valid" N_Cat.thy "nseq : dn_axioms --> no_excl_sf (ntau True nseq) --> \ \ (T |- ntau True nseq) : derrec (rulefs fill_cat_rules) {}" (fn _ => [ (safe_tac (ces dn_axioms.elims)), ALLGOALS Clarsimp_tac, (ALLGOALS (rtac (cut_f RS drs.derI))), ALLGOALS Clarsimp_tac, Safe_tac, (TRYALL (rtac derl_derrec_trans THEN' resolve_tac cat_dmonos)), (TRYALL (resolve_tac singleton_sub_fcr_thms)), ALLGOALS Clarsimp_tac, TRYALL (rtac conjI), (TRYALL (eresolve_tac [fill_hollows_derF, fill_hollows_derT])), (TRYALL atac), (TRYALL (rtac der_lolli_idf)), (TRYALL (resolve_tac singleton_sub_fcr_thms)), (ALLGOALS (rtac (cut_f RS drs.derI))), ALLGOALS Clarsimp_tac, Safe_tac, (EVERY (map (rtac derl_derrec_trans THEN' resolve_tac cat_dmonos) [8,5,4,1])), (TRYALL (resolve_tac singleton_sub_fcr_thms)), ALLGOALS Clarsimp_tac, TRYALL (rtac conjI), (EVERY (map (eresolve_tac [fill_hollows_derF, fill_hollows_derT]) [12,7,6,1])), TRYALL atac, (EVERY (map (rtac der_idf) [8,5,4,1])), (TRYALL (rtac drr_np THEN' match_tac cat_ids)), (TRYALL (resolve_tac singleton_sub_fcr_thms)), (ALLGOALS (rtac drr_np THEN' resolve_tac cat_ids)), (TRYALL (resolve_tac singleton_sub_fcr_thms)) ]) ; val _ = qed_goal_spec_mp "dn_hctxt_ax_valid" N_Cat.thy "nseq : hctxt dn_axioms --> no_excl_sf (ntau True nseq) --> \ \ (T |- ntau True nseq) : derrec (rulefs fill_cat_rules) {}" (fn _ => [ Clarify_tac 1, (dtac hctxt_ex1 1), Clarify_tac 1, (ftac fill_hctxt_cat_nseq 1), atac 2, (rtac derrec_trans 2), atac 3, Simp_tac 2, (etac dn_ax_valid 2), (etac contrapos_pp 2 THEN eatac hctxt_excl_lemT 1 2), (etac dn_axioms.elim 1), ALLGOALS Clarsimp_tac ]) ; local open drs in val drs2 = dlNil RSN (2, dlCons) RSN (2, dlCons) ; val drs3 = dlNil RSN (2, dlCons) RSN (2, dlCons) RSN (2, dlCons) ; val drs_cut = drs2 RS (cut_f RS derI) ; end ; val vcth = ([singletonI RS drs.dpI, der_pne] MRS drs_cut) ; val d2p = tdfc [dand_idRI, dand_mono, drl.asmI] ; val _ = qed_goal_spec_mp "filldn_rules_valid" N_Cat.thy "(ps, c) : filldn --> no_excl_sf (ntau True c) --> \ \ (T |- ntau True c) : derrec (rulefs fill_cat_rules) \ \ ((%p. T |- ntau True p) ` (set ps))" (fn _ => [ (safe_tac (ces [filldn.elim, gfilldn.elim])), ALLGOALS (clarsimp_tac init_css), (eatac dn_hctxt_ax_valid 1 7), (* for subgoals 1,2,3, single premise rules *) (TRYALL (ftac (mk_mono' ctxt_nrulefs_one_prem))), (rtac dn_ac0_one_prem 1), (rtac ([dnf_splrs_sub, dn_splrs_one_prem] MRS subset_trans) 2), (force_tac (cesimps [dn_pl1, dn_pr2]) 3), (safe_tac (ces one_prem.elims)), (ALLGOALS (clarsimp_tac init_css)), (datac dn_ac0_valid 1 1), etac vcth 1, (datac dnf_splrs_valid 1 1), etac vcth 1, (datac dn_pl1_pr2_valid 1 1), etac vcth 1, (* for last 3 subgoals, two-premise rules *) (ALLGOALS (dresolve_tac lem27s THEN' atac THEN' atac)), (ALLGOALS (rtac ([d2p, drs3] MRS derl_derrec_trans))), (TRYALL (resolve_tac singleton_sub_fcr_thms)), (TRYALL (etac der_pne)), (TRYALL (rtac drs.dpI THEN' solve_in)) ]) ; val dne_tacs = [ (ALLGOALS (EVERY' [etac rtranclE, etac excl_fmls.elim, Force_tac])), (ALLGOALS (EVERY' [eresolve_tac ipsubfml_2_cases])), Safe_tac, (TRYALL (EVERY' [datac rmerge_subfml 1, eresolve_tac [disjI1, disjI2]])), (TRYALL (EVERY' excl_ex_fwd_rt_tacs)) ] ; val _ = qed_goal_spec_mp "dn_lrs_excl" N_Cat.thy "(A, B, C) : dn_lollia Un dn_ands Un dn_ora Un dn_excls --> \ \ P : excl_fmls --> \ \ (P, ntau b A) : ipsubfml^* | (P, ntau b B) : ipsubfml^* --> \ \ (EX Q. (Q, ntau b C) : ipsubfml^* & Q : excl_fmls)" (fn _ => [ (safe_tac (ces [dn_lollia.elim, dn_ora.elim, dn_ands.elim, dn_excls.elim])), (ALLGOALS Clarsimp_tac), Safe_tac, (ALLGOALS Clarsimp_tac), (TRYALL (EVERY' [rtac exI, rtac conjI, rtac rtrancl_refl, rtac excl_fmls.I])), EVERY dne_tacs, EVERY dne_tacs, (TRYALL (EVERY' excl_ex_rt_tacs)) ]) ; val _ = qed_goal_spec_mp "dn_lrs_rmerge1_excl" N_Cat.thy "(Ra, Rb, Rc) : rmerge1 (A, B, C) --> P : excl_fmls --> \ \ (A, B, C) : dn_lollia Un dn_ands Un dn_ora Un dn_excls --> \ \ (ALL b. (P, ntau b Ra) : ipsubfml^* | (P, ntau b Rb) : ipsubfml^* --> \ \ (EX Q. (Q, ntau b Rc) : ipsubfml^* & Q : excl_fmls))" (fn _ => [ (rtac impI 1), (rtac impI 1), (rtac impI 1), (etac rmerge1_induct 1), ALLGOALS Clarsimp_tac, (TRYALL (rtac conjI)), (TRYALL (rtac impI)), (LASTGOAL (EVERY' [rtac dn_lrs_excl, Fast_tac, atac, Fast_tac])), (LASTGOAL (EVERY' [rtac dn_lrs_excl, Fast_tac, atac, Fast_tac])), ALLGOALS Clarsimp_tac, (TRYALL (rtac conjI)), (TRYALL (rtac impI)), (TRYALL (EVERY' [rtac exI, rtac conjI, rtac rtrancl_refl, rtac excl_fmls.I])), (ALLGOALS (EVERY' [etac rtranclE, etac excl_fmls.elim, Force_tac])), (ALLGOALS (EVERY' [eresolve_tac ipsubfml_2_cases])), ALLGOALS hyp_subst_tac, (TRYALL (EVERY' [datac rmerge_subfml 1, eresolve_tac [disjI1, disjI2], etac ex_forward, etac conj_forward2s, etac tct.rsr, resolve_tac ipsubfml.intrs])), (TRYALL (EVERY' [ etac allE, etac conjE, mp_tac, etac ex_forward, etac conj_forward2s, etac tct.rsr, resolve_tac ipsubfml.intrs])) ]) ; val ipsf_rtc_elims' = Seq.list_of (eresolve_tac ipsubfml_2_cases 3 rtranclE) ; val ipsf_rtc_elims = map (tacthm (TRYALL hyp_subst_tac)) ipsf_rtc_elims' ; val _ = qed_goal_spec_mp "excl_ns_F" N_Cat.thy "P : excl_fmls --> (P, F) : ipsubfml^* --> R" (fn _ => [ (Clarify_tac 1), (etac excl_fmls.elim 1), (etac rtranclE 1), Force_tac 1, eresolve_tac ipsubfml_0_cases 1 ]) ; val _ = qed_goal_spec_mp "excl_ns_T" N_Cat.thy "P : excl_fmls --> (P, T) : ipsubfml^* --> R" (fn _ => [ (Clarify_tac 1), (etac excl_fmls.elim 1), (etac rtranclE 1), Force_tac 1, eresolve_tac ipsubfml_0_cases 1 ]) ; val _ = qed_goal_spec_mp "dn_ac0bsplrs_excl" N_Cat.thy "(ps, c) : nrulefs (dn_bprs Un dn_splrs Un dn_ac0) --> \ \ p : set ps --> ~ no_excl_sf (ntau b p) --> \ \ ~ no_excl_sf (ntau b c)" (fn _ => [ (clarsimp_tac (ces nrulefs.elims, esimps (dn_splrs :: dn_bprs :: dn_ac0 :: sn_lir_defs @ dn_plr_defs @ dn_ac0_defs)) 1), Safe_tac, (ALLGOALS (clarsimp_tac (claset (), esimps [] addsplits [split_if_asm]))) ]) ; val _ = qed_goal_spec_mp "ctxt_dn_ac0bsplrs_excl" N_Cat.thy "(ps, c) : ctxt (nrulefs (dn_bprs Un dn_splrs Un dn_ac0)) --> \ \ (ALL p. p : set ps --> (ALL b. ~ no_excl_sf (ntau b p) --> \ \ ~ no_excl_sf (ntau b c)))" (fn _ => [ (rtac impI 1), (etac pair_ctxt_induct 1), strip_tac 1, (eatac dn_ac0bsplrs_excl 2 1), ALLGOALS Clarsimp_tac, Fast_tac 1 ]) ; (* preservation of non-FILL sequents *) val _ = qed_goal_spec_mp "non_fill_dn_pres" N_Cat.thy "(ps, c) : biilldn --> p : set ps --> \ \ ~ no_excl_sf (ntau True p) --> ~ no_excl_sf (ntau True c)" (fn _ => [ (safe_tac (ces [biilldn.elim, gbiilldn.elim])), LASTGOAL Clarsimp_tac, (TRYALL (dtac (mk_mono' cnr_mono RS ctxt_dn_ac0bsplrs_excl) THEN' Fast_tac)), TRYALL atac, TRYALL contr_tac, rewtac no_excl_sf_def, Safe_tac, (TRYALL (EVERY' [(datac dn_lrs_rmerge1_excl 1), Clarify_tac, Force_tac, Fast_tac ])) ]) ; (* a FILL sequent provable in BiILLdn is provable in FILLdn *) val _ = qed_goal_spec_mp "dn_biill_excl" N_Cat.thy "(ps, c) : biilldn --> no_excl_sf (ntau True c) --> (ps, c) : filldn" (fn _ => [ (safe_tac (ces [biilldn.elim, gbiilldn.elim])), (TRYALL (rtac filldn.I)), TRYALL atac, (TRYALL (eresolve_tac gfilldn.intrs THEN_ALL_NEW atac)), (etac dn_excls.elim 3), (dtac rmerge1_excl_lemT 3), Force_tac 3, Force_tac 3, (rewtac dn_splrs), (rewtac dn_bprs), (TRYALL (etac (ctxt_ex1 RS bexE) THEN' etac nrulefs.elim)), Safe_tac, (ALLGOALS (clarsimp_tac (cesimps [dn_pr1, dn_pl2, sn_excla]))), (TRYALL (EVERY' [etac (mk_dupE ctxt_single_one_premE), Clarify_tac, dtac ctxt_excl_lemT, Force_tac, Force_tac ])), (TRYALL (dtac (reop rev (nrulefs.iisubI RS singleton_subsetI RS ctxt_mono RS subsetD)))), (TRYALL (eresolve_tac gfilldn.intrs o incr THEN' MSSG (simp_tac (esimps [dnf_splrs, dn_bprs])))) ]) ; val _ = qed_goal_spec_mp "dn_biill_sfill" N_Cat.thy "(ps, c) : biilldn --> no_excl_sf (ntau True c) --> (ps, c) : sfilldn" (fn _ => [ strip_tac 1, (rtac sfilldn.I 1), (EVERY' [rtac ballI, etac insertE, hyp_subst_tac, atac] 2), (eatac (mkpp non_fill_dn_pres) 2 2), (eatac dn_biill_excl 1 1) ]) ; (* a more useful introduction rule *) val _ = bind_thm ("sfilldn_I", biilldn_filldn RS subsetD RS dn_biill_sfill) ; val _ = qed_goal_spec_mp "dn_der_biill_sfill" N_Cat.thy "c : derrec biilldn ps --> no_excl_sf (ntau True c) --> c : derrec sfilldn ps" (fn _ => [ (rtac impI 1), (etac drs.inductr 1), (rtac impI 1), (etac drs.dpI 1), Clarify_tac 1, (fatac dn_biill_sfill 1 1), (etac drs.derI 1), (clarsimp_tac (cesimps [drs.all]) 1), (datac bspec 1 1), etac mp 1, (eatac (mkpp non_fill_dn_pres) 2 1) ]) ; val der_sf_f = [asm_rl, s_filldn, subset_refl] MRS der_mono ; val _ = bind_thm ("dn_der_biill_fill", dn_der_biill_sfill RS der_sf_f) ; val der_b_f = [asm_rl, biilldn_filldn, subset_refl] MRS der_mono ; val _ = bind_thm ("dn_der_fill_sfill", der_b_f RS dn_der_biill_sfill) ; (* FILL sequent, if FILLdn-provable then FILL-valid *) val _ = qed_goal_spec_mp "filldn_valid" N_Cat.thy "c : derrec filldn ps --> \ \ no_excl_sf (ntau True c) --> \ \ (T |- ntau True c) : derrec (rulefs fill_cat_rules) \ \ ((%p. T |- ntau True p) ` ps)" (fn _ => [ (rtac impI 1), (etac drs.inductr 1), (rtac impI 1), (rtac drs.dpI 1), (etac rev_image_eqI 1), rtac refl 1, Clarify_tac 1, (fatac filldn_rules_valid 1 1), (rtac derrec_trans 1), (atac 2), Clarify_tac 1, (datac bspec 1 1), etac mp 1, (eatac (mkpp (biilldn_filldn RS subsetD RS non_fill_dn_pres)) 2 1) ]) ; val _ = qed_goal_spec_mp "sfilldn_valid" N_Cat.thy "c : derrec sfilldn ps --> \ \ (T |- ntau True c) : derrec (rulefs fill_cat_rules) \ \ ((%p. T |- ntau True p) ` ps)" (fn _ => [ rtac impI 1, etac drs.elim 1, (rtac drs.dpI 1), Force_tac 1, (etac sfilldn.elim 1), Clarsimp_tac 1, (rtac filldn_valid 1), atac 2, (etac drs.derI 1), (etac ders_mono 1), rtac s_filldn 1, rtac subset_refl 1 ]) ; val filldn_valid_np = simplify (esimps []) (read_instantiate [("ps", "{}")] filldn_valid) ; val sfilldn_valid_np = simplify (esimps []) (read_instantiate [("ps", "{}")] sfilldn_valid) ; val _ = qed_goal_spec_mp "filldn_valid_np_alt" N_Cat.thy "($ca => $cs) : derrec filldn {} --> \ \ no_excl_sf (ntau True cs) --> no_excl_sf (ntau False ca) --> \ \ (ntau False ca |- ntau True cs) : derrec (rulefs fill_cat_rules) {}" (fn _ => [ Clarify_tac 1, (dtac filldn_valid_np 1), ALLGOALS Clarsimp_tac, (rtac derl_derrec_trans 1), (rtac Tlolli_to_seq 1), (TRYALL (resolve_tac singleton_sub_fcr_thms)), Clarsimp_tac 1 ]) ;