Theory Abs_State

(* Author: Tobias Nipkow *)

subsection "Computable State"

theory Abs_State
imports Abs_Int0
begin

type_synonym 'a st_rep = "(vname * 'a) list"

fun fun_rep :: "('a::top) st_rep ⇒ vname ⇒ 'a" where
"fun_rep [] = (λx. ⊤)" |
"fun_rep ((x,a)#ps) = (fun_rep ps) (x := a)"

lemma fun_rep_map_of[code]: ― ‹original def is too slow›
  "fun_rep ps = (%x. case map_of ps x of None ⇒ ⊤ | Some a ⇒ a)"
by(induction ps rule: fun_rep.induct) auto

definition eq_st :: "('a::top) st_rep ⇒ 'a st_rep ⇒ bool" where
"eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"

hide_type st  ― ‹hide previous def to avoid long names›
declare [[typedef_overloaded]] ― ‹allow quotient types to depend on classes›

quotient_type 'a st = "('a::top) st_rep" / eq_st
morphisms rep_st St
by (metis eq_st_def equivpI reflpI sympI transpI)

lift_definition update :: "('a::top) st ⇒ vname ⇒ 'a ⇒ 'a st"
  is "λps x a. (x,a)#ps"
by(auto simp: eq_st_def)

lift_definition "fun" :: "('a::top) st ⇒ vname ⇒ 'a" is fun_rep
by(simp add: eq_st_def)

definition show_st :: "vname set ⇒ ('a::top) st ⇒ (vname * 'a)set" where
"show_st X S = (λx. (x, fun S x)) ` X"

definition "show_acom C = map_acom (map_option (show_st (vars(strip C)))) C"
definition "show_acom_opt = map_option show_acom"

lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
by transfer auto

definition γ_st :: "(('a::top) ⇒ 'b set) ⇒ 'a st ⇒ (vname ⇒ 'b) set" where
"γ_st γ F = {f. ∀x. f x ∈ γ(fun F x)}"

instantiation st :: (order_top) order
begin

definition less_eq_st_rep :: "'a st_rep ⇒ 'a st_rep ⇒ bool" where
"less_eq_st_rep ps1 ps2 =
  ((∀x ∈ set(map fst ps1) ∪ set(map fst ps2). fun_rep ps1 x ≤ fun_rep ps2 x))"

lemma less_eq_st_rep_iff:
  "less_eq_st_rep r1 r2 = (∀x. fun_rep r1 x ≤ fun_rep r2 x)"
apply(auto simp: less_eq_st_rep_def fun_rep_map_of split: option.split)
apply (metis Un_iff map_of_eq_None_iff option.distinct(1))
apply (metis Un_iff map_of_eq_None_iff option.distinct(1))
done

corollary less_eq_st_rep_iff_fun:
  "less_eq_st_rep r1 r2 = (fun_rep r1 ≤ fun_rep r2)"
by (metis less_eq_st_rep_iff le_fun_def)

lift_definition less_eq_st :: "'a st ⇒ 'a st ⇒ bool" is less_eq_st_rep
by(auto simp add: eq_st_def less_eq_st_rep_iff)

definition less_st where "F < (G::'a st) = (F ≤ G ∧ ¬ G ≤ F)"

instance
proof (standard, goal_cases)
  case 1 show ?case by(rule less_st_def)
next
  case 2 show ?case by transfer (auto simp: less_eq_st_rep_def)
next
  case 3 thus ?case by transfer (metis less_eq_st_rep_iff order_trans)
next
  case 4 thus ?case
    by transfer (metis less_eq_st_rep_iff eq_st_def fun_eq_iff antisym)
qed

end

lemma le_st_iff: "(F ≤ G) = (∀x. fun F x ≤ fun G x)"
by transfer (rule less_eq_st_rep_iff)

fun map2_st_rep :: "('a::top ⇒ 'a ⇒ 'a) ⇒ 'a st_rep ⇒ 'a st_rep ⇒ 'a st_rep" where
"map2_st_rep f [] ps2 = map (%(x,y). (x, f ⊤ y)) ps2" |
"map2_st_rep f ((x,y)#ps1) ps2 =
  (let y2 = fun_rep ps2 x
   in (x,f y y2) # map2_st_rep f ps1 ps2)"

lemma fun_rep_map2_rep[simp]: "f ⊤ ⊤ = ⊤ ⟹
  fun_rep (map2_st_rep f ps1 ps2) = (λx. f (fun_rep ps1 x) (fun_rep ps2 x))"
apply(induction f ps1 ps2 rule: map2_st_rep.induct)
apply(simp add: fun_rep_map_of map_of_map fun_eq_iff split: option.split)
apply(fastforce simp: fun_rep_map_of fun_eq_iff split:option.splits)
done

instantiation st :: (semilattice_sup_top) semilattice_sup_top
begin

lift_definition sup_st :: "'a st ⇒ 'a st ⇒ 'a st" is "map2_st_rep (⊔)"
by (simp add: eq_st_def)

lift_definition top_st :: "'a st" is "[]" .

instance
proof (standard, goal_cases)
  case 1 show ?case by transfer (simp add:less_eq_st_rep_iff)
next
  case 2 show ?case by transfer (simp add:less_eq_st_rep_iff)
next
  case 3 thus ?case by transfer (simp add:less_eq_st_rep_iff)
next
  case 4 show ?case by transfer (simp add:less_eq_st_rep_iff fun_rep_map_of)
qed

end

lemma fun_top: "fun ⊤ = (λx. ⊤)"
by transfer simp

lemma mono_update[simp]:
  "a1 ≤ a2 ⟹ S1 ≤ S2 ⟹ update S1 x a1 ≤ update S2 x a2"
by transfer (auto simp add: less_eq_st_rep_def)

lemma mono_fun: "S1 ≤ S2 ⟹ fun S1 x ≤ fun S2 x"
by transfer (simp add: less_eq_st_rep_iff)

locale Gamma_semilattice = Val_semilattice where γ=γ
  for γ :: "'av::semilattice_sup_top ⇒ val set"
begin

abbreviation γ⇩s :: "'av st ⇒ state set"
where "γ⇩s == γ_st γ"

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

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

lemma gamma_s_top[simp]: "γ⇩s ⊤ = UNIV"
by(auto simp: γ_st_def fun_top)

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

lemma mono_gamma_s: "f ≤ g ⟹ γ⇩s f ⊆ γ⇩s g"
by(simp add:γ_st_def le_st_iff subset_iff) (metis mono_gamma subsetD)

lemma mono_gamma_o:
  "S1 ≤ S2 ⟹ γ⇩o S1 ⊆ γ⇩o S2"
by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)

lemma mono_gamma_c: "C1 ≤ C2 ⟹ γ⇩c C1 ≤ γ⇩c C2"
by (simp add: less_eq_acom_def mono_gamma_o size_annos anno_map_acom size_annos_same[of C1 C2])

lemma in_gamma_option_iff:
  "x ∈ γ_option r u ⟷ (∃u'. u = Some u' ∧ x ∈ r u')"
by (cases u) auto

end

end