1.1 --- a/src/HOL/Isar_Examples/Basic_Logic.thy Fri Feb 21 17:06:48 2014 +0100
1.2 +++ b/src/HOL/Isar_Examples/Basic_Logic.thy Fri Feb 21 18:23:11 2014 +0100
1.3 @@ -291,7 +291,7 @@
1.4 cases actually coincide. Consequently the proof may be rephrased as
1.5 follows. *}
1.6
1.7 -lemma "P \<or> P --> P"
1.8 +lemma "P \<or> P \<longrightarrow> P"
1.9 proof
1.10 assume "P \<or> P"
1.11 then show P
1.12 @@ -307,7 +307,7 @@
1.13 are implicitly performed when concluding the single rule step of the
1.14 double-dot proof as follows. *}
1.15
1.16 -lemma "P \<or> P --> P"
1.17 +lemma "P \<or> P \<longrightarrow> P"
1.18 proof
1.19 assume "P \<or> P"
1.20 then show P ..
2.1 --- a/src/HOL/Isar_Examples/Fibonacci.thy Fri Feb 21 17:06:48 2014 +0100
2.2 +++ b/src/HOL/Isar_Examples/Fibonacci.thy Fri Feb 21 18:23:11 2014 +0100
2.3 @@ -150,7 +150,7 @@
2.4 with hyp have "gcd (fib m) (fib ((n - m) mod m))
2.5 = gcd (fib m) (fib (n - m))" by simp
2.6 also have "\<dots> = gcd (fib m) (fib n)"
2.7 - using `m <= n` by (rule gcd_fib_diff)
2.8 + using `m \<le> n` by (rule gcd_fib_diff)
2.9 finally have "gcd (fib m) (fib ((n - m) mod m)) =
2.10 gcd (fib m) (fib n)" .
2.11 with False show ?thesis by simp
3.1 --- a/src/HOL/Isar_Examples/Group.thy Fri Feb 21 17:06:48 2014 +0100
3.2 +++ b/src/HOL/Isar_Examples/Group.thy Fri Feb 21 18:23:11 2014 +0100
3.3 @@ -27,19 +27,19 @@
3.4 proof -
3.5 have "x * inverse x = 1 * (x * inverse x)"
3.6 by (simp only: group_left_one)
3.7 - also have "... = 1 * x * inverse x"
3.8 + also have "\<dots> = 1 * x * inverse x"
3.9 by (simp only: group_assoc)
3.10 - also have "... = inverse (inverse x) * inverse x * x * inverse x"
3.11 + also have "\<dots> = inverse (inverse x) * inverse x * x * inverse x"
3.12 by (simp only: group_left_inverse)
3.13 - also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
3.14 + also have "\<dots> = inverse (inverse x) * (inverse x * x) * inverse x"
3.15 by (simp only: group_assoc)
3.16 - also have "... = inverse (inverse x) * 1 * inverse x"
3.17 + also have "\<dots> = inverse (inverse x) * 1 * inverse x"
3.18 by (simp only: group_left_inverse)
3.19 - also have "... = inverse (inverse x) * (1 * inverse x)"
3.20 + also have "\<dots> = inverse (inverse x) * (1 * inverse x)"
3.21 by (simp only: group_assoc)
3.22 - also have "... = inverse (inverse x) * inverse x"
3.23 + also have "\<dots> = inverse (inverse x) * inverse x"
3.24 by (simp only: group_left_one)
3.25 - also have "... = 1"
3.26 + also have "\<dots> = 1"
3.27 by (simp only: group_left_inverse)
3.28 finally show ?thesis .
3.29 qed
3.30 @@ -52,11 +52,11 @@
3.31 proof -
3.32 have "x * 1 = x * (inverse x * x)"
3.33 by (simp only: group_left_inverse)
3.34 - also have "... = x * inverse x * x"
3.35 + also have "\<dots> = x * inverse x * x"
3.36 by (simp only: group_assoc)
3.37 - also have "... = 1 * x"
3.38 + also have "\<dots> = 1 * x"
3.39 by (simp only: group_right_inverse)
3.40 - also have "... = x"
3.41 + also have "\<dots> = x"
3.42 by (simp only: group_left_one)
3.43 finally show ?thesis .
3.44 qed
3.45 @@ -92,25 +92,25 @@
3.46 note calculation = this
3.47 -- {* first calculational step: init calculation register *}
3.48
3.49 - have "... = x * inverse x * x"
3.50 + have "\<dots> = x * inverse x * x"
3.51 by (simp only: group_assoc)
3.52
3.53 note calculation = trans [OF calculation this]
3.54 -- {* general calculational step: compose with transitivity rule *}
3.55
3.56 - have "... = 1 * x"
3.57 + have "\<dots> = 1 * x"
3.58 by (simp only: group_right_inverse)
3.59
3.60 note calculation = trans [OF calculation this]
3.61 -- {* general calculational step: compose with transitivity rule *}
3.62
3.63 - have "... = x"
3.64 + have "\<dots> = x"
3.65 by (simp only: group_left_one)
3.66
3.67 note calculation = trans [OF calculation this]
3.68 - -- {* final calculational step: compose with transitivity rule ... *}
3.69 + -- {* final calculational step: compose with transitivity rule \dots *}
3.70 from calculation
3.71 - -- {* ... and pick up the final result *}
3.72 + -- {* \dots\ and pick up the final result *}
3.73
3.74 show ?thesis .
3.75 qed
3.76 @@ -168,13 +168,13 @@
3.77 proof -
3.78 have "1 = x * inverse x"
3.79 by (simp only: group_right_inverse)
3.80 - also have "... = (e * x) * inverse x"
3.81 + also have "\<dots> = (e * x) * inverse x"
3.82 by (simp only: eq)
3.83 - also have "... = e * (x * inverse x)"
3.84 + also have "\<dots> = e * (x * inverse x)"
3.85 by (simp only: group_assoc)
3.86 - also have "... = e * 1"
3.87 + also have "\<dots> = e * 1"
3.88 by (simp only: group_right_inverse)
3.89 - also have "... = e"
3.90 + also have "\<dots> = e"
3.91 by (simp only: group_right_one)
3.92 finally show ?thesis .
3.93 qed
3.94 @@ -187,13 +187,13 @@
3.95 proof -
3.96 have "inverse x = 1 * inverse x"
3.97 by (simp only: group_left_one)
3.98 - also have "... = (x' * x) * inverse x"
3.99 + also have "\<dots> = (x' * x) * inverse x"
3.100 by (simp only: eq)
3.101 - also have "... = x' * (x * inverse x)"
3.102 + also have "\<dots> = x' * (x * inverse x)"
3.103 by (simp only: group_assoc)
3.104 - also have "... = x' * 1"
3.105 + also have "\<dots> = x' * 1"
3.106 by (simp only: group_right_inverse)
3.107 - also have "... = x'"
3.108 + also have "\<dots> = x'"
3.109 by (simp only: group_right_one)
3.110 finally show ?thesis .
3.111 qed
3.112 @@ -207,11 +207,11 @@
3.113 have "(inverse y * inverse x) * (x * y) =
3.114 (inverse y * (inverse x * x)) * y"
3.115 by (simp only: group_assoc)
3.116 - also have "... = (inverse y * 1) * y"
3.117 + also have "\<dots> = (inverse y * 1) * y"
3.118 by (simp only: group_left_inverse)
3.119 - also have "... = inverse y * y"
3.120 + also have "\<dots> = inverse y * y"
3.121 by (simp only: group_right_one)
3.122 - also have "... = 1"
3.123 + also have "\<dots> = 1"
3.124 by (simp only: group_left_inverse)
3.125 finally show ?thesis .
3.126 qed
3.127 @@ -229,15 +229,15 @@
3.128 proof -
3.129 have "x = x * 1"
3.130 by (simp only: group_right_one)
3.131 - also have "... = x * (inverse y * y)"
3.132 + also have "\<dots> = x * (inverse y * y)"
3.133 by (simp only: group_left_inverse)
3.134 - also have "... = x * (inverse x * y)"
3.135 + also have "\<dots> = x * (inverse x * y)"
3.136 by (simp only: eq)
3.137 - also have "... = (x * inverse x) * y"
3.138 + also have "\<dots> = (x * inverse x) * y"
3.139 by (simp only: group_assoc)
3.140 - also have "... = 1 * y"
3.141 + also have "\<dots> = 1 * y"
3.142 by (simp only: group_right_inverse)
3.143 - also have "... = y"
3.144 + also have "\<dots> = y"
3.145 by (simp only: group_left_one)
3.146 finally show ?thesis .
3.147 qed
4.1 --- a/src/HOL/Isar_Examples/Group_Context.thy Fri Feb 21 17:06:48 2014 +0100
4.2 +++ b/src/HOL/Isar_Examples/Group_Context.thy Fri Feb 21 18:23:11 2014 +0100
4.3 @@ -13,7 +13,7 @@
4.4 context
4.5 fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70)
4.6 and one :: "'a"
4.7 - and inverse :: "'a => 'a"
4.8 + and inverse :: "'a \<Rightarrow> 'a"
4.9 assumes assoc: "(x ** y) ** z = x ** (y ** z)"
4.10 and left_one: "one ** x = x"
4.11 and left_inverse: "inverse x ** x = one"
5.1 --- a/src/HOL/Isar_Examples/Group_Notepad.thy Fri Feb 21 17:06:48 2014 +0100
5.2 +++ b/src/HOL/Isar_Examples/Group_Notepad.thy Fri Feb 21 18:23:11 2014 +0100
5.3 @@ -14,7 +14,7 @@
5.4
5.5 fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70)
5.6 and one :: "'a"
5.7 - and inverse :: "'a => 'a"
5.8 + and inverse :: "'a \<Rightarrow> 'a"
5.9 assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
5.10 and left_one: "\<And>x. one ** x = x"
5.11 and left_inverse: "\<And>x. inverse x ** x = one"
6.1 --- a/src/HOL/Isar_Examples/Hoare.thy Fri Feb 21 17:06:48 2014 +0100
6.2 +++ b/src/HOL/Isar_Examples/Hoare.thy Fri Feb 21 18:23:11 2014 +0100
6.3 @@ -22,41 +22,39 @@
6.4 type_synonym 'a assn = "'a set"
6.5
6.6 datatype 'a com =
6.7 - Basic "'a => 'a"
6.8 + Basic "'a \<Rightarrow> 'a"
6.9 | Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60)
6.10 | Cond "'a bexp" "'a com" "'a com"
6.11 | While "'a bexp" "'a assn" "'a com"
6.12
6.13 abbreviation Skip ("SKIP")
6.14 - where "SKIP == Basic id"
6.15 + where "SKIP \<equiv> Basic id"
6.16
6.17 -type_synonym 'a sem = "'a => 'a => bool"
6.18 +type_synonym 'a sem = "'a \<Rightarrow> 'a \<Rightarrow> bool"
6.19
6.20 -primrec iter :: "nat => 'a bexp => 'a sem => 'a sem"
6.21 +primrec iter :: "nat \<Rightarrow> 'a bexp \<Rightarrow> 'a sem \<Rightarrow> 'a sem"
6.22 where
6.23 - "iter 0 b S s s' = (s ~: b & s = s')"
6.24 -| "iter (Suc n) b S s s' = (s : b & (EX s''. S s s'' & iter n b S s'' s'))"
6.25 + "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
6.26 +| "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
6.27
6.28 -primrec Sem :: "'a com => 'a sem"
6.29 +primrec Sem :: "'a com \<Rightarrow> 'a sem"
6.30 where
6.31 - "Sem (Basic f) s s' = (s' = f s)"
6.32 -| "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')"
6.33 -| "Sem (Cond b c1 c2) s s' =
6.34 - (if s : b then Sem c1 s s' else Sem c2 s s')"
6.35 -| "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')"
6.36 + "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
6.37 +| "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
6.38 +| "Sem (Cond b c1 c2) s s' \<longleftrightarrow>
6.39 + (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
6.40 +| "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
6.41
6.42 -definition Valid :: "'a bexp => 'a com => 'a bexp => bool"
6.43 - ("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
6.44 - where "|- P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' --> s : P --> s' : Q)"
6.45 -
6.46 -notation (xsymbols) Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
6.47 +definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
6.48 + ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
6.49 + where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
6.50
6.51 lemma ValidI [intro?]:
6.52 - "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"
6.53 + "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
6.54 by (simp add: Valid_def)
6.55
6.56 lemma ValidD [dest?]:
6.57 - "|- P c Q ==> Sem c s s' ==> s : P ==> s' : Q"
6.58 + "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
6.59 by (simp add: Valid_def)
6.60
6.61
6.62 @@ -71,12 +69,13 @@
6.63 to the state space. This subsumes the common rules of \name{skip}
6.64 and \name{assign}, as formulated in \S\ref{sec:hoare-isar}. *}
6.65
6.66 -theorem basic: "|- {s. f s : P} (Basic f) P"
6.67 +theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P"
6.68 proof
6.69 - fix s s' assume s: "s : {s. f s : P}"
6.70 + fix s s'
6.71 + assume s: "s \<in> {s. f s \<in> P}"
6.72 assume "Sem (Basic f) s s'"
6.73 then have "s' = f s" by simp
6.74 - with s show "s' : P" by simp
6.75 + with s show "s' \<in> P" by simp
6.76 qed
6.77
6.78 text {*
6.79 @@ -84,26 +83,27 @@
6.80 established in a straight forward manner as follows.
6.81 *}
6.82
6.83 -theorem seq: "|- P c1 Q ==> |- Q c2 R ==> |- P (c1; c2) R"
6.84 +theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R"
6.85 proof
6.86 - assume cmd1: "|- P c1 Q" and cmd2: "|- Q c2 R"
6.87 - fix s s' assume s: "s : P"
6.88 + assume cmd1: "\<turnstile> P c1 Q" and cmd2: "\<turnstile> Q c2 R"
6.89 + fix s s'
6.90 + assume s: "s \<in> P"
6.91 assume "Sem (c1; c2) s s'"
6.92 then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'"
6.93 by auto
6.94 - from cmd1 sem1 s have "s'' : Q" ..
6.95 - with cmd2 sem2 show "s' : R" ..
6.96 + from cmd1 sem1 s have "s'' \<in> Q" ..
6.97 + with cmd2 sem2 show "s' \<in> R" ..
6.98 qed
6.99
6.100 -theorem conseq: "P' <= P ==> |- P c Q ==> Q <= Q' ==> |- P' c Q'"
6.101 +theorem conseq: "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P' c Q'"
6.102 proof
6.103 - assume P'P: "P' <= P" and QQ': "Q <= Q'"
6.104 - assume cmd: "|- P c Q"
6.105 + assume P'P: "P' \<subseteq> P" and QQ': "Q \<subseteq> Q'"
6.106 + assume cmd: "\<turnstile> P c Q"
6.107 fix s s' :: 'a
6.108 assume sem: "Sem c s s'"
6.109 - assume "s : P'" with P'P have "s : P" ..
6.110 - with cmd sem have "s' : Q" ..
6.111 - with QQ' show "s' : Q'" ..
6.112 + assume "s : P'" with P'P have "s \<in> P" ..
6.113 + with cmd sem have "s' \<in> Q" ..
6.114 + with QQ' show "s' \<in> Q'" ..
6.115 qed
6.116
6.117 text {* The rule for conditional commands is directly reflected by the
6.118 @@ -111,26 +111,27 @@
6.119 which cases apply. *}
6.120
6.121 theorem cond:
6.122 - assumes case_b: "|- (P Int b) c1 Q"
6.123 - and case_nb: "|- (P Int -b) c2 Q"
6.124 - shows "|- P (Cond b c1 c2) Q"
6.125 + assumes case_b: "\<turnstile> (P \<inter> b) c1 Q"
6.126 + and case_nb: "\<turnstile> (P \<inter> -b) c2 Q"
6.127 + shows "\<turnstile> P (Cond b c1 c2) Q"
6.128 proof
6.129 - fix s s' assume s: "s : P"
6.130 + fix s s'
6.131 + assume s: "s \<in> P"
6.132 assume sem: "Sem (Cond b c1 c2) s s'"
6.133 - show "s' : Q"
6.134 + show "s' \<in> Q"
6.135 proof cases
6.136 - assume b: "s : b"
6.137 + assume b: "s \<in> b"
6.138 from case_b show ?thesis
6.139 proof
6.140 from sem b show "Sem c1 s s'" by simp
6.141 - from s b show "s : P Int b" by simp
6.142 + from s b show "s \<in> P \<inter> b" by simp
6.143 qed
6.144 next
6.145 - assume nb: "s ~: b"
6.146 + assume nb: "s \<notin> b"
6.147 from case_nb show ?thesis
6.148 proof
6.149 from sem nb show "Sem c2 s s'" by simp
6.150 - from s nb show "s : P Int -b" by simp
6.151 + from s nb show "s : P \<inter> -b" by simp
6.152 qed
6.153 qed
6.154 qed
6.155 @@ -143,22 +144,22 @@
6.156 of the semantics of \texttt{WHILE}. *}
6.157
6.158 theorem while:
6.159 - assumes body: "|- (P Int b) c P"
6.160 - shows "|- P (While b X c) (P Int -b)"
6.161 + assumes body: "\<turnstile> (P \<inter> b) c P"
6.162 + shows "\<turnstile> P (While b X c) (P \<inter> -b)"
6.163 proof
6.164 - fix s s' assume s: "s : P"
6.165 + fix s s' assume s: "s \<in> P"
6.166 assume "Sem (While b X c) s s'"
6.167 then obtain n where "iter n b (Sem c) s s'" by auto
6.168 - from this and s show "s' : P Int -b"
6.169 + from this and s show "s' \<in> P \<inter> -b"
6.170 proof (induct n arbitrary: s)
6.171 case 0
6.172 then show ?case by auto
6.173 next
6.174 case (Suc n)
6.175 - then obtain s'' where b: "s : b" and sem: "Sem c s s''"
6.176 + then obtain s'' where b: "s \<in> b" and sem: "Sem c s s''"
6.177 and iter: "iter n b (Sem c) s'' s'" by auto
6.178 - from Suc and b have "s : P Int b" by simp
6.179 - with body sem have "s'' : P" ..
6.180 + from Suc and b have "s \<in> P \<inter> b" by simp
6.181 + with body sem have "s'' \<in> P" ..
6.182 with iter show ?case by (rule Suc)
6.183 qed
6.184 qed
6.185 @@ -188,29 +189,26 @@
6.186 @{ML Syntax_Trans.quote_tr'},). *}
6.187
6.188 syntax
6.189 - "_quote" :: "'b => ('a => 'b)" ("(.'(_').)" [0] 1000)
6.190 - "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000)
6.191 + "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(.'(_').)" [0] 1000)
6.192 + "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000)
6.193 "_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
6.194 ("_[_'/\<acute>_]" [1000] 999)
6.195 - "_Assert" :: "'a => 'a set" ("(.{_}.)" [0] 1000)
6.196 - "_Assign" :: "idt => 'b => 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61)
6.197 - "_Cond" :: "'a bexp => 'a com => 'a com => 'a com"
6.198 + "_Assert" :: "'a \<Rightarrow> 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)
6.199 + "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61)
6.200 + "_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
6.201 ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
6.202 - "_While_inv" :: "'a bexp => 'a assn => 'a com => 'a com"
6.203 + "_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"
6.204 ("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61)
6.205 - "_While" :: "'a bexp => 'a com => 'a com"
6.206 + "_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"
6.207 ("(0WHILE _ //DO _ /OD)" [0, 0] 61)
6.208
6.209 -syntax (xsymbols)
6.210 - "_Assert" :: "'a => 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)
6.211 -
6.212 translations
6.213 - ".{b}." => "CONST Collect .(b)."
6.214 - "B [a/\<acute>x]" => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."
6.215 - "\<acute>x := a" => "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
6.216 - "IF b THEN c1 ELSE c2 FI" => "CONST Cond .{b}. c1 c2"
6.217 - "WHILE b INV i DO c OD" => "CONST While .{b}. i c"
6.218 - "WHILE b DO c OD" == "WHILE b INV CONST undefined DO c OD"
6.219 + "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect .(b)."
6.220 + "B [a/\<acute>x]" \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
6.221 + "\<acute>x := a" \<rightharpoonup> "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
6.222 + "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
6.223 + "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
6.224 + "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
6.225
6.226 parse_translation {*
6.227 let
6.228 @@ -259,28 +257,28 @@
6.229 calculational proofs, with the inclusion expressed in terms of sets
6.230 or predicates. Reversed order is supported as well. *}
6.231
6.232 -lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q"
6.233 +lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q"
6.234 by (unfold Valid_def) blast
6.235 -lemma [trans] : "P' <= P ==> |- P c Q ==> |- P' c Q"
6.236 +lemma [trans] : "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P' c Q"
6.237 by (unfold Valid_def) blast
6.238
6.239 -lemma [trans]: "Q <= Q' ==> |- P c Q ==> |- P c Q'"
6.240 +lemma [trans]: "Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P c Q'"
6.241 by (unfold Valid_def) blast
6.242 -lemma [trans]: "|- P c Q ==> Q <= Q' ==> |- P c Q'"
6.243 +lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q'"
6.244 by (unfold Valid_def) blast
6.245
6.246 lemma [trans]:
6.247 - "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"
6.248 + "\<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> (\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
6.249 by (simp add: Valid_def)
6.250 lemma [trans]:
6.251 - "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"
6.252 + "(\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
6.253 by (simp add: Valid_def)
6.254
6.255 lemma [trans]:
6.256 - "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."
6.257 + "\<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> (\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
6.258 by (simp add: Valid_def)
6.259 lemma [trans]:
6.260 - "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."
6.261 + "(\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
6.262 by (simp add: Valid_def)
6.263
6.264
6.265 @@ -289,13 +287,13 @@
6.266 instances for any number of basic assignments, without producing
6.267 additional verification conditions.} *}
6.268
6.269 -lemma skip [intro?]: "|- P SKIP P"
6.270 +lemma skip [intro?]: "\<turnstile> P SKIP P"
6.271 proof -
6.272 - have "|- {s. id s : P} SKIP P" by (rule basic)
6.273 + have "\<turnstile> {s. id s \<in> P} SKIP P" by (rule basic)
6.274 then show ?thesis by simp
6.275 qed
6.276
6.277 -lemma assign: "|- P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
6.278 +lemma assign: "\<turnstile> P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
6.279 by (rule basic)
6.280
6.281 text {* Note that above formulation of assignment corresponds to our
6.282 @@ -315,7 +313,7 @@
6.283
6.284 lemmas [trans, intro?] = seq
6.285
6.286 -lemma seq_assoc [simp]: "( |- P c1;(c2;c3) Q) = ( |- P (c1;c2);c3 Q)"
6.287 +lemma seq_assoc [simp]: "\<turnstile> P c1;(c2;c3) Q \<longleftrightarrow> \<turnstile> P (c1;c2);c3 Q"
6.288 by (auto simp add: Valid_def)
6.289
6.290 text {* Conditional statements. *}
6.291 @@ -323,30 +321,30 @@
6.292 lemmas [trans, intro?] = cond
6.293
6.294 lemma [trans, intro?]:
6.295 - "|- .{\<acute>P & \<acute>b}. c1 Q
6.296 - ==> |- .{\<acute>P & ~ \<acute>b}. c2 Q
6.297 - ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
6.298 + "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c1 Q
6.299 + \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace> c2 Q
6.300 + \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> IF \<acute>b THEN c1 ELSE c2 FI Q"
6.301 by (rule cond) (simp_all add: Valid_def)
6.302
6.303 text {* While statements --- with optional invariant. *}
6.304
6.305 lemma [intro?]:
6.306 - "|- (P Int b) c P ==> |- P (While b P c) (P Int -b)"
6.307 + "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
6.308 by (rule while)
6.309
6.310 lemma [intro?]:
6.311 - "|- (P Int b) c P ==> |- P (While b undefined c) (P Int -b)"
6.312 + "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
6.313 by (rule while)
6.314
6.315
6.316 lemma [intro?]:
6.317 - "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
6.318 - ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."
6.319 + "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
6.320 + \<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>"
6.321 by (simp add: while Collect_conj_eq Collect_neg_eq)
6.322
6.323 lemma [intro?]:
6.324 - "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
6.325 - ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."
6.326 + "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
6.327 + \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
6.328 by (simp add: while Collect_conj_eq Collect_neg_eq)
6.329
6.330
6.331 @@ -378,13 +376,9 @@
6.332 by (auto simp: Valid_def)
6.333
6.334 lemma iter_aux:
6.335 - "\<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
6.336 - (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)"
6.337 - apply(induct n)
6.338 - apply clarsimp
6.339 - apply (simp (no_asm_use))
6.340 - apply blast
6.341 - done
6.342 + "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
6.343 + (\<And>s s'. s \<in> I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> I \<and> s' \<notin> b)"
6.344 + by (induct n) auto
6.345
6.346 lemma WhileRule:
6.347 "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
7.1 --- a/src/HOL/Isar_Examples/Hoare_Ex.thy Fri Feb 21 17:06:48 2014 +0100
7.2 +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Fri Feb 21 18:23:11 2014 +0100
7.3 @@ -32,7 +32,7 @@
7.4 text {* Using the basic @{text assign} rule directly is a bit
7.5 cumbersome. *}
7.6
7.7 -lemma "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
7.8 +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>"
7.9 by (rule assign)
7.10
7.11 text {* Certainly we want the state modification already done, e.g.\
7.12 @@ -40,31 +40,31 @@
7.13 update for us; we may apply the Simplifier afterwards to achieve
7.14 ``obvious'' consequences as well. *}
7.15
7.16 -lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."
7.17 +lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>N := 10 \<lbrace>\<acute>N = 10\<rbrace>"
7.18 by hoare
7.19
7.20 -lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
7.21 +lemma "\<turnstile> \<lbrace>2 * \<acute>N = 10\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
7.22 by hoare
7.23
7.24 -lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
7.25 +lemma "\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
7.26 by hoare simp
7.27
7.28 -lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
7.29 +lemma "\<turnstile> \<lbrace>\<acute>N + 1 = a + 1\<rbrace> \<acute>N := \<acute>N + 1 \<lbrace>\<acute>N = a + 1\<rbrace>"
7.30 by hoare
7.31
7.32 -lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
7.33 +lemma "\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N := \<acute>N + 1 \<lbrace>\<acute>N = a + 1\<rbrace>"
7.34 by hoare simp
7.35
7.36 -lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
7.37 +lemma "\<turnstile> \<lbrace>a = a \<and> b = b\<rbrace> \<acute>M := a; \<acute>N := b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
7.38 by hoare
7.39
7.40 -lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
7.41 +lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>M := a; \<acute>N := b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
7.42 by hoare simp
7.43
7.44 lemma
7.45 - "|- .{\<acute>M = a & \<acute>N = b}.
7.46 + "\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
7.47 \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I
7.48 - .{\<acute>M = b & \<acute>N = a}."
7.49 + \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
7.50 by hoare simp
7.51
7.52 text {* It is important to note that statements like the following one
7.53 @@ -72,10 +72,10 @@
7.54 extra-logical nature of record fields, we cannot formulate a theorem
7.55 relating record selectors and updates schematically. *}
7.56
7.57 -lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."
7.58 +lemma "\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N := \<acute>N \<lbrace>\<acute>N = a\<rbrace>"
7.59 by hoare
7.60
7.61 -lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}."
7.62 +lemma "\<turnstile> \<lbrace>\<acute>x = a\<rbrace> \<acute>x := \<acute>x \<lbrace>\<acute>x = a\<rbrace>"
7.63 oops
7.64
7.65 lemma
7.66 @@ -88,27 +88,27 @@
7.67 rule in order to achieve the intended precondition. Certainly, the
7.68 \name{hoare} method is able to handle this case, too. *}
7.69
7.70 -lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
7.71 +lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
7.72 proof -
7.73 - have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}."
7.74 + have "\<lbrace>\<acute>M = \<acute>N\<rbrace> \<subseteq> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace>"
7.75 by auto
7.76 - also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
7.77 + also have "\<turnstile> \<dots> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
7.78 by hoare
7.79 finally show ?thesis .
7.80 qed
7.81
7.82 -lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
7.83 +lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
7.84 proof -
7.85 - have "!!m n::nat. m = n --> m + 1 ~= n"
7.86 + have "\<And>m n::nat. m = n \<longrightarrow> m + 1 \<noteq> n"
7.87 -- {* inclusion of assertions expressed in ``pure'' logic, *}
7.88 -- {* without mentioning the state space *}
7.89 by simp
7.90 - also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
7.91 + also have "\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
7.92 by hoare
7.93 finally show ?thesis .
7.94 qed
7.95
7.96 -lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
7.97 +lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
7.98 by hoare simp
7.99
7.100
7.101 @@ -120,24 +120,24 @@
7.102 structured proof based on single-step Hoare rules. *}
7.103
7.104 lemma
7.105 - "|- .{\<acute>M = 0 & \<acute>S = 0}.
7.106 - WHILE \<acute>M ~= a
7.107 + "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
7.108 + WHILE \<acute>M \<noteq> a
7.109 DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
7.110 - .{\<acute>S = a * b}."
7.111 + \<lbrace>\<acute>S = a * b\<rbrace>"
7.112 proof -
7.113 - let "|- _ ?while _" = ?thesis
7.114 - let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}."
7.115 + let "\<turnstile> _ ?while _" = ?thesis
7.116 + let "\<lbrace>\<acute>?inv\<rbrace>" = "\<lbrace>\<acute>S = \<acute>M * b\<rbrace>"
7.117
7.118 - have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto
7.119 - also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}."
7.120 + have "\<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> \<subseteq> \<lbrace>\<acute>?inv\<rbrace>" by auto
7.121 + also have "\<turnstile> \<dots> ?while \<lbrace>\<acute>?inv \<and> \<not> (\<acute>M \<noteq> a)\<rbrace>"
7.122 proof
7.123 let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1"
7.124 - have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}."
7.125 + have "\<lbrace>\<acute>?inv \<and> \<acute>M \<noteq> a\<rbrace> \<subseteq> \<lbrace>\<acute>S + b = (\<acute>M + 1) * b\<rbrace>"
7.126 by auto
7.127 - also have "|- ... ?c .{\<acute>?inv}." by hoare
7.128 - finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." .
7.129 + also have "\<turnstile> \<dots> ?c \<lbrace>\<acute>?inv\<rbrace>" by hoare
7.130 + finally show "\<turnstile> \<lbrace>\<acute>?inv \<and> \<acute>M \<noteq> a\<rbrace> ?c \<lbrace>\<acute>?inv\<rbrace>" .
7.131 qed
7.132 - also have "... <= .{\<acute>S = a * b}." by auto
7.133 + also have "\<dots> \<subseteq> \<lbrace>\<acute>S = a * b\<rbrace>" by auto
7.134 finally show ?thesis .
7.135 qed
7.136
7.137 @@ -147,11 +147,11 @@
7.138 specify the \texttt{WHILE} loop invariant in the original statement. *}
7.139
7.140 lemma
7.141 - "|- .{\<acute>M = 0 & \<acute>S = 0}.
7.142 - WHILE \<acute>M ~= a
7.143 - INV .{\<acute>S = \<acute>M * b}.
7.144 + "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
7.145 + WHILE \<acute>M \<noteq> a
7.146 + INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
7.147 DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
7.148 - .{\<acute>S = a * b}."
7.149 + \<lbrace>\<acute>S = a * b\<rbrace>"
7.150 by hoare auto
7.151
7.152
7.153 @@ -168,37 +168,37 @@
7.154 the state space. *}
7.155
7.156 theorem
7.157 - "|- .{True}.
7.158 + "\<turnstile> \<lbrace>True\<rbrace>
7.159 \<acute>S := 0; \<acute>I := 1;
7.160 - WHILE \<acute>I ~= n
7.161 + WHILE \<acute>I \<noteq> n
7.162 DO
7.163 \<acute>S := \<acute>S + \<acute>I;
7.164 \<acute>I := \<acute>I + 1
7.165 OD
7.166 - .{\<acute>S = (SUM j<n. j)}."
7.167 - (is "|- _ (_; ?while) _")
7.168 + \<lbrace>\<acute>S = (\<Sum>j<n. j)\<rbrace>"
7.169 + (is "\<turnstile> _ (_; ?while) _")
7.170 proof -
7.171 - let ?sum = "\<lambda>k::nat. SUM j<k. j"
7.172 + let ?sum = "\<lambda>k::nat. \<Sum>j<k. j"
7.173 let ?inv = "\<lambda>s i::nat. s = ?sum i"
7.174
7.175 - have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
7.176 + have "\<turnstile> \<lbrace>True\<rbrace> \<acute>S := 0; \<acute>I := 1 \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
7.177 proof -
7.178 - have "True --> 0 = ?sum 1"
7.179 + have "True \<longrightarrow> 0 = ?sum 1"
7.180 by simp
7.181 - also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
7.182 + also have "\<turnstile> \<lbrace>\<dots>\<rbrace> \<acute>S := 0; \<acute>I := 1 \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
7.183 by hoare
7.184 finally show ?thesis .
7.185 qed
7.186 - also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}."
7.187 + also have "\<turnstile> \<dots> ?while \<lbrace>?inv \<acute>S \<acute>I \<and> \<not> \<acute>I \<noteq> n\<rbrace>"
7.188 proof
7.189 let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
7.190 - have "!!s i. ?inv s i & i ~= n --> ?inv (s + i) (i + 1)"
7.191 + have "\<And>s i. ?inv s i \<and> i \<noteq> n \<longrightarrow> ?inv (s + i) (i + 1)"
7.192 by simp
7.193 - also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}."
7.194 + also have "\<turnstile> \<lbrace>\<acute>S + \<acute>I = ?sum (\<acute>I + 1)\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
7.195 by hoare
7.196 - finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." .
7.197 + finally show "\<turnstile> \<lbrace>?inv \<acute>S \<acute>I \<and> \<acute>I \<noteq> n\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>" .
7.198 qed
7.199 - also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n"
7.200 + also have "\<And>s i. s = ?sum i \<and> \<not> i \<noteq> n \<longrightarrow> s = ?sum n"
7.201 by simp
7.202 finally show ?thesis .
7.203 qed
7.204 @@ -208,27 +208,29 @@
7.205 structured manner. *}
7.206
7.207 theorem
7.208 - "|- .{True}.
7.209 + "\<turnstile> \<lbrace>True\<rbrace>
7.210 \<acute>S := 0; \<acute>I := 1;
7.211 - WHILE \<acute>I ~= n
7.212 - INV .{\<acute>S = (SUM j<\<acute>I. j)}.
7.213 + WHILE \<acute>I \<noteq> n
7.214 + INV \<lbrace>\<acute>S = (\<Sum>j<\<acute>I. j)\<rbrace>
7.215 DO
7.216 \<acute>S := \<acute>S + \<acute>I;
7.217 \<acute>I := \<acute>I + 1
7.218 OD
7.219 - .{\<acute>S = (SUM j<n. j)}."
7.220 + \<lbrace>\<acute>S = (\<Sum>j<n. j)\<rbrace>"
7.221 proof -
7.222 - let ?sum = "\<lambda>k::nat. SUM j<k. j"
7.223 + let ?sum = "\<lambda>k::nat. \<Sum>j<k. j"
7.224 let ?inv = "\<lambda>s i::nat. s = ?sum i"
7.225
7.226 show ?thesis
7.227 proof hoare
7.228 show "?inv 0 1" by simp
7.229 next
7.230 - fix s i assume "?inv s i & i ~= n"
7.231 + fix s i
7.232 + assume "?inv s i \<and> i \<noteq> n"
7.233 then show "?inv (s + i) (i + 1)" by simp
7.234 next
7.235 - fix s i assume "?inv s i & ~ i ~= n"
7.236 + fix s i
7.237 + assume "?inv s i \<and> \<not> i \<noteq> n"
7.238 then show "s = ?sum n" by simp
7.239 qed
7.240 qed
7.241 @@ -237,15 +239,15 @@
7.242 provided that the invariant is given beforehand. *}
7.243
7.244 theorem
7.245 - "|- .{True}.
7.246 + "\<turnstile> \<lbrace>True\<rbrace>
7.247 \<acute>S := 0; \<acute>I := 1;
7.248 - WHILE \<acute>I ~= n
7.249 - INV .{\<acute>S = (SUM j<\<acute>I. j)}.
7.250 + WHILE \<acute>I \<noteq> n
7.251 + INV \<lbrace>\<acute>S = (\<Sum>j<\<acute>I. j)\<rbrace>
7.252 DO
7.253 \<acute>S := \<acute>S + \<acute>I;
7.254 \<acute>I := \<acute>I + 1
7.255 OD
7.256 - .{\<acute>S = (SUM j<n. j)}."
7.257 + \<lbrace>\<acute>S = (\<Sum>j<n. j)\<rbrace>"
7.258 by hoare auto
7.259
7.260
7.261 @@ -273,18 +275,18 @@
7.262 by (induct n) simp_all
7.263
7.264 lemma
7.265 - "|- .{i = \<acute>I & \<acute>time = 0}.
7.266 - timeit (
7.267 - WHILE \<acute>I \<noteq> 0
7.268 - INV .{2 *\<acute> time + \<acute>I * \<acute>I + 5 * \<acute>I = i * i + 5 * i}.
7.269 - DO
7.270 - \<acute>J := \<acute>I;
7.271 - WHILE \<acute>J \<noteq> 0
7.272 - INV .{0 < \<acute>I & 2 * \<acute>time + \<acute>I * \<acute>I + 3 * \<acute>I + 2 * \<acute>J - 2 = i * i + 5 * i}.
7.273 - DO \<acute>J := \<acute>J - 1 OD;
7.274 - \<acute>I := \<acute>I - 1
7.275 - OD
7.276 - ) .{2*\<acute>time = i*i + 5*i}."
7.277 + "\<turnstile> \<lbrace>i = \<acute>I \<and> \<acute>time = 0\<rbrace>
7.278 + (timeit
7.279 + (WHILE \<acute>I \<noteq> 0
7.280 + INV \<lbrace>2 *\<acute> time + \<acute>I * \<acute>I + 5 * \<acute>I = i * i + 5 * i\<rbrace>
7.281 + DO
7.282 + \<acute>J := \<acute>I;
7.283 + WHILE \<acute>J \<noteq> 0
7.284 + 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>
7.285 + DO \<acute>J := \<acute>J - 1 OD;
7.286 + \<acute>I := \<acute>I - 1
7.287 + OD))
7.288 + \<lbrace>2 * \<acute>time = i * i + 5 * i\<rbrace>"
7.289 apply simp
7.290 apply hoare
7.291 apply simp
8.1 --- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Fri Feb 21 17:06:48 2014 +0100
8.2 +++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Fri Feb 21 18:23:11 2014 +0100
8.3 @@ -14,40 +14,40 @@
8.4
8.5 subsection {* Tilings *}
8.6
8.7 -inductive_set tiling :: "'a set set => 'a set set"
8.8 +inductive_set tiling :: "'a set set \<Rightarrow> 'a set set"
8.9 for A :: "'a set set"
8.10 where
8.11 - empty: "{} : tiling A"
8.12 -| Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A"
8.13 + empty: "{} \<in> tiling A"
8.14 +| Un: "a \<in> A \<Longrightarrow> t \<in> tiling A \<Longrightarrow> a \<subseteq> - t \<Longrightarrow> a \<union> t \<in> tiling A"
8.15
8.16
8.17 text "The union of two disjoint tilings is a tiling."
8.18
8.19 lemma tiling_Un:
8.20 - assumes "t : tiling A"
8.21 - and "u : tiling A"
8.22 - and "t Int u = {}"
8.23 - shows "t Un u : tiling A"
8.24 + assumes "t \<in> tiling A"
8.25 + and "u \<in> tiling A"
8.26 + and "t \<inter> u = {}"
8.27 + shows "t \<union> u \<in> tiling A"
8.28 proof -
8.29 let ?T = "tiling A"
8.30 - from `t : ?T` and `t Int u = {}`
8.31 - show "t Un u : ?T"
8.32 + from `t \<in> ?T` and `t \<inter> u = {}`
8.33 + show "t \<union> u \<in> ?T"
8.34 proof (induct t)
8.35 case empty
8.36 - with `u : ?T` show "{} Un u : ?T" by simp
8.37 + with `u \<in> ?T` show "{} \<union> u \<in> ?T" by simp
8.38 next
8.39 case (Un a t)
8.40 - show "(a Un t) Un u : ?T"
8.41 + show "(a \<union> t) \<union> u \<in> ?T"
8.42 proof -
8.43 - have "a Un (t Un u) : ?T"
8.44 - using `a : A`
8.45 + have "a \<union> (t \<union> u) \<in> ?T"
8.46 + using `a \<in> A`
8.47 proof (rule tiling.Un)
8.48 - from `(a Un t) Int u = {}` have "t Int u = {}" by blast
8.49 - then show "t Un u: ?T" by (rule Un)
8.50 - from `a <= - t` and `(a Un t) Int u = {}`
8.51 - show "a <= - (t Un u)" by blast
8.52 + from `(a \<union> t) \<inter> u = {}` have "t \<inter> u = {}" by blast
8.53 + then show "t \<union> u \<in> ?T" by (rule Un)
8.54 + from `a \<subseteq> - t` and `(a \<union> t) \<inter> u = {}`
8.55 + show "a \<subseteq> - (t \<union> u)" by blast
8.56 qed
8.57 - also have "a Un (t Un u) = (a Un t) Un u"
8.58 + also have "a \<union> (t \<union> u) = (a \<union> t) \<union> u"
8.59 by (simp only: Un_assoc)
8.60 finally show ?thesis .
8.61 qed
8.62 @@ -57,22 +57,21 @@
8.63
8.64 subsection {* Basic properties of ``below'' *}
8.65
8.66 -definition below :: "nat => nat set"
8.67 +definition below :: "nat \<Rightarrow> nat set"
8.68 where "below n = {i. i < n}"
8.69
8.70 -lemma below_less_iff [iff]: "(i: below k) = (i < k)"
8.71 +lemma below_less_iff [iff]: "i \<in> below k \<longleftrightarrow> i < k"
8.72 by (simp add: below_def)
8.73
8.74 lemma below_0: "below 0 = {}"
8.75 by (simp add: below_def)
8.76
8.77 -lemma Sigma_Suc1:
8.78 - "m = n + 1 ==> below m <*> B = ({n} <*> B) Un (below n <*> B)"
8.79 +lemma Sigma_Suc1: "m = n + 1 \<Longrightarrow> below m \<times> B = ({n} \<times> B) \<union> (below n \<times> B)"
8.80 by (simp add: below_def less_Suc_eq) blast
8.81
8.82 lemma Sigma_Suc2:
8.83 - "m = n + 2 ==> A <*> below m =
8.84 - (A <*> {n}) Un (A <*> {n + 1}) Un (A <*> below n)"
8.85 + "m = n + 2 \<Longrightarrow>
8.86 + A \<times> below m = (A \<times> {n}) \<union> (A \<times> {n + 1}) \<union> (A \<times> below n)"
8.87 by (auto simp add: below_def)
8.88
8.89 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2
8.90 @@ -80,22 +79,22 @@
8.91
8.92 subsection {* Basic properties of ``evnodd'' *}
8.93
8.94 -definition evnodd :: "(nat * nat) set => nat => (nat * nat) set"
8.95 - where "evnodd A b = A Int {(i, j). (i + j) mod 2 = b}"
8.96 +definition evnodd :: "(nat \<times> nat) set \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set"
8.97 + where "evnodd A b = A \<inter> {(i, j). (i + j) mod 2 = b}"
8.98
8.99 -lemma evnodd_iff: "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)"
8.100 +lemma evnodd_iff: "(i, j) \<in> evnodd A b \<longleftrightarrow> (i, j) \<in> A \<and> (i + j) mod 2 = b"
8.101 by (simp add: evnodd_def)
8.102
8.103 -lemma evnodd_subset: "evnodd A b <= A"
8.104 +lemma evnodd_subset: "evnodd A b \<subseteq> A"
8.105 unfolding evnodd_def by (rule Int_lower1)
8.106
8.107 -lemma evnoddD: "x : evnodd A b ==> x : A"
8.108 +lemma evnoddD: "x \<in> evnodd A b \<Longrightarrow> x \<in> A"
8.109 by (rule subsetD) (rule evnodd_subset)
8.110
8.111 -lemma evnodd_finite: "finite A ==> finite (evnodd A b)"
8.112 +lemma evnodd_finite: "finite A \<Longrightarrow> finite (evnodd A b)"
8.113 by (rule finite_subset) (rule evnodd_subset)
8.114
8.115 -lemma evnodd_Un: "evnodd (A Un B) b = evnodd A b Un evnodd B b"
8.116 +lemma evnodd_Un: "evnodd (A \<union> B) b = evnodd A b \<union> evnodd B b"
8.117 unfolding evnodd_def by blast
8.118
8.119 lemma evnodd_Diff: "evnodd (A - B) b = evnodd A b - evnodd B b"
8.120 @@ -112,60 +111,60 @@
8.121
8.122 subsection {* Dominoes *}
8.123
8.124 -inductive_set domino :: "(nat * nat) set set"
8.125 +inductive_set domino :: "(nat \<times> nat) set set"
8.126 where
8.127 - horiz: "{(i, j), (i, j + 1)} : domino"
8.128 -| vertl: "{(i, j), (i + 1, j)} : domino"
8.129 + horiz: "{(i, j), (i, j + 1)} \<in> domino"
8.130 +| vertl: "{(i, j), (i + 1, j)} \<in> domino"
8.131
8.132 lemma dominoes_tile_row:
8.133 - "{i} <*> below (2 * n) : tiling domino"
8.134 - (is "?B n : ?T")
8.135 + "{i} \<times> below (2 * n) \<in> tiling domino"
8.136 + (is "?B n \<in> ?T")
8.137 proof (induct n)
8.138 case 0
8.139 show ?case by (simp add: below_0 tiling.empty)
8.140 next
8.141 case (Suc n)
8.142 - let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
8.143 - have "?B (Suc n) = ?a Un ?B n"
8.144 + let ?a = "{i} \<times> {2 * n + 1} \<union> {i} \<times> {2 * n}"
8.145 + have "?B (Suc n) = ?a \<union> ?B n"
8.146 by (auto simp add: Sigma_Suc Un_assoc)
8.147 - also have "... : ?T"
8.148 + also have "\<dots> \<in> ?T"
8.149 proof (rule tiling.Un)
8.150 - have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
8.151 + have "{(i, 2 * n), (i, 2 * n + 1)} \<in> domino"
8.152 by (rule domino.horiz)
8.153 also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast
8.154 - finally show "... : domino" .
8.155 - show "?B n : ?T" by (rule Suc)
8.156 - show "?a <= - ?B n" by blast
8.157 + finally show "\<dots> \<in> domino" .
8.158 + show "?B n \<in> ?T" by (rule Suc)
8.159 + show "?a \<subseteq> - ?B n" by blast
8.160 qed
8.161 finally show ?case .
8.162 qed
8.163
8.164 lemma dominoes_tile_matrix:
8.165 - "below m <*> below (2 * n) : tiling domino"
8.166 - (is "?B m : ?T")
8.167 + "below m \<times> below (2 * n) \<in> tiling domino"
8.168 + (is "?B m \<in> ?T")
8.169 proof (induct m)
8.170 case 0
8.171 show ?case by (simp add: below_0 tiling.empty)
8.172 next
8.173 case (Suc m)
8.174 - let ?t = "{m} <*> below (2 * n)"
8.175 - have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
8.176 - also have "... : ?T"
8.177 + let ?t = "{m} \<times> below (2 * n)"
8.178 + have "?B (Suc m) = ?t \<union> ?B m" by (simp add: Sigma_Suc)
8.179 + also have "\<dots> \<in> ?T"
8.180 proof (rule tiling_Un)
8.181 - show "?t : ?T" by (rule dominoes_tile_row)
8.182 - show "?B m : ?T" by (rule Suc)
8.183 - show "?t Int ?B m = {}" by blast
8.184 + show "?t \<in> ?T" by (rule dominoes_tile_row)
8.185 + show "?B m \<in> ?T" by (rule Suc)
8.186 + show "?t \<inter> ?B m = {}" by blast
8.187 qed
8.188 finally show ?case .
8.189 qed
8.190
8.191 lemma domino_singleton:
8.192 - assumes "d : domino"
8.193 + assumes "d \<in> domino"
8.194 and "b < 2"
8.195 - shows "EX i j. evnodd d b = {(i, j)}" (is "?P d")
8.196 + shows "\<exists>i j. evnodd d b = {(i, j)}" (is "?P d")
8.197 using assms
8.198 proof induct
8.199 - from `b < 2` have b_cases: "b = 0 | b = 1" by arith
8.200 + from `b < 2` have b_cases: "b = 0 \<or> b = 1" by arith
8.201 fix i j
8.202 note [simp] = evnodd_empty evnodd_insert mod_Suc
8.203 from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
8.204 @@ -173,7 +172,7 @@
8.205 qed
8.206
8.207 lemma domino_finite:
8.208 - assumes "d: domino"
8.209 + assumes "d \<in> domino"
8.210 shows "finite d"
8.211 using assms
8.212 proof induct
8.213 @@ -186,18 +185,19 @@
8.214 subsection {* Tilings of dominoes *}
8.215
8.216 lemma tiling_domino_finite:
8.217 - assumes t: "t : tiling domino" (is "t : ?T")
8.218 + assumes t: "t \<in> tiling domino" (is "t \<in> ?T")
8.219 shows "finite t" (is "?F t")
8.220 using t
8.221 proof induct
8.222 show "?F {}" by (rule finite.emptyI)
8.223 fix a t assume "?F t"
8.224 - assume "a : domino" then have "?F a" by (rule domino_finite)
8.225 - from this and `?F t` show "?F (a Un t)" by (rule finite_UnI)
8.226 + assume "a \<in> domino"
8.227 + then have "?F a" by (rule domino_finite)
8.228 + from this and `?F t` show "?F (a \<union> t)" by (rule finite_UnI)
8.229 qed
8.230
8.231 lemma tiling_domino_01:
8.232 - assumes t: "t : tiling domino" (is "t : ?T")
8.233 + assumes t: "t \<in> tiling domino" (is "t \<in> ?T")
8.234 shows "card (evnodd t 0) = card (evnodd t 1)"
8.235 using t
8.236 proof induct
8.237 @@ -207,33 +207,34 @@
8.238 case (Un a t)
8.239 let ?e = evnodd
8.240 note hyp = `card (?e t 0) = card (?e t 1)`
8.241 - and at = `a <= - t`
8.242 + and at = `a \<subseteq> - t`
8.243 have card_suc:
8.244 - "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
8.245 + "\<And>b. b < 2 \<Longrightarrow> card (?e (a \<union> t) b) = Suc (card (?e t b))"
8.246 proof -
8.247 - fix b :: nat assume "b < 2"
8.248 - have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
8.249 + fix b :: nat
8.250 + assume "b < 2"
8.251 + have "?e (a \<union> t) b = ?e a b \<union> ?e t b" by (rule evnodd_Un)
8.252 also obtain i j where e: "?e a b = {(i, j)}"
8.253 proof -
8.254 from `a \<in> domino` and `b < 2`
8.255 - have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
8.256 + have "\<exists>i j. ?e a b = {(i, j)}" by (rule domino_singleton)
8.257 then show ?thesis by (blast intro: that)
8.258 qed
8.259 - also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
8.260 - also have "card ... = Suc (card (?e t b))"
8.261 + also have "\<dots> \<union> ?e t b = insert (i, j) (?e t b)" by simp
8.262 + also have "card \<dots> = Suc (card (?e t b))"
8.263 proof (rule card_insert_disjoint)
8.264 from `t \<in> tiling domino` have "finite t"
8.265 by (rule tiling_domino_finite)
8.266 then show "finite (?e t b)"
8.267 by (rule evnodd_finite)
8.268 - from e have "(i, j) : ?e a b" by simp
8.269 - with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
8.270 + from e have "(i, j) \<in> ?e a b" by simp
8.271 + with at show "(i, j) \<notin> ?e t b" by (blast dest: evnoddD)
8.272 qed
8.273 finally show "?thesis b" .
8.274 qed
8.275 - then have "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
8.276 + then have "card (?e (a \<union> t) 0) = Suc (card (?e t 0))" by simp
8.277 also from hyp have "card (?e t 0) = card (?e t 1)" .
8.278 - also from card_suc have "Suc ... = card (?e (a Un t) 1)"
8.279 + also from card_suc have "Suc \<dots> = card (?e (a \<union> t) 1)"
8.280 by simp
8.281 finally show ?case .
8.282 qed
8.283 @@ -241,23 +242,23 @@
8.284
8.285 subsection {* Main theorem *}
8.286
8.287 -definition mutilated_board :: "nat => nat => (nat * nat) set"
8.288 +definition mutilated_board :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set"
8.289 where
8.290 "mutilated_board m n =
8.291 - below (2 * (m + 1)) <*> below (2 * (n + 1))
8.292 + below (2 * (m + 1)) \<times> below (2 * (n + 1))
8.293 - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
8.294
8.295 -theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"
8.296 +theorem mutil_not_tiling: "mutilated_board m n \<notin> tiling domino"
8.297 proof (unfold mutilated_board_def)
8.298 let ?T = "tiling domino"
8.299 - let ?t = "below (2 * (m + 1)) <*> below (2 * (n + 1))"
8.300 + let ?t = "below (2 * (m + 1)) \<times> below (2 * (n + 1))"
8.301 let ?t' = "?t - {(0, 0)}"
8.302 let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"
8.303
8.304 - show "?t'' ~: ?T"
8.305 + show "?t'' \<notin> ?T"
8.306 proof
8.307 - have t: "?t : ?T" by (rule dominoes_tile_matrix)
8.308 - assume t'': "?t'' : ?T"
8.309 + have t: "?t \<in> ?T" by (rule dominoes_tile_matrix)
8.310 + assume t'': "?t'' \<in> ?T"
8.311
8.312 let ?e = evnodd
8.313 have fin: "finite (?e ?t 0)"
8.314 @@ -271,23 +272,23 @@
8.315 proof (rule card_Diff1_less)
8.316 from _ fin show "finite (?e ?t' 0)"
8.317 by (rule finite_subset) auto
8.318 - show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0" by simp
8.319 + show "(2 * m + 1, 2 * n + 1) \<in> ?e ?t' 0" by simp
8.320 qed
8.321 then show ?thesis by simp
8.322 qed
8.323 - also have "... < card (?e ?t 0)"
8.324 + also have "\<dots> < card (?e ?t 0)"
8.325 proof -
8.326 - have "(0, 0) : ?e ?t 0" by simp
8.327 + have "(0, 0) \<in> ?e ?t 0" by simp
8.328 with fin have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"
8.329 by (rule card_Diff1_less)
8.330 then show ?thesis by simp
8.331 qed
8.332 - also from t have "... = card (?e ?t 1)"
8.333 + also from t have "\<dots> = card (?e ?t 1)"
8.334 by (rule tiling_domino_01)
8.335 also have "?e ?t 1 = ?e ?t'' 1" by simp
8.336 - also from t'' have "card ... = card (?e ?t'' 0)"
8.337 + also from t'' have "card \<dots> = card (?e ?t'' 0)"
8.338 by (rule tiling_domino_01 [symmetric])
8.339 - finally have "... < ..." . then show False ..
8.340 + finally have "\<dots> < \<dots>" . then show False ..
8.341 qed
8.342 qed
8.343
9.1 --- a/src/HOL/Isar_Examples/Nested_Datatype.thy Fri Feb 21 17:06:48 2014 +0100
9.2 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Fri Feb 21 18:23:11 2014 +0100
9.3 @@ -7,12 +7,11 @@
9.4 subsection {* Terms and substitution *}
9.5
9.6 datatype ('a, 'b) "term" =
9.7 - Var 'a
9.8 - | App 'b "('a, 'b) term list"
9.9 + Var 'a
9.10 +| App 'b "('a, 'b) term list"
9.11
9.12 -primrec
9.13 - subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
9.14 - subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
9.15 +primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term"
9.16 + and subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
9.17 where
9.18 "subst_term f (Var a) = f a"
9.19 | "subst_term f (App b ts) = App b (subst_term_list f ts)"
9.20 @@ -24,18 +23,18 @@
9.21 text {* \medskip A simple lemma about composition of substitutions. *}
9.22
9.23 lemma
9.24 - "subst_term (subst_term f1 o f2) t =
9.25 + "subst_term (subst_term f1 \<circ> f2) t =
9.26 subst_term f1 (subst_term f2 t)"
9.27 and
9.28 - "subst_term_list (subst_term f1 o f2) ts =
9.29 + "subst_term_list (subst_term f1 \<circ> f2) ts =
9.30 subst_term_list f1 (subst_term_list f2 ts)"
9.31 by (induct t and ts) simp_all
9.32
9.33 -lemma "subst_term (subst_term f1 o f2) t =
9.34 +lemma "subst_term (subst_term f1 \<circ> f2) t =
9.35 subst_term f1 (subst_term f2 t)"
9.36 proof -
9.37 let "?P t" = ?thesis
9.38 - let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
9.39 + let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 \<circ> f2) ts =
9.40 subst_term_list f1 (subst_term_list f2 ts)"
9.41 show ?thesis
9.42 proof (induct t)
9.43 @@ -57,8 +56,8 @@
9.44 subsection {* Alternative induction *}
9.45
9.46 theorem term_induct' [case_names Var App]:
9.47 - assumes var: "!!a. P (Var a)"
9.48 - and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"
9.49 + assumes var: "\<And>a. P (Var a)"
9.50 + and app: "\<And>b ts. (\<forall>t \<in> set ts. P t) \<Longrightarrow> P (App b ts)"
9.51 shows "P t"
9.52 proof (induct t)
9.53 fix a show "P (Var a)" by (rule var)
9.54 @@ -72,8 +71,7 @@
9.55 then show "\<forall>t' \<in> set (t # ts). P t'" by simp
9.56 qed
9.57
9.58 -lemma
9.59 - "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
9.60 +lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
9.61 proof (induct t rule: term_induct')
9.62 case (Var a)
9.63 show ?case by (simp add: o_def)