structure calks = struct val thy = theory "calks" end ; use_legacy_bindings calks.thy ; (* use the additive cut rule *) val lksss_car_der = [transfer calks.thy car_der, lksss_double_eqv] MRS trans ; val () = qed_goal "lks_cas_cap" calks.thy "((X |- mins A Y, mins A X |- Y): cas lksss A) = ((X |- Y): cap lksss A)" (fn _ => [ (simp_tac (esimps [cas_eq, car_eq, cap_eq, mins_def, lksss_double_eqv]) 1) ]) ; (* applying l/rcg_gen_step to logical intro rules *) val _ = bind_thm ("rcg_ir_lksne'", tacsthm [ use_sg_tac, atac 1, etac lksir_no_antec 1, (TRYALL (etac thin_rl)) ] ([wk_adm_extrs, extrs_ir_lksne] MRS transfer calks.thy rcg_gen_step)) ; val _ = bind_thm ("lcg_il_lksne'", tacsthm [ use_sg_tac, atac 1, etac lksil_no_antec 1, (TRYALL (etac thin_rl)) ] ([wk_adm_extrs, extrs_il_lksne] MRS transfer calks.thy lcg_gen_step)) ; val [lcg_il_lksne, rcg_ir_lksne] = map (simpUV o simpWZ) [lcg_il_lksne', rcg_ir_lksne'] ; (* ; val prems = it ; *) (* note - proof of lcstep and rcstep does not depend on the actual rules, only the link between lkne and lkss, expressed in lkss.extI *) fun mk_lksne th = rewrite_rule [mk_eq (lksss_extrs RS sym)] (read_instantiate_sg calks.thy [("rls", "lksne")] th) ; fun mk_step' th = full_simplify (esimps [extend_def]) (refl RSN (3, th)) ; val lcstep' = mk_step' (mk_lksne slcgstep) ; val rcstep' = mk_step' (mk_lksne srcgstep) ; (* ; val prems = it ; *) val ths = (single_eq_single RS iffD1 RS revcut_rl) :: ([hd prod.inject, sequent.inject] RL [iffD1 RS conjE]) ; val [cas_axl, cas_axr] = [[lksss_wk_adm], [lksne.axiom RS in_extrs RS (lksss_extrs RS set_cong RS iffD2)]] MRL map (transfer calks.thy) [gen_cas_axl, gen_cas_axr] ; val [car_axl, car_axr] = map (tacthm (TRYALL (match_tac [lks_axd]))) ([cas_axl, cas_axr] RL [cas_car]) ; val car_axl' = rewrite_rule [mins_def'] car_axl ; val car_axr' = rewrite_rule [mins_def'] car_axr ; fun tacC8g cf X Y = [ (forw_inst_tac [("x", cf)] spec), (etac impE), (resolve_tac ipsfIs), (eres_inst_tac [("xa", X), ("x", Y)] allE2), (etac impE), (rtac conjI THEN_ALL_NEW (TRY o atac) THEN_ALL_NEW (eatac wk_admD_alt 1 THEN' (force_tac (cesimps ([mins_def, extend_def] @ union_ac))))) ] ; (* simpler version of prstep goes with simpler rules (where principal formula not copied into conclusion), note: could enlarge lksss - see calkx.ML *) val gprstep' = prove_goal calks.thy "wk_adm drls --> \ \ (ps, {#} |- {#A#}) : lksir & (qs, {#A#} |- {#}) : lksil & \ \ pse = map (extend (X |- Y)) ps & qse = map (extend (X |- Y)) qs & \ \ set pse Un set qse <= derrec drls {} & \ \ (ALL sfa X Y. (sfa, A) : ipsubfml --> \ \ (X |- Y) : cap drls sfa) --> (X |- Y) : cap drls A" (fn _ => [ Safe_tac, (etac lksil.elims 1), (ALLGOALS (etac lksir.elims)), (ALLGOALS (REPEAT o eresolve_tac ths)), (ALLGOALS (eresolve_tac ([[sym],[sym]] MRL fc2Es) THEN' atac)), (* avoid the following until most subgoals removed *) Safe_tac, (ALLGOALS (full_simp_tac (esimps [cap_eq, extend_def]))), Safe_tac, (* level 8 *) (EVERY' (tacC8g "Aa" "mins Ba X" "Y") 1), (EVERY' (tacC8g "Ba" "X" "Y") 1), atac 1, (EVERY' (tacC8g "Aa" "X" "mins Ba Y") 1), (EVERY' (tacC8g "Ba" "X" "Y") 1), atac 1, (EVERY' (tacC8g "Aa" "X" "Y") 1), atac 1, (EVERY' (tacC8g "Aa" "X" "mins Ba Y") 1), (EVERY' (tacC8g "Ba" "X" "Y") 1), atac 1 ]) RS mp RS mp ; val sprstep' = lksss_wk_adm RS gprstep' ; fun tacC8q cf {Xl, Yl, Xr, Yr} = [ (forw_inst_tac [("x", cf)] spec), (etac impE), (resolve_tac ipsfIs), (eres_inst_tac [("xa", Xl), ("x", Yl)] allE2), (eres_inst_tac [("xa", Xr), ("x", Yr)] allE2), (etac impE), (rtac conjI THEN_ALL_NEW full_simp_tac (esimps ([mins_def] @ union_ac))) ] ; val lksss_cwd = [lksss_ctr_adm, lksss_wk_adm] MRS (ballI RS ctr_wk_le_double) ; val cwd = reop (fn [a,b,c,d] => [c,b,a,d]) (tacthm (etac thin_rl 1) (ballI RS ctr_wk_le_double)) ; val gprstep_q' = prove_goal calks.thy "All (ctr_adm drls) --> wk_adm drls --> \ \ (ps, {#} |- {#A#}) : lksir & (qs, {#A#} |- {#}) : lksil & \ \ pse = map (extend (Xl |- Yl)) ps & qse = map (extend (Xr |- Yr)) qs & \ \ set pse Un set qse <= derrec drls {} & \ \ (ALL sfa Xl Yl Xr Yr. (sfa, A) : ipsubfml --> \ \ (Xl |- Yl, Xr |- Yr) : caq drls sfa) --> \ \ (Xl |- Yl, Xr |- Yr) : caq drls A" (fn _ => [ Safe_tac, (etac lksil.elims 1), (ALLGOALS (etac lksir.elims)), (ALLGOALS (REPEAT o eresolve_tac ths)), (ALLGOALS (eresolve_tac ([[sym],[sym]] MRL fc2Es) THEN' atac)), (* avoid the following until most subgoals removed *) Safe_tac, (ALLGOALS (full_simp_tac (esimps [caq_eq, extend_def]))), Safe_tac, (* level 8 *) (EVERY' (tacC8q "Ba" {Xl = "mins Aa Xl", Yl = "Yl", Xr = "Xr", Yr = "Yr"}) 4), (EVERY' (tacC8q "Aa" {Xl = "Xr", Yl = "Yr", Xr = "Xl + Xr", Yr = "Yl + Yr"}) 4), (EVERY' (tacC8q "Aa" {Xl = "Xr", Yl = "Yr", Xr = "Xl", Yr = "Yl"}) 3), (EVERY' (tacC8q "Aa" {Xl = "Xl", Yl = "mins Ba Yl", Xr = "Xr", Yr = "Yr"}) 2), (EVERY' (tacC8q "Ba" {Xr = "Xr", Yr = "Yr", Xl = "Xl + Xr", Yl = "Yl + Yr"}) 2), (EVERY' (tacC8q "Aa" {Xl = "Xl", Yl = "Yl", Xr = "mins Ba Xr", Yr = "Yr"}) 1), (EVERY' (tacC8q "Ba" {Xl = "Xl", Yl = "Yl", Xr = "Xl + Xr", Yr = "Yl + Yr"}) 1), (TRYALL (EVERY' [(chop_last o etac cwd), atac, etac spec, (simp_tac (esimps union_ac addsimprocs pmgsps)) ])) ]) RS mp RS mp RS mp ; val sprstep_q' = lksss_ctr_adm RS ([allI, lksss_wk_adm] MRS gprstep_q') ; val gptacs = [ (rtac drs.derI), (REPEAT o (dresolve_tac lksne.intros)), (etac subsetD), (etac extrs.I), (* backtracking needed here *) Simp_tac, (rtac conjI), (etac sym), (MSSG (simp_tac (esimps [mins_def, extend_def]))), (asm_full_simp_tac (esimps [drs.all]))] ; val gprstep'' = meta_std (prove_goal calks.thy "wk_adm drls --> ?Q --> extrs lksne <= drls --> (X |- Y) : derrec drls {}" (fn _ => [ (strip_tac 1), (rtac cap_der 1), (eatac gprstep' 1 1), Safe_tac, (PRIMITIVE (fst o freeze_thaw o standard)), (REPEAT (EVERY' gptacs 1)) ])) ; val gprstep_q'' = meta_std (prove_goal calks.thy "All (ctr_adm drls) --> wk_adm drls --> ?Q --> extrs lksne <= drls --> \ \ (Xl + Xr |- Yl + Yr) : derrec drls {}" (fn _ => [ (strip_tac 1), (rtac caq_der 1), (eatac gprstep_q' 2 1), Safe_tac, (PRIMITIVE (fst o freeze_thaw o standard)), (REPEAT (EVERY' gptacs 1)) ])) ; val gprstep_q = standard (full_simplify (HOL_ss addsimps [cas_caq RS sym]) gprstep_q'') ; val sprstep'' = tacsthm [ LASTGOAL (rtac (lksss_extrs RS equalityD2)), rtac lksss_wk_adm 1] gprstep'' ; val sprstep = standard (full_simplify (HOL_ss addsimps [lks_cas_cap RS sym]) (sprstep'' RS (lksss_car_der RS iffD2))) ; val sprstep_q = standard (tacsthm [ LASTGOAL (rtac (lksss_extrs RS equalityD2)), rtac allI 1, rtac lksss_ctr_adm 1, rtac lksss_wk_adm 1] gprstep_q) ; val _ = qed_goalw_spec_mp "gen_lksne_c8sg" calks.thy [c8sg_prop_def] "All (ctr_adm drls) --> wk_adm drls --> extrs lksne <= drls --> \ \ c8sg_prop ipsubfml lksne drls A" (fn _ => [ (safe_tac (ces [lksne.elims])), (* case of id rules in lksne get eliminated because wrong form *) (ALLGOALS (clarsimp_tac (cesimps [extend_def]))), (TRYALL (rtac (car_eq' RS iffD2))), (TRYALL (MSSG (clarify_tac (ces (lks_concl_ilrcEs @ single_not_zeroEs))))), rewtac Zero_multiset_def, (rtac gprstep_q 1), (TRYALL (rtac refl)), (TRYALL atac), TRYALL Asm_simp_tac ]) ; val gen_lksne_c8 = gen_lksne_c8sg RS c8sg_ger ; val lksss_c8sg = [lksss_ctr_adm, lksss_wk_adm, lksss_extrs RS equalityD2] MRS (allI RS gen_lksne_c8sg) ; val lksne_c8sg = rewrite_rule [lksss_def] lksss_c8sg ; val lks_scas_all' = [wf_ipsubfml, lksne_c8sg, lksne_ctr_adm, lks_iscrls, lksne.axiom] MRS tacthm (TRYALL (rtac allI)) (transfer calks.thy gen_scas_all) ; val lks_scas_all = fold_rule [lksss_def] lks_scas_all' ; (* this could be part of an alternative approach *) val tacC8_simplef = tacC8_simplef' ipsfIs ; val tacC8 = tacC8' ipsfIs ; fun tacC8_slk cf = tacC8_simplef [transfer calks.thy lksss_double] cf ; fun tacC8s cf sl sr = EVERY' (tacC8 cf sl sr) THEN' full_simp_tac (spsimpsf ()) ; val _ = qed_goalw "lks_c8" calks.thy [c8ger_prop_def] "c8ger_prop ipsubfml lksss A (lksil Un lksir)" (fn _ => [ (safe_tac (ces ([lksir.elims, lksil.elims] @ single_not_emptyEs))), (ALLGOALS (datac single_ms_trans 1)), (ALLGOALS (eresolve_tac fcEs)), (safe_tac (cds [single_eq_single RS iffD1])), (ALLGOALS Full_simp_tac), (EVERY' (tacC8_slk "Aa") 3), (tacC8s "Aa" "X |- {#Aa#} + Y" "{#Aa#} + {#Ba#} + X |- Y" 1), (tacC8s "Ba" "X |- Y + {#Ba#}" "X + (X + {#Ba#}) |- Y + Y" 1), (tacC8s "Aa" "X |- {#Aa#} + {#Ba#} + Y" "{#Aa#} + X |- Y" 2), (tacC8s "Ba" "X + X |- Y + (Y + {#Ba#})" "X + {#Ba#} |- Y" 2), (tacC8s "Aa" "X |- {#Aa#} + Y" "{#Aa#} + X |- {#Ba#} + Y" 3), (tacC8s "Ba" "X + X |- Y + (Y + {#Ba#})" "X + {#Ba#} |- Y" 3), (ALLGOALS (chop_last o dtac lksss_singles)), (ALLGOALS (rtac (lksss_singles_iff RS iffD1))), (ALLGOALS Clarsimp_tac) ]) ;