src/HOL/Divides.thy
changeset 15251 bb6f072c8d10
parent 15140 322485b816ac
child 15439 71c0f98e31f1
     1.1 --- a/src/HOL/Divides.thy	Mon Oct 18 13:40:45 2004 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Oct 19 18:18:45 2004 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4  by (simp add: mod_geq)
     1.5  
     1.6  lemma mod_1 [simp]: "m mod Suc 0 = 0"
     1.7 -apply (induct_tac "m")
     1.8 +apply (induct "m")
     1.9  apply (simp_all (no_asm_simp) add: mod_geq)
    1.10  done
    1.11  
    1.12 @@ -98,7 +98,7 @@
    1.13  done
    1.14  
    1.15  lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
    1.16 -apply (subgoal_tac " (n + m) mod n = (n+m-n) mod n") 
    1.17 +apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n") 
    1.18  apply (simp add: add_commute)
    1.19  apply (subst mod_geq [symmetric], simp_all)
    1.20  done
    1.21 @@ -107,7 +107,7 @@
    1.22  by (simp add: add_commute mod_add_self2)
    1.23  
    1.24  lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
    1.25 -apply (induct_tac "k")
    1.26 +apply (induct "k")
    1.27  apply (simp_all add: add_left_commute [of _ n])
    1.28  done
    1.29  
    1.30 @@ -117,7 +117,7 @@
    1.31  lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
    1.32  apply (case_tac "n=0", simp)
    1.33  apply (case_tac "k=0", simp)
    1.34 -apply (induct_tac "m" rule: nat_less_induct)
    1.35 +apply (induct "m" rule: nat_less_induct)
    1.36  apply (subst mod_if, simp)
    1.37  apply (simp add: mod_geq diff_less diff_mult_distrib)
    1.38  done
    1.39 @@ -127,7 +127,7 @@
    1.40  
    1.41  lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
    1.42  apply (case_tac "n=0", simp)
    1.43 -apply (induct_tac "m", simp)
    1.44 +apply (induct "m", simp)
    1.45  apply (rename_tac "k")
    1.46  apply (cut_tac m = "k*n" and n = n in mod_add_self2)
    1.47  apply (simp add: add_commute)
    1.48 @@ -158,7 +158,7 @@
    1.49  (*Main Result about quotient and remainder.*)
    1.50  lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
    1.51  apply (case_tac "n=0", simp)
    1.52 -apply (induct_tac "m" rule: nat_less_induct)
    1.53 +apply (induct "m" rule: nat_less_induct)
    1.54  apply (subst mod_if)
    1.55  apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse diff_less)
    1.56  done
    1.57 @@ -219,7 +219,7 @@
    1.58  by (cut_tac m = m and n = n in mod_div_equality2, arith)
    1.59  
    1.60  lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
    1.61 -apply (induct_tac "m" rule: nat_less_induct)
    1.62 +apply (induct "m" rule: nat_less_induct)
    1.63  apply (case_tac "na<n", simp) 
    1.64  txt{*case @{term "n \<le> na"}*}
    1.65  apply (simp add: mod_geq diff_less)
    1.66 @@ -389,7 +389,7 @@
    1.67  subsection{*Further Facts about Quotient and Remainder*}
    1.68  
    1.69  lemma div_1 [simp]: "m div Suc 0 = m"
    1.70 -apply (induct_tac "m")
    1.71 +apply (induct "m")
    1.72  apply (simp_all (no_asm_simp) add: div_geq)
    1.73  done
    1.74  
    1.75 @@ -397,7 +397,7 @@
    1.76  by (simp add: div_geq)
    1.77  
    1.78  lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
    1.79 -apply (subgoal_tac " (n + m) div n = Suc ((n+m-n) div n) ")
    1.80 +apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
    1.81  apply (simp add: add_commute)
    1.82  apply (subst div_geq [symmetric], simp_all)
    1.83  done
    1.84 @@ -418,7 +418,7 @@
    1.85  lemma div_le_mono [rule_format (no_asm)]:
    1.86       "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
    1.87  apply (case_tac "k=0", simp)
    1.88 -apply (induct_tac "n" rule: nat_less_induct, clarify)
    1.89 +apply (induct "n" rule: nat_less_induct, clarify)
    1.90  apply (case_tac "n<k")
    1.91  (* 1  case n<k *)
    1.92  apply simp
    1.93 @@ -434,13 +434,13 @@
    1.94  lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
    1.95  apply (subgoal_tac "0<n")
    1.96   prefer 2 apply simp 
    1.97 -apply (induct_tac "k" rule: nat_less_induct)
    1.98 +apply (induct_tac k rule: nat_less_induct)
    1.99  apply (rename_tac "k")
   1.100  apply (case_tac "k<n", simp)
   1.101  apply (subgoal_tac "~ (k<m) ")
   1.102   prefer 2 apply simp 
   1.103  apply (simp add: div_geq)
   1.104 -apply (subgoal_tac " (k-n) div n \<le> (k-m) div n")
   1.105 +apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
   1.106   prefer 2
   1.107   apply (blast intro: div_le_mono diff_le_mono2)
   1.108  apply (rule le_trans, simp)
   1.109 @@ -457,14 +457,14 @@
   1.110  (* Similar for "less than" *) 
   1.111  lemma div_less_dividend [rule_format, simp]:
   1.112       "!!n::nat. 1<n ==> 0 < m --> m div n < m"
   1.113 -apply (induct_tac "m" rule: nat_less_induct)
   1.114 +apply (induct_tac m rule: nat_less_induct)
   1.115  apply (rename_tac "m")
   1.116  apply (case_tac "m<n", simp)
   1.117  apply (subgoal_tac "0<n")
   1.118   prefer 2 apply simp 
   1.119  apply (simp add: div_geq)
   1.120  apply (case_tac "n<m")
   1.121 - apply (subgoal_tac " (m-n) div n < (m-n) ")
   1.122 + apply (subgoal_tac "(m-n) div n < (m-n) ")
   1.123    apply (rule impI less_trans_Suc)+
   1.124  apply assumption
   1.125    apply (simp_all add: diff_less)
   1.126 @@ -473,7 +473,7 @@
   1.127  text{*A fact for the mutilated chess board*}
   1.128  lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
   1.129  apply (case_tac "n=0", simp)
   1.130 -apply (induct_tac "m" rule: nat_less_induct)
   1.131 +apply (induct "m" rule: nat_less_induct)
   1.132  apply (case_tac "Suc (na) <n")
   1.133  (* case Suc(na) < n *)
   1.134  apply (frule lessI [THEN less_trans], simp add: less_not_refl3)