author wenzelm Fri Feb 21 18:23:11 2014 +0100 (2014-02-21) changeset 55656 eb07b0acbebc parent 55655 af028f35af60 child 55657 d5ad50aea356 child 55659 4089f6e98ab9
more symbols;
 src/HOL/Isar_Examples/Basic_Logic.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Fibonacci.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Group.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Group_Context.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Group_Notepad.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Hoare.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Hoare_Ex.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Mutilated_Checkerboard.thy file | annotate | diff | revisions src/HOL/Isar_Examples/Nested_Datatype.thy file | annotate | diff | revisions
     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.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.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)"       ("(.'(_').)"  1000)
6.191 -  "_antiquote"   :: "('a => 'b) => 'b"       ("\<acute>_"  1000)
6.192 +  "_quote"       :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"       ("(.'(_').)"  1000)
6.193 +  "_antiquote"   :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"       ("\<acute>_"  1000)
6.194    "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
6.195          ("_[_'/\<acute>_]"  999)
6.196 -  "_Assert"      :: "'a => 'a set"           ("(.{_}.)"  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>)"  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>)"  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.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.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.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.264
6.265
6.266 @@ -289,13 +287,13 @@
6.267    instances for any number of basic assignments, without producing
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.73
8.74  lemma below_0: "below 0 = {}"
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.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)