src/HOL/Statespace/StateSpaceLocale.thy
author haftmann
Fri Jan 02 08:12:46 2009 +0100 (2009-01-02)
changeset 29332 edc1e2a56398
parent 29247 95d3a82857e5
child 38838 62f6ba39b3d4
permissions -rw-r--r--
named code theorem for Fract_norm
     1 (*  Title:      StateSpaceLocale.thy
     2     ID:         $Id$
     3     Author:     Norbert Schirmer, TU Muenchen
     4 *)
     5 
     6 header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}
     7 
     8 theory StateSpaceLocale imports StateFun 
     9 uses "state_space.ML" "state_fun.ML"
    10 begin
    11 
    12 setup StateFun.setup
    13 
    14 text {* For every type that is to be stored in a state space, an
    15 instance of this locale is imported in order convert the abstract and
    16 concrete values.*}
    17 
    18 
    19 locale project_inject =
    20  fixes project :: "'value \<Rightarrow> 'a"
    21  and   "inject":: "'a \<Rightarrow> 'value"
    22  assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
    23 
    24 lemma (in project_inject)
    25  ex_project [statefun_simp]: "\<exists>v. project v = x"
    26   apply (rule_tac x= "inject x" in exI)
    27   apply (simp add: project_inject_cancel)
    28   done
    29 
    30 lemma (in project_inject)
    31  project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
    32   by (rule ext) (simp add: project_inject_cancel)
    33 
    34 lemma (in project_inject)
    35  project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
    36   by (rule ext) (simp add: project_inject_cancel)
    37 
    38 
    39 
    40 end