diff -r a9a1ed3f5023 -r 16b5a67ee279 Nominal/nominal_function.ML
--- /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