--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 30 14:07:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 30 14:17:19 2013 +0200
@@ -602,8 +602,8 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
- val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
- val nested_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
+ val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
+ val nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
val nested_set_maps = maps set_map_of_bnf nested_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -726,7 +726,7 @@
val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss;
val tacss =
- map2 (map o mk_iter_tac pre_map_defs (nested_map_id's @ nesting_map_id's) iter_defs)
+ map2 (map o mk_iter_tac pre_map_defs (nested_map_idents @ nesting_map_idents) iter_defs)
ctor_iter_thms ctr_defss;
fun prove goal tac =
@@ -763,7 +763,7 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
- val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
+ val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -919,10 +919,10 @@
val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
val unfold_tacss =
- map3 (map oo mk_coiter_tac unfold_defs nesting_map_id's)
+ map3 (map oo mk_coiter_tac unfold_defs nesting_map_idents)
(map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
val corec_tacss =
- map3 (map oo mk_coiter_tac corec_defs nesting_map_id's)
+ map3 (map oo mk_coiter_tac corec_defs nesting_map_idents)
(map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
fun prove goal tac =
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Fri Aug 30 14:07:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Fri Aug 30 14:17:19 2013 +0200
@@ -94,17 +94,17 @@
@{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv
split_conv unit_case_Unity} @ sum_prod_thms_map;
-fun mk_iter_tac pre_map_defs map_id's iter_defs ctor_iter ctr_def ctxt =
- unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_id's @
+fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter ctr_def ctxt =
+ unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_idents @
iter_unfold_thms) THEN HEADGOAL (rtac refl);
val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
-fun mk_coiter_tac coiter_defs map_id's ctor_dtor_coiter pre_map_def ctr_def ctxt =
+fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def ctr_def ctxt =
unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN
HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN'
asm_simp_tac (put_simpset ss_if_True_False ctxt)) THEN_MAYBE
- (unfold_thms_tac ctxt (pre_map_def :: map_id's @ coiter_unfold_thms) THEN
+ (unfold_thms_tac ctxt (pre_map_def :: map_idents @ coiter_unfold_thms) THEN
HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)));
fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt =
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Aug 30 14:07:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Aug 30 14:17:19 2013 +0200
@@ -14,10 +14,6 @@
Proof.state
end;
-(* TODO:
- - error handling for indirect calls
-*)
-
structure BNF_FP_Rec_Sugar : BNF_FP_REC_SUGAR =
struct
@@ -341,7 +337,7 @@
val defs = build_defs lthy' bs funs_data rec_specs get_indices;
- fun prove def_thms' {ctr_specs, nested_map_id's, nested_map_comps, ...} induct_thm fun_data
+ fun prove def_thms' {ctr_specs, nested_map_idents, nested_map_comps, ...} induct_thm fun_data
lthy =
let
val fun_name = #fun_name (hd fun_data);
@@ -351,7 +347,7 @@
|> map_filter (try (fn (x, [y]) =>
(#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
|> map (fn (user_eqn, num_extra_args, rec_thm) =>
- mk_primrec_tac lthy num_extra_args nested_map_id's nested_map_comps def_thms rec_thm
+ mk_primrec_tac lthy num_extra_args nested_map_idents nested_map_comps def_thms rec_thm
|> K |> Goal.prove lthy [] [] user_eqn)
val notes =
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Fri Aug 30 14:07:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Fri Aug 30 14:17:19 2013 +0200
@@ -22,10 +22,10 @@
open BNF_Util
open BNF_Tactics
-fun mk_primrec_tac ctxt num_extra_args map_id's map_comps fun_defs recx =
+fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx =
unfold_thms_tac ctxt fun_defs THEN
HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
- unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_id's) THEN
+ unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_idents) THEN
HEADGOAL (rtac refl);
fun mk_primcorec_taut_tac ctxt =
@@ -54,10 +54,10 @@
fun mk_primcorec_disc_tac ctxt defs disc k m exclsss =
mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
-fun mk_primcorec_eq_tac ctxt defs sel k m exclsss maps map_id's map_comps =
+fun mk_primcorec_eq_tac ctxt defs sel k m exclsss maps map_idents map_comps =
mk_primcorec_prelude ctxt defs (sel RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @
- maps @ map_comps @ map_id's) THEN HEADGOAL (rtac refl);
+ maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl);
fun mk_primcorec_dtr_to_ctr_tac ctxt m collapse disc sels =
HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Fri Aug 30 14:07:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Fri Aug 30 14:17:19 2013 +0200
@@ -35,7 +35,7 @@
type rec_spec =
{recx: term,
- nested_map_id's: thm list,
+ nested_map_idents: thm list,
nested_map_comps: thm list,
ctr_specs: rec_ctr_spec list}
@@ -94,7 +94,7 @@
type rec_spec =
{recx: term,
- nested_map_id's: thm list,
+ nested_map_idents: thm list,
nested_map_comps: thm list,
ctr_specs: rec_ctr_spec list};
@@ -336,7 +336,7 @@
fun mk_spec {T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...} =
{recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
- nested_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
+ nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
nested_map_comps = map map_comp_of_bnf nested_bnfs,
ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
in