author wenzelm
Wed, 24 Oct 2007 19:21:40 +0200
changeset 25174 d70d6dbc3a60
parent 25171 4a9c25bffc9b
child 29235 2d62b637fa80
permissions -rw-r--r--
be explicit about .ML files;

(*  Title:      StateSpaceLocale.thy
    ID:         $Id$
    Author:     Norbert Schirmer, TU Muenchen

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

theory StateSpaceLocale imports StateFun 
uses "state_space.ML" "state_fun.ML"

setup StateFun.setup

text {* For every type that is to be stored in a state space, an
instance of this locale is imported in order convert the abstract and
concrete values.*}

locale project_inject =
 fixes project :: "'value \<Rightarrow> 'a"
 and   "inject":: "'a \<Rightarrow> 'value"
 assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"

lemma (in project_inject)
 ex_project [statefun_simp]: "\<exists>v. project v = x"
  apply (rule_tac x= "inject x" in exI)
  apply (simp add: project_inject_cancel)

lemma (in project_inject)
 project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
  by (rule ext) (simp add: project_inject_cancel)

lemma (in project_inject)
 project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
  by (rule ext) (simp add: project_inject_cancel)