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