[STATEMENT]
lemma hconf_heap_clone_mono:
  assumes "heap_clone P h a h' res"
  and "hconf h"
  shows "hconf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
using \<open>heap_clone P h a h' res\<close>
[PROOF STATE]
proof (prove)
using this:
heap_clone P h a h' res

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>hT. \<lbrakk>h' = h; res = None; typeof_addr h a = \<lfloor>hT\<rfloor>; allocate h hT = {}\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 3. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
case CloneFail
[PROOF STATE]
proof (state)
this:
h' = h
res = None
typeof_addr h a = \<lfloor>hT_\<rfloor>
allocate h hT_ = {}

goal (3 subgoals):
 1. \<And>hT. \<lbrakk>h' = h; res = None; typeof_addr h a = \<lfloor>hT\<rfloor>; allocate h hT = {}\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 3. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
h' = h
res = None
typeof_addr h a = \<lfloor>hT_\<rfloor>
allocate h hT_ = {}

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
using \<open>hconf h\<close>
[PROOF STATE]
proof (prove)
using this:
h' = h
res = None
typeof_addr h a = \<lfloor>hT_\<rfloor>
allocate h hT_ = {}
hconf h

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
by(fastforce intro: hconf_heap_ops_mono dest: typeof_addr_is_type)
[PROOF STATE]
proof (state)
this:
hconf h'

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
case (ObjClone C h'' a' FDTs obs)
[PROOF STATE]
proof (state)
this:
res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>
typeof_addr h a = \<lfloor>Class_type C\<rfloor>
(h'', a') \<in> allocate h (Class_type C)
P \<turnstile> C has_fields FDTs
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'' obs h'

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
note FDTs = \<open>P \<turnstile> C has_fields FDTs\<close>
[PROOF STATE]
proof (state)
this:
P \<turnstile> C has_fields FDTs

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
let ?als = "map (\<lambda>((F, D), Tfm). CField D F) FDTs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
let ?Ts = "map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
note \<open>heap_copies a a' ?als h'' obs h'\<close>
[PROOF STATE]
proof (state)
this:
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'' obs h'

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'' obs h'

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
from \<open>typeof_addr h a = \<lfloor>Class_type C\<rfloor>\<close> \<open>hconf h\<close>
[PROOF STATE]
proof (chain)
picking this:
typeof_addr h a = \<lfloor>Class_type C\<rfloor>
hconf h
[PROOF STEP]
have "is_class P C"
[PROOF STATE]
proof (prove)
using this:
typeof_addr h a = \<lfloor>Class_type C\<rfloor>
hconf h

goal (1 subgoal):
 1. is_class P C
[PROOF STEP]
by(auto dest: typeof_addr_is_type)
[PROOF STATE]
proof (state)
this:
is_class P C

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
from \<open>(h'', a') \<in> allocate h (Class_type C)\<close>
[PROOF STATE]
proof (chain)
picking this:
(h'', a') \<in> allocate h (Class_type C)
[PROOF STEP]
have "h \<unlhd> h''" "hconf h''"
[PROOF STATE]
proof (prove)
using this:
(h'', a') \<in> allocate h (Class_type C)

goal (1 subgoal):
 1. h \<unlhd> h'' &&& hconf h''
[PROOF STEP]
by(rule hext_heap_ops hconf_allocate_mono)+(simp_all add: \<open>hconf h\<close> \<open>is_class P C\<close>)
[PROOF STATE]
proof (state)
this:
h \<unlhd> h''
hconf h''

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
note \<open>hconf h''\<close>
[PROOF STATE]
proof (state)
this:
hconf h''

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hconf h''

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
from \<open>typeof_addr h a = \<lfloor>Class_type C\<rfloor>\<close> FDTs
[PROOF STATE]
proof (chain)
picking this:
typeof_addr h a = \<lfloor>Class_type C\<rfloor>
P \<turnstile> C has_fields FDTs
[PROOF STEP]
have "list_all2 (\<lambda>al T. P,h \<turnstile> a@al : T) ?als ?Ts"
[PROOF STATE]
proof (prove)
using this:
typeof_addr h a = \<lfloor>Class_type C\<rfloor>
P \<turnstile> C has_fields FDTs

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
[PROOF STEP]
unfolding list_all2_map1 list_all2_map2 list_all2_same
[PROOF STATE]
proof (prove)
using this:
typeof_addr h a = \<lfloor>Class_type C\<rfloor>
P \<turnstile> C has_fields FDTs

goal (1 subgoal):
 1. \<forall>x\<in>set FDTs. P,h \<turnstile> a@(case x of (x, xa) \<Rightarrow> (case x of (F, D) \<Rightarrow> \<lambda>Tfm. CField D F) xa) : (case x of (FD, T) \<Rightarrow> fst (the (map_of FDTs FD)))
[PROOF STEP]
by(fastforce intro: addr_loc_type.intros simp add: has_field_def dest: weak_map_of_SomeI)
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
hence "list_all2 (\<lambda>al T. P,h'' \<turnstile> a@al : T) ?als ?Ts"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h'' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
[PROOF STEP]
by(rule list_all2_mono)(rule addr_loc_type_hext_mono[OF _ \<open>h \<unlhd> h''\<close>])
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h'' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h'' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
from \<open>(h'', a') \<in> allocate h (Class_type C)\<close> \<open>is_class P C\<close>
[PROOF STATE]
proof (chain)
picking this:
(h'', a') \<in> allocate h (Class_type C)
is_class P C
[PROOF STEP]
have "typeof_addr h'' a' = \<lfloor>Class_type C\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
(h'', a') \<in> allocate h (Class_type C)
is_class P C

goal (1 subgoal):
 1. typeof_addr h'' a' = \<lfloor>Class_type C\<rfloor>
[PROOF STEP]
by(auto dest: allocate_SomeD)
[PROOF STATE]
proof (state)
this:
typeof_addr h'' a' = \<lfloor>Class_type C\<rfloor>

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
with FDTs
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C has_fields FDTs
typeof_addr h'' a' = \<lfloor>Class_type C\<rfloor>
[PROOF STEP]
have "list_all2 (\<lambda>al T. P,h'' \<turnstile> a'@al : T) ?als ?Ts"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C has_fields FDTs
typeof_addr h'' a' = \<lfloor>Class_type C\<rfloor>

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h'' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
[PROOF STEP]
unfolding list_all2_map1 list_all2_map2 list_all2_same
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C has_fields FDTs
typeof_addr h'' a' = \<lfloor>Class_type C\<rfloor>

goal (1 subgoal):
 1. \<forall>x\<in>set FDTs. P,h'' \<turnstile> a'@(case x of (x, xa) \<Rightarrow> (case x of (F, D) \<Rightarrow> \<lambda>Tfm. CField D F) xa) : (case x of (FD, T) \<Rightarrow> fst (the (map_of FDTs FD)))
[PROOF STEP]
by(fastforce intro: addr_loc_type.intros simp add: has_field_def dest: weak_map_of_SomeI)
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h'' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'' obs h'
hconf h''
list_all2 (addr_loc_type P h'' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
list_all2 (addr_loc_type P h'' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
[PROOF STEP]
have "hconf h'"
[PROOF STATE]
proof (prove)
using this:
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'' obs h'
hconf h''
list_all2 (addr_loc_type P h'' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
list_all2 (addr_loc_type P h'' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
by(rule hconf_heap_copies_mono)
[PROOF STATE]
proof (state)
this:
hconf h'

goal (2 subgoals):
 1. \<And>C h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h'a, a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
 2. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
hconf h'

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
using ObjClone
[PROOF STATE]
proof (prove)
using this:
hconf h'
res = \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>
typeof_addr h a = \<lfloor>Class_type C\<rfloor>
(h'', a') \<in> allocate h (Class_type C)
P \<turnstile> C has_fields FDTs
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h'' obs h'

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hconf h'

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
case (ArrClone T n h'' a' FDTs obs)
[PROOF STATE]
proof (state)
this:
res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>
typeof_addr h a = \<lfloor>Array_type T n\<rfloor>
(h'', a') \<in> allocate h (Array_type T n)
P \<turnstile> Object has_fields FDTs
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'' obs h'

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
let ?als = "map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
let ?Ts = "map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
note \<open>heap_copies a a' ?als h'' obs h'\<close>
[PROOF STATE]
proof (state)
this:
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'' obs h'

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'' obs h'

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
from \<open>typeof_addr h a = \<lfloor>Array_type T n\<rfloor>\<close> \<open>hconf h\<close>
[PROOF STATE]
proof (chain)
picking this:
typeof_addr h a = \<lfloor>Array_type T n\<rfloor>
hconf h
[PROOF STEP]
have "is_type P (T\<lfloor>\<rceil>)"
[PROOF STATE]
proof (prove)
using this:
typeof_addr h a = \<lfloor>Array_type T n\<rfloor>
hconf h

goal (1 subgoal):
 1. is_type P (T\<lfloor>\<rceil>)
[PROOF STEP]
by(auto dest: typeof_addr_is_type)
[PROOF STATE]
proof (state)
this:
is_type P (T\<lfloor>\<rceil>)

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
from \<open>(h'', a') \<in> allocate h (Array_type T n)\<close>
[PROOF STATE]
proof (chain)
picking this:
(h'', a') \<in> allocate h (Array_type T n)
[PROOF STEP]
have "h \<unlhd> h''" "hconf h''"
[PROOF STATE]
proof (prove)
using this:
(h'', a') \<in> allocate h (Array_type T n)

goal (1 subgoal):
 1. h \<unlhd> h'' &&& hconf h''
[PROOF STEP]
by(rule hext_heap_ops hconf_allocate_mono)+(simp_all add: \<open>hconf h\<close> \<open>is_type P (T\<lfloor>\<rceil>)\<close>[simplified])
[PROOF STATE]
proof (state)
this:
h \<unlhd> h''
hconf h''

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
note \<open>hconf h''\<close>
[PROOF STATE]
proof (state)
this:
hconf h''

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hconf h''

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
from \<open>h \<unlhd> h''\<close> \<open>typeof_addr h a = \<lfloor>Array_type T n\<rfloor>\<close>
[PROOF STATE]
proof (chain)
picking this:
h \<unlhd> h''
typeof_addr h a = \<lfloor>Array_type T n\<rfloor>
[PROOF STEP]
have type'a: "typeof_addr h'' a = \<lfloor>Array_type T n\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
h \<unlhd> h''
typeof_addr h a = \<lfloor>Array_type T n\<rfloor>

goal (1 subgoal):
 1. typeof_addr h'' a = \<lfloor>Array_type T n\<rfloor>
[PROOF STEP]
by(auto intro: hext_arrD)
[PROOF STATE]
proof (state)
this:
typeof_addr h'' a = \<lfloor>Array_type T n\<rfloor>

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
note FDTs = \<open>P \<turnstile> Object has_fields FDTs\<close>
[PROOF STATE]
proof (state)
this:
P \<turnstile> Object has_fields FDTs

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
from type'a FDTs
[PROOF STATE]
proof (chain)
picking this:
typeof_addr h'' a = \<lfloor>Array_type T n\<rfloor>
P \<turnstile> Object has_fields FDTs
[PROOF STEP]
have "list_all2 (\<lambda>al T. P,h'' \<turnstile> a@al : T) ?als ?Ts"
[PROOF STATE]
proof (prove)
using this:
typeof_addr h'' a = \<lfloor>Array_type T n\<rfloor>
P \<turnstile> Object has_fields FDTs

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h'' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
[PROOF STEP]
by(fastforce intro: list_all2_all_nthI addr_loc_type.intros simp add: has_field_def distinct_fst_def list_all2_append list_all2_map1 list_all2_map2 list_all2_same dest: weak_map_of_SomeI)
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h'' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h'' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
from \<open>(h'', a') \<in> allocate h (Array_type T n)\<close> \<open>is_type P (T\<lfloor>\<rceil>)\<close>
[PROOF STATE]
proof (chain)
picking this:
(h'', a') \<in> allocate h (Array_type T n)
is_type P (T\<lfloor>\<rceil>)
[PROOF STEP]
have "typeof_addr h'' a' = \<lfloor>Array_type T n\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
(h'', a') \<in> allocate h (Array_type T n)
is_type P (T\<lfloor>\<rceil>)

goal (1 subgoal):
 1. typeof_addr h'' a' = \<lfloor>Array_type T n\<rfloor>
[PROOF STEP]
by(auto dest: allocate_SomeD)
[PROOF STATE]
proof (state)
this:
typeof_addr h'' a' = \<lfloor>Array_type T n\<rfloor>

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
hence "list_all2 (\<lambda>al T. P,h'' \<turnstile> a'@al : T) ?als ?Ts"
[PROOF STATE]
proof (prove)
using this:
typeof_addr h'' a' = \<lfloor>Array_type T n\<rfloor>

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h'' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
[PROOF STEP]
using FDTs
[PROOF STATE]
proof (prove)
using this:
typeof_addr h'' a' = \<lfloor>Array_type T n\<rfloor>
P \<turnstile> Object has_fields FDTs

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h'' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
[PROOF STEP]
by(fastforce intro: list_all2_all_nthI addr_loc_type.intros simp add: has_field_def distinct_fst_def list_all2_append list_all2_map1 list_all2_map2 list_all2_same dest: weak_map_of_SomeI)
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h'' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'' obs h'
hconf h''
list_all2 (addr_loc_type P h'' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
list_all2 (addr_loc_type P h'' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
[PROOF STEP]
have "hconf h'"
[PROOF STATE]
proof (prove)
using this:
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'' obs h'
hconf h''
list_all2 (addr_loc_type P h'' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
list_all2 (addr_loc_type P h'' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
by(rule hconf_heap_copies_mono)
[PROOF STATE]
proof (state)
this:
hconf h'

goal (1 subgoal):
 1. \<And>T n h'a a' FDTs obs. \<lbrakk>res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>; typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h'a, a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'a obs h'\<rbrakk> \<Longrightarrow> hconf h'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
hconf h'

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
using ArrClone
[PROOF STATE]
proof (prove)
using this:
hconf h'
res = \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>
typeof_addr h a = \<lfloor>Array_type T n\<rfloor>
(h'', a') \<in> allocate h (Array_type T n)
P \<turnstile> Object has_fields FDTs
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h'' obs h'

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hconf h'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem external_call_hconf:
  assumes major: "P,t \<turnstile> \<langle>a\<bullet>M(vs), h\<rangle> -ta\<rightarrow>ext \<langle>va, h'\<rangle>"
  and minor: "P,h \<turnstile> a\<bullet>M(vs) : U" "hconf h"
  shows "hconf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
using major minor
[PROOF STATE]
proof (prove)
using this:
P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
P,h \<turnstile> a\<bullet>M(vs) : U
hconf h

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
by cases(fastforce intro: hconf_heap_clone_mono)+


[STATEMENT]
lemma red_external_conf_extRet:
  assumes wf: "wf_prog wf_md P"
  shows "\<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs), h\<rangle> -ta\<rightarrow>ext \<langle>va, h'\<rangle>; P,h \<turnstile> a\<bullet>M(vs) : U; hconf h; preallocated h; P,h \<turnstile> t \<surd>t \<rbrakk>
  \<Longrightarrow> conf_extRet P h' va U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>; P,h \<turnstile> a\<bullet>M(vs) : U; hconf h; preallocated h; P,h \<turnstile> t \<surd>t\<rbrakk> \<Longrightarrow> conf_extRet P h' va U
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P

goal (1 subgoal):
 1. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>; P,h \<turnstile> a\<bullet>M(vs) : U; hconf h; preallocated h; P,h \<turnstile> t \<surd>t\<rbrakk> \<Longrightarrow> conf_extRet P h' va U
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>; P,h \<turnstile> a\<bullet>M(vs) : U; hconf h; preallocated h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P\<rbrakk> \<Longrightarrow> conf_extRet P h' va U
[PROOF STEP]
apply(frule red_external_hext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>; P,h \<turnstile> a\<bullet>M(vs) : U; hconf h; preallocated h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; h \<unlhd> h'\<rbrakk> \<Longrightarrow> conf_extRet P h' va U
[PROOF STEP]
apply(drule (1) preallocated_hext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>; P,h \<turnstile> a\<bullet>M(vs) : U; hconf h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; h \<unlhd> h'; preallocated h'\<rbrakk> \<Longrightarrow> conf_extRet P h' va U
[PROOF STEP]
apply(auto elim!: red_external.cases external_WT'.cases external_WT_defs_cases dest!: sees_wf_native[OF wf])
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>C. \<lbrakk>hconf h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; preallocated h; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = start; U = Void\<rbrakk> \<Longrightarrow> P,h \<turnstile> Addr (addr_of_sys_xcpt IllegalThreadState) :\<le> Class Throwable
 2. \<And>C. \<lbrakk>hconf h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; preallocated h; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = join; U = Void\<rbrakk> \<Longrightarrow> P,h \<turnstile> Addr (addr_of_sys_xcpt InterruptedException) :\<le> Class Throwable
 3. \<And>hT. \<lbrakk>hconf h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; preallocated h; typeof_addr h a = \<lfloor>hT\<rfloor>; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; M = wait; U = Void\<rbrakk> \<Longrightarrow> P,h \<turnstile> Addr (addr_of_sys_xcpt InterruptedException) :\<le> Class Throwable
 4. \<And>hT. \<lbrakk>hconf h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; preallocated h; typeof_addr h a = \<lfloor>hT\<rfloor>; vs = []; ta = \<lbrace>(UnlockFail, a)\<rbrace>; va = RetEXC IllegalMonitorState; h' = h; M = wait; U = Void\<rbrakk> \<Longrightarrow> P,h \<turnstile> Addr (addr_of_sys_xcpt IllegalMonitorState) :\<le> Class Throwable
 5. \<And>hT. \<lbrakk>hconf h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; preallocated h; typeof_addr h a = \<lfloor>hT\<rfloor>; vs = []; ta = \<lbrace>WokenUp, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; M = wait; U = Void\<rbrakk> \<Longrightarrow> P,h \<turnstile> Addr (addr_of_sys_xcpt InterruptedException) :\<le> Class Throwable
 6. \<And>hT. \<lbrakk>hconf h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; preallocated h; typeof_addr h a = \<lfloor>hT\<rfloor>; vs = []; ta = \<lbrace>(UnlockFail, a)\<rbrace>; va = RetEXC IllegalMonitorState; h' = h; M = notify; U = Void\<rbrakk> \<Longrightarrow> P,h \<turnstile> Addr (addr_of_sys_xcpt IllegalMonitorState) :\<le> Class Throwable
 7. \<And>hT. \<lbrakk>hconf h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; preallocated h; typeof_addr h a = \<lfloor>hT\<rfloor>; vs = []; ta = \<lbrace>(UnlockFail, a)\<rbrace>; va = RetEXC IllegalMonitorState; h' = h; M = notifyAll; U = Void\<rbrakk> \<Longrightarrow> P,h \<turnstile> Addr (addr_of_sys_xcpt IllegalMonitorState) :\<le> Class Throwable
 8. \<And>hT obs a'. \<lbrakk>hconf h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; h \<unlhd> h'; preallocated h'; typeof_addr h a = \<lfloor>hT\<rfloor>; vs = []; ta = (K$ [], [], [], [], [], obs); va = RetVal (Addr a'); heap_clone P h a h' \<lfloor>(obs, a')\<rfloor>; M = clone; U = Class Object\<rbrakk> \<Longrightarrow> P,h' \<turnstile> Addr a' :\<le> Class Object
 9. \<And>hT. \<lbrakk>hconf h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; h \<unlhd> h'; preallocated h'; typeof_addr h a = \<lfloor>hT\<rfloor>; vs = []; ta = \<lbrace>\<rbrace>; va = RetEXC OutOfMemory; heap_clone P h a h' None; M = clone; U = Class Object\<rbrakk> \<Longrightarrow> P,h' \<turnstile> Addr (addr_of_sys_xcpt OutOfMemory) :\<le> Class Throwable
 10. \<And>hT. \<lbrakk>hconf h; P,h \<turnstile> t \<surd>t; wf_prog wf_md P; preallocated h; typeof_addr h a = \<lfloor>hT\<rfloor>; vs = []; ta = \<lbrace>\<rbrace>; va = RetVal (Addr (thread_id2addr t)); h' = h; M = currentThread; U = Class Thread\<rbrakk> \<Longrightarrow> P,h \<turnstile> Addr (thread_id2addr t) :\<le> Class Thread
[PROOF STEP]
apply(auto simp add: conf_def tconf_def intro: xcpt_subcls_Throwable dest!: hext_heap_write)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>hT obs a' C. \<lbrakk>hconf h; wf_prog wf_md P; h \<unlhd> h'; preallocated h'; typeof_addr h a = \<lfloor>hT\<rfloor>; vs = []; ta = (K$ [], [], [], [], [], obs); va = RetVal (Addr a'); heap_clone P h a h' \<lfloor>(obs, a')\<rfloor>; M = clone; U = Class Object; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>T'. (\<exists>z. typeof_addr h' a' = \<lfloor>z\<rfloor> \<and> ty_of_htype z = T') \<and> P \<turnstile> T' \<le> Class Object
[PROOF STEP]
apply(case_tac hT)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>hT obs a' C x1. \<lbrakk>hconf h; wf_prog wf_md P; h \<unlhd> h'; preallocated h'; typeof_addr h a = \<lfloor>hT\<rfloor>; vs = []; ta = (K$ [], [], [], [], [], obs); va = RetVal (Addr a'); heap_clone P h a h' \<lfloor>(obs, a')\<rfloor>; M = clone; U = Class Object; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; hT = Class_type x1\<rbrakk> \<Longrightarrow> \<exists>T'. (\<exists>z. typeof_addr h' a' = \<lfloor>z\<rfloor> \<and> ty_of_htype z = T') \<and> P \<turnstile> T' \<le> Class Object
 2. \<And>hT obs a' C x21 x22. \<lbrakk>hconf h; wf_prog wf_md P; h \<unlhd> h'; preallocated h'; typeof_addr h a = \<lfloor>hT\<rfloor>; vs = []; ta = (K$ [], [], [], [], [], obs); va = RetVal (Addr a'); heap_clone P h a h' \<lfloor>(obs, a')\<rfloor>; M = clone; U = Class Object; typeof_addr h (thread_id2addr t) = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; hT = Array_type x21 x22\<rbrakk> \<Longrightarrow> \<exists>T'. (\<exists>z. typeof_addr h' a' = \<lfloor>z\<rfloor> \<and> ty_of_htype z = T') \<and> P \<turnstile> T' \<le> Class Object
[PROOF STEP]
apply(auto 4 4 dest!: typeof_addr_heap_clone dest: typeof_addr_is_type intro: widen_array_object subcls_C_Object)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma heap_copy_loc_progress:
  assumes hconf: "hconf h"
  and alconfa: "P,h \<turnstile> a@al : T"
  and alconfa': "P,h \<turnstile> a'@al : T"
  shows "\<exists>v h'. heap_copy_loc a a' al h ([ReadMem a al v, WriteMem a' al v]) h' \<and> P,h \<turnstile> v :\<le> T \<and> hconf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v h'. heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h' \<and> P,h \<turnstile> v :\<le> T \<and> hconf h'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>v h'. heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h' \<and> P,h \<turnstile> v :\<le> T \<and> hconf h'
[PROOF STEP]
from heap_read_total[OF hconf alconfa]
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. heap_read h a al v \<and> P,h \<turnstile> v :\<le> T
[PROOF STEP]
obtain v where "heap_read h a al v" "P,h \<turnstile> v :\<le> T"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. heap_read h a al v \<and> P,h \<turnstile> v :\<le> T

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>heap_read h a al v; P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
heap_read h a al v
P,h \<turnstile> v :\<le> T

goal (1 subgoal):
 1. \<exists>v h'. heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h' \<and> P,h \<turnstile> v :\<le> T \<and> hconf h'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
heap_read h a al v
P,h \<turnstile> v :\<le> T

goal (1 subgoal):
 1. \<exists>v h'. heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h' \<and> P,h \<turnstile> v :\<le> T \<and> hconf h'
[PROOF STEP]
from heap_write_total[OF hconf alconfa' \<open>P,h \<turnstile> v :\<le> T\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>h'. heap_write h a' al v h'
[PROOF STEP]
obtain h' where "heap_write h a' al v h'"
[PROOF STATE]
proof (prove)
using this:
\<exists>h'. heap_write h a' al v h'

goal (1 subgoal):
 1. (\<And>h'. heap_write h a' al v h' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
heap_write h a' al v h'

goal (1 subgoal):
 1. \<exists>v h'. heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h' \<and> P,h \<turnstile> v :\<le> T \<and> hconf h'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
heap_write h a' al v h'

goal (1 subgoal):
 1. \<exists>v h'. heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h' \<and> P,h \<turnstile> v :\<le> T \<and> hconf h'
[PROOF STEP]
hence "hconf h'"
[PROOF STATE]
proof (prove)
using this:
heap_write h a' al v h'

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
using hconf alconfa' \<open>P,h \<turnstile> v :\<le> T\<close>
[PROOF STATE]
proof (prove)
using this:
heap_write h a' al v h'
hconf h
P,h \<turnstile> a'@al : T
P,h \<turnstile> v :\<le> T

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
by(rule hconf_heap_write_mono)
[PROOF STATE]
proof (state)
this:
hconf h'

goal (1 subgoal):
 1. \<exists>v h'. heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h' \<and> P,h \<turnstile> v :\<le> T \<and> hconf h'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
heap_read h a al v
P,h \<turnstile> v :\<le> T
heap_write h a' al v h'
hconf h'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
heap_read h a al v
P,h \<turnstile> v :\<le> T
heap_write h a' al v h'
hconf h'

goal (1 subgoal):
 1. \<exists>v h'. heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h' \<and> P,h \<turnstile> v :\<le> T \<and> hconf h'
[PROOF STEP]
by(blast intro: heap_copy_loc.intros)
[PROOF STATE]
proof (state)
this:
\<exists>v h'. heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h' \<and> P,h \<turnstile> v :\<le> T \<and> hconf h'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma heap_copies_progress:
  assumes "hconf h"
  and "list_all2 (\<lambda>al T. P,h \<turnstile> a@al : T) als Ts"
  and "list_all2 (\<lambda>al T. P,h \<turnstile> a'@al : T) als Ts"
  shows "\<exists>vs h'. heap_copies a a' als h (concat (map (\<lambda>(al, v). [ReadMem a al v, WriteMem a' al v]) (zip als vs))) h' \<and> hconf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hconf h
list_all2 (addr_loc_type P h a) als Ts
list_all2 (addr_loc_type P h a') als Ts

goal (1 subgoal):
 1. \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'
[PROOF STEP]
proof(induct als arbitrary: h Ts)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) [] Ts; list_all2 (addr_loc_type P h a') [] Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' [] h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) [] vs)) h' \<and> hconf h'
 2. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
hconf h
list_all2 (addr_loc_type P h a) [] Ts
list_all2 (addr_loc_type P h a') [] Ts

goal (2 subgoals):
 1. \<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) [] Ts; list_all2 (addr_loc_type P h a') [] Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' [] h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) [] vs)) h' \<and> hconf h'
 2. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
hconf h
list_all2 (addr_loc_type P h a) [] Ts
list_all2 (addr_loc_type P h a') [] Ts

goal (1 subgoal):
 1. \<exists>vs h'. heap_copies a a' [] h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) [] vs)) h' \<and> hconf h'
[PROOF STEP]
by(auto intro: heap_copies.Nil)
[PROOF STATE]
proof (state)
this:
\<exists>vs h'. heap_copies a a' [] h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) [] vs)) h' \<and> hconf h'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
case (Cons al als)
[PROOF STATE]
proof (state)
this:
\<lbrakk>hconf ?h15; list_all2 (addr_loc_type P ?h15 a) als ?Ts15; list_all2 (addr_loc_type P ?h15 a') als ?Ts15\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als ?h15 (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'
hconf h
list_all2 (addr_loc_type P h a) (al # als) Ts
list_all2 (addr_loc_type P h a') (al # als) Ts

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
from \<open>list_all2 (\<lambda>al T. P,h \<turnstile> a@al : T) (al # als) Ts\<close>
[PROOF STATE]
proof (chain)
picking this:
list_all2 (addr_loc_type P h a) (al # als) Ts
[PROOF STEP]
obtain T' Ts' where [simp]: "Ts = T' # Ts'"
    and "P,h \<turnstile> a@al : T'" "list_all2 (\<lambda>al T. P,h \<turnstile> a@al : T) als Ts'"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h a) (al # als) Ts

goal (1 subgoal):
 1. (\<And>T' Ts'. \<lbrakk>Ts = T' # Ts'; P,h \<turnstile> a@al : T'; list_all2 (addr_loc_type P h a) als Ts'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: list_all2_Cons1)
[PROOF STATE]
proof (state)
this:
Ts = T' # Ts'
P,h \<turnstile> a@al : T'
list_all2 (addr_loc_type P h a) als Ts'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
from \<open>list_all2 (\<lambda>al T. P,h \<turnstile> a'@al : T) (al # als) Ts\<close>
[PROOF STATE]
proof (chain)
picking this:
list_all2 (addr_loc_type P h a') (al # als) Ts
[PROOF STEP]
have "P,h \<turnstile> a'@al : T'" and "list_all2 (\<lambda>al T. P,h \<turnstile> a'@al : T) als Ts'"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h a') (al # als) Ts

goal (1 subgoal):
 1. P,h \<turnstile> a'@al : T' &&& list_all2 (addr_loc_type P h a') als Ts'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> a'@al : T'
list_all2 (addr_loc_type P h a') als Ts'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
from \<open>hconf h\<close> \<open>P,h \<turnstile> a@al : T'\<close> \<open>P,h \<turnstile> a'@al : T'\<close>
[PROOF STATE]
proof (chain)
picking this:
hconf h
P,h \<turnstile> a@al : T'
P,h \<turnstile> a'@al : T'
[PROOF STEP]
obtain v h' where "heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h'"
    and "hconf h'"
[PROOF STATE]
proof (prove)
using this:
hconf h
P,h \<turnstile> a@al : T'
P,h \<turnstile> a'@al : T'

goal (1 subgoal):
 1. (\<And>v h'. \<lbrakk>heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h'; hconf h'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest: heap_copy_loc_progress)
[PROOF STATE]
proof (state)
this:
heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h'
hconf h'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h'
hconf h'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
hence "h \<unlhd> h'"
[PROOF STATE]
proof (prove)
using this:
heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h'
hconf h'

goal (1 subgoal):
 1. h \<unlhd> h'
[PROOF STEP]
by-(rule hext_heap_copy_loc)
[PROOF STATE]
proof (state)
this:
h \<unlhd> h'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
h \<unlhd> h'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
note \<open>hconf h'\<close>
[PROOF STATE]
proof (state)
this:
hconf h'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hconf h'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
from \<open>list_all2 (\<lambda>al T. P,h \<turnstile> a@al : T) als Ts'\<close>
[PROOF STATE]
proof (chain)
picking this:
list_all2 (addr_loc_type P h a) als Ts'
[PROOF STEP]
have "list_all2 (\<lambda>al T. P,h' \<turnstile> a@al : T) als Ts'"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h a) als Ts'

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h' a) als Ts'
[PROOF STEP]
by(rule list_all2_mono)(rule addr_loc_type_hext_mono[OF _ \<open>h \<unlhd> h'\<close>])
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a) als Ts'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a) als Ts'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
from \<open>list_all2 (\<lambda>al T. P,h \<turnstile> a'@al : T) als Ts'\<close>
[PROOF STATE]
proof (chain)
picking this:
list_all2 (addr_loc_type P h a') als Ts'
[PROOF STEP]
have "list_all2 (\<lambda>al T. P,h' \<turnstile> a'@al : T) als Ts'"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h a') als Ts'

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h' a') als Ts'
[PROOF STEP]
by(rule list_all2_mono)(rule addr_loc_type_hext_mono[OF _ \<open>h \<unlhd> h'\<close>])
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a') als Ts'

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
hconf h'
list_all2 (addr_loc_type P h' a) als Ts'
list_all2 (addr_loc_type P h' a') als Ts'
[PROOF STEP]
have "\<exists>vs h''. heap_copies a a' als h' (concat (map (\<lambda>(al, v). [ReadMem a al v, WriteMem a' al v]) (zip als vs))) h'' \<and> hconf h''"
[PROOF STATE]
proof (prove)
using this:
hconf h'
list_all2 (addr_loc_type P h' a) als Ts'
list_all2 (addr_loc_type P h' a') als Ts'

goal (1 subgoal):
 1. \<exists>vs h''. heap_copies a a' als h' (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h'' \<and> hconf h''
[PROOF STEP]
by(rule Cons)
[PROOF STATE]
proof (state)
this:
\<exists>vs h''. heap_copies a a' als h' (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h'' \<and> hconf h''

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>vs h''. heap_copies a a' als h' (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h'' \<and> hconf h''

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>vs h''. heap_copies a a' als h' (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h'' \<and> hconf h''
[PROOF STEP]
obtain vs h''
    where "heap_copies a a' als h' (concat (map (\<lambda>(al, v). [ReadMem a al v, WriteMem a' al v]) (zip als vs))) h''"
    and "hconf h''"
[PROOF STATE]
proof (prove)
using this:
\<exists>vs h''. heap_copies a a' als h' (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h'' \<and> hconf h''

goal (1 subgoal):
 1. (\<And>vs h''. \<lbrakk>heap_copies a a' als h' (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h''; hconf h''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
heap_copies a a' als h' (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h''
hconf h''

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h'
hconf h'
heap_copies a a' als h' (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h''
hconf h''
[PROOF STEP]
have "heap_copies a a' (al # als) h ([ReadMem a al v, WriteMem a' al v] @ (concat (map (\<lambda>(al, v). [ReadMem a al v, WriteMem a' al v]) (zip als vs)))) h''"
[PROOF STATE]
proof (prove)
using this:
heap_copy_loc a a' al h [ReadMem a al v, WriteMem a' al v] h'
hconf h'
heap_copies a a' als h' (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h''
hconf h''

goal (1 subgoal):
 1. heap_copies a a' (al # als) h ([ReadMem a al v, WriteMem a' al v] @ concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h''
[PROOF STEP]
by- (rule heap_copies.Cons)
[PROOF STATE]
proof (state)
this:
heap_copies a a' (al # als) h ([ReadMem a al v, WriteMem a' al v] @ concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h''

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
heap_copies a a' (al # als) h ([ReadMem a al v, WriteMem a' al v] @ concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h''

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
have "[ReadMem a al v, WriteMem a' al v] @ (concat (map (\<lambda>(al, v). [ReadMem a al v, WriteMem a' al v]) (zip als vs))) =
            (concat (map (\<lambda>(al, v). [ReadMem a al v, WriteMem a' al v]) (zip (al # als) (v # vs))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [ReadMem a al v, WriteMem a' al v] @ concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs) = concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (al # als) (v # vs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[ReadMem a al v, WriteMem a' al v] @ concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs) = concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (al # als) (v # vs))

goal (1 subgoal):
 1. \<And>aa als h Ts. \<lbrakk>\<And>h Ts. \<lbrakk>hconf h; list_all2 (addr_loc_type P h a) als Ts; list_all2 (addr_loc_type P h a') als Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' als h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) als vs)) h' \<and> hconf h'; hconf h; list_all2 (addr_loc_type P h a) (aa # als) Ts; list_all2 (addr_loc_type P h a') (aa # als) Ts\<rbrakk> \<Longrightarrow> \<exists>vs h'. heap_copies a a' (aa # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (aa # als) vs)) h' \<and> hconf h'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
heap_copies a a' (al # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (al # als) (v # vs))) h''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
heap_copies a a' (al # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (al # als) (v # vs))) h''

goal (1 subgoal):
 1. \<exists>vs h'. heap_copies a a' (al # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (al # als) vs)) h' \<and> hconf h'
[PROOF STEP]
using \<open>hconf h''\<close>
[PROOF STATE]
proof (prove)
using this:
heap_copies a a' (al # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (al # als) (v # vs))) h''
hconf h''

goal (1 subgoal):
 1. \<exists>vs h'. heap_copies a a' (al # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (al # als) vs)) h' \<and> hconf h'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>vs h'. heap_copies a a' (al # als) h (concat (map2 (\<lambda>al v. [ReadMem a al v, WriteMem a' al v]) (al # als) vs)) h' \<and> hconf h'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma heap_clone_progress:
  assumes wf: "wf_prog wf_md P"
  and typea: "typeof_addr h a = \<lfloor>hT\<rfloor>"
  and hconf: "hconf h"
  shows "\<exists>h' res. heap_clone P h a h' res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
from typea hconf
[PROOF STATE]
proof (chain)
picking this:
typeof_addr h a = \<lfloor>hT\<rfloor>
hconf h
[PROOF STEP]
have "is_htype P hT"
[PROOF STATE]
proof (prove)
using this:
typeof_addr h a = \<lfloor>hT\<rfloor>
hconf h

goal (1 subgoal):
 1. is_htype P hT
[PROOF STEP]
by(rule typeof_addr_is_type)
[PROOF STATE]
proof (state)
this:
is_htype P hT

goal (1 subgoal):
 1. \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
proof(cases "allocate h hT = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. allocate h hT = {} \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. allocate h hT \<noteq> {} \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
allocate h hT = {}

goal (2 subgoals):
 1. allocate h hT = {} \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. allocate h hT \<noteq> {} \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
with typea CloneFail[of h a hT P]
[PROOF STATE]
proof (chain)
picking this:
typeof_addr h a = \<lfloor>hT\<rfloor>
\<lbrakk>typeof_addr h a = \<lfloor>hT\<rfloor>; allocate h hT = {}\<rbrakk> \<Longrightarrow> heap_clone P h a h None
allocate h hT = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
typeof_addr h a = \<lfloor>hT\<rfloor>
\<lbrakk>typeof_addr h a = \<lfloor>hT\<rfloor>; allocate h hT = {}\<rbrakk> \<Longrightarrow> heap_clone P h a h None
allocate h hT = {}

goal (1 subgoal):
 1. \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>h' res. heap_clone P h a h' res

goal (1 subgoal):
 1. allocate h hT \<noteq> {} \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. allocate h hT \<noteq> {} \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
allocate h hT \<noteq> {}

goal (1 subgoal):
 1. allocate h hT \<noteq> {} \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
allocate h hT \<noteq> {}
[PROOF STEP]
obtain h' a' where new: "(h', a') \<in> allocate h hT"
[PROOF STATE]
proof (prove)
using this:
allocate h hT \<noteq> {}

goal (1 subgoal):
 1. (\<And>h' a'. (h', a') \<in> allocate h hT \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule not_empty_pairE)
[PROOF STATE]
proof (state)
this:
(h', a') \<in> allocate h hT

goal (1 subgoal):
 1. allocate h hT \<noteq> {} \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
hence "h \<unlhd> h'"
[PROOF STATE]
proof (prove)
using this:
(h', a') \<in> allocate h hT

goal (1 subgoal):
 1. h \<unlhd> h'
[PROOF STEP]
by(rule hext_allocate)
[PROOF STATE]
proof (state)
this:
h \<unlhd> h'

goal (1 subgoal):
 1. allocate h hT \<noteq> {} \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
have "hconf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
using new hconf \<open>is_htype P hT\<close>
[PROOF STATE]
proof (prove)
using this:
(h', a') \<in> allocate h hT
hconf h
is_htype P hT

goal (1 subgoal):
 1. hconf h'
[PROOF STEP]
by(rule hconf_allocate_mono)
[PROOF STATE]
proof (state)
this:
hconf h'

goal (1 subgoal):
 1. allocate h hT \<noteq> {} \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
proof(cases hT)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
case [simp]: (Class_type C)
[PROOF STATE]
proof (state)
this:
hT = Class_type C

goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
from \<open>is_htype P hT\<close>
[PROOF STATE]
proof (chain)
picking this:
is_htype P hT
[PROOF STEP]
have "is_class P C"
[PROOF STATE]
proof (prove)
using this:
is_htype P hT

goal (1 subgoal):
 1. is_class P C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_class P C

goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
from wf_Fields_Ex[OF wf this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>FDTs. P \<turnstile> C has_fields FDTs
[PROOF STEP]
obtain FDTs where FDTs: "P \<turnstile> C has_fields FDTs"
[PROOF STATE]
proof (prove)
using this:
\<exists>FDTs. P \<turnstile> C has_fields FDTs

goal (1 subgoal):
 1. (\<And>FDTs. P \<turnstile> C has_fields FDTs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P \<turnstile> C has_fields FDTs

goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
let ?als = "map (\<lambda>((F, D), Tfm). CField D F) FDTs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
let ?Ts = "map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
from typea FDTs
[PROOF STATE]
proof (chain)
picking this:
typeof_addr h a = \<lfloor>hT\<rfloor>
P \<turnstile> C has_fields FDTs
[PROOF STEP]
have "list_all2 (\<lambda>al T. P,h \<turnstile> a@al : T) ?als ?Ts"
[PROOF STATE]
proof (prove)
using this:
typeof_addr h a = \<lfloor>hT\<rfloor>
P \<turnstile> C has_fields FDTs

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
[PROOF STEP]
unfolding list_all2_map1 list_all2_map2 list_all2_same
[PROOF STATE]
proof (prove)
using this:
typeof_addr h a = \<lfloor>hT\<rfloor>
P \<turnstile> C has_fields FDTs

goal (1 subgoal):
 1. \<forall>x\<in>set FDTs. P,h \<turnstile> a@(case x of (x, xa) \<Rightarrow> (case x of (F, D) \<Rightarrow> \<lambda>Tfm. CField D F) xa) : (case x of (FD, T) \<Rightarrow> fst (the (map_of FDTs FD)))
[PROOF STEP]
by(fastforce intro: addr_loc_type.intros simp add: has_field_def dest: weak_map_of_SomeI)
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
hence "list_all2 (\<lambda>al T. P,h' \<turnstile> a@al : T) ?als ?Ts"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
[PROOF STEP]
by(rule list_all2_mono)(simp add: addr_loc_type_hext_mono[OF _ \<open>h \<unlhd> h'\<close>] split_def)
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
from new \<open>is_class P C\<close>
[PROOF STATE]
proof (chain)
picking this:
(h', a') \<in> allocate h hT
is_class P C
[PROOF STEP]
have "typeof_addr h' a' = \<lfloor>Class_type C\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
(h', a') \<in> allocate h hT
is_class P C

goal (1 subgoal):
 1. typeof_addr h' a' = \<lfloor>Class_type C\<rfloor>
[PROOF STEP]
by(auto dest: allocate_SomeD)
[PROOF STATE]
proof (state)
this:
typeof_addr h' a' = \<lfloor>Class_type C\<rfloor>

goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
with FDTs
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C has_fields FDTs
typeof_addr h' a' = \<lfloor>Class_type C\<rfloor>
[PROOF STEP]
have "list_all2 (\<lambda>al T. P,h' \<turnstile> a'@al : T) ?als ?Ts"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C has_fields FDTs
typeof_addr h' a' = \<lfloor>Class_type C\<rfloor>

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
[PROOF STEP]
unfolding list_all2_map1 list_all2_map2 list_all2_same
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C has_fields FDTs
typeof_addr h' a' = \<lfloor>Class_type C\<rfloor>

goal (1 subgoal):
 1. \<forall>x\<in>set FDTs. P,h' \<turnstile> a'@(case x of (x, xa) \<Rightarrow> (case x of (F, D) \<Rightarrow> \<lambda>Tfm. CField D F) xa) : (case x of (FD, T) \<Rightarrow> fst (the (map_of FDTs FD)))
[PROOF STEP]
by(fastforce intro: addr_loc_type.intros map_of_SomeI simp add: has_field_def dest: weak_map_of_SomeI)
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list_all2 (addr_loc_type P h' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
list_all2 (addr_loc_type P h' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
[PROOF STEP]
obtain obs h'' where "heap_copies a a' ?als h' obs h''" "hconf h''"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)
list_all2 (addr_loc_type P h' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs)

goal (1 subgoal):
 1. (\<And>obs h''. \<lbrakk>heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h' obs h''; hconf h''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: heap_copies_progress[OF \<open>hconf h'\<close>])
[PROOF STATE]
proof (state)
this:
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h' obs h''
hconf h''

goal (2 subgoals):
 1. \<And>x1. hT = Class_type x1 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
 2. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
with typea new FDTs ObjClone[of h a C h' a' P FDTs obs h'']
[PROOF STATE]
proof (chain)
picking this:
typeof_addr h a = \<lfloor>hT\<rfloor>
(h', a') \<in> allocate h hT
P \<turnstile> C has_fields FDTs
\<lbrakk>typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h', a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h' obs h''\<rbrakk> \<Longrightarrow> heap_clone P h a h'' \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h' obs h''
hconf h''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
typeof_addr h a = \<lfloor>hT\<rfloor>
(h', a') \<in> allocate h hT
P \<turnstile> C has_fields FDTs
\<lbrakk>typeof_addr h a = \<lfloor>Class_type C\<rfloor>; (h', a') \<in> allocate h (Class_type C); P \<turnstile> C has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h' obs h''\<rbrakk> \<Longrightarrow> heap_clone P h a h'' \<lfloor>(NewHeapElem a' (Class_type C) # obs, a')\<rfloor>
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs) h' obs h''
hconf h''

goal (1 subgoal):
 1. \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>h' res. heap_clone P h a h' res

goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
case [simp]: (Array_type T n)
[PROOF STATE]
proof (state)
this:
hT = Array_type T n

goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
[PROOF STEP]
obtain FDTs where FDTs: "P \<turnstile> Object has_fields FDTs"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P

goal (1 subgoal):
 1. (\<And>FDTs. P \<turnstile> Object has_fields FDTs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: wf_Fields_Ex is_class_Object)
[PROOF STATE]
proof (state)
this:
P \<turnstile> Object has_fields FDTs

goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
let ?als = "map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
let ?Ts = "map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
from \<open>h \<unlhd> h'\<close> typea
[PROOF STATE]
proof (chain)
picking this:
h \<unlhd> h'
typeof_addr h a = \<lfloor>hT\<rfloor>
[PROOF STEP]
have type'a: "typeof_addr h' a = \<lfloor>Array_type T n\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
h \<unlhd> h'
typeof_addr h a = \<lfloor>hT\<rfloor>

goal (1 subgoal):
 1. typeof_addr h' a = \<lfloor>Array_type T n\<rfloor>
[PROOF STEP]
by(auto intro: hext_arrD)
[PROOF STATE]
proof (state)
this:
typeof_addr h' a = \<lfloor>Array_type T n\<rfloor>

goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
from type'a FDTs
[PROOF STATE]
proof (chain)
picking this:
typeof_addr h' a = \<lfloor>Array_type T n\<rfloor>
P \<turnstile> Object has_fields FDTs
[PROOF STEP]
have "list_all2 (\<lambda>al T. P,h' \<turnstile> a@al : T) ?als ?Ts"
[PROOF STATE]
proof (prove)
using this:
typeof_addr h' a = \<lfloor>Array_type T n\<rfloor>
P \<turnstile> Object has_fields FDTs

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
[PROOF STEP]
by(fastforce intro: list_all2_all_nthI addr_loc_type.intros simp add: has_field_def list_all2_append list_all2_map1 list_all2_map2 list_all2_same dest: weak_map_of_SomeI)
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)

goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)

goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
from new \<open>is_htype P hT\<close>
[PROOF STATE]
proof (chain)
picking this:
(h', a') \<in> allocate h hT
is_htype P hT
[PROOF STEP]
have "typeof_addr h' a' = \<lfloor>Array_type T n\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
(h', a') \<in> allocate h hT
is_htype P hT

goal (1 subgoal):
 1. typeof_addr h' a' = \<lfloor>Array_type T n\<rfloor>
[PROOF STEP]
by(auto dest: allocate_SomeD)
[PROOF STATE]
proof (state)
this:
typeof_addr h' a' = \<lfloor>Array_type T n\<rfloor>

goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
hence "list_all2 (\<lambda>al T. P,h' \<turnstile> a'@al : T) ?als ?Ts"
[PROOF STATE]
proof (prove)
using this:
typeof_addr h' a' = \<lfloor>Array_type T n\<rfloor>

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
[PROOF STEP]
using FDTs
[PROOF STATE]
proof (prove)
using this:
typeof_addr h' a' = \<lfloor>Array_type T n\<rfloor>
P \<turnstile> Object has_fields FDTs

goal (1 subgoal):
 1. list_all2 (addr_loc_type P h' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
[PROOF STEP]
by(fastforce intro: list_all2_all_nthI addr_loc_type.intros simp add: has_field_def list_all2_append list_all2_map1 list_all2_map2 list_all2_same dest: weak_map_of_SomeI)
[PROOF STATE]
proof (state)
this:
list_all2 (addr_loc_type P h' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)

goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list_all2 (addr_loc_type P h' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
list_all2 (addr_loc_type P h' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
[PROOF STEP]
obtain obs h'' where "heap_copies a a' ?als h' obs h''" "hconf h''"
[PROOF STATE]
proof (prove)
using this:
list_all2 (addr_loc_type P h' a) (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)
list_all2 (addr_loc_type P h' a') (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) (map (\<lambda>(FD, T). fst (the (map_of FDTs FD))) FDTs @ replicate n T)

goal (1 subgoal):
 1. (\<And>obs h''. \<lbrakk>heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h' obs h''; hconf h''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: heap_copies_progress[OF \<open>hconf h'\<close>])
[PROOF STATE]
proof (state)
this:
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h' obs h''
hconf h''

goal (1 subgoal):
 1. \<And>x21 x22. hT = Array_type x21 x22 \<Longrightarrow> \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
with typea new FDTs ArrClone[of h a T n h' a' P FDTs obs h'']
[PROOF STATE]
proof (chain)
picking this:
typeof_addr h a = \<lfloor>hT\<rfloor>
(h', a') \<in> allocate h hT
P \<turnstile> Object has_fields FDTs
\<lbrakk>typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h', a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h' obs h''\<rbrakk> \<Longrightarrow> heap_clone P h a h'' \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h' obs h''
hconf h''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
typeof_addr h a = \<lfloor>hT\<rfloor>
(h', a') \<in> allocate h hT
P \<turnstile> Object has_fields FDTs
\<lbrakk>typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; (h', a') \<in> allocate h (Array_type T n); P \<turnstile> Object has_fields FDTs; heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h' obs h''\<rbrakk> \<Longrightarrow> heap_clone P h a h'' \<lfloor>(NewHeapElem a' (Array_type T n) # obs, a')\<rfloor>
heap_copies a a' (map (\<lambda>((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h' obs h''
hconf h''

goal (1 subgoal):
 1. \<exists>h' res. heap_clone P h a h' res
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>h' res. heap_clone P h a h' res

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>h' res. heap_clone P h a h' res

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>h' res. heap_clone P h a h' res

goal:
No subgoals!
[PROOF STEP]
qed