src/HOL/Statespace/StateSpaceLocale.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45358 4849133d7a78
child 46950 d0181abdbdac
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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 uses "state_space.ML" "state_fun.ML"
     9 begin
    10 
    11 setup StateFun.setup
    12 
    13 text {* For every type that is to be stored in a state space, an
    14 instance of this locale is imported in order convert the abstract and
    15 concrete values.*}
    16 
    17 
    18 locale project_inject =
    19  fixes project :: "'value \<Rightarrow> 'a"
    20   and inject :: "'a \<Rightarrow> 'value"
    21  assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
    22 begin
    23 
    24 lemma ex_project [statefun_simp]: "\<exists>v. project v = x"
    25 proof
    26   show "project (inject x) = x"
    27     by (rule project_inject_cancel)
    28 qed
    29 
    30 lemma project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
    31   by (rule ext) (simp add: project_inject_cancel)
    32 
    33 lemma project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
    34   by (rule ext) (simp add: project_inject_cancel)
    35 
    36 end
    37 
    38 end