src/HOL/Statespace/StateFun.thy
 author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51474 1e9e68247ad1 parent 45358 4849133d7a78 child 58889 5b7a9633cfa8 permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
     1 (*  Title:      HOL/Statespace/StateFun.thy

     2     Author:     Norbert Schirmer, TU Muenchen

     3 *)

     4

     5 header {* State Space Representation as Function \label{sec:StateFun}*}

     6

     7 theory StateFun imports DistinctTreeProver

     8 begin

     9

    10

    11 text {* 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.  *}

    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