[STATEMENT]
lemma mem_correct_pair:
  "mem_correct lookup_pair update_pair inv_pair"
  if injective: "\<forall> k k'. key1 k = key1 k' \<and> key2 k = key2 k' \<longrightarrow> k = k'"
[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]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift_p inv_pair (lookup_pair k)
[PROOF STEP]
unfolding lookup_pair_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift_p inv_pair (get_k2 \<bind> (\<lambda>k2. if key1 k = k2 then lookup2 (key2 k) else get_k1 \<bind> (\<lambda>k1. if key1 k = k1 then lookup1 (key2 k) else State_Monad.return None)))
[PROOF STEP]
by (auto 4 4
        intro!: lift_pI
        dest: get_state inv_pair_lookup1 inv_pair_lookup2
        simp: State_Monad.bind_def State_Monad.run_state_return
        split: if_split_asm prod.split_asm
        )
[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]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift_p inv_pair (update_pair k v)
[PROOF STEP]
unfolding update_pair_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift_p inv_pair (get_k1 \<bind> (\<lambda>k1. if key1 k = k1 then update1 (key2 k) v else get_k2 \<bind> (\<lambda>k2. if key1 k = k2 then update2 (key2 k) v else move12 (key1 k) \<bind> (\<lambda>_. update1 (key2 k) v))))
[PROOF STEP]
apply (auto 4 4
        intro!: lift_pI intro: inv_pair_update1 inv_pair_update2
        dest: get_state
        simp: State_Monad.bind_def get_state State_Monad.run_state_return
        split: if_split_asm prod.split_asm
        )+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>heap heap' x1 x2 x1a x2a x2b. \<lbrakk>inv_pair heap; run_state get_k1 heap = (x1, x2); key1 k \<noteq> x1; run_state get_k2 x2 = (x1a, x2a); key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state (update1 (key2 k) v) x2b = ((), heap')\<rbrakk> \<Longrightarrow> inv_pair heap'
[PROOF STEP]
apply (elim inv_pair_update1 inv_pair_move12)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>heap heap' x1 x2 x1a x2a x2b. \<lbrakk>inv_pair heap; run_state get_k1 heap = (x1, x2); key1 k \<noteq> x1; run_state get_k2 x2 = (x1a, x2a); key1 k \<noteq> x1a\<rbrakk> \<Longrightarrow> inv_pair x2a
 2. \<And>heap heap' x1 x2 x1a x2a x2b. \<lbrakk>inv_pair heap; run_state get_k1 heap = (x1, x2); key1 k \<noteq> x1; run_state get_k2 x2 = (x1a, x2a); key1 k \<noteq> x1a\<rbrakk> \<Longrightarrow> fst (run_state get_k1 x2a) \<noteq> key1 k
 3. \<And>heap heap' x1 x2 x1a x2a x2b. \<lbrakk>inv_pair heap; run_state get_k1 heap = (x1, x2); key1 k \<noteq> x1; run_state get_k2 x2 = (x1a, x2a); key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b)\<rbrakk> \<Longrightarrow> fst (run_state get_k1 x2b) = key1 k
[PROOF STEP]
apply (((subst get_state, assumption)+)?, auto intro: move12_keys dest: get_state; fail)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[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]
let ?m = "snd (State_Monad.run_state (lookup2 (key2 k)) m)"
[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]
have "map_of1 ?m \<subseteq>\<^sub>m map_of1 m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m
[PROOF STEP]
by (smt 3 domIff inv_pair_P_D local.lookup_keys lookup_correct map_le_def map_of1_def surjective_pairing)
[PROOF STATE]
proof (state)
this:
map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 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]
moreover
[PROOF STATE]
proof (state)
this:
map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 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]
have "map_of2 ?m \<subseteq>\<^sub>m map_of2 m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m
[PROOF STEP]
by (smt 3 domIff inv_pair_P_D local.lookup_keys lookup_correct map_le_def map_of2_def surjective_pairing)
[PROOF STATE]
proof (state)
this:
map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 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]
moreover
[PROOF STATE]
proof (state)
this:
map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 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]
have "dom (map_of1 ?m) \<inter> dom (map_of2 m) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 m) = {}
[PROOF STEP]
using 3 \<open>map_of1 ?m \<subseteq>\<^sub>m map_of1 m\<close> inv_pair_domD map_le_implies_dom_le
[PROOF STATE]
proof (prove)
using this:
inv_pair m
map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m
inv_pair ?m \<Longrightarrow> dom (map_of1 ?m) \<inter> dom (map_of2 ?m) = {}
?f \<subseteq>\<^sub>m ?g \<Longrightarrow> dom ?f \<subseteq> dom ?g

goal (1 subgoal):
 1. dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 m) = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 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]
moreover
[PROOF STATE]
proof (state)
this:
dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 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]
have "inv_pair ?m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_pair (snd (run_state (lookup2 (key2 k)) m))
[PROOF STEP]
using 3 inv_pair_lookup2 surjective_pairing
[PROOF STATE]
proof (prove)
using this:
inv_pair m
\<lbrakk>run_state (lookup2 ?k) ?m = (?v, ?m'); inv_pair ?m\<rbrakk> \<Longrightarrow> inv_pair ?m'
?t = (fst ?t, snd ?t)

goal (1 subgoal):
 1. inv_pair (snd (run_state (lookup2 (key2 k)) m))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
inv_pair (snd (run_state (lookup2 (key2 k)) 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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m
map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m
dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 m) = {}
inv_pair (snd (run_state (lookup2 (key2 k)) m))
[PROOF STEP]
have "pair.map_of ?m \<subseteq>\<^sub>m pair.map_of m"
[PROOF STATE]
proof (prove)
using this:
map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m
map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m
dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 m) = {}
inv_pair (snd (run_state (lookup2 (key2 k)) m))

goal (1 subgoal):
 1. pair.map_of (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of m
[PROOF STEP]
apply (subst map_of_eq_pair[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup2 (key2 k)) m))\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (lookup2 (key2 k)) m))
 2. \<lbrakk>map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup2 (key2 k)) m))\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (lookup2 (key2 k)) m)) ++ map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of m
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup2 (key2 k)) m))\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (lookup2 (key2 k)) m)) ++ map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<lbrakk>map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup2 (key2 k)) m))\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (lookup2 (key2 k)) m))
[PROOF STEP]
apply (subst map_of_eq_pair[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup2 (key2 k)) m))\<rbrakk> \<Longrightarrow> inv_pair m
 2. \<lbrakk>map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup2 (key2 k)) m))\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (lookup2 (key2 k)) m)) ++ map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m ++ map_of2 m
 3. \<lbrakk>map_of1 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup2 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup2 (key2 k)) m))\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (lookup2 (key2 k)) m))
[PROOF STEP]
by (auto intro: 3 map_add_mono)
[PROOF STATE]
proof (state)
this:
pair.map_of (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of 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:
pair.map_of (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of 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]
moreover
[PROOF STATE]
proof (state)
this:
pair.map_of (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of 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:
pair.map_of (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of 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]
let ?m = "snd (State_Monad.run_state (lookup1 (key2 k)) m)"
[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]
have "map_of1 ?m \<subseteq>\<^sub>m map_of1 m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m
[PROOF STEP]
by (smt 3 domIff inv_pair_P_D local.lookup_keys lookup_correct map_le_def map_of1_def surjective_pairing)
[PROOF STATE]
proof (state)
this:
map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 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]
moreover
[PROOF STATE]
proof (state)
this:
map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 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]
have "map_of2 ?m \<subseteq>\<^sub>m map_of2 m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m
[PROOF STEP]
by (smt 3 domIff inv_pair_P_D local.lookup_keys lookup_correct map_le_def map_of2_def surjective_pairing)
[PROOF STATE]
proof (state)
this:
map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 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]
moreover
[PROOF STATE]
proof (state)
this:
map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 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]
have "dom (map_of1 ?m) \<inter> dom (map_of2 m) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 m) = {}
[PROOF STEP]
using 3 \<open>map_of1 ?m \<subseteq>\<^sub>m map_of1 m\<close> inv_pair_domD map_le_implies_dom_le
[PROOF STATE]
proof (prove)
using this:
inv_pair m
map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m
inv_pair ?m \<Longrightarrow> dom (map_of1 ?m) \<inter> dom (map_of2 ?m) = {}
?f \<subseteq>\<^sub>m ?g \<Longrightarrow> dom ?f \<subseteq> dom ?g

goal (1 subgoal):
 1. dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 m) = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 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]
moreover
[PROOF STATE]
proof (state)
this:
dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 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]
have "inv_pair ?m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_pair (snd (run_state (lookup1 (key2 k)) m))
[PROOF STEP]
using 3 inv_pair_lookup1 surjective_pairing
[PROOF STATE]
proof (prove)
using this:
inv_pair m
\<lbrakk>run_state (lookup1 ?k) ?m = (?v, ?m'); inv_pair ?m\<rbrakk> \<Longrightarrow> inv_pair ?m'
?t = (fst ?t, snd ?t)

goal (1 subgoal):
 1. inv_pair (snd (run_state (lookup1 (key2 k)) m))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
inv_pair (snd (run_state (lookup1 (key2 k)) 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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m
map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m
dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 m) = {}
inv_pair (snd (run_state (lookup1 (key2 k)) m))
[PROOF STEP]
have "pair.map_of ?m \<subseteq>\<^sub>m pair.map_of m"
[PROOF STATE]
proof (prove)
using this:
map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m
map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m
dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 m) = {}
inv_pair (snd (run_state (lookup1 (key2 k)) m))

goal (1 subgoal):
 1. pair.map_of (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of m
[PROOF STEP]
apply (subst map_of_eq_pair[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup1 (key2 k)) m))\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (lookup1 (key2 k)) m))
 2. \<lbrakk>map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup1 (key2 k)) m))\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (lookup1 (key2 k)) m)) ++ map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of m
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup1 (key2 k)) m))\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (lookup1 (key2 k)) m)) ++ map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of m
 2. \<lbrakk>map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup1 (key2 k)) m))\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (lookup1 (key2 k)) m))
[PROOF STEP]
apply (subst map_of_eq_pair[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup1 (key2 k)) m))\<rbrakk> \<Longrightarrow> inv_pair m
 2. \<lbrakk>map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup1 (key2 k)) m))\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (lookup1 (key2 k)) m)) ++ map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m ++ map_of2 m
 3. \<lbrakk>map_of1 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of1 m; map_of2 (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (lookup1 (key2 k)) m))) \<inter> dom (map_of2 m) = {}; inv_pair (snd (run_state (lookup1 (key2 k)) m))\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (lookup1 (key2 k)) m))
[PROOF STEP]
by (auto intro: 3 map_add_mono)
[PROOF STATE]
proof (state)
this:
pair.map_of (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of 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:
pair.map_of (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of 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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pair.map_of (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of m
pair.map_of (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
pair.map_of (snd (run_state (lookup2 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of m
pair.map_of (snd (run_state (lookup1 (key2 k)) m)) \<subseteq>\<^sub>m pair.map_of m

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:if_split prod.split
        simp: Let_def lookup_pair_def State_Monad.bind_def State_Monad.run_state_return dest: get_state intro: map_le_refl
        )
[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 prems: (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]
let ?m1 = "snd (State_Monad.run_state (update1 (key2 k) v) m)"
[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]
let ?m2 = "snd (State_Monad.run_state (update2 (key2 k) v) m)"
[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]
from prems
[PROOF STATE]
proof (chain)
picking this:
inv_pair m
[PROOF STEP]
have disjoint: "dom (map_of1 m) \<inter> dom (map_of2 m) = {}"
[PROOF STATE]
proof (prove)
using this:
inv_pair m

goal (1 subgoal):
 1. dom (map_of1 m) \<inter> dom (map_of2 m) = {}
[PROOF STEP]
by (simp add: inv_pair_domD)
[PROOF STATE]
proof (state)
this:
dom (map_of1 m) \<inter> dom (map_of2 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]
show ?case
[PROOF STATE]
proof (prove)
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]
apply (auto
        intro: map_le_refl dest: get_state
        split: prod.split
        simp: Let_def update_pair_def State_Monad.bind_def State_Monad.run_state_return
        )
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
case (1 m')
[PROOF STATE]
proof (state)
this:
run_state get_k1 m = (key1 k, m')

goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
run_state get_k1 m = (key1 k, m')
[PROOF STEP]
have "m' = m"
[PROOF STATE]
proof (prove)
using this:
run_state get_k1 m = (key1 k, m')

goal (1 subgoal):
 1. m' = m
[PROOF STEP]
by (rule get_state)
[PROOF STATE]
proof (state)
this:
m' = m

goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from 1 prems
[PROOF STATE]
proof (chain)
picking this:
run_state get_k1 m = (key1 k, m')
inv_pair m
[PROOF STEP]
have "map_of1 ?m1 \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
using this:
run_state get_k1 m = (key1 k, m')
inv_pair m

goal (1 subgoal):
 1. map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v)
[PROOF STEP]
by (smt inv_pair_P_D map_le_def map_of1_def surjective_pairing domIff
          fst_conv fun_upd_apply injective update_correct update_keys
          )
[PROOF STATE]
proof (state)
this:
map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v)

goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v)

goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
inv_pair m
[PROOF STEP]
have "map_of2 ?m1 \<subseteq>\<^sub>m map_of2 m"
[PROOF STATE]
proof (prove)
using this:
inv_pair m

goal (1 subgoal):
 1. map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m
[PROOF STEP]
by (smt domIff inv_pair_P_D update_correct update_keys map_le_def map_of2_def surjective_pairing)
[PROOF STATE]
proof (state)
this:
map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m

goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m

goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
inv_pair m
[PROOF STEP]
have "dom (map_of1 ?m1) \<inter> dom (map_of2 m) = {}"
[PROOF STATE]
proof (prove)
using this:
inv_pair m

goal (1 subgoal):
 1. dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}
[PROOF STEP]
by (smt inv_pair_P_D[OF \<open>inv_pair m\<close>] domIff Int_emptyI eq_snd_iff inv_pair_neq
          map_of1_def map_of2_def update_keys(1)
          )
[PROOF STATE]
proof (state)
this:
dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}

goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}

goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from 1 prems
[PROOF STATE]
proof (chain)
picking this:
run_state get_k1 m = (key1 k, m')
inv_pair m
[PROOF STEP]
have "k \<notin> dom (map_of2 m)"
[PROOF STATE]
proof (prove)
using this:
run_state get_k1 m = (key1 k, m')
inv_pair m

goal (1 subgoal):
 1. k \<notin> dom (map_of2 m)
[PROOF STEP]
using inv_pair_neq map_of2_def
[PROOF STATE]
proof (prove)
using this:
run_state get_k1 m = (key1 k, m')
inv_pair m
\<lbrakk>inv_pair ?m; fst (run_state get_k1 ?m) = fst (run_state get_k2 ?m)\<rbrakk> \<Longrightarrow> False
map_of2 ?m ?k = (if key1 ?k = fst (run_state get_k2 ?m) then mem2.map_of ?m (key2 ?k) else None)

goal (1 subgoal):
 1. k \<notin> dom (map_of2 m)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
k \<notin> dom (map_of2 m)

goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k \<notin> dom (map_of2 m)

goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from 1 prems
[PROOF STATE]
proof (chain)
picking this:
run_state get_k1 m = (key1 k, m')
inv_pair m
[PROOF STEP]
have "inv_pair ?m1"
[PROOF STATE]
proof (prove)
using this:
run_state get_k1 m = (key1 k, m')
inv_pair m

goal (1 subgoal):
 1. inv_pair (snd (run_state (update1 (key2 k) v) m))
[PROOF STEP]
using inv_pair_update1 fst_conv surjective_pairing
[PROOF STATE]
proof (prove)
using this:
run_state get_k1 m = (key1 k, m')
inv_pair m
\<lbrakk>run_state (update1 (key2 ?k) ?v) ?m = (?v', ?m'); inv_pair ?m; fst (run_state get_k1 ?m) = key1 ?k\<rbrakk> \<Longrightarrow> inv_pair ?m'
fst (?x1.0, ?x2.0) = ?x1.0
?t = (fst ?t, snd ?t)

goal (1 subgoal):
 1. inv_pair (snd (run_state (update1 (key2 k) v) m))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
inv_pair (snd (run_state (update1 (key2 k) v) m))

goal (3 subgoals):
 1. \<And>x2. run_state get_k1 m = (key1 k, x2) \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 3. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v)
map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m
dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}
k \<notin> dom (map_of2 m)
inv_pair (snd (run_state (update1 (key2 k) v) m))
[PROOF STEP]
show "pair.map_of (snd (State_Monad.run_state (update1 (key2 k) v) m')) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
using this:
map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v)
map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m
dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}
k \<notin> dom (map_of2 m)
inv_pair (snd (run_state (update1 (key2 k) v) m))

goal (1 subgoal):
 1. pair.map_of (snd (run_state (update1 (key2 k) v) m')) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
unfolding \<open>m' = m\<close>
[PROOF STATE]
proof (prove)
using this:
map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v)
map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m
dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}
k \<notin> dom (map_of2 m)
inv_pair (snd (run_state (update1 (key2 k) v) m))

goal (1 subgoal):
 1. pair.map_of (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
using disjoint
[PROOF STATE]
proof (prove)
using this:
map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v)
map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m
dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}
k \<notin> dom (map_of2 m)
inv_pair (snd (run_state (update1 (key2 k) v) m))
dom (map_of1 m) \<inter> dom (map_of2 m) = {}

goal (1 subgoal):
 1. pair.map_of (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
apply (subst map_of_eq_pair[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}; k \<notin> dom (map_of2 m); inv_pair (snd (run_state (update1 (key2 k) v) m)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update1 (key2 k) v) m))
 2. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}; k \<notin> dom (map_of2 m); inv_pair (snd (run_state (update1 (key2 k) v) m)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update1 (key2 k) v) m)) ++ map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}; k \<notin> dom (map_of2 m); inv_pair (snd (run_state (update1 (key2 k) v) m)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update1 (key2 k) v) m)) ++ map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}; k \<notin> dom (map_of2 m); inv_pair (snd (run_state (update1 (key2 k) v) m)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update1 (key2 k) v) m))
[PROOF STEP]
apply (subst map_of_eq_pair[symmetric], rule prems)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}; k \<notin> dom (map_of2 m); inv_pair (snd (run_state (update1 (key2 k) v) m)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update1 (key2 k) v) m)) ++ map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m (map_of1 m ++ map_of2 m)(k \<mapsto> v)
 2. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}; k \<notin> dom (map_of2 m); inv_pair (snd (run_state (update1 (key2 k) v) m)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update1 (key2 k) v) m))
[PROOF STEP]
apply (subst map_add_upd2[symmetric])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}; k \<notin> dom (map_of2 m); inv_pair (snd (run_state (update1 (key2 k) v) m)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> dom (map_of1 m) \<inter> dom (map_of2 m) = {}
 2. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}; k \<notin> dom (map_of2 m); inv_pair (snd (run_state (update1 (key2 k) v) m)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> k \<notin> dom (map_of2 m)
 3. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}; k \<notin> dom (map_of2 m); inv_pair (snd (run_state (update1 (key2 k) v) m)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update1 (key2 k) v) m)) ++ map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v) ++ map_of2 m
 4. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m))) \<inter> dom (map_of2 m) = {}; k \<notin> dom (map_of2 m); inv_pair (snd (run_state (update1 (key2 k) v) m)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update1 (key2 k) v) m))
[PROOF STEP]
by (auto intro: map_add_mono)
[PROOF STATE]
proof (state)
this:
pair.map_of (snd (run_state (update1 (key2 k) v) m')) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)

goal (2 subgoals):
 1. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
case (2 k1 m' m'')
[PROOF STATE]
proof (state)
this:
key1 k \<noteq> k1
run_state get_k2 m' = (key1 k, m'')
run_state get_k1 m = (k1, m')

goal (2 subgoals):
 1. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
key1 k \<noteq> k1
run_state get_k2 m' = (key1 k, m'')
run_state get_k1 m = (k1, m')
[PROOF STEP]
have "m' = m" "m'' = m"
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
run_state get_k2 m' = (key1 k, m'')
run_state get_k1 m = (k1, m')

goal (1 subgoal):
 1. m' = m &&& m'' = m
[PROOF STEP]
by (auto dest: get_state)
[PROOF STATE]
proof (state)
this:
m' = m
m'' = m

goal (2 subgoals):
 1. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from 2 prems
[PROOF STATE]
proof (chain)
picking this:
key1 k \<noteq> k1
run_state get_k2 m' = (key1 k, m'')
run_state get_k1 m = (k1, m')
inv_pair m
[PROOF STEP]
have "map_of2 ?m2 \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
run_state get_k2 m' = (key1 k, m'')
run_state get_k1 m = (k1, m')
inv_pair m

goal (1 subgoal):
 1. map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)
[PROOF STEP]
unfolding \<open>m' = m\<close> \<open>m'' = m\<close>
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
run_state get_k2 m = (key1 k, m)
run_state get_k1 m = (k1, m)
inv_pair m

goal (1 subgoal):
 1. map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)
[PROOF STEP]
by (smt inv_pair_P_D map_le_def map_of2_def surjective_pairing domIff
          fst_conv fun_upd_apply injective update_correct update_keys
          )
[PROOF STATE]
proof (state)
this:
map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)

goal (2 subgoals):
 1. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)

goal (2 subgoals):
 1. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
inv_pair m
[PROOF STEP]
have "map_of1 ?m2 \<subseteq>\<^sub>m map_of1 m"
[PROOF STATE]
proof (prove)
using this:
inv_pair m

goal (1 subgoal):
 1. map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m
[PROOF STEP]
by (smt domIff inv_pair_P_D update_correct update_keys map_le_def map_of1_def surjective_pairing)
[PROOF STATE]
proof (state)
this:
map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m

goal (2 subgoals):
 1. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m

goal (2 subgoals):
 1. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
key1 k \<noteq> k1
run_state get_k2 m' = (key1 k, m'')
run_state get_k1 m = (k1, m')
[PROOF STEP]
have "dom (map_of1 ?m2) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}"
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
run_state get_k2 m' = (key1 k, m'')
run_state get_k1 m = (k1, m')

goal (1 subgoal):
 1. dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}
[PROOF STEP]
unfolding \<open>m' = m\<close>
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
run_state get_k2 m = (key1 k, m'')
run_state get_k1 m = (k1, m)

goal (1 subgoal):
 1. dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}
[PROOF STEP]
by (smt domIff \<open>map_of1 ?m2 \<subseteq>\<^sub>m map_of1 m\<close> disjoint_iff_not_equal fst_conv fun_upd_apply
          map_le_def map_of1_def map_of2_def
          )
[PROOF STATE]
proof (state)
this:
dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}

goal (2 subgoals):
 1. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}

goal (2 subgoals):
 1. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from 2 prems
[PROOF STATE]
proof (chain)
picking this:
key1 k \<noteq> k1
run_state get_k2 m' = (key1 k, m'')
run_state get_k1 m = (k1, m')
inv_pair m
[PROOF STEP]
have "inv_pair ?m2"
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
run_state get_k2 m' = (key1 k, m'')
run_state get_k1 m = (k1, m')
inv_pair m

goal (1 subgoal):
 1. inv_pair (snd (run_state (update2 (key2 k) v) m))
[PROOF STEP]
unfolding \<open>m' = m\<close>
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
run_state get_k2 m = (key1 k, m'')
run_state get_k1 m = (k1, m)
inv_pair m

goal (1 subgoal):
 1. inv_pair (snd (run_state (update2 (key2 k) v) m))
[PROOF STEP]
using inv_pair_update2 fst_conv surjective_pairing
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
run_state get_k2 m = (key1 k, m'')
run_state get_k1 m = (k1, m)
inv_pair m
\<lbrakk>run_state (update2 (key2 ?k) ?v) ?m = (?v', ?m'); inv_pair ?m; fst (run_state get_k2 ?m) = key1 ?k\<rbrakk> \<Longrightarrow> inv_pair ?m'
fst (?x1.0, ?x2.0) = ?x1.0
?t = (fst ?t, snd ?t)

goal (1 subgoal):
 1. inv_pair (snd (run_state (update2 (key2 k) v) m))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
inv_pair (snd (run_state (update2 (key2 k) v) m))

goal (2 subgoals):
 1. \<And>x1 x2 x2a. \<lbrakk>key1 k \<noteq> x1; run_state get_k2 x2 = (key1 k, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update2 (key2 k) v) x2a)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)
map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m
dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}
inv_pair (snd (run_state (update2 (key2 k) v) m))
[PROOF STEP]
show "pair.map_of (snd (State_Monad.run_state (update2 (key2 k) v) m'')) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
using this:
map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)
map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m
dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}
inv_pair (snd (run_state (update2 (key2 k) v) m))

goal (1 subgoal):
 1. pair.map_of (snd (run_state (update2 (key2 k) v) m'')) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
unfolding \<open>m' = m\<close> \<open>m'' = m\<close>
[PROOF STATE]
proof (prove)
using this:
map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)
map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m
dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}
inv_pair (snd (run_state (update2 (key2 k) v) m))

goal (1 subgoal):
 1. pair.map_of (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
apply (subst map_of_eq_pair[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}; inv_pair (snd (run_state (update2 (key2 k) v) m))\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update2 (key2 k) v) m))
 2. \<lbrakk>map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}; inv_pair (snd (run_state (update2 (key2 k) v) m))\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update2 (key2 k) v) m)) ++ map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}; inv_pair (snd (run_state (update2 (key2 k) v) m))\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update2 (key2 k) v) m)) ++ map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<lbrakk>map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}; inv_pair (snd (run_state (update2 (key2 k) v) m))\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update2 (key2 k) v) m))
[PROOF STEP]
apply (subst map_of_eq_pair[symmetric], rule prems)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}; inv_pair (snd (run_state (update2 (key2 k) v) m))\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update2 (key2 k) v) m)) ++ map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m (map_of1 m ++ map_of2 m)(k \<mapsto> v)
 2. \<lbrakk>map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}; inv_pair (snd (run_state (update2 (key2 k) v) m))\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update2 (key2 k) v) m))
[PROOF STEP]
apply (subst map_add_upd[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}; inv_pair (snd (run_state (update2 (key2 k) v) m))\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update2 (key2 k) v) m)) ++ map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m ++ map_of2 m(k \<mapsto> v)
 2. \<lbrakk>map_of2 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of1 (snd (run_state (update2 (key2 k) v) m)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update2 (key2 k) v) m))) \<inter> dom (map_of2 m(k \<mapsto> v)) = {}; inv_pair (snd (run_state (update2 (key2 k) v) m))\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update2 (key2 k) v) m))
[PROOF STEP]
by (rule map_add_mono)
[PROOF STATE]
proof (state)
this:
pair.map_of (snd (run_state (update2 (key2 k) v) m'')) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
case (3 k1 m1 k2 m2 m3)
[PROOF STATE]
proof (state)
this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)
[PROOF STEP]
have "m1 = m" "m2 = m"
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)

goal (1 subgoal):
 1. m1 = m &&& m2 = m
[PROOF STEP]
by (auto dest: get_state)
[PROOF STATE]
proof (state)
this:
m1 = m
m2 = m

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
let ?m3 = "snd (State_Monad.run_state (update1 (key2 k) v) m3)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from 3 prems
[PROOF STATE]
proof (chain)
picking this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)
inv_pair m
[PROOF STEP]
have "map_of1 ?m3 \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)
inv_pair m

goal (1 subgoal):
 1. map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)
[PROOF STEP]
unfolding \<open>m2 = m\<close>
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m = ((), m3)
run_state get_k2 m1 = (k2, m)
run_state get_k1 m = (k1, m1)
inv_pair m

goal (1 subgoal):
 1. map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)
[PROOF STEP]
by (smt inv_pair_P_D map_le_def map_of1_def surjective_pairing domIff
          fst_conv fun_upd_apply injective
          inv_pair_move12 move12_correct move12_keys update_correct update_keys
          )
[PROOF STATE]
proof (state)
this:
map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
have "map_of2 ?m3 \<subseteq>\<^sub>m map_of1 m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m
[PROOF STEP]
from prems 3
[PROOF STATE]
proof (chain)
picking this:
inv_pair m
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)
[PROOF STEP]
have "P m" "P m3"
[PROOF STATE]
proof (prove)
using this:
inv_pair m
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)

goal (1 subgoal):
 1. P m &&& P m3
[PROOF STEP]
unfolding \<open>m1 = m\<close> \<open>m2 = m\<close>
[PROOF STATE]
proof (prove)
using this:
inv_pair m
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m = ((), m3)
run_state get_k2 m = (k2, m)
run_state get_k1 m = (k1, m)

goal (1 subgoal):
 1. P m &&& P m3
[PROOF STEP]
using inv_pair_P_D[OF prems]
[PROOF STATE]
proof (prove)
using this:
inv_pair m
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m = ((), m3)
run_state get_k2 m = (k2, m)
run_state get_k1 m = (k1, m)
P m

goal (1 subgoal):
 1. P m &&& P m3
[PROOF STEP]
by (auto elim: lift_p_P[OF move12_inv])
[PROOF STATE]
proof (state)
this:
P m
P m3

goal (1 subgoal):
 1. map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m
[PROOF STEP]
from 3(3)[unfolded \<open>m2 = m\<close>]
[PROOF STATE]
proof (chain)
picking this:
run_state (move12 (key1 k)) m = ((), m3)
[PROOF STEP]
have "mem2.map_of ?m3 \<subseteq>\<^sub>m mem1.map_of m"
[PROOF STATE]
proof (prove)
using this:
run_state (move12 (key1 k)) m = ((), m3)

goal (1 subgoal):
 1. mem2.map_of (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m mem1.map_of m
[PROOF STEP]
by - (erule map_le_trans[OF update_correct(3)[OF \<open>P m3\<close>] move12_correct(2)[OF \<open>P m\<close>]])
[PROOF STATE]
proof (state)
this:
mem2.map_of (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m mem1.map_of m

goal (1 subgoal):
 1. map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m
[PROOF STEP]
with 3 prems
[PROOF STATE]
proof (chain)
picking this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)
inv_pair m
mem2.map_of (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m mem1.map_of m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)
inv_pair m
mem2.map_of (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m mem1.map_of m

goal (1 subgoal):
 1. map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m
[PROOF STEP]
unfolding \<open>m1 = m\<close> \<open>m2 = m\<close> map_le_def map_of2_def
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m = ((), m3)
run_state get_k2 m = (k2, m)
run_state get_k1 m = (k1, m)
inv_pair m
\<forall>a\<in>dom (mem2.map_of (snd (run_state (update1 (key2 k) v) m3))). mem2.map_of (snd (run_state (update1 (key2 k) v) m3)) a = mem1.map_of m a

goal (1 subgoal):
 1. \<forall>a\<in>dom (\<lambda>ka. if key1 ka = fst (run_state get_k2 (snd (run_state (update1 (key2 k) v) m3))) then mem2.map_of (snd (run_state (update1 (key2 k) v) m3)) (key2 ka) else None). (if key1 a = fst (run_state get_k2 (snd (run_state (update1 (key2 k) v) m3))) then mem2.map_of (snd (run_state (update1 (key2 k) v) m3)) (key2 a) else None) = map_of1 m a
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a y. \<lbrakk>key1 k \<noteq> k1; key1 k \<noteq> k2; run_state (move12 (key1 k)) m = ((), m3); run_state get_k2 m = (k2, m); run_state get_k1 m = (k1, m); inv_pair m; \<forall>a\<in>dom (mem2.map_of (snd (run_state (update1 (key2 k) v) m3))). mem2.map_of (snd (run_state (update1 (key2 k) v) m3)) a = mem1.map_of m a; mem2.map_of (snd (run_state (update1 (key2 k) v) m3)) (key2 a) = Some y; key1 a = fst (run_state get_k2 (snd (run_state (update1 (key2 k) v) m3)))\<rbrakk> \<Longrightarrow> Some y = map_of1 m a
[PROOF STEP]
apply (frule move12_keys(2), simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a y. \<lbrakk>key1 k \<noteq> k1; key1 k \<noteq> k2; run_state (move12 (key1 k)) m = ((), m3); run_state get_k2 m = (k2, m); run_state get_k1 m = (k1, m); inv_pair m; \<forall>a\<in>dom (mem2.map_of (snd (run_state (update1 (key2 k) v) m3))). mem2.map_of (snd (run_state (update1 (key2 k) v) m3)) a = mem1.map_of m a; mem2.map_of (snd (run_state (update1 (key2 k) v) m3)) (key2 a) = Some y; key1 a = fst (run_state get_k2 (snd (run_state (update1 (key2 k) v) m3))); fst (run_state get_k2 m3) = k1\<rbrakk> \<Longrightarrow> Some y = map_of1 m a
[PROOF STEP]
by (metis
            domI inv_pair_def map_of1_def surjective_pairing
            inv_pair_move12 move12_keys(2) update_keys(2)
            )
[PROOF STATE]
proof (state)
this:
map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from prems 3
[PROOF STATE]
proof (chain)
picking this:
inv_pair m
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)
[PROOF STEP]
have "dom (map_of1 ?m3) \<inter> dom (map_of1 m) = {}"
[PROOF STATE]
proof (prove)
using this:
inv_pair m
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)

goal (1 subgoal):
 1. dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}
[PROOF STEP]
unfolding \<open>m1 = m\<close> \<open>m2 = m\<close>
[PROOF STATE]
proof (prove)
using this:
inv_pair m
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m = ((), m3)
run_state get_k2 m = (k2, m)
run_state get_k1 m = (k1, m)

goal (1 subgoal):
 1. dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}
[PROOF STEP]
by (smt inv_pair_P_D disjoint_iff_not_equal map_of1_def surjective_pairing domIff
          fst_conv inv_pair_move12 move12_keys update_keys
          )
[PROOF STATE]
proof (state)
this:
dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)
[PROOF STEP]
have "k \<notin> dom (map_of1 m)"
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)

goal (1 subgoal):
 1. k \<notin> dom (map_of1 m)
[PROOF STEP]
by (simp add: domIff map_of1_def)
[PROOF STATE]
proof (state)
this:
k \<notin> dom (map_of1 m)

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k \<notin> dom (map_of1 m)

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
from 3 prems
[PROOF STATE]
proof (chain)
picking this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)
inv_pair m
[PROOF STEP]
have "inv_pair ?m3"
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m2 = ((), m3)
run_state get_k2 m1 = (k2, m2)
run_state get_k1 m = (k1, m1)
inv_pair m

goal (1 subgoal):
 1. inv_pair (snd (run_state (update1 (key2 k) v) m3))
[PROOF STEP]
unfolding \<open>m2 = m\<close>
[PROOF STATE]
proof (prove)
using this:
key1 k \<noteq> k1
key1 k \<noteq> k2
run_state (move12 (key1 k)) m = ((), m3)
run_state get_k2 m1 = (k2, m)
run_state get_k1 m = (k1, m1)
inv_pair m

goal (1 subgoal):
 1. inv_pair (snd (run_state (update1 (key2 k) v) m3))
[PROOF STEP]
by (metis inv_pair_move12 inv_pair_update1 move12_keys(1) fst_conv surjective_pairing)
[PROOF STATE]
proof (state)
this:
inv_pair (snd (run_state (update1 (key2 k) v) m3))

goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x2b. \<lbrakk>key1 k \<noteq> x1; key1 k \<noteq> x1a; run_state (move12 (key1 k)) x2a = ((), x2b); run_state get_k2 x2 = (x1a, x2a); run_state get_k1 m = (x1, x2)\<rbrakk> \<Longrightarrow> pair.map_of (snd (run_state (update1 (key2 k) v) x2b)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)
map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m
dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}
k \<notin> dom (map_of1 m)
inv_pair (snd (run_state (update1 (key2 k) v) m3))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)
map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m
dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}
k \<notin> dom (map_of1 m)
inv_pair (snd (run_state (update1 (key2 k) v) m3))

goal (1 subgoal):
 1. pair.map_of (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
unfolding \<open>m1 = m\<close> \<open>m2 = m\<close>
[PROOF STATE]
proof (prove)
using this:
map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)
map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m
dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}
k \<notin> dom (map_of1 m)
inv_pair (snd (run_state (update1 (key2 k) v) m3))

goal (1 subgoal):
 1. pair.map_of (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
using disjoint
[PROOF STATE]
proof (prove)
using this:
map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v)
map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m
dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}
k \<notin> dom (map_of1 m)
inv_pair (snd (run_state (update1 (key2 k) v) m3))
dom (map_of1 m) \<inter> dom (map_of2 m) = {}

goal (1 subgoal):
 1. pair.map_of (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
apply (subst map_of_eq_pair[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update1 (key2 k) v) m3))
 2. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update1 (key2 k) v) m3)) ++ map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update1 (key2 k) v) m3)) ++ map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)
 2. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update1 (key2 k) v) m3))
[PROOF STEP]
apply (subst map_of_eq_pair[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair m
 2. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update1 (key2 k) v) m3)) ++ map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m (map_of1 m ++ map_of2 m)(k \<mapsto> v)
 3. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update1 (key2 k) v) m3))
[PROOF STEP]
apply (rule prems)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update1 (key2 k) v) m3)) ++ map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m (map_of1 m ++ map_of2 m)(k \<mapsto> v)
 2. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update1 (key2 k) v) m3))
[PROOF STEP]
apply (subst (2) map_add_comm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> dom (map_of1 m) \<inter> dom (map_of2 m) = {}
 2. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update1 (key2 k) v) m3)) ++ map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m (map_of2 m ++ map_of1 m)(k \<mapsto> v)
 3. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update1 (key2 k) v) m3))
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update1 (key2 k) v) m3)) ++ map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m (map_of2 m ++ map_of1 m)(k \<mapsto> v)
 2. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update1 (key2 k) v) m3))
 3. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> dom (map_of1 m) \<inter> dom (map_of2 m) = {}
[PROOF STEP]
apply (subst map_add_upd2[symmetric])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> dom (map_of2 m) \<inter> dom (map_of1 m) = {}
 2. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> k \<notin> dom (map_of1 m)
 3. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> map_of1 (snd (run_state (update1 (key2 k) v) m3)) ++ map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v) ++ map_of1 m
 4. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> inv_pair (snd (run_state (update1 (key2 k) v) m3))
 5. \<lbrakk>map_of1 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of2 m(k \<mapsto> v); map_of2 (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m map_of1 m; dom (map_of1 (snd (run_state (update1 (key2 k) v) m3))) \<inter> dom (map_of1 m) = {}; k \<notin> dom (map_of1 m); inv_pair (snd (run_state (update1 (key2 k) v) m3)); dom (map_of1 m) \<inter> dom (map_of2 m) = {}\<rbrakk> \<Longrightarrow> dom (map_of1 m) \<inter> dom (map_of2 m) = {}
[PROOF STEP]
apply (auto intro: map_add_mono)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
pair.map_of (snd (run_state (update1 (key2 k) v) m3)) \<subseteq>\<^sub>m pair.map_of m(k \<mapsto> v)

goal:
No subgoals!
[PROOF STEP]
qed
[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 emptyI:
  assumes "inv_pair m" "mem1.map_of m \<subseteq>\<^sub>m Map.empty" "mem2.map_of m \<subseteq>\<^sub>m Map.empty"
  shows "pair.map_of m \<subseteq>\<^sub>m Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pair.map_of m \<subseteq>\<^sub>m Map.empty
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inv_pair m
mem1.map_of m \<subseteq>\<^sub>m Map.empty
mem2.map_of m \<subseteq>\<^sub>m Map.empty

goal (1 subgoal):
 1. pair.map_of m \<subseteq>\<^sub>m Map.empty
[PROOF STEP]
by (auto simp: map_of1_def map_of2_def map_le_def map_of_eq_pair[symmetric])