# HG changeset patch # User blanchet # Date 1446497918 -3600 # Node ID 078c9fd2e052d820425a72942771b804474996ac # Parent 0b39a1f2660489f507fd9cd1e45481d6358dd94b don't pollute local theory with needless names diff -r 0b39a1f26604 -r 078c9fd2e052 NEWS --- a/NEWS Mon Nov 02 21:49:49 2015 +0100 +++ b/NEWS Mon Nov 02 21:58:38 2015 +0100 @@ -400,7 +400,9 @@ - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF structure on the raw type to an abstract type defined using typedef. - Always generate "case_transfer" theorem. - - Allow discriminators and selectors with the same name as the type. + - Allow discriminators and selectors with the same name as the type + being defined. + - Avoid various internal name clashes (e.g., 'datatype f = f'). * Transfer: - new methods for interactive debugging of 'transfer' and diff -r 0b39a1f26604 -r 078c9fd2e052 src/HOL/BNF_Fixpoint_Base.thy --- a/src/HOL/BNF_Fixpoint_Base.thy Mon Nov 02 21:49:49 2015 +0100 +++ b/src/HOL/BNF_Fixpoint_Base.thy Mon Nov 02 21:58:38 2015 +0100 @@ -14,9 +14,6 @@ imports BNF_Composition Basic_BNFs begin -lemma False_imp_eq_True: "(False \ Q) \ Trueprop True" - by standard simp_all - lemma conj_imp_eq_imp_imp: "(P \ Q \ PROP R) \ (P \ Q \ PROP R)" by standard simp_all diff -r 0b39a1f26604 -r 078c9fd2e052 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Nov 02 21:49:49 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Nov 02 21:58:38 2015 +0100 @@ -105,14 +105,13 @@ val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms val transfer_gfp_sugar_thms: theory -> gfp_sugar_thms -> gfp_sugar_thms - val mk_co_recs_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list -> - typ list -> typ list -> int list -> int list list -> term list -> Proof.context -> - (term list - * (typ list list * typ list list list list * term list list * term list list list list) option - * (string * term list * term list list - * (((term list list * term list list * term list list list list * term list list list list) - * term list list list) * typ list)) option) - * Proof.context + val mk_co_recs_prelims: Proof.context -> BNF_Util.fp_kind -> typ list list list -> typ list -> + typ list -> typ list -> typ list -> int list -> int list list -> term list -> + term list + * (typ list list * typ list list list list * term list list * term list list list list) option + * (string * term list * term list list + * (((term list list * term list list * term list list list list * term list list list list) + * term list list list) * typ list)) option val repair_nullary_single_ctr: typ list list -> typ list list val mk_corec_p_pred_types: typ list -> int list -> typ list list val mk_corec_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list -> @@ -1176,7 +1175,7 @@ | unzip_recT _ (Type (@{type_name prod}, Ts as [_, TFree _])) = Ts | unzip_recT _ T = [T]; -fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy = +fun mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts = let val Css = map2 replicate ns Cs; val x_Tssss = @@ -1188,11 +1187,11 @@ val x_Tsss' = map (map flat_rec_arg_args) x_Tssss; val f_Tss = map2 (map2 (curry (op --->))) x_Tsss' Css; - val ((fss, xssss), lthy) = lthy + val ((fss, xssss), _) = ctxt |> mk_Freess "f" f_Tss ||>> mk_Freessss "x" x_Tssss; in - ((f_Tss, x_Tssss, fss, xssss), lthy) + (f_Tss, x_Tssss, fss, xssss) end; fun unzip_corecT (Type (@{type_name sum}, _)) T = [T] @@ -1222,14 +1221,14 @@ mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss (binder_fun_types (fastype_of dtor_corec))); -fun mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts lthy = +fun mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts = let val p_Tss = mk_corec_p_pred_types Cs ns; val (q_Tssss, g_Tsss, g_Tssss, corec_types) = mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts; - val (((((Free (x, _), cs), pss), qssss), gssss), lthy) = lthy + val (((((Free (x, _), cs), pss), qssss), gssss), _) = ctxt |> yield_singleton (mk_Frees "x") dummyT ||>> mk_Frees "a" Cs ||>> mk_Freess "p" p_Tss @@ -1238,7 +1237,7 @@ val cpss = map2 (map o rapp) cs pss; - fun build_sum_inj mk_inj = build_map lthy [] (uncurry mk_inj o dest_sumT o snd); + fun build_sum_inj mk_inj = build_map ctxt [] (uncurry mk_inj o dest_sumT o snd); fun build_dtor_corec_arg _ [] [cg] = cg | build_dtor_corec_arg T [cq] [cg, cg'] = @@ -1250,25 +1249,25 @@ val cgssss = map2 (map o map o map o rapp) cs gssss; val cqgsss = @{map 3} (@{map 3} (@{map 3} build_dtor_corec_arg)) g_Tsss cqssss cgssss; in - ((x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)), lthy) + (x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)) end; -fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy = +fun mk_co_recs_prelims ctxt fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 = let - val thy = Proof_Context.theory_of lthy; + val thy = Proof_Context.theory_of ctxt; val (xtor_co_rec_fun_Ts, xtor_co_recs) = mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 |> `(binder_fun_types o fastype_of o hd); - val ((recs_args_types, corecs_args_types), lthy') = + val (recs_args_types, corecs_args_types) = if fp = Least_FP then - mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy - |>> (rpair NONE o SOME) + mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts + |> (rpair NONE o SOME) else - mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy - |>> (pair NONE o SOME); + mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts + |> (pair NONE o SOME); in - ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') + (xtor_co_recs, recs_args_types, corecs_args_types) end; fun mk_preds_getterss_join c cps absT abs cqgss = @@ -2175,8 +2174,9 @@ val kss = map (fn n => 1 upto n) ns; val mss = map (map length) ctr_Tsss; - val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') = - mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy; + val (xtor_co_recs, recs_args_types, corecs_args_types) = + mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0; + val lthy' = lthy; fun define_ctrs_dtrs_for_type fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms diff -r 0b39a1f26604 -r 078c9fd2e052 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Nov 02 21:49:49 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Nov 02 21:58:38 2015 +0100 @@ -255,8 +255,8 @@ val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs; val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As; - val ((xtor_co_recs, recs_args_types, corecs_args_types), _) = - mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy; + val (xtor_co_recs, recs_args_types, corecs_args_types) = + mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0; fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b;