1(* Title: HOL/Statespace/StateFun.thy 2 Author: Norbert Schirmer, TU Muenchen 3*) 4 5section \<open>State Space Representation as Function \label{sec:StateFun}\<close> 6 7theory StateFun imports DistinctTreeProver 8begin 9 10 11text \<open>The state space is represented as a function from names to 12values. We neither fix the type of names nor the type of values. We 13define lookup and update functions and provide simprocs that simplify 14expressions containing these, similar to HOL-records. 15 16The lookup and update function get constructor/destructor functions as 17parameters. These are used to embed various HOL-types into the 18abstract value type. Conceptually the abstract value type is a sum of 19all types that we attempt to store in the state space. 20 21The update is actually generalized to a map function. The map supplies 22better compositionality, especially if you think of nested state 23spaces.\<close> 24 25definition K_statefun :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where "K_statefun c x \<equiv> c" 26 27lemma K_statefun_apply [simp]: "K_statefun c x = c" 28 by (simp add: K_statefun_def) 29 30lemma K_statefun_comp [simp]: "(K_statefun c \<circ> f) = K_statefun c" 31 by (rule ext) (simp add: comp_def) 32 33lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x" 34 by (rule refl) 35 36definition lookup :: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a" 37 where "lookup destr n s = destr (s n)" 38 39definition update :: 40 "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)" 41 where "update destr constr n f s = s(n := constr (f (destr (s n))))" 42 43lemma lookup_update_same: 44 "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) = 45 f (destr (s n))" 46 by (simp add: lookup_def update_def) 47 48lemma lookup_update_id_same: 49 "lookup destr n (update destr' id n (K_statefun (lookup id n s')) s) = 50 lookup destr n s'" 51 by (simp add: lookup_def update_def) 52 53lemma lookup_update_other: 54 "n\<noteq>m \<Longrightarrow> lookup destr n (update destr' constr m f s) = lookup destr n s" 55 by (simp add: lookup_def update_def) 56 57 58lemma id_id_cancel: "id (id x) = x" 59 by (simp add: id_def) 60 61lemma destr_contstr_comp_id: "(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id" 62 by (rule ext) simp 63 64 65 66lemma block_conj_cong: "(P \<and> Q) = (P \<and> Q)" 67 by simp 68 69lemma conj1_False: "P \<equiv> False \<Longrightarrow> (P \<and> Q) \<equiv> False" 70 by simp 71 72lemma conj2_False: "Q \<equiv> False \<Longrightarrow> (P \<and> Q) \<equiv> False" 73 by simp 74 75lemma conj_True: "P \<equiv> True \<Longrightarrow> Q \<equiv> True \<Longrightarrow> (P \<and> Q) \<equiv> True" 76 by simp 77 78lemma conj_cong: "P \<equiv> P' \<Longrightarrow> Q \<equiv> Q' \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> Q')" 79 by simp 80 81 82lemma update_apply: "(update destr constr n f s x) = 83 (if x=n then constr (f (destr (s n))) else s x)" 84 by (simp add: update_def) 85 86lemma ex_id: "\<exists>x. id x = y" 87 by (simp add: id_def) 88 89lemma swap_ex_eq: 90 "\<exists>s. f s = x \<equiv> True \<Longrightarrow> 91 \<exists>s. x = f s \<equiv> True" 92 apply (rule eq_reflection) 93 apply auto 94 done 95 96lemmas meta_ext = eq_reflection [OF ext] 97 98(* This lemma only works if the store is welltyped: 99 "\<exists>x. s ''n'' = (c x)" 100 or in general when c (d x) = x, 101 (for example: c=id and d=id) 102 *) 103lemma "update d c n (K_statespace (lookup d n s)) s = s" 104 apply (simp add: update_def lookup_def) 105 apply (rule ext) 106 apply simp 107 oops 108 109end 110