Skip to content

Commit 716002e

Browse files
jvanbrueggejvanbruegge
committed
Automate recursive mrsbnf
1 parent d5ef4d0 commit 716002e

File tree

3 files changed

+129
-9
lines changed

3 files changed

+129
-9
lines changed

‎Tools/mrsbnf_def.ML‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -889,10 +889,7 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
889889
val free_fs = take free free_fs';
890890

891891
val free_prems = map (HOLogic.mk_Trueprop o mk_supp_bound) free_fs;
892-
val live_fs' = filter (member (op=) lives o domain_type o fastype_of) live_fs;;
893-
894-
val _ = @{print} (MRBNF_Def.frees_of_mrbnf mrbnf, MRBNF_Def.bounds_of_mrbnf mrbnf, MRBNF_Def.lives_of_mrbnf mrbnf)
895-
val _ = @{print} (Fs, Bs, As)
892+
val live_fs' = filter (member (op=) lives o domain_type o fastype_of) live_fs;
896893

897894
val map_is_Sb = fold_rev Logic.all (free_fs @ live_fs') (fold_rev (curry Logic.mk_implies) free_prems (mk_Trueprop_eq (
898895
Term.list_comb (Term.subst_atomic_types (filter_out (member (op=) lives o snd) (As' ~~ As)) mapx, MRBNF_Def.interlace
@@ -915,7 +912,6 @@ fun mk_mrsbnf_axioms mrbnfs bmv lthy =
915912
) Injs)
916913
) end
917914
)));
918-
val _ = @{print} (Thm.cterm_of lthy map_is_Sb)
919915

920916
val RVrs_aTs = map (HOLogic.dest_setT o body_type o fastype_of) RVrs;
921917

‎Tools/tvsubst.ML‎

Lines changed: 126 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ sig
2626
};
2727

2828
val create_tvsubst_of_mrsbnf: (binding -> binding) -> MRBNF_FP_Def_Sugar.fp_result
29-
-> MRSBNF_Def.mrsbnf -> binding
29+
-> MRSBNF_Def.mrsbnf -> MRBNF_Def.mrbnf -> thm -> binding
3030
-> (Proof.context -> tactic) eta_model option list -> string -> local_theory
3131
-> tvsubst_result list * local_theory
3232
end
@@ -279,7 +279,7 @@ fun define_tvsubst_consts qualify (fp_res : MRBNF_FP_Def_Sugar.fp_result) (etas
279279

280280
in (defs, lthy) end;
281281

282-
fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf tvsubst_b models QREC_fixed_name no_defs_lthy =
282+
fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor tvsubst_b models QREC_fixed_name no_defs_lthy =
283283
let
284284
val (fp_res, mrsbnf, etas, lthy) = prove_model_axioms fp_res mrsbnf models no_defs_lthy;
285285

@@ -1597,7 +1597,130 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf tvsubst_b models QREC_fixed_n
15971597
}]
15981598
} lthy;
15991599

1600-
val _ = @{print} bmv
1600+
val rec_mrbnf =
1601+
let
1602+
val tyenv = Sign.typ_match (Proof_Context.theory_of lthy)
1603+
(MRBNF_Def.T_of_mrbnf rec_mrbnf, #T quot) Vartab.empty
1604+
in MRBNF_Def.morph_mrbnf (MRBNF_Util.subst_typ_morphism (
1605+
map (fn (n, (s, T)) => (TVar (n, s), T)) (Vartab.dest tyenv)
1606+
)) rec_mrbnf end;
1607+
1608+
val rec_bmv_facts = BMV_Monad_Def.leader BMV_Monad_Def.facts_of_bmv_monad bmv;
1609+
1610+
val (rec_mrsbnf, lthy) = MRSBNF_Def.mrsbnf_def (K BNF_Def.Dont_Note) qualify NONE
1611+
(rec_mrbnf :: tl (MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf)) rec_bmv
1612+
(map (fn i => if i <> 0 then
1613+
let val axioms = nth (MRSBNF_Def.axioms_of_mrsbnf mrsbnf) i;
1614+
in {
1615+
map_Injs = Option.map (map (fn thm => fn ctxt => rtac ctxt thm 1)) (#map_Injs axioms),
1616+
map_Sb = Option.map (fn thm =>
1617+
fn ctxt => HEADGOAL (rtac ctxt thm THEN_ALL_NEW assume_tac ctxt)
1618+
) (#map_Sb axioms),
1619+
map_is_Sb = fn ctxt => HEADGOAL (rtac ctxt (#map_is_Sb axioms) THEN_ALL_NEW assume_tac ctxt),
1620+
set_Sb = map (fn thm => fn ctxt => rtac ctxt thm 1) (#set_Sb axioms),
1621+
set_Vrs = map (fn thm => fn ctxt => rtac ctxt thm 1) (#set_Vrs axioms)
1622+
} end
1623+
else {
1624+
map_Injs = NONE,
1625+
map_Sb = NONE,
1626+
map_is_Sb = fn ctxt => EVERY1 [
1627+
rtac ctxt ext,
1628+
Subgoal.FOCUS_PARAMS (fn {context=ctxt, params, ...} =>
1629+
let val (fs, t) = split_last (map (Thm.term_of o snd) params);
1630+
in rtac ctxt (infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt o mk_imsupp) fs @
1631+
[NONE, SOME (Thm.cterm_of ctxt t)]
1632+
) fresh_induct) 1 end
1633+
) ctxt,
1634+
REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt (@{thms imsupp_supp_bound[THEN iffD2] infinite_UNIV})),
1635+
REPEAT_DETERM_N netas o rtac ctxt @{thm case_split[rotated]},
1636+
rtac ctxt sym,
1637+
rtac ctxt trans,
1638+
rtac ctxt (Drule.rotate_prems (~netas) tvsubst_not_isInj),
1639+
REPEAT_DETERM o assume_tac ctxt,
1640+
REPEAT_DETERM_N (length rho_prems' + nvars + 1) o SELECT_GOAL (REPEAT_DETERM (FIRST1 [
1641+
assume_tac ctxt,
1642+
resolve_tac ctxt (@{thms IImsupp_Inj_comp_bound injI} @ maps (the_default []) FVars_Injs
1643+
@ maps (flat o #Vrs_Injss) (BMV_Monad_Def.axioms_of_bmv_monad rec_bmv)
1644+
),
1645+
eresolve_tac ctxt (map (fn thm => thm RS iffD1) (maps #Inj_inj (BMV_Monad_Def.facts_of_bmv_monad rec_bmv))),
1646+
EqSubst.eqsubst_tac ctxt [0] (@{thms IImsupp_Inj_comp SSupp_Inj_comp IImsupp_def comp_apply UN_empty2 Un_empty_left Un_empty_right}
1647+
@ maps (flat o #Vrs_Injss) (BMV_Monad_Def.axioms_of_bmv_monad rec_bmv)
1648+
)
1649+
])),
1650+
rtac ctxt sym,
1651+
rtac ctxt trans,
1652+
rtac ctxt vvsubst_ctor,
1653+
REPEAT_DETERM o assume_tac ctxt,
1654+
rtac ctxt sym,
1655+
SUBGOAL (fn (t, i) =>
1656+
let
1657+
fun strip_all (Const (@{const_name Pure.all}, _) $ Abs (x, T, t)) = apfst (cons (x, T)) (strip_all t)
1658+
| strip_all t = ([], t)
1659+
val ctor = fst (Term.dest_comb (fst (HOLogic.dest_eq (
1660+
HOLogic.dest_Trueprop (snd (Logic.strip_horn (snd (strip_all t))))
1661+
))));
1662+
in rtac ctxt (mk_arg_cong lthy 1 ctor) i end
1663+
),
1664+
SELECT_GOAL (Local_Defs.unfold0_tac ctxt [the (#Map_map mrsbnf_facts) RS sym]),
1665+
rtac ctxt trans,
1666+
rtac ctxt (@{thm trans[OF comp_apply[symmetric]]} OF [
1667+
#map_is_Sb mrsbnf_axioms RS sym RS fun_cong
1668+
]),
1669+
REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt @{thm supp_id_bound}),
1670+
rtac ctxt sym,
1671+
rtac ctxt (MRBNF_Def.map_cong0_of_mrbnf mrbnf),
1672+
REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id}),
1673+
REPEAT_DETERM o (rtac ctxt refl ORELSE' EVERY' [
1674+
SELECT_GOAL (Local_Defs.unfold0_tac ctxt (#set_Vrs mrsbnf_axioms)),
1675+
EqSubst.eqsubst_asm_tac ctxt [0] (map_filter (Option.map (#eta_compl_free o #axioms)) defs),
1676+
rtac ctxt allI,
1677+
rotate_tac ~1,
1678+
etac ctxt @{thm contrapos_nn},
1679+
SELECT_GOAL (Local_Defs.unfold0_tac ctxt (flat (map_filter (Option.map (fn def =>
1680+
[snd (#isInj def), snd (#Inj def)]
1681+
)) defs))),
1682+
hyp_subst_tac ctxt,
1683+
rtac ctxt exI,
1684+
rtac ctxt refl,
1685+
etac ctxt @{thm emptyE}
1686+
]),
1687+
REPEAT_DETERM o Goal.assume_rule_tac ctxt,
1688+
EVERY' (map_filter (Option.map (fn def => EVERY' [
1689+
SELECT_GOAL (Local_Defs.unfold0_tac ctxt [snd (#isInj def)]),
1690+
etac ctxt exE,
1691+
rotate_tac ~1,
1692+
etac ctxt @{thm subst[OF sym]},
1693+
rtac ctxt sym,
1694+
rtac ctxt trans,
1695+
resolve_tac ctxt (map_filter I tvsubst_Injs),
1696+
REPEAT_DETERM_N (length rho_prems') o SELECT_GOAL (REPEAT_DETERM (FIRST1 [
1697+
assume_tac ctxt,
1698+
resolve_tac ctxt (@{thms IImsupp_Inj_comp_bound injI} @ maps (the_default []) FVars_Injs
1699+
@ maps (flat o #Vrs_Injss) (BMV_Monad_Def.axioms_of_bmv_monad rec_bmv)
1700+
),
1701+
eresolve_tac ctxt (map (fn thm => thm RS iffD1) (maps #Inj_inj (BMV_Monad_Def.facts_of_bmv_monad rec_bmv))),
1702+
EqSubst.eqsubst_tac ctxt [0] (@{thms IImsupp_Inj_comp SSupp_Inj_comp IImsupp_def comp_apply UN_empty2 Un_empty_left Un_empty_right}
1703+
@ maps (flat o #Vrs_Injss) (BMV_Monad_Def.axioms_of_bmv_monad rec_bmv)
1704+
)
1705+
])),
1706+
REPEAT_DETERM o EqSubst.eqsubst_tac ctxt [0] (@{thms comp_apply} @ [snd (#Inj def)]),
1707+
rtac ctxt sym,
1708+
rtac ctxt trans,
1709+
rtac ctxt vvsubst_ctor,
1710+
REPEAT_DETERM o assume_tac ctxt,
1711+
REPEAT_DETERM o EVERY' [
1712+
SELECT_GOAL (Local_Defs.unfold0_tac ctxt (snd (#noclash quot) :: maps (the_default []) eta_set_emptiess)),
1713+
REPEAT_DETERM1 o resolve_tac ctxt @{thms Int_empty_left conjI}
1714+
],
1715+
rtac ctxt (arg_cong OF [Local_Defs.unfold0 ctxt @{thms comp_def} (#eta_natural (#axioms def) RS fun_cong)]),
1716+
REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id})
1717+
])) defs)
1718+
],
1719+
set_Sb = [],
1720+
set_Vrs = replicate nvars (fn ctxt => rtac ctxt refl 1)
1721+
}) (0 upto length ops - 1)) lthy;
1722+
1723+
val _ = @{print} rec_mrsbnf
16011724

16021725
(*
16031726
val results = @{map 6} (fn tvsubst => fn defs => fn tvsubst_VVrs => fn tvsubst_not_isVVr => fn VVrs' => fn tvsubst_permute => {

‎operations/BMV_Fixpoint.thy‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1550,11 +1550,12 @@ let
15501550
15511551
val fp_res = the (MRBNF_FP_Def_Sugar.fp_result_of lthy @{type_name FTerm})
15521552
val mrsbnf = the (MRSBNF_Def.mrsbnf_of lthy @{type_name FTerm_pre})
1553+
val mrbnf = the (MRBNF_Def.mrbnf_of lthy @{type_name FTerm});
15531554
15541555
open BNF_Util
15551556
15561557
val x = TVSubst.create_tvsubst_of_mrsbnf
1557-
I fp_res mrsbnf @{binding tvsubst_FTerm'} [SOME {
1558+
I fp_res mrsbnf mrbnf @{thm FTerm.vvsubst_cctor} @{binding tvsubst_FTerm'} [SOME {
15581559
eta = @{term "\<eta> :: 'v::var \<Rightarrow> ('tv::var, 'v::var, 'a::var, 'b::var, 'c, 'd) FTerm_pre"},
15591560
Inj = (@{term "Var :: 'v \<Rightarrow> ('tv::var, 'v::var) FTerm"}, @{thm Var_def}),
15601561
tacs = {

0 commit comments

Comments
 (0)