# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID b742489618193243ff15e1fb14f95e03c26002f3
# Parent  479a779b89a69581512a92ded79de58c137bf97e
made 'ctr_sugar' more friendly to the 'datatype_realizer'
* * *
reverted changes to 'datatype_realizer.ML'

diff -r 479a779b89a6 -r b74248961819 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -20,6 +20,7 @@
      co_iterss: term list list,
      mapss: thm list list,
      co_inducts: thm list,
+     co_inductss: thm list list,
      co_iter_thmsss: thm list list list,
      disc_co_itersss: thm list list list,
      sel_co_iterssss: thm list list list list};
@@ -129,6 +130,7 @@
    co_iterss: term list list,
    mapss: thm list list,
    co_inducts: thm list,
+   co_inductss: thm list list,
    co_iter_thmsss: thm list list list,
    disc_co_itersss: thm list list list,
    sel_co_iterssss: thm list list list list};
@@ -136,8 +138,8 @@
 fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index;
 
 fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
-    ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss}
-    : fp_sugar) =
+    ctr_sugars, co_iterss, mapss, co_inducts, co_inductss, co_iter_thmsss, disc_co_itersss,
+    sel_co_iterssss} : fp_sugar) =
   {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
     nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    fp_res = morph_fp_result phi fp_res,
@@ -146,6 +148,7 @@
    co_iterss = map (map (Morphism.term phi)) co_iterss,
    mapss = map (map (Morphism.thm phi)) mapss,
    co_inducts = map (Morphism.thm phi) co_inducts,
+   co_inductss = map (map (Morphism.thm phi)) co_inductss,
    co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss,
    disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
    sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
@@ -178,14 +181,15 @@
     (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
 
 fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
-    ctr_sugars co_iterss mapss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy =
+    ctr_sugars co_iterss mapss co_inducts co_inductss co_iter_thmsss disc_co_itersss
+    sel_co_iterssss lthy =
   (0, lthy)
   |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
     register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
         nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
         ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
-        co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss,
-        sel_co_iterssss = sel_co_iterssss}
+        co_inductss = co_inductss, co_iter_thmsss = co_iter_thmsss,
+        disc_co_itersss = disc_co_itersss, sel_co_iterssss = sel_co_iterssss}
       lthy)) Ts
   |> snd;
 
@@ -664,7 +668,10 @@
             mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_maps
               pre_set_defss)
           |> singleton (Proof_Context.export names_lthy lthy)
-          |> Thm.close_derivation;
+          (* for "datatype_realizer.ML": *)
+          |> Thm.name_derivation (fst (dest_Type (hd fpTs)) ^ Long_Name.separator ^
+            (if nn > 1 then space_implode "_" (tl fp_b_names) ^ Long_Name.separator else "") ^
+            inductN);
       in
         `(conj_dests nn) thm
       end;
@@ -1218,8 +1225,8 @@
                     Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
                       mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
                         (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
+                    |> Morphism.thm phi
                     |> Thm.close_derivation
-                    |> Morphism.thm phi
                   end;
 
                 val sumEN_thm' =
@@ -1391,7 +1398,8 @@
         lthy
         |> Local_Theory.notes (common_notes @ notes) |> snd
         |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
-          iterss mapss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] []
+          iterss mapss [induct_thm] (transpose [induct_thms]) (transpose [fold_thmss, rec_thmss])
+          [] []
       end;
 
     fun derive_note_coinduct_coiters_thms_for_types
@@ -1449,6 +1457,7 @@
         |> Local_Theory.notes (common_notes @ notes) |> snd
         |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
           ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
+          (transpose [coinduct_thms, strong_coinduct_thms])
           (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
           (transpose [sel_unfold_thmsss, sel_corec_thmsss])
       end;
diff -r 479a779b89a6 -r b74248961819 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -212,14 +212,14 @@
               (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
           |>> split_list;
 
-        val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
-              sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
+        val ((co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
+              disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
           if fp = Least_FP then
             derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
               xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
               co_iterss co_iter_defss lthy
-            |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) =>
-              ([induct], fold_thmss, rec_thmss, [], [], [], []))
+            |> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) =>
+              ([induct], [inducts], fold_thmss, rec_thmss, [], [], [], []))
             ||> (fn info => (SOME info, NONE))
           else
             derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
@@ -229,8 +229,8 @@
             |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
                     (disc_unfold_thmss, disc_corec_thmss, _), _,
                     (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
-              (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
-               disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
+              (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss, corec_thmss,
+               disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
             ||> (fn info => (NONE, SOME info));
 
         val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
@@ -239,6 +239,7 @@
           {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
            nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
            ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
+           co_inductss = transpose co_inductss,
            co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
            disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
            sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
diff -r 479a779b89a6 -r b74248961819 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -99,9 +99,9 @@
       else
         ((fp_sugars0, (NONE, NONE)), lthy);
 
-    val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ =
-      fp_sugars;
-    val inducts = conj_dests nn induct;
+    val {ctr_sugars, co_inducts = [induct], co_inductss = inductss, co_iterss,
+      co_iter_thmsss = iter_thmsss, ...} :: _ = fp_sugars;
+    val inducts = map the_single inductss;
 
     val mk_dtyp = dtyp_of_typ Ts;
 
diff -r 479a779b89a6 -r b74248961819 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -359,8 +359,10 @@
 
     val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
-    val ((((((((xss, xss'), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) = no_defs_lthy |>
-      mk_Freess' "x" ctr_Tss
+    val (((((((([exh_y], (xss, xss')), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) =
+      no_defs_lthy
+      |> mk_Frees "y" [fcT] (* for compatibility with "datatype_realizer.ML" *)
+      ||>> mk_Freess' "x" ctr_Tss
       ||>> mk_Freess "y" ctr_Tss
       ||>> mk_Frees "f" case_Ts
       ||>> mk_Frees "g" case_Ts
@@ -529,8 +531,8 @@
     fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
 
     val exhaust_goal =
-      let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (u, xctr)]) in
-        fold_rev Logic.all [p, u] (mk_imp_p (map2 mk_prem xctrs xss))
+      let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (exh_y, xctr)]) in
+        fold_rev Logic.all [p, exh_y] (mk_imp_p (map2 mk_prem xctrs xss))
       end;
 
     val inject_goalss =
@@ -556,7 +558,10 @@
 
     fun after_qed thmss lthy =
       let
-        val ([exhaust_thm], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
+        val ([exhaust_thm0], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
+        (* for "datatype_realizer.ML": *)
+        val exhaust_thm =
+          Thm.name_derivation (fcT_name ^ Long_Name.separator ^ exhaustN) exhaust_thm0;
 
         val inject_thms = flat inject_thmss;
 
@@ -611,7 +616,8 @@
           in
             (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
              Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
-            |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))
+            |> pairself (singleton (Proof_Context.export names_lthy lthy) #>
+              Thm.close_derivation)
           end;
 
         val split_lhs = q $ ufcase;
@@ -632,14 +638,14 @@
         fun prove_split selss goal =
           Goal.prove_sorry lthy [] [] goal (fn _ =>
             mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
-          |> Thm.close_derivation
-          |> singleton (Proof_Context.export names_lthy lthy);
+          |> singleton (Proof_Context.export names_lthy lthy)
+          |> Thm.close_derivation;
 
         fun prove_split_asm asm_goal split_thm =
           Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} =>
             mk_split_asm_tac ctxt split_thm)
-          |> Thm.close_derivation
-          |> singleton (Proof_Context.export names_lthy lthy);
+          |> singleton (Proof_Context.export names_lthy lthy)
+          |> Thm.close_derivation;
 
         val (split_thm, split_asm_thm) =
           let
@@ -693,8 +699,8 @@
                   val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs);
                 in
                   Goal.prove_sorry lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
+                  |> singleton (Proof_Context.export names_lthy lthy)
                   |> Thm.close_derivation
-                  |> singleton (Proof_Context.export names_lthy lthy)
                 end;
 
               fun mk_alternate_disc_def k =
@@ -706,8 +712,8 @@
                   Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
                     mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
                       (nth distinct_thms (2 - k)) uexhaust_thm)
+                  |> singleton (Proof_Context.export names_lthy lthy)
                   |> Thm.close_derivation
-                  |> singleton (Proof_Context.export names_lthy lthy)
                 end;
 
               val has_alternate_disc_def =
@@ -843,8 +849,8 @@
                     mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
                       (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
                       disc_exclude_thmsss')
+                  |> singleton (Proof_Context.export names_lthy lthy)
                   |> Thm.close_derivation
-                  |> singleton (Proof_Context.export names_lthy lthy)
                 end;
 
               val (sel_split_thm, sel_split_asm_thm) =
@@ -865,8 +871,8 @@
                 in
                   Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
                     mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
+                  |> singleton (Proof_Context.export names_lthy lthy)
                   |> Thm.close_derivation
-                  |> singleton (Proof_Context.export names_lthy lthy)
                 end;
             in
               (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,