--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon May 27 16:52:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon May 27 16:53:21 2013 +0200
@@ -45,14 +45,13 @@
(typ list * typ list) list list list
val define_fold_rec: (term list list * typ list list * term list list list)
* (term list list * typ list list * term list list list) -> (string -> binding) -> typ list ->
- typ list -> typ list -> term -> term -> Proof.context ->
- (term * term * thm * thm) * Proof.context
+ typ list -> term -> term -> Proof.context -> (term * term * thm * thm) * Proof.context
val define_unfold_corec: term list * term list list
* ((term list list * term list list list list * term list list list list)
* (typ list * typ list list list * typ list list))
* ((term list list * term list list list list * term list list list list)
* (typ list * typ list list list * typ list list)) ->
- (string -> binding) -> 'a list -> typ list -> typ list -> term -> term -> Proof.context ->
+ (string -> binding) -> typ list -> typ list -> term -> term -> Proof.context ->
(term * term * thm * thm) * Proof.context
val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm ->
thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->
@@ -220,31 +219,30 @@
val mk_ctor = mk_ctor_or_dtor range_type;
val mk_dtor = mk_ctor_or_dtor domain_type;
-fun mk_co_iter lfp Ts Us t =
+fun mk_co_iter thy lfp fpT Us t =
let
val (bindings, body) = strip_type (fastype_of t);
val (f_Us, prebody) = split_last bindings;
- val Type (_, Ts0) = if lfp then prebody else body;
+ val fpT0 = if lfp then prebody else body;
val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us);
+ val rho = tvar_subst thy (fpT0 :: Us0) (fpT :: Us);
in
- Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
+ Term.subst_TVars rho t
+ end;
+
+fun mk_co_iters thy lfp fpTs Cs ts0 =
+ let
+ val nn = length fpTs;
+ val (fpTs0, Cs0) =
+ map ((not lfp ? swap) o dest_funT o snd o strip_typeN nn o fastype_of) ts0
+ |> split_list;
+ val rho = tvar_subst thy (fpTs0 @ Cs0) (fpTs @ Cs);
+ in
+ map (Term.subst_TVars rho) ts0
end;
val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
-fun mk_fp_iters ctxt lfp fpTs Cs fp_iters0 =
- let
- val thy = Proof_Context.theory_of ctxt;
- val nn = length fpTs;
- val (fpTs0, Cs0) =
- map ((not lfp ? swap) o dest_funT o snd o strip_typeN nn o fastype_of) fp_iters0
- |> split_list;
- val rho = tvar_subst thy (fpTs0 @ Cs0) (fpTs @ Cs);
- val subst = Term.subst_TVars rho;
- in
- map subst fp_iters0 |> (fn ts => (ts, mk_fp_iter_fun_types (hd ts)))
- end;
-
fun unzip_recT fpTs T =
let
fun project_recT proj =
@@ -351,8 +349,12 @@
fun mk_un_fold_co_rec_prelims lfp fpTs Cs ns mss fp_folds0 fp_recs0 lthy =
let
- val (fp_folds, fp_fold_fun_Ts) = mk_fp_iters lthy lfp fpTs Cs fp_folds0;
- val (fp_recs, fp_rec_fun_Ts) = mk_fp_iters lthy lfp fpTs Cs fp_recs0;
+ val thy = Proof_Context.theory_of lthy;
+
+ val (fp_fold_fun_Ts, fp_folds) = mk_co_iters thy lfp fpTs Cs fp_folds0
+ |> `(mk_fp_iter_fun_types o hd);
+ val (fp_rec_fun_Ts, fp_recs) = mk_co_iters thy lfp fpTs Cs fp_recs0
+ |> `(mk_fp_iter_fun_types o hd);
val ((fold_rec_args_types, unfold_corec_args_types), lthy') =
if lfp then
@@ -480,11 +482,13 @@
Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss)
end;
-fun define_fold_rec (fold_only, rec_only) mk_binding fpTs As Cs ctor_fold ctor_rec lthy0 =
+fun define_fold_rec (fold_only, rec_only) mk_binding fpTs Cs ctor_fold ctor_rec lthy0 =
let
+ val thy = Proof_Context.theory_of lthy0;
+
val nn = length fpTs;
- val fpT_to_C = snd (strip_typeN nn (fastype_of ctor_fold));
+ val fpT_to_C as Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of ctor_fold));
fun generate_iter (suf, ctor_iter, (fss, f_Tss, xsss)) =
let
@@ -508,17 +512,19 @@
val [fold_def, rec_def] = map (Morphism.thm phi) defs;
- val [foldx, recx] = map (mk_co_iter true As Cs o Morphism.term phi) csts;
+ val [foldx, recx] = map (mk_co_iter thy true fpT Cs o Morphism.term phi) csts;
in
((foldx, recx, fold_def, rec_def), lthy')
end;
-fun define_unfold_corec (cs, cpss, unfold_only, corec_only) mk_binding fpTs As Cs dtor_unfold
+fun define_unfold_corec (cs, cpss, unfold_only, corec_only) mk_binding fpTs Cs dtor_unfold
dtor_corec lthy0 =
let
+ val thy = Proof_Context.theory_of lthy0;
+
val nn = length fpTs;
- val C_to_fpT = snd (strip_typeN nn (fastype_of dtor_unfold));
+ val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of dtor_unfold));
fun generate_coiter (suf, dtor_coiter, ((pfss, cqssss, cfssss),
(f_sum_prod_Ts, f_Tsss, pf_Tss))) =
@@ -543,12 +549,12 @@
val [unfold_def, corec_def] = map (Morphism.thm phi) defs;
- val [unfold, corec] = map (mk_co_iter false As Cs o Morphism.term phi) csts;
+ val [unfold, corec] = map (mk_co_iter thy false fpT Cs o Morphism.term phi) csts;
in
((unfold, corec, unfold_def, corec_def), lthy')
- end;
+ end ;
-fun derive_induct_fold_rec_thms_for_types pre_bnfs ctor_folds0 ctor_recs0 ctor_induct ctor_fold_thms
+fun derive_induct_fold_rec_thms_for_types pre_bnfs ctor_folds ctor_recs ctor_induct ctor_fold_thms
ctor_rec_thms nesting_bnfs nested_bnfs fpTs Cs ctrss ctr_defss folds recs fold_defs rec_defs
lthy =
let
@@ -567,8 +573,8 @@
val fp_b_names = map base_name_of_typ fpTs;
- val (_, ctor_fold_fun_Ts) = mk_fp_iters lthy true fpTs Cs ctor_folds0;
- val (_, ctor_rec_fun_Ts) = mk_fp_iters lthy true fpTs Cs ctor_recs0;
+ val ctor_fold_fun_Ts = mk_fp_iter_fun_types (hd ctor_folds);
+ val ctor_rec_fun_Ts = mk_fp_iter_fun_types (hd ctor_recs);
val (((gss, _, _), (hss, _, _)), names_lthy0) =
mk_fold_rec_args_types fpTs Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy;
@@ -706,7 +712,7 @@
(fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
end;
-fun derive_coinduct_unfold_corec_thms_for_types pre_bnfs dtor_unfolds0 dtor_corecs0 dtor_coinduct
+fun derive_coinduct_unfold_corec_thms_for_types pre_bnfs dtor_unfolds dtor_corecs dtor_coinduct
dtor_strong_induct dtor_ctors dtor_unfold_thms dtor_corec_thms nesting_bnfs nested_bnfs fpTs Cs
As kss mss ns ctr_defss ctr_sugars unfolds corecs unfold_defs corec_defs lthy =
let
@@ -722,8 +728,8 @@
val fp_b_names = map base_name_of_typ fpTs;
- val (_, dtor_unfold_fun_Ts) = mk_fp_iters lthy false fpTs Cs dtor_unfolds0;
- val (_, dtor_corec_fun_Ts) = mk_fp_iters lthy false fpTs Cs dtor_corecs0;
+ val dtor_unfold_fun_Ts = mk_fp_iter_fun_types (hd dtor_unfolds);
+ val dtor_corec_fun_Ts = mk_fp_iter_fun_types (hd dtor_corecs);
val ctrss = map (map (mk_ctr As) o #ctrs) ctr_sugars;
val discss = map (map (mk_disc_or_sel As) o #discs) ctr_sugars;
@@ -1321,8 +1327,7 @@
(wrap_ctrs
#> derive_maps_sets_rels
##>> (if lfp then define_fold_rec (the fold_rec_args_types)
- else define_unfold_corec (the unfold_corec_args_types))
- mk_binding fpTs As Cs fp_fold fp_rec
+ else define_unfold_corec (the unfold_corec_args_types)) mk_binding fpTs Cs fp_fold fp_rec
#> massage_res, lthy')
end;
@@ -1343,7 +1348,7 @@
let
val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs),
(rec_thmss, rec_attrs)) =
- derive_induct_fold_rec_thms_for_types pre_bnfs fp_folds0 fp_recs0 fp_induct fp_fold_thms
+ derive_induct_fold_rec_thms_for_types pre_bnfs fp_folds fp_recs fp_induct fp_fold_thms
fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs ctrss ctr_defss folds recs fold_defs
rec_defs lthy;
@@ -1380,7 +1385,7 @@
(disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
(disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
(sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
- derive_coinduct_unfold_corec_thms_for_types pre_bnfs fp_folds0 fp_recs0 fp_induct
+ derive_coinduct_unfold_corec_thms_for_types pre_bnfs fp_folds fp_recs fp_induct
fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As
kss mss ns ctr_defss ctr_sugars unfolds corecs unfold_defs corec_defs lthy;
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon May 27 16:52:39 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon May 27 16:53:21 2013 +0200
@@ -142,10 +142,9 @@
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
fun quintuple_for_scope code_type code_term code_string
- ({hol_ctxt = {ctxt = ctxt0, stds, ...}, card_assigns, bits, bisim_depth,
+ ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
datatypes, ...} : scope) =
let
- val ctxt = set_show_all_types ctxt0
val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
@{typ bisim_iterator}]
val (iter_assigns, card_assigns) =