44656
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
45111
|
3 |
theory Abs_State_den
|
|
4 |
imports Abs_Int_den0_fun
|
44932
|
5 |
"~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
|
|
6 |
(* Library import merely to allow string lists to be sorted for output *)
|
44656
|
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 astate = FunDom "string \<Rightarrow> 'a" "string list"
|
|
14 |
|
|
15 |
fun "fun" where "fun (FunDom f _) = f"
|
|
16 |
fun dom where "dom (FunDom _ A) = A"
|
|
17 |
|
44932
|
18 |
definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
|
|
19 |
|
|
20 |
definition "list S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
|
44656
|
21 |
|
|
22 |
definition "lookup F x = (if x : set(dom F) then fun F x else Top)"
|
|
23 |
|
|
24 |
definition "update F x y =
|
44932
|
25 |
FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
|
44656
|
26 |
|
|
27 |
lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
|
|
28 |
by(rule ext)(auto simp: lookup_def update_def)
|
|
29 |
|
|
30 |
instantiation astate :: (SL_top) SL_top
|
|
31 |
begin
|
|
32 |
|
|
33 |
definition "le_astate F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
|
|
34 |
|
|
35 |
definition
|
|
36 |
"join_astate F G =
|
44932
|
37 |
FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
|
44656
|
38 |
|
44923
|
39 |
definition "Top = FunDom (\<lambda>x. Top) []"
|
44656
|
40 |
|
|
41 |
instance
|
|
42 |
proof
|
|
43 |
case goal2 thus ?case
|
|
44 |
apply(auto simp: le_astate_def)
|
|
45 |
by (metis lookup_def preord_class.le_trans top)
|
|
46 |
qed (auto simp: le_astate_def lookup_def join_astate_def Top_astate_def)
|
|
47 |
|
|
48 |
end
|
|
49 |
|
|
50 |
end
|