author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46334  3858dc8eabd8 
child 47818  151d137f1095 
permissions  rwrr 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

1 
theory Collecting 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

2 
imports Complete_Lattice_ix ACom 
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 
45885  18 
"(SKIP {S}) \<le> (SKIP {S'}) = (S \<le> S')"  
19 
"(x ::= e {S}) \<le> (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<le> S')"  

20 
"(c1;c2) \<le> (c1';c2') = (c1 \<le> c1' \<and> c2 \<le> c2')"  

21 
"(IF b THEN c1 ELSE c2 {S}) \<le> (IF b' THEN c1' ELSE c2' {S'}) = 

22 
(b=b' \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')"  

23 
"({Inv} WHILE b DO c {P}) \<le> ({Inv'} WHILE b' DO c' {P'}) = 

24 
(b=b' \<and> c \<le> c' \<and> Inv \<le> Inv' \<and> P \<le> P')"  

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 

f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

33 
lemma Semi_le: "c1;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')" 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

34 
by (cases c) auto 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

35 

f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

36 
lemma If_le: "IF b THEN c1 ELSE c2 {S} \<le> c \<longleftrightarrow> 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

37 
(\<exists>c1' c2' S'. c= IF b THEN c1' ELSE c2' {S'} \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')" 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

38 
by (cases c) auto 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

39 

f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

40 
lemma While_le: "{Inv} WHILE b DO c {P} \<le> w \<longleftrightarrow> 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

41 
(\<exists>Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \<and> c \<le> c' \<and> Inv \<le> Inv' \<and> P \<le> P')" 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

42 
by (cases w) auto 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

43 

f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

44 
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

45 
"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

46 

f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

47 
instance 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

48 
proof 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

49 
case goal1 show ?case by(simp add: less_acom_def) 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

50 
next 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

51 
case goal2 thus ?case by (induct x) auto 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

52 
next 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

53 
case goal3 thus ?case 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

54 
apply(induct x y arbitrary: z rule: less_eq_acom.induct) 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

55 
apply (auto intro: le_trans simp: SKIP_le Assign_le Semi_le If_le While_le) 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

56 
done 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

57 
next 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

58 
case goal4 thus ?case 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

59 
apply(induct x y rule: less_eq_acom.induct) 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

60 
apply (auto intro: le_antisym) 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

61 
done 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

62 
qed 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

63 

f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

64 
end 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

65 

45919  66 
fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where 
67 
"sub\<^isub>1(c1;c2) = c1"  

68 
"sub\<^isub>1(IF b THEN c1 ELSE c2 {S}) = c1"  

69 
"sub\<^isub>1({I} WHILE b DO c {P}) = c" 

45903  70 

45919  71 
fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where 
72 
"sub\<^isub>2(c1;c2) = c2"  

73 
"sub\<^isub>2(IF b THEN c1 ELSE c2 {S}) = c2" 

45903  74 

75 
fun invar :: "'a acom \<Rightarrow> 'a" where 

76 
"invar({I} WHILE b DO c {P}) = I" 

77 

46116  78 
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

79 
where 
45903  80 
"lift F com.SKIP M = (SKIP {F (post ` M)})"  
81 
"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

82 
"lift F (c1;c2) M = 
45919  83 
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

84 
"lift F (IF b THEN c1 ELSE c2) M = 
45919  85 
IF b THEN lift F c1 (sub\<^isub>1 ` M) ELSE lift F c2 (sub\<^isub>2 ` M) 
45903  86 
{F (post ` M)}"  
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

87 
"lift F (WHILE b DO c) M = 
45903  88 
{F (invar ` M)} 
45919  89 
WHILE b DO lift F c (sub\<^isub>1 ` M) 
45903  90 
{F (post ` M)}" 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

91 

45903  92 
interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter" 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

93 
proof 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

94 
case goal1 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

95 
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

96 
proof(induction a arbitrary: A) 
45903  97 
case Semi from Semi.prems show ?case by(force intro!: Semi.IH) 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

98 
next 
45903  99 
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

100 
next 
45903  101 
case While from While.prems show ?case by(force intro!: While.IH) 
102 
qed force+ 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

103 
with goal1 show ?case by auto 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

104 
next 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

105 
case goal2 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

106 
thus ?case 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

107 
proof(induction b arbitrary: i A) 
45903  108 
case SKIP thus ?case by (force simp:SKIP_le) 
109 
next 

110 
case Assign thus ?case by (force simp:Assign_le) 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

111 
next 
45903  112 
case Semi from Semi.prems show ?case 
113 
by (force intro!: Semi.IH simp:Semi_le) 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

114 
next 
45903  115 
case If from If.prems show ?case by (force simp: If_le intro!: If.IH) 
116 
next 

117 
case While from While.prems show ?case 

118 
by(fastforce simp: While_le intro: While.IH) 

119 
qed 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

120 
next 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

121 
case goal3 
45903  122 
have "strip(lift Inter i A) = i" 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

123 
proof(induction i arbitrary: A) 
45903  124 
case Semi from Semi.prems show ?case 
125 
by (fastforce simp: strip_eq_Semi subset_iff intro!: Semi.IH) 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

126 
next 
45903  127 
case If from If.prems show ?case 
128 
by (fastforce intro!: If.IH simp: strip_eq_If) 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

129 
next 
45903  130 
case While from While.prems show ?case 
131 
by(fastforce intro: While.IH simp: strip_eq_While) 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

132 
qed auto 
45903  133 
thus ?case by auto 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

134 
qed 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

135 

f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

136 
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

137 
by(induction c d rule: less_eq_acom.induct) auto 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

138 

f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

139 
subsubsection "Collecting semantics" 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

140 

45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

141 
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

142 
"step S (SKIP {P}) = (SKIP {S})"  
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

143 
"step S (x ::= e {P}) = 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

144 
(x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})"  
45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

145 
"step S (c1; c2) = step S c1; step (post c1) c2"  
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

146 
"step S (IF b THEN c1 ELSE c2 {P}) = 
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

147 
IF b THEN step {s:S. bval b s} c1 ELSE step {s:S. \<not> bval b s} c2 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

148 
{post c1 \<union> post c2}"  
45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

149 
"step S ({Inv} WHILE b DO c {P}) = 
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

150 
{S \<union> post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}" 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

151 

46070  152 
definition CS :: "com \<Rightarrow> state set acom" where 
153 
"CS c = lfp (step UNIV) c" 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

154 

46334  155 
lemma mono2_step: "c1 \<le> c2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 c1 \<le> step S2 c2" 
156 
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

157 
case 2 thus ?case by fastforce 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

158 
next 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

159 
case 3 thus ?case by(simp add: le_post) 
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 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

162 
next 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

163 
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

164 
qed auto 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

165 

45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

166 
lemma mono_step: "mono (step S)" 
46334  167 
by(blast intro: monoI mono2_step) 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

168 

45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

169 
lemma strip_step: "strip(step S c) = strip c" 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

170 
by (induction c arbitrary: S) auto 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

171 

46066  172 
lemma lfp_cs_unfold: "lfp (step S) c = step S (lfp (step S) c)" 
45903  173 
apply(rule lfp_unfold[OF _ mono_step]) 
174 
apply(simp add: strip_step) 

175 
done 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

176 

46070  177 
lemma CS_unfold: "CS c = step UNIV (CS c)" 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

178 
by (metis CS_def lfp_cs_unfold) 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

179 

46070  180 
lemma strip_CS[simp]: "strip(CS c) = c" 
45903  181 
by(simp add: CS_def index_lfp[simplified]) 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

182 

f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset

183 
end 