--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Dec 28 17:22:16 2016 +0100
@@ -82,17 +82,17 @@
val gfp_rec_sugar_interpretation: string ->
(BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
- val primcorec_ursive: bool -> corec_option list -> ((binding * typ) * mixfix) list ->
+ val primcorec_ursive: bool -> bool -> corec_option list -> ((binding * typ) * mixfix) list ->
((binding * Token.T list list) * term) list -> term option list -> Proof.context ->
(term * 'a list) list list * (thm list list -> local_theory -> local_theory) * local_theory
- val primcorec_ursive_cmd: bool -> corec_option list ->
+ val primcorec_ursive_cmd: bool -> bool -> corec_option list ->
(binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
Proof.context ->
(term * 'a list) list list * (thm list list -> local_theory -> local_theory) * local_theory
- val primcorecursive_cmd: corec_option list ->
+ val primcorecursive_cmd: bool -> corec_option list ->
(binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
Proof.context -> Proof.state
- val primcorec_cmd: corec_option list ->
+ val primcorec_cmd: bool -> corec_option list ->
(binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
local_theory -> local_theory
end;
@@ -1082,7 +1082,7 @@
fun is_trivial_implies thm =
uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm));
-fun primcorec_ursive auto opts fixes specs of_specs_opt lthy =
+fun primcorec_ursive int auto opts fixes specs of_specs_opt lthy =
let
val thy = Proof_Context.theory_of lthy;
@@ -1581,12 +1581,15 @@
end)
end;
- fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';
+ fun after_qed thmss' =
+ fold_map Local_Theory.define defs
+ #> tap (uncurry (print_def_consts int))
+ #-> prove thmss';
in
(goalss, after_qed, lthy)
end;
-fun primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy =
+fun primcorec_ursive_cmd int auto opts (raw_fixes, raw_specs_of) lthy =
let
val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes);
val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups));
@@ -1596,17 +1599,18 @@
val (fixes, specs) =
fst (Specification.read_multi_specs raw_fixes (map (fn spec => (spec, [], [])) raw_specs) lthy);
in
- primcorec_ursive auto opts fixes specs of_specs_opt lthy
+ primcorec_ursive int auto opts fixes specs of_specs_opt lthy
end;
-val primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
- lthy
- |> Proof.theorem NONE after_qed goalss
- |> Proof.refine_singleton (Method.primitive_text (K I))) ooo primcorec_ursive_cmd false;
+fun primcorecursive_cmd int = (fn (goalss, after_qed, lthy) =>
+ lthy
+ |> Proof.theorem NONE after_qed goalss
+ |> Proof.refine_singleton (Method.primitive_text (K I))) ooo
+ primcorec_ursive_cmd int false;
-val primcorec_cmd = (fn (goalss, after_qed, lthy) =>
+fun primcorec_cmd int = (fn (goalss, after_qed, lthy) =>
lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo
- primcorec_ursive_cmd true;
+ primcorec_ursive_cmd int true;
val corec_option_parser = Parse.group (K "option")
(Plugin_Name.parse_filter >> Plugins_Option
@@ -1621,13 +1625,13 @@
"define primitive corecursive functions"
((Scan.optional (@{keyword "("} |--
Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
- (Parse.vars -- where_alt_props_of_parser) >> uncurry primcorecursive_cmd);
+ (Parse.vars -- where_alt_props_of_parser) >> uncurry (primcorecursive_cmd true));
val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
"define primitive corecursive functions"
((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
--| @{keyword ")"}) []) --
- (Parse.vars -- where_alt_props_of_parser) >> uncurry primcorec_cmd);
+ (Parse.vars -- where_alt_props_of_parser) >> uncurry (primcorec_cmd true));
val _ = Theory.setup (gfp_rec_sugar_interpretation transfer_plugin
gfp_rec_sugar_transfer_interpretation);