# HG changeset patch # User nipkow # Date 1247682898 -7200 # Node ID a2a3685f61c3cb4690eb7b13982b680fc9304e51 # Parent 0e209ff7f236c919ba98b1a71b12695696e665c1 Made "prime" executable diff -r 0e209ff7f236 -r a2a3685f61c3 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Jul 15 15:09:33 2009 +0200 +++ b/src/HOL/GCD.thy Wed Jul 15 20:34:58 2009 +0200 @@ -159,7 +159,6 @@ transfer_int_nat_gcd transfer_int_nat_gcd_closures] - subsection {* GCD *} (* was gcd_induct *) @@ -1553,32 +1552,6 @@ apply (case_tac "p >= 0") by (blast, auto simp add: prime_ge_0_int) -(* To do: determine primality of any numeral *) - -lemma zero_not_prime_nat [simp]: "~prime (0::nat)" - by (simp add: prime_nat_def) - -lemma zero_not_prime_int [simp]: "~prime (0::int)" - by (simp add: prime_int_def) - -lemma one_not_prime_nat [simp]: "~prime (1::nat)" - by (simp add: prime_nat_def) - -lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)" - by (simp add: prime_nat_def One_nat_def) - -lemma one_not_prime_int [simp]: "~prime (1::int)" - by (simp add: prime_int_def) - -lemma two_is_prime_nat [simp]: "prime (2::nat)" - apply (auto simp add: prime_nat_def) - apply (case_tac m) - apply (auto dest!: dvd_imp_le) - done - -lemma two_is_prime_int [simp]: "prime (2::int)" - by (rule two_is_prime_nat [transferred direction: nat "op <= (0::int)"]) - lemma prime_imp_coprime_nat: "prime (p::nat) \ \ p dvd n \ coprime p n" apply (unfold prime_nat_def) apply (metis gcd_dvd1_nat gcd_dvd2_nat) @@ -1625,15 +1598,70 @@ apply auto done -lemma prime_imp_power_coprime_nat: "prime (p::nat) \ ~ p dvd a \ - coprime a (p^m)" +subsubsection{* Make prime naively executable *} + +lemma zero_not_prime_nat [simp]: "~prime (0::nat)" + by (simp add: prime_nat_def) + +lemma zero_not_prime_int [simp]: "~prime (0::int)" + by (simp add: prime_int_def) + +lemma one_not_prime_nat [simp]: "~prime (1::nat)" + by (simp add: prime_nat_def) + +lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)" + by (simp add: prime_nat_def One_nat_def) + +lemma one_not_prime_int [simp]: "~prime (1::int)" + by (simp add: prime_int_def) + +lemma prime_nat_code[code]: + "prime(p::nat) = (p > 1 & (ALL n : {1<.. 1 & (list_all (%n. ~ n dvd p) [2.. 1 & (ALL n : {1<.. 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))" +apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto) +apply simp +done + +lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard] + +declare successor_int_def[simp] + +lemma two_is_prime_nat [simp]: "prime (2::nat)" +by simp + +lemma two_is_prime_int [simp]: "prime (2::int)" +by simp + + +lemma prime_imp_power_coprime_nat: "prime (p::nat) \ ~ p dvd a \ coprime a (p^m)" apply (rule coprime_exp_nat) apply (subst gcd_commute_nat) apply (erule (1) prime_imp_coprime_nat) done -lemma prime_imp_power_coprime_int: "prime (p::int) \ ~ p dvd a \ - coprime a (p^m)" +lemma prime_imp_power_coprime_int: "prime (p::int) \ ~ p dvd a \ coprime a (p^m)" apply (rule coprime_exp_int) apply (subst gcd_commute_int) apply (erule (1) prime_imp_coprime_int) @@ -1652,12 +1680,10 @@ apply auto done -lemma primes_imp_powers_coprime_nat: "prime (p::nat) \ prime q \ p ~= q \ - coprime (p^m) (q^n)" +lemma primes_imp_powers_coprime_nat: "prime (p::nat) \ prime q \ p ~= q \ coprime (p^m) (q^n)" by (rule coprime_exp2_nat, rule primes_coprime_nat) -lemma primes_imp_powers_coprime_int: "prime (p::int) \ prime q \ p ~= q \ - coprime (p^m) (q^n)" +lemma primes_imp_powers_coprime_int: "prime (p::int) \ prime q \ p ~= q \ coprime (p^m) (q^n)" by (rule coprime_exp2_int, rule primes_coprime_int) lemma prime_factor_nat: "n \ (1::nat) \ \ p. prime p \ p dvd n" diff -r 0e209ff7f236 -r a2a3685f61c3 src/HOL/List.thy --- a/src/HOL/List.thy Wed Jul 15 15:09:33 2009 +0200 +++ b/src/HOL/List.thy Wed Jul 15 20:34:58 2009 +0200 @@ -3190,7 +3190,7 @@ begin definition -successor_int_def: "successor = (%i\int. i+1)" +successor_int_def[simp]: "successor = (%i\int. i+1)" instance by intro_classes (simp_all add: successor_int_def)