src/HOL/Statespace/StateSpaceLocale.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 63167 0909deb8059b
child 69605 a96320074298
permissions -rw-r--r--
more fundamental definition of div and mod on int
     1 (*  Title:      HOL/Statespace/StateSpaceLocale.thy
     2     Author:     Norbert Schirmer, TU Muenchen
     3 *)
     4 
     5 section \<open>Setup for State Space Locales \label{sec:StateSpaceLocale}\<close>
     6 
     7 theory StateSpaceLocale imports StateFun 
     8 keywords "statespace" :: thy_decl
     9 begin
    10 
    11 ML_file "state_space.ML"
    12 ML_file "state_fun.ML"
    13 
    14 text \<open>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.\<close>
    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 begin
    24 
    25 lemma ex_project [statefun_simp]: "\<exists>v. project v = x"
    26 proof
    27   show "project (inject x) = x"
    28     by (rule project_inject_cancel)
    29 qed
    30 
    31 lemma project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
    32   by (rule ext) (simp add: project_inject_cancel)
    33 
    34 lemma project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
    35   by (rule ext) (simp add: project_inject_cancel)
    36 
    37 end
    38 
    39 end