slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
--- a/src/HOL/Algebra/Exponent.thy Tue Jun 10 15:30:33 2008 +0200
+++ b/src/HOL/Algebra/Exponent.thy Tue Jun 10 15:30:54 2008 +0200
@@ -5,8 +5,9 @@
exponent p s yields the greatest power of p that divides s.
*)
-theory Exponent imports Main Primes Binomial begin
-
+theory Exponent
+imports Main Primes Binomial
+begin
section {*The Combinatorial Argument Underlying the First Sylow Theorem*}
definition exponent :: "nat => nat => nat" where
@@ -56,7 +57,7 @@
lemma prime_power_dvd_cases [rule_format (no_asm)]: "prime p
==> \<forall>m n. p^c dvd m*n -->
(\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
-apply (induct_tac "c")
+apply (induct c)
apply clarify
apply (case_tac "a")
apply simp
@@ -90,7 +91,7 @@
(*Lemma for power_dvd_bound*)
lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n"
-apply (induct_tac "n")
+apply (induct n)
apply (simp (no_asm_simp))
apply simp
apply (subgoal_tac "2 * n + 2 <= p * p^n", simp)
@@ -244,17 +245,17 @@
lemma p_not_div_choose_lemma [rule_format]:
"[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
==> k<K --> exponent p ((j+k) choose k) = 0"
-apply (case_tac "prime p")
+apply (cases "prime p")
prefer 2 apply simp
-apply (induct_tac "k")
+apply (induct k)
apply (simp (no_asm))
(*induction step*)
-apply (subgoal_tac "(Suc (j+n) choose Suc n) > 0")
+apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0")
prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
-apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) =
- exponent p (Suc n)")
+apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) =
+ exponent p (Suc k)")
txt{*First, use the assumed equation. We simplify the LHS to
- @{term "exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n)"}
+ @{term "exponent p (Suc (j + k) choose Suc k) + exponent p (Suc k)"}
the common terms cancel, proving the conclusion.*}
apply (simp del: bad_Sucs add: exponent_mult_add)
txt{*Establishing the equation requires first applying
--- a/src/HOL/Auth/Message.thy Tue Jun 10 15:30:33 2008 +0200
+++ b/src/HOL/Auth/Message.thy Tue Jun 10 15:30:54 2008 +0200
@@ -9,7 +9,9 @@
header{*Theory of Agents and Messages for Security Protocols*}
-theory Message imports Main begin
+theory Message
+imports Main
+begin
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
@@ -321,7 +323,7 @@
text{*In any message, there is an upper bound N on its greatest nonce.*}
lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
-apply (induct_tac "msg")
+apply (induct msg)
apply (simp_all (no_asm_simp) add: exI parts_insert2)
txt{*MPair case: blast works out the necessary sum itself!*}
prefer 2 apply auto apply (blast elim!: add_leE)
--- a/src/HOL/Complex/CLim.thy Tue Jun 10 15:30:33 2008 +0200
+++ b/src/HOL/Complex/CLim.thy Tue Jun 10 15:30:54 2008 +0200
@@ -123,7 +123,7 @@
lemma CDERIV_pow [simp]:
"DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
-apply (induct_tac "n")
+apply (induct n)
apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
apply (auto simp add: left_distrib real_of_nat_Suc)
apply (case_tac "n")
--- a/src/HOL/Hyperreal/HyperDef.thy Tue Jun 10 15:30:33 2008 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Tue Jun 10 15:30:54 2008 +0200
@@ -396,7 +396,7 @@
by (insert power_increasing [of 0 n "2::hypreal"], simp)
lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n"
-apply (induct_tac "n")
+apply (induct n)
apply (auto simp add: left_distrib)
apply (cut_tac n = n in two_hrealpow_ge_one, arith)
done
--- a/src/HOL/Hyperreal/HyperNat.thy Tue Jun 10 15:30:33 2008 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Tue Jun 10 15:30:54 2008 +0200
@@ -30,7 +30,7 @@
by transfer (rule Zero_not_Suc)
lemma hSuc_hSuc_eq [iff]: "\<And>m n. (hSuc m = hSuc n) = (m = n)"
-by transfer (rule Suc_Suc_eq)
+by transfer (rule nat.inject)
lemma zero_less_hSuc [iff]: "\<And>n. 0 < hSuc n"
by transfer (rule zero_less_Suc)
@@ -328,11 +328,13 @@
(*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
lemma HNatInfinite_FreeUltrafilterNat_lemma:
- "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
- ==> {n. N < f n} \<in> FreeUltrafilterNat"
-apply (induct_tac N)
+ assumes "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat"
+ shows "{n. N < f n} \<in> FreeUltrafilterNat"
+apply (induct N)
+using assms
apply (drule_tac x = 0 in spec, simp)
-apply (drule_tac x = "Suc n" in spec)
+using assms
+apply (drule_tac x = "Suc N" in spec)
apply (elim ultra, auto)
done
--- a/src/HOL/Word/BinBoolList.thy Tue Jun 10 15:30:33 2008 +0200
+++ b/src/HOL/Word/BinBoolList.thy Tue Jun 10 15:30:54 2008 +0200
@@ -174,7 +174,7 @@
lemma bin_to_bl_aux_bintr [rule_format] :
"ALL m bin bl. bin_to_bl_aux n (bintrunc m bin) bl =
replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
- apply (induct_tac "n")
+ apply (induct n)
apply clarsimp
apply clarsimp
apply (case_tac "m")
@@ -259,12 +259,12 @@
lemma nth_bin_to_bl_aux [rule_format] :
"ALL w n bl. n < m + length bl --> (bin_to_bl_aux m w bl) ! n =
(if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))"
- apply (induct_tac "m")
+ apply (induct m)
apply clarsimp
apply clarsimp
apply (case_tac w rule: bin_exhaust)
apply clarsimp
- apply (case_tac "na - n")
+ apply (case_tac "n - m")
apply arith
apply simp
apply (rule_tac f = "%n. bl ! n" in arg_cong)
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Jun 10 15:30:33 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Jun 10 15:30:54 2008 +0200
@@ -973,7 +973,7 @@
apply (rule mp)
prefer 2 apply assumption
apply (rule_tac x="x" in spec)
-apply (rule nat_induct)
+apply (rule nat.induct)
apply simp
apply (rule allI)
apply (case_tac "Forall Q xa")
@@ -1016,7 +1016,7 @@
apply (rule mp)
prefer 2 apply assumption
apply (rule_tac x="x" in spec)
-apply (rule nat_induct)
+apply (rule nat.induct)
apply simp
apply (rule allI)
apply (rule_tac x="xa" in Seq_cases)