1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 30 14:07:49 2013 +0200
1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 30 14:17:19 2013 +0200
1.3 @@ -602,8 +602,8 @@
1.4
1.5 val pre_map_defs = map map_def_of_bnf pre_bnfs;
1.6 val pre_set_defss = map set_defs_of_bnf pre_bnfs;
1.7 - val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
1.8 - val nested_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
1.9 + val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
1.10 + val nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
1.11 val nested_set_maps = maps set_map_of_bnf nested_bnfs;
1.12
1.13 val fp_b_names = map base_name_of_typ fpTs;
1.14 @@ -726,7 +726,7 @@
1.15 val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss;
1.16
1.17 val tacss =
1.18 - map2 (map o mk_iter_tac pre_map_defs (nested_map_id's @ nesting_map_id's) iter_defs)
1.19 + map2 (map o mk_iter_tac pre_map_defs (nested_map_idents @ nesting_map_idents) iter_defs)
1.20 ctor_iter_thms ctr_defss;
1.21
1.22 fun prove goal tac =
1.23 @@ -763,7 +763,7 @@
1.24
1.25 val pre_map_defs = map map_def_of_bnf pre_bnfs;
1.26 val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
1.27 - val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
1.28 + val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
1.29 val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
1.30
1.31 val fp_b_names = map base_name_of_typ fpTs;
1.32 @@ -919,10 +919,10 @@
1.33 val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
1.34
1.35 val unfold_tacss =
1.36 - map3 (map oo mk_coiter_tac unfold_defs nesting_map_id's)
1.37 + map3 (map oo mk_coiter_tac unfold_defs nesting_map_idents)
1.38 (map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
1.39 val corec_tacss =
1.40 - map3 (map oo mk_coiter_tac corec_defs nesting_map_id's)
1.41 + map3 (map oo mk_coiter_tac corec_defs nesting_map_idents)
1.42 (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
1.43
1.44 fun prove goal tac =
2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Fri Aug 30 14:07:49 2013 +0200
2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Fri Aug 30 14:17:19 2013 +0200
2.3 @@ -94,17 +94,17 @@
2.4 @{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv
2.5 split_conv unit_case_Unity} @ sum_prod_thms_map;
2.6
2.7 -fun mk_iter_tac pre_map_defs map_id's iter_defs ctor_iter ctr_def ctxt =
2.8 - unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_id's @
2.9 +fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter ctr_def ctxt =
2.10 + unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_idents @
2.11 iter_unfold_thms) THEN HEADGOAL (rtac refl);
2.12
2.13 val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
2.14
2.15 -fun mk_coiter_tac coiter_defs map_id's ctor_dtor_coiter pre_map_def ctr_def ctxt =
2.16 +fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def ctr_def ctxt =
2.17 unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN
2.18 HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN'
2.19 asm_simp_tac (put_simpset ss_if_True_False ctxt)) THEN_MAYBE
2.20 - (unfold_thms_tac ctxt (pre_map_def :: map_id's @ coiter_unfold_thms) THEN
2.21 + (unfold_thms_tac ctxt (pre_map_def :: map_idents @ coiter_unfold_thms) THEN
2.22 HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)));
2.23
2.24 fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt =
3.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Aug 30 14:07:49 2013 +0200
3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Aug 30 14:17:19 2013 +0200
3.3 @@ -14,10 +14,6 @@
3.4 Proof.state
3.5 end;
3.6
3.7 -(* TODO:
3.8 - - error handling for indirect calls
3.9 -*)
3.10 -
3.11 structure BNF_FP_Rec_Sugar : BNF_FP_REC_SUGAR =
3.12 struct
3.13
3.14 @@ -341,7 +337,7 @@
3.15
3.16 val defs = build_defs lthy' bs funs_data rec_specs get_indices;
3.17
3.18 - fun prove def_thms' {ctr_specs, nested_map_id's, nested_map_comps, ...} induct_thm fun_data
3.19 + fun prove def_thms' {ctr_specs, nested_map_idents, nested_map_comps, ...} induct_thm fun_data
3.20 lthy =
3.21 let
3.22 val fun_name = #fun_name (hd fun_data);
3.23 @@ -351,7 +347,7 @@
3.24 |> map_filter (try (fn (x, [y]) =>
3.25 (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
3.26 |> map (fn (user_eqn, num_extra_args, rec_thm) =>
3.27 - mk_primrec_tac lthy num_extra_args nested_map_id's nested_map_comps def_thms rec_thm
3.28 + mk_primrec_tac lthy num_extra_args nested_map_idents nested_map_comps def_thms rec_thm
3.29 |> K |> Goal.prove lthy [] [] user_eqn)
3.30
3.31 val notes =
4.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Fri Aug 30 14:07:49 2013 +0200
4.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Fri Aug 30 14:17:19 2013 +0200
4.3 @@ -22,10 +22,10 @@
4.4 open BNF_Util
4.5 open BNF_Tactics
4.6
4.7 -fun mk_primrec_tac ctxt num_extra_args map_id's map_comps fun_defs recx =
4.8 +fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx =
4.9 unfold_thms_tac ctxt fun_defs THEN
4.10 HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
4.11 - unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_id's) THEN
4.12 + unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_idents) THEN
4.13 HEADGOAL (rtac refl);
4.14
4.15 fun mk_primcorec_taut_tac ctxt =
4.16 @@ -54,10 +54,10 @@
4.17 fun mk_primcorec_disc_tac ctxt defs disc k m exclsss =
4.18 mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
4.19
4.20 -fun mk_primcorec_eq_tac ctxt defs sel k m exclsss maps map_id's map_comps =
4.21 +fun mk_primcorec_eq_tac ctxt defs sel k m exclsss maps map_idents map_comps =
4.22 mk_primcorec_prelude ctxt defs (sel RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
4.23 unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @
4.24 - maps @ map_comps @ map_id's) THEN HEADGOAL (rtac refl);
4.25 + maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl);
4.26
4.27 fun mk_primcorec_dtr_to_ctr_tac ctxt m collapse disc sels =
4.28 HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN
5.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Fri Aug 30 14:07:49 2013 +0200
5.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Fri Aug 30 14:17:19 2013 +0200
5.3 @@ -35,7 +35,7 @@
5.4
5.5 type rec_spec =
5.6 {recx: term,
5.7 - nested_map_id's: thm list,
5.8 + nested_map_idents: thm list,
5.9 nested_map_comps: thm list,
5.10 ctr_specs: rec_ctr_spec list}
5.11
5.12 @@ -94,7 +94,7 @@
5.13
5.14 type rec_spec =
5.15 {recx: term,
5.16 - nested_map_id's: thm list,
5.17 + nested_map_idents: thm list,
5.18 nested_map_comps: thm list,
5.19 ctr_specs: rec_ctr_spec list};
5.20
5.21 @@ -336,7 +336,7 @@
5.22
5.23 fun mk_spec {T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...} =
5.24 {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
5.25 - nested_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
5.26 + nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
5.27 nested_map_comps = map map_comp_of_bnf nested_bnfs,
5.28 ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
5.29 in