--- a/src/HOL/Tools/function_package/fundef.ML Tue Jun 23 12:09:14 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,226 +0,0 @@
-(* Title: HOL/Tools/function_package/fundef.ML
- Author: Alexander Krauss, TU Muenchen
-
-A package for general recursive function definitions.
-Isar commands.
-*)
-
-signature FUNDEF =
-sig
- val add_fundef : (binding * typ option * mixfix) list
- -> (Attrib.binding * term) list
- -> FundefCommon.fundef_config
- -> local_theory
- -> Proof.state
- val add_fundef_cmd : (binding * string option * mixfix) list
- -> (Attrib.binding * string) list
- -> FundefCommon.fundef_config
- -> local_theory
- -> Proof.state
-
- val termination_proof : term option -> local_theory -> Proof.state
- val termination_proof_cmd : string option -> local_theory -> Proof.state
- 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
-end
-
-
-structure Fundef : FUNDEF =
-struct
-
-open FundefLib
-open FundefCommon
-
-val simp_attribs = map (Attrib.internal o K)
- [Simplifier.simp_add,
- Code.add_default_eqn_attribute,
- Nitpick_Const_Simp_Thms.add,
- Quickcheck_RecFun_Simp_Thms.add]
-
-val psimp_attribs = map (Attrib.internal o K)
- [Simplifier.simp_add,
- Nitpick_Const_Psimp_Thms.add]
-
-fun note_theorem ((name, atts), ths) =
- LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
-
-fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
-
-fun add_simps fnames post sort extra_qualify label 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 (LocalTheory.note Thm.generatedK) spec lthy
-
- val saved_simps = flat (map snd saved_spec_simps)
- val simps_by_f = sort saved_simps
-
- fun add_for_f fname simps =
- note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
- in
- (saved_simps,
- fold2 add_for_f fnames simps_by_f lthy)
- end
-
-fun gen_add_fundef 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) = FundefCommon.get_preproc lthy config ctxt' fixes spec
-
- val defname = mk_defname fixes
-
- val ((goalstate, cont), lthy) =
- FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy
-
- fun afterqed [[proof]] lthy =
- let
- val FundefResult {fs, R, psimps, trsimps, simple_pinducts, termination,
- domintros, cases, ...} =
- cont (Thm.close_derivation proof)
-
- val fnames = map (fst o fst) fixes
- val qualify = Long_Name.qualify defname
- val addsmps = add_simps fnames post sort_cont
-
- val (((psimps', pinducts'), (_, [termination'])), lthy) =
- lthy
- |> addsmps (Binding.qualify false "partial") "psimps"
- psimp_attribs psimps
- ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
- ||>> note_theorem ((qualify "pinduct",
- [Attrib.internal (K (RuleCases.case_names cnames)),
- Attrib.internal (K (RuleCases.consumes 1)),
- Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
- ||>> note_theorem ((qualify "termination", []), [termination])
- ||> (snd o note_theorem ((qualify "cases",
- [Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
- ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
-
- val cdata = FundefCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
- pinducts=snd pinducts', termination=termination',
- fs=fs, R=R, defname=defname }
- val _ =
- if not is_external then ()
- else Specification.print_consts lthy (K false) (map fst fixes)
- in
- lthy
- |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata)
- end
- in
- lthy
- |> is_external ? LocalTheory.set_group (serial_string ())
- |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
- |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
- end
-
-val add_fundef = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
-val add_fundef_cmd = gen_add_fundef true Specification.read_spec "_::type"
-
-fun gen_termination_proof prep_term raw_term_opt lthy =
- let
- val term_opt = Option.map (prep_term lthy) raw_term_opt
- val data = the (case term_opt of
- SOME t => (import_fundef_data t lthy
- handle Option.Option =>
- error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
- | NONE => (import_last_fundef lthy handle Option.Option => error "Not a function"))
-
- val FundefCtxData { termination, R, add_simps, case_names, psimps,
- pinducts, defname, ...} = data
- 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, True_implies_equals])
- val tsimps = map remove_domain_condition psimps
- val tinduct = map remove_domain_condition pinducts
- val qualify = Long_Name.qualify defname;
- in
- lthy
- |> add_simps I "simps" simp_attribs tsimps |> snd
- |> note_theorem
- ((qualify "induct",
- [Attrib.internal (K (RuleCases.case_names case_names))]),
- tinduct) |> snd
- end
- in
- lthy
- |> ProofContext.note_thmss ""
- [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
- |> ProofContext.note_thmss ""
- [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
- |> ProofContext.note_thmss ""
- [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
- [([Goal.norm_result termination], [])])] |> snd
- |> Proof.theorem_i NONE afterqed [[(goal, [])]]
- end
-
-val termination_proof = gen_termination_proof Syntax.check_term;
-val termination_proof_cmd = gen_termination_proof Syntax.read_term;
-
-fun termination term_opt lthy =
- lthy
- |> LocalTheory.set_group (serial_string ())
- |> termination_proof term_opt;
-
-fun termination_cmd term_opt lthy =
- lthy
- |> LocalTheory.set_group (serial_string ())
- |> termination_proof_cmd term_opt;
-
-
-(* Datatype hook to declare datatype congs as "fundef_congs" *)
-
-
-fun add_case_cong n thy =
- Context.theory_map (FundefCtxTree.map_fundef_congs (Thm.add_thm
- (Datatype.get_datatype thy n |> the
- |> #case_cong
- |> safe_mk_meta_eq)))
- thy
-
-val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
-
-
-(* setup *)
-
-val setup =
- Attrib.setup @{binding fundef_cong}
- (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del)
- "declaration of congruence rule for function definitions"
- #> setup_case_cong
- #> FundefRelation.setup
- #> FundefCommon.TerminationSimps.setup
-
-val get_congs = FundefCtxTree.get_fundef_congs
-
-
-(* outer syntax *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ =
- OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
- (fundef_parser default_config
- >> (fn ((config, fixes), statements) => add_fundef_cmd fixes statements config));
-
-val _ =
- OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
- (Scan.option P.term >> termination_cmd);
-
-end;
-
-
-end