equal
deleted
inserted
replaced
|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 subsection "Collecting Semantics of Commands" |
|
4 |
1 theory Collecting |
5 theory Collecting |
2 imports Complete_Lattice Big_Step ACom |
6 imports Complete_Lattice Big_Step ACom |
3 begin |
7 begin |
4 |
8 |
5 subsection "The generic Step function" |
9 subsubsection "The generic Step function" |
6 |
10 |
7 notation |
11 notation |
8 sup (infixl "\<squnion>" 65) and |
12 sup (infixl "\<squnion>" 65) and |
9 inf (infixl "\<sqinter>" 70) and |
13 inf (infixl "\<sqinter>" 70) and |
10 bot ("\<bottom>") and |
14 bot ("\<bottom>") and |
28 |
32 |
29 lemma strip_Step[simp]: "strip(Step f g S C) = strip C" |
33 lemma strip_Step[simp]: "strip(Step f g S C) = strip C" |
30 by(induct C arbitrary: S) auto |
34 by(induct C arbitrary: S) auto |
31 |
35 |
32 |
36 |
33 subsection "Collecting Semantics of Commands" |
|
34 |
|
35 subsubsection "Annotated commands as a complete lattice" |
37 subsubsection "Annotated commands as a complete lattice" |
36 |
38 |
37 instantiation acom :: (order) order |
39 instantiation acom :: (order) order |
38 begin |
40 begin |
39 |
41 |