theory gcd imports Main begin (* definition (model) *) fun gcd :: "nat \ nat \ nat" where "gcd m 0 = m" | "gcd m n = gcd n (m mod n)" (* equivalent definitions *) fun gcd' :: "nat \ nat \ nat" where "gcd' m n = (if n = 0 then m else gcd' n (m mod n))" thm gcd'.simps thm gcd.simps fun gcd2 :: "nat \ nat \ nat" where "gcd2 m n = (case n=0 of True \m | False \ gcd2 n (m mod n))" thm gcd2.simps lemma [simp]: "gcd' m 0 = m" apply simp done lemma [simp]: "\ (n = 0) ==> gcd' m n = gcd' n (m mod n)" apply(simp) done declare gcd'.simps [simp del] lemma gcd'_mult_distrib2: " k * gcd' m n = gcd' (k * m) (k *n)" apply (induct m n rule: gcd'.induct) sorry thm gcd'_mult_distrib2 (*instantiating theorems, of, where, THEN*) lemmas gcd'_mult_0 = gcd'_mult_distrib2 [of k 1] (*problem variable k not longer ?k*) lemmas gcd'_mult_1 = gcd'_mult_distrib2 [of _ 1] lemmas gcd'_mult_2 = gcd'_mult_distrib2 [where m = 1] thm gcd'_mult_0 lemmas gcd'_mult_3 = gcd'_mult_0 [simplified] (* properties of gcd *) declare gcd'.simps [simp del] lemma gcd'_dvd_both: "(gcd' m n) dvd m \ (gcd' m n) dvd n" apply (induct m n rule: gcd'.induct) apply(case_tac "n=0") apply(clarify) apply(simp_all) apply (blast dest: dvd_mod_imp_dvd) done (*apply (blast dest: dvd_mod_imp_dvd) *) thm dvd_mod_imp_dvd lemmas gcd'_dvd1 [iff] = gcd'_dvd_both[THEN conjunct1] lemmas gcd'_dvd2 [iff] = gcd'_dvd_both[THEN conjunct2] thm gcd'.induct lemma gcd'_greatest [rule_format]: "k dvd m \ k dvd n \ k dvd gcd' m n" apply (induct m n rule: gcd'.induct) apply( case_tac "n = 0") apply(clarify) apply(simp_all) apply (simp_all add: dvd_mod) done thm dvd_mod theorem gcd'_greatest_iff [iff] : "(k dvd gcd' m n) = (k dvd m \ k dvd n)" thm dvd_trans by (blast intro! : gcd'_greatest intro: dvd_trans ) lemma dvd_nat_greater [rule_format]: "(k::nat) dvd m \ m \ 0 \ k \ m" by (clarsimp simp add: dvd_def) lemma gcd'_not_zero [rule_format]: "(0 < m \ 0 < n) \ 0 < (gcd' m n)" apply (induct m n rule:gcd'.induct) apply(case_tac "n=0") by simp+ theorem gcd'_greater [rule_format]: "(k dvd m \ k dvd n) \ (0 < m \ 0 < n) \ k \ gcd' m n" apply (rule impI) apply (rule dvd_nat_greater) by (simp add: gcd'_not_zero) theorem gcd'_distrib: "k * gcd' m n = gcd' (k * m) (k * n)" apply (induct_tac m n rule: gcd'.induct) apply simp apply(case_tac "n=0") apply(simp_all) oops (*Proving some facts for gcd*) lemma gcd_dvd_both: "(gcd m n) dvd m \ (gcd m n) dvd n" apply (induct m n rule: gcd.induct) apply simp apply clarsimp thm dvd_mod_imp_dvd by (erule dvd_mod_imp_dvd) lemmas gcd_dvd1 [iff] = gcd_dvd_both[THEN conjunct1] lemmas gcd_dvd2 [iff] = gcd_dvd_both[THEN conjunct2] lemma gcd_common [rule_format]: "k dvd m \ k dvd n \ k dvd (gcd m n)" apply (induct m n rule: gcd.induct) apply simp apply clarsimp by (erule dvd_mod) theorem gcd_common_iff [iff]: "(k dvd gcd m n) = (k dvd m \ k dvd n)" by (blast intro!: gcd_common intro: dvd_trans) (*lemma dvd_nat_greater [rule_format]: "(k::nat) dvd m \ m \ 0 \ k \ m" by (clarsimp simp add: dvd_def)*) lemma gcd_not_zero [rule_format]: "(0 < m \ 0 < n) \ 0 < (gcd m n)" apply (induct m n rule:gcd.induct) by simp+ theorem gcd_greatest [rule_format]: "(k dvd m \ k dvd n) \ (0 < m \ 0 < n) \ k \ gcd m n" apply (rule impI) apply (rule dvd_nat_greater) apply (simp) apply (rule gcd_not_zero) apply clarsimp done (* further properties *) theorem gcd_distrib: "k * gcd m n = gcd (k * m) (k * n)" apply (induct_tac m n rule: gcd.induct) apply simp apply (subst gcd.simps) apply (simp only:) apply (subst mod_mult_distrib2) apply (case_tac k) by simp+ (* equivalent definitions *) (*fun gcd' :: "nat \ nat \ nat" where "gcd' m n = (if n = 0 then m else gcd' n (m mod n))"*) theorem gcd'_eq_gcd: "gcd' m n = gcd m n" apply (induct m n rule: gcd.induct) by simp+ theorem gcd'_distrib: "k * gcd' m n = gcd' (k * m) (k * n)" by (simp only: gcd'_eq_gcd gcd_distrib) definition gcd_spec :: "nat \ nat \ nat" where "gcd_spec m n \ (if m = 0 then n else if n = 0 then m else SOME k. k dvd m \ k dvd n \ (\l. l dvd m \ l dvd n \ l \ k))" theorem gcd_spec_eq_gcd: "gcd_spec m n = gcd m n" apply (unfold gcd_spec_def) apply (split split_if) apply safe apply (case_tac n) apply clarsimp+ apply (rule some_equality) apply clarsimp apply (simp add: gcd_greatest) apply (rule le_antisym) apply (simp add: gcd_greatest) apply simp done (*Some further properties*) lemma "gcd m n = gcd n m" sorry (* Work also with gcd2*) end