no longer declare .psimps rules as [simp].
This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.
(* Title: HOL/Tools/Function/function.ML
Author: Alexander Krauss, TU Muenchen
A package for general recursive function definitions.
Isar commands.
*)
signature FUNCTION =
sig
include FUNCTION_DATA
val add_function: (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> Function_Common.function_config ->
(Proof.context -> tactic) -> local_theory -> info * local_theory
val add_function_cmd: (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> Function_Common.function_config ->
(Proof.context -> tactic) -> local_theory -> info * local_theory
val function: (binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> Function_Common.function_config ->
local_theory -> Proof.state
val function_cmd: (binding * string option * mixfix) list ->
(Attrib.binding * string) list -> Function_Common.function_config ->
local_theory -> Proof.state
val prove_termination: term option -> tactic -> local_theory ->
info * local_theory
val prove_termination_cmd: string option -> tactic -> local_theory ->
info * local_theory
val termination : term option -> local_theory -> Proof.state
val termination_cmd : string option -> local_theory -> Proof.state
val setup : theory -> theory
val get_congs : Proof.context -> thm list
val get_info : Proof.context -> term -> info
end
structure Function : FUNCTION =
struct
open Function_Lib
open Function_Common
val simp_attribs = map (Attrib.internal o K)
[Simplifier.simp_add,
Code.add_default_eqn_attribute,
Nitpick_Simps.add]
val psimp_attribs = map (Attrib.internal o K)
[Nitpick_Psimps.add]
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
fun add_simps fnames post sort extra_qualify label mod_binding moreatts
simps lthy =
let
val spec = post simps
|> map (apfst (apsnd (fn ats => moreatts @ ats)))
|> map (apfst (apfst extra_qualify))
val (saved_spec_simps, lthy) =
fold_map Local_Theory.note spec lthy
val saved_simps = maps snd saved_spec_simps
val simps_by_f = sort saved_simps
fun add_for_f fname simps =
Local_Theory.note
((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
#> snd
in
(saved_simps, fold2 add_for_f fnames simps_by_f lthy)
end
fun prepare_function is_external prep default_constraint fixspec eqns config lthy =
let
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
val fixes = map (apfst (apfst Binding.name_of)) fixes0;
val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
val defname = mk_defname fixes
val FunctionConfig {partials, ...} = config
val ((goal_state, cont), lthy') =
Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
fun afterqed [[proof]] lthy =
let
val FunctionResult {fs, R, psimps, trsimps, simple_pinducts,
termination, domintros, cases, ...} =
cont (Thm.close_derivation proof)
val fnames = map (fst o fst) fixes
fun qualify n = Binding.name n
|> Binding.qualify true defname
val conceal_partial = if partials then I else Binding.conceal
val addsmps = add_simps fnames post sort_cont
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
|> addsmps (conceal_partial o Binding.qualify false "partial")
"psimps" conceal_partial psimp_attribs psimps
||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
||> fold_option (Spec_Rules.add Spec_Rules.Equational o pair fs) trsimps
||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
[Attrib.internal (K (Rule_Cases.case_names cnames)),
Attrib.internal (K (Rule_Cases.consumes 1)),
Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
||> (snd o Local_Theory.note ((qualify "cases",
[Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros
val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
fs=fs, R=R, defname=defname, is_partial=true }
val _ =
if not is_external then ()
else Specification.print_consts lthy (K false) (map fst fixes)
in
(info,
lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
end
in
((goal_state, afterqed), lthy')
end
fun gen_add_function is_external prep default_constraint fixspec eqns config tac lthy =
let
val ((goal_state, afterqed), lthy') =
prepare_function is_external prep default_constraint fixspec eqns config lthy
val pattern_thm =
case SINGLE (tac lthy') goal_state of
NONE => error "pattern completeness and compatibility proof failed"
| SOME st => Goal.finish lthy' st
in
lthy'
|> afterqed [[pattern_thm]]
end
val add_function =
gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
fun gen_function is_external prep default_constraint fixspec eqns config lthy =
let
val ((goal_state, afterqed), lthy') =
prepare_function is_external prep default_constraint fixspec eqns config lthy
in
lthy'
|> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
|> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
end
val function =
gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
val function_cmd = gen_function true Specification.read_spec "_::type"
fun prepare_termination_proof prep_term raw_term_opt lthy =
let
val term_opt = Option.map (prep_term lthy) raw_term_opt
val info = the (case term_opt of
SOME t => (import_function_data t lthy
handle Option.Option =>
error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
| NONE => (import_last_function lthy handle Option.Option => error "Not a function"))
val { termination, fs, R, add_simps, case_names, psimps,
pinducts, defname, ...} = info
val domT = domain_type (fastype_of R)
val goal = HOLogic.mk_Trueprop
(HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
fun afterqed [[totality]] lthy =
let
val totality = Thm.close_derivation totality
val remove_domain_condition =
full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])
val tsimps = map remove_domain_condition psimps
val tinduct = map remove_domain_condition pinducts
fun qualify n = Binding.name n
|> Binding.qualify true defname
in
lthy
|> add_simps I "simps" I simp_attribs tsimps
||>> Local_Theory.note
((qualify "induct",
[Attrib.internal (K (Rule_Cases.case_names case_names))]),
tinduct)
|-> (fn (simps, (_, inducts)) => fn lthy =>
let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
simps=SOME simps, inducts=SOME inducts, termination=termination }
in
(info',
lthy
|> Local_Theory.declaration false (add_function_data o morph_function_data info')
|> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
end)
end
in
(goal, afterqed, termination)
end
fun gen_prove_termination prep_term raw_term_opt tac lthy =
let
val (goal, afterqed, termination) =
prepare_termination_proof prep_term raw_term_opt lthy
val totality = Goal.prove lthy [] [] goal (K tac)
in
afterqed [[totality]] lthy
end
val prove_termination = gen_prove_termination Syntax.check_term
val prove_termination_cmd = gen_prove_termination Syntax.read_term
fun gen_termination prep_term raw_term_opt lthy =
let
val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
in
lthy
|> ProofContext.note_thmss ""
[((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
|> ProofContext.note_thmss ""
[((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
|> ProofContext.note_thmss ""
[((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
[([Goal.norm_result termination], [])])] |> snd
|> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
end
val termination = gen_termination Syntax.check_term
val termination_cmd = gen_termination Syntax.read_term
(* Datatype hook to declare datatype congs as "function_congs" *)
fun add_case_cong n thy =
let
val cong = #case_cong (Datatype.the_info thy n)
|> safe_mk_meta_eq
in
Context.theory_map
(Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
end
val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
(* setup *)
val setup =
Attrib.setup @{binding fundef_cong}
(Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
"declaration of congruence rule for function definitions"
#> setup_case_cong
#> Function_Relation.setup
#> Function_Common.Termination_Simps.setup
val get_congs = Function_Ctx_Tree.get_function_congs
fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
|> the_single |> snd
(* outer syntax *)
val _ =
Outer_Syntax.local_theory_to_proof "function" "define general recursive functions"
Keyword.thy_goal
(function_parser default_config
>> (fn ((config, fixes), statements) => function_cmd fixes statements config))
val _ =
Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
Keyword.thy_goal
(Scan.option Parse.term >> termination_cmd)
end