theory Primports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Real"beginfun 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)donefun 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)donefun 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)donelemma "doub n = add n n"apply(induct n)apply(simp)apply(simp add: add_lem)donelemma fixes a b::nat shows "(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2"apply(simp add: power2_sum)donelemma 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]) qedlemma "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 bapply(induct n)apply(simp)apply(simp)end