src/HOL/Statespace/StateSpaceLocale.thy
author hoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51474 1e9e68247ad1
parent 48891 c0eafbd55de3
child 58825 2065f49da190
permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
wenzelm@41959
     1
(*  Title:      HOL/Statespace/StateSpaceLocale.thy
schirmer@25171
     2
    Author:     Norbert Schirmer, TU Muenchen
schirmer@25171
     3
*)
schirmer@25171
     4
schirmer@25171
     5
header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}
schirmer@25171
     6
schirmer@25171
     7
theory StateSpaceLocale imports StateFun 
wenzelm@46950
     8
keywords "statespace" :: thy_decl
schirmer@25171
     9
begin
schirmer@25171
    10
wenzelm@48891
    11
ML_file "state_space.ML"
wenzelm@48891
    12
ML_file "state_fun.ML"
schirmer@25171
    13
setup StateFun.setup
schirmer@25171
    14
schirmer@25171
    15
text {* For every type that is to be stored in a state space, an
schirmer@25171
    16
instance of this locale is imported in order convert the abstract and
schirmer@25171
    17
concrete values.*}
schirmer@25171
    18
schirmer@25171
    19
norbert@29247
    20
locale project_inject =
schirmer@25171
    21
 fixes project :: "'value \<Rightarrow> 'a"
wenzelm@38838
    22
  and inject :: "'a \<Rightarrow> 'value"
schirmer@25171
    23
 assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
wenzelm@45358
    24
begin
schirmer@25171
    25
wenzelm@45358
    26
lemma ex_project [statefun_simp]: "\<exists>v. project v = x"
wenzelm@45358
    27
proof
wenzelm@45358
    28
  show "project (inject x) = x"
wenzelm@45358
    29
    by (rule project_inject_cancel)
wenzelm@45358
    30
qed
schirmer@25171
    31
wenzelm@45358
    32
lemma project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
schirmer@25171
    33
  by (rule ext) (simp add: project_inject_cancel)
schirmer@25171
    34
wenzelm@45358
    35
lemma project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
schirmer@25171
    36
  by (rule ext) (simp add: project_inject_cancel)
schirmer@25171
    37
wenzelm@45358
    38
end
schirmer@25171
    39
schirmer@25171
    40
end