[STATEMENT]
lemma geometric_spmf_conv_while:
  shows "geometric_spmf p = map_spmf snd (while (True, 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geometric_spmf p = map_spmf snd (local.while (True, 0))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. geometric_spmf p = map_spmf snd (local.while (True, 0))
[PROOF STEP]
have "map_spmf ((+) x) (geometric_spmf p) = map_spmf snd (while (True, x))" (is "?lhs = ?rhs") for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf ((+) x) (geometric_spmf p) = map_spmf snd (local.while (True, x))
[PROOF STEP]
proof(rule spmf.leq_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ord_spmf (=) (map_spmf ((+) x) (geometric_spmf p)) (map_spmf snd (local.while (True, x)))
 2. ord_spmf (=) (map_spmf snd (local.while (True, x))) (map_spmf ((+) x) (geometric_spmf p))
[PROOF STEP]
show "ord_spmf (=) ?lhs ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_spmf (=) (map_spmf ((+) x) (geometric_spmf p)) (map_spmf snd (local.while (True, x)))
[PROOF STEP]
proof(induction arbitrary: x rule: geometric_spmf_fixp_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. spmf.admissible (\<lambda>a. \<forall>x. ord_spmf (=) (map_spmf ((+) x) (a p)) (map_spmf snd (local.while (True, x))))
 2. \<And>x. ord_spmf (=) (map_spmf ((+) x) (return_pmf None)) (map_spmf snd (local.while (True, x)))
 3. \<And>geometric_spmf' x. (\<And>x. ord_spmf (=) (map_spmf ((+) x) (geometric_spmf' p)) (map_spmf snd (local.while (True, x)))) \<Longrightarrow> ord_spmf (=) (map_spmf ((+) x) (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p)))) (map_spmf snd (local.while (True, x)))
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. spmf.admissible (\<lambda>a. \<forall>x. ord_spmf (=) (map_spmf ((+) x) (a p)) (map_spmf snd (local.while (True, x))))
 2. \<And>x. ord_spmf (=) (map_spmf ((+) x) (return_pmf None)) (map_spmf snd (local.while (True, x)))
 3. \<And>geometric_spmf' x. (\<And>x. ord_spmf (=) (map_spmf ((+) x) (geometric_spmf' p)) (map_spmf snd (local.while (True, x)))) \<Longrightarrow> ord_spmf (=) (map_spmf ((+) x) (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p)))) (map_spmf snd (local.while (True, x)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf.admissible (\<lambda>a. \<forall>x. ord_spmf (=) (map_spmf ((+) x) (a p)) (map_spmf snd (local.while (True, x))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
spmf.admissible (\<lambda>a. \<forall>x. ord_spmf (=) (map_spmf ((+) x) (a p)) (map_spmf snd (local.while (True, x))))

goal (2 subgoals):
 1. \<And>x. ord_spmf (=) (map_spmf ((+) x) (return_pmf None)) (map_spmf snd (local.while (True, x)))
 2. \<And>geometric_spmf' x. (\<And>x. ord_spmf (=) (map_spmf ((+) x) (geometric_spmf' p)) (map_spmf snd (local.while (True, x)))) \<Longrightarrow> ord_spmf (=) (map_spmf ((+) x) (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p)))) (map_spmf snd (local.while (True, x)))
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. ord_spmf (=) (map_spmf ((+) x) (return_pmf None)) (map_spmf snd (local.while (True, x)))
 2. \<And>geometric_spmf' x. (\<And>x. ord_spmf (=) (map_spmf ((+) x) (geometric_spmf' p)) (map_spmf snd (local.while (True, x)))) \<Longrightarrow> ord_spmf (=) (map_spmf ((+) x) (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p)))) (map_spmf snd (local.while (True, x)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_spmf (=) (map_spmf ((+) x) (return_pmf None)) (map_spmf snd (local.while (True, x)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ord_spmf (=) (map_spmf ((+) x) (return_pmf None)) (map_spmf snd (local.while (True, x)))

goal (1 subgoal):
 1. \<And>geometric_spmf' x. (\<And>x. ord_spmf (=) (map_spmf ((+) x) (geometric_spmf' p)) (map_spmf snd (local.while (True, x)))) \<Longrightarrow> ord_spmf (=) (map_spmf ((+) x) (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p)))) (map_spmf snd (local.while (True, x)))
[PROOF STEP]
case (step geometric')
[PROOF STATE]
proof (state)
this:
ord_spmf (=) (map_spmf ((+) ?x) (geometric' p)) (map_spmf snd (local.while (True, ?x)))

goal (1 subgoal):
 1. \<And>geometric_spmf' x. (\<And>x. ord_spmf (=) (map_spmf ((+) x) (geometric_spmf' p)) (map_spmf snd (local.while (True, x)))) \<Longrightarrow> ord_spmf (=) (map_spmf ((+) x) (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p)))) (map_spmf snd (local.while (True, x)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_spmf (=) (map_spmf ((+) x) (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric' p)))) (map_spmf snd (local.while (True, x)))
[PROOF STEP]
using step.IH[of "Suc x"]
[PROOF STATE]
proof (prove)
using this:
ord_spmf (=) (map_spmf ((+) (Suc x)) (geometric' p)) (map_spmf snd (local.while (True, Suc x)))

goal (1 subgoal):
 1. ord_spmf (=) (map_spmf ((+) x) (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric' p)))) (map_spmf snd (local.while (True, x)))
[PROOF STEP]
apply(rewrite while.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_spmf (=) (map_spmf ((+) (Suc x)) (geometric' p)) (map_spmf snd (local.while (True, Suc x))) \<Longrightarrow> ord_spmf (=) (map_spmf ((+) x) (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric' p)))) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> local.while else return_spmf (True, x)))
[PROOF STEP]
apply(clarsimp simp add: map_spmf_bind_spmf bind_map_spmf intro!: ord_spmf_bind_reflI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ord_spmf (=) (map_spmf (\<lambda>a. Suc (x + a)) (geometric' p)) (map_spmf snd (local.while (True, Suc x))); x \<in> set_spmf (bernoulli p)\<rbrakk> \<Longrightarrow> (x \<longrightarrow> ord_spmf (=) (return_spmf x) (map_spmf snd (local.while (False, x)))) \<and> (\<not> x \<longrightarrow> ord_spmf (=) (map_spmf ((+) x) (map_spmf ((+) (Suc 0)) (geometric' p))) (map_spmf snd (local.while (True, Suc x))))
[PROOF STEP]
apply(rewrite while.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ord_spmf (=) (map_spmf (\<lambda>a. Suc (x + a)) (geometric' p)) (map_spmf snd (local.while (True, Suc x))); x \<in> set_spmf (bernoulli p)\<rbrakk> \<Longrightarrow> (x \<longrightarrow> ord_spmf (=) (return_spmf x) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> local.while else return_spmf (False, x)))) \<and> (\<not> x \<longrightarrow> ord_spmf (=) (map_spmf ((+) x) (map_spmf ((+) (Suc 0)) (geometric' p))) (map_spmf snd (local.while (True, Suc x))))
[PROOF STEP]
apply(clarsimp simp add: spmf.map_comp o_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ord_spmf (=) (map_spmf ((+) x) (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric' p)))) (map_spmf snd (local.while (True, x)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ord_spmf (=) (map_spmf ((+) x) (geometric_spmf p)) (map_spmf snd (local.while (True, x)))

goal (1 subgoal):
 1. ord_spmf (=) (map_spmf snd (local.while (True, x))) (map_spmf ((+) x) (geometric_spmf p))
[PROOF STEP]
have "ord_spmf (=) ?rhs ?lhs"
      and "ord_spmf (=) (map_spmf snd (while (False, x))) (return_spmf x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_spmf (=) (map_spmf snd (local.while (True, x))) (map_spmf ((+) x) (geometric_spmf p)) &&& ord_spmf (=) (map_spmf snd (local.while (False, x))) (return_spmf x)
[PROOF STEP]
proof(induction arbitrary: x and x rule: while_fixp_induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. spmf.admissible (\<lambda>a. \<forall>x. ord_spmf (=) (map_spmf snd (a (True, x))) (map_spmf ((+) x) (geometric_spmf p)) \<and> ord_spmf (=) (map_spmf snd (a (False, x))) (return_spmf x))
 2. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (map_spmf ((+) x) (geometric_spmf p))
 3. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (return_spmf x)
 4. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 5. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (5 subgoals):
 1. spmf.admissible (\<lambda>a. \<forall>x. ord_spmf (=) (map_spmf snd (a (True, x))) (map_spmf ((+) x) (geometric_spmf p)) \<and> ord_spmf (=) (map_spmf snd (a (False, x))) (return_spmf x))
 2. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (map_spmf ((+) x) (geometric_spmf p))
 3. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (return_spmf x)
 4. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 5. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf.admissible (\<lambda>a. \<forall>x. ord_spmf (=) (map_spmf snd (a (True, x))) (map_spmf ((+) x) (geometric_spmf p)) \<and> ord_spmf (=) (map_spmf snd (a (False, x))) (return_spmf x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
spmf.admissible (\<lambda>a. \<forall>x. ord_spmf (=) (map_spmf snd (a (True, x))) (map_spmf ((+) x) (geometric_spmf p)) \<and> ord_spmf (=) (map_spmf snd (a (False, x))) (return_spmf x))

goal (4 subgoals):
 1. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (map_spmf ((+) x) (geometric_spmf p))
 2. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (return_spmf x)
 3. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 4. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (map_spmf ((+) x) (geometric_spmf p))
 2. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (return_spmf x)
 3. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 4. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (map_spmf ((+) x) (geometric_spmf p))
 2. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (return_spmf x)
 3. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 4. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_spmf (=) (map_spmf snd (return_pmf None)) (map_spmf ((+) x) (geometric_spmf p))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ord_spmf (=) (map_spmf snd (return_pmf None)) (map_spmf ((+) x) (geometric_spmf p))

goal (3 subgoals):
 1. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (return_spmf x)
 2. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 3. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (return_spmf x)
 2. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 3. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>x. ord_spmf (=) (map_spmf snd (return_pmf None)) (return_spmf x)
 2. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 3. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_spmf (=) (map_spmf snd (return_pmf None)) (return_spmf x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ord_spmf (=) (map_spmf snd (return_pmf None)) (return_spmf x)

goal (2 subgoals):
 1. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 2. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 2. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
case (step while')
[PROOF STATE]
proof (state)
this:
ord_spmf (=) (map_spmf snd (while' (True, ?x))) (map_spmf ((+) ?x) (geometric_spmf p))
ord_spmf (=) (map_spmf snd (while' (False, ?x))) (return_spmf ?x)

goal (2 subgoals):
 1. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 2. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
 2. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
[PROOF STEP]
using step.IH(1)[of "Suc x"] step.IH(2)[of x]
[PROOF STATE]
proof (prove)
using this:
ord_spmf (=) (map_spmf snd (while' (True, Suc x))) (map_spmf ((+) (Suc x)) (geometric_spmf p))
ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)

goal (1 subgoal):
 1. ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))
[PROOF STEP]
by(rewrite geometric_spmf.simps)(clarsimp simp add: map_spmf_bind_spmf bind_map_spmf spmf.map_comp o_def intro!: ord_spmf_bind_reflI)
[PROOF STATE]
proof (state)
this:
ord_spmf (=) (map_spmf snd (if fst (True, x) then (case (True, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (True, x))) (map_spmf ((+) x) (geometric_spmf p))

goal (1 subgoal):
 1. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>while' x. \<lbrakk>\<And>x. ord_spmf (=) (map_spmf snd (while' (True, x))) (map_spmf ((+) x) (geometric_spmf p)); \<And>x. ord_spmf (=) (map_spmf snd (while' (False, x))) (return_spmf x)\<rbrakk> \<Longrightarrow> ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ord_spmf (=) (map_spmf snd (if fst (False, x) then (case (False, x) of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)) \<bind> while' else return_spmf (False, x))) (return_spmf x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ord_spmf (=) (map_spmf snd (local.while (True, x))) (map_spmf ((+) x) (geometric_spmf p))
ord_spmf (=) (map_spmf snd (local.while (False, x))) (return_spmf x)

goal (1 subgoal):
 1. ord_spmf (=) (map_spmf snd (local.while (True, x))) (map_spmf ((+) x) (geometric_spmf p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ord_spmf (=) (map_spmf snd (local.while (True, x))) (map_spmf ((+) x) (geometric_spmf p))
ord_spmf (=) (map_spmf snd (local.while (False, x))) (return_spmf x)
[PROOF STEP]
show "ord_spmf (=) ?rhs ?lhs"
[PROOF STATE]
proof (prove)
using this:
ord_spmf (=) (map_spmf snd (local.while (True, x))) (map_spmf ((+) x) (geometric_spmf p))
ord_spmf (=) (map_spmf snd (local.while (False, x))) (return_spmf x)

goal (1 subgoal):
 1. ord_spmf (=) (map_spmf snd (local.while (True, x))) (map_spmf ((+) x) (geometric_spmf p))
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
ord_spmf (=) (map_spmf snd (local.while (True, x))) (map_spmf ((+) x) (geometric_spmf p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map_spmf ((+) ?x) (geometric_spmf p) = map_spmf snd (local.while (True, ?x))

goal (1 subgoal):
 1. geometric_spmf p = map_spmf snd (local.while (True, 0))
[PROOF STEP]
from this[of 0]
[PROOF STATE]
proof (chain)
picking this:
map_spmf ((+) 0) (geometric_spmf p) = map_spmf snd (local.while (True, 0))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map_spmf ((+) 0) (geometric_spmf p) = map_spmf snd (local.while (True, 0))

goal (1 subgoal):
 1. geometric_spmf p = map_spmf snd (local.while (True, 0))
[PROOF STEP]
by(simp cong: map_spmf_cong)
[PROOF STATE]
proof (state)
this:
geometric_spmf p = map_spmf snd (local.while (True, 0))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lossless_geometric [simp]: "lossless_spmf (geometric_spmf p) \<longleftrightarrow> p > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (geometric_spmf p) = (0 < p)
[PROOF STEP]
proof(cases "0 < p \<and> p < 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < p \<and> p < 1 \<Longrightarrow> lossless_spmf (geometric_spmf p) = (0 < p)
 2. \<not> (0 < p \<and> p < 1) \<Longrightarrow> lossless_spmf (geometric_spmf p) = (0 < p)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < p \<and> p < 1

goal (2 subgoals):
 1. 0 < p \<and> p < 1 \<Longrightarrow> lossless_spmf (geometric_spmf p) = (0 < p)
 2. \<not> (0 < p \<and> p < 1) \<Longrightarrow> lossless_spmf (geometric_spmf p) = (0 < p)
[PROOF STEP]
let ?body = "\<lambda>(b, x :: nat). map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < p \<and> p < 1 \<Longrightarrow> lossless_spmf (geometric_spmf p) = (0 < p)
 2. \<not> (0 < p \<and> p < 1) \<Longrightarrow> lossless_spmf (geometric_spmf p) = (0 < p)
[PROOF STEP]
have "lossless_spmf (while (True, 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (local.while (True, 0))
[PROOF STEP]
proof(rule termination_0_1_immediate)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s. fst s \<Longrightarrow> ?p \<le> spmf (map_spmf fst (case s of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p))) False
 2. 0 < ?p
 3. \<And>s. fst s \<Longrightarrow> lossless_spmf (case s of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p))
[PROOF STEP]
have "{x. x} = {True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. x} = {True}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. x} = {True}

goal (3 subgoals):
 1. \<And>s. fst s \<Longrightarrow> ?p \<le> spmf (map_spmf fst (case s of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p))) False
 2. 0 < ?p
 3. \<And>s. fst s \<Longrightarrow> lossless_spmf (case s of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{x. x} = {True}
[PROOF STEP]
show "p \<le> spmf (map_spmf fst (?body s)) False" for s :: "bool \<times> nat"
[PROOF STATE]
proof (prove)
using this:
{x. x} = {True}

goal (1 subgoal):
 1. p \<le> spmf (map_spmf fst (case s of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p))) False
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
{x. x} = {True}
0 < p \<and> p < 1

goal (1 subgoal):
 1. p \<le> spmf (map_spmf fst (case s of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p))) False
[PROOF STEP]
by(cases s)(simp add: spmf.map_comp o_def spmf_map vimage_def spmf_conv_measure_spmf[symmetric])
[PROOF STATE]
proof (state)
this:
p \<le> spmf (map_spmf fst (case ?s1 of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p))) False

goal (2 subgoals):
 1. 0 < p
 2. \<And>s. fst s \<Longrightarrow> lossless_spmf (case s of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p))
[PROOF STEP]
show "0 < p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < p
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
0 < p \<and> p < 1

goal (1 subgoal):
 1. 0 < p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < p

goal (1 subgoal):
 1. \<And>s. fst s \<Longrightarrow> lossless_spmf (case s of (b, x) \<Rightarrow> map_spmf (\<lambda>b'. (\<not> b', x + (if b' then 0 else 1))) (bernoulli p))
[PROOF STEP]
qed(clarsimp)
[PROOF STATE]
proof (state)
this:
lossless_spmf (local.while (True, 0))

goal (2 subgoals):
 1. 0 < p \<and> p < 1 \<Longrightarrow> lossless_spmf (geometric_spmf p) = (0 < p)
 2. \<not> (0 < p \<and> p < 1) \<Longrightarrow> lossless_spmf (geometric_spmf p) = (0 < p)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
0 < p \<and> p < 1
lossless_spmf (local.while (True, 0))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < p \<and> p < 1
lossless_spmf (local.while (True, 0))

goal (1 subgoal):
 1. lossless_spmf (geometric_spmf p) = (0 < p)
[PROOF STEP]
by(simp add: geometric_spmf_conv_while)
[PROOF STATE]
proof (state)
this:
lossless_spmf (geometric_spmf p) = (0 < p)

goal (1 subgoal):
 1. \<not> (0 < p \<and> p < 1) \<Longrightarrow> lossless_spmf (geometric_spmf p) = (0 < p)
[PROOF STEP]
qed(auto simp add: spmf_geometric_nonpos spmf_geometric_ge_1)


[STATEMENT]
lemma spmf_geometric:
  assumes p: "0 < p" "p < 1"
  shows "spmf (geometric_spmf p) n = (1 - p) ^ n * p" (is "?lhs n = ?rhs n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (geometric_spmf p) n = (1 - p) ^ n * p
[PROOF STEP]
proof(rule spmf_ub_tight)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. spmf (geometric_spmf p) x \<le> (1 - p) ^ x * p
 2. (\<Sum>\<^sup>+ x. ennreal ((1 - p) ^ x * p)) = ennreal (weight_spmf (geometric_spmf p))
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. spmf (geometric_spmf p) x \<le> (1 - p) ^ x * p
 2. (\<Sum>\<^sup>+ x. ennreal ((1 - p) ^ x * p)) = ennreal (weight_spmf (geometric_spmf p))
[PROOF STEP]
have "ennreal (?lhs n) \<le> ennreal (?rhs n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (spmf (geometric_spmf p) n) \<le> ennreal ((1 - p) ^ n * p)
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
0 < p
p < 1

goal (1 subgoal):
 1. ennreal (spmf (geometric_spmf p) n) \<le> ennreal ((1 - p) ^ n * p)
[PROOF STEP]
proof(induction arbitrary: n rule: geometric_spmf_fixp_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. spmf.admissible (\<lambda>a. 0 < p \<longrightarrow> p < 1 \<longrightarrow> (\<forall>x. ennreal (spmf (a p) x) \<le> ennreal ((1 - p) ^ x * p)))
 2. \<And>n. \<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (return_pmf None) n) \<le> ennreal ((1 - p) ^ n * p)
 3. \<And>geometric_spmf' n. \<lbrakk>\<And>n. \<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (geometric_spmf' p) n) \<le> ennreal ((1 - p) ^ n * p); 0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p))) n) \<le> ennreal ((1 - p) ^ n * p)
[PROOF STEP]
case adm
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. spmf.admissible (\<lambda>a. 0 < p \<longrightarrow> p < 1 \<longrightarrow> (\<forall>x. ennreal (spmf (a p) x) \<le> ennreal ((1 - p) ^ x * p)))
 2. \<And>n. \<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (return_pmf None) n) \<le> ennreal ((1 - p) ^ n * p)
 3. \<And>geometric_spmf' n. \<lbrakk>\<And>n. \<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (geometric_spmf' p) n) \<le> ennreal ((1 - p) ^ n * p); 0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p))) n) \<le> ennreal ((1 - p) ^ n * p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf.admissible (\<lambda>a. 0 < p \<longrightarrow> p < 1 \<longrightarrow> (\<forall>x. ennreal (spmf (a p) x) \<le> ennreal ((1 - p) ^ x * p)))
[PROOF STEP]
by(rule cont_intro)+
[PROOF STATE]
proof (state)
this:
spmf.admissible (\<lambda>a. 0 < p \<longrightarrow> p < 1 \<longrightarrow> (\<forall>x. ennreal (spmf (a p) x) \<le> ennreal ((1 - p) ^ x * p)))

goal (2 subgoals):
 1. \<And>n. \<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (return_pmf None) n) \<le> ennreal ((1 - p) ^ n * p)
 2. \<And>geometric_spmf' n. \<lbrakk>\<And>n. \<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (geometric_spmf' p) n) \<le> ennreal ((1 - p) ^ n * p); 0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p))) n) \<le> ennreal ((1 - p) ^ n * p)
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:
0 < p
p < 1

goal (2 subgoals):
 1. \<And>n. \<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (return_pmf None) n) \<le> ennreal ((1 - p) ^ n * p)
 2. \<And>geometric_spmf' n. \<lbrakk>\<And>n. \<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (geometric_spmf' p) n) \<le> ennreal ((1 - p) ^ n * p); 0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p))) n) \<le> ennreal ((1 - p) ^ n * p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (spmf (return_pmf None) n) \<le> ennreal ((1 - p) ^ n * p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ennreal (spmf (return_pmf None) n) \<le> ennreal ((1 - p) ^ n * p)

goal (1 subgoal):
 1. \<And>geometric_spmf' n. \<lbrakk>\<And>n. \<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (geometric_spmf' p) n) \<le> ennreal ((1 - p) ^ n * p); 0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p))) n) \<le> ennreal ((1 - p) ^ n * p)
[PROOF STEP]
case (step geometric_spmf')
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (geometric_spmf' p) ?n) \<le> ennreal ((1 - p) ^ ?n * p)
0 < p
p < 1

goal (1 subgoal):
 1. \<And>geometric_spmf' n. \<lbrakk>\<And>n. \<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (geometric_spmf' p) n) \<le> ennreal ((1 - p) ^ n * p); 0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p))) n) \<le> ennreal ((1 - p) ^ n * p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (geometric_spmf' p) ?n) \<le> ennreal ((1 - p) ^ ?n * p)
0 < p
p < 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < p; p < 1\<rbrakk> \<Longrightarrow> ennreal (spmf (geometric_spmf' p) ?n) \<le> ennreal ((1 - p) ^ ?n * p)
0 < p
p < 1

goal (1 subgoal):
 1. ennreal (spmf (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p))) n) \<le> ennreal ((1 - p) ^ n * p)
[PROOF STEP]
by(cases n)(simp_all add: ennreal_spmf_bind nn_integral_measure_spmf UNIV_bool nn_integral_count_space_finite ennreal_mult spmf_map vimage_def mult.assoc spmf_conv_measure_spmf[symmetric] mult_mono split: split_indicator)
[PROOF STATE]
proof (state)
this:
ennreal (spmf (bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p))) n) \<le> ennreal ((1 - p) ^ n * p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ennreal (spmf (geometric_spmf p) n) \<le> ennreal ((1 - p) ^ n * p)

goal (2 subgoals):
 1. \<And>x. spmf (geometric_spmf p) x \<le> (1 - p) ^ x * p
 2. (\<Sum>\<^sup>+ x. ennreal ((1 - p) ^ x * p)) = ennreal (weight_spmf (geometric_spmf p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal (spmf (geometric_spmf p) n) \<le> ennreal ((1 - p) ^ n * p)
[PROOF STEP]
show "?lhs n \<le> ?rhs n"
[PROOF STATE]
proof (prove)
using this:
ennreal (spmf (geometric_spmf p) n) \<le> ennreal ((1 - p) ^ n * p)

goal (1 subgoal):
 1. spmf (geometric_spmf p) n \<le> (1 - p) ^ n * p
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
ennreal (spmf (geometric_spmf p) n) \<le> ennreal ((1 - p) ^ n * p)
0 < p
p < 1

goal (1 subgoal):
 1. spmf (geometric_spmf p) n \<le> (1 - p) ^ n * p
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
spmf (geometric_spmf p) n \<le> (1 - p) ^ n * p

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal ((1 - p) ^ x * p)) = ennreal (weight_spmf (geometric_spmf p))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal ((1 - p) ^ x * p)) = ennreal (weight_spmf (geometric_spmf p))
[PROOF STEP]
have "(\<Sum>i. ennreal (p * (1 - p) ^ i)) = ennreal (p * (1 / (1 - (1 - p))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i. ennreal (p * (1 - p) ^ i)) = ennreal (p * (1 / (1 - (1 - p))))
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
0 < p
p < 1

goal (1 subgoal):
 1. (\<Sum>i. ennreal (p * (1 - p) ^ i)) = ennreal (p * (1 / (1 - (1 - p))))
[PROOF STEP]
by (intro suminf_ennreal_eq sums_mult geometric_sums) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i. ennreal (p * (1 - p) ^ i)) = ennreal (p * (1 / (1 - (1 - p))))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal ((1 - p) ^ x * p)) = ennreal (weight_spmf (geometric_spmf p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i. ennreal (p * (1 - p) ^ i)) = ennreal (p * (1 / (1 - (1 - p))))
[PROOF STEP]
show "(\<Sum>\<^sup>+ x. ennreal ((1 - p) ^ x * p)) = weight_spmf (geometric_spmf p)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i. ennreal (p * (1 - p) ^ i)) = ennreal (p * (1 / (1 - (1 - p))))

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal ((1 - p) ^ x * p)) = ennreal (weight_spmf (geometric_spmf p))
[PROOF STEP]
using lossless_geometric[of p] p
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i. ennreal (p * (1 - p) ^ i)) = ennreal (p * (1 / (1 - (1 - p))))
lossless_spmf (geometric_spmf p) = (0 < p)
0 < p
p < 1

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal ((1 - p) ^ x * p)) = ennreal (weight_spmf (geometric_spmf p))
[PROOF STEP]
unfolding lossless_spmf_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i. ennreal (p * (1 - p) ^ i)) = ennreal (p * (1 / (1 - (1 - p))))
(weight_spmf (geometric_spmf p) = 1) = (0 < p)
0 < p
p < 1

goal (1 subgoal):
 1. (\<Sum>\<^sup>+ x. ennreal ((1 - p) ^ x * p)) = ennreal (weight_spmf (geometric_spmf p))
[PROOF STEP]
by (simp add: nn_integral_count_space_nat field_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sup>+ x. ennreal ((1 - p) ^ x * p)) = ennreal (weight_spmf (geometric_spmf p))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [def_pat_rules]: "ASSN_ANNOT$A \<equiv> UNPROTECT (ASSN_ANNOT A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSN_ANNOT $ A \<equiv> UNPROTECT (ASSN_ANNOT A)
[PROOF STEP]
by simp


[STATEMENT]
lemma [sepref_fr_rules]: "(return o (\<lambda>x. x), RETURN o PR_CONST (ASSN_ANNOT A)) \<in> A\<^sup>d\<rightarrow>\<^sub>aA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> (\<lambda>x. x), (RETURN \<circ>\<circ> PR_CONST) (ASSN_ANNOT A)) \<in> A\<^sup>d \<rightarrow>\<^sub>a A
[PROOF STEP]
by sepref_to_hoare sep_auto


[STATEMENT]
lemma annotate_assn: "x \<equiv> ASSN_ANNOT A x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<equiv> ASSN_ANNOT A x
[PROOF STEP]
by simp


[STATEMENT]
lemma [safe_constraint_rules]:
  "IS_ID Id"
  "IS_ID R1 \<Longrightarrow> IS_ID R2 \<Longrightarrow> IS_ID (R1 \<rightarrow> R2)"
  "IS_ID R \<Longrightarrow> IS_ID (\<langle>R\<rangle>option_rel)"
  "IS_ID R \<Longrightarrow> IS_ID (\<langle>R\<rangle>list_rel)"
  "IS_ID R1 \<Longrightarrow> IS_ID R2 \<Longrightarrow> IS_ID (R1 \<times>\<^sub>r R2)"
  "IS_ID R1 \<Longrightarrow> IS_ID R2 \<Longrightarrow> IS_ID (\<langle>R1,R2\<rangle>sum_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (IS_ID Id &&& (\<lbrakk>IS_ID R1; IS_ID R2\<rbrakk> \<Longrightarrow> IS_ID (R1 \<rightarrow> R2)) &&& (IS_ID R \<Longrightarrow> IS_ID (\<langle>R\<rangle>option_rel))) &&& (IS_ID R \<Longrightarrow> IS_ID (\<langle>R\<rangle>list_rel)) &&& (\<lbrakk>IS_ID R1; IS_ID R2\<rbrakk> \<Longrightarrow> IS_ID (R1 \<times>\<^sub>r R2)) &&& (\<lbrakk>IS_ID R1; IS_ID R2\<rbrakk> \<Longrightarrow> IS_ID (\<langle>R1, R2\<rangle>sum_rel))
[PROOF STEP]
by (auto simp: IS_ID_def)


[STATEMENT]
lemma [safe_constraint_rules]:
  "IS_BELOW_ID Id"
  "IS_BELOW_ID R \<Longrightarrow> IS_BELOW_ID (\<langle>R\<rangle>option_rel)"
  "IS_BELOW_ID R1 \<Longrightarrow> IS_BELOW_ID R2 \<Longrightarrow> IS_BELOW_ID (R1 \<times>\<^sub>r R2)"
  "IS_BELOW_ID R1 \<Longrightarrow> IS_BELOW_ID R2 \<Longrightarrow> IS_BELOW_ID (\<langle>R1,R2\<rangle>sum_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (IS_BELOW_ID Id &&& (IS_BELOW_ID R \<Longrightarrow> IS_BELOW_ID (\<langle>R\<rangle>option_rel))) &&& (\<lbrakk>IS_BELOW_ID R1; IS_BELOW_ID R2\<rbrakk> \<Longrightarrow> IS_BELOW_ID (R1 \<times>\<^sub>r R2)) &&& (\<lbrakk>IS_BELOW_ID R1; IS_BELOW_ID R2\<rbrakk> \<Longrightarrow> IS_BELOW_ID (\<langle>R1, R2\<rangle>sum_rel))
[PROOF STEP]
by (auto simp: IS_ID_def IS_BELOW_ID_def option_rel_def sum_rel_def list_rel_def)


[STATEMENT]
lemma IS_BELOW_ID_fun_rel_aux: "R1\<supseteq>Id \<Longrightarrow> IS_BELOW_ID R2 \<Longrightarrow> IS_BELOW_ID (R1 \<rightarrow> R2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Id \<subseteq> R1; IS_BELOW_ID R2\<rbrakk> \<Longrightarrow> IS_BELOW_ID (R1 \<rightarrow> R2)
[PROOF STEP]
by (auto simp: IS_BELOW_ID_def dest: fun_relD)


[STATEMENT]
lemma IS_BELOW_ID_list_rel[safe_constraint_rules]:
  "IS_BELOW_ID R \<Longrightarrow> IS_BELOW_ID (\<langle>R\<rangle>list_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IS_BELOW_ID R \<Longrightarrow> IS_BELOW_ID (\<langle>R\<rangle>list_rel)
[PROOF STEP]
unfolding IS_BELOW_ID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> Id \<Longrightarrow> \<langle>R\<rangle>list_rel \<subseteq> Id
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>R \<subseteq> Id; (a, b) \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
fix l l'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>R \<subseteq> Id; (a, b) \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
assume A: "R\<subseteq>Id"
[PROOF STATE]
proof (state)
this:
R \<subseteq> Id

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>R \<subseteq> Id; (a, b) \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
assume "(l,l')\<in>\<langle>R\<rangle>list_rel"
[PROOF STATE]
proof (state)
this:
(l, l') \<in> \<langle>R\<rangle>list_rel

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>R \<subseteq> Id; (a, b) \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
thus "l=l'"
[PROOF STATE]
proof (prove)
using this:
(l, l') \<in> \<langle>R\<rangle>list_rel

goal (1 subgoal):
 1. l = l'
[PROOF STEP]
apply induction
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. [] = []
 2. \<And>x x' l l'. \<lbrakk>(x, x') \<in> R; (l, l') \<in> \<langle>R\<rangle>list_rel; l = l'\<rbrakk> \<Longrightarrow> x # l = x' # l'
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> Id

goal (2 subgoals):
 1. [] = []
 2. \<And>x x' l l'. \<lbrakk>(x, x') \<in> R; (l, l') \<in> \<langle>R\<rangle>list_rel; l = l'\<rbrakk> \<Longrightarrow> x # l = x' # l'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = l'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma IS_ID_imp_BELOW_ID[constraint_rules]:
  "IS_ID R \<Longrightarrow> IS_BELOW_ID R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IS_ID R \<Longrightarrow> IS_BELOW_ID R
[PROOF STEP]
by (auto simp: IS_ID_def IS_BELOW_ID_def )


[STATEMENT]
lemma inv_fun_rel_eq[simp]: "(A\<rightarrow>B)\<inverse> = A\<inverse>\<rightarrow>B\<inverse>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<rightarrow> B)\<inverse> = A\<inverse> \<rightarrow> B\<inverse>
[PROOF STEP]
by (auto dest: fun_relD)


[STATEMENT]
lemma inv_option_rel_eq[simp]: "(\<langle>K\<rangle>option_rel)\<inverse> = \<langle>K\<inverse>\<rangle>option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>K\<rangle>option_rel)\<inverse> = \<langle>K\<inverse>\<rangle>option_rel
[PROOF STEP]
by (auto simp: option_rel_def)


[STATEMENT]
lemma inv_prod_rel_eq[simp]: "(P \<times>\<^sub>r Q)\<inverse> = P\<inverse> \<times>\<^sub>r Q\<inverse>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<times>\<^sub>r Q)\<inverse> = P\<inverse> \<times>\<^sub>r Q\<inverse>
[PROOF STEP]
by (auto)


[STATEMENT]
lemma inv_sum_rel_eq[simp]: "(\<langle>P,Q\<rangle>sum_rel)\<inverse> = \<langle>P\<inverse>,Q\<inverse>\<rangle>sum_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>P, Q\<rangle>sum_rel)\<inverse> = \<langle>P\<inverse>, Q\<inverse>\<rangle>sum_rel
[PROOF STEP]
by (auto simp: sum_rel_def)


[STATEMENT]
lemma inv_list_rel_eq[simp]: "(\<langle>R\<rangle>list_rel)\<inverse> = \<langle>R\<inverse>\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>R\<rangle>list_rel)\<inverse> = \<langle>R\<inverse>\<rangle>list_rel
[PROOF STEP]
unfolding list_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(l, l'). list_all2 (\<lambda>x x'. (x, x') \<in> R) l l'}\<inverse> = {(l, l'). list_all2 (\<lambda>x x'. (x, x') \<in> R\<inverse>) l l'}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. list_all2 (\<lambda>x x'. (x, x') \<in> R) b a \<Longrightarrow> list_all2 (\<lambda>x x'. (x, x') \<in> R\<inverse>) a b
 2. \<And>a b. list_all2 (\<lambda>x x'. (x, x') \<in> R\<inverse>) a b \<Longrightarrow> list_all2 (\<lambda>x x'. (x, x') \<in> R) b a
[PROOF STEP]
apply (subst list.rel_flip[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. list_all2 (\<lambda>x x'. (x, x') \<in> R) b a \<Longrightarrow> list_all2 (\<lambda>x x'. (x, x') \<in> R\<inverse>)\<inverse>\<inverse> b a
 2. \<And>a b. list_all2 (\<lambda>x x'. (x, x') \<in> R\<inverse>) a b \<Longrightarrow> list_all2 (\<lambda>x x'. (x, x') \<in> R) b a
[PROOF STEP]
apply (simp add: conversep_iff[abs_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. list_all2 (\<lambda>x x'. (x, x') \<in> R\<inverse>) a b \<Longrightarrow> list_all2 (\<lambda>x x'. (x, x') \<in> R) b a
[PROOF STEP]
apply (subst list.rel_flip[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. list_all2 (\<lambda>x x'. (x, x') \<in> R\<inverse>) a b \<Longrightarrow> list_all2 (\<lambda>x x'. (x, x') \<in> R)\<inverse>\<inverse> a b
[PROOF STEP]
apply (simp add: conversep_iff[abs_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma IS_LEFT_UNIQUED: "\<lbrakk>IS_LEFT_UNIQUE r; (y, x) \<in> r; (z, x) \<in> r\<rbrakk> \<Longrightarrow> y = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IS_LEFT_UNIQUE r; (y, x) \<in> r; (z, x) \<in> r\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
by (auto simp: IS_LEFT_UNIQUE_def dest: single_valuedD)


[STATEMENT]
lemma prop2p:
  "IS_LEFT_UNIQUE R = left_unique (rel2p R)"
  "IS_RIGHT_UNIQUE R = right_unique (rel2p R)"
  "right_unique (rel2p (R\<inverse>)) = left_unique (rel2p R)"
  "IS_LEFT_TOTAL R = left_total (rel2p R)"
  "IS_RIGHT_TOTAL R = right_total (rel2p R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (IS_LEFT_UNIQUE R = left_unique (rel2p R) &&& single_valued R = right_unique (rel2p R)) &&& right_unique (rel2p (R\<inverse>)) = left_unique (rel2p R) &&& IS_LEFT_TOTAL R = left_total (rel2p R) &&& IS_RIGHT_TOTAL R = right_total (rel2p R)
[PROOF STEP]
by (auto
    simp: IS_LEFT_UNIQUE_def left_unique_def single_valued_def
    simp: right_unique_def
    simp: IS_LEFT_TOTAL_def left_total_def
    simp: IS_RIGHT_TOTAL_def right_total_def
    simp: rel2p_def
    )


[STATEMENT]
lemma p2prop:
  "left_unique P = IS_LEFT_UNIQUE (p2rel P)"
  "right_unique P = IS_RIGHT_UNIQUE (p2rel P)"
  "left_total P = IS_LEFT_TOTAL (p2rel P)"
  "right_total P = IS_RIGHT_TOTAL (p2rel P)"
  "bi_unique P \<longleftrightarrow> left_unique P \<and> right_unique P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (left_unique P = IS_LEFT_UNIQUE (p2rel P) &&& right_unique P = single_valued (p2rel P)) &&& left_total P = IS_LEFT_TOTAL (p2rel P) &&& right_total P = IS_RIGHT_TOTAL (p2rel P) &&& bi_unique P = (left_unique P \<and> right_unique P)
[PROOF STEP]
by (auto
    simp: IS_LEFT_UNIQUE_def left_unique_def single_valued_def
    simp: right_unique_def bi_unique_alt_def
    simp: IS_LEFT_TOTAL_def left_total_def
    simp: IS_RIGHT_TOTAL_def right_total_def
    simp: p2rel_def
    )


[STATEMENT]
lemma [safe_constraint_rules]:
  "IS_LEFT_UNIQUE Id"
  "IS_LEFT_UNIQUE R1 \<Longrightarrow> IS_LEFT_UNIQUE R2 \<Longrightarrow> IS_LEFT_UNIQUE (R1\<times>\<^sub>rR2)"
  "IS_LEFT_UNIQUE R1 \<Longrightarrow> IS_LEFT_UNIQUE R2 \<Longrightarrow> IS_LEFT_UNIQUE (\<langle>R1,R2\<rangle>sum_rel)"
  "IS_LEFT_UNIQUE R \<Longrightarrow> IS_LEFT_UNIQUE (\<langle>R\<rangle>option_rel)"
  "IS_LEFT_UNIQUE R \<Longrightarrow> IS_LEFT_UNIQUE (\<langle>R\<rangle>list_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (IS_LEFT_UNIQUE Id &&& (\<lbrakk>IS_LEFT_UNIQUE R1; IS_LEFT_UNIQUE R2\<rbrakk> \<Longrightarrow> IS_LEFT_UNIQUE (R1 \<times>\<^sub>r R2))) &&& (\<lbrakk>IS_LEFT_UNIQUE R1; IS_LEFT_UNIQUE R2\<rbrakk> \<Longrightarrow> IS_LEFT_UNIQUE (\<langle>R1, R2\<rangle>sum_rel)) &&& (IS_LEFT_UNIQUE R \<Longrightarrow> IS_LEFT_UNIQUE (\<langle>R\<rangle>option_rel)) &&& (IS_LEFT_UNIQUE R \<Longrightarrow> IS_LEFT_UNIQUE (\<langle>R\<rangle>list_rel))
[PROOF STEP]
by (auto simp: IS_LEFT_UNIQUE_def prod_rel_sv sum_rel_sv option_rel_sv list_rel_sv)


[STATEMENT]
lemma IS_LEFT_TOTAL_alt: "IS_LEFT_TOTAL R \<longleftrightarrow> (\<forall>x. \<exists>y. (x,y)\<in>R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IS_LEFT_TOTAL R = (\<forall>x. \<exists>y. (x, y) \<in> R)
[PROOF STEP]
by (auto simp: IS_LEFT_TOTAL_def)


[STATEMENT]
lemma IS_RIGHT_TOTAL_alt: "IS_RIGHT_TOTAL R \<longleftrightarrow> (\<forall>x. \<exists>y. (y,x)\<in>R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IS_RIGHT_TOTAL R = (\<forall>x. \<exists>y. (y, x) \<in> R)
[PROOF STEP]
by (auto simp: IS_RIGHT_TOTAL_def)


[STATEMENT]
lemma [safe_constraint_rules]:
  "IS_LEFT_TOTAL Id"
  "IS_LEFT_TOTAL R1 \<Longrightarrow> IS_LEFT_TOTAL R2 \<Longrightarrow> IS_LEFT_TOTAL (R1\<times>\<^sub>rR2)"
  "IS_LEFT_TOTAL R1 \<Longrightarrow> IS_LEFT_TOTAL R2 \<Longrightarrow> IS_LEFT_TOTAL (\<langle>R1,R2\<rangle>sum_rel)"
  "IS_LEFT_TOTAL R \<Longrightarrow> IS_LEFT_TOTAL (\<langle>R\<rangle>option_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (IS_LEFT_TOTAL Id &&& (\<lbrakk>IS_LEFT_TOTAL R1; IS_LEFT_TOTAL R2\<rbrakk> \<Longrightarrow> IS_LEFT_TOTAL (R1 \<times>\<^sub>r R2))) &&& (\<lbrakk>IS_LEFT_TOTAL R1; IS_LEFT_TOTAL R2\<rbrakk> \<Longrightarrow> IS_LEFT_TOTAL (\<langle>R1, R2\<rangle>sum_rel)) &&& (IS_LEFT_TOTAL R \<Longrightarrow> IS_LEFT_TOTAL (\<langle>R\<rangle>option_rel))
[PROOF STEP]
apply (auto simp: IS_LEFT_TOTAL_alt sum_rel_def option_rel_def list_rel_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x. \<exists>y. (x, y) \<in> R1; \<forall>x. \<exists>y. (x, y) \<in> R2\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a. x = Inl a \<and> (\<exists>a'. y = Inl a' \<and> (a, a') \<in> R1)) \<or> (\<exists>a. x = Inr a \<and> (\<exists>a'. y = Inr a' \<and> (a, a') \<in> R2))
 2. \<And>x. \<forall>x. \<exists>y. (x, y) \<in> R \<Longrightarrow> \<exists>y. x = None \<and> y = None \<or> (\<exists>a. x = Some a \<and> (\<exists>a'. y = Some a' \<and> (a, a') \<in> R))
[PROOF STEP]
apply (rename_tac x; case_tac x; auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x. \<exists>y. (x, y) \<in> R \<Longrightarrow> \<exists>y. x = None \<and> y = None \<or> (\<exists>a. x = Some a \<and> (\<exists>a'. y = Some a' \<and> (a, a') \<in> R))
[PROOF STEP]
apply (rename_tac x; case_tac x; auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [safe_constraint_rules]: "IS_LEFT_TOTAL R \<Longrightarrow> IS_LEFT_TOTAL (\<langle>R\<rangle>list_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IS_LEFT_TOTAL R \<Longrightarrow> IS_LEFT_TOTAL (\<langle>R\<rangle>list_rel)
[PROOF STEP]
unfolding IS_LEFT_TOTAL_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<exists>y. (x, y) \<in> R \<Longrightarrow> \<forall>x. \<exists>y. (x, y) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>x. \<exists>y. (x, y) \<in> R \<Longrightarrow> \<exists>y. (x, y) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
assume A: "\<forall>x.\<exists>y. (x,y)\<in>R"
[PROOF STATE]
proof (state)
this:
\<forall>x. \<exists>y. (x, y) \<in> R

goal (1 subgoal):
 1. \<And>x. \<forall>x. \<exists>y. (x, y) \<in> R \<Longrightarrow> \<exists>y. (x, y) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>x. \<exists>y. (x, y) \<in> R \<Longrightarrow> \<exists>y. (x, y) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
show "\<exists>l'. (l,l')\<in>\<langle>R\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l'. (l, l') \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
apply (induction l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>l'. ([], l') \<in> \<langle>R\<rangle>list_rel
 2. \<And>a l. \<exists>l'. (l, l') \<in> \<langle>R\<rangle>list_rel \<Longrightarrow> \<exists>l'. (a # l, l') \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
\<forall>x. \<exists>y. (x, y) \<in> R

goal (2 subgoals):
 1. \<exists>l'. ([], l') \<in> \<langle>R\<rangle>list_rel
 2. \<And>a l. \<exists>l'. (l, l') \<in> \<langle>R\<rangle>list_rel \<Longrightarrow> \<exists>l'. (a # l, l') \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
by (auto simp: list_rel_split_right_iff)
[PROOF STATE]
proof (state)
this:
\<exists>l'. (l, l') \<in> \<langle>R\<rangle>list_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [safe_constraint_rules]:
  "IS_RIGHT_TOTAL Id"
  "IS_RIGHT_TOTAL R1 \<Longrightarrow> IS_RIGHT_TOTAL R2 \<Longrightarrow> IS_RIGHT_TOTAL (R1\<times>\<^sub>rR2)"
  "IS_RIGHT_TOTAL R1 \<Longrightarrow> IS_RIGHT_TOTAL R2 \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R1,R2\<rangle>sum_rel)"
  "IS_RIGHT_TOTAL R \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R\<rangle>option_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (IS_RIGHT_TOTAL Id &&& (\<lbrakk>IS_RIGHT_TOTAL R1; IS_RIGHT_TOTAL R2\<rbrakk> \<Longrightarrow> IS_RIGHT_TOTAL (R1 \<times>\<^sub>r R2))) &&& (\<lbrakk>IS_RIGHT_TOTAL R1; IS_RIGHT_TOTAL R2\<rbrakk> \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R1, R2\<rangle>sum_rel)) &&& (IS_RIGHT_TOTAL R \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R\<rangle>option_rel))
[PROOF STEP]
apply (auto simp: IS_RIGHT_TOTAL_alt sum_rel_def option_rel_def) []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>IS_RIGHT_TOTAL R1; IS_RIGHT_TOTAL R2\<rbrakk> \<Longrightarrow> IS_RIGHT_TOTAL (R1 \<times>\<^sub>r R2)
 2. \<lbrakk>IS_RIGHT_TOTAL R1; IS_RIGHT_TOTAL R2\<rbrakk> \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R1, R2\<rangle>sum_rel)
 3. IS_RIGHT_TOTAL R \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R\<rangle>option_rel)
[PROOF STEP]
apply (auto simp: IS_RIGHT_TOTAL_alt sum_rel_def option_rel_def) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>IS_RIGHT_TOTAL R1; IS_RIGHT_TOTAL R2\<rbrakk> \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R1, R2\<rangle>sum_rel)
 2. IS_RIGHT_TOTAL R \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R\<rangle>option_rel)
[PROOF STEP]
apply (auto simp: IS_RIGHT_TOTAL_alt sum_rel_def option_rel_def) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x. \<exists>y. (y, x) \<in> R1; \<forall>x. \<exists>y. (y, x) \<in> R2\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>a. y = Inl a \<and> (\<exists>a'. x = Inl a' \<and> (a, a') \<in> R1)) \<or> (\<exists>a. y = Inr a \<and> (\<exists>a'. x = Inr a' \<and> (a, a') \<in> R2))
 2. IS_RIGHT_TOTAL R \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R\<rangle>option_rel)
[PROOF STEP]
apply (rename_tac x; case_tac x; auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IS_RIGHT_TOTAL R \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R\<rangle>option_rel)
[PROOF STEP]
apply (clarsimp simp: IS_RIGHT_TOTAL_alt option_rel_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x. \<exists>y. (y, x) \<in> R \<Longrightarrow> \<exists>y. y = None \<and> x = None \<or> (\<exists>a. y = Some a \<and> (\<exists>a'. x = Some a' \<and> (a, a') \<in> R))
[PROOF STEP]
apply (rename_tac x; case_tac x; auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [safe_constraint_rules]: "IS_RIGHT_TOTAL R \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R\<rangle>list_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IS_RIGHT_TOTAL R \<Longrightarrow> IS_RIGHT_TOTAL (\<langle>R\<rangle>list_rel)
[PROOF STEP]
unfolding IS_RIGHT_TOTAL_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<exists>y. (y, x) \<in> R \<Longrightarrow> \<forall>x. \<exists>y. (y, x) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>x. \<exists>y. (y, x) \<in> R \<Longrightarrow> \<exists>y. (y, x) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
assume A: "\<forall>x.\<exists>y. (y,x)\<in>R"
[PROOF STATE]
proof (state)
this:
\<forall>x. \<exists>y. (y, x) \<in> R

goal (1 subgoal):
 1. \<And>x. \<forall>x. \<exists>y. (y, x) \<in> R \<Longrightarrow> \<exists>y. (y, x) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>x. \<exists>y. (y, x) \<in> R \<Longrightarrow> \<exists>y. (y, x) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
show "\<exists>l'. (l',l)\<in>\<langle>R\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l'. (l', l) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
apply (induction l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>l'. (l', []) \<in> \<langle>R\<rangle>list_rel
 2. \<And>a l. \<exists>l'. (l', l) \<in> \<langle>R\<rangle>list_rel \<Longrightarrow> \<exists>l'. (l', a # l) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
\<forall>x. \<exists>y. (y, x) \<in> R

goal (2 subgoals):
 1. \<exists>l'. (l', []) \<in> \<langle>R\<rangle>list_rel
 2. \<And>a l. \<exists>l'. (l', l) \<in> \<langle>R\<rangle>list_rel \<Longrightarrow> \<exists>l'. (l', a # l) \<in> \<langle>R\<rangle>list_rel
[PROOF STEP]
by (auto simp: list_rel_split_left_iff)
[PROOF STATE]
proof (state)
this:
\<exists>l'. (l', l) \<in> \<langle>R\<rangle>list_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [constraint_simps]:
  "IS_LEFT_TOTAL (R\<inverse>) \<longleftrightarrow> IS_RIGHT_TOTAL R "
  "IS_RIGHT_TOTAL (R\<inverse>) \<longleftrightarrow> IS_LEFT_TOTAL R  "
  "IS_LEFT_UNIQUE (R\<inverse>) \<longleftrightarrow> IS_RIGHT_UNIQUE R"
  "IS_RIGHT_UNIQUE (R\<inverse>) \<longleftrightarrow> IS_LEFT_UNIQUE R "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (IS_LEFT_TOTAL (R\<inverse>) = IS_RIGHT_TOTAL R &&& IS_RIGHT_TOTAL (R\<inverse>) = IS_LEFT_TOTAL R) &&& IS_LEFT_UNIQUE (R\<inverse>) = single_valued R &&& single_valued (R\<inverse>) = IS_LEFT_UNIQUE R
[PROOF STEP]
by (auto simp: IS_RIGHT_TOTAL_alt IS_LEFT_TOTAL_alt IS_LEFT_UNIQUE_def)


[STATEMENT]
lemma [safe_constraint_rules]:
  "IS_RIGHT_UNIQUE A \<Longrightarrow> IS_RIGHT_TOTAL B \<Longrightarrow> IS_RIGHT_TOTAL (A\<rightarrow>B)"
  "IS_RIGHT_TOTAL A \<Longrightarrow> IS_RIGHT_UNIQUE B \<Longrightarrow> IS_RIGHT_UNIQUE (A\<rightarrow>B)"
  "IS_LEFT_UNIQUE A \<Longrightarrow> IS_LEFT_TOTAL B \<Longrightarrow> IS_LEFT_TOTAL (A\<rightarrow>B)"
  "IS_LEFT_TOTAL A \<Longrightarrow> IS_LEFT_UNIQUE B \<Longrightarrow> IS_LEFT_UNIQUE (A\<rightarrow>B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>single_valued A; IS_RIGHT_TOTAL B\<rbrakk> \<Longrightarrow> IS_RIGHT_TOTAL (A \<rightarrow> B)) &&& (\<lbrakk>IS_RIGHT_TOTAL A; single_valued B\<rbrakk> \<Longrightarrow> single_valued (A \<rightarrow> B))) &&& (\<lbrakk>IS_LEFT_UNIQUE A; IS_LEFT_TOTAL B\<rbrakk> \<Longrightarrow> IS_LEFT_TOTAL (A \<rightarrow> B)) &&& (\<lbrakk>IS_LEFT_TOTAL A; IS_LEFT_UNIQUE B\<rbrakk> \<Longrightarrow> IS_LEFT_UNIQUE (A \<rightarrow> B))
[PROOF STEP]
apply (simp_all add: prop2p rel2p)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>right_unique (rel2p A); right_total (rel2p B)\<rbrakk> \<Longrightarrow> right_total (rel_fun (rel2p A) (rel2p B))
 2. \<lbrakk>right_total (rel2p A); right_unique (rel2p B)\<rbrakk> \<Longrightarrow> right_unique (rel_fun (rel2p A) (rel2p B))
 3. \<lbrakk>left_unique (rel2p A); left_total (rel2p B)\<rbrakk> \<Longrightarrow> left_total (rel_fun (rel2p A) (rel2p B))
 4. \<lbrakk>left_total (rel2p A); left_unique (rel2p B)\<rbrakk> \<Longrightarrow> left_unique (rel_fun (rel2p A) (rel2p B))
[PROOF STEP]
apply (blast intro!: transfer_raw)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [constraint_rules]:
  "IS_BELOW_ID R \<Longrightarrow> IS_RIGHT_UNIQUE R"
  "IS_BELOW_ID R \<Longrightarrow> IS_LEFT_UNIQUE R"
  "IS_ID R \<Longrightarrow> IS_RIGHT_TOTAL R"
  "IS_ID R \<Longrightarrow> IS_LEFT_TOTAL R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((IS_BELOW_ID R \<Longrightarrow> single_valued R) &&& (IS_BELOW_ID R \<Longrightarrow> IS_LEFT_UNIQUE R)) &&& (IS_ID R \<Longrightarrow> IS_RIGHT_TOTAL R) &&& (IS_ID R \<Longrightarrow> IS_LEFT_TOTAL R)
[PROOF STEP]
by (auto simp: IS_BELOW_ID_def IS_ID_def IS_LEFT_UNIQUE_def IS_RIGHT_TOTAL_def IS_LEFT_TOTAL_def
    intro: single_valuedI)


[STATEMENT]
lemma param_distinct[param]: "\<lbrakk>IS_LEFT_UNIQUE A; IS_RIGHT_UNIQUE A\<rbrakk> \<Longrightarrow> (distinct, distinct) \<in> \<langle>A\<rangle>list_rel \<rightarrow> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IS_LEFT_UNIQUE A; single_valued A\<rbrakk> \<Longrightarrow> (distinct, distinct) \<in> \<langle>A\<rangle>list_rel \<rightarrow> bool_rel
[PROOF STEP]
apply (fold rel2p_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IS_LEFT_UNIQUE A; single_valued A\<rbrakk> \<Longrightarrow> rel2p (\<langle>A\<rangle>list_rel \<rightarrow> bool_rel) distinct distinct
[PROOF STEP]
apply (simp add: rel2p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IS_LEFT_UNIQUE A; single_valued A\<rbrakk> \<Longrightarrow> rel_fun (list_all2 (rel2p A)) (=) distinct distinct
[PROOF STEP]
apply (rule distinct_transfer)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IS_LEFT_UNIQUE A; single_valued A\<rbrakk> \<Longrightarrow> bi_unique (rel2p A)
[PROOF STEP]
apply (simp add: p2prop)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma param_Image[param]:
  assumes "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A"
  shows "((``), (``)) \<in> \<langle>A\<times>\<^sub>rB\<rangle>set_rel \<rightarrow> \<langle>A\<rangle>set_rel \<rightarrow> \<langle>B\<rangle>set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((``), (``)) \<in> \<langle>A \<times>\<^sub>r B\<rangle>set_rel \<rightarrow> \<langle>A\<rangle>set_rel \<rightarrow> \<langle>B\<rangle>set_rel
[PROOF STEP]
apply (clarsimp simp: set_rel_def; intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' aa a'a. \<lbrakk>\<forall>x\<in>a. \<exists>y\<in>a'. (x, y) \<in> A \<times>\<^sub>r B; \<forall>y\<in>a'. \<exists>x\<in>a. (x, y) \<in> A \<times>\<^sub>r B; \<forall>x\<in>aa. \<exists>y\<in>a'a. (x, y) \<in> A; \<forall>y\<in>a'a. \<exists>x\<in>aa. (x, y) \<in> A\<rbrakk> \<Longrightarrow> \<forall>x\<in>a `` aa. \<exists>y\<in>a' `` a'a. (x, y) \<in> B
 2. \<And>a a' aa a'a. \<lbrakk>\<forall>x\<in>a. \<exists>y\<in>a'. (x, y) \<in> A \<times>\<^sub>r B; \<forall>y\<in>a'. \<exists>x\<in>a. (x, y) \<in> A \<times>\<^sub>r B; \<forall>x\<in>aa. \<exists>y\<in>a'a. (x, y) \<in> A; \<forall>y\<in>a'a. \<exists>x\<in>aa. (x, y) \<in> A\<rbrakk> \<Longrightarrow> \<forall>y\<in>a' `` a'a. \<exists>x\<in>a `` aa. (x, y) \<in> B
[PROOF STEP]
apply (fastforce dest: IS_RIGHT_UNIQUED[OF assms(2)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>\<forall>x\<in>a. \<exists>y\<in>a'. (x, y) \<in> A \<times>\<^sub>r B; \<forall>y\<in>a'. \<exists>x\<in>a. (x, y) \<in> A \<times>\<^sub>r B; \<forall>x\<in>aa. \<exists>y\<in>a'a. (x, y) \<in> A; \<forall>y\<in>a'a. \<exists>x\<in>aa. (x, y) \<in> A\<rbrakk> \<Longrightarrow> \<forall>y\<in>a' `` a'a. \<exists>x\<in>a `` aa. (x, y) \<in> B
[PROOF STEP]
apply (fastforce dest: IS_LEFT_UNIQUED[OF assms(1)])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pres_eq_iff_svb: "((=),(=))\<in>K\<rightarrow>K\<rightarrow>bool_rel \<longleftrightarrow> (single_valued K \<and> single_valued (K\<inverse>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((=), (=)) \<in> K \<rightarrow> K \<rightarrow> bool_rel) = (single_valued K \<and> single_valued (K\<inverse>))
[PROOF STEP]
apply (safe intro!: single_valuedI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y z. \<lbrakk>((=), (=)) \<in> K \<rightarrow> K \<rightarrow> bool_rel; (x, y) \<in> K; (x, z) \<in> K\<rbrakk> \<Longrightarrow> y = z
 2. \<And>x y z. \<lbrakk>((=), (=)) \<in> K \<rightarrow> K \<rightarrow> bool_rel; (y, x) \<in> K; (z, x) \<in> K\<rbrakk> \<Longrightarrow> y = z
 3. \<And>a a' aa a'a. \<lbrakk>(aa, a') \<in> K; (aa, a'a) \<in> K; single_valued K; single_valued (K\<inverse>)\<rbrakk> \<Longrightarrow> a' = a'a
 4. \<And>a a' aa a'a. \<lbrakk>(a, a'a) \<in> K; (aa, a'a) \<in> K; single_valued K; single_valued (K\<inverse>)\<rbrakk> \<Longrightarrow> a = aa
[PROOF STEP]
apply (metis (full_types) IdD fun_relD1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y z. \<lbrakk>((=), (=)) \<in> K \<rightarrow> K \<rightarrow> bool_rel; (y, x) \<in> K; (z, x) \<in> K\<rbrakk> \<Longrightarrow> y = z
 2. \<And>a a' aa a'a. \<lbrakk>(aa, a') \<in> K; (aa, a'a) \<in> K; single_valued K; single_valued (K\<inverse>)\<rbrakk> \<Longrightarrow> a' = a'a
 3. \<And>a a' aa a'a. \<lbrakk>(a, a'a) \<in> K; (aa, a'a) \<in> K; single_valued K; single_valued (K\<inverse>)\<rbrakk> \<Longrightarrow> a = aa
[PROOF STEP]
apply (metis (full_types) IdD fun_relD1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' aa a'a. \<lbrakk>(aa, a') \<in> K; (aa, a'a) \<in> K; single_valued K; single_valued (K\<inverse>)\<rbrakk> \<Longrightarrow> a' = a'a
 2. \<And>a a' aa a'a. \<lbrakk>(a, a'a) \<in> K; (aa, a'a) \<in> K; single_valued K; single_valued (K\<inverse>)\<rbrakk> \<Longrightarrow> a = aa
[PROOF STEP]
by (auto dest: single_valuedD)


[STATEMENT]
lemma [constraint_rules]: "\<lbrakk>single_valued R; single_valued (R\<inverse>)\<rbrakk> \<Longrightarrow> IS_PRES_EQ R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued R; single_valued (R\<inverse>)\<rbrakk> \<Longrightarrow> IS_PRES_EQ R
[PROOF STEP]
by (simp add: pres_eq_iff_svb IS_PRES_EQ_def)


[STATEMENT]
lemma b_assn_pure_conv[constraint_simps]: "b_assn (pure R) P = pure (b_rel R P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_assn (pure R) P = pure (b_rel R P)
[PROOF STEP]
by (auto intro!: ext simp: b_rel_def b_assn_def pure_def)


[STATEMENT]
lemma b_rel_nesting[simp]:
  "b_rel (b_rel R P1) P2 = b_rel R (\<lambda>x. P1 x \<and> P2 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_rel (b_rel R P1) P2 = b_rel R (\<lambda>x. P1 x \<and> P2 x)
[PROOF STEP]
by (auto simp: b_rel_def)


[STATEMENT]
lemma b_rel_triv[simp]:
  "b_rel R (\<lambda>_. True) = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_rel R (\<lambda>_. True) = R
[PROOF STEP]
by (auto simp: b_rel_def)


[STATEMENT]
lemma b_assn_nesting[simp]:
  "b_assn (b_assn A P1) P2 = b_assn A (\<lambda>x. P1 x \<and> P2 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_assn (b_assn A P1) P2 = b_assn A (\<lambda>x. P1 x \<and> P2 x)
[PROOF STEP]
by (auto simp: b_assn_def pure_def intro!: ext)


[STATEMENT]
lemma b_assn_triv[simp]:
  "b_assn A (\<lambda>_. True) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_assn A (\<lambda>_. True) = A
[PROOF STEP]
by (auto simp: b_assn_def pure_def intro!: ext)


[STATEMENT]
lemma b_rel_simp[simp]: "(x,y)\<in>b_rel R P \<longleftrightarrow> (x,y)\<in>R \<and> P y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> b_rel R P) = ((x, y) \<in> R \<and> P y)
[PROOF STEP]
by (auto simp: b_rel_def)


[STATEMENT]
lemma b_assn_simp[simp]: "b_assn A P x y = A x y * \<up>(P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_assn A P x y = A x y * \<up> (P x)
[PROOF STEP]
by (auto simp: b_assn_def)


[STATEMENT]
lemma b_rel_Range[simp]: "Range (b_rel R P) = Range R \<inter> Collect P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Range (b_rel R P) = Range R \<inter> Collect P
[PROOF STEP]
by auto


[STATEMENT]
lemma b_assn_rdom[simp]: "rdomp (b_assn R P) x \<longleftrightarrow> rdomp R x \<and> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdomp (b_assn R P) x = (rdomp R x \<and> P x)
[PROOF STEP]
by (auto simp: rdomp_def)


[STATEMENT]
lemma b_rel_below_id[constraint_rules]:
  "IS_BELOW_ID R \<Longrightarrow> IS_BELOW_ID (b_rel R P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IS_BELOW_ID R \<Longrightarrow> IS_BELOW_ID (b_rel R P)
[PROOF STEP]
by (auto simp: IS_BELOW_ID_def)


[STATEMENT]
lemma b_rel_left_unique[constraint_rules]:
  "IS_LEFT_UNIQUE R \<Longrightarrow> IS_LEFT_UNIQUE (b_rel R P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IS_LEFT_UNIQUE R \<Longrightarrow> IS_LEFT_UNIQUE (b_rel R P)
[PROOF STEP]
by (auto simp: IS_LEFT_UNIQUE_def single_valued_def)


[STATEMENT]
lemma b_rel_right_unique[constraint_rules]:
  "IS_RIGHT_UNIQUE R \<Longrightarrow> IS_RIGHT_UNIQUE (b_rel R P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued R \<Longrightarrow> single_valued (b_rel R P)
[PROOF STEP]
by (auto simp: single_valued_def)

\<comment> \<open>Registered as safe rule, although may loose information in the
    odd case that purity depends condition.\<close>


[STATEMENT]
lemma b_assn_is_pure[safe_constraint_rules]:
  "is_pure A \<Longrightarrow> is_pure (b_assn A P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure A \<Longrightarrow> is_pure (b_assn A P)
[PROOF STEP]
by (auto simp: is_pure_conv b_assn_pure_conv)

\<comment> \<open>Most general form\<close>


[STATEMENT]
lemma b_assn_subtyping_match[sepref_frame_match_rules]:
  assumes "hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt A' x y"
  assumes "\<lbrakk>vassn_tag (hn_ctxt A x y); vassn_tag (hn_ctxt A' x y); P x\<rbrakk> \<Longrightarrow> P' x"
  shows "hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A' P') x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A' P') x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt A' x y
\<lbrakk>vassn_tag (hn_ctxt A x y); vassn_tag (hn_ctxt A' x y); P x\<rbrakk> \<Longrightarrow> P' x

goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A' P') x y
[PROOF STEP]
unfolding hn_ctxt_def b_assn_def entailst_def entails_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h. h \<Turnstile> A x y * \<up> (P x) \<longrightarrow> h \<Turnstile> A' x y * true
\<lbrakk>vassn_tag (A x y); vassn_tag (A' x y); P x\<rbrakk> \<Longrightarrow> P' x

goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> A x y * \<up> (P x) \<longrightarrow> h \<Turnstile> A' x y * \<up> (P' x) * true
[PROOF STEP]
by (fastforce simp: vassn_tag_def mod_star_conv)

\<comment> \<open>Simplified forms:\<close>


[STATEMENT]
lemma b_assn_subtyping_match_eqA[sepref_frame_match_rules]:
  assumes "\<lbrakk>vassn_tag (hn_ctxt A x y); P x\<rbrakk> \<Longrightarrow> P' x"
  shows "hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A P') x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A P') x y
[PROOF STEP]
apply (rule b_assn_subtyping_match)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt A x y
 2. \<lbrakk>vassn_tag (hn_ctxt A x y); vassn_tag (hn_ctxt A x y); P x\<rbrakk> \<Longrightarrow> P' x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt A x y
[PROOF STEP]
unfolding hn_ctxt_def b_assn_def entailst_def entails_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> A x y * \<up> (P x) \<longrightarrow> h \<Turnstile> A x y * true
[PROOF STEP]
by (fastforce simp: vassn_tag_def mod_star_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vassn_tag (hn_ctxt A x y); vassn_tag (hn_ctxt A x y); P x\<rbrakk> \<Longrightarrow> P' x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vassn_tag (hn_ctxt A x y); vassn_tag (hn_ctxt A x y); P x\<rbrakk> \<Longrightarrow> P' x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>vassn_tag (hn_ctxt A x y); P x\<rbrakk> \<Longrightarrow> P' x

goal (1 subgoal):
 1. \<lbrakk>vassn_tag (hn_ctxt A x y); vassn_tag (hn_ctxt A x y); P x\<rbrakk> \<Longrightarrow> P' x
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma b_assn_subtyping_match_tR[sepref_frame_match_rules]:
  assumes "\<lbrakk>P x\<rbrakk> \<Longrightarrow> hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt A' x y"
  shows "hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt A' x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt A' x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P x \<Longrightarrow> hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt A' x y

goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt A' x y
[PROOF STEP]
unfolding hn_ctxt_def b_assn_def entailst_def entails_def
[PROOF STATE]
proof (prove)
using this:
P x \<Longrightarrow> \<forall>h. h \<Turnstile> A x y \<longrightarrow> h \<Turnstile> A' x y * true

goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> A x y * \<up> (P x) \<longrightarrow> h \<Turnstile> A' x y * true
[PROOF STEP]
by (fastforce simp: vassn_tag_def mod_star_conv)


[STATEMENT]
lemma b_assn_subtyping_match_tL[sepref_frame_match_rules]:
  assumes "hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt A' x y"
  assumes "\<lbrakk>vassn_tag (hn_ctxt A x y)\<rbrakk> \<Longrightarrow> P' x"
  shows "hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A' P') x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A' P') x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt A' x y
vassn_tag (hn_ctxt A x y) \<Longrightarrow> P' x

goal (1 subgoal):
 1. hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A' P') x y
[PROOF STEP]
unfolding hn_ctxt_def b_assn_def entailst_def entails_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h. h \<Turnstile> A x y \<longrightarrow> h \<Turnstile> A' x y * true
vassn_tag (A x y) \<Longrightarrow> P' x

goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> A x y \<longrightarrow> h \<Turnstile> A' x y * \<up> (P' x) * true
[PROOF STEP]
by (fastforce simp: vassn_tag_def mod_star_conv)


[STATEMENT]
lemma b_assn_subtyping_match_eqA_tR[sepref_frame_match_rules]:
  "hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt A x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_ctxt A x y
[PROOF STEP]
unfolding hn_ctxt_def b_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A x y * \<up> (P x) \<Longrightarrow>\<^sub>t A x y
[PROOF STEP]
by (sep_auto intro!: enttI)


[STATEMENT]
lemma b_assn_subtyping_match_eqA_tL[sepref_frame_match_rules]:
  assumes "\<lbrakk>vassn_tag (hn_ctxt A x y)\<rbrakk> \<Longrightarrow> P' x"
  shows "hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A P') x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A P') x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vassn_tag (hn_ctxt A x y) \<Longrightarrow> P' x

goal (1 subgoal):
 1. hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A P') x y
[PROOF STEP]
unfolding hn_ctxt_def b_assn_def entailst_def entails_def
[PROOF STATE]
proof (prove)
using this:
vassn_tag (A x y) \<Longrightarrow> P' x

goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> A x y \<longrightarrow> h \<Turnstile> A x y * \<up> (P' x) * true
[PROOF STEP]
by (fastforce simp: vassn_tag_def mod_star_conv)

\<comment> \<open>General form\<close>


[STATEMENT]
lemma b_rel_subtyping_merge[sepref_frame_merge_rules]:
  assumes "hn_ctxt A x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y"
  shows "hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt (b_assn A' P') x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn Am (\<lambda>x. P x \<or> P' x)) x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt (b_assn A' P') x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn Am (\<lambda>x. P x \<or> P' x)) x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hn_ctxt A x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y

goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt (b_assn A' P') x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn Am (\<lambda>x. P x \<or> P' x)) x y
[PROOF STEP]
unfolding hn_ctxt_def b_assn_def entailst_def entails_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h. h \<Turnstile> A x y \<or>\<^sub>A A' x y \<longrightarrow> h \<Turnstile> Am x y * true

goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> A x y * \<up> (P x) \<or>\<^sub>A A' x y * \<up> (P' x) \<longrightarrow> h \<Turnstile> Am x y * \<up> (P x \<or> P' x) * true
[PROOF STEP]
by (fastforce simp: vassn_tag_def)

\<comment> \<open>Simplified forms\<close>


[STATEMENT]
lemma b_rel_subtyping_merge_eqA[sepref_frame_merge_rules]:
  shows "hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt (b_assn A P') x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A (\<lambda>x. P x \<or> P' x)) x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt (b_assn A P') x y \<Longrightarrow>\<^sub>t hn_ctxt (b_assn A (\<lambda>x. P x \<or> P' x)) x y
[PROOF STEP]
apply (rule b_rel_subtyping_merge)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt A x y \<or>\<^sub>A hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt A x y
[PROOF STEP]
by simp


[STATEMENT]
lemma b_rel_subtyping_merge_tL[sepref_frame_merge_rules]:
  assumes "hn_ctxt A x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y"
  shows "hn_ctxt A x y \<or>\<^sub>A hn_ctxt (b_assn A' P') x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt A x y \<or>\<^sub>A hn_ctxt (b_assn A' P') x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y
[PROOF STEP]
using b_rel_subtyping_merge[of A x y A' Am "\<lambda>_. True" P', simplified] assms
[PROOF STATE]
proof (prove)
using this:
hn_ctxt A x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y \<Longrightarrow> hn_ctxt A x y \<or>\<^sub>A hn_ctxt (b_assn A' P') x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y
hn_ctxt A x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y

goal (1 subgoal):
 1. hn_ctxt A x y \<or>\<^sub>A hn_ctxt (b_assn A' P') x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y
[PROOF STEP]
.


[STATEMENT]
lemma b_rel_subtyping_merge_tR[sepref_frame_merge_rules]:
  assumes "hn_ctxt A x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y"
  shows "hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y
[PROOF STEP]
using b_rel_subtyping_merge[of A x y A' Am P "\<lambda>_. True", simplified] assms
[PROOF STATE]
proof (prove)
using this:
hn_ctxt A x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y \<Longrightarrow> hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y
hn_ctxt A x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y

goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y
[PROOF STEP]
.


[STATEMENT]
lemma b_rel_subtyping_merge_eqA_tL[sepref_frame_merge_rules]:
  shows "hn_ctxt A x y \<or>\<^sub>A hn_ctxt (b_assn A P') x y \<Longrightarrow>\<^sub>t hn_ctxt A x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt A x y \<or>\<^sub>A hn_ctxt (b_assn A P') x y \<Longrightarrow>\<^sub>t hn_ctxt A x y
[PROOF STEP]
using b_rel_subtyping_merge_eqA[of A "\<lambda>_. True" x y P', simplified]
[PROOF STATE]
proof (prove)
using this:
hn_ctxt A x y \<or>\<^sub>A hn_ctxt (b_assn A P') x y \<Longrightarrow>\<^sub>t hn_ctxt A x y

goal (1 subgoal):
 1. hn_ctxt A x y \<or>\<^sub>A hn_ctxt (b_assn A P') x y \<Longrightarrow>\<^sub>t hn_ctxt A x y
[PROOF STEP]
.


[STATEMENT]
lemma b_assn_invalid_merge1: "hn_invalid (b_assn A P) x y \<or>\<^sub>A hn_invalid (b_assn A P') x y
  \<Longrightarrow>\<^sub>t hn_invalid (b_assn A (\<lambda>x. P x \<or> P' x)) x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_invalid (b_assn A P) x y \<or>\<^sub>A hn_invalid (b_assn A P') x y \<Longrightarrow>\<^sub>t hn_invalid (b_assn A (\<lambda>x. P x \<or> P' x)) x y
[PROOF STEP]
by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)


[STATEMENT]
lemma b_assn_invalid_merge2: "hn_invalid (b_assn A P) x y \<or>\<^sub>A hn_invalid A x y
  \<Longrightarrow>\<^sub>t hn_invalid A x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_invalid (b_assn A P) x y \<or>\<^sub>A hn_invalid A x y \<Longrightarrow>\<^sub>t hn_invalid A x y
[PROOF STEP]
by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)


[STATEMENT]
lemma b_assn_invalid_merge3: "hn_invalid A x y \<or>\<^sub>A hn_invalid (b_assn A P) x y
  \<Longrightarrow>\<^sub>t hn_invalid A x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_invalid A x y \<or>\<^sub>A hn_invalid (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_invalid A x y
[PROOF STEP]
by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)


[STATEMENT]
lemma b_assn_invalid_merge4: "hn_invalid (b_assn A P) x y \<or>\<^sub>A hn_ctxt (b_assn A P') x y
  \<Longrightarrow>\<^sub>t hn_invalid (b_assn A (\<lambda>x. P x \<or> P' x)) x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_invalid (b_assn A P) x y \<or>\<^sub>A hn_ctxt (b_assn A P') x y \<Longrightarrow>\<^sub>t hn_invalid (b_assn A (\<lambda>x. P x \<or> P' x)) x y
[PROOF STEP]
by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)


[STATEMENT]
lemma b_assn_invalid_merge5: "hn_ctxt (b_assn A P') x y \<or>\<^sub>A hn_invalid (b_assn A P) x y
  \<Longrightarrow>\<^sub>t hn_invalid (b_assn A (\<lambda>x. P x \<or> P' x)) x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (b_assn A P') x y \<or>\<^sub>A hn_invalid (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_invalid (b_assn A (\<lambda>x. P x \<or> P' x)) x y
[PROOF STEP]
by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)


[STATEMENT]
lemma b_assn_invalid_merge6: "hn_invalid (b_assn A P) x y \<or>\<^sub>A hn_ctxt A x y
  \<Longrightarrow>\<^sub>t hn_invalid A x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_invalid (b_assn A P) x y \<or>\<^sub>A hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_invalid A x y
[PROOF STEP]
by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)


[STATEMENT]
lemma b_assn_invalid_merge7: "hn_ctxt A x y \<or>\<^sub>A hn_invalid (b_assn A P) x y
  \<Longrightarrow>\<^sub>t hn_invalid A x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt A x y \<or>\<^sub>A hn_invalid (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_invalid A x y
[PROOF STEP]
by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)


[STATEMENT]
lemma b_assn_invalid_merge8: "hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_invalid A x y
  \<Longrightarrow>\<^sub>t hn_invalid A x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (b_assn A P) x y \<or>\<^sub>A hn_invalid A x y \<Longrightarrow>\<^sub>t hn_invalid A x y
[PROOF STEP]
by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)


[STATEMENT]
lemma b_assn_invalid_merge9: "hn_invalid A x y \<or>\<^sub>A hn_ctxt (b_assn A P) x y
  \<Longrightarrow>\<^sub>t hn_invalid A x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_invalid A x y \<or>\<^sub>A hn_ctxt (b_assn A P) x y \<Longrightarrow>\<^sub>t hn_invalid A x y
[PROOF STEP]
by (sep_auto simp: hn_ctxt_def invalid_assn_def entailst_def)


[STATEMENT]
lemma [sepref_relprops_simps]:
  "CONSTRAINT (IS_PURE IS_ID) A \<Longrightarrow> CONSTRAINT (IS_PURE IS_BELOW_ID) A"
  "CONSTRAINT (IS_PURE IS_ID) A \<Longrightarrow> CONSTRAINT (IS_PURE IS_LEFT_TOTAL) A"
  "CONSTRAINT (IS_PURE IS_ID) A \<Longrightarrow> CONSTRAINT (IS_PURE IS_RIGHT_TOTAL) A"
  "CONSTRAINT (IS_PURE IS_BELOW_ID) A \<Longrightarrow> CONSTRAINT (IS_PURE IS_LEFT_UNIQUE) A"
  "CONSTRAINT (IS_PURE IS_BELOW_ID) A \<Longrightarrow> CONSTRAINT (IS_PURE IS_RIGHT_UNIQUE) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((CONSTRAINT (IS_PURE IS_ID) A \<Longrightarrow> CONSTRAINT (IS_PURE IS_BELOW_ID) A) &&& (CONSTRAINT (IS_PURE IS_ID) A \<Longrightarrow> CONSTRAINT (IS_PURE IS_LEFT_TOTAL) A)) &&& (CONSTRAINT (IS_PURE IS_ID) A \<Longrightarrow> CONSTRAINT (IS_PURE IS_RIGHT_TOTAL) A) &&& (CONSTRAINT (IS_PURE IS_BELOW_ID) A \<Longrightarrow> CONSTRAINT (IS_PURE IS_LEFT_UNIQUE) A) &&& (CONSTRAINT (IS_PURE IS_BELOW_ID) A \<Longrightarrow> CONSTRAINT (IS_PURE single_valued) A)
[PROOF STEP]
by (auto
    simp: IS_ID_def IS_BELOW_ID_def IS_PURE_def IS_LEFT_UNIQUE_def
    simp: IS_LEFT_TOTAL_def IS_RIGHT_TOTAL_def
    simp: single_valued_below_Id)


[STATEMENT]
lemma [sepref_relprops_transform]: "single_valued (R\<inverse>) = IS_LEFT_UNIQUE R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued (R\<inverse>) = IS_LEFT_UNIQUE R
[PROOF STEP]
by (auto simp: IS_LEFT_UNIQUE_def)


[STATEMENT]
lemma hn_if[sepref_comb_rules]:
  assumes P: "\<Gamma> \<Longrightarrow>\<^sub>t \<Gamma>1 * hn_val bool_rel a a'"
  assumes RT: "a \<Longrightarrow> hn_refine (\<Gamma>1 * hn_val bool_rel a a') b' \<Gamma>2b R b"
  assumes RE: "\<not>a \<Longrightarrow> hn_refine (\<Gamma>1 * hn_val bool_rel a a') c' \<Gamma>2c R c"
  assumes IMP: "TERM If \<Longrightarrow> \<Gamma>2b \<or>\<^sub>A \<Gamma>2c \<Longrightarrow>\<^sub>t \<Gamma>'"
  shows "hn_refine \<Gamma> (if a' then b' else c') \<Gamma>' R (If$a$b$c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine \<Gamma> (if a' then b' else c') \<Gamma>' R (If $ a $ b $ c)
[PROOF STEP]
using P RT RE IMP[OF TERMI]
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<Longrightarrow>\<^sub>t \<Gamma>1 * hn_val bool_rel a a'
a \<Longrightarrow> hn_refine (\<Gamma>1 * hn_val bool_rel a a') b' \<Gamma>2b R b
\<not> a \<Longrightarrow> hn_refine (\<Gamma>1 * hn_val bool_rel a a') c' \<Gamma>2c R c
\<Gamma>2b \<or>\<^sub>A \<Gamma>2c \<Longrightarrow>\<^sub>t \<Gamma>'

goal (1 subgoal):
 1. hn_refine \<Gamma> (if a' then b' else c') \<Gamma>' R (If $ a $ b $ c)
[PROOF STEP]
unfolding APP_def PROTECT2_def
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<Longrightarrow>\<^sub>t \<Gamma>1 * hn_val bool_rel a a'
a \<Longrightarrow> hn_refine (\<Gamma>1 * hn_val bool_rel a a') b' \<Gamma>2b R b
\<not> a \<Longrightarrow> hn_refine (\<Gamma>1 * hn_val bool_rel a a') c' \<Gamma>2c R c
\<Gamma>2b \<or>\<^sub>A \<Gamma>2c \<Longrightarrow>\<^sub>t \<Gamma>'

goal (1 subgoal):
 1. hn_refine \<Gamma> (if a' then b' else c') \<Gamma>' R (if a then b else c)
[PROOF STEP]
by (rule hnr_If)


[STATEMENT]
lemma hn_let[sepref_comb_rules]:
  assumes P: "\<Gamma> \<Longrightarrow>\<^sub>t \<Gamma>1 * hn_ctxt R v v'"
  assumes R: "\<And>x x'. x=v \<Longrightarrow> hn_refine (\<Gamma>1 * hn_ctxt R x x') (f' x')
    (\<Gamma>' x x') R2 (f x)"
  assumes F: "\<And>x x'. \<Gamma>' x x' \<Longrightarrow>\<^sub>t \<Gamma>2 * hn_ctxt R' x x'"
  shows
    "hn_refine \<Gamma> (Let v' f') (\<Gamma>2 * hn_ctxt R' v v') R2 (Let$v$(\<lambda>\<^sub>2x. f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine \<Gamma> (Let v' f') (\<Gamma>2 * hn_ctxt R' v v') R2 (Let $ v $ (\<lambda>x. (#f x#)))
[PROOF STEP]
apply (rule hn_refine_cons[OF P _ F entt_refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma>1 * hn_ctxt R v v') (Let v' f') (\<Gamma>' v v') R2 (Let $ v $ (\<lambda>x. (#f x#)))
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma>1 * hn_ctxt R v v') (f' v') (\<Gamma>' v v') R2 (f v)
[PROOF STEP]
apply (rule R)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = v
[PROOF STEP]
by simp


[STATEMENT]
lemma hnr_default[sepref_import_param]: "(default,default)\<in>Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (default, default) \<in> Id
[PROOF STEP]
by simp


[STATEMENT]
lemma unit_hnr[sepref_import_param]: "((),())\<in>unit_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((), ()) \<in> unit_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma param_min_nat[param,sepref_import_param]: "(min,min)\<in>nat_rel \<rightarrow> nat_rel \<rightarrow> nat_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (min, min) \<in> nat_rel \<rightarrow> nat_rel \<rightarrow> nat_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma param_max_nat[param,sepref_import_param]: "(max,max)\<in>nat_rel \<rightarrow> nat_rel \<rightarrow> nat_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (max, max) \<in> nat_rel \<rightarrow> nat_rel \<rightarrow> nat_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma param_min_int[param,sepref_import_param]: "(min,min)\<in>int_rel \<rightarrow> int_rel \<rightarrow> int_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (min, min) \<in> int_rel \<rightarrow> int_rel \<rightarrow> int_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma param_max_int[param,sepref_import_param]: "(max,max)\<in>int_rel \<rightarrow> int_rel \<rightarrow> int_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (max, max) \<in> int_rel \<rightarrow> int_rel \<rightarrow> int_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma uminus_hnr[sepref_import_param]: "(uminus,uminus)\<in>int_rel \<rightarrow> int_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (uminus, uminus) \<in> int_rel \<rightarrow> int_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma nat_param[param,sepref_import_param]: "(nat,nat) \<in> int_rel \<rightarrow> nat_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nat, nat) \<in> int_rel \<rightarrow> nat_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma int_param[param,sepref_import_param]: "(int,int) \<in> nat_rel \<rightarrow> int_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (int, int) \<in> nat_rel \<rightarrow> int_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma prod_assn_precise[constraint_rules]:
  "precise P1 \<Longrightarrow> precise P2 \<Longrightarrow> precise (prod_assn P1 P2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>precise P1; precise P2\<rbrakk> \<Longrightarrow> precise (P1 \<times>\<^sub>a P2)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F'. \<lbrakk>precise P1; precise P2; h \<Turnstile> (P1 \<times>\<^sub>a P2) a p * F \<and>\<^sub>A (P1 \<times>\<^sub>a P2) a' p * F'\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
apply (clarsimp simp: prod_assn_def star_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * (P2 b bc * F) \<and>\<^sub>A P1 aa ac * (P2 ba bc * F')\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * (P2 b bc * F) \<and>\<^sub>A P1 aa ac * (P2 ba bc * F')\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * (P2 b bc * F) \<and>\<^sub>A P1 aa ac * (P2 ba bc * F')\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
apply (erule (1) prec_frame)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P2; (ab, bb) \<Turnstile> P1 a ac * (P2 b bc * F) \<and>\<^sub>A P1 aa ac * (P2 ba bc * F')\<rbrakk> \<Longrightarrow> P1 a ac * (P2 b bc * F) \<Longrightarrow>\<^sub>A P1 a (?p4 a b aa ba ab bb ac bc F F') * ?F1.4 a b aa ba ab bb ac bc F F'
 2. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P2; (ab, bb) \<Turnstile> P1 a ac * (P2 b bc * F) \<and>\<^sub>A P1 aa ac * (P2 ba bc * F')\<rbrakk> \<Longrightarrow> P1 aa ac * (P2 ba bc * F') \<Longrightarrow>\<^sub>A P1 aa (?p4 a b aa ba ab bb ac bc F F') * ?F2.4 a b aa ba ab bb ac bc F F'
 3. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * (P2 b bc * F) \<and>\<^sub>A P1 aa ac * (P2 ba bc * F')\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
apply frame_inference+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; precise P2; (ab, bb) \<Turnstile> P1 a ac * (P2 b bc * F) \<and>\<^sub>A P1 aa ac * (P2 ba bc * F')\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
apply (erule (1) prec_frame)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; (ab, bb) \<Turnstile> P1 a ac * (P2 b bc * F) \<and>\<^sub>A P1 aa ac * (P2 ba bc * F')\<rbrakk> \<Longrightarrow> P1 a ac * (P2 b bc * F) \<Longrightarrow>\<^sub>A P2 b (?p24 a b aa ba ab bb ac bc F F') * ?F1.24 a b aa ba ab bb ac bc F F'
 2. \<And>a b aa ba ab bb ac bc F F'. \<lbrakk>precise P1; (ab, bb) \<Turnstile> P1 a ac * (P2 b bc * F) \<and>\<^sub>A P1 aa ac * (P2 ba bc * F')\<rbrakk> \<Longrightarrow> P1 aa ac * (P2 ba bc * F') \<Longrightarrow>\<^sub>A P2 ba (?p24 a b aa ba ab bb ac bc F F') * ?F2.24 a b aa ba ab bb ac bc F F'
[PROOF STEP]
apply frame_inference+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done