# HG changeset patch
# User wenzelm
# Date 1393003391 -3600
# Node ID eb07b0acbebc517d43dd67b6db1d2edb22456eaa
# Parent  af028f35af60ca6c7e8192c2c141abbf23fe0b3c
more symbols;

diff -r af028f35af60 -r eb07b0acbebc src/HOL/Isar_Examples/Basic_Logic.thy
--- a/src/HOL/Isar_Examples/Basic_Logic.thy	Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Fri Feb 21 18:23:11 2014 +0100
@@ -291,7 +291,7 @@
   cases actually coincide.  Consequently the proof may be rephrased as
   follows. *}
 
-lemma "P \<or> P --> P"
+lemma "P \<or> P \<longrightarrow> P"
 proof
   assume "P \<or> P"
   then show P
@@ -307,7 +307,7 @@
   are implicitly performed when concluding the single rule step of the
   double-dot proof as follows. *}
 
-lemma "P \<or> P --> P"
+lemma "P \<or> P \<longrightarrow> P"
 proof
   assume "P \<or> P"
   then show P ..
diff -r af028f35af60 -r eb07b0acbebc src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Fri Feb 21 18:23:11 2014 +0100
@@ -150,7 +150,7 @@
       with hyp have "gcd (fib m) (fib ((n - m) mod m))
           = gcd (fib m) (fib (n - m))" by simp
       also have "\<dots> = gcd (fib m) (fib n)"
-        using `m <= n` by (rule gcd_fib_diff)
+        using `m \<le> n` by (rule gcd_fib_diff)
       finally have "gcd (fib m) (fib ((n - m) mod m)) =
           gcd (fib m) (fib n)" .
       with False show ?thesis by simp
diff -r af028f35af60 -r eb07b0acbebc src/HOL/Isar_Examples/Group.thy
--- a/src/HOL/Isar_Examples/Group.thy	Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Group.thy	Fri Feb 21 18:23:11 2014 +0100
@@ -27,19 +27,19 @@
 proof -
   have "x * inverse x = 1 * (x * inverse x)"
     by (simp only: group_left_one)
-  also have "... = 1 * x * inverse x"
+  also have "\<dots> = 1 * x * inverse x"
     by (simp only: group_assoc)
-  also have "... = inverse (inverse x) * inverse x * x * inverse x"
+  also have "\<dots> = inverse (inverse x) * inverse x * x * inverse x"
     by (simp only: group_left_inverse)
-  also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
+  also have "\<dots> = inverse (inverse x) * (inverse x * x) * inverse x"
     by (simp only: group_assoc)
-  also have "... = inverse (inverse x) * 1 * inverse x"
+  also have "\<dots> = inverse (inverse x) * 1 * inverse x"
     by (simp only: group_left_inverse)
-  also have "... = inverse (inverse x) * (1 * inverse x)"
+  also have "\<dots> = inverse (inverse x) * (1 * inverse x)"
     by (simp only: group_assoc)
-  also have "... = inverse (inverse x) * inverse x"
+  also have "\<dots> = inverse (inverse x) * inverse x"
     by (simp only: group_left_one)
-  also have "... = 1"
+  also have "\<dots> = 1"
     by (simp only: group_left_inverse)
   finally show ?thesis .
 qed
@@ -52,11 +52,11 @@
 proof -
   have "x * 1 = x * (inverse x * x)"
     by (simp only: group_left_inverse)
-  also have "... = x * inverse x * x"
+  also have "\<dots> = x * inverse x * x"
     by (simp only: group_assoc)
-  also have "... = 1 * x"
+  also have "\<dots> = 1 * x"
     by (simp only: group_right_inverse)
-  also have "... = x"
+  also have "\<dots> = x"
     by (simp only: group_left_one)
   finally show ?thesis .
 qed
@@ -92,25 +92,25 @@
   note calculation = this
     -- {* first calculational step: init calculation register *}
 
-  have "... = x * inverse x * x"
+  have "\<dots> = x * inverse x * x"
     by (simp only: group_assoc)
 
   note calculation = trans [OF calculation this]
     -- {* general calculational step: compose with transitivity rule *}
 
-  have "... = 1 * x"
+  have "\<dots> = 1 * x"
     by (simp only: group_right_inverse)
 
   note calculation = trans [OF calculation this]
     -- {* general calculational step: compose with transitivity rule *}
 
-  have "... = x"
+  have "\<dots> = x"
     by (simp only: group_left_one)
 
   note calculation = trans [OF calculation this]
-    -- {* final calculational step: compose with transitivity rule ... *}
+    -- {* final calculational step: compose with transitivity rule \dots *}
   from calculation
-    -- {* ... and pick up the final result *}
+    -- {* \dots\ and pick up the final result *}
 
   show ?thesis .
 qed
@@ -168,13 +168,13 @@
 proof -
   have "1 = x * inverse x"
     by (simp only: group_right_inverse)
-  also have "... = (e * x) * inverse x"
+  also have "\<dots> = (e * x) * inverse x"
     by (simp only: eq)
-  also have "... = e * (x * inverse x)"
+  also have "\<dots> = e * (x * inverse x)"
     by (simp only: group_assoc)
-  also have "... = e * 1"
+  also have "\<dots> = e * 1"
     by (simp only: group_right_inverse)
-  also have "... = e"
+  also have "\<dots> = e"
     by (simp only: group_right_one)
   finally show ?thesis .
 qed
@@ -187,13 +187,13 @@
 proof -
   have "inverse x = 1 * inverse x"
     by (simp only: group_left_one)
-  also have "... = (x' * x) * inverse x"
+  also have "\<dots> = (x' * x) * inverse x"
     by (simp only: eq)
-  also have "... = x' * (x * inverse x)"
+  also have "\<dots> = x' * (x * inverse x)"
     by (simp only: group_assoc)
-  also have "... = x' * 1"
+  also have "\<dots> = x' * 1"
     by (simp only: group_right_inverse)
-  also have "... = x'"
+  also have "\<dots> = x'"
     by (simp only: group_right_one)
   finally show ?thesis .
 qed
@@ -207,11 +207,11 @@
     have "(inverse y * inverse x) * (x * y) =
         (inverse y * (inverse x * x)) * y"
       by (simp only: group_assoc)
-    also have "... = (inverse y * 1) * y"
+    also have "\<dots> = (inverse y * 1) * y"
       by (simp only: group_left_inverse)
-    also have "... = inverse y * y"
+    also have "\<dots> = inverse y * y"
       by (simp only: group_right_one)
-    also have "... = 1"
+    also have "\<dots> = 1"
       by (simp only: group_left_inverse)
     finally show ?thesis .
   qed
@@ -229,15 +229,15 @@
 proof -
   have "x = x * 1"
     by (simp only: group_right_one)
-  also have "... = x * (inverse y * y)"
+  also have "\<dots> = x * (inverse y * y)"
     by (simp only: group_left_inverse)
-  also have "... = x * (inverse x * y)"
+  also have "\<dots> = x * (inverse x * y)"
     by (simp only: eq)
-  also have "... = (x * inverse x) * y"
+  also have "\<dots> = (x * inverse x) * y"
     by (simp only: group_assoc)
-  also have "... = 1 * y"
+  also have "\<dots> = 1 * y"
     by (simp only: group_right_inverse)
-  also have "... = y"
+  also have "\<dots> = y"
     by (simp only: group_left_one)
   finally show ?thesis .
 qed
diff -r af028f35af60 -r eb07b0acbebc src/HOL/Isar_Examples/Group_Context.thy
--- a/src/HOL/Isar_Examples/Group_Context.thy	Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Group_Context.thy	Fri Feb 21 18:23:11 2014 +0100
@@ -13,7 +13,7 @@
 context
   fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
     and one :: "'a"
-    and inverse :: "'a => 'a"
+    and inverse :: "'a \<Rightarrow> 'a"
   assumes assoc: "(x ** y) ** z = x ** (y ** z)"
     and left_one: "one ** x = x"
     and left_inverse: "inverse x ** x = one"
diff -r af028f35af60 -r eb07b0acbebc src/HOL/Isar_Examples/Group_Notepad.thy
--- a/src/HOL/Isar_Examples/Group_Notepad.thy	Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Group_Notepad.thy	Fri Feb 21 18:23:11 2014 +0100
@@ -14,7 +14,7 @@
 
   fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
     and one :: "'a"
-    and inverse :: "'a => 'a"
+    and inverse :: "'a \<Rightarrow> 'a"
   assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
     and left_one: "\<And>x. one ** x = x"
     and left_inverse: "\<And>x. inverse x ** x = one"
diff -r af028f35af60 -r eb07b0acbebc src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Fri Feb 21 18:23:11 2014 +0100
@@ -22,41 +22,39 @@
 type_synonym 'a assn = "'a set"
 
 datatype 'a com =
-    Basic "'a => 'a"
+    Basic "'a \<Rightarrow> 'a"
   | Seq "'a com" "'a com"    ("(_;/ _)" [60, 61] 60)
   | Cond "'a bexp" "'a com" "'a com"
   | While "'a bexp" "'a assn" "'a com"
 
 abbreviation Skip  ("SKIP")
-  where "SKIP == Basic id"
-
-type_synonym 'a sem = "'a => 'a => bool"
+  where "SKIP \<equiv> Basic id"
 
-primrec iter :: "nat => 'a bexp => 'a sem => 'a sem"
-where
-  "iter 0 b S s s' = (s ~: b & s = s')"
-| "iter (Suc n) b S s s' = (s : b & (EX s''. S s s'' & iter n b S s'' s'))"
+type_synonym 'a sem = "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
-primrec Sem :: "'a com => 'a sem"
+primrec iter :: "nat \<Rightarrow> 'a bexp \<Rightarrow> 'a sem \<Rightarrow> 'a sem"
 where
-  "Sem (Basic f) s s' = (s' = f s)"
-| "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')"
-| "Sem (Cond b c1 c2) s s' =
-    (if s : b then Sem c1 s s' else Sem c2 s s')"
-| "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')"
+  "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
+| "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
 
-definition Valid :: "'a bexp => 'a com => 'a bexp => bool"
-    ("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
-  where "|- P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' --> s : P --> s' : Q)"
+primrec Sem :: "'a com \<Rightarrow> 'a sem"
+where
+  "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
+| "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
+| "Sem (Cond b c1 c2) s s' \<longleftrightarrow>
+    (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
+| "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
 
-notation (xsymbols) Valid  ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+    ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+  where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
 
 lemma ValidI [intro?]:
-    "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"
+    "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
   by (simp add: Valid_def)
 
 lemma ValidD [dest?]:
-    "|- P c Q ==> Sem c s s' ==> s : P ==> s' : Q"
+    "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
   by (simp add: Valid_def)
 
 
@@ -71,12 +69,13 @@
   to the state space.  This subsumes the common rules of \name{skip}
   and \name{assign}, as formulated in \S\ref{sec:hoare-isar}. *}
 
-theorem basic: "|- {s. f s : P} (Basic f) P"
+theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P"
 proof
-  fix s s' assume s: "s : {s. f s : P}"
+  fix s s'
+  assume s: "s \<in> {s. f s \<in> P}"
   assume "Sem (Basic f) s s'"
   then have "s' = f s" by simp
-  with s show "s' : P" by simp
+  with s show "s' \<in> P" by simp
 qed
 
 text {*
@@ -84,26 +83,27 @@
  established in a straight forward manner as follows.
 *}
 
-theorem seq: "|- P c1 Q ==> |- Q c2 R ==> |- P (c1; c2) R"
+theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R"
 proof
-  assume cmd1: "|- P c1 Q" and cmd2: "|- Q c2 R"
-  fix s s' assume s: "s : P"
+  assume cmd1: "\<turnstile> P c1 Q" and cmd2: "\<turnstile> Q c2 R"
+  fix s s'
+  assume s: "s \<in> P"
   assume "Sem (c1; c2) s s'"
   then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'"
     by auto
-  from cmd1 sem1 s have "s'' : Q" ..
-  with cmd2 sem2 show "s' : R" ..
+  from cmd1 sem1 s have "s'' \<in> Q" ..
+  with cmd2 sem2 show "s' \<in> R" ..
 qed
 
-theorem conseq: "P' <= P ==> |- P c Q ==> Q <= Q' ==> |- P' c Q'"
+theorem conseq: "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P' c Q'"
 proof
-  assume P'P: "P' <= P" and QQ': "Q <= Q'"
-  assume cmd: "|- P c Q"
+  assume P'P: "P' \<subseteq> P" and QQ': "Q \<subseteq> Q'"
+  assume cmd: "\<turnstile> P c Q"
   fix s s' :: 'a
   assume sem: "Sem c s s'"
-  assume "s : P'" with P'P have "s : P" ..
-  with cmd sem have "s' : Q" ..
-  with QQ' show "s' : Q'" ..
+  assume "s : P'" with P'P have "s \<in> P" ..
+  with cmd sem have "s' \<in> Q" ..
+  with QQ' show "s' \<in> Q'" ..
 qed
 
 text {* The rule for conditional commands is directly reflected by the
@@ -111,26 +111,27 @@
   which cases apply. *}
 
 theorem cond:
-  assumes case_b: "|- (P Int b) c1 Q"
-    and case_nb: "|- (P Int -b) c2 Q"
-  shows "|- P (Cond b c1 c2) Q"
+  assumes case_b: "\<turnstile> (P \<inter> b) c1 Q"
+    and case_nb: "\<turnstile> (P \<inter> -b) c2 Q"
+  shows "\<turnstile> P (Cond b c1 c2) Q"
 proof
-  fix s s' assume s: "s : P"
+  fix s s'
+  assume s: "s \<in> P"
   assume sem: "Sem (Cond b c1 c2) s s'"
-  show "s' : Q"
+  show "s' \<in> Q"
   proof cases
-    assume b: "s : b"
+    assume b: "s \<in> b"
     from case_b show ?thesis
     proof
       from sem b show "Sem c1 s s'" by simp
-      from s b show "s : P Int b" by simp
+      from s b show "s \<in> P \<inter> b" by simp
     qed
   next
-    assume nb: "s ~: b"
+    assume nb: "s \<notin> b"
     from case_nb show ?thesis
     proof
       from sem nb show "Sem c2 s s'" by simp
-      from s nb show "s : P Int -b" by simp
+      from s nb show "s : P \<inter> -b" by simp
     qed
   qed
 qed
@@ -143,22 +144,22 @@
   of the semantics of \texttt{WHILE}. *}
 
 theorem while:
-  assumes body: "|- (P Int b) c P"
-  shows "|- P (While b X c) (P Int -b)"
+  assumes body: "\<turnstile> (P \<inter> b) c P"
+  shows "\<turnstile> P (While b X c) (P \<inter> -b)"
 proof
-  fix s s' assume s: "s : P"
+  fix s s' assume s: "s \<in> P"
   assume "Sem (While b X c) s s'"
   then obtain n where "iter n b (Sem c) s s'" by auto
-  from this and s show "s' : P Int -b"
+  from this and s show "s' \<in> P \<inter> -b"
   proof (induct n arbitrary: s)
     case 0
     then show ?case by auto
   next
     case (Suc n)
-    then obtain s'' where b: "s : b" and sem: "Sem c s s''"
+    then obtain s'' where b: "s \<in> b" and sem: "Sem c s s''"
       and iter: "iter n b (Sem c) s'' s'" by auto
-    from Suc and b have "s : P Int b" by simp
-    with body sem have "s'' : P" ..
+    from Suc and b have "s \<in> P \<inter> b" by simp
+    with body sem have "s'' \<in> P" ..
     with iter show ?case by (rule Suc)
   qed
 qed
@@ -188,29 +189,26 @@
   @{ML Syntax_Trans.quote_tr'},). *}
 
 syntax
-  "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)" [0] 1000)
-  "_antiquote"   :: "('a => 'b) => 'b"       ("\<acute>_" [1000] 1000)
+  "_quote"       :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"       ("(.'(_').)" [0] 1000)
+  "_antiquote"   :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"       ("\<acute>_" [1000] 1000)
   "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
         ("_[_'/\<acute>_]" [1000] 999)
-  "_Assert"      :: "'a => 'a set"           ("(.{_}.)" [0] 1000)
-  "_Assign"      :: "idt => 'b => 'a com"    ("(\<acute>_ :=/ _)" [70, 65] 61)
-  "_Cond"        :: "'a bexp => 'a com => 'a com => 'a com"
+  "_Assert"      :: "'a \<Rightarrow> 'a set"           ("(\<lbrace>_\<rbrace>)" [0] 1000)
+  "_Assign"      :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"    ("(\<acute>_ :=/ _)" [70, 65] 61)
+  "_Cond"        :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
         ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
-  "_While_inv"   :: "'a bexp => 'a assn => 'a com => 'a com"
+  "_While_inv"   :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"
         ("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)
-  "_While"       :: "'a bexp => 'a com => 'a com"
+  "_While"       :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"
         ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)
 
-syntax (xsymbols)
-  "_Assert"      :: "'a => 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
-
 translations
-  ".{b}."                   => "CONST Collect .(b)."
-  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."
-  "\<acute>x := a"                 => "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
-  "IF b THEN c1 ELSE c2 FI" => "CONST Cond .{b}. c1 c2"
-  "WHILE b INV i DO c OD"   => "CONST While .{b}. i c"
-  "WHILE b DO c OD"         == "WHILE b INV CONST undefined DO c OD"
+  "\<lbrace>b\<rbrace>"                     \<rightharpoonup> "CONST Collect .(b)."
+  "B [a/\<acute>x]"                \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
+  "\<acute>x := a"                 \<rightharpoonup> "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
+  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
+  "WHILE b INV i DO c OD"   \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
+  "WHILE b DO c OD"         \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
 
 parse_translation {*
   let
@@ -259,28 +257,28 @@
   calculational proofs, with the inclusion expressed in terms of sets
   or predicates.  Reversed order is supported as well. *}
 
-lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q"
+lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q"
   by (unfold Valid_def) blast
-lemma [trans] : "P' <= P ==> |- P c Q ==> |- P' c Q"
+lemma [trans] : "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P' c Q"
   by (unfold Valid_def) blast
 
-lemma [trans]: "Q <= Q' ==> |- P c Q ==> |- P c Q'"
+lemma [trans]: "Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P c Q'"
   by (unfold Valid_def) blast
-lemma [trans]: "|- P c Q ==> Q <= Q' ==> |- P c Q'"
+lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q'"
   by (unfold Valid_def) blast
 
 lemma [trans]:
-    "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"
+    "\<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> (\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
   by (simp add: Valid_def)
 lemma [trans]:
-    "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"
+    "(\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
   by (simp add: Valid_def)
 
 lemma [trans]:
-    "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."
+    "\<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> (\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
   by (simp add: Valid_def)
 lemma [trans]:
-    "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."
+    "(\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
   by (simp add: Valid_def)
 
 
@@ -289,13 +287,13 @@
   instances for any number of basic assignments, without producing
   additional verification conditions.} *}
 
-lemma skip [intro?]: "|- P SKIP P"
+lemma skip [intro?]: "\<turnstile> P SKIP P"
 proof -
-  have "|- {s. id s : P} SKIP P" by (rule basic)
+  have "\<turnstile> {s. id s \<in> P} SKIP P" by (rule basic)
   then show ?thesis by simp
 qed
 
-lemma assign: "|- P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
+lemma assign: "\<turnstile> P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
   by (rule basic)
 
 text {* Note that above formulation of assignment corresponds to our
@@ -315,7 +313,7 @@
 
 lemmas [trans, intro?] = seq
 
-lemma seq_assoc [simp]: "( |- P c1;(c2;c3) Q) = ( |- P (c1;c2);c3 Q)"
+lemma seq_assoc [simp]: "\<turnstile> P c1;(c2;c3) Q \<longleftrightarrow> \<turnstile> P (c1;c2);c3 Q"
   by (auto simp add: Valid_def)
 
 text {* Conditional statements. *}
@@ -323,30 +321,30 @@
 lemmas [trans, intro?] = cond
 
 lemma [trans, intro?]:
-  "|- .{\<acute>P & \<acute>b}. c1 Q
-      ==> |- .{\<acute>P & ~ \<acute>b}. c2 Q
-      ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
+  "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c1 Q
+      \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace> c2 Q
+      \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> IF \<acute>b THEN c1 ELSE c2 FI Q"
     by (rule cond) (simp_all add: Valid_def)
 
 text {* While statements --- with optional invariant. *}
 
 lemma [intro?]:
-    "|- (P Int b) c P ==> |- P (While b P c) (P Int -b)"
+    "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
   by (rule while)
 
 lemma [intro?]:
-    "|- (P Int b) c P ==> |- P (While b undefined c) (P Int -b)"
+    "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
   by (rule while)
 
 
 lemma [intro?]:
-  "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
-    ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."
+  "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
+    \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b INV \<lbrace>\<acute>P\<rbrace> DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
   by (simp add: while Collect_conj_eq Collect_neg_eq)
 
 lemma [intro?]:
-  "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
-    ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."
+  "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
+    \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
   by (simp add: while Collect_conj_eq Collect_neg_eq)
 
 
@@ -378,13 +376,9 @@
   by (auto simp: Valid_def)
 
 lemma iter_aux:
-  "\<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
-       (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)"
-  apply(induct n)
-   apply clarsimp
-   apply (simp (no_asm_use))
-   apply blast
-  done
+  "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
+       (\<And>s s'. s \<in> I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> I \<and> s' \<notin> b)"
+  by (induct n) auto
 
 lemma WhileRule:
     "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
diff -r af028f35af60 -r eb07b0acbebc src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Fri Feb 21 18:23:11 2014 +0100
@@ -32,7 +32,7 @@
 text {* Using the basic @{text assign} rule directly is a bit
   cumbersome. *}
 
-lemma "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
+lemma "\<turnstile> \<lbrace>\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) \<in> \<lbrace>\<acute>N = 10\<rbrace>\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
   by (rule assign)
 
 text {* Certainly we want the state modification already done, e.g.\
@@ -40,31 +40,31 @@
   update for us; we may apply the Simplifier afterwards to achieve
   ``obvious'' consequences as well. *}
 
-lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."
+lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>N := 10 \<lbrace>\<acute>N = 10\<rbrace>"
   by hoare
 
-lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
+lemma "\<turnstile> \<lbrace>2 * \<acute>N = 10\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
   by hoare
 
-lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
+lemma "\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
   by hoare simp
 
-lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
+lemma "\<turnstile> \<lbrace>\<acute>N + 1 = a + 1\<rbrace> \<acute>N := \<acute>N + 1 \<lbrace>\<acute>N = a + 1\<rbrace>"
   by hoare
 
-lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
+lemma "\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N := \<acute>N + 1 \<lbrace>\<acute>N = a + 1\<rbrace>"
   by hoare simp
 
-lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
+lemma "\<turnstile> \<lbrace>a = a \<and> b = b\<rbrace> \<acute>M := a; \<acute>N := b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
   by hoare
 
-lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
+lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>M := a; \<acute>N := b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
   by hoare simp
 
 lemma
-  "|- .{\<acute>M = a & \<acute>N = b}.
+  "\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
       \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I
-      .{\<acute>M = b & \<acute>N = a}."
+      \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
   by hoare simp
 
 text {* It is important to note that statements like the following one
@@ -72,10 +72,10 @@
   extra-logical nature of record fields, we cannot formulate a theorem
   relating record selectors and updates schematically. *}
 
-lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."
+lemma "\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N := \<acute>N \<lbrace>\<acute>N = a\<rbrace>"
   by hoare
 
-lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}."
+lemma "\<turnstile> \<lbrace>\<acute>x = a\<rbrace> \<acute>x := \<acute>x \<lbrace>\<acute>x = a\<rbrace>"
   oops
 
 lemma
@@ -88,27 +88,27 @@
   rule in order to achieve the intended precondition.  Certainly, the
   \name{hoare} method is able to handle this case, too. *}
 
-lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
+lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
 proof -
-  have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}."
+  have "\<lbrace>\<acute>M = \<acute>N\<rbrace> \<subseteq> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace>"
     by auto
-  also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
+  also have "\<turnstile> \<dots> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
     by hoare
   finally show ?thesis .
 qed
 
-lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
+lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
 proof -
-  have "!!m n::nat. m = n --> m + 1 ~= n"
+  have "\<And>m n::nat. m = n \<longrightarrow> m + 1 \<noteq> n"
       -- {* inclusion of assertions expressed in ``pure'' logic, *}
       -- {* without mentioning the state space *}
     by simp
-  also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
+  also have "\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
     by hoare
   finally show ?thesis .
 qed
 
-lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
+lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
   by hoare simp
 
 
@@ -120,24 +120,24 @@
   structured proof based on single-step Hoare rules. *}
 
 lemma
-  "|- .{\<acute>M = 0 & \<acute>S = 0}.
-      WHILE \<acute>M ~= a
+  "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
+      WHILE \<acute>M \<noteq> a
       DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
-      .{\<acute>S = a * b}."
+      \<lbrace>\<acute>S = a * b\<rbrace>"
 proof -
-  let "|- _ ?while _" = ?thesis
-  let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}."
+  let "\<turnstile> _ ?while _" = ?thesis
+  let "\<lbrace>\<acute>?inv\<rbrace>" = "\<lbrace>\<acute>S = \<acute>M * b\<rbrace>"
 
-  have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto
-  also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}."
+  have "\<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> \<subseteq> \<lbrace>\<acute>?inv\<rbrace>" by auto
+  also have "\<turnstile> \<dots> ?while \<lbrace>\<acute>?inv \<and> \<not> (\<acute>M \<noteq> a)\<rbrace>"
   proof
     let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1"
-    have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}."
+    have "\<lbrace>\<acute>?inv \<and> \<acute>M \<noteq> a\<rbrace> \<subseteq> \<lbrace>\<acute>S + b = (\<acute>M + 1) * b\<rbrace>"
       by auto
-    also have "|- ... ?c .{\<acute>?inv}." by hoare
-    finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." .
+    also have "\<turnstile> \<dots> ?c \<lbrace>\<acute>?inv\<rbrace>" by hoare
+    finally show "\<turnstile> \<lbrace>\<acute>?inv \<and> \<acute>M \<noteq> a\<rbrace> ?c \<lbrace>\<acute>?inv\<rbrace>" .
   qed
-  also have "... <= .{\<acute>S = a * b}." by auto
+  also have "\<dots> \<subseteq> \<lbrace>\<acute>S = a * b\<rbrace>" by auto
   finally show ?thesis .
 qed
 
@@ -147,11 +147,11 @@
   specify the \texttt{WHILE} loop invariant in the original statement. *}
 
 lemma
-  "|- .{\<acute>M = 0 & \<acute>S = 0}.
-      WHILE \<acute>M ~= a
-      INV .{\<acute>S = \<acute>M * b}.
+  "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
+      WHILE \<acute>M \<noteq> a
+      INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
       DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
-      .{\<acute>S = a * b}."
+      \<lbrace>\<acute>S = a * b\<rbrace>"
   by hoare auto
 
 
@@ -168,37 +168,37 @@
   the state space. *}
 
 theorem
-  "|- .{True}.
+  "\<turnstile> \<lbrace>True\<rbrace>
       \<acute>S := 0; \<acute>I := 1;
-      WHILE \<acute>I ~= n
+      WHILE \<acute>I \<noteq> n
       DO
         \<acute>S := \<acute>S + \<acute>I;
         \<acute>I := \<acute>I + 1
       OD
-      .{\<acute>S = (SUM j<n. j)}."
-  (is "|- _ (_; ?while) _")
+      \<lbrace>\<acute>S = (\<Sum>j<n. j)\<rbrace>"
+  (is "\<turnstile> _ (_; ?while) _")
 proof -
-  let ?sum = "\<lambda>k::nat. SUM j<k. j"
+  let ?sum = "\<lambda>k::nat. \<Sum>j<k. j"
   let ?inv = "\<lambda>s i::nat. s = ?sum i"
 
-  have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
+  have "\<turnstile> \<lbrace>True\<rbrace> \<acute>S := 0; \<acute>I := 1 \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
   proof -
-    have "True --> 0 = ?sum 1"
+    have "True \<longrightarrow> 0 = ?sum 1"
       by simp
-    also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
+    also have "\<turnstile> \<lbrace>\<dots>\<rbrace> \<acute>S := 0; \<acute>I := 1 \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
       by hoare
     finally show ?thesis .
   qed
-  also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}."
+  also have "\<turnstile> \<dots> ?while \<lbrace>?inv \<acute>S \<acute>I \<and> \<not> \<acute>I \<noteq> n\<rbrace>"
   proof
     let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
-    have "!!s i. ?inv s i & i ~= n -->  ?inv (s + i) (i + 1)"
+    have "\<And>s i. ?inv s i \<and> i \<noteq> n \<longrightarrow> ?inv (s + i) (i + 1)"
       by simp
-    also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}."
+    also have "\<turnstile> \<lbrace>\<acute>S + \<acute>I = ?sum (\<acute>I + 1)\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
       by hoare
-    finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." .
+    finally show "\<turnstile> \<lbrace>?inv \<acute>S \<acute>I \<and> \<acute>I \<noteq> n\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>" .
   qed
-  also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n"
+  also have "\<And>s i. s = ?sum i \<and> \<not> i \<noteq> n \<longrightarrow> s = ?sum n"
     by simp
   finally show ?thesis .
 qed
@@ -208,27 +208,29 @@
   structured manner. *}
 
 theorem
-  "|- .{True}.
+  "\<turnstile> \<lbrace>True\<rbrace>
       \<acute>S := 0; \<acute>I := 1;
-      WHILE \<acute>I ~= n
-      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
+      WHILE \<acute>I \<noteq> n
+      INV \<lbrace>\<acute>S = (\<Sum>j<\<acute>I. j)\<rbrace>
       DO
         \<acute>S := \<acute>S + \<acute>I;
         \<acute>I := \<acute>I + 1
       OD
-      .{\<acute>S = (SUM j<n. j)}."
+      \<lbrace>\<acute>S = (\<Sum>j<n. j)\<rbrace>"
 proof -
-  let ?sum = "\<lambda>k::nat. SUM j<k. j"
+  let ?sum = "\<lambda>k::nat. \<Sum>j<k. j"
   let ?inv = "\<lambda>s i::nat. s = ?sum i"
 
   show ?thesis
   proof hoare
     show "?inv 0 1" by simp
   next
-    fix s i assume "?inv s i & i ~= n"
+    fix s i
+    assume "?inv s i \<and> i \<noteq> n"
     then show "?inv (s + i) (i + 1)" by simp
   next
-    fix s i assume "?inv s i & ~ i ~= n"
+    fix s i
+    assume "?inv s i \<and> \<not> i \<noteq> n"
     then show "s = ?sum n" by simp
   qed
 qed
@@ -237,15 +239,15 @@
   provided that the invariant is given beforehand. *}
 
 theorem
-  "|- .{True}.
+  "\<turnstile> \<lbrace>True\<rbrace>
       \<acute>S := 0; \<acute>I := 1;
-      WHILE \<acute>I ~= n
-      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
+      WHILE \<acute>I \<noteq> n
+      INV \<lbrace>\<acute>S = (\<Sum>j<\<acute>I. j)\<rbrace>
       DO
         \<acute>S := \<acute>S + \<acute>I;
         \<acute>I := \<acute>I + 1
       OD
-      .{\<acute>S = (SUM j<n. j)}."
+      \<lbrace>\<acute>S = (\<Sum>j<n. j)\<rbrace>"
   by hoare auto
 
 
@@ -273,18 +275,18 @@
   by (induct n) simp_all
 
 lemma
-  "|- .{i = \<acute>I & \<acute>time = 0}.
-    timeit (
-    WHILE \<acute>I \<noteq> 0
-    INV .{2 *\<acute> time + \<acute>I * \<acute>I + 5 * \<acute>I = i * i + 5 * i}.
-    DO
-      \<acute>J := \<acute>I;
-      WHILE \<acute>J \<noteq> 0
-      INV .{0 < \<acute>I & 2 * \<acute>time + \<acute>I * \<acute>I + 3 * \<acute>I + 2 * \<acute>J - 2 = i * i + 5 * i}.
-      DO \<acute>J := \<acute>J - 1 OD;
-        \<acute>I := \<acute>I - 1
-    OD
-    ) .{2*\<acute>time = i*i + 5*i}."
+  "\<turnstile> \<lbrace>i = \<acute>I \<and> \<acute>time = 0\<rbrace>
+    (timeit
+      (WHILE \<acute>I \<noteq> 0
+        INV \<lbrace>2 *\<acute> time + \<acute>I * \<acute>I + 5 * \<acute>I = i * i + 5 * i\<rbrace>
+        DO
+          \<acute>J := \<acute>I;
+          WHILE \<acute>J \<noteq> 0
+          INV \<lbrace>0 < \<acute>I \<and> 2 * \<acute>time + \<acute>I * \<acute>I + 3 * \<acute>I + 2 * \<acute>J - 2 = i * i + 5 * i\<rbrace>
+          DO \<acute>J := \<acute>J - 1 OD;
+          \<acute>I := \<acute>I - 1
+        OD))
+    \<lbrace>2 * \<acute>time = i * i + 5 * i\<rbrace>"
   apply simp
   apply hoare
       apply simp
diff -r af028f35af60 -r eb07b0acbebc src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Fri Feb 21 18:23:11 2014 +0100
@@ -14,40 +14,40 @@
 
 subsection {* Tilings *}
 
-inductive_set tiling :: "'a set set => 'a set set"
+inductive_set tiling :: "'a set set \<Rightarrow> 'a set set"
   for A :: "'a set set"
 where
-  empty: "{} : tiling A"
-| Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A"
+  empty: "{} \<in> tiling A"
+| Un: "a \<in> A \<Longrightarrow> t \<in> tiling A \<Longrightarrow> a \<subseteq> - t \<Longrightarrow> a \<union> t \<in> tiling A"
 
 
 text "The union of two disjoint tilings is a tiling."
 
 lemma tiling_Un:
-  assumes "t : tiling A"
-    and "u : tiling A"
-    and "t Int u = {}"
-  shows "t Un u : tiling A"
+  assumes "t \<in> tiling A"
+    and "u \<in> tiling A"
+    and "t \<inter> u = {}"
+  shows "t \<union> u \<in> tiling A"
 proof -
   let ?T = "tiling A"
-  from `t : ?T` and `t Int u = {}`
-  show "t Un u : ?T"
+  from `t \<in> ?T` and `t \<inter> u = {}`
+  show "t \<union> u \<in> ?T"
   proof (induct t)
     case empty
-    with `u : ?T` show "{} Un u : ?T" by simp
+    with `u \<in> ?T` show "{} \<union> u \<in> ?T" by simp
   next
     case (Un a t)
-    show "(a Un t) Un u : ?T"
+    show "(a \<union> t) \<union> u \<in> ?T"
     proof -
-      have "a Un (t Un u) : ?T"
-        using `a : A`
+      have "a \<union> (t \<union> u) \<in> ?T"
+        using `a \<in> A`
       proof (rule tiling.Un)
-        from `(a Un t) Int u = {}` have "t Int u = {}" by blast
-        then show "t Un u: ?T" by (rule Un)
-        from `a <= - t` and `(a Un t) Int u = {}`
-        show "a <= - (t Un u)" by blast
+        from `(a \<union> t) \<inter> u = {}` have "t \<inter> u = {}" by blast
+        then show "t \<union> u \<in> ?T" by (rule Un)
+        from `a \<subseteq> - t` and `(a \<union> t) \<inter> u = {}`
+        show "a \<subseteq> - (t \<union> u)" by blast
       qed
-      also have "a Un (t Un u) = (a Un t) Un u"
+      also have "a \<union> (t \<union> u) = (a \<union> t) \<union> u"
         by (simp only: Un_assoc)
       finally show ?thesis .
     qed
@@ -57,22 +57,21 @@
 
 subsection {* Basic properties of ``below'' *}
 
-definition below :: "nat => nat set"
+definition below :: "nat \<Rightarrow> nat set"
   where "below n = {i. i < n}"
 
-lemma below_less_iff [iff]: "(i: below k) = (i < k)"
+lemma below_less_iff [iff]: "i \<in> below k \<longleftrightarrow> i < k"
   by (simp add: below_def)
 
 lemma below_0: "below 0 = {}"
   by (simp add: below_def)
 
-lemma Sigma_Suc1:
-    "m = n + 1 ==> below m <*> B = ({n} <*> B) Un (below n <*> B)"
+lemma Sigma_Suc1: "m = n + 1 \<Longrightarrow> below m \<times> B = ({n} \<times> B) \<union> (below n \<times> B)"
   by (simp add: below_def less_Suc_eq) blast
 
 lemma Sigma_Suc2:
-  "m = n + 2 ==> A <*> below m =
-    (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"
+  "m = n + 2 \<Longrightarrow>
+    A \<times> below m = (A \<times> {n}) \<union> (A \<times> {n + 1}) \<union> (A \<times> below n)"
   by (auto simp add: below_def)
 
 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2
@@ -80,22 +79,22 @@
 
 subsection {* Basic properties of ``evnodd'' *}
 
-definition evnodd :: "(nat * nat) set => nat => (nat * nat) set"
-  where "evnodd A b = A Int {(i, j). (i + j) mod 2 = b}"
+definition evnodd :: "(nat \<times> nat) set \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set"
+  where "evnodd A b = A \<inter> {(i, j). (i + j) mod 2 = b}"
 
-lemma evnodd_iff: "(i, j): evnodd A b = ((i, j): A  & (i + j) mod 2 = b)"
+lemma evnodd_iff: "(i, j) \<in> evnodd A b \<longleftrightarrow> (i, j) \<in> A  \<and> (i + j) mod 2 = b"
   by (simp add: evnodd_def)
 
-lemma evnodd_subset: "evnodd A b <= A"
+lemma evnodd_subset: "evnodd A b \<subseteq> A"
   unfolding evnodd_def by (rule Int_lower1)
 
-lemma evnoddD: "x : evnodd A b ==> x : A"
+lemma evnoddD: "x \<in> evnodd A b \<Longrightarrow> x \<in> A"
   by (rule subsetD) (rule evnodd_subset)
 
-lemma evnodd_finite: "finite A ==> finite (evnodd A b)"
+lemma evnodd_finite: "finite A \<Longrightarrow> finite (evnodd A b)"
   by (rule finite_subset) (rule evnodd_subset)
 
-lemma evnodd_Un: "evnodd (A Un B) b = evnodd A b Un evnodd B b"
+lemma evnodd_Un: "evnodd (A \<union> B) b = evnodd A b \<union> evnodd B b"
   unfolding evnodd_def by blast
 
 lemma evnodd_Diff: "evnodd (A - B) b = evnodd A b - evnodd B b"
@@ -112,60 +111,60 @@
 
 subsection {* Dominoes *}
 
-inductive_set domino :: "(nat * nat) set set"
+inductive_set domino :: "(nat \<times> nat) set set"
 where
-  horiz: "{(i, j), (i, j + 1)} : domino"
-| vertl: "{(i, j), (i + 1, j)} : domino"
+  horiz: "{(i, j), (i, j + 1)} \<in> domino"
+| vertl: "{(i, j), (i + 1, j)} \<in> domino"
 
 lemma dominoes_tile_row:
-  "{i} <*> below (2 * n) : tiling domino"
-  (is "?B n : ?T")
+  "{i} \<times> below (2 * n) \<in> tiling domino"
+  (is "?B n \<in> ?T")
 proof (induct n)
   case 0
   show ?case by (simp add: below_0 tiling.empty)
 next
   case (Suc n)
-  let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
-  have "?B (Suc n) = ?a Un ?B n"
+  let ?a = "{i} \<times> {2 * n + 1} \<union> {i} \<times> {2 * n}"
+  have "?B (Suc n) = ?a \<union> ?B n"
     by (auto simp add: Sigma_Suc Un_assoc)
-  also have "... : ?T"
+  also have "\<dots> \<in> ?T"
   proof (rule tiling.Un)
-    have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
+    have "{(i, 2 * n), (i, 2 * n + 1)} \<in> domino"
       by (rule domino.horiz)
     also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast
-    finally show "... : domino" .
-    show "?B n : ?T" by (rule Suc)
-    show "?a <= - ?B n" by blast
+    finally show "\<dots> \<in> domino" .
+    show "?B n \<in> ?T" by (rule Suc)
+    show "?a \<subseteq> - ?B n" by blast
   qed
   finally show ?case .
 qed
 
 lemma dominoes_tile_matrix:
-  "below m <*> below (2 * n) : tiling domino"
-  (is "?B m : ?T")
+  "below m \<times> below (2 * n) \<in> tiling domino"
+  (is "?B m \<in> ?T")
 proof (induct m)
   case 0
   show ?case by (simp add: below_0 tiling.empty)
 next
   case (Suc m)
-  let ?t = "{m} <*> below (2 * n)"
-  have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
-  also have "... : ?T"
+  let ?t = "{m} \<times> below (2 * n)"
+  have "?B (Suc m) = ?t \<union> ?B m" by (simp add: Sigma_Suc)
+  also have "\<dots> \<in> ?T"
   proof (rule tiling_Un)
-    show "?t : ?T" by (rule dominoes_tile_row)
-    show "?B m : ?T" by (rule Suc)
-    show "?t Int ?B m = {}" by blast
+    show "?t \<in> ?T" by (rule dominoes_tile_row)
+    show "?B m \<in> ?T" by (rule Suc)
+    show "?t \<inter> ?B m = {}" by blast
   qed
   finally show ?case .
 qed
 
 lemma domino_singleton:
-  assumes "d : domino"
+  assumes "d \<in> domino"
     and "b < 2"
-  shows "EX i j. evnodd d b = {(i, j)}"  (is "?P d")
+  shows "\<exists>i j. evnodd d b = {(i, j)}"  (is "?P d")
   using assms
 proof induct
-  from `b < 2` have b_cases: "b = 0 | b = 1" by arith
+  from `b < 2` have b_cases: "b = 0 \<or> b = 1" by arith
   fix i j
   note [simp] = evnodd_empty evnodd_insert mod_Suc
   from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
@@ -173,7 +172,7 @@
 qed
 
 lemma domino_finite:
-  assumes "d: domino"
+  assumes "d \<in> domino"
   shows "finite d"
   using assms
 proof induct
@@ -186,18 +185,19 @@
 subsection {* Tilings of dominoes *}
 
 lemma tiling_domino_finite:
-  assumes t: "t : tiling domino"  (is "t : ?T")
+  assumes t: "t \<in> tiling domino"  (is "t \<in> ?T")
   shows "finite t"  (is "?F t")
   using t
 proof induct
   show "?F {}" by (rule finite.emptyI)
   fix a t assume "?F t"
-  assume "a : domino" then have "?F a" by (rule domino_finite)
-  from this and `?F t` show "?F (a Un t)" by (rule finite_UnI)
+  assume "a \<in> domino"
+  then have "?F a" by (rule domino_finite)
+  from this and `?F t` show "?F (a \<union> t)" by (rule finite_UnI)
 qed
 
 lemma tiling_domino_01:
-  assumes t: "t : tiling domino"  (is "t : ?T")
+  assumes t: "t \<in> tiling domino"  (is "t \<in> ?T")
   shows "card (evnodd t 0) = card (evnodd t 1)"
   using t
 proof induct
@@ -207,33 +207,34 @@
   case (Un a t)
   let ?e = evnodd
   note hyp = `card (?e t 0) = card (?e t 1)`
-    and at = `a <= - t`
+    and at = `a \<subseteq> - t`
   have card_suc:
-    "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
+    "\<And>b. b < 2 \<Longrightarrow> card (?e (a \<union> t) b) = Suc (card (?e t b))"
   proof -
-    fix b :: nat assume "b < 2"
-    have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
+    fix b :: nat
+    assume "b < 2"
+    have "?e (a \<union> t) b = ?e a b \<union> ?e t b" by (rule evnodd_Un)
     also obtain i j where e: "?e a b = {(i, j)}"
     proof -
       from `a \<in> domino` and `b < 2`
-      have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
+      have "\<exists>i j. ?e a b = {(i, j)}" by (rule domino_singleton)
       then show ?thesis by (blast intro: that)
     qed
-    also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
-    also have "card ... = Suc (card (?e t b))"
+    also have "\<dots> \<union> ?e t b = insert (i, j) (?e t b)" by simp
+    also have "card \<dots> = Suc (card (?e t b))"
     proof (rule card_insert_disjoint)
       from `t \<in> tiling domino` have "finite t"
         by (rule tiling_domino_finite)
       then show "finite (?e t b)"
         by (rule evnodd_finite)
-      from e have "(i, j) : ?e a b" by simp
-      with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
+      from e have "(i, j) \<in> ?e a b" by simp
+      with at show "(i, j) \<notin> ?e t b" by (blast dest: evnoddD)
     qed
     finally show "?thesis b" .
   qed
-  then have "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
+  then have "card (?e (a \<union> t) 0) = Suc (card (?e t 0))" by simp
   also from hyp have "card (?e t 0) = card (?e t 1)" .
-  also from card_suc have "Suc ... = card (?e (a Un t) 1)"
+  also from card_suc have "Suc \<dots> = card (?e (a \<union> t) 1)"
     by simp
   finally show ?case .
 qed
@@ -241,23 +242,23 @@
 
 subsection {* Main theorem *}
 
-definition mutilated_board :: "nat => nat => (nat * nat) set"
+definition mutilated_board :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set"
   where
     "mutilated_board m n =
-      below (2 * (m + 1)) <*> below (2 * (n + 1))
+      below (2 * (m + 1)) \<times> below (2 * (n + 1))
         - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
 
-theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"
+theorem mutil_not_tiling: "mutilated_board m n \<notin> tiling domino"
 proof (unfold mutilated_board_def)
   let ?T = "tiling domino"
-  let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))"
+  let ?t = "below (2 * (m + 1)) \<times> below (2 * (n + 1))"
   let ?t' = "?t - {(0, 0)}"
   let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"
 
-  show "?t'' ~: ?T"
+  show "?t'' \<notin> ?T"
   proof
-    have t: "?t : ?T" by (rule dominoes_tile_matrix)
-    assume t'': "?t'' : ?T"
+    have t: "?t \<in> ?T" by (rule dominoes_tile_matrix)
+    assume t'': "?t'' \<in> ?T"
 
     let ?e = evnodd
     have fin: "finite (?e ?t 0)"
@@ -271,23 +272,23 @@
       proof (rule card_Diff1_less)
         from _ fin show "finite (?e ?t' 0)"
           by (rule finite_subset) auto
-        show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
+        show "(2 * m + 1, 2 * n + 1) \<in> ?e ?t' 0" by simp
       qed
       then show ?thesis by simp
     qed
-    also have "... < card (?e ?t 0)"
+    also have "\<dots> < card (?e ?t 0)"
     proof -
-      have "(0, 0) : ?e ?t 0" by simp
+      have "(0, 0) \<in> ?e ?t 0" by simp
       with fin have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"
         by (rule card_Diff1_less)
       then show ?thesis by simp
     qed
-    also from t have "... = card (?e ?t 1)"
+    also from t have "\<dots> = card (?e ?t 1)"
       by (rule tiling_domino_01)
     also have "?e ?t 1 = ?e ?t'' 1" by simp
-    also from t'' have "card ... = card (?e ?t'' 0)"
+    also from t'' have "card \<dots> = card (?e ?t'' 0)"
       by (rule tiling_domino_01 [symmetric])
-    finally have "... < ..." . then show False ..
+    finally have "\<dots> < \<dots>" . then show False ..
   qed
 qed
 
diff -r af028f35af60 -r eb07b0acbebc src/HOL/Isar_Examples/Nested_Datatype.thy
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy	Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy	Fri Feb 21 18:23:11 2014 +0100
@@ -7,12 +7,11 @@
 subsection {* Terms and substitution *}
 
 datatype ('a, 'b) "term" =
-    Var 'a
-  | App 'b "('a, 'b) term list"
+  Var 'a
+| App 'b "('a, 'b) term list"
 
-primrec
-  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
-  subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
+primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term"
+  and subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
 where
   "subst_term f (Var a) = f a"
 | "subst_term f (App b ts) = App b (subst_term_list f ts)"
@@ -24,18 +23,18 @@
 text {* \medskip A simple lemma about composition of substitutions. *}
 
 lemma
-  "subst_term (subst_term f1 o f2) t =
+  "subst_term (subst_term f1 \<circ> f2) t =
     subst_term f1 (subst_term f2 t)"
   and
-  "subst_term_list (subst_term f1 o f2) ts =
+  "subst_term_list (subst_term f1 \<circ> f2) ts =
     subst_term_list f1 (subst_term_list f2 ts)"
   by (induct t and ts) simp_all
 
-lemma "subst_term (subst_term f1 o f2) t =
+lemma "subst_term (subst_term f1 \<circ> f2) t =
     subst_term f1 (subst_term f2 t)"
 proof -
   let "?P t" = ?thesis
-  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
+  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 \<circ> f2) ts =
     subst_term_list f1 (subst_term_list f2 ts)"
   show ?thesis
   proof (induct t)
@@ -57,8 +56,8 @@
 subsection {* Alternative induction *}
 
 theorem term_induct' [case_names Var App]:
-  assumes var: "!!a. P (Var a)"
-    and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"
+  assumes var: "\<And>a. P (Var a)"
+    and app: "\<And>b ts. (\<forall>t \<in> set ts. P t) \<Longrightarrow> P (App b ts)"
   shows "P t"
 proof (induct t)
   fix a show "P (Var a)" by (rule var)
@@ -72,8 +71,7 @@
   then show "\<forall>t' \<in> set (t # ts). P t'" by simp
 qed
 
-lemma
-  "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
+lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
 proof (induct t rule: term_induct')
   case (Var a)
   show ?case by (simp add: o_def)