# HG changeset patch # User wenzelm # Date 1164892645 -3600 # Node ID cb13024d0e364750d976f3378adbc01ec1e227bf # Parent 6588b947d631b086f79cfed865ecd2f5766b29a7 Goal.norm/close_result; diff -r 6588b947d631 -r cb13024d0e36 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Thu Nov 30 14:17:22 2006 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Nov 30 14:17:25 2006 +0100 @@ -74,8 +74,8 @@ val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data val qualify = NameSpace.qualified defname - - val (((psimps', pinducts'), (_, [termination'])), lthy) = + + val (((psimps', pinducts'), (_, [termination'])), lthy) = lthy |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec) ||>> PROFILE "adding pinduct" (note_theorem ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts)) @@ -86,7 +86,7 @@ val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps', pinducts=snd pinducts', termination=termination', f=f, R=R } - + in lthy (* FIXME proper handling of morphism *) |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *) @@ -135,7 +135,7 @@ let val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data - val totality = PROFILE "closing" Drule.close_derivation totality + val totality = PROFILE "closing" Goal.close_result totality val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) @@ -145,7 +145,7 @@ (* FIXME: How to generate code from (possibly) local contexts*) val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)] - + val qualify = NameSpace.qualified defname; in lthy @@ -164,8 +164,9 @@ val goal = FundefTermination.mk_total_termination_goal f R in lthy - |> ProofContext.note_thmss_i "" [(("termination", - [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd + |> ProofContext.note_thmss_i "" + [(("termination", [ContextRules.intro_query NONE]), + [([Goal.norm_result termination], [])])] |> snd |> set_termination_rule termination |> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]] end @@ -184,23 +185,23 @@ (* Datatype hook to declare datatype congs as "fundef_congs" *) -fun add_case_cong n thy = - Context.theory_map (map_fundef_congs (Drule.add_rule +fun add_case_cong n thy = + Context.theory_map (map_fundef_congs (Drule.add_rule (DatatypePackage.get_datatype thy n |> the |> #case_cong - |> safe_mk_meta_eq))) + |> safe_mk_meta_eq))) thy val case_cong_hook = fold add_case_cong -val setup_case_cong_hook = +val setup_case_cong_hook = DatatypeHooks.add case_cong_hook #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy) (* setup *) -val setup = - FundefData.init +val setup = + FundefData.init #> FundefCongs.init #> TerminationRule.init #> Attrib.add_attributes diff -r 6588b947d631 -r cb13024d0e36 src/HOL/Tools/function_package/fundef_prep.ML --- a/src/HOL/Tools/function_package/fundef_prep.ML Thu Nov 30 14:17:22 2006 +0100 +++ b/src/HOL/Tools/function_package/fundef_prep.ML Thu Nov 30 14:17:25 2006 +0100 @@ -237,7 +237,7 @@ |> fold_rev (implies_intr o cprop_of) h_assums |> fold_rev (implies_intr o cprop_of) ags |> fold_rev forall_intr cqs - |> Drule.close_derivation + |> Goal.close_result in replace_lemma end @@ -367,7 +367,7 @@ |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it) val goal = complete COMP (graph_is_function COMP conjunctionI) - |> Drule.close_derivation + |> Goal.close_result val goalI = Goal.protect goal |> fold_rev (implies_intr o cprop_of) compat diff -r 6588b947d631 -r cb13024d0e36 src/HOL/Tools/function_package/fundef_proof.ML --- a/src/HOL/Tools/function_package/fundef_proof.ML Thu Nov 30 14:17:22 2006 +0100 +++ b/src/HOL/Tools/function_package/fundef_proof.ML Thu Nov 30 14:17:25 2006 +0100 @@ -299,7 +299,7 @@ let val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data - val provedgoal = PROFILE "Closing Derivation" Drule.close_derivation provedgoal + val provedgoal = PROFILE "Closing result" Goal.close_result provedgoal val graph_is_function = PROFILE "Getting function theorem" (fn x => (x COMP conjunctionD1) |> forall_elim_vars 0) provedgoal diff -r 6588b947d631 -r cb13024d0e36 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Nov 30 14:17:22 2006 +0100 +++ b/src/HOL/Tools/res_axioms.ML Thu Nov 30 14:17:25 2006 +0100 @@ -485,7 +485,7 @@ (case skolem thy (name, Thm.transfer thy th) of NONE => ([th],thy) | SOME (thy',cls) => - let val cls = map Drule.local_standard cls + let val cls = map Goal.close_result cls in if null cls then warning ("skolem_cache: empty clause set for " ^ name) else (); @@ -506,7 +506,7 @@ "" => skolem_thm th (*no name, so can't cache*) | s => case Symtab.lookup (!clause_cache) s of NONE => - let val cls = map Drule.local_standard (skolem_thm th) + let val cls = map Goal.close_result (skolem_thm th) in Output.debug "inserted into cache"; change clause_cache (Symtab.update (s, (th, cls))); cls end diff -r 6588b947d631 -r cb13024d0e36 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Nov 30 14:17:22 2006 +0100 +++ b/src/Pure/Isar/locale.ML Thu Nov 30 14:17:25 2006 +0100 @@ -1809,7 +1809,8 @@ val (ctxt, (_, facts)) = activate_facts true (K I) (ProofContext.init pred_thy, axiomify predicate_axioms elemss'); val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt; - val export = singleton (ProofContext.export_standard view_ctxt thy_ctxt); + val export = Goal.close_result o Goal.norm_result o + singleton (ProofContext.export view_ctxt thy_ctxt); val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])])); val elems' = maps #2 (filter (equal "" o #1 o #1) elemss'); val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems'; diff -r 6588b947d631 -r cb13024d0e36 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Thu Nov 30 14:17:22 2006 +0100 +++ b/src/Pure/Isar/specification.ML Thu Nov 30 14:17:25 2006 +0100 @@ -273,7 +273,9 @@ prep_statement attrib (prep_stmt loc) elems raw_concl ctxt; fun after_qed' results goal_ctxt' = - let val results' = burrow (ProofContext.export_standard goal_ctxt' lthy) results in + let val results' = + burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results + in lthy |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results') |> (fn (res, lthy') =>