|
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 |
|
13 datatype 'a st = FunDom "name \<Rightarrow> 'a" "name list" |
|
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 |
|
22 fun show_st_up where |
|
23 "show_st_up Bot = Bot" | |
|
24 "show_st_up (Up S) = Up(show_st S)" |
|
25 |
|
26 definition "show_acom = map_acom show_st_up" |
|
27 |
|
28 definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)" |
|
29 |
|
30 definition "update F x y = |
|
31 FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)" |
|
32 |
|
33 lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)" |
|
34 by(rule ext)(auto simp: lookup_def update_def) |
|
35 |
|
36 definition "rep_st rep F = {f. \<forall>x. f x \<in> rep(lookup F x)}" |
|
37 |
|
38 instantiation st :: (SL_top) SL_top |
|
39 begin |
|
40 |
|
41 definition "le_st F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)" |
|
42 |
|
43 definition |
|
44 "join_st F G = |
|
45 FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))" |
|
46 |
|
47 definition "\<top> = FunDom (\<lambda>x. \<top>) []" |
|
48 |
|
49 instance |
|
50 proof |
|
51 case goal2 thus ?case |
|
52 apply(auto simp: le_st_def) |
|
53 by (metis lookup_def preord_class.le_trans top) |
|
54 qed (auto simp: le_st_def lookup_def join_st_def Top_st_def) |
|
55 |
|
56 end |
|
57 |
|
58 lemma mono_lookup: "F \<sqsubseteq> F' \<Longrightarrow> lookup F x \<sqsubseteq> lookup F' x" |
|
59 by(auto simp add: lookup_def le_st_def) |
|
60 |
|
61 lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'" |
|
62 by(auto simp add: le_st_def lookup_def update_def) |
|
63 |
|
64 context Rep |
|
65 begin |
|
66 |
|
67 abbreviation fun_in_rep :: "(name \<Rightarrow> 'b) \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where |
|
68 "s <:f S == s \<in> rep_st rep S" |
|
69 |
|
70 notation fun_in_rep (infix "<:\<^sub>f" 50) |
|
71 |
|
72 lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T" |
|
73 apply(auto simp add: rep_st_def le_st_def dest: le_rep) |
|
74 by (metis in_rep_Top le_rep lookup_def subsetD) |
|
75 |
|
76 abbreviation in_rep_up :: "(name \<Rightarrow> 'b) \<Rightarrow> 'a st up \<Rightarrow> bool" (infix "<:up" 50) |
|
77 where "s <:up S == s : rep_up (rep_st rep) S" |
|
78 |
|
79 notation (output) in_rep_up (infix "<:\<^sub>u\<^sub>p" 50) |
|
80 |
|
81 lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T" |
|
82 by (cases S) (auto intro:fun_in_rep_le) |
|
83 |
|
84 lemma in_rep_up_iff: "x <:up u \<longleftrightarrow> (\<exists>u'. u = Up u' \<and> x <:f u')" |
|
85 by (cases u) auto |
|
86 |
|
87 lemma in_rep_Top_fun: "s <:f \<top>" |
|
88 by(simp add: rep_st_def lookup_def Top_st_def) |
|
89 |
|
90 lemma in_rep_Top_up: "s <:up \<top>" |
|
91 by(simp add: Top_up_def in_rep_Top_fun) |
|
92 |
|
93 end |
|
94 |
|
95 end |