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"