# HG changeset patch
# User krauss
# Date 1285660447 -7200
# Node ID 150f831ce4a339a3717d10a69ae447cb04005f4f
# Parent  ec6dfd9ce573f65639cf93accf774921c45aebbc
no longer declare .psimps rules as [simp].

This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.

diff -r ec6dfd9ce573 -r 150f831ce4a3 NEWS
--- a/NEWS	Tue Sep 28 09:43:13 2010 +0200
+++ b/NEWS	Tue Sep 28 09:54:07 2010 +0200
@@ -236,6 +236,9 @@
 generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
 The theorems bij_def and surj_def are unchanged.
 
+* Function package: .psimps rules are no longer implicitly declared [simp].
+INCOMPATIBILITY.
+
 *** FOL ***
 
 * All constant names are now qualified.  INCOMPATIBILITY.
diff -r ec6dfd9ce573 -r 150f831ce4a3 doc-src/Functions/Thy/Functions.thy
--- a/doc-src/Functions/Thy/Functions.thy	Tue Sep 28 09:43:13 2010 +0200
+++ b/doc-src/Functions/Thy/Functions.thy	Tue Sep 28 09:54:07 2010 +0200
@@ -763,11 +763,10 @@
   \noindent The hypothesis in our lemma was used to satisfy the first premise in
   the induction rule. However, we also get @{term
   "findzero_dom (f, n)"} as a local assumption in the induction step. This
-  allows to unfold @{term "findzero f n"} using the @{text psimps}
-  rule, and the rest is trivial. Since the @{text psimps} rules carry the
-  @{text "[simp]"} attribute by default, we just need a single step:
+  allows unfolding @{term "findzero f n"} using the @{text psimps}
+  rule, and the rest is trivial.
  *}
-apply simp
+apply (simp add: findzero.psimps)
 done
 
 text {*
@@ -794,7 +793,7 @@
   have "f n \<noteq> 0"
   proof 
     assume "f n = 0"
-    with dom have "findzero f n = n" by simp
+    with dom have "findzero f n = n" by (simp add: findzero.psimps)
     with x_range show False by auto
   qed
   
@@ -805,7 +804,7 @@
     with `f n \<noteq> 0` show ?thesis by simp
   next
     assume "x \<in> {Suc n ..< findzero f n}"
-    with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by simp
+    with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by (simp add: findzero.psimps)
     with IH and `f n \<noteq> 0`
     show ?thesis by simp
   qed
@@ -1069,7 +1068,7 @@
 *}
 (*<*)oops(*>*)
 lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"
-  by (induct rule:nz.pinduct) auto
+  by (induct rule:nz.pinduct) (auto simp: nz.psimps)
 
 text {*
   We formulate this as a partial correctness lemma with the condition
@@ -1105,7 +1104,7 @@
 lemma f91_estimate: 
   assumes trm: "f91_dom n" 
   shows "n < f91 n + 11"
-using trm by induct auto
+using trm by induct (auto simp: f91.psimps)
 
 termination
 proof
diff -r ec6dfd9ce573 -r 150f831ce4a3 src/HOL/Imperative_HOL/Mrec.thy
--- a/src/HOL/Imperative_HOL/Mrec.thy	Tue Sep 28 09:43:13 2010 +0200
+++ b/src/HOL/Imperative_HOL/Mrec.thy	Tue Sep 28 09:54:07 2010 +0200
@@ -54,7 +54,7 @@
            | None \<Rightarrow> None)
    | None \<Rightarrow> None
    )"
-apply (cases "mrec_dom (x,h)", simp)
+apply (cases "mrec_dom (x,h)", simp add: mrec.psimps)
 apply (frule mrec_default)
 apply (frule mrec_di_reverse, simp)
 by (auto split: sum.split option.split simp: mrec_default)
@@ -105,7 +105,7 @@
       proof (cases a)
         case (Inl aa)
         from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
-          by auto
+          by (auto simp: mrec.psimps)
       next
         case (Inr b)
         note Inr' = this
@@ -122,15 +122,15 @@
             apply auto
             apply (rule rec_case)
             apply auto
-            unfolding MREC_def by auto
+            unfolding MREC_def by (auto simp: mrec.psimps)
         next
           case None
-          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto
+          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by (auto simp: mrec.psimps)
         qed
       qed
     next
       case None
-      from this 1(1) mrec 1(3) show ?thesis by simp
+      from this 1(1) mrec 1(3) show ?thesis by (simp add: mrec.psimps)
     qed
   qed
   from this h'_r show ?thesis by simp
diff -r ec6dfd9ce573 -r 150f831ce4a3 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Sep 28 09:43:13 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML	Tue Sep 28 09:54:07 2010 +0200
@@ -52,8 +52,7 @@
    Nitpick_Simps.add]
 
 val psimp_attribs = map (Attrib.internal o K)
-  [Simplifier.simp_add,
-   Nitpick_Psimps.add]
+  [Nitpick_Psimps.add]
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 
diff -r ec6dfd9ce573 -r 150f831ce4a3 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Tue Sep 28 09:43:13 2010 +0200
+++ b/src/HOL/ex/Fundefs.thy	Tue Sep 28 09:54:07 2010 +0200
@@ -51,7 +51,7 @@
   assumes trm: "nz_dom x"
   shows "nz x = 0"
 using trm
-by induct auto
+by induct (auto simp: nz.psimps)
 
 termination nz
   by (relation "less_than") (auto simp:nz_is_zero)
@@ -71,7 +71,7 @@
 lemma f91_estimate: 
   assumes trm: "f91_dom n"
   shows "n < f91 n + 11"
-using trm by induct auto
+using trm by induct (auto simp: f91.psimps)
 
 termination
 proof
diff -r ec6dfd9ce573 -r 150f831ce4a3 src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Tue Sep 28 09:43:13 2010 +0200
+++ b/src/HOL/ex/Unification.thy	Tue Sep 28 09:54:07 2010 +0200
@@ -158,6 +158,7 @@
                                          Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
   by pat_completeness auto
 
+declare unify.psimps[simp]
 
 subsection {* Partial correctness *}
 
@@ -533,4 +534,6 @@
   qed
 qed
 
+declare unify.psimps[simp del]
+
 end