theory Pr+ −
imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Real"+ −
begin+ −
+ −
fun + −
add :: "nat \<Rightarrow> nat \<Rightarrow> nat" + −
where+ −
"add 0 n = n" |+ −
"add (Suc m) n = Suc (add m n)"+ −
+ −
fun + −
doub :: "nat \<Rightarrow> nat" + −
where+ −
"doub 0 = 0" |+ −
"doub n = n + n"+ −
+ −
lemma add_lem:+ −
"add m n = m + n"+ −
apply(induct m arbitrary: )+ −
apply(auto)+ −
done+ −
+ −
fun + −
count :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"+ −
where+ −
"count n Nil = 0" |+ −
"count n (x # xs) = (if n = x then (add 1 (count n xs)) else count n xs)"+ −
+ −
value "count 3 [1,2,3,3,4,3,5]"+ −
+ −
fun + −
count2 :: "nat \<Rightarrow> nat list \<Rightarrow> nat" + −
where+ −
"count2 n Nil = 0" |+ −
"count2 n (Cons x xs) = (if n = x then (add 1 (count2 n xs)) else count2 n xs)"+ −
+ −
value "count2 (2::nat) [2,2,3::nat]"+ −
+ −
lemma+ −
"count2 x xs \<le> length xs"+ −
apply(induct xs)+ −
apply(simp)+ −
apply(simp)+ −
apply(auto)+ −
done+ −
+ −
fun + −
sum :: "nat \<Rightarrow> nat"+ −
where+ −
"sum 0 = 0"+ −
| "sum (Suc n) = (Suc n) + sum n"+ −
+ −
lemma+ −
"sum n = (n * (Suc n)) div 2"+ −
apply(induct n)+ −
apply(auto)+ −
done+ −
+ −
+ −
lemma+ −
"doub n = add n n"+ −
apply(induct n)+ −
apply(simp)+ −
apply(simp add: add_lem)+ −
done+ −
+ −
lemma + −
fixes a b::nat+ −
shows "(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2"+ −
apply(simp add: power2_sum)+ −
done+ −
+ −
lemma+ −
fixes a b c::"real"+ −
assumes eq: "a * c \<le> b * c" and ineq: "b < a"+ −
shows "c \<le> 0"+ −
proof -+ −
{+ −
assume "0 < c" + −
then have "b * c < a * c" using ineq by(auto)+ −
then have "False" using eq by auto+ −
} then show "c \<le> 0" by (auto simp add: not_le[symmetric]) + −
qed+ −
+ −
+ −
+ −
+ −
lemma "n > 1 \<Longrightarrow> \<not>(prime (2 * n))"+ −
by (metis One_nat_def Suc_leI less_Suc0 not_le numeral_eq_one_iff prime_product semiring_norm(85))+ −
+ −
+ −
+ −
lemma + −
fixes n::"nat"+ −
assumes a: "n > 1"+ −
and b: "\<not>(prime n)"+ −
shows "\<not>(prime ((2 ^ n) - 1))" + −
using a b+ −
apply(induct n)+ −
apply(simp)+ −
apply(simp)+ −
+ −
+ −
+ −
end+ −