# HG changeset patch
# User huffman
# Date 1267976566 28800
# Node ID 5da59c1ddece31dd5a74f7bec07df5ca2988d3d6
# Parent  61fd75e33137df7c5acb124cd660f448bb891269
add lemmas Nats_cases and Nats_induct

diff -r 61fd75e33137 -r 5da59c1ddece src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Mar 07 07:29:34 2010 -0800
+++ b/src/HOL/Nat.thy	Sun Mar 07 07:42:46 2010 -0800
@@ -1400,6 +1400,20 @@
 apply (rule of_nat_mult [symmetric])
 done
 
+lemma Nats_cases [cases set: Nats]:
+  assumes "x \<in> \<nat>"
+  obtains (of_nat) n where "x = of_nat n"
+  unfolding Nats_def
+proof -
+  from `x \<in> \<nat>` have "x \<in> range of_nat" unfolding Nats_def .
+  then obtain n where "x = of_nat n" ..
+  then show thesis ..
+qed
+
+lemma Nats_induct [case_names of_nat, induct set: Nats]:
+  "x \<in> \<nat> \<Longrightarrow> (\<And>n. P (of_nat n)) \<Longrightarrow> P x"
+  by (rule Nats_cases) auto
+
 end