Function package no longer overwrites theorems.
authorkrauss
Thu Apr 03 16:34:52 2008 +0200 (2008-04-03)
changeset 2652903ad378ed5f0
parent 26528 944f9bf26d2d
child 26530 777f334ff652
Function package no longer overwrites theorems.
Some tuning.
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/function_package/mutual.ML
     1.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Thu Apr 03 16:03:59 2008 +0200
     1.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Thu Apr 03 16:34:52 2008 +0200
     1.3 @@ -81,8 +81,7 @@
     1.4  fun branch_vars t = 
     1.5      let 
     1.6        val t' = snd (dest_all_all t)
     1.7 -      val assumes = Logic.strip_imp_prems t'
     1.8 -      val concl = Logic.strip_imp_concl t'
     1.9 +      val (assumes, concl) = Logic.strip_horn t'
    1.10      in (fold (curry add_term_vars) assumes [], term_vars concl)
    1.11      end
    1.12  
    1.13 @@ -104,9 +103,9 @@
    1.14  fun mk_branch ctx t = 
    1.15      let
    1.16        val (ctx', fixes, impl) = dest_all_all_ctx ctx t
    1.17 -      val assms = Logic.strip_imp_prems impl
    1.18 +      val (assms, concl) = Logic.strip_horn impl
    1.19      in
    1.20 -      (ctx', fixes, assms, rhs_of (Logic.strip_imp_concl impl))
    1.21 +      (ctx', fixes, assms, rhs_of concl)
    1.22      end
    1.23      
    1.24  fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
     2.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Apr 03 16:03:59 2008 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Apr 03 16:34:52 2008 +0200
     2.3 @@ -37,7 +37,6 @@
     2.4        psimps : thm list, 
     2.5        trsimps : thm list option, 
     2.6  
     2.7 -      subset_pinducts : thm list, 
     2.8        simple_pinducts : thm list, 
     2.9        cases : thm,
    2.10        termination : thm,
    2.11 @@ -51,7 +50,8 @@
    2.12        defname : string,
    2.13  
    2.14        (* contains no logical entities: invariant under morphisms *)
    2.15 -      add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
    2.16 +      add_simps : (string -> string) -> string -> Attrib.src list -> thm list 
    2.17 +                  -> local_theory -> thm list * local_theory,
    2.18        case_names : string list,
    2.19  
    2.20        fs : term list,
    2.21 @@ -179,9 +179,7 @@
    2.22      let
    2.23        fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
    2.24        val (qs, imp) = open_all_all geq
    2.25 -
    2.26 -      val gs = Logic.strip_imp_prems imp
    2.27 -      val eq = Logic.strip_imp_concl imp
    2.28 +      val (gs, eq) = Logic.strip_horn imp
    2.29  
    2.30        val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
    2.31            handle TERM _ => error (input_error "Not an equation")
     3.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Thu Apr 03 16:03:59 2008 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Thu Apr 03 16:34:52 2008 +0200
     3.3 @@ -684,7 +684,7 @@
     3.4          |> forall_intr (cterm_of thy a)
     3.5          |> forall_intr (cterm_of thy P)
     3.6      in
     3.7 -      (subset_induct_all, simple_induct_rule)
     3.8 +      simple_induct_rule
     3.9      end
    3.10  
    3.11  
    3.12 @@ -927,7 +927,7 @@
    3.13                          
    3.14              val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
    3.15                           
    3.16 -            val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule" 
    3.17 +            val simple_pinduct = PROFILE "Proving partial induction rule" 
    3.18                                                             (mk_partial_induct_rule newthy globals R complete_thm) xclauses
    3.19                                                     
    3.20                                                     
    3.21 @@ -940,7 +940,7 @@
    3.22                                                                          
    3.23            in 
    3.24              FundefResult {fs=[f], G=G, R=R, cases=complete_thm, 
    3.25 -                          psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct], 
    3.26 +                          psimps=psimps, simple_pinducts=[simple_pinduct], 
    3.27                            termination=total_intro, trsimps=trsimps,
    3.28                            domintros=dom_intros}
    3.29            end
     4.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Apr 03 16:03:59 2008 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Apr 03 16:34:52 2008 +0200
     4.3 @@ -40,11 +40,12 @@
     4.4  
     4.5  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
     4.6  
     4.7 -fun add_simps fnames post sort label moreatts simps lthy =
     4.8 +fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
     4.9      let
    4.10        val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
    4.11        val spec = post simps
    4.12                     |> map (apfst (apsnd (append atts)))
    4.13 +                   |> map (apfst (apfst extra_qualify))
    4.14  
    4.15        val (saved_spec_simps, lthy) =
    4.16          fold_map note_theorem spec lthy
    4.17 @@ -61,7 +62,7 @@
    4.18  
    4.19  fun fundef_afterqed config fixes post defname cont sort_cont cnames [[proof]] lthy =
    4.20      let
    4.21 -      val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    4.22 +      val FundefResult {fs, R, psimps, trsimps,  simple_pinducts, termination, domintros, cases, ...} = 
    4.23            cont (Goal.close_result proof)
    4.24  
    4.25        val fnames = map (fst o fst) fixes
    4.26 @@ -70,8 +71,8 @@
    4.27  
    4.28        val (((psimps', pinducts'), (_, [termination'])), lthy) =
    4.29            lthy
    4.30 -            |> addsmps "psimps" [] psimps
    4.31 -            ||> fold_option (snd oo addsmps "simps" []) trsimps
    4.32 +            |> addsmps (NameSpace.qualified "partial") "psimps" [] psimps
    4.33 +            ||> fold_option (snd oo addsmps I "simps" []) trsimps
    4.34              ||>> note_theorem ((qualify "pinduct",
    4.35                     [Attrib.internal (K (RuleCases.case_names cnames)),
    4.36                      Attrib.internal (K (RuleCases.consumes 1)),
    4.37 @@ -125,7 +126,7 @@
    4.38        val qualify = NameSpace.qualified defname;
    4.39      in
    4.40        lthy
    4.41 -        |> add_simps "simps" allatts tsimps |> snd
    4.42 +        |> add_simps I "simps" allatts tsimps |> snd
    4.43          |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd
    4.44      end
    4.45  
     5.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Apr 03 16:03:59 2008 +0200
     5.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Apr 03 16:34:52 2008 +0200
     5.3 @@ -133,8 +133,8 @@
     5.4  fun dest_term (t : term) =
     5.5      let
     5.6        val (vars, prop) = FundefLib.dest_all_all t
     5.7 -      val prems = Logic.strip_imp_prems prop
     5.8 -      val (lhs, rhs) = Logic.strip_imp_concl prop
     5.9 +      val (prems, concl) = Logic.strip_horn prop
    5.10 +      val (lhs, rhs) = concl
    5.11                           |> HOLogic.dest_Trueprop
    5.12                           |> HOLogic.dest_mem |> fst
    5.13                           |> HOLogic.dest_prod
     6.1 --- a/src/HOL/Tools/function_package/mutual.ML	Thu Apr 03 16:03:59 2008 +0200
     6.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Thu Apr 03 16:34:52 2008 +0200
     6.3 @@ -269,7 +269,7 @@
     6.4  fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
     6.5      let
     6.6        val result = inner_cont proof
     6.7 -      val FundefResult {fs=[f], G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct],
     6.8 +      val FundefResult {fs=[f], G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
     6.9                          termination,domintros} = result
    6.10                                                                                                                 
    6.11        val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
    6.12 @@ -290,7 +290,7 @@
    6.13        val mdomintros = map_option (map (full_simplify rew_ss)) domintros
    6.14      in
    6.15        FundefResult { fs=fs, G=G, R=R,
    6.16 -                     psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
    6.17 +                     psimps=mpsimps, simple_pinducts=minducts,
    6.18                       cases=cases, termination=mtermination,
    6.19                       domintros=mdomintros,
    6.20                       trsimps=mtrsimps}