[STATEMENT]
lemma rel_state_lookup:
  "((=) ===> rel_state (=)) pair.lookup_pair lookup_pair"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> local.rel_state (=)) pair.lookup_pair local.lookup_pair
[PROOF STEP]
unfolding pair.lookup_pair_def lookup_pair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> local.rel_state (=)) (\<lambda>k. let k' = key1 k in local.get_k2 \<bind> (\<lambda>k2. if k' = k2 then local.lookup2 (key2 k) else local.get_k1 \<bind> (\<lambda>k1. if k' = k1 then local.lookup1 (key2 k) else State_Monad.return None))) (\<lambda>k. let k' = key1 k in !k_ref2 \<bind> (\<lambda>k2. if k' = k2 then !m_ref2 \<bind> (\<lambda>m2. local.mem_lookup m2 (key2 k)) else !k_ref1 \<bind> (\<lambda>k1. if k' = k1 then !m_ref1 \<bind> (\<lambda>m1. local.mem_lookup m1 (key2 k)) else return None)))
[PROOF STEP]
unfolding
    mem_lookup1_def[symmetric] mem_lookup2_def[symmetric]
    get_k2_def[symmetric] get_k2'_def[symmetric]
    get_k1_def[symmetric] get_k1'_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> local.rel_state (=)) (\<lambda>k. let k' = key1 k in local.get_k2 \<bind> (\<lambda>k2. if k' = k2 then local.lookup2 (key2 k) else local.get_k1 \<bind> (\<lambda>k1. if k' = k1 then local.lookup1 (key2 k) else State_Monad.return None))) (\<lambda>k. let k' = key1 k in local.get_k2' \<bind> (\<lambda>k2. if k' = k2 then local.mem_lookup2 (key2 k) else local.get_k1' \<bind> (\<lambda>k1. if k' = k1 then local.mem_lookup1 (key2 k) else return None)))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma rel_state_update:
  "((=) ===> (=) ===> rel_state (=)) pair.update_pair update_pair"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> (=) ===> local.rel_state (=)) pair.update_pair local.update_pair
[PROOF STEP]
unfolding pair.update_pair_def update_pair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> (=) ===> local.rel_state (=)) (\<lambda>k v. let k' = key1 k in local.get_k1 \<bind> (\<lambda>k1. if k' = k1 then local.update1 (key2 k) v else local.get_k2 \<bind> (\<lambda>k2. if k' = k2 then local.update2 (key2 k) v else local.move12 k' \<bind> (\<lambda>_. local.update1 (key2 k) v)))) (\<lambda>k v. let k' = key1 k in !k_ref1 \<bind> (\<lambda>k1. if k' = k1 then !m_ref1 \<bind> (\<lambda>m. local.mem_update m (key2 k) v) else !k_ref2 \<bind> (\<lambda>k2. if k' = k2 then !m_ref2 \<bind> (\<lambda>m. local.mem_update m (key2 k) v) else !k_ref1 \<bind> (\<lambda>k1. local.mem_empty \<bind> (\<lambda>m. !m_ref1 \<bind> (\<lambda>m1. k_ref2 := k1 \<bind> (\<lambda>_. k_ref1 := k' \<bind> (\<lambda>_. m_ref2 := m1 \<bind> (\<lambda>_. m_ref1 := m)))))) \<bind> (\<lambda>_. !m_ref1 \<bind> (\<lambda>m. local.mem_update m (key2 k) v)))))
[PROOF STEP]
unfolding move12'_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> (=) ===> local.rel_state (=)) (\<lambda>k v. let k' = key1 k in local.get_k1 \<bind> (\<lambda>k1. if k' = k1 then local.update1 (key2 k) v else local.get_k2 \<bind> (\<lambda>k2. if k' = k2 then local.update2 (key2 k) v else local.move12 k' \<bind> (\<lambda>_. local.update1 (key2 k) v)))) (\<lambda>k v. let k' = key1 k in !k_ref1 \<bind> (\<lambda>k1. if k' = k1 then !m_ref1 \<bind> (\<lambda>m. local.mem_update m (key2 k) v) else !k_ref2 \<bind> (\<lambda>k2. if k' = k2 then !m_ref2 \<bind> (\<lambda>m. local.mem_update m (key2 k) v) else local.move12' k' \<bind> (\<lambda>_. !m_ref1 \<bind> (\<lambda>m. local.mem_update m (key2 k) v)))))
[PROOF STEP]
unfolding
    update1'_def[symmetric] update2'_def[symmetric]
    get_k2_def[symmetric] get_k2'_def[symmetric]
    get_k1_def[symmetric] get_k1'_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> (=) ===> local.rel_state (=)) (\<lambda>k v. let k' = key1 k in local.get_k1 \<bind> (\<lambda>k1. if k' = k1 then local.update1 (key2 k) v else local.get_k2 \<bind> (\<lambda>k2. if k' = k2 then local.update2 (key2 k) v else local.move12 k' \<bind> (\<lambda>_. local.update1 (key2 k) v)))) (\<lambda>k v. let k' = key1 k in local.get_k1' \<bind> (\<lambda>k1. if k' = k1 then local.update1' (key2 k) v else local.get_k2' \<bind> (\<lambda>k2. if k' = k2 then local.update2' (key2 k) v else local.move12' k' \<bind> (\<lambda>_. local.update1' (key2 k) v))))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma inv_pairD:
  "inv_pair_weak heap" if "pair.inv_pair heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv_pair_weak heap
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
pair.inv_pair heap

goal (1 subgoal):
 1. local.inv_pair_weak heap
[PROOF STEP]
unfolding pair.inv_pair_def
[PROOF STATE]
proof (prove)
using this:
let k1 = fst (run_state local.get_k1 heap); k2 = fst (run_state local.get_k2 heap) in (\<forall>k\<in>dom (pair.mem1.map_of heap). \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>dom (pair.mem2.map_of heap). \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> local.inv_pair_weak heap

goal (1 subgoal):
 1. local.inv_pair_weak heap
[PROOF STEP]
by (auto simp: Let_def)


[STATEMENT]
lemma mem_rel_state_ofI:
  "mem.rel_state (=) m' m" if
  "rel_state (=) m' m"
  "\<And> heap. pair.inv_pair heap \<Longrightarrow>
    (case State_Monad.run_state m' heap of (_, heap) \<Rightarrow> inv_pair_weak heap \<longrightarrow> pair.inv_pair heap)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mem.rel_state (=) m' m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mem.rel_state (=) m' m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mem.rel_state (=) m' m
[PROOF STEP]
apply (rule mem.rel_state_intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>heap v heap'. \<lbrakk>pair.inv_pair heap; run_state m' heap = (v, heap')\<rbrakk> \<Longrightarrow> \<exists>v'. v = v' \<and> execute m heap = Some (v', heap')
 2. \<And>heap v heap'. \<lbrakk>pair.inv_pair heap; run_state m' heap = (v, heap')\<rbrakk> \<Longrightarrow> pair.inv_pair heap'
[PROOF STEP]
subgoal for heap v heap'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pair.inv_pair heap; run_state m' heap = (v, heap')\<rbrakk> \<Longrightarrow> \<exists>v'. v = v' \<and> execute m heap = Some (v', heap')
[PROOF STEP]
by (auto elim: rel_state_elim[OF that(1)] dest!: inv_pairD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>heap v heap'. \<lbrakk>pair.inv_pair heap; run_state m' heap = (v, heap')\<rbrakk> \<Longrightarrow> pair.inv_pair heap'
[PROOF STEP]
subgoal premises prems for heap v heap'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.inv_pair heap'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pair.inv_pair heap'
[PROOF STEP]
from prems that(1)
[PROOF STATE]
proof (chain)
picking this:
pair.inv_pair heap
run_state m' heap = (v, heap')
local.rel_state (=) m' m
[PROOF STEP]
have "inv_pair_weak heap'"
[PROOF STATE]
proof (prove)
using this:
pair.inv_pair heap
run_state m' heap = (v, heap')
local.rel_state (=) m' m

goal (1 subgoal):
 1. local.inv_pair_weak heap'
[PROOF STEP]
by (fastforce elim: rel_state_elim dest: inv_pairD)
[PROOF STATE]
proof (state)
this:
local.inv_pair_weak heap'

goal (1 subgoal):
 1. pair.inv_pair heap'
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
pair.inv_pair heap
run_state m' heap = (v, heap')
local.inv_pair_weak heap'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pair.inv_pair heap
run_state m' heap = (v, heap')
local.inv_pair_weak heap'

goal (1 subgoal):
 1. pair.inv_pair heap'
[PROOF STEP]
by (auto dest: that(2))
[PROOF STATE]
proof (state)
this:
pair.inv_pair heap'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mem.rel_state (=) m' m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mem_rel_state_ofI':
  "mem.rel_state (=) m' m" if
  "rel_state (=) m' m"
  "DP_CRelVS.lift_p pair.inv_pair m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mem.rel_state (=) m' m
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
local.rel_state (=) m' m
DP_CRelVS.lift_p pair.inv_pair m'

goal (1 subgoal):
 1. mem.rel_state (=) m' m
[PROOF STEP]
by (auto elim: DP_CRelVS.lift_p_P intro: mem_rel_state_ofI)


[STATEMENT]
lemma rel_state_lookup':
  "((=) ===> mem.rel_state (=)) pair.lookup_pair lookup_pair"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> mem.rel_state (=)) pair.lookup_pair local.lookup_pair
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. x = y \<Longrightarrow> mem.rel_state (=) (pair.lookup_pair x) (local.lookup_pair y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. mem.rel_state (=) (pair.lookup_pair x) (local.lookup_pair x)
[PROOF STEP]
apply (rule mem_rel_state_ofI')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. local.rel_state (=) (pair.lookup_pair x) (local.lookup_pair x)
 2. \<And>x. DP_CRelVS.lift_p pair.inv_pair (pair.lookup_pair x)
[PROOF STEP]
using rel_state_lookup
[PROOF STATE]
proof (prove)
using this:
((=) ===> local.rel_state (=)) pair.lookup_pair local.lookup_pair

goal (2 subgoals):
 1. \<And>x. local.rel_state (=) (pair.lookup_pair x) (local.lookup_pair x)
 2. \<And>x. DP_CRelVS.lift_p pair.inv_pair (pair.lookup_pair x)
[PROOF STEP]
apply (rule rel_funD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x = x
 2. \<And>x. DP_CRelVS.lift_p pair.inv_pair (pair.lookup_pair x)
[PROOF STEP]
apply (rule refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. DP_CRelVS.lift_p pair.inv_pair (pair.lookup_pair x)
[PROOF STEP]
apply (rule lookup_inv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rel_state_update':
  "((=) ===> (=) ===> mem.rel_state (=)) pair.update_pair update_pair"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> (=) ===> mem.rel_state (=)) pair.update_pair local.update_pair
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> mem.rel_state (=) (pair.update_pair x xa) (local.update_pair y ya)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> mem.rel_state (=) (pair.update_pair y ya) (local.update_pair y ya)
[PROOF STEP]
apply (rule mem_rel_state_ofI')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> local.rel_state (=) (pair.update_pair y ya) (local.update_pair y ya)
 2. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p pair.inv_pair (pair.update_pair y ya)
[PROOF STEP]
subgoal for x y a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; a = b\<rbrakk> \<Longrightarrow> local.rel_state (=) (pair.update_pair y b) (local.update_pair y b)
[PROOF STEP]
using rel_state_update
[PROOF STATE]
proof (prove)
using this:
((=) ===> (=) ===> local.rel_state (=)) pair.update_pair local.update_pair

goal (1 subgoal):
 1. \<lbrakk>x = y; a = b\<rbrakk> \<Longrightarrow> local.rel_state (=) (pair.update_pair y b) (local.update_pair y b)
[PROOF STEP]
by (blast dest: rel_funD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; xa = ya\<rbrakk> \<Longrightarrow> DP_CRelVS.lift_p pair.inv_pair (pair.update_pair y ya)
[PROOF STEP]
by (rule update_inv)


[STATEMENT]
lemma mem_rel_state_resultD:
  "result_of m heap = fst (run_state m' heap)" if "mem.rel_state (=) m' m" "pair.inv_pair heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. result_of m heap = fst (run_state m' heap)
[PROOF STEP]
by (metis (mono_tags, lifting) mem.rel_state_elim option.sel that)


[STATEMENT]
lemma map_of_heap_eq:
  "mem.map_of_heap heap = pair.pair.map_of heap" if "pair.inv_pair heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mem.map_of_heap heap = pair.pair.map_of heap
[PROOF STEP]
unfolding mem.map_of_heap_def pair.pair.map_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>k. result_of (local.lookup_pair k) heap) = (\<lambda>k. fst (run_state (pair.lookup_pair k) heap))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
pair.inv_pair heap

goal (1 subgoal):
 1. (\<lambda>k. result_of (local.lookup_pair k) heap) = (\<lambda>k. fst (run_state (pair.lookup_pair k) heap))
[PROOF STEP]
by (simp add: mem_rel_state_resultD[OF rel_state_lookup'[THEN rel_funD]])


[STATEMENT]
lemma init_state_empty1:
  "pair.mem1.map_of heap' k = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.mem1.map_of heap' k = None
[PROOF STEP]
using init
[PROOF STATE]
proof (prove)
using this:
execute (local.init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. pair.mem1.map_of heap' k = None
[PROOF STEP]
unfolding pair.mem1.map_of_def lookup1_def mem_lookup_def init_state_def
[PROOF STATE]
proof (prove)
using this:
execute (local.mem_empty \<bind> (\<lambda>m1. local.mem_empty \<bind> init_state_inner k1 k2 m1)) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. fst (run_state (state_of (!m_ref1 \<bind> (\<lambda>m. let i = to_index k in if i < size then Array.nth m i else return None))) heap') = None
[PROOF STEP]
by (auto
        simp: init_state_inner_nth init_state_inner_alloc(3) execute_simps Let_def
        elim!: execute_bind_success'[OF success_empty])
     (metis
        Array.present_alloc Memory_Heap.length_mem_empty execute_new execute_nth(1) fst_conv
        length_def mem_empty_def nth_mem_empty option.sel present_alloc_get snd_conv
     )


[STATEMENT]
lemma init_state_empty2:
  "pair.mem2.map_of heap' k = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.mem2.map_of heap' k = None
[PROOF STEP]
using init
[PROOF STATE]
proof (prove)
using this:
execute (local.init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. pair.mem2.map_of heap' k = None
[PROOF STEP]
unfolding pair.mem2.map_of_def lookup2_def mem_lookup_def init_state_def
[PROOF STATE]
proof (prove)
using this:
execute (local.mem_empty \<bind> (\<lambda>m1. local.mem_empty \<bind> init_state_inner k1 k2 m1)) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. fst (run_state (state_of (!m_ref2 \<bind> (\<lambda>m. let i = to_index k in if i < size then Array.nth m i else return None))) heap') = None
[PROOF STEP]
by (auto
        simp: execute_simps init_state_inner_nth init_state_inner_alloc(4) Let_def
        elim!: execute_bind_success'[OF success_empty]
     )
     (metis fst_conv nth_mem_empty option.sel snd_conv)


[STATEMENT]
lemma init_state_inv':
  "pair.inv_pair heap'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.inv_pair heap'
[PROOF STEP]
unfolding pair.inv_pair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let k1 = fst (run_state local.get_k1 heap'); k2 = fst (run_state local.get_k2 heap') in (\<forall>k\<in>dom (pair.mem1.map_of heap'). \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>dom (pair.mem2.map_of heap'). \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> local.inv_pair_weak heap'
[PROOF STEP]
apply (auto simp: Let_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>k y. pair.mem1.map_of heap' k = Some y \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state local.get_k1 heap') \<and> key2 k' = k
 2. \<And>k y. pair.mem2.map_of heap' k = Some y \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state local.get_k2 heap') \<and> key2 k' = k
 3. fst (run_state local.get_k1 heap') = fst (run_state local.get_k2 heap') \<Longrightarrow> False
 4. local.inv_pair_weak heap'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.mem1.map_of heap' k_ = Some y_ \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state local.get_k1 heap') \<and> key2 k' = k_
[PROOF STEP]
using init_state_empty1
[PROOF STATE]
proof (prove)
using this:
pair.mem1.map_of heap' ?k = None

goal (1 subgoal):
 1. pair.mem1.map_of heap' k_ = Some y_ \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state local.get_k1 heap') \<and> key2 k' = k_
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k y. pair.mem2.map_of heap' k = Some y \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state local.get_k2 heap') \<and> key2 k' = k
 2. fst (run_state local.get_k1 heap') = fst (run_state local.get_k2 heap') \<Longrightarrow> False
 3. local.inv_pair_weak heap'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.mem2.map_of heap' k_ = Some y_ \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state local.get_k2 heap') \<and> key2 k' = k_
[PROOF STEP]
using init_state_empty2
[PROOF STATE]
proof (prove)
using this:
pair.mem2.map_of heap' ?k = None

goal (1 subgoal):
 1. pair.mem2.map_of heap' k_ = Some y_ \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state local.get_k2 heap') \<and> key2 k' = k_
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. fst (run_state local.get_k1 heap') = fst (run_state local.get_k2 heap') \<Longrightarrow> False
 2. local.inv_pair_weak heap'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (run_state local.get_k1 heap') = fst (run_state local.get_k2 heap') \<Longrightarrow> False
[PROOF STEP]
using neq init
[PROOF STATE]
proof (prove)
using this:
k1 \<noteq> k2
execute (local.init_state k1 k2) heap = Some ((k_ref1, k_ref2, m_ref1, m_ref2), heap')

goal (1 subgoal):
 1. fst (run_state local.get_k1 heap') = fst (run_state local.get_k2 heap') \<Longrightarrow> False
[PROOF STEP]
by (simp add: get_k1_def get_k2_def init_state_k1 init_state_k2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv_pair_weak heap'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv_pair_weak heap'
[PROOF STEP]
by (rule init_state_inv[OF init])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma init_state_empty:
  "pair.pair.map_of heap' \<subseteq>\<^sub>m Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.pair.map_of heap' \<subseteq>\<^sub>m Map.empty
[PROOF STEP]
using neq
[PROOF STATE]
proof (prove)
using this:
k1 \<noteq> k2

goal (1 subgoal):
 1. pair.pair.map_of heap' \<subseteq>\<^sub>m Map.empty
[PROOF STEP]
by (intro pair.emptyI init_state_inv' map_emptyI init_state_empty1 init_state_empty2)


[STATEMENT]
lemma supp_transform: "supp (transform a e) \<subseteq> supp e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (ccTransform a e) \<subseteq> supp e
[PROOF STEP]
by (induction rule: transform.induct)
       (auto simp add: exp_assn.supp Let_supp dest!: subsetD[OF supp_map_transform] subsetD[OF supp_map_transform_step] )


[STATEMENT]
lemma transform_alts_Nil[simp]: "transform_alts [] S = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transform_alts [] S = S
[PROOF STEP]
by (induction  S) auto


[STATEMENT]
lemma Astack_transform_alts[simp]:
    "Astack (transform_alts as S) = Astack S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Astack (transform_alts as S) = Astack S
[PROOF STEP]
by (induction rule: transform_alts.induct) auto


[STATEMENT]
lemma fresh_star_transform_alts[intro]: "a \<sharp>* S \<Longrightarrow> a \<sharp>* transform_alts as S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp>* S \<Longrightarrow> a \<sharp>* transform_alts as S
[PROOF STEP]
by (induction as S  rule: transform_alts.induct) (auto simp add: fresh_star_Cons)


[STATEMENT]
lemma closed_consistent:
    assumes "fv e = ({}::var set)"
    shows "consistent (\<bottom>, 0, []) ([], e, [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent (\<bottom>, 0, []) ([], e, [])
[PROOF STEP]
by (auto simp add: edom_empty_iff_bot closed_a_consistent[OF assms])