[STATEMENT]
lemma hn_rel_compI:
    "\<lbrakk>nofail a; (b,a)\<in>\<langle>R2\<rangle>nres_rel\<rbrakk> \<Longrightarrow> hn_rel R1 b c \<Longrightarrow>\<^sub>A hn_rel (hr_comp R1 R2) a c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nofail a; (b, a) \<in> \<langle>R2\<rangle>nres_rel\<rbrakk> \<Longrightarrow> hn_rel R1 b c \<Longrightarrow>\<^sub>A hn_rel (hr_comp R1 R2) a c
[PROOF STEP]
unfolding hr_comp_def hn_rel_def nres_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nofail a; (b, a) \<in> {(c, a). c \<le> \<Down> R2 a}\<rbrakk> \<Longrightarrow> \<exists>\<^sub>Ax. R1 x c * \<up> (RETURN x \<le> b) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax. (\<exists>\<^sub>Ab. R1 b c * \<up> ((b, x) \<in> R2)) * \<up> (RETURN x \<le> a)
[PROOF STEP]
apply (clarsimp intro!: ent_ex_preI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>nofail a; b \<le> \<Down> R2 a; RETURN x \<le> b\<rbrakk> \<Longrightarrow> R1 x c \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax b. R1 b c * \<up> ((b, x) \<in> R2 \<and> RETURN x \<le> a)
[PROOF STEP]
apply (drule (1) order_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>nofail a; b \<le> \<Down> R2 a; RETURN x \<le> \<Down> R2 a\<rbrakk> \<Longrightarrow> R1 x c \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax b. R1 b c * \<up> ((b, x) \<in> R2 \<and> RETURN x \<le> a)
[PROOF STEP]
apply (simp add: ret_le_down_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>nofail a; b \<le> \<Down> R2 a; \<exists>aa. (x, aa) \<in> R2 \<and> RETURN aa \<le> a\<rbrakk> \<Longrightarrow> R1 x c \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax b. R1 b c * \<up> ((b, x) \<in> R2 \<and> RETURN x \<le> a)
[PROOF STEP]
by sep_auto


[STATEMENT]
lemma hr_comp_precise[constraint_rules]:
    assumes [safe_constraint_rules]: "precise R"
    assumes SV: "single_valued S"
    shows "precise (hr_comp R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise (hr_comp R S)
[PROOF STEP]
apply (rule preciseI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F'. h \<Turnstile> hr_comp R S a p * F \<and>\<^sub>A hr_comp R S a' p * F' \<Longrightarrow> a = a'
[PROOF STEP]
unfolding hr_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F'. h \<Turnstile> (\<exists>\<^sub>Ab. R b p * \<up> ((b, a) \<in> S)) * F \<and>\<^sub>A (\<exists>\<^sub>Ab. R b p * \<up> ((b, a') \<in> S)) * F' \<Longrightarrow> a = a'
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa b p F F' ba bb. \<lbrakk>(aa, b) \<Turnstile> R bb p * F \<and>\<^sub>A R ba p * F'; (bb, a) \<in> S; (ba, a') \<in> S\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
by (metis SV assms(1) preciseD single_valuedD)


[STATEMENT]
lemma hr_comp_assoc: "hr_comp (hr_comp R S) T = hr_comp R (S O T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hr_comp (hr_comp R S) T = hr_comp R (S O T)
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. hr_comp (hr_comp R S) T x xa = hr_comp R (S O T) x xa
[PROOF STEP]
unfolding hr_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (\<exists>\<^sub>Ab. (\<exists>\<^sub>Aba. R ba xa * \<up> ((ba, b) \<in> S)) * \<up> ((b, x) \<in> T)) = (\<exists>\<^sub>Ab. R b xa * \<up> ((b, x) \<in> S O T))
[PROOF STEP]
apply (rule ent_iffI; clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<exists>\<^sub>Ab ba. R ba xa * \<up> ((ba, b) \<in> S \<and> (b, x) \<in> T) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. R b xa * \<up> ((b, x) \<in> S O T)
 2. \<And>x xa. \<exists>\<^sub>Ab. R b xa * \<up> ((b, x) \<in> S O T) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab ba. R ba xa * \<up> ((ba, b) \<in> S \<and> (b, x) \<in> T)
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<exists>\<^sub>Ab. R b xa * \<up> ((b, x) \<in> S O T) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab ba. R ba xa * \<up> ((ba, b) \<in> S \<and> (b, x) \<in> T)
[PROOF STEP]
apply (rule ent_ex_preI; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb y z. \<lbrakk>(xb, y) \<in> S; (y, z) \<in> T\<rbrakk> \<Longrightarrow> R xb xa \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab ba. R ba xa * \<up> ((ba, b) \<in> S \<and> (b, z) \<in> T)
[PROOF STEP]
(* TODO:
      sep_auto/solve_entails is too eager splitting the subgoal here! *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb y z. \<lbrakk>(xb, y) \<in> S; (y, z) \<in> T\<rbrakk> \<Longrightarrow> R xb xa \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab ba. R ba xa * \<up> ((ba, b) \<in> S \<and> (b, z) \<in> T)
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hnr_comp:
    assumes R: "\<And>b1 c1. P b1 \<Longrightarrow> hn_refine (R1 b1 c1 * \<Gamma>) (c c1) (R1p b1 c1 * \<Gamma>') R (b b1)"
    assumes S: "\<And>a1 b1. \<lbrakk>Q a1; (b1,a1)\<in>R1'\<rbrakk> \<Longrightarrow> (b b1,a a1)\<in>\<langle>R'\<rangle>nres_rel"
    assumes PQ: "\<And>a1 b1. \<lbrakk>Q a1; (b1,a1)\<in>R1'\<rbrakk> \<Longrightarrow> P b1"
    assumes Q: "Q a1"
    shows "hn_refine
      (hr_comp R1 R1' a1 c1 * \<Gamma>)
      (c c1)
      (hr_comp R1p R1' a1 c1 * \<Gamma>')
      (hr_comp R R')
      (a a1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hr_comp R1 R1' a1 c1 * \<Gamma>) (c c1) (hr_comp R1p R1' a1 c1 * \<Gamma>') (hr_comp R R') (a a1)
[PROOF STEP]
unfolding hn_refine_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (a a1) \<longrightarrow> <hr_comp R1 R1' a1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
proof clarsimp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nofail (a a1) \<Longrightarrow> <hr_comp R1 R1' a1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
assume NF: "nofail (a a1)"
[PROOF STATE]
proof (state)
this:
nofail (a a1)

goal (1 subgoal):
 1. nofail (a a1) \<Longrightarrow> <hr_comp R1 R1' a1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
show "
      <hr_comp R1 R1' a1 c1 * \<Gamma>>
        c c1
      <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <hr_comp R1 R1' a1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
apply (subst hr_comp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <(\<exists>\<^sub>Ab. R1 b c1 * \<up> ((b, a1) \<in> R1')) * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
apply (clarsimp intro!: norm_pre_ex_rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. (b, a1) \<in> R1' \<Longrightarrow> <R1 b c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. (b, a1) \<in> R1' \<Longrightarrow> <R1 b c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
fix b1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. (b, a1) \<in> R1' \<Longrightarrow> <R1 b c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
assume R1: "(b1, a1) \<in> R1'"
[PROOF STATE]
proof (state)
this:
(b1, a1) \<in> R1'

goal (1 subgoal):
 1. \<And>b. (b, a1) \<in> R1' \<Longrightarrow> <R1 b c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
from S R1 Q
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Q ?a1.0; (?b1.0, ?a1.0) \<in> R1'\<rbrakk> \<Longrightarrow> (b ?b1.0, a ?a1.0) \<in> \<langle>R'\<rangle>nres_rel
(b1, a1) \<in> R1'
Q a1
[PROOF STEP]
have R': "(b b1, a a1) \<in> \<langle>R'\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q ?a1.0; (?b1.0, ?a1.0) \<in> R1'\<rbrakk> \<Longrightarrow> (b ?b1.0, a ?a1.0) \<in> \<langle>R'\<rangle>nres_rel
(b1, a1) \<in> R1'
Q a1

goal (1 subgoal):
 1. (b b1, a a1) \<in> \<langle>R'\<rangle>nres_rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(b b1, a a1) \<in> \<langle>R'\<rangle>nres_rel

goal (1 subgoal):
 1. \<And>b. (b, a1) \<in> R1' \<Longrightarrow> <R1 b c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
with NF
[PROOF STATE]
proof (chain)
picking this:
nofail (a a1)
(b b1, a a1) \<in> \<langle>R'\<rangle>nres_rel
[PROOF STEP]
have NFB: "nofail (b b1)"
[PROOF STATE]
proof (prove)
using this:
nofail (a a1)
(b b1, a a1) \<in> \<langle>R'\<rangle>nres_rel

goal (1 subgoal):
 1. nofail (b b1)
[PROOF STEP]
by (simp add: nres_rel_def pw_le_iff refine_pw_simps)
[PROOF STATE]
proof (state)
this:
nofail (b b1)

goal (1 subgoal):
 1. \<And>b. (b, a1) \<in> R1' \<Longrightarrow> <R1 b c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
from PQ R1 Q
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Q ?a1.0; (?b1.0, ?a1.0) \<in> R1'\<rbrakk> \<Longrightarrow> P ?b1.0
(b1, a1) \<in> R1'
Q a1
[PROOF STEP]
have P: "P b1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q ?a1.0; (?b1.0, ?a1.0) \<in> R1'\<rbrakk> \<Longrightarrow> P ?b1.0
(b1, a1) \<in> R1'
Q a1

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

goal (1 subgoal):
 1. \<And>b. (b, a1) \<in> R1' \<Longrightarrow> <R1 b c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
with NFB R
[PROOF STATE]
proof (chain)
picking this:
nofail (b b1)
P ?b1.0 \<Longrightarrow> hn_refine (R1 ?b1.0 ?c1.0 * \<Gamma>) (c ?c1.0) (R1p ?b1.0 ?c1.0 * \<Gamma>') R (b ?b1.0)
P b1
[PROOF STEP]
have "<R1 b1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel R (b b1) r * (R1p b1 c1 * \<Gamma>')>\<^sub>t"
[PROOF STATE]
proof (prove)
using this:
nofail (b b1)
P ?b1.0 \<Longrightarrow> hn_refine (R1 ?b1.0 ?c1.0 * \<Gamma>) (c ?c1.0) (R1p ?b1.0 ?c1.0 * \<Gamma>') R (b ?b1.0)
P b1

goal (1 subgoal):
 1. <R1 b1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel R (b b1) r * (R1p b1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
unfolding hn_refine_alt
[PROOF STATE]
proof (prove)
using this:
nofail (b b1)
P ?b1.0 \<Longrightarrow> nofail (b ?b1.0) \<longrightarrow> <R1 ?b1.0 ?c1.0 * \<Gamma>> c ?c1.0 <\<lambda>r. hn_rel R (b ?b1.0) r * (R1p ?b1.0 ?c1.0 * \<Gamma>')>\<^sub>t
P b1

goal (1 subgoal):
 1. <R1 b1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel R (b b1) r * (R1p b1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
<R1 b1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel R (b b1) r * (R1p b1 c1 * \<Gamma>')>\<^sub>t

goal (1 subgoal):
 1. \<And>b. (b, a1) \<in> R1' \<Longrightarrow> <R1 b c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
thus "<R1 b1 c1 * \<Gamma>>
        c c1
        <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t"
[PROOF STATE]
proof (prove)
using this:
<R1 b1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel R (b b1) r * (R1p b1 c1 * \<Gamma>')>\<^sub>t

goal (1 subgoal):
 1. <R1 b1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t
[PROOF STEP]
apply (rule cons_post_rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. hn_rel R (b b1) x * (R1p b1 c1 * \<Gamma>') * true \<Longrightarrow>\<^sub>A hn_rel (hr_comp R R') (a a1) x * (hr_comp R1p R1' a1 c1 * \<Gamma>') * true
[PROOF STEP]
apply (solve_entails)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. hn_rel R (b b1) x * R1p b1 c1 * \<Gamma>' * true \<Longrightarrow>\<^sub>A hn_rel (hr_comp R R') (a a1) x * hr_comp R1p R1' a1 c1 * \<Gamma>' * true
[PROOF STEP]
by (intro ent_star_mono hn_rel_compI[OF NF R'] hr_compI[OF R1] ent_refl)
[PROOF STATE]
proof (state)
this:
<R1 b1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
<hr_comp R1 R1' a1 c1 * \<Gamma>> c c1 <\<lambda>r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \<Gamma>')>\<^sub>t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hnr_comp1_aux:
    assumes R: "\<And>b1 c1. P b1 \<Longrightarrow> hn_refine (hn_ctxt R1 b1 c1) (c c1) (hn_ctxt R1p b1 c1) R (b$b1)"
    assumes S: "\<And>a1 b1. \<lbrakk>Q a1; (b1,a1)\<in>R1'\<rbrakk> \<Longrightarrow> (b$b1,a$a1)\<in>\<langle>R'\<rangle>nres_rel"
    assumes PQ: "\<And>a1 b1. \<lbrakk>Q a1; (b1,a1)\<in>R1'\<rbrakk> \<Longrightarrow> P b1"
    assumes Q: "Q a1"
    shows "hn_refine
      (hr_comp R1 R1' a1 c1)
      (c c1)
      (hr_comp R1p R1' a1 c1)
      (hr_comp R R')
      (a a1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hr_comp R1 R1' a1 c1) (c c1) (hr_comp R1p R1' a1 c1) (hr_comp R R') (a a1)
[PROOF STEP]
using assms hnr_comp[where \<Gamma>=emp and \<Gamma>'=emp and a=a and b=b and c=c and P=P and Q=Q]
[PROOF STATE]
proof (prove)
using this:
P ?b1.0 \<Longrightarrow> hn_refine (hn_ctxt R1 ?b1.0 ?c1.0) (c ?c1.0) (hn_ctxt R1p ?b1.0 ?c1.0) R (b $ ?b1.0)
\<lbrakk>Q ?a1.0; (?b1.0, ?a1.0) \<in> R1'\<rbrakk> \<Longrightarrow> (b $ ?b1.0, a $ ?a1.0) \<in> \<langle>R'\<rangle>nres_rel
\<lbrakk>Q ?a1.0; (?b1.0, ?a1.0) \<in> R1'\<rbrakk> \<Longrightarrow> P ?b1.0
Q a1
\<lbrakk>\<And>b1 c1. P b1 \<Longrightarrow> hn_refine (?R1.0 b1 c1 * emp) (c c1) (?R1p b1 c1 * emp) ?R (b b1); \<And>a1 b1. \<lbrakk>Q a1; (b1, a1) \<in> ?R1'\<rbrakk> \<Longrightarrow> (b b1, a a1) \<in> \<langle>?R'\<rangle>nres_rel; \<And>a1 b1. \<lbrakk>Q a1; (b1, a1) \<in> ?R1'\<rbrakk> \<Longrightarrow> P b1; Q ?a1.0\<rbrakk> \<Longrightarrow> hn_refine (hr_comp ?R1.0 ?R1' ?a1.0 ?c1.0 * emp) (c ?c1.0) (hr_comp ?R1p ?R1' ?a1.0 ?c1.0 * emp) (hr_comp ?R ?R') (a ?a1.0)

goal (1 subgoal):
 1. hn_refine (hr_comp R1 R1' a1 c1) (c c1) (hr_comp R1p R1' a1 c1) (hr_comp R R') (a a1)
[PROOF STEP]
unfolding hn_ctxt_def
[PROOF STATE]
proof (prove)
using this:
P ?b1.0 \<Longrightarrow> hn_refine (R1 ?b1.0 ?c1.0) (c ?c1.0) (R1p ?b1.0 ?c1.0) R (b $ ?b1.0)
\<lbrakk>Q ?a1.0; (?b1.0, ?a1.0) \<in> R1'\<rbrakk> \<Longrightarrow> (b $ ?b1.0, a $ ?a1.0) \<in> \<langle>R'\<rangle>nres_rel
\<lbrakk>Q ?a1.0; (?b1.0, ?a1.0) \<in> R1'\<rbrakk> \<Longrightarrow> P ?b1.0
Q a1
\<lbrakk>\<And>b1 c1. P b1 \<Longrightarrow> hn_refine (?R1.0 b1 c1 * emp) (c c1) (?R1p b1 c1 * emp) ?R (b b1); \<And>a1 b1. \<lbrakk>Q a1; (b1, a1) \<in> ?R1'\<rbrakk> \<Longrightarrow> (b b1, a a1) \<in> \<langle>?R'\<rangle>nres_rel; \<And>a1 b1. \<lbrakk>Q a1; (b1, a1) \<in> ?R1'\<rbrakk> \<Longrightarrow> P b1; Q ?a1.0\<rbrakk> \<Longrightarrow> hn_refine (hr_comp ?R1.0 ?R1' ?a1.0 ?c1.0 * emp) (c ?c1.0) (hr_comp ?R1p ?R1' ?a1.0 ?c1.0 * emp) (hr_comp ?R ?R') (a ?a1.0)

goal (1 subgoal):
 1. hn_refine (hr_comp R1 R1' a1 c1) (c c1) (hr_comp R1p R1' a1 c1) (hr_comp R R') (a a1)
[PROOF STEP]
by auto


[STATEMENT]
lemma hfcomp:
    assumes A: "(f,g) \<in> [P]\<^sub>a RR' \<rightarrow> S"
    assumes B: "(g,h) \<in> [Q]\<^sub>f T \<rightarrow> \<langle>U\<rangle>nres_rel"
    shows "(f,h) \<in> [\<lambda>a. Q a \<and> (\<forall>a'. (a',a)\<in>T \<longrightarrow> P a')]\<^sub>a
      hrp_comp RR' T \<rightarrow> hr_comp S U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [\<lambda>a. Q a \<and> (\<forall>a'. (a', a) \<in> T \<longrightarrow> P a')]\<^sub>a hrp_comp RR' T \<rightarrow> hr_comp S U
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> [P]\<^sub>a RR' \<rightarrow> S
(g, h) \<in> [Q]\<^sub>f T \<rightarrow> \<langle>U\<rangle>nres_rel

goal (1 subgoal):
 1. (f, h) \<in> [\<lambda>a. Q a \<and> (\<forall>a'. (a', a) \<in> T \<longrightarrow> P a')]\<^sub>a hrp_comp RR' T \<rightarrow> hr_comp S U
[PROOF STEP]
unfolding fref_def hfref_def hrp_comp_def
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> {(f, g). \<forall>c a. P a \<longrightarrow> hn_refine (fst RR' a c) (f c) (snd RR' a c) S (g a)}
(g, h) \<in> {(f, g). \<forall>x y. Q y \<and> (x, y) \<in> T \<longrightarrow> (f x, g y) \<in> \<langle>U\<rangle>nres_rel}

goal (1 subgoal):
 1. (f, h) \<in> {(f, g). \<forall>c a. Q a \<and> (\<forall>a'. (a', a) \<in> T \<longrightarrow> P a') \<longrightarrow> hn_refine (fst (hr_comp (fst RR') T, hr_comp (snd RR') T) a c) (f c) (snd (hr_comp (fst RR') T, hr_comp (snd RR') T) a c) (hr_comp S U) (g a)}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a. \<lbrakk>\<forall>c a. P a \<longrightarrow> hn_refine (fst RR' a c) (f c) (snd RR' a c) S (g a); \<forall>x y. Q y \<and> (x, y) \<in> T \<longrightarrow> (g x, h y) \<in> \<langle>U\<rangle>nres_rel; Q a; \<forall>a'. (a', a) \<in> T \<longrightarrow> P a'\<rbrakk> \<Longrightarrow> hn_refine (hr_comp (fst RR') T a c) (f c) (hr_comp (snd RR') T a c) (hr_comp S U) (h a)
[PROOF STEP]
apply (rule hnr_comp1_aux[of
        P "fst RR'" f "snd RR'" S g "\<lambda>a. Q a \<and> (\<forall>a'. (a',a)\<in>T \<longrightarrow> P a')" T h U])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c a b1 c1. \<lbrakk>\<forall>c a. P a \<longrightarrow> hn_refine (fst RR' a c) (f c) (snd RR' a c) S (g a); \<forall>x y. Q y \<and> (x, y) \<in> T \<longrightarrow> (g x, h y) \<in> \<langle>U\<rangle>nres_rel; Q a; \<forall>a'. (a', a) \<in> T \<longrightarrow> P a'; P b1\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (fst RR') b1 c1) (f c1) (hn_ctxt (snd RR') b1 c1) S (g $ b1)
 2. \<And>c a a1 b1. \<lbrakk>\<forall>c a. P a \<longrightarrow> hn_refine (fst RR' a c) (f c) (snd RR' a c) S (g a); \<forall>x y. Q y \<and> (x, y) \<in> T \<longrightarrow> (g x, h y) \<in> \<langle>U\<rangle>nres_rel; Q a; \<forall>a'. (a', a) \<in> T \<longrightarrow> P a'; Q a1 \<and> (\<forall>a'. (a', a1) \<in> T \<longrightarrow> P a'); (b1, a1) \<in> T\<rbrakk> \<Longrightarrow> (g $ b1, h $ a1) \<in> \<langle>U\<rangle>nres_rel
 3. \<And>c a a1 b1. \<lbrakk>\<forall>c a. P a \<longrightarrow> hn_refine (fst RR' a c) (f c) (snd RR' a c) S (g a); \<forall>x y. Q y \<and> (x, y) \<in> T \<longrightarrow> (g x, h y) \<in> \<langle>U\<rangle>nres_rel; Q a; \<forall>a'. (a', a) \<in> T \<longrightarrow> P a'; Q a1 \<and> (\<forall>a'. (a', a1) \<in> T \<longrightarrow> P a'); (b1, a1) \<in> T\<rbrakk> \<Longrightarrow> P b1
 4. \<And>c a. \<lbrakk>\<forall>c a. P a \<longrightarrow> hn_refine (fst RR' a c) (f c) (snd RR' a c) S (g a); \<forall>x y. Q y \<and> (x, y) \<in> T \<longrightarrow> (g x, h y) \<in> \<langle>U\<rangle>nres_rel; Q a; \<forall>a'. (a', a) \<in> T \<longrightarrow> P a'\<rbrakk> \<Longrightarrow> Q a \<and> (\<forall>a'. (a', a) \<in> T \<longrightarrow> P a')
[PROOF STEP]
apply (auto simp: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hfref_weaken_pre_nofail:
    assumes "(f,g) \<in> [P]\<^sub>a R \<rightarrow> S"
    shows "(f,g) \<in> [\<lambda>x. nofail (g x) \<longrightarrow> P x]\<^sub>a R \<rightarrow> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> [\<lambda>x. nofail (g x) \<longrightarrow> P x]\<^sub>a R \<rightarrow> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> [P]\<^sub>a R \<rightarrow> S

goal (1 subgoal):
 1. (f, g) \<in> [\<lambda>x. nofail (g x) \<longrightarrow> P x]\<^sub>a R \<rightarrow> S
[PROOF STEP]
unfolding hfref_def hn_refine_def
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> {(f, g). \<forall>c a. P a \<longrightarrow> nofail (g a) \<longrightarrow> <fst R a c> f c <\<lambda>r. snd R a c * (\<exists>\<^sub>Ax. S x r * \<up> (RETURN x \<le> g a))>\<^sub>t}

goal (1 subgoal):
 1. (f, g) \<in> {(f, ga). \<forall>c a. (nofail (g a) \<longrightarrow> P a) \<longrightarrow> nofail (ga a) \<longrightarrow> <fst R a c> f c <\<lambda>r. snd R a c * (\<exists>\<^sub>Ax. S x r * \<up> (RETURN x \<le> ga a))>\<^sub>t}
[PROOF STEP]
by auto


[STATEMENT]
lemma hfref_cons:
    assumes "(f,g) \<in> [P]\<^sub>a R \<rightarrow> S"
    assumes "\<And>x. P' x \<Longrightarrow> P x"
    assumes "\<And>x y. fst R' x y \<Longrightarrow>\<^sub>t fst R x y"
    assumes "\<And>x y. snd R x y \<Longrightarrow>\<^sub>t snd R' x y"
    assumes "\<And>x y. S x y \<Longrightarrow>\<^sub>t S' x y"
    shows "(f,g) \<in> [P']\<^sub>a R' \<rightarrow> S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> [P']\<^sub>a R' \<rightarrow> S'
[PROOF STEP]
unfolding hfref_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> {(f, g). \<forall>c a. P' a \<longrightarrow> hn_refine (fst R' a c) (f c) (snd R' a c) S' (g a)}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a. P' a \<Longrightarrow> hn_refine (fst R' a c) (f c) (snd R' a c) S' (g a)
[PROOF STEP]
apply (rule hn_refine_cons)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c a. P' a \<Longrightarrow> fst R' a c \<Longrightarrow>\<^sub>t ?P'3 c a
 2. \<And>c a. P' a \<Longrightarrow> hn_refine (?P'3 c a) (f c) (?Q3 c a) (?R3 c a) (g a)
 3. \<And>c a. P' a \<Longrightarrow> ?Q3 c a \<Longrightarrow>\<^sub>t snd R' a c
 4. \<And>c a x y. P' a \<Longrightarrow> ?R3 c a x y \<Longrightarrow>\<^sub>t S' x y
[PROOF STEP]
apply (rule assms(3))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c a. P' a \<Longrightarrow> hn_refine (fst R a c) (f c) (?Q3 c a) (?R3 c a) (g a)
 2. \<And>c a. P' a \<Longrightarrow> ?Q3 c a \<Longrightarrow>\<^sub>t snd R' a c
 3. \<And>c a x y. P' a \<Longrightarrow> ?R3 c a x y \<Longrightarrow>\<^sub>t S' x y
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c a. P' a \<Longrightarrow> ?Q3 c a \<Longrightarrow>\<^sub>t snd R' a c
 2. \<And>c a x y. P' a \<Longrightarrow> ?R3 c a x y \<Longrightarrow>\<^sub>t S' x y
 3. \<And>c a. P' a \<Longrightarrow> hn_refine (fst R a c) (f c) (?Q3 c a) (?R3 c a) (g a)
[PROOF STEP]
apply (rule entt_trans[OF assms(4)]; sep_auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c a x y. P' a \<Longrightarrow> ?R3 c a x y \<Longrightarrow>\<^sub>t S' x y
 2. \<And>c a. P' a \<Longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) (?R3 c a) (g a)
[PROOF STEP]
apply (rule assms(5))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a. P' a \<Longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (g a)
[PROOF STEP]
apply (frule assms(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a. \<lbrakk>P' a; P a\<rbrakk> \<Longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (g a)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> [P]\<^sub>a R \<rightarrow> S

goal (1 subgoal):
 1. \<And>c a. \<lbrakk>P' a; P a\<rbrakk> \<Longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (g a)
[PROOF STEP]
unfolding hfref_def
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> {(f, g). \<forall>c a. P a \<longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (g a)}

goal (1 subgoal):
 1. \<And>c a. \<lbrakk>P' a; P a\<rbrakk> \<Longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (g a)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_hrp_comp:
    "hrp_comp (A *\<^sub>a B) (C \<times>\<^sub>r D) = hrp_comp A C *\<^sub>a hrp_comp B D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hrp_comp (A *\<^sub>a B) (C \<times>\<^sub>r D) = hrp_comp A C *\<^sub>a hrp_comp B D
[PROOF STEP]
unfolding hrp_comp_def hfprod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hr_comp (fst (fst A \<times>\<^sub>a fst B, snd A \<times>\<^sub>a snd B)) (C \<times>\<^sub>r D), hr_comp (snd (fst A \<times>\<^sub>a fst B, snd A \<times>\<^sub>a snd B)) (C \<times>\<^sub>r D)) = (fst (hr_comp (fst A) C, hr_comp (snd A) C) \<times>\<^sub>a fst (hr_comp (fst B) D, hr_comp (snd B) D), snd (hr_comp (fst A) C, hr_comp (snd A) C) \<times>\<^sub>a snd (hr_comp (fst B) D, hr_comp (snd B) D))
[PROOF STEP]
by simp


[STATEMENT]
lemma hrp_comp_keep: "hrp_comp (A\<^sup>k) B = (hr_comp A B)\<^sup>k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hrp_comp (A\<^sup>k) B = (hr_comp A B)\<^sup>k
[PROOF STEP]
by (auto simp: hrp_comp_def)


[STATEMENT]
lemma hr_comp_invalid: "hr_comp (invalid_assn R1) R2 = invalid_assn (hr_comp R1 R2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hr_comp (invalid_assn R1) R2 = invalid_assn (hr_comp R1 R2)
[PROOF STEP]
apply (intro ent_iffI entailsI ext)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa h. h \<Turnstile> hr_comp (invalid_assn R1) R2 x xa \<Longrightarrow> h \<Turnstile> invalid_assn (hr_comp R1 R2) x xa
 2. \<And>x xa h. h \<Turnstile> invalid_assn (hr_comp R1 R2) x xa \<Longrightarrow> h \<Turnstile> hr_comp (invalid_assn R1) R2 x xa
[PROOF STEP]
unfolding invalid_assn_def hr_comp_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa h. h \<Turnstile> (\<exists>\<^sub>Ab. \<up> (\<exists>h. h \<Turnstile> R1 b xa) * true * \<up> ((b, x) \<in> R2)) \<Longrightarrow> h \<Turnstile> \<up> (\<exists>h. h \<Turnstile> (\<exists>\<^sub>Ab. R1 b xa * \<up> ((b, x) \<in> R2))) * true
 2. \<And>x xa h. h \<Turnstile> \<up> (\<exists>h. h \<Turnstile> (\<exists>\<^sub>Ab. R1 b xa * \<up> ((b, x) \<in> R2))) * true \<Longrightarrow> h \<Turnstile> (\<exists>\<^sub>Ab. \<up> (\<exists>h. h \<Turnstile> R1 b xa) * true * \<up> ((b, x) \<in> R2))
[PROOF STEP]
by auto


[STATEMENT]
lemma hrp_comp_dest: "hrp_comp (A\<^sup>d) B = (hr_comp A B)\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hrp_comp (A\<^sup>d) B = (hr_comp A B)\<^sup>d
[PROOF STEP]
by (auto simp: hrp_comp_def hr_comp_invalid)


[STATEMENT]
lemma hfref_imp: "hrp_imp RR RR' \<Longrightarrow> [P]\<^sub>a RR \<rightarrow> S \<subseteq> [P]\<^sub>a RR' \<rightarrow> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hrp_imp RR RR' \<Longrightarrow> [P]\<^sub>a RR \<rightarrow> S \<subseteq> [P]\<^sub>a RR' \<rightarrow> S
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>hrp_imp RR RR'; (a, b) \<in> [P]\<^sub>a RR \<rightarrow> S\<rbrakk> \<Longrightarrow> (a, b) \<in> [P]\<^sub>a RR' \<rightarrow> S
[PROOF STEP]
apply (erule hfref_cons)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b x. \<lbrakk>hrp_imp RR RR'; P x\<rbrakk> \<Longrightarrow> P x
 2. \<And>a b x y. hrp_imp RR RR' \<Longrightarrow> fst RR' x y \<Longrightarrow>\<^sub>t fst RR x y
 3. \<And>a b x y. hrp_imp RR RR' \<Longrightarrow> snd RR x y \<Longrightarrow>\<^sub>t snd RR' x y
 4. \<And>a b x y. hrp_imp RR RR' \<Longrightarrow> S x y \<Longrightarrow>\<^sub>t S x y
[PROOF STEP]
apply (simp_all add: hrp_imp_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hrp_imp_refl: "hrp_imp RR RR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hrp_imp RR RR
[PROOF STEP]
unfolding hrp_imp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. (fst RR a b \<Longrightarrow>\<^sub>t fst RR a b) \<and> (snd RR a b \<Longrightarrow>\<^sub>t snd RR a b)
[PROOF STEP]
by auto


[STATEMENT]
lemma hrp_imp_reflI: "RR = RR' \<Longrightarrow> hrp_imp RR RR'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR = RR' \<Longrightarrow> hrp_imp RR RR'
[PROOF STEP]
unfolding hrp_imp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RR = RR' \<Longrightarrow> \<forall>a b. (fst RR' a b \<Longrightarrow>\<^sub>t fst RR a b) \<and> (snd RR a b \<Longrightarrow>\<^sub>t snd RR' a b)
[PROOF STEP]
by auto


[STATEMENT]
lemma hrp_comp_cong: "hrp_imp A A' \<Longrightarrow> B=B' \<Longrightarrow> hrp_imp (hrp_comp A B) (hrp_comp A' B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hrp_imp A A'; B = B'\<rbrakk> \<Longrightarrow> hrp_imp (hrp_comp A B) (hrp_comp A' B')
[PROOF STEP]
by (sep_auto simp: hrp_imp_def hrp_comp_def hr_comp_def entailst_def)


[STATEMENT]
lemma hrp_prod_cong: "hrp_imp A A' \<Longrightarrow> hrp_imp B B' \<Longrightarrow> hrp_imp (A*\<^sub>aB) (A'*\<^sub>aB')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hrp_imp A A'; hrp_imp B B'\<rbrakk> \<Longrightarrow> hrp_imp (A *\<^sub>a B) (A' *\<^sub>a B')
[PROOF STEP]
by (sep_auto simp: hrp_imp_def prod_assn_def intro: entt_star_mono)


[STATEMENT]
lemma hrp_imp_trans: "hrp_imp A B \<Longrightarrow> hrp_imp B C \<Longrightarrow> hrp_imp A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hrp_imp A B; hrp_imp B C\<rbrakk> \<Longrightarrow> hrp_imp A C
[PROOF STEP]
unfolding hrp_imp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b. (fst B a b \<Longrightarrow>\<^sub>t fst A a b) \<and> (snd A a b \<Longrightarrow>\<^sub>t snd B a b); \<forall>a b. (fst C a b \<Longrightarrow>\<^sub>t fst B a b) \<and> (snd B a b \<Longrightarrow>\<^sub>t snd C a b)\<rbrakk> \<Longrightarrow> \<forall>a b. (fst C a b \<Longrightarrow>\<^sub>t fst A a b) \<and> (snd A a b \<Longrightarrow>\<^sub>t snd C a b)
[PROOF STEP]
by (fastforce intro: entt_trans)


[STATEMENT]
lemma fcomp_norm_dflt_init: "x\<in>[P]\<^sub>a R \<rightarrow> T \<Longrightarrow> hrp_imp R S \<Longrightarrow> x\<in>[P]\<^sub>a S \<rightarrow> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> [P]\<^sub>a R \<rightarrow> T; hrp_imp R S\<rbrakk> \<Longrightarrow> x \<in> [P]\<^sub>a S \<rightarrow> T
[PROOF STEP]
apply (erule rev_subsetD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hrp_imp R S \<Longrightarrow> [P]\<^sub>a R \<rightarrow> T \<subseteq> [P]\<^sub>a S \<rightarrow> T
[PROOF STEP]
by (rule hfref_imp)


[STATEMENT]
lemma comp_PRE_cong[cong]:
    assumes "R\<equiv>R'"
    assumes "\<And>x. P x \<equiv> P' x"
    assumes "\<And>x. S x \<equiv> S' x"
    assumes "\<And>x y. \<lbrakk>P x; (y,x)\<in>R; y\<in>Domain R; S' x \<rbrakk> \<Longrightarrow> Q x y \<equiv> Q' x y"
    shows "comp_PRE R P Q S \<equiv> comp_PRE R' P' Q' S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_PRE R P Q S \<equiv> comp_PRE R' P' Q' S'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
R \<equiv> R'
P ?x \<equiv> P' ?x
S ?x \<equiv> S' ?x
\<lbrakk>P ?x; (?y, ?x) \<in> R; ?y \<in> Domain R; S' ?x\<rbrakk> \<Longrightarrow> Q ?x ?y \<equiv> Q' ?x ?y

goal (1 subgoal):
 1. comp_PRE R P Q S \<equiv> comp_PRE R' P' Q' S'
[PROOF STEP]
by (fastforce simp: comp_PRE_def intro!: eq_reflection ext)


[STATEMENT]
lemma fref_compI_PRE:
    "\<lbrakk> (f,g)\<in>fref P R1 R2; (g,h)\<in>fref Q S1 S2 \<rbrakk>
      \<Longrightarrow> (f,h) \<in> fref (comp_PRE S1 Q (\<lambda>_. P) (\<lambda>_. True)) (R1 O S1) (R2 O S2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(f, g) \<in> [P]\<^sub>f R1 \<rightarrow> R2; (g, h) \<in> [Q]\<^sub>f S1 \<rightarrow> S2\<rbrakk> \<Longrightarrow> (f, h) \<in> [comp_PRE S1 Q (\<lambda>_. P) (\<lambda>_. True)]\<^sub>f R1 O S1 \<rightarrow> R2 O S2
[PROOF STEP]
using fref_compI[of P R1 R2 Q S1 S2]
[PROOF STATE]
proof (prove)
using this:
([P]\<^sub>f R1 \<rightarrow> R2) O ([Q]\<^sub>f S1 \<rightarrow> S2) \<subseteq> [\<lambda>x. Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> P y)]\<^sub>f R1 O S1 \<rightarrow> R2 O S2

goal (1 subgoal):
 1. \<lbrakk>(f, g) \<in> [P]\<^sub>f R1 \<rightarrow> R2; (g, h) \<in> [Q]\<^sub>f S1 \<rightarrow> S2\<rbrakk> \<Longrightarrow> (f, h) \<in> [comp_PRE S1 Q (\<lambda>_. P) (\<lambda>_. True)]\<^sub>f R1 O S1 \<rightarrow> R2 O S2
[PROOF STEP]
unfolding comp_PRE_def
[PROOF STATE]
proof (prove)
using this:
([P]\<^sub>f R1 \<rightarrow> R2) O ([Q]\<^sub>f S1 \<rightarrow> S2) \<subseteq> [\<lambda>x. Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> P y)]\<^sub>f R1 O S1 \<rightarrow> R2 O S2

goal (1 subgoal):
 1. \<lbrakk>(f, g) \<in> [P]\<^sub>f R1 \<rightarrow> R2; (g, h) \<in> [Q]\<^sub>f S1 \<rightarrow> S2\<rbrakk> \<Longrightarrow> (f, h) \<in> [\<lambda>x. True \<longrightarrow> Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> P y)]\<^sub>f R1 O S1 \<rightarrow> R2 O S2
[PROOF STEP]
by auto


[STATEMENT]
lemma PRE_D1: "(Q x \<and> P x) \<longrightarrow> comp_PRE S1 Q (\<lambda>x _. P x) S x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q x \<and> P x \<longrightarrow> comp_PRE S1 Q (\<lambda>x _. P x) S x
[PROOF STEP]
by (auto simp: comp_PRE_def)


[STATEMENT]
lemma fref_weaken_pre:
    assumes "\<And>x. P x \<longrightarrow> P' x"
    assumes "(f,h) \<in> fref P' R S"
    shows "(f,h) \<in> fref P R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [P]\<^sub>f R \<rightarrow> S
[PROOF STEP]
apply (rule rev_subsetD[OF assms(2) fref_mono])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. P x \<Longrightarrow> P' x
 2. R \<subseteq> R
 3. S \<subseteq> S
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
P ?x \<longrightarrow> P' ?x

goal (3 subgoals):
 1. \<And>x. P x \<Longrightarrow> P' x
 2. R \<subseteq> R
 3. S \<subseteq> S
[PROOF STEP]
by auto


[STATEMENT]
lemma fref_PRE_D1:
    assumes "(f,h) \<in> fref (comp_PRE S1 Q (\<lambda>x _. P x) X) R S"
    shows "(f,h) \<in> fref (\<lambda>x. Q x \<and> P x) R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [\<lambda>x. Q x \<and> P x]\<^sub>f R \<rightarrow> S
[PROOF STEP]
by (rule fref_weaken_pre[OF PRE_D1 assms])


[STATEMENT]
lemma fref_PRE_D2:
    assumes "(f,h) \<in> fref (comp_PRE S1 Q P X) R S"
    shows "(f,h) \<in> fref (\<lambda>x. Q x \<and> (\<forall>y. (y,x)\<in>S1 \<longrightarrow> X x \<longrightarrow> P x y)) R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [\<lambda>x. Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> X x \<longrightarrow> P x y)]\<^sub>f R \<rightarrow> S
[PROOF STEP]
by (rule fref_weaken_pre[OF PRE_D2 assms])


[STATEMENT]
lemma hfref_weaken_pre:
    assumes "\<And>x. P x \<longrightarrow> P' x"
    assumes "(f,h) \<in> hfref P' R S"
    shows "(f,h) \<in> hfref P R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [P]\<^sub>a R \<rightarrow> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P ?x \<longrightarrow> P' ?x
(f, h) \<in> [P']\<^sub>a R \<rightarrow> S

goal (1 subgoal):
 1. (f, h) \<in> [P]\<^sub>a R \<rightarrow> S
[PROOF STEP]
by (auto simp: hfref_def)


[STATEMENT]
lemma hfref_weaken_pre':
    assumes "\<And>x. \<lbrakk>P x; rdomp (fst R) x\<rbrakk> \<Longrightarrow> P' x"
    assumes "(f,h) \<in> hfref P' R S"
    shows "(f,h) \<in> hfref P R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [P]\<^sub>a R \<rightarrow> S
[PROOF STEP]
apply (rule hfrefI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a. P a \<Longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (h a)
[PROOF STEP]
apply (rule hn_refine_preI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a ha. \<lbrakk>P a; ha \<Turnstile> fst R a c\<rbrakk> \<Longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (h a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P ?x; rdomp (fst R) ?x\<rbrakk> \<Longrightarrow> P' ?x
(f, h) \<in> [P']\<^sub>a R \<rightarrow> S

goal (1 subgoal):
 1. \<And>c a ha. \<lbrakk>P a; ha \<Turnstile> fst R a c\<rbrakk> \<Longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (h a)
[PROOF STEP]
by (auto simp: hfref_def rdomp_def)


[STATEMENT]
lemma hfref_weaken_pre_nofail':
    assumes "(f,g) \<in> [P]\<^sub>a R \<rightarrow> S"
    assumes "\<And>x. \<lbrakk>nofail (g x); Q x\<rbrakk> \<Longrightarrow> P x"
    shows "(f,g) \<in> [Q]\<^sub>a R \<rightarrow> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> [Q]\<^sub>a R \<rightarrow> S
[PROOF STEP]
apply (rule hfref_weaken_pre[OF _ assms(1)[THEN hfref_weaken_pre_nofail]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Q x \<longrightarrow> nofail (g x) \<longrightarrow> P x
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>nofail (g ?x); Q ?x\<rbrakk> \<Longrightarrow> P ?x

goal (1 subgoal):
 1. \<And>x. Q x \<longrightarrow> nofail (g x) \<longrightarrow> P x
[PROOF STEP]
by blast


[STATEMENT]
lemma hfref_compI_PRE_aux:
    assumes A: "(f,g) \<in> [P]\<^sub>a RR' \<rightarrow> S"
    assumes B: "(g,h) \<in> [Q]\<^sub>f T \<rightarrow> \<langle>U\<rangle>nres_rel"
    shows "(f,h) \<in> [comp_PRE T Q (\<lambda>_. P) (\<lambda>_. True)]\<^sub>a
      hrp_comp RR' T \<rightarrow> hr_comp S U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [comp_PRE T Q (\<lambda>_. P) (\<lambda>_. True)]\<^sub>a hrp_comp RR' T \<rightarrow> hr_comp S U
[PROOF STEP]
apply (rule hfref_weaken_pre[OF _ hfcomp[OF A B]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. comp_PRE T Q (\<lambda>_. P) (\<lambda>_. True) x \<longrightarrow> Q x \<and> (\<forall>a'. (a', x) \<in> T \<longrightarrow> P a')
[PROOF STEP]
by (auto simp: comp_PRE_def)


[STATEMENT]
lemma hfref_compI_PRE:
    assumes A: "(f,g) \<in> [P]\<^sub>a RR' \<rightarrow> S"
    assumes B: "(g,h) \<in> [Q]\<^sub>f T \<rightarrow> \<langle>U\<rangle>nres_rel"
    shows "(f,h) \<in> [comp_PRE T Q (\<lambda>x y. P y) (\<lambda>x. nofail (h x))]\<^sub>a
      hrp_comp RR' T \<rightarrow> hr_comp S U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [comp_PRE T Q (\<lambda>x. P) (\<lambda>x. nofail (h x))]\<^sub>a hrp_comp RR' T \<rightarrow> hr_comp S U
[PROOF STEP]
using hfref_compI_PRE_aux[OF A B, THEN hfref_weaken_pre_nofail]
[PROOF STATE]
proof (prove)
using this:
(f, h) \<in> [\<lambda>x. nofail (h x) \<longrightarrow> comp_PRE T Q (\<lambda>_. P) (\<lambda>_. True) x]\<^sub>a hrp_comp RR' T \<rightarrow> hr_comp S U

goal (1 subgoal):
 1. (f, h) \<in> [comp_PRE T Q (\<lambda>x. P) (\<lambda>x. nofail (h x))]\<^sub>a hrp_comp RR' T \<rightarrow> hr_comp S U
[PROOF STEP]
apply (rule hfref_weaken_pre[rotated])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. comp_PRE T Q (\<lambda>x. P) (\<lambda>x. nofail (h x)) x \<longrightarrow> nofail (h x) \<longrightarrow> comp_PRE T Q (\<lambda>_. P) (\<lambda>_. True) x
[PROOF STEP]
apply (auto simp: comp_PRE_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hfref_PRE_D1:
    assumes "(f,h) \<in> hfref (comp_PRE S1 Q (\<lambda>x _. P x) X) R S"
    shows "(f,h) \<in> hfref (\<lambda>x. Q x \<and> P x) R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [\<lambda>x. Q x \<and> P x]\<^sub>a R \<rightarrow> S
[PROOF STEP]
by (rule hfref_weaken_pre[OF PRE_D1 assms])


[STATEMENT]
lemma hfref_PRE_D2:
    assumes "(f,h) \<in> hfref (comp_PRE S1 Q P X) R S"
    shows "(f,h) \<in> hfref (\<lambda>x. Q x \<and> (\<forall>y. (y,x)\<in>S1 \<longrightarrow> X x \<longrightarrow> P x y)) R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [\<lambda>x. Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> X x \<longrightarrow> P x y)]\<^sub>a R \<rightarrow> S
[PROOF STEP]
by (rule hfref_weaken_pre[OF PRE_D2 assms])


[STATEMENT]
lemma hfref_PRE_D3:
    assumes "(f,h) \<in> hfref (comp_PRE S1 Q P X) R S"
    shows "(f,h) \<in> hfref (comp_PRE S1 Q P X) R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [comp_PRE S1 Q P X]\<^sub>a R \<rightarrow> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, h) \<in> [comp_PRE S1 Q P X]\<^sub>a R \<rightarrow> S

goal (1 subgoal):
 1. (f, h) \<in> [comp_PRE S1 Q P X]\<^sub>a R \<rightarrow> S
[PROOF STEP]
.


[STATEMENT]
lemma uncurry0_add_app_tag: "uncurry0 (RETURN c) = uncurry0 (RETURN$c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uncurry0 (RETURN c) = uncurry0 (RETURN $ c)
[PROOF STEP]
by simp


[STATEMENT]
lemma prod_casesK[to_hfref_post]: "case_prod (\<lambda>_ _. k) = (\<lambda>_. k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(uu_, uu_). k) = (\<lambda>_. k)
[PROOF STEP]
by auto


[STATEMENT]
lemma uncurry0_hfref_post[to_hfref_post]: "hfref (uncurry0 True) R S = hfref (\<lambda>_. True) R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [uncurry0 True]\<^sub>a R \<rightarrow> S = R \<rightarrow>\<^sub>a S
[PROOF STEP]
apply (fo_rule arg_cong fun_cong)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uncurry0 True = (\<lambda>_. True)
[PROOF STEP]
by auto


[STATEMENT]
lemma [fcomp_norm_simps]: "CONSTRAINT is_pure P \<Longrightarrow> pure (the_pure P) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CONSTRAINT is_pure P \<Longrightarrow> pure (the_pure P) = P
[PROOF STEP]
by simp


[STATEMENT]
lemma ensure_fref_nresI: "(f,g)\<in>[P]\<^sub>f R\<rightarrow>S \<Longrightarrow> (RETURN o f, RETURN o g)\<in>[P]\<^sub>f R\<rightarrow>\<langle>S\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> [P]\<^sub>f R \<rightarrow> S \<Longrightarrow> (RETURN \<circ> f, RETURN \<circ> g) \<in> [P]\<^sub>f R \<rightarrow> \<langle>S\<rangle>nres_rel
[PROOF STEP]
by (auto intro: nres_relI simp: fref_def)


[STATEMENT]
lemma ensure_fref_nres_unfold:
    "\<And>f. RETURN o (uncurry0 f) = uncurry0 (RETURN f)"
    "\<And>f. RETURN o (uncurry f) = uncurry (RETURN oo f)"
    "\<And>f. (RETURN ooo uncurry) f = uncurry (RETURN ooo f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. (RETURN \<circ>\<circ> uncurry0) f = uncurry0 (RETURN f)) &&& (\<And>f. (RETURN \<circ>\<circ> uncurry) f = uncurry (RETURN \<circ>\<circ> f)) &&& (\<And>f. (RETURN \<circ>\<circ>\<circ> uncurry) f = uncurry (RETURN \<circ>\<circ>\<circ> f))
[PROOF STEP]
by auto


[STATEMENT]
lemma auto_weaken_pre_init_hf:
    assumes "\<And>x. PROTECT P x \<longrightarrow> P' x"
    assumes "(f,h) \<in> hfref P' R S"
    shows "(f,h) \<in> hfref P R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [P]\<^sub>a R \<rightarrow> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
PROTECT P ?x \<longrightarrow> P' ?x
(f, h) \<in> [P']\<^sub>a R \<rightarrow> S

goal (1 subgoal):
 1. (f, h) \<in> [P]\<^sub>a R \<rightarrow> S
[PROOF STEP]
by (auto simp: hfref_def)


[STATEMENT]
lemma auto_weaken_pre_init_f:
    assumes "\<And>x. PROTECT P x \<longrightarrow> P' x"
    assumes "(f,h) \<in> fref P' R S"
    shows "(f,h) \<in> fref P R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [P]\<^sub>f R \<rightarrow> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
PROTECT P ?x \<longrightarrow> P' ?x
(f, h) \<in> [P']\<^sub>f R \<rightarrow> S

goal (1 subgoal):
 1. (f, h) \<in> [P]\<^sub>f R \<rightarrow> S
[PROOF STEP]
by (auto simp: fref_def)


[STATEMENT]
lemma auto_weaken_pre_uncurry_step:
    assumes "PROTECT f a \<equiv> f'"
    shows "PROTECT (\<lambda>(x,y). f x y) (a,b) \<equiv> f' b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROTECT (\<lambda>(x, y). f x y) (a, b) \<equiv> f' b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
PROTECT f a \<equiv> f'

goal (1 subgoal):
 1. PROTECT (\<lambda>(x, y). f x y) (a, b) \<equiv> f' b
[PROOF STEP]
by (auto simp: curry_def dest!: meta_eq_to_obj_eq intro!: eq_reflection)


[STATEMENT]
lemma auto_weaken_pre_uncurry_finish:
    "PROTECT f x \<equiv> f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROTECT f x \<equiv> f x
[PROOF STEP]
by (auto)


[STATEMENT]
lemma auto_weaken_pre_uncurry_start:
    assumes "P \<equiv> P'"
    assumes "P'\<longrightarrow>Q"
    shows "P\<longrightarrow>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<longrightarrow> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<equiv> P'
P' \<longrightarrow> Q

goal (1 subgoal):
 1. P \<longrightarrow> Q
[PROOF STEP]
by (auto)


[STATEMENT]
lemma auto_weaken_pre_comp_PRE_I:
    assumes "S x \<Longrightarrow> P x"
    assumes "\<And>y. \<lbrakk>(y,x)\<in>R; P x; S x\<rbrakk> \<Longrightarrow> Q x y"
    shows "comp_PRE R P Q S x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_PRE R P Q S x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
S x \<Longrightarrow> P x
\<lbrakk>(?y, x) \<in> R; P x; S x\<rbrakk> \<Longrightarrow> Q x ?y

goal (1 subgoal):
 1. comp_PRE R P Q S x
[PROOF STEP]
by (auto simp: comp_PRE_def)


[STATEMENT]
lemma auto_weaken_pre_to_imp_nf:
    "(A\<longrightarrow>B\<longrightarrow>C) = (A\<and>B \<longrightarrow> C)"
    "((A\<and>B)\<and>C) = (A\<and>B\<and>C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<longrightarrow> B \<longrightarrow> C) = (A \<and> B \<longrightarrow> C) &&& ((A \<and> B) \<and> C) = (A \<and> B \<and> C)
[PROOF STEP]
by auto


[STATEMENT]
lemma auto_weaken_pre_add_dummy_imp:
    "P \<Longrightarrow> True \<longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> True \<longrightarrow> P
[PROOF STEP]
by simp


[STATEMENT]
lemma hfsynth_ID_R_D:
    fixes I :: "'a itself"
    assumes "hfsynth_ID_R R a"
    assumes "intf_of_assn R I"
    shows "a ::\<^sub>i I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a ::\<^sub>i I
[PROOF STEP]
by simp


[STATEMENT]
lemma hfsynth_hnr_from_hfI:
    assumes "\<forall>x xi. P x \<and> hfsynth_ID_R (fst R) x \<longrightarrow> hn_refine (emp * hn_ctxt (fst R) x xi) (f$xi) (emp * hn_ctxt (snd R) x xi) S (g$x)"
    shows "(f,g) \<in> [P]\<^sub>a R \<rightarrow> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> [P]\<^sub>a R \<rightarrow> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x xi. P x \<and> hfsynth_ID_R (fst R) x \<longrightarrow> hn_refine (emp * hn_ctxt (fst R) x xi) (f $ xi) (emp * hn_ctxt (snd R) x xi) S (g $ x)

goal (1 subgoal):
 1. (f, g) \<in> [P]\<^sub>a R \<rightarrow> S
[PROOF STEP]
unfolding hfref_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x xi. P x \<and> hfsynth_ID_R (fst R) x \<longrightarrow> hn_refine (emp * hn_ctxt (fst R) x xi) (f $ xi) (emp * hn_ctxt (snd R) x xi) S (g $ x)

goal (1 subgoal):
 1. (f, g) \<in> {(f, g). \<forall>c a. P a \<longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (g a)}
[PROOF STEP]
by (auto simp: hn_ctxt_def)


[STATEMENT]
lemma hfsynth_ID_R_uncurry_unfold:
    "hfsynth_ID_R (to_hnr_prod R S) (a,b) \<equiv> hfsynth_ID_R R a \<and> hfsynth_ID_R S b"
    "hfsynth_ID_R (fst (hf_pres R k)) \<equiv> hfsynth_ID_R R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hfsynth_ID_R (to_hnr_prod R S) (a, b) \<equiv> hfsynth_ID_R R a \<and> hfsynth_ID_R S b) &&& hfsynth_ID_R (fst (hf_pres R k)) \<equiv> hfsynth_ID_R R
[PROOF STEP]
by (auto intro!: eq_reflection)


[STATEMENT]
lemma distinct_count_atmost_1':
  "distinct xs = (\<forall>a. count (mset xs) a \<le> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs = (\<forall>a. count (mset xs) a \<le> 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct xs = (\<forall>a. count (mset xs) a \<le> 1)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct xs = (\<forall>a. count (mset xs) a \<le> 1)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct xs = (\<forall>a. count (mset xs) a \<le> 1)
[PROOF STEP]
have "count (mset xs) x = (if x \<in> set xs then 1 else 0) \<longleftrightarrow> count (mset xs) x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (count (mset xs) x = (if x \<in> set xs then 1 else 0)) = (count (mset xs) x \<le> 1)
[PROOF STEP]
using count_eq_zero_iff[of "mset xs" x]
[PROOF STATE]
proof (prove)
using this:
(count (mset xs) x = 0) = (x \<notin># mset xs)

goal (1 subgoal):
 1. (count (mset xs) x = (if x \<in> set xs then 1 else 0)) = (count (mset xs) x \<le> 1)
[PROOF STEP]
by (cases "count (mset xs) x") (auto simp del: count_mset_0_iff)
[PROOF STATE]
proof (state)
this:
(count (mset xs) x = (if x \<in> set xs then 1 else 0)) = (count (mset xs) x \<le> 1)

goal (1 subgoal):
 1. distinct xs = (\<forall>a. count (mset xs) a \<le> 1)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(count (mset xs) ?x2 = (if ?x2 \<in> set xs then 1 else 0)) = (count (mset xs) ?x2 \<le> 1)

goal (1 subgoal):
 1. distinct xs = (\<forall>a. count (mset xs) a \<le> 1)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(count (mset xs) ?x2 = (if ?x2 \<in> set xs then 1 else 0)) = (count (mset xs) ?x2 \<le> 1)

goal (1 subgoal):
 1. distinct xs = (\<forall>a. count (mset xs) a \<le> 1)
[PROOF STEP]
unfolding distinct_count_atmost_1
[PROOF STATE]
proof (prove)
using this:
(count (mset xs) ?x2 = (if ?x2 \<in> set xs then 1 else 0)) = (count (mset xs) ?x2 \<le> 1)

goal (1 subgoal):
 1. (\<forall>a. count (mset xs) a = (if a \<in> set xs then 1 else 0)) = (\<forall>a. count (mset xs) a \<le> 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct xs = (\<forall>a. count (mset xs) a \<le> 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_mset_mono:
  assumes "distinct ys" "mset xs \<subseteq># mset ys"
  shows   "distinct xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs
[PROOF STEP]
unfolding distinct_count_atmost_1'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. count (mset xs) a \<le> 1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. count (mset xs) a \<le> 1
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. count (mset xs) a \<le> 1
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
mset xs \<subseteq># mset ys
[PROOF STEP]
have "count (mset xs) x \<le> count (mset ys) x"
[PROOF STATE]
proof (prove)
using this:
mset xs \<subseteq># mset ys

goal (1 subgoal):
 1. count (mset xs) x \<le> count (mset ys) x
[PROOF STEP]
by (rule mset_subset_eq_count)
[PROOF STATE]
proof (state)
this:
count (mset xs) x \<le> count (mset ys) x

goal (1 subgoal):
 1. \<And>a. count (mset xs) a \<le> 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count (mset xs) x \<le> count (mset ys) x

goal (1 subgoal):
 1. \<And>a. count (mset xs) a \<le> 1
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
distinct ys
[PROOF STEP]
have "\<dots> \<le> 1"
[PROOF STATE]
proof (prove)
using this:
distinct ys

goal (1 subgoal):
 1. count (mset ys) x \<le> 1
[PROOF STEP]
unfolding distinct_count_atmost_1'
[PROOF STATE]
proof (prove)
using this:
\<forall>a. count (mset ys) a \<le> 1

goal (1 subgoal):
 1. count (mset ys) x \<le> 1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
count (mset ys) x \<le> 1

goal (1 subgoal):
 1. \<And>a. count (mset xs) a \<le> 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
count (mset xs) x \<le> 1
[PROOF STEP]
show "count (mset xs) x \<le> 1"
[PROOF STATE]
proof (prove)
using this:
count (mset xs) x \<le> 1

goal (1 subgoal):
 1. count (mset xs) x \<le> 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
count (mset xs) x \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_eq_imp_distinct_iff:
  assumes "mset xs = mset ys"
  shows   "distinct xs \<longleftrightarrow> distinct ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs = distinct ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mset xs = mset ys

goal (1 subgoal):
 1. distinct xs = distinct ys
[PROOF STEP]
by (simp add: distinct_count_atmost_1')


[STATEMENT]
lemma total_on_subset: "total_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> total_on A R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>total_on B R; A \<subseteq> B\<rbrakk> \<Longrightarrow> total_on A R
[PROOF STEP]
by (auto simp: total_on_def)


[STATEMENT]
lemma sorted_wrt_Nil [simp]: "sorted_wrt R []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R []
[PROOF STEP]
by (rule sorted_wrt.intros)


[STATEMENT]
lemma sorted_wrt_Cons: "sorted_wrt R (x # xs) \<longleftrightarrow> (\<forall>y\<in>set xs. (x,y) \<in> R) \<and> sorted_wrt R xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (x # xs) = ((\<forall>y\<in>set xs. (x, y) \<in> R) \<and> Linorder_Relations.sorted_wrt R xs)
[PROOF STEP]
by (auto intro: sorted_wrt.intros elim: sorted_wrt.cases)


[STATEMENT]
lemma sorted_wrt_singleton [simp]: "sorted_wrt R [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R [x]
[PROOF STEP]
by (intro sorted_wrt.intros) simp_all


[STATEMENT]
lemma sorted_wrt_many:
  assumes "trans R"
  shows   "sorted_wrt R (x # y # xs) \<longleftrightarrow> (x,y) \<in> R \<and> sorted_wrt R (y # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (x # y # xs) = ((x, y) \<in> R \<and> Linorder_Relations.sorted_wrt R (y # xs))
[PROOF STEP]
by (force intro: sorted_wrt.intros transD[OF assms] elim: sorted_wrt.cases)


[STATEMENT]
lemma sorted_wrt_imp_le_last:
  assumes "sorted_wrt R xs" "xs \<noteq> []" "x \<in> set xs" "x \<noteq> last xs"
  shows   "(x, last xs) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, last xs) \<in> R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Linorder_Relations.sorted_wrt R xs
xs \<noteq> []
x \<in> set xs
x \<noteq> last xs

goal (1 subgoal):
 1. (x, last xs) \<in> R
[PROOF STEP]
by induction auto


[STATEMENT]
lemma sorted_wrt_append:
  assumes "sorted_wrt R xs" "sorted_wrt R ys"
          "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set ys \<Longrightarrow> (x,y) \<in> R" "trans R"
  shows   "sorted_wrt R (xs @ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (xs @ ys)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Linorder_Relations.sorted_wrt R xs
Linorder_Relations.sorted_wrt R ys
\<lbrakk>?x \<in> set xs; ?y \<in> set ys\<rbrakk> \<Longrightarrow> (?x, ?y) \<in> R
trans R

goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (xs @ ys)
[PROOF STEP]
by (induction xs) (auto simp: sorted_wrt_Cons)


[STATEMENT]
lemma sorted_wrt_snoc:
  assumes "sorted_wrt R xs" "(last xs, y) \<in> R" "trans R"
  shows   "sorted_wrt R (xs @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (xs @ [y])
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
Linorder_Relations.sorted_wrt R xs
(last xs, y) \<in> R

goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (xs @ [y])
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (last [], y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R ([] @ [y])
 2. \<And>xs x. \<lbrakk>Linorder_Relations.sorted_wrt R xs; (last xs, y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R (xs @ [y]); \<And>y. y \<in> set xs \<Longrightarrow> (x, y) \<in> R; (last (x # xs), y) \<in> R\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
case (2 xs x)
[PROOF STATE]
proof (state)
this:
Linorder_Relations.sorted_wrt R xs
?y \<in> set xs \<Longrightarrow> (x, ?y) \<in> R
(last xs, y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R (xs @ [y])
(last (x # xs), y) \<in> R

goal (2 subgoals):
 1. (last [], y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R ([] @ [y])
 2. \<And>xs x. \<lbrakk>Linorder_Relations.sorted_wrt R xs; (last xs, y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R (xs @ [y]); \<And>y. y \<in> set xs \<Longrightarrow> (x, y) \<in> R; (last (x # xs), y) \<in> R\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
proof (cases "xs = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
 2. xs \<noteq> [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
 2. xs \<noteq> [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
Linorder_Relations.sorted_wrt R xs
?y \<in> set xs \<Longrightarrow> (x, ?y) \<in> R
(last xs, y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R (xs @ [y])
(last (x # xs), y) \<in> R
xs \<noteq> []
[PROOF STEP]
have "(z,y) \<in> R" if "z \<in> set xs" for z
[PROOF STATE]
proof (prove)
using this:
Linorder_Relations.sorted_wrt R xs
?y \<in> set xs \<Longrightarrow> (x, ?y) \<in> R
(last xs, y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R (xs @ [y])
(last (x # xs), y) \<in> R
xs \<noteq> []

goal (1 subgoal):
 1. (z, y) \<in> R
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
Linorder_Relations.sorted_wrt R xs
?y \<in> set xs \<Longrightarrow> (x, ?y) \<in> R
(last xs, y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R (xs @ [y])
(last (x # xs), y) \<in> R
xs \<noteq> []
z \<in> set xs

goal (1 subgoal):
 1. (z, y) \<in> R
[PROOF STEP]
by (cases "z = last xs")
                    (auto intro: assms transD[OF assms(3), OF sorted_wrt_imp_le_last[OF 2(1)]])
[PROOF STATE]
proof (state)
this:
?z \<in> set xs \<Longrightarrow> (?z, y) \<in> R

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
 2. xs \<noteq> [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
[PROOF STEP]
have *: "last xs \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []

goal (1 subgoal):
 1. last xs \<in> set xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
last xs \<in> set xs

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
 2. xs \<noteq> [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last xs \<in> set xs

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
 2. xs \<noteq> [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
from 2 False
[PROOF STATE]
proof (chain)
picking this:
Linorder_Relations.sorted_wrt R xs
?y \<in> set xs \<Longrightarrow> (x, ?y) \<in> R
(last xs, y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R (xs @ [y])
(last (x # xs), y) \<in> R
xs \<noteq> []
[PROOF STEP]
have "(x,y) \<in> R"
[PROOF STATE]
proof (prove)
using this:
Linorder_Relations.sorted_wrt R xs
?y \<in> set xs \<Longrightarrow> (x, ?y) \<in> R
(last xs, y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R (xs @ [y])
(last (x # xs), y) \<in> R
xs \<noteq> []

goal (1 subgoal):
 1. (x, y) \<in> R
[PROOF STEP]
by (intro transD[OF assms(3) 2(2)[OF *]]) simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> R

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
 2. xs \<noteq> [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
last xs \<in> set xs
(x, y) \<in> R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
last xs \<in> set xs
(x, y) \<in> R

goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
using 2 False
[PROOF STATE]
proof (prove)
using this:
last xs \<in> set xs
(x, y) \<in> R
Linorder_Relations.sorted_wrt R xs
?y \<in> set xs \<Longrightarrow> (x, ?y) \<in> R
(last xs, y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R (xs @ [y])
(last (x # xs), y) \<in> R
xs \<noteq> []

goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
by (auto intro!: sorted_wrt.intros)
[PROOF STATE]
proof (state)
this:
Linorder_Relations.sorted_wrt R ((x # xs) @ [y])

goal (1 subgoal):
 1. xs = [] \<Longrightarrow> Linorder_Relations.sorted_wrt R ((x # xs) @ [y])
[PROOF STEP]
qed (insert 2, auto intro: sorted_wrt.intros)
[PROOF STATE]
proof (state)
this:
Linorder_Relations.sorted_wrt R ((x # xs) @ [y])

goal (1 subgoal):
 1. (last [], y) \<in> R \<Longrightarrow> Linorder_Relations.sorted_wrt R ([] @ [y])
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma sorted_wrt_conv_nth:
  "sorted_wrt R xs \<longleftrightarrow> (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> (xs!i, xs!j) \<in> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> (xs ! i, xs ! j) \<in> R)
[PROOF STEP]
by (induction xs) (auto simp: sorted_wrt_Cons nth_Cons set_conv_nth split: nat.splits)


[STATEMENT]
lemma linorder_on_cases:
  assumes "linorder_on A R" "x \<in> A" "y \<in> A"
  shows   "x = y \<or> ((x, y) \<in> R \<and> (y, x) \<notin> R) \<or> ((y, x) \<in> R \<and> (x, y) \<notin> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y \<or> (x, y) \<in> R \<and> (y, x) \<notin> R \<or> (y, x) \<in> R \<and> (x, y) \<notin> R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
x \<in> A
y \<in> A

goal (1 subgoal):
 1. x = y \<or> (x, y) \<in> R \<and> (y, x) \<notin> R \<or> (y, x) \<in> R \<and> (x, y) \<notin> R
[PROOF STEP]
by (auto simp: linorder_on_def refl_on_def total_on_def antisym_def)


[STATEMENT]
lemma sorted_wrt_linorder_imp_index_le:
  assumes "linorder_on A R" "set xs \<subseteq> A" "sorted_wrt R xs"
          "x \<in> set xs" "y \<in> set xs" "(x,y) \<in> R"
  shows   "index xs x \<le> index xs y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
define i j where "i = index xs x" and "j = index xs y"
[PROOF STATE]
proof (state)
this:
i = index xs x
j = index xs y

goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
i = index xs x
j = index xs y

goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
assume "j < i"
[PROOF STATE]
proof (state)
this:
j < i

goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < i

goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
y \<in> set xs
(x, y) \<in> R
[PROOF STEP]
have "i < length xs"
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
y \<in> set xs
(x, y) \<in> R

goal (1 subgoal):
 1. i < length xs
[PROOF STEP]
by (simp add: i_def)
[PROOF STATE]
proof (state)
this:
i < length xs

goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < i
i < length xs
[PROOF STEP]
have "(xs!j,xs!i) \<in> R"
[PROOF STATE]
proof (prove)
using this:
j < i
i < length xs

goal (1 subgoal):
 1. (xs ! j, xs ! i) \<in> R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
j < i
i < length xs
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
y \<in> set xs
(x, y) \<in> R

goal (1 subgoal):
 1. (xs ! j, xs ! i) \<in> R
[PROOF STEP]
by (auto simp: sorted_wrt_conv_nth)
[PROOF STATE]
proof (state)
this:
(xs ! j, xs ! i) \<in> R

goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
y \<in> set xs
(x, y) \<in> R
(xs ! j, xs ! i) \<in> R
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
y \<in> set xs
(x, y) \<in> R
(xs ! j, xs ! i) \<in> R

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (auto simp: linorder_on_def antisym_def i_def j_def)
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
j < i \<Longrightarrow> x = y

goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
hence "i \<le> j \<or> x = y"
[PROOF STATE]
proof (prove)
using this:
j < i \<Longrightarrow> x = y

goal (1 subgoal):
 1. i \<le> j \<or> x = y
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
i \<le> j \<or> x = y

goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> j \<or> x = y

goal (1 subgoal):
 1. index xs x \<le> index xs y
[PROOF STEP]
by (auto simp: i_def j_def)
[PROOF STATE]
proof (state)
this:
index xs x \<le> index xs y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sorted_wrt_linorder_index_le_imp:
  assumes "linorder_on A R" "set xs \<subseteq> A" "sorted_wrt R xs"
          "x \<in> set xs" "y \<in> set xs" "index xs x \<le> index xs y"
  shows   "(x,y) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> R
[PROOF STEP]
proof (cases "x = y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> (x, y) \<in> R
 2. x \<noteq> y \<Longrightarrow> (x, y) \<in> R
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (2 subgoals):
 1. x = y \<Longrightarrow> (x, y) \<in> R
 2. x \<noteq> y \<Longrightarrow> (x, y) \<in> R
[PROOF STEP]
define i j where "i = index xs x" and "j = index xs y"
[PROOF STATE]
proof (state)
this:
i = index xs x
j = index xs y

goal (2 subgoals):
 1. x = y \<Longrightarrow> (x, y) \<in> R
 2. x \<noteq> y \<Longrightarrow> (x, y) \<in> R
[PROOF STEP]
from False and assms
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
y \<in> set xs
index xs x \<le> index xs y
[PROOF STEP]
have "i \<noteq> j"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
y \<in> set xs
index xs x \<le> index xs y

goal (1 subgoal):
 1. i \<noteq> j
[PROOF STEP]
by (simp add: i_def j_def)
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (2 subgoals):
 1. x = y \<Longrightarrow> (x, y) \<in> R
 2. x \<noteq> y \<Longrightarrow> (x, y) \<in> R
[PROOF STEP]
with \<open>index xs x \<le> index xs y\<close>
[PROOF STATE]
proof (chain)
picking this:
index xs x \<le> index xs y
i \<noteq> j
[PROOF STEP]
have "i < j"
[PROOF STATE]
proof (prove)
using this:
index xs x \<le> index xs y
i \<noteq> j

goal (1 subgoal):
 1. i < j
[PROOF STEP]
by (simp add: i_def j_def)
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. x = y \<Longrightarrow> (x, y) \<in> R
 2. x \<noteq> y \<Longrightarrow> (x, y) \<in> R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. x = y \<Longrightarrow> (x, y) \<in> R
 2. x \<noteq> y \<Longrightarrow> (x, y) \<in> R
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
y \<in> set xs
index xs x \<le> index xs y
[PROOF STEP]
have "j < length xs"
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
y \<in> set xs
index xs x \<le> index xs y

goal (1 subgoal):
 1. j < length xs
[PROOF STEP]
by (simp add: j_def)
[PROOF STATE]
proof (state)
this:
j < length xs

goal (2 subgoals):
 1. x = y \<Longrightarrow> (x, y) \<in> R
 2. x \<noteq> y \<Longrightarrow> (x, y) \<in> R
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i < j
j < length xs
[PROOF STEP]
have "(xs ! i, xs ! j) \<in> R"
[PROOF STATE]
proof (prove)
using this:
i < j
j < length xs

goal (1 subgoal):
 1. (xs ! i, xs ! j) \<in> R
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
i < j
j < length xs
Linorder_Relations.sorted_wrt R xs

goal (1 subgoal):
 1. (xs ! i, xs ! j) \<in> R
[PROOF STEP]
by (auto simp: sorted_wrt_conv_nth)
[PROOF STATE]
proof (state)
this:
(xs ! i, xs ! j) \<in> R

goal (2 subgoals):
 1. x = y \<Longrightarrow> (x, y) \<in> R
 2. x \<noteq> y \<Longrightarrow> (x, y) \<in> R
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
y \<in> set xs
index xs x \<le> index xs y
(xs ! i, xs ! j) \<in> R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
x \<in> set xs
y \<in> set xs
index xs x \<le> index xs y
(xs ! i, xs ! j) \<in> R

goal (1 subgoal):
 1. (x, y) \<in> R
[PROOF STEP]
by (simp_all add: i_def j_def)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> R

goal (1 subgoal):
 1. x = y \<Longrightarrow> (x, y) \<in> R
[PROOF STEP]
qed (insert assms, auto simp: linorder_on_def refl_on_def)


[STATEMENT]
lemma sorted_wrt_linorder_index_le_iff:
  assumes "linorder_on A R" "set xs \<subseteq> A" "sorted_wrt R xs"
          "x \<in> set xs" "y \<in> set xs"
  shows   "index xs x \<le> index xs y \<longleftrightarrow> (x,y) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (index xs x \<le> index xs y) = ((x, y) \<in> R)
[PROOF STEP]
using sorted_wrt_linorder_index_le_imp[OF assms] sorted_wrt_linorder_imp_index_le[OF assms]
[PROOF STATE]
proof (prove)
using this:
index xs x \<le> index xs y \<Longrightarrow> (x, y) \<in> R
(x, y) \<in> R \<Longrightarrow> index xs x \<le> index xs y

goal (1 subgoal):
 1. (index xs x \<le> index xs y) = ((x, y) \<in> R)
[PROOF STEP]
by blast


[STATEMENT]
lemma sorted_wrt_linorder_index_less_iff:
  assumes "linorder_on A R" "set xs \<subseteq> A" "sorted_wrt R xs"
          "x \<in> set xs" "y \<in> set xs"
  shows   "index xs x < index xs y \<longleftrightarrow> (y,x) \<notin> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (index xs x < index xs y) = ((y, x) \<notin> R)
[PROOF STEP]
by (subst sorted_wrt_linorder_index_le_iff[OF assms(1-3) assms(5,4), symmetric]) auto


[STATEMENT]
lemma sorted_wrt_distinct_linorder_nth:
  assumes "linorder_on A R" "set xs \<subseteq> A" "sorted_wrt R xs" "distinct xs"
          "i < length xs" "j < length xs"
  shows   "(xs!i, xs!j) \<in> R \<longleftrightarrow> i \<le> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
proof (cases i j rule: linorder_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. i < j \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
 2. i = j \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
 3. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
i < j

goal (3 subgoals):
 1. i < j \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
 2. i = j \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
 3. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
distinct xs
i < length xs
j < length xs
i < j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
distinct xs
i < length xs
j < length xs
i < j

goal (1 subgoal):
 1. ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
by (simp add: sorted_wrt_conv_nth)
[PROOF STATE]
proof (state)
this:
((xs ! i, xs ! j) \<in> R) = (i \<le> j)

goal (2 subgoals):
 1. i = j \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
 2. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = j \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
 2. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
case equal
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. i = j \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
 2. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
distinct xs
i < length xs
j < length xs
[PROOF STEP]
have "xs ! i \<in> set xs" "xs ! j \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
distinct xs
i < length xs
j < length xs

goal (1 subgoal):
 1. xs ! i \<in> set xs &&& xs ! j \<in> set xs
[PROOF STEP]
by (auto simp: set_conv_nth)
[PROOF STATE]
proof (state)
this:
xs ! i \<in> set xs
xs ! j \<in> set xs

goal (2 subgoals):
 1. i = j \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
 2. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
set xs \<subseteq> A
xs ! i \<in> set xs
xs ! j \<in> set xs
[PROOF STEP]
have "xs ! i \<in> A" "xs ! j \<in> A"
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> A
xs ! i \<in> set xs
xs ! j \<in> set xs

goal (1 subgoal):
 1. xs ! i \<in> A &&& xs ! j \<in> A
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
xs ! i \<in> A
xs ! j \<in> A

goal (2 subgoals):
 1. i = j \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
 2. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
with \<open>linorder_on A R\<close> and equal
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
i = j
xs ! i \<in> A
xs ! j \<in> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
i = j
xs ! i \<in> A
xs ! j \<in> A

goal (1 subgoal):
 1. ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
by (simp add: linorder_on_def refl_on_def)
[PROOF STATE]
proof (state)
this:
((xs ! i, xs ! j) \<in> R) = (i \<le> j)

goal (1 subgoal):
 1. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
case greater
[PROOF STATE]
proof (state)
this:
j < i

goal (1 subgoal):
 1. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
distinct xs
i < length xs
j < length xs
j < i
[PROOF STEP]
have "(xs!j, xs!i) \<in> R"
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
distinct xs
i < length xs
j < length xs
j < i

goal (1 subgoal):
 1. (xs ! j, xs ! i) \<in> R
[PROOF STEP]
by (auto simp add: sorted_wrt_conv_nth)
[PROOF STATE]
proof (state)
this:
(xs ! j, xs ! i) \<in> R

goal (1 subgoal):
 1. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(xs ! j, xs ! i) \<in> R

goal (1 subgoal):
 1. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
from assms and greater
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
distinct xs
i < length xs
j < length xs
j < i
[PROOF STEP]
have "xs ! i \<noteq> xs ! j"
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
set xs \<subseteq> A
Linorder_Relations.sorted_wrt R xs
distinct xs
i < length xs
j < length xs
j < i

goal (1 subgoal):
 1. xs ! i \<noteq> xs ! j
[PROOF STEP]
by (simp add: nth_eq_iff_index_eq)
[PROOF STATE]
proof (state)
this:
xs ! i \<noteq> xs ! j

goal (1 subgoal):
 1. j < i \<Longrightarrow> ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(xs ! j, xs ! i) \<in> R
xs ! i \<noteq> xs ! j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(xs ! j, xs ! i) \<in> R
xs ! i \<noteq> xs ! j

goal (1 subgoal):
 1. ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
using \<open>linorder_on A R\<close> greater
[PROOF STATE]
proof (prove)
using this:
(xs ! j, xs ! i) \<in> R
xs ! i \<noteq> xs ! j
linorder_on A R
j < i

goal (1 subgoal):
 1. ((xs ! i, xs ! j) \<in> R) = (i \<le> j)
[PROOF STEP]
by (auto simp: linorder_on_def antisym_def)
[PROOF STATE]
proof (state)
this:
((xs ! i, xs ! j) \<in> R) = (i \<le> j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linorder_linorder_of_list [intro, simp]:
  assumes "distinct xs"
  shows   "linorder_on (set xs) (linorder_of_list xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linorder_on (set xs) (linorder_of_list xs)
[PROOF STEP]
unfolding linorder_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl_on (set xs) (linorder_of_list xs) \<and> antisym (linorder_of_list xs) \<and> trans (linorder_of_list xs) \<and> total_on (set xs) (linorder_of_list xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct xs

goal (1 subgoal):
 1. refl_on (set xs) (linorder_of_list xs) \<and> antisym (linorder_of_list xs) \<and> trans (linorder_of_list xs) \<and> total_on (set xs) (linorder_of_list xs)
[PROOF STEP]
by (auto simp: refl_on_def antisym_def trans_def total_on_def linorder_of_list_def)


[STATEMENT]
lemma sorted_wrt_linorder_of_list [intro, simp]:
  "distinct xs \<Longrightarrow> sorted_wrt (linorder_of_list xs) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> Linorder_Relations.sorted_wrt (linorder_of_list xs) xs
[PROOF STEP]
by (auto simp: sorted_wrt_conv_nth linorder_of_list_def index_nth_id)


[STATEMENT]
lemma set_insert_wrt [simp]: "set (insert_wrt R x xs) = insert x (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (insert_wrt R x xs) = insert x (set xs)
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma mset_insert_wrt [simp]: "mset (insert_wrt R x xs) = add_mset x (mset xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (insert_wrt R x xs) = add_mset x (mset xs)
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma length_insert_wrt [simp]: "length (insert_wrt R x xs) = Suc (length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (insert_wrt R x xs) = Suc (length xs)
[PROOF STEP]
by (induction xs) simp_all


[STATEMENT]
lemma set_insort_wrt [simp]: "set (insort_wrt R xs) = set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (insort_wrt R xs) = set xs
[PROOF STEP]
by (induction xs) (simp_all add: insort_wrt_def)


[STATEMENT]
lemma mset_insort_wrt [simp]: "mset (insort_wrt R xs) = mset xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (insort_wrt R xs) = mset xs
[PROOF STEP]
by (induction xs) (simp_all add: insort_wrt_def)


[STATEMENT]
lemma length_insort_wrt [simp]: "length (insort_wrt R xs) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (insort_wrt R xs) = length xs
[PROOF STEP]
by (induction xs) (simp_all add: insort_wrt_def)


[STATEMENT]
lemma sorted_wrt_insert_wrt [intro]:
  "linorder_on A R \<Longrightarrow> set (x # xs) \<subseteq> A \<Longrightarrow>
     sorted_wrt R xs \<Longrightarrow> sorted_wrt R (insert_wrt R x xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>linorder_on A R; set (x # xs) \<subseteq> A; Linorder_Relations.sorted_wrt R xs\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x xs)
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>linorder_on A R; set [x] \<subseteq> A; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x [])
 2. \<And>a xs. \<lbrakk>\<lbrakk>linorder_on A R; set (x # xs) \<subseteq> A; Linorder_Relations.sorted_wrt R xs\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x xs); linorder_on A R; set (x # a # xs) \<subseteq> A; Linorder_Relations.sorted_wrt R (a # xs)\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x (a # xs))
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>linorder_on A R; set (x # ys) \<subseteq> A; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x ys)
linorder_on A R
set (x # y # ys) \<subseteq> A
Linorder_Relations.sorted_wrt R (y # ys)

goal (2 subgoals):
 1. \<lbrakk>linorder_on A R; set [x] \<subseteq> A; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x [])
 2. \<And>a xs. \<lbrakk>\<lbrakk>linorder_on A R; set (x # xs) \<subseteq> A; Linorder_Relations.sorted_wrt R xs\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x xs); linorder_on A R; set (x # a # xs) \<subseteq> A; Linorder_Relations.sorted_wrt R (a # xs)\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x (a # xs))
[PROOF STEP]
from Cons.prems
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
set (x # y # ys) \<subseteq> A
Linorder_Relations.sorted_wrt R (y # ys)
[PROOF STEP]
have "(x,y) \<in> R \<or> (y,x) \<in> R"
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
set (x # y # ys) \<subseteq> A
Linorder_Relations.sorted_wrt R (y # ys)

goal (1 subgoal):
 1. (x, y) \<in> R \<or> (y, x) \<in> R
[PROOF STEP]
by (cases "x = y") (auto simp: linorder_on_def refl_on_def total_on_def)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> R \<or> (y, x) \<in> R

goal (2 subgoals):
 1. \<lbrakk>linorder_on A R; set [x] \<subseteq> A; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x [])
 2. \<And>a xs. \<lbrakk>\<lbrakk>linorder_on A R; set (x # xs) \<subseteq> A; Linorder_Relations.sorted_wrt R xs\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x xs); linorder_on A R; set (x # a # xs) \<subseteq> A; Linorder_Relations.sorted_wrt R (a # xs)\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x (a # xs))
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>linorder_on A R; set (x # ys) \<subseteq> A; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x ys)
linorder_on A R
set (x # y # ys) \<subseteq> A
Linorder_Relations.sorted_wrt R (y # ys)
(x, y) \<in> R \<or> (y, x) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>linorder_on A R; set (x # ys) \<subseteq> A; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x ys)
linorder_on A R
set (x # y # ys) \<subseteq> A
Linorder_Relations.sorted_wrt R (y # ys)
(x, y) \<in> R \<or> (y, x) \<in> R

goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (insert_wrt R x (y # ys))
[PROOF STEP]
by (auto simp: sorted_wrt_Cons intro: transD simp: linorder_on_def)
[PROOF STATE]
proof (state)
this:
Linorder_Relations.sorted_wrt R (insert_wrt R x (y # ys))

goal (1 subgoal):
 1. \<lbrakk>linorder_on A R; set [x] \<subseteq> A; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> Linorder_Relations.sorted_wrt R (insert_wrt R x [])
[PROOF STEP]
qed auto


[STATEMENT]
lemma sorted_wrt_insort [intro]:
  assumes "linorder_on A R" "set xs \<subseteq> A"
  shows   "sorted_wrt R (insort_wrt R xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (insort_wrt R xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (insort_wrt R xs)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
set xs \<subseteq> A
[PROOF STEP]
have "set (insort_wrt R xs) = set xs \<and> sorted_wrt R (insort_wrt R xs)"
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
set xs \<subseteq> A

goal (1 subgoal):
 1. set (insort_wrt R xs) = set xs \<and> Linorder_Relations.sorted_wrt R (insort_wrt R xs)
[PROOF STEP]
by (induction xs) (auto simp: insort_wrt_def intro!: sorted_wrt_insert_wrt)
[PROOF STATE]
proof (state)
this:
set (insort_wrt R xs) = set xs \<and> Linorder_Relations.sorted_wrt R (insort_wrt R xs)

goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (insort_wrt R xs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (insort_wrt R xs) = set xs \<and> Linorder_Relations.sorted_wrt R (insort_wrt R xs)

goal (1 subgoal):
 1. Linorder_Relations.sorted_wrt R (insort_wrt R xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Linorder_Relations.sorted_wrt R (insort_wrt R xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_insort_wrt [simp]: "distinct (insort_wrt R xs) \<longleftrightarrow> distinct xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (insort_wrt R xs) = distinct xs
[PROOF STEP]
by (simp add: distinct_count_atmost_1)


[STATEMENT]
lemma sorted_wrt_linorder_unique:
  assumes "linorder_on A R" "mset xs = mset ys" "sorted_wrt R xs" "sorted_wrt R ys"
  shows   "xs = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
from \<open>mset xs = mset ys\<close>
[PROOF STATE]
proof (chain)
picking this:
mset xs = mset ys
[PROOF STEP]
have "length xs = length ys"
[PROOF STATE]
proof (prove)
using this:
mset xs = mset ys

goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
by (rule mset_eq_length)
[PROOF STATE]
proof (state)
this:
length xs = length ys

goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
from this and assms(2-)
[PROOF STATE]
proof (chain)
picking this:
length xs = length ys
mset xs = mset ys
Linorder_Relations.sorted_wrt R xs
Linorder_Relations.sorted_wrt R ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
mset xs = mset ys
Linorder_Relations.sorted_wrt R xs
Linorder_Relations.sorted_wrt R ys

goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
proof (induction xs ys rule: list_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>mset [] = mset []; Linorder_Relations.sorted_wrt R []; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys; mset (x # xs) = mset (y # ys); Linorder_Relations.sorted_wrt R (x # xs); Linorder_Relations.sorted_wrt R (y # ys)\<rbrakk> \<Longrightarrow> x # xs = y # ys
[PROOF STEP]
case (Cons x xs y ys)
[PROOF STATE]
proof (state)
this:
length xs = length ys
\<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys
mset (x # xs) = mset (y # ys)
Linorder_Relations.sorted_wrt R (x # xs)
Linorder_Relations.sorted_wrt R (y # ys)

goal (2 subgoals):
 1. \<lbrakk>mset [] = mset []; Linorder_Relations.sorted_wrt R []; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys; mset (x # xs) = mset (y # ys); Linorder_Relations.sorted_wrt R (x # xs); Linorder_Relations.sorted_wrt R (y # ys)\<rbrakk> \<Longrightarrow> x # xs = y # ys
[PROOF STEP]
have "set (x # xs) = set_mset (mset (x # xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (x # xs) = set_mset (mset (x # xs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (x # xs) = set_mset (mset (x # xs))

goal (2 subgoals):
 1. \<lbrakk>mset [] = mset []; Linorder_Relations.sorted_wrt R []; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys; mset (x # xs) = mset (y # ys); Linorder_Relations.sorted_wrt R (x # xs); Linorder_Relations.sorted_wrt R (y # ys)\<rbrakk> \<Longrightarrow> x # xs = y # ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (x # xs) = set_mset (mset (x # xs))

goal (2 subgoals):
 1. \<lbrakk>mset [] = mset []; Linorder_Relations.sorted_wrt R []; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys; mset (x # xs) = mset (y # ys); Linorder_Relations.sorted_wrt R (x # xs); Linorder_Relations.sorted_wrt R (y # ys)\<rbrakk> \<Longrightarrow> x # xs = y # ys
[PROOF STEP]
have "mset (x # xs) = mset (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (x # xs) = mset (y # ys)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
mset (x # xs) = mset (y # ys)

goal (2 subgoals):
 1. \<lbrakk>mset [] = mset []; Linorder_Relations.sorted_wrt R []; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys; mset (x # xs) = mset (y # ys); Linorder_Relations.sorted_wrt R (x # xs); Linorder_Relations.sorted_wrt R (y # ys)\<rbrakk> \<Longrightarrow> x # xs = y # ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mset (x # xs) = mset (y # ys)

goal (2 subgoals):
 1. \<lbrakk>mset [] = mset []; Linorder_Relations.sorted_wrt R []; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys; mset (x # xs) = mset (y # ys); Linorder_Relations.sorted_wrt R (x # xs); Linorder_Relations.sorted_wrt R (y # ys)\<rbrakk> \<Longrightarrow> x # xs = y # ys
[PROOF STEP]
have "set_mset \<dots> = set (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_mset (mset (y # ys)) = set (y # ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_mset (mset (y # ys)) = set (y # ys)

goal (2 subgoals):
 1. \<lbrakk>mset [] = mset []; Linorder_Relations.sorted_wrt R []; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys; mset (x # xs) = mset (y # ys); Linorder_Relations.sorted_wrt R (x # xs); Linorder_Relations.sorted_wrt R (y # ys)\<rbrakk> \<Longrightarrow> x # xs = y # ys
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) = set (y # ys)
[PROOF STEP]
have eq: "set (x # xs) = set (y # ys)"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) = set (y # ys)

goal (1 subgoal):
 1. set (x # xs) = set (y # ys)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (x # xs) = set (y # ys)

goal (2 subgoals):
 1. \<lbrakk>mset [] = mset []; Linorder_Relations.sorted_wrt R []; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys; mset (x # xs) = mset (y # ys); Linorder_Relations.sorted_wrt R (x # xs); Linorder_Relations.sorted_wrt R (y # ys)\<rbrakk> \<Longrightarrow> x # xs = y # ys
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> False
[PROOF STEP]
assume "x \<noteq> y"
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> False
[PROOF STEP]
with eq
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) = set (y # ys)
x \<noteq> y
[PROOF STEP]
have "x \<in> set ys" "y \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) = set (y # ys)
x \<noteq> y

goal (1 subgoal):
 1. x \<in> set ys &&& y \<in> set xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set ys
y \<in> set xs

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> False
[PROOF STEP]
with Cons.prems and assms(1) and eq
[PROOF STATE]
proof (chain)
picking this:
mset (x # xs) = mset (y # ys)
Linorder_Relations.sorted_wrt R (x # xs)
Linorder_Relations.sorted_wrt R (y # ys)
linorder_on A R
set (x # xs) = set (y # ys)
x \<in> set ys
y \<in> set xs
[PROOF STEP]
have "(x, y) \<in> R" "(y, x) \<in> R"
[PROOF STATE]
proof (prove)
using this:
mset (x # xs) = mset (y # ys)
Linorder_Relations.sorted_wrt R (x # xs)
Linorder_Relations.sorted_wrt R (y # ys)
linorder_on A R
set (x # xs) = set (y # ys)
x \<in> set ys
y \<in> set xs

goal (1 subgoal):
 1. (x, y) \<in> R &&& (y, x) \<in> R
[PROOF STEP]
by (auto simp: sorted_wrt_Cons)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> R
(y, x) \<in> R

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> False
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
linorder_on A R
(x, y) \<in> R
(y, x) \<in> R
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
using this:
linorder_on A R
(x, y) \<in> R
(y, x) \<in> R

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (auto simp: linorder_on_def antisym_def)
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> False
[PROOF STEP]
with \<open>x \<noteq> y\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
x = y
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
x = y

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

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

goal (2 subgoals):
 1. \<lbrakk>mset [] = mset []; Linorder_Relations.sorted_wrt R []; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> [] = []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; \<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys; mset (x # xs) = mset (y # ys); Linorder_Relations.sorted_wrt R (x # xs); Linorder_Relations.sorted_wrt R (y # ys)\<rbrakk> \<Longrightarrow> x # xs = y # ys
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
length xs = length ys
\<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys
mset (x # xs) = mset (y # ys)
Linorder_Relations.sorted_wrt R (x # xs)
Linorder_Relations.sorted_wrt R (y # ys)
x = y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
\<lbrakk>mset xs = mset ys; Linorder_Relations.sorted_wrt R xs; Linorder_Relations.sorted_wrt R ys\<rbrakk> \<Longrightarrow> xs = ys
mset (x # xs) = mset (y # ys)
Linorder_Relations.sorted_wrt R (x # xs)
Linorder_Relations.sorted_wrt R (y # ys)
x = y

goal (1 subgoal):
 1. x # xs = y # ys
[PROOF STEP]
by (auto simp: sorted_wrt_Cons)
[PROOF STATE]
proof (state)
this:
x # xs = y # ys

goal (1 subgoal):
 1. \<lbrakk>mset [] = mset []; Linorder_Relations.sorted_wrt R []; Linorder_Relations.sorted_wrt R []\<rbrakk> \<Longrightarrow> [] = []
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
xs = ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_remdups: "mset (remdups xs) = mset_set (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (remdups xs) = mset_set (set xs)
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mset (remdups []) = mset_set (set [])
 2. \<And>a xs. mset (remdups xs) = mset_set (set xs) \<Longrightarrow> mset (remdups (a # xs)) = mset_set (set (a # xs))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
mset (remdups xs) = mset_set (set xs)

goal (2 subgoals):
 1. mset (remdups []) = mset_set (set [])
 2. \<And>a xs. mset (remdups xs) = mset_set (set xs) \<Longrightarrow> mset (remdups (a # xs)) = mset_set (set (a # xs))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
mset (remdups xs) = mset_set (set xs)

goal (1 subgoal):
 1. mset (remdups (x # xs)) = mset_set (set (x # xs))
[PROOF STEP]
by (cases "x \<in> set xs") (auto simp: insert_absorb)
[PROOF STATE]
proof (state)
this:
mset (remdups (x # xs)) = mset_set (set (x # xs))

goal (1 subgoal):
 1. mset (remdups []) = mset_set (set [])
[PROOF STEP]
qed auto