47619

1 
(* Author: Tobias Nipkow *)


2 


3 
theory Abs_State


4 
imports Abs_Int0


5 
begin


6 

49396

7 
subsubsection "Setbased lattices"

47619

8 


9 
instantiation com :: vars


10 
begin


11 


12 
fun vars_com :: "com \<Rightarrow> vname set" where


13 
"vars com.SKIP = {}" 


14 
"vars (x::=e) = {x} \<union> vars e" 


15 
"vars (c1;c2) = vars c1 \<union> vars c2" 


16 
"vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2" 


17 
"vars (WHILE b DO c) = vars b \<union> vars c"


18 


19 
instance ..


20 


21 
end


22 


23 


24 
lemma finite_avars: "finite(vars(a::aexp))"


25 
by(induction a) simp_all


26 


27 
lemma finite_bvars: "finite(vars(b::bexp))"


28 
by(induction b) (simp_all add: finite_avars)


29 


30 
lemma finite_cvars: "finite(vars(c::com))"


31 
by(induction c) (simp_all add: finite_avars finite_bvars)


32 


33 

49396

34 
class L =


35 
fixes L :: "vname set \<Rightarrow> 'a set"

47619

36 


37 

49396

38 
instantiation acom :: (L)L

47619

39 
begin


40 

49396

41 
definition L_acom where


42 
"L X = {C. vars(strip C) \<subseteq> X \<and> (\<forall>a \<in> set(annos C). a \<in> L X)}"

47619

43 


44 
instance ..


45 


46 
end


47 


48 

49396

49 
instantiation option :: (L)L

47619

50 
begin


51 

49396

52 
definition L_option where


53 
"L X = {opt. case opt of None \<Rightarrow> True  Some x \<Rightarrow> x \<in> L X}"

47619

54 

49396

55 
lemma L_option_simps[simp]: "None \<in> L X" "(Some x \<in> L X) = (x \<in> L X)"


56 
by(simp_all add: L_option_def)

47619

57 


58 
instance ..


59 


60 
end


61 

49396

62 
class semilatticeL = join + L +

49577

63 
fixes top :: "com \<Rightarrow> 'a"

49396

64 
assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<sqsubseteq> x \<squnion> y"


65 
and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<sqsubseteq> x \<squnion> y"

47619

66 
and join_least[simp]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"

49396

67 
and top[simp]: "x \<in> L(vars c) \<Longrightarrow> x \<sqsubseteq> top c"


68 
and top_in_L[simp]: "top c \<in> L(vars c)"


69 
and join_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"

47619

70 

49577

71 
notation (input) top ("\<top>\<^bsub>_\<^esub>")


72 
notation (latex output) top ("\<top>\<^bsub>\<^raw:\isa{>_\<^raw:}>\<^esub>")

47619

73 

49396

74 
instantiation option :: (semilatticeL)semilatticeL

47619

75 
begin


76 


77 
definition top_option where "top c = Some(top c)"


78 


79 
instance proof


80 
case goal1 thus ?case by(cases x, simp, cases y, simp_all)


81 
next


82 
case goal2 thus ?case by(cases y, simp, cases x, simp_all)


83 
next


84 
case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)


85 
next


86 
case goal4 thus ?case by(cases x, simp_all add: top_option_def)


87 
next


88 
case goal5 thus ?case by(simp add: top_option_def)


89 
next

49396

90 
case goal6 thus ?case by(simp add: L_option_def split: option.splits)

47619

91 
qed


92 


93 
end


94 


95 


96 
subsection "Abstract State with Computable Ordering"


97 


98 
hide_type st "to avoid long names"


99 


100 
text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}


101 


102 
datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname set"


103 

49344

104 
fun "fun" where "fun (FunDom f X) = f"


105 
fun dom where "dom (FunDom f X) = X"

47619

106 


107 
definition "show_st S = (\<lambda>x. (x, fun S x)) ` dom S"


108 


109 
value [code] "show_st (FunDom (\<lambda>x. 1::int) {''a'',''b''})"


110 


111 
definition "show_acom = map_acom (Option.map show_st)"


112 
definition "show_acom_opt = Option.map show_acom"


113 


114 
definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"


115 


116 
lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"


117 
by(rule ext)(auto simp: update_def)


118 


119 
lemma dom_update[simp]: "dom (update S x y) = dom S"


120 
by(simp add: update_def)


121 


122 
definition "\<gamma>_st \<gamma> F = {f. \<forall>x\<in>dom F. f x \<in> \<gamma>(fun F x)}"


123 


124 


125 
instantiation st :: (preord) preord


126 
begin


127 


128 
definition le_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" where


129 
"F \<sqsubseteq> G = (dom F = dom G \<and> (\<forall>x \<in> dom F. fun F x \<sqsubseteq> fun G x))"


130 


131 
instance


132 
proof


133 
case goal2 thus ?case by(auto simp: le_st_def)(metis preord_class.le_trans)


134 
qed (auto simp: le_st_def)


135 


136 
end


137 


138 
instantiation st :: (join) join


139 
begin


140 


141 
definition join_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" where


142 
"F \<squnion> G = FunDom (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"


143 


144 
instance ..


145 


146 
end


147 

49396

148 
instantiation st :: (type) L

47619

149 
begin


150 

49396

151 
definition L_st :: "vname set \<Rightarrow> 'a st set" where


152 
"L X = {F. dom F = X}"

47619

153 


154 
instance ..


155 


156 
end


157 

49396

158 
instantiation st :: (semilattice) semilatticeL

47619

159 
begin


160 


161 
definition top_st where "top c = FunDom (\<lambda>x. \<top>) (vars c)"


162 


163 
instance


164 
proof

49396

165 
qed (auto simp: le_st_def join_st_def top_st_def L_st_def)

47619

166 


167 
end


168 


169 

49399

170 
text{* Trick to make code generator happy. *}


171 
lemma [code]: "L = (L :: _ \<Rightarrow> _ st set)"


172 
by(rule refl)


173 
(* L is not used in the code but is part of a type class that is used.


174 
Hence the code generator wants to build a dictionary with L in it.


175 
But L is not executable. This looping defn makes it look as if it were. *)


176 


177 

47619

178 
lemma mono_fun: "F \<sqsubseteq> G \<Longrightarrow> x : dom F \<Longrightarrow> fun F x \<sqsubseteq> fun G x"


179 
by(auto simp: le_st_def)


180 


181 
lemma mono_update[simp]:


182 
"a1 \<sqsubseteq> a2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> update S1 x a1 \<sqsubseteq> update S2 x a2"


183 
by(auto simp add: le_st_def update_def)


184 


185 

49396

186 
locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"

47619

187 
begin


188 

49497

189 
abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set"


190 
where "\<gamma>\<^isub>s == \<gamma>_st \<gamma>"

47619

191 


192 
abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"

49497

193 
where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>s"

47619

194 


195 
abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"


196 
where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"


197 

49497

198 
lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (top c) = UNIV"

47619

199 
by(auto simp: top_st_def \<gamma>_st_def)


200 


201 
lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (top c) = UNIV"


202 
by (simp add: top_option_def)


203 


204 
(* FIXME (maybe also le \<rightarrow> sqle?) *)


205 

49497

206 
lemma mono_gamma_s: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"

47619

207 
apply(simp add:\<gamma>_st_def subset_iff le_st_def split: if_splits)


208 
by (metis mono_gamma subsetD)


209 


210 
lemma mono_gamma_o:


211 
"S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"

49497

212 
by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)

47619

213 


214 
lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"


215 
by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)


216 


217 
lemma in_gamma_option_iff:


218 
"x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"


219 
by (cases u) auto


220 


221 
end


222 


223 
end
