--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_function.ML Mon Jan 17 14:37:18 2011 +0100
@@ -0,0 +1,211 @@
+(* Nominal Mutual Functions
+ Author: Christian Urban
+
+ heavily based on the code of Alexander Krauss
+ (code forked on 14 January 2011)
+
+Main entry points to the nominal function package.
+*)
+
+signature NOMINAL_FUNCTION =
+sig
+ include FUNCTION_DATA
+
+ val add_nominal_function: (binding * typ option * mixfix) list ->
+ (Attrib.binding * term) list -> Function_Common.function_config ->
+ (Proof.context -> tactic) -> local_theory -> info * local_theory
+
+ val add_nominal_function_cmd: (binding * string option * mixfix) list ->
+ (Attrib.binding * string) list -> Function_Common.function_config ->
+ (Proof.context -> tactic) -> local_theory -> info * local_theory
+
+ val nominal_function: (binding * typ option * mixfix) list ->
+ (Attrib.binding * term) list -> Function_Common.function_config ->
+ local_theory -> Proof.state
+
+ val nominal_function_cmd: (binding * string option * mixfix) list ->
+ (Attrib.binding * string) list -> Function_Common.function_config ->
+ local_theory -> Proof.state
+
+ val setup : theory -> theory
+ val get_congs : Proof.context -> thm list
+
+ val get_info : Proof.context -> term -> info
+end
+
+
+structure Nominal_Function : NOMINAL_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
+
+(* nominal *)
+fun prepare_nominal_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, tailrec, default, ...} = config
+ val _ =
+ if tailrec then Output.legacy_feature
+ "'function (tailrec)' command. Use 'partial_function (tailrec)'."
+ else ()
+ val _ =
+ if is_some default then Output.legacy_feature
+ "'function (default)'. Use 'partial_function'."
+ else ()
+
+ val ((goal_state, cont), lthy') =
+ Nominal_Function_Mutual.prepare_nominal_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
+ ||> (case trsimps of NONE => I | SOME thms =>
+ addsmps I "simps" I simp_attribs thms #> snd
+ #> Spec_Rules.add Spec_Rules.Equational (fs, thms))
+ ||>> 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]))
+ ||> (case domintros of NONE => I | SOME thms =>
+ Local_Theory.note ((qualify "domintros", []), thms) #> snd)
+
+ 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_nominal_function is_external prep default_constraint fixspec eqns config tac lthy =
+ let
+ val ((goal_state, afterqed), lthy') =
+ prepare_nominal_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_nominal_function =
+ gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+val add_nominal_function_cmd = gen_add_nominal_function true Specification.read_spec "_::type"
+
+fun gen_nominal_function is_external prep default_constraint fixspec eqns config lthy =
+ let
+ val ((goal_state, afterqed), lthy') =
+ prepare_nominal_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 nominal_function =
+ gen_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+val nominal_function_cmd = gen_nominal_function true Specification.read_spec "_::type"
+
+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 *)
+
+(* nominal *)
+val _ =
+ Outer_Syntax.local_theory_to_proof "nominal_primrec" "define general recursive nominal functions"
+ Keyword.thy_goal
+ (function_parser default_config
+ >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
+
+
+end