# 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 (\\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;