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