1 theory Pr |
|
2 imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Real" |
|
3 begin |
|
4 |
|
5 fun |
|
6 add :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
7 where |
|
8 "add 0 n = n" | |
|
9 "add (Suc m) n = Suc (add m n)" |
|
10 |
|
11 fun |
|
12 doub :: "nat \<Rightarrow> nat" |
|
13 where |
|
14 "doub 0 = 0" | |
|
15 "doub n = n + n" |
|
16 |
|
17 lemma add_lem: |
|
18 "add m n = m + n" |
|
19 apply(induct m arbitrary: ) |
|
20 apply(auto) |
|
21 done |
|
22 |
|
23 fun |
|
24 count :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" |
|
25 where |
|
26 "count n Nil = 0" | |
|
27 "count n (x # xs) = (if n = x then (add 1 (count n xs)) else count n xs)" |
|
28 |
|
29 value "count 3 [1,2,3,3,4,3,5]" |
|
30 |
|
31 fun |
|
32 count2 :: "nat \<Rightarrow> nat list \<Rightarrow> nat" |
|
33 where |
|
34 "count2 n Nil = 0" | |
|
35 "count2 n (Cons x xs) = (if n = x then (add 1 (count2 n xs)) else count2 n xs)" |
|
36 |
|
37 value "count2 (2::nat) [2,2,3::nat]" |
|
38 |
|
39 lemma |
|
40 "count2 x xs \<le> length xs" |
|
41 apply(induct xs) |
|
42 apply(simp) |
|
43 apply(simp) |
|
44 apply(auto) |
|
45 done |
|
46 |
|
47 fun |
|
48 sum :: "nat \<Rightarrow> nat" |
|
49 where |
|
50 "sum 0 = 0" |
|
51 | "sum (Suc n) = (Suc n) + sum n" |
|
52 |
|
53 lemma |
|
54 "sum n = (n * (Suc n)) div 2" |
|
55 apply(induct n) |
|
56 apply(auto) |
|
57 done |
|
58 |
|
59 |
|
60 lemma |
|
61 "doub n = add n n" |
|
62 apply(induct n) |
|
63 apply(simp) |
|
64 apply(simp add: add_lem) |
|
65 done |
|
66 |
|
67 lemma |
|
68 fixes a b::nat |
|
69 shows "(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2" |
|
70 apply(simp add: power2_sum) |
|
71 done |
|
72 |
|
73 lemma |
|
74 fixes a b c::"real" |
|
75 assumes eq: "a * c \<le> b * c" and ineq: "b < a" |
|
76 shows "c \<le> 0" |
|
77 proof - |
|
78 { |
|
79 assume "0 < c" |
|
80 then have "b * c < a * c" using ineq by(auto) |
|
81 then have "False" using eq by auto |
|
82 } then show "c \<le> 0" by (auto simp add: not_le[symmetric]) |
|
83 qed |
|
84 |
|
85 |
|
86 |
|
87 |
|
88 lemma "n > 1 \<Longrightarrow> \<not>(prime (2 * n))" |
|
89 by (metis One_nat_def Suc_leI less_Suc0 not_le numeral_eq_one_iff prime_product semiring_norm(85)) |
|
90 |
|
91 |
|
92 |
|
93 lemma |
|
94 fixes n::"nat" |
|
95 assumes a: "n > 1" |
|
96 and b: "\<not>(prime n)" |
|
97 shows "\<not>(prime ((2 ^ n) - 1))" |
|
98 using a b |
|
99 apply(induct n) |
|
100 apply(simp) |
|
101 apply(simp) |
|
102 |
|
103 |
|
104 |
|
105 end |
|