src/HOL/IMP/Abs_State.thy

renamed name -> vname

(* 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"\<sqsubseteq>"}: *}

datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"

fun "fun" where "fun (FunDom f _) = f"
fun dom where "dom (FunDom _ A) = A"

definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"

definition "show_st S = [(x,fun S x). x \<leftarrow> sort(dom S)]"

fun show_st_up where
"show_st_up Bot = Bot" |
"show_st_up (Up S) = Up(show_st S)"

definition "show_acom = map_acom show_st_up"
definition "show_acom_opt = Option.map show_acom"

definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)"

definition "update F x y =
  FunDom ((fun F)(x:=y)) (if x \<in> 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 "rep_st rep F = {f. \<forall>x. f x \<in> rep(lookup F x)}"

instantiation st :: (SL_top) SL_top
begin

definition "le_st F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"

definition
"join_st F G =
 FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"

definition "\<top> = FunDom (\<lambda>x. \<top>) []"

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 \<sqsubseteq> F' \<Longrightarrow> lookup F x \<sqsubseteq> lookup F' x"
by(auto simp add: lookup_def le_st_def)

lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
by(auto simp add: le_st_def lookup_def update_def)

context Val_abs
begin

abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
"s <:f S == s \<in> rep_st rep S"

notation fun_in_rep (infix "<:\<^sub>f" 50)

lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T"
apply(auto simp add: rep_st_def le_st_def dest: le_rep)
by (metis in_rep_Top le_rep lookup_def subsetD)

abbreviation in_rep_up :: "state \<Rightarrow> 'a st up \<Rightarrow> bool"  (infix "<:up" 50)
where "s <:up S == s : rep_up (rep_st rep) S"

notation (output) in_rep_up (infix "<:\<^sub>u\<^sub>p" 50)

lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T"
by (cases S) (auto intro:fun_in_rep_le)

lemma in_rep_up_iff: "x <:up u \<longleftrightarrow> (\<exists>u'. u = Up u' \<and> x <:f u')"
by (cases u) auto

lemma in_rep_Top_fun: "s <:f \<top>"
by(simp add: rep_st_def lookup_def Top_st_def)

lemma in_rep_Top_up: "s <:up \<top>"
by(simp add: Top_up_def in_rep_Top_fun)

end

end