src/HOL/Tools/function_package/fundef_package.ML
changeset 23819 2040846d1bbe
parent 23473 997bca36d4fe
child 24039 273698405054
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jul 16 21:17:12 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jul 16 21:22:43 2007 +0200
     1.3 @@ -44,20 +44,20 @@
     1.4  
     1.5  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
     1.6  
     1.7 -fun add_simps fixes post sort label moreatts simps lthy =
     1.8 +fun add_simps fnames post sort label moreatts simps lthy =
     1.9      let
    1.10 -      val fnames = map (fst o fst) fixes
    1.11 +      val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
    1.12 +      val spec = post simps
    1.13 +                   |> map (apfst (apsnd (append atts)))
    1.14  
    1.15        val (saved_spec_simps, lthy) =
    1.16 -        fold_map note_theorem (post simps) lthy
    1.17 +        fold_map note_theorem spec lthy
    1.18 +
    1.19        val saved_simps = flat (map snd saved_spec_simps)
    1.20 -
    1.21        val simps_by_f = sort saved_simps
    1.22  
    1.23        fun add_for_f fname simps =
    1.24 -        note_theorem
    1.25 -          ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts),
    1.26 -            simps) #> snd
    1.27 +        note_theorem ((NameSpace.qualified fname label, []), simps) #> snd
    1.28      in
    1.29        (saved_simps,
    1.30         fold2 add_for_f fnames simps_by_f lthy)
    1.31 @@ -68,8 +68,9 @@
    1.32        val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    1.33            cont (Goal.close_result proof)
    1.34  
    1.35 +      val fnames = map (fst o fst) fixes
    1.36        val qualify = NameSpace.qualified defname
    1.37 -      val addsmps = add_simps fixes post sort_cont
    1.38 +      val addsmps = add_simps fnames post sort_cont
    1.39  
    1.40        val (((psimps', pinducts'), (_, [termination'])), lthy) =
    1.41            lthy
    1.42 @@ -107,11 +108,11 @@
    1.43  fun gen_add_fundef prep fixspec eqnss config flags lthy =
    1.44      let
    1.45        val ((fixes, spec), ctxt') = prepare_spec prep fixspec eqnss lthy
    1.46 -      val (eqs, post) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    1.47 +      val (eqs, post, sort_cont) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    1.48  
    1.49        val defname = mk_defname fixes
    1.50  
    1.51 -      val ((goalstate, cont, sort_cont), lthy) =
    1.52 +      val ((goalstate, cont), lthy) =
    1.53            FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy
    1.54  
    1.55        val afterqed = fundef_afterqed config fixes post defname cont sort_cont
    1.56 @@ -190,6 +191,7 @@
    1.57      DatatypeHooks.add case_cong_hook
    1.58      #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
    1.59  
    1.60 +
    1.61  (* ad-hoc method to convert elimination-style goals to existential statements *)
    1.62  
    1.63  fun insert_int_goal thy subg st =