updated tests to Isabelle2011-1;

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 \<Rightarrow> 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 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P (n + 1) \<Longrightarrow> P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> 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 \<Longrightarrow> 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 \<le> 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 \<le> 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 \<le> 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 \<le> 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 \<and> 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"