tuned proofs;
authorwenzelm
Wed Nov 15 20:50:23 2006 +0100 (2006-11-15)
changeset 21392e571e84cbe89
parent 21391 a8809f46bd7f
child 21393 c648e24fd7ee
tuned proofs;
src/HOL/ex/Abstract_NAT.thy
     1.1 --- a/src/HOL/ex/Abstract_NAT.thy	Wed Nov 15 20:50:22 2006 +0100
     1.2 +++ b/src/HOL/ex/Abstract_NAT.thy	Wed Nov 15 20:50:23 2006 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4      case zero
     1.5      show "\<exists>!y. ?R zero y"
     1.6      proof
     1.7 -      show "?R zero e" by (rule Rec_zero)
     1.8 +      show "?R zero e" ..
     1.9        fix y assume "?R zero y"
    1.10        then show "y = e" by cases simp_all
    1.11      qed
    1.12 @@ -54,7 +54,7 @@
    1.13        and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" by blast
    1.14      show "\<exists>!z. ?R (succ m) z"
    1.15      proof
    1.16 -      from y show "?R (succ m) (r m y)" by (rule Rec_succ)
    1.17 +      from y show "?R (succ m) (r m y)" ..
    1.18        fix z assume "?R (succ m) z"
    1.19        then obtain u where "z = r m u" and "?R m u" by cases simp_all
    1.20        with yy' show "z = r m y" by (simp only:)
    1.21 @@ -77,7 +77,7 @@
    1.22  
    1.23  lemma rec_zero [simp]: "rec e r zero = e"
    1.24  proof (rule rec_eval)
    1.25 -  show "Rec e r zero e" by (rule Rec_zero)
    1.26 +  show "Rec e r zero e" ..
    1.27  qed
    1.28  
    1.29  lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)"
    1.30 @@ -85,7 +85,7 @@
    1.31    let ?R = "Rec e r"
    1.32    have "?R m (rec e r m)"
    1.33      unfolding rec_def using Rec_functional by (rule theI')
    1.34 -  then show "?R (succ m) (r m (rec e r m))" by (rule Rec_succ)
    1.35 +  then show "?R (succ m) (r m (rec e r m))" ..
    1.36  qed
    1.37  
    1.38  
    1.39 @@ -108,6 +108,10 @@
    1.40  lemma add_succ_right: "add m (succ n) = succ (add m n)"
    1.41    by (induct m) simp_all
    1.42  
    1.43 +lemma "add (succ (succ (succ zero))) (succ (succ zero)) =
    1.44 +    succ (succ (succ (succ (succ zero))))"
    1.45 +  by simp
    1.46 +
    1.47  
    1.48  text {* \medskip Example: replication (polymorphic) *}
    1.49