--- 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 *)
--- 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