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