more symbols;
authorwenzelm
Fri Feb 21 18:23:11 2014 +0100 (2014-02-21)
changeset 55656eb07b0acbebc
parent 55655 af028f35af60
child 55657 d5ad50aea356
child 55659 4089f6e98ab9
more symbols;
src/HOL/Isar_Examples/Basic_Logic.thy
src/HOL/Isar_Examples/Fibonacci.thy
src/HOL/Isar_Examples/Group.thy
src/HOL/Isar_Examples/Group_Context.thy
src/HOL/Isar_Examples/Group_Notepad.thy
src/HOL/Isar_Examples/Hoare.thy
src/HOL/Isar_Examples/Hoare_Ex.thy
src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
src/HOL/Isar_Examples/Nested_Datatype.thy
     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 -
    6.16 -type_synonym 'a sem = "'a => 'a => bool"
    6.17 +  where "SKIP \<equiv> Basic id"
    6.18  
    6.19 -primrec iter :: "nat => 'a bexp => 'a sem => 'a sem"
    6.20 -where
    6.21 -  "iter 0 b S s s' = (s ~: b & s = s')"
    6.22 -| "iter (Suc n) b S s s' = (s : b & (EX s''. S s s'' & iter n b S s'' s'))"
    6.23 +type_synonym 'a sem = "'a \<Rightarrow> 'a \<Rightarrow> bool"
    6.24  
    6.25 -primrec Sem :: "'a com => 'a sem"
    6.26 +primrec iter :: "nat \<Rightarrow> 'a bexp \<Rightarrow> 'a sem \<Rightarrow> 'a sem"
    6.27  where
    6.28 -  "Sem (Basic f) s s' = (s' = f s)"
    6.29 -| "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')"
    6.30 -| "Sem (Cond b c1 c2) s s' =
    6.31 -    (if s : b then Sem c1 s s' else Sem c2 s s')"
    6.32 -| "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')"
    6.33 +  "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
    6.34 +| "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.35  
    6.36 -definition Valid :: "'a bexp => 'a com => 'a bexp => bool"
    6.37 -    ("(3|- _/ (2_)/ _)" [100, 55, 100] 50)
    6.38 -  where "|- P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' --> s : P --> s' : Q)"
    6.39 +primrec Sem :: "'a com \<Rightarrow> 'a sem"
    6.40 +where
    6.41 +  "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
    6.42 +| "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
    6.43 +| "Sem (Cond b c1 c2) s s' \<longleftrightarrow>
    6.44 +    (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
    6.45 +| "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
    6.46  
    6.47 -notation (xsymbols) Valid  ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
    6.48 +definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
    6.49 +    ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
    6.50 +  where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
    6.51  
    6.52  lemma ValidI [intro?]:
    6.53 -    "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"
    6.54 +    "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
    6.55    by (simp add: Valid_def)
    6.56  
    6.57  lemma ValidD [dest?]:
    6.58 -    "|- P c Q ==> Sem c s s' ==> s : P ==> s' : Q"
    6.59 +    "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
    6.60    by (simp add: Valid_def)
    6.61  
    6.62  
    6.63 @@ -71,12 +69,13 @@
    6.64    to the state space.  This subsumes the common rules of \name{skip}
    6.65    and \name{assign}, as formulated in \S\ref{sec:hoare-isar}. *}
    6.66  
    6.67 -theorem basic: "|- {s. f s : P} (Basic f) P"
    6.68 +theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P"
    6.69  proof
    6.70 -  fix s s' assume s: "s : {s. f s : P}"
    6.71 +  fix s s'
    6.72 +  assume s: "s \<in> {s. f s \<in> P}"
    6.73    assume "Sem (Basic f) s s'"
    6.74    then have "s' = f s" by simp
    6.75 -  with s show "s' : P" by simp
    6.76 +  with s show "s' \<in> P" by simp
    6.77  qed
    6.78  
    6.79  text {*
    6.80 @@ -84,26 +83,27 @@
    6.81   established in a straight forward manner as follows.
    6.82  *}
    6.83  
    6.84 -theorem seq: "|- P c1 Q ==> |- Q c2 R ==> |- P (c1; c2) R"
    6.85 +theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R"
    6.86  proof
    6.87 -  assume cmd1: "|- P c1 Q" and cmd2: "|- Q c2 R"
    6.88 -  fix s s' assume s: "s : P"
    6.89 +  assume cmd1: "\<turnstile> P c1 Q" and cmd2: "\<turnstile> Q c2 R"
    6.90 +  fix s s'
    6.91 +  assume s: "s \<in> P"
    6.92    assume "Sem (c1; c2) s s'"
    6.93    then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'"
    6.94      by auto
    6.95 -  from cmd1 sem1 s have "s'' : Q" ..
    6.96 -  with cmd2 sem2 show "s' : R" ..
    6.97 +  from cmd1 sem1 s have "s'' \<in> Q" ..
    6.98 +  with cmd2 sem2 show "s' \<in> R" ..
    6.99  qed
   6.100  
   6.101 -theorem conseq: "P' <= P ==> |- P c Q ==> Q <= Q' ==> |- P' c Q'"
   6.102 +theorem conseq: "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P' c Q'"
   6.103  proof
   6.104 -  assume P'P: "P' <= P" and QQ': "Q <= Q'"
   6.105 -  assume cmd: "|- P c Q"
   6.106 +  assume P'P: "P' \<subseteq> P" and QQ': "Q \<subseteq> Q'"
   6.107 +  assume cmd: "\<turnstile> P c Q"
   6.108    fix s s' :: 'a
   6.109    assume sem: "Sem c s s'"
   6.110 -  assume "s : P'" with P'P have "s : P" ..
   6.111 -  with cmd sem have "s' : Q" ..
   6.112 -  with QQ' show "s' : Q'" ..
   6.113 +  assume "s : P'" with P'P have "s \<in> P" ..
   6.114 +  with cmd sem have "s' \<in> Q" ..
   6.115 +  with QQ' show "s' \<in> Q'" ..
   6.116  qed
   6.117  
   6.118  text {* The rule for conditional commands is directly reflected by the
   6.119 @@ -111,26 +111,27 @@
   6.120    which cases apply. *}
   6.121  
   6.122  theorem cond:
   6.123 -  assumes case_b: "|- (P Int b) c1 Q"
   6.124 -    and case_nb: "|- (P Int -b) c2 Q"
   6.125 -  shows "|- P (Cond b c1 c2) Q"
   6.126 +  assumes case_b: "\<turnstile> (P \<inter> b) c1 Q"
   6.127 +    and case_nb: "\<turnstile> (P \<inter> -b) c2 Q"
   6.128 +  shows "\<turnstile> P (Cond b c1 c2) Q"
   6.129  proof
   6.130 -  fix s s' assume s: "s : P"
   6.131 +  fix s s'
   6.132 +  assume s: "s \<in> P"
   6.133    assume sem: "Sem (Cond b c1 c2) s s'"
   6.134 -  show "s' : Q"
   6.135 +  show "s' \<in> Q"
   6.136    proof cases
   6.137 -    assume b: "s : b"
   6.138 +    assume b: "s \<in> b"
   6.139      from case_b show ?thesis
   6.140      proof
   6.141        from sem b show "Sem c1 s s'" by simp
   6.142 -      from s b show "s : P Int b" by simp
   6.143 +      from s b show "s \<in> P \<inter> b" by simp
   6.144      qed
   6.145    next
   6.146 -    assume nb: "s ~: b"
   6.147 +    assume nb: "s \<notin> b"
   6.148      from case_nb show ?thesis
   6.149      proof
   6.150        from sem nb show "Sem c2 s s'" by simp
   6.151 -      from s nb show "s : P Int -b" by simp
   6.152 +      from s nb show "s : P \<inter> -b" by simp
   6.153      qed
   6.154    qed
   6.155  qed
   6.156 @@ -143,22 +144,22 @@
   6.157    of the semantics of \texttt{WHILE}. *}
   6.158  
   6.159  theorem while:
   6.160 -  assumes body: "|- (P Int b) c P"
   6.161 -  shows "|- P (While b X c) (P Int -b)"
   6.162 +  assumes body: "\<turnstile> (P \<inter> b) c P"
   6.163 +  shows "\<turnstile> P (While b X c) (P \<inter> -b)"
   6.164  proof
   6.165 -  fix s s' assume s: "s : P"
   6.166 +  fix s s' assume s: "s \<in> P"
   6.167    assume "Sem (While b X c) s s'"
   6.168    then obtain n where "iter n b (Sem c) s s'" by auto
   6.169 -  from this and s show "s' : P Int -b"
   6.170 +  from this and s show "s' \<in> P \<inter> -b"
   6.171    proof (induct n arbitrary: s)
   6.172      case 0
   6.173      then show ?case by auto
   6.174    next
   6.175      case (Suc n)
   6.176 -    then obtain s'' where b: "s : b" and sem: "Sem c s s''"
   6.177 +    then obtain s'' where b: "s \<in> b" and sem: "Sem c s s''"
   6.178        and iter: "iter n b (Sem c) s'' s'" by auto
   6.179 -    from Suc and b have "s : P Int b" by simp
   6.180 -    with body sem have "s'' : P" ..
   6.181 +    from Suc and b have "s \<in> P \<inter> b" by simp
   6.182 +    with body sem have "s'' \<in> P" ..
   6.183      with iter show ?case by (rule Suc)
   6.184    qed
   6.185  qed
   6.186 @@ -188,29 +189,26 @@
   6.187    @{ML Syntax_Trans.quote_tr'},). *}
   6.188  
   6.189  syntax
   6.190 -  "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)" [0] 1000)
   6.191 -  "_antiquote"   :: "('a => 'b) => 'b"       ("\<acute>_" [1000] 1000)
   6.192 +  "_quote"       :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"       ("(.'(_').)" [0] 1000)
   6.193 +  "_antiquote"   :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"       ("\<acute>_" [1000] 1000)
   6.194    "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
   6.195          ("_[_'/\<acute>_]" [1000] 999)
   6.196 -  "_Assert"      :: "'a => 'a set"           ("(.{_}.)" [0] 1000)
   6.197 -  "_Assign"      :: "idt => 'b => 'a com"    ("(\<acute>_ :=/ _)" [70, 65] 61)
   6.198 -  "_Cond"        :: "'a bexp => 'a com => 'a com => 'a com"
   6.199 +  "_Assert"      :: "'a \<Rightarrow> 'a set"           ("(\<lbrace>_\<rbrace>)" [0] 1000)
   6.200 +  "_Assign"      :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"    ("(\<acute>_ :=/ _)" [70, 65] 61)
   6.201 +  "_Cond"        :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
   6.202          ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
   6.203 -  "_While_inv"   :: "'a bexp => 'a assn => 'a com => 'a com"
   6.204 +  "_While_inv"   :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"
   6.205          ("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)
   6.206 -  "_While"       :: "'a bexp => 'a com => 'a com"
   6.207 +  "_While"       :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"
   6.208          ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)
   6.209  
   6.210 -syntax (xsymbols)
   6.211 -  "_Assert"      :: "'a => 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
   6.212 -
   6.213  translations
   6.214 -  ".{b}."                   => "CONST Collect .(b)."
   6.215 -  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."
   6.216 -  "\<acute>x := a"                 => "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
   6.217 -  "IF b THEN c1 ELSE c2 FI" => "CONST Cond .{b}. c1 c2"
   6.218 -  "WHILE b INV i DO c OD"   => "CONST While .{b}. i c"
   6.219 -  "WHILE b DO c OD"         == "WHILE b INV CONST undefined DO c OD"
   6.220 +  "\<lbrace>b\<rbrace>"                     \<rightharpoonup> "CONST Collect .(b)."
   6.221 +  "B [a/\<acute>x]"                \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
   6.222 +  "\<acute>x := a"                 \<rightharpoonup> "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
   6.223 +  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
   6.224 +  "WHILE b INV i DO c OD"   \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
   6.225 +  "WHILE b DO c OD"         \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
   6.226  
   6.227  parse_translation {*
   6.228    let
   6.229 @@ -259,28 +257,28 @@
   6.230    calculational proofs, with the inclusion expressed in terms of sets
   6.231    or predicates.  Reversed order is supported as well. *}
   6.232  
   6.233 -lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q"
   6.234 +lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q"
   6.235    by (unfold Valid_def) blast
   6.236 -lemma [trans] : "P' <= P ==> |- P c Q ==> |- P' c Q"
   6.237 +lemma [trans] : "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P' c Q"
   6.238    by (unfold Valid_def) blast
   6.239  
   6.240 -lemma [trans]: "Q <= Q' ==> |- P c Q ==> |- P c Q'"
   6.241 +lemma [trans]: "Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P c Q'"
   6.242    by (unfold Valid_def) blast
   6.243 -lemma [trans]: "|- P c Q ==> Q <= Q' ==> |- P c Q'"
   6.244 +lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q'"
   6.245    by (unfold Valid_def) blast
   6.246  
   6.247  lemma [trans]:
   6.248 -    "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"
   6.249 +    "\<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> (\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
   6.250    by (simp add: Valid_def)
   6.251  lemma [trans]:
   6.252 -    "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"
   6.253 +    "(\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
   6.254    by (simp add: Valid_def)
   6.255  
   6.256  lemma [trans]:
   6.257 -    "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."
   6.258 +    "\<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> (\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
   6.259    by (simp add: Valid_def)
   6.260  lemma [trans]:
   6.261 -    "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."
   6.262 +    "(\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
   6.263    by (simp add: Valid_def)
   6.264  
   6.265  
   6.266 @@ -289,13 +287,13 @@
   6.267    instances for any number of basic assignments, without producing
   6.268    additional verification conditions.} *}
   6.269  
   6.270 -lemma skip [intro?]: "|- P SKIP P"
   6.271 +lemma skip [intro?]: "\<turnstile> P SKIP P"
   6.272  proof -
   6.273 -  have "|- {s. id s : P} SKIP P" by (rule basic)
   6.274 +  have "\<turnstile> {s. id s \<in> P} SKIP P" by (rule basic)
   6.275    then show ?thesis by simp
   6.276  qed
   6.277  
   6.278 -lemma assign: "|- P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
   6.279 +lemma assign: "\<turnstile> P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
   6.280    by (rule basic)
   6.281  
   6.282  text {* Note that above formulation of assignment corresponds to our
   6.283 @@ -315,7 +313,7 @@
   6.284  
   6.285  lemmas [trans, intro?] = seq
   6.286  
   6.287 -lemma seq_assoc [simp]: "( |- P c1;(c2;c3) Q) = ( |- P (c1;c2);c3 Q)"
   6.288 +lemma seq_assoc [simp]: "\<turnstile> P c1;(c2;c3) Q \<longleftrightarrow> \<turnstile> P (c1;c2);c3 Q"
   6.289    by (auto simp add: Valid_def)
   6.290  
   6.291  text {* Conditional statements. *}
   6.292 @@ -323,30 +321,30 @@
   6.293  lemmas [trans, intro?] = cond
   6.294  
   6.295  lemma [trans, intro?]:
   6.296 -  "|- .{\<acute>P & \<acute>b}. c1 Q
   6.297 -      ==> |- .{\<acute>P & ~ \<acute>b}. c2 Q
   6.298 -      ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
   6.299 +  "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c1 Q
   6.300 +      \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace> c2 Q
   6.301 +      \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> IF \<acute>b THEN c1 ELSE c2 FI Q"
   6.302      by (rule cond) (simp_all add: Valid_def)
   6.303  
   6.304  text {* While statements --- with optional invariant. *}
   6.305  
   6.306  lemma [intro?]:
   6.307 -    "|- (P Int b) c P ==> |- P (While b P c) (P Int -b)"
   6.308 +    "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
   6.309    by (rule while)
   6.310  
   6.311  lemma [intro?]:
   6.312 -    "|- (P Int b) c P ==> |- P (While b undefined c) (P Int -b)"
   6.313 +    "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
   6.314    by (rule while)
   6.315  
   6.316  
   6.317  lemma [intro?]:
   6.318 -  "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
   6.319 -    ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."
   6.320 +  "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
   6.321 +    \<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.322    by (simp add: while Collect_conj_eq Collect_neg_eq)
   6.323  
   6.324  lemma [intro?]:
   6.325 -  "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
   6.326 -    ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."
   6.327 +  "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
   6.328 +    \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
   6.329    by (simp add: while Collect_conj_eq Collect_neg_eq)
   6.330  
   6.331  
   6.332 @@ -378,13 +376,9 @@
   6.333    by (auto simp: Valid_def)
   6.334  
   6.335  lemma iter_aux:
   6.336 -  "\<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
   6.337 -       (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)"
   6.338 -  apply(induct n)
   6.339 -   apply clarsimp
   6.340 -   apply (simp (no_asm_use))
   6.341 -   apply blast
   6.342 -  done
   6.343 +  "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
   6.344 +       (\<And>s s'. s \<in> I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> I \<and> s' \<notin> b)"
   6.345 +  by (induct n) auto
   6.346  
   6.347  lemma WhileRule:
   6.348      "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)