Quelle  StateFun.thy

(*  Title:      HOL/Statespace/StateFun.thy
    Author:     Norbert Schirmer, TU Muenchen
*)

section ‹State Space Representation as Function \label{sec:StateFun}›

theory StateFun imports DistinctTreeProver 
begin


text ‹The state space is represented as a function from names to
 . We neither fix the type of names nor the type of values. We
  lookup and update functions and provide simprocs that simplify
  containing these, similar to HOL-records.

  lookup and update function get constructor/destructor functions as
 . These are used to embed various HOL-types into the
  value type. Conceptually the abstract value type is a sum of
  types that we attempt to store in the state space.

  update is actually generalized to a map function. The map supplies
  compositionality, especially if you think of nested state
 .›

definition K_statefun :: "'a ==> 'b ==> 'a" where "K_statefun c x ≡ c"

lemma K_statefun_apply [simp]: "K_statefun c x = c"
  by (simp add: K_statefun_def)

lemma K_statefun_comp [simp]: "(K_statefun c ∘ f) = K_statefun c"
  by (rule ext) (simp add: comp_def)

lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
  by (rule refl)

definition lookup :: "('v ==> 'a) ==> 'n ==> ('n ==> 'v) ==> 'a"
  where "lookup destr n s = destr (s n)"

definition update ::
  "('v ==> 'a1) ==> ('a2 ==> 'v) ==> 'n ==> ('a1 ==> 'a2) ==> ('n ==> 'v) ==> ('n ==> 'v)"
  where "update destr constr n f s = s(n := constr (f (destr (s n))))"

lemma lookup_update_same:
  "(∧v. destr (constr v) = v) ==> lookup destr n (update destr constr n f s) =
         f (destr (s n))"  
  by (simp add: lookup_def update_def)

lemma lookup_update_id_same:
  "lookup destr n (update destr' id n (K_statefun (lookup id n s')) s) =
     lookup destr n s'"  
  by (simp add: lookup_def update_def)

lemma lookup_update_other:
  "n≠m ==> lookup destr n (update destr' constr m f s) = lookup destr n s"  
  by (simp add: lookup_def update_def)


lemma id_id_cancel: "id (id x) = x" 
  by (simp add: id_def)
  
lemma destr_contstr_comp_id: "(∧v. destr (constr v) = v) ==> destr ∘ constr = id"
  by (rule ext) simp



lemma block_conj_cong: "(P ∧ Q) = (P ∧ Q)"
  by simp

lemma conj1_False: "P ≡ False ==> (P ∧ Q) ≡ False"
  by simp

lemma conj2_False: "Q ≡ False ==> (P ∧ Q) ≡ False"
  by simp

lemma conj_True: "P ≡ True ==> Q ≡ True ==> (P ∧ Q) ≡ True"
  by simp

lemma conj_cong: "P ≡ P' ==> Q ≡ Q' ==> (P ∧ Q) ≡ (P' ∧ Q')"
  by simp


lemma update_apply: "(update destr constr n f s x) =
     (if x=n then constr (f (destr (s n))) else s x)"
  by (simp add: update_def)

lemma ex_id: "∃x. id x = y"
  by (simp add: id_def)

lemma swap_ex_eq: 
  "∃s. f s = x ≡ True ==>
   ∃s. x = f s ≡ True"
  apply (rule eq_reflection)
  apply auto
  done

lemmas meta_ext = eq_reflection [OF ext]

(* This lemma only works if the store is welltyped:
    "\<exists>x.  s ''n'' = (c x)" 
   or in general when c (d x) = x,
     (for example: c=id and d=id)
 *)
lemma "update d c n (K_statespace (lookup d n s)) s = s"
  apply (simp add: update_def lookup_def)
  apply (rule ext)
  apply simp
  oops

end