From 75a9e6fa64913e49e55557a6db1b50e8dbc7d25f Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Wed, 28 Sep 2011 09:35:01 +0000 Subject: updated tests to Isabelle2011-1; --- etc/isar/AHundredProofs.thy | 7 ++-- etc/isar/AHundredTheorems.thy | 10 ++--- etc/isar/AThousandTheorems.thy | 6 +-- etc/isar/BigErrors.thy | 4 +- etc/isar/ChosenLogic2.thy | 2 +- etc/isar/Fibonacci.thy | 65 +++++++++++++++++---------------- etc/isar/HighlightSize.thy | 2 +- etc/isar/IllegalEscape.thy | 2 +- etc/isar/MMMtests.thy | 6 +-- etc/isar/NamesInStrings.thy | 2 +- etc/isar/Parsing.thy | 26 +++++++------ etc/isar/ParsingBug1.thy | 2 +- etc/isar/Persistent.thy | 2 +- etc/isar/Trac280-subrev.thy | 3 +- etc/isar/Unicode.thy | 47 ++++++++++++------------ etc/isar/XEmacsSyntacticContextProb.thy | 2 +- etc/isar/bad2.thy | 2 +- etc/isar/trace_simp.thy | 4 +- 18 files changed, 96 insertions(+), 98 deletions(-) diff --git a/etc/isar/AHundredProofs.thy b/etc/isar/AHundredProofs.thy index 6f59f4e0..2687b306 100644 --- a/etc/isar/AHundredProofs.thy +++ b/etc/isar/AHundredProofs.thy @@ -1,7 +1,8 @@ -theory AHundredProofs imports Main +theory AHundredProofs +imports Main begin -ML {* val start = start_timing(); *} +ML {* val start = Timing.start () *} theorem and_comms1: "A & B --> B & A" proof @@ -1003,6 +1004,6 @@ proof qed qed -ML {* Output.warning (#message (end_timing start)); *} +ML {* warning (Timing.message (Timing.result start)) *} end diff --git a/etc/isar/AHundredTheorems.thy b/etc/isar/AHundredTheorems.thy index b26bf539..ab6ad8fd 100644 --- a/etc/isar/AHundredTheorems.thy +++ b/etc/isar/AHundredTheorems.thy @@ -1,9 +1,10 @@ -theory AHundredTheorems imports Main +theory AHundredTheorems +imports Main begin (* test this *) -ML {* val start = start_timing(); *} +ML {* val start = Timing.start () *} (* ELISP: -- (setq start (current-time)) -- *) lemma foo: "P --> P" by auto @@ -110,10 +111,7 @@ lemma foo100: "P --> P" by auto (* NB: this doesn't work because of comment aggregation *) (* ELISP: -- (message "Time taken: %f seconds" (time-to-seconds (time-since start))) -- *) -ML {* Output.warning (#message (end_timing start)); *} +ML {* warning (Timing.message (Timing.result start)) *} end - - - diff --git a/etc/isar/AThousandTheorems.thy b/etc/isar/AThousandTheorems.thy index 233dc1ed..6e565f90 100644 --- a/etc/isar/AThousandTheorems.thy +++ b/etc/isar/AThousandTheorems.thy @@ -1,7 +1,7 @@ theory AThousandTheorems imports Main begin -ML {* val start = start_timing(); *} +ML {* val start = Timing.start () *} (* ELISP: -- (setq start (current-time)) -- *) lemma foo: "P --> P" by auto @@ -1006,10 +1006,8 @@ lemma foo998: "P --> P" by auto lemma foo999: "P --> P" by auto lemma foo1000: "P --> P" by auto -ML {* Output.warning (#message (end_timing start)); *} +ML {* warning (Timing.message (Timing.result start)) *} (* ELISP: -- (message "Time taken: %f seconds" (time-to-seconds (time-since start))) -- *) end - - diff --git a/etc/isar/BigErrors.thy b/etc/isar/BigErrors.thy index ec6d5580..0dd41e42 100644 --- a/etc/isar/BigErrors.thy +++ b/etc/isar/BigErrors.thy @@ -6,12 +6,12 @@ begin consts foo :: 'a consts bar :: 'a -ML {* warning (cat_lines (List.tabulate (300,K "This is a big warning message"))); *} +ML {* warning (cat_lines (replicate 300 "This is a big warning message")); *} (* Attempt to get a big error with "error" fails, but we can use printing function (see FaultyErrors.thy) *) -ML {* Output.error_msg (cat_lines (List.tabulate (10000,K "This is a big error message"))); *} +ML {* Output.error_msg (cat_lines (replicate 10000 "This is a big error message")); *} (* Note about FaultyErrors: the above generates an error interactively but does *not* generate an error when diff --git a/etc/isar/ChosenLogic2.thy b/etc/isar/ChosenLogic2.thy index f2801a74..a7a6c934 100644 --- a/etc/isar/ChosenLogic2.thy +++ b/etc/isar/ChosenLogic2.thy @@ -1,6 +1,6 @@ (* -*- isabelle-chosen-logic: "HOL" -*- *) -theory ChosenLogic imports HOL +theory ChosenLogic2 imports HOL begin end diff --git a/etc/isar/Fibonacci.thy b/etc/isar/Fibonacci.thy index 382683f9..d26f3af3 100644 --- a/etc/isar/Fibonacci.thy +++ b/etc/isar/Fibonacci.thy @@ -1,6 +1,6 @@ -(* Copied from Isabelle2009/src/HOL/Isar_examples/ *) +(* Copied from Isabelle2011-1/src/HOL/Isar_examples/ *) -(* Title: HOL/Isar_examples/Fibonacci.thy +(* Title: HOL/Isar_Examples/Fibonacci.thy Author: Gertrud Bauer Copyright 1999 Technische Universitaet Muenchen @@ -17,31 +17,32 @@ Fibonacci numbers: proofs of laws taken from header {* Fib and Gcd commute *} theory Fibonacci -imports Primes +imports "~~/src/HOL/Number_Theory/Primes" begin -text_raw {* - \footnote{Isar version by Gertrud Bauer. Original tactic script by - Larry Paulson. A few proofs of laws taken from - \cite{Concrete-Math}.} -*} +text_raw {* \footnote{Isar version by Gertrud Bauer. Original tactic + script by Larry Paulson. A few proofs of laws taken from + \cite{Concrete-Math}.} *} + + +declare One_nat_def [simp] subsection {* Fibonacci numbers *} fun fib :: "nat \ nat" where "fib 0 = 0" - | "fib (Suc 0) = 1" - | "fib (Suc (Suc x)) = fib x + fib (Suc x)" +| "fib (Suc 0) = 1" +| "fib (Suc (Suc x)) = fib x + fib (Suc x)" -lemma [simp]: "0 < fib (Suc n)" +lemma [simp]: "fib (Suc n) > 0" by (induct n rule: fib.induct) simp_all text {* Alternative induction rule. *} theorem fib_induct: - "P 0 \ P 1 \ (\n. P (n + 1) \ P n \ P (n + 2)) \ P (n::nat)" + "P 0 ==> P 1 ==> (!!n. P (n + 1) ==> P n ==> P (n + 2)) ==> P (n::nat)" by (induct rule: fib.induct) simp_all @@ -78,20 +79,21 @@ proof (induct n rule: fib_induct) fix n have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)" by simp + also have "... = fib (n + 2) + fib (n + 1)" by simp also have "gcd (fib (n + 2)) ... = gcd (fib (n + 2)) (fib (n + 1))" - by (simp only: gcd_add2') + by (rule gcd_add2_nat) also have "... = gcd (fib (n + 1)) (fib (n + 1 + 1))" - by (simp add: gcd_commute) + by (simp add: gcd_commute_nat) also assume "... = 1" finally show "?P (n + 2)" . qed -lemma gcd_mult_add: "0 < n \ gcd (n * k + m) n = gcd m n" +lemma gcd_mult_add: "(0::nat) < n ==> gcd (n * k + m) n = gcd m n" proof - assume "0 < n" then have "gcd (n * k + m) n = gcd n (m mod n)" - by (simp add: gcd_non_0 add_commute) - also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0) + by (simp add: gcd_non_0_nat add_commute) + also from `0 < n` have "... = gcd m n" by (simp add: gcd_non_0_nat) finally show ?thesis . qed @@ -102,26 +104,26 @@ proof (cases m) next case (Suc k) then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))" - by (simp add: gcd_commute) + by (simp add: gcd_commute_nat) also have "fib (n + k + 1) - = fib (k + 1) * fib (n + 1) + fib k * fib n" + = fib (k + 1) * fib (n + 1) + fib k * fib n" by (rule fib_add) also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))" by (simp add: gcd_mult_add) also have "... = gcd (fib n) (fib (k + 1))" - by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel) + by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel_nat) also have "... = gcd (fib m) (fib n)" - using Suc by (simp add: gcd_commute) + using Suc by (simp add: gcd_commute_nat) finally show ?thesis . qed lemma gcd_fib_diff: - assumes "m \ n" + assumes "m <= n" shows "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" proof - have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))" by (simp add: gcd_fib_add) - also from `m \ n` have "n - m + m = n" by simp + also from `m <= n` have "n - m + m = n" by simp finally show ?thesis . qed @@ -130,7 +132,7 @@ lemma gcd_fib_mod: shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" proof (induct n rule: nat_less_induct) case (1 n) note hyp = this - show ?case + show ?case proof - have "n mod m = (if n < m then n else (n - m) mod m)" by (rule mod_if) @@ -138,29 +140,28 @@ proof (induct n rule: nat_less_induct) proof (cases "n < m") case True then show ?thesis by simp next - case False then have "m \ n" by simp + case False then have "m <= n" by simp from `0 < m` and False have "n - m < n" by simp with hyp have "gcd (fib m) (fib ((n - m) mod m)) - = gcd (fib m) (fib (n - m))" by simp + = gcd (fib m) (fib (n - m))" by simp also have "... = gcd (fib m) (fib n)" - using `m \ n` by (rule gcd_fib_diff) + using `m <= n` by (rule gcd_fib_diff) finally have "gcd (fib m) (fib ((n - m) mod m)) = - gcd (fib m) (fib n)" . + gcd (fib m) (fib n)" . with False show ?thesis by simp qed finally show ?thesis . qed qed - theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n") -proof (induct m n rule: gcd_induct) +proof (induct m n rule: gcd_nat_induct) fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp fix n :: nat assume n: "0 < n" - then have "gcd m n = gcd n (m mod n)" by (rule gcd_non_0) + then have "gcd m n = gcd n (m mod n)" by (simp add: gcd_non_0_nat) also assume hyp: "fib ... = gcd (fib n) (fib (m mod n))" also from n have "... = gcd (fib n) (fib m)" by (rule gcd_fib_mod) - also have "... = gcd (fib m) (fib n)" by (rule gcd_commute) + also have "... = gcd (fib m) (fib n)" by (rule gcd_commute_nat) finally show "fib (gcd m n) = gcd (fib m) (fib n)" . qed diff --git a/etc/isar/HighlightSize.thy b/etc/isar/HighlightSize.thy index 386db167..7c68b74f 100644 --- a/etc/isar/HighlightSize.thy +++ b/etc/isar/HighlightSize.thy @@ -6,7 +6,7 @@ begin lemmas rules = sym refl trans sym refl trans sym refl trans sym refl trans sym refl trans ML_command {* Pretty.writeln (Pretty.markup Markup.hilite - [ProofContext.pretty_fact @{context} ("foo", @{thms rules(1-14)})]) *} + [Proof_Context.pretty_fact @{context} ("foo", @{thms rules(1-14)})]) *} end diff --git a/etc/isar/IllegalEscape.thy b/etc/isar/IllegalEscape.thy index c1d4fde5..3478830b 100644 --- a/etc/isar/IllegalEscape.thy +++ b/etc/isar/IllegalEscape.thy @@ -3,5 +3,5 @@ theory IllegalEscape imports Main begin lemma X: "a=b ==> b=a" by simp -- "Text with \illegal escape sequence" - + oops end diff --git a/etc/isar/MMMtests.thy b/etc/isar/MMMtests.thy index 76f84993..994a8ee0 100644 --- a/etc/isar/MMMtests.thy +++ b/etc/isar/MMMtests.thy @@ -12,7 +12,7 @@ text {* subsection {* and this one. *} -ML_setup {* +ML {* (* Whereas this region is edited in SML mode. For that to work, you need to have installed SML mode in your Emacs, otherwise MMM mode won't bother. See Stefan Monnier's page at @@ -22,11 +22,11 @@ ML_setup {* | foo (x::xs) = x * foo xs *} -ML {* (* and this one *) *} +ML_val {* (* and this one *) *} ML_command {* (* and this one *) *} -typed_print_translation {* (* and even this one *) *} +print_translation {* [] (* and even this one *) *} text {* You can enter the text for a MMM region conveniently diff --git a/etc/isar/NamesInStrings.thy b/etc/isar/NamesInStrings.thy index 3d56e8c8..366b9a2a 100644 --- a/etc/isar/NamesInStrings.thy +++ b/etc/isar/NamesInStrings.thy @@ -1,4 +1,4 @@ -theory "Names In Strings" = Main: (* NB: must also check case without quotes! *) +theory "Names In Strings" imports Main begin (* NB: must also check case without quotes! *) lemma foo: "B --> B" by auto diff --git a/etc/isar/Parsing.thy b/etc/isar/Parsing.thy index 60d47e3d..98e8819e 100644 --- a/etc/isar/Parsing.thy +++ b/etc/isar/Parsing.thy @@ -3,7 +3,7 @@ (* First, start with successive comments before a real command *) -theory Parsing = Main: +theory Parsing imports Main begin (* Then a comment *after* a command. Also one which mentions the names of commands, such as theory or theorem or proof itself, @@ -38,12 +38,12 @@ text {* nesting (* may be the other way around *) *} theorem and_comms: "A & B --> B & A" proof assume "A & B" (* it's "important" that we test "strings" I guess *) - thus "B & A" - proof - assume A B (* blah boo bah *) - show ?thesis (* bah boo bah *) - .. - qed + then show "B & A" + proof + assume B A (* blah boo bah *) + then show ?thesis (* bah boo bah *) + .. + qed qed (* Another thing: nesting with { and } can be tricky. *) @@ -51,12 +51,14 @@ qed theorem and_comms_again: "A & B --> B & A" proof assume "A & B" - thus "B & A" - proof { - assume A B - show ?thesis + then show "B & A" + proof + { + assume B A + then show ?thesis .. - } qed + } + qed qed (* Now the end of file is coming up. Funny things happen diff --git a/etc/isar/ParsingBug1.thy b/etc/isar/ParsingBug1.thy index e1a783ab..e56a5ae9 100644 --- a/etc/isar/ParsingBug1.thy +++ b/etc/isar/ParsingBug1.thy @@ -6,7 +6,7 @@ *) -theory ParsingBug1 = Main: +theory ParsingBug1 imports Main begin theorem "P" proof - diff --git a/etc/isar/Persistent.thy b/etc/isar/Persistent.thy index f9258ce5..8a042886 100644 --- a/etc/isar/Persistent.thy +++ b/etc/isar/Persistent.thy @@ -25,7 +25,7 @@ Tests: *) -theory Persistent = Main: +theory Persistent imports Main begin theorem and_comms: "A & B --> B & A" proof diff --git a/etc/isar/Trac280-subrev.thy b/etc/isar/Trac280-subrev.thy index 2c5984c1..ff392ec3 100644 --- a/etc/isar/Trac280-subrev.thy +++ b/etc/isar/Trac280-subrev.thy @@ -1,4 +1,4 @@ -theory Test imports Main begin +theory "Trac280-subrev" imports Main begin lemma assumes asm: "P\<^isub>i \ Q\<^isub>i" @@ -12,4 +12,3 @@ qed end - diff --git a/etc/isar/Unicode.thy b/etc/isar/Unicode.thy index 0305091b..95140e6a 100644 --- a/etc/isar/Unicode.thy +++ b/etc/isar/Unicode.thy @@ -40,31 +40,30 @@ thm alef_bet.induct text {* Interpreting Hebrew letters as numbers. *} -consts - mispar :: "alef_bet => nat" -primrec +primrec mispar :: "alef_bet => nat" +where "mispar א = 1" - "mispar ב = 2" - "mispar ג = 3" - "mispar ד = 4" - "mispar ה = 5" - "mispar ו = 6" - "mispar ז = 7" - "mispar ח = 8" - "mispar ט = 9" - "mispar י = 10" - "mispar כ = 20" - "mispar ל = 30" - "mispar מ = 40" - "mispar נ = 50" - "mispar ס = 60" - "mispar ע = 70" - "mispar פ = 80" - "mispar צ = 90" - "mispar ק = 100" - "mispar ר = 200" - "mispar ש = 300" - "mispar ת = 400" +| "mispar ב = 2" +| "mispar ג = 3" +| "mispar ד = 4" +| "mispar ה = 5" +| "mispar ו = 6" +| "mispar ז = 7" +| "mispar ח = 8" +| "mispar ט = 9" +| "mispar י = 10" +| "mispar כ = 20" +| "mispar ל = 30" +| "mispar מ = 40" +| "mispar נ = 50" +| "mispar ס = 60" +| "mispar ע = 70" +| "mispar פ = 80" +| "mispar צ = 90" +| "mispar ק = 100" +| "mispar ר = 200" +| "mispar ש = 300" +| "mispar ת = 400" thm mispar.simps diff --git a/etc/isar/XEmacsSyntacticContextProb.thy b/etc/isar/XEmacsSyntacticContextProb.thy index d910a6ba..ef295a93 100644 --- a/etc/isar/XEmacsSyntacticContextProb.thy +++ b/etc/isar/XEmacsSyntacticContextProb.thy @@ -10,7 +10,7 @@ Workaround added Fri Aug 10 13:55:28 BST 2001 *) -theory XEmacsSyntacticContextProb = Main: +theory XEmacsSyntacticContextProb imports Main begin term " (f x)" diff --git a/etc/isar/bad2.thy b/etc/isar/bad2.thy index 11fecd77..7a12fdb8 100644 --- a/etc/isar/bad2.thy +++ b/etc/isar/bad2.thy @@ -1 +1 @@ -theory A = unknown: +theory bad2 imports unknown begin diff --git a/etc/isar/trace_simp.thy b/etc/isar/trace_simp.thy index 44f6e5af..de651e5b 100644 --- a/etc/isar/trace_simp.thy +++ b/etc/isar/trace_simp.thy @@ -6,8 +6,8 @@ text {* this produces massive amount of simplifier trace, but terminates eventually: *} -declare [[trace_simp]] -ML {* reset quick_and_dirty *} +declare [[simp_trace]] +ML {* quick_and_dirty := false *} datatype ord = Zero | Succ ord | Limit "nat => ord" -- cgit v1.2.3