src/HOL/Tools/function_package/fundef_package.ML
changeset 22733 0b14bb35be90
parent 22725 83099f0a9d8d
child 22846 fb79144af9a3
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Apr 20 00:28:07 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Apr 20 10:06:11 2007 +0200
     1.3 @@ -13,13 +13,13 @@
     1.4                        -> ((bstring * Attrib.src list) * (string * bool)) list 
     1.5                        -> FundefCommon.fundef_config
     1.6                        -> local_theory
     1.7 -                      -> string * Proof.state
     1.8 +                      -> Proof.state
     1.9  
    1.10      val add_fundef_i:  (string * typ option * mixfix) list
    1.11                         -> ((bstring * Attrib.src list) * (term * bool)) list
    1.12                         -> FundefCommon.fundef_config
    1.13                         -> local_theory
    1.14 -                       -> string * Proof.state
    1.15 +                       -> Proof.state
    1.16  
    1.17      val setup_termination_proof : string option -> local_theory -> Proof.state
    1.18  
    1.19 @@ -70,7 +70,7 @@
    1.20  
    1.21  fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
    1.22      let
    1.23 -      val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    1.24 +      val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    1.25            cont (Goal.close_result proof)
    1.26  
    1.27        val qualify = NameSpace.qualified defname
    1.28 @@ -87,12 +87,12 @@
    1.29              ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
    1.30  
    1.31        val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
    1.32 -                                  pinducts=snd pinducts', termination=termination', f=f, R=R }
    1.33 +                                  pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname }
    1.34        val cdata' = cdata |> morph_fundef_data (LocalTheory.target_morphism lthy);  (* FIXME !? *)
    1.35      in
    1.36        lthy 
    1.37 -        |> LocalTheory.declaration (fn phi => add_fundef_data defname (morph_fundef_data phi cdata)) (* save in target *)
    1.38 -        |> Context.proof_map (add_fundef_data defname cdata') (* also save in local context *)
    1.39 +        |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata)) (* save in target *)
    1.40 +        |> Context.proof_map (add_fundef_data cdata') (* also save in local context *)
    1.41      end (* FIXME: Add cases for induct and cases thm *)
    1.42  
    1.43  
    1.44 @@ -129,18 +129,17 @@
    1.45  
    1.46        val afterqed = fundef_afterqed config fixes spec defname cont sort_cont
    1.47      in
    1.48 -      (defname, lthy
    1.49 -         |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
    1.50 -         |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd)
    1.51 +      lthy
    1.52 +        |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
    1.53 +        |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
    1.54      end
    1.55  
    1.56  
    1.57 -fun total_termination_afterqed defname data [[totality]] lthy =
    1.58 +fun total_termination_afterqed data [[totality]] lthy =
    1.59      let
    1.60 -      val FundefCtxData { add_simps, psimps, pinducts, ... } = data
    1.61 +      val FundefCtxData { add_simps, psimps, pinducts, defname, ... } = data
    1.62  
    1.63        val totality = Goal.close_result totality
    1.64 -                       |> Thm.varifyT (* FIXME ! *)
    1.65  
    1.66        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
    1.67  
    1.68 @@ -159,16 +158,16 @@
    1.69      end
    1.70  
    1.71  
    1.72 -fun setup_termination_proof name_opt lthy =
    1.73 +fun setup_termination_proof term_opt lthy =
    1.74      let
    1.75 -        val defname = the_default (get_last_fundef (Context.Proof lthy)) name_opt
    1.76 -        val data = the (get_fundef_data defname (Context.Proof lthy))
    1.77 -                   handle Option.Option => raise ERROR ("No such function definition: " ^ defname)
    1.78 +      val data = the (case term_opt of
    1.79 +                        SOME t => import_fundef_data (ProofContext.read_term lthy t) (Context.Proof lthy)
    1.80 +                      | NONE => import_last_fundef (Context.Proof lthy))
    1.81 +          handle Option.Option => raise ERROR ("Not a function: " ^ quote (the_default "" term_opt))
    1.82  
    1.83          val FundefCtxData {termination, R, ...} = data
    1.84          val domT = domain_type (fastype_of R)
    1.85          val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
    1.86 -                     |> Type.freeze (* FIXME ! *)
    1.87      in
    1.88        lthy
    1.89          |> ProofContext.note_thmss_i "" [(("", [ContextRules.rule_del]), [([allI], [])])] |> snd
    1.90 @@ -176,8 +175,7 @@
    1.91          |> ProofContext.note_thmss_i ""
    1.92            [(("termination", [ContextRules.intro_bang (SOME 0)]),
    1.93              [([Goal.norm_result termination], [])])] |> snd
    1.94 -        |> set_termination_rule termination
    1.95 -        |> Proof.theorem_i NONE (total_termination_afterqed defname data) [[(goal, [])]]
    1.96 +        |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
    1.97      end
    1.98  
    1.99  
   1.100 @@ -230,12 +228,12 @@
   1.101    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   1.102    (fundef_parser default_config
   1.103       >> (fn ((config, fixes), statements) =>
   1.104 -            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config #> snd)
   1.105 +            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config)
   1.106              #> Toplevel.print));
   1.107  
   1.108  val terminationP =
   1.109    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   1.110 -  (P.opt_target -- Scan.option P.name
   1.111 +  (P.opt_target -- Scan.option P.term
   1.112      >> (fn (target, name) =>
   1.113             Toplevel.print o
   1.114             Toplevel.local_theory_to_proof target (setup_termination_proof name)));