28 FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)" |
28 FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)" |
29 |
29 |
30 lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)" |
30 lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)" |
31 by(rule ext)(auto simp: lookup_def update_def) |
31 by(rule ext)(auto simp: lookup_def update_def) |
32 |
32 |
33 definition "rep_st rep F = {f. \<forall>x. f x \<in> rep(lookup F x)}" |
33 definition "\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(lookup F x)}" |
34 |
34 |
35 instantiation st :: (SL_top) SL_top |
35 instantiation st :: (SL_top) SL_top |
36 begin |
36 begin |
37 |
37 |
38 definition "le_st F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)" |
38 definition "le_st F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)" |
59 by(auto simp add: le_st_def lookup_def update_def) |
59 by(auto simp add: le_st_def lookup_def update_def) |
60 |
60 |
61 context Val_abs |
61 context Val_abs |
62 begin |
62 begin |
63 |
63 |
64 abbreviation rep_f :: "'a st \<Rightarrow> state set" ("\<gamma>\<^isub>f") |
64 abbreviation \<gamma>\<^isub>f :: "'a st \<Rightarrow> state set" |
65 where "\<gamma>\<^isub>f == rep_st rep" |
65 where "\<gamma>\<^isub>f == \<gamma>_st \<gamma>" |
66 |
66 |
67 abbreviation rep_u :: "'a st option \<Rightarrow> state set" ("\<gamma>\<^isub>u") |
67 abbreviation \<gamma>\<^isub>o :: "'a st option \<Rightarrow> state set" |
68 where "\<gamma>\<^isub>u == rep_option \<gamma>\<^isub>f" |
68 where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>f" |
69 |
69 |
70 abbreviation rep_c :: "'a st option acom \<Rightarrow> state set acom" ("\<gamma>\<^isub>c") |
70 abbreviation \<gamma>\<^isub>c :: "'a st option acom \<Rightarrow> state set acom" |
71 where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>u" |
71 where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o" |
72 |
72 |
73 lemma rep_f_Top[simp]: "rep_f Top = UNIV" |
73 lemma gamma_f_Top[simp]: "\<gamma>\<^isub>f Top = UNIV" |
74 by(auto simp: Top_st_def rep_st_def lookup_def) |
74 by(auto simp: Top_st_def \<gamma>_st_def lookup_def) |
75 |
75 |
76 lemma rep_u_Top[simp]: "rep_u Top = UNIV" |
76 lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV" |
77 by (simp add: Top_option_def) |
77 by (simp add: Top_option_def) |
78 |
78 |
79 (* FIXME (maybe also le \<rightarrow> sqle?) *) |
79 (* FIXME (maybe also le \<rightarrow> sqle?) *) |
80 |
80 |
81 lemma mono_rep_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g" |
81 lemma mono_gamma_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>f f \<subseteq> \<gamma>\<^isub>f g" |
82 apply(simp add:rep_st_def subset_iff lookup_def le_st_def split: if_splits) |
82 apply(simp add:\<gamma>_st_def subset_iff lookup_def le_st_def split: if_splits) |
83 by (metis UNIV_I mono_rep rep_Top subsetD) |
83 by (metis UNIV_I mono_gamma gamma_Top subsetD) |
84 |
84 |
85 lemma mono_rep_u: |
85 lemma mono_gamma_o: |
86 "sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^isub>u sa \<subseteq> \<gamma>\<^isub>u sa'" |
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_rep_f) |
87 by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f) |
88 |
88 |
89 lemma mono_rep_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^isub>c ca \<le> \<gamma>\<^isub>c ca'" |
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_rep_u) |
90 by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o) |
91 |
91 |
92 lemma in_rep_up_iff: "x : rep_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')" |
92 lemma in_gamma_option_iff: |
|
93 "x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')" |
93 by (cases u) auto |
94 by (cases u) auto |
94 |
95 |
95 end |
96 end |
96 |
97 |
97 end |
98 end |