(* 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"
by (simp add: K_statefun_def)
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))
"
by (simp add: lookup_def update_def)
lemma lookup_update_id_same:
"lookup destr n (update destr' id n (K_statefun (lookup id n s')) s) =
lookup destr n s
'"
by (simp add: lookup_def update_def)
lemma lookup_update_other:
"n\m \ lookup destr n (update destr' constr m f s) = lookup destr n s"
by (simp add: lookup_def update_def)
lemma id_id_cancel:
"id (id x) = x"
by (simp add: id_def)
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)
"
by (simp add: update_def)
lemma ex_id:
"\x. id x = y"
by (simp add: id_def)
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:
"\<exists>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"
apply (simp add: update_def lookup_def)
apply (rule ext)
apply simp
oops
end
