Skip to content

Commit 18f8987

Browse files
jvanbrueggejvanbruegge
committed
Get mrsbnf composition to work
1 parent 345a7a6 commit 18f8987

File tree

4 files changed

+129
-44
lines changed

4 files changed

+129
-44
lines changed

‎Tools/bmv_monad_def.ML‎

Lines changed: 67 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1532,9 +1532,9 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
15321532
val (x, _) = names_lthy
15331533
|> apfst hd o mk_Frees "x" [leader ops_of_bmv_monad outer];
15341534

1535-
val new_Injs = filter (member (op=) frees o domain_type o fastype_of) (
1535+
val new_Injs = distinct (op=) (filter (member (op=) frees o domain_type o fastype_of) (
15361536
maps (leader Injs_of_bmv_monad) (outer :: inners')
1537-
);
1537+
));
15381538

15391539
fun option x f y = the_default x (Option.map f y)
15401540
val new_RVrs = map_filter (fn a =>
@@ -1609,9 +1609,11 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
16091609
);
16101610
val Supps = map (fn live => Term.absfree (dest_Free x) (foldl1 mk_Un (@{map_filter 2} (
16111611
fn Inr _ => K NONE | Inl inner => fn set => if null (leader lives_of_bmv_monad inner) then NONE
1612-
else Option.map (mk_UNION (set $ x)) (
1613-
List.find (curry (op=) live o HOLogic.dest_setT o body_type o fastype_of) (the (leader Supps_of_bmv_monad inner))
1614-
)
1612+
else case filter (curry (op=) live o HOLogic.dest_setT o body_type o fastype_of) (the (leader Supps_of_bmv_monad inner)) of
1613+
[] => NONE
1614+
| xs => SOME (mk_UNION (set $ x) (Term.abs ("a", HOLogic.dest_setT (fastype_of (set $ x))) (
1615+
foldl1 mk_Un (map (fn s => s $ Bound 0) xs)))
1616+
)
16151617
) inners (the (leader Supps_of_bmv_monad outer))))) lives;
16161618
in SOME { Map = Map, Supps = Supps } end;
16171619

@@ -1670,14 +1672,26 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
16701672
],
16711673
Supp_Map = map (fn _ => fn ctxt => EVERY1 [
16721674
K (Local_Defs.unfold0_tac ctxt @{thms image_Un image_UN}),
1673-
REPEAT_DETERM o rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\<union>)"]},
1674-
REPEAT_DETERM o EVERY' [
1675-
EqSubst.eqsubst_tac ctxt [0] (#Supp_Map (#axioms param)),
1676-
SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms image_comp[unfolded comp_def] image_Un image_UN}),
1677-
rtac ctxt @{thm UN_cong},
1678-
SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms image_UN[symmetric]}),
1679-
resolve_tac ctxt (flat (map_filter (Option.map (#Supp_Map o #axioms) o leader params_of_bmv_monad) inners'))
1680-
]
1675+
SUBGOAL (fn (goal, _) =>
1676+
let
1677+
fun strip_all (Const (@{const_name Pure.all}, _) $ Abs (x, T, t)) = apfst (cons (x, T)) (strip_all t)
1678+
| strip_all t = ([], t)
1679+
val T = snd (snd (split_last (fst (strip_all goal))))
1680+
val thms = map (fn thm =>
1681+
let
1682+
val arg = Var (hd (Term.add_vars (Thm.prop_of thm) []));
1683+
val tyenv = Sign.typ_match (Proof_Context.theory_of ctxt)
1684+
(fastype_of arg, T) Vartab.empty;
1685+
val insts = map (fn (x, (s, T)) => ((x, s), Thm.ctyp_of ctxt T)) (Vartab.dest tyenv)
1686+
in instantiate_normalize (TVars.make insts, Vars.empty) thm end
1687+
) (#Supp_Map (#axioms param));
1688+
in Local_Defs.unfold0_tac ctxt (@{thms UN_simps(10)} @ thms) end
1689+
),
1690+
EVERY' (map (fn thm => TRY o EqSubst.eqsubst_tac ctxt [0] [thm])
1691+
(flat (map_filter (Option.map (#Supp_Map o #axioms) o leader params_of_bmv_monad) inners'))
1692+
),
1693+
K (Local_Defs.unfold0_tac ctxt @{thms image_UN[symmetric] image_Un[symmetric]}),
1694+
rtac ctxt refl
16811695
]) Supps,
16821696
Supp_bd = map (fn _ => fn ctxt => REPEAT_DETERM (resolve_tac ctxt (
16831697
flat (map_filter (Option.map (#Supp_bd o #axioms) o leader params_of_bmv_monad) inners')
@@ -1696,9 +1710,10 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
16961710
etac ctxt @{thm UN_I} ORELSE' REPEAT_DETERM o FIRST' [
16971711
rtac ctxt @{thm UnI2} THEN' etac ctxt @{thm UN_I},
16981712
rtac ctxt @{thm UnI1} THEN' etac ctxt @{thm UN_I},
1713+
eresolve_tac ctxt @{thms UnI1 UnI2},
16991714
rtac ctxt @{thm UnI1}
17001715
],
1701-
assume_tac ctxt
1716+
TRY o assume_tac ctxt
17021717
]
17031718
]
17041719
) inners)
@@ -1732,10 +1747,29 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
17321747
EqSubst.eqsubst_tac ctxt [0] (#Supp_Sb param),
17331748
REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt @{thm SSupp_Inj_bound})
17341749
],
1750+
SUBGOAL (fn (goal, _) =>
1751+
let
1752+
fun strip_all (Const (@{const_name Pure.all}, _) $ Abs (x, T, t)) = apfst (cons (x, T)) (strip_all t)
1753+
| strip_all t = ([], t)
1754+
val T = snd (snd (split_last (fst (strip_all goal))))
1755+
val thms = map (fn thm =>
1756+
let
1757+
val arg = Var (hd (Term.add_vars (Thm.prop_of thm) []));
1758+
val tyenv = Sign.typ_match (Proof_Context.theory_of ctxt)
1759+
(fastype_of arg, T) Vartab.empty;
1760+
val insts = map (fn (x, (s, T)) => ((x, s), Thm.ctyp_of ctxt T)) (Vartab.dest tyenv)
1761+
in instantiate_normalize (TVars.make insts, Vars.empty) thm end
1762+
) (#Supp_Map (#axioms param));
1763+
in Local_Defs.unfold0_tac ctxt (@{thms UN_simps(10)} @ thms) end
1764+
),
1765+
REPEAT_DETERM o EVERY' [
1766+
EqSubst.eqsubst_tac ctxt [0] (flat (maps (map_filter (Option.map #Supp_Sb) o params_of_bmv_monad) inners')),
1767+
REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt @{thm SSupp_Inj_bound})
1768+
],
17351769
K (Local_Defs.unfold0_tac ctxt (
17361770
@{thms image_Un image_UN image_comp[unfolded comp_def] UN_empty2 Union_UN_swap
17371771
Un_empty_right Un_empty_left UN_Un Union_Un_distrib UN_UN_flatten UN_Un_distrib}
1738-
@ #Supp_Map (#axioms param) @ #Vrs_Map param @ flat (#Supp_Injss facts)
1772+
@ #Vrs_Map param @ flat (#Supp_Injss facts)
17391773
)),
17401774
REPEAT_DETERM o EVERY' [
17411775
EqSubst.eqsubst_tac ctxt [0] (flat (maps (map_filter (Option.map #Supp_Sb) o params_of_bmv_monad) inners')),
@@ -1846,11 +1880,26 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
18461880
EqSubst.eqsubst_tac ctxt [0] (#Vrs_Sbs axioms @ #Supp_Sb param),
18471881
REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt @{thm SSupp_Inj_bound})
18481882
],
1883+
SUBGOAL (fn (goal, _) =>
1884+
let
1885+
fun strip_all (Const (@{const_name Pure.all}, _) $ Abs (x, T, t)) = apfst (cons (x, T)) (strip_all t)
1886+
| strip_all t = ([], t)
1887+
val T = snd (snd (split_last (fst (strip_all goal))))
1888+
val thms = map (fn thm =>
1889+
let
1890+
val arg = Var (hd (Term.add_vars (Thm.prop_of thm) []));
1891+
val tyenv = Sign.typ_match (Proof_Context.theory_of ctxt)
1892+
(fastype_of arg, T) Vartab.empty;
1893+
val insts = map (fn (x, (s, T)) => ((x, s), Thm.ctyp_of ctxt T)) (Vartab.dest tyenv)
1894+
in instantiate_normalize (TVars.make insts, Vars.empty) thm end
1895+
) (#Supp_Map (#axioms param));
1896+
in Local_Defs.unfold0_tac ctxt (@{thms UN_simps(10)} @ thms) end
1897+
),
18491898
K (Local_Defs.unfold0_tac ctxt (
18501899
@{thms image_Un image_UN image_comp[unfolded comp_def] UN_empty2 Union_UN_swap Un_assoc[symmetric]
1851-
Un_empty_right Un_empty_left UN_Un Union_Un_distrib UN_UN_flatten UN_Un_distrib}
1900+
Un_empty_right Un_empty_left UN_Un Union_Un_distrib UN_UN_flatten UN_Un_distrib id_bnf_apply}
18521901
@ #Vrs_Map param @ flat (#Vrs_Injss axioms)
1853-
@ #Supp_Map (#axioms param) @ flat (maps (
1902+
@ flat (maps (
18541903
#Supp_Injss o leader facts_of_bmv_monad
18551904
) (outer :: inners'))
18561905
)),
@@ -1860,7 +1909,7 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
18601909
),
18611910
REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt @{thm SSupp_Inj_bound})
18621911
],
1863-
K (Local_Defs.unfold0_tac ctxt @{thms image_Un Union_UN_swap image_UN UN_empty2 Un_empty_left Un_empty_right UN_UN_flatten UN_Un_distrib Un_assoc[symmetric]}),
1912+
K (Local_Defs.unfold0_tac ctxt @{thms image_single image_Un Union_UN_swap image_UN UN_empty2 Un_empty_left Un_empty_right UN_UN_flatten UN_Un_distrib Un_assoc[symmetric]}),
18641913
rtac ctxt refl ORELSE' EVERY' [
18651914
rtac ctxt @{thm set_eqI},
18661915
K (Local_Defs.unfold0_tac ctxt @{thms Un_iff}),

‎Tools/mrsbnf_comp.ML‎

Lines changed: 32 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,7 @@ fun compose_mrsbnfs inline_policy fact_policy qualify outer inners oDs Dss oAs A
8989
[] => NONE | x::_ => SOME (x, SOME (nth (MRSBNF_Def.axioms_of_mrsbnf mrsbnf) i))
9090
) mrbnfs (0 upto length mrbnfs - 1) end
9191
) inners);
92+
val (mrbnfs, axioms') = split_list (distinct ((op=) o apply2 (MRBNF_Def.T_of_mrbnf o fst)) (mrbnfs ~~ axioms'));
9293

9394
val mrbnfs = map (fn mrbnf =>
9495
let
@@ -196,7 +197,7 @@ fun compose_mrsbnfs inline_policy fact_policy qualify outer inners oDs Dss oAs A
196197
infer_instantiate' ctxt (map (Option.map (fn t =>
197198
let
198199
val t' = case t of
199-
Const (@{const_name id}, Type("fun", [TVar ((n, i), s), _])) =>
200+
Const (@{const_name id}, Type ("fun", [TVar ((n, i), s), _])) =>
200201
HOLogic.id_const (TVar ((n, i+1), s))
201202
| t => t
202203
in Thm.cterm_of lthy t' end
@@ -261,14 +262,16 @@ fun compose_mrsbnfs inline_policy fact_policy qualify outer inners oDs Dss oAs A
261262
REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt @{thm SSupp_Inj_bound})
262263
],
263264
K (Local_Defs.unfold0_tac ctxt (#Vrs_Map (the (BMV_Monad_Def.leader BMV_Monad_Def.params_of_bmv_monad outer_bmv)))),
264-
K (Local_Defs.unfold0_tac ctxt (map_filter #Map_map (MRSBNF_Def.facts_of_mrsbnf outer))),
265+
K (Local_Defs.unfold0_tac ctxt (no_reflexive (map_filter #Map_map (MRSBNF_Def.facts_of_mrsbnf outer)))),
265266
REPEAT_DETERM o EVERY' [
266267
EqSubst.eqsubst_tac ctxt [0] thms,
267268
REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id}
268269
],
269270
K (Local_Defs.unfold0_tac ctxt @{thms image_comp[unfolded comp_def] image_Un}),
270271
REPEAT_DETERM o EVERY' [
271-
EqSubst.eqsubst_tac ctxt [0] (maps (maps #set_Sb o MRSBNF_Def.axioms_of_mrsbnf) inners),
272+
EqSubst.eqsubst_tac ctxt [0] (maps (maps (map (
273+
Local_Defs.unfold0 ctxt (flat (#set_unfoldss (snd mrbnf_unfolds)))
274+
) o #set_Sb) o MRSBNF_Def.axioms_of_mrsbnf) inners),
272275
REPEAT_DETERM o (assume_tac ctxt ORELSE' rtac ctxt @{thm SSupp_Inj_bound})
273276
],
274277
K (Local_Defs.unfold_tac ctxt (
@@ -295,13 +298,30 @@ fun compose_mrsbnfs inline_policy fact_policy qualify outer inners oDs Dss oAs A
295298
]),
296299
set_Vrs = replicate (length (BMV_Monad_Def.leader BMV_Monad_Def.frees_of_bmv_monad bmv)) (fn ctxt => EVERY1 [
297300
K (Local_Defs.unfold0_tac ctxt (bmv_unfolds @ #map_unfolds (snd mrbnf_unfolds) @ flat (#set_unfoldss (snd mrbnf_unfolds)))),
298-
REPEAT_DETERM o EVERY' [
299-
EqSubst.eqsubst_tac ctxt [0] (MRBNF_Def.set_map_of_mrbnf outer_mrbnf),
300-
REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id}
301-
],
302-
K (Local_Defs.unfold_tac ctxt (
303-
@{thms UN_empty2 Un_empty_right Un_empty_left image_id Un_assoc[symmetric] Un_Union_image}
304-
@ no_reflexive (flat (maps (map #set_Vrs o MRSBNF_Def.axioms_of_mrsbnf) inners))
301+
SUBGOAL (fn (goal, _) =>
302+
let
303+
val outer_set_maps = @{map_filter 2} (fn MRBNF_Def.Live_Var => SOME | _ => K NONE) (MRBNF_Def.var_types_of_mrbnf outer_mrbnf) (MRBNF_Def.set_map_of_mrbnf outer_mrbnf);
304+
fun strip_all (Const (@{const_name Pure.all}, _) $ Abs (x, T, t)) = apfst (cons (x, T)) (strip_all t)
305+
| strip_all t = ([], t)
306+
val T = snd (snd (split_last (fst (strip_all goal))))
307+
val thms = map (fn thm =>
308+
let
309+
val arg = Var (hd (Term.add_vars (Thm.prop_of thm) []));
310+
val tyenv = Sign.typ_match (Proof_Context.theory_of ctxt)
311+
(fastype_of arg, T) Vartab.empty;
312+
val insts = map (fn (x, (s, T)) => ((x, s), Thm.ctyp_of ctxt T)) (Vartab.dest tyenv)
313+
in instantiate_normalize (TVars.make insts, Vars.empty) thm end
314+
) outer_set_maps;
315+
in REPEAT_DETERM (EVERY1 [
316+
EqSubst.eqsubst_tac ctxt [0] thms,
317+
REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id}
318+
]) end
319+
),
320+
K (Local_Defs.unfold_tac ctxt (@{thms UN_empty2 Un_empty_right Un_empty_left image_id
321+
Un_assoc[symmetric] Un_Union_image UN_singleton Un_absorb
322+
} @ no_reflexive (map (Local_Defs.unfold0 ctxt (
323+
flat (#set_unfoldss (snd mrbnf_unfolds))
324+
)) (flat (maps (map #set_Vrs o MRSBNF_Def.axioms_of_mrsbnf) inners)))
305325
)),
306326
rtac ctxt refl
307327
])
@@ -325,7 +345,7 @@ fun mrsbnf_of_typ _ _ qualify Ds0 var_types (T as TFree T') (accum:(thm list * (
325345
| mrsbnf_of_typ optim const_policy qualify' Ds0 var_types (T as Type (n, Ts)) ((bmv_unfolds:thm list, accum), lthy) = (case mrsbnf_of lthy n of
326346
NONE => ((Inr MRBNF_Comp.DEADID_mrbnf, ([T], [])), ((bmv_unfolds, accum), lthy))
327347
| SOME (outer, lthy) =>
328-
if optim andalso forall is_TFree Ts then
348+
if optim andalso forall is_TFree Ts andalso length Ts = length (subtract (op=) Ds0 (Term.add_tfreesT T [])) then
329349
let
330350
val mrbnf = case outer of
331351
Inl mrsbnf => nth (MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf) (BMV_Monad_Def.leader_of_bmv_monad (MRSBNF_Def.bmv_monad_of_mrsbnf mrsbnf))
@@ -339,8 +359,7 @@ fun mrsbnf_of_typ _ _ qualify Ds0 var_types (T as TFree T') (accum:(thm list * (
339359
T'::_ => error ("Variable " ^ Syntax.string_of_typ lthy T' ^ " is forced dead by type " ^ Syntax.string_of_typ lthy T ^ " but was specified as other usage")
340360
| [] => ()
341361
val Ts' = subtract (op=) deads Ts;
342-
val _ = @{print} T
343-
val _ = @{print} Ts'
362+
344363
val var_types = map (AList.lookup (op=) var_types o dest_TFree) Ts';
345364
val var_types = @{map 3} (fn req => fn var_type => fn T => if member (op=) Ds0 (dest_TFree T) then
346365
MRBNF_Def.Dead_Var else the_default var_type req
@@ -384,8 +403,6 @@ fun mrsbnf_of_typ _ _ qualify Ds0 var_types (T as TFree T') (accum:(thm list * (
384403
(fn i => mrsbnf_of_typ optim const_policy (qualify i) Ds0 var_types)
385404
(if length Ts' = 1 then [0] else 1 upto length Ts') Ts' ((bmv_unfolds, accum), lthy));
386405

387-
val _ = @{print} T
388-
val _ = @{print} Ts'
389406
val Xs = rev (Term.add_tfreesT T []);
390407
val Xs' = map (swap o `(the_default MRBNF_Def.Live_Var o AList.lookup (op=) var_types)) Xs
391408

‎Tools/mrsbnf_def.ML‎

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -64,13 +64,21 @@ fun apply_mrsbnf_axioms ({
6464
map_is_Sb=f1, map_Sb=f2, set_Sb=f3s, set_Vrs=f4s, map_Injs=f5s
6565
}: ('a -> 'b) mrsbnf_axioms) ({
6666
map_is_Sb, map_Sb, set_Sb, set_Vrs, map_Injs
67-
}: 'a mrsbnf_axioms) = {
67+
}: 'a mrsbnf_axioms) =
68+
let
69+
fun checkLength name xs ys = if length xs <> length ys then error (
70+
"UnequalLength: " ^ name ^ " (" ^ string_of_int (length xs) ^ " vs. " ^ string_of_int (length ys) ^ ")"
71+
) else ()
72+
val _ = checkLength "set_Sb" set_Sb f3s
73+
val _ = checkLength "set_Vrs" set_Vrs f4s
74+
val _ = Option.map (fn map_Injs => checkLength "map_Injs" map_Injs (the f5s)) map_Injs
75+
in {
6876
map_is_Sb = f1 map_is_Sb,
6977
map_Sb = Option.map (fn t => the f2 t) map_Sb,
7078
map_Injs = Option.map (fn ts => map2 (curry (op|>)) ts (the f5s)) map_Injs,
7179
set_Sb = map2 (curry (op|>)) set_Sb f3s,
7280
set_Vrs = map2 (curry (op|>)) set_Vrs f4s
73-
}: 'b mrsbnf_axioms
81+
}: 'b mrsbnf_axioms end
7482

7583
type mrsbnf_facts = {
7684
SSupp_map_subset: thm option list,
@@ -803,6 +811,8 @@ fun prove_axioms mrbnfs bmv tacs lthy =
803811
let
804812
val (goals, vars, mrbnfs, bmv) = mk_mrsbnf_axioms mrbnfs bmv lthy;
805813
val tacs' = map (map_mrsbnf_axioms (fn tac => fn goal => Goal.prove_sorry lthy [] [] goal (tac o #context))) tacs;
814+
val _ = if length tacs' = length goals then () else
815+
error ("Expected " ^ string_of_int (length goals) ^ " sets of axiom tactics, but got " ^ string_of_int (length tacs'))
806816
in (map2 apply_mrsbnf_axioms tacs' goals, vars, mrbnfs, bmv) end
807817

808818
fun mrsbnf_def fact_policy qualify name_opt mrbnfs bmv tacs lthy =

‎operations/BMV_Fixpoint.thy‎

Lines changed: 18 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -17,24 +17,33 @@ Multithreading.parallel_proofs := 0
1717

1818
local_setup \<open>fn lthy =>
1919
let
20-
val ((mrsbnf, tys), (_, lthy)) = MRSBNF_Comp.mrsbnf_of_typ true (K BNF_Def.Dont_Note)
20+
val ((mrsbnf, tys), ((bmv_unfolds, (_, mrbnf_unfolds)), lthy)) = MRSBNF_Comp.mrsbnf_of_typ true (K BNF_Def.Dont_Note)
2121
I [] (map (apfst dest_TFree) [(@{typ 'v}, MRBNF_Def.Free_Var),
2222
(@{typ 'btv}, MRBNF_Def.Bound_Var), (@{typ 'bv}, MRBNF_Def.Bound_Var)])
2323
@{typ "('tv, 'v, 'btv, 'bv, 'c, 'd) FTerm_pre'"}
24-
((MRBNF_Comp.empty_comp_cache, MRBNF_Comp.empty_unfolds), lthy);
25-
26-
val _ = @{print} mrsbnf
27-
in lthy end
28-
\<close>
29-
30-
31-
24+
(([], (MRBNF_Comp.empty_comp_cache, MRBNF_Comp.empty_unfolds)), lthy);
3225
26+
val unfold_defs = Thm.cterm_of lthy o Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy) bmv_unfolds []
27+
val unfold_defs' = Local_Defs.unfold0 lthy (bmv_unfolds @ #map_unfolds mrbnf_unfolds)
28+
val mrsbnf = case mrsbnf of MRBNF_Util.Inl x => x | _ => error "impossible"
29+
val bmv = MRSBNF_Def.bmv_monad_of_mrsbnf mrsbnf;
3330
31+
val _ = @{print} (map unfold_defs (BMV_Monad_Def.Sbs_of_bmv_monad bmv))
32+
val _ = @{print} (map (map unfold_defs' o #set_Vrs) (MRSBNF_Def.axioms_of_mrsbnf mrsbnf))
3433
34+
val (_, lthy) = BMV_Monad_Def.note_bmv_monad_thms (K BNF_Def.Note_All) I (SOME @{binding FTerm_pre'}) bmv lthy
3535
36+
val notes = [
37+
("bmv_defs", bmv_unfolds)
38+
] |> (map (fn (thmN, thms) =>
39+
((Binding.name thmN, []), [(thms, [])])
40+
));
3641
42+
val (noted, lthy) = Local_Theory.notes notes lthy
3743
44+
in lthy end
45+
\<close>
46+
print_theorems
3847

3948

4049

0 commit comments

Comments
 (0)