# HG changeset patch
# User krauss
# Date 1207233292 -7200
# Node ID 03ad378ed5f0affb5d667a29145ae2b41dd9efe9
# Parent  944f9bf26d2d23032b772ab191192ba294187559
Function package no longer overwrites theorems.
Some tuning.

diff -r 944f9bf26d2d -r 03ad378ed5f0 src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML	Thu Apr 03 16:34:52 2008 +0200
@@ -81,8 +81,7 @@
 fun branch_vars t = 
     let 
       val t' = snd (dest_all_all t)
-      val assumes = Logic.strip_imp_prems t'
-      val concl = Logic.strip_imp_concl t'
+      val (assumes, concl) = Logic.strip_horn t'
     in (fold (curry add_term_vars) assumes [], term_vars concl)
     end
 
@@ -104,9 +103,9 @@
 fun mk_branch ctx t = 
     let
       val (ctx', fixes, impl) = dest_all_all_ctx ctx t
-      val assms = Logic.strip_imp_prems impl
+      val (assms, concl) = Logic.strip_horn impl
     in
-      (ctx', fixes, assms, rhs_of (Logic.strip_imp_concl impl))
+      (ctx', fixes, assms, rhs_of concl)
     end
     
 fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
diff -r 944f9bf26d2d -r 03ad378ed5f0 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Apr 03 16:34:52 2008 +0200
@@ -37,7 +37,6 @@
       psimps : thm list, 
       trsimps : thm list option, 
 
-      subset_pinducts : thm list, 
       simple_pinducts : thm list, 
       cases : thm,
       termination : thm,
@@ -51,7 +50,8 @@
       defname : string,
 
       (* contains no logical entities: invariant under morphisms *)
-      add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+      add_simps : (string -> string) -> string -> Attrib.src list -> thm list 
+                  -> local_theory -> thm list * local_theory,
       case_names : string list,
 
       fs : term list,
@@ -179,9 +179,7 @@
     let
       fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
       val (qs, imp) = open_all_all geq
-
-      val gs = Logic.strip_imp_prems imp
-      val eq = Logic.strip_imp_concl imp
+      val (gs, eq) = Logic.strip_horn imp
 
       val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
           handle TERM _ => error (input_error "Not an equation")
diff -r 944f9bf26d2d -r 03ad378ed5f0 src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Thu Apr 03 16:34:52 2008 +0200
@@ -684,7 +684,7 @@
         |> forall_intr (cterm_of thy a)
         |> forall_intr (cterm_of thy P)
     in
-      (subset_induct_all, simple_induct_rule)
+      simple_induct_rule
     end
 
 
@@ -927,7 +927,7 @@
                         
             val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
                          
-            val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule" 
+            val simple_pinduct = PROFILE "Proving partial induction rule" 
                                                            (mk_partial_induct_rule newthy globals R complete_thm) xclauses
                                                    
                                                    
@@ -940,7 +940,7 @@
                                                                         
           in 
             FundefResult {fs=[f], G=G, R=R, cases=complete_thm, 
-                          psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct], 
+                          psimps=psimps, simple_pinducts=[simple_pinduct], 
                           termination=total_intro, trsimps=trsimps,
                           domintros=dom_intros}
           end
diff -r 944f9bf26d2d -r 03ad378ed5f0 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Apr 03 16:34:52 2008 +0200
@@ -40,11 +40,12 @@
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
 
-fun add_simps fnames post sort label moreatts simps lthy =
+fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
     let
       val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
       val spec = post simps
                    |> map (apfst (apsnd (append atts)))
+                   |> map (apfst (apfst extra_qualify))
 
       val (saved_spec_simps, lthy) =
         fold_map note_theorem spec lthy
@@ -61,7 +62,7 @@
 
 fun fundef_afterqed config fixes post defname cont sort_cont cnames [[proof]] lthy =
     let
-      val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
+      val FundefResult {fs, R, psimps, trsimps,  simple_pinducts, termination, domintros, cases, ...} = 
           cont (Goal.close_result proof)
 
       val fnames = map (fst o fst) fixes
@@ -70,8 +71,8 @@
 
       val (((psimps', pinducts'), (_, [termination'])), lthy) =
           lthy
-            |> addsmps "psimps" [] psimps
-            ||> fold_option (snd oo addsmps "simps" []) trsimps
+            |> addsmps (NameSpace.qualified "partial") "psimps" [] psimps
+            ||> fold_option (snd oo addsmps I "simps" []) trsimps
             ||>> note_theorem ((qualify "pinduct",
                    [Attrib.internal (K (RuleCases.case_names cnames)),
                     Attrib.internal (K (RuleCases.consumes 1)),
@@ -125,7 +126,7 @@
       val qualify = NameSpace.qualified defname;
     in
       lthy
-        |> add_simps "simps" allatts tsimps |> snd
+        |> add_simps I "simps" allatts tsimps |> snd
         |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd
     end
 
diff -r 944f9bf26d2d -r 03ad378ed5f0 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Apr 03 16:34:52 2008 +0200
@@ -133,8 +133,8 @@
 fun dest_term (t : term) =
     let
       val (vars, prop) = FundefLib.dest_all_all t
-      val prems = Logic.strip_imp_prems prop
-      val (lhs, rhs) = Logic.strip_imp_concl prop
+      val (prems, concl) = Logic.strip_horn prop
+      val (lhs, rhs) = concl
                          |> HOLogic.dest_Trueprop
                          |> HOLogic.dest_mem |> fst
                          |> HOLogic.dest_prod
diff -r 944f9bf26d2d -r 03ad378ed5f0 src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Thu Apr 03 16:34:52 2008 +0200
@@ -269,7 +269,7 @@
 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
     let
       val result = inner_cont proof
-      val FundefResult {fs=[f], G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct],
+      val FundefResult {fs=[f], G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
                         termination,domintros} = result
                                                                                                                
       val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
@@ -290,7 +290,7 @@
       val mdomintros = map_option (map (full_simplify rew_ss)) domintros
     in
       FundefResult { fs=fs, G=G, R=R,
-                     psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
+                     psimps=mpsimps, simple_pinducts=minducts,
                      cases=cases, termination=mtermination,
                      domintros=mdomintros,
                      trsimps=mtrsimps}