src/HOL/Nat.thy
changeset 35633 5da59c1ddece
parent 35416 d8d7d1b785af
child 35828 46cfc4b8112e
     1.1 --- a/src/HOL/Nat.thy	Sun Mar 07 07:29:34 2010 -0800
     1.2 +++ b/src/HOL/Nat.thy	Sun Mar 07 07:42:46 2010 -0800
     1.3 @@ -1400,6 +1400,20 @@
     1.4  apply (rule of_nat_mult [symmetric])
     1.5  done
     1.6  
     1.7 +lemma Nats_cases [cases set: Nats]:
     1.8 +  assumes "x \<in> \<nat>"
     1.9 +  obtains (of_nat) n where "x = of_nat n"
    1.10 +  unfolding Nats_def
    1.11 +proof -
    1.12 +  from `x \<in> \<nat>` have "x \<in> range of_nat" unfolding Nats_def .
    1.13 +  then obtain n where "x = of_nat n" ..
    1.14 +  then show thesis ..
    1.15 +qed
    1.16 +
    1.17 +lemma Nats_induct [case_names of_nat, induct set: Nats]:
    1.18 +  "x \<in> \<nat> \<Longrightarrow> (\<And>n. P (of_nat n)) \<Longrightarrow> P x"
    1.19 +  by (rule Nats_cases) auto
    1.20 +
    1.21  end
    1.22  
    1.23