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
schirmer@25171
     1
(*  Title:      StateSpaceLocale.thy
schirmer@25171
     2
    ID:         $Id$
schirmer@25171
     3
    Author:     Norbert Schirmer, TU Muenchen
schirmer@25171
     4
*)
schirmer@25171
     5
schirmer@25171
     6
header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}
schirmer@25171
     7
schirmer@25171
     8
theory StateSpaceLocale imports StateFun 
wenzelm@25174
     9
uses "state_space.ML" "state_fun.ML"
schirmer@25171
    10
begin
schirmer@25171
    11
schirmer@25171
    12
setup StateFun.setup
schirmer@25171
    13
schirmer@25171
    14
text {* For every type that is to be stored in a state space, an
schirmer@25171
    15
instance of this locale is imported in order convert the abstract and
schirmer@25171
    16
concrete values.*}
schirmer@25171
    17
schirmer@25171
    18
norbert@29247
    19
locale project_inject =
schirmer@25171
    20
 fixes project :: "'value \<Rightarrow> 'a"
schirmer@25171
    21
 and   "inject":: "'a \<Rightarrow> 'value"
schirmer@25171
    22
 assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
schirmer@25171
    23
schirmer@25171
    24
lemma (in project_inject)
schirmer@25171
    25
 ex_project [statefun_simp]: "\<exists>v. project v = x"
schirmer@25171
    26
  apply (rule_tac x= "inject x" in exI)
schirmer@25171
    27
  apply (simp add: project_inject_cancel)
schirmer@25171
    28
  done
schirmer@25171
    29
schirmer@25171
    30
lemma (in project_inject)
schirmer@25171
    31
 project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
schirmer@25171
    32
  by (rule ext) (simp add: project_inject_cancel)
schirmer@25171
    33
schirmer@25171
    34
lemma (in project_inject)
schirmer@25171
    35
 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
schirmer@25171
    38
schirmer@25171
    39
schirmer@25171
    40
end