# HG changeset patch
# User wenzelm
# Date 1515776283 -3600
# Node ID 64d928bacddd818dd39e9926ccca688d348b6e0d
# Parent  060efe5321898ae789b0fb9e699beab037d25bec
prefer formal comments;

diff -r 060efe532189 -r 64d928bacddd src/HOL/Hoare/Examples.thy
--- a/src/HOL/Hoare/Examples.thy	Fri Jan 12 17:14:34 2018 +0100
+++ b/src/HOL/Hoare/Examples.thy	Fri Jan 12 17:58:03 2018 +0100
@@ -1,15 +1,15 @@
 (*  Title:      HOL/Hoare/Examples.thy
     Author:     Norbert Galm
     Copyright   1998 TUM
+*)
 
-Various examples.
-*)
+chapter \<open>Various examples\<close>
 
 theory Examples imports Hoare_Logic Arith2 begin
 
-(*** ARITHMETIC ***)
+section \<open>ARITHMETIC\<close>
 
-(** multiplication by successive addition **)
+subsection \<open>multiplication by successive addition\<close>
 
 lemma multiply_by_add: "VARS m s a b
   {a=A & b=B}
@@ -53,7 +53,8 @@
  apply (auto simp add:int_distrib)
 done
 
-(** Euclid's algorithm for GCD **)
+
+subsection \<open>Euclid's algorithm for GCD\<close>
 
 lemma Euclid_GCD: "VARS a b
  {0<A & 0<B}
@@ -63,7 +64,7 @@
  DO IF a<b THEN b := b-a ELSE a := a-b FI OD
  {a = gcd A B}"
 apply vcg
-(*Now prove the verification conditions*)
+  \<comment> \<open>Now prove the verification conditions\<close>
   apply auto
   apply(simp add: gcd_diff_r less_imp_le)
  apply(simp add: linorder_not_less gcd_diff_l)
@@ -78,19 +79,22 @@
  DO IF a<b THEN b := b-a; t := t+1 ELSE a := a-b; t := t+1 FI OD
  {a = gcd A B & t \<le> max A B + 2}"
 apply vcg
-(*Now prove the verification conditions*)
+  \<comment> \<open>Now prove the verification conditions\<close>
   apply auto
   apply(simp add: gcd_diff_r less_imp_le)
  apply(simp add: linorder_not_less gcd_diff_l)
 apply(erule gcd_nnn)
 done
 
-(** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
-(* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
-   where it is given without the invariant. Instead of defining scm
-   explicitly we have used the theorem scm x y = x*y/gcd x y and avoided
-   division by mupltiplying with gcd x y.
-*)
+
+subsection \<open>Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM\<close>
+
+text \<open>
+  From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
+  where it is given without the invariant. Instead of defining \<open>scm\<close>
+  explicitly we have used the theorem \<open>scm x y = x * y / gcd x y\<close> and avoided
+  division by mupltiplying with \<open>gcd x y\<close>.
+\<close>
 
 lemmas distribs =
   diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2
@@ -107,7 +111,8 @@
 apply(simp add: distribs gcd_nnn)
 done
 
-(** Power by iterated squaring and multiplication **)
+
+subsection \<open>Power by iterated squaring and multiplication\<close>
 
 lemma power_by_mult: "VARS a b c
  {a=A & b=B}
@@ -126,7 +131,8 @@
 apply simp
 done
 
-(** Factorial **)
+
+subsection \<open>Factorial\<close>
 
 lemma factorial: "VARS a b
  {a=A}
@@ -178,9 +184,10 @@
 apply arith
 done
 
-(** Square root **)
 
-(* the easy way: *)
+subsection \<open>Square root\<close>
+
+\<comment> \<open>the easy way:\<close>
 
 lemma sqrt: "VARS r x
  {True}
@@ -202,8 +209,7 @@
 apply vcg_simp
 done
 
-(* without multiplication *)
-
+\<comment> \<open>without multiplication\<close>
 lemma sqrt_without_multiplication: "VARS u w r
  {x=X}
  u := 1; w := 1; r := (0::nat);
@@ -215,7 +221,7 @@
 done
 
 
-(*** LISTS ***)
+section \<open>LISTS\<close>
 
 lemma imperative_reverse: "VARS y x
  {x=X}
@@ -270,9 +276,10 @@
 done
 
 
-(*** ARRAYS ***)
+section \<open>ARRAYS\<close>
 
-(* Search for a key *)
+subsection \<open>Search for a key\<close>
+
 lemma zero_search: "VARS A i
  {True}
  i := 0;
@@ -297,15 +304,15 @@
 apply(blast elim!: less_SucE)
 done
 
-(* 
-The `partition' procedure for quicksort.
-`A' is the array to be sorted (modelled as a list).
-Elements of A must be of class order to infer at the end
-that the elements between u and l are equal to pivot.
+text \<open>
+  The \<open>partition\<close> procedure for quicksort.
+    \<^item> \<open>A\<close> is the array to be sorted (modelled as a list).
+    \<^item> Elements of \<open>A\<close> must be of class order to infer at the end
+      that the elements between u and l are equal to pivot.
 
-Ambiguity warnings of parser are due to := being used
-both for assignment and list update.
-*)
+  Ambiguity warnings of parser are due to \<open>:=\<close> being used
+  both for assignment and list update.
+\<close>
 lemma lem: "m - Suc 0 < n ==> m < Suc n"
 by arith
 
@@ -327,7 +334,7 @@
      IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
   OD
  {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
-(* expand and delete abbreviations first *)
+\<comment> \<open>expand and delete abbreviations first\<close>
 apply (simp)
 apply (erule thin_rl)+
 apply vcg_simp
diff -r 060efe532189 -r 64d928bacddd src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Fri Jan 12 17:14:34 2018 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Fri Jan 12 17:58:03 2018 +0100
@@ -61,7 +61,7 @@
   \<open>[(@{const_syntax Valid}, K (Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"}))]\<close>
 
 
-(*** The proof rules ***)
+section \<open>The proof rules\<close>
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
 by (auto simp:Valid_def)
@@ -115,17 +115,18 @@
     SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
-(* Special syntax for guarded statements and guarded array updates: *)
-
+\<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close>
 syntax
   "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
   "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
 translations
   "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
   "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
-  (* reverse translation not possible because of duplicate "a" *)
+  \<comment> \<open>reverse translation not possible because of duplicate \<open>a\<close>\<close>
 
-text\<open>Note: there is no special syntax for guarded array access. Thus
-you must write \<open>j < length a \<rightarrow> a[i] := a!j\<close>.\<close>
+text \<open>
+  Note: there is no special syntax for guarded array access. Thus
+  you must write \<open>j < length a \<rightarrow> a[i] := a!j\<close>.
+\<close>
 
 end
diff -r 060efe532189 -r 64d928bacddd src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Fri Jan 12 17:14:34 2018 +0100
+++ b/src/HOL/Hoare/SchorrWaite.thy	Fri Jan 12 17:58:03 2018 +0100
@@ -203,20 +203,20 @@
  t := root; p := Null;
  WHILE p \<noteq> Null \<or> t \<noteq> Null \<and> \<not> t^.m
  INV {\<exists>stack.
-          List (S c l r) p stack \<and>                                         (*i1*)
-          (\<forall>x \<in> set stack. m x) \<and>                                        (*i2*)
-          R = reachable (relS{l, r}) {t,p} \<and>                           (*i3*)
-          (\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow>                                        (*i4*)
+          List (S c l r) p stack \<and>                                      \<comment> \<open>\<open>i1\<close>\<close>
+          (\<forall>x \<in> set stack. m x) \<and>                                       \<comment> \<open>\<open>i2\<close>\<close>
+          R = reachable (relS{l, r}) {t,p} \<and>                            \<comment> \<open>\<open>i3\<close>\<close>
+          (\<forall>x. x \<in> R \<and> \<not>m x \<longrightarrow>                                         \<comment> \<open>\<open>i4\<close>\<close>
                  x \<in> reachable (relS{l,r}|m) ({t}\<union>set(map r stack))) \<and>
-          (\<forall>x. m x \<longrightarrow> x \<in> R) \<and>                                         (*i5*)
-          (\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and>       (*i6*)
-          (stkOk c l r iL iR t stack)                                    (*i7*) }
+          (\<forall>x. m x \<longrightarrow> x \<in> R) \<and>                                         \<comment> \<open>\<open>i5\<close>\<close>
+          (\<forall>x. x \<notin> set stack \<longrightarrow> r x = iR x \<and> l x = iL x) \<and>             \<comment> \<open>\<open>i6\<close>\<close>
+          (stkOk c l r iL iR t stack)                                   \<comment> \<open>\<open>i7\<close>\<close>}
  DO IF t = Null \<or> t^.m
       THEN IF p^.c
-               THEN q := t; t := p; p := p^.r; t^.r := q               (*pop*)
-               ELSE q := t; t := p^.r; p^.r := p^.l;                      (*swing*)
+               THEN q := t; t := p; p := p^.r; t^.r := q                \<comment> \<open>\<open>pop\<close>\<close>
+               ELSE q := t; t := p^.r; p^.r := p^.l;                    \<comment> \<open>\<open>swing\<close>\<close>
                         p^.l := q; p^.c := True          FI    
-      ELSE q := p; p := t; t := t^.l; p^.l := q;                         (*push*)
+      ELSE q := p; p := t; t := t^.l; p^.l := q;                        \<comment> \<open>\<open>push\<close>\<close>
                p^.m := True; p^.c := False            FI       OD
  {(\<forall>x. (x \<in> R) = m x) \<and> (r = iR \<and> l = iL) }"
   (is "VARS c m l r t p q root {?Pre c m l r root} (?c1; ?c2; ?c3) {?Post c m l r}")
diff -r 060efe532189 -r 64d928bacddd src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Fri Jan 12 17:14:34 2018 +0100
+++ b/src/HOL/Hoare/Separation.thy	Fri Jan 12 17:58:03 2018 +0100
@@ -156,7 +156,7 @@
 proofs. Here comes a simple example of a program proof that uses a law
 of separation logic instead.\<close>
 
-(* a law of separation logic *)
+\<comment> \<open>a law of separation logic\<close>
 lemma star_comm: "P ** Q = Q ** P"
   by(auto simp add:star_def ortho_def dest: map_add_comm)