src/HOL/Statespace/StateFun.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 63167 0909deb8059b
permissions -rw-r--r--
more fundamental definition of div and mod on int
     1 (*  Title:      HOL/Statespace/StateFun.thy
     2     Author:     Norbert Schirmer, TU Muenchen
     3 *)
     4 
     5 section \<open>State Space Representation as Function \label{sec:StateFun}\<close>
     6 
     7 theory StateFun imports DistinctTreeProver 
     8 begin
     9 
    10 
    11 text \<open>The state space is represented as a function from names to
    12 values. We neither fix the type of names nor the type of values. We
    13 define lookup and update functions and provide simprocs that simplify
    14 expressions containing these, similar to HOL-records.
    15 
    16 The lookup and update function get constructor/destructor functions as
    17 parameters. These are used to embed various HOL-types into the
    18 abstract value type. Conceptually the abstract value type is a sum of
    19 all types that we attempt to store in the state space.
    20 
    21 The update is actually generalized to a map function. The map supplies
    22 better compositionality, especially if you think of nested state
    23 spaces.\<close> 
    24 
    25 definition K_statefun :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where "K_statefun c x \<equiv> c"
    26 
    27 lemma K_statefun_apply [simp]: "K_statefun c x = c"
    28   by (simp add: K_statefun_def)
    29 
    30 lemma K_statefun_comp [simp]: "(K_statefun c \<circ> f) = K_statefun c"
    31   by (rule ext) (simp add: comp_def)
    32 
    33 lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
    34   by (rule refl)
    35 
    36 definition lookup :: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
    37   where "lookup destr n s = destr (s n)"
    38 
    39 definition 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 
    43 lemma 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 
    48 lemma 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 
    53 lemma 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 
    58 lemma id_id_cancel: "id (id x) = x" 
    59   by (simp add: id_def)
    60   
    61 lemma destr_contstr_comp_id: "(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id"
    62   by (rule ext) simp
    63 
    64 
    65 
    66 lemma block_conj_cong: "(P \<and> Q) = (P \<and> Q)"
    67   by simp
    68 
    69 lemma conj1_False: "P \<equiv> False \<Longrightarrow> (P \<and> Q) \<equiv> False"
    70   by simp
    71 
    72 lemma conj2_False: "Q \<equiv> False \<Longrightarrow> (P \<and> Q) \<equiv> False"
    73   by simp
    74 
    75 lemma conj_True: "P \<equiv> True \<Longrightarrow> Q \<equiv> True \<Longrightarrow> (P \<and> Q) \<equiv> True"
    76   by simp
    77 
    78 lemma conj_cong: "P \<equiv> P' \<Longrightarrow> Q \<equiv> Q' \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> Q')"
    79   by simp
    80 
    81 
    82 lemma 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 
    86 lemma ex_id: "\<exists>x. id x = y"
    87   by (simp add: id_def)
    88 
    89 lemma 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 
    96 lemmas 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  *)
   103 lemma "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 
   109 end