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