src/HOL/Statespace/StateFun.thy
author schirmer
Wed Oct 24 18:36:09 2007 +0200 (2007-10-24)
changeset 25171 4a9c25bffc9b
child 25174 d70d6dbc3a60
permissions -rw-r--r--
added Statespace library
     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 (*uses "state_space.ML" (state_fun)*)
    10 begin
    11 
    12 
    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.
    17 
    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.
    22 
    23 The update is actually generalized to a map function. The map supplies
    24 better compositionality, especially if you think of nested state
    25 spaces.  *} 
    26 
    27 constdefs K_statefun:: "'a \<Rightarrow> 'b \<Rightarrow> 'a" "K_statefun c x \<equiv> c"
    28 
    29 lemma K_statefun_apply [simp]: "K_statefun c x = c"
    30   by (simp add: K_statefun_def)
    31 
    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)
    34 
    35 lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
    36   by (rule refl)
    37 
    38 constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
    39 "lookup destr n s \<equiv> destr (s n)"
    40 
    41 constdefs update:: 
    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))))"
    44 
    45 lemma lookup_update_same:
    46   "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) = 
    47          f (destr (s n))"  
    48   by (simp add: lookup_def update_def)
    49 
    50 lemma lookup_update_id_same:
    51   "lookup destr n (update destr' id n (K_statefun (lookup id n s')) s) =                  
    52      lookup destr n s'"  
    53   by (simp add: lookup_def update_def)
    54 
    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)
    58 
    59 
    60 lemma id_id_cancel: "id (id x) = x" 
    61   by (simp add: id_def)
    62   
    63 lemma destr_contstr_comp_id:
    64 "(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id"
    65   by (rule ext) simp
    66 
    67 
    68 
    69 lemma block_conj_cong: "(P \<and> Q) = (P \<and> Q)"
    70   by simp
    71 
    72 lemma conj1_False: "(P\<equiv>False) \<Longrightarrow> (P \<and> Q) \<equiv> False"
    73   by simp
    74 
    75 lemma conj2_False: "\<lbrakk>Q\<equiv>False\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> False"
    76   by simp
    77 
    78 lemma conj_True: "\<lbrakk>P\<equiv>True; Q\<equiv>True\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> True"
    79   by simp
    80 
    81 lemma conj_cong: "\<lbrakk>P\<equiv>P'; Q\<equiv>Q'\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> Q')"
    82   by simp
    83 
    84 
    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)
    88 
    89 lemma ex_id: "\<exists>x. id x = y"
    90   by (simp add: id_def)
    91 
    92 lemma swap_ex_eq: 
    93   "\<exists>s. f s = x \<equiv> True \<Longrightarrow>
    94    \<exists>s. x = f s \<equiv> True"
    95   apply (rule eq_reflection)
    96   apply auto
    97   done
    98 
    99 lemmas meta_ext = eq_reflection [OF ext]
   100 
   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)
   105  *)
   106 lemma "update d c n (K_statespace (lookup d n s)) s = s"
   107   apply (simp add: update_def lookup_def)
   108   apply (rule ext)
   109   apply simp
   110   oops
   111 
   112 (*use "state_fun"
   113 setup StateFun.setup
   114 *)
   115 end