--- a/src/HOL/IMP/ACom.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/ACom.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,11 +1,11 @@
(* Author: Tobias Nipkow *)
+subsection "Annotated Commands"
+
theory ACom
imports Com
begin
-subsection "Annotated Commands"
-
datatype 'a acom =
SKIP 'a ("SKIP {_}" 61) |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
--- a/src/HOL/IMP/Abs_Int0.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,10 +1,12 @@
(* Author: Tobias Nipkow *)
+subsection "Abstract Interpretation"
+
theory Abs_Int0
imports Abs_Int_init
begin
-subsection "Orderings"
+subsubsection "Orderings"
text\<open>The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are
defined in @{theory Main}, more precisely in theories @{theory HOL.Orderings} and @{theory HOL.Lattices}.
@@ -139,7 +141,7 @@
using pfp_inv[OF assms(2), where P = "%x. g x = g x0"] assms(1) by simp
-subsection "Abstract Interpretation"
+subsubsection "Abstract Interpretation"
definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
"\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}"
--- a/src/HOL/IMP/Abs_Int1.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,11 +1,11 @@
(* Author: Tobias Nipkow *)
+subsection "Computable Abstract Interpretation"
+
theory Abs_Int1
imports Abs_State
begin
-subsection "Computable Abstract Interpretation"
-
text\<open>Abstract interpretation over type @{text st} instead of functions.\<close>
context Gamma_semilattice
--- a/src/HOL/IMP/Abs_Int1_const.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,11 +1,11 @@
(* Author: Tobias Nipkow *)
+subsection "Constant Propagation"
+
theory Abs_Int1_const
imports Abs_Int1
begin
-subsection "Constant Propagation"
-
datatype const = Const val | Any
fun \<gamma>_const where
--- a/src/HOL/IMP/Abs_Int1_parity.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,11 +1,11 @@
(* Author: Tobias Nipkow *)
+subsection "Parity Analysis"
+
theory Abs_Int1_parity
imports Abs_Int1
begin
-subsection "Parity Analysis"
-
datatype parity = Even | Odd | Either
text\<open>Instantiation of class @{class order} with type @{typ parity}:\<close>
--- a/src/HOL/IMP/Abs_Int2.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,5 +1,7 @@
(* Author: Tobias Nipkow *)
+subsection "Backward Analysis of Expressions"
+
theory Abs_Int2
imports Abs_Int1
begin
@@ -24,7 +26,7 @@
end
-subsection "Backward Analysis of Expressions"
+subsubsection "Extended Framework"
subclass (in bounded_lattice) semilattice_sup_top ..
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,11 +1,11 @@
(* Author: Tobias Nipkow *)
+subsection "Interval Analysis"
+
theory Abs_Int2_ivl
imports Abs_Int2
begin
-subsection "Interval Analysis"
-
type_synonym eint = "int extended"
type_synonym eint2 = "eint * eint"
--- a/src/HOL/IMP/Abs_Int3.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,12 +1,11 @@
(* Author: Tobias Nipkow *)
+subsection "Widening and Narrowing"
+
theory Abs_Int3
imports Abs_Int2_ivl
begin
-
-subsection "Widening and Narrowing"
-
class widen =
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
--- a/src/HOL/IMP/Abs_Int_Tests.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int_Tests.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,9 +1,11 @@
+(* Author: Tobias Nipkow *)
+
+subsection "Abstract Interpretation Test Programs"
+
theory Abs_Int_Tests
imports Com
begin
-subsection "Test Programs"
-
text\<open>For constant propagation:\<close>
text\<open>Straight line code:\<close>
--- a/src/HOL/IMP/Abs_State.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_State.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,5 +1,7 @@
(* Author: Tobias Nipkow *)
+subsection "Computable State"
+
theory Abs_State
imports Abs_Int0
begin
--- a/src/HOL/IMP/Collecting.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Collecting.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,8 +1,12 @@
+(* Author: Tobias Nipkow *)
+
+subsection "Collecting Semantics of Commands"
+
theory Collecting
imports Complete_Lattice Big_Step ACom
begin
-subsection "The generic Step function"
+subsubsection "The generic Step function"
notation
sup (infixl "\<squnion>" 65) and
@@ -30,8 +34,6 @@
by(induct C arbitrary: S) auto
-subsection "Collecting Semantics of Commands"
-
subsubsection "Annotated commands as a complete lattice"
instantiation acom :: (order) order
--- a/src/HOL/IMP/Collecting1.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Collecting1.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,9 +1,9 @@
+subsection "A small step semantics on annotated commands"
+
theory Collecting1
imports Collecting
begin
-subsection "A small step semantics on annotated commands"
-
text\<open>The idea: the state is propagated through the annotated command as an
annotation @{term "{s}"}, all other annotations are @{term "{}"}. It is easy
to show that this semantics approximates the collecting semantics.\<close>
--- a/src/HOL/IMP/Collecting_Examples.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Collecting_Examples.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,8 +1,10 @@
+subsection "Collecting Semantics Examples"
+
theory Collecting_Examples
imports Collecting Vars
begin
-subsection "Pretty printing state sets"
+subsubsection "Pretty printing state sets"
text\<open>Tweak code generation to work with sets of non-equality types:\<close>
declare insert_code[code del] union_coset_filter[code del]
@@ -27,7 +29,7 @@
annotate (\<lambda>p. (\<lambda>s. (\<lambda>x. (x, s x)) ` (vars_acom C)) ` anno C p) (strip C)"
-subsection "Examples"
+subsubsection "Examples"
definition "c0 = WHILE Less (V ''x'') (N 3)
DO ''x'' ::= Plus (V ''x'') (N 2)"
--- a/src/HOL/IMP/Complete_Lattice.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Complete_Lattice.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,5 +1,9 @@
+(* Author: Tobias Nipkow *)
+
section "Abstract Interpretation"
+subsection "Complete Lattice"
+
theory Complete_Lattice
imports Main
begin