[STATEMENT]
lemma map_of_le_pair:
  "pair.map_of (Pair_Storage k1 k2 m1 m2) \<subseteq>\<^sub>m (map_of m1 ++ map_of m2)"
  if "inv_pair (Pair_Storage k1 k2 m1 m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.map_of (Pair_Storage k1 k2 m1 m2) \<subseteq>\<^sub>m local.map_of m1 ++ local.map_of m2
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. pair.map_of (Pair_Storage k1 k2 m1 m2) \<subseteq>\<^sub>m local.map_of m1 ++ local.map_of m2
[PROOF STEP]
unfolding pair.map_of_def
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. (\<lambda>k. fst (run_state (lookup_pair k) (Pair_Storage k1 k2 m1 m2))) \<subseteq>\<^sub>m local.map_of m1 ++ local.map_of m2
[PROOF STEP]
unfolding lookup_pair_def inv_pair_def map_of_def map_le_def dom_def map_add_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` {a. fst (run_state (lookup a) m1) \<noteq> None} \<subseteq> {k1} \<and> key ` {a. fst (run_state (lookup a) m2) \<noteq> None} \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. \<forall>a\<in>{a. fst (run_state (State (\<lambda>mem. case mem of Pair_Storage k1 k2 m1 m2 \<Rightarrow> let k' = key a in if k' = k2 then case run_state (lookup a) m2 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m1 m) else if k' = k1 then case run_state (lookup a) m1 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m m2) else (None, mem))) (Pair_Storage k1 k2 m1 m2)) \<noteq> None}. fst (run_state (State (\<lambda>mem. case mem of Pair_Storage k1 k2 m1 m2 \<Rightarrow> let k' = key a in if k' = k2 then case run_state (lookup a) m2 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m1 m) else if k' = k1 then case run_state (lookup a) m1 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m m2) else (None, mem))) (Pair_Storage k1 k2 m1 m2)) = (case fst (run_state (lookup a) m2) of None \<Rightarrow> fst (run_state (lookup a) m1) | Some x \<Rightarrow> Some x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a y. \<lbrakk>key ` {a. \<exists>y. fst (run_state (lookup a) m1) = Some y} \<subseteq> {k1}; key ` {a. \<exists>y. fst (run_state (lookup a) m2) = Some y} \<subseteq> {k2}; k1 \<noteq> k2; P m1; P m2; fst (let k' = key a in if k' = k2 then case run_state (lookup a) m2 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m1 m) else if k' = k1 then case run_state (lookup a) m1 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m m2) else (None, Pair_Storage k1 k2 m1 m2)) = Some y\<rbrakk> \<Longrightarrow> Some y = (case fst (run_state (lookup a) m2) of None \<Rightarrow> fst (run_state (lookup a) m1) | Some x \<Rightarrow> Some x)
[PROOF STEP]
apply (auto 4 6 split: prod.split_asm if_split_asm option.split simp: Let_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pair_le_map_of:
  "map_of m1 ++ map_of m2 \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 k2 m1 m2)"
  if "inv_pair (Pair_Storage k1 k2 m1 m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.map_of m1 ++ local.map_of m2 \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 k2 m1 m2)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. local.map_of m1 ++ local.map_of m2 \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 k2 m1 m2)
[PROOF STEP]
unfolding pair.map_of_def
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. local.map_of m1 ++ local.map_of m2 \<subseteq>\<^sub>m (\<lambda>k. fst (run_state (lookup_pair k) (Pair_Storage k1 k2 m1 m2)))
[PROOF STEP]
unfolding lookup_pair_def inv_pair_def map_of_def map_le_def dom_def map_add_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` {a. fst (run_state (lookup a) m1) \<noteq> None} \<subseteq> {k1} \<and> key ` {a. fst (run_state (lookup a) m2) \<noteq> None} \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. \<forall>a\<in>{a. (case fst (run_state (lookup a) m2) of None \<Rightarrow> fst (run_state (lookup a) m1) | Some x \<Rightarrow> Some x) \<noteq> None}. (case fst (run_state (lookup a) m2) of None \<Rightarrow> fst (run_state (lookup a) m1) | Some x \<Rightarrow> Some x) = fst (run_state (State (\<lambda>mem. case mem of Pair_Storage k1 k2 m1 m2 \<Rightarrow> let k' = key a in if k' = k2 then case run_state (lookup a) m2 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m1 m) else if k' = k1 then case run_state (lookup a) m1 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m m2) else (None, mem))) (Pair_Storage k1 k2 m1 m2))
[PROOF STEP]
by (auto 4 5 split: prod.split_asm if_split_asm option.split simp: Let_def)


[STATEMENT]
lemma map_of_eq_pair:
  "map_of m1 ++ map_of m2 = pair.map_of (Pair_Storage k1 k2 m1 m2)"
  if "inv_pair (Pair_Storage k1 k2 m1 m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.map_of m1 ++ local.map_of m2 = pair.map_of (Pair_Storage k1 k2 m1 m2)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. local.map_of m1 ++ local.map_of m2 = pair.map_of (Pair_Storage k1 k2 m1 m2)
[PROOF STEP]
unfolding pair.map_of_def
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. local.map_of m1 ++ local.map_of m2 = (\<lambda>k. fst (run_state (lookup_pair k) (Pair_Storage k1 k2 m1 m2)))
[PROOF STEP]
unfolding lookup_pair_def inv_pair_def map_of_def map_le_def dom_def map_add_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` {a. fst (run_state (lookup a) m1) \<noteq> None} \<subseteq> {k1} \<and> key ` {a. fst (run_state (lookup a) m2) \<noteq> None} \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. (\<lambda>x. case fst (run_state (lookup x) m2) of None \<Rightarrow> fst (run_state (lookup x) m1) | Some x \<Rightarrow> Some x) = (\<lambda>k. fst (run_state (State (\<lambda>mem. case mem of Pair_Storage k1 k2 m1 m2 \<Rightarrow> let k' = key k in if k' = k2 then case run_state (lookup k) m2 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m1 m) else if k' = k1 then case run_state (lookup k) m1 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m m2) else (None, mem))) (Pair_Storage k1 k2 m1 m2)))
[PROOF STEP]
by (auto 4 7 split: prod.split_asm if_split_asm option.split simp: Let_def)


[STATEMENT]
lemma inv_pair_neq[simp, dest]:
  False if "inv_pair (Pair_Storage k k x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k k x y)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k k x y of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto


[STATEMENT]
lemma inv_pair_P_D1:
  "P m1" if "inv_pair (Pair_Storage k1 k2 m1 m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P m1
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. P m1
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. P m1
[PROOF STEP]
by auto


[STATEMENT]
lemma inv_pair_P_D2:
  "P m2" if "inv_pair (Pair_Storage k1 k2 m1 m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P m2
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. P m2
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. P m2
[PROOF STEP]
by auto


[STATEMENT]
lemma inv_pair_domD[intro]:
  "dom (map_of m1) \<inter> dom (map_of m2) = {}" if "inv_pair (Pair_Storage k1 k2 m1 m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (local.map_of m1) \<inter> dom (local.map_of m2) = {}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. dom (local.map_of m1) \<inter> dom (local.map_of m2) = {}
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. dom (local.map_of m1) \<inter> dom (local.map_of m2) = {}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma mem_correct_pair:
  "mem_correct lookup_pair update_pair inv_pair"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mem_correct lookup_pair update_pair inv_pair
[PROOF STEP]
proof (standard, goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>k. lift_p inv_pair (lookup_pair k)
 2. \<And>k v. lift_p inv_pair (update_pair k v)
 3. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 4. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
case (1 k) \<comment> \<open>Lookup invariant\<close>
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>k. lift_p inv_pair (lookup_pair k)
 2. \<And>k v. lift_p inv_pair (update_pair k v)
 3. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 4. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
with lookup_inv[of k]
[PROOF STATE]
proof (chain)
picking this:
lift_p P (lookup k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lift_p P (lookup k)

goal (1 subgoal):
 1. lift_p inv_pair (lookup_pair k)
[PROOF STEP]
unfolding lookup_pair_def Let_def
[PROOF STATE]
proof (prove)
using this:
lift_p P (lookup k)

goal (1 subgoal):
 1. lift_p inv_pair (State (\<lambda>mem. case mem of Pair_Storage k1 k2 m1 m2 \<Rightarrow> if key k = k2 then case run_state (lookup k) m2 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m1 m) else if key k = k1 then case run_state (lookup k) m1 of (v, m) \<Rightarrow> (v, Pair_Storage k1 k2 m m2) else (None, mem)))
[PROOF STEP]
by (auto intro!: lift_pI split: pair_storage.split_asm if_split_asm prod.split_asm)
       (auto dest: lift_p_P simp: inv_pair_def,
         (force dest!: lookup_correct[of _ k] map_le_implies_dom_le)+
       )
[PROOF STATE]
proof (state)
this:
lift_p inv_pair (lookup_pair k)

goal (3 subgoals):
 1. \<And>k v. lift_p inv_pair (update_pair k v)
 2. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 3. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>k v. lift_p inv_pair (update_pair k v)
 2. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 3. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
case (2 k v) \<comment> \<open>Update invariant\<close>
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>k v. lift_p inv_pair (update_pair k v)
 2. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 3. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
with update_inv[of k v] update_correct[OF P_empty, of k v] P_empty
[PROOF STATE]
proof (chain)
picking this:
lift_p P (update k v)
local.map_of (snd (run_state (update k v) empty)) \<subseteq>\<^sub>m local.map_of empty(k \<mapsto> v)
P empty
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lift_p P (update k v)
local.map_of (snd (run_state (update k v) empty)) \<subseteq>\<^sub>m local.map_of empty(k \<mapsto> v)
P empty

goal (1 subgoal):
 1. lift_p inv_pair (update_pair k v)
[PROOF STEP]
unfolding update_pair_def Let_def
[PROOF STATE]
proof (prove)
using this:
lift_p P (update k v)
local.map_of (snd (run_state (update k v) empty)) \<subseteq>\<^sub>m local.map_of empty(k \<mapsto> v)
P empty

goal (1 subgoal):
 1. lift_p inv_pair (State (case_pair_storage (\<lambda>k1 k2 m1 m2. if key k = k1 then case run_state (update k v) m1 of (x, m) \<Rightarrow> ((), Pair_Storage k1 k2 m m2) else if key k = k2 then case run_state (update k v) m2 of (x, m) \<Rightarrow> ((), Pair_Storage k1 k2 m1 m) else case run_state (update k v) empty of (x, m) \<Rightarrow> ((), Pair_Storage (key k) k1 m m1))))
[PROOF STEP]
by (auto intro!: lift_pI split: pair_storage.split_asm if_split_asm prod.split_asm)
       (auto dest: lift_p_P simp: inv_pair_def,
         (force dest: lift_p_P dest!: update_correct[of _ k v] map_le_implies_dom_le)+
       )
[PROOF STATE]
proof (state)
this:
lift_p inv_pair (update_pair k v)

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
case (3 m k)
[PROOF STATE]
proof (state)
this:
inv_pair m

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
inv_pair m

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
fix m1 v1 m1' m2 v2 m2' k1 k2
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
assume assms:
      "State_Monad.run_state (lookup k) m1 = (v1, m1')" "State_Monad.run_state (lookup k) m2 = (v2, m2')"
      "inv_pair (Pair_Storage k1 k2 m1 m2)"
[PROOF STATE]
proof (state)
this:
run_state (lookup k) m1 = (v1, m1')
run_state (lookup k) m2 = (v2, m2')
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
run_state (lookup k) m1 = (v1, m1')
run_state (lookup k) m2 = (v2, m2')
inv_pair (Pair_Storage k1 k2 m1 m2)
[PROOF STEP]
have "P m1" "P m2"
[PROOF STATE]
proof (prove)
using this:
run_state (lookup k) m1 = (v1, m1')
run_state (lookup k) m2 = (v2, m2')
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. P m1 &&& P m2
[PROOF STEP]
by (auto intro: inv_pair_P_D1 inv_pair_P_D2)
[PROOF STATE]
proof (state)
this:
P m1
P m2

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have [intro]: "map_of m1' \<subseteq>\<^sub>m map_of m1" "map_of m2' \<subseteq>\<^sub>m map_of m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.map_of m1' \<subseteq>\<^sub>m local.map_of m1 &&& local.map_of m2' \<subseteq>\<^sub>m local.map_of m2
[PROOF STEP]
using lookup_correct[OF \<open>P m1\<close>, of k] lookup_correct[OF \<open>P m2\<close>, of k] assms
[PROOF STATE]
proof (prove)
using this:
local.map_of (snd (run_state (lookup k) m1)) \<subseteq>\<^sub>m local.map_of m1
local.map_of (snd (run_state (lookup k) m2)) \<subseteq>\<^sub>m local.map_of m2
run_state (lookup k) m1 = (v1, m1')
run_state (lookup k) m2 = (v2, m2')
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. local.map_of m1' \<subseteq>\<^sub>m local.map_of m1 &&& local.map_of m2' \<subseteq>\<^sub>m local.map_of m2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.map_of m1' \<subseteq>\<^sub>m local.map_of m1
local.map_of m2' \<subseteq>\<^sub>m local.map_of m2

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from inv_pair_domD[OF assms(3)]
[PROOF STATE]
proof (chain)
picking this:
dom (local.map_of m1) \<inter> dom (local.map_of m2) = {}
[PROOF STEP]
have 1: "dom (map_of m1') \<inter> dom (map_of m2) = {}"
[PROOF STATE]
proof (prove)
using this:
dom (local.map_of m1) \<inter> dom (local.map_of m2) = {}

goal (1 subgoal):
 1. dom (local.map_of m1') \<inter> dom (local.map_of m2) = {}
[PROOF STEP]
by (metis (no_types) \<open>map_of m1' \<subseteq>\<^sub>m map_of m1\<close> disjoint_iff_not_equal domIff map_le_def)
[PROOF STATE]
proof (state)
this:
dom (local.map_of m1') \<inter> dom (local.map_of m2) = {}

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have inv1: "inv_pair (Pair_Storage (key k) k2 m1' m2)" if "k2 \<noteq> key k" "k1 = key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_pair (Pair_Storage (key k) k2 m1' m2)
[PROOF STEP]
using that \<open>P m1\<close> \<open>P m2\<close>
[PROOF STATE]
proof (prove)
using this:
k2 \<noteq> key k
k1 = key k
P m1
P m2

goal (1 subgoal):
 1. inv_pair (Pair_Storage (key k) k2 m1' m2)
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
k2 \<noteq> key k
k1 = key k
P m1
P m2

goal (1 subgoal):
 1. case Pair_Storage (key k) k2 m1' m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> key ` dom (local.map_of m1') \<subseteq> {key k} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> P m1'
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa y. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key xa \<notin> {}; local.map_of m1' xa = Some y\<rbrakk> \<Longrightarrow> key xa = key k
 2. \<And>x xa y. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key xa \<notin> {}; local.map_of m2 xa = Some y\<rbrakk> \<Longrightarrow> key xa = k2
 3. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m1'
[PROOF STEP]
subgoal for x' y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m1' y = Some y_\<rbrakk> \<Longrightarrow> key y = key k
[PROOF STEP]
using assms(1,3) lookup_correct[OF \<open>P m1\<close>, of k, THEN map_le_implies_dom_le]
[PROOF STATE]
proof (prove)
using this:
run_state (lookup k) m1 = (v1, m1')
inv_pair (Pair_Storage k1 k2 m1 m2)
dom (local.map_of (snd (run_state (lookup k) m1))) \<subseteq> dom (local.map_of m1)

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m1' y = Some y_\<rbrakk> \<Longrightarrow> key y = key k
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
run_state (lookup k) m1 = (v1, m1')
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2
dom (local.map_of (snd (run_state (lookup k) m1))) \<subseteq> dom (local.map_of m1)

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m1' y = Some y_\<rbrakk> \<Longrightarrow> key y = key k
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key xa \<notin> {}; local.map_of m2 xa = Some y\<rbrakk> \<Longrightarrow> key xa = k2
 2. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m1'
[PROOF STEP]
subgoal for x' y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m2 y = Some y_\<rbrakk> \<Longrightarrow> key y = k2
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m2 y = Some y_\<rbrakk> \<Longrightarrow> key y = k2
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m2 y = Some y_\<rbrakk> \<Longrightarrow> key y = k2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m1'
[PROOF STEP]
using lookup_inv[of k] assms
[PROOF STATE]
proof (prove)
using this:
lift_p P (lookup k)
run_state (lookup k) m1 = (v1, m1')
run_state (lookup k) m2 = (v2, m2')
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m1'
[PROOF STEP]
unfolding lift_p_def
[PROOF STATE]
proof (prove)
using this:
\<forall>heap. P heap \<longrightarrow> (case run_state (lookup k) heap of (x, xa) \<Rightarrow> P xa)
run_state (lookup k) m1 = (v1, m1')
run_state (lookup k) m2 = (v2, m2')
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m1'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 \<noteq> key k; k1 = key k\<rbrakk> \<Longrightarrow> inv_pair (Pair_Storage (key k) k2 m1' m2)

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have inv2: "inv_pair (Pair_Storage k1 (key k) m1 m2')" if "k2 = key k" "k1 \<noteq> key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_pair (Pair_Storage k1 (key k) m1 m2')
[PROOF STEP]
using that \<open>P m1\<close> \<open>P m2\<close>
[PROOF STATE]
proof (prove)
using this:
k2 = key k
k1 \<noteq> key k
P m1
P m2

goal (1 subgoal):
 1. inv_pair (Pair_Storage k1 (key k) m1 m2')
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
k2 = key k
k1 \<noteq> key k
P m1
P m2

goal (1 subgoal):
 1. case Pair_Storage k1 (key k) m1 m2' of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2') \<subseteq> {key k} \<and> P m2'
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa y. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key xa \<notin> {}; local.map_of m1 xa = Some y\<rbrakk> \<Longrightarrow> key xa = k1
 2. \<And>x xa y. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key xa \<notin> {}; local.map_of m2' xa = Some y\<rbrakk> \<Longrightarrow> key xa = key k
 3. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m2'
[PROOF STEP]
subgoal for x' y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key y \<notin> {}; local.map_of m1 y = Some y_\<rbrakk> \<Longrightarrow> key y = k1
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key y \<notin> {}; local.map_of m1 y = Some y_\<rbrakk> \<Longrightarrow> key y = k1
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key y \<notin> {}; local.map_of m1 y = Some y_\<rbrakk> \<Longrightarrow> key y = k1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key xa \<notin> {}; local.map_of m2' xa = Some y\<rbrakk> \<Longrightarrow> key xa = key k
 2. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m2'
[PROOF STEP]
subgoal for x x' y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key x' \<notin> {}; local.map_of m2' x' = Some y\<rbrakk> \<Longrightarrow> key x' = key k
[PROOF STEP]
using assms(2,3) lookup_correct[OF \<open>P m2\<close>, of k, THEN map_le_implies_dom_le]
[PROOF STATE]
proof (prove)
using this:
run_state (lookup k) m2 = (v2, m2')
inv_pair (Pair_Storage k1 k2 m1 m2)
dom (local.map_of (snd (run_state (lookup k) m2))) \<subseteq> dom (local.map_of m2)

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key x' \<notin> {}; local.map_of m2' x' = Some y\<rbrakk> \<Longrightarrow> key x' = key k
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
run_state (lookup k) m2 = (v2, m2')
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2
dom (local.map_of (snd (run_state (lookup k) m2))) \<subseteq> dom (local.map_of m2)

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key x' \<notin> {}; local.map_of m2' x' = Some y\<rbrakk> \<Longrightarrow> key x' = key k
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m2'
[PROOF STEP]
using lookup_inv[of k] assms
[PROOF STATE]
proof (prove)
using this:
lift_p P (lookup k)
run_state (lookup k) m1 = (v1, m1')
run_state (lookup k) m2 = (v2, m2')
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m2'
[PROOF STEP]
unfolding lift_p_def
[PROOF STATE]
proof (prove)
using this:
\<forall>heap. P heap \<longrightarrow> (case run_state (lookup k) heap of (x, xa) \<Rightarrow> P xa)
run_state (lookup k) m1 = (v1, m1')
run_state (lookup k) m2 = (v2, m2')
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m2'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 = key k; k1 \<noteq> key k\<rbrakk> \<Longrightarrow> inv_pair (Pair_Storage k1 (key k) m1 m2')

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have A:
      "pair.map_of (Pair_Storage (key k) k2 m1' m2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) k2 m1 m2)"
      if "k2 \<noteq> key k" "k1 = key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.map_of (Pair_Storage (key k) k2 m1' m2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) k2 m1 m2)
[PROOF STEP]
using inv1 assms(3) 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k2 \<noteq> key k; k1 = key k\<rbrakk> \<Longrightarrow> inv_pair (Pair_Storage (key k) k2 m1' m2)
inv_pair (Pair_Storage k1 k2 m1 m2)
dom (local.map_of m1') \<inter> dom (local.map_of m2) = {}

goal (1 subgoal):
 1. pair.map_of (Pair_Storage (key k) k2 m1' m2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) k2 m1 m2)
[PROOF STEP]
by (auto intro: map_add_mono map_le_refl simp: that map_of_eq_pair[symmetric])
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 \<noteq> key k; k1 = key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) k2 m1' m2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) k2 m1 m2)

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have B:
      "pair.map_of (Pair_Storage k1 (key k) m1 m2') \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 (key k) m1 m2)"
      if "k2 = key k" "k1 \<noteq> key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.map_of (Pair_Storage k1 (key k) m1 m2') \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 (key k) m1 m2)
[PROOF STEP]
using inv2 assms(3) that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k2 = key k; k1 \<noteq> key k\<rbrakk> \<Longrightarrow> inv_pair (Pair_Storage k1 (key k) m1 m2')
inv_pair (Pair_Storage k1 k2 m1 m2)
k2 = key k
k1 \<noteq> key k

goal (1 subgoal):
 1. pair.map_of (Pair_Storage k1 (key k) m1 m2') \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 (key k) m1 m2)
[PROOF STEP]
by (auto intro: map_add_mono map_le_refl simp: map_of_eq_pair[symmetric] dest: inv_pair_domD)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 = key k; k1 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage k1 (key k) m1 m2') \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 (key k) m1 m2)

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
note A B
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 \<noteq> key k; k1 = key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) k2 m1' m2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) k2 m1 m2)
\<lbrakk>k2 = key k; k1 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage k1 (key k) m1 m2') \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 (key k) m1 m2)

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>run_state (lookup k) ?m1.2 = (?v1.2, ?m1'2); run_state (lookup k) ?m2.2 = (?v2.2, ?m2'2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 \<noteq> key k; ?k1.2 = key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) ?k2.2 ?m1'2 ?m2.2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) ?k2.2 ?m1.2 ?m2.2)
\<lbrakk>run_state (lookup k) ?m1.2 = (?v1.2, ?m1'2); run_state (lookup k) ?m2.2 = (?v2.2, ?m2'2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 = key k; ?k1.2 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2'2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2.2)

goal (2 subgoals):
 1. \<And>m k. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
with \<open>inv_pair m\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_pair m
\<lbrakk>run_state (lookup k) ?m1.2 = (?v1.2, ?m1'2); run_state (lookup k) ?m2.2 = (?v2.2, ?m2'2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 \<noteq> key k; ?k1.2 = key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) ?k2.2 ?m1'2 ?m2.2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) ?k2.2 ?m1.2 ?m2.2)
\<lbrakk>run_state (lookup k) ?m1.2 = (?v1.2, ?m1'2); run_state (lookup k) ?m2.2 = (?v2.2, ?m2'2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 = key k; ?k1.2 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2'2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2.2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
inv_pair m
\<lbrakk>run_state (lookup k) ?m1.2 = (?v1.2, ?m1'2); run_state (lookup k) ?m2.2 = (?v2.2, ?m2'2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 \<noteq> key k; ?k1.2 = key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) ?k2.2 ?m1'2 ?m2.2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) ?k2.2 ?m1.2 ?m2.2)
\<lbrakk>run_state (lookup k) ?m1.2 = (?v1.2, ?m1'2); run_state (lookup k) ?m2.2 = (?v2.2, ?m2'2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 = key k; ?k1.2 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2'2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2.2)

goal (1 subgoal):
 1. pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m
[PROOF STEP]
by (auto split: pair_storage.split if_split prod.split simp: Let_def lookup_pair_def)
[PROOF STATE]
proof (state)
this:
pair.map_of (snd (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m pair.map_of m

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
case (4 m k v)
[PROOF STATE]
proof (state)
this:
inv_pair m

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
inv_pair m

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
fix m1 v1 m1' m2 v2 m2' m3 k1 k2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
assume assms:
      "State_Monad.run_state (update k v) m1 = ((), m1')" "State_Monad.run_state (update k v) m2 = ((), m2')"
      "State_Monad.run_state (update k v) empty = ((), m3)"
      "inv_pair (Pair_Storage k1 k2 m1 m2)"
[PROOF STATE]
proof (state)
this:
run_state (update k v) m1 = ((), m1')
run_state (update k v) m2 = ((), m2')
run_state (update k v) empty = ((), m3)
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
run_state (update k v) m1 = ((), m1')
run_state (update k v) m2 = ((), m2')
run_state (update k v) empty = ((), m3)
inv_pair (Pair_Storage k1 k2 m1 m2)
[PROOF STEP]
have "P m1" "P m2"
[PROOF STATE]
proof (prove)
using this:
run_state (update k v) m1 = ((), m1')
run_state (update k v) m2 = ((), m2')
run_state (update k v) empty = ((), m3)
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. P m1 &&& P m2
[PROOF STEP]
by (auto intro: inv_pair_P_D1 inv_pair_P_D2)
[PROOF STATE]
proof (state)
this:
P m1
P m2

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from assms(3) P_empty update_inv[of k v]
[PROOF STATE]
proof (chain)
picking this:
run_state (update k v) empty = ((), m3)
P empty
lift_p P (update k v)
[PROOF STEP]
have "P m3"
[PROOF STATE]
proof (prove)
using this:
run_state (update k v) empty = ((), m3)
P empty
lift_p P (update k v)

goal (1 subgoal):
 1. P m3
[PROOF STEP]
unfolding lift_p_def
[PROOF STATE]
proof (prove)
using this:
run_state (update k v) empty = ((), m3)
P empty
\<forall>heap. P heap \<longrightarrow> (case run_state (update k v) heap of (x, xa) \<Rightarrow> P xa)

goal (1 subgoal):
 1. P m3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P m3

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have [intro]: "map_of m1' \<subseteq>\<^sub>m map_of m1(k \<mapsto> v)" "map_of m2' \<subseteq>\<^sub>m map_of m2(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.map_of m1' \<subseteq>\<^sub>m local.map_of m1(k \<mapsto> v) &&& local.map_of m2' \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)
[PROOF STEP]
using update_correct[OF \<open>P m1\<close>, of k v] update_correct[OF \<open>P m2\<close>, of k v] assms
[PROOF STATE]
proof (prove)
using this:
local.map_of (snd (run_state (update k v) m1)) \<subseteq>\<^sub>m local.map_of m1(k \<mapsto> v)
local.map_of (snd (run_state (update k v) m2)) \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)
run_state (update k v) m1 = ((), m1')
run_state (update k v) m2 = ((), m2')
run_state (update k v) empty = ((), m3)
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. local.map_of m1' \<subseteq>\<^sub>m local.map_of m1(k \<mapsto> v) &&& local.map_of m2' \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.map_of m1' \<subseteq>\<^sub>m local.map_of m1(k \<mapsto> v)
local.map_of m2' \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have "map_of m3 \<subseteq>\<^sub>m map_of empty(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.map_of m3 \<subseteq>\<^sub>m local.map_of empty(k \<mapsto> v)
[PROOF STEP]
using assms(3) update_correct[OF P_empty, of k v]
[PROOF STATE]
proof (prove)
using this:
run_state (update k v) empty = ((), m3)
local.map_of (snd (run_state (update k v) empty)) \<subseteq>\<^sub>m local.map_of empty(k \<mapsto> v)

goal (1 subgoal):
 1. local.map_of m3 \<subseteq>\<^sub>m local.map_of empty(k \<mapsto> v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.map_of m3 \<subseteq>\<^sub>m local.map_of empty(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.map_of m3 \<subseteq>\<^sub>m local.map_of empty(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have "\<dots> \<subseteq>\<^sub>m map_of m2(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.map_of empty(k \<mapsto> v) \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)
[PROOF STEP]
using empty_correct
[PROOF STATE]
proof (prove)
using this:
local.map_of empty \<subseteq>\<^sub>m Map.empty

goal (1 subgoal):
 1. local.map_of empty(k \<mapsto> v) \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)
[PROOF STEP]
by (auto elim: map_le_trans intro!: map_le_upd)
[PROOF STATE]
proof (state)
this:
local.map_of empty(k \<mapsto> v) \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
local.map_of m3 \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)
[PROOF STEP]
have "map_of m3 \<subseteq>\<^sub>m map_of m2(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
using this:
local.map_of m3 \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)

goal (1 subgoal):
 1. local.map_of m3 \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
local.map_of m3 \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have 1: "dom (map_of m1) \<inter> dom (map_of m2(k \<mapsto> v)) = {}" if "k1 \<noteq> key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (local.map_of m1) \<inter> dom (local.map_of m2(k \<mapsto> v)) = {}
[PROOF STEP]
using assms(4) that
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)
k1 \<noteq> key k

goal (1 subgoal):
 1. dom (local.map_of m1) \<inter> dom (local.map_of m2(k \<mapsto> v)) = {}
[PROOF STEP]
by (force simp: inv_pair_def)
[PROOF STATE]
proof (state)
this:
k1 \<noteq> key k \<Longrightarrow> dom (local.map_of m1) \<inter> dom (local.map_of m2(k \<mapsto> v)) = {}

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have 2: "dom (map_of m3) \<inter> dom (map_of m1) = {}" if "k1 \<noteq> key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (local.map_of m3) \<inter> dom (local.map_of m1) = {}
[PROOF STEP]
using \<open>local.map_of m3 \<subseteq>\<^sub>m local.map_of empty(k \<mapsto> v)\<close> assms(4) that
[PROOF STATE]
proof (prove)
using this:
local.map_of m3 \<subseteq>\<^sub>m local.map_of empty(k \<mapsto> v)
inv_pair (Pair_Storage k1 k2 m1 m2)
k1 \<noteq> key k

goal (1 subgoal):
 1. dom (local.map_of m3) \<inter> dom (local.map_of m1) = {}
[PROOF STEP]
by (fastforce dest!: map_le_implies_dom_le simp: inv_pair_def)
[PROOF STATE]
proof (state)
this:
k1 \<noteq> key k \<Longrightarrow> dom (local.map_of m3) \<inter> dom (local.map_of m1) = {}

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have inv: "inv_pair (Pair_Storage (key k) k1 m3 m1)" if "k2 \<noteq> key k" "k1 \<noteq> key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_pair (Pair_Storage (key k) k1 m3 m1)
[PROOF STEP]
using that \<open>P m1\<close> \<open>P m2\<close> \<open>P m3\<close>
[PROOF STATE]
proof (prove)
using this:
k2 \<noteq> key k
k1 \<noteq> key k
P m1
P m2
P m3

goal (1 subgoal):
 1. inv_pair (Pair_Storage (key k) k1 m3 m1)
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
k2 \<noteq> key k
k1 \<noteq> key k
P m1
P m2
P m3

goal (1 subgoal):
 1. case Pair_Storage (key k) k1 m3 m1 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k; P m1; P m2; P m3\<rbrakk> \<Longrightarrow> key ` dom (local.map_of m3) \<subseteq> {key k} \<and> key ` dom (local.map_of m1) \<subseteq> {k1}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y. \<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k; P m1; P m2; P m3; key xa \<notin> {}; local.map_of m3 xa = Some y\<rbrakk> \<Longrightarrow> key xa = key k
 2. \<And>x xa y. \<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k; P m1; P m2; P m3; key xa \<notin> {}; local.map_of m1 xa = Some y\<rbrakk> \<Longrightarrow> key xa = k1
[PROOF STEP]
subgoal for x x' y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k; P m1; P m2; P m3; key x' \<notin> {}; local.map_of m3 x' = Some y\<rbrakk> \<Longrightarrow> key x' = key k
[PROOF STEP]
using assms(3) update_correct[OF P_empty, of k v, THEN map_le_implies_dom_le]
          empty_correct
[PROOF STATE]
proof (prove)
using this:
run_state (update k v) empty = ((), m3)
dom (local.map_of (snd (run_state (update k v) empty))) \<subseteq> dom (local.map_of empty(k \<mapsto> v))
local.map_of empty \<subseteq>\<^sub>m Map.empty

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k; P m1; P m2; P m3; key x' \<notin> {}; local.map_of m3 x' = Some y\<rbrakk> \<Longrightarrow> key x' = key k
[PROOF STEP]
by (auto dest: map_le_implies_dom_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa y. \<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k; P m1; P m2; P m3; key xa \<notin> {}; local.map_of m1 xa = Some y\<rbrakk> \<Longrightarrow> key xa = k1
[PROOF STEP]
subgoal for x x' y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k; P m1; P m2; P m3; key x' \<notin> {}; local.map_of m1 x' = Some y\<rbrakk> \<Longrightarrow> key x' = k1
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k; P m1; P m2; P m3; key x' \<notin> {}; local.map_of m1 x' = Some y\<rbrakk> \<Longrightarrow> key x' = k1
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k; P m1; P m2; P m3; key x' \<notin> {}; local.map_of m1 x' = Some y\<rbrakk> \<Longrightarrow> key x' = k1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k\<rbrakk> \<Longrightarrow> inv_pair (Pair_Storage (key k) k1 m3 m1)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have A:
      "pair.map_of (Pair_Storage (key k) k1 m3 m1) \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 k2 m1 m2)(k \<mapsto> v)"
      if "k2 \<noteq> key k" "k1 \<noteq> key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.map_of (Pair_Storage (key k) k1 m3 m1) \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 k2 m1 m2)(k \<mapsto> v)
[PROOF STEP]
using inv assms(4) \<open>map_of m3 \<subseteq>\<^sub>m map_of m2(k \<mapsto> v)\<close> 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k\<rbrakk> \<Longrightarrow> inv_pair (Pair_Storage (key k) k1 m3 m1)
inv_pair (Pair_Storage k1 k2 m1 m2)
local.map_of m3 \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v)
k1 \<noteq> key k \<Longrightarrow> dom (local.map_of m1) \<inter> dom (local.map_of m2(k \<mapsto> v)) = {}

goal (1 subgoal):
 1. pair.map_of (Pair_Storage (key k) k1 m3 m1) \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 k2 m1 m2)(k \<mapsto> v)
[PROOF STEP]
apply (simp add: that map_of_eq_pair[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inv_pair (Pair_Storage (key k) k1 m3 m1); inv_pair (Pair_Storage k1 k2 m1 m2); local.map_of m3 \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v); k \<notin> dom (local.map_of m1) \<and> dom (local.map_of m1) \<inter> dom (local.map_of m2) = {}\<rbrakk> \<Longrightarrow> local.map_of m3 ++ local.map_of m1 \<subseteq>\<^sub>m (local.map_of m1 ++ local.map_of m2)(k \<mapsto> v)
[PROOF STEP]
apply (subst map_add_upd[symmetric], subst Map.map_add_comm, rule 2, rule that)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inv_pair (Pair_Storage (key k) k1 m3 m1); inv_pair (Pair_Storage k1 k2 m1 m2); local.map_of m3 \<subseteq>\<^sub>m local.map_of m2(k \<mapsto> v); k \<notin> dom (local.map_of m1) \<and> dom (local.map_of m1) \<inter> dom (local.map_of m2) = {}\<rbrakk> \<Longrightarrow> local.map_of m1 ++ local.map_of m3 \<subseteq>\<^sub>m local.map_of m1 ++ local.map_of m2(k \<mapsto> v)
[PROOF STEP]
by (rule map_add_mono; auto)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) k1 m3 m1) \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 k2 m1 m2)(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have inv1: "inv_pair (Pair_Storage (key k) k2 m1' m2)" if "k2 \<noteq> key k" "k1 = key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_pair (Pair_Storage (key k) k2 m1' m2)
[PROOF STEP]
using that \<open>P m1\<close> \<open>P m2\<close>
[PROOF STATE]
proof (prove)
using this:
k2 \<noteq> key k
k1 = key k
P m1
P m2

goal (1 subgoal):
 1. inv_pair (Pair_Storage (key k) k2 m1' m2)
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
k2 \<noteq> key k
k1 = key k
P m1
P m2

goal (1 subgoal):
 1. case Pair_Storage (key k) k2 m1' m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> key ` dom (local.map_of m1') \<subseteq> {key k} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> P m1'
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa y. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key xa \<notin> {}; local.map_of m1' xa = Some y\<rbrakk> \<Longrightarrow> key xa = key k
 2. \<And>x xa y. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key xa \<notin> {}; local.map_of m2 xa = Some y\<rbrakk> \<Longrightarrow> key xa = k2
 3. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m1'
[PROOF STEP]
subgoal for x' y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m1' y = Some y_\<rbrakk> \<Longrightarrow> key y = key k
[PROOF STEP]
using assms(1,4) update_correct[OF \<open>P m1\<close>, of k v, THEN map_le_implies_dom_le]
[PROOF STATE]
proof (prove)
using this:
run_state (update k v) m1 = ((), m1')
inv_pair (Pair_Storage k1 k2 m1 m2)
dom (local.map_of (snd (run_state (update k v) m1))) \<subseteq> dom (local.map_of m1(k \<mapsto> v))

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m1' y = Some y_\<rbrakk> \<Longrightarrow> key y = key k
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
run_state (update k v) m1 = ((), m1')
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2
dom (local.map_of (snd (run_state (update k v) m1))) \<subseteq> dom (local.map_of m1(k \<mapsto> v))

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m1' y = Some y_\<rbrakk> \<Longrightarrow> key y = key k
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key xa \<notin> {}; local.map_of m2 xa = Some y\<rbrakk> \<Longrightarrow> key xa = k2
 2. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m1'
[PROOF STEP]
subgoal for x' y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m2 y = Some y_\<rbrakk> \<Longrightarrow> key y = k2
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m2 y = Some y_\<rbrakk> \<Longrightarrow> key y = k2
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2; key y \<notin> {}; local.map_of m2 y = Some y_\<rbrakk> \<Longrightarrow> key y = k2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m1'
[PROOF STEP]
using update_inv[of k v] assms
[PROOF STATE]
proof (prove)
using this:
lift_p P (update k v)
run_state (update k v) m1 = ((), m1')
run_state (update k v) m2 = ((), m2')
run_state (update k v) empty = ((), m3)
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m1'
[PROOF STEP]
unfolding lift_p_def
[PROOF STATE]
proof (prove)
using this:
\<forall>heap. P heap \<longrightarrow> (case run_state (update k v) heap of (x, xa) \<Rightarrow> P xa)
run_state (update k v) m1 = ((), m1')
run_state (update k v) m2 = ((), m2')
run_state (update k v) empty = ((), m3)
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 \<noteq> key k; k1 = key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m1'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 \<noteq> key k; k1 = key k\<rbrakk> \<Longrightarrow> inv_pair (Pair_Storage (key k) k2 m1' m2)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have inv2: "inv_pair (Pair_Storage k1 (key k) m1 m2')" if "k2 = key k" "k1 \<noteq> key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_pair (Pair_Storage k1 (key k) m1 m2')
[PROOF STEP]
using that \<open>P m1\<close> \<open>P m2\<close>
[PROOF STATE]
proof (prove)
using this:
k2 = key k
k1 \<noteq> key k
P m1
P m2

goal (1 subgoal):
 1. inv_pair (Pair_Storage k1 (key k) m1 m2')
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
k2 = key k
k1 \<noteq> key k
P m1
P m2

goal (1 subgoal):
 1. case Pair_Storage k1 (key k) m1 m2' of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2') \<subseteq> {key k} \<and> P m2'
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa y. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key xa \<notin> {}; local.map_of m1 xa = Some y\<rbrakk> \<Longrightarrow> key xa = k1
 2. \<And>x xa y. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key xa \<notin> {}; local.map_of m2' xa = Some y\<rbrakk> \<Longrightarrow> key xa = key k
 3. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m2'
[PROOF STEP]
subgoal for x' y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key y \<notin> {}; local.map_of m1 y = Some y_\<rbrakk> \<Longrightarrow> key y = k1
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key y \<notin> {}; local.map_of m1 y = Some y_\<rbrakk> \<Longrightarrow> key y = k1
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key y \<notin> {}; local.map_of m1 y = Some y_\<rbrakk> \<Longrightarrow> key y = k1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key xa \<notin> {}; local.map_of m2' xa = Some y\<rbrakk> \<Longrightarrow> key xa = key k
 2. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m2'
[PROOF STEP]
subgoal for x x' y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key x' \<notin> {}; local.map_of m2' x' = Some y\<rbrakk> \<Longrightarrow> key x' = key k
[PROOF STEP]
using assms(2,4) update_correct[OF \<open>P m2\<close>, of k v, THEN map_le_implies_dom_le]
[PROOF STATE]
proof (prove)
using this:
run_state (update k v) m2 = ((), m2')
inv_pair (Pair_Storage k1 k2 m1 m2)
dom (local.map_of (snd (run_state (update k v) m2))) \<subseteq> dom (local.map_of m2(k \<mapsto> v))

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key x' \<notin> {}; local.map_of m2' x' = Some y\<rbrakk> \<Longrightarrow> key x' = key k
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
run_state (update k v) m2 = ((), m2')
case Pair_Storage k1 k2 m1 m2 of Pair_Storage k1 k2 m1 m2 \<Rightarrow> key ` dom (local.map_of m1) \<subseteq> {k1} \<and> key ` dom (local.map_of m2) \<subseteq> {k2} \<and> k1 \<noteq> k2 \<and> P m1 \<and> P m2
dom (local.map_of (snd (run_state (update k v) m2))) \<subseteq> dom (local.map_of m2(k \<mapsto> v))

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2; key x' \<notin> {}; local.map_of m2' x' = Some y\<rbrakk> \<Longrightarrow> key x' = key k
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m2'
[PROOF STEP]
using update_inv[of k v] assms
[PROOF STATE]
proof (prove)
using this:
lift_p P (update k v)
run_state (update k v) m1 = ((), m1')
run_state (update k v) m2 = ((), m2')
run_state (update k v) empty = ((), m3)
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m2'
[PROOF STEP]
unfolding lift_p_def
[PROOF STATE]
proof (prove)
using this:
\<forall>heap. P heap \<longrightarrow> (case run_state (update k v) heap of (x, xa) \<Rightarrow> P xa)
run_state (update k v) m1 = ((), m1')
run_state (update k v) m2 = ((), m2')
run_state (update k v) empty = ((), m3)
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. \<lbrakk>k2 = key k; k1 \<noteq> key k; P m1; P m2\<rbrakk> \<Longrightarrow> P m2'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 = key k; k1 \<noteq> key k\<rbrakk> \<Longrightarrow> inv_pair (Pair_Storage k1 (key k) m1 m2')

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have C:
      "pair.map_of (Pair_Storage (key k) k2 m1' m2) \<subseteq>\<^sub>m
       pair.map_of (Pair_Storage (key k) k2 m1 m2)(k \<mapsto> v)"
      if "k2 \<noteq> key k" "k1 = key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.map_of (Pair_Storage (key k) k2 m1' m2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) k2 m1 m2)(k \<mapsto> v)
[PROOF STEP]
using inv1[OF that] assms(4) \<open>inv_pair m\<close>
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage (key k) k2 m1' m2)
inv_pair (Pair_Storage k1 k2 m1 m2)
inv_pair m

goal (1 subgoal):
 1. pair.map_of (Pair_Storage (key k) k2 m1' m2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) k2 m1 m2)(k \<mapsto> v)
[PROOF STEP]
by (simp add: that map_of_eq_pair[symmetric])
         (subst map_add_upd2[symmetric]; force simp: inv_pair_def intro: map_add_mono map_le_refl)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 \<noteq> key k; k1 = key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) k2 m1' m2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) k2 m1 m2)(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have B:
      "pair.map_of (Pair_Storage k1 (key k) m1 m2') \<subseteq>\<^sub>m
       pair.map_of (Pair_Storage k1 (key k) m1 m2)(k \<mapsto> v)"
      if "k2 = key k" "k1 \<noteq> key k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.map_of (Pair_Storage k1 (key k) m1 m2') \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 (key k) m1 m2)(k \<mapsto> v)
[PROOF STEP]
using inv2[OF that] assms(4)
[PROOF STATE]
proof (prove)
using this:
inv_pair (Pair_Storage k1 (key k) m1 m2')
inv_pair (Pair_Storage k1 k2 m1 m2)

goal (1 subgoal):
 1. pair.map_of (Pair_Storage k1 (key k) m1 m2') \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 (key k) m1 m2)(k \<mapsto> v)
[PROOF STEP]
by (simp add: that map_of_eq_pair[symmetric])
         (subst map_add_upd[symmetric]; rule map_add_mono; force simp: inv_pair_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 = key k; k1 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage k1 (key k) m1 m2') \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 (key k) m1 m2)(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
note A B C
[PROOF STATE]
proof (state)
this:
\<lbrakk>k2 \<noteq> key k; k1 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) k1 m3 m1) \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 k2 m1 m2)(k \<mapsto> v)
\<lbrakk>k2 = key k; k1 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage k1 (key k) m1 m2') \<subseteq>\<^sub>m pair.map_of (Pair_Storage k1 (key k) m1 m2)(k \<mapsto> v)
\<lbrakk>k2 \<noteq> key k; k1 = key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) k2 m1' m2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) k2 m1 m2)(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>run_state (update k v) ?m1.2 = ((), ?m1'2); run_state (update k v) ?m2.2 = ((), ?m2'2); run_state (update k v) empty = ((), ?m3.2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 \<noteq> key k; ?k1.2 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) ?k1.2 ?m3.2 ?m1.2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2)(k \<mapsto> v)
\<lbrakk>run_state (update k v) ?m1.2 = ((), ?m1'2); run_state (update k v) ?m2.2 = ((), ?m2'2); run_state (update k v) empty = ((), ?m3.2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 = key k; ?k1.2 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2'2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2.2)(k \<mapsto> v)
\<lbrakk>run_state (update k v) ?m1.2 = ((), ?m1'2); run_state (update k v) ?m2.2 = ((), ?m2'2); run_state (update k v) empty = ((), ?m3.2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 \<noteq> key k; ?k1.2 = key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) ?k2.2 ?m1'2 ?m2.2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) ?k2.2 ?m1.2 ?m2.2)(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>m k v. inv_pair m \<Longrightarrow> pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
with \<open>inv_pair m\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_pair m
\<lbrakk>run_state (update k v) ?m1.2 = ((), ?m1'2); run_state (update k v) ?m2.2 = ((), ?m2'2); run_state (update k v) empty = ((), ?m3.2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 \<noteq> key k; ?k1.2 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) ?k1.2 ?m3.2 ?m1.2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2)(k \<mapsto> v)
\<lbrakk>run_state (update k v) ?m1.2 = ((), ?m1'2); run_state (update k v) ?m2.2 = ((), ?m2'2); run_state (update k v) empty = ((), ?m3.2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 = key k; ?k1.2 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2'2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2.2)(k \<mapsto> v)
\<lbrakk>run_state (update k v) ?m1.2 = ((), ?m1'2); run_state (update k v) ?m2.2 = ((), ?m2'2); run_state (update k v) empty = ((), ?m3.2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 \<noteq> key k; ?k1.2 = key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) ?k2.2 ?m1'2 ?m2.2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) ?k2.2 ?m1.2 ?m2.2)(k \<mapsto> v)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
inv_pair m
\<lbrakk>run_state (update k v) ?m1.2 = ((), ?m1'2); run_state (update k v) ?m2.2 = ((), ?m2'2); run_state (update k v) empty = ((), ?m3.2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 \<noteq> key k; ?k1.2 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) ?k1.2 ?m3.2 ?m1.2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2)(k \<mapsto> v)
\<lbrakk>run_state (update k v) ?m1.2 = ((), ?m1'2); run_state (update k v) ?m2.2 = ((), ?m2'2); run_state (update k v) empty = ((), ?m3.2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 = key k; ?k1.2 \<noteq> key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2'2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage ?k1.2 (key k) ?m1.2 ?m2.2)(k \<mapsto> v)
\<lbrakk>run_state (update k v) ?m1.2 = ((), ?m1'2); run_state (update k v) ?m2.2 = ((), ?m2'2); run_state (update k v) empty = ((), ?m3.2); inv_pair (Pair_Storage ?k1.2 ?k2.2 ?m1.2 ?m2.2); ?k2.2 \<noteq> key k; ?k1.2 = key k\<rbrakk> \<Longrightarrow> pair.map_of (Pair_Storage (key k) ?k2.2 ?m1'2 ?m2.2) \<subseteq>\<^sub>m pair.map_of (Pair_Storage (key k) ?k2.2 ?m1.2 ?m2.2)(k \<mapsto> v)

goal (1 subgoal):
 1. pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
by (auto split: pair_storage.split if_split prod.split simp: Let_def update_pair_def)
[PROOF STATE]
proof (state)
this:
pair.map_of (snd (run_state (update_pair k v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nprv_hyp[simp,intro]:
"\<phi> \<in> F \<Longrightarrow> F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> nprv F \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> F; F \<subseteq> fmla; finite F\<rbrakk> \<Longrightarrow> nprv F \<phi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<phi> \<in> F; F \<subseteq> fmla; finite F\<rbrakk> \<Longrightarrow> prv (imp (scnj F) \<phi>)
[PROOF STEP]
by (simp add: prv_scnj_imp_in subset_iff)


[STATEMENT]
lemma prv_nprv0I: "prv \<phi> \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> nprv {} \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv \<phi>; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {} \<phi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv \<phi>; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj {}) \<phi>)
[PROOF STEP]
by (simp add: prv_imp_triv)


[STATEMENT]
lemma prv_nprv_emp: "\<phi> \<in> fmla \<Longrightarrow> prv \<phi> \<longleftrightarrow> nprv {} \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv \<phi> = nprv {} \<phi>
[PROOF STEP]
using prv_nprv0I
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prv ?\<phi>; ?\<phi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {} ?\<phi>

goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv \<phi> = nprv {} \<phi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prv ?\<phi>; ?\<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv (imp (scnj {}) ?\<phi>)

goal (1 subgoal):
 1. \<phi> \<in> fmla \<Longrightarrow> prv \<phi> = prv (imp (scnj {}) \<phi>)
[PROOF STEP]
by (metis asList eqv finite.simps insert_not_empty lcnj.simps(1) ldsj.cases
  list.simps(15) prv_eqvI prv_imp_mp prv_imp_tru scnj_def tru)


[STATEMENT]
lemma nprv_mono:
assumes "nprv G \<phi>"
and "F \<subseteq> fmla" "finite F" "G \<subseteq> F" "\<phi> \<in> fmla"
shows "nprv F \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<phi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nprv G \<phi>
F \<subseteq> fmla
finite F
G \<subseteq> F
\<phi> \<in> fmla

goal (1 subgoal):
 1. nprv F \<phi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
using this:
prv (imp (scnj G) \<phi>)
F \<subseteq> fmla
finite F
G \<subseteq> F
\<phi> \<in> fmla

goal (1 subgoal):
 1. prv (imp (scnj F) \<phi>)
[PROOF STEP]
by (meson order_trans prv_prv_imp_trans prv_scnj_mono rev_finite_subset scnj)


[STATEMENT]
lemma nprv_cut:
assumes "nprv F \<phi>" and "nprv (insert \<phi> F) \<psi>"
and "F \<subseteq> fmla" "finite F"  "\<phi> \<in> fmla"  "\<psi> \<in> fmla"
shows "nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
nprv F \<phi>
nprv (insert \<phi> F) \<psi>
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
\<psi> \<in> fmla

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
using this:
prv (imp (scnj F) \<phi>)
prv (imp (scnj (insert \<phi> F)) \<psi>)
F \<subseteq> fmla
finite F
\<phi> \<in> fmla
\<psi> \<in> fmla

goal (1 subgoal):
 1. prv (imp (scnj F) \<psi>)
[PROOF STEP]
by (metis (full_types) cnj finite.insertI
  insert_subset prv_imp_cnj prv_imp_cnj_scnj prv_imp_refl prv_prv_imp_trans scnj)


[STATEMENT]
lemma nprv_strong_cut2:
"nprv F \<phi>1 \<Longrightarrow> nprv (insert \<phi>1 F) \<phi>2 \<Longrightarrow> nprv (insert \<phi>2 (insert \<phi>1 F)) \<psi> \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F \<phi>1; nprv (insert \<phi>1 F) \<phi>2; nprv (insert \<phi>2 (insert \<phi>1 F)) \<psi>; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F \<psi>
[PROOF STEP]
by (meson finite.insertI insert_subsetI nprv_cut)


[STATEMENT]
lemma nprv_cut2:
"nprv F \<phi>1 \<Longrightarrow> nprv F \<phi>2 \<Longrightarrow>
 F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv (insert \<phi>2 (insert \<phi>1 F)) \<psi> \<Longrightarrow> nprv F \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv F \<phi>1; nprv F \<phi>2; F \<subseteq> fmla; finite F; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla; nprv (insert \<phi>2 (insert \<phi>1 F)) \<psi>\<rbrakk> \<Longrightarrow> nprv F \<psi>
[PROOF STEP]
by (meson finite.insertI insert_subsetI nprv_mono nprv_strong_cut2 subset_insertI)


[STATEMENT]
lemma nprv_insertShiftI:
"nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi> \<Longrightarrow> nprv (insert \<phi>2 (insert \<phi>1 F)) \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv (insert \<phi>1 (insert \<phi>2 F)) \<psi> \<Longrightarrow> nprv (insert \<phi>2 (insert \<phi>1 F)) \<psi>
[PROOF STEP]
by (simp add: insert_commute)


[STATEMENT]
lemma nprv_insertShift2I:
"nprv (insert \<phi>3 (insert \<phi>1 (insert \<phi>2 F))) \<psi> \<Longrightarrow> nprv (insert \<phi>1 (insert \<phi>2 (insert \<phi>3 F))) \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv (insert \<phi>3 (insert \<phi>1 (insert \<phi>2 F))) \<psi> \<Longrightarrow> nprv (insert \<phi>1 (insert \<phi>2 (insert \<phi>3 F))) \<psi>
[PROOF STEP]
by (simp add: insert_commute)


[STATEMENT]
lemma prv_nprvI: "prv \<phi> \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> nprv F \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prv \<phi>; \<phi> \<in> fmla; F \<subseteq> fmla; finite F\<rbrakk> \<Longrightarrow> nprv F \<phi>
[PROOF STEP]
using prv_nprv0I
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prv ?\<phi>; ?\<phi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {} ?\<phi>

goal (1 subgoal):
 1. \<lbrakk>prv \<phi>; \<phi> \<in> fmla; F \<subseteq> fmla; finite F\<rbrakk> \<Longrightarrow> nprv F \<phi>
[PROOF STEP]
by (simp add: nprv_def prv_imp_triv)


[STATEMENT]
lemma prv_nprv1I:
assumes "\<phi> \<in> fmla" "\<psi> \<in> fmla" and "prv (imp \<phi> \<psi>)"
shows "nprv {\<phi>} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {\<phi>} \<psi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<psi> \<in> fmla
prv (imp \<phi> \<psi>)

goal (1 subgoal):
 1. nprv {\<phi>} \<psi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
\<psi> \<in> fmla
prv (imp \<phi> \<psi>)

goal (1 subgoal):
 1. prv (imp (scnj {\<phi>}) \<psi>)
[PROOF STEP]
by (simp add: prv_scnj_imp)


[STATEMENT]
lemma prv_nprv2I:
assumes "prv (imp \<phi>1 (imp \<phi>2 \<psi>))" "\<phi>1 \<in> fmla" "\<phi>2 \<in> fmla" "\<psi> \<in> fmla"
shows "nprv {\<phi>1,\<phi>2} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv {\<phi>1, \<phi>2} \<psi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi>1 (imp \<phi>2 \<psi>))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<psi> \<in> fmla

goal (1 subgoal):
 1. nprv {\<phi>1, \<phi>2} \<psi>
[PROOF STEP]
unfolding nprv_def
[PROOF STATE]
proof (prove)
using this:
prv (imp \<phi>1 (imp \<phi>2 \<psi>))
\<phi>1 \<in> fmla
\<phi>2 \<in> fmla
\<psi> \<in> fmla

goal (1 subgoal):
 1. prv (imp (scnj {\<phi>1, \<phi>2}) \<psi>)
[PROOF STEP]
by (meson cnj empty_subsetI finite.simps insert_subsetI prv_cnj_imp_monoR2 prv_prv_imp_trans prv_scnj2_imp_cnj scnj)


[STATEMENT]
lemma nprv_prvI: "nprv {} \<phi> \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> prv \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {} \<phi>; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv \<phi>
[PROOF STEP]
using prv_nprv_emp
[PROOF STATE]
proof (prove)
using this:
?\<phi> \<in> fmla \<Longrightarrow> prv ?\<phi> = nprv {} ?\<phi>

goal (1 subgoal):
 1. \<lbrakk>nprv {} \<phi>; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> prv \<phi>
[PROOF STEP]
by auto


[STATEMENT]
lemma nprv_clear: "nprv {} \<phi> \<Longrightarrow> F \<subseteq> fmla \<Longrightarrow> finite F \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> nprv F \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {} \<phi>; F \<subseteq> fmla; finite F; \<phi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv F \<phi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_cut_set:
assumes F:  "finite F" "F \<subseteq> fmla" and G: "finite G" "G \<subseteq> fmla" "\<chi> \<in> fmla"
and n1: "\<And> \<psi>. \<psi> \<in> G \<Longrightarrow> nprv F \<psi>" and n2: "nprv (G \<union> F) \<chi>"
shows "nprv F \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
using G F n1 n2
[PROOF STATE]
proof (prove)
using this:
finite G
G \<subseteq> fmla
\<chi> \<in> fmla
finite F
F \<subseteq> fmla
?\<psi> \<in> G \<Longrightarrow> nprv F ?\<psi>
nprv (G \<union> F) \<chi>

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
proof(induction arbitrary: F \<chi>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>F \<chi>. \<lbrakk>{} \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> {} \<Longrightarrow> nprv F \<psi>; nprv ({} \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv F \<chi>
 2. \<And>x F Fa \<chi>. \<lbrakk>finite F; x \<notin> F; \<And>Fa \<chi>. \<lbrakk>F \<subseteq> fmla; \<chi> \<in> fmla; finite Fa; Fa \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> F \<Longrightarrow> nprv Fa \<psi>; nprv (F \<union> Fa) \<chi>\<rbrakk> \<Longrightarrow> nprv Fa \<chi>; insert x F \<subseteq> fmla; \<chi> \<in> fmla; finite Fa; Fa \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> insert x F \<Longrightarrow> nprv Fa \<psi>; nprv (insert x F \<union> Fa) \<chi>\<rbrakk> \<Longrightarrow> nprv Fa \<chi>
[PROOF STEP]
case (insert \<psi> G F \<chi>)
[PROOF STATE]
proof (state)
this:
finite G
\<psi> \<notin> G
\<lbrakk>G \<subseteq> fmla; ?\<chi> \<in> fmla; finite ?F; ?F \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv ?F \<psi>; nprv (G \<union> ?F) ?\<chi>\<rbrakk> \<Longrightarrow> nprv ?F ?\<chi>
insert \<psi> G \<subseteq> fmla
\<chi> \<in> fmla
finite F
F \<subseteq> fmla
?\<psi> \<in> insert \<psi> G \<Longrightarrow> nprv F ?\<psi>
nprv (insert \<psi> G \<union> F) \<chi>

goal (2 subgoals):
 1. \<And>F \<chi>. \<lbrakk>{} \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> {} \<Longrightarrow> nprv F \<psi>; nprv ({} \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv F \<chi>
 2. \<And>x F Fa \<chi>. \<lbrakk>finite F; x \<notin> F; \<And>Fa \<chi>. \<lbrakk>F \<subseteq> fmla; \<chi> \<in> fmla; finite Fa; Fa \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> F \<Longrightarrow> nprv Fa \<psi>; nprv (F \<union> Fa) \<chi>\<rbrakk> \<Longrightarrow> nprv Fa \<chi>; insert x F \<subseteq> fmla; \<chi> \<in> fmla; finite Fa; Fa \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> insert x F \<Longrightarrow> nprv Fa \<psi>; nprv (insert x F \<union> Fa) \<chi>\<rbrakk> \<Longrightarrow> nprv Fa \<chi>
[PROOF STEP]
hence 0: "nprv F \<psi>"
[PROOF STATE]
proof (prove)
using this:
finite G
\<psi> \<notin> G
\<lbrakk>G \<subseteq> fmla; ?\<chi> \<in> fmla; finite ?F; ?F \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> G \<Longrightarrow> nprv ?F \<psi>; nprv (G \<union> ?F) ?\<chi>\<rbrakk> \<Longrightarrow> nprv ?F ?\<chi>
insert \<psi> G \<subseteq> fmla
\<chi> \<in> fmla
finite F
F \<subseteq> fmla
?\<psi> \<in> insert \<psi> G \<Longrightarrow> nprv F ?\<psi>
nprv (insert \<psi> G \<union> F) \<chi>

goal (1 subgoal):
 1. nprv F \<psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nprv F \<psi>

goal (2 subgoals):
 1. \<And>F \<chi>. \<lbrakk>{} \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> {} \<Longrightarrow> nprv F \<psi>; nprv ({} \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv F \<chi>
 2. \<And>x F Fa \<chi>. \<lbrakk>finite F; x \<notin> F; \<And>Fa \<chi>. \<lbrakk>F \<subseteq> fmla; \<chi> \<in> fmla; finite Fa; Fa \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> F \<Longrightarrow> nprv Fa \<psi>; nprv (F \<union> Fa) \<chi>\<rbrakk> \<Longrightarrow> nprv Fa \<chi>; insert x F \<subseteq> fmla; \<chi> \<in> fmla; finite Fa; Fa \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> insert x F \<Longrightarrow> nprv Fa \<psi>; nprv (insert x F \<union> Fa) \<chi>\<rbrakk> \<Longrightarrow> nprv Fa \<chi>
[PROOF STEP]
have 1: "nprv (insert \<psi> F) \<chi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv (insert \<psi> F) \<chi>
[PROOF STEP]
using insert.prems
[PROOF STATE]
proof (prove)
using this:
insert \<psi> G \<subseteq> fmla
\<chi> \<in> fmla
finite F
F \<subseteq> fmla
?\<psi> \<in> insert \<psi> G \<Longrightarrow> nprv F ?\<psi>
nprv (insert \<psi> G \<union> F) \<chi>

goal (1 subgoal):
 1. nprv (insert \<psi> F) \<chi>
[PROOF STEP]
apply-
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv (insert \<psi> F) \<chi>
[PROOF STEP]
apply(rule insert.IH)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
 2. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> \<chi> \<in> fmla
 3. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> finite (insert \<psi> F)
 4. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> insert \<psi> F \<subseteq> fmla
 5. \<And>\<psi>'. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>; \<psi>' \<in> G\<rbrakk> \<Longrightarrow> nprv (insert \<psi> F) \<psi>'
 6. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv (G \<union> insert \<psi> F) \<chi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> G \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> \<chi> \<in> fmla
 2. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> finite (insert \<psi> F)
 3. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> insert \<psi> F \<subseteq> fmla
 4. \<And>\<psi>'. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>; \<psi>' \<in> G\<rbrakk> \<Longrightarrow> nprv (insert \<psi> F) \<psi>'
 5. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv (G \<union> insert \<psi> F) \<chi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> \<chi> \<in> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> finite (insert \<psi> F)
 2. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> insert \<psi> F \<subseteq> fmla
 3. \<And>\<psi>'. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>; \<psi>' \<in> G\<rbrakk> \<Longrightarrow> nprv (insert \<psi> F) \<psi>'
 4. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv (G \<union> insert \<psi> F) \<chi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> finite (insert \<psi> F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> insert \<psi> F \<subseteq> fmla
 2. \<And>\<psi>'. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>; \<psi>' \<in> G\<rbrakk> \<Longrightarrow> nprv (insert \<psi> F) \<psi>'
 3. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv (G \<union> insert \<psi> F) \<chi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> insert \<psi> F \<subseteq> fmla
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<psi>'. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>; \<psi>' \<in> G\<rbrakk> \<Longrightarrow> nprv (insert \<psi> F) \<psi>'
 2. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv (G \<union> insert \<psi> F) \<chi>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>; \<psi>'_ \<in> G\<rbrakk> \<Longrightarrow> nprv (insert \<psi> F) \<psi>'_
[PROOF STEP]
by (meson finite.simps insert_subset nprv_mono subsetD subset_insertI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert \<psi> G \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>'. \<psi>' \<in> insert \<psi> G \<Longrightarrow> nprv F \<psi>'; nprv (insert \<psi> G \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv (G \<union> insert \<psi> F) \<chi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nprv (insert \<psi> F) \<chi>

goal (2 subgoals):
 1. \<And>F \<chi>. \<lbrakk>{} \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> {} \<Longrightarrow> nprv F \<psi>; nprv ({} \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv F \<chi>
 2. \<And>x F Fa \<chi>. \<lbrakk>finite F; x \<notin> F; \<And>Fa \<chi>. \<lbrakk>F \<subseteq> fmla; \<chi> \<in> fmla; finite Fa; Fa \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> F \<Longrightarrow> nprv Fa \<psi>; nprv (F \<union> Fa) \<chi>\<rbrakk> \<Longrightarrow> nprv Fa \<chi>; insert x F \<subseteq> fmla; \<chi> \<in> fmla; finite Fa; Fa \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> insert x F \<Longrightarrow> nprv Fa \<psi>; nprv (insert x F \<union> Fa) \<chi>\<rbrakk> \<Longrightarrow> nprv Fa \<chi>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
using insert.prems
[PROOF STATE]
proof (prove)
using this:
insert \<psi> G \<subseteq> fmla
\<chi> \<in> fmla
finite F
F \<subseteq> fmla
?\<psi> \<in> insert \<psi> G \<Longrightarrow> nprv F ?\<psi>
nprv (insert \<psi> G \<union> F) \<chi>

goal (1 subgoal):
 1. nprv F \<chi>
[PROOF STEP]
by (intro nprv_cut[OF 0 1]) auto
[PROOF STATE]
proof (state)
this:
nprv F \<chi>

goal (1 subgoal):
 1. \<And>F \<chi>. \<lbrakk>{} \<subseteq> fmla; \<chi> \<in> fmla; finite F; F \<subseteq> fmla; \<And>\<psi>. \<psi> \<in> {} \<Longrightarrow> nprv F \<psi>; nprv ({} \<union> F) \<chi>\<rbrakk> \<Longrightarrow> nprv F \<chi>
[PROOF STEP]
qed(insert nprv_clear, auto)


[STATEMENT]
lemma nprv_clear2_1:
"nprv {\<phi>2} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>2} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear2_2:
"nprv {\<phi>1} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>1} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear3_1:
"nprv {\<phi>2,\<phi>3} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>2, \<phi>3} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear3_2:
"nprv {\<phi>1,\<phi>3} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>1, \<phi>3} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear3_3:
"nprv {\<phi>1,\<phi>2} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>1, \<phi>2} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear4_1:
"nprv {\<phi>2,\<phi>3,\<phi>4} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<phi>4 \<in> fmla \<Longrightarrow>\<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3,\<phi>4} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>2, \<phi>3, \<phi>4} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<phi>4 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3, \<phi>4} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear4_2:
"nprv {\<phi>1,\<phi>3,\<phi>4} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<phi>4 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3,\<phi>4} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>1, \<phi>3, \<phi>4} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<phi>4 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3, \<phi>4} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear4_3:
"nprv {\<phi>1,\<phi>2,\<phi>4} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<phi>4 \<in> fmla \<Longrightarrow>\<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3,\<phi>4} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>1, \<phi>2, \<phi>4} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<phi>4 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3, \<phi>4} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear4_4:
"nprv {\<phi>1,\<phi>2,\<phi>3} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<phi>4 \<in> fmla \<Longrightarrow>\<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3,\<phi>4} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>1, \<phi>2, \<phi>3} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<phi>4 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3, \<phi>4} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear5_1:
"nprv {\<phi>2,\<phi>3,\<phi>4,\<phi>5} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<phi>4 \<in> fmla \<Longrightarrow> \<phi>5 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3,\<phi>4,\<phi>5} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>2, \<phi>3, \<phi>4, \<phi>5} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<phi>4 \<in> fmla; \<phi>5 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3, \<phi>4, \<phi>5} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto


[STATEMENT]
lemma nprv_clear5_2:
"nprv {\<phi>1,\<phi>3,\<phi>4,\<phi>5} \<psi> \<Longrightarrow> \<phi>1 \<in> fmla \<Longrightarrow> \<phi>2 \<in> fmla \<Longrightarrow> \<phi>3 \<in> fmla \<Longrightarrow> \<phi>4 \<in> fmla \<Longrightarrow> \<phi>5 \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
 nprv {\<phi>1,\<phi>2,\<phi>3,\<phi>4,\<phi>5} \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nprv {\<phi>1, \<phi>3, \<phi>4, \<phi>5} \<psi>; \<phi>1 \<in> fmla; \<phi>2 \<in> fmla; \<phi>3 \<in> fmla; \<phi>4 \<in> fmla; \<phi>5 \<in> fmla; \<psi> \<in> fmla\<rbrakk> \<Longrightarrow> nprv {\<phi>1, \<phi>2, \<phi>3, \<phi>4, \<phi>5} \<psi>
[PROOF STEP]
by (rule nprv_mono) auto