--- a/src/HOL/Library/old_recdef.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Library/old_recdef.ML Tue Dec 03 15:20:30 2019 +0100
@@ -2842,7 +2842,7 @@
|> Global_Theory.add_thmss
(((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
- ||> Spec_Rules.add_global name Spec_Rules.equational_recdef [lhs] (flat rules)
+ ||> Spec_Rules.add_global (Binding.name bname) Spec_Rules.equational_recdef [lhs] (flat rules)
||> null tcs ? Code.declare_default_eqns_global (map (rpair true) (flat rules));
val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
val thy3 =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Dec 03 15:20:30 2019 +0100
@@ -1414,10 +1414,13 @@
|> massage_simple_notes fp_b_name;
val (noted, lthy') = lthy
- |> uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) map_thms)
+ |> uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)
+ (`(single o lhs_head_of o hd) map_thms)
|> fp = Least_FP ?
- uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) rel_code_thms)
- |> uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) set0_thms)
+ uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)
+ (`(single o lhs_head_of o hd) rel_code_thms)
+ |> uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)
+ (`(single o lhs_head_of o hd) set0_thms)
|> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (rel_code_thms @ map_thms @ set_thms))
|> Local_Theory.notes (anonymous_notes @ notes);
@@ -2689,7 +2692,7 @@
|> massage_multi_notes fp_b_names fpTs;
in
lthy
- |> Spec_Rules.add "" Spec_Rules.equational recs (flat rec_thmss)
+ |> Spec_Rules.add Binding.empty Spec_Rules.equational recs (flat rec_thmss)
|> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat rec_thmss))
|> Local_Theory.notes (common_notes @ notes)
(* for "datatype_realizer.ML": *)
@@ -2869,7 +2872,7 @@
|> massage_multi_notes fp_b_names fpTs;
in
lthy
- |> fold (Spec_Rules.add "" Spec_Rules.equational corecs)
+ |> fold (Spec_Rules.add Binding.empty Spec_Rules.equational corecs)
[flat corec_sel_thmss, flat corec_thmss]
|> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) corec_code_thms)
|> Local_Theory.notes (common_notes @ notes)
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Dec 03 15:20:30 2019 +0100
@@ -1630,21 +1630,21 @@
val ssig_bnf = #fp_bnf ssig_fp_sugar;
- val (dead_ssig_bnf, lthy) = bnf_kill_all_but 1 ssig_bnf lthy;
+ val (dead_ssig_bnf, lthy') = bnf_kill_all_but 1 ssig_bnf lthy;
val dead_pre_rel = mk_rel preT dead_pre_bnf;
val dead_k_rel = mk_rel k_T dead_k_bnf;
val dead_ssig_rel = mk_rel ssig_T dead_ssig_bnf;
- val (((parametric_consts, rho_rhs), rho_data), lthy) =
- extract_rho_from_equation friend_parse_info fun_b version Y preT ssig_T fun_t parsed_eq lthy;
+ val (((parametric_consts, rho_rhs), rho_data), lthy'') =
+ extract_rho_from_equation friend_parse_info fun_b version Y preT ssig_T fun_t parsed_eq lthy';
- val const_transfer_goals = map (mk_const_transfer_goal lthy) parametric_consts;
+ val const_transfer_goals = map (mk_const_transfer_goal lthy'') parametric_consts;
val rho_transfer_goal =
- mk_rho_parametricity_goal lthy Y Z preT ssig_T dead_pre_rel dead_k_rel dead_ssig_rel rho_rhs;
+ mk_rho_parametricity_goal lthy'' Y Z preT ssig_T dead_pre_rel dead_k_rel dead_ssig_rel rho_rhs;
in
- ((rho_data, (const_transfer_goals, rho_transfer_goal)), lthy)
+ ((rho_data, (const_transfer_goals, rho_transfer_goal)), lthy'')
end;
fun explore_corec_equation ctxt could_be_friend friend fun_name fun_free
@@ -1814,12 +1814,12 @@
fun pat_completeness_auto ctxt =
Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt;
- val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy) =
+ val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy') =
Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
[(((Binding.concealed Binding.empty, []), parsed_eq), [], [])]
Function_Common.default_config pat_completeness_auto lthy;
in
- ((defname, (pelim, pinduct, psimp)), lthy)
+ ((defname, (pelim, pinduct, psimp)), lthy')
end;
fun build_corecUU_arg_and_goals prove_termin (Free (fun_base_name, _)) (arg_ts, explored_rhs) lthy =
@@ -1983,48 +1983,48 @@
(* FIXME: does this work with locales that fix variables? *)
val no_base = has_no_corec_info lthy fpT_name;
- val lthy = lthy |> no_base ? setup_base fpT_name;
+ val lthy1 = lthy |> no_base ? setup_base fpT_name;
- fun extract_rho lthy =
+ fun extract_rho lthy' =
let
- val lthy = lthy |> Variable.declare_typ fun_T;
+ val lthy'' = lthy' |> Variable.declare_typ fun_T;
val (prepared as (_, _, version, Y, Z, preT, k_T, ssig_T, dead_pre_bnf, dead_k_bnf, _,
- ssig_fp_sugar, buffer), lthy) =
- prepare_friend_corec fun_name fun_T lthy;
- val friend_parse_info = friend_parse_info_of lthy arg_Ts res_T buffer;
+ ssig_fp_sugar, buffer), lthy''') =
+ prepare_friend_corec fun_name fun_T lthy'';
+ val friend_parse_info = friend_parse_info_of lthy''' arg_Ts res_T buffer;
val parsed_eq' = parsed_eq ||> subst_atomic [(fun_free, fun_t)];
in
- lthy
+ lthy'''
|> extract_rho_return_transfer_goals b version dead_pre_bnf dead_k_bnf Y Z preT k_T ssig_T
ssig_fp_sugar friend_parse_info fun_t parsed_eq'
|>> pair prepared
end;
- val ((prepareds, (rho_datas, transfer_goal_datas)), lthy) =
- if friend then extract_rho lthy |>> (apfst single ##> (apfst single #> apsnd single))
- else (([], ([], [])), lthy);
+ val ((prepareds, (rho_datas, transfer_goal_datas)), lthy2) =
+ if friend then extract_rho lthy1 |>> (apfst single ##> (apfst single #> apsnd single))
+ else (([], ([], [])), lthy1);
- val ((buffer, corec_infos), lthy) =
+ val ((buffer, corec_infos), lthy3) =
if friend then
- ((#13 (the_single prepareds), []), lthy)
+ ((#13 (the_single prepareds), []), lthy2)
else
- corec_info_of res_T lthy
+ corec_info_of res_T lthy2
||> no_base ? update_coinduct_cong_intross_dynamic fpT_name
|>> (fn info as {buffer, ...} => (buffer, [info]));
- val corec_parse_info = corec_parse_info_of lthy arg_Ts res_T buffer;
+ val corec_parse_info = corec_parse_info_of lthy3 arg_Ts res_T buffer;
val explored_eq =
- explore_corec_equation lthy true friend fun_name fun_free corec_parse_info res_T parsed_eq;
+ explore_corec_equation lthy3 true friend fun_name fun_free corec_parse_info res_T parsed_eq;
- val (((inner_fp_triple, termin_goals), corecUU_arg), lthy) =
- build_corecUU_arg_and_goals (not long_cmd) fun_free explored_eq lthy;
+ val (((inner_fp_triple, termin_goals), corecUU_arg), lthy4) =
+ build_corecUU_arg_and_goals (not long_cmd) fun_free explored_eq lthy3;
fun def_fun (inner_fp_elims0, inner_fp_inducts0, inner_fp_simps0) const_transfers
- rho_transfers_foldeds lthy =
+ rho_transfers_foldeds lthy5 =
let
- fun register_friend lthy =
+ fun register_friend lthy' =
let
val [(old_corec_info, fp_b, version, Y, Z, _, k_T, _, _, dead_k_bnf, sig_fp_sugar,
ssig_fp_sugar, _)] = prepareds;
@@ -2035,53 +2035,53 @@
val rho_transfer_folded =
(case rho_transfers_foldeds of
[] =>
- derive_rho_transfer_folded lthy fpT_name const_transfers rho_def rho_transfer_goal
+ derive_rho_transfer_folded lthy' fpT_name const_transfers rho_def rho_transfer_goal
| [thm] => thm);
in
- lthy
+ lthy'
|> register_coinduct_dynamic_friend fpT_name fun_name
|> register_friend_corec fun_name fp_b version Y Z k_T dead_k_bnf sig_fp_sugar
ssig_fp_sugar fun_t rho rho_transfer_folded old_corec_info
end;
- val (friend_infos, lthy) = lthy |> (if friend then register_friend #>> single else pair []);
- val (corec_info as {corecUU = corecUU0, ...}, lthy) =
+ val (friend_infos, lthy6) = lthy5 |> (if friend then register_friend #>> single else pair []);
+ val (corec_info as {corecUU = corecUU0, ...}, lthy7) =
(case corec_infos of
- [] => corec_info_of res_T lthy
- | [info] => (info, lthy));
+ [] => corec_info_of res_T lthy6
+ | [info] => (info, lthy6));
- val def_rhs = mk_corec_fun_def_rhs lthy arg_Ts corecUU0 corecUU_arg;
+ val def_rhs = mk_corec_fun_def_rhs lthy7 arg_Ts corecUU0 corecUU_arg;
val def = ((b, mx), ((Binding.concealed (Thm.def_binding b), []), def_rhs));
- val ((fun_t0, (_, fun_def0)), (lthy, lthy_old)) = lthy
+ val ((fun_lhs0, (_, fun_def0)), (lthy9, lthy8')) = lthy7
|> Local_Theory.open_target |> snd
|> Local_Theory.define def
- |> tap (fn (def, lthy) => print_def_consts int [def] lthy)
+ |> tap (fn (def, lthy') => print_def_consts int [def] lthy')
||> `Local_Theory.close_target;
- val parsed_eq = parse_corec_equation lthy [fun_free] eq;
- val views0 = generate_views lthy eq fun_free parsed_eq;
+ val parsed_eq = parse_corec_equation lthy9 [fun_free] eq;
+ val views0 = generate_views lthy9 eq fun_free parsed_eq;
- val lthy' = lthy |> fold Variable.declare_typ (res_T :: arg_Ts);
- val phi = Proof_Context.export_morphism lthy_old lthy';
+ val lthy9' = lthy9 |> fold Variable.declare_typ (res_T :: arg_Ts);
+ val phi = Proof_Context.export_morphism lthy8' lthy9';
- val fun_t = Morphism.term phi fun_t0; (* FIXME: shadows "fun_t" -- identical? *)
+ val fun_lhs = Morphism.term phi fun_lhs0;
val fun_def = Morphism.thm phi fun_def0;
val inner_fp_elims = map (Morphism.thm phi) inner_fp_elims0;
val inner_fp_inducts = map (Morphism.thm phi) inner_fp_inducts0;
val inner_fp_simps = map (Morphism.thm phi) inner_fp_simps0;
val (code_goal, _, _, _, _) = morph_views phi views0;
- fun derive_and_note_friend_extra_theorems lthy =
+ fun derive_and_note_friend_extra_theorems lthy' =
let
val k_T = #7 (the_single prepareds);
val rho_def = snd (the_single rho_datas);
- val (eq_algrho, algrho_eq) = derive_eq_algrho lthy corec_info (the_single friend_infos)
- fun_t k_T code_goal const_transfers rho_def fun_def;
+ val (eq_algrho, algrho_eq) = derive_eq_algrho lthy' corec_info (the_single friend_infos)
+ fun_lhs k_T code_goal const_transfers rho_def fun_def;
val notes =
- (if Config.get lthy bnf_internals then
+ (if Config.get lthy' bnf_internals then
[(eq_algrhoN, [eq_algrho])]
else
[])
@@ -2090,14 +2090,14 @@
(Binding.qualify false friendN (Binding.name thmN)), []),
[(thms, [])]));
in
- lthy
+ lthy'
|> register_friend_extra fun_name eq_algrho algrho_eq
|> Local_Theory.notes notes |> snd
end;
- val lthy = lthy |> friend ? derive_and_note_friend_extra_theorems;
+ val lthy10 = lthy9 |> friend ? derive_and_note_friend_extra_theorems;
- val code_thm = derive_code lthy inner_fp_simps code_goal corec_info fun_t fun_def;
+ val code_thm = derive_code lthy10 inner_fp_simps code_goal corec_info fun_lhs fun_def;
(* TODO:
val ctr_thmss = map mk_thm (#2 views);
val disc_thmss = map mk_thm (#3 views);
@@ -2107,7 +2107,7 @@
val uniques =
if null inner_fp_simps then
- [derive_unique lthy phi (#1 views0) corec_info fpT_name fun_def]
+ [derive_unique lthy10 phi (#1 views0) corec_info fpT_name fun_def]
else
[];
@@ -2117,7 +2117,7 @@
val simp_thmss = map2 append disc_iff_or_disc_thmss sel_thmss;
*)
- val ((_, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy) = lthy
+ val ((_, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy11) = lthy10
|> derive_and_update_coinduct_cong_intross [corec_info];
val cong_intros_pairs = AList.group (op =) cong_intro_pairs;
@@ -2134,7 +2134,7 @@
(inner_inductN, inner_fp_inducts, []),
(uniqueN, uniques, [])] @
map (fn (thmN, thms) => (thmN, thms, [])) cong_intros_pairs @
- (if Config.get lthy bnf_internals then
+ (if Config.get lthy11 bnf_internals then
[(inner_elimN, inner_fp_elims, []),
(inner_simpN, inner_fp_simps, [])]
else
@@ -2152,12 +2152,12 @@
[(thms, [])]))
|> filter_out (null o fst o hd o snd);
in
- lthy
+ lthy11
(* TODO:
- |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat sel_thmss)
- |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat ctr_thmss)
+ |> Spec_Rules.add Spec_Rules.equational ([fun_lhs], flat sel_thmss)
+ |> Spec_Rules.add Spec_Rules.equational ([fun_lhs], flat ctr_thmss)
*)
- |> Spec_Rules.add "" Spec_Rules.equational [fun_t0] [code_thm]
+ |> Spec_Rules.add Binding.empty Spec_Rules.equational [fun_lhs] [code_thm]
|> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
|> Local_Theory.notes (anonymous_notes @ notes)
|> snd
@@ -2177,16 +2177,16 @@
val const_transfer_goals = fold (union (op aconv) o fst) transfer_goal_datas [];
val (const_transfers, const_transfer_goals') =
if long_cmd then ([], const_transfer_goals)
- else fold (maybe_prove_transfer_goal lthy) const_transfer_goals ([], []);
+ else fold (maybe_prove_transfer_goal lthy4) const_transfer_goals ([], []);
in
((def_fun, (([res_T], prepareds, rho_datas, map snd transfer_goal_datas),
- (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals'))), lthy)
+ (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals'))), lthy4)
end;
fun corec_cmd int opts (raw_fixes, raw_eq) lthy =
let
val ((def_fun, (_, (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals))),
- lthy) =
+ lthy') =
prepare_corec_ursive_cmd int false opts (raw_fixes, raw_eq) lthy;
in
if not (null termin_goals) then
@@ -2196,32 +2196,32 @@
error ("Transfer prover failed (try " ^ quote (#1 \<^command_keyword>\<open>corecursive\<close>) ^
" instead of " ^ quote (#1 \<^command_keyword>\<open>corec\<close>) ^ ")")
else
- def_fun inner_fp_triple const_transfers [] lthy
+ def_fun inner_fp_triple const_transfers [] lthy'
end;
fun corecursive_cmd int opts (raw_fixes, raw_eq) lthy =
let
val ((def_fun, (([Type (fpT_name, _)], prepareds, rho_datas, rho_transfer_goals),
- (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals))), lthy) =
+ (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals))), lthy') =
prepare_corec_ursive_cmd int true opts (raw_fixes, raw_eq) lthy;
val (rho_transfer_goals', unprime_rho_transfer_and_folds) =
@{map 3} (fn (_, _, _, _, _, _, _, _, _, _, _, _, _) => fn (_, rho_def) =>
- prime_rho_transfer_goal lthy fpT_name rho_def)
+ prime_rho_transfer_goal lthy' fpT_name rho_def)
prepareds rho_datas rho_transfer_goals
|> split_list;
in
Proof.theorem NONE (fn [termin_thms, const_transfers', rho_transfers'] =>
let
val remove_domain_condition =
- full_simplify (put_simpset HOL_basic_ss lthy
+ full_simplify (put_simpset HOL_basic_ss lthy'
addsimps (@{thm True_implies_equals} :: termin_thms));
in
def_fun (@{apply 3} (map remove_domain_condition) inner_fp_triple)
(const_transfers @ const_transfers')
(map2 (fn f => f) unprime_rho_transfer_and_folds rho_transfers')
end)
- (map (map (rpair [])) [termin_goals, const_transfer_goals, rho_transfer_goals']) lthy
+ (map (map (rpair [])) [termin_goals, const_transfer_goals, rho_transfer_goals']) lthy'
end;
fun friend_of_corec_cmd ((raw_fun_name, raw_fun_T_opt), raw_eq) lthy =
@@ -2248,24 +2248,24 @@
val (arg_Ts, res_T as Type (fpT_name, _)) = strip_type fun_T;
val no_base = has_no_corec_info lthy fpT_name;
- val lthy = lthy |> no_base ? setup_base fpT_name;
+ val lthy1 = lthy |> no_base ? setup_base fpT_name;
- val lthy = lthy |> Variable.declare_typ fun_T;
+ val lthy2 = lthy1 |> Variable.declare_typ fun_T;
val ((old_corec_info, fp_b, version, Y, Z, preT, k_T, ssig_T, dead_pre_bnf, dead_k_bnf,
- sig_fp_sugar, ssig_fp_sugar, buffer), lthy) =
- prepare_friend_corec fun_name fun_T lthy;
- val friend_parse_info = friend_parse_info_of lthy arg_Ts res_T buffer;
+ sig_fp_sugar, ssig_fp_sugar, buffer), lthy3) =
+ prepare_friend_corec fun_name fun_T lthy2;
+ val friend_parse_info = friend_parse_info_of lthy3 arg_Ts res_T buffer;
- val parsed_eq = parse_corec_equation lthy [] code_goal;
+ val parsed_eq = parse_corec_equation lthy3 [] code_goal;
- val (((rho, rho_def), (const_transfer_goals, rho_transfer_goal)), lthy) =
+ val (((rho, rho_def), (const_transfer_goals, rho_transfer_goal)), lthy4) =
extract_rho_return_transfer_goals fun_b version dead_pre_bnf dead_k_bnf Y Z preT k_T ssig_T
- ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy;
+ ssig_fp_sugar friend_parse_info fun_t parsed_eq lthy3;
fun register_friend_extra_and_note_thms code_goal code_thm const_transfers k_T friend_info
- lthy =
+ lthy5 =
let
- val (corec_info, lthy) = corec_info_of res_T lthy;
+ val (corec_info, lthy6) = corec_info_of res_T lthy5;
val fun_free = Free (Binding.name_of fun_b, fun_T);
@@ -2273,25 +2273,25 @@
| freeze_fun t = t;
val eq = Term.map_aterms freeze_fun code_goal;
- val parsed_eq = parse_corec_equation lthy [fun_free] eq;
+ val parsed_eq = parse_corec_equation lthy6 [fun_free] eq;
- val corec_parse_info = corec_parse_info_of lthy arg_Ts res_T buffer;
- val explored_eq = explore_corec_equation lthy false false fun_name fun_free corec_parse_info
+ val corec_parse_info = corec_parse_info_of lthy6 arg_Ts res_T buffer;
+ val explored_eq = explore_corec_equation lthy6 false false fun_name fun_free corec_parse_info
res_T parsed_eq;
- val ((_, corecUU_arg), _) = build_corecUU_arg_and_goals false fun_free explored_eq lthy;
+ val ((_, corecUU_arg), _) = build_corecUU_arg_and_goals false fun_free explored_eq lthy6;
- val eq_corecUU = derive_eq_corecUU lthy corec_info fun_t corecUU_arg code_thm;
- val (eq_algrho, algrho_eq) = derive_eq_algrho lthy corec_info friend_info fun_t k_T
+ val eq_corecUU = derive_eq_corecUU lthy6 corec_info fun_t corecUU_arg code_thm;
+ val (eq_algrho, algrho_eq) = derive_eq_algrho lthy6 corec_info friend_info fun_t k_T
code_goal const_transfers rho_def eq_corecUU;
- val ((_, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy) = lthy
+ val ((_, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy7) = lthy6
|> register_friend_extra fun_name eq_algrho algrho_eq
|> register_coinduct_dynamic_friend fpT_name fun_name
|> derive_and_update_coinduct_cong_intross [corec_info];
val cong_intros_pairs = AList.group (op =) cong_intro_pairs;
- val unique = derive_unique lthy Morphism.identity code_goal corec_info fpT_name eq_corecUU;
+ val unique = derive_unique lthy7 Morphism.identity code_goal corec_info fpT_name eq_corecUU;
val notes =
[(codeN, [code_thm], []),
@@ -2299,7 +2299,7 @@
(cong_introsN, maps snd cong_intros_pairs, []),
(uniqueN, [unique], [])] @
map (fn (thmN, thms) => (thmN, thms, [])) cong_intros_pairs @
- (if Config.get lthy bnf_internals then
+ (if Config.get lthy7 bnf_internals then
[(eq_algrhoN, [eq_algrho], []),
(eq_corecUUN, [eq_corecUU], [])]
else
@@ -2309,14 +2309,14 @@
(Binding.qualify false friendN (Binding.name thmN)), attrs),
[(thms, [])]));
in
- lthy
+ lthy7
|> Local_Theory.notes notes |> snd
end;
val (rho_transfer_goal', unprime_rho_transfer_and_fold) =
- prime_rho_transfer_goal lthy fpT_name rho_def rho_transfer_goal;
+ prime_rho_transfer_goal lthy4 fpT_name rho_def rho_transfer_goal;
in
- lthy
+ lthy4
|> Proof.theorem NONE (fn [[code_thm], const_transfers, [rho_transfer']] =>
register_friend_corec fun_name fp_b version Y Z k_T dead_k_bnf sig_fp_sugar ssig_fp_sugar
fun_t rho (unprime_rho_transfer_and_fold rho_transfer') old_corec_info
@@ -2331,13 +2331,13 @@
val no_base = has_no_corec_info lthy fpT_name;
- val (corec_info as {version, ...}, lthy) = lthy
+ val (corec_info as {version, ...}, lthy1) = lthy
|> corec_info_of fpT;
- val lthy = lthy |> no_base ? setup_base fpT_name;
+ val lthy2 = lthy1 |> no_base ? setup_base fpT_name;
- val ((changed, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy) = lthy
+ val ((changed, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy3) = lthy2
|> derive_and_update_coinduct_cong_intross [corec_info];
- val lthy = lthy |> (changed orelse no_base) ? update_coinduct_cong_intross_dynamic fpT_name;
+ val lthy4 = lthy3 |> (changed orelse no_base) ? update_coinduct_cong_intross_dynamic fpT_name;
val cong_intros_pairs = AList.group (op =) cong_intro_pairs;
val notes =
@@ -2349,16 +2349,16 @@
(Binding.qualify false ("v" ^ string_of_int version) (Binding.name thmN))), attrs),
[(thms, [])]));
in
- lthy |> Local_Theory.notes notes |> snd
+ lthy4 |> Local_Theory.notes notes |> snd
end;
fun consolidate lthy =
let
val corec_infoss = map (corec_infos_of lthy o fst) (all_codatatype_extras_of lthy);
- val (changeds, lthy) = lthy
+ val (changeds, lthy') = lthy
|> fold_map (apfst fst oo derive_and_update_coinduct_cong_intross) corec_infoss;
in
- if exists I changeds then lthy else raise Same.SAME
+ if exists I changeds then lthy' else raise Same.SAME
end;
fun consolidate_global thy =
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Dec 03 15:20:30 2019 +0100
@@ -1533,9 +1533,10 @@
val fun_ts0 = map fst def_infos;
in
lthy
- |> Spec_Rules.add "" (Spec_Rules.equational_primcorec primcorec_types) fun_ts0 (flat sel_thmss)
- |> Spec_Rules.add "" Spec_Rules.equational fun_ts0 (flat ctr_thmss)
- |> Spec_Rules.add "" Spec_Rules.equational fun_ts0 (flat code_thmss)
+ |> Spec_Rules.add Binding.empty (Spec_Rules.equational_primcorec primcorec_types)
+ fun_ts0 (flat sel_thmss)
+ |> Spec_Rules.add Binding.empty Spec_Rules.equational fun_ts0 (flat ctr_thmss)
+ |> Spec_Rules.add Binding.empty Spec_Rules.equational fun_ts0 (flat code_thmss)
|> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss))
|> Local_Theory.notes (anonymous_notes @ common_notes @ notes)
|> snd
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Dec 03 15:20:30 2019 +0100
@@ -637,7 +637,7 @@
val transfer = exists (can (fn Transfer_Option => ())) opts;
val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
- val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map (#1 o #1) fixes));
+ val spec_name = Binding.conglomerate (map (#1 o #1) fixes);
val mk_notes =
flat oooo @{map 4} (fn js => fn prefix => fn qualify => fn thms =>
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Dec 03 15:20:30 2019 +0100
@@ -373,8 +373,9 @@
val (noted, lthy3) =
lthy2
- |> Spec_Rules.add "" Spec_Rules.equational size_consts size_simps
- |> Spec_Rules.add "" Spec_Rules.equational overloaded_size_consts overloaded_size_simps
+ |> Spec_Rules.add Binding.empty Spec_Rules.equational size_consts size_simps
+ |> Spec_Rules.add Binding.empty Spec_Rules.equational
+ overloaded_size_consts overloaded_size_simps
|> Code.declare_default_eqns (map (rpair true) (flat size_thmss))
(*Ideally, this would be issued only if the "code" plugin is enabled.*)
|> Local_Theory.notes notes;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Dec 03 15:20:30 2019 +0100
@@ -1111,10 +1111,10 @@
((qualify true (Binding.name thmN), attrs), [(thms, [])]));
val (noted, lthy') = lthy
- |> Spec_Rules.add "" Spec_Rules.equational [casex] case_thms
- |> fold (uncurry (Spec_Rules.add "" Spec_Rules.equational))
+ |> Spec_Rules.add Binding.empty Spec_Rules.equational [casex] case_thms
+ |> fold (uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational))
(AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
- |> fold (uncurry (Spec_Rules.add "" Spec_Rules.equational))
+ |> fold (uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational))
(filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Case_Translation.register
--- a/src/HOL/Tools/Function/function.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/Function/function.ML Tue Dec 03 15:20:30 2019 +0100
@@ -211,7 +211,7 @@
lthy2
|> Local_Theory.declaration {syntax = false, pervasive = false}
(fn phi => add_function_data (transform_function_data phi info'))
- |> Spec_Rules.add "" Spec_Rules.equational_recdef fs tsimps)
+ |> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef fs tsimps)
end)
end
in
--- a/src/HOL/Tools/Function/partial_function.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Tue Dec 03 15:20:30 2019 +0100
@@ -302,7 +302,7 @@
val ((_, [rec_rule']), lthy'') = lthy' |> Local_Theory.note (eq_abinding, [rec_rule])
in
lthy''
- |> Spec_Rules.add "" Spec_Rules.equational_recdef [f] [rec_rule']
+ |> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef [f] [rec_rule']
|> note_qualified ("simps", [rec_rule'])
|> note_qualified ("mono", [mono_thm])
|> (case raw_induct of NONE => I | SOME thm => note_qualified ("raw_induct", [thm]))
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Tue Dec 03 15:20:30 2019 +0100
@@ -500,7 +500,7 @@
val specs =
if s = \<^const_name>\<open>The\<close> then
- [{name = "", rough_classification = Spec_Rules.Unknown,
+ [{pos = Position.none, name = "", rough_classification = Spec_Rules.Unknown,
terms = [Logic.varify_global \<^term>\<open>The\<close>],
rules = [@{thm theI_unique}]}]
else if s = \<^const_name>\<open>finite\<close> then
@@ -508,7 +508,7 @@
if card = Inf orelse card = Fin_or_Inf then
spec_rules ()
else
- [{name = "", rough_classification = Spec_Rules.equational,
+ [{pos = Position.none, name = "", rough_classification = Spec_Rules.equational,
terms = [Logic.varify_global \<^term>\<open>finite\<close>],
rules = [Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\<open>finite A = True\<close>)]}]
end
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Tue Dec 03 15:20:30 2019 +0100
@@ -278,7 +278,7 @@
fun gen_primrec prep_spec int raw_fixes raw_spec lthy =
let
val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
- val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map (#1 o #1) fixes));
+ val spec_name = Binding.conglomerate (map (#1 o #1) fixes);
fun attr_bindings prefix = map (fn ((b, attrs), _) =>
(Binding.qualify false prefix b, attrs)) spec;
fun simp_attr_binding prefix =
--- a/src/HOL/Tools/inductive.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/inductive.ML Tue Dec 03 15:20:30 2019 +0100
@@ -71,7 +71,7 @@
term list -> (Attrib.binding * term) list -> thm list ->
term list -> (binding * mixfix) list ->
local_theory -> result * local_theory
- val declare_rules: binding -> bool -> bool -> string -> string list -> term list ->
+ val declare_rules: binding -> bool -> bool -> binding -> string list -> term list ->
thm list -> binding list -> Token.src list list -> (thm * string list * int) list ->
thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory
val add_ind_def: add_ind_def
@@ -1099,7 +1099,7 @@
val _ = message (quiet_mode andalso not verbose)
("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
- val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map #1 cnames_syn));
+ val spec_name = Binding.conglomerate (map #1 cnames_syn);
val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn; (* FIXME *)
val ((intr_names, intr_atts), intr_ts) =
apfst split_list (split_list (map (check_rule lthy cs params) intros));
--- a/src/HOL/Tools/inductive_set.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/inductive_set.ML Tue Dec 03 15:20:30 2019 +0100
@@ -503,7 +503,7 @@
val rec_name =
if Binding.is_empty alt_name then Binding.conglomerate (map #1 cnames_syn) else alt_name;
val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn; (* FIXME *)
- val spec_name = Local_Theory.full_name lthy3 (Binding.conglomerate (map #1 cnames_syn));
+ val spec_name = Binding.conglomerate (map #1 cnames_syn);
val (intr_names, intr_atts) = split_list (map fst intros);
val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
val (intrs', elims', eqs', induct, inducts, lthy4) =
--- a/src/HOL/Tools/record.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/HOL/Tools/record.ML Tue Dec 03 15:20:30 2019 +0100
@@ -1814,7 +1814,7 @@
fun add_spec_rule rule =
let val head = head_of (lhs_of_equation (Thm.prop_of rule))
- in Spec_Rules.add_global "" Spec_Rules.equational [head] [rule] end;
+ in Spec_Rules.add_global Binding.empty Spec_Rules.equational [head] [rule] end;
(* definition *)
--- a/src/Pure/General/binding.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/General/binding.ML Tue Dec 03 15:20:30 2019 +0100
@@ -122,7 +122,7 @@
fun is_empty_atts (b, atts) = is_empty b andalso null atts;
fun conglomerate [b] = b
- | conglomerate bs = name (space_implode "_" (map name_of bs));
+ | conglomerate bs = name (space_implode "_" (map name_of (filter_out is_empty bs)));
(* user qualifier *)
--- a/src/Pure/Isar/spec_rules.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/Isar/spec_rules.ML Tue Dec 03 15:20:30 2019 +0100
@@ -1,7 +1,9 @@
(* Title: Pure/Isar/spec_rules.ML
Author: Makarius
-Rules that characterize specifications, with rough classification.
+Rules that characterize specifications, with optional name and
+rough classification.
+
NB: In the face of arbitrary morphisms, the original shape of
specifications may get lost.
*)
@@ -11,6 +13,7 @@
datatype recursion =
Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion
val recursion_ord: recursion ord
+ val encode_recursion: recursion XML.Encode.T
datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown
val rough_classification_ord: rough_classification ord
val equational_primrec: string list -> rough_classification
@@ -23,14 +26,20 @@
val is_co_inductive: rough_classification -> bool
val is_relational: rough_classification -> bool
val is_unknown: rough_classification -> bool
- type spec =
- {name: string, rough_classification: rough_classification, terms: term list, rules: thm list}
- val get: Proof.context -> spec list
- val get_global: theory -> spec list
- val retrieve: Proof.context -> term -> spec list
- val retrieve_global: theory -> term -> spec list
- val add: string -> rough_classification -> term list -> thm list -> local_theory -> local_theory
- val add_global: string -> rough_classification -> term list -> thm list -> theory -> theory
+ val encode_rough_classification: rough_classification XML.Encode.T
+ type spec_rule =
+ {pos: Position.T,
+ name: string,
+ rough_classification: rough_classification,
+ terms: term list,
+ rules: thm list}
+ val get: Proof.context -> spec_rule list
+ val get_global: theory -> spec_rule list
+ val dest_theory: theory -> spec_rule list
+ val retrieve: Proof.context -> term -> spec_rule list
+ val retrieve_global: theory -> term -> spec_rule list
+ val add: binding -> rough_classification -> term list -> thm list -> local_theory -> local_theory
+ val add_global: binding -> rough_classification -> term list -> thm list -> theory -> theory
end;
structure Spec_Rules: SPEC_RULES =
@@ -48,6 +57,16 @@
| recursion_ord (Primcorec Ts1, Primcorec Ts2) = list_ord fast_string_ord (Ts1, Ts2)
| recursion_ord rs = int_ord (apply2 recursion_index rs);
+val encode_recursion =
+ let open XML.Encode in
+ variant
+ [fn Primrec a => ([], list string a),
+ fn Recdef => ([], []),
+ fn Primcorec a => ([], list string a),
+ fn Corec => ([], []),
+ fn Unknown_Recursion => ([], [])]
+ end;
+
(* rough classification *)
@@ -69,24 +88,38 @@
val is_relational = is_inductive orf is_co_inductive;
val is_unknown = fn Unknown => true | _ => false;
+val encode_rough_classification =
+ let open XML.Encode in
+ variant
+ [fn Equational r => ([], encode_recursion r),
+ fn Inductive => ([], []),
+ fn Co_Inductive => ([], []),
+ fn Unknown => ([], [])]
+ end;
+
(* rules *)
-type spec =
- {name: string, rough_classification: rough_classification, terms: term list, rules: thm list};
+type spec_rule =
+ {pos: Position.T,
+ name: string,
+ rough_classification: rough_classification,
+ terms: term list,
+ rules: thm list};
-fun eq_spec (specs: spec * spec) =
+fun eq_spec (specs: spec_rule * spec_rule) =
(op =) (apply2 #name specs) andalso
is_equal (rough_classification_ord (apply2 #rough_classification specs)) andalso
eq_list (op aconv) (apply2 #terms specs) andalso
eq_list Thm.eq_thm_prop (apply2 #rules specs);
-fun map_spec_rules f ({name, rough_classification, terms, rules}: spec) : spec =
- {name = name, rough_classification = rough_classification, terms = terms, rules = map f rules};
+fun map_spec_rules f ({pos, name, rough_classification, terms, rules}: spec_rule) : spec_rule =
+ {pos = pos, name = name, rough_classification = rough_classification, terms = terms,
+ rules = map f rules};
structure Rules = Generic_Data
(
- type T = spec Item_Net.T;
+ type T = spec_rule Item_Net.T;
val empty : T = Item_Net.init eq_spec #terms;
val extend = I;
val merge = Item_Net.merge;
@@ -95,17 +128,22 @@
(* get *)
-fun get_generic context =
+fun get_generic imports context =
let
val thy = Context.theory_of context;
val transfer = Global_Theory.transfer_theories thy;
+ fun imported spec =
+ imports |> exists (fn thy => Item_Net.member (Rules.get (Context.Theory thy)) spec);
in
Item_Net.content (Rules.get context)
+ |> filter_out imported
|> (map o map_spec_rules) transfer
end;
-val get = get_generic o Context.Proof;
-val get_global = get_generic o Context.Theory;
+val get = get_generic [] o Context.Proof;
+val get_global = get_generic [] o Context.Theory;
+
+fun dest_theory thy = rev (get_generic (Theory.parents_of thy) (Context.Theory thy));
(* retrieve *)
@@ -120,11 +158,13 @@
(* add *)
-fun add name rough_classification terms rules lthy =
+fun add b rough_classification terms rules lthy =
let val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules) in
lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => fn context =>
let
+ val pos = Position.thread_data ();
+ val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi b);
val (terms', rules') =
map (Thm.transfer (Context.theory_of context)) thms0
|> Morphism.fact phi
@@ -133,14 +173,17 @@
||> map Thm.trim_context;
in
context |> (Rules.map o Item_Net.update)
- {name = name, rough_classification = rough_classification,
+ {pos = pos, name = name, rough_classification = rough_classification,
terms = terms', rules = rules'}
end)
end;
-fun add_global name rough_classification terms rules =
- (Context.theory_map o Rules.map o Item_Net.update)
- {name = name, rough_classification = rough_classification,
- terms = terms, rules = map Thm.trim_context rules};
+fun add_global b rough_classification terms rules thy =
+ thy |> (Context.theory_map o Rules.map o Item_Net.update)
+ {pos = Position.thread_data (),
+ name = Sign.full_name thy b,
+ rough_classification = rough_classification,
+ terms = terms,
+ rules = map Thm.trim_context rules};
end;
--- a/src/Pure/Isar/specification.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/Isar/specification.ML Tue Dec 03 15:20:30 2019 +0100
@@ -216,6 +216,10 @@
val specs =
map ((apsnd o map) (prep_att vars_ctxt) o fst) raw_concls ~~ map close concls;
+ val spec_name =
+ Binding.conglomerate (if null decls then map (#1 o #1) specs else map (#1 o #1) decls);
+
+
(*consts*)
val (consts, consts_thy) = thy
|> fold_map (fn ((b, _, mx), (_, t)) => Theory.specify_const ((b, Term.type_of t), mx)) decls;
@@ -229,7 +233,7 @@
(*facts*)
val (facts, facts_lthy) = axioms_thy
|> Named_Target.theory_init
- |> Spec_Rules.add "" Spec_Rules.Unknown consts (maps (maps #1 o #2) axioms)
+ |> Spec_Rules.add spec_name Spec_Rules.Unknown consts (maps (maps #1 o #2) axioms)
|> Local_Theory.notes axioms;
in ((consts, map (the_single o #2) facts), Local_Theory.exit_global facts_lthy) end;
@@ -265,7 +269,7 @@
|> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
val th = prove lthy2 raw_th;
- val lthy3 = lthy2 |> Spec_Rules.add const_name Spec_Rules.equational [lhs] [th];
+ val lthy3 = lthy2 |> Spec_Rules.add name Spec_Rules.equational [lhs] [th];
val ([(def_name, [th'])], lthy4) = lthy3
|> Local_Theory.notes [((name, atts), [([th], [])])];
--- a/src/Pure/Proof/extraction.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/Proof/extraction.ML Tue Dec 03 15:20:30 2019 +0100
@@ -816,7 +816,6 @@
val fu = Type.legacy_freeze u;
val head = head_of (strip_abs_body fu);
val b = Binding.qualified_name (extr_name s vs);
- val const_name = Sign.full_name thy b;
in
thy
|> Sign.add_consts [(b, fastype_of ft, NoSyn)]
@@ -824,7 +823,8 @@
[((Binding.qualified_name (Thm.def_name (extr_name s vs)),
Logic.mk_equals (head, ft)), [])]
|-> (fn [def_thm] =>
- Spec_Rules.add_global const_name Spec_Rules.equational [head] [def_thm]
+ Spec_Rules.add_global b Spec_Rules.equational
+ [Thm.term_of (Thm.lhs_of def_thm)] [def_thm]
#> Code.declare_default_eqns_global [(def_thm, true)])
end;
--- a/src/Pure/Thy/export_theory.ML Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML Tue Dec 03 15:20:30 2019 +0100
@@ -67,7 +67,7 @@
|> the_default ([], false);
-(* locales content *)
+(* locales *)
fun locale_content thy loc =
let
@@ -141,14 +141,32 @@
val thy_ctxt = Proof_Context.init_global thy;
+ (* spec rules *)
+
+ fun position_properties pos =
+ Position.offset_properties_of (adjust_pos pos) @ Position.id_properties_of pos;
+
+ fun spec_rule_content {pos, name, rough_classification, terms, rules} =
+ let
+ val spec =
+ terms @ map Thm.plain_prop_of rules
+ |> Term_Subst.zero_var_indexes_list
+ |> map Logic.unvarify_global;
+ in
+ {props = position_properties pos,
+ name = name,
+ rough_classification = rough_classification,
+ typargs = rev (fold Term.add_tfrees spec []),
+ args = rev (fold Term.add_frees spec []),
+ terms = map (fn t => (t, Term.type_of t)) (take (length terms) spec),
+ rules = drop (length terms) spec}
+ end;
+
+
(* entities *)
fun make_entity_markup name xname pos serial =
- let
- val props =
- Position.offset_properties_of (adjust_pos pos) @
- Position.id_properties_of pos @
- Markup.serial_properties serial;
+ let val props = position_properties pos @ Markup.serial_properties serial;
in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
fun entity_markup space name =
@@ -232,6 +250,9 @@
val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
in ((sorts @ typargs, args, prop), proof) end;
+ fun standard_prop_of thm =
+ standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
+
val encode_prop =
let open XML.Encode Term_XML.Encode
in triple (list (pair string sort)) (list (pair string typ)) encode_term end;
@@ -247,6 +268,7 @@
(* theorems and proof terms *)
val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps;
+ val prep_thm = clean_thm #> Thm.unconstrainT;
val lookup_thm_id = Global_Theory.lookup_thm_id thy;
@@ -267,7 +289,7 @@
fun encode_thm thm_id raw_thm =
let
val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
- val thm = clean_thm (Thm.unconstrainT raw_thm);
+ val thm = prep_thm raw_thm;
val proof0 =
if Proofterm.export_standard_enabled () then
@@ -275,8 +297,7 @@
{full = true, expand_name = SOME o expand_name thm_id} thm
else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm
else MinProof;
- val (prop, SOME proof) =
- standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0);
+ val (prop, SOME proof) = standard_prop_of thm (SOME proof0);
val _ = Thm.expose_proofs thy [thm];
in
(prop, deps, proof) |>
@@ -397,6 +418,23 @@
if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs);
+ (* spec rules *)
+
+ val encode_specs =
+ let open XML.Encode Term_XML.Encode in
+ list (fn {props, name, rough_classification, typargs, args, terms, rules} =>
+ pair properties (pair string (pair Spec_Rules.encode_rough_classification
+ (pair (list (pair string sort)) (pair (list (pair string typ))
+ (pair (list (pair encode_term typ)) (list encode_term))))))
+ (props, (name, (rough_classification, (typargs, (args, (terms, rules)))))))
+ end;
+
+ val _ =
+ (case Spec_Rules.dest_theory thy of
+ [] => ()
+ | spec_rules => export_body thy "spec_rules" (encode_specs (map spec_rule_content spec_rules)));
+
+
(* parents *)
val _ =
--- a/src/Pure/Thy/export_theory.scala Mon Dec 02 17:51:54 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala Tue Dec 03 15:20:30 2019 +0100
@@ -42,6 +42,7 @@
arities: Boolean = true,
constdefs: Boolean = true,
typedefs: Boolean = true,
+ spec_rules: Boolean = true,
cache: Term.Cache = Term.make_cache()): Session =
{
val thys =
@@ -56,7 +57,8 @@
session, theory, types = types, consts = consts,
axioms = axioms, thms = thms, classes = classes, locales = locales,
locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
- constdefs = constdefs, typedefs = typedefs, cache = Some(cache))
+ constdefs = constdefs, typedefs = typedefs,
+ spec_rules = spec_rules, cache = Some(cache))
}
}
}))
@@ -90,7 +92,8 @@
classrel: List[Classrel],
arities: List[Arity],
constdefs: List[Constdef],
- typedefs: List[Typedef])
+ typedefs: List[Typedef],
+ spec_rules: List[Spec_Rule])
{
override def toString: String = name
@@ -116,7 +119,8 @@
classrel.map(_.cache(cache)),
arities.map(_.cache(cache)),
constdefs.map(_.cache(cache)),
- typedefs.map(_.cache(cache)))
+ typedefs.map(_.cache(cache)),
+ spec_rules.map(_.cache(cache)))
}
def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
@@ -131,6 +135,7 @@
arities: Boolean = true,
constdefs: Boolean = true,
typedefs: Boolean = true,
+ spec_rules: Boolean = true,
cache: Option[Term.Cache] = None): Theory =
{
val parents =
@@ -155,7 +160,8 @@
if (classrel) read_classrel(provider) else Nil,
if (arities) read_arities(provider) else Nil,
if (constdefs) read_constdefs(provider) else Nil,
- if (typedefs) read_typedefs(provider) else Nil)
+ if (typedefs) read_typedefs(provider) else Nil,
+ if (spec_rules) read_spec_rules(provider) else Nil)
if (cache.isDefined) theory.cache(cache.get) else theory
}
@@ -643,4 +649,102 @@
for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
}
+
+
+ /* Pure spec rules */
+
+ sealed abstract class Recursion
+ {
+ def cache(cache: Term.Cache): Recursion =
+ this match {
+ case Primrec(types) => Primrec(types.map(cache.string))
+ case Primcorec(types) => Primcorec(types.map(cache.string))
+ case _ => this
+ }
+ }
+ case class Primrec(types: List[String]) extends Recursion
+ case object Recdef extends Recursion
+ case class Primcorec(types: List[String]) extends Recursion
+ case object Corec extends Recursion
+ case object Unknown_Recursion extends Recursion
+
+ val decode_recursion: XML.Decode.T[Recursion] =
+ {
+ import XML.Decode._
+ variant(List(
+ { case (Nil, a) => Primrec(list(string)(a)) },
+ { case (Nil, Nil) => Recdef },
+ { case (Nil, a) => Primcorec(list(string)(a)) },
+ { case (Nil, Nil) => Corec },
+ { case (Nil, Nil) => Unknown_Recursion }))
+ }
+
+
+ sealed abstract class Rough_Classification
+ {
+ def is_equational: Boolean = this.isInstanceOf[Equational]
+ def is_inductive: Boolean = this == Inductive
+ def is_co_inductive: Boolean = this == Co_Inductive
+ def is_relational: Boolean = is_inductive || is_co_inductive
+ def is_unknown: Boolean = this == Unknown
+
+ def cache(cache: Term.Cache): Rough_Classification =
+ this match {
+ case Equational(recursion) => Equational(recursion.cache(cache))
+ case _ => this
+ }
+ }
+ case class Equational(recursion: Recursion) extends Rough_Classification
+ case object Inductive extends Rough_Classification
+ case object Co_Inductive extends Rough_Classification
+ case object Unknown extends Rough_Classification
+
+ val decode_rough_classification: XML.Decode.T[Rough_Classification] =
+ {
+ import XML.Decode._
+ variant(List(
+ { case (Nil, a) => Equational(decode_recursion(a)) },
+ { case (Nil, Nil) => Inductive },
+ { case (Nil, Nil) => Co_Inductive },
+ { case (Nil, Nil) => Unknown }))
+ }
+
+
+ sealed case class Spec_Rule(
+ pos: Position.T,
+ name: String,
+ rough_classification: Rough_Classification,
+ typargs: List[(String, Term.Sort)],
+ args: List[(String, Term.Typ)],
+ terms: List[(Term.Term, Term.Typ)],
+ rules: List[Term.Term])
+ {
+ def id: Option[Long] = Position.Id.unapply(pos)
+
+ def cache(cache: Term.Cache): Spec_Rule =
+ Spec_Rule(
+ cache.position(pos),
+ cache.string(name),
+ rough_classification.cache(cache),
+ typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
+ args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
+ terms.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }),
+ rules.map(cache.term(_)))
+ }
+
+ def read_spec_rules(provider: Export.Provider): List[Spec_Rule] =
+ {
+ val body = provider.uncompressed_yxml(export_prefix + "spec_rules")
+ val spec_rules =
+ {
+ import XML.Decode._
+ import Term_XML.Decode._
+ list(
+ pair(properties, pair(string, pair(decode_rough_classification,
+ pair(list(pair(string, sort)), pair(list(pair(string, typ)),
+ pair(list(pair(term, typ)), list(term))))))))(body)
+ }
+ for ((pos, (name, (rough_classification, (typargs, (args, (terms, rules)))))) <- spec_rules)
+ yield Spec_Rule(pos, name, rough_classification, typargs, args, terms, rules)
+ }
}