# HG changeset patch
# User blanchet
# Date 1398241407 -7200
# Node ID 2ffa440b30743f9da38074b36102c75babc5e383
# Parent  ce8297d5017aa7f6bae7b6f53b474b7f94701a0c
manual merge + added 'rel_distincts' field to record for symmetry

diff -r ce8297d5017a -r 2ffa440b3074 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 23 10:23:27 2014 +0200
@@ -29,7 +29,8 @@
      co_rec_thms: thm list,
      disc_co_recs: thm list,
      sel_co_recss: thm list list,
-     rel_injects: thm list};
+     rel_injects: thm list,
+     rel_distincts: thm list};
 
   val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
   val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
@@ -145,12 +146,14 @@
    co_rec_thms: thm list,
    disc_co_recs: thm list,
    sel_co_recss: thm list list,
-   rel_injects: thm list};
+   rel_injects: thm list,
+   rel_distincts: thm list};
 
-fun morph_fp_sugar phi ({T, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
-    nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, maps, common_co_inducts, co_inducts,
-    co_rec_thms, disc_co_recs, sel_co_recss, rel_injects} : fp_sugar) =
+fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
+    nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
+    co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) =
   {T = Morphism.typ phi T,
+   BT = Morphism.typ phi BT,
    X = Morphism.typ phi X,
    fp = fp,
    fp_res = morph_fp_result phi fp_res,
@@ -170,7 +173,8 @@
    co_rec_thms = map (Morphism.thm phi) co_rec_thms,
    disc_co_recs = map (Morphism.thm phi) disc_co_recs,
    sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss,
-   rel_injects = map (Morphism.thm phi) rel_injects};
+   rel_injects = map (Morphism.thm phi) rel_injects,
+   rel_distincts = map (Morphism.thm phi) rel_distincts};
 
 val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
 
@@ -198,35 +202,36 @@
   val eq: T * T -> bool = op = o pairself (map #T);
 );
 
-fun with_repaired_path f (fp_sugars : fp_sugar list) thy =
+fun with_repaired_path f (fp_sugars as ({T = Type (s, _), ...} : fp_sugar) :: _) thy =
   thy
-  (* FIXME: |> Sign.root_path*)
-  |> Sign.add_path (Long_Name.qualifier (mk_common_name (map (fst o dest_Type o #T) fp_sugars)))
+  |> Sign.root_path (* FIXME *)
+  |> Sign.add_path (Long_Name.qualifier s)
   |> f fp_sugars
   |> Sign.restore_naming thy;
 
 val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
 
 fun register_fp_sugars fp_sugars =
-  fold (fn fp_sugar as {T as Type (s, _), ...} =>
+  fold (fn fp_sugar as {T = Type (s, _), ...} =>
       Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
     fp_sugars
   #> Local_Theory.background_theory (FP_Sugar_Interpretation.data fp_sugars);
 
-fun register_as_fp_sugars Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs (fp_res as {Ts, ...})
-    ctrXs_Tsss ctr_defss ctr_sugars co_recs mapss common_co_inducts co_inductss co_rec_thmss
-    disc_co_recss sel_co_recsss =
+fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
+    ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss
+    co_rec_thmss disc_co_recss sel_co_recsss rel_injectss rel_distinctss =
   let
     val fp_sugars =
       map_index (fn (kk, T) =>
-        {T = T, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
+        {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
          pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, nested_bnfs = nested_bnfs,
          nesting_bnfs = nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk,
-         ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, maps = nth mapss kk,
-         common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
-         co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk,
-         sel_co_recss = nth sel_co_recsss kk}) Ts
+         ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk,
+         maps = nth mapss kk, common_co_inducts = common_co_inducts,
+         co_inducts = nth co_inductss kk, co_rec_thms = nth co_rec_thmss kk,
+         disc_co_recs = nth disc_co_recss kk, sel_co_recss = nth sel_co_recsss kk,
+         rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk}) Ts
   in
     register_fp_sugars fp_sugars
   end;
@@ -451,7 +456,6 @@
 fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val nn = length fpTs;
 
     val (xtor_co_rec_fun_Ts, xtor_co_recs) =
       mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 |> `(binder_fun_types o fastype_of o hd);
@@ -1320,7 +1324,7 @@
       injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
 
     fun derive_note_induct_recs_thms_for_types
-        ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
+        ((((mapss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)),
           (recs, rec_defs)), lthy) =
       let
         val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
@@ -1331,7 +1335,7 @@
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;
 
         val simp_thmss =
-          map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injects rel_distincts setss;
+          map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injectss rel_distinctss setss;
 
         val common_notes =
           (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
@@ -1346,13 +1350,14 @@
         lthy
         |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
         |> Local_Theory.notes (common_notes @ notes) |> snd
-        |> register_as_fp_sugars Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
-          ctrXs_Tsss ctr_defss ctr_sugars recs mapss [induct_thm] (map single induct_thms)
-          rec_thmss (replicate nn []) (replicate nn []) rel_injects
+        |> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs
+          fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm]
+          (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss
+          rel_distinctss
       end;
 
     fun derive_note_coinduct_corecs_thms_for_types
-        ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
+        ((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
           (corecs, corec_defs)), lthy) =
       let
         val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
@@ -1373,7 +1378,7 @@
         val simp_thmss =
           map6 mk_simp_thms ctr_sugars
             (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
-            mapss rel_injects rel_distincts setss;
+            mapss rel_injectss rel_distinctss setss;
 
         val common_notes =
           (if nn > 1 then
@@ -1399,10 +1404,10 @@
         |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
           [flat sel_corec_thmss, flat corec_thmss]
         |> Local_Theory.notes (common_notes @ notes) |> snd
-        |> register_as_fp_sugars Xs Greatest_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
-          ctrXs_Tsss ctr_defss ctr_sugars corecs mapss [coinduct_thm, strong_coinduct_thm]
-          (transpose [coinduct_thms, strong_coinduct_thms]) corec_thmss disc_corec_thmss
-          sel_corec_thmsss rel_injects
+        |> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos nested_bnfs
+          nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
+          [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms])
+          corec_thmss disc_corec_thmss sel_corec_thmsss rel_injectss rel_distinctss
       end;
 
     val lthy'' = lthy'
diff -r ce8297d5017a -r 2ffa440b3074 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Apr 23 10:23:27 2014 +0200
@@ -274,21 +274,22 @@
 
         val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
 
-        fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec maps
-            co_inducts co_rec_thms disc_corec_thms sel_corec_thmss rel_injects =
+        fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
+            co_rec_def maps co_inducts co_rec_thms disc_corec_thms sel_corec_thmss
+            ({rel_injects, rel_distincts, ...} : fp_sugar) =
           {T = T, BT = Term.dummyT (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res,
            fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info, nested_bnfs = nested_bnfs,
            nesting_bnfs = nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs,
-           ctr_sugar = ctr_sugar, co_rec = co_rec, maps = maps,
+           ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
            common_co_inducts = common_co_inducts, co_inducts = co_inducts,
            co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
-           sel_co_recss = sel_corec_thmss, rel_injects = rel_injects}
+           sel_co_recss = sel_corec_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
           |> morph_fp_sugar phi;
 
         val target_fp_sugars =
-          map15 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
-            co_recs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss sel_corec_thmsss
-            (map #rel_injects fp_sugars0);
+          map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
+            co_recs co_rec_defs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss
+            sel_corec_thmsss fp_sugars0;
 
         val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
       in
diff -r ce8297d5017a -r 2ffa440b3074 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Wed Apr 23 10:23:27 2014 +0200
@@ -39,6 +39,10 @@
       'o -> 'p) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
     'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
+ val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+      'o -> 'p -> 'q) ->
+    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
+    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list
   val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
   val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
@@ -215,6 +219,13 @@
       map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s
   | map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
+fun map16 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
+  | map16 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) (x16::x16s) =
+    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 ::
+      map16 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s
+  | map16 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
 fun fold_map4 _ [] [] [] [] acc = ([], acc)
   | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
     let
@@ -471,7 +482,7 @@
   end;
 
 fun mk_inj t =
-  let val T as Type (@{type_name fun}, [domT, ranT]) = fastype_of t in
+  let val T as Type (@{type_name fun}, [domT, _]) = fastype_of t in
     Const (@{const_name inj_on}, T --> HOLogic.mk_setT domT --> HOLogic.boolT) $ t
       $ HOLogic.mk_UNIV domT
   end;
diff -r ce8297d5017a -r 2ffa440b3074 src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Wed Apr 23 10:23:27 2014 +0200
@@ -64,8 +64,10 @@
 
 fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
 
-fun fp_sugar_only_type_ctr f fp_sugar = 
-  if is_Type (T_of_bnf (bnf_of_fp_sugar fp_sugar)) then f fp_sugar else I
+fun fp_sugar_only_type_ctr f fp_sugars =
+  (case filter (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugars of
+    [] => I
+  | fp_sugars' => f fp_sugars')
 
 (* relation constraints - bi_total & co. *)
 
@@ -344,7 +346,7 @@
     snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
   end
 
-val _ = Context.>> (Context.map_theory (fp_sugar_interpretation
-  (fp_sugar_only_type_ctr (fn fp_sugar => map_local_theory (transfer_fp_sugar_interpretation fp_sugar)))))
+val _ = Context.>> (Context.map_theory (fp_sugar_interpretation (fp_sugar_only_type_ctr
+  (fn fp_sugars => map_local_theory (fold transfer_fp_sugar_interpretation fp_sugars)))))
 
 end