equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory Abs_State_den |
|
4 imports Abs_Int_den0_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 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 |
|
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)]" |
|
21 |
|
22 definition "lookup F x = (if x : set(dom F) then fun F x else Top)" |
|
23 |
|
24 definition "update F x y = |
|
25 FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)" |
|
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 = |
|
37 FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))" |
|
38 |
|
39 definition "Top = FunDom (\<lambda>x. Top) []" |
|
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 |
|