less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
authorwenzelm
Wed Aug 17 16:30:38 2011 +0200 (2011-08-17)
changeset 4423947ecd30e018d
parent 44238 36120feb70ed
child 44240 4b1a63678839
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function.ML
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Wed Aug 17 16:01:27 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Wed Aug 17 16:30:38 2011 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4      local_theory -> Proof.context
     1.5    val add_fun_cmd : (binding * string option * mixfix) list ->
     1.6      (Attrib.binding * string) list -> Function_Common.function_config ->
     1.7 -    local_theory -> Proof.context
     1.8 +    bool -> local_theory -> Proof.context
     1.9  
    1.10    val setup : theory -> theory
    1.11  end
    1.12 @@ -150,7 +150,7 @@
    1.13  val fun_config = FunctionConfig { sequential=true, default=NONE,
    1.14    domintros=false, partials=false }
    1.15  
    1.16 -fun gen_add_fun add fixes statements config lthy =
    1.17 +fun gen_add_fun add lthy =
    1.18    let
    1.19      fun pat_completeness_auto ctxt =
    1.20        Pat_Completeness.pat_completeness_tac ctxt 1
    1.21 @@ -160,18 +160,18 @@
    1.22          (Function_Common.get_termination_prover lthy lthy) lthy
    1.23    in
    1.24      lthy
    1.25 -    |> add fixes statements config pat_completeness_auto |> snd
    1.26 +    |> add pat_completeness_auto |> snd
    1.27      |> Local_Theory.restore
    1.28      |> prove_termination |> snd
    1.29    end
    1.30  
    1.31 -val add_fun = gen_add_fun Function.add_function
    1.32 -val add_fun_cmd = gen_add_fun Function.add_function_cmd
    1.33 +fun add_fun a b c = gen_add_fun (Function.add_function a b c)
    1.34 +fun add_fun_cmd a b c int = gen_add_fun (fn tac => Function.add_function_cmd a b c tac int)
    1.35  
    1.36  
    1.37  
    1.38  val _ =
    1.39 -  Outer_Syntax.local_theory "fun" "define general recursive functions (short version)"
    1.40 +  Outer_Syntax.local_theory' "fun" "define general recursive functions (short version)"
    1.41    Keyword.thy_decl
    1.42    (function_parser fun_config
    1.43       >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
     2.1 --- a/src/HOL/Tools/Function/function.ML	Wed Aug 17 16:01:27 2011 +0200
     2.2 +++ b/src/HOL/Tools/Function/function.ML	Wed Aug 17 16:30:38 2011 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4  
     2.5    val add_function_cmd: (binding * string option * mixfix) list ->
     2.6      (Attrib.binding * string) list -> Function_Common.function_config ->
     2.7 -    (Proof.context -> tactic) -> local_theory -> info * local_theory
     2.8 +    (Proof.context -> tactic) -> bool -> local_theory -> info * local_theory
     2.9  
    2.10    val function: (binding * typ option * mixfix) list ->
    2.11      (Attrib.binding * term) list -> Function_Common.function_config ->
    2.12 @@ -22,7 +22,7 @@
    2.13  
    2.14    val function_cmd: (binding * string option * mixfix) list ->
    2.15      (Attrib.binding * string) list -> Function_Common.function_config ->
    2.16 -    local_theory -> Proof.state
    2.17 +    bool -> local_theory -> Proof.state
    2.18  
    2.19    val prove_termination: term option -> tactic -> local_theory -> 
    2.20      info * local_theory
    2.21 @@ -76,7 +76,7 @@
    2.22      (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
    2.23    end
    2.24  
    2.25 -fun prepare_function is_external prep default_constraint fixspec eqns config lthy =
    2.26 +fun prepare_function do_print prep default_constraint fixspec eqns config lthy =
    2.27    let
    2.28      val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
    2.29      val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
    2.30 @@ -125,19 +125,19 @@
    2.31            pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
    2.32            fs=fs, R=R, defname=defname, is_partial=true }
    2.33  
    2.34 -        val _ = Proof_Display.print_consts is_external lthy (K false) (map fst fixes)
    2.35 +        val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
    2.36        in
    2.37 -        (info, 
    2.38 +        (info,
    2.39           lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
    2.40        end
    2.41    in
    2.42      ((goal_state, afterqed), lthy')
    2.43    end
    2.44  
    2.45 -fun gen_add_function is_external prep default_constraint fixspec eqns config tac lthy =
    2.46 +fun gen_add_function do_print prep default_constraint fixspec eqns config tac lthy =
    2.47    let
    2.48      val ((goal_state, afterqed), lthy') =
    2.49 -      prepare_function is_external prep default_constraint fixspec eqns config lthy
    2.50 +      prepare_function do_print prep default_constraint fixspec eqns config lthy
    2.51      val pattern_thm =
    2.52        case SINGLE (tac lthy') goal_state of
    2.53          NONE => error "pattern completeness and compatibility proof failed"
    2.54 @@ -149,12 +149,12 @@
    2.55  
    2.56  val add_function =
    2.57    gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
    2.58 -val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
    2.59 +fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec "_::type" a b c d
    2.60  
    2.61 -fun gen_function is_external prep default_constraint fixspec eqns config lthy =
    2.62 +fun gen_function do_print prep default_constraint fixspec eqns config lthy =
    2.63    let
    2.64      val ((goal_state, afterqed), lthy') =
    2.65 -      prepare_function is_external prep default_constraint fixspec eqns config lthy
    2.66 +      prepare_function do_print prep default_constraint fixspec eqns config lthy
    2.67    in
    2.68      lthy'
    2.69      |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
    2.70 @@ -163,7 +163,7 @@
    2.71  
    2.72  val function =
    2.73    gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
    2.74 -val function_cmd = gen_function true Specification.read_spec "_::type"
    2.75 +fun function_cmd a b c int = gen_function int Specification.read_spec "_::type" a b c
    2.76  
    2.77  fun prepare_termination_proof prep_term raw_term_opt lthy =
    2.78    let
    2.79 @@ -277,7 +277,7 @@
    2.80  (* outer syntax *)
    2.81  
    2.82  val _ =
    2.83 -  Outer_Syntax.local_theory_to_proof "function" "define general recursive functions"
    2.84 +  Outer_Syntax.local_theory_to_proof' "function" "define general recursive functions"
    2.85    Keyword.thy_goal
    2.86    (function_parser default_config
    2.87       >> (fn ((config, fixes), statements) => function_cmd fixes statements config))