equal
deleted
inserted
replaced
1 (* Title: StateSpaceLocale.thy |
1 (* Title: StateSpaceLocale.thy |
2 ID: $Id$ |
|
3 Author: Norbert Schirmer, TU Muenchen |
2 Author: Norbert Schirmer, TU Muenchen |
4 *) |
3 *) |
5 |
4 |
6 header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*} |
5 header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*} |
7 |
6 |
16 concrete values.*} |
15 concrete values.*} |
17 |
16 |
18 |
17 |
19 locale project_inject = |
18 locale project_inject = |
20 fixes project :: "'value \<Rightarrow> 'a" |
19 fixes project :: "'value \<Rightarrow> 'a" |
21 and "inject":: "'a \<Rightarrow> 'value" |
20 and inject :: "'a \<Rightarrow> 'value" |
22 assumes project_inject_cancel [statefun_simp]: "project (inject x) = x" |
21 assumes project_inject_cancel [statefun_simp]: "project (inject x) = x" |
23 |
22 |
24 lemma (in project_inject) |
23 lemma (in project_inject) |
25 ex_project [statefun_simp]: "\<exists>v. project v = x" |
24 ex_project [statefun_simp]: "\<exists>v. project v = x" |
26 apply (rule_tac x= "inject x" in exI) |
25 apply (rule_tac x= "inject x" in exI) |