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