Theory Abs_State

(* Author: Tobias Nipkow *)

section "Abstract State with Computable Ordering"

theory Abs_State
imports Abs_Int0
  "HOL-Library.Char_ord" "HOL-Library.List_Lexorder"
  (* Library import merely to allow string lists to be sorted for output *)
begin

text‹A concrete type of state with computable ‹⊑›:›

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 (map_option show_st)"
definition "show_acom_opt = map_option 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 = (∀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 (standard, goal_cases)
  case 2 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 γ⇩f :: "'av st ⇒ state set"
where "γ⇩f == γ_st γ"

abbreviation γ⇩o :: "'av st option ⇒ state set"
where "γ⇩o == γ_option γ⇩f"

abbreviation γ⇩c :: "'av st option acom ⇒ state set acom"
where "γ⇩c == map_acom γ⇩o"

lemma gamma_f_Top[simp]: "γ⇩f Top = UNIV"
by(auto simp: Top_st_def γ_st_def lookup_def)

lemma gamma_o_Top[simp]: "γ⇩o Top = UNIV"
by (simp add: Top_option_def)

(* FIXME (maybe also le → sqle?) *)

lemma mono_gamma_f: "f ⊑ g ⟹ γ⇩f f ⊆ γ⇩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' ⟹ γ⇩o sa ⊆ γ⇩o sa'"
by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f)

lemma mono_gamma_c: "ca ⊑ ca' ⟹ γ⇩c ca ≤ γ⇩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