# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1322414105 0
# Node ID 1afcbaf4242b9c7fceb8a051a58cd03b95dc3fe4
# Parent  da0fccee125c1a132597ee802c044f3ce1ce57d2
termination does not automatically prove equivariance for the defined function (label: no_eqvt)

diff -r da0fccee125c -r 1afcbaf4242b Nominal/nominal_termination.ML
--- a/Nominal/nominal_termination.ML	Sat Nov 26 09:53:52 2011 +0000
+++ b/Nominal/nominal_termination.ML	Sun Nov 27 17:15:05 2011 +0000
@@ -11,8 +11,8 @@
 sig
   include NOMINAL_FUNCTION_DATA
 
-  val termination : term option -> local_theory -> Proof.state
-  val termination_cmd : string option -> local_theory -> Proof.state
+  val termination : bool -> term option -> local_theory -> Proof.state
+  val termination_cmd : bool -> string option -> local_theory -> Proof.state
 
 end
 
@@ -30,7 +30,7 @@
 
 val eqvt_attrib =  Attrib.internal (K Nominal_ThmDecls.eqvt_add)
 
-fun prepare_termination_proof prep_term raw_term_opt lthy =
+fun prepare_termination_proof prep_term is_eqvt raw_term_opt lthy =
   let
     val term_opt = Option.map (prep_term lthy) raw_term_opt
     val info = the (case term_opt of
@@ -59,7 +59,7 @@
         in
           lthy
           |> add_simps I "simps" I simp_attribs tsimps
-          ||>> Local_Theory.note ((qualify "eqvt", [eqvt_attrib]), teqvts)
+          ||>> Local_Theory.note ((qualify "eqvt", if is_eqvt then [eqvt_attrib] else []), teqvts)
           ||>> Local_Theory.note
              ((qualify "induct",
                [Attrib.internal (K (Rule_Cases.case_names case_names))]),
@@ -80,9 +80,9 @@
     (goal, afterqed, termination)
   end
 
-fun gen_termination prep_term raw_term_opt lthy =
+fun gen_termination prep_term is_eqvt raw_term_opt lthy =
   let
-    val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
+    val (goal, afterqed, termination) = prepare_termination_proof prep_term is_eqvt raw_term_opt lthy
   in
     lthy
     |> Proof_Context.note_thmss ""
@@ -102,13 +102,14 @@
 
 val option_parser =
   (Scan.optional (Parse.$$$ "(" |-- Parse.!!! 
-    (Parse.reserved "eqvt" >> K true) --| Parse.$$$ ")") false)
+    ((Parse.reserved "eqvt" >> K (true, true)) ||
+     (Parse.reserved "no_eqvt" >> K (true, false))) --| Parse.$$$ ")") (false, 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))
+     (fn ((is_nominal, is_eqvt), opt_trm) => 
+        if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm))
 
 end