# HG changeset patch # User Christian Urban # Date 1300304534 -3600 # Node ID 34df2cffe25922b2571bcc99d4b9ae67ddb42e86 # Parent 56b8d977d1c00041ce00454e306c0cf3a2979cb6 ported changes from function package....needs Isabelle 16 March or above diff -r 56b8d977d1c0 -r 34df2cffe259 Nominal/nominal_function.ML --- a/Nominal/nominal_function.ML Tue Mar 15 00:40:39 2011 +0100 +++ b/Nominal/nominal_function.ML Wed Mar 16 20:42:14 2011 +0100 @@ -81,11 +81,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'." @@ -96,7 +92,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) @@ -111,9 +107,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 56b8d977d1c0 -r 34df2cffe259 Nominal/nominal_function_core.ML --- a/Nominal/nominal_function_core.ML Tue Mar 15 00:40:39 2011 +0100 +++ b/Nominal/nominal_function_core.ML Wed Mar 16 20:42:14 2011 +0100 @@ -908,62 +908,10 @@ -(* 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 - - (* nominal *) fun prepare_nominal_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) @@ -1026,9 +974,6 @@ (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim G_eqvt) 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*) @@ -1054,13 +999,11 @@ 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 56b8d977d1c0 -r 34df2cffe259 Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Tue Mar 15 00:40:39 2011 +0100 +++ b/Nominal/nominal_mutual.ML Wed Mar 16 20:42:14 2011 +0100 @@ -253,7 +253,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) = @@ -270,7 +270,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 @@ -278,7 +277,7 @@ FunctionResult { fs=fs, G=G, R=R, psimps=mpsimps, simple_pinducts=minducts, cases=cases, termination=mtermination, - domintros=mdomintros, trsimps=mtrsimps} + domintros=mdomintros} end (* nominal *)