src/HOL/Statespace/StateFun.thy
changeset 25171 4a9c25bffc9b
child 25174 d70d6dbc3a60
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Statespace/StateFun.thy	Wed Oct 24 18:36:09 2007 +0200
     1.3 @@ -0,0 +1,115 @@
     1.4 +(*  Title:      StateFun.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Norbert Schirmer, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* State Space Representation as Function \label{sec:StateFun}*}
    1.10 +
    1.11 +theory StateFun imports DistinctTreeProver 
    1.12 +(*uses "state_space.ML" (state_fun)*)
    1.13 +begin
    1.14 +
    1.15 +
    1.16 +text {* The state space is represented as a function from names to
    1.17 +values. We neither fix the type of names nor the type of values. We
    1.18 +define lookup and update functions and provide simprocs that simplify
    1.19 +expressions containing these, similar to HOL-records.
    1.20 +
    1.21 +The lookup and update function get constructor/destructor functions as
    1.22 +parameters. These are used to embed various HOL-types into the
    1.23 +abstract value type. Conceptually the abstract value type is a sum of
    1.24 +all types that we attempt to store in the state space.
    1.25 +
    1.26 +The update is actually generalized to a map function. The map supplies
    1.27 +better compositionality, especially if you think of nested state
    1.28 +spaces.  *} 
    1.29 +
    1.30 +constdefs K_statefun:: "'a \<Rightarrow> 'b \<Rightarrow> 'a" "K_statefun c x \<equiv> c"
    1.31 +
    1.32 +lemma K_statefun_apply [simp]: "K_statefun c x = c"
    1.33 +  by (simp add: K_statefun_def)
    1.34 +
    1.35 +lemma K_statefun_comp [simp]: "(K_statefun c \<circ> f) = K_statefun c"
    1.36 +  by (rule ext) (simp add: K_statefun_apply comp_def)
    1.37 +
    1.38 +lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
    1.39 +  by (rule refl)
    1.40 +
    1.41 +constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
    1.42 +"lookup destr n s \<equiv> destr (s n)"
    1.43 +
    1.44 +constdefs update:: 
    1.45 +  "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
    1.46 +"update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
    1.47 +
    1.48 +lemma lookup_update_same:
    1.49 +  "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) = 
    1.50 +         f (destr (s n))"  
    1.51 +  by (simp add: lookup_def update_def)
    1.52 +
    1.53 +lemma lookup_update_id_same:
    1.54 +  "lookup destr n (update destr' id n (K_statefun (lookup id n s')) s) =                  
    1.55 +     lookup destr n s'"  
    1.56 +  by (simp add: lookup_def update_def)
    1.57 +
    1.58 +lemma lookup_update_other:
    1.59 +  "n\<noteq>m \<Longrightarrow> lookup destr n (update destr' constr m f s) = lookup destr n s"  
    1.60 +  by (simp add: lookup_def update_def)
    1.61 +
    1.62 +
    1.63 +lemma id_id_cancel: "id (id x) = x" 
    1.64 +  by (simp add: id_def)
    1.65 +  
    1.66 +lemma destr_contstr_comp_id:
    1.67 +"(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id"
    1.68 +  by (rule ext) simp
    1.69 +
    1.70 +
    1.71 +
    1.72 +lemma block_conj_cong: "(P \<and> Q) = (P \<and> Q)"
    1.73 +  by simp
    1.74 +
    1.75 +lemma conj1_False: "(P\<equiv>False) \<Longrightarrow> (P \<and> Q) \<equiv> False"
    1.76 +  by simp
    1.77 +
    1.78 +lemma conj2_False: "\<lbrakk>Q\<equiv>False\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> False"
    1.79 +  by simp
    1.80 +
    1.81 +lemma conj_True: "\<lbrakk>P\<equiv>True; Q\<equiv>True\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> True"
    1.82 +  by simp
    1.83 +
    1.84 +lemma conj_cong: "\<lbrakk>P\<equiv>P'; Q\<equiv>Q'\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> Q')"
    1.85 +  by simp
    1.86 +
    1.87 +
    1.88 +lemma update_apply: "(update destr constr n f s x) = 
    1.89 +     (if x=n then constr (f (destr (s n))) else s x)"
    1.90 +  by (simp add: update_def)
    1.91 +
    1.92 +lemma ex_id: "\<exists>x. id x = y"
    1.93 +  by (simp add: id_def)
    1.94 +
    1.95 +lemma swap_ex_eq: 
    1.96 +  "\<exists>s. f s = x \<equiv> True \<Longrightarrow>
    1.97 +   \<exists>s. x = f s \<equiv> True"
    1.98 +  apply (rule eq_reflection)
    1.99 +  apply auto
   1.100 +  done
   1.101 +
   1.102 +lemmas meta_ext = eq_reflection [OF ext]
   1.103 +
   1.104 +(* This lemma only works if the store is welltyped:
   1.105 +    "\<exists>x.  s ''n'' = (c x)" 
   1.106 +   or in general when c (d x) = x,
   1.107 +     (for example: c=id and d=id)
   1.108 + *)
   1.109 +lemma "update d c n (K_statespace (lookup d n s)) s = s"
   1.110 +  apply (simp add: update_def lookup_def)
   1.111 +  apply (rule ext)
   1.112 +  apply simp
   1.113 +  oops
   1.114 +
   1.115 +(*use "state_fun"
   1.116 +setup StateFun.setup
   1.117 +*)
   1.118 +end
   1.119 \ No newline at end of file