25171
|
1 |
(* Title: StateFun.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Norbert Schirmer, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* State Space Representation as Function \label{sec:StateFun}*}
|
|
7 |
|
|
8 |
theory StateFun imports DistinctTreeProver
|
|
9 |
begin
|
|
10 |
|
|
11 |
|
|
12 |
text {* The state space is represented as a function from names to
|
|
13 |
values. We neither fix the type of names nor the type of values. We
|
|
14 |
define lookup and update functions and provide simprocs that simplify
|
|
15 |
expressions containing these, similar to HOL-records.
|
|
16 |
|
|
17 |
The lookup and update function get constructor/destructor functions as
|
|
18 |
parameters. These are used to embed various HOL-types into the
|
|
19 |
abstract value type. Conceptually the abstract value type is a sum of
|
|
20 |
all types that we attempt to store in the state space.
|
|
21 |
|
|
22 |
The update is actually generalized to a map function. The map supplies
|
|
23 |
better compositionality, especially if you think of nested state
|
|
24 |
spaces. *}
|
|
25 |
|
|
26 |
constdefs K_statefun:: "'a \<Rightarrow> 'b \<Rightarrow> 'a" "K_statefun c x \<equiv> c"
|
|
27 |
|
|
28 |
lemma K_statefun_apply [simp]: "K_statefun c x = c"
|
|
29 |
by (simp add: K_statefun_def)
|
|
30 |
|
|
31 |
lemma K_statefun_comp [simp]: "(K_statefun c \<circ> f) = K_statefun c"
|
|
32 |
by (rule ext) (simp add: K_statefun_apply comp_def)
|
|
33 |
|
|
34 |
lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
|
|
35 |
by (rule refl)
|
|
36 |
|
|
37 |
constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
|
|
38 |
"lookup destr n s \<equiv> destr (s n)"
|
|
39 |
|
|
40 |
constdefs update::
|
|
41 |
"('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
|
|
42 |
"update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
|
|
43 |
|
|
44 |
lemma lookup_update_same:
|
|
45 |
"(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) =
|
|
46 |
f (destr (s n))"
|
|
47 |
by (simp add: lookup_def update_def)
|
|
48 |
|
|
49 |
lemma lookup_update_id_same:
|
|
50 |
"lookup destr n (update destr' id n (K_statefun (lookup id n s')) s) =
|
|
51 |
lookup destr n s'"
|
|
52 |
by (simp add: lookup_def update_def)
|
|
53 |
|
|
54 |
lemma lookup_update_other:
|
|
55 |
"n\<noteq>m \<Longrightarrow> lookup destr n (update destr' constr m f s) = lookup destr n s"
|
|
56 |
by (simp add: lookup_def update_def)
|
|
57 |
|
|
58 |
|
|
59 |
lemma id_id_cancel: "id (id x) = x"
|
|
60 |
by (simp add: id_def)
|
|
61 |
|
|
62 |
lemma destr_contstr_comp_id:
|
|
63 |
"(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id"
|
|
64 |
by (rule ext) simp
|
|
65 |
|
|
66 |
|
|
67 |
|
|
68 |
lemma block_conj_cong: "(P \<and> Q) = (P \<and> Q)"
|
|
69 |
by simp
|
|
70 |
|
|
71 |
lemma conj1_False: "(P\<equiv>False) \<Longrightarrow> (P \<and> Q) \<equiv> False"
|
|
72 |
by simp
|
|
73 |
|
|
74 |
lemma conj2_False: "\<lbrakk>Q\<equiv>False\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> False"
|
|
75 |
by simp
|
|
76 |
|
|
77 |
lemma conj_True: "\<lbrakk>P\<equiv>True; Q\<equiv>True\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> True"
|
|
78 |
by simp
|
|
79 |
|
|
80 |
lemma conj_cong: "\<lbrakk>P\<equiv>P'; Q\<equiv>Q'\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> Q')"
|
|
81 |
by simp
|
|
82 |
|
|
83 |
|
|
84 |
lemma update_apply: "(update destr constr n f s x) =
|
|
85 |
(if x=n then constr (f (destr (s n))) else s x)"
|
|
86 |
by (simp add: update_def)
|
|
87 |
|
|
88 |
lemma ex_id: "\<exists>x. id x = y"
|
|
89 |
by (simp add: id_def)
|
|
90 |
|
|
91 |
lemma swap_ex_eq:
|
|
92 |
"\<exists>s. f s = x \<equiv> True \<Longrightarrow>
|
|
93 |
\<exists>s. x = f s \<equiv> True"
|
|
94 |
apply (rule eq_reflection)
|
|
95 |
apply auto
|
|
96 |
done
|
|
97 |
|
|
98 |
lemmas meta_ext = eq_reflection [OF ext]
|
|
99 |
|
|
100 |
(* This lemma only works if the store is welltyped:
|
|
101 |
"\<exists>x. s ''n'' = (c x)"
|
|
102 |
or in general when c (d x) = x,
|
|
103 |
(for example: c=id and d=id)
|
|
104 |
*)
|
|
105 |
lemma "update d c n (K_statespace (lookup d n s)) s = s"
|
|
106 |
apply (simp add: update_def lookup_def)
|
|
107 |
apply (rule ext)
|
|
108 |
apply simp
|
|
109 |
oops
|
|
110 |
|
|
111 |
end |