src/HOL/Divides.thy
 changeset 14640 b31870c50c68 parent 14437 92f6aa05b7bb child 15131 c69542757a4d
```     1.1 --- a/src/HOL/Divides.thy	Thu Apr 22 09:23:13 2004 +0200
1.2 +++ b/src/HOL/Divides.thy	Thu Apr 22 10:43:06 2004 +0200
1.3 @@ -753,6 +753,95 @@
1.4    apply arith
1.5    done
1.6
1.7 +subsection {*An ``induction'' law for modulus arithmetic.*}
1.8 +
1.9 +lemma mod_induct_0:
1.10 +  assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
1.11 +  and base: "P i" and i: "i<p"
1.12 +  shows "P 0"
1.13 +proof (rule ccontr)
1.14 +  assume contra: "\<not>(P 0)"
1.15 +  from i have p: "0<p" by simp
1.16 +  have "\<forall>k. 0<k \<longrightarrow> \<not> P (p-k)" (is "\<forall>k. ?A k")
1.17 +  proof
1.18 +    fix k
1.19 +    show "?A k"
1.20 +    proof (induct k)
1.21 +      show "?A 0" by simp  -- "by contradiction"
1.22 +    next
1.23 +      fix n
1.24 +      assume ih: "?A n"
1.25 +      show "?A (Suc n)"
1.26 +      proof (clarsimp)
1.27 +	assume y: "P (p - Suc n)"
1.28 +	have n: "Suc n < p"
1.29 +	proof (rule ccontr)
1.30 +	  assume "\<not>(Suc n < p)"
1.31 +	  hence "p - Suc n = 0"
1.32 +	    by simp
1.33 +	  with y contra show "False"
1.34 +	    by simp
1.35 +	qed
1.36 +	hence n2: "Suc (p - Suc n) = p-n" by arith
1.37 +	from p have "p - Suc n < p" by arith
1.38 +	with y step have z: "P ((Suc (p - Suc n)) mod p)"
1.39 +	  by blast
1.40 +	show "False"
1.41 +	proof (cases "n=0")
1.42 +	  case True
1.43 +	  with z n2 contra show ?thesis by simp
1.44 +	next
1.45 +	  case False
1.46 +	  with p have "p-n < p" by arith
1.47 +	  with z n2 False ih show ?thesis by simp
1.48 +	qed
1.49 +      qed
1.50 +    qed
1.51 +  qed
1.52 +  moreover
1.53 +  from i obtain k where "0<k \<and> i+k=p"
1.54 +    by (blast dest: less_imp_add_positive)
1.55 +  hence "0<k \<and> i=p-k" by auto
1.56 +  moreover
1.57 +  note base
1.58 +  ultimately
1.59 +  show "False" by blast
1.60 +qed
1.61 +
1.62 +lemma mod_induct:
1.63 +  assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
1.64 +  and base: "P i" and i: "i<p" and j: "j<p"
1.65 +  shows "P j"
1.66 +proof -
1.67 +  have "\<forall>j<p. P j"
1.68 +  proof
1.69 +    fix j
1.70 +    show "j<p \<longrightarrow> P j" (is "?A j")
1.71 +    proof (induct j)
1.72 +      from step base i show "?A 0"
1.73 +	by (auto elim: mod_induct_0)
1.74 +    next
1.75 +      fix k
1.76 +      assume ih: "?A k"
1.77 +      show "?A (Suc k)"
1.78 +      proof
1.79 +	assume suc: "Suc k < p"
1.80 +	hence k: "k<p" by simp
1.81 +	with ih have "P k" ..
1.82 +	with step k have "P (Suc k mod p)"
1.83 +	  by blast
1.84 +	moreover
1.85 +	from suc have "Suc k mod p = Suc k"
1.86 +	  by simp
1.87 +	ultimately
1.88 +	show "P (Suc k)" by simp
1.89 +      qed
1.90 +    qed
1.91 +  qed
1.92 +  with j show ?thesis by blast
1.93 +qed
1.94 +
1.95 +
1.96  ML
1.97  {*
1.98  val div_def = thm "div_def"
```