don't pollute local theory with needless names
authorblanchet
Mon Nov 02 21:58:38 2015 +0100 (2015-11-02)
changeset 61551078c9fd2e052
parent 61550 0b39a1f26604
child 61553 933eb9e6a1cc
child 61555 e27cfd2bf094
don't pollute local theory with needless names
NEWS
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
     1.1 --- a/NEWS	Mon Nov 02 21:49:49 2015 +0100
     1.2 +++ b/NEWS	Mon Nov 02 21:58:38 2015 +0100
     1.3 @@ -400,7 +400,9 @@
     1.4    - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
     1.5      structure on the raw type to an abstract type defined using typedef.
     1.6    - Always generate "case_transfer" theorem.
     1.7 -  - Allow discriminators and selectors with the same name as the type.
     1.8 +  - Allow discriminators and selectors with the same name as the type
     1.9 +    being defined.
    1.10 +  - Avoid various internal name clashes (e.g., 'datatype f = f').
    1.11  
    1.12  * Transfer:
    1.13    - new methods for interactive debugging of 'transfer' and
     2.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Mon Nov 02 21:49:49 2015 +0100
     2.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Mon Nov 02 21:58:38 2015 +0100
     2.3 @@ -14,9 +14,6 @@
     2.4  imports BNF_Composition Basic_BNFs
     2.5  begin
     2.6  
     2.7 -lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
     2.8 -  by standard simp_all
     2.9 -
    2.10  lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
    2.11    by standard simp_all
    2.12  
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Nov 02 21:49:49 2015 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Nov 02 21:58:38 2015 +0100
     3.3 @@ -105,14 +105,13 @@
     3.4    val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
     3.5    val transfer_gfp_sugar_thms: theory -> gfp_sugar_thms -> gfp_sugar_thms
     3.6  
     3.7 -  val mk_co_recs_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list ->
     3.8 -     typ list -> typ list -> int list -> int list list -> term list -> Proof.context ->
     3.9 -     (term list
    3.10 -      * (typ list list * typ list list list list * term list list * term list list list list) option
    3.11 -      * (string * term list * term list list
    3.12 -         * (((term list list * term list list * term list list list list * term list list list list)
    3.13 -             * term list list list) * typ list)) option)
    3.14 -     * Proof.context
    3.15 +  val mk_co_recs_prelims: Proof.context -> BNF_Util.fp_kind -> typ list list list -> typ list ->
    3.16 +     typ list -> typ list -> typ list -> int list -> int list list -> term list ->
    3.17 +     term list
    3.18 +     * (typ list list * typ list list list list * term list list * term list list list list) option
    3.19 +     * (string * term list * term list list
    3.20 +        * (((term list list * term list list * term list list list list * term list list list list)
    3.21 +            * term list list list) * typ list)) option
    3.22    val repair_nullary_single_ctr: typ list list -> typ list list
    3.23    val mk_corec_p_pred_types: typ list -> int list -> typ list list
    3.24    val mk_corec_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list ->
    3.25 @@ -1176,7 +1175,7 @@
    3.26    | unzip_recT _ (Type (@{type_name prod}, Ts as [_, TFree _])) = Ts
    3.27    | unzip_recT _ T = [T];
    3.28  
    3.29 -fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy =
    3.30 +fun mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts =
    3.31    let
    3.32      val Css = map2 replicate ns Cs;
    3.33      val x_Tssss =
    3.34 @@ -1188,11 +1187,11 @@
    3.35      val x_Tsss' = map (map flat_rec_arg_args) x_Tssss;
    3.36      val f_Tss = map2 (map2 (curry (op --->))) x_Tsss' Css;
    3.37  
    3.38 -    val ((fss, xssss), lthy) = lthy
    3.39 +    val ((fss, xssss), _) = ctxt
    3.40        |> mk_Freess "f" f_Tss
    3.41        ||>> mk_Freessss "x" x_Tssss;
    3.42    in
    3.43 -    ((f_Tss, x_Tssss, fss, xssss), lthy)
    3.44 +    (f_Tss, x_Tssss, fss, xssss)
    3.45    end;
    3.46  
    3.47  fun unzip_corecT (Type (@{type_name sum}, _)) T = [T]
    3.48 @@ -1222,14 +1221,14 @@
    3.49     mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss
    3.50       (binder_fun_types (fastype_of dtor_corec)));
    3.51  
    3.52 -fun mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts lthy =
    3.53 +fun mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts =
    3.54    let
    3.55      val p_Tss = mk_corec_p_pred_types Cs ns;
    3.56  
    3.57      val (q_Tssss, g_Tsss, g_Tssss, corec_types) =
    3.58        mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts;
    3.59  
    3.60 -    val (((((Free (x, _), cs), pss), qssss), gssss), lthy) = lthy
    3.61 +    val (((((Free (x, _), cs), pss), qssss), gssss), _) = ctxt
    3.62        |> yield_singleton (mk_Frees "x") dummyT
    3.63        ||>> mk_Frees "a" Cs
    3.64        ||>> mk_Freess "p" p_Tss
    3.65 @@ -1238,7 +1237,7 @@
    3.66  
    3.67      val cpss = map2 (map o rapp) cs pss;
    3.68  
    3.69 -    fun build_sum_inj mk_inj = build_map lthy [] (uncurry mk_inj o dest_sumT o snd);
    3.70 +    fun build_sum_inj mk_inj = build_map ctxt [] (uncurry mk_inj o dest_sumT o snd);
    3.71  
    3.72      fun build_dtor_corec_arg _ [] [cg] = cg
    3.73        | build_dtor_corec_arg T [cq] [cg, cg'] =
    3.74 @@ -1250,25 +1249,25 @@
    3.75      val cgssss = map2 (map o map o map o rapp) cs gssss;
    3.76      val cqgsss = @{map 3} (@{map 3} (@{map 3} build_dtor_corec_arg)) g_Tsss cqssss cgssss;
    3.77    in
    3.78 -    ((x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)), lthy)
    3.79 +    (x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types))
    3.80    end;
    3.81  
    3.82 -fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy =
    3.83 +fun mk_co_recs_prelims ctxt fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 =
    3.84    let
    3.85 -    val thy = Proof_Context.theory_of lthy;
    3.86 +    val thy = Proof_Context.theory_of ctxt;
    3.87  
    3.88      val (xtor_co_rec_fun_Ts, xtor_co_recs) =
    3.89        mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 |> `(binder_fun_types o fastype_of o hd);
    3.90  
    3.91 -    val ((recs_args_types, corecs_args_types), lthy') =
    3.92 +    val (recs_args_types, corecs_args_types) =
    3.93        if fp = Least_FP then
    3.94 -        mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
    3.95 -        |>> (rpair NONE o SOME)
    3.96 +        mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts
    3.97 +        |> (rpair NONE o SOME)
    3.98        else
    3.99 -        mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
   3.100 -        |>> (pair NONE o SOME);
   3.101 +        mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts
   3.102 +        |> (pair NONE o SOME);
   3.103    in
   3.104 -    ((xtor_co_recs, recs_args_types, corecs_args_types), lthy')
   3.105 +    (xtor_co_recs, recs_args_types, corecs_args_types)
   3.106    end;
   3.107  
   3.108  fun mk_preds_getterss_join c cps absT abs cqgss =
   3.109 @@ -2175,8 +2174,9 @@
   3.110      val kss = map (fn n => 1 upto n) ns;
   3.111      val mss = map (map length) ctr_Tsss;
   3.112  
   3.113 -    val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') =
   3.114 -      mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
   3.115 +    val (xtor_co_recs, recs_args_types, corecs_args_types) =
   3.116 +      mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0;
   3.117 +    val lthy' = lthy;
   3.118  
   3.119      fun define_ctrs_dtrs_for_type fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor
   3.120          ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Nov 02 21:49:49 2015 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Nov 02 21:58:38 2015 +0100
     4.3 @@ -255,8 +255,8 @@
     4.4          val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
     4.5          val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
     4.6  
     4.7 -        val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
     4.8 -          mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
     4.9 +        val (xtor_co_recs, recs_args_types, corecs_args_types) =
    4.10 +          mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0;
    4.11  
    4.12          fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b;
    4.13