diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/Statespace/StateFun.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Statespace/StateFun.thy	Wed Oct 24 18:36:09 2007 +0200
@@ -0,0 +1,115 @@
+(*  Title:      StateFun.thy
+    ID:         $Id$
+    Author:     Norbert Schirmer, TU Muenchen
+*)
+
+header {* State Space Representation as Function \label{sec:StateFun}*}
+
+theory StateFun imports DistinctTreeProver 
+(*uses "state_space.ML" (state_fun)*)
+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.  *} 
+
+constdefs K_statefun:: "'a \<Rightarrow> 'b \<Rightarrow> 'a" "K_statefun c x \<equiv> 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 \<circ> f) = K_statefun c"
+  by (rule ext) (simp add: K_statefun_apply comp_def)
+
+lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
+  by (rule refl)
+
+constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
+"lookup destr n s \<equiv> destr (s n)"
+
+constdefs update:: 
+  "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
+"update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
+
+lemma lookup_update_same:
+  "(\<And>v. destr (constr v) = v) \<Longrightarrow> 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\<noteq>m \<Longrightarrow> 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:
+"(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id"
+  by (rule ext) simp
+
+
+
+lemma block_conj_cong: "(P \<and> Q) = (P \<and> Q)"
+  by simp
+
+lemma conj1_False: "(P\<equiv>False) \<Longrightarrow> (P \<and> Q) \<equiv> False"
+  by simp
+
+lemma conj2_False: "\<lbrakk>Q\<equiv>False\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> False"
+  by simp
+
+lemma conj_True: "\<lbrakk>P\<equiv>True; Q\<equiv>True\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> True"
+  by simp
+
+lemma conj_cong: "\<lbrakk>P\<equiv>P'; Q\<equiv>Q'\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> 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: "\<exists>x. id x = y"
+  by (simp add: id_def)
+
+lemma swap_ex_eq: 
+  "\<exists>s. f s = x \<equiv> True \<Longrightarrow>
+   \<exists>s. x = f s \<equiv> 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
+
+(*use "state_fun"
+setup StateFun.setup
+*)
+end
\ No newline at end of file