equal
deleted
inserted
replaced
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) |