# Theory StateFun

theory StateFun
imports DistinctTreeProver
(*  Title:      HOL/Statespace/StateFun.thy
Author:     Norbert Schirmer, TU Muenchen
*)

section ‹State Space Representation as Function \label{sec:StateFun}›

theory StateFun imports DistinctTreeProver
begin

text ‹The state space is represented as a function from names to
values. We neither fix the type of names nor the type of values. We
define lookup and update functions and provide simprocs that simplify
expressions containing these, similar to HOL-records.

The lookup and update function get constructor/destructor functions as
parameters. These are used to embed various HOL-types into the
abstract value type. Conceptually the abstract value type is a sum of
all types that we attempt to store in the state space.

The update is actually generalized to a map function. The map supplies
better compositionality, especially if you think of nested state
spaces.›

definition K_statefun :: "'a ⇒ 'b ⇒ 'a" where "K_statefun c x ≡ c"

lemma K_statefun_apply [simp]: "K_statefun c x = c"

lemma K_statefun_comp [simp]: "(K_statefun c ∘ f) = K_statefun c"
by (rule ext) (simp add: comp_def)

lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
by (rule refl)

definition lookup :: "('v ⇒ 'a) ⇒ 'n ⇒ ('n ⇒ 'v) ⇒ 'a"
where "lookup destr n s = destr (s n)"

definition update ::
"('v ⇒ 'a1) ⇒ ('a2 ⇒ 'v) ⇒ 'n ⇒ ('a1 ⇒ 'a2) ⇒ ('n ⇒ 'v) ⇒ ('n ⇒ 'v)"
where "update destr constr n f s = s(n := constr (f (destr (s n))))"

lemma lookup_update_same:
"(⋀v. destr (constr v) = v) ⟹ lookup destr n (update destr constr n f s) =
f (destr (s n))"

lemma lookup_update_id_same:
"lookup destr n (update destr' id n (K_statefun (lookup id n s')) s) =
lookup destr n s'"

lemma lookup_update_other:
"n≠m ⟹ lookup destr n (update destr' constr m f s) = lookup destr n s"

lemma id_id_cancel: "id (id x) = x"

lemma destr_contstr_comp_id: "(⋀v. destr (constr v) = v) ⟹ destr ∘ constr = id"
by (rule ext) simp

lemma block_conj_cong: "(P ∧ Q) = (P ∧ Q)"
by simp

lemma conj1_False: "P ≡ False ⟹ (P ∧ Q) ≡ False"
by simp

lemma conj2_False: "Q ≡ False ⟹ (P ∧ Q) ≡ False"
by simp

lemma conj_True: "P ≡ True ⟹ Q ≡ True ⟹ (P ∧ Q) ≡ True"
by simp

lemma conj_cong: "P ≡ P' ⟹ Q ≡ Q' ⟹ (P ∧ Q) ≡ (P' ∧ Q')"
by simp

lemma update_apply: "(update destr constr n f s x) =
(if x=n then constr (f (destr (s n))) else s x)"

lemma ex_id: "∃x. id x = y"

lemma swap_ex_eq:
"∃s. f s = x ≡ True ⟹
∃s. x = f s ≡ True"
apply (rule eq_reflection)
apply auto
done

lemmas meta_ext = eq_reflection [OF ext]

(* This lemma only works if the store is welltyped:
"∃x.  s ''n'' = (c x)"
or in general when c (d x) = x,
(for example: c=id and d=id)
*)
lemma "update d c n (K_statespace (lookup d n s)) s = s"