src/HOL/Codatatype/Tools/bnf_wrap.ML

 *)
 
 signature BNF_WRAP =
 sig
   val no_name: binding
-  val wrap: ({prems: thm list, context: Proof.context} -> tactic) list list ->
+  val mk_half_pairss: 'a list -> ('a * 'a) list list
+  val wrap_data: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     (term list * term) * (binding list * binding list list) -> local_theory -> local_theory
 end;
 
 structure BNF_Wrap : BNF_WRAP =
 struct

   case head_of t of
     Const (s, _) => s
   | Free (s, _) => s
   | _ => error "Cannot extract name of constructor";
 
-fun prepare_wrap prep_term ((raw_ctrs, raw_caseof), (raw_disc_names, raw_sel_namess))
+fun prepare_wrap_data prep_term ((raw_ctrs, raw_caseof), (raw_disc_names, raw_sel_namess))
   no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
     (* TODO: attributes (simp, case_names, etc.) *)
     (* TODO: case syntax *)

     val caseof0 = prep_term no_defs_lthy raw_caseof;
 
     val n = length ctrs0;
     val ks = 1 upto n;
 
-    val (T_name, As0) = dest_Type (body_type (fastype_of (hd ctrs0)));
+    val _ = if n > 0 then () else error "No constructors specified";
+
+    val Type (T_name, As0) = body_type (fastype_of (hd ctrs0));
     val b = Binding.qualified_name T_name;
 
     val (As, B) =
       no_defs_lthy
       |> mk_TFrees (length As0)
       ||> the_single o fst o mk_TFrees 1;
 
     fun mk_ctr Ts ctr =
-      let val Ts0 = snd (dest_Type (body_type (fastype_of ctr))) in
+      let val Type (_, Ts0) = body_type (fastype_of ctr) in
         Term.subst_atomic_types (Ts0 ~~ Ts) ctr
       end;
 
     val T = Type (T_name, As);
     val ctrs = map (mk_ctr As) ctrs0;

           fallback_sel_name m l ctr
         else
           sel) (1 upto m) o pad_list no_name m) ctrs0 ms;
 
     fun mk_caseof Ts T =
-      let val (binders, body) = strip_type (fastype_of caseof0) in
-        Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ Ts)) caseof0
-      end;
+      let
+        val (binders, body) = strip_type (fastype_of caseof0)
+        val Type (_, Ts0) = List.last binders
+      in Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) caseof0 end;
 
     val caseofB = mk_caseof As B;
     val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
     fun mk_caseofB_term eta_fs = Term.list_comb (caseofB, eta_fs);

 
     val discs0 = map (Morphism.term phi) raw_discs;
     val selss0 = map (map (Morphism.term phi)) raw_selss;
 
     fun mk_disc_or_sel Ts t =
-      Term.subst_atomic_types (snd (dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
+      Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
 
     val discs = map (mk_disc_or_sel As) discs0;
     val selss = map (map (mk_disc_or_sel As)) selss0;
 
     fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
 
     val goal_exhaust =
       let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in
-        mk_imp_p (map2 mk_prem xctrs xss)
+        fold_rev Logic.all [p, v] (mk_imp_p (map2 mk_prem xctrs xss))
       end;
 
     val goal_injectss =
       let
         fun mk_goal _ _ [] [] = []
           | mk_goal xctr yctr xs ys =
-            [mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr),
-              Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))];
+            [fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr),
+              Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))];
       in
         map4 mk_goal xctrs yctrs xss yss
       end;
 
     val goal_half_distinctss =
-      map (map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq)) (mk_half_pairss xctrs);
-
-    val goal_cases = map2 (fn xctr => fn xf => mk_Trueprop_eq (caseofB_fs $ xctr, xf)) xctrs xfs;
-
-    val goals = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases];
+      let
+        fun mk_goal ((xs, t), (xs', t')) =
+          fold_rev Logic.all (xs @ xs')
+            (HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, t'))));
+      in
+        map (map mk_goal) (mk_half_pairss (xss ~~ xctrs))
+      end;
+
+    val goal_cases =
+      map3 (fn xs => fn xctr => fn xf =>
+        fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (caseofB_fs $ xctr, xf))) xss xctrs xfs;
+
+    val goalss = [goal_exhaust] :: goal_injectss @ goal_half_distinctss @ [goal_cases];
 
     fun after_qed thmss lthy =
       let
         val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
           (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss)));

           if has_not_other_disc_def orelse forall I no_discs then
             []
           else
             let
               fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))];
-              val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs));
+              val goal = fold_rev Logic.all [p, v] (mk_imp_p (map mk_prem discs));
             in
               [Skip_Proof.prove lthy [] [] goal (fn _ =>
                  mk_disc_exhaust_tac n exhaust_thm discI_thms)]
             end;
 

            (discsN, disc_thms),
            (disc_exclusN, disc_exclus_thms),
            (disc_exhaustN, disc_exhaust_thms),
            (distinctN, distinct_thms),
            (exhaustN, [exhaust_thm]),
-           (injectN, (flat inject_thmss)),
+           (injectN, flat inject_thmss),
            (nchotomyN, [nchotomy_thm]),
-           (selsN, (flat sel_thmss)),
+           (selsN, flat sel_thmss),
            (splitN, [split_thm]),
            (split_asmN, [split_asm_thm]),
            (weak_case_cong_thmsN, [weak_case_cong_thm])]
           |> filter_out (null o snd)
           |> map (fn (thmN, thms) =>
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
       in
         lthy |> Local_Theory.notes notes |> snd
       end;
   in
-    (goals, after_qed, lthy')
+    (goalss, after_qed, lthy')
   end;
 
-fun wrap tacss = (fn (goalss, after_qed, lthy) =>
+fun wrap_data tacss = (fn (goalss, after_qed, lthy) =>
   map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss
   |> (fn thms => after_qed thms lthy)) oo
-  prepare_wrap (singleton o Type_Infer_Context.infer_types)
+  prepare_wrap_data (K I) (* FIXME? (singleton o Type_Infer_Context.infer_types) *)
 
 val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]";
 val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]";
 
 val wrap_data_cmd = (fn (goalss, after_qed, lthy) =>
   Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo
-  prepare_wrap Syntax.read_term;
+  prepare_wrap_data Syntax.read_term;
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"
     (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term --
       Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], []))