compatibility option to use "rep_datatype"

--- a/etc/isar-keywords.el	Fri Sep 28 09:12:50 2012 +0200
+++ b/etc/isar-keywords.el	Fri Sep 28 09:12:50 2012 +0200
@@ -342,6 +342,7 @@
     "overloaded"
     "permissive"
     "pervasive"
+    "rep_compat"
     "shows"
     "structure"
     "unchecked"

--- a/src/HOL/BNF/BNF_Wrap.thy	Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/BNF_Wrap.thy	Fri Sep 28 09:12:50 2012 +0200
@@ -11,7 +11,8 @@
 imports BNF_Util
 keywords
   "wrap_data" :: thy_goal and
-  "no_dests"
+  "no_dests" and
+  "rep_compat"
 begin
 
 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"

--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Fri Sep 28 09:12:50 2012 +0200
@@ -10,7 +10,7 @@
   val datatypes: bool ->
     (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
       BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
-    bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
+    (bool * bool) * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
       (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
     local_theory -> local_theory
   val parse_datatype_cmd: bool ->
@@ -144,8 +144,8 @@
 fun defaults_of ((_, ds), _) = ds;
 fun ctr_mixfix_of (_, mx) = mx;
 
-fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp (no_dests, specs)
-    no_defs_lthy0 =
+fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp
+    (wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
     (* TODO: integration with function package ("size") *)
@@ -153,6 +153,9 @@
     val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
       else ();
 
+    fun qualify mandatory fp_b_name =
+      Binding.qualify mandatory fp_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
+
     val nn = length specs;
     val fp_bs = map type_binding_of specs;
     val fp_b_names = map Binding.name_of fp_bs;
@@ -198,7 +201,7 @@
 
     val disc_bindingss = map (map disc_of) ctr_specss;
     val ctr_bindingss =
-      map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
+      map2 (fn fp_b_name => map (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;
 
@@ -424,7 +427,7 @@
           map3 (fn k => fn xs => fn tuple_x => fold_rev Term.lambda xs (ctor $
             mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs;
 
-        val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b;
+        val case_binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ caseN) fp_b);
 
         val case_rhs =
           fold_rev Term.lambda (fs @ [u])
@@ -490,7 +493,7 @@
 
             val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
           in
-            wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss,
+            wrap_datatype tacss (((wrap_opts, ctrs0), casex0), (disc_bindings, (sel_bindingss,
               sel_defaultss))) lthy
           end;
 
@@ -566,7 +569,7 @@
                (setsN, flat set_thmss, code_simp_attrs)]
               |> filter_out (null o #2)
               |> map (fn (thmN, thms, attrs) =>
-                ((Binding.qualify true fp_b_name (Binding.name thmN), attrs), [(thms, [])]));
+                ((qualify true fp_b_name (Binding.name thmN), attrs), [(thms, [])]));
           in
             (wrap_res, lthy |> Local_Theory.notes notes |> snd)
           end;
@@ -578,7 +581,7 @@
             fun generate_rec_like (suf, fp_rec_like, (fss, f_Tss, xssss)) =
               let
                 val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
-                val binding = Binding.suffix_name ("_" ^ suf) fp_b;
+                val binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b);
                 val spec =
                   mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
                     Term.list_comb (fp_rec_like,
@@ -618,7 +621,7 @@
                 pf_Tss))) =
               let
                 val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
-                val binding = Binding.suffix_name ("_" ^ suf) fp_b;
+                val binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b);
                 val spec =
                   mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),
                     Term.list_comb (fp_rec_like,
@@ -820,18 +823,18 @@
         val common_notes =
           (if nn > 1 then [(inductN, [induct_thm], [induct_case_names_attr])] else [])
           |> map (fn (thmN, thms, attrs) =>
-            ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
+            ((qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
 
         val notes =
-          [(inductN, map single induct_thms,
+          [(foldN, fold_thmss, K code_simp_attrs),
+           (inductN, map single induct_thms,
             fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
-           (foldN, fold_thmss, K code_simp_attrs),
            (recN, rec_thmss, K code_simp_attrs),
            (simpsN, simp_thmss, K [])]
           |> maps (fn (thmN, thmss, attrs) =>
-            map3 (fn b => fn Type (T_name, _) => fn thms =>
-              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name),
-                [(thms, [])])) fp_bs fpTs thmss);
+            map3 (fn fp_b_name => fn Type (T_name, _) => fn thms =>
+              ((qualify true fp_b_name (Binding.name thmN), attrs T_name),
+               [(thms, [])])) fp_b_names fpTs thmss);
       in
         lthy |> Local_Theory.notes (common_notes @ notes) |> snd
       end;
@@ -1081,7 +1084,7 @@
            else
              [])
           |> map (fn (thmN, thms, attrs) =>
-            ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
+            ((qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
 
         val notes =
           [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
@@ -1096,9 +1099,9 @@
            (strong_coinductN, map single strong_coinduct_thms, []), (* FIXME: attribs *)
            (unfoldN, unfold_thmss, [])]
           |> maps (fn (thmN, thmss, attrs) =>
-            map_filter (fn (_, []) => NONE | (b, thms) =>
-              SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
-                [(thms, [])])) (fp_bs ~~ thmss));
+            map_filter (fn (_, []) => NONE | (fp_b_name, thms) =>
+              SOME ((qualify true fp_b_name (Binding.name thmN), attrs),
+                [(thms, [])])) (fp_b_names ~~ thmss));
       in
         lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
       end;

--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Fri Sep 28 09:12:50 2012 +0200
@@ -7,6 +7,8 @@
 
 signature BNF_WRAP =
 sig
+  val rep_compat_prefix: string
+
   val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
   val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
 
@@ -16,11 +18,11 @@
   val name_of_ctr: term -> string
 
   val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
-    ((bool * term list) * term) *
+    (((bool * bool) * term list) * term) *
       (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
     (term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
      thm list list) * local_theory
-  val parse_wrap_options: bool parser
+  val parse_wrap_options: (bool * bool) parser
   val parse_bound_term: (binding * string) parser
 end;
 
@@ -30,6 +32,8 @@
 open BNF_Util
 open BNF_Wrap_Tactics
 
+val rep_compat_prefix = "new";
+
 val isN = "is_";
 val unN = "un_";
 fun mk_unN 1 1 suf = unN ^ suf
@@ -49,6 +53,7 @@
 val nchotomyN = "nchotomy";
 val selsN = "sels";
 val splitN = "split";
+val splitsN = "splits";
 val split_asmN = "split_asm";
 val weak_case_cong_thmsN = "weak_case_cong";
 
@@ -103,7 +108,7 @@
 
 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
 
-fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case),
+fun prepare_wrap_datatype prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case),
     (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
@@ -123,6 +128,10 @@
     val data_b = Binding.qualified_name dataT_name;
     val data_b_name = Binding.name_of data_b;
 
+    fun qualify mandatory =
+      Binding.qualify mandatory data_b_name o
+      (rep_compat ? Binding.qualify false rep_compat_prefix);
+
     val (As, B) =
       no_defs_lthy
       |> mk_TFrees' (map Type.sort_of_atyp As0)
@@ -144,13 +153,12 @@
     fun can_omit_disc_binding k m =
       n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k));
 
-    val std_disc_binding =
-      Binding.qualify false data_b_name o Binding.name o prefix isN o base_name_of_ctr;
+    val std_disc_binding = qualify false 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 data_b_name)
+        Option.map (qualify false)
           (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
@@ -166,7 +174,7 @@
     val sel_bindingss =
       pad_list [] n raw_sel_bindingss
       |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
-        Binding.qualify false data_b_name
+        qualify false
           (if Binding.eq_name (sel, Binding.empty) orelse Binding.eq_name (sel, std_binding) then
             std_sel_binding m l ctr
           else
@@ -618,10 +626,11 @@
            (selsN, all_sel_thms, simp_attrs),
            (splitN, [split_thm], []),
            (split_asmN, [split_asm_thm], []),
+           (splitsN, [split_thm, split_asm_thm], []),
            (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
           |> filter_out (null o #2)
           |> map (fn (thmN, thms, attrs) =>
-            ((Binding.qualify true data_b_name (Binding.name thmN), attrs), [(thms, [])]));
+            ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
 
         val notes' =
           [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
@@ -652,7 +661,9 @@
 val parse_bound_termss = parse_bracket_list parse_bound_terms;
 
 val parse_wrap_options =
-  Scan.optional (@{keyword "("} |-- (@{keyword "no_dests"} >> K true) --| @{keyword ")"}) false;
+  Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_dests"} >> K (true, false)) ||
+      (@{keyword "rep_compat"} >> K (false, true))) --| @{keyword ")"}
+    >> (pairself (exists I) o split_list)) (false, false);
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"