--- a/src/HOL/Hoare/Arith2.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Arith2.thy Wed Dec 23 22:25:22 2020 +0100
@@ -1,12 +1,12 @@
(* Title: HOL/Hoare/Arith2.thy
Author: Norbert Galm
Copyright 1995 TUM
-
-More arithmetic. Much of this duplicates ex/Primes.
*)
+section \<open>More arithmetic\<close>
+
theory Arith2
-imports Main
+ imports Main
begin
definition cd :: "[nat, nat, nat] \<Rightarrow> bool"
@@ -21,7 +21,7 @@
| "fac (Suc n) = Suc n * fac n"
-subsubsection \<open>cd\<close>
+subsection \<open>cd\<close>
lemma cd_nnn: "0<n \<Longrightarrow> cd n n n"
apply (simp add: cd_def)
@@ -48,7 +48,7 @@
done
-subsubsection \<open>gcd\<close>
+subsection \<open>gcd\<close>
lemma gcd_nnn: "0<n \<Longrightarrow> n = gcd n n"
apply (unfold gcd_def)
@@ -79,7 +79,7 @@
done
-subsubsection \<open>pow\<close>
+subsection \<open>pow\<close>
lemma sq_pow_div2 [simp]:
"m mod 2 = 0 \<Longrightarrow> ((n::nat)*n)^(m div 2) = n^m"
--- a/src/HOL/Hoare/Examples.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Examples.thy Wed Dec 23 22:25:22 2020 +0100
@@ -3,13 +3,15 @@
Copyright 1998 TUM
*)
-chapter \<open>Various examples\<close>
-
-theory Examples imports Hoare_Logic Arith2 begin
+section \<open>Various examples\<close>
-section \<open>ARITHMETIC\<close>
+theory Examples
+ imports Hoare_Logic Arith2
+begin
-subsection \<open>multiplication by successive addition\<close>
+subsection \<open>Arithmetic\<close>
+
+subsubsection \<open>Multiplication by successive addition\<close>
lemma multiply_by_add: "VARS m s a b
{a=A \<and> b=B}
@@ -54,7 +56,7 @@
done
-subsection \<open>Euclid's algorithm for GCD\<close>
+subsubsection \<open>Euclid's algorithm for GCD\<close>
lemma Euclid_GCD: "VARS a b
{0<A & 0<B}
@@ -87,7 +89,7 @@
done
-subsection \<open>Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM\<close>
+subsubsection \<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),
@@ -112,7 +114,7 @@
done
-subsection \<open>Power by iterated squaring and multiplication\<close>
+subsubsection \<open>Power by iterated squaring and multiplication\<close>
lemma power_by_mult: "VARS a b c
{a=A & b=B}
@@ -132,7 +134,7 @@
done
-subsection \<open>Factorial\<close>
+subsubsection \<open>Factorial\<close>
lemma factorial: "VARS a b
{a=A}
@@ -185,7 +187,7 @@
done
-subsection \<open>Square root\<close>
+subsubsection \<open>Square root\<close>
\<comment> \<open>the easy way:\<close>
@@ -221,7 +223,7 @@
done
-section \<open>LISTS\<close>
+subsection \<open>Lists\<close>
lemma imperative_reverse: "VARS y x
{x=X}
@@ -276,9 +278,9 @@
done
-section \<open>ARRAYS\<close>
+subsection \<open>Arrays\<close>
-subsection \<open>Search for a key\<close>
+subsubsection \<open>Search for a key\<close>
lemma zero_search: "VARS A i
{True}
--- a/src/HOL/Hoare/ExamplesAbort.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/ExamplesAbort.thy Wed Dec 23 22:25:22 2020 +0100
@@ -1,11 +1,13 @@
(* Title: HOL/Hoare/ExamplesAbort.thy
Author: Tobias Nipkow
Copyright 1998 TUM
-
-Some small examples for programs that may abort.
*)
-theory ExamplesAbort imports Hoare_Logic_Abort begin
+section \<open>Some small examples for programs that may abort\<close>
+
+theory ExamplesAbort
+ imports Hoare_Logic_Abort
+begin
lemma "VARS x y z::nat
{y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
--- a/src/HOL/Hoare/ExamplesTC.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/ExamplesTC.thy Wed Dec 23 22:25:22 2020 +0100
@@ -5,9 +5,7 @@
section \<open>Examples using Hoare Logic for Total Correctness\<close>
theory ExamplesTC
-
-imports Hoare_Logic
-
+ imports Hoare_Logic
begin
text \<open>
--- a/src/HOL/Hoare/Heap.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Heap.thy Wed Dec 23 22:25:22 2020 +0100
@@ -1,12 +1,15 @@
(* Title: HOL/Hoare/Heap.thy
Author: Tobias Nipkow
Copyright 2002 TUM
-
-Pointers, heaps and heap abstractions.
-See the paper by Mehta and Nipkow.
*)
-theory Heap imports Main begin
+section \<open>Pointers, heaps and heap abstractions\<close>
+
+text \<open>See the paper by Mehta and Nipkow.\<close>
+
+theory Heap
+ imports Main
+begin
subsection "References"
@@ -22,9 +25,9 @@
"addr (Ref a) = a"
-section "The heap"
+subsection "The heap"
-subsection "Paths in the heap"
+subsubsection "Paths in the heap"
primrec Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" where
"Path h x [] y \<longleftrightarrow> x = y"
@@ -55,7 +58,7 @@
by simp
-subsection "Non-repeating paths"
+subsubsection "Non-repeating paths"
definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as"
@@ -78,9 +81,9 @@
by (case_tac Ps, auto)
-subsection "Lists on the heap"
+subsubsection "Lists on the heap"
-subsubsection "Relational abstraction"
+paragraph "Relational abstraction"
definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
where "List h x as = Path h x as Null"
@@ -131,7 +134,7 @@
done
-subsection "Functional abstraction"
+subsubsection "Functional abstraction"
definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
--- a/src/HOL/Hoare/HeapSyntax.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/HeapSyntax.thy Wed Dec 23 22:25:22 2020 +0100
@@ -3,7 +3,11 @@
Copyright 2002 TUM
*)
-theory HeapSyntax imports Hoare_Logic Heap begin
+section \<open>Heap syntax\<close>
+
+theory HeapSyntax
+ imports Hoare_Logic Heap
+begin
subsection "Field access and update"
--- a/src/HOL/Hoare/HeapSyntaxAbort.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Wed Dec 23 22:25:22 2020 +0100
@@ -3,7 +3,11 @@
Copyright 2002 TUM
*)
-theory HeapSyntaxAbort imports Hoare_Logic_Abort Heap begin
+section \<open>Heap syntax (abort)\<close>
+
+theory HeapSyntaxAbort
+ imports Hoare_Logic_Abort Heap
+begin
subsection "Field access and update"
--- a/src/HOL/Hoare/Hoare_Logic.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy Wed Dec 23 22:25:22 2020 +0100
@@ -4,7 +4,13 @@
Author: Walter Guttmann (extension to total-correctness proofs)
*)
-section \<open>Sugared semantic embedding of Hoare logic\<close>
+section \<open>Hoare logic\<close>
+
+theory Hoare_Logic
+ imports Hoare_Syntax Hoare_Tac
+begin
+
+subsection \<open>Sugared semantic embedding of Hoare logic\<close>
text \<open>
Strictly speaking a shallow embedding (as implemented by Norbert Galm
@@ -12,10 +18,6 @@
later.
\<close>
-theory Hoare_Logic
-imports Hoare_Syntax Hoare_Tac
-begin
-
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
type_synonym 'a var = "'a \<Rightarrow> nat"
@@ -167,7 +169,7 @@
qed
-subsection \<open>Concrete syntax\<close>
+subsubsection \<open>Concrete syntax\<close>
setup \<open>
Hoare_Syntax.setup
@@ -181,7 +183,7 @@
\<close>
-subsection \<open>Proof methods: VCG\<close>
+subsubsection \<open>Proof methods: VCG\<close>
declare BasicRule [Hoare_Tac.BasicRule]
and SkipRule [Hoare_Tac.SkipRule]
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 22:25:22 2020 +0100
@@ -7,7 +7,7 @@
section \<open>Hoare Logic with an Abort statement for modelling run time errors\<close>
theory Hoare_Logic_Abort
-imports Hoare_Syntax Hoare_Tac
+ imports Hoare_Syntax Hoare_Tac
begin
type_synonym 'a bexp = "'a set"
--- a/src/HOL/Hoare/Hoare_Syntax.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Syntax.thy Wed Dec 23 22:25:22 2020 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/Hoare/Hoare_Syntax.thy
Author: Leonor Prensa Nieto & Tobias Nipkow
Author: Walter Guttmann (extension to total-correctness proofs)
+*)
-Concrete syntax for Hoare logic, with translations for variables.
-*)
+section \<open>Concrete syntax for Hoare logic, with translations for variables\<close>
theory Hoare_Syntax
imports Main
--- a/src/HOL/Hoare/Hoare_Tac.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Tac.thy Wed Dec 23 22:25:22 2020 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/Hoare/Hoare_Tac.thy
Author: Leonor Prensa Nieto & Tobias Nipkow
Author: Walter Guttmann (extension to total-correctness proofs)
+*)
-Derivation of the proof rules and, most importantly, the VCG tactic.
-*)
+section \<open>Hoare logic VCG tactic\<close>
theory Hoare_Tac
imports Main
--- a/src/HOL/Hoare/Pointer_Examples.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Pointer_Examples.thy Wed Dec 23 22:25:22 2020 +0100
@@ -1,17 +1,20 @@
(* Title: HOL/Hoare/Pointer_Examples.thy
Author: Tobias Nipkow
Copyright 2002 TUM
-
-Examples of verifications of pointer programs.
*)
-theory Pointer_Examples imports HeapSyntax begin
+section \<open>Examples of verifications of pointer programs\<close>
+
+theory Pointer_Examples
+ imports HeapSyntax
+begin
axiomatization where unproven: "PROP A"
-section "Verifications"
-subsection "List reversal"
+subsection "Verifications"
+
+subsubsection "List reversal"
text "A short but unreadable proof:"
@@ -105,7 +108,7 @@
done
-subsection "Searching in a list"
+subsubsection "Searching in a list"
text\<open>What follows is a sequence of successively more intelligent proofs that
a simple loop finds an element in a linked list.
@@ -174,7 +177,8 @@
apply clarsimp
done
-subsection "Splicing two lists"
+
+subsubsection "Splicing two lists"
lemma "VARS tl p q pp qq
{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> size Qs \<le> size Ps}
@@ -204,7 +208,7 @@
done
-subsection "Merging two lists"
+subsubsection "Merging two lists"
text"This is still a bit rough, especially the proof."
@@ -392,7 +396,7 @@
text"The proof is automatic, but requires a numbet of special lemmas."
-subsection "Cyclic list reversal"
+subsubsection "Cyclic list reversal"
text\<open>We consider two algorithms for the reversal of circular lists.
@@ -468,7 +472,7 @@
done
-subsection "Storage allocation"
+subsubsection "Storage allocation"
definition new :: "'a set \<Rightarrow> 'a"
where "new A = (SOME a. a \<notin> A)"
--- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy Wed Dec 23 22:25:22 2020 +0100
@@ -1,15 +1,17 @@
(* Title: HOL/Hoare/Pointer_ExamplesAbort.thy
Author: Tobias Nipkow
Copyright 2002 TUM
-
-Examples of verifications of pointer programs
*)
-theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin
+section \<open>Examples of verifications of pointer programs\<close>
-section "Verifications"
+theory Pointer_ExamplesAbort
+ imports HeapSyntaxAbort
+begin
-subsection "List reversal"
+subsection "Verifications"
+
+subsubsection "List reversal"
text "Interestingly, this proof is the same as for the unguarded program:"
--- a/src/HOL/Hoare/Pointers0.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Pointers0.thy Wed Dec 23 22:25:22 2020 +0100
@@ -9,7 +9,11 @@
- in fact in some case they appear to get (a bit) more complicated.
*)
-theory Pointers0 imports Hoare_Logic begin
+section \<open>Alternative pointers\<close>
+
+theory Pointers0
+ imports Hoare_Logic
+begin
subsection "References"
@@ -40,9 +44,9 @@
by vcg_simp
-section "The heap"
+subsection "The heap"
-subsection "Paths in the heap"
+subsubsection "Paths in the heap"
primrec Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
where
@@ -68,9 +72,9 @@
lemma [simp]: "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
by(induct as, simp, simp add:eq_sym_conv)
-subsection "Lists on the heap"
+subsubsection "Lists on the heap"
-subsubsection "Relational abstraction"
+paragraph "Relational abstraction"
definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool"
where "List h x as = Path h x as Null"
@@ -118,7 +122,7 @@
apply(fastforce dest:List_hd_not_in_tl)
done
-subsection "Functional abstraction"
+subsubsection "Functional abstraction"
definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool"
where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
@@ -173,9 +177,9 @@
done
-section "Verifications"
+subsection "Verifications"
-subsection "List reversal"
+subsubsection "List reversal"
text "A short but unreadable proof:"
@@ -256,7 +260,7 @@
done
-subsection "Searching in a list"
+subsubsection "Searching in a list"
text\<open>What follows is a sequence of successively more intelligent proofs that
a simple loop finds an element in a linked list.
@@ -312,7 +316,7 @@
done
-subsection "Merging two lists"
+subsubsection "Merging two lists"
text"This is still a bit rough, especially the proof."
@@ -398,7 +402,7 @@
(* TODO: merging with islist/list instead of List: an improvement?
needs (is)path, which is not so easy to prove either. *)
-subsection "Storage allocation"
+subsubsection "Storage allocation"
definition new :: "'a set \<Rightarrow> 'a::ref"
where "new A = (SOME a. a \<notin> A & a \<noteq> Null)"
@@ -427,5 +431,4 @@
apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
done
-
end
--- a/src/HOL/Hoare/SchorrWaite.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/SchorrWaite.thy Wed Dec 23 22:25:22 2020 +0100
@@ -1,14 +1,15 @@
(* Title: HOL/Hoare/SchorrWaite.thy
Author: Farhad Mehta
Copyright 2003 TUM
-
-Proof of the Schorr-Waite graph marking algorithm.
*)
+section \<open>Proof of the Schorr-Waite graph marking algorithm\<close>
-theory SchorrWaite imports HeapSyntax begin
+theory SchorrWaite
+ imports HeapSyntax
+begin
-section \<open>Machinery for the Schorr-Waite proof\<close>
+subsection \<open>Machinery for the Schorr-Waite proof\<close>
definition
\<comment> \<open>Relations induced by a mapping\<close>
@@ -194,8 +195,7 @@
done
-section\<open>The Schorr-Waite algorithm\<close>
-
+subsection \<open>The Schorr-Waite algorithm\<close>
theorem SchorrWaiteAlgorithm:
"VARS c m l r t p q root
@@ -573,4 +573,3 @@
qed
end
-
--- a/src/HOL/Hoare/SepLogHeap.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/SepLogHeap.thy Wed Dec 23 22:25:22 2020 +0100
@@ -1,13 +1,14 @@
(* Title: HOL/Hoare/SepLogHeap.thy
Author: Tobias Nipkow
Copyright 2002 TUM
-
-Heap abstractions (at the moment only Path and List)
-for Separation Logic.
*)
+section \<open>Heap abstractions for Separation Logic\<close>
+
+text \<open>(at the moment only Path and List)\<close>
+
theory SepLogHeap
-imports Main
+ imports Main
begin
type_synonym heap = "(nat \<Rightarrow> nat option)"
@@ -15,6 +16,7 @@
text\<open>\<open>Some\<close> means allocated, \<open>None\<close> means
free. Address \<open>0\<close> serves as the null reference.\<close>
+
subsection "Paths in the heap"
primrec Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
--- a/src/HOL/Hoare/Separation.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Separation.thy Wed Dec 23 22:25:22 2020 +0100
@@ -9,10 +9,13 @@
into parser and pretty printer, which is not very modular.
Alternative: some syntax like <P> which stands for P H. No more
compact, but avoids the funny H.
-
*)
-theory Separation imports Hoare_Logic_Abort SepLogHeap begin
+section \<open>Separation logic\<close>
+
+theory Separation
+ imports Hoare_Logic_Abort SepLogHeap
+begin
text\<open>The semantic definition of a few connectives:\<close>
--- a/src/HOL/Hoare/document/root.tex Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/document/root.tex Wed Dec 23 22:25:22 2020 +0100
@@ -1,4 +1,4 @@
-\documentclass[11pt,a4paper]{report}
+\documentclass[11pt,a4paper]{article}
\usepackage{graphicx}
\usepackage[english]{babel}
\usepackage{isabelle,isabellesym}
@@ -10,7 +10,12 @@
\begin{document}
\title{Hoare Logic}
-\author{Various}
+\author{
+ Norbert Galm \\
+ Walter Guttmann \\
+ Farhad Mehta \\
+ Tobias Nipkow \\
+ Leonor Prensa Nieto}
\maketitle
\begin{abstract}
@@ -27,7 +32,11 @@
\thispagestyle{empty}
\tableofcontents
-\newpage
+\begin{center}
+ \includegraphics[scale=0.5]{session_graph}
+\end{center}
+
+\clearpage
\input{session}