src/HOL/Tools/function_package/fundef_package.ML
changeset 21319 cf814e36f788
parent 21255 617fdb08abe9
child 21359 072e83a0b5bb
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Nov 13 12:10:49 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Nov 13 13:51:22 2006 +0100
     1.3 @@ -38,8 +38,6 @@
     1.4  open FundefLib
     1.5  open FundefCommon
     1.6  
     1.7 -(*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*)
     1.8 -
     1.9  fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    1.10      let val (xs, ys) = split_list ps
    1.11      in xs ~~ f ys end
    1.12 @@ -64,8 +62,9 @@
    1.13      end
    1.14  
    1.15  
    1.16 -fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy =
    1.17 +fun fundef_afterqed config fixes spec mutual_info defname data [[result]] lthy =
    1.18      let
    1.19 +      val FundefConfig { domintros, ...} = config
    1.20        val Prep {f, R, ...} = data
    1.21        val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
    1.22        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    1.23 @@ -119,7 +118,7 @@
    1.24        val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) =
    1.25            FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy
    1.26  
    1.27 -      val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
    1.28 +      val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
    1.29      in
    1.30        (name, lthy
    1.31           |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
    1.32 @@ -162,6 +161,7 @@
    1.33        lthy
    1.34          |> ProofContext.note_thmss_i [(("termination",
    1.35                                          [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
    1.36 +        |> set_termination_rule termination
    1.37          |> Proof.theorem_i PureThy.internalK NONE
    1.38                             (total_termination_afterqed name data) NONE ("", [])
    1.39                             [(("", []), [(goal, [])])]
    1.40 @@ -199,9 +199,11 @@
    1.41  val setup = 
    1.42      FundefData.init 
    1.43        #> FundefCongs.init
    1.44 +      #> TerminationRule.init
    1.45        #>  Attrib.add_attributes
    1.46              [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
    1.47        #> setup_case_cong_hook
    1.48 +      #> FundefRelation.setup
    1.49  
    1.50  val get_congs = FundefCommon.get_fundef_congs o Context.Theory
    1.51