Removed (now unneeded) declaration of realizers for induction on natural numbers.
authorberghofe
Wed Aug 07 16:47:36 2002 +0200 (2002-08-07)
changeset 1346871118807d303
parent 13467 d66b526192bf
child 13469 70d8dfef587d
Removed (now unneeded) declaration of realizers for induction on natural numbers.
src/HOL/Extraction.thy
     1.1 --- a/src/HOL/Extraction.thy	Wed Aug 07 16:46:15 2002 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Wed Aug 07 16:47:36 2002 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  *}
     1.5  
     1.6  lemmas [extraction_expand] =
     1.7 -  nat.exhaust atomize_eq atomize_all atomize_imp
     1.8 +  atomize_eq atomize_all atomize_imp
     1.9    allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
    1.10    notE' impE' impE iffE imp_cong simp_thms
    1.11    induct_forall_eq induct_implies_eq induct_equal_eq
    1.12 @@ -407,37 +407,4 @@
    1.13    classical: "Null"
    1.14      "\<Lambda>P. classical \<cdot> _"
    1.15  
    1.16 -
    1.17 -subsection {* Induction on natural numbers *}
    1.18 -
    1.19 -theorem nat_ind_realizer:
    1.20 -  "R f 0 \<Longrightarrow> (\<And>y h. R h y \<Longrightarrow> R (g y h) (Suc y)) \<Longrightarrow>
    1.21 -     (R::'a \<Rightarrow> nat \<Rightarrow> bool) (nat_rec f g x) x"
    1.22 -proof -
    1.23 -  assume r1: "R f 0"
    1.24 -  assume r2: "\<And>y h. R h y \<Longrightarrow> R (g y h) (Suc y)"
    1.25 -  show "R (nat_rec f g x) x"
    1.26 -  proof (induct x)
    1.27 -    case 0
    1.28 -    from r1 show ?case by simp
    1.29 -  next
    1.30 -    case (Suc n)
    1.31 -    from Suc have "R (g n (nat_rec f g n)) (Suc n)" by (rule r2)
    1.32 -    thus ?case by simp
    1.33 -  qed
    1.34 -qed
    1.35 -
    1.36 -realizers
    1.37 -  Nat.nat_induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"
    1.38 -    "\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"
    1.39 -
    1.40 -  Nat.nat_induct: "Null"
    1.41 -    "\<Lambda>P n. nat_induct \<cdot> _ \<cdot> _"
    1.42 -
    1.43 -  Nat.nat.induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"
    1.44 -    "\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"
    1.45 -
    1.46 -  Nat.nat.induct: "Null"
    1.47 -    "\<Lambda>P n. nat_induct \<cdot> _ \<cdot> _"
    1.48 -
    1.49  end