--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Pr.thy Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,105 @@
+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
\ No newline at end of file