--- 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)" ("(.'(_').)" [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"
--- 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)