--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_termination.ML	Tue Jul 19 09:41:33 2011 +0100
@@ -0,0 +1,112 @@
+(*  Nominal Termination
+    Author: Christian Urban
+
+    heavily based on the code of Alexander Krauss
+    (code forked on 18 July 2011)
+
+Redefinition of the termination command
+*)
+
+signature NOMINAL_FUNCTION_TERMINATION =
+sig
+  include NOMINAL_FUNCTION_DATA
+
+  val termination : term option -> local_theory -> Proof.state
+  val termination_cmd : string option -> local_theory -> Proof.state
+
+end
+
+structure Nominal_Function_Termination : NOMINAL_FUNCTION_TERMINATION =
+struct
+
+open Function_Lib
+open Function_Common
+open Nominal_Function_Common
+
+val simp_attribs = map (Attrib.internal o K)
+  [Simplifier.simp_add,
+   Code.add_default_eqn_attribute,
+   Nitpick_Simps.add]
+
+val eqvt_attrib =  Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+
+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, eqvts, ...} = 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
+          val teqvts = map remove_domain_condition eqvts
+  
+          fun qualify n = Binding.name n
+            |> Binding.qualify true defname
+        in
+          lthy
+          |> add_simps I "simps" I simp_attribs tsimps
+          ||>> Local_Theory.note ((qualify "eqvt", [eqvt_attrib]), teqvts)
+          ||>> Local_Theory.note
+             ((qualify "induct",
+               [Attrib.internal (K (Rule_Cases.case_names case_names))]),
+              tinduct)
+          |-> (fn ((simps, (_, eqvts)), (_, 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, eqvts=eqvts }
+            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_termination prep_term raw_term_opt lthy =
+  let
+    val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
+  in
+    lthy
+    |> Proof_Context.note_thmss ""
+       [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
+    |> Proof_Context.note_thmss ""
+       [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+    |> Proof_Context.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
+
+(* outer syntax *)
+
+val option_parser =
+  (Scan.optional (Parse.$$$ "(" |-- Parse.!!! 
+    (Parse.reserved "eqvt" >> K true) --| Parse.$$$ ")") false)
+
+val _ =
+  Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
+  Keyword.thy_goal
+  (option_parser -- Scan.option Parse.term >> 
+     (fn (is_eqvt, trm) => 
+        if is_eqvt then termination_cmd trm else Function.termination_cmd trm))
+
+end