do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
authorwenzelm
Sun Sep 06 21:55:13 2015 +0200 (2015-09-06)
changeset 61121efe8b18306b7
parent 61120 65082457c117
child 61122 af67ed04da64
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
NEWS
src/HOL/Library/RBT_Impl.thy
src/HOL/Nitpick.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/partial_function.ML
     1.1 --- a/NEWS	Sun Sep 06 19:09:20 2015 +0200
     1.2 +++ b/NEWS	Sun Sep 06 21:55:13 2015 +0200
     1.3 @@ -282,6 +282,11 @@
     1.4  * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
     1.5  command. Minor INCOMPATIBILITY, use 'function' instead.
     1.6  
     1.7 +* Recursive function definitions ('fun', 'function', 'partial_function')
     1.8 +no longer expose the low-level "_def" facts of the internal
     1.9 +construction. INCOMPATIBILITY, enable option "function_defs" in the
    1.10 +context for rare situations where these facts are really needed.
    1.11 +
    1.12  * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    1.13  
    1.14  
     2.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Sep 06 19:09:20 2015 +0200
     2.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sun Sep 06 21:55:13 2015 +0200
     2.3 @@ -1757,9 +1757,9 @@
     2.4    compare.eq.refl compare.eq.simps
     2.5    compare.EQ_def compare.GT_def compare.LT_def
     2.6    equal_compare_def
     2.7 -  skip_red_def skip_red.simps skip_red.cases skip_red.induct 
     2.8 +  skip_red.simps skip_red.cases skip_red.induct 
     2.9    skip_black_def
    2.10 -  compare_height_def compare_height.simps
    2.11 +  compare_height.simps
    2.12  
    2.13  subsection \<open>union and intersection of sorted associative lists\<close>
    2.14  
     3.1 --- a/src/HOL/Nitpick.thy	Sun Sep 06 19:09:20 2015 +0200
     3.2 +++ b/src/HOL/Nitpick.thy	Sun Sep 06 21:55:13 2015 +0200
     3.3 @@ -239,8 +239,8 @@
     3.4  
     3.5  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def
     3.6    card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
     3.7 -  size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
     3.8 -  num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def uminus_frac_def
     3.9 +  size_list_simp nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    3.10 +  num_def denom_def frac_def plus_frac_def times_frac_def uminus_frac_def
    3.11    number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
    3.12    wfrec'_def
    3.13  
     4.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Sep 06 19:09:20 2015 +0200
     4.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Sep 06 21:55:13 2015 +0200
     4.3 @@ -646,11 +646,6 @@
     4.4  hide_fact (open) orelse_def
     4.5  no_notation orelse (infixr "orelse" 55)
     4.6  
     4.7 -hide_fact
     4.8 -  exhaustive_int'_def
     4.9 -  exhaustive_integer'_def
    4.10 -  exhaustive_natural'_def
    4.11 -
    4.12  hide_const valtermify_absdummy valtermify_fun_upd valterm_emptyset valtermify_insert valtermify_pair
    4.13    valtermify_Inl valtermify_Inr
    4.14    termify_fun_upd term_emptyset termify_insert termify_pair setify
     5.1 --- a/src/HOL/Tools/Function/function_core.ML	Sun Sep 06 19:09:20 2015 +0200
     5.2 +++ b/src/HOL/Tools/Function/function_core.ML	Sun Sep 06 21:55:13 2015 +0200
     5.3 @@ -7,7 +7,6 @@
     5.4  signature FUNCTION_CORE =
     5.5  sig
     5.6    val trace: bool Unsynchronized.ref
     5.7 -
     5.8    val prepare_function : Function_Common.function_config
     5.9      -> string (* defname *)
    5.10      -> ((bstring * typ) * mixfix) list (* defined symbol *)
    5.11 @@ -504,10 +503,12 @@
    5.12        Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT)
    5.13          $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
    5.14        |> Syntax.check_term lthy
    5.15 +    val def_binding =
    5.16 +      if Config.get lthy function_defs then (Binding.name fdefname, [])
    5.17 +      else Attrib.empty_binding
    5.18    in
    5.19      Local_Theory.define
    5.20 -      ((Binding.name (function_name fname), mixfix),
    5.21 -        ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy
    5.22 +      ((Binding.name (function_name fname), mixfix), (def_binding, f_def)) lthy
    5.23    end
    5.24  
    5.25  fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
     6.1 --- a/src/HOL/Tools/Function/function_lib.ML	Sun Sep 06 19:09:20 2015 +0200
     6.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Sun Sep 06 21:55:13 2015 +0200
     6.3 @@ -7,6 +7,8 @@
     6.4  
     6.5  signature FUNCTION_LIB =
     6.6  sig
     6.7 +  val function_defs: bool Config.T
     6.8 +
     6.9    val plural: string -> string -> 'a list -> string
    6.10  
    6.11    val dest_all_all: term -> term list * term
    6.12 @@ -30,6 +32,9 @@
    6.13  structure Function_Lib: FUNCTION_LIB =
    6.14  struct
    6.15  
    6.16 +val function_defs = Attrib.setup_config_bool @{binding function_defs} (K false)
    6.17 +
    6.18 +
    6.19  (* "The variable" ^ plural " is" "s are" vs *)
    6.20  fun plural sg pl [x] = sg
    6.21    | plural sg pl _ = pl
     7.1 --- a/src/HOL/Tools/Function/mutual.ML	Sun Sep 06 19:09:20 2015 +0200
     7.2 +++ b/src/HOL/Tools/Function/mutual.ML	Sun Sep 06 21:55:13 2015 +0200
     7.3 @@ -128,11 +128,13 @@
     7.4    let
     7.5      fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
     7.6        let
     7.7 +        val def_binding =
     7.8 +          if Config.get lthy function_defs then (Binding.name (Thm.def_name fname), [])
     7.9 +          else Attrib.empty_binding
    7.10          val ((f, (_, f_defthm)), lthy') =
    7.11            Local_Theory.define
    7.12              ((Binding.name fname, mixfix),
    7.13 -              ((Binding.concealed (Binding.name (Thm.def_name fname)), []),
    7.14 -              Term.subst_bound (fsum, f_def))) lthy
    7.15 +              (def_binding, Term.subst_bound (fsum, f_def))) lthy
    7.16        in
    7.17          (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
    7.18             f=SOME f, f_defthm=SOME f_defthm },
     8.1 --- a/src/HOL/Tools/Function/partial_function.ML	Sun Sep 06 19:09:20 2015 +0200
     8.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Sun Sep 06 21:55:13 2015 +0200
     8.3 @@ -258,9 +258,11 @@
     8.4      val inst_mono_thm = Thm.forall_elim (Thm.cterm_of lthy x_uc) mono_thm
     8.5  
     8.6      val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
     8.7 -    val f_def_binding = Binding.concealed (Binding.name (Thm.def_name fname));
     8.8 +    val f_def_binding =
     8.9 +      if Config.get lthy Function_Lib.function_defs then (Binding.name (Thm.def_name fname), [])
    8.10 +      else Attrib.empty_binding;
    8.11      val ((f, (_, f_def)), lthy') = Local_Theory.define
    8.12 -      ((f_binding, mixfix), ((f_def_binding, []), f_def_rhs)) lthy;
    8.13 +      ((f_binding, mixfix), (f_def_binding, f_def_rhs)) lthy;
    8.14  
    8.15      val eqn = HOLogic.mk_eq (list_comb (f, args),
    8.16          Term.betapplys (F, f :: args))