# HG changeset patch # User krauss # Date 1298649588 -3600 # Node ID b368a7aee46a94652e629081b5a14f9331f4166d # Parent 6611b9cef38b7de1c3fe5c3b2092a57f4664ae1a removed support for tail-recursion from function package (now implemented by partial_function) diff -r 6611b9cef38b -r b368a7aee46a NEWS --- 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 *** diff -r 6611b9cef38b -r b368a7aee46a doc-src/Functions/Thy/Functions.thy --- 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 \ nat) \ nat \ nat" +function (*<*)(domintros)(*>*)findzero :: "(nat \ nat) \ nat \ 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 \ findzero_dom (f, x)" - "findzero_dom (f, Suc x) \ 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 \ n \ 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 \ nat) \ nat \ 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 {* diff -r 6611b9cef38b -r b368a7aee46a doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 \ f_dom"}. - \end{description} *} diff -r 6611b9cef38b -r b368a7aee46a src/HOL/Tools/Function/fun.ML --- 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 diff -r 6611b9cef38b -r b368a7aee46a src/HOL/Tools/Function/function.ML --- 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)), diff -r 6611b9cef38b -r b368a7aee46a src/HOL/Tools/Function/function_common.ML --- 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.$$$ ")") []) diff -r 6611b9cef38b -r b368a7aee46a src/HOL/Tools/Function/function_core.ML --- 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) diff -r 6611b9cef38b -r b368a7aee46a src/HOL/Tools/Function/mutual.ML --- 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 =