src/HOL/Statespace/StateFun.thy
changeset 35114 b1fd1d756e20
parent 25408 156f6f7082b8
child 35416 d8d7d1b785af
equal deleted inserted replaced
35113:1a0c129bb2e0 35114:b1fd1d756e20
     1 (*  Title:      StateFun.thy
     1 (*  Title:      StateFun.thy
     2     ID:         $Id$
       
     3     Author:     Norbert Schirmer, TU Muenchen
     2     Author:     Norbert Schirmer, TU Muenchen
     4 *)
     3 *)
     5 
     4 
     6 header {* State Space Representation as Function \label{sec:StateFun}*}
     5 header {* State Space Representation as Function \label{sec:StateFun}*}
     7 
     6 
    32   by (rule ext) (simp add: K_statefun_apply comp_def)
    31   by (rule ext) (simp add: K_statefun_apply comp_def)
    33 
    32 
    34 lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
    33 lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
    35   by (rule refl)
    34   by (rule refl)
    36 
    35 
    37 constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
    36 definition lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
    38 "lookup destr n s \<equiv> destr (s n)"
    37   where "lookup destr n s = destr (s n)"
    39 
    38 
    40 constdefs update:: 
    39 definition update::
    41   "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
    40   "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
    42 "update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
    41   where "update destr constr n f s = s(n := constr (f (destr (s n))))"
    43 
    42 
    44 lemma lookup_update_same:
    43 lemma lookup_update_same:
    45   "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) = 
    44   "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) = 
    46          f (destr (s n))"  
    45          f (destr (s n))"  
    47   by (simp add: lookup_def update_def)
    46   by (simp add: lookup_def update_def)