(* Author: Tobias Nipkow *) theory Abs_State imports Abs_Int0_fun "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord" (* Library import merely to allow string lists to be sorted for output *) begin subsection "Abstract State with Computable Ordering" text{* A concrete type of state with computable @{text"\"}: *} datatype 'a st = FunDom "vname \ 'a" "vname list" fun "fun" where "fun (FunDom f xs) = f" fun dom where "dom (FunDom f xs) = xs" definition [simp]: "inter_list xs ys = [x\xs. x \ set ys]" definition "show_st S = [(x,fun S x). x \ sort(dom S)]" definition "show_acom = map_acom (Option.map show_st)" definition "show_acom_opt = Option.map show_acom" definition "lookup F x = (if x : set(dom F) then fun F x else \)" definition "update F x y = FunDom ((fun F)(x:=y)) (if x \ set(dom F) then dom F else x # dom F)" lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)" by(rule ext)(auto simp: lookup_def update_def) definition "\_st \ F = {f. \x. f x \ \(lookup F x)}" instantiation st :: (SL_top) SL_top begin definition "le_st F G = (ALL x : set(dom G). lookup F x \ fun G x)" definition "join_st F G = FunDom (\x. fun F x \ fun G x) (inter_list (dom F) (dom G))" definition "\ = FunDom (\x. \) []" instance proof case goal2 thus ?case apply(auto simp: le_st_def) by (metis lookup_def preord_class.le_trans top) qed (auto simp: le_st_def lookup_def join_st_def Top_st_def) end lemma mono_lookup: "F \ F' \ lookup F x \ lookup F' x" by(auto simp add: lookup_def le_st_def) lemma mono_update: "a \ a' \ S \ S' \ update S x a \ update S' x a'" by(auto simp add: le_st_def lookup_def update_def) locale Gamma = Val_abs where \=\ for \ :: "'av::SL_top \ val set" begin abbreviation \\<^isub>f :: "'av st \ state set" where "\\<^isub>f == \_st \" abbreviation \\<^isub>o :: "'av st option \ state set" where "\\<^isub>o == \_option \\<^isub>f" abbreviation \\<^isub>c :: "'av st option acom \ state set acom" where "\\<^isub>c == map_acom \\<^isub>o" lemma gamma_f_Top[simp]: "\\<^isub>f Top = UNIV" by(auto simp: Top_st_def \_st_def lookup_def) lemma gamma_o_Top[simp]: "\\<^isub>o Top = UNIV" by (simp add: Top_option_def) (* FIXME (maybe also le \ sqle?) *) lemma mono_gamma_f: "f \ g \ \\<^isub>f f \ \\<^isub>f g" apply(simp add:\_st_def subset_iff lookup_def le_st_def split: if_splits) by (metis UNIV_I mono_gamma gamma_Top subsetD) lemma mono_gamma_o: "sa \ sa' \ \\<^isub>o sa \ \\<^isub>o sa'" by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f) lemma mono_gamma_c: "ca \ ca' \ \\<^isub>c ca \ \\<^isub>c ca'" by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o) lemma in_gamma_option_iff: "x : \_option r u \ (\u'. u = Some u' \ x : r u')" by (cases u) auto end end