--- 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
--- 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
--- 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}")
--- 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)