doc-src/Functions/Thy/Functions.thy

   @{subgoals[display,indent=0]}
 
   \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 {*
   Proofs about partial functions are often not harder than for total
   functions. Fig.~\ref{findzero_isar} shows a slightly more

                and IH: "\<lbrakk>f n \<noteq> 0; x \<in> {Suc n ..< findzero f (Suc n)}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"
                and x_range: "x \<in> {n ..< findzero f n}"
   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
   
   from x_range have "x = n \<or> x \<in> {Suc n ..< findzero f n}" by auto
   thus "f x \<noteq> 0"
   proof
     assume "x = n"
     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
 qed
 text_raw {*

   the zero function. And in fact we have no problem proving this
   property by induction.
 *}
 (*<*)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
   @{term "nz_dom n"}. This allows us to prove it with the @{text
   pinduct} rule before we have proved termination. With this lemma,

 by pat_completeness auto
 
 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
   let ?R = "measure (\<lambda>x. 101 - x)"
   show "wf ?R" ..