removed support for tail-recursion from function package (now implemented by partial_function)

--- a/NEWS	Fri Feb 25 16:57:44 2011 +0100
+++ b/NEWS	Fri Feb 25 16:59:48 2011 +0100
@@ -27,6 +27,9 @@
   - sledgehammer available_provers ~> sledgehammer supported_provers
     INCOMPATIBILITY.
 
+* Function package: discontinued option "tailrec".
+INCOMPATIBILITY. Use partial_function instead.
+
 
 *** Document preparation ***
 

--- a/doc-src/Functions/Thy/Functions.thy	Fri Feb 25 16:57:44 2011 +0100
+++ b/doc-src/Functions/Thy/Functions.thy	Fri Feb 25 16:59:48 2011 +0100
@@ -702,7 +702,7 @@
   for a zero of a given function f. 
 *}
 
-function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+function (*<*)(domintros)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
 where
   "findzero f n = (if f n = 0 then n else findzero f (Suc n))"
 by pat_completeness auto
@@ -959,79 +959,6 @@
   for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}.
 *}
 
-(*lemma findzero_nicer_domintros:
-  "f x = 0 \<Longrightarrow> findzero_dom (f, x)"
-  "findzero_dom (f, Suc x) \<Longrightarrow> findzero_dom (f, x)"
-by (rule accpI, erule findzero_rel.cases, auto)+
-*)
-  
-subsection {* A Useful Special Case: Tail recursion *}
-
-text {*
-  The domain predicate is our trick that allows us to model partiality
-  in a world of total functions. The downside of this is that we have
-  to carry it around all the time. The termination proof above allowed
-  us to replace the abstract @{term "findzero_dom (f, n)"} by the more
-  concrete @{term "(x \<ge> n \<and> f x = (0::nat))"}, but the condition is still
-  there and can only be discharged for special cases.
-  In particular, the domain predicate guards the unfolding of our
-  function, since it is there as a condition in the @{text psimp}
-  rules. 
-
-  Now there is an important special case: We can actually get rid
-  of the condition in the simplification rules, \emph{if the function
-  is tail-recursive}. The reason is that for all tail-recursive
-  equations there is a total function satisfying them, even if they
-  are non-terminating. 
-
-%  A function is tail recursive, if each call to the function is either
-%  equal
-%
-%  So the outer form of the 
-%
-%if it can be written in the following
-%  form:
-%  {term[display] "f x = (if COND x then BASE x else f (LOOP x))"}
-
-
-  The function package internally does the right construction and can
-  derive the unconditional simp rules, if we ask it to do so. Luckily,
-  our @{const "findzero"} function is tail-recursive, so we can just go
-  back and add another option to the \cmd{function} command:
-
-\vspace{1ex}
-\noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
-\cmd{where}\isanewline%
-\ \ \ldots\\%
-
-  
-  \noindent Now, we actually get unconditional simplification rules, even
-  though the function is partial:
-*}
-
-thm findzero.simps
-
-text {*
-  @{thm[display] findzero.simps}
-
-  \noindent Of course these would make the simplifier loop, so we better remove
-  them from the simpset:
-*}
-
-declare findzero.simps[simp del]
-
-text {* 
-  Getting rid of the domain conditions in the simplification rules is
-  not only useful because it simplifies proofs. It is also required in
-  order to use Isabelle's code generator to generate ML code
-  from a function definition.
-  Since the code generator only works with equations, it cannot be
-  used with @{text "psimp"} rules. Thus, in order to generate code for
-  partial functions, they must be defined as a tail recursion.
-  Luckily, many functions have a relatively natural tail recursive
-  definition.
-*}
-
 section {* Nested recursion *}
 
 text {*

--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Feb 25 16:57:44 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Feb 25 16:59:48 2011 +0100
@@ -444,7 +444,7 @@
     ;
     equations: (thmdecl? prop + '|')
     ;
-    functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
+    functionopts: '(' (('sequential' | 'domintros') + ',') ')'
     ;
     'termination' ( term )?
   \end{rail}
@@ -515,14 +515,6 @@
   introduction rules for the domain predicate. While mostly not
   needed, they can be helpful in some proofs about partial functions.
 
-  \item @{text tailrec} generates the unconstrained recursive
-  equations even without a termination proof, provided that the
-  function is tail-recursive. This currently only works
-
-  \item @{text "default d"} allows to specify a default value for a
-  (partial) function, which will ensure that @{text "f x = d x"}
-  whenever @{text "x \<notin> f_dom"}.
-
   \end{description}
 *}
 

--- a/src/HOL/Tools/Function/fun.ML	Fri Feb 25 16:57:44 2011 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Fri Feb 25 16:59:48 2011 +0100
@@ -137,7 +137,7 @@
 
 
 val fun_config = FunctionConfig { sequential=true, default=NONE,
-  domintros=false, partials=false, tailrec=false }
+  domintros=false, partials=false }
 
 fun gen_add_fun add fixes statements config lthy =
   let

--- a/src/HOL/Tools/Function/function.ML	Fri Feb 25 16:57:44 2011 +0100
+++ b/src/HOL/Tools/Function/function.ML	Fri Feb 25 16:59:48 2011 +0100
@@ -85,11 +85,7 @@
     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 FunctionConfig {partials, default, ...} = config
     val _ =
       if is_some default then Output.legacy_feature
         "'function (default)'. Use 'partial_function'."
@@ -100,7 +96,7 @@
 
     fun afterqed [[proof]] lthy =
       let
-        val FunctionResult {fs, R, psimps, trsimps, simple_pinducts,
+        val FunctionResult {fs, R, psimps, simple_pinducts,
           termination, domintros, cases, ...} =
           cont (Thm.close_derivation proof)
 
@@ -115,9 +111,6 @@
           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)),

--- a/src/HOL/Tools/Function/function_common.ML	Fri Feb 25 16:57:44 2011 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Feb 25 16:59:48 2011 +0100
@@ -87,10 +87,7 @@
  {fs: term list,
   G: term,
   R: term,
-
   psimps : thm list,
-  trsimps : thm list option,
-
   simple_pinducts : thm list,
   cases : thm,
   termination : thm,
@@ -187,29 +184,25 @@
   | Default of string
   | DomIntros
   | No_Partials
-  | Tailrec
 
 datatype function_config = FunctionConfig of
  {sequential: bool,
   default: string option,
   domintros: bool,
-  partials: bool,
-  tailrec: bool}
+  partials: bool}
 
-fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
-    FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec}
-  | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
-    FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, tailrec=tailrec}
-  | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
-    FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials, tailrec=tailrec}
-  | apply_opt Tailrec (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
-    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=partials, tailrec=true}
-  | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
-    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false, tailrec=true}
+fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials}) =
+    FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials}
+  | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials}) =
+    FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials}
+  | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials}) =
+    FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials}
+  | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials}) =
+    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false}
 
 val default_config =
   FunctionConfig { sequential=false, default=NONE,
-    domintros=false, partials=true, tailrec=false }
+    domintros=false, partials=true}
 
 
 (* Analyzing function equations *)
@@ -344,8 +337,7 @@
     ((Parse.reserved "sequential" >> K Sequential)
      || ((Parse.reserved "default" |-- Parse.term) >> Default)
      || (Parse.reserved "domintros" >> K DomIntros)
-     || (Parse.reserved "no_partials" >> K No_Partials)
-     || (Parse.reserved "tailrec" >> K Tailrec))
+     || (Parse.reserved "no_partials" >> K No_Partials))
 
   fun config_parser default =
     (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])

--- a/src/HOL/Tools/Function/function_core.ML	Fri Feb 25 16:57:44 2011 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Feb 25 16:59:48 2011 +0100
@@ -817,61 +817,9 @@
 
 
 
-(* Tail recursion (probably very fragile)
- *
- * FIXME:
- * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
- * - Must we really replace the fvar by f here?
- * - Splitting is not configured automatically: Problems with case?
- *)
-fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
-  let
-    val Globals {domT, ranT, fvar, ...} = globals
-
-    val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
-
-    val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
-      Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
-        (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
-        (fn {prems=[a], ...} =>
-          ((rtac (G_induct OF [a]))
-          THEN_ALL_NEW rtac accI
-          THEN_ALL_NEW etac R_cases
-          THEN_ALL_NEW asm_full_simp_tac (simpset_of octxt)) 1)
-
-    val default_thm =
-      forall_intr_vars graph_implies_dom COMP (f_def COMP fundef_default_value)
-
-    fun mk_trsimp clause psimp =
-      let
-        val ClauseInfo {qglr = (oqs, _, _, _), cdata =
-          ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
-        val thy = ProofContext.theory_of ctxt
-        val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
-
-        val trsimp = Logic.list_implies(gs,
-          HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
-        val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
-        fun simp_default_tac ss =
-          asm_full_simp_tac (ss addsimps [default_thm, Let_def])
-      in
-        Goal.prove ctxt [] [] trsimp (fn _ =>
-          rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
-          THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
-          THEN (simp_default_tac (simpset_of ctxt) 1)
-          THEN TRY ((etac not_acc_down 1)
-            THEN ((etac R_cases)
-              THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1))
-        |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
-      end
-  in
-    map2 mk_trsimp clauses psimps
-  end
-
-
 fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
   let
-    val FunctionConfig {domintros, tailrec, default=default_opt, ...} = config
+    val FunctionConfig {domintros, default=default_opt, ...} = config
 
     val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)
     val fvar = Free (fname, fT)
@@ -932,9 +880,6 @@
       (prove_stuff lthy globals G f R xclauses complete compat
          compat_store G_elim) f_defthm
 
-    val mk_trsimps =
-      mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
-
     fun mk_partial_rules provedgoal =
       let
         val newthy = theory_of_thm provedgoal (*FIXME*)
@@ -959,13 +904,10 @@
           if domintros then SOME (PROFILE "Proving domain introduction rules"
              (map (mk_domain_intro lthy globals R R_elim)) xclauses)
            else NONE
-        val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
-
       in
         FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
           psimps=psimps, simple_pinducts=[simple_pinduct],
-          termination=total_intro, trsimps=trsimps,
-          domintros=dom_intros}
+          termination=total_intro, domintros=dom_intros}
       end
   in
     ((f, goalstate, mk_partial_rules), lthy)

--- a/src/HOL/Tools/Function/mutual.ML	Fri Feb 25 16:57:44 2011 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Feb 25 16:59:48 2011 +0100
@@ -249,7 +249,7 @@
 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
   let
     val result = inner_cont proof
-    val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
+    val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
       termination, domintros, ...} = result
 
     val (all_f_defs, fs) =
@@ -266,7 +266,6 @@
 
     val rew_ss = HOL_basic_ss addsimps all_f_defs
     val mpsimps = map2 mk_mpsimp fqgars psimps
-    val mtrsimps = Option.map (map2 mk_mpsimp fqgars) trsimps
     val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
     val mtermination = full_simplify rew_ss termination
     val mdomintros = Option.map (map (full_simplify rew_ss)) domintros
@@ -274,7 +273,7 @@
     FunctionResult { fs=fs, G=G, R=R,
       psimps=mpsimps, simple_pinducts=minducts,
       cases=cases, termination=mtermination,
-      domintros=mdomintros, trsimps=mtrsimps}
+      domintros=mdomintros}
   end
 
 fun prepare_function_mutual config defname fixes eqss lthy =