src/HOL/Statespace/StateSpaceLocale.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 38838 62f6ba39b3d4
child 41959 b460124855b8
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
schirmer@25171
     1
(*  Title:      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@25174
     8
uses "state_space.ML" "state_fun.ML"
schirmer@25171
     9
begin
schirmer@25171
    10
schirmer@25171
    11
setup StateFun.setup
schirmer@25171
    12
schirmer@25171
    13
text {* For every type that is to be stored in a state space, an
schirmer@25171
    14
instance of this locale is imported in order convert the abstract and
schirmer@25171
    15
concrete values.*}
schirmer@25171
    16
schirmer@25171
    17
norbert@29247
    18
locale project_inject =
schirmer@25171
    19
 fixes project :: "'value \<Rightarrow> 'a"
wenzelm@38838
    20
  and inject :: "'a \<Rightarrow> 'value"
schirmer@25171
    21
 assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
schirmer@25171
    22
schirmer@25171
    23
lemma (in project_inject)
schirmer@25171
    24
 ex_project [statefun_simp]: "\<exists>v. project v = x"
schirmer@25171
    25
  apply (rule_tac x= "inject x" in exI)
schirmer@25171
    26
  apply (simp add: project_inject_cancel)
schirmer@25171
    27
  done
schirmer@25171
    28
schirmer@25171
    29
lemma (in project_inject)
schirmer@25171
    30
 project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
schirmer@25171
    31
  by (rule ext) (simp add: project_inject_cancel)
schirmer@25171
    32
schirmer@25171
    33
lemma (in project_inject)
schirmer@25171
    34
 project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
schirmer@25171
    35
  by (rule ext) (simp add: project_inject_cancel)
schirmer@25171
    36
schirmer@25171
    37
schirmer@25171
    38
schirmer@25171
    39
end