author | nipkow |
Sat, 31 Dec 2011 17:53:50 +0100 | |
changeset 46063 | 81ebd0cdb300 |
parent 46039 | 698de142f6f9 |
child 46334 | 3858dc8eabd8 |
permissions | -rw-r--r-- |
45111 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
theory Abs_State |
|
4 |
imports Abs_Int0_fun |
|
5 |
"~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord" |
|
6 |
(* Library import merely to allow string lists to be sorted for output *) |
|
7 |
begin |
|
8 |
||
9 |
subsection "Abstract State with Computable Ordering" |
|
10 |
||
11 |
text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *} |
|
12 |
||
45212 | 13 |
datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list" |
45111 | 14 |
|
15 |
fun "fun" where "fun (FunDom f _) = f" |
|
16 |
fun dom where "dom (FunDom _ A) = A" |
|
17 |
||
18 |
definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]" |
|
19 |
||
20 |
definition "show_st S = [(x,fun S x). x \<leftarrow> sort(dom S)]" |
|
21 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
22 |
definition "show_acom = map_acom (Option.map show_st)" |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
23 |
definition "show_acom_opt = Option.map show_acom" |
45111 | 24 |
|
25 |
definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)" |
|
26 |
||
27 |
definition "update F x y = |
|
28 |
FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)" |
|
29 |
||
30 |
lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)" |
|
31 |
by(rule ext)(auto simp: lookup_def update_def) |
|
32 |
||
46039 | 33 |
definition "\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(lookup F x)}" |
45111 | 34 |
|
35 |
instantiation st :: (SL_top) SL_top |
|
36 |
begin |
|
37 |
||
38 |
definition "le_st F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)" |
|
39 |
||
40 |
definition |
|
41 |
"join_st F G = |
|
42 |
FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))" |
|
43 |
||
44 |
definition "\<top> = FunDom (\<lambda>x. \<top>) []" |
|
45 |
||
46 |
instance |
|
47 |
proof |
|
48 |
case goal2 thus ?case |
|
49 |
apply(auto simp: le_st_def) |
|
50 |
by (metis lookup_def preord_class.le_trans top) |
|
51 |
qed (auto simp: le_st_def lookup_def join_st_def Top_st_def) |
|
52 |
||
53 |
end |
|
54 |
||
55 |
lemma mono_lookup: "F \<sqsubseteq> F' \<Longrightarrow> lookup F x \<sqsubseteq> lookup F' x" |
|
56 |
by(auto simp add: lookup_def le_st_def) |
|
57 |
||
58 |
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'" |
|
59 |
by(auto simp add: le_st_def lookup_def update_def) |
|
60 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
61 |
context Val_abs |
45111 | 62 |
begin |
63 |
||
46063 | 64 |
abbreviation \<gamma>\<^isub>f :: "'av st \<Rightarrow> state set" |
46039 | 65 |
where "\<gamma>\<^isub>f == \<gamma>_st \<gamma>" |
45111 | 66 |
|
46063 | 67 |
abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set" |
46039 | 68 |
where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f" |
45111 | 69 |
|
46063 | 70 |
abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom" |
46039 | 71 |
where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o" |
45111 | 72 |
|
46039 | 73 |
lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV" |
74 |
by(auto simp: Top_st_def \<gamma>_st_def lookup_def) |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
75 |
|
46039 | 76 |
lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
77 |
by (simp add: Top_option_def) |
45111 | 78 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
79 |
(* FIXME (maybe also le \<rightarrow> sqle?) *) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
80 |
|
46039 | 81 |
lemma mono_gamma_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g" |
82 |
apply(simp add:\<gamma>_st_def subset_iff lookup_def le_st_def split: if_splits) |
|
83 |
by (metis UNIV_I mono_gamma gamma_Top subsetD) |
|
45111 | 84 |
|
46039 | 85 |
lemma mono_gamma_o: |
86 |
"sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>o sa \<subseteq> \<gamma>\<^isub>o sa'" |
|
87 |
by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f) |
|
45111 | 88 |
|
46039 | 89 |
lemma mono_gamma_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'" |
90 |
by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o) |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
91 |
|
46039 | 92 |
lemma in_gamma_option_iff: |
93 |
"x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')" |
|
45111 | 94 |
by (cases u) auto |
95 |
||
96 |
end |
|
97 |
||
98 |
end |