3 Author: Norbert Schirmer, TU Muenchen
6 header {* State Space Representation as Function \label{sec:StateFun}*}
8 theory StateFun imports DistinctTreeProver
9 (*uses "state_space.ML" (state_fun)*)
13 text {* The state space is represented as a function from names to
14 values. We neither fix the type of names nor the type of values. We
15 define lookup and update functions and provide simprocs that simplify
16 expressions containing these, similar to HOL-records.
18 The lookup and update function get constructor/destructor functions as
19 parameters. These are used to embed various HOL-types into the
20 abstract value type. Conceptually the abstract value type is a sum of
21 all types that we attempt to store in the state space.
23 The update is actually generalized to a map function. The map supplies
24 better compositionality, especially if you think of nested state
27 constdefs K_statefun:: "'a \<Rightarrow> 'b \<Rightarrow> 'a" "K_statefun c x \<equiv> c"
29 lemma K_statefun_apply [simp]: "K_statefun c x = c"
30 by (simp add: K_statefun_def)
32 lemma K_statefun_comp [simp]: "(K_statefun c \<circ> f) = K_statefun c"
33 by (rule ext) (simp add: K_statefun_apply comp_def)
35 lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
38 constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
39 "lookup destr n s \<equiv> destr (s n)"
42 "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
43 "update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
45 lemma lookup_update_same:
46 "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) =
48 by (simp add: lookup_def update_def)
50 lemma lookup_update_id_same:
51 "lookup destr n (update destr' id n (K_statefun (lookup id n s')) s) =
53 by (simp add: lookup_def update_def)
55 lemma lookup_update_other:
56 "n\<noteq>m \<Longrightarrow> lookup destr n (update destr' constr m f s) = lookup destr n s"
57 by (simp add: lookup_def update_def)
60 lemma id_id_cancel: "id (id x) = x"
63 lemma destr_contstr_comp_id:
64 "(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id"
69 lemma block_conj_cong: "(P \<and> Q) = (P \<and> Q)"
72 lemma conj1_False: "(P\<equiv>False) \<Longrightarrow> (P \<and> Q) \<equiv> False"
75 lemma conj2_False: "\<lbrakk>Q\<equiv>False\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> False"
78 lemma conj_True: "\<lbrakk>P\<equiv>True; Q\<equiv>True\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> True"
81 lemma conj_cong: "\<lbrakk>P\<equiv>P'; Q\<equiv>Q'\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> Q')"
85 lemma update_apply: "(update destr constr n f s x) =
86 (if x=n then constr (f (destr (s n))) else s x)"
87 by (simp add: update_def)
89 lemma ex_id: "\<exists>x. id x = y"
93 "\<exists>s. f s = x \<equiv> True \<Longrightarrow>
94 \<exists>s. x = f s \<equiv> True"
95 apply (rule eq_reflection)
99 lemmas meta_ext = eq_reflection [OF ext]
101 (* This lemma only works if the store is welltyped:
102 "\<exists>x. s ''n'' = (c x)"
103 or in general when c (d x) = x,
104 (for example: c=id and d=id)
106 lemma "update d c n (K_statespace (lookup d n s)) s = s"
107 apply (simp add: update_def lookup_def)