src/HOL/Statespace/StateFun.thy
changeset 35114 b1fd1d756e20
parent 25408 156f6f7082b8
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Statespace/StateFun.thy	Thu Feb 11 22:19:58 2010 +0100
     1.2 +++ b/src/HOL/Statespace/StateFun.thy	Thu Feb 11 22:55:16 2010 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      StateFun.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Norbert Schirmer, TU Muenchen
     1.7  *)
     1.8  
     1.9 @@ -34,12 +33,12 @@
    1.10  lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
    1.11    by (rule refl)
    1.12  
    1.13 -constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
    1.14 -"lookup destr n s \<equiv> destr (s n)"
    1.15 +definition lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
    1.16 +  where "lookup destr n s = destr (s n)"
    1.17  
    1.18 -constdefs update:: 
    1.19 +definition update::
    1.20    "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
    1.21 -"update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
    1.22 +  where "update destr constr n f s = s(n := constr (f (destr (s n))))"
    1.23  
    1.24  lemma lookup_update_same:
    1.25    "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) =