merged

--- 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_model.ML	Mon May 27 16:52:39 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon May 27 16:53:21 2013 +0200
@@ -943,8 +943,8 @@
                                    T T' (rep_of name)
       in
         Pretty.block (Pretty.breaks
-            [Syntax.pretty_term (set_show_all_types ctxt) t1,
-             Pretty.str oper, Syntax.pretty_term ctxt t2])
+            [Syntax.pretty_term ctxt t1, Pretty.str oper,
+             Syntax.pretty_term ctxt t2])
       end
     fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
       Pretty.block (Pretty.breaks

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

--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon May 27 16:52:39 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon May 27 16:53:21 2013 +0200
@@ -72,7 +72,6 @@
   val eta_expand : typ list -> term -> int -> term
   val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
   val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
-  val set_show_all_types : Proof.context -> Proof.context
   val indent_size : int
   val pstrs : string -> Pretty.T list
   val unyxml : string -> string
@@ -288,11 +287,6 @@
 fun DETERM_TIMEOUT delay tac st =
   Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
 
-fun set_show_all_types ctxt =
-  Config.put show_all_types
-    (Config.get ctxt show_types orelse Config.get ctxt show_sorts
-      orelse Config.get ctxt show_all_types) ctxt
-
 val indent_size = 2
 
 val pstrs = Pretty.breaks o map Pretty.str o space_explode " "