1 theory Pr

     2 imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Real"

     3 begin

     4 

     5 lemma 

     6   fixes a b::nat

     7   shows "(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2"

     8 apply(simp add: power2_sum)

     9 done

    10 

    11 lemma

    12   fixes a b c::"real"

    13   assumes eq: "a * c \<le> b * c" and ineq: "b < a"

    14   shows "c \<le> 0"

    15 proof -

    16   {

    17     assume  "0 < c" 

    18     then have "b * c < a * c" using ineq by(auto)

    19     then have "False" using eq by auto

    20   } then show "c \<le> 0" by (auto simp add: not_le[symmetric]) 

    21 qed

    22     

    23 

    24 

    25 

    26 lemma "n > 1 \<Longrightarrow> \<not>(prime (2 * n))"

    27 by (metis One_nat_def Suc_leI less_Suc0 not_le numeral_eq_one_iff prime_product semiring_norm(85))

    28 

    29 

    30 

    31 lemma 

    32  fixes n::"nat"

    33  assumes a: "n > 1"

    34     and  b: "\<not>(prime n)"

    35  shows "\<not>(prime ((2 ^ n) - 1))"   

    36 using a b

    37 apply(induct n)

    38 apply(simp)

    39 apply(simp)

    40 

    41 

    42 

    43 end