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