src/HOL/MicroJava/J/State.thy
author ballarin
Fri Aug 29 15:19:02 2003 +0200 (2003-08-29)
changeset 14174 f3cafd2929d5
parent 14144 7195c9b0423f
child 16417 9bc16273c2d4
permissions -rw-r--r--
Methods rule_tac etc support static (Isar) contexts.
nipkow@8011
     1
(*  Title:      HOL/MicroJava/J/State.thy
nipkow@8011
     2
    ID:         $Id$
nipkow@8011
     3
    Author:     David von Oheimb
nipkow@8011
     4
    Copyright   1999 Technische Universitaet Muenchen
oheimb@11070
     5
*)
nipkow@8011
     6
kleing@12911
     7
header {* \isaheader{Program State} *}
nipkow@8011
     8
oheimb@11026
     9
theory State = TypeRel + Value:
nipkow@8011
    10
kleing@12517
    11
types 
nipkow@14134
    12
  fields_ = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
nipkow@8011
    13
kleing@12517
    14
  obj = "cname \<times> fields_"    -- "class instance with class name and fields"
nipkow@8011
    15
nipkow@8011
    16
constdefs
kleing@12517
    17
  obj_ty  :: "obj => ty"
kleing@10042
    18
 "obj_ty obj  == Class (fst obj)"
nipkow@8011
    19
nipkow@14134
    20
  init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)"
kleing@12517
    21
 "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
nipkow@8011
    22
  
kleing@12517
    23
nipkow@14134
    24
types aheap  = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
nipkow@14134
    25
      locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
nipkow@8011
    26
kleing@12517
    27
      state  = "aheap \<times> locals"      -- "heap, local parameter including This"
streckem@13672
    28
      xstate = "val option \<times> state" -- "state including exception information"
kleing@12517
    29
nipkow@8011
    30
syntax
kleing@12517
    31
  heap    :: "state => aheap"
kleing@12517
    32
  locals  :: "state => locals"
kleing@12517
    33
  Norm    :: "state => xstate"
streckem@13672
    34
  abrupt  :: "xstate \<Rightarrow> val option"
streckem@13672
    35
  store   :: "xstate \<Rightarrow> state"
streckem@13672
    36
  lookup_obj   :: "state \<Rightarrow> val \<Rightarrow> obj"
nipkow@8011
    37
nipkow@8011
    38
translations
kleing@10061
    39
  "heap"   => "fst"
kleing@10061
    40
  "locals" => "snd"
kleing@12517
    41
  "Norm s" == "(None,s)"
streckem@13672
    42
  "abrupt"     => "fst"
streckem@13672
    43
  "store"      => "snd"
streckem@13672
    44
 "lookup_obj s a'"  == "the (heap s (the_Addr a'))"
streckem@13672
    45
nipkow@8011
    46
nipkow@8011
    47
constdefs
streckem@13672
    48
  raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option"
streckem@13672
    49
  "raise_if b x xo \<equiv> if b \<and>  (xo = None) then Some (Addr (XcptRef x)) else xo"
nipkow@8011
    50
streckem@13672
    51
  new_Addr  :: "aheap => loc \<times> val option"
streckem@13672
    52
  "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"
nipkow@8011
    53
streckem@13672
    54
  np    :: "val => val option => val option"
kleing@10042
    55
 "np v == raise_if (v = Null) NullPointer"
nipkow@8011
    56
kleing@12517
    57
  c_hupd  :: "aheap => xstate => xstate"
oheimb@11026
    58
 "c_hupd h'== \<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
nipkow@8011
    59
kleing@12517
    60
  cast_ok :: "'c prog => cname => aheap => val => bool"
oheimb@11026
    61
 "cast_ok G C h v == v = Null \<or> G\<turnstile>obj_ty (the (h (the_Addr v)))\<preceq> Class C"
oheimb@11026
    62
oheimb@11026
    63
lemma obj_ty_def2 [simp]: "obj_ty (C,fs) = Class C"
oheimb@11026
    64
apply (unfold obj_ty_def)
oheimb@11026
    65
apply (simp (no_asm))
oheimb@11026
    66
done
oheimb@11026
    67
streckem@13672
    68
streckem@13672
    69
lemma new_AddrD: "new_Addr hp = (ref, xcp) \<Longrightarrow>
streckem@13672
    70
  hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
streckem@13672
    71
apply (drule sym)
oheimb@11026
    72
apply (unfold new_Addr_def)
oheimb@11026
    73
apply(simp add: Pair_fst_snd_eq Eps_split)
oheimb@11026
    74
apply(rule someI)
oheimb@11026
    75
apply(rule disjI2)
ballarin@14174
    76
apply(rule_tac r = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
oheimb@11026
    77
apply auto
oheimb@11026
    78
done
oheimb@11026
    79
oheimb@11026
    80
lemma raise_if_True [simp]: "raise_if True x y \<noteq> None"
oheimb@11026
    81
apply (unfold raise_if_def)
oheimb@11026
    82
apply auto
oheimb@11026
    83
done
oheimb@11026
    84
oheimb@11026
    85
lemma raise_if_False [simp]: "raise_if False x y = y"
oheimb@11026
    86
apply (unfold raise_if_def)
oheimb@11026
    87
apply auto
oheimb@11026
    88
done
oheimb@11026
    89
oheimb@11026
    90
lemma raise_if_Some [simp]: "raise_if c x (Some y) \<noteq> None"
oheimb@11026
    91
apply (unfold raise_if_def)
oheimb@11026
    92
apply auto
oheimb@11026
    93
done
oheimb@11026
    94
kleing@12517
    95
lemma raise_if_Some2 [simp]: 
kleing@12517
    96
  "raise_if c z (if x = None then Some y else x) \<noteq> None"
oheimb@11026
    97
apply (unfold raise_if_def)
oheimb@11026
    98
apply(induct_tac "x")
oheimb@11026
    99
apply auto
oheimb@11026
   100
done
oheimb@11026
   101
oheimb@11026
   102
lemma raise_if_SomeD [rule_format (no_asm)]: 
streckem@13672
   103
  "raise_if c x y = Some z \<longrightarrow> c \<and>  Some z = Some (Addr (XcptRef x)) |  y = Some z"
oheimb@11026
   104
apply (unfold raise_if_def)
oheimb@11026
   105
apply auto
oheimb@11026
   106
done
oheimb@11026
   107
kleing@12517
   108
lemma raise_if_NoneD [rule_format (no_asm)]: 
kleing@12517
   109
  "raise_if c x y = None --> \<not> c \<and>  y = None"
oheimb@11026
   110
apply (unfold raise_if_def)
oheimb@11026
   111
apply auto
oheimb@11026
   112
done
oheimb@11026
   113
kleing@12517
   114
lemma np_NoneD [rule_format (no_asm)]: 
kleing@12517
   115
  "np a' x' = None --> x' = None \<and>  a' \<noteq> Null"
oheimb@11026
   116
apply (unfold np_def raise_if_def)
oheimb@11026
   117
apply auto
oheimb@11026
   118
done
oheimb@11026
   119
oheimb@11026
   120
lemma np_None [rule_format (no_asm), simp]: "a' \<noteq> Null --> np a' x' = x'"
oheimb@11026
   121
apply (unfold np_def raise_if_def)
oheimb@11026
   122
apply auto
oheimb@11026
   123
done
oheimb@11026
   124
oheimb@11026
   125
lemma np_Some [simp]: "np a' (Some xc) = Some xc"
oheimb@11026
   126
apply (unfold np_def raise_if_def)
oheimb@11026
   127
apply auto
oheimb@11026
   128
done
oheimb@11026
   129
streckem@13672
   130
lemma np_Null [simp]: "np Null None = Some (Addr (XcptRef NullPointer))"
oheimb@11026
   131
apply (unfold np_def raise_if_def)
oheimb@11026
   132
apply auto
oheimb@11026
   133
done
oheimb@11026
   134
oheimb@11026
   135
lemma np_Addr [simp]: "np (Addr a) None = None"
oheimb@11026
   136
apply (unfold np_def raise_if_def)
oheimb@11026
   137
apply auto
oheimb@11026
   138
done
oheimb@11026
   139
oheimb@11026
   140
lemma np_raise_if [simp]: "(np Null (raise_if c xc None)) =  
streckem@13672
   141
  Some (Addr (XcptRef (if c then  xc else NullPointer)))"
oheimb@11026
   142
apply (unfold raise_if_def)
oheimb@11026
   143
apply (simp (no_asm))
oheimb@11026
   144
done
nipkow@8011
   145
streckem@14144
   146
lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x"
streckem@14144
   147
by (simp add: c_hupd_def split_beta)
streckem@14144
   148
nipkow@8011
   149
end