1(* Title: HOL/Statespace/StateSpaceLocale.thy 2 Author: Norbert Schirmer, TU Muenchen 3*) 4 5section \<open>Setup for State Space Locales \label{sec:StateSpaceLocale}\<close> 6 7theory StateSpaceLocale imports StateFun 8keywords "statespace" :: thy_decl 9begin 10 11ML_file "state_space.ML" 12ML_file "state_fun.ML" 13 14text \<open>For every type that is to be stored in a state space, an 15instance of this locale is imported in order convert the abstract and 16concrete values.\<close> 17 18 19locale 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" 23begin 24 25lemma ex_project [statefun_simp]: "\<exists>v. project v = x" 26proof 27 show "project (inject x) = x" 28 by (rule project_inject_cancel) 29qed 30 31lemma project_inject_comp_id [statefun_simp]: "project \<circ> inject = id" 32 by (rule ext) (simp add: project_inject_cancel) 33 34lemma project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f" 35 by (rule ext) (simp add: project_inject_cancel) 36 37end 38 39end 40