diff -r 5b01f7c233f8 -r a33d3040bf7e thys/Pr.thy
--- a/thys/Pr.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-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