# HG changeset patch
# User blanchet
# Date 1458747433 -3600
# Node ID add334b71e16016880572e6b4cf30bcb9b4b0a7f
# Parent  9d706e37ddab492223d799cba3cc0101f0fb038c
sorted out type issue with sort constraints

diff -r 9d706e37ddab -r add334b71e16 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue Mar 22 13:44:50 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Wed Mar 23 16:37:13 2016 +0100
@@ -555,8 +555,9 @@
 
     val T_name = Local_Theory.full_name lthy T_b;
 
-    val tyargs = map2 (fn alive => pair (if alive then SOME Binding.empty else NONE)
-      o rpair @{sort type}) (fp_alives @ [true]) (Es @ [Y]);
+    val tyargs = map2 (fn alive => fn T =>
+        (if alive then SOME Binding.empty else NONE, (T, Type.sort_of_atyp T)))
+      (fp_alives @ [true]) (Es @ [Y]);
     val ctr_specs = [(((Binding.empty, ctr_b), [(sel_b, rhsT)]), NoSyn)];
     val spec = (((((tyargs, T_b), NoSyn), ctr_specs),
       (Binding.empty, Binding.empty, Binding.empty)), []);
@@ -590,8 +591,9 @@
     val As = Es @ [Y];
     val ssig_sig_T = Type (sig_T_name, Es @ [Type (T_name, As)]);
 
-    val tyargs = map2 (fn alive => pair (if alive then SOME Binding.empty else NONE)
-      o rpair @{sort type}) (fp_alives @ [true]) As;
+    val tyargs = map2 (fn alive => fn T =>
+        (if alive then SOME Binding.empty else NONE, (T, Type.sort_of_atyp T)))
+      (fp_alives @ [true]) (Es @ [Y]);
     val ctr_specs =
       [(((Binding.empty, Oper_b), [(Binding.empty, ssig_sig_T)]), NoSyn),
        (((Binding.empty, VLeaf_b), [(Binding.empty, Y)]), NoSyn),
@@ -2066,12 +2068,12 @@
   let
     val fp_sugar as {T = Type (_, fpT_args0), pre_bnf, fp_bnf, fp_res, ...} =
       checked_fp_sugar_of lthy fpT_name;
-    val num_fp_tyargs = length fpT_args0;
-    val fp_alives = liveness_of_fp_bnf num_fp_tyargs fp_bnf;
+    val fpT_Ss = map Type.sort_of_atyp fpT_args0;
+    val fp_alives = liveness_of_fp_bnf (length fpT_args0) fp_bnf;
 
     val (((Es, Fs0), [Y, Z]), names_lthy) = lthy
-      |> mk_TFrees num_fp_tyargs
-      ||>> mk_TFrees num_fp_tyargs
+      |> mk_TFrees' fpT_Ss
+      ||>> mk_TFrees' fpT_Ss
       ||>> mk_TFrees 2;
     val Fs = @{map 3} (fn alive => fn E => fn F => if alive then F else E) fp_alives Es Fs0;
 
@@ -2602,13 +2604,13 @@
      : corec_info)
     lthy =
   let
-    val {pre_bnf = live_pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} =
+    val {T = Type (_, fpT_args0), pre_bnf = live_pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} =
       checked_fp_sugar_of lthy fpT_name;
-    val num_fp_tyargs = length res_Ds;
-    val live_fp_alives = liveness_of_fp_bnf num_fp_tyargs live_fp_bnf;
+    val fpT_Ss = map Type.sort_of_atyp fpT_args0;
+    val live_fp_alives = liveness_of_fp_bnf (length fpT_args0) live_fp_bnf;
 
     val ((Ds, [Y, Z]), names_lthy) = lthy
-      |> mk_TFrees num_fp_tyargs
+      |> mk_TFrees' fpT_Ss
       ||>> mk_TFrees 2;
 
     (* FIXME *)
@@ -3077,12 +3079,12 @@
     val _ = not (null arg_Ts) orelse
       error "Function with no argument cannot be registered as friend";
 
-    val {pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} = checked_fp_sugar_of lthy fpT_name;
-    val num_fp_tyargs = length res_Ds;
+    val {T = Type (fpT_name, fpT_args0), pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} =
+      checked_fp_sugar_of lthy fpT_name;
+    val num_fp_tyargs = length fpT_args0;
+    val fpT_Ss = map Type.sort_of_atyp fpT_args0;
     val live_fp_alives = liveness_of_fp_bnf num_fp_tyargs live_fp_bnf;
 
-    val fpT_name = fst (dest_Type res_T);
-
     val (old_info as {friend_names = old_friend_names, sig_fp_sugars = old_sig_fp_sugar :: _,
            buffer = old_buffer, ...}, lthy) =
       corec_info_of res_T lthy;
@@ -3099,7 +3101,7 @@
 
     val lthy = lthy |> Variable.declare_typ friend_T;
     val ((Ds, [Y, Z]), _) = lthy
-      |> mk_TFrees num_fp_tyargs
+      |> mk_TFrees' fpT_Ss
       ||>> mk_TFrees 2;
 
     (* FIXME *)
diff -r 9d706e37ddab -r add334b71e16 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 22 13:44:50 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Mar 23 16:37:13 2016 +0100
@@ -225,12 +225,12 @@
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val SOME ({fp_res_index, fp_res = {dtors, dtor_ctors, ...},
+    val SOME ({fp_res_index, fp_res = {dtors = dtors0, dtor_ctors, ...},
         absT_info = {rep = rep0, abs_inverse, ...},
         fp_ctr_sugar = {ctr_defs, ctr_sugar = {casex, exhaust, case_thms, ...}, ...}, ...}) =
       fp_sugar_of ctxt fpT_name;
 
-    val (f_Ts, Type (_, [fpT, _])) = strip_fun_type (fastype_of casex);
+    val (f_Ts, Type (_, [fpT as Type (_, As), _])) = strip_fun_type (fastype_of casex);
     val x_Tss = map binder_types f_Ts;
 
     val (((u, fs), xss), _) = ctxt
@@ -238,7 +238,9 @@
       ||>> mk_Frees "f" f_Ts
       ||>> mk_Freess "x" x_Tss;
 
-    val dtor = nth dtors fp_res_index;
+    val dtor0 = nth dtors0 fp_res_index;
+    val dtor = mk_dtor As dtor0;
+
     val u' = dtor $ u;
 
     val absT = fastype_of u';
@@ -264,7 +266,7 @@
     val fpT0 as Type (_, As0) = domain_type (body_fun_type (fastype_of casex));
 
     val (As, _) = ctxt
-      |> mk_TFrees (length As0);
+      |> mk_TFrees' (map Type.sort_of_atyp As0);
     val fpT = Type (fpT_name, As);
 
     val (var_name, ()) = singleton (Variable.variant_frees ctxt []) ("x", ());
@@ -666,7 +668,7 @@
     Symtab.make_list (names ~~ thms)
   end;
 
-fun derive_coinduct ctxt (fpT as Type (fpT_name, _)) dtor_coinduct =
+fun derive_coinduct ctxt (fpT as Type (fpT_name, fpT_args)) dtor_coinduct =
   let
     val thy = Proof_Context.theory_of ctxt;
 
@@ -677,14 +679,15 @@
     val SOME {X as TVar ((X_s, _), _), fp_res = {dtor_ctors, ...}, pre_bnf,
         absT_info = {abs_inverse, ...}, live_nesting_bnfs,
         fp_ctr_sugar = {ctrXs_Tss, ctr_defs,
-          ctr_sugar = ctr_sugar0 as {T = T0, ctrs = ctrs0, discs = discs0, ...}, ...}, ...} =
+          ctr_sugar = ctr_sugar0 as {T = Type (_, T0_args), ctrs = ctrs0, discs = discs0, ...},
+            ...}, ...} =
       fp_sugar_of ctxt fpT_name;
 
     val n = length ctrXs_Tss;
     val ms = map length ctrXs_Tss;
 
     val X' = TVar ((X_s, maxidx_of_typ fpT + 1), @{sort type});
-    val As_rho = tvar_subst thy [T0] [fpT];
+    val As_rho = tvar_subst thy T0_args fpT_args;
     val substXAT = Term.typ_subst_TVars As_rho o Tsubst X X';
     val substXA = Term.subst_TVars As_rho o substT X X';
     val phi = Morphism.typ_morphism "BNF" substXAT $> Morphism.term_morphism "BNF" substXA;
@@ -1970,9 +1973,7 @@
   end;
 
 fun update_coinduct_cong_intross_dynamic fpT_name lthy =
-  let
-    val all_corec_infos = corec_infos_of lthy fpT_name;
-  in
+  let val all_corec_infos = corec_infos_of lthy fpT_name in
     lthy
     |> fold_map (apfst snd oo derive_coinduct_cong_intros) all_corec_infos
     |> snd