src/HOL/Statespace/StateSpaceLocale.thy
author Norbert Schirmer <norbert.schirmer@web.de>
Thu, 18 Dec 2008 11:16:48 +0100
changeset 29247 95d3a82857e5
parent 29235 2d62b637fa80
child 38838 62f6ba39b3d4
permissions -rw-r--r--
adapted statespace module to new locales;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     1
(*  Title:      StateSpaceLocale.thy
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     2
    ID:         $Id$
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     3
    Author:     Norbert Schirmer, TU Muenchen
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     4
*)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     5
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     6
header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     7
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     8
theory StateSpaceLocale imports StateFun 
25174
d70d6dbc3a60 be explicit about .ML files;
wenzelm
parents: 25171
diff changeset
     9
uses "state_space.ML" "state_fun.ML"
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    10
begin
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    11
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    12
setup StateFun.setup
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    13
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    14
text {* For every type that is to be stored in a state space, an
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    15
instance of this locale is imported in order convert the abstract and
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    16
concrete values.*}
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    17
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    18
29247
95d3a82857e5 adapted statespace module to new locales;
Norbert Schirmer <norbert.schirmer@web.de>
parents: 29235
diff changeset
    19
locale project_inject =
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    20
 fixes project :: "'value \<Rightarrow> 'a"
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    21
 and   "inject":: "'a \<Rightarrow> 'value"
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    22
 assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    23
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    24
lemma (in project_inject)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    25
 ex_project [statefun_simp]: "\<exists>v. project v = x"
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    26
  apply (rule_tac x= "inject x" in exI)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    27
  apply (simp add: project_inject_cancel)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    28
  done
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    29
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    30
lemma (in project_inject)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    31
 project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    32
  by (rule ext) (simp add: project_inject_cancel)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    33
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    34
lemma (in project_inject)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    35
 project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    36
  by (rule ext) (simp add: project_inject_cancel)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    37
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    38
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    39
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    40
end