(* TODO - put this earlier *) Addsimps (map (transfer (the_context())) [ms_single_eq_mins,ms_single_eq_mins', ms_single_eq_sp, ms_single_eq_sp', ms_single_eq_ps, ms_single_eq_ps']) ; open Genrules_nested ; val snrfsI = (singletonI RS read_instantiate [("fs", "(?f_s, ?ss)")] nrulefs.iisubI RS mem_same) ; val snrfsI = (singletonI RS nrulefs.iisubI RS mem_same) ; (* Goal "c = ($ca => $cs) --> ([p], c) : ctxt (nrulefs dn_splrs) --> \ \ (c, c') : ms_deep_equiv --> \ \ ([c'], d') : nrulefs {sn_rp, sn_drp, \ \ invert sn_rp, invert sn_drp, sn_gl, sn_gr, sn_ig, sn_eg} --> \ \ (EX p' q q' d. (p, p') : ms_deep_equiv & \ \ ([p'], q) : nrulefs {sn_rp, sn_drp, \ \ invert sn_rp, invert sn_drp, sn_gl, sn_gr, sn_ig, sn_eg} & \ \ (q, q') : ms_deep_equiv & \ \ ([q'], d) : ctxt (nrulefs dn_splrs) & \ \ (d, d') : ms_deep_equiv)" ; *) val nstac = (REPEAT_ALL_NEW (FIRST' [ares_tac [exI, rev_conjI, msde.seqs], rtac refl_msde', eresolve_tac ctxt.intrs])) ; val dctac = REPEAT_ALL_NEW (FIRST' [resolve_tac [exI, rev_conjI], nk_msde_tac, ctxt_tac]) ; (* lemma for single premise logical rules *) fun mkr sn_rule = rewrite_rule [meta_eq_def, Bidi_def'] sn_rule RSN (2, trans) ; fun litacs sn_lr = [ (etac nrulefs.elim), Clarify_tac, (dtac (mkr sn_lr)), Clarsimp_tac ] ; fun dcstacs sn_lr = [ dctac, (EVERY' (litacs sn_lr)), (rtac ctxt.same), (rtac (subset_refl RS mk_gpcm sn_lr)) ] ; fun keep_trans_tacs trans_thm = [ (REPEAT o dtac keep_msdeI), (datac ([keepFD, keepFD] MRS trans_thm) 1), (REPEAT o ematch_tac [keepF_thin]), (REPEAT o dtac keepD) ] ; val comtacs = [ (resolve_tac rfs_lrs_ns), (EVERY' (keep_trans_tacs trans_msde')), (EVERY' (keep_trans_tacs trans_msde')), (REPEAT_ALL_NEW (eresolve_tac [msde_com_nseqE, msde_nseq_comE]) THEN_ALL_NEW (TRY o (eresolve_tac (ms_of_ns_nested_seqs_EmptyE :: cnnE_ths @ cpnnE_ths) THEN' atac))), (clarify_tac (ces nested_seqs.elims)), (etac ctxt.elim THEN_ALL_NEW Clarify_tac), (etac ms_of_ns_nseqs_EmptyE ORELSE' MSSG dctac) o incr, (etac ms_of_ns_nseqs_EmptyE ORELSE' MSSG dctac) o incr ] ; val msotac = (rtac msde.seqs THEN_ALL_NEW (TRY o rtac refl_msde') THEN_ALL_NEW EVERY' [ (rtac msde.ms_of), (rtac refl_mmsde_eq'), Force_tac o incr ] ) ; (* why doesn't this work ? val msotac = (rtac msde.seqs THEN_ALL_NEW (TRY o rtac refl_msde') THEN_ALL_NEW rtac refl_ms_of_ns_eq) ; by (REPEAT_FIRST (etac keepF_thin)) ; *) fun ictacs sn_lr = [ (EVERY' (litacs sn_lr) 1), (REPEAT (dtac keep_msdeI 1)), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 1), (rtac trans_msde' 1), perm_msde_tac 1, (rtac trans_msde' 2), perm_msde_tac 3, (rtac ctxt.same 3), (rtac (subset_refl RS mk_gpcm sn_lr) 3), (msotac THEN_ALL_NEW EVERY' [ (simp_tac (esimps [symmetric mins_def', symmetric mins_def, mins_assoc, mins_assoc_alt])), (rtac mins_eqI), (rtac (ms_of_ns_NComma RS sym))]) 2, msotac 1, TRY (Simp_tac 1), inc_ref_tac case_count ] ; fun dctxt_tacs sn_lr sg _ = [ rtac conjI 1, rtac (sn_lr RS def_imp_eq) 1, (rtac impI 1), (etac pair_dctxt_induct 1), ALLGOALS Clarsimp_tac, nstac 7, nstac 6, nstac 1, (* last two and first subgoals *) (etac ctxt_nseqs_NIE 4), (EVERY' comtacs 4), (etac ctxt_nseqs_NI_altE 3), (EVERY' comtacs 3), (etac ctxt_nseqs_NIE 2), (EVERY' comtacs 2), (etac ctxt_nseqs_NI_altE 1), (EVERY' comtacs 1), (* (TRYALL (eatac ms_of_ns_nested_seqs_EmptyE 1)), (TRYALL (etac ms_of_ns_nseqs_EmptyE)), *) (* now no goals involve ctxt *) TRY (EVERY' (dcstacs sn_lr) sg), TRY (EVERY' (dcstacs sn_lr) sg), REPEAT (EVERY (ictacs sn_lr)) ] ; (* for dn_pl1t, after all comtacs, first two sg OK with ictacs, then third fails by (PRIMITIVE (rotate_prems 1)) ; by (EVERY (ictacs sn_lr)) ; problem - pl1t isn't closed under dctxt *) val dcstr = "?sn_lr = (?t :: nested psc) & \ \ ((ps, c) : dctxt (nrulefs {?sn_lr}) --> (ALL p. ps = [p] --> \ \ (EX p' c'. (p, p') : ms_deep_equiv & (c', c) : ms_deep_equiv & \ \ ([p'], c') : ctxt (nrulefs {?sn_lr}))))" ; fun mk_dcthm sn_lr sg = let val th = prove_goal Msde.thy dcstr (dctxt_tacs sn_lr sg) ; in refl RSN (2, meta_std (th RS conjunct2)) end ; system "date" ; (* 6 secs *) val dc_anda = mk_dcthm sn_anda 3 ; val dc_tA = mk_dcthm sn_tA 3 ; val dc_ors = mk_dcthm sn_ors 1 ; val dc_lollis = mk_dcthm sn_lollis 1 ; val dc_excla = mk_dcthm sn_excla 3 ; val dc_fS = mk_dcthm sn_fS 1 ; val dc_splrs = [dc_anda, dc_ors, dc_excla, dc_lollis, dc_tA, dc_fS]; (* dc lemmas for propagation rules *) val dc_pl1 = mk_dcthm dn_pl1 0 ; val dc_pr1 = mk_dcthm dn_pr1 0 ; val dc_pl2 = mk_dcthm dn_pl2 0 ; val dc_pr2 = mk_dcthm dn_pr2 0 ; val dc_bprs = [dc_pl1, dc_pr1, dc_pl2, dc_pr2] ; (* dc lemmas for variant propagation rules *) (* these fail, these rules do not actually allow dctxt val dc_pl1t = mk_dcthm dn_pl1t 0 ; val dc_pr1t = mk_dcthm dn_pr1t 0 ; val dc_plc = mk_dcthm dn_plc 0 ; val dc_prc = mk_dcthm dn_prc 0 ; following ones OK *) val dc_pl1tg = mk_dcthm dn_pl1tg 0 ; val dc_pr1tg = mk_dcthm dn_pr1tg 0 ; val dc_plcg = mk_dcthm dn_plcg 0 ; val dc_prcg = mk_dcthm dn_prcg 0 ; val dc_pxxg_ths = [ dc_pl1tg, dc_pr1tg, dc_plcg, dc_prcg ] ; (* dctxt of some rules in biilldn *) val cmnk = [asm_rl, asm_rl, keepFD, keepFD] MRS ctxt_msde_nested' ; fun mk_dctxt_biilldn_th gbiilldn_dnI dc_lr = prove_goal Ndeep.thy "psc : dctxt (nrulefs {?sn_rule}) --> psc : derl biilldn" (fn _ => [ (rtac impI 1), (ftac dctxt_nested' 1), (ftac (mk_mono' dctxt_nrulefs_one_prem) 2), (etac one_prem.elim 3), Clarify_tac 3, (ftac dc_lr 3), Clarify_tac 3, (resolve_tac rfs_lrs_ns 1), (simp_tac (esimps (sn_rule_defs @ dn_plr_defs)) 1), (clarsimp_tac (ces [pscs.elim, nested_seqs.elim], esimps []) 1), (REPEAT (dtac keep_msdeI 1)), dtac cmnk 1, (resolve_tac rfs_lrs_ns 1), atac 1, atac 1, (REPEAT (ematch_tac [keepF_thin] 1)), (clarify_tac (ces [msde_nseqsE, nested_seqs.elim]) 1), (rtac rcdthm 1), (eatac msde_seqs_biilldn 1 1), (rtac rcdthm 1), (eatac msde_seqs_biilldn 1 2), (rtac (biilldn.I RS drl.singleI) 1), Simp_tac 2, (rtac gbiilldn_dnI 1), (etac cnr_mono' 1), (force_tac (cesimps [dn_splrs, dn_bprs]) 1) ]) RS mp ; val dctxt_biilldn_ths = map (mk_dctxt_biilldn_th gbiilldn.dn_splrs) dc_splrs @ map (mk_dctxt_biilldn_th gbiilldn.dn_bprs) dc_bprs ; val _ = qed_goalw_spec_mp "dctxt_bprs_biilldn" Ndeep.thy [dn_bprs] "psc : dctxt (nrulefs dn_bprs) --> psc : derl biilldn" (fn _ => [ (clarsimp_tac (cesimps [nrulefs_ii, dctxt_Un]) 1), Safe_tac, (TRYALL (eresolve_tac dctxt_biilldn_ths)) ]) ; val _ = qed_goalw_spec_mp "dctxt_splrs_biilldn" Ndeep.thy [dn_splrs] "psc : dctxt (nrulefs dn_splrs) --> psc : derl biilldn" (fn _ => [ (clarsimp_tac (cesimps [nrulefs_ii, dctxt_Un]) 1), Safe_tac, (TRYALL (eresolve_tac dctxt_biilldn_ths)) ]) ; val _ = qed_goal_spec_mp "dctxt_sn_ac0_biilldn" Ndeep.thy "psc : dctxt (nrulefs sn_ac0) --> psc : derl biilldn" (fn _ => [ (rtac impI 1), (ftac (mk_mono' dctxt_nrulefs_one_prem) 1), (rtac sn_ac0_one_prem 1), (etac one_prem.elim 1), hyp_subst_tac 1, (ftac dctxt_dn_ac0_msde 1), (ftac dctxt_nested' 1), (rtac sn_ac0_ns 1), (eatac msde_ns_biilldn 1 1) ]) ; (* to show two premise rules of shallow system derivable in deep system, need a hollow-weakening admissibility result for deep system *) val dth = full_simplify init_ss (gbiilldn.dn_axioms RS biilldn.I RS drs.pscI) ; val axtacs = [ Clarsimp_tac, (rtac biilldn_msde'), (rtac msde.seqs THEN_ALL_NEW (resolve_tac msde_assocs ORELSE' rtac refl_msde')) o incr, (rtac (hctxt.same RS dth)), (resolve_tac dn_axioms.intrs THEN_ALL_NEW solve_hollows_tac) ] ; fun dgtacs gbxxI = [ (rtac drs.derIsingle 1), atac 2, (rtac biilldn.I 1), (rtac gbxxI 1), (ctxt_tac 1), Force_tac 1 ] ; fun oplrtacs (dn_xxrs_one_prem, dctxt_xxrs_biilldn, gbxxI) = [ (etac (mk_dupE cn_one_prem') 1), (rtac dn_xxrs_one_prem 1), Clarsimp_tac 1, (etac nested_seqs.elim 1), hyp_subst_tac 1, ((etac ctxt.elim THEN_ALL_NEW Clarsimp_tac) 1), (etac dd1th 1), (rtac dctxt_xxrs_biilldn 1), dctxt_tac 1, EVERY (dgtacs gbxxI), EVERY (dgtacs gbxxI) ] ; fun rmtacs gbxxI = [ (rtac (biilldn.I RS drs.derI)), (etac gbxxI), (REPEAT o dtac hollows_rmerge), solve_rmerge1, Force_tac, Force_tac ] ; fun p2lrtacs (gbxxI, dn_lr_elim, dn_lr_I) = [ (etac rmerge1.elim THEN_ALL_NEW Clarsimp_tac), (EVERY' (rmtacs gbxxI)), (EVERY' (rmtacs gbxxI)), (clarify_tac (ces nested_seqs.elims)), (REPEAT o (etac allE2 THEN' dtac (refl RS rev_mp))), (etac dn_lr_elim), Clarsimp_tac, (REPEAT o dtac hollows_rmerge), (rtac biilldn_msde'), (rtac msde.seqs THEN_ALL_NEW (resolve_tac msde_assocs ORELSE' rtac refl_msde')) o incr, (rtac (biilldn.I RS drs.derI)), (rtac (dn_lr_I RS gbxxI)), (solve_rmerge1 o incr o incr), solve_rmerge, solve_rmerge, Force_tac, Simp_tac, rtac conjI, (etac biilldn_msde' THEN' MSSG safe_msde_tac), (etac biilldn_msde' THEN' MSSG safe_msde_tac) ] ; val _ = qed_goal_spec_mp "hollow_weak" Ndeep.thy "XY : derrec biilldn {} --> (ALL X Y. XY = ($X => $Y) --> U : hollows --> \ \ V : hollows --> ($U,,, $X => $Y,,, $V) : derrec biilldn {})" (fn _ => [ rtac impI 1, (etac drs.inductre 1), (chop_tac 1 (etac thin_rl 1)), (* ps : dersrec biilldn {} *) (safe_tac (ces [biilldn.elim, gbiilldn.elim])), ALLGOALS Clarsimp_tac, (* dn_axioms *) ((etac hctxt.elim THEN_ALL_NEW Clarsimp_tac) 8), rtac dth 9, solve_hctxt_tac 9, rtac dth 9, solve_hctxt_tac 9, ((etac dn_axioms.elim THEN_ALL_NEW EVERY' axtacs) 8), (* dn_ac0 *) (etac (mk_dupE cn_one_prem') 1), (rtac dn_ac0_one_prem 1), Clarsimp_tac 1, (dtac ctxt_dn_ac0_msde 1), (etac nested_seqs.elim 1), hyp_subst_tac 1, (etac allE2 1), (dtac (refl RS rev_mp) 1), (etac msde_nseqsE 1), (etac biilldn_msde' 1), safe_msde_tac 1, (EVERY (oplrtacs (dn_splrs_one_prem, dctxt_splrs_biilldn, gbiilldn.dn_splrs))), (EVERY (oplrtacs (dn_bprs_one_prem, dctxt_bprs_biilldn, gbiilldn.dn_bprs))), (EVERY' (p2lrtacs (gbiilldn.dn_ands, dn_ands.elim, dn_ands.I)) 1), (EVERY' (p2lrtacs (gbiilldn.dn_ora, dn_ora.elim, dn_ora.I)) 1), (EVERY' (p2lrtacs (gbiilldn.dn_lollia, dn_lollia.elim, dn_lollia.I)) 1), (EVERY' (p2lrtacs (gbiilldn.dn_excls, dn_excls.elim, dn_excls.I)) 1) ]) ; val hollow_weak' = refl RSN (2, hollow_weak) ; fun sdtacs (dn_lrI, gbxxI) _ = [ (clarsimp_tac (ces nrulefs.elims, esimps []) 1), (cut_facts_tac [ex_hollows_NComma_rmerge] 1), (cut_facts_tac [ex_hollows_NComma_rmerge] 1), Safe_tac, (rtac adm.I 1), (rtac impI 1), (rtac drs.derI 1), (rtac biilldn.I 1), (rtac gbxxI 1), (rtac rmerge1.base 2), (rtac dn_lrI 1), Force_tac 3, atac 1, atac 1, Full_simp_tac 1, etac conj_forward 1, (REPEAT (EVERY [dtac hollow_weak' 1, etac biilldn_msde' 3, (safe_msde_tac THEN_ALL_NEW resolve_tac (refl_msde' :: msde_cases)) 3, atac 1, atac 1 ])) ] ; val _ = qed_goalw_spec_mp "sn_ands_dn" Ndeep.thy [sn_ands] "nrulefs {sn_ands} <= adm biilldn" (sdtacs (dn_ands.I, gbiilldn.dn_ands)) ; val _ = qed_goalw_spec_mp "sn_ora_dn" Ndeep.thy [sn_ora] "nrulefs {sn_ora} <= adm biilldn" (sdtacs (dn_ora.I, gbiilldn.dn_ora)) ; val _ = qed_goalw_spec_mp "sn_lollia_dn" Ndeep.thy [sn_lollia] "nrulefs {sn_lollia} <= adm biilldn" (sdtacs (dn_lollia.I, gbiilldn.dn_lollia)) ; val _ = qed_goalw_spec_mp "sn_excls_dn" Ndeep.thy [sn_excls] "nrulefs {sn_excls} <= adm biilldn" (sdtacs (dn_excls.I, gbiilldn.dn_excls)); val sn_lr_dns = [sn_ands_dn, sn_ora_dn, sn_lollia_dn, sn_excls_dn] RL [subsetD] ; (* would now like dctxt of dn_pl1t to be in ctxt of dn_pl1tg for which dctxt of dn_pl1tg is now sufficient, use map mk_ext_msde dn_pxxg_ths ; *) system "date" ; val dcustr = "(([p], c) : dctxt (nrulefs (?sn_lrsA Un ?sn_lrsB :: nested psc set)) --> \ \ (EX p' c'. (p, p') : ms_deep_equiv & (c', c) : ms_deep_equiv & \ \ ([p'], c') : ctxt (nrulefs (?sn_lrsAg Un ?sn_lrsBg))))" ; fun dc_Un_tacs dc_th1 dc_th2 _ = [ (clarsimp_tac (cesimps [ nrulefs_Un2, ctxt_Un, dctxt_Un]) 1), Safe_tac, (dtac dc_th1 1), (dtac dc_th2 2), REPEAT (Fast_tac 1) ] ; fun mk_dc_Un dc_th1 dc_th2 = let val th = prove_goal Msde.thy dcustr (dc_Un_tacs dc_th1 dc_th2) ; in full_simplify init_ss (meta_std th) end ; val _ = bind_thm ("dctxt_repeat", singleton_subsetI RS mk_gpcm sn_repeat RS transfer CRotate.thy dctxt.same) ; val _ = qed_goal_spec_mp "dctxt_repeat_eq" Msde.thy "(Xs, Y) : dctxt (nrulefs {sn_repeat}) --> Xs = [Y]" (fn _ => [ (rtac impI 1), (etac pair_dctxt_induct 1), ALLGOALS Clarsimp_tac, (clarsimp_tac (ces nrulefs.elims, esimps [sn_repeat]) 1) ]) ; val dc_repeat' = prove_goal Msde.thy dcstr (fn _ => [ rtac conjI 1, rtac (sn_repeat RS def_imp_eq) 1, (rtac impI 1), (dtac dctxt_repeat_eq 1), Clarify_tac 1, (REPEAT_ALL_NEW (resolve_tac [exI, conjI, refl_msde', ctxt.same, mk_gpcm sn_repeat, subset_refl]) 1) ]) ; val _ = bind_thm ("dc_repeat", refl RSN (2, meta_std (dc_repeat' RS conjunct2))) ; val dc_pl1_repeat = (mk_dc_Un dc_repeat dc_pl1) ; val dc_pl2_repeat = (mk_dc_Un dc_repeat dc_pl2) ; val dc_pr1_repeat = (mk_dc_Un dc_repeat dc_pr1) ; val dc_pr2_repeat = (mk_dc_Un dc_repeat dc_pr2) ; val _ = bind_thm ("dctxt_rpt_nes", singleton_subsetI RS mk_gpcm sn_rpt_nes RS transfer Msde.thy dctxt.same) ; val _ = bind_thm ("ctxt_rpt_nes", singleton_subsetI RS mk_gpcm sn_rpt_nes RS transfer Msde.thy ctxt.same) ; val _ = qed_goal_spec_mp "ctxt_rpt_nes_eq" Msde.thy "(Xs, Y) : ctxt (nrulefs {sn_rpt_nes}) --> Xs = [Y]" (fn _ => [ (rtac impI 1), (etac pair_ctxt_induct 1), ALLGOALS Clarsimp_tac, (clarsimp_tac (ces nrulefs.elims, esimps [sn_rpt_nes]) 1) ]) ; val _ = qed_goal_spec_mp "dctxt_rpt_nes_eq" Msde.thy "(Xs, Y) : dctxt (nrulefs {sn_rpt_nes}) --> Xs = [Y]" (fn _ => [ (rtac impI 1), (etac pair_dctxt_induct 1), ALLGOALS Clarsimp_tac, (clarsimp_tac (ces nrulefs.elims, esimps [sn_rpt_nes]) 1) ]) ; val dc_rpt_nes' = prove_goal Msde.thy dcstr (fn _ => [ rtac conjI 1, rtac (sn_rpt_nes RS def_imp_eq) 1, (rtac impI 1), (ftac dctxt_nested 1), (resolve_tac rfs_lrs_ns 1), (dtac dctxt_rpt_nes_eq 1), Clarsimp_tac 1, (etac nested_seqs.elim 1), hyp_subst_tac 1, (REPEAT_ALL_NEW (resolve_tac [exI, conjI, refl_msde', singletonI, ctxt_rpt_nes ]) 1) ]) ; val _ = bind_thm ("dc_rpt_nes", refl RSN (2, meta_std (dc_rpt_nes' RS conjunct2))) ; val dc_pl1_rpt_nes = (mk_dc_Un dc_rpt_nes dc_pl1) ; val dc_pl2_rpt_nes = (mk_dc_Un dc_rpt_nes dc_pl2) ; val dc_pr1_rpt_nes = (mk_dc_Un dc_rpt_nes dc_pr1) ; val dc_pr2_rpt_nes = (mk_dc_Un dc_rpt_nes dc_pr2) ; val gpstr = "c = ($ca => $cs) --> ([p], c) : ctxt (nrulefs {?sn_lr :: nested psc}) --> \ \ (c, c') : ms_deep_equiv --> ([c'], d') : nrulefs {?sn_rule} --> " ; val gcstr = "(EX p' q q' d. (p, p') : ms_deep_equiv & \ \ ([p'], q) : nrulefs {?sn_rule} & (q, q') : ms_deep_equiv & \ \ ([q'], d) : ctxt (nrulefs {?sn_lr}) & (d, d') : ms_deep_equiv)" ; val gc_lrs_str = "(EX p' q q' d. (p, p') : ms_deep_equiv & \ \ ([p'], q) : nrulefs {?sn_rule} & (q, q') : ms_deep_equiv & \ \ ([q'], d) : ctxt (nrulefs ?sn_lrsg) & (d, d') : ms_deep_equiv)" ; val gstr = gpstr ^ gcstr ; val gdcstr = "(EX p' q q' d. (p, p') : ms_deep_equiv & \ \ ([p'], q) : nrulefs {?sn_rule} & (q, q') : ms_deep_equiv & \ \ ([q'], d :: nested) : dctxt (nrulefs {?sn_lr}) & (d, d') : ms_deep_equiv)" ; val gdc_lrs_str = "(EX p' q q' d. (p, p') : ms_deep_equiv & \ \ ([p'], q) : nrulefs {?sn_rule} & (q, q') : ms_deep_equiv & \ \ ([q'], d :: nested) : dctxt (nrulefs ?sn_lrs) & (d, d') : ms_deep_equiv)" ; (* here, note how we have ctxt in the assumptions and dctxt in the conclusion, as this makes the proof easier *) val gdstr = gpstr ^ gdcstr ; val gd_lrs_str = gpstr ^ gdc_lrs_str ; fun dcoktacs dc_lr _ = [ Safe_tac, (dtac dc_lr 1), Safe_tac, (REPEAT_FIRST (resolve_tac [exI, conjI])), atac 4, atac 2, atac 1, (eatac trans_msde' 1 2), (eatac trans_msde' 1 1) ] ; fun mk_dcokthm dc_lr = prove_goal CRotate.thy (gdc_lrs_str ^ " --> " ^ gc_lrs_str) (dcoktacs dc_lr) RS mp ; (* val dcok_anda = mk_dcokthm dc_anda ; val dcok_ors = mk_dcokthm dc_ors ; val dcok_excla = mk_dcokthm dc_excla ; val dcok_lollis = mk_dcokthm dc_lollis ; val dcok_tA = mk_dcokthm dc_tA ; val dcok_fS = mk_dcokthm dc_fS ; val dcokthms = [dcok_anda, dcok_ors, dcok_excla, dcok_lollis, dcok_tA, dcok_fS]; *) val dcokthms = map mk_dcokthm dc_splrs ; (* val dcok_pl1 = mk_dcokthm dc_pl1 ; val dcok_pr1 = mk_dcokthm dc_pr1 ; val dcok_pl2 = mk_dcokthm dc_pl2 ; val dcok_pr2 = mk_dcokthm dc_pr2 ; val dcokpthms = [dcok_pl1, dcok_pr1, dcok_pl2, dcok_pr2] ; *) val dcokpthms = map mk_dcokthm dc_bprs ; (* val dcok_pl1_repeat = mk_dcokthm dc_pl1_repeat ; val dcok_pl2_repeat = mk_dcokthm dc_pl2_repeat ; val dcok_pr1_repeat = mk_dcokthm dc_pr1_repeat ; val dcok_pr2_repeat = mk_dcokthm dc_pr2_repeat ; val dcok_pl1_rpt_nes = mk_dcokthm dc_pl1_rpt_nes ; val dcok_pl2_rpt_nes = mk_dcokthm dc_pl2_rpt_nes ; val dcok_pr1_rpt_nes = mk_dcokthm dc_pr1_rpt_nes ; val dcok_pr2_rpt_nes = mk_dcokthm dc_pr2_rpt_nes ; val dcokprthms = [dcok_pl1_rpt_nes, dcok_pr1_rpt_nes, dcok_pl2_rpt_nes, dcok_pr2_rpt_nes] ; *) val dcokprthms = map mk_dcokthm [dc_pl1_rpt_nes, dc_pr1_rpt_nes, dc_pl2_rpt_nes, dc_pr2_rpt_nes] ; fun comb_msde (tha, thb) = let val thbe = mk_ext_msde thb ; val thaE = tacthm Safe_tac (tha RS exE) ; in tacthm (eatac thbe 2 2) thaE end ; val dc_g_ths as tha :: _ = ListPair.map comb_msde (map mk_dctxt_msde dn_pxxg_msde_ths, dc_pxxg_ths) ; val dc_pxxUng_ths = ListPair.map (uncurry mk_dc_Un) (dc_g_ths, [dc_pl1, dc_pr1, dc_pl1, dc_pr1]) ; val dcokpgthms = map mk_dcokthm dc_pxxUng_ths ; (* to solve eg ([$X,,, (A,,, B) => ($Y => $Z)], ?q) : nrulefs {sn_rp} second version where premise is the variable *) (* can often replace nrftacs by rtac (subset_refl RS mk_gpcm sn_rule) *) val nrftacs = [ (rtac nrulefs_find), (clarsimp_tac (cesimps sn_rule_defs)), (REPEAT o (EVERY' [ (rtac conjI), (clarsimp_tac (cesimps [nFind_def])), (rtac findf_match) ])), (clarsimp_tac (cesimps [nFind_def])), rtac refl ] ; val nrftacs' = [ (rtac nrulefs_find), (clarsimp_tac (cesimps sn_rule_defs)), rtac rev_conjI, (REPEAT o (EVERY' [ (rtac conjI), (clarsimp_tac (cesimps [nFind_def])), (rtac findf_match) ])), (clarsimp_tac (cesimps [nFind_def])), (rtac findf_match), (clarsimp_tac (cesimps [nFind_def])), rtac refl ] ; (* case where due to context, actual logical rule is hidden within one part *) fun hoptacs sn_rule = [ REPEAT o dtac keep_msdeI, (REPEAT_ALL_NEW (resolve_tac [exI, conjI])), perm_msde_tac, (* EVERY' nrftacs, *) (rtac (singleton_subsetI RS mk_gpcm sn_rule) THEN' solve_in), (* next step, no need for msde ; logical rule ; final msde *) (rtac refl_msde'), gctxt_mono_tac, perm_msde_tac, inc_ref_tac' case_count ] ; fun alt_hoptacs sn_rule = [ REPEAT o dtac keep_msdeI, (REPEAT_ALL_NEW (resolve_tac [exI, conjI])), perm_msde_tac, (* EVERY' nrftacs, *) (rtac (singleton_subsetI RS mk_gpcm sn_rule) THEN' solve_in), (* next step, no need for msde ; logical rule ; final msde *) (rtac refl_msde'), gctxt_mono_tac, perm_msde_tac, inc_ref_tac' case_count ] ; (* to solve, eg, ($Z,,, A &&& B => $U, ($X,,, A &&& B),,, $Y => $U) : ms_deep_equiv *) val cftacs = [ (rtac msde.seqs THEN' (rtac refl_msde' ORELSE' (rtac refl_msde' o incr))), (rtac msde.ms_of), (clarsimp_tac (cesimps [symmetric mins_def', symmetric mins_def, mins_commute, mins_assoc, mins_assoc_alt])), (rtac refl_mmsde_eq'), REPEAT o rtac mins_eqI, (resolve_tac [refl, ms_of_ns_NComma RS sym]), Clarsimp_tac THEN_ALL_NEW Force_tac (* !! *) ] ; fun initmpttacs sn_rule = [ (safe_tac (ces nrulefs.elims)), (* 8 subgoals *) (dtac (mkr sn_rule) 1), Clarsimp_tac 1, ((eresolve_tac [ctxt.elim, dctxt.elim] THEN_ALL_NEW Clarify_tac) 1) ] ; fun lrtctacs sn_rule sn_lr = [ (* logical rule in trivial context - alternative version *) (REPEAT o dtac keep_msdeI), (REPEAT_ALL_NEW (resolve_tac [exI, conjI])), perm_msde_tac, (* (EVERY' nrftacs), *) (rtac (subset_refl RS mk_gpcm sn_rule)), (resolve_tac [ctxt.same, dctxt.same] o incr), (rtac (singleton_subsetI RS mk_gpcm sn_lr) THEN' solve_in) o incr, (perm_msde_tac ORELSE' EVERY' [ (rtac trans_msde'), (perm_msde_tac o incr), (EVERY' cftacs) ]) o incr, (perm_msde_tac ORELSE' ((rtac msde.seqs THEN_ALL_NEW (TRY o rtac refl_msde') THEN_ALL_NEW EVERY' [ (rtac msde.ms_of), (rtac refl_mmsde_eq'), MSSG Simp_tac, Force_tac ] ))), inc_ref_tac' case_count ] ; fun cnstacs sn_rule sn_lr = [ (datac ctxt_nseq_lem 1), (clarsimp_tac (ces [nrulefs.elim], esimps [sn_lr])), TRY o (rtac pscs_nestedI), Clarify_tac, (datac (sym_msde' RS trans_msde' RS sym_msde') 1), ((etac ctxt.elim THEN_ALL_NEW Clarify_tac)), (EVERY' (alt_hoptacs sn_rule) o incr), (EVERY' (alt_hoptacs sn_rule) o incr), EVERY' (litacs sn_lr), EVERY' (lrtctacs sn_rule sn_lr) ] ; fun mpttacs sn_rule sn_lr _ = [ EVERY (initmpttacs sn_rule), EVERY' (litacs sn_lr) 1, nosg_tac 3 ORELSE EVERY' (lrtctacs sn_rule sn_lr) 1, (SOMEGOAL (EVERY' (hoptacs sn_rule))), EVERY' (cnstacs sn_rule sn_lr) 1 ] ; fun mk_permute_thm gstr tacs sn_rule sn_lr = prove_goal (the_context ()) gstr (tacs sn_rule sn_lr) ; fun mk_permute_thm' tacsf = prove_goal (the_context ()) tacsf ; (* could do these with gstr instead of gdstr *) (* don't need any of these system "date" ; (* 7 secs for 10 *) val p_rp_anda = mk_permute_thm gdstr mpttacs sn_rp sn_anda ; (* OK *) val p_drp_ors = mk_permute_thm gdstr mpttacs sn_drp sn_ors ; (* OK *) val p_drp_anda = mk_permute_thm gdstr mpttacs sn_drp sn_anda ; (* OK *) val p_rp_ors = mk_permute_thm gdstr mpttacs sn_rp sn_ors ; (* OK *) val p_drp_excla = mk_permute_thm gdstr mpttacs sn_drp sn_excla ; (* OK *) val p_rp_excla = mk_permute_thm gdstr mpttacs sn_rp sn_excla ; (* OK *) val p_drp_lollis = mk_permute_thm gdstr mpttacs sn_drp sn_lollis ; (* OK *) val p_rp_lollis = mk_permute_thm gdstr mpttacs sn_rp sn_lollis ; (* OK *) val p_drp_tA = mk_permute_thm gdstr mpttacs sn_drp sn_tA ; (* OK *) val p_rp_tA = mk_permute_thm gdstr mpttacs sn_rp sn_tA ; (* OK *) val p_drp_fS = mk_permute_thm gdstr mpttacs sn_drp sn_fS ; (* OK *) val p_rp_fS = mk_permute_thm gdstr mpttacs sn_rp sn_fS ; (* OK *) system "date" ; *) fun xalt_choptacs sn_rule sn_lr sg = [ Clarify_tac sg, ((REPEAT_DETERM o dtac keep_msdeI) sg), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) sg), (trans_perm2_msde_tac (sg+4)), ((gctxt_mono_tac ORELSE' gctxt_rule_tac (singleton_subsetI RS mk_gpcm sn_lr)) (sg+3)), (perm_msde_tac (sg+2)), (rtac (subset_refl RS mk_gpcm sn_rule) (sg+1)), (trans_safe_msde_tac sg), inc_ref_tac case_count ] ; fun alt_choptacs sn_rule sn_lr sg = [ Clarify_tac sg, ((REPEAT_DETERM o dtac keep_msdeI) sg), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) sg), DETERM (perm_msde_tac (sg+4)), ((gctxt_mono_tac ORELSE' gctxt_rule_tac (singleton_subsetI RS mk_gpcm sn_lr)) (sg+3)), (perm_msde_tac sg), (rtac (subset_refl RS mk_gpcm sn_rule) sg), (perm_msde_tac sg), inc_ref_tac case_count ] ; fun choptacs sn_rule sn_lr sg = [ Clarify_tac sg, ((REPEAT_DETERM o dtac keep_msdeI) sg), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) sg), DETERM (perm_msde_tac (sg+4)), ((gctxt_mono_tac ORELSE' gctxt_rule_tac (singleton_subsetI RS mk_gpcm sn_lr)) (sg+3)), (perm_msde_tac (sg+2)), (* (EVERY' nrftacs' (sg+1)), *) (rtac (subset_refl RS mk_gpcm sn_rule) (sg+1)), (perm_msde_tac ORELSE' EVERY' [ (rtac trans_msde'), (perm_msde_tac), (* why do we need this again ? *) (rtac trans_msde'), (perm_msde_tac), (EVERY' cftacs) ]) sg, inc_ref_tac case_count ] ; fun alt_lrtctacs sn_rule sn_lr = [ (* logical rule in trivial context - alternative version *) (REPEAT (dtac keep_msdeI 1)), (REPEAT_ALL_NEW (resolve_tac [exI, conjI]) 1), perm_msde_tac 5, (gctxt_rule_tac (subset_refl RS mk_gpcm sn_lr) 4), perm_msde_tac 3, (* (EVERY' nrftacs' 2), *) (rtac (subset_refl RS mk_gpcm sn_rule) 2), (rtac trans_msde' 1), (perm_msde_tac 1), rtac refl_msde' 1 ORELSE (EVERY' cftacs 1), inc_ref_tac case_count ] ; fun mpttacs_i sn_rule sn_lr _ = [ EVERY (initmpttacs sn_rule), EVERY' (litacs sn_lr) 1, (TRY (EVERY [ (* if the eresolve_tac works, two resulting subgoals, otherwise one *) ((eresolve_tac [Nsf_msde_commaE, Nsf_msde_comma_altE] THEN_ALL_NEW Clarify_tac) 1), EVERY (alt_lrtctacs sn_rule sn_lr) ])), EVERY (alt_lrtctacs sn_rule sn_lr), (SOMEGOAL (EVERY' (hoptacs sn_rule))), ((etac ctxt.elim THEN_ALL_NEW Clarify_tac) 1), (* level 7 *) ((etac msde_nseq_comE THEN_ALL_NEW (EVERY o choptacs sn_rule sn_lr)) 5), ((etac msde_nseq_comE THEN_ALL_NEW (EVERY o choptacs sn_rule sn_lr)) 4), (etac ctxt_nseqsE 3), ((resolve_tac rfs_lrs_ns) 3), (EVERY' (keep_trans_tacs trans_msde') 3), ((eatac nseq_msde_commaE 1 THEN_ALL_NEW (EVERY o choptacs sn_rule sn_lr)) 3), (etac ctxt_nseqs_altE 2), ((resolve_tac rfs_lrs_ns) 2), (EVERY' (keep_trans_tacs trans_msde') 2), ((eatac nseq_msde_comma_altE 1 THEN_ALL_NEW (EVERY o choptacs sn_rule sn_lr)) 2), EVERY' (litacs sn_lr) 1, ((etac msde_nseq_comE THEN_ALL_NEW (EVERY o choptacs sn_rule sn_lr)) 1) ] ; (* could do these with gstr instead of gdstr *) system "date" ; (* 17 secs for 10 *) val p_irp_anda = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_rp) sn_anda ; val p_idrp_ors = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_drp) sn_ors ; val p_irp_excla = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_rp) sn_excla ; val p_idrp_lollis = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_drp) sn_lollis ; val p_irp_tA = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_rp) sn_tA ; val p_idrp_fS = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_drp) sn_fS ; val p_idrp_anda = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_drp) sn_anda ; val p_irp_ors = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_rp) sn_ors ; val p_irp_lollis = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_rp) sn_lollis ; val p_idrp_excla = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_drp) sn_excla ; val p_idrp_tA = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_drp) sn_tA ; val p_irp_fS = mk_permute_thm gdstr mpttacs_i (mk_inv_def sn_rp) sn_fS ; system "date" ; val piths = [refl] RL map meta_std [ p_irp_anda, p_idrp_anda, p_irp_ors, p_idrp_ors, p_irp_lollis, p_idrp_lollis, p_irp_excla, p_idrp_excla, p_irp_tA, p_idrp_tA, p_irp_fS, p_idrp_fS ] RL dcokthms ; fun mpttacs_g sn_rule sn_lr _ = let val ectac = (EVERY o choptacs sn_rule sn_lr) ; in [ EVERY (initmpttacs sn_rule), EVERY' (litacs sn_lr) 1, (TRY ((REPEAT_ALL_NEW (eresolve_tac [Nsf_msde_commaE, Nsf_msde_comma_altE, msde_com_nseqE]) THEN_ALL_NEW Clarsimp_tac) 1)), (* following line for sn_anda' *) (etac msde_Nsf_comE THEN_ALL_NEW MSSG Clarsimp_tac) 1 ORELSE EVERY (alt_lrtctacs sn_rule sn_lr), (* OK *) (SOMEGOAL (EVERY' (hoptacs sn_rule))), ((etac ctxt.elim THEN_ALL_NEW Clarify_tac) 1), (* level 7 *) ((etac msde_nseq_comE THEN_ALL_NEW ectac) 5), ((etac msde_nseq_comE THEN_ALL_NEW ectac) 4), (etac ctxt_nseqsE 3), ((resolve_tac rfs_lrs_ns) 3), (EVERY' (keep_trans_tacs trans_msde') 3), (eatac nseq_msde_commaE 1 3), (ectac 4 ORELSE ectac 3), (clarify_tac (ces nested_seqs.elims) 3) , ((etac msde_com_nseqE THEN_ALL_NEW clarsimp_tac (cesimps msde_equivs)) 3), ((etac ctxt.elim THEN_ALL_NEW Clarify_tac) 3), ectac 5, ectac 4, (etac ctxt_nseqs_altE 2), ((resolve_tac rfs_lrs_ns) 2), (EVERY' (keep_trans_tacs trans_msde') 2), (eatac nseq_msde_comma_altE 1 2), (ectac 3 ORELSE ectac 2), (clarify_tac (ces nested_seqs.elims) 2) , ((etac msde_com_nseqE THEN_ALL_NEW clarsimp_tac (cesimps msde_equivs)) 2), ((etac ctxt.elim THEN_ALL_NEW Clarify_tac) 2), ectac 4, ectac 3, (TRYALL (EVERY' (litacs sn_lr))), (etac msde_nseqLD1E' 1), (Clarsimp_tac 1), ectac 1, (ALLGOALS (eresolve_tac [Nseq_msde_comma_alt_symE, Nseq_msde_comma_symE] THEN_ALL_NEW ectac)) ] end ; (* don't need any of these system "date" ; (* 45 secs for 10 TODO examine why so much slower *) val p_gl_anda = mk_permute_thm gdstr mpttacs_g sn_gl sn_anda ; (* OK *) val p_gr_anda = mk_permute_thm gdstr mpttacs_g sn_gr sn_anda ; (* OK *) val p_gl_ors = mk_permute_thm gdstr mpttacs_g sn_gl sn_ors ; (* OK *) val p_gr_ors = mk_permute_thm gdstr mpttacs_g sn_gr sn_ors ; (* OK *) val p_gl_lollis = mk_permute_thm gdstr mpttacs_g sn_gl sn_lollis ; (* OK *) val p_gr_lollis = mk_permute_thm gdstr mpttacs_g sn_gr sn_lollis ; (* OK *) val p_gl_excla = mk_permute_thm gdstr mpttacs_g sn_gl sn_excla ; (* OK *) val p_gr_excla = mk_permute_thm gdstr mpttacs_g sn_gr sn_excla ; (* OK *) val p_gl_tA = mk_permute_thm gdstr mpttacs_g sn_gl sn_tA ; (* OK *) val p_gr_tA = mk_permute_thm gdstr mpttacs_g sn_gr sn_tA ; (* OK *) val p_gl_fS = mk_permute_thm gdstr mpttacs_g sn_gl sn_fS ; (* OK *) val p_gr_fS = mk_permute_thm gdstr mpttacs_g sn_gr sn_fS ; (* OK *) *) system "date" ; (* simpler rules, but proofs no easier but note, ctxt (sn_anda') does NOT include all of ctxt (sn_anda)! val p_gl_anda' = mk_permute_thm gdstr mpttacs_g sn_gl sn_anda' ; (* OK *) val p_gr_anda' = mk_permute_thm gdstr mpttacs_g sn_gr sn_anda' ; (* OK *) val p_gl_ors' = mk_permute_thm gdstr mpttacs_g sn_gl sn_ors' ; (* OK *) val p_gr_ors' = mk_permute_thm gdstr mpttacs_g sn_gr sn_ors' ; (* OK *) val p_gl_lollis' = mk_permute_thm gdstr mpttacs_g sn_gl sn_lollis' ; (* OK *) val p_gr_lollis' = mk_permute_thm gdstr mpttacs_g sn_gr sn_lollis' ; (* OK *) val p_gl_excla' = mk_permute_thm gdstr mpttacs_g sn_gl sn_excla' ; (* OK *) val p_gr_excla' = mk_permute_thm gdstr mpttacs_g sn_gr sn_excla' ; (* OK *) val p_gl_tA' = mk_permute_thm gdstr mpttacs_g sn_gl sn_tA' ; (* OK *) val p_gr_tA' = mk_permute_thm gdstr mpttacs_g sn_gr sn_tA' ; (* OK *) val p_gl_fS' = mk_permute_thm gdstr mpttacs_g sn_gl sn_fS' ; (* OK *) val p_gr_fS' = mk_permute_thm gdstr mpttacs_g sn_gr sn_fS' ; (* OK *) system "date" ; *) (* now for ig and eg, same tactics work! *) val p_ig_anda = mk_permute_thm gdstr mpttacs_g sn_ig sn_anda ; (* OK *) val p_eg_anda = mk_permute_thm gdstr mpttacs_g sn_eg sn_anda ; (* OK *) val p_ig_ors = mk_permute_thm gdstr mpttacs_g sn_ig sn_ors ; (* OK *) val p_eg_ors = mk_permute_thm gdstr mpttacs_g sn_eg sn_ors ; (* OK *) val p_ig_lollis = mk_permute_thm gdstr mpttacs_g sn_ig sn_lollis ; (* OK *) val p_eg_lollis = mk_permute_thm gdstr mpttacs_g sn_eg sn_lollis ; (* OK *) val p_ig_excla = mk_permute_thm gdstr mpttacs_g sn_ig sn_excla ; (* OK *) val p_eg_excla = mk_permute_thm gdstr mpttacs_g sn_eg sn_excla ; (* OK *) val p_ig_tA = mk_permute_thm gdstr mpttacs_g sn_ig sn_tA ; (* OK *) val p_eg_tA = mk_permute_thm gdstr mpttacs_g sn_eg sn_tA ; (* OK *) val p_ig_fS = mk_permute_thm gdstr mpttacs_g sn_ig sn_fS ; (* OK *) val p_eg_fS = mk_permute_thm gdstr mpttacs_g sn_eg sn_fS ; (* OK *) val piegths = [refl] RL map meta_std [ p_ig_anda, p_eg_anda, p_ig_ors, p_eg_ors, p_ig_lollis, p_eg_lollis, p_ig_excla, p_eg_excla, p_ig_tA, p_eg_tA, p_ig_fS, p_eg_fS ] RL dcokthms ; system "date" ; (* simpler rules, but proofs no easier but note, ctxt (sn_anda') does NOT include all of ctxt (sn_anda)! val p_ig_anda' = mk_permute_thm gdstr mpttacs_g sn_ig sn_anda' ; (* OK *) val p_eg_anda' = mk_permute_thm gdstr mpttacs_g sn_eg sn_anda' ; (* OK *) val p_ig_ors' = mk_permute_thm gdstr mpttacs_g sn_ig sn_ors' ; (* OK *) val p_eg_ors' = mk_permute_thm gdstr mpttacs_g sn_eg sn_ors' ; (* OK *) val p_ig_lollis' = mk_permute_thm gdstr mpttacs_g sn_ig sn_lollis' ; (* OK *) val p_eg_lollis' = mk_permute_thm gdstr mpttacs_g sn_eg sn_lollis' ; (* OK *) val p_ig_excla' = mk_permute_thm gdstr mpttacs_g sn_ig sn_excla' ; (* OK *) val p_eg_excla' = mk_permute_thm gdstr mpttacs_g sn_eg sn_excla' ; (* OK *) val p_ig_tA' = mk_permute_thm gdstr mpttacs_g sn_ig sn_tA' ; (* OK *) val p_eg_tA' = mk_permute_thm gdstr mpttacs_g sn_eg sn_tA' ; (* OK *) val p_ig_fS' = mk_permute_thm gdstr mpttacs_g sn_ig sn_fS' ; (* OK *) val p_eg_fS' = mk_permute_thm gdstr mpttacs_g sn_eg sn_fS' ; (* OK *) system "date" ; *) (* can be convenient to save screen space by (REPEAT_SOME (ematch_tac [keepF_thin])) ; by prune_params_tac ; *)