--- a/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 13:56:57 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200
@@ -92,7 +92,7 @@
val mk_set_minimalN: int -> string
val mk_set_inductN: int -> string
- val mk_common_name: binding list -> string
+ val mk_common_name: string list -> string
val split_conj_thm: thm -> thm list
val split_conj_prems: int -> thm -> thm
@@ -246,7 +246,7 @@
val sel_coitersN = selN ^ "_" ^ coitersN
val sel_corecsN = selN ^ "_" ^ corecsN
-val mk_common_name = space_implode "_" o map Binding.name_of;
+val mk_common_name = space_implode "_";
fun retype_free T (Free (s, _)) = Free (s, T);
@@ -377,7 +377,7 @@
fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
let
- val name = mk_common_name bs;
+ val name = mk_common_name (map Binding.name_of bs);
fun qualify i =
let val namei = name ^ nonzero_string_of_int i;
in Binding.qualify true namei end;
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 21 13:56:57 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 21 15:53:29 2012 +0200
@@ -52,11 +52,11 @@
fun mk_uncurried2_fun f xss =
mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss);
-fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v));
+fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));
-fun tack z_name (c, v) f =
- let val z = Free (z_name, mk_sumT (fastype_of v, fastype_of c)) in
- Term.lambda z (mk_sum_case (Term.lambda v v, Term.lambda c (f $ c)) $ z)
+fun tack z_name (c, u) f =
+ let val z = Free (z_name, mk_sumT (fastype_of u, fastype_of c)) in
+ Term.lambda z (mk_sum_case (Term.lambda u u, Term.lambda c (f $ c)) $ z)
end;
fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters";
@@ -92,7 +92,8 @@
val nn = length specs;
val fp_bs = map type_binding_of specs;
- val fp_common_name = mk_common_name fp_bs;
+ val fp_b_names = map Binding.name_of fp_bs;
+ val fp_common_name = mk_common_name fp_b_names;
fun prepare_type_arg (ty, c) =
let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
@@ -132,8 +133,7 @@
val disc_bindingss = map (map disc_of) ctr_specss;
val ctr_bindingss =
- map2 (fn fp_b => map (Binding.qualify false (Binding.name_of fp_b) o ctr_of))
- fp_bs ctr_specss;
+ map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
val ctr_argsss = map (map args_of) ctr_specss;
val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
@@ -333,19 +333,21 @@
fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss),
disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
let
+ val fp_b_name = Binding.name_of fp_b;
+
val unfT = domain_type (fastype_of fld);
val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts;
val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss;
- val ((((u, fs), xss), v'), _) =
+ val ((((w, fs), xss), u'), _) =
no_defs_lthy
- |> yield_singleton (mk_Frees "u") unfT
+ |> yield_singleton (mk_Frees "w") unfT
||>> mk_Frees "f" case_Ts
||>> mk_Freess "x" ctr_Tss
- ||>> yield_singleton (Variable.variant_fixes) (Binding.name_of fp_b);
+ ||>> yield_singleton Variable.variant_fixes fp_b_name;
- val v = Free (v', fpT);
+ val u = Free (u', fpT);
val ctr_rhss =
map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $
@@ -354,8 +356,8 @@
val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b;
val case_rhs =
- fold_rev Term.lambda (fs @ [v])
- (mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (unf $ v));
+ fold_rev Term.lambda (fs @ [u])
+ (mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (unf $ u));
val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
|> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
@@ -378,8 +380,8 @@
val fld_iff_unf_thm =
let
val goal =
- fold_rev Logic.all [u, v]
- (mk_Trueprop_eq (HOLogic.mk_eq (v, fld $ u), HOLogic.mk_eq (unf $ v, u)));
+ fold_rev Logic.all [w, u]
+ (mk_Trueprop_eq (HOLogic.mk_eq (u, fld $ w), HOLogic.mk_eq (unf $ u, w)));
in
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [unfT, fpT])
@@ -525,12 +527,12 @@
fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss,
iter_defs, rec_defs), lthy) =
let
- val (((phis, phis'), vs'), names_lthy) =
+ val (((phis, phis'), us'), names_lthy) =
lthy
|> mk_Frees' "P" (map mk_pred1T fpTs)
- ||>> Variable.variant_fixes (map Binding.name_of fp_bs);
+ ||>> Variable.variant_fixes fp_b_names;
- val vs = map2 (curry Free) vs' fpTs;
+ val us = map2 (curry Free) us' fpTs;
fun mk_sets_nested bnf =
let
@@ -595,7 +597,7 @@
val goal =
Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) phis vs)));
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) phis us)));
val kksss = map (map (map (fst o snd) o #2)) raw_premss;
@@ -629,7 +631,7 @@
else
(case find_index (curry (op =) T) fpTs of
~1 => build_map (build_call fiter_likes maybe_tick) T U
- | j => maybe_tick (nth vs j) (nth fiter_likes j));
+ | j => maybe_tick (nth us j) (nth fiter_likes j));
fun mk_U maybe_mk_prodT =
typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
@@ -696,11 +698,11 @@
val discIss = map #7 wrap_ress;
val sel_thmsss = map #8 wrap_ress;
- val (vs', _) =
+ val (us', _) =
lthy
- |> Variable.variant_fixes (map Binding.name_of fp_bs);
+ |> Variable.variant_fixes fp_b_names;
- val vs = map2 (curry Free) vs' fpTs;
+ val us = map2 (curry Free) us' fpTs;
val (coinduct_thms, coinduct_thm) =
let
@@ -728,7 +730,7 @@
else
(case find_index (curry (op =) U) fpTs of
~1 => build_map (build_call fiter_likes maybe_tack) T U
- | j => maybe_tack (nth cs j, nth vs j) (nth fiter_likes j));
+ | j => maybe_tack (nth cs j, nth us j) (nth fiter_likes j));
fun mk_U maybe_mk_sumT =
typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 13:56:57 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200
@@ -64,7 +64,7 @@
val ks = 1 upto n;
val m = live - n (*passive, if 0 don't generate a new BNF*);
val ls = 1 upto m;
- val b = Binding.name (mk_common_name bs);
+ val b = Binding.name (mk_common_name (map Binding.name_of bs));
(* TODO: check if m, n, etc., are sane *)
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 13:56:57 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 15:53:29 2012 +0200
@@ -33,7 +33,7 @@
val n = length bnfs; (*active*)
val ks = 1 upto n;
val m = live - n; (*passive, if 0 don't generate a new BNF*)
- val b = Binding.name (mk_common_name bs);
+ val b = Binding.name (mk_common_name (map Binding.name_of bs));
(* TODO: check if m, n, etc., are sane *)
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Fri Sep 21 13:56:57 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Fri Sep 21 15:53:29 2012 +0200
@@ -112,6 +112,7 @@
val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0));
val data_b = Binding.qualified_name dataT_name;
+ val data_b_name = Binding.name_of data_b;
val (As, B) =
no_defs_lthy
@@ -135,12 +136,12 @@
n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k));
val std_disc_binding =
- Binding.qualify false (Binding.name_of data_b) o Binding.name o prefix isN o base_name_of_ctr;
+ Binding.qualify false data_b_name o Binding.name o prefix isN o base_name_of_ctr;
val disc_bindings =
raw_disc_bindings'
|> map4 (fn k => fn m => fn ctr => fn disc =>
- Option.map (Binding.qualify false (Binding.name_of data_b))
+ Option.map (Binding.qualify false data_b_name)
(if Binding.eq_name (disc, Binding.empty) then
if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr)
else if Binding.eq_name (disc, std_binding) then
@@ -156,7 +157,7 @@
val sel_bindingss =
pad_list [] n raw_sel_bindingss
|> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
- Binding.qualify false (Binding.name_of data_b)
+ Binding.qualify false data_b_name
(if Binding.eq_name (sel, Binding.empty) orelse Binding.eq_name (sel, std_binding) then
std_sel_binding m l ctr
else
@@ -171,15 +172,16 @@
val casex = mk_case As B;
val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
- val ((((((((xss, xss'), yss), fs), gs), (u, u')), v), (p, p')), names_lthy) = no_defs_lthy |>
+ val (((((((xss, xss'), yss), fs), gs), [u', v']), (p, p')), names_lthy) = no_defs_lthy |>
mk_Freess' "x" ctr_Tss
||>> mk_Freess "y" ctr_Tss
||>> mk_Frees "f" case_Ts
||>> mk_Frees "g" case_Ts
- ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "u") dataT
- ||>> yield_singleton (mk_Frees "v") dataT
+ ||>> (apfst (map (rpair dataT)) oo Variable.variant_fixes) [data_b_name, data_b_name ^ "'"]
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
+ val u = Free u';
+ val v = Free v';
val q = Free (fst p', mk_pred1T B);
val xctrs = map2 (curry Term.list_comb) ctrs xss;
@@ -619,8 +621,7 @@
(weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
|> filter_out (null o #2)
|> map (fn (thmN, thms, attrs) =>
- ((Binding.qualify true (Binding.name_of data_b) (Binding.name thmN), attrs),
- [(thms, [])]));
+ ((Binding.qualify true data_b_name (Binding.name thmN), attrs), [(thms, [])]));
val notes' =
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]