Goal.norm/close_result;
authorwenzelm
Thu Nov 30 14:17:25 2006 +0100 (2006-11-30)
changeset 21602cb13024d0e36
parent 21601 6588b947d631
child 21603 0fa36ea9aaf5
Goal.norm/close_result;
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/function_package/fundef_proof.ML
src/HOL/Tools/res_axioms.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Nov 30 14:17:22 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Nov 30 14:17:25 2006 +0100
     1.3 @@ -74,8 +74,8 @@
     1.4        val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
     1.5        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
     1.6        val qualify = NameSpace.qualified defname
     1.7 -          
     1.8 -      val (((psimps', pinducts'), (_, [termination'])), lthy) = 
     1.9 +
    1.10 +      val (((psimps', pinducts'), (_, [termination'])), lthy) =
    1.11            lthy
    1.12              |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
    1.13              ||>> PROFILE "adding pinduct" (note_theorem ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
    1.14 @@ -86,7 +86,7 @@
    1.15        val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
    1.16                                    pinducts=snd pinducts', termination=termination', f=f, R=R }
    1.17  
    1.18 -      
    1.19 +
    1.20      in
    1.21        lthy  (* FIXME proper handling of morphism *)
    1.22          |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *)
    1.23 @@ -135,7 +135,7 @@
    1.24      let
    1.25        val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data
    1.26  
    1.27 -      val totality = PROFILE "closing" Drule.close_derivation totality
    1.28 +      val totality = PROFILE "closing" Goal.close_result totality
    1.29  
    1.30        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
    1.31  
    1.32 @@ -145,7 +145,7 @@
    1.33          (* FIXME: How to generate code from (possibly) local contexts*)
    1.34        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
    1.35        val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
    1.36 -        
    1.37 +
    1.38        val qualify = NameSpace.qualified defname;
    1.39      in
    1.40        lthy
    1.41 @@ -164,8 +164,9 @@
    1.42          val goal = FundefTermination.mk_total_termination_goal f R
    1.43      in
    1.44        lthy
    1.45 -        |> ProofContext.note_thmss_i "" [(("termination",
    1.46 -                                        [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
    1.47 +        |> ProofContext.note_thmss_i ""
    1.48 +          [(("termination", [ContextRules.intro_query NONE]),
    1.49 +            [([Goal.norm_result termination], [])])] |> snd
    1.50          |> set_termination_rule termination
    1.51          |> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]]
    1.52      end
    1.53 @@ -184,23 +185,23 @@
    1.54  (* Datatype hook to declare datatype congs as "fundef_congs" *)
    1.55  
    1.56  
    1.57 -fun add_case_cong n thy = 
    1.58 -    Context.theory_map (map_fundef_congs (Drule.add_rule 
    1.59 +fun add_case_cong n thy =
    1.60 +    Context.theory_map (map_fundef_congs (Drule.add_rule
    1.61                            (DatatypePackage.get_datatype thy n |> the
    1.62                             |> #case_cong
    1.63 -                           |> safe_mk_meta_eq))) 
    1.64 +                           |> safe_mk_meta_eq)))
    1.65                         thy
    1.66  
    1.67  val case_cong_hook = fold add_case_cong
    1.68  
    1.69 -val setup_case_cong_hook = 
    1.70 +val setup_case_cong_hook =
    1.71      DatatypeHooks.add case_cong_hook
    1.72      #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
    1.73  
    1.74  (* setup *)
    1.75  
    1.76 -val setup = 
    1.77 -    FundefData.init 
    1.78 +val setup =
    1.79 +    FundefData.init
    1.80        #> FundefCongs.init
    1.81        #> TerminationRule.init
    1.82        #>  Attrib.add_attributes
     2.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Thu Nov 30 14:17:22 2006 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Thu Nov 30 14:17:25 2006 +0100
     2.3 @@ -237,7 +237,7 @@
     2.4                                  |> fold_rev (implies_intr o cprop_of) h_assums
     2.5                                  |> fold_rev (implies_intr o cprop_of) ags
     2.6                                  |> fold_rev forall_intr cqs
     2.7 -                                |> Drule.close_derivation
     2.8 +                                |> Goal.close_result
     2.9      in
    2.10        replace_lemma
    2.11      end
    2.12 @@ -367,7 +367,7 @@
    2.13                                    |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
    2.14  
    2.15          val goal = complete COMP (graph_is_function COMP conjunctionI)
    2.16 -                            |> Drule.close_derivation
    2.17 +                            |> Goal.close_result
    2.18  
    2.19          val goalI = Goal.protect goal
    2.20                                   |> fold_rev (implies_intr o cprop_of) compat
     3.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Thu Nov 30 14:17:22 2006 +0100
     3.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Thu Nov 30 14:17:25 2006 +0100
     3.3 @@ -299,7 +299,7 @@
     3.4      let
     3.5        val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
     3.6                                                                              
     3.7 -      val provedgoal = PROFILE "Closing Derivation" Drule.close_derivation provedgoal
     3.8 +      val provedgoal = PROFILE "Closing result" Goal.close_result provedgoal
     3.9                         
    3.10        val graph_is_function = PROFILE "Getting function theorem" (fn x => (x COMP conjunctionD1) |> forall_elim_vars 0) provedgoal
    3.11                                
     4.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Nov 30 14:17:22 2006 +0100
     4.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Nov 30 14:17:25 2006 +0100
     4.3 @@ -485,7 +485,7 @@
     4.4          (case skolem thy (name, Thm.transfer thy th) of
     4.5               NONE => ([th],thy)
     4.6             | SOME (thy',cls) => 
     4.7 -               let val cls = map Drule.local_standard cls
     4.8 +               let val cls = map Goal.close_result cls
     4.9                 in
    4.10                    if null cls then warning ("skolem_cache: empty clause set for " ^ name)
    4.11                    else ();
    4.12 @@ -506,7 +506,7 @@
    4.13          "" => skolem_thm th (*no name, so can't cache*)
    4.14        | s  => case Symtab.lookup (!clause_cache) s of
    4.15                  NONE => 
    4.16 -                  let val cls = map Drule.local_standard (skolem_thm th)
    4.17 +                  let val cls = map Goal.close_result (skolem_thm th)
    4.18                    in Output.debug "inserted into cache";
    4.19                       change clause_cache (Symtab.update (s, (th, cls))); cls 
    4.20                    end
     5.1 --- a/src/Pure/Isar/locale.ML	Thu Nov 30 14:17:22 2006 +0100
     5.2 +++ b/src/Pure/Isar/locale.ML	Thu Nov 30 14:17:25 2006 +0100
     5.3 @@ -1809,7 +1809,8 @@
     5.4      val (ctxt, (_, facts)) = activate_facts true (K I)
     5.5        (ProofContext.init pred_thy, axiomify predicate_axioms elemss');
     5.6      val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt;
     5.7 -    val export = singleton (ProofContext.export_standard view_ctxt thy_ctxt);
     5.8 +    val export = Goal.close_result o Goal.norm_result o
     5.9 +      singleton (ProofContext.export view_ctxt thy_ctxt);
    5.10      val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
    5.11      val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
    5.12      val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
     6.1 --- a/src/Pure/Isar/specification.ML	Thu Nov 30 14:17:22 2006 +0100
     6.2 +++ b/src/Pure/Isar/specification.ML	Thu Nov 30 14:17:25 2006 +0100
     6.3 @@ -273,7 +273,9 @@
     6.4        prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
     6.5  
     6.6      fun after_qed' results goal_ctxt' =
     6.7 -      let val results' = burrow (ProofContext.export_standard goal_ctxt' lthy) results in
     6.8 +      let val results' =
     6.9 +        burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results
    6.10 +      in
    6.11          lthy
    6.12          |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
    6.13          |> (fn (res, lthy') =>