author | nipkow |
Sun, 16 Sep 2012 11:50:03 +0200 | |
changeset 49396 | 73fb17ed2e08 |
parent 49344 | ce1ccb78ecda |
child 49397 | 4f9585401f1a |
permissions | -rw-r--r-- |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
1 |
theory Collecting |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
2 |
imports Complete_Lattice ACom |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
3 |
begin |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
4 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
5 |
subsection "Collecting Semantics of Commands" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
6 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
7 |
subsubsection "Annotated commands as a complete lattice" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
8 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
9 |
(* Orderings could also be lifted generically (thus subsuming the |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
10 |
instantiation for preord and order), but then less_eq_acom would need to |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
11 |
become a definition, eg less_eq_acom = lift2 less_eq, and then proofs would |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
12 |
need to unfold this defn first. *) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
13 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
14 |
instantiation acom :: (order) order |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
15 |
begin |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
16 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
17 |
fun less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where |
49344 | 18 |
"(SKIP {P}) \<le> (SKIP {P'}) = (P \<le> P')" | |
19 |
"(x ::= e {P}) \<le> (x' ::= e' {P'}) = (x=x' \<and> e=e' \<and> P \<le> P')" | |
|
20 |
"(C1;C2) \<le> (C1';C2') = (C1 \<le> C1' \<and> C2 \<le> C2')" | |
|
21 |
"(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) \<le> (IF b' THEN {P1'} C1' ELSE {P2'} C2' {Q'}) = |
|
22 |
(b=b' \<and> P1 \<le> P1' \<and> C1 \<le> C1' \<and> P2 \<le> P2' \<and> C2 \<le> C2' \<and> Q \<le> Q')" | |
|
23 |
"({I} WHILE b DO {P} C {Q}) \<le> ({I'} WHILE b' DO {P'} C' {Q'}) = |
|
24 |
(b=b' \<and> C \<le> C' \<and> I \<le> I' \<and> P \<le> P' \<and> Q \<le> Q')" | |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
25 |
"less_eq_acom _ _ = False" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
26 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
27 |
lemma SKIP_le: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
28 |
by (cases c) auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
29 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
30 |
lemma Assign_le: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
31 |
by (cases c) auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
32 |
|
49095 | 33 |
lemma Seq_le: "C1;C2 \<le> C \<longleftrightarrow> (\<exists>C1' C2'. C = C1';C2' \<and> C1 \<le> C1' \<and> C2 \<le> C2')" |
34 |
by (cases C) auto |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
35 |
|
49095 | 36 |
lemma If_le: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<le> C \<longleftrightarrow> |
37 |
(\<exists>p1' p2' C1' C2' S'. C = IF b THEN {p1'} C1' ELSE {p2'} C2' {S'} \<and> |
|
38 |
p1 \<le> p1' \<and> p2 \<le> p2' \<and> C1 \<le> C1' \<and> C2 \<le> C2' \<and> S \<le> S')" |
|
39 |
by (cases C) auto |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
40 |
|
49095 | 41 |
lemma While_le: "{I} WHILE b DO {p} C {P} \<le> W \<longleftrightarrow> |
42 |
(\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> C \<le> C' \<and> p \<le> p' \<and> I \<le> I' \<and> P \<le> P')" |
|
43 |
by (cases W) auto |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
44 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
45 |
definition less_acom :: "'a acom \<Rightarrow> 'a acom \<Rightarrow> bool" where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
46 |
"less_acom x y = (x \<le> y \<and> \<not> y \<le> x)" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
47 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
48 |
instance |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
49 |
proof |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
50 |
case goal1 show ?case by(simp add: less_acom_def) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
51 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
52 |
case goal2 thus ?case by (induct x) auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
53 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
54 |
case goal3 thus ?case |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
55 |
apply(induct x y arbitrary: z rule: less_eq_acom.induct) |
47818 | 56 |
apply (auto intro: le_trans simp: SKIP_le Assign_le Seq_le If_le While_le) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
57 |
done |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
58 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
59 |
case goal4 thus ?case |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
60 |
apply(induct x y rule: less_eq_acom.induct) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
61 |
apply (auto intro: le_antisym) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
62 |
done |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
63 |
qed |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
64 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
65 |
end |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
66 |
|
45919 | 67 |
fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where |
49095 | 68 |
"sub\<^isub>1(C1;C2) = C1" | |
49344 | 69 |
"sub\<^isub>1(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = C1" | |
70 |
"sub\<^isub>1({I} WHILE b DO {P} C {Q}) = C" |
|
45903 | 71 |
|
45919 | 72 |
fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where |
49095 | 73 |
"sub\<^isub>2(C1;C2) = C2" | |
49344 | 74 |
"sub\<^isub>2(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = C2" |
45903 | 75 |
|
49095 | 76 |
fun anno\<^isub>1 :: "'a acom \<Rightarrow> 'a" where |
49344 | 77 |
"anno\<^isub>1(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = P1" | |
78 |
"anno\<^isub>1({I} WHILE b DO {P} C {Q}) = I" |
|
49095 | 79 |
|
80 |
fun anno\<^isub>2 :: "'a acom \<Rightarrow> 'a" where |
|
49344 | 81 |
"anno\<^isub>2(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = P2" | |
82 |
"anno\<^isub>2({I} WHILE b DO {P} C {Q}) = P" |
|
49095 | 83 |
|
45903 | 84 |
|
46116 | 85 |
fun lift :: "('a set \<Rightarrow> 'b) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'b acom" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
86 |
where |
45903 | 87 |
"lift F com.SKIP M = (SKIP {F (post ` M)})" | |
88 |
"lift F (x ::= a) M = (x ::= a {F (post ` M)})" | |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
89 |
"lift F (c1;c2) M = |
45919 | 90 |
lift F c1 (sub\<^isub>1 ` M); lift F c2 (sub\<^isub>2 ` M)" | |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
91 |
"lift F (IF b THEN c1 ELSE c2) M = |
49095 | 92 |
IF b THEN {F (anno\<^isub>1 ` M)} lift F c1 (sub\<^isub>1 ` M) ELSE {F (anno\<^isub>2 ` M)} lift F c2 (sub\<^isub>2 ` M) |
45903 | 93 |
{F (post ` M)}" | |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
94 |
"lift F (WHILE b DO c) M = |
49095 | 95 |
{F (anno\<^isub>1 ` M)} |
96 |
WHILE b DO {F (anno\<^isub>2 ` M)} lift F c (sub\<^isub>1 ` M) |
|
45903 | 97 |
{F (post ` M)}" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
98 |
|
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
99 |
interpretation Complete_Lattice "{C. strip C = c}" "lift Inter c" for c |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
100 |
proof |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
101 |
case goal1 |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
102 |
have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
103 |
proof(induction a arbitrary: A) |
47818 | 104 |
case Seq from Seq.prems show ?case by(force intro!: Seq.IH) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
105 |
next |
45903 | 106 |
case If from If.prems show ?case by(force intro!: If.IH) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
107 |
next |
45903 | 108 |
case While from While.prems show ?case by(force intro!: While.IH) |
109 |
qed force+ |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
110 |
with goal1 show ?case by auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
111 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
112 |
case goal2 |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
113 |
thus ?case |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
114 |
proof(simp, induction b arbitrary: c A) |
45903 | 115 |
case SKIP thus ?case by (force simp:SKIP_le) |
116 |
next |
|
117 |
case Assign thus ?case by (force simp:Assign_le) |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
118 |
next |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
119 |
case Seq from Seq.prems show ?case by(force intro!: Seq.IH simp:Seq_le) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
120 |
next |
45903 | 121 |
case If from If.prems show ?case by (force simp: If_le intro!: If.IH) |
122 |
next |
|
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
123 |
case While from While.prems show ?case by(fastforce simp: While_le intro: While.IH) |
45903 | 124 |
qed |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
125 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
126 |
case goal3 |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
127 |
have "strip(lift Inter c A) = c" |
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
128 |
proof(induction c arbitrary: A) |
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
129 |
case Seq from Seq.prems show ?case by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
130 |
next |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
131 |
case If from If.prems show ?case by (fastforce intro!: If.IH simp: strip_eq_If) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
132 |
next |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
133 |
case While from While.prems show ?case by(fastforce intro: While.IH simp: strip_eq_While) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
134 |
qed auto |
45903 | 135 |
thus ?case by auto |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
136 |
qed |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
137 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
138 |
lemma le_post: "c \<le> d \<Longrightarrow> post c \<le> post d" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
139 |
by(induction c d rule: less_eq_acom.induct) auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
140 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
141 |
subsubsection "Collecting semantics" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
142 |
|
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
143 |
fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
144 |
"step S (SKIP {P}) = (SKIP {S})" | |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
145 |
"step S (x ::= e {P}) = |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
146 |
(x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" | |
49095 | 147 |
"step S (C1; C2) = step S C1; step (post C1) C2" | |
148 |
"step S (IF b THEN {P1} C1 ELSE {P2} C2 {P}) = |
|
149 |
IF b THEN {{s:S. bval b s}} step P1 C1 ELSE {{s:S. \<not> bval b s}} step P2 C2 |
|
150 |
{post C1 \<union> post C2}" | |
|
151 |
"step S ({I} WHILE b DO {P} C {P'}) = |
|
152 |
{S \<union> post C} WHILE b DO {{s:I. bval b s}} step P C {{s:I. \<not> bval b s}}" |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
153 |
|
46070 | 154 |
definition CS :: "com \<Rightarrow> state set acom" where |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
155 |
"CS c = lfp c (step UNIV)" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
156 |
|
46334 | 157 |
lemma mono2_step: "c1 \<le> c2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 c1 \<le> step S2 c2" |
158 |
proof(induction c1 c2 arbitrary: S1 S2 rule: less_eq_acom.induct) |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
159 |
case 2 thus ?case by fastforce |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
160 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
161 |
case 3 thus ?case by(simp add: le_post) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
162 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
163 |
case 4 thus ?case by(simp add: subset_iff)(metis le_post set_mp)+ |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
164 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
165 |
case 5 thus ?case by(simp add: subset_iff) (metis le_post set_mp) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
166 |
qed auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
167 |
|
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
168 |
lemma mono_step: "mono (step S)" |
46334 | 169 |
by(blast intro: monoI mono2_step) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
170 |
|
49095 | 171 |
lemma strip_step: "strip(step S C) = strip C" |
172 |
by (induction C arbitrary: S) auto |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
173 |
|
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
174 |
lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))" |
45903 | 175 |
apply(rule lfp_unfold[OF _ mono_step]) |
176 |
apply(simp add: strip_step) |
|
177 |
done |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
178 |
|
46070 | 179 |
lemma CS_unfold: "CS c = step UNIV (CS c)" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
180 |
by (metis CS_def lfp_cs_unfold) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
181 |
|
46070 | 182 |
lemma strip_CS[simp]: "strip(CS c) = c" |
45903 | 183 |
by(simp add: CS_def index_lfp[simplified]) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
184 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
185 |
end |