[STATEMENT]
lemma inv_pair_update1:
  "inv_pair m'"
  if "State_Monad.run_state (update1 (key2 k) v) m = (v', m')" "inv_pair m" "fst (State_Monad.run_state get_k1 m) = key1 k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_pair m'
[PROOF STEP]
using that update_inv[of "key2 k" v] inv_pair_P_D[OF \<open>inv_pair m\<close>]
[PROOF STATE]
proof (prove)
using this:
run_state (update1 (key2 k) v) m = (v', m')
inv_pair m
fst (run_state get_k1 m) = key1 k
lift_p P (update1 (key2 k) v)
lift_p P (update2 (key2 k) v)
P m

goal (1 subgoal):
 1. inv_pair m'
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
run_state (update1 (key2 k) v) m = (v', m')
let k1 = fst (run_state get_k1 m); k2 = fst (run_state get_k2 m) in (\<forall>k\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> P m
fst (run_state get_k1 m) = key1 k
lift_p P (update1 (key2 k) v)
lift_p P (update2 (key2 k) v)
P m

goal (1 subgoal):
 1. let k1 = fst (run_state get_k1 m'); k2 = fst (run_state get_k2 m') in (\<forall>k\<in>dom (mem1.map_of m'). \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>dom (mem2.map_of m'). \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> P m'
[PROOF STEP]
apply (auto
        simp: Let_def update_keys
        dest: lift_p_P update_correct[of _ "key2 k" v, THEN map_le_implies_dom_le]
     )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ka y. \<lbrakk>run_state (update1 (key2 k) v) m = ((), m'); fst (run_state get_k1 m) = key1 k; lift_p P (update1 (key2 k) v); lift_p P (update2 (key2 k) v); P m; \<forall>ka\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = key1 k \<and> key2 k' = ka; \<forall>k\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = fst (run_state get_k2 m) \<and> key2 k' = k; key1 k \<noteq> fst (run_state get_k2 m); mem1.map_of m' ka = Some y\<rbrakk> \<Longrightarrow> \<exists>k'. key1 k' = key1 k \<and> key2 k' = ka
 2. \<And>ka y. \<lbrakk>run_state (update1 (key2 k) v) m = ((), m'); fst (run_state get_k1 m) = key1 k; lift_p P (update1 (key2 k) v); lift_p P (update2 (key2 k) v); P m; \<forall>ka\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = key1 k \<and> key2 k' = ka; \<forall>k\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = fst (run_state get_k2 m) \<and> key2 k' = k; key1 k \<noteq> fst (run_state get_k2 m); mem2.map_of m' ka = Some y\<rbrakk> \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state get_k2 m) \<and> key2 k' = ka
[PROOF STEP]
apply (frule update_correct[of _ "key2 k" v, THEN map_le_implies_dom_le]; auto 13 2; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ka y. \<lbrakk>run_state (update1 (key2 k) v) m = ((), m'); fst (run_state get_k1 m) = key1 k; lift_p P (update1 (key2 k) v); lift_p P (update2 (key2 k) v); P m; \<forall>ka\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = key1 k \<and> key2 k' = ka; \<forall>k\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = fst (run_state get_k2 m) \<and> key2 k' = k; key1 k \<noteq> fst (run_state get_k2 m); mem2.map_of m' ka = Some y\<rbrakk> \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state get_k2 m) \<and> key2 k' = ka
[PROOF STEP]
apply (frule update_correct[of _ "key2 k" v, THEN map_le_implies_dom_le]; auto 13 2; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done