1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 17:26:05 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 17:26:05 2012 +0200
1.3 @@ -83,7 +83,7 @@
1.4 if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types ();
1.5
1.6 fun type_args_constrained_of (((cAs, _), _), _) = cAs;
1.7 -fun type_binder_of (((_, b), _), _) = b;
1.8 +fun type_binding_of (((_, b), _), _) = b;
1.9 fun mixfix_of ((_, mx), _) = mx;
1.10 fun ctr_specs_of (_, ctr_specs) = ctr_specs;
1.11
1.12 @@ -123,14 +123,14 @@
1.13 locale and shadows an existing global type*)
1.14 val fake_thy =
1.15 Theory.copy #> fold (fn spec => perhaps (try (Sign.add_type no_defs_lthy
1.16 - (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs;
1.17 + (type_binding_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs;
1.18 val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;
1.19
1.20 fun mk_fake_T b =
1.21 Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))),
1.22 unsorted_As);
1.23
1.24 - val fp_bs = map type_binder_of specs;
1.25 + val fp_bs = map type_binding_of specs;
1.26 val fake_Ts = map mk_fake_T fp_bs;
1.27
1.28 val mixfixes = map mixfix_of specs;
1.29 @@ -140,14 +140,14 @@
1.30
1.31 val ctr_specss = map ctr_specs_of specs;
1.32
1.33 - val disc_binderss = map (map disc_of) ctr_specss;
1.34 - val ctr_binderss =
1.35 + val disc_bindingss = map (map disc_of) ctr_specss;
1.36 + val ctr_bindingss =
1.37 map2 (fn fp_b => map (Binding.qualify false (Binding.name_of fp_b) o ctr_of))
1.38 fp_bs ctr_specss;
1.39 val ctr_argsss = map (map args_of) ctr_specss;
1.40 val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
1.41
1.42 - val sel_bindersss = map (map (map fst)) ctr_argsss;
1.43 + val sel_bindingsss = map (map (map fst)) ctr_argsss;
1.44 val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
1.45 val raw_sel_defaultsss = map (map defaults_of) ctr_specss;
1.46
1.47 @@ -218,8 +218,8 @@
1.48
1.49 fun mk_iter_like Ts Us t =
1.50 let
1.51 - val (binders, body) = strip_type (fastype_of t);
1.52 - val (f_Us, prebody) = split_last binders;
1.53 + val (bindings, body) = strip_type (fastype_of t);
1.54 + val (f_Us, prebody) = split_last bindings;
1.55 val Type (_, Ts0) = if lfp then prebody else body;
1.56 val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us);
1.57 in
1.58 @@ -334,8 +334,8 @@
1.59 end;
1.60
1.61 fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec),
1.62 - fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_binders), ctr_mixfixes), ctr_Tss),
1.63 - disc_binders), sel_binderss), raw_sel_defaultss) no_defs_lthy =
1.64 + fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss),
1.65 + disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
1.66 let
1.67 val unfT = domain_type (fastype_of fld);
1.68 val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
1.69 @@ -353,7 +353,7 @@
1.70 map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $
1.71 mk_InN_balanced ctr_sum_prod_T n (HOLogic.mk_tuple xs) k)) ks xss;
1.72
1.73 - val case_binder = Binding.suffix_name ("_" ^ caseN) fp_b;
1.74 + val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b;
1.75
1.76 val case_rhs =
1.77 fold_rev Term.lambda (fs @ [v])
1.78 @@ -362,7 +362,7 @@
1.79 val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
1.80 |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
1.81 Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
1.82 - (case_binder :: ctr_binders) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
1.83 + (case_binding :: ctr_bindings) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
1.84 ||> `Local_Theory.restore;
1.85
1.86 val phi = Proof_Context.export_morphism lthy lthy';
1.87 @@ -420,25 +420,23 @@
1.88 fun generate_iter_like (suf, fp_iter_like, (fss, f_Tss, xssss)) =
1.89 let
1.90 val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
1.91 -
1.92 - val binder = Binding.suffix_name ("_" ^ suf) fp_b;
1.93 -
1.94 + val binding = Binding.suffix_name ("_" ^ suf) fp_b;
1.95 val spec =
1.96 - mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binder, res_T)),
1.97 + mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
1.98 Term.list_comb (fp_iter_like,
1.99 map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss));
1.100 - in (binder, spec) end;
1.101 + in (binding, spec) end;
1.102
1.103 val iter_like_infos =
1.104 [(iterN, fp_iter, iter_only),
1.105 (recN, fp_rec, rec_only)];
1.106
1.107 - val (binders, specs) = map generate_iter_like iter_like_infos |> split_list;
1.108 + val (bindings, specs) = map generate_iter_like iter_like_infos |> split_list;
1.109
1.110 val ((csts, defs), (lthy', lthy)) = no_defs_lthy
1.111 |> apfst split_list o fold_map2 (fn b => fn spec =>
1.112 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
1.113 - #>> apsnd snd) binders specs
1.114 + #>> apsnd snd) bindings specs
1.115 ||> `Local_Theory.restore;
1.116
1.117 val phi = Proof_Context.export_morphism lthy lthy';
1.118 @@ -463,25 +461,23 @@
1.119 pf_Tss))) =
1.120 let
1.121 val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
1.122 -
1.123 - val binder = Binding.suffix_name ("_" ^ suf) fp_b;
1.124 -
1.125 + val binding = Binding.suffix_name ("_" ^ suf) fp_b;
1.126 val spec =
1.127 - mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)),
1.128 + mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),
1.129 Term.list_comb (fp_iter_like,
1.130 map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss));
1.131 - in (binder, spec) end;
1.132 + in (binding, spec) end;
1.133
1.134 val coiter_like_infos =
1.135 [(coiterN, fp_iter, coiter_only),
1.136 (corecN, fp_rec, corec_only)];
1.137
1.138 - val (binders, specs) = map generate_coiter_like coiter_like_infos |> split_list;
1.139 + val (bindings, specs) = map generate_coiter_like coiter_like_infos |> split_list;
1.140
1.141 val ((csts, defs), (lthy', lthy)) = no_defs_lthy
1.142 |> apfst split_list o fold_map2 (fn b => fn spec =>
1.143 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
1.144 - #>> apsnd snd) binders specs
1.145 + #>> apsnd snd) bindings specs
1.146 ||> `Local_Theory.restore;
1.147
1.148 val phi = Proof_Context.export_morphism lthy lthy';
1.149 @@ -496,7 +492,7 @@
1.150
1.151 fun wrap lthy =
1.152 let val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss in
1.153 - wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, (sel_binderss,
1.154 + wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss,
1.155 sel_defaultss))) lthy
1.156 end;
1.157
1.158 @@ -685,8 +681,8 @@
1.159
1.160 val lthy' = lthy
1.161 |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
1.162 - fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~
1.163 - ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss ~~ raw_sel_defaultsss)
1.164 + fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
1.165 + ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
1.166 |>> split_list |> wrap_types_and_define_iter_likes
1.167 |> (if lfp then derive_iter_rec_thms_for_types else derive_coiter_corec_thms_for_types);
1.168
1.169 @@ -701,11 +697,11 @@
1.170 val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
1.171
1.172 val parse_binding_colon = Parse.binding --| @{keyword ":"};
1.173 -val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binder;
1.174 +val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binding;
1.175
1.176 val parse_ctr_arg =
1.177 @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
1.178 - (Parse.typ >> pair no_binder);
1.179 + (Parse.typ >> pair no_binding);
1.180
1.181 val parse_defaults =
1.182 @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
2.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 12 17:26:05 2012 +0200
2.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 12 17:26:05 2012 +0200
2.3 @@ -7,7 +7,7 @@
2.4
2.5 signature BNF_WRAP =
2.6 sig
2.7 - val no_binder: binding
2.8 + val no_binding: binding
2.9 val mk_half_pairss: 'a list -> ('a * 'a) list list
2.10 val mk_ctr: typ list -> term -> term
2.11 val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
2.12 @@ -45,8 +45,8 @@
2.13 val split_asmN = "split_asm";
2.14 val weak_case_cong_thmsN = "weak_case_cong";
2.15
2.16 -val no_binder = @{binding ""};
2.17 -val std_binder = @{binding _};
2.18 +val no_binding = @{binding ""};
2.19 +val std_binding = @{binding _};
2.20
2.21 val induct_simp_attrs = @{attributes [induct_simp]};
2.22 val cong_attrs = @{attributes [cong]};
2.23 @@ -80,7 +80,7 @@
2.24 | _ => error "Cannot extract name of constructor");
2.25
2.26 fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case),
2.27 - (raw_disc_binders, (raw_sel_binderss, raw_sel_defaultss))) no_defs_lthy =
2.28 + (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
2.29 let
2.30 (* TODO: sanity checks on arguments *)
2.31 (* TODO: attributes (simp, case_names, etc.) *)
2.32 @@ -111,47 +111,47 @@
2.33
2.34 val ms = map length ctr_Tss;
2.35
2.36 - val raw_disc_binders' = pad_list no_binder n raw_disc_binders;
2.37 + val raw_disc_bindings' = pad_list no_binding n raw_disc_bindings;
2.38
2.39 fun can_really_rely_on_disc k =
2.40 - not (Binding.eq_name (nth raw_disc_binders' (k - 1), no_binder)) orelse nth ms (k - 1) = 0;
2.41 + not (Binding.eq_name (nth raw_disc_bindings' (k - 1), no_binding)) orelse nth ms (k - 1) = 0;
2.42 fun can_rely_on_disc k =
2.43 can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2));
2.44 - fun can_omit_disc_binder k m =
2.45 + fun can_omit_disc_binding k m =
2.46 n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k));
2.47
2.48 - val std_disc_binder =
2.49 + val std_disc_binding =
2.50 Binding.qualify false (Binding.name_of data_b) o Binding.name o prefix isN o base_name_of_ctr;
2.51
2.52 - val disc_binders =
2.53 - raw_disc_binders'
2.54 + val disc_bindings =
2.55 + raw_disc_bindings'
2.56 |> map4 (fn k => fn m => fn ctr => fn disc =>
2.57 Option.map (Binding.qualify false (Binding.name_of data_b))
2.58 - (if Binding.eq_name (disc, no_binder) then
2.59 - if can_omit_disc_binder k m then NONE else SOME (std_disc_binder ctr)
2.60 - else if Binding.eq_name (disc, std_binder) then
2.61 - SOME (std_disc_binder ctr)
2.62 + (if Binding.eq_name (disc, no_binding) then
2.63 + if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr)
2.64 + else if Binding.eq_name (disc, std_binding) then
2.65 + SOME (std_disc_binding ctr)
2.66 else
2.67 SOME disc)) ks ms ctrs0;
2.68
2.69 - val no_discs = map is_none disc_binders;
2.70 + val no_discs = map is_none disc_bindings;
2.71 val no_discs_at_all = forall I no_discs;
2.72
2.73 - fun std_sel_binder m l = Binding.name o mk_unN m l o base_name_of_ctr;
2.74 + fun std_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
2.75
2.76 - val sel_binderss =
2.77 - pad_list [] n raw_sel_binderss
2.78 + val sel_bindingss =
2.79 + pad_list [] n raw_sel_bindingss
2.80 |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
2.81 Binding.qualify false (Binding.name_of data_b)
2.82 - (if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, std_binder) then
2.83 - std_sel_binder m l ctr
2.84 + (if Binding.eq_name (sel, no_binding) orelse Binding.eq_name (sel, std_binding) then
2.85 + std_sel_binding m l ctr
2.86 else
2.87 - sel)) (1 upto m) o pad_list no_binder m) ctrs0 ms;
2.88 + sel)) (1 upto m) o pad_list no_binding m) ctrs0 ms;
2.89
2.90 fun mk_case Ts T =
2.91 let
2.92 - val (binders, body) = strip_type (fastype_of case0)
2.93 - val Type (_, Ts0) = List.last binders
2.94 + val (bindings, body) = strip_type (fastype_of case0)
2.95 + val Type (_, Ts0) = List.last bindings
2.96 in Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) case0 end;
2.97
2.98 val casex = mk_case As B;
2.99 @@ -191,7 +191,7 @@
2.100
2.101 fun alternate_disc_lhs get_disc k =
2.102 HOLogic.mk_not
2.103 - (case nth disc_binders (k - 1) of
2.104 + (case nth disc_bindings (k - 1) of
2.105 NONE => nth exist_xs_v_eq_ctrs (k - 1)
2.106 | SOME b => get_disc b (k - 1) $ v);
2.107
2.108 @@ -237,22 +237,22 @@
2.109 Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ v)
2.110 end;
2.111
2.112 - val sel_binders = flat sel_binderss;
2.113 - val uniq_sel_binders = distinct Binding.eq_name sel_binders;
2.114 - val all_sels_distinct = (length uniq_sel_binders = length sel_binders);
2.115 + val sel_bindings = flat sel_bindingss;
2.116 + val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
2.117 + val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
2.118
2.119 - val sel_binder_index =
2.120 - if all_sels_distinct then 1 upto length sel_binders
2.121 - else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_binders) sel_binders;
2.122 + val sel_binding_index =
2.123 + if all_sels_distinct then 1 upto length sel_bindings
2.124 + else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
2.125
2.126 val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
2.127 val sel_infos =
2.128 - AList.group (op =) (sel_binder_index ~~ proto_sels)
2.129 + AList.group (op =) (sel_binding_index ~~ proto_sels)
2.130 |> sort (int_ord o pairself fst)
2.131 - |> map snd |> curry (op ~~) uniq_sel_binders;
2.132 - val sel_binders = map fst sel_infos;
2.133 + |> map snd |> curry (op ~~) uniq_sel_bindings;
2.134 + val sel_bindings = map fst sel_infos;
2.135
2.136 - fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss;
2.137 + fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss;
2.138
2.139 val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
2.140 no_defs_lthy
2.141 @@ -263,7 +263,7 @@
2.142 else pair (alternate_disc k, alternate_disc_no_def)
2.143 | SOME b => Specification.definition (SOME (b, NONE, NoSyn),
2.144 ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd)
2.145 - ks ms exist_xs_v_eq_ctrs disc_binders
2.146 + ks ms exist_xs_v_eq_ctrs disc_bindings
2.147 ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
2.148 Specification.definition (SOME (b, NONE, NoSyn),
2.149 ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos