author wenzelm Fri, 21 Feb 2014 18:23:11 +0100 changeset 55656 eb07b0acbebc parent 55655 af028f35af60 child 55657 d5ad50aea356 child 55659 4089f6e98ab9
more symbols;
 src/HOL/Isar_Examples/Basic_Logic.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Fibonacci.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Group.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Group_Context.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Group_Notepad.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Hoare.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Hoare_Ex.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Mutilated_Checkerboard.thy file | annotate | diff | comparison | revisions src/HOL/Isar_Examples/Nested_Datatype.thy file | annotate | diff | comparison | revisions
--- 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 ..
--- 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
--- 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
--- 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"
--- 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"
--- 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)"       ("(.'(_').)"  1000)
-  "_antiquote"   :: "('a => 'b) => 'b"       ("\<acute>_"  1000)
+  "_quote"       :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"       ("(.'(_').)"  1000)
+  "_antiquote"   :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"       ("\<acute>_"  1000)
"_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
("_[_'/\<acute>_]"  999)
-  "_Assert"      :: "'a => 'a set"           ("(.{_}.)"  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>)"  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>)"  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"
--- 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
--- 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

--- 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)