# HG changeset patch
# User wenzelm
# Date 957558614 -7200
# Node ID 0a5edcbe06958c08a8accd465f17977b9de1e19d
# Parent  abc0f3722aed526639c4955aa95843bce86baea0
adapted to new arithmetic simprocs;

diff -r abc0f3722aed -r 0a5edcbe0695 src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Fri May 05 22:29:02 2000 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Fri May 05 22:30:14 2000 +0200
@@ -30,7 +30,7 @@
 recdef fib less_than
  "fib 0 = 0"
  "fib 1 = 1"
- "fib (Suc (Suc x)) = fib x + fib(Suc x)";
+ "fib (Suc (Suc x)) = fib x + fib (Suc x)";
 
 lemma [simp]: "0 < fib (Suc n)";
   by (induct n rule: fib.induct) (simp+);
@@ -76,8 +76,8 @@
   fix n; 
   have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"; 
     by simp;
-  also; have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))"; 
-    by (simp add: gcd_add2);
+  also; have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))";
+    by (simp only: gcd_add2);
   also; have "... = gcd (fib (n + 1), fib (n + 1 + 1))";
     by (simp add: gcd_commute);
   also; assume "... = 1";
@@ -94,9 +94,9 @@
 qed;
 
 lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"; 
-proof (rule nat.exhaust [of m]);
+proof (cases m);
   assume "m = 0";
-  thus "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)"; by simp;
+  thus ?thesis; by simp;
 next;
   fix k; assume "m = Suc k"; 
   hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))";
@@ -123,7 +123,7 @@
   finally; show ?thesis; .;
 qed;
 
-lemma if_cases: 
+lemma if_cases:    (* FIXME move to HOL.thy (!?) *)
   "[| Q ==> P x; ~ Q ==> P y |] ==> P (if Q then x else y)"; by simp;
 
 lemma gcd_fib_mod: 
diff -r abc0f3722aed -r 0a5edcbe0695 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Fri May 05 22:29:02 2000 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Fri May 05 22:30:14 2000 +0200
@@ -23,7 +23,7 @@
 inductive "tiling A"
   intrs
     empty: "{} : tiling A"
-    Un:    "[| a : A;  t : tiling A;  a <= - t |]
+    Un:    "a : A ==> t : tiling A ==> a <= - t
               ==> a Un t : tiling A";
 
 
@@ -67,12 +67,12 @@
   by (simp add: below_def);
 
 lemma Sigma_Suc1:
-    "below (Suc n) <*> B = ({n} <*> B) Un (below n <*> B)";
+    "m = n + 1 ==> below m <*> B = ({n} <*> B) Un (below n <*> B)";
   by (simp add: below_def less_Suc_eq) blast;
 
 lemma Sigma_Suc2:
-    "A <*> below (Suc n) = (A <*> {n}) Un (A <*> (below n))";
-  by (simp add: below_def less_Suc_eq) blast;
+    "m = n + 2 ==> A <*> below m = (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)";
+  by (auto simp add: below_def) arith;
 
 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2;
 
@@ -81,10 +81,10 @@
 
 constdefs
   evnodd :: "(nat * nat) set => nat => (nat * nat) set"
-  "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}";
+  "evnodd A b == A Int {(i, j). (i + j) mod #2 = b}";
 
 lemma evnodd_iff:
-    "(i, j): evnodd A b = ((i, j): A  & (i + j) mod 2 = b)";
+    "(i, j): evnodd A b = ((i, j): A  & (i + j) mod #2 = b)";
   by (simp add: evnodd_def);
 
 lemma evnodd_subset: "evnodd A b <= A";
@@ -106,7 +106,7 @@
   by (simp add: evnodd_def);
 
 lemma evnodd_insert: "evnodd (insert (i, j) C) b =
-    (if (i + j) mod 2 = b
+    (if (i + j) mod #2 = b
       then insert (i, j) (evnodd C b) else evnodd C b)";
   by (simp add: evnodd_def) blast;
 
@@ -130,7 +130,8 @@
   fix n; assume hyp: "?P n";
   let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}";
 
-  have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc);
+  have "?B (Suc n) = ?a Un ?B n";
+    by (auto simp add: Sigma_Suc Un_assoc);
   also; have "... : ?T";
   proof (rule tiling.Un);
     have "{(i, 2 * n), (i, 2 * n + 1)} : domino";
@@ -163,7 +164,7 @@
 qed;
 
 lemma domino_singleton:
-  "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}";
+  "d : domino ==> b < 2 ==> EX i j. evnodd d b = {(i, j)}";
 proof -;
   assume b: "b < 2";
   assume "d : domino";
diff -r abc0f3722aed -r 0a5edcbe0695 src/HOL/Isar_examples/ROOT.ML
--- a/src/HOL/Isar_examples/ROOT.ML	Fri May 05 22:29:02 2000 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML	Fri May 05 22:30:14 2000 +0200
@@ -12,9 +12,9 @@
 time_use_thy "Group";
 time_use_thy "Summation";
 time_use_thy "KnasterTarski";
-(*TEMPORARILY DELETED time_use_thy "MutilatedCheckerboard";*)
+time_use_thy "MutilatedCheckerboard";
 with_path "../Induct" time_use_thy "MultisetOrder";
 with_path "../W0" time_use_thy "W_correct";
-(*TEMPORARILY DELETED with_path "../ex" time_use_thy "Fibonacci";*)
+with_path "../ex" time_use_thy "Fibonacci";
 time_use_thy "Puzzle";
 time_use_thy "NestedDatatype";
diff -r abc0f3722aed -r 0a5edcbe0695 src/HOL/Isar_examples/Summation.thy
--- a/src/HOL/Isar_examples/Summation.thy	Fri May 05 22:29:02 2000 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Fri May 05 22:30:14 2000 +0200
@@ -34,35 +34,20 @@
 *};
 
 consts
-  sum :: "[nat => nat, nat] => nat";
+  sum :: "(nat => nat) => nat => nat";
 
 primrec
   "sum f 0 = 0"
   "sum f (Suc n) = f n + sum f n";
 
 syntax
-  "_SUM" :: "[idt, nat, nat] => nat"
+  "_SUM" :: "idt => nat => nat => nat"
     ("SUM _ < _. _" [0, 0, 10] 10);
 translations
   "SUM i < k. b" == "sum (\\<lambda>i. b) k";
 
 
 subsection {* Summation laws *};
-(*<*)
-(* FIXME binary arithmetic does not yet work here *)
-
-syntax
-  "3" :: nat  ("3")
-  "4" :: nat  ("4")
-  "6" :: nat  ("6");
-
-translations
-  "3" == "Suc 2"
-  "4" == "Suc 3"
-  "6" == "Suc (Suc 4)";
-
-theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
-(*>*)
 
 text {*
  The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
@@ -139,31 +124,39 @@
   finally; show "?P (Suc n)"; by simp;
 qed;
 
+text {*
+ Subsequently we require some additional tweaking of Isabelle built-in
+ arithmetic simplifications, such as bringing in distributivity by
+ hand.
+*};
+
+lemmas distrib = add_mult_distrib add_mult_distrib2;
+
 theorem sum_of_squares:
-  "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
+  "#6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
   (is "?P n" is "?S n = _");
 proof (induct n);
   show "?P 0"; by simp;
 
   fix n;
-  have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
+  have "?S (n + 1) = ?S n + #6 * (n + 1)^2"; by (simp add: distrib);
   also; assume "?S n = n * (n + 1) * (2 * n + 1)";
-  also; have "... + 6 * (n + 1)^2 =
-    (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
+  also; have "... + #6 * (n + 1)^2 =
+    (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by (simp add: distrib);
   finally; show "?P (Suc n)"; by simp;
 qed;
 
 theorem sum_of_cubes:
-  "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
+  "#4 * (SUM i < n + 1. i^#3) = (n * (n + 1))^2"
   (is "?P n" is "?S n = _");
 proof (induct n);
-  show "?P 0"; by simp;
+  show "?P 0"; by (simp add: power_eq_if);
 
   fix n;
-  have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;
+  have "?S (n + 1) = ?S n + #4 * (n + 1)^#3"; by (simp add: power_eq_if distrib);
   also; assume "?S n = (n * (n + 1))^2";
-  also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2";
-    by simp;
+  also; have "... + #4 * (n + 1)^#3 = ((n + 1) * ((n + 1) + 1))^2";
+    by (simp add: power_eq_if distrib);
   finally; show "?P (Suc n)"; by simp;
 qed;