[STATEMENT]
lemma
  "precise P1 \<Longrightarrow> precise P2 \<Longrightarrow> precise (prod_assn P1 P2)" \<comment> \<open>Original proof\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>precise P1; precise P2\<rbrakk> \<Longrightarrow> precise (P1 \<times>\<^sub>a P2)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F'. \<lbrakk>precise P1; precise P2; h \<Turnstile> (P1 \<times>\<^sub>a P2) a p * F \<and>\<^sub>A (P1 \<times>\<^sub>a P2) a' p * F'\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
apply (clarsimp simp: prod_assn_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba
[PROOF STEP]
proof (rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
fix F F' h as a b a' b' ap bp
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
assume P1: "precise P1" and P2: "precise P2"
[PROOF STATE]
proof (state)
this:
precise P1
precise P2

goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
assume F: "(h, as) \<Turnstile> P1 a ap * P2 b bp * F \<and>\<^sub>A P1 a' ap * P2 b' bp * F'"
[PROOF STATE]
proof (state)
this:
(h, as) \<Turnstile> P1 a ap * P2 b bp * F \<and>\<^sub>A P1 a' ap * P2 b' bp * F'

goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
from F
[PROOF STATE]
proof (chain)
picking this:
(h, as) \<Turnstile> P1 a ap * P2 b bp * F \<and>\<^sub>A P1 a' ap * P2 b' bp * F'
[PROOF STEP]
have "(h, as) \<Turnstile> P1 a ap * (P2 b bp * F) \<and>\<^sub>A P1 a' ap * (P2 b' bp * F')"
[PROOF STATE]
proof (prove)
using this:
(h, as) \<Turnstile> P1 a ap * P2 b bp * F \<and>\<^sub>A P1 a' ap * P2 b' bp * F'

goal (1 subgoal):
 1. (h, as) \<Turnstile> P1 a ap * (P2 b bp * F) \<and>\<^sub>A P1 a' ap * (P2 b' bp * F')
[PROOF STEP]
by (simp only: mult.assoc)
[PROOF STATE]
proof (state)
this:
(h, as) \<Turnstile> P1 a ap * (P2 b bp * F) \<and>\<^sub>A P1 a' ap * (P2 b' bp * F')

goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
with preciseD[OF P1]
[PROOF STATE]
proof (chain)
picking this:
?h \<Turnstile> P1 ?a ?p * ?F \<and>\<^sub>A P1 ?a' ?p * ?F' \<Longrightarrow> ?a = ?a'
(h, as) \<Turnstile> P1 a ap * (P2 b bp * F) \<and>\<^sub>A P1 a' ap * (P2 b' bp * F')
[PROOF STEP]
show "a=a'"
[PROOF STATE]
proof (prove)
using this:
?h \<Turnstile> P1 ?a ?p * ?F \<and>\<^sub>A P1 ?a' ?p * ?F' \<Longrightarrow> ?a = ?a'
(h, as) \<Turnstile> P1 a ap * (P2 b bp * F) \<and>\<^sub>A P1 a' ap * (P2 b' bp * F')

goal (1 subgoal):
 1. a = a'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = a'

goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
from F
[PROOF STATE]
proof (chain)
picking this:
(h, as) \<Turnstile> P1 a ap * P2 b bp * F \<and>\<^sub>A P1 a' ap * P2 b' bp * F'
[PROOF STEP]
have "(h, as) \<Turnstile> P2 b bp * (P1 a ap * F) \<and>\<^sub>A P2 b' bp * (P1 a' ap * F')"
[PROOF STATE]
proof (prove)
using this:
(h, as) \<Turnstile> P1 a ap * P2 b bp * F \<and>\<^sub>A P1 a' ap * P2 b' bp * F'

goal (1 subgoal):
 1. (h, as) \<Turnstile> P2 b bp * (P1 a ap * F) \<and>\<^sub>A P2 b' bp * (P1 a' ap * F')
[PROOF STEP]
by (simp only: mult.assoc[where 'a=assn] mult.commute[where 'a=assn] mult.left_commute[where 'a=assn])
[PROOF STATE]
proof (state)
this:
(h, as) \<Turnstile> P2 b bp * (P1 a ap * F) \<and>\<^sub>A P2 b' bp * (P1 a' ap * F')

goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * P2 b bc * F \<and>\<^sub>A P1 aa ac * P2 ba bc * F'\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
with preciseD[OF P2]
[PROOF STATE]
proof (chain)
picking this:
?h \<Turnstile> P2 ?a ?p * ?F \<and>\<^sub>A P2 ?a' ?p * ?F' \<Longrightarrow> ?a = ?a'
(h, as) \<Turnstile> P2 b bp * (P1 a ap * F) \<and>\<^sub>A P2 b' bp * (P1 a' ap * F')
[PROOF STEP]
show "b=b'"
[PROOF STATE]
proof (prove)
using this:
?h \<Turnstile> P2 ?a ?p * ?F \<and>\<^sub>A P2 ?a' ?p * ?F' \<Longrightarrow> ?a = ?a'
(h, as) \<Turnstile> P2 b bp * (P1 a ap * F) \<and>\<^sub>A P2 b' bp * (P1 a' ap * F')

goal (1 subgoal):
 1. b = b'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
b = b'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma intf_of_prod_assn[intf_of_assn]:
  assumes "intf_of_assn A TYPE('a)" "intf_of_assn B TYPE('b)"
  shows "intf_of_assn (prod_assn A B) TYPE('a * 'b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intf_of_assn (A \<times>\<^sub>a B) TYPE('a \<times> 'b)
[PROOF STEP]
by simp


[STATEMENT]
lemma pure_prod[constraint_rules]:
  assumes P1: "is_pure P1" and P2: "is_pure P2"
  shows "is_pure (prod_assn P1 P2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure (P1 \<times>\<^sub>a P2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_pure (P1 \<times>\<^sub>a P2)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
is_pure P1
[PROOF STEP]
obtain P1' where P1': "\<And>x x'. P1 x x' = \<up>(P1' x x')"
[PROOF STATE]
proof (prove)
using this:
is_pure P1

goal (1 subgoal):
 1. (\<And>P1'. (\<And>x x'. P1 x x' = \<up> (P1' x x')) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using is_pureE
[PROOF STATE]
proof (prove)
using this:
is_pure P1
\<lbrakk>is_pure ?P; \<And>P'. (\<And>x x'. ?P x x' = \<up> (P' x x')) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>P1'. (\<And>x x'. P1 x x' = \<up> (P1' x x')) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P1 ?x ?x' = \<up> (P1' ?x ?x')

goal (1 subgoal):
 1. is_pure (P1 \<times>\<^sub>a P2)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
is_pure P2
[PROOF STEP]
obtain P2' where P2': "\<And>x x'. P2 x x' = \<up>(P2' x x')"
[PROOF STATE]
proof (prove)
using this:
is_pure P2

goal (1 subgoal):
 1. (\<And>P2'. (\<And>x x'. P2 x x' = \<up> (P2' x x')) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using is_pureE
[PROOF STATE]
proof (prove)
using this:
is_pure P2
\<lbrakk>is_pure ?P; \<And>P'. (\<And>x x'. ?P x x' = \<up> (P' x x')) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>P2'. (\<And>x x'. P2 x x' = \<up> (P2' x x')) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P2 ?x ?x' = \<up> (P2' ?x ?x')

goal (1 subgoal):
 1. is_pure (P1 \<times>\<^sub>a P2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure (P1 \<times>\<^sub>a P2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x x'. (P1 \<times>\<^sub>a P2) x x' = \<up> (?P' x x')
[PROOF STEP]
fix x x'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x x'. (P1 \<times>\<^sub>a P2) x x' = \<up> (?P' x x')
[PROOF STEP]
show "prod_assn P1 P2 x x' =
         \<up> (case (x, x') of ((a1, a2), c1, c2) \<Rightarrow> P1' a1 c1 \<and> P2' a2 c2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P1 \<times>\<^sub>a P2) x x' = \<up> (case (x, x') of ((a1, a2), c1, c2) \<Rightarrow> P1' a1 c1 \<and> P2' a2 c2)
[PROOF STEP]
unfolding prod_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (x, x') of ((a1, a2), c1, c2) \<Rightarrow> P1 a1 c1 * P2 a2 c2) = \<up> (case (x, x') of ((a1, a2), c1, c2) \<Rightarrow> P1' a1 c1 \<and> P2' a2 c2)
[PROOF STEP]
apply (simp add: P1' P2' split: prod.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(P1 \<times>\<^sub>a P2) x x' = \<up> (case (x, x') of ((a1, a2), c1, c2) \<Rightarrow> P1' a1 c1 \<and> P2' a2 c2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_pure (P1 \<times>\<^sub>a P2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prod_frame_match[sepref_frame_match_rules]:
  assumes "hn_ctxt A (fst x) (fst y) \<Longrightarrow>\<^sub>t hn_ctxt A' (fst x) (fst y)"
  assumes "hn_ctxt B (snd x) (snd y) \<Longrightarrow>\<^sub>t hn_ctxt B' (snd x) (snd y)"
  shows "hn_ctxt (prod_assn A B) x y \<Longrightarrow>\<^sub>t hn_ctxt (prod_assn A' B') x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (A \<times>\<^sub>a B) x y \<Longrightarrow>\<^sub>t hn_ctxt (A' \<times>\<^sub>a B') x y
[PROOF STEP]
apply (cases x; cases y; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>x = (a, b); y = (aa, ba)\<rbrakk> \<Longrightarrow> hn_ctxt (A \<times>\<^sub>a B) (a, b) (aa, ba) \<Longrightarrow>\<^sub>t hn_ctxt (A' \<times>\<^sub>a B') (a, b) (aa, ba)
[PROOF STEP]
apply (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>x = (a, b); y = (aa, ba)\<rbrakk> \<Longrightarrow> A a aa * B b ba \<Longrightarrow>\<^sub>t A' a aa * B' b ba
[PROOF STEP]
apply (rule entt_star_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>x = (a, b); y = (aa, ba)\<rbrakk> \<Longrightarrow> A a aa \<Longrightarrow>\<^sub>t A' a aa
 2. \<And>a b aa ba. \<lbrakk>x = (a, b); y = (aa, ba)\<rbrakk> \<Longrightarrow> B b ba \<Longrightarrow>\<^sub>t B' b ba
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hn_ctxt A (fst x) (fst y) \<Longrightarrow>\<^sub>t hn_ctxt A' (fst x) (fst y)
hn_ctxt B (snd x) (snd y) \<Longrightarrow>\<^sub>t hn_ctxt B' (snd x) (snd y)

goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>x = (a, b); y = (aa, ba)\<rbrakk> \<Longrightarrow> A a aa \<Longrightarrow>\<^sub>t A' a aa
 2. \<And>a b aa ba. \<lbrakk>x = (a, b); y = (aa, ba)\<rbrakk> \<Longrightarrow> B b ba \<Longrightarrow>\<^sub>t B' b ba
[PROOF STEP]
apply (auto simp: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_frame_merge[sepref_frame_merge_rules]:
  assumes "hn_ctxt A (fst x) (fst y) \<or>\<^sub>A hn_ctxt A' (fst x) (fst y) \<Longrightarrow>\<^sub>t hn_ctxt Am (fst x) (fst y)"
  assumes "hn_ctxt B (snd x) (snd y) \<or>\<^sub>A hn_ctxt B' (snd x) (snd y) \<Longrightarrow>\<^sub>t hn_ctxt Bm (snd x) (snd y)"
  shows "hn_ctxt (prod_assn A B) x y \<or>\<^sub>A hn_ctxt (prod_assn A' B') x y \<Longrightarrow>\<^sub>t hn_ctxt (prod_assn Am Bm) x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (A \<times>\<^sub>a B) x y \<or>\<^sub>A hn_ctxt (A' \<times>\<^sub>a B') x y \<Longrightarrow>\<^sub>t hn_ctxt (Am \<times>\<^sub>a Bm) x y
[PROOF STEP]
by (blast intro: entt_disjE prod_frame_match
    entt_disjD1[OF assms(1)] entt_disjD2[OF assms(1)]
    entt_disjD1[OF assms(2)] entt_disjD2[OF assms(2)])


[STATEMENT]
lemma entt_invalid_prod: "hn_invalid (prod_assn A B) p p' \<Longrightarrow>\<^sub>t hn_ctxt (prod_assn (invalid_assn A) (invalid_assn B)) p p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_invalid (A \<times>\<^sub>a B) p p' \<Longrightarrow>\<^sub>t hn_ctxt (invalid_assn A \<times>\<^sub>a invalid_assn B) p p'
[PROOF STEP]
apply (simp add: hn_ctxt_def invalid_assn_def[abs_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up> (\<exists>a b. (a, b) \<Turnstile> (A \<times>\<^sub>a B) p p') \<Longrightarrow>\<^sub>t ((\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> A x y) * true) \<times>\<^sub>a (\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> B x y) * true)) p p'
[PROOF STEP]
apply (rule enttI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up> (\<exists>a b. (a, b) \<Turnstile> (A \<times>\<^sub>a B) p p') \<Longrightarrow>\<^sub>A ((\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> A x y) * true) \<times>\<^sub>a (\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> B x y) * true)) p p' * true
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<Turnstile> (A \<times>\<^sub>a B) p p' \<Longrightarrow> emp \<Longrightarrow>\<^sub>A ((\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> A x y) * true) \<times>\<^sub>a (\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> B x y) * true)) p p' * true
[PROOF STEP]
apply (cases p; cases p'; auto simp: mod_star_conv pure_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_assn_ctxt: "prod_assn A1 A2 x y = z \<Longrightarrow> hn_ctxt (prod_assn A1 A2) x y = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A1 \<times>\<^sub>a A2) x y = z \<Longrightarrow> hn_ctxt (A1 \<times>\<^sub>a A2) x y = z
[PROOF STEP]
by (simp add: hn_ctxt_def)


[STATEMENT]
lemma hn_case_prod'[sepref_prep_comb_rule,sepref_comb_rules]:
  assumes FR: "\<Gamma>\<Longrightarrow>\<^sub>thn_ctxt (prod_assn P1 P2) p' p * \<Gamma>1"
  assumes Pair: "\<And>a1 a2 a1' a2'. \<lbrakk>p'=(a1',a2')\<rbrakk>
    \<Longrightarrow> hn_refine (hn_ctxt P1 a1' a1 * hn_ctxt P2 a2' a2 * \<Gamma>1 * hn_invalid (prod_assn P1 P2) p' p) (f a1 a2)
          (hn_ctxt P1' a1' a1 * hn_ctxt P2' a2' a2 * hn_ctxt XX1 p' p * \<Gamma>1') R (f' a1' a2')"
  shows "hn_refine \<Gamma> (case_prod f p) (hn_ctxt (prod_assn P1' P2') p' p * \<Gamma>1')
    R (case_prod$(\<lambda>\<^sub>2a b. f' a b)$p')" (is "?G \<Gamma>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine \<Gamma> (case p of (x, xa) \<Rightarrow> f x xa) (hn_ctxt (P1' \<times>\<^sub>a P2') p' p * \<Gamma>1') R (case_prod $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ p')
[PROOF STEP]
apply1 (rule hn_refine_cons_pre[OF FR])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt (P1 \<times>\<^sub>a P2) p' p * \<Gamma>1) (case p of (x, xa) \<Rightarrow> f x xa) (hn_ctxt (P1' \<times>\<^sub>a P2') p' p * \<Gamma>1') R (case_prod $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ p')
[PROOF STEP]
apply1 extract_hnr_invalids
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1 h2. \<lbrakk>h2 \<Turnstile> \<Gamma>1; hn_invalid (P1 \<times>\<^sub>a P2) p' p = true\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (P1 \<times>\<^sub>a P2) p' p * \<Gamma>1) (case p of (x, xa) \<Rightarrow> f x xa) (hn_ctxt (P1' \<times>\<^sub>a P2') p' p * \<Gamma>1') R (case_prod $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ p')
[PROOF STEP]
apply1 (cases p; cases p'; simp add: prod_assn_pair_conv[THEN prod_assn_ctxt])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h2 a b aa ba. \<lbrakk>h2 \<Turnstile> \<Gamma>1; hn_invalid (P1 \<times>\<^sub>a P2) (aa, ba) (a, b) = true; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> hn_refine (P1 aa a * P2 ba b * \<Gamma>1) (f a b) (P1' aa a * P2' ba b * \<Gamma>1') R (f' aa ba)
[PROOF STEP]
apply (rule hn_refine_cons[OF _ Pair _ entt_refl])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>h2 a b aa ba. \<lbrakk>h2 \<Turnstile> \<Gamma>1; hn_invalid (P1 \<times>\<^sub>a P2) (aa, ba) (a, b) = true; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> P1 aa a * P2 ba b * \<Gamma>1 \<Longrightarrow>\<^sub>t hn_ctxt P1 aa a * hn_ctxt P2 ba b * \<Gamma>1 * hn_invalid (P1 \<times>\<^sub>a P2) p' p
 2. \<And>h2 a b aa ba. \<lbrakk>h2 \<Turnstile> \<Gamma>1; hn_invalid (P1 \<times>\<^sub>a P2) (aa, ba) (a, b) = true; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> p' = (aa, ba)
 3. \<And>h2 a b aa ba. \<lbrakk>h2 \<Turnstile> \<Gamma>1; hn_invalid (P1 \<times>\<^sub>a P2) (aa, ba) (a, b) = true; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> hn_ctxt P1' aa a * hn_ctxt P2' ba b * hn_ctxt XX1 p' p * \<Gamma>1' \<Longrightarrow>\<^sub>t P1' aa a * P2' ba b * \<Gamma>1'
[PROOF STEP]
applyS (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>h2 a b aa ba. \<lbrakk>h2 \<Turnstile> \<Gamma>1; hn_invalid (P1 \<times>\<^sub>a P2) (aa, ba) (a, b) = true; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> p' = (aa, ba)
 2. \<And>h2 a b aa ba. \<lbrakk>h2 \<Turnstile> \<Gamma>1; hn_invalid (P1 \<times>\<^sub>a P2) (aa, ba) (a, b) = true; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> hn_ctxt P1' aa a * hn_ctxt P2' ba b * hn_ctxt XX1 p' p * \<Gamma>1' \<Longrightarrow>\<^sub>t P1' aa a * P2' ba b * \<Gamma>1'
[PROOF STEP]
applyS simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h2 a b aa ba. \<lbrakk>h2 \<Turnstile> \<Gamma>1; hn_invalid (P1 \<times>\<^sub>a P2) (aa, ba) (a, b) = true; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> hn_ctxt P1' aa a * hn_ctxt P2' ba b * hn_ctxt XX1 p' p * \<Gamma>1' \<Longrightarrow>\<^sub>t P1' aa a * P2' ba b * \<Gamma>1'
[PROOF STEP]
applyS (simp add: hn_ctxt_def entt_fr_refl entt_fr_drop)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hn_case_prod_old:
  assumes P: "\<Gamma>\<Longrightarrow>\<^sub>t\<Gamma>1 * hn_ctxt (prod_assn P1 P2) p' p"
  assumes R: "\<And>a1 a2 a1' a2'. \<lbrakk>p'=(a1',a2')\<rbrakk>
    \<Longrightarrow> hn_refine (\<Gamma>1 * hn_ctxt P1 a1' a1 * hn_ctxt P2 a2' a2 * hn_invalid (prod_assn P1 P2) p' p) (f a1 a2)
          (\<Gamma>h a1 a1' a2 a2') R (f' a1' a2')"
  assumes M: "\<And>a1 a1' a2 a2'. \<Gamma>h a1 a1' a2 a2'
    \<Longrightarrow>\<^sub>t \<Gamma>' * hn_ctxt P1' a1' a1 * hn_ctxt P2' a2' a2 * hn_ctxt Pxx p' p"
  shows "hn_refine \<Gamma> (case_prod f p) (\<Gamma>' * hn_ctxt (prod_assn P1' P2') p' p)
    R (case_prod$(\<lambda>\<^sub>2a b. f' a b)$p')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine \<Gamma> (case p of (x, xa) \<Rightarrow> f x xa) (\<Gamma>' * hn_ctxt (P1' \<times>\<^sub>a P2') p' p) R (case_prod $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ p')
[PROOF STEP]
apply1 (cases p; cases p'; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> hn_refine \<Gamma> (f a b) (\<Gamma>' * hn_ctxt (P1' \<times>\<^sub>a P2') (aa, ba) (a, b)) R (f' aa ba)
[PROOF STEP]
apply1 (rule hn_refine_cons_pre[OF P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> hn_refine (\<Gamma>1 * hn_ctxt (P1 \<times>\<^sub>a P2) p' p) (f a b) (\<Gamma>' * hn_ctxt (P1' \<times>\<^sub>a P2') (aa, ba) (a, b)) R (f' aa ba)
[PROOF STEP]
apply (rule hn_refine_preI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * hn_ctxt (P1 \<times>\<^sub>a P2) p' p\<rbrakk> \<Longrightarrow> hn_refine (\<Gamma>1 * hn_ctxt (P1 \<times>\<^sub>a P2) p' p) (f a b) (\<Gamma>' * hn_ctxt (P1' \<times>\<^sub>a P2') (aa, ba) (a, b)) R (f' aa ba)
[PROOF STEP]
apply (simp add: hn_ctxt_def assn_aci)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> hn_refine (\<Gamma>1 * P1 aa a * P2 ba b) (f a b) (\<Gamma>' * P1' aa a * P2' ba b) R (f' aa ba)
[PROOF STEP]
apply (rule hn_refine_cons[OF _ R])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> \<Gamma>1 * P1 aa a * P2 ba b \<Longrightarrow>\<^sub>t \<Gamma>1 * hn_ctxt P1 aa a * hn_ctxt P2 ba b * hn_invalid (P1 \<times>\<^sub>a P2) p' p
 2. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> p' = (aa, ba)
 3. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> \<Gamma>h a aa b ba \<Longrightarrow>\<^sub>t \<Gamma>' * P1' aa a * P2' ba b
 4. \<And>a b aa ba h x y. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> R x y \<Longrightarrow>\<^sub>t R x y
[PROOF STEP]
apply1 (rule enttI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> \<Gamma>1 * P1 aa a * P2 ba b \<Longrightarrow>\<^sub>A \<Gamma>1 * hn_ctxt P1 aa a * hn_ctxt P2 ba b * hn_invalid (P1 \<times>\<^sub>a P2) p' p * true
 2. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> p' = (aa, ba)
 3. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> \<Gamma>h a aa b ba \<Longrightarrow>\<^sub>t \<Gamma>' * P1' aa a * P2' ba b
 4. \<And>a b aa ba h x y. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> R x y \<Longrightarrow>\<^sub>t R x y
[PROOF STEP]
applyS (sep_auto simp add: hn_ctxt_def invalid_assn_def mod_star_conv)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> p' = (aa, ba)
 2. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> \<Gamma>h a aa b ba \<Longrightarrow>\<^sub>t \<Gamma>' * P1' aa a * P2' ba b
 3. \<And>a b aa ba h x y. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> R x y \<Longrightarrow>\<^sub>t R x y
[PROOF STEP]
applyS simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> \<Gamma>h a aa b ba \<Longrightarrow>\<^sub>t \<Gamma>' * P1' aa a * P2' ba b
 2. \<And>a b aa ba h x y. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> R x y \<Longrightarrow>\<^sub>t R x y
[PROOF STEP]
apply1 (rule entt_trans[OF M])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba h. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> \<Gamma>' * hn_ctxt P1' aa a * hn_ctxt P2' ba b * hn_ctxt Pxx p' p \<Longrightarrow>\<^sub>t \<Gamma>' * P1' aa a * P2' ba b
 2. \<And>a b aa ba h x y. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> R x y \<Longrightarrow>\<^sub>t R x y
[PROOF STEP]
applyS (sep_auto intro!: enttI simp: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba h x y. \<lbrakk>p = (a, b); p' = (aa, ba); h \<Turnstile> \<Gamma>1 * P1 aa a * P2 ba b\<rbrakk> \<Longrightarrow> R x y \<Longrightarrow>\<^sub>t R x y
[PROOF STEP]
applyS simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hn_Pair[sepref_fr_rules]: "hn_refine
  (hn_ctxt P1 x1 x1' * hn_ctxt P2 x2 x2')
  (return (x1',x2'))
  (hn_invalid P1 x1 x1' * hn_invalid P2 x2 x2')
  (prod_assn P1 P2)
  (RETURN$(Pair$x1$x2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt P1 x1 x1' * hn_ctxt P2 x2 x2') (return (x1', x2')) (hn_invalid P1 x1 x1' * hn_invalid P2 x2 x2') (P1 \<times>\<^sub>a P2) (RETURN $ (Pair $ x1 $ x2))
[PROOF STEP]
unfolding hn_refine_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (RETURN $ (Pair $ x1 $ x2)) \<longrightarrow> <hn_ctxt P1 x1 x1' * hn_ctxt P2 x2 x2'> return (x1', x2') <\<lambda>r. hn_invalid P1 x1 x1' * hn_invalid P2 x2 x2' * (\<exists>\<^sub>Ax. (P1 \<times>\<^sub>a P2) x r * \<up> (RETURN x \<le> RETURN $ (Pair $ x1 $ x2)))>\<^sub>t
[PROOF STEP]
apply (sep_auto simp: hn_ctxt_def prod_assn_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P1 x1 x1' * P2 x2 x2' \<Longrightarrow>\<^sub>A invalid_assn P1 x1 x1' * invalid_assn P2 x2 x2' * P1 x1 x1' * P2 x2 x2' * true
[PROOF STEP]
apply (rule ent_frame_fwd[OF invalidate_clone'[of P1]], frame_inference)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invalid_assn P1 x1 x1' * P1 x1 x1' * true * P2 x2 x2' \<Longrightarrow>\<^sub>A invalid_assn P1 x1 x1' * invalid_assn P2 x2 x2' * P1 x1 x1' * P2 x2 x2' * true
[PROOF STEP]
apply (rule ent_frame_fwd[OF invalidate_clone'[of P2]], frame_inference)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invalid_assn P2 x2 x2' * P2 x2 x2' * true * (invalid_assn P1 x1 x1' * P1 x1 x1' * true) \<Longrightarrow>\<^sub>A invalid_assn P1 x1 x1' * invalid_assn P2 x2 x2' * P1 x1 x1' * P2 x2 x2' * true
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fst_hnr[sepref_fr_rules]: "(return o fst,RETURN o fst) \<in> (prod_assn A B)\<^sup>d \<rightarrow>\<^sub>a A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> fst, RETURN \<circ> fst) \<in> (A \<times>\<^sub>a B)\<^sup>d \<rightarrow>\<^sub>a A
[PROOF STEP]
by sepref_to_hoare sep_auto


[STATEMENT]
lemma snd_hnr[sepref_fr_rules]: "(return o snd,RETURN o snd) \<in> (prod_assn A B)\<^sup>d \<rightarrow>\<^sub>a B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> snd, RETURN \<circ> snd) \<in> (A \<times>\<^sub>a B)\<^sup>d \<rightarrow>\<^sub>a B
[PROOF STEP]
by sepref_to_hoare sep_auto


[STATEMENT]
lemma rdomp_prodD[dest!]: "rdomp (prod_assn A B) (a,b) \<Longrightarrow> rdomp A a \<and> rdomp B b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdomp (A \<times>\<^sub>a B) (a, b) \<Longrightarrow> rdomp A a \<and> rdomp B b
[PROOF STEP]
unfolding rdomp_def prod_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>h c. h \<Turnstile> (case ((a, b), c) of ((a1, a2), c1, c2) \<Rightarrow> A a1 c1 * B a2 c2) \<Longrightarrow> (\<exists>h c. h \<Turnstile> A a c) \<and> (\<exists>h c. h \<Turnstile> B b c)
[PROOF STEP]
by (sep_auto simp: mod_star_conv)


[STATEMENT]
lemma option_assn_simps[simp]:
  "option_assn P None v' = \<up>(v'=None)"
  "option_assn P v None = \<up>(v=None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. option_assn P None v' = \<up> (v' = None) &&& option_assn P v None = \<up> (v = None)
[PROOF STEP]
apply (cases v', simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. option_assn P v None = \<up> (v = None)
[PROOF STEP]
apply (cases v, simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma option_assn_alt_def: "option_assn R a b =
  (case (a,b) of (Some x, Some y) \<Rightarrow> R x y
  | (None,None) \<Rightarrow> emp
  | _ \<Rightarrow> false)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. option_assn R a b = (case (a, b) of (None, None) \<Rightarrow> emp | (None, Some a) \<Rightarrow> false | (Some x, None) \<Rightarrow> false | (Some x, Some y) \<Rightarrow> R x y)
[PROOF STEP]
by (auto split: option.split)


[STATEMENT]
lemma option_assn_pure_conv[constraint_simps]: "option_assn (pure R) = pure (\<langle>R\<rangle>option_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. option_assn (pure R) = pure (\<langle>R\<rangle>option_rel)
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. option_assn (pure R) x xa = pure (\<langle>R\<rangle>option_rel) x xa
[PROOF STEP]
apply (rename_tac a c)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a c. option_assn (pure R) a c = pure (\<langle>R\<rangle>option_rel) a c
[PROOF STEP]
apply (case_tac "(pure R,a,c)" rule: option_assn.cases)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a c P. (pure R, a, c) = (P, None, None) \<Longrightarrow> option_assn (pure R) a c = pure (\<langle>R\<rangle>option_rel) a c
 2. \<And>a c P aa ca. (pure R, a, c) = (P, Some aa, Some ca) \<Longrightarrow> option_assn (pure R) a c = pure (\<langle>R\<rangle>option_rel) a c
 3. \<And>a c uu_ v. (pure R, a, c) = (uu_, Some v, None) \<Longrightarrow> option_assn (pure R) a c = pure (\<langle>R\<rangle>option_rel) a c
 4. \<And>a c uu_ v. (pure R, a, c) = (uu_, None, Some v) \<Longrightarrow> option_assn (pure R) a c = pure (\<langle>R\<rangle>option_rel) a c
[PROOF STEP]
by (auto simp: pure_def)


[STATEMENT]
lemma hr_comp_option_conv[simp, fcomp_norm_unfold]: "
  hr_comp (option_assn R) (\<langle>R'\<rangle>option_rel)
  = option_assn (hr_comp R R')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hr_comp (option_assn R) (\<langle>R'\<rangle>option_rel) = option_assn (hr_comp R R')
[PROOF STEP]
unfolding hr_comp_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a c. \<exists>\<^sub>Ab. option_assn R b c * \<up> ((b, a) \<in> \<langle>R'\<rangle>option_rel)) = option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R'))
[PROOF STEP]
apply (intro ext ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a c. \<exists>\<^sub>Ab. option_assn R b c * \<up> ((b, a) \<in> \<langle>R'\<rangle>option_rel) \<Longrightarrow>\<^sub>A option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a c
 2. \<And>a c. option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a c \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. option_assn R b c * \<up> ((b, a) \<in> \<langle>R'\<rangle>option_rel)
[PROOF STEP]
apply solve_entails
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a c b. (b, a) \<in> \<langle>R'\<rangle>option_rel \<Longrightarrow> option_assn R b c \<Longrightarrow>\<^sub>A option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a c
 2. \<And>a c. option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a c \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. option_assn R b c * \<up> ((b, a) \<in> \<langle>R'\<rangle>option_rel)
[PROOF STEP]
apply (case_tac "(R,b,c)" rule: option_assn.cases)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a c b P. \<lbrakk>(b, a) \<in> \<langle>R'\<rangle>option_rel; (R, b, c) = (P, None, None)\<rbrakk> \<Longrightarrow> option_assn R b c \<Longrightarrow>\<^sub>A option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a c
 2. \<And>a c b P aa ca. \<lbrakk>(b, a) \<in> \<langle>R'\<rangle>option_rel; (R, b, c) = (P, Some aa, Some ca)\<rbrakk> \<Longrightarrow> option_assn R b c \<Longrightarrow>\<^sub>A option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a c
 3. \<And>a c b uu_ v. \<lbrakk>(b, a) \<in> \<langle>R'\<rangle>option_rel; (R, b, c) = (uu_, Some v, None)\<rbrakk> \<Longrightarrow> option_assn R b c \<Longrightarrow>\<^sub>A option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a c
 4. \<And>a c b uu_ v. \<lbrakk>(b, a) \<in> \<langle>R'\<rangle>option_rel; (R, b, c) = (uu_, None, Some v)\<rbrakk> \<Longrightarrow> option_assn R b c \<Longrightarrow>\<^sub>A option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a c
 5. \<And>a c. option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a c \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. option_assn R b c * \<up> ((b, a) \<in> \<langle>R'\<rangle>option_rel)
[PROOF STEP]
apply clarsimp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ca. (Some aa, a) \<in> \<langle>R'\<rangle>option_rel \<Longrightarrow> R aa ca \<Longrightarrow>\<^sub>A option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a (Some ca)
 2. \<And>a c. option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a c \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. option_assn R b c * \<up> ((b, a) \<in> \<langle>R'\<rangle>option_rel)
[PROOF STEP]
apply (sep_auto simp: option_assn_alt_def split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a c. option_assn (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> R')) a c \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. option_assn R b c * \<up> ((b, a) \<in> \<langle>R'\<rangle>option_rel)
[PROOF STEP]
apply (clarsimp simp: option_assn_alt_def split: option.splits; safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a c. emp \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. (case b of None \<Rightarrow> emp | Some x \<Rightarrow> case None of None \<Rightarrow> false | Some xa \<Rightarrow> R x xa) * \<up> (b = None)
 2. \<And>a c x2 x2a. \<exists>\<^sub>Ab. R b x2 * \<up> ((b, x2a) \<in> R') \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. (case b of None \<Rightarrow> false | Some x \<Rightarrow> case Some x2 of None \<Rightarrow> false | Some xa \<Rightarrow> R x xa) * \<up> ((b, Some x2a) \<in> \<langle>R'\<rangle>option_rel)
[PROOF STEP]
apply (sep_auto split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a c x2 x2a. \<exists>\<^sub>Ab. R b x2 * \<up> ((b, x2a) \<in> R') \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. (case b of None \<Rightarrow> false | Some x \<Rightarrow> case Some x2 of None \<Rightarrow> false | Some xa \<Rightarrow> R x xa) * \<up> ((b, Some x2a) \<in> \<langle>R'\<rangle>option_rel)
[PROOF STEP]
apply (intro ent_ex_preI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a c x2 x2a b. R b x2 * \<up> ((b, x2a) \<in> R') \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. (case b of None \<Rightarrow> false | Some x \<Rightarrow> case Some x2 of None \<Rightarrow> false | Some xa \<Rightarrow> R x xa) * \<up> ((b, Some x2a) \<in> \<langle>R'\<rangle>option_rel)
[PROOF STEP]
apply (rule ent_ex_postI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a c x2 x2a b. R b x2 * \<up> ((b, x2a) \<in> R') \<Longrightarrow>\<^sub>A (case ?b70 a c x2 x2a b of None \<Rightarrow> false | Some x \<Rightarrow> case Some x2 of None \<Rightarrow> false | Some xa \<Rightarrow> R x xa) * \<up> ((?b70 a c x2 x2a b, Some x2a) \<in> \<langle>R'\<rangle>option_rel)
[PROOF STEP]
apply (sep_auto split: option.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma option_assn_precise[safe_constraint_rules]:
  assumes "precise P"
  shows "precise (option_assn P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise (option_assn P)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a' h p F F'. h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F' \<Longrightarrow> a = a'
[PROOF STEP]
fix a a' p h F F'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a' h p F F'. h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F' \<Longrightarrow> a = a'
[PROOF STEP]
assume A: "h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'"
[PROOF STATE]
proof (state)
this:
h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'

goal (1 subgoal):
 1. \<And>a a' h p F F'. h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F' \<Longrightarrow> a = a'
[PROOF STEP]
thus "a=a'"
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'

goal (1 subgoal):
 1. a = a'
[PROOF STEP]
proof (cases "(P,a,p)" rule: option_assn.cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>Pa. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, None, None)\<rbrakk> \<Longrightarrow> a = a'
 2. \<And>Pa aa c. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, Some aa, Some c)\<rbrakk> \<Longrightarrow> a = a'
 3. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, Some v, None)\<rbrakk> \<Longrightarrow> a = a'
 4. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, None, Some v)\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
case (2 _ av pv)
[PROOF STATE]
proof (state)
this:
(P, a, p) = (P_, Some av, Some pv)

goal (4 subgoals):
 1. \<And>Pa. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, None, None)\<rbrakk> \<Longrightarrow> a = a'
 2. \<And>Pa aa c. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, Some aa, Some c)\<rbrakk> \<Longrightarrow> a = a'
 3. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, Some v, None)\<rbrakk> \<Longrightarrow> a = a'
 4. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, None, Some v)\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
hence [simp]: "a=Some av" "p=Some pv"
[PROOF STATE]
proof (prove)
using this:
(P, a, p) = (P_, Some av, Some pv)

goal (1 subgoal):
 1. a = Some av &&& p = Some pv
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a = Some av
p = Some pv

goal (4 subgoals):
 1. \<And>Pa. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, None, None)\<rbrakk> \<Longrightarrow> a = a'
 2. \<And>Pa aa c. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, Some aa, Some c)\<rbrakk> \<Longrightarrow> a = a'
 3. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, Some v, None)\<rbrakk> \<Longrightarrow> a = a'
 4. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, None, Some v)\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'
[PROOF STEP]
obtain av' where [simp]: "a'=Some av'"
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'

goal (1 subgoal):
 1. (\<And>av'. a' = Some av' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases a', simp_all)
[PROOF STATE]
proof (state)
this:
a' = Some av'

goal (4 subgoals):
 1. \<And>Pa. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, None, None)\<rbrakk> \<Longrightarrow> a = a'
 2. \<And>Pa aa c. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, Some aa, Some c)\<rbrakk> \<Longrightarrow> a = a'
 3. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, Some v, None)\<rbrakk> \<Longrightarrow> a = a'
 4. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, None, Some v)\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'
[PROOF STEP]
have "h \<Turnstile> P av pv * F \<and>\<^sub>A P av' pv * F'"
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'

goal (1 subgoal):
 1. h \<Turnstile> P av pv * F \<and>\<^sub>A P av' pv * F'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h \<Turnstile> P av pv * F \<and>\<^sub>A P av' pv * F'

goal (4 subgoals):
 1. \<And>Pa. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, None, None)\<rbrakk> \<Longrightarrow> a = a'
 2. \<And>Pa aa c. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, Some aa, Some c)\<rbrakk> \<Longrightarrow> a = a'
 3. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, Some v, None)\<rbrakk> \<Longrightarrow> a = a'
 4. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, None, Some v)\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
with \<open>precise P\<close>
[PROOF STATE]
proof (chain)
picking this:
precise P
h \<Turnstile> P av pv * F \<and>\<^sub>A P av' pv * F'
[PROOF STEP]
have "av=av'"
[PROOF STATE]
proof (prove)
using this:
precise P
h \<Turnstile> P av pv * F \<and>\<^sub>A P av' pv * F'

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

goal (4 subgoals):
 1. \<And>Pa. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, None, None)\<rbrakk> \<Longrightarrow> a = a'
 2. \<And>Pa aa c. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, Some aa, Some c)\<rbrakk> \<Longrightarrow> a = a'
 3. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, Some v, None)\<rbrakk> \<Longrightarrow> a = a'
 4. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, None, Some v)\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
av = av'

goal (1 subgoal):
 1. a = a'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a = a'

goal (3 subgoals):
 1. \<And>Pa. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (Pa, None, None)\<rbrakk> \<Longrightarrow> a = a'
 2. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, Some v, None)\<rbrakk> \<Longrightarrow> a = a'
 3. \<And>uu_ v. \<lbrakk>h \<Turnstile> option_assn P a p * F \<and>\<^sub>A option_assn P a' p * F'; (P, a, p) = (uu_, None, Some v)\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
a = a'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pure_option[safe_constraint_rules]:
  assumes P: "is_pure P"
  shows "is_pure (option_assn P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure (option_assn P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_pure (option_assn P)
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
is_pure P
[PROOF STEP]
obtain P' where P': "\<And>x x'. P x x' = \<up>(P' x x')"
[PROOF STATE]
proof (prove)
using this:
is_pure P

goal (1 subgoal):
 1. (\<And>P'. (\<And>x x'. P x x' = \<up> (P' x x')) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using is_pureE
[PROOF STATE]
proof (prove)
using this:
is_pure P
\<lbrakk>is_pure ?P; \<And>P'. (\<And>x x'. ?P x x' = \<up> (P' x x')) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>P'. (\<And>x x'. P x x' = \<up> (P' x x')) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P ?x ?x' = \<up> (P' ?x ?x')

goal (1 subgoal):
 1. is_pure (option_assn P)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure (option_assn P)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x x'. option_assn P x x' = \<up> (?P' x x')
[PROOF STEP]
fix x x'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x x'. option_assn P x x' = \<up> (?P' x x')
[PROOF STEP]
show "option_assn P x x' =
         \<up> (case (x, x') of
             (None,None) \<Rightarrow> True | (Some v, Some v') \<Rightarrow> P' v v' | _ \<Rightarrow> False
           )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. option_assn P x x' = \<up> (case (x, x') of (None, None) \<Rightarrow> True | (None, Some a) \<Rightarrow> False | (Some v, None) \<Rightarrow> False | (Some v, Some v') \<Rightarrow> P' v v')
[PROOF STEP]
apply (simp add: P' split: prod.split option.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
option_assn P x x' = \<up> (case (x, x') of (None, None) \<Rightarrow> True | (None, Some a) \<Rightarrow> False | (Some v, None) \<Rightarrow> False | (Some v, Some v') \<Rightarrow> P' v v')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_pure (option_assn P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hn_ctxt_option: "option_assn A x y = z \<Longrightarrow> hn_ctxt (option_assn A) x y = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. option_assn A x y = z \<Longrightarrow> hn_ctxt (option_assn A) x y = z
[PROOF STEP]
by (simp add: hn_ctxt_def)


[STATEMENT]
lemma hn_case_option[sepref_prep_comb_rule, sepref_comb_rules]:
  fixes p p' P
  defines [simp]: "INVE \<equiv> hn_invalid (option_assn P) p p'"
  assumes FR: "\<Gamma> \<Longrightarrow>\<^sub>t hn_ctxt (option_assn P) p p' * F"
  assumes Rn: "p=None \<Longrightarrow> hn_refine (hn_ctxt (option_assn P) p p' * F) f1' (hn_ctxt XX1 p p' * \<Gamma>1') R f1"
  assumes Rs: "\<And>x x'. \<lbrakk> p=Some x; p'=Some x' \<rbrakk> \<Longrightarrow>
    hn_refine (hn_ctxt P x x' * INVE * F) (f2' x') (hn_ctxt P' x x' * hn_ctxt XX2 p p' * \<Gamma>2') R (f2 x)"
  assumes MERGE1: "\<Gamma>1' \<or>\<^sub>A \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'"
  shows "hn_refine \<Gamma> (case_option f1' f2' p') (hn_ctxt (option_assn P') p p' * \<Gamma>') R (case_option$f1$(\<lambda>\<^sub>2x. f2 x)$p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine \<Gamma> (case p' of None \<Rightarrow> f1' | Some x \<Rightarrow> f2' x) (hn_ctxt (option_assn P') p p' * \<Gamma>') R (case_option $ f1 $ (\<lambda>x. (#f2 x#)) $ p)
[PROOF STEP]
apply (rule hn_refine_cons_pre[OF FR])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt (option_assn P) p p' * F) (case p' of None \<Rightarrow> f1' | Some x \<Rightarrow> f2' x) (hn_ctxt (option_assn P') p p' * \<Gamma>') R (case_option $ f1 $ (\<lambda>x. (#f2 x#)) $ p)
[PROOF STEP]
apply1 extract_hnr_invalids
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1 h2. \<lbrakk>h2 \<Turnstile> F; hn_invalid (option_assn P) p p' = true\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (option_assn P) p p' * F) (case p' of None \<Rightarrow> f1' | Some x \<Rightarrow> f2' x) (hn_ctxt (option_assn P') p p' * \<Gamma>') R (case_option $ f1 $ (\<lambda>x. (#f2 x#)) $ p)
[PROOF STEP]
apply (cases p; cases p'; simp add: option_assn.simps[THEN hn_ctxt_option])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>h2. \<lbrakk>h2 \<Turnstile> F; hn_invalid (option_assn P) None None = true; p = None; p' = None\<rbrakk> \<Longrightarrow> hn_refine F f1' \<Gamma>' R f1
 2. \<And>h2 a aa. \<lbrakk>h2 \<Turnstile> F; hn_invalid (option_assn P) (Some a) (Some aa) = true; p = Some a; p' = Some aa\<rbrakk> \<Longrightarrow> hn_refine (P a aa * F) (f2' aa) (P' a aa * \<Gamma>') R (f2 a)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) None None = true; p = None; p' = None\<rbrakk> \<Longrightarrow> hn_refine F f1' \<Gamma>' R f1
[PROOF STEP]
apply (rule hn_refine_cons[OF _ Rn _ entt_refl]; assumption?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) None None = true; p = None; p' = None\<rbrakk> \<Longrightarrow> F \<Longrightarrow>\<^sub>t hn_ctxt (option_assn P) p p' * F
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) None None = true; p = None; p' = None\<rbrakk> \<Longrightarrow> hn_ctxt XX1 p p' * \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) None None = true; p = None; p' = None\<rbrakk> \<Longrightarrow> hn_ctxt XX1 p p' * \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply (subst mult.commute, rule entt_fr_drop)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) None None = true; p = None; p' = None\<rbrakk> \<Longrightarrow> \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply (rule entt_trans[OF _ MERGE1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) None None = true; p = None; p' = None\<rbrakk> \<Longrightarrow> \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>1' \<or>\<^sub>A \<Gamma>2'
[PROOF STEP]
apply (simp add: ent_disjI1' ent_disjI2')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h2 a aa. \<lbrakk>h2 \<Turnstile> F; hn_invalid (option_assn P) (Some a) (Some aa) = true; p = Some a; p' = Some aa\<rbrakk> \<Longrightarrow> hn_refine (P a aa * F) (f2' aa) (P' a aa * \<Gamma>') R (f2 a)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) (Some a_) (Some aa_) = true; p = Some a_; p' = Some aa_\<rbrakk> \<Longrightarrow> hn_refine (P a_ aa_ * F) (f2' aa_) (P' a_ aa_ * \<Gamma>') R (f2 a_)
[PROOF STEP]
apply (rule hn_refine_cons[OF _ Rs _ entt_refl]; assumption?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) (Some a_) (Some aa_) = true; p = Some a_; p' = Some aa_\<rbrakk> \<Longrightarrow> P a_ aa_ * F \<Longrightarrow>\<^sub>t hn_ctxt P a_ aa_ * INVE * F
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) (Some a_) (Some aa_) = true; p = Some a_; p' = Some aa_\<rbrakk> \<Longrightarrow> hn_ctxt P' a_ aa_ * hn_ctxt XX2 p p' * \<Gamma>2' \<Longrightarrow>\<^sub>t P' a_ aa_ * \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) (Some a_) (Some aa_) = true; p = Some a_; p' = Some aa_\<rbrakk> \<Longrightarrow> hn_ctxt P' a_ aa_ * hn_ctxt XX2 p p' * \<Gamma>2' \<Longrightarrow>\<^sub>t P' a_ aa_ * \<Gamma>'
[PROOF STEP]
apply (rule entt_star_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) (Some a_) (Some aa_) = true; p = Some a_; p' = Some aa_\<rbrakk> \<Longrightarrow> hn_ctxt P' a_ aa_ * hn_ctxt XX2 p p' \<Longrightarrow>\<^sub>t P' a_ aa_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) (Some a_) (Some aa_) = true; p = Some a_; p' = Some aa_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_fr_drop)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) (Some a_) (Some aa_) = true; p = Some a_; p' = Some aa_\<rbrakk> \<Longrightarrow> hn_ctxt P' a_ aa_ \<Longrightarrow>\<^sub>t P' a_ aa_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) (Some a_) (Some aa_) = true; p = Some a_; p' = Some aa_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) (Some a_) (Some aa_) = true; p = Some a_; p' = Some aa_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_trans[OF _ MERGE1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (option_assn P) (Some a_) (Some aa_) = true; p = Some a_; p' = Some aa_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>1' \<or>\<^sub>A \<Gamma>2'
[PROOF STEP]
applyS (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hn_None[sepref_fr_rules]:
  "hn_refine emp (return None) emp (option_assn P) (RETURN$None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine emp (return None) emp (option_assn P) (RETURN $ None)
[PROOF STEP]
by rule sep_auto


[STATEMENT]
lemma hn_Some[sepref_fr_rules]: "hn_refine
  (hn_ctxt P v v')
  (return (Some v'))
  (hn_invalid P v v')
  (option_assn P)
  (RETURN$(Some$v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt P v v') (return (Some v')) (hn_invalid P v v') (option_assn P) (RETURN $ (Some $ v))
[PROOF STEP]
by rule (sep_auto simp: hn_ctxt_def invalidate_clone')


[STATEMENT]
lemma option_assn_eq[sepref_comb_rules]:
  fixes a b :: "'a option"
  assumes F1: "\<Gamma> \<Longrightarrow>\<^sub>t hn_ctxt (option_assn P) a a' * hn_ctxt (option_assn P) b b' * \<Gamma>1"
  assumes EQ: "\<And>va va' vb vb'. hn_refine
    (hn_ctxt P va va' * hn_ctxt P vb vb' * \<Gamma>1)
    (eq' va' vb')
    (\<Gamma>' va va' vb vb')
    bool_assn
    (RETURN$((=) $va$vb))"
  assumes F2:
    "\<And>va va' vb vb'.
      \<Gamma>' va va' vb vb' \<Longrightarrow>\<^sub>t hn_ctxt P va va' * hn_ctxt P vb vb' * \<Gamma>1"
  shows "hn_refine
    \<Gamma>
    (imp_option_eq eq' a' b')
    (hn_ctxt (option_assn P) a a' * hn_ctxt (option_assn P) b b' * \<Gamma>1)
    bool_assn
    (RETURN$((=) $a$b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine \<Gamma> (imp_option_eq eq' a' b') (hn_ctxt (option_assn P) a a' * hn_ctxt (option_assn P) b b' * \<Gamma>1) bool_assn (RETURN $ ((=) $ a $ b))
[PROOF STEP]
apply (rule hn_refine_cons_pre[OF F1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt (option_assn P) a a' * hn_ctxt (option_assn P) b b' * \<Gamma>1) (imp_option_eq eq' a' b') (hn_ctxt (option_assn P) a a' * hn_ctxt (option_assn P) b b' * \<Gamma>1) bool_assn (RETURN $ ((=) $ a $ b))
[PROOF STEP]
unfolding imp_option_eq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt (option_assn P) a a' * hn_ctxt (option_assn P) b b' * \<Gamma>1) (case (a', b') of (None, None) \<Rightarrow> return True | (None, Some aa) \<Rightarrow> return False | (Some a, None) \<Rightarrow> return False | (Some a, Some b) \<Rightarrow> eq' a b) (hn_ctxt (option_assn P) a a' * hn_ctxt (option_assn P) b b' * \<Gamma>1) bool_assn (RETURN $ ((=) $ a $ b))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (RETURN $ ((=) $ a $ b)) \<Longrightarrow> <hn_ctxt (option_assn P) a a' * hn_ctxt (option_assn P) b b' * \<Gamma>1> case (a', b') of (None, None) \<Rightarrow> return True | (None, Some aa) \<Rightarrow> return False | (Some a, None) \<Rightarrow> return False | (Some a, Some b) \<Rightarrow> eq' a b <\<lambda>r. hn_ctxt (option_assn P) a a' * hn_ctxt (option_assn P) b b' * \<Gamma>1 * (\<exists>\<^sub>Ax. bool_assn x r * \<up> (RETURN x \<le> RETURN $ ((=) $ a $ b)))>\<^sub>t
[PROOF STEP]
apply (simp split: option.split add: hn_ctxt_def, intro impI conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b' = None; a' = None; a = None; b = None\<rbrakk> \<Longrightarrow> <\<Gamma>1> return True <\<lambda>r. \<exists>\<^sub>Ax. \<Gamma>1 * bool_assn x r * true * \<up> x>
 2. b' = None \<Longrightarrow> \<forall>x2. a' = Some x2 \<longrightarrow> b = None \<longrightarrow> <option_assn P a (Some x2) * \<Gamma>1> return False <\<lambda>r. \<exists>\<^sub>Ax. option_assn P a (Some x2) * \<Gamma>1 * bool_assn x r * true * \<up> (x = (a = None))>
 3. \<forall>x2. b' = Some x2 \<longrightarrow> (a' = None \<longrightarrow> a = None \<longrightarrow> <option_assn P b (Some x2) * \<Gamma>1> return False <\<lambda>r. \<exists>\<^sub>Ax. option_assn P b (Some x2) * \<Gamma>1 * bool_assn x r * true * \<up> (x = (None = b))>) \<and> (\<forall>x2a. a' = Some x2a \<longrightarrow> <option_assn P a (Some x2a) * option_assn P b (Some x2) * \<Gamma>1> eq' x2a x2 <\<lambda>r. \<exists>\<^sub>Ax. option_assn P a (Some x2a) * option_assn P b (Some x2) * \<Gamma>1 * bool_assn x r * true * \<up> (x = (a = b))>)
[PROOF STEP]
apply (sep_auto split: option.split simp: hn_ctxt_def pure_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b' = None \<Longrightarrow> \<forall>x2. a' = Some x2 \<longrightarrow> b = None \<longrightarrow> <option_assn P a (Some x2) * \<Gamma>1> return False <\<lambda>r. \<exists>\<^sub>Ax. option_assn P a (Some x2) * \<Gamma>1 * bool_assn x r * true * \<up> (x = (a = None))>
 2. \<forall>x2. b' = Some x2 \<longrightarrow> (a' = None \<longrightarrow> a = None \<longrightarrow> <option_assn P b (Some x2) * \<Gamma>1> return False <\<lambda>r. \<exists>\<^sub>Ax. option_assn P b (Some x2) * \<Gamma>1 * bool_assn x r * true * \<up> (x = (None = b))>) \<and> (\<forall>x2a. a' = Some x2a \<longrightarrow> <option_assn P a (Some x2a) * option_assn P b (Some x2) * \<Gamma>1> eq' x2a x2 <\<lambda>r. \<exists>\<^sub>Ax. option_assn P a (Some x2a) * option_assn P b (Some x2) * \<Gamma>1 * bool_assn x r * true * \<up> (x = (a = b))>)
[PROOF STEP]
apply (cases a, (sep_auto split: option.split simp: hn_ctxt_def pure_def)+)[]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x2. b' = Some x2 \<longrightarrow> (a' = None \<longrightarrow> a = None \<longrightarrow> <option_assn P b (Some x2) * \<Gamma>1> return False <\<lambda>r. \<exists>\<^sub>Ax. option_assn P b (Some x2) * \<Gamma>1 * bool_assn x r * true * \<up> (x = (None = b))>) \<and> (\<forall>x2a. a' = Some x2a \<longrightarrow> <option_assn P a (Some x2a) * option_assn P b (Some x2) * \<Gamma>1> eq' x2a x2 <\<lambda>r. \<exists>\<^sub>Ax. option_assn P a (Some x2a) * option_assn P b (Some x2) * \<Gamma>1 * bool_assn x r * true * \<up> (x = (a = b))>)
[PROOF STEP]
apply (cases a, (sep_auto split: option.split simp: hn_ctxt_def pure_def)+)[]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa x2 x2a. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a\<rbrakk> \<Longrightarrow> <P aa x2a * option_assn P b (Some x2) * \<Gamma>1> eq' x2a x2 <\<lambda>r. \<exists>\<^sub>Ax. P aa x2a * option_assn P b (Some x2) * \<Gamma>1 * true * \<up> (r = x \<and> x = (Some aa = b))>
[PROOF STEP]
apply (cases b, (sep_auto split: option.split simp: hn_ctxt_def pure_def)+)[]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa x2 x2a aaa. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> <P aa x2a * P aaa x2 * \<Gamma>1> eq' x2a x2 <\<lambda>r. \<exists>\<^sub>Ax. P aa x2a * P aaa x2 * \<Gamma>1 * true * \<up> (r = x \<and> x = (aa = aaa))>
[PROOF STEP]
apply (rule cons_post_rule)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa x2 x2a aaa. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> <P aa x2a * P aaa x2 * \<Gamma>1> eq' x2a x2 <?Q111 aa x2 x2a aaa>
 2. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> ?Q111 aa x2 x2a aaa x \<Longrightarrow>\<^sub>A \<exists>\<^sub>Axa. P aa x2a * P aaa x2 * \<Gamma>1 * true * \<up> (x = xa \<and> xa = (aa = aaa))
[PROOF STEP]
apply (rule hn_refineD[OF EQ[unfolded hn_ctxt_def]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa x2 x2a aaa. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> nofail (RETURN $ ((=) $ aa $ aaa))
 2. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> \<Gamma>' aa x2a aaa x2 * (\<exists>\<^sub>Axa. bool_assn xa x * \<up> (RETURN xa \<le> RETURN $ ((=) $ aa $ aaa))) * true \<Longrightarrow>\<^sub>A \<exists>\<^sub>Axa. P aa x2a * P aaa x2 * \<Gamma>1 * true * \<up> (x = xa \<and> xa = (aa = aaa))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> \<Gamma>' aa x2a aaa x2 * (\<exists>\<^sub>Axa. bool_assn xa x * \<up> (RETURN xa \<le> RETURN $ ((=) $ aa $ aaa))) * true \<Longrightarrow>\<^sub>A \<exists>\<^sub>Axa. P aa x2a * P aaa x2 * \<Gamma>1 * true * \<up> (x = xa \<and> xa = (aa = aaa))
[PROOF STEP]
apply (rule ent_frame_fwd[OF F2[THEN enttD,unfolded hn_ctxt_def]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> \<Gamma>' aa x2a aaa x2 * (\<exists>\<^sub>Axa. bool_assn xa x * \<up> (RETURN xa \<le> RETURN $ ((=) $ aa $ aaa))) * true \<Longrightarrow>\<^sub>A \<Gamma>' (?va119 aa x2 x2a aaa x) (?va'119 aa x2 x2a aaa x) (?vb119 aa x2 x2a aaa x) (?vb'119 aa x2 x2a aaa x) * ?F117 aa x2 x2a aaa x
 2. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> P (?va119 aa x2 x2a aaa x) (?va'119 aa x2 x2a aaa x) * P (?vb119 aa x2 x2a aaa x) (?vb'119 aa x2 x2a aaa x) * \<Gamma>1 * true * ?F117 aa x2 x2a aaa x \<Longrightarrow>\<^sub>A \<exists>\<^sub>Axa. P aa x2a * P aaa x2 * \<Gamma>1 * true * \<up> (x = xa \<and> xa = (aa = aaa))
[PROOF STEP]
apply (fr_rot 2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> (\<exists>\<^sub>Axa. bool_assn xa x * \<up> (RETURN xa \<le> RETURN $ ((=) $ aa $ aaa))) * true * \<Gamma>' aa x2a aaa x2 \<Longrightarrow>\<^sub>A \<Gamma>' (?va119 aa x2 x2a aaa x) (?va'119 aa x2 x2a aaa x) (?vb119 aa x2 x2a aaa x) (?vb'119 aa x2 x2a aaa x) * ?F117 aa x2 x2a aaa x
 2. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> P (?va119 aa x2 x2a aaa x) (?va'119 aa x2 x2a aaa x) * P (?vb119 aa x2 x2a aaa x) (?vb'119 aa x2 x2a aaa x) * \<Gamma>1 * true * ?F117 aa x2 x2a aaa x \<Longrightarrow>\<^sub>A \<exists>\<^sub>Axa. P aa x2a * P aaa x2 * \<Gamma>1 * true * \<up> (x = xa \<and> xa = (aa = aaa))
[PROOF STEP]
apply (fr_rot_rhs 1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> (\<exists>\<^sub>Axa. bool_assn xa x * \<up> (RETURN xa \<le> RETURN $ ((=) $ aa $ aaa))) * true * \<Gamma>' aa x2a aaa x2 \<Longrightarrow>\<^sub>A ?F117 aa x2 x2a aaa x * \<Gamma>' (?va119 aa x2 x2a aaa x) (?va'119 aa x2 x2a aaa x) (?vb119 aa x2 x2a aaa x) (?vb'119 aa x2 x2a aaa x)
 2. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> P (?va119 aa x2 x2a aaa x) (?va'119 aa x2 x2a aaa x) * P (?vb119 aa x2 x2a aaa x) (?vb'119 aa x2 x2a aaa x) * \<Gamma>1 * true * ?F117 aa x2 x2a aaa x \<Longrightarrow>\<^sub>A \<exists>\<^sub>Axa. P aa x2a * P aaa x2 * \<Gamma>1 * true * \<up> (x = xa \<and> xa = (aa = aaa))
[PROOF STEP]
apply (rule fr_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> (\<exists>\<^sub>Axa. bool_assn xa x * \<up> (RETURN xa \<le> RETURN $ ((=) $ aa $ aaa))) * true \<Longrightarrow>\<^sub>A ?F117 aa x2 x2a aaa x
 2. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> P aa x2a * P aaa x2 * \<Gamma>1 * true * ?F117 aa x2 x2a aaa x \<Longrightarrow>\<^sub>A \<exists>\<^sub>Axa. P aa x2a * P aaa x2 * \<Gamma>1 * true * \<up> (x = xa \<and> xa = (aa = aaa))
[PROOF STEP]
apply (rule ent_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa x2 x2a aaa x. \<lbrakk>a = Some aa; b' = Some x2; a' = Some x2a; b = Some aaa\<rbrakk> \<Longrightarrow> P aa x2a * P aaa x2 * \<Gamma>1 * true * ((\<exists>\<^sub>Axa. bool_assn xa x * \<up> (RETURN xa \<le> RETURN $ ((=) $ aa $ aaa))) * true) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Axa. P aa x2a * P aaa x2 * \<Gamma>1 * true * \<up> (x = xa \<and> xa = (aa = aaa))
[PROOF STEP]
apply (sep_auto simp: pure_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [pat_rules]:
  "(=) $a$None \<equiv> is_None$a"
  "(=) $None$a \<equiv> is_None$a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) $ a $ None \<equiv> is_None $ a) &&& (=) $ None $ a \<equiv> is_None $ a
[PROOF STEP]
apply (rule eq_reflection, simp split: option.split)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hn_is_None[sepref_fr_rules]: "hn_refine
  (hn_ctxt (option_assn P) a a')
  (return (is_None a'))
  (hn_ctxt (option_assn P) a a')
  bool_assn
  (RETURN$(is_None$a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt (option_assn P) a a') (return (is_None a')) (hn_ctxt (option_assn P) a a') bool_assn (RETURN $ (is_None $ a))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (RETURN $ (is_None $ a)) \<Longrightarrow> <hn_ctxt (option_assn P) a a'> return (is_None a') <\<lambda>r. hn_ctxt (option_assn P) a a' * (\<exists>\<^sub>Ax. bool_assn x r * \<up> (RETURN x \<le> RETURN $ (is_None $ a)))>\<^sub>t
[PROOF STEP]
apply (sep_auto split: option.split simp: hn_ctxt_def pure_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in -) sepref_the_complete[sepref_fr_rules]:
  assumes "x\<noteq>None"
  shows "hn_refine
    (hn_ctxt (option_assn R) x xi)
    (return (the xi))
    (hn_invalid (option_assn R) x xi)
    (R)
    (RETURN$(the$x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt (option_assn R) x xi) (return (the xi)) (hn_invalid (option_assn R) x xi) R (RETURN $ (the $ x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> None

goal (1 subgoal):
 1. hn_refine (hn_ctxt (option_assn R) x xi) (return (the xi)) (hn_invalid (option_assn R) x xi) R (RETURN $ (the $ x))
[PROOF STEP]
apply (cases x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> None; x = None\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (option_assn R) x xi) (return (the xi)) (hn_invalid (option_assn R) x xi) R (RETURN $ (the $ x))
 2. \<And>a. \<lbrakk>x \<noteq> None; x = Some a\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (option_assn R) x xi) (return (the xi)) (hn_invalid (option_assn R) x xi) R (RETURN $ (the $ x))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>x \<noteq> None; x = Some a\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (option_assn R) x xi) (return (the xi)) (hn_invalid (option_assn R) x xi) R (RETURN $ (the $ x))
[PROOF STEP]
apply (cases xi)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>x \<noteq> None; x = Some a; xi = None\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (option_assn R) x xi) (return (the xi)) (hn_invalid (option_assn R) x xi) R (RETURN $ (the $ x))
 2. \<And>a aa. \<lbrakk>x \<noteq> None; x = Some a; xi = Some aa\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (option_assn R) x xi) (return (the xi)) (hn_invalid (option_assn R) x xi) R (RETURN $ (the $ x))
[PROOF STEP]
apply (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>x \<noteq> None; x = Some a; xi = Some aa\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (option_assn R) x xi) (return (the xi)) (hn_invalid (option_assn R) x xi) R (RETURN $ (the $ x))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>x \<noteq> None; x = Some a; xi = Some aa; nofail (RETURN $ (the $ x))\<rbrakk> \<Longrightarrow> <hn_ctxt (option_assn R) x xi> return (the xi) <\<lambda>r. hn_invalid (option_assn R) x xi * (\<exists>\<^sub>Axa. R xa r * \<up> (RETURN xa \<le> RETURN $ (the $ x)))>\<^sub>t
[PROOF STEP]
apply (sep_auto simp: hn_ctxt_def invalidate_clone' vassn_tagI invalid_assn_const)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in -) sepref_the_id:
  assumes "CONSTRAINT (IS_PURE IS_ID) R"
  shows "hn_refine
    (hn_ctxt (option_assn R) x xi)
    (return (the xi))
    (hn_ctxt (option_assn R) x xi)
    (R)
    (RETURN$(the$x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt (option_assn R) x xi) (return (the xi)) (hn_ctxt (option_assn R) x xi) R (RETURN $ (the $ x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CONSTRAINT (IS_PURE IS_ID) R

goal (1 subgoal):
 1. hn_refine (hn_ctxt (option_assn R) x xi) (return (the xi)) (hn_ctxt (option_assn R) x xi) R (RETURN $ (the $ x))
[PROOF STEP]
apply (clarsimp simp: IS_PURE_def IS_ID_def hn_ctxt_def is_pure_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R = id_assn \<Longrightarrow> hn_refine (option_assn id_assn x xi) (return (the xi)) (option_assn id_assn x xi) id_assn (RETURN (the x))
[PROOF STEP]
apply (cases x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>R = id_assn; x = None\<rbrakk> \<Longrightarrow> hn_refine (option_assn id_assn x xi) (return (the xi)) (option_assn id_assn x xi) id_assn (RETURN (the x))
 2. \<And>a. \<lbrakk>R = id_assn; x = Some a\<rbrakk> \<Longrightarrow> hn_refine (option_assn id_assn x xi) (return (the xi)) (option_assn id_assn x xi) id_assn (RETURN (the x))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>R = id_assn; x = None\<rbrakk> \<Longrightarrow> hn_refine (\<up> (xi = None)) (return (the xi)) (\<up> (xi = None)) id_assn (RETURN (the None))
 2. \<And>a. \<lbrakk>R = id_assn; x = Some a\<rbrakk> \<Longrightarrow> hn_refine (option_assn id_assn x xi) (return (the xi)) (option_assn id_assn x xi) id_assn (RETURN (the x))
[PROOF STEP]
apply (cases xi)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>R = id_assn; x = None; xi = None\<rbrakk> \<Longrightarrow> hn_refine (\<up> (xi = None)) (return (the xi)) (\<up> (xi = None)) id_assn (RETURN (the None))
 2. \<And>a. \<lbrakk>R = id_assn; x = None; xi = Some a\<rbrakk> \<Longrightarrow> hn_refine (\<up> (xi = None)) (return (the xi)) (\<up> (xi = None)) id_assn (RETURN (the None))
 3. \<And>a. \<lbrakk>R = id_assn; x = Some a\<rbrakk> \<Longrightarrow> hn_refine (option_assn id_assn x xi) (return (the xi)) (option_assn id_assn x xi) id_assn (RETURN (the x))
[PROOF STEP]
apply (simp add: hn_ctxt_def invalid_assn_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>R = id_assn; x = None; xi = None\<rbrakk> \<Longrightarrow> hn_refine emp (return (the None)) emp id_assn (RETURN (the None))
 2. \<And>a. \<lbrakk>R = id_assn; x = None; xi = Some a\<rbrakk> \<Longrightarrow> hn_refine (\<up> (xi = None)) (return (the xi)) (\<up> (xi = None)) id_assn (RETURN (the None))
 3. \<And>a. \<lbrakk>R = id_assn; x = Some a\<rbrakk> \<Longrightarrow> hn_refine (option_assn id_assn x xi) (return (the xi)) (option_assn id_assn x xi) id_assn (RETURN (the x))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>R = id_assn; x = None; xi = None; nofail (RETURN (the None))\<rbrakk> \<Longrightarrow> <emp> return (the None) <\<lambda>r. emp * (\<exists>\<^sub>Ax. id_assn x r * \<up> (RETURN x \<le> RETURN (the None)))>\<^sub>t
 2. \<And>a. \<lbrakk>R = id_assn; x = None; xi = Some a\<rbrakk> \<Longrightarrow> hn_refine (\<up> (xi = None)) (return (the xi)) (\<up> (xi = None)) id_assn (RETURN (the None))
 3. \<And>a. \<lbrakk>R = id_assn; x = Some a\<rbrakk> \<Longrightarrow> hn_refine (option_assn id_assn x xi) (return (the xi)) (option_assn id_assn x xi) id_assn (RETURN (the x))
[PROOF STEP]
apply (sep_auto simp: pure_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>R = id_assn; x = None; xi = Some a\<rbrakk> \<Longrightarrow> hn_refine (\<up> (xi = None)) (return (the xi)) (\<up> (xi = None)) id_assn (RETURN (the None))
 2. \<And>a. \<lbrakk>R = id_assn; x = Some a\<rbrakk> \<Longrightarrow> hn_refine (option_assn id_assn x xi) (return (the xi)) (option_assn id_assn x xi) id_assn (RETURN (the x))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>R = id_assn; x = None; xi = Some a; nofail (RETURN (the None))\<rbrakk> \<Longrightarrow> <\<up> (xi = None)> return (the xi) <\<lambda>r. \<up> (xi = None) * (\<exists>\<^sub>Ax. id_assn x r * \<up> (RETURN x \<le> RETURN (the None)))>\<^sub>t
 2. \<And>a. \<lbrakk>R = id_assn; x = Some a\<rbrakk> \<Longrightarrow> hn_refine (option_assn id_assn x xi) (return (the xi)) (option_assn id_assn x xi) id_assn (RETURN (the x))
[PROOF STEP]
apply (sep_auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>R = id_assn; x = Some a\<rbrakk> \<Longrightarrow> hn_refine (option_assn id_assn x xi) (return (the xi)) (option_assn id_assn x xi) id_assn (RETURN (the x))
[PROOF STEP]
apply (simp add: option_assn_pure_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>R = id_assn; x = Some a\<rbrakk> \<Longrightarrow> hn_refine (id_assn (Some a) xi) (return (the xi)) (id_assn (Some a) xi) id_assn (RETURN a)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>R = id_assn; x = Some a; nofail (RETURN a)\<rbrakk> \<Longrightarrow> <id_assn (Some a) xi> return (the xi) <\<lambda>r. id_assn (Some a) xi * (\<exists>\<^sub>Ax. id_assn x r * \<up> (RETURN x \<le> RETURN a))>\<^sub>t
[PROOF STEP]
apply (sep_auto simp: pure_def invalid_assn_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_aux_simps[simp]:
  "list_assn P [] l' = (\<up>(l'=[]))"
  "list_assn P l [] = (\<up>(l=[]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn P [] l' = \<up> (l' = []) &&& list_assn P l [] = \<up> (l = [])
[PROOF STEP]
unfolding hn_ctxt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn P [] l' = \<up> (l' = []) &&& list_assn P l [] = \<up> (l = [])
[PROOF STEP]
apply (cases l')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. l' = [] \<Longrightarrow> list_assn P [] l' = \<up> (l' = [])
 2. \<And>a list. l' = a # list \<Longrightarrow> list_assn P [] l' = \<up> (l' = [])
 3. list_assn P l [] = \<up> (l = [])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list. l' = a # list \<Longrightarrow> list_assn P [] l' = \<up> (l' = [])
 2. list_assn P l [] = \<up> (l = [])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn P l [] = \<up> (l = [])
[PROOF STEP]
apply (cases l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> list_assn P l [] = \<up> (l = [])
 2. \<And>a list. l = a # list \<Longrightarrow> list_assn P l [] = \<up> (l = [])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> list_assn P l [] = \<up> (l = [])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_aux_append[simp]:
  "length l1=length l1' \<Longrightarrow>
    list_assn P (l1@l2) (l1'@l2')
    = list_assn P l1 l1' * list_assn P l2 l2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l1 = length l1' \<Longrightarrow> list_assn P (l1 @ l2) (l1' @ l2') = list_assn P l1 l1' * list_assn P l2 l2'
[PROOF STEP]
apply (induct rule: list_induct2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. list_assn P ([] @ l2) ([] @ l2') = list_assn P [] [] * list_assn P l2 l2'
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_assn P (xs @ l2) (ys @ l2') = list_assn P xs ys * list_assn P l2 l2'\<rbrakk> \<Longrightarrow> list_assn P ((x # xs) @ l2) ((y # ys) @ l2') = list_assn P (x # xs) (y # ys) * list_assn P l2 l2'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_assn P (xs @ l2) (ys @ l2') = list_assn P xs ys * list_assn P l2 l2'\<rbrakk> \<Longrightarrow> list_assn P ((x # xs) @ l2) ((y # ys) @ l2') = list_assn P (x # xs) (y # ys) * list_assn P l2 l2'
[PROOF STEP]
apply (simp add: star_assoc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_aux_ineq_len: "length l \<noteq> length li \<Longrightarrow> list_assn A l li = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l \<noteq> length li \<Longrightarrow> list_assn A l li = false
[PROOF STEP]
proof (induction l arbitrary: li)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>li. length [] \<noteq> length li \<Longrightarrow> list_assn A [] li = false
 2. \<And>a l li. \<lbrakk>\<And>li. length l \<noteq> length li \<Longrightarrow> list_assn A l li = false; length (a # l) \<noteq> length li\<rbrakk> \<Longrightarrow> list_assn A (a # l) li = false
[PROOF STEP]
case (Cons x l li)
[PROOF STATE]
proof (state)
this:
length l \<noteq> length ?li \<Longrightarrow> list_assn A l ?li = false
length (x # l) \<noteq> length li

goal (2 subgoals):
 1. \<And>li. length [] \<noteq> length li \<Longrightarrow> list_assn A [] li = false
 2. \<And>a l li. \<lbrakk>\<And>li. length l \<noteq> length li \<Longrightarrow> list_assn A l li = false; length (a # l) \<noteq> length li\<rbrakk> \<Longrightarrow> list_assn A (a # l) li = false
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
length l \<noteq> length ?li \<Longrightarrow> list_assn A l ?li = false
length (x # l) \<noteq> length li

goal (1 subgoal):
 1. list_assn A (x # l) li = false
[PROOF STEP]
by (cases li; auto)
[PROOF STATE]
proof (state)
this:
list_assn A (x # l) li = false

goal (1 subgoal):
 1. \<And>li. length [] \<noteq> length li \<Longrightarrow> list_assn A [] li = false
[PROOF STEP]
qed simp


[STATEMENT]
lemma list_assn_aux_append2[simp]:
  assumes "length l2=length l2'"
  shows "list_assn P (l1@l2) (l1'@l2')
    = list_assn P l1 l1' * list_assn P l2 l2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn P (l1 @ l2) (l1' @ l2') = list_assn P l1 l1' * list_assn P l2 l2'
[PROOF STEP]
apply (cases "length l1 = length l1'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length l1 = length l1' \<Longrightarrow> list_assn P (l1 @ l2) (l1' @ l2') = list_assn P l1 l1' * list_assn P l2 l2'
 2. length l1 \<noteq> length l1' \<Longrightarrow> list_assn P (l1 @ l2) (l1' @ l2') = list_assn P l1 l1' * list_assn P l2 l2'
[PROOF STEP]
apply (erule list_assn_aux_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l1 \<noteq> length l1' \<Longrightarrow> list_assn P (l1 @ l2) (l1' @ l2') = list_assn P l1 l1' * list_assn P l2 l2'
[PROOF STEP]
apply (simp add: list_assn_aux_ineq_len assms)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_pure_conv[constraint_simps]: "list_assn (pure R) = pure (\<langle>R\<rangle>list_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn (pure R) = pure (\<langle>R\<rangle>list_rel)
[PROOF STEP]
proof (intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. list_assn (pure R) x xa = pure (\<langle>R\<rangle>list_rel) x xa
[PROOF STEP]
fix l li
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. list_assn (pure R) x xa = pure (\<langle>R\<rangle>list_rel) x xa
[PROOF STEP]
show "list_assn (pure R) l li = pure (\<langle>R\<rangle>list_rel) l li"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn (pure R) l li = pure (\<langle>R\<rangle>list_rel) l li
[PROOF STEP]
apply (induction "pure R" l li rule: list_assn.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. list_assn (pure R) [] [] = pure (\<langle>R\<rangle>list_rel) [] []
 2. \<And>a as c cs. list_assn (pure R) as cs = pure (\<langle>R\<rangle>list_rel) as cs \<Longrightarrow> list_assn (pure R) (a # as) (c # cs) = pure (\<langle>R\<rangle>list_rel) (a # as) (c # cs)
 3. \<And>v va. list_assn (pure R) (v # va) [] = pure (\<langle>R\<rangle>list_rel) (v # va) []
 4. \<And>v va. list_assn (pure R) [] (v # va) = pure (\<langle>R\<rangle>list_rel) [] (v # va)
[PROOF STEP]
by (auto simp: pure_def)
[PROOF STATE]
proof (state)
this:
list_assn (pure R) l li = pure (\<langle>R\<rangle>list_rel) l li

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_assn_simps[simp]:
  "hn_ctxt (list_assn P) [] l' = (\<up>(l'=[]))"
  "hn_ctxt (list_assn P) l [] = (\<up>(l=[]))"
  "hn_ctxt (list_assn P) [] [] = emp"
  "hn_ctxt (list_assn P) (a#as) (c#cs) = hn_ctxt P a c * hn_ctxt (list_assn P) as cs"
  "hn_ctxt (list_assn P) (a#as) [] = false"
  "hn_ctxt (list_assn P) [] (c#cs) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hn_ctxt (list_assn P) [] l' = \<up> (l' = []) &&& hn_ctxt (list_assn P) l [] = \<up> (l = []) &&& hn_ctxt (list_assn P) [] [] = emp) &&& hn_ctxt (list_assn P) (a # as) (c # cs) = hn_ctxt P a c * hn_ctxt (list_assn P) as cs &&& hn_ctxt (list_assn P) (a # as) [] = false &&& hn_ctxt (list_assn P) [] (c # cs) = false
[PROOF STEP]
unfolding hn_ctxt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list_assn P [] l' = \<up> (l' = []) &&& list_assn P l [] = \<up> (l = []) &&& list_assn P [] [] = emp) &&& list_assn P (a # as) (c # cs) = P a c * list_assn P as cs &&& list_assn P (a # as) [] = false &&& list_assn P [] (c # cs) = false
[PROOF STEP]
apply (cases l')
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. l' = [] \<Longrightarrow> list_assn P [] l' = \<up> (l' = [])
 2. \<And>a list. l' = a # list \<Longrightarrow> list_assn P [] l' = \<up> (l' = [])
 3. list_assn P l [] = \<up> (l = [])
 4. list_assn P [] [] = emp
 5. list_assn P (a # as) (c # cs) = P a c * list_assn P as cs
 6. list_assn P (a # as) [] = false
 7. list_assn P [] (c # cs) = false
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a list. l' = a # list \<Longrightarrow> list_assn P [] l' = \<up> (l' = [])
 2. list_assn P l [] = \<up> (l = [])
 3. list_assn P [] [] = emp
 4. list_assn P (a # as) (c # cs) = P a c * list_assn P as cs
 5. list_assn P (a # as) [] = false
 6. list_assn P [] (c # cs) = false
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. list_assn P l [] = \<up> (l = [])
 2. list_assn P [] [] = emp
 3. list_assn P (a # as) (c # cs) = P a c * list_assn P as cs
 4. list_assn P (a # as) [] = false
 5. list_assn P [] (c # cs) = false
[PROOF STEP]
apply (cases l)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. l = [] \<Longrightarrow> list_assn P l [] = \<up> (l = [])
 2. \<And>a list. l = a # list \<Longrightarrow> list_assn P l [] = \<up> (l = [])
 3. list_assn P [] [] = emp
 4. list_assn P (a # as) (c # cs) = P a c * list_assn P as cs
 5. list_assn P (a # as) [] = false
 6. list_assn P [] (c # cs) = false
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a list. l = a # list \<Longrightarrow> list_assn P l [] = \<up> (l = [])
 2. list_assn P [] [] = emp
 3. list_assn P (a # as) (c # cs) = P a c * list_assn P as cs
 4. list_assn P (a # as) [] = false
 5. list_assn P [] (c # cs) = false
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. list_assn P [] [] = emp
 2. list_assn P (a # as) (c # cs) = P a c * list_assn P as cs
 3. list_assn P (a # as) [] = false
 4. list_assn P [] (c # cs) = false
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_precise[constraint_rules]: "precise P \<Longrightarrow> precise (list_assn P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise P \<Longrightarrow> precise (list_assn P)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a' h p F F'. \<lbrakk>precise P; h \<Turnstile> list_assn P a p * F \<and>\<^sub>A list_assn P a' p * F'\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
fix l1 l2 l h F1 F2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a' h p F F'. \<lbrakk>precise P; h \<Turnstile> list_assn P a p * F \<and>\<^sub>A list_assn P a' p * F'\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
assume P: "precise P"
[PROOF STATE]
proof (state)
this:
precise P

goal (1 subgoal):
 1. \<And>a a' h p F F'. \<lbrakk>precise P; h \<Turnstile> list_assn P a p * F \<and>\<^sub>A list_assn P a' p * F'\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
assume "h\<Turnstile>list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2"
[PROOF STATE]
proof (state)
this:
h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2

goal (1 subgoal):
 1. \<And>a a' h p F F'. \<lbrakk>precise P; h \<Turnstile> list_assn P a p * F \<and>\<^sub>A list_assn P a' p * F'\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
thus "l1=l2"
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2

goal (1 subgoal):
 1. l1 = l2
[PROOF STEP]
proof (induct l arbitrary: l1 l2 F1 F2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 [] * F1 \<and>\<^sub>A list_assn P l2 [] * F2 \<Longrightarrow> l1 = l2
 2. \<And>a l l1 l2 F1 F2. \<lbrakk>\<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2 \<Longrightarrow> l1 = l2; h \<Turnstile> list_assn P l1 (a # l) * F1 \<and>\<^sub>A list_assn P l2 (a # l) * F2\<rbrakk> \<Longrightarrow> l1 = l2
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
h \<Turnstile> list_assn P l1 [] * F1 \<and>\<^sub>A list_assn P l2 [] * F2

goal (2 subgoals):
 1. \<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 [] * F1 \<and>\<^sub>A list_assn P l2 [] * F2 \<Longrightarrow> l1 = l2
 2. \<And>a l l1 l2 F1 F2. \<lbrakk>\<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2 \<Longrightarrow> l1 = l2; h \<Turnstile> list_assn P l1 (a # l) * F1 \<and>\<^sub>A list_assn P l2 (a # l) * F2\<rbrakk> \<Longrightarrow> l1 = l2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> list_assn P l1 [] * F1 \<and>\<^sub>A list_assn P l2 [] * F2

goal (1 subgoal):
 1. l1 = l2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l1 = l2

goal (1 subgoal):
 1. \<And>a l l1 l2 F1 F2. \<lbrakk>\<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2 \<Longrightarrow> l1 = l2; h \<Turnstile> list_assn P l1 (a # l) * F1 \<and>\<^sub>A list_assn P l2 (a # l) * F2\<rbrakk> \<Longrightarrow> l1 = l2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l l1 l2 F1 F2. \<lbrakk>\<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2 \<Longrightarrow> l1 = l2; h \<Turnstile> list_assn P l1 (a # l) * F1 \<and>\<^sub>A list_assn P l2 (a # l) * F2\<rbrakk> \<Longrightarrow> l1 = l2
[PROOF STEP]
case (Cons a ls)
[PROOF STATE]
proof (state)
this:
h \<Turnstile> list_assn P ?l1.0 ls * ?F1.0 \<and>\<^sub>A list_assn P ?l2.0 ls * ?F2.0 \<Longrightarrow> ?l1.0 = ?l2.0
h \<Turnstile> list_assn P l1 (a # ls) * F1 \<and>\<^sub>A list_assn P l2 (a # ls) * F2

goal (1 subgoal):
 1. \<And>a l l1 l2 F1 F2. \<lbrakk>\<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2 \<Longrightarrow> l1 = l2; h \<Turnstile> list_assn P l1 (a # l) * F1 \<and>\<^sub>A list_assn P l2 (a # l) * F2\<rbrakk> \<Longrightarrow> l1 = l2
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
h \<Turnstile> list_assn P ?l1.0 ls * ?F1.0 \<and>\<^sub>A list_assn P ?l2.0 ls * ?F2.0 \<Longrightarrow> ?l1.0 = ?l2.0
h \<Turnstile> list_assn P l1 (a # ls) * F1 \<and>\<^sub>A list_assn P l2 (a # ls) * F2
[PROOF STEP]
obtain a1 ls1 where [simp]: "l1=a1#ls1"
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> list_assn P ?l1.0 ls * ?F1.0 \<and>\<^sub>A list_assn P ?l2.0 ls * ?F2.0 \<Longrightarrow> ?l1.0 = ?l2.0
h \<Turnstile> list_assn P l1 (a # ls) * F1 \<and>\<^sub>A list_assn P l2 (a # ls) * F2

goal (1 subgoal):
 1. (\<And>a1 ls1. l1 = a1 # ls1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases l1, simp)
[PROOF STATE]
proof (state)
this:
l1 = a1 # ls1

goal (1 subgoal):
 1. \<And>a l l1 l2 F1 F2. \<lbrakk>\<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2 \<Longrightarrow> l1 = l2; h \<Turnstile> list_assn P l1 (a # l) * F1 \<and>\<^sub>A list_assn P l2 (a # l) * F2\<rbrakk> \<Longrightarrow> l1 = l2
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
h \<Turnstile> list_assn P ?l1.0 ls * ?F1.0 \<and>\<^sub>A list_assn P ?l2.0 ls * ?F2.0 \<Longrightarrow> ?l1.0 = ?l2.0
h \<Turnstile> list_assn P l1 (a # ls) * F1 \<and>\<^sub>A list_assn P l2 (a # ls) * F2
[PROOF STEP]
obtain a2 ls2 where [simp]: "l2=a2#ls2"
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> list_assn P ?l1.0 ls * ?F1.0 \<and>\<^sub>A list_assn P ?l2.0 ls * ?F2.0 \<Longrightarrow> ?l1.0 = ?l2.0
h \<Turnstile> list_assn P l1 (a # ls) * F1 \<and>\<^sub>A list_assn P l2 (a # ls) * F2

goal (1 subgoal):
 1. (\<And>a2 ls2. l2 = a2 # ls2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases l2, simp)
[PROOF STATE]
proof (state)
this:
l2 = a2 # ls2

goal (1 subgoal):
 1. \<And>a l l1 l2 F1 F2. \<lbrakk>\<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2 \<Longrightarrow> l1 = l2; h \<Turnstile> list_assn P l1 (a # l) * F1 \<and>\<^sub>A list_assn P l2 (a # l) * F2\<rbrakk> \<Longrightarrow> l1 = l2
[PROOF STEP]
from Cons.prems
[PROOF STATE]
proof (chain)
picking this:
h \<Turnstile> list_assn P l1 (a # ls) * F1 \<and>\<^sub>A list_assn P l2 (a # ls) * F2
[PROOF STEP]
have M:
      "h \<Turnstile> P a1 a * list_assn P ls1 ls * F1
        \<and>\<^sub>A P a2 a * list_assn P ls2 ls * F2"
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> list_assn P l1 (a # ls) * F1 \<and>\<^sub>A list_assn P l2 (a # ls) * F2

goal (1 subgoal):
 1. h \<Turnstile> P a1 a * list_assn P ls1 ls * F1 \<and>\<^sub>A P a2 a * list_assn P ls2 ls * F2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h \<Turnstile> P a1 a * list_assn P ls1 ls * F1 \<and>\<^sub>A P a2 a * list_assn P ls2 ls * F2

goal (1 subgoal):
 1. \<And>a l l1 l2 F1 F2. \<lbrakk>\<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2 \<Longrightarrow> l1 = l2; h \<Turnstile> list_assn P l1 (a # l) * F1 \<and>\<^sub>A list_assn P l2 (a # l) * F2\<rbrakk> \<Longrightarrow> l1 = l2
[PROOF STEP]
have "a1=a2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a1 = a2
[PROOF STEP]
apply (rule preciseD[OF P, where a=a1 and a'=a2 and p=a
        and F= "list_assn P ls1 ls * F1"
        and F'="list_assn P ls2 ls * F2"
        ])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ?h \<Turnstile> P a1 a * (list_assn P ls1 ls * F1) \<and>\<^sub>A P a2 a * (list_assn P ls2 ls * F2)
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> P a1 a * list_assn P ls1 ls * F1 \<and>\<^sub>A P a2 a * list_assn P ls2 ls * F2

goal (1 subgoal):
 1. ?h \<Turnstile> P a1 a * (list_assn P ls1 ls * F1) \<and>\<^sub>A P a2 a * (list_assn P ls2 ls * F2)
[PROOF STEP]
by (simp add: star_assoc)
[PROOF STATE]
proof (state)
this:
a1 = a2

goal (1 subgoal):
 1. \<And>a l l1 l2 F1 F2. \<lbrakk>\<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2 \<Longrightarrow> l1 = l2; h \<Turnstile> list_assn P l1 (a # l) * F1 \<and>\<^sub>A list_assn P l2 (a # l) * F2\<rbrakk> \<Longrightarrow> l1 = l2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a1 = a2

goal (1 subgoal):
 1. \<And>a l l1 l2 F1 F2. \<lbrakk>\<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2 \<Longrightarrow> l1 = l2; h \<Turnstile> list_assn P l1 (a # l) * F1 \<and>\<^sub>A list_assn P l2 (a # l) * F2\<rbrakk> \<Longrightarrow> l1 = l2
[PROOF STEP]
have "ls1=ls2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls1 = ls2
[PROOF STEP]
apply (rule Cons.hyps[where ?F1.0="P a1 a * F1" and ?F2.0="P a2 a * F2"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<Turnstile> list_assn P ls1 ls * (P a1 a * F1) \<and>\<^sub>A list_assn P ls2 ls * (P a2 a * F2)
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
h \<Turnstile> P a1 a * list_assn P ls1 ls * F1 \<and>\<^sub>A P a2 a * list_assn P ls2 ls * F2

goal (1 subgoal):
 1. h \<Turnstile> list_assn P ls1 ls * (P a1 a * F1) \<and>\<^sub>A list_assn P ls2 ls * (P a2 a * F2)
[PROOF STEP]
by (simp only: star_aci)
[PROOF STATE]
proof (state)
this:
ls1 = ls2

goal (1 subgoal):
 1. \<And>a l l1 l2 F1 F2. \<lbrakk>\<And>l1 l2 F1 F2. h \<Turnstile> list_assn P l1 l * F1 \<and>\<^sub>A list_assn P l2 l * F2 \<Longrightarrow> l1 = l2; h \<Turnstile> list_assn P l1 (a # l) * F1 \<and>\<^sub>A list_assn P l2 (a # l) * F2\<rbrakk> \<Longrightarrow> l1 = l2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a1 = a2
ls1 = ls2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a1 = a2
ls1 = ls2

goal (1 subgoal):
 1. l1 = l2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l1 = l2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l1 = l2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_assn_pure[constraint_rules]:
  assumes P: "is_pure P"
  shows "is_pure (list_assn P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure (list_assn P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_pure (list_assn P)
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
is_pure P
[PROOF STEP]
obtain P' where P_eq: "\<And>x x'. P x x' = \<up>(P' x x')"
[PROOF STATE]
proof (prove)
using this:
is_pure P

goal (1 subgoal):
 1. (\<And>P'. (\<And>x x'. P x x' = \<up> (P' x x')) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule is_pureE) blast
[PROOF STATE]
proof (state)
this:
P ?x ?x' = \<up> (P' ?x ?x')

goal (1 subgoal):
 1. is_pure (list_assn P)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
P ?x ?x' = \<up> (P' ?x ?x')

goal (1 subgoal):
 1. is_pure (list_assn P)
[PROOF STEP]
fix l l'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_pure (list_assn P)
[PROOF STEP]
have "list_assn P l l' = \<up>(list_all2 P' l l')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn P l l' = \<up> (list_all2 P' l l')
[PROOF STEP]
by (induct P\<equiv>P l l' rule: list_assn.induct)
         (simp_all add: P_eq)
[PROOF STATE]
proof (state)
this:
list_assn P l l' = \<up> (list_all2 P' l l')

goal (1 subgoal):
 1. is_pure (list_assn P)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
list_assn P ?l2 ?l'2 = \<up> (list_all2 P' ?l2 ?l'2)

goal (1 subgoal):
 1. is_pure (list_assn P)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
list_assn P ?l2 ?l'2 = \<up> (list_all2 P' ?l2 ?l'2)

goal (1 subgoal):
 1. is_pure (list_assn P)
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
is_pure (list_assn P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_assn_mono:
  "\<lbrakk>\<And>x x'. P x x'\<Longrightarrow>\<^sub>AP' x x'\<rbrakk> \<Longrightarrow> list_assn P l l' \<Longrightarrow>\<^sub>A list_assn P' l l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x x'. P x x' \<Longrightarrow>\<^sub>A P' x x') \<Longrightarrow> list_assn P l l' \<Longrightarrow>\<^sub>A list_assn P' l l'
[PROOF STEP]
unfolding hn_ctxt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x x'. P x x' \<Longrightarrow>\<^sub>A P' x x') \<Longrightarrow> list_assn P l l' \<Longrightarrow>\<^sub>A list_assn P' l l'
[PROOF STEP]
apply (induct P l l' rule: list_assn.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>P. (\<And>x x'. P x x' \<Longrightarrow>\<^sub>A P' x x') \<Longrightarrow> list_assn P [] [] \<Longrightarrow>\<^sub>A list_assn P' [] []
 2. \<And>P a as c cs. \<lbrakk>(\<And>x x'. P x x' \<Longrightarrow>\<^sub>A P' x x') \<Longrightarrow> list_assn P as cs \<Longrightarrow>\<^sub>A list_assn P' as cs; \<And>x x'. P x x' \<Longrightarrow>\<^sub>A P' x x'\<rbrakk> \<Longrightarrow> list_assn P (a # as) (c # cs) \<Longrightarrow>\<^sub>A list_assn P' (a # as) (c # cs)
 3. \<And>uu_ v va. (\<And>x x'. uu_ x x' \<Longrightarrow>\<^sub>A P' x x') \<Longrightarrow> list_assn uu_ (v # va) [] \<Longrightarrow>\<^sub>A list_assn P' (v # va) []
 4. \<And>uu_ v va. (\<And>x x'. uu_ x x' \<Longrightarrow>\<^sub>A P' x x') \<Longrightarrow> list_assn uu_ [] (v # va) \<Longrightarrow>\<^sub>A list_assn P' [] (v # va)
[PROOF STEP]
by (auto intro: ent_star_mono)


[STATEMENT]
lemma list_assn_monot:
  "\<lbrakk>\<And>x x'. P x x'\<Longrightarrow>\<^sub>tP' x x'\<rbrakk> \<Longrightarrow> list_assn P l l' \<Longrightarrow>\<^sub>t list_assn P' l l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x x'. P x x' \<Longrightarrow>\<^sub>t P' x x') \<Longrightarrow> list_assn P l l' \<Longrightarrow>\<^sub>t list_assn P' l l'
[PROOF STEP]
unfolding hn_ctxt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x x'. P x x' \<Longrightarrow>\<^sub>t P' x x') \<Longrightarrow> list_assn P l l' \<Longrightarrow>\<^sub>t list_assn P' l l'
[PROOF STEP]
apply (induct P l l' rule: list_assn.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>P. (\<And>x x'. P x x' \<Longrightarrow>\<^sub>t P' x x') \<Longrightarrow> list_assn P [] [] \<Longrightarrow>\<^sub>t list_assn P' [] []
 2. \<And>P a as c cs. \<lbrakk>(\<And>x x'. P x x' \<Longrightarrow>\<^sub>t P' x x') \<Longrightarrow> list_assn P as cs \<Longrightarrow>\<^sub>t list_assn P' as cs; \<And>x x'. P x x' \<Longrightarrow>\<^sub>t P' x x'\<rbrakk> \<Longrightarrow> list_assn P (a # as) (c # cs) \<Longrightarrow>\<^sub>t list_assn P' (a # as) (c # cs)
 3. \<And>uu_ v va. (\<And>x x'. uu_ x x' \<Longrightarrow>\<^sub>t P' x x') \<Longrightarrow> list_assn uu_ (v # va) [] \<Longrightarrow>\<^sub>t list_assn P' (v # va) []
 4. \<And>uu_ v va. (\<And>x x'. uu_ x x' \<Longrightarrow>\<^sub>t P' x x') \<Longrightarrow> list_assn uu_ [] (v # va) \<Longrightarrow>\<^sub>t list_assn P' [] (v # va)
[PROOF STEP]
by (auto intro: entt_star_mono)