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--
     1 (*  Title:      StateSpaceLocale.thy

     2     Author:     Norbert Schirmer, TU Muenchen

     3 *)

     4

     5 header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}

     6

     7 theory StateSpaceLocale imports StateFun

     8 uses "state_space.ML" "state_fun.ML"

     9 begin

    10

    11 setup StateFun.setup

    12

    13 text {* For every type that is to be stored in a state space, an

    14 instance of this locale is imported in order convert the abstract and

    15 concrete values.*}

    16

    17

    18 locale project_inject =

    19  fixes project :: "'value \<Rightarrow> 'a"

    20   and inject :: "'a \<Rightarrow> 'value"

    21  assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"

    22

    23 lemma (in project_inject)

    24  ex_project [statefun_simp]: "\<exists>v. project v = x"

    25   apply (rule_tac x= "inject x" in exI)

    26   apply (simp add: project_inject_cancel)

    27   done

    28

    29 lemma (in project_inject)

    30  project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"

    31   by (rule ext) (simp add: project_inject_cancel)

    32

    33 lemma (in project_inject)

    34  project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"

    35   by (rule ext) (simp add: project_inject_cancel)

    36

    37

    38

    39 end