Skip to content

Commit af57b15

Browse files
jvanbrueggejvanbruegge
committed
Split internal definitions from user-facing ones
1 parent fd8fd6a commit af57b15

File tree

4 files changed

+28
-28
lines changed

4 files changed

+28
-28
lines changed

‎Tools/bmv_monad_def.ML‎

Lines changed: 24 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,7 @@ signature BMV_MONAD_DEF = sig
8484
val facts_of_bmv_monad: bmv_monad -> bmv_monad_facts list;
8585
val params_of_bmv_monad: bmv_monad -> thm bmv_monad_param option list;
8686
val unfolds_of_bmv_monad: bmv_monad -> thm list;
87+
val defs_of_bmv_monad: bmv_monad -> thm list;
8788

8889
val mk_small_prems_of_bmv_monad: bmv_monad -> int -> term list -> term list -> term list list;
8990

@@ -102,7 +103,8 @@ signature BMV_MONAD_DEF = sig
102103
val note_bmv_monad_thms: (Proof.context -> BNF_Def.fact_policy) -> (binding -> binding)
103104
-> binding option -> bmv_monad -> local_theory -> (string * thm list) list * local_theory
104105
val bmv_monad_def: BNF_Def.inline_policy -> (Proof.context -> BNF_Def.fact_policy)
105-
-> (binding -> binding) -> binding option -> (Proof.context -> tactic) bmv_monad_model -> local_theory -> (bmv_monad * thm list) * local_theory
106+
-> (binding -> binding) -> binding option -> (Proof.context -> tactic) bmv_monad_model
107+
-> thm list -> local_theory -> (bmv_monad * thm list) * local_theory
106108

107109
val unsafe_slice_bmv_monad: int -> bmv_monad -> bmv_monad;
108110

@@ -274,12 +276,13 @@ datatype bmv_monad = BMV of {
274276
bd_infinite_regular_card_order: thm,
275277
axioms: thm bmv_monad_axioms list,
276278
facts: bmv_monad_facts list,
277-
unfolds: thm list
279+
unfolds: thm list,
280+
defs: thm list
278281
}
279282

280283
fun morph_bmv_monad phi (BMV {
281284
ops, var_class, leader, frees, lives, lives', deads, consts, params, axioms, bd_infinite_regular_card_order,
282-
facts, unfolds
285+
facts, unfolds, defs
283286
}) = BMV {
284287
ops = map (Morphism.typ phi) ops,
285288
leader = leader,
@@ -293,7 +296,8 @@ fun morph_bmv_monad phi (BMV {
293296
axioms = map (morph_bmv_monad_axioms phi) axioms,
294297
facts = map (morph_bmv_monad_facts phi) facts,
295298
bd_infinite_regular_card_order = Morphism.thm phi bd_infinite_regular_card_order,
296-
unfolds = map (Morphism.thm phi) unfolds
299+
unfolds = map (Morphism.thm phi) unfolds,
300+
defs = map (Morphism.thm phi) defs
297301
}
298302

299303
fun Rep_bmv (BMV x) = x
@@ -319,6 +323,7 @@ val facts_of_bmv_monad = #facts o Rep_bmv
319323
val params_of_bmv_monad = #params o Rep_bmv
320324
val bd_infinite_regular_card_order_of_bmv_monad = #bd_infinite_regular_card_order o Rep_bmv
321325
val unfolds_of_bmv_monad = #unfolds o Rep_bmv
326+
val defs_of_bmv_monad = #defs o Rep_bmv
322327

323328
fun leader f bmv = nth (f bmv) (leader_of_bmv_monad bmv)
324329

@@ -832,7 +837,7 @@ fun note_bmv_monad_thms fact_policy qualify bmv_b_opt bmv lthy =
832837
|> fact_policy <> BNF_Def.Dont_Note ? note_unless_dont_note
833838
end
834839

835-
fun mk_bmv_monad const_policy fact_policy qualify bmv_b_opt (model: thm bmv_monad_model) unfolds lthy =
840+
fun mk_bmv_monad const_policy fact_policy qualify bmv_b_opt (model: thm bmv_monad_model) unfolds defs lthy =
836841
let
837842
val consts = {
838843
bd = #bd (#consts model),
@@ -1006,7 +1011,8 @@ fun mk_bmv_monad const_policy fact_policy qualify bmv_b_opt (model: thm bmv_mona
10061011
axioms = axioms',
10071012
facts = facts @ maps facts_of_bmv_monad (#bmv_ops model),
10081013
bd_infinite_regular_card_order = #bd_infinite_regular_card_order model,
1009-
unfolds = unfolds
1014+
unfolds = unfolds,
1015+
defs = defs
10101016
} : bmv_monad;
10111017

10121018
val (_, lthy) = note_bmv_monad_thms fact_policy qualify bmv_b_opt bmv lthy;
@@ -1067,7 +1073,7 @@ fun mk_thm_model (model: 'a bmv_monad_model) params axioms bd_irco = {
10671073
tacs = axioms
10681074
} : thm bmv_monad_model;
10691075

1070-
fun bmv_monad_def const_policy fact_policy qualify bmv_b_opt (model: (Proof.context -> tactic) bmv_monad_model) lthy =
1076+
fun bmv_monad_def const_policy fact_policy qualify bmv_b_opt (model: (Proof.context -> tactic) bmv_monad_model) defs lthy =
10711077
let
10721078
val frees = map (fn T => TFree (apsnd (
10731079
Sign.minimize_sort (Proof_Context.theory_of lthy) o cons (#var_class model)
@@ -1087,7 +1093,7 @@ fun bmv_monad_def const_policy fact_policy qualify bmv_b_opt (model: (Proof.cont
10871093
)) (fn {context=ctxt, ...} => Local_Defs.unfold0_tac ctxt unfold_set THEN #bd_infinite_regular_card_order model ctxt);
10881094

10891095
val model = mk_thm_model model params axioms bd_irco;
1090-
in apfst (rpair unfold_set) (mk_bmv_monad const_policy fact_policy qualify bmv_b_opt model unfold_set lthy) end
1096+
in apfst (rpair unfold_set) (mk_bmv_monad const_policy fact_policy qualify bmv_b_opt model unfold_set defs lthy) end
10911097

10921098
fun pbmv_monad_of_mrbnf qualify mrbnf lthy =
10931099
let
@@ -1216,7 +1222,7 @@ fun pbmv_monad_of_mrbnf qualify mrbnf lthy =
12161222
REPEAT_DETERM o (rtac ctxt refl ORELSE' Goal.assume_rule_tac ctxt)
12171223
]
12181224
}]
1219-
} lthy) end;
1225+
} [] lthy) end;
12201226

12211227
fun register_mrbnf_as_pbmv_monad name lthy =
12221228
let
@@ -1252,7 +1258,8 @@ fun unsafe_slice_bmv_monad n bmv =
12521258
bd_infinite_regular_card_order = bd_infinite_regular_card_order_of_bmv_monad bmv,
12531259
axioms = [f (axioms_of_bmv_monad bmv)],
12541260
facts = [f (facts_of_bmv_monad bmv)],
1255-
unfolds = unfolds_of_bmv_monad bmv
1261+
unfolds = unfolds_of_bmv_monad bmv,
1262+
defs = defs_of_bmv_monad bmv
12561263
} end;
12571264

12581265
fun demote_bmv_monad inline_policy const_policy qualify b_opt bmv { lives=dlives, frees=dfrees } lthy =
@@ -1519,7 +1526,7 @@ fun demote_bmv_monad inline_policy const_policy qualify b_opt bmv { lives=dlives
15191526
}) new_ops new_Injss new_RVrss extra_Vrs (map (hd o axioms_of_bmv_monad) demoted_bmvs)
15201527
(map (hd o params_of_bmv_monad) demoted_bmvs) (map (hd o facts_of_bmv_monad) demoted_bmvs)
15211528
}: (Proof.context -> tactic) bmv_monad_model;
1522-
in bmv_monad_def inline_policy const_policy qualify b_opt model lthy end
1529+
in bmv_monad_def inline_policy const_policy qualify b_opt model [] lthy end
15231530

15241531
fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) either list)
15251532
(oAs: { frees: typ list, deads: typ list }) (Ass : ({ frees: typ list, lives: typ list, deads: typ list }) option list) lthy =
@@ -2090,7 +2097,8 @@ fun compose_bmv_monad qualify (outer : bmv_monad) (inners : (bmv_monad, typ) eit
20902097
val name = qualify (Binding.conglomerate (map_filter (
20912098
try (Binding.name o short_type_name o fst o dest_Type) o leader ops_of_bmv_monad
20922099
) (outer :: inners')));
2093-
val (res, lthy) = bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) qualify (SOME name) model lthy
2100+
val (res, lthy) = bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) qualify (SOME name) model
2101+
(maps defs_of_bmv_monad (outer :: inners')) lthy
20942102
in (res, lthy) end;
20952103

20962104
fun seal_bmv_monad qualify unfolds name tys bmv info_opt lthy =
@@ -2334,20 +2342,10 @@ fun seal_bmv_monad qualify unfolds name tys bmv info_opt lthy =
23342342
}]
23352343
} : (Proof.context -> tactic) bmv_monad_model;
23362344

2337-
fun set_unfolds thms (BMV {
2338-
ops, var_class, leader: int, frees, lives, lives', deads, consts, params, bd_infinite_regular_card_order,
2339-
axioms, facts, ...
2340-
}) = BMV {
2341-
ops = ops, var_class = var_class, leader = leader, frees = frees, lives = lives, lives' = lives',
2342-
deads = deads, consts = consts, params = params, bd_infinite_regular_card_order = bd_infinite_regular_card_order,
2343-
axioms = axioms, facts = facts, unfolds = thms
2344-
}
2345+
val new_defs = map (Local_Defs.unfold lthy unfolds) defs;
2346+
val ((bmv, _), lthy) = bmv_monad_def BNF_Def.Hardly_Inline (K BNF_Def.Note_Some) qualify NONE model new_defs lthy;
23452347

2346-
val ((bmv, _), lthy) = bmv_monad_def BNF_Def.Hardly_Inline (K BNF_Def.Note_Some) qualify NONE model lthy;
2347-
val new_unfolds = map (Local_Defs.unfold lthy unfolds) defs;
2348-
val bmv = set_unfolds new_unfolds bmv;
2349-
2350-
in ((bmv, new_unfolds, defs, (T_name, info)), lthy) end
2348+
in ((bmv, new_defs, defs, (T_name, info)), lthy) end
23512349

23522350
fun pbmv_monad_cmd (((((((b_ops, Sbs), RVrs), Injs), Vrs), param_opt), bd), extra_Vrs) lthy =
23532351
let
@@ -2610,7 +2608,7 @@ fun pbmv_monad_cmd (((((((b_ops, Sbs), RVrs), Injs), Vrs), param_opt), bd), extr
26102608
tacs = axioms
26112609
} : thm bmv_monad_model;
26122610

2613-
val (bmv, lthy) = mk_bmv_monad BNF_Def.Smart_Inline (K BNF_Def.Note_Some) I (SOME (Binding.name b)) model (bmv_defs @ maps unfolds_of_bmv_monad bmv_ops) lthy;
2611+
val (bmv, lthy) = mk_bmv_monad BNF_Def.Smart_Inline (K BNF_Def.Note_Some) I (SOME (Binding.name b)) model (bmv_defs @ maps unfolds_of_bmv_monad bmv_ops) [] lthy;
26142612

26152613
val lthy = register_pbmv_monad b bmv lthy;
26162614
in lthy end;

‎Tools/mrbnf_sugar.ML‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -817,6 +817,7 @@ fun create_binder_datatype (spec : spec) lthy =
817817
Union_empty Un_empty_left Un_empty_right UN_single UN_singleton Un_absorb
818818
} @ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf
819819
@ BMV_Monad_Def.unfolds_of_bmv_monad bmv
820+
@ BMV_Monad_Def.defs_of_bmv_monad bmv
820821
@ [#Abs_inverse (snd info) OF @{thms UNIV_I}]
821822
)),
822823
rtac ctxt refl
@@ -831,6 +832,7 @@ fun create_binder_datatype (spec : spec) lthy =
831832
Un_absorb
832833
} @ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf
833834
@ BMV_Monad_Def.unfolds_of_bmv_monad bmv
835+
@ BMV_Monad_Def.defs_of_bmv_monad bmv
834836
)),
835837
Subgoal.FOCUS_PARAMS (fn {context=ctxt, params, ...} =>
836838
rtac ctxt (infer_instantiate' ctxt [SOME (snd (hd params))] (#Abs_cases (snd info))) 1
@@ -865,6 +867,7 @@ fun create_binder_datatype (spec : spec) lthy =
865867
@{thms comp_def sum.set_map UN_empty2 Un_empty_right Un_empty_left UN_singleton map_sum.simps map_prod_simp id_apply sum.inject}
866868
@ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf
867869
@ BMV_Monad_Def.unfolds_of_bmv_monad bmv
870+
@ BMV_Monad_Def.defs_of_bmv_monad bmv
868871
@ [#Abs_inverse (snd info) OF @{thms UNIV_I}, #Abs_inject (snd info) OF @{thms UNIV_I UNIV_I}]
869872
)),
870873
REPEAT_DETERM o FIRST' [

‎Tools/tvsubst.ML‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1599,7 +1599,7 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe
15991599
] end
16001600
) ctxt 1
16011601
}]
1602-
} lthy;
1602+
} [] (*TODO: Put definitions here *) lthy;
16031603

16041604
val rec_mrbnf =
16051605
let

‎operations/BMV_Fixpoint.thy‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -478,7 +478,6 @@ interpretation tvsubst: QREC_fixed_FTerm "avoiding_set1 f1 f2"
478478
apply (rule trans)
479479
apply (rule FTerm.permute_ctor)
480480
apply (assumption)+
481-
thm trans[OF comp_apply[symmetric] FTerm_pre.map_Sb_strong(1)[THEN fun_cong]]
482481
apply (subst trans[OF comp_apply[symmetric] FTerm_pre.map_Sb_strong(1)[THEN fun_cong]])
483482
apply (assumption | rule supp_id_bound bij_id f_prems)+
484483
apply (unfold0 id_o o_id inv_o_simp2 comp_apply)

0 commit comments

Comments
 (0)