# Theory StateFun

theory StateFun
imports DistinctTreeProver
(*  Title:      HOL/Statespace/StateFun.thy    Author:     Norbert Schirmer, TU Muenchen*)header {* State Space Representation as Function \label{sec:StateFun}*}theory StateFun imports DistinctTreeProver begintext {* The state space is represented as a function from names tovalues. We neither fix the type of names nor the type of values. Wedefine lookup and update functions and provide simprocs that simplifyexpressions containing these, similar to HOL-records.The lookup and update function get constructor/destructor functions asparameters. These are used to embed various HOL-types into theabstract value type. Conceptually the abstract value type is a sum ofall types that we attempt to store in the state space.The update is actually generalized to a map function. The map suppliesbetter compositionality, especially if you think of nested statespaces.  *} 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 o 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 o constr = id"  by (rule ext) simplemma block_conj_cong: "(P ∧ Q) = (P ∧ Q)"  by simplemma conj1_False: "P ≡ False ==> (P ∧ Q) ≡ False"  by simplemma conj2_False: "Q ≡ False ==> (P ∧ Q) ≡ False"  by simplemma conj_True: "P ≡ True ==> Q ≡ True ==> (P ∧ Q) ≡ True"  by simplemma conj_cong: "P ≡ P' ==> Q ≡ Q' ==> (P ∧ Q) ≡ (P' ∧ Q')"  by simplemma 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  donelemmas 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"  apply (simp add: update_def lookup_def)  apply (rule ext)  apply simp  oopsend