src/HOL/MicroJava/J/State.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 44042 2ff2a54d0fb5
child 47394 a360406f1fcb
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/MicroJava/J/State.thy
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     2
    Author:     David von Oheimb
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     3
    Copyright   1999 Technische Universitaet Muenchen
11070
cc421547e744 improved document (added headers etc)
oheimb
parents: 11026
diff changeset
     4
*)
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     5
12911
704713ca07ea new document
kleing
parents: 12545
diff changeset
     6
header {* \isaheader{Program State} *}
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     7
32356
e11cd88e6ade temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents: 30235
diff changeset
     8
theory State
e11cd88e6ade temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents: 30235
diff changeset
     9
imports TypeRel Value
e11cd88e6ade temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents: 30235
diff changeset
    10
begin
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    11
42463
f270e3e18be5 modernized specifications;
wenzelm
parents: 35416
diff changeset
    12
type_synonym 
24783
5a3e336a2e37 avoid internal names;
wenzelm
parents: 16417
diff changeset
    13
  fields' = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    14
42463
f270e3e18be5 modernized specifications;
wenzelm
parents: 35416
diff changeset
    15
type_synonym
24783
5a3e336a2e37 avoid internal names;
wenzelm
parents: 16417
diff changeset
    16
  obj = "cname \<times> fields'"    -- "class instance with class name and fields"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    17
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35102
diff changeset
    18
definition obj_ty :: "obj => ty" where
10042
7164dc0d24d8 unsymbolized
kleing
parents: 9348
diff changeset
    19
 "obj_ty obj  == Class (fst obj)"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    20
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35102
diff changeset
    21
definition init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" where
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11372
diff changeset
    22
 "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
32356
e11cd88e6ade temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents: 30235
diff changeset
    23
42463
f270e3e18be5 modernized specifications;
wenzelm
parents: 35416
diff changeset
    24
type_synonym aheap = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
f270e3e18be5 modernized specifications;
wenzelm
parents: 35416
diff changeset
    25
type_synonym locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    26
42463
f270e3e18be5 modernized specifications;
wenzelm
parents: 35416
diff changeset
    27
type_synonym state = "aheap \<times> locals"      -- "heap, local parameter including This"
f270e3e18be5 modernized specifications;
wenzelm
parents: 35416
diff changeset
    28
type_synonym xstate = "val option \<times> state" -- "state including exception information"
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11372
diff changeset
    29
35102
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    30
abbreviation (input)
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    31
  heap :: "state => aheap"
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    32
  where "heap == fst"
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    33
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    34
abbreviation (input)
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    35
  locals :: "state => locals"
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    36
  where "locals == snd"
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    37
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    38
abbreviation "Norm s == (None, s)"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    39
35102
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    40
abbreviation (input)
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    41
  abrupt :: "xstate \<Rightarrow> val option"
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    42
  where "abrupt == fst"
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    43
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    44
abbreviation (input)
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    45
  store :: "xstate \<Rightarrow> state"
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    46
  where "store == snd"
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    47
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    48
abbreviation
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    49
  lookup_obj :: "state \<Rightarrow> val \<Rightarrow> obj"
cc7a0b9f938c modernized translations;
wenzelm
parents: 32359
diff changeset
    50
  where "lookup_obj s a' == the (heap s (the_Addr a'))"
13672
b95d12325b51 Added compiler
streckem
parents: 12911
diff changeset
    51
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35102
diff changeset
    52
definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where
13672
b95d12325b51 Added compiler
streckem
parents: 12911
diff changeset
    53
  "raise_if b x xo \<equiv> if b \<and>  (xo = None) then Some (Addr (XcptRef x)) else xo"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    54
44042
2ff2a54d0fb5 fixed document;
wenzelm
parents: 44035
diff changeset
    55
text {* Make @{text new_Addr} completely specified (at least for the code generator) *}
44035
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
    56
(*
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35102
diff changeset
    57
definition new_Addr  :: "aheap => loc \<times> val option" where
13672
b95d12325b51 Added compiler
streckem
parents: 12911
diff changeset
    58
  "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"
44035
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
    59
*)
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
    60
consts nat_to_loc' :: "nat => loc'"
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
    61
code_datatype nat_to_loc'
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
    62
definition new_Addr  :: "aheap => loc \<times> val option" where
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
    63
  "new_Addr h \<equiv> 
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
    64
   if \<exists>n. h (Loc (nat_to_loc' n)) = None 
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
    65
   then (Loc (nat_to_loc' (LEAST n. h (Loc (nat_to_loc' n)) = None)), None)
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
    66
   else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    67
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35102
diff changeset
    68
definition np    :: "val => val option => val option" where
10042
7164dc0d24d8 unsymbolized
kleing
parents: 9348
diff changeset
    69
 "np v == raise_if (v = Null) NullPointer"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    70
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35102
diff changeset
    71
definition c_hupd  :: "aheap => xstate => xstate" where
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    72
 "c_hupd h'== \<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    73
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35102
diff changeset
    74
definition cast_ok :: "'c prog => cname => aheap => val => bool" where
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    75
 "cast_ok G C h v == v = Null \<or> G\<turnstile>obj_ty (the (h (the_Addr v)))\<preceq> Class C"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    76
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    77
lemma obj_ty_def2 [simp]: "obj_ty (C,fs) = Class C"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    78
apply (unfold obj_ty_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    79
apply (simp (no_asm))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    80
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    81
13672
b95d12325b51 Added compiler
streckem
parents: 12911
diff changeset
    82
b95d12325b51 Added compiler
streckem
parents: 12911
diff changeset
    83
lemma new_AddrD: "new_Addr hp = (ref, xcp) \<Longrightarrow>
b95d12325b51 Added compiler
streckem
parents: 12911
diff changeset
    84
  hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
b95d12325b51 Added compiler
streckem
parents: 12911
diff changeset
    85
apply (drule sym)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    86
apply (unfold new_Addr_def)
44035
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
    87
apply (simp split: split_if_asm)
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
    88
apply (erule LeastI)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    89
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    90
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    91
lemma raise_if_True [simp]: "raise_if True x y \<noteq> None"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    92
apply (unfold raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    93
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    94
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    95
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    96
lemma raise_if_False [simp]: "raise_if False x y = y"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    97
apply (unfold raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    98
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
    99
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   100
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   101
lemma raise_if_Some [simp]: "raise_if c x (Some y) \<noteq> None"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   102
apply (unfold raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   103
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   104
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   105
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11372
diff changeset
   106
lemma raise_if_Some2 [simp]: 
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11372
diff changeset
   107
  "raise_if c z (if x = None then Some y else x) \<noteq> None"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   108
apply (unfold raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   109
apply(induct_tac "x")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   110
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   111
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   112
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   113
lemma raise_if_SomeD [rule_format (no_asm)]: 
13672
b95d12325b51 Added compiler
streckem
parents: 12911
diff changeset
   114
  "raise_if c x y = Some z \<longrightarrow> c \<and>  Some z = Some (Addr (XcptRef x)) |  y = Some z"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   115
apply (unfold raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   116
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   117
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   118
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11372
diff changeset
   119
lemma raise_if_NoneD [rule_format (no_asm)]: 
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11372
diff changeset
   120
  "raise_if c x y = None --> \<not> c \<and>  y = None"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   121
apply (unfold raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   122
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   123
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   124
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11372
diff changeset
   125
lemma np_NoneD [rule_format (no_asm)]: 
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11372
diff changeset
   126
  "np a' x' = None --> x' = None \<and>  a' \<noteq> Null"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   127
apply (unfold np_def raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   128
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   129
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   130
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   131
lemma np_None [rule_format (no_asm), simp]: "a' \<noteq> Null --> np a' x' = x'"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   132
apply (unfold np_def raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   133
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   134
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   135
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   136
lemma np_Some [simp]: "np a' (Some xc) = Some xc"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   137
apply (unfold np_def raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   138
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   139
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   140
13672
b95d12325b51 Added compiler
streckem
parents: 12911
diff changeset
   141
lemma np_Null [simp]: "np Null None = Some (Addr (XcptRef NullPointer))"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   142
apply (unfold np_def raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   143
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   144
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   145
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   146
lemma np_Addr [simp]: "np (Addr a) None = None"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   147
apply (unfold np_def raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   148
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   149
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   150
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   151
lemma np_raise_if [simp]: "(np Null (raise_if c xc None)) =  
13672
b95d12325b51 Added compiler
streckem
parents: 12911
diff changeset
   152
  Some (Addr (XcptRef (if c then  xc else NullPointer)))"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   153
apply (unfold raise_if_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   154
apply (simp (no_asm))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 10061
diff changeset
   155
done
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
   156
14144
7195c9b0423f added lemma c_hupd_fst
streckem
parents: 14134
diff changeset
   157
lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x"
7195c9b0423f added lemma c_hupd_fst
streckem
parents: 14134
diff changeset
   158
by (simp add: c_hupd_def split_beta)
7195c9b0423f added lemma c_hupd_fst
streckem
parents: 14134
diff changeset
   159
44035
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   160
text {* Naive implementation for @{term "new_Addr"} by exhaustive search *}
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   161
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   162
definition gen_new_Addr :: "aheap => nat \<Rightarrow> loc \<times> val option" where
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   163
  "gen_new_Addr h n \<equiv> 
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   164
   if \<exists>a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None 
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   165
   then (Loc (nat_to_loc' (LEAST a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None)), None)
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   166
   else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))"
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   167
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   168
lemma new_Addr_code_code [code]:
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   169
  "new_Addr h = gen_new_Addr h 0"
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   170
by(simp only: new_Addr_def gen_new_Addr_def split: split_if) simp
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   171
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   172
lemma gen_new_Addr_code [code]:
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   173
  "gen_new_Addr h n = (if h (Loc (nat_to_loc' n)) = None then (Loc (nat_to_loc' n), None) else gen_new_Addr h (Suc n))"
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   174
apply(simp add: gen_new_Addr_def)
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   175
apply(rule impI)
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   176
apply(rule conjI)
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   177
 apply safe[1]
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   178
  apply(auto intro: arg_cong[where f=nat_to_loc'] Least_equality)[1]
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   179
 apply(rule arg_cong[where f=nat_to_loc'])
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   180
 apply(rule arg_cong[where f=Least])
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   181
 apply(rule ext)
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   182
 apply(safe, simp_all)[1]
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   183
 apply(rename_tac "n'")
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   184
 apply(case_tac "n = n'", simp_all)[1]
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   185
apply clarify
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   186
apply(subgoal_tac "a = n")
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   187
 apply(auto intro: Least_equality arg_cong[where f=nat_to_loc'])[1]
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   188
apply(rule ccontr)
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   189
apply(erule_tac x="a" in allE)
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   190
apply simp
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   191
done
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   192
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   193
instantiation loc' :: equal begin
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   194
definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'"
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   195
instance proof qed(simp add: equal_loc'_def)
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
   196
end
44035
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   197
322d1657c40c replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents: 42463
diff changeset
   198
end