# HG changeset patch
# User haftmann
# Date 1213104654 -7200
# Node ID 5f139027c3653201b320b4b0784fe4a8ab401e44
# Parent  791607529f6d6c0c357a6cca454087d8d43071de
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar

diff -r 791607529f6d -r 5f139027c365 src/HOL/Algebra/Exponent.thy
--- 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 
diff -r 791607529f6d -r 5f139027c365 src/HOL/Auth/Message.thy
--- 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)
diff -r 791607529f6d -r 5f139027c365 src/HOL/Complex/CLim.thy
--- 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")
diff -r 791607529f6d -r 5f139027c365 src/HOL/Hyperreal/HyperDef.thy
--- 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
diff -r 791607529f6d -r 5f139027c365 src/HOL/Hyperreal/HyperNat.thy
--- 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
 
diff -r 791607529f6d -r 5f139027c365 src/HOL/Word/BinBoolList.thy
--- 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) 
diff -r 791607529f6d -r 5f139027c365 src/HOLCF/IOA/meta_theory/Sequence.thy
--- 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)