# HG changeset patch
# User wenzelm
# Date 1393012453 -3600
# Node ID b45af39fcdaee2875d6787ee7cd50a70db4ed526
# Parent  ec14796cd140bd238f6b720450a0a7b8125e02f2
tuned;

diff -r ec14796cd140 -r b45af39fcdae src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Fri Feb 21 20:47:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Fri Feb 21 20:54:13 2014 +0100
@@ -189,26 +189,24 @@
   @{ML Syntax_Trans.quote_tr'},). *}
 
 syntax
-  "_quote"       :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"       ("(.'(_').)" [0] 1000)
-  "_antiquote"   :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"       ("\<acute>_" [1000] 1000)
-  "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
-        ("_[_'/\<acute>_]" [1000] 999)
-  "_Assert"      :: "'a \<Rightarrow> 'a set"           ("(\<lbrace>_\<rbrace>)" [0] 1000)
-  "_Assign"      :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"    ("(\<acute>_ :=/ _)" [70, 65] 61)
-  "_Cond"        :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
-        ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
-  "_While_inv"   :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"
-        ("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)
-  "_While"       :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"
-        ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)
+  "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"
+  "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"  ("\<acute>_" [1000] 1000)
+  "_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"  ("_[_'/\<acute>_]" [1000] 999)
+  "_Assert" :: "'a \<Rightarrow> 'a set"  ("(\<lbrace>_\<rbrace>)" [0] 1000)
+  "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"  ("(\<acute>_ :=/ _)" [70, 65] 61)
+  "_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
+    ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
+  "_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"
+    ("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)
+  "_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)
 
 translations
-  "\<lbrace>b\<rbrace>"                     \<rightharpoonup> "CONST Collect .(b)."
-  "B [a/\<acute>x]"                \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
-  "\<acute>x := a"                 \<rightharpoonup> "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
+  "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect (_quote b)"
+  "B [a/\<acute>x]" \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
+  "\<acute>x := a" \<rightharpoonup> "CONST Basic (_quote (\<acute>(_update_name x (\<lambda>_. a))))"
   "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
-  "WHILE b INV i DO c OD"   \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
-  "WHILE b DO c OD"         \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
+  "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
+  "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
 
 parse_translation {*
   let
@@ -328,12 +326,10 @@
 
 text {* While statements --- with optional invariant. *}
 
-lemma [intro?]:
-    "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
+lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
   by (rule while)
 
-lemma [intro?]:
-    "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
+lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
   by (rule while)