src/HOL/Statespace/StateSpaceLocale.thy
author wenzelm
Thu Mar 14 16:55:06 2019 +0100 (5 weeks ago)
changeset 69913 ca515cf61651
parent 69605 a96320074298
permissions -rw-r--r--
more specific keyword kinds;
wenzelm@41959
     1
(*  Title:      HOL/Statespace/StateSpaceLocale.thy
schirmer@25171
     2
    Author:     Norbert Schirmer, TU Muenchen
schirmer@25171
     3
*)
schirmer@25171
     4
wenzelm@63167
     5
section \<open>Setup for State Space Locales \label{sec:StateSpaceLocale}\<close>
schirmer@25171
     6
schirmer@25171
     7
theory StateSpaceLocale imports StateFun 
wenzelm@69913
     8
keywords "statespace" :: thy_defn
schirmer@25171
     9
begin
schirmer@25171
    10
wenzelm@69605
    11
ML_file \<open>state_space.ML\<close>
wenzelm@69605
    12
ML_file \<open>state_fun.ML\<close>
schirmer@25171
    13
wenzelm@63167
    14
text \<open>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
wenzelm@63167
    16
concrete values.\<close>
schirmer@25171
    17
schirmer@25171
    18
norbert@29247
    19
locale project_inject =
schirmer@25171
    20
 fixes project :: "'value \<Rightarrow> 'a"
wenzelm@38838
    21
  and inject :: "'a \<Rightarrow> 'value"
schirmer@25171
    22
 assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
wenzelm@45358
    23
begin
schirmer@25171
    24
wenzelm@45358
    25
lemma ex_project [statefun_simp]: "\<exists>v. project v = x"
wenzelm@45358
    26
proof
wenzelm@45358
    27
  show "project (inject x) = x"
wenzelm@45358
    28
    by (rule project_inject_cancel)
wenzelm@45358
    29
qed
schirmer@25171
    30
wenzelm@45358
    31
lemma project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
schirmer@25171
    32
  by (rule ext) (simp add: project_inject_cancel)
schirmer@25171
    33
wenzelm@45358
    34
lemma 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
wenzelm@45358
    37
end
schirmer@25171
    38
nipkow@62390
    39
end