[STATEMENT]
lemma GTT_to_RR2:
  assumes "gtt_syms \<G> |\<subseteq>| \<F>"
  shows "RR2_spec (GTT_to_RR2_reg \<F> \<G>) (ggtt_lang \<F> \<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_reg \<F> \<G>) (map_both gterm_of_term ` Restr (map_both term_of_gterm ` gtt_lang \<G>) {t. funas_term t \<subseteq> fset \<F>})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_reg \<F> \<G>) (map_both gterm_of_term ` Restr (map_both term_of_gterm ` gtt_lang \<G>) {t. funas_term t \<subseteq> fset \<F>})
[PROOF STEP]
have *: "snd ` (X \<times> X) = X" for X
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` (X \<times> X) = X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd ` (?X1 \<times> ?X1) = ?X1

goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_reg \<F> \<G>) (map_both gterm_of_term ` Restr (map_both term_of_gterm ` gtt_lang \<G>) {t. funas_term t \<subseteq> fset \<F>})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR2_spec (GTT_to_RR2_reg \<F> \<G>) (map_both gterm_of_term ` Restr (map_both term_of_gterm ` gtt_lang \<G>) {t. funas_term t \<subseteq> fset \<F>})
[PROOF STEP]
unfolding gtt_lang_from_agtt_lang GTT_to_RR2_reg_def RR2_spec_def
    parallel_closure_automaton[OF GTT_to_RR2_root, of \<F> \<G>, unfolded RR2_spec_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {gpair t u |t u. (t, u) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)} = {gpair t u |t u. (t, u) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>}}
[PROOF STEP]
proof (intro arg_cong[where f = "\<lambda>X. {gpair t u |t u. (t,u) \<in> X}"] equalityI subrelI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. (x, y) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>) \<Longrightarrow> (x, y) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>}
 2. \<And>x y. (x, y) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>} \<Longrightarrow> (x, y) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)
[PROOF STEP]
case (1 s t)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)

goal (2 subgoals):
 1. \<And>x y. (x, y) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>) \<Longrightarrow> (x, y) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>}
 2. \<And>x y. (x, y) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>} \<Longrightarrow> (x, y) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(s, t) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)

goal (1 subgoal):
 1. (s, t) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>}
[PROOF STEP]
using subsetD[OF equalityD2[OF gtt_lang_from_agtt_lang], of "(s, t)" \<G>]
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)
(s, t) \<in> lift_root_step UNIV PAny EParallel (agtt_lang \<G>) \<Longrightarrow> (s, t) \<in> gtt_lang \<G>

goal (1 subgoal):
 1. (s, t) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>}
[PROOF STEP]
by (intro rev_image_eqI[of "(term_of_gterm s, term_of_gterm t)"])
         (auto simp: funas_term_of_gterm_conv subsetD[OF lift_root_step_mono]
           dest: subsetD[OF lift_root_step_sig[unfolded \<T>\<^sub>G_equivalent_def, OF agtt_lang_syms[OF assms]]])
[PROOF STATE]
proof (state)
this:
(s, t) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>}

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>} \<Longrightarrow> (x, y) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>} \<Longrightarrow> (x, y) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)
[PROOF STEP]
case (2 s t)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>}

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>} \<Longrightarrow> (x, y) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)
[PROOF STEP]
from image_mono[OF agtt_lang_syms[OF assms], of snd, unfolded *]
[PROOF STATE]
proof (chain)
picking this:
snd ` agtt_lang \<G> \<subseteq> gterms (fset \<F>)
[PROOF STEP]
have *: "snd ` agtt_lang \<G> \<subseteq> gterms UNIV"
[PROOF STATE]
proof (prove)
using this:
snd ` agtt_lang \<G> \<subseteq> gterms (fset \<F>)

goal (1 subgoal):
 1. snd ` agtt_lang \<G> \<subseteq> gterms UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd ` agtt_lang \<G> \<subseteq> gterms UNIV

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>} \<Longrightarrow> (x, y) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s, t) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> map_both gterm_of_term ` Restr (map_both term_of_gterm ` lift_root_step UNIV PAny EParallel (agtt_lang \<G>)) {t. funas_term t \<subseteq> fset \<F>}

goal (1 subgoal):
 1. (s, t) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)
[PROOF STEP]
by (auto intro!: lift_root_step_sig_transfer[unfolded \<T>\<^sub>G_equivalent_def, OF _ *, of _ _ _ "fset \<F>"]
        simp: funas_gterm_gterm_of_term funas_term_of_gterm_conv)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> lift_root_step (fset \<F>) PAny EParallel (agtt_lang \<G>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
RR2_spec (GTT_to_RR2_reg \<F> \<G>) (map_both gterm_of_term ` Restr (map_both term_of_gterm ` gtt_lang \<G>) {t. funas_term t \<subseteq> fset \<F>})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_add_mono:
  "(m1 ++ m2) \<subseteq>\<^sub>m (m1' ++ m2')" if "m1 \<subseteq>\<^sub>m m1'" "m2 \<subseteq>\<^sub>m m2'" "dom m1 \<inter> dom m2' = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m1 ++ m2 \<subseteq>\<^sub>m m1' ++ m2'
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
m1 \<subseteq>\<^sub>m m1'
m2 \<subseteq>\<^sub>m m2'
dom m1 \<inter> dom m2' = {}

goal (1 subgoal):
 1. m1 ++ m2 \<subseteq>\<^sub>m m1' ++ m2'
[PROOF STEP]
unfolding map_le_def map_add_def dom_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>{a. m1 a \<noteq> None}. m1 a = m1' a
\<forall>a\<in>{a. m2 a \<noteq> None}. m2 a = m2' a
{a. m1 a \<noteq> None} \<inter> {a. m2' a \<noteq> None} = {}

goal (1 subgoal):
 1. \<forall>a\<in>{a. (case m2 a of None \<Rightarrow> m1 a | Some x \<Rightarrow> Some x) \<noteq> None}. (case m2 a of None \<Rightarrow> m1 a | Some x \<Rightarrow> Some x) = (case m2' a of None \<Rightarrow> m1' a | Some x \<Rightarrow> Some x)
[PROOF STEP]
by (auto split: option.splits)


[STATEMENT]
lemma map_add_upd2:
  "f(x \<mapsto> y) ++ g = (f ++ g)(x \<mapsto> y)" if "dom f \<inter> dom g = {}" "x \<notin> dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f(x \<mapsto> y) ++ g = (f ++ g)(x \<mapsto> y)
[PROOF STEP]
apply (subst map_add_comm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dom (f(x \<mapsto> y)) \<inter> dom g = {}
 2. g ++ f(x \<mapsto> y) = (f ++ g)(x \<mapsto> y)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. g ++ f(x \<mapsto> y) = (f ++ g)(x \<mapsto> y)
 2. dom (f(x \<mapsto> y)) \<inter> dom g = {}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (g ++ f)(x \<mapsto> y) = (f ++ g)(x \<mapsto> y)
 2. dom (f(x \<mapsto> y)) \<inter> dom g = {}
[PROOF STEP]
apply (subst map_add_comm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. dom g \<inter> dom f = {}
 2. (f ++ g)(x \<mapsto> y) = (f ++ g)(x \<mapsto> y)
 3. dom (f(x \<mapsto> y)) \<inter> dom g = {}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
dom f \<inter> dom g = {}
x \<notin> dom g

goal (3 subgoals):
 1. dom g \<inter> dom f = {}
 2. (f ++ g)(x \<mapsto> y) = (f ++ g)(x \<mapsto> y)
 3. dom (f(x \<mapsto> y)) \<inter> dom g = {}
[PROOF STEP]
by auto


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

goal (1 subgoal):
 1. pair.map_of m \<subseteq>\<^sub>m map_of1 m ++ map_of2 m
[PROOF STEP]
unfolding pair.map_of_def map_of1_def map_of2_def
[PROOF STATE]
proof (prove)
using this:
inv_pair m

goal (1 subgoal):
 1. (\<lambda>k. fst (run_state (lookup_pair k) m)) \<subseteq>\<^sub>m (\<lambda>k. if key1 k = fst (run_state get_k1 m) then mem1.map_of m (key2 k) else None) ++ (\<lambda>k. if key1 k = fst (run_state get_k2 m) then mem2.map_of m (key2 k) else None)
[PROOF STEP]
unfolding lookup_pair_def inv_pair_def map_of_def map_le_def dom_def map_add_def
[PROOF STATE]
proof (prove)
using this:
let k1 = fst (run_state get_k1 m); k2 = fst (run_state get_k2 m) in (\<forall>k\<in>{a. mem1.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>{a. mem2.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> P m

goal (1 subgoal):
 1. \<forall>a\<in>{a. fst (run_state (let k' = key1 a in get_k2 \<bind> (\<lambda>k2. if k' = k2 then lookup2 (key2 a) else get_k1 \<bind> (\<lambda>k1. if k' = k1 then lookup1 (key2 a) else State_Monad.return None))) m) \<noteq> None}. fst (run_state (let k' = key1 a in get_k2 \<bind> (\<lambda>k2. if k' = k2 then lookup2 (key2 a) else get_k1 \<bind> (\<lambda>k1. if k' = k1 then lookup1 (key2 a) else State_Monad.return None))) m) = (case if key1 a = fst (run_state get_k2 m) then mem2.map_of m (key2 a) else None of None \<Rightarrow> if key1 a = fst (run_state get_k1 m) then mem1.map_of m (key2 a) else None | Some x \<Rightarrow> Some x)
[PROOF STEP]
unfolding State_Monad.bind_def
[PROOF STATE]
proof (prove)
using this:
let k1 = fst (run_state get_k1 m); k2 = fst (run_state get_k2 m) in (\<forall>k\<in>{a. mem1.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>{a. mem2.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> P m

goal (1 subgoal):
 1. \<forall>a\<in>{a. fst (run_state (let k' = key1 a in State (\<lambda>s. case run_state get_k2 s of (aa, x) \<Rightarrow> run_state (if k' = aa then lookup2 (key2 a) else State (\<lambda>s. case run_state get_k1 s of (aa, x) \<Rightarrow> run_state (if k' = aa then lookup1 (key2 a) else State_Monad.return None) x)) x)) m) \<noteq> None}. fst (run_state (let k' = key1 a in State (\<lambda>s. case run_state get_k2 s of (aa, x) \<Rightarrow> run_state (if k' = aa then lookup2 (key2 a) else State (\<lambda>s. case run_state get_k1 s of (aa, x) \<Rightarrow> run_state (if k' = aa then lookup1 (key2 a) else State_Monad.return None) x)) x)) m) = (case if key1 a = fst (run_state get_k2 m) then mem2.map_of m (key2 a) else None of None \<Rightarrow> if key1 a = fst (run_state get_k1 m) then mem1.map_of m (key2 a) else None | Some x \<Rightarrow> Some x)
[PROOF STEP]
by (auto 4 4
        simp: mem2.map_of_def mem1.map_of_def Let_def
        dest: get_state split: prod.split_asm if_split_asm
     )


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

goal (1 subgoal):
 1. map_of1 m ++ map_of2 m \<subseteq>\<^sub>m pair.map_of m
[PROOF STEP]
unfolding pair.map_of_def map_of1_def map_of2_def
[PROOF STATE]
proof (prove)
using this:
inv_pair m

goal (1 subgoal):
 1. (\<lambda>k. if key1 k = fst (run_state get_k1 m) then mem1.map_of m (key2 k) else None) ++ (\<lambda>k. if key1 k = fst (run_state get_k2 m) then mem2.map_of m (key2 k) else None) \<subseteq>\<^sub>m (\<lambda>k. fst (run_state (lookup_pair k) m))
[PROOF STEP]
unfolding lookup_pair_def inv_pair_def map_of_def map_le_def dom_def map_add_def
[PROOF STATE]
proof (prove)
using this:
let k1 = fst (run_state get_k1 m); k2 = fst (run_state get_k2 m) in (\<forall>k\<in>{a. mem1.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>{a. mem2.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> P m

goal (1 subgoal):
 1. \<forall>a\<in>{a. (case if key1 a = fst (run_state get_k2 m) then mem2.map_of m (key2 a) else None of None \<Rightarrow> if key1 a = fst (run_state get_k1 m) then mem1.map_of m (key2 a) else None | Some x \<Rightarrow> Some x) \<noteq> None}. (case if key1 a = fst (run_state get_k2 m) then mem2.map_of m (key2 a) else None of None \<Rightarrow> if key1 a = fst (run_state get_k1 m) then mem1.map_of m (key2 a) else None | Some x \<Rightarrow> Some x) = fst (run_state (let k' = key1 a in get_k2 \<bind> (\<lambda>k2. if k' = k2 then lookup2 (key2 a) else get_k1 \<bind> (\<lambda>k1. if k' = k1 then lookup1 (key2 a) else State_Monad.return None))) m)
[PROOF STEP]
unfolding State_Monad.bind_def
[PROOF STATE]
proof (prove)
using this:
let k1 = fst (run_state get_k1 m); k2 = fst (run_state get_k2 m) in (\<forall>k\<in>{a. mem1.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>{a. mem2.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> P m

goal (1 subgoal):
 1. \<forall>a\<in>{a. (case if key1 a = fst (run_state get_k2 m) then mem2.map_of m (key2 a) else None of None \<Rightarrow> if key1 a = fst (run_state get_k1 m) then mem1.map_of m (key2 a) else None | Some x \<Rightarrow> Some x) \<noteq> None}. (case if key1 a = fst (run_state get_k2 m) then mem2.map_of m (key2 a) else None of None \<Rightarrow> if key1 a = fst (run_state get_k1 m) then mem1.map_of m (key2 a) else None | Some x \<Rightarrow> Some x) = fst (run_state (let k' = key1 a in State (\<lambda>s. case run_state get_k2 s of (aa, x) \<Rightarrow> run_state (if k' = aa then lookup2 (key2 a) else State (\<lambda>s. case run_state get_k1 s of (aa, x) \<Rightarrow> run_state (if k' = aa then lookup1 (key2 a) else State_Monad.return None) x)) x)) m)
[PROOF STEP]
by (auto
        simp: mem2.map_of_def mem1.map_of_def State_Monad.run_state_return Let_def
        dest: get_state split: prod.splits if_split_asm option.split
     )


[STATEMENT]
lemma map_of_eq_pair:
  "map_of1 m ++ map_of2 m = pair.map_of m"
  if "inv_pair m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of1 m ++ map_of2 m = pair.map_of m
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inv_pair m

goal (1 subgoal):
 1. map_of1 m ++ map_of2 m = pair.map_of m
[PROOF STEP]
unfolding pair.map_of_def map_of1_def map_of2_def
[PROOF STATE]
proof (prove)
using this:
inv_pair m

goal (1 subgoal):
 1. (\<lambda>k. if key1 k = fst (run_state get_k1 m) then mem1.map_of m (key2 k) else None) ++ (\<lambda>k. if key1 k = fst (run_state get_k2 m) then mem2.map_of m (key2 k) else None) = (\<lambda>k. fst (run_state (lookup_pair k) m))
[PROOF STEP]
unfolding lookup_pair_def inv_pair_def map_of_def map_le_def dom_def map_add_def
[PROOF STATE]
proof (prove)
using this:
let k1 = fst (run_state get_k1 m); k2 = fst (run_state get_k2 m) in (\<forall>k\<in>{a. mem1.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>{a. mem2.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> P m

goal (1 subgoal):
 1. (\<lambda>x. case if key1 x = fst (run_state get_k2 m) then mem2.map_of m (key2 x) else None of None \<Rightarrow> if key1 x = fst (run_state get_k1 m) then mem1.map_of m (key2 x) else None | Some x \<Rightarrow> Some x) = (\<lambda>k. fst (run_state (let k' = key1 k in get_k2 \<bind> (\<lambda>k2. if k' = k2 then lookup2 (key2 k) else get_k1 \<bind> (\<lambda>k1. if k' = k1 then lookup1 (key2 k) else State_Monad.return None))) m))
[PROOF STEP]
unfolding State_Monad.bind_def
[PROOF STATE]
proof (prove)
using this:
let k1 = fst (run_state get_k1 m); k2 = fst (run_state get_k2 m) in (\<forall>k\<in>{a. mem1.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>{a. mem2.map_of m a \<noteq> None}. \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> P m

goal (1 subgoal):
 1. (\<lambda>x. case if key1 x = fst (run_state get_k2 m) then mem2.map_of m (key2 x) else None of None \<Rightarrow> if key1 x = fst (run_state get_k1 m) then mem1.map_of m (key2 x) else None | Some x \<Rightarrow> Some x) = (\<lambda>k. fst (run_state (let k' = key1 k in State (\<lambda>s. case run_state get_k2 s of (a, x) \<Rightarrow> run_state (if k' = a then lookup2 (key2 k) else State (\<lambda>s. case run_state get_k1 s of (a, x) \<Rightarrow> run_state (if k' = a then lookup1 (key2 k) else State_Monad.return None) x)) x)) m))
[PROOF STEP]
by (auto 4 4
        simp: mem2.map_of_def mem1.map_of_def State_Monad.run_state_return Let_def
        dest: get_state split: prod.splits option.split
     )


[STATEMENT]
lemma inv_pair_neq[simp]:
  False if "inv_pair m" "fst (State_Monad.run_state get_k1 m) = fst (State_Monad.run_state get_k2 m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inv_pair m
fst (run_state get_k1 m) = fst (run_state get_k2 m)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
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) = fst (run_state get_k2 m)

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


[STATEMENT]
lemma inv_pair_P_D:
  "P m" if "inv_pair m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P m
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inv_pair m

goal (1 subgoal):
 1. P m
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
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

goal (1 subgoal):
 1. P m
[PROOF STEP]
by (auto simp: Let_def)


[STATEMENT]
lemma inv_pair_domD[intro]:
  "dom (map_of1 m) \<inter> dom (map_of2 m) = {}" if "inv_pair m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (map_of1 m) \<inter> dom (map_of2 m) = {}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inv_pair m

goal (1 subgoal):
 1. dom (map_of1 m) \<inter> dom (map_of2 m) = {}
[PROOF STEP]
unfolding inv_pair_def map_of1_def map_of2_def
[PROOF STATE]
proof (prove)
using this:
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

goal (1 subgoal):
 1. dom (\<lambda>k. if key1 k = fst (run_state get_k1 m) then mem1.map_of m (key2 k) else None) \<inter> dom (\<lambda>k. if key1 k = fst (run_state get_k2 m) then mem2.map_of m (key2 k) else None) = {}
[PROOF STEP]
by (auto split: if_split_asm)


[STATEMENT]
lemma move12_correct1:
  "map_of1 heap' \<subseteq>\<^sub>m Map.empty" if "State_Monad.run_state (move12 k1) heap = (x, heap')" "P heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of1 heap' \<subseteq>\<^sub>m Map.empty
[PROOF STEP]
using move12_correct[OF that(2,1)]
[PROOF STATE]
proof (prove)
using this:
mem1.map_of heap' \<subseteq>\<^sub>m Map.empty
mem2.map_of heap' \<subseteq>\<^sub>m mem1.map_of heap

goal (1 subgoal):
 1. map_of1 heap' \<subseteq>\<^sub>m Map.empty
[PROOF STEP]
unfolding map_of1_def
[PROOF STATE]
proof (prove)
using this:
mem1.map_of heap' \<subseteq>\<^sub>m Map.empty
mem2.map_of heap' \<subseteq>\<^sub>m mem1.map_of heap

goal (1 subgoal):
 1. (\<lambda>k. if key1 k = fst (run_state get_k1 heap') then mem1.map_of heap' (key2 k) else None) \<subseteq>\<^sub>m Map.empty
[PROOF STEP]
by (auto simp: move12_keys map_le_def)


[STATEMENT]
lemma move12_correct2:
  "map_of2 heap' \<subseteq>\<^sub>m map_of1 heap" if "State_Monad.run_state (move12 k1) heap = (x, heap')" "P heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of2 heap' \<subseteq>\<^sub>m map_of1 heap
[PROOF STEP]
using move12_correct(2)[OF that(2,1)] that
[PROOF STATE]
proof (prove)
using this:
mem2.map_of heap' \<subseteq>\<^sub>m mem1.map_of heap
run_state (move12 k1) heap = (x, heap')
P heap

goal (1 subgoal):
 1. map_of2 heap' \<subseteq>\<^sub>m map_of1 heap
[PROOF STEP]
unfolding map_of1_def map_of2_def
[PROOF STATE]
proof (prove)
using this:
mem2.map_of heap' \<subseteq>\<^sub>m mem1.map_of heap
run_state (move12 k1) heap = (x, heap')
P heap

goal (1 subgoal):
 1. (\<lambda>k. if key1 k = fst (run_state get_k2 heap') then mem2.map_of heap' (key2 k) else None) \<subseteq>\<^sub>m (\<lambda>k. if key1 k = fst (run_state get_k1 heap) then mem1.map_of heap (key2 k) else None)
[PROOF STEP]
by (auto simp: move12_keys map_le_def)


[STATEMENT]
lemma dom_empty[simp]:
  "dom (map_of1 heap') = {}" if "State_Monad.run_state (move12 k1) heap = (x, heap')" "P heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (map_of1 heap') = {}
[PROOF STEP]
using move12_correct1[OF that]
[PROOF STATE]
proof (prove)
using this:
map_of1 heap' \<subseteq>\<^sub>m Map.empty

goal (1 subgoal):
 1. dom (map_of1 heap') = {}
[PROOF STEP]
by (auto dest: map_le_implies_dom_le)


[STATEMENT]
lemma inv_pair_lookup1:
  "inv_pair m'" if "State_Monad.run_state (lookup1 k) m = (v, m')" "inv_pair m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_pair m'
[PROOF STEP]
using that lookup_inv[of k] inv_pair_P_D[OF \<open>inv_pair m\<close>]
[PROOF STATE]
proof (prove)
using this:
run_state (lookup1 k) m = (v, m')
inv_pair m
lift_p P (lookup1 k)
lift_p P (lookup2 k)
P m

goal (1 subgoal):
 1. inv_pair m'
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
run_state (lookup1 k) 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
lift_p P (lookup1 k)
lift_p P (lookup2 k)
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]
by (auto 4 4
        simp: Let_def lookup_keys
        dest: lift_p_P lookup_correct[of _ k, THEN map_le_implies_dom_le]
     )


[STATEMENT]
lemma inv_pair_lookup2:
  "inv_pair m'" if "State_Monad.run_state (lookup2 k) m = (v, m')" "inv_pair m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_pair m'
[PROOF STEP]
using that lookup_inv[of k] inv_pair_P_D[OF \<open>inv_pair m\<close>]
[PROOF STATE]
proof (prove)
using this:
run_state (lookup2 k) m = (v, m')
inv_pair m
lift_p P (lookup1 k)
lift_p P (lookup2 k)
P m

goal (1 subgoal):
 1. inv_pair m'
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
run_state (lookup2 k) 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
lift_p P (lookup1 k)
lift_p P (lookup2 k)
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]
by (auto 4 4
        simp: Let_def lookup_keys
        dest: lift_p_P lookup_correct[of _ k, THEN map_le_implies_dom_le]
     )


[STATEMENT]
lemma inv_pair_update2:
  "inv_pair m'"
  if "State_Monad.run_state (update2 (key2 k) v) m = (v', m')" "inv_pair m" "fst (State_Monad.run_state get_k2 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 (update2 (key2 k) v) m = (v', m')
inv_pair m
fst (run_state get_k2 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 (update2 (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_k2 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 (update2 (key2 k) v) m = ((), m'); fst (run_state get_k2 m) = key1 k; lift_p P (update1 (key2 k) v); lift_p P (update2 (key2 k) v); P m; \<forall>k\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = fst (run_state get_k1 m) \<and> key2 k' = k; \<forall>ka\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = key1 k \<and> key2 k' = ka; fst (run_state get_k1 m) \<noteq> key1 k; mem1.map_of m' ka = Some y\<rbrakk> \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state get_k1 m) \<and> key2 k' = ka
 2. \<And>ka y. \<lbrakk>run_state (update2 (key2 k) v) m = ((), m'); fst (run_state get_k2 m) = key1 k; lift_p P (update1 (key2 k) v); lift_p P (update2 (key2 k) v); P m; \<forall>k\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = fst (run_state get_k1 m) \<and> key2 k' = k; \<forall>ka\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = key1 k \<and> key2 k' = ka; fst (run_state get_k1 m) \<noteq> key1 k; mem2.map_of m' ka = Some y\<rbrakk> \<Longrightarrow> \<exists>k'. key1 k' = key1 k \<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 (update2 (key2 k) v) m = ((), m'); fst (run_state get_k2 m) = key1 k; lift_p P (update1 (key2 k) v); lift_p P (update2 (key2 k) v); P m; \<forall>k\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = fst (run_state get_k1 m) \<and> key2 k' = k; \<forall>ka\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = key1 k \<and> key2 k' = ka; fst (run_state get_k1 m) \<noteq> key1 k; mem2.map_of m' ka = Some y\<rbrakk> \<Longrightarrow> \<exists>k'. key1 k' = key1 k \<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


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

goal (1 subgoal):
 1. inv_pair m'
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
run_state (move12 k) 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) \<noteq> k
lift_p P (move12 k)
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 move12_keys
        dest: lift_p_P move12_correct[of _ "k", THEN map_le_implies_dom_le]
     )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ka y. \<lbrakk>run_state (move12 k) m = ((), m'); fst (run_state get_k1 m) \<noteq> k; lift_p P (move12 k); P m; \<forall>k\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = fst (run_state get_k1 m) \<and> key2 k' = k; \<forall>k\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = fst (run_state get_k2 m) \<and> key2 k' = k; fst (run_state get_k1 m) \<noteq> fst (run_state get_k2 m); mem2.map_of m' ka = Some y\<rbrakk> \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state get_k1 m) \<and> key2 k' = ka
[PROOF STEP]
apply (blast dest: move12_correct[of _ "k", THEN map_le_implies_dom_le])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done