src/HOL/Tools/function_package/fundef_package.ML
changeset 21602 cb13024d0e36
parent 21511 16c62deb1adf
child 21658 5e31241e1e3c
     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