# Theory Abs_State

Up to index of Isabelle/HOL/HOL-IMP

theory Abs_State
imports Abs_Int0
`(* Author: Tobias Nipkow *)theory Abs_Stateimports Abs_Int0beginsubsubsection "Set-based lattices"instantiation com :: varsbeginfun vars_com :: "com => vname set" where"vars com.SKIP = {}" |"vars (x::=e) = {x} ∪ vars e" |"vars (c1;c2) = vars c1 ∪ vars c2" |"vars (IF b THEN c1 ELSE c2) = vars b ∪ vars c1 ∪ vars c2" |"vars (WHILE b DO c) = vars b ∪ vars c"instance ..endlemma finite_avars: "finite(vars(a::aexp))"by(induction a) simp_alllemma finite_bvars: "finite(vars(b::bexp))"by(induction b) (simp_all add: finite_avars)lemma finite_cvars: "finite(vars(c::com))"by(induction c) (simp_all add: finite_avars finite_bvars)class L =fixes L :: "vname set => 'a set"instantiation acom :: (L)Lbegindefinition L_acom where"L X = {C. vars(strip C) ⊆ X ∧ (∀a ∈ set(annos C). a ∈ L X)}"instance ..endinstantiation option :: (L)Lbegindefinition L_option where"L X = {opt. case opt of None => True | Some x => x ∈ L X}"lemma L_option_simps[simp]: "None ∈ L X" "(Some x ∈ L X) = (x ∈ L X)"by(simp_all add: L_option_def)instance ..endclass semilatticeL = join + L +fixes top :: "com => 'a"assumes join_ge1 [simp]: "x ∈ L X ==> y ∈ L X ==> x \<sqsubseteq> x \<squnion> y"and join_ge2 [simp]: "x ∈ L X ==> y ∈ L X ==> y \<sqsubseteq> x \<squnion> y"and join_least[simp]: "x \<sqsubseteq> z ==> y \<sqsubseteq> z ==> x \<squnion> y \<sqsubseteq> z"and top[simp]: "x ∈ L(vars c) ==> x \<sqsubseteq> top c"and top_in_L[simp]: "top c ∈ L(vars c)"and join_in_L[simp]: "x ∈ L X ==> y ∈ L X ==> x \<squnion> y ∈ L X"notation (input) top ("\<top>⇘_⇙")notation (latex output) top ("\<top>⇘\isa{_}⇙")instantiation option :: (semilatticeL)semilatticeLbegindefinition top_option where "top c = Some(top c)"instance proof  case goal1 thus ?case by(cases x, simp, cases y, simp_all)next  case goal2 thus ?case by(cases y, simp, cases x, simp_all)next  case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)next  case goal4 thus ?case by(cases x, simp_all add: top_option_def)next  case goal5 thus ?case by(simp add: top_option_def)next  case goal6 thus ?case by(simp add: L_option_def split: option.splits)qedendsubsection "Abstract State with Computable Ordering"hide_type  st  --"to avoid long names"text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}datatype 'a st = FunDom "vname => 'a" "vname set"fun "fun" where "fun (FunDom f X) = f"fun dom where "dom (FunDom f X) = X"definition "show_st S = (λx. (x, fun S x)) ` dom S"value [code] "show_st (FunDom (λx. 1::int) {''a'',''b''})"definition "show_acom = map_acom (Option.map show_st)"definition "show_acom_opt = Option.map show_acom"definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"by(rule ext)(auto simp: update_def)lemma dom_update[simp]: "dom (update S x y) = dom S"by(simp add: update_def)definition "γ_st γ F = {f. ∀x∈dom F. f x ∈ γ(fun F x)}"instantiation st :: (preord) preordbegindefinition le_st :: "'a st => 'a st => bool" where"F \<sqsubseteq> G = (dom F = dom G ∧ (∀x ∈ dom F. fun F x \<sqsubseteq> fun G x))"instanceproof  case goal2 thus ?case by(auto simp: le_st_def)(metis preord_class.le_trans)qed (auto simp: le_st_def)endinstantiation st :: (join) joinbegindefinition join_st :: "'a st => 'a st => 'a st" where"F \<squnion> G = FunDom (λx. fun F x \<squnion> fun G x) (dom F)"instance ..endinstantiation st :: (type) Lbegindefinition L_st :: "vname set => 'a st set" where"L X = {F. dom F = X}"instance ..endinstantiation st :: (semilattice) semilatticeLbegindefinition top_st where "top c = FunDom (λx. \<top>) (vars c)"instanceproofqed (auto simp: le_st_def join_st_def top_st_def L_st_def)endtext{* Trick to make code generator happy. *}lemma [code]: "L = (L :: _ => _ st set)"by(rule refl)(* L is not used in the code but is part of a type class that is used.   Hence the code generator wants to build a dictionary with L in it.   But L is not executable. This looping defn makes it look as if it were. *)lemma mono_fun: "F \<sqsubseteq> G ==> x : dom F ==> fun F x \<sqsubseteq> fun G x"by(auto simp: le_st_def)lemma mono_update[simp]:  "a1 \<sqsubseteq> a2 ==> S1 \<sqsubseteq> S2 ==> update S1 x a1 \<sqsubseteq> update S2 x a2"by(auto simp add: le_st_def update_def)locale Gamma = Val_abs where γ=γ for γ :: "'av::semilattice => val set"beginabbreviation γ⇣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 (top c) = UNIV"by(auto simp: top_st_def γ_st_def)lemma gamma_o_Top[simp]: "γ⇣o (top c) = UNIV"by (simp add: top_option_def)(* FIXME (maybe also le -> sqle?) *)lemma mono_gamma_s: "f \<sqsubseteq> g ==> γ⇣s f ⊆ γ⇣s g"apply(simp add:γ_st_def subset_iff le_st_def split: if_splits)by (metis mono_gamma subsetD)lemma mono_gamma_o:  "S1 \<sqsubseteq> S2 ==> γ⇣o S1 ⊆ γ⇣o S2"by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)lemma mono_gamma_c: "C1 \<sqsubseteq> C2 ==> γ⇣c C1 ≤ γ⇣c C2"by (induction C1 C2 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) autoendend`