made sugared 'coinduct' theorem construction n2m-proof

--- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Nov 04 10:52:41 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Nov 04 10:52:41 2013 +0100
@@ -79,8 +79,8 @@
 
   val mk_map: int -> typ list -> typ list -> term -> term
   val mk_rel: int -> typ list -> typ list -> term -> term
-  val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
-  val build_rel: local_theory -> (typ * typ -> term) -> typ * typ -> term
+  val build_map: Proof.context -> (typ * typ -> term) -> typ * typ -> term
+  val build_rel: Proof.context -> (typ * typ -> term) -> typ * typ -> term
 
   val mk_witness: int list * term -> thm list -> nonemptiness_witness
   val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
@@ -501,7 +501,7 @@
     Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   end;
 
-fun build_map_or_rel mk const of_bnf dest lthy build_simple =
+fun build_map_or_rel mk const of_bnf dest ctxt build_simple =
   let
     fun build (TU as (T, U)) =
       if T = U then
@@ -511,7 +511,7 @@
           (Type (s, Ts), Type (s', Us)) =>
           if s = s' then
             let
-              val bnf = the (bnf_of lthy s);
+              val bnf = the (bnf_of ctxt s);
               val live = live_of_bnf bnf;
               val mapx = mk live Ts Us (of_bnf bnf);
               val TUs' = map dest (fst (strip_typeN live (fastype_of mapx)));

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
@@ -40,7 +40,6 @@
   val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
   val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
   val dest_map: Proof.context -> string -> term -> term * term list
-  val dest_ctr: Proof.context -> string -> term -> term * term list
 
   type lfp_sugar_thms =
     (thm list * thm * Args.src list)
@@ -348,7 +347,7 @@
 fun nesty_bnfs ctxt ctr_Tsss Us =
   map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []);
 
-fun indexify proj xs f p = f (find_index (curry op = (proj p)) xs) p;
+fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
 
 type lfp_sugar_thms =
   (thm list * thm * Args.src list)
@@ -390,7 +389,7 @@
         ns mss ctr_Tsss ctor_iter_fun_Tss;
 
     val z_Tsss' = map (map flat_rec_arg_args) z_Tssss;
-    val h_Tss = map2 (map2 (curry op --->)) z_Tsss' Css;
+    val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css;
 
     val hss = map2 (map2 retype_free) h_Tss gss;
     val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss;
@@ -412,7 +411,7 @@
     val f_sum_prod_Ts = map range_type fun_Ts;
     val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
     val f_Tsss = map2 (map2 (dest_tupleT o length)) ctr_Tsss' f_prod_Tss;
-    val f_Tssss = map3 (fn C => map2 (map2 (map (curry op --> C) oo unzip_corecT)))
+    val f_Tssss = map3 (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT)))
       Cs ctr_Tsss' f_Tsss;
     val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
   in
@@ -537,7 +536,7 @@
 
     fun generate_iter suf (f_Tss, _, fss, xssss) ctor_iter =
       let
-        val res_T = fold_rev (curry op --->) f_Tss fpT_to_C;
+        val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
         val b = mk_binding suf;
         val spec =
           mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of b, res_T)),
@@ -556,7 +555,7 @@
 
     fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter =
       let
-        val res_T = fold_rev (curry op --->) pf_Tss C_to_fpT;
+        val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
         val b = mk_binding suf;
         val spec =
           mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of b, res_T)),
@@ -605,7 +604,7 @@
         val lives = lives_of_bnf bnf;
         val sets = sets_of_bnf bnf;
         fun mk_set U =
-          (case find_index (curry op = U) lives of
+          (case find_index (curry (op =) U) lives of
             ~1 => Term.dummy
           | i => nth sets i);
       in
@@ -622,7 +621,7 @@
           end;
 
         fun mk_raw_prem_prems _ (x as Free (_, Type _)) (X as TFree _) =
-            [([], (find_index (curry op = X) Xs + 1, x))]
+            [([], (find_index (curry (op =) X) Xs + 1, x))]
           | mk_raw_prem_prems names_lthy (x as Free (s, Type (T_name, Ts0))) (Type (_, Xs_Ts0)) =
             (case AList.lookup (op =) setss_nested T_name of
               NONE => []
@@ -662,7 +661,7 @@
 
         val goal =
           Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
-            HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry op $) ps us)));
+            HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us)));
 
         val kksss = map (map (map (fst o snd) o #2)) raw_premss;
 
@@ -781,39 +780,29 @@
           map4 (fn u => fn v => fn uvr => fn uv_eq =>
             fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
 
-        fun build_rel rs' T =
-          (case find_index (curry op = T) fpTs of
-            ~1 =>
-            if exists_subtype_in fpTs T then
-              let
-                val Type (s, Ts) = T
-                val bnf = the (bnf_of lthy s);
-                val live = live_of_bnf bnf;
-                val rel = mk_rel live Ts Ts (rel_of_bnf bnf);
-                val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
-              in Term.list_comb (rel, map (build_rel rs') Ts') end
-            else
-              HOLogic.eq_const T
-          | kk => nth rs' kk);
+        fun build_the_rel rs' T Xs_T =
+          build_rel lthy (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
+          |> Term.subst_atomic_types (Xs ~~ fpTs);
 
-        fun build_rel_app rs' usel vsel = fold rapp [usel, vsel] (build_rel rs' (fastype_of usel));
+        fun build_rel_app rs' usel vsel Xs_T =
+          fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T);
 
-        fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels =
+        fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels ctrXs_Ts =
           (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @
           (if null usels then
              []
            else
              [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
-                Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app rs') usels vsels))]);
+                Library.foldr1 HOLogic.mk_conj (map3 (build_rel_app rs') usels vsels ctrXs_Ts))]);
 
-        fun mk_prem_concl rs' n udiscs uselss vdiscs vselss =
-          Library.foldr1 HOLogic.mk_conj
-            (flat (map5 (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss))
+        fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss =
+          Library.foldr1 HOLogic.mk_conj (flat (map6 (mk_prem_ctr_concls rs' n)
+            (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss))
           handle List.Empty => @{term True};
 
-        fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss =
+        fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss =
           fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
-            HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss)));
+            HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss)));
 
         val concl =
           HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -821,8 +810,8 @@
                uvrs us vs));
 
         fun mk_goal rs' =
-          Logic.list_implies (map8 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss,
-            concl);
+          Logic.list_implies (map9 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss
+            ctrXs_Tsss, concl);
 
         val goals = map mk_goal [rs, strong_rs];