# HG changeset patch
# User nipkow
# Date 1534791266 -7200
# Node ID 403dd13cf6e97cb27a13e4565e19ead826f5e381
# Parent  9fc50a3e07f6b140b4bf9f3151dc3ca44ab5bd7f
avoid session qualification because no tex is generated when used;
tuned sectioning

diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/AExp.thy
--- a/src/HOL/IMP/AExp.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/AExp.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,9 +1,9 @@
 section "Arithmetic and Boolean Expressions"
 
+subsection "Arithmetic Expressions"
+
 theory AExp imports Main begin
 
-subsection "Arithmetic Expressions"
-
 type_synonym vname = string
 type_synonym val = int
 type_synonym state = "vname \<Rightarrow> val"
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/BExp.thy
--- a/src/HOL/IMP/BExp.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/BExp.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,6 +1,6 @@
-theory BExp imports AExp begin
+subsection "Boolean Expressions"
 
-subsection "Boolean Expressions"
+theory BExp imports AExp begin
 
 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
 
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Big_Step.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,9 +1,9 @@
 (* Author: Gerwin Klein, Tobias Nipkow *)
 
+subsection "Big-Step Semantics of Commands"
+
 theory Big_Step imports Com begin
 
-subsection "Big-Step Semantics of Commands"
-
 text \<open>
 The big-step semantics is a straight-forward inductive definition
 with concrete syntax. Note that the first parameter is a tuple,
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Compiler2.thy
--- a/src/HOL/IMP/Compiler2.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Compiler2.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,16 +1,16 @@
 (* Author: Gerwin Klein *)
 
+section \<open>Compiler Correctness, Reverse Direction\<close>
+
 theory Compiler2
 imports Compiler
 begin
 
 text \<open>
 The preservation of the source code semantics is already shown in the 
-parent theory @{theory "HOL-IMP.Compiler"}. This here shows the second direction.
+parent theory @{text "Compiler"}. This here shows the second direction.
 \<close>
 
-section \<open>Compiler Correctness, Reverse Direction\<close>
-
 subsection \<open>Definitions\<close>
 
 text \<open>Execution in @{term n} steps for simpler induction\<close>
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Hoare.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -2,9 +2,9 @@
 
 section "Hoare Logic"
 
-theory Hoare imports Big_Step begin
+subsection "Hoare Logic for Partial Correctness"
 
-subsection "Hoare Logic for Partial Correctness"
+theory Hoare imports Big_Step begin
 
 type_synonym assn = "state \<Rightarrow> bool"
 
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Hoare_Examples.thy
--- a/src/HOL/IMP/Hoare_Examples.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Hoare_Examples.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,5 +1,7 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Examples"
+
 theory Hoare_Examples imports Hoare begin
 
 hide_const (open) sum
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Hoare_Total.thy
--- a/src/HOL/IMP/Hoare_Total.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Hoare_Total.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -2,12 +2,12 @@
 
 subsection "Hoare Logic for Total Correctness"
 
+subsubsection "Separate Termination Relation"
+
 theory Hoare_Total
 imports Hoare_Examples
 begin
 
-subsubsection "Hoare Logic for Total Correctness --- Separate Termination Relation"
-
 text\<open>Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only
 works if execution is deterministic (which it is in our case).\<close>
 
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Hoare_Total_EX.thy
--- a/src/HOL/IMP/Hoare_Total_EX.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Hoare_Total_EX.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,11 +1,11 @@
 (* Author: Tobias Nipkow *)
 
+subsubsection "\<open>nat\<close>-Indexed Invariant"
+
 theory Hoare_Total_EX
 imports Hoare
 begin
 
-subsubsection "Hoare Logic for Total Correctness --- \<open>nat\<close>-Indexed Invariant"
-
 text\<open>This is the standard set of rules that you find in many publications.
 The While-rule is different from the one in Concrete Semantics in that the
 invariant is indexed by natural numbers and goes down by 1 with
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Hoare_Total_EX2.thy
--- a/src/HOL/IMP/Hoare_Total_EX2.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Hoare_Total_EX2.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,11 +1,11 @@
 (* Author: Tobias Nipkow *)
 
+subsubsection "Hoare Logic for Total Correctness With Logical Variables"
+
 theory Hoare_Total_EX2
 imports Hoare
 begin
 
-subsubsection "Hoare Logic for Total Correctness --- With Logical Variables"
-
 text\<open>This is the standard set of rules that you find in many publications.
 In the while-rule, a logical variable is needed to remember the pre-value
 of the variant (an expression that decreases by one with each iteration).
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Live_True.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,10 +1,12 @@
 (* Author: Tobias Nipkow *)
 
+subsection "True Liveness Analysis"
+
 theory Live_True
 imports "HOL-Library.While_Combinator" Vars Big_Step
 begin
 
-subsection "True Liveness Analysis"
+subsubsection "Analysis"
 
 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
 "L SKIP X = X" |
@@ -50,7 +52,7 @@
 declare L.simps(5)[simp del]
 
 
-subsection "Correctness"
+subsubsection "Correctness"
 
 theorem L_correct:
   "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
@@ -103,7 +105,7 @@
 qed
 
 
-subsection "Executability"
+subsubsection "Executability"
 
 lemma L_subset_vars: "L c X \<subseteq> rvars c \<union> X"
 proof(induction c arbitrary: X)
@@ -157,7 +159,7 @@
 by eval
 
 
-subsection "Limiting the number of iterations"
+subsubsection "Limiting the number of iterations"
 
 text\<open>The final parameter is the default value:\<close>
 
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Poly_Types.thy
--- a/src/HOL/IMP/Poly_Types.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Poly_Types.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,6 +1,6 @@
-theory Poly_Types imports Types begin
+subsection "Type Variables"
 
-subsection "Type Variables"
+theory Poly_Types imports Types begin
 
 datatype ty = Ity | Rty | TV nat
 
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Sec_Type_Expr.thy
--- a/src/HOL/IMP/Sec_Type_Expr.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Sec_Type_Expr.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,10 +1,10 @@
 section "Security Type Systems"
 
+subsection "Security Levels and Expressions"
+
 theory Sec_Type_Expr imports Big_Step
 begin
 
-subsection "Security Levels and Expressions"
-
 type_synonym level = nat
 
 class sec =
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Sec_Typing.thy
--- a/src/HOL/IMP/Sec_Typing.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Sec_Typing.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,9 +1,11 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Security Typing of Commands"
+
 theory Sec_Typing imports Sec_Type_Expr
 begin
 
-subsection "Syntax Directed Typing"
+subsubsection "Syntax Directed Typing"
 
 inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
 Skip:
@@ -174,7 +176,7 @@
 qed
 
 
-subsection "The Standard Typing System"
+subsubsection "The Standard Typing System"
 
 text\<open>The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The
 standard formulation, however, is slightly different, replacing the maximum
@@ -213,7 +215,7 @@
 apply (metis max.absorb2 While)
 by (metis anti_mono)
 
-subsection "A Bottom-Up Typing System"
+subsubsection "A Bottom-Up Typing System"
 
 inductive sec_type2 :: "com \<Rightarrow> level \<Rightarrow> bool" ("(\<turnstile> _ : _)" [0,0] 50) where
 Skip2:
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/Sec_TypingT.thy
--- a/src/HOL/IMP/Sec_TypingT.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/Sec_TypingT.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,7 +1,9 @@
+subsection "Termination-Sensitive Systems"
+
 theory Sec_TypingT imports Sec_Type_Expr
 begin
 
-subsection "A Termination-Sensitive Syntax Directed System"
+subsubsection "A Syntax Directed System"
 
 inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where
 Skip:
@@ -163,7 +165,7 @@
     by (metis \<open>s' = t' (\<le> l)\<close>)
 qed
 
-subsection "The Standard Termination-Sensitive System"
+subsubsection "The Standard System"
 
 text\<open>The predicate @{prop"l \<turnstile> c"} is nicely intuitive and executable. The
 standard formulation, however, is slightly different, replacing the maximum
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/VCG.thy
--- a/src/HOL/IMP/VCG.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/VCG.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,11 +1,12 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Verification Condition Generation"
+
 theory VCG imports Hoare begin
 
-subsection "Verification Conditions"
+subsubsection "Annotated Commands"
 
-text\<open>Annotated commands: commands where loops are annotated with
-invariants.\<close>
+text\<open>Commands where loops are annotated with invariants.\<close>
 
 datatype acom =
   Askip                  ("SKIP") |
@@ -25,7 +26,9 @@
 "strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" |
 "strip ({_} WHILE b DO C) = (WHILE b DO strip C)"
 
-text\<open>Weakest precondition from annotated commands:\<close>
+subsubsection "Weeakest Precondistion and Verification Condition"
+
+text\<open>Weakest precondition:\<close>
 
 fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
 "pre SKIP Q = Q" |
@@ -48,7 +51,7 @@
     vc C I)"
 
 
-text \<open>Soundness:\<close>
+subsubsection "Soundness"
 
 lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile> {pre C Q} strip C {Q}"
 proof(induction C arbitrary: Q)
@@ -70,7 +73,7 @@
 by (metis strengthen_pre vc_sound)
 
 
-text\<open>Completeness:\<close>
+subsubsection "Completeness"
 
 lemma pre_mono:
   "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre C P s \<Longrightarrow> pre C P' s"
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/VCG_Total_EX.thy
--- a/src/HOL/IMP/VCG_Total_EX.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/VCG_Total_EX.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,11 +1,13 @@
 (* Author: Tobias Nipkow *)
 
+subsection "Verification Conditions for Total Correctness"
+
+subsubsection "The Standard Approach"
+
 theory VCG_Total_EX
 imports Hoare_Total_EX
 begin
 
-subsection "Verification Conditions for Total Correctness"
-
 text\<open>Annotated commands: commands where loops are annotated with
 invariants.\<close>
 
diff -r 9fc50a3e07f6 -r 403dd13cf6e9 src/HOL/IMP/VCG_Total_EX2.thy
--- a/src/HOL/IMP/VCG_Total_EX2.thy	Fri Aug 17 11:26:35 2018 +0000
+++ b/src/HOL/IMP/VCG_Total_EX2.thy	Mon Aug 20 20:54:26 2018 +0200
@@ -1,11 +1,11 @@
 (* Author: Tobias Nipkow *)
 
+subsubsection "VCG for Total Correctness With Logical Variables"
+
 theory VCG_Total_EX2
 imports Hoare_Total_EX2
 begin
 
-subsection "Verification Conditions for Total Correctness"
-
 text \<open>
 Theory \<open>VCG_Total_EX\<close> conatins a VCG built on top of a Hoare logic without logical variables.
 As a result the completeness proof runs into a problem. This theory uses a Hoare logic