# HG changeset patch # User blanchet # Date 1348235609 -7200 # Node ID acc583e141677a42624b162c6dd05666ed91567e # Parent 860b7c6bd913ded93d8606ae6b8e3787a7b54154 tuned variable names diff -r 860b7c6bd913 -r acc583e14167 src/HOL/Codatatype/Tools/bnf_fp.ML --- 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; diff -r 860b7c6bd913 -r acc583e14167 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- 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); diff -r 860b7c6bd913 -r acc583e14167 src/HOL/Codatatype/Tools/bnf_gfp.ML --- 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 *) diff -r 860b7c6bd913 -r acc583e14167 src/HOL/Codatatype/Tools/bnf_lfp.ML --- 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 *) diff -r 860b7c6bd913 -r acc583e14167 src/HOL/Codatatype/Tools/bnf_wrap.ML --- 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)]