1.1 --- a/etc/isar-keywords.el Fri Sep 28 09:12:50 2012 +0200
1.2 +++ b/etc/isar-keywords.el Fri Sep 28 09:12:50 2012 +0200
1.3 @@ -342,6 +342,7 @@
1.4 "overloaded"
1.5 "permissive"
1.6 "pervasive"
1.7 + "rep_compat"
1.8 "shows"
1.9 "structure"
1.10 "unchecked"
2.1 --- a/src/HOL/BNF/BNF_Wrap.thy Fri Sep 28 09:12:50 2012 +0200
2.2 +++ b/src/HOL/BNF/BNF_Wrap.thy Fri Sep 28 09:12:50 2012 +0200
2.3 @@ -11,7 +11,8 @@
2.4 imports BNF_Util
2.5 keywords
2.6 "wrap_data" :: thy_goal and
2.7 - "no_dests"
2.8 + "no_dests" and
2.9 + "rep_compat"
2.10 begin
2.11
2.12 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
3.1 --- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML Fri Sep 28 09:12:50 2012 +0200
3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML Fri Sep 28 09:12:50 2012 +0200
3.3 @@ -10,7 +10,7 @@
3.4 val datatypes: bool ->
3.5 (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
3.6 BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
3.7 - bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
3.8 + (bool * bool) * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
3.9 (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
3.10 local_theory -> local_theory
3.11 val parse_datatype_cmd: bool ->
3.12 @@ -144,8 +144,8 @@
3.13 fun defaults_of ((_, ds), _) = ds;
3.14 fun ctr_mixfix_of (_, mx) = mx;
3.15
3.16 -fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp (no_dests, specs)
3.17 - no_defs_lthy0 =
3.18 +fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp
3.19 + (wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 =
3.20 let
3.21 (* TODO: sanity checks on arguments *)
3.22 (* TODO: integration with function package ("size") *)
3.23 @@ -153,6 +153,9 @@
3.24 val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
3.25 else ();
3.26
3.27 + fun qualify mandatory fp_b_name =
3.28 + Binding.qualify mandatory fp_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
3.29 +
3.30 val nn = length specs;
3.31 val fp_bs = map type_binding_of specs;
3.32 val fp_b_names = map Binding.name_of fp_bs;
3.33 @@ -198,7 +201,7 @@
3.34
3.35 val disc_bindingss = map (map disc_of) ctr_specss;
3.36 val ctr_bindingss =
3.37 - map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
3.38 + map2 (fn fp_b_name => map (qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
3.39 val ctr_argsss = map (map args_of) ctr_specss;
3.40 val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
3.41
3.42 @@ -424,7 +427,7 @@
3.43 map3 (fn k => fn xs => fn tuple_x => fold_rev Term.lambda xs (ctor $
3.44 mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs;
3.45
3.46 - val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b;
3.47 + val case_binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ caseN) fp_b);
3.48
3.49 val case_rhs =
3.50 fold_rev Term.lambda (fs @ [u])
3.51 @@ -490,7 +493,7 @@
3.52
3.53 val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
3.54 in
3.55 - wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss,
3.56 + wrap_datatype tacss (((wrap_opts, ctrs0), casex0), (disc_bindings, (sel_bindingss,
3.57 sel_defaultss))) lthy
3.58 end;
3.59
3.60 @@ -566,7 +569,7 @@
3.61 (setsN, flat set_thmss, code_simp_attrs)]
3.62 |> filter_out (null o #2)
3.63 |> map (fn (thmN, thms, attrs) =>
3.64 - ((Binding.qualify true fp_b_name (Binding.name thmN), attrs), [(thms, [])]));
3.65 + ((qualify true fp_b_name (Binding.name thmN), attrs), [(thms, [])]));
3.66 in
3.67 (wrap_res, lthy |> Local_Theory.notes notes |> snd)
3.68 end;
3.69 @@ -578,7 +581,7 @@
3.70 fun generate_rec_like (suf, fp_rec_like, (fss, f_Tss, xssss)) =
3.71 let
3.72 val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
3.73 - val binding = Binding.suffix_name ("_" ^ suf) fp_b;
3.74 + val binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b);
3.75 val spec =
3.76 mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
3.77 Term.list_comb (fp_rec_like,
3.78 @@ -618,7 +621,7 @@
3.79 pf_Tss))) =
3.80 let
3.81 val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
3.82 - val binding = Binding.suffix_name ("_" ^ suf) fp_b;
3.83 + val binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b);
3.84 val spec =
3.85 mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),
3.86 Term.list_comb (fp_rec_like,
3.87 @@ -820,18 +823,18 @@
3.88 val common_notes =
3.89 (if nn > 1 then [(inductN, [induct_thm], [induct_case_names_attr])] else [])
3.90 |> map (fn (thmN, thms, attrs) =>
3.91 - ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
3.92 + ((qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
3.93
3.94 val notes =
3.95 - [(inductN, map single induct_thms,
3.96 + [(foldN, fold_thmss, K code_simp_attrs),
3.97 + (inductN, map single induct_thms,
3.98 fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
3.99 - (foldN, fold_thmss, K code_simp_attrs),
3.100 (recN, rec_thmss, K code_simp_attrs),
3.101 (simpsN, simp_thmss, K [])]
3.102 |> maps (fn (thmN, thmss, attrs) =>
3.103 - map3 (fn b => fn Type (T_name, _) => fn thms =>
3.104 - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name),
3.105 - [(thms, [])])) fp_bs fpTs thmss);
3.106 + map3 (fn fp_b_name => fn Type (T_name, _) => fn thms =>
3.107 + ((qualify true fp_b_name (Binding.name thmN), attrs T_name),
3.108 + [(thms, [])])) fp_b_names fpTs thmss);
3.109 in
3.110 lthy |> Local_Theory.notes (common_notes @ notes) |> snd
3.111 end;
3.112 @@ -1081,7 +1084,7 @@
3.113 else
3.114 [])
3.115 |> map (fn (thmN, thms, attrs) =>
3.116 - ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
3.117 + ((qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
3.118
3.119 val notes =
3.120 [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
3.121 @@ -1096,9 +1099,9 @@
3.122 (strong_coinductN, map single strong_coinduct_thms, []), (* FIXME: attribs *)
3.123 (unfoldN, unfold_thmss, [])]
3.124 |> maps (fn (thmN, thmss, attrs) =>
3.125 - map_filter (fn (_, []) => NONE | (b, thms) =>
3.126 - SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
3.127 - [(thms, [])])) (fp_bs ~~ thmss));
3.128 + map_filter (fn (_, []) => NONE | (fp_b_name, thms) =>
3.129 + SOME ((qualify true fp_b_name (Binding.name thmN), attrs),
3.130 + [(thms, [])])) (fp_b_names ~~ thmss));
3.131 in
3.132 lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
3.133 end;
4.1 --- a/src/HOL/BNF/Tools/bnf_wrap.ML Fri Sep 28 09:12:50 2012 +0200
4.2 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML Fri Sep 28 09:12:50 2012 +0200
4.3 @@ -7,6 +7,8 @@
4.4
4.5 signature BNF_WRAP =
4.6 sig
4.7 + val rep_compat_prefix: string
4.8 +
4.9 val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
4.10 val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
4.11
4.12 @@ -16,11 +18,11 @@
4.13 val name_of_ctr: term -> string
4.14
4.15 val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
4.16 - ((bool * term list) * term) *
4.17 + (((bool * bool) * term list) * term) *
4.18 (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
4.19 (term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
4.20 thm list list) * local_theory
4.21 - val parse_wrap_options: bool parser
4.22 + val parse_wrap_options: (bool * bool) parser
4.23 val parse_bound_term: (binding * string) parser
4.24 end;
4.25
4.26 @@ -30,6 +32,8 @@
4.27 open BNF_Util
4.28 open BNF_Wrap_Tactics
4.29
4.30 +val rep_compat_prefix = "new";
4.31 +
4.32 val isN = "is_";
4.33 val unN = "un_";
4.34 fun mk_unN 1 1 suf = unN ^ suf
4.35 @@ -49,6 +53,7 @@
4.36 val nchotomyN = "nchotomy";
4.37 val selsN = "sels";
4.38 val splitN = "split";
4.39 +val splitsN = "splits";
4.40 val split_asmN = "split_asm";
4.41 val weak_case_cong_thmsN = "weak_case_cong";
4.42
4.43 @@ -103,7 +108,7 @@
4.44
4.45 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
4.46
4.47 -fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case),
4.48 +fun prepare_wrap_datatype prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case),
4.49 (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
4.50 let
4.51 (* TODO: sanity checks on arguments *)
4.52 @@ -123,6 +128,10 @@
4.53 val data_b = Binding.qualified_name dataT_name;
4.54 val data_b_name = Binding.name_of data_b;
4.55
4.56 + fun qualify mandatory =
4.57 + Binding.qualify mandatory data_b_name o
4.58 + (rep_compat ? Binding.qualify false rep_compat_prefix);
4.59 +
4.60 val (As, B) =
4.61 no_defs_lthy
4.62 |> mk_TFrees' (map Type.sort_of_atyp As0)
4.63 @@ -144,13 +153,12 @@
4.64 fun can_omit_disc_binding k m =
4.65 n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k));
4.66
4.67 - val std_disc_binding =
4.68 - Binding.qualify false data_b_name o Binding.name o prefix isN o base_name_of_ctr;
4.69 + val std_disc_binding = qualify false o Binding.name o prefix isN o base_name_of_ctr;
4.70
4.71 val disc_bindings =
4.72 raw_disc_bindings'
4.73 |> map4 (fn k => fn m => fn ctr => fn disc =>
4.74 - Option.map (Binding.qualify false data_b_name)
4.75 + Option.map (qualify false)
4.76 (if Binding.eq_name (disc, Binding.empty) then
4.77 if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr)
4.78 else if Binding.eq_name (disc, std_binding) then
4.79 @@ -166,7 +174,7 @@
4.80 val sel_bindingss =
4.81 pad_list [] n raw_sel_bindingss
4.82 |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
4.83 - Binding.qualify false data_b_name
4.84 + qualify false
4.85 (if Binding.eq_name (sel, Binding.empty) orelse Binding.eq_name (sel, std_binding) then
4.86 std_sel_binding m l ctr
4.87 else
4.88 @@ -618,10 +626,11 @@
4.89 (selsN, all_sel_thms, simp_attrs),
4.90 (splitN, [split_thm], []),
4.91 (split_asmN, [split_asm_thm], []),
4.92 + (splitsN, [split_thm, split_asm_thm], []),
4.93 (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
4.94 |> filter_out (null o #2)
4.95 |> map (fn (thmN, thms, attrs) =>
4.96 - ((Binding.qualify true data_b_name (Binding.name thmN), attrs), [(thms, [])]));
4.97 + ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
4.98
4.99 val notes' =
4.100 [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
4.101 @@ -652,7 +661,9 @@
4.102 val parse_bound_termss = parse_bracket_list parse_bound_terms;
4.103
4.104 val parse_wrap_options =
4.105 - Scan.optional (@{keyword "("} |-- (@{keyword "no_dests"} >> K true) --| @{keyword ")"}) false;
4.106 + Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_dests"} >> K (true, false)) ||
4.107 + (@{keyword "rep_compat"} >> K (false, true))) --| @{keyword ")"}
4.108 + >> (pairself (exists I) o split_list)) (false, false);
4.109
4.110 val _ =
4.111 Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"