# HG changeset patch # User Christian Urban # Date 1418141861 0 # Node ID 79336e47e14d529235200904443b125e644a8cb0 # Parent 7545b1bc15147f316d5cf0c860b9e8c6f1ce45e3 added Pr theory diff -r 7545b1bc1514 -r 79336e47e14d Fahad/CodeSamples/SequenceComprehensions.scala --- a/Fahad/CodeSamples/SequenceComprehensions.scala Wed Nov 12 12:24:26 2014 +0000 +++ b/Fahad/CodeSamples/SequenceComprehensions.scala Tue Dec 09 16:17:41 2014 +0000 @@ -1,3 +1,17 @@ + +case class Twice(i: Int) { + def apply(x: Int, y: Int): Int = x * y + //def unapply(z: Int): Option[Int] = if (z % 2 == 0) Some(z/2) else None +} + +Twice(21) match { + case Twice(n) => println(n) +} + +Twice(21, 3) match { + case Twice(n) => println(n) +} + package Main @@ -26,4 +40,4 @@ i <- Iterator.range(0, 20); j <- Iterator.range(i + 1, 20) if i + j == 32 ) println("(" + i + ", " + j + ")") -} \ No newline at end of file +} diff -r 7545b1bc1514 -r 79336e47e14d thys/Pr.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/thys/Pr.thy Tue Dec 09 16:17:41 2014 +0000 @@ -0,0 +1,43 @@ +theory Pr +imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Real" +begin + +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 \ b * c" and ineq: "b < a" + shows "c \ 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 \ 0" by (auto simp add: not_le[symmetric]) +qed + + + + +lemma "n > 1 \ \(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: "\(prime n)" + shows "\(prime ((2 ^ n) - 1))" +using a b +apply(induct n) +apply(simp) +apply(simp) + + + +end \ No newline at end of file