[STATEMENT]
lemma rel_resource_pos_distr:
  "rel_resource A B OO rel_resource A' B' \<le> rel_resource (A OO A') (B OO B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A B OO rel_resource A' B' \<le> rel_resource (A OO A') (B OO B')
[PROOF STEP]
proof(rule predicate2I)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (rel_resource A B OO rel_resource A' B') x y \<Longrightarrow> rel_resource (A OO A') (B OO B') x y
[PROOF STEP]
show "rel_resource (A OO A') (B OO B') res1 res3"
    if "(rel_resource A B OO rel_resource A' B') res1 res3"
    for res1 res3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource (A OO A') (B OO B') res1 res3
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(rel_resource A B OO rel_resource A' B') res1 res3

goal (1 subgoal):
 1. rel_resource (A OO A') (B OO B') res1 res3
[PROOF STEP]
apply(coinduction arbitrary: res1 res3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>res1a__ res3. (rel_resource A B OO rel_resource A' B') res1a__ res3 \<Longrightarrow> rel_fun (A OO A') (rel_spmf (rel_prod (B OO B') (\<lambda>res1 res2. (\<exists>res1a__ res3. res1 = res1a__ \<and> res2 = res3 \<and> (rel_resource A B OO rel_resource A' B') res1a__ res3) \<or> rel_resource (A OO A') (B OO B') res1 res2))) (run_resource res1a__) (run_resource res3)
[PROOF STEP]
apply(erule relcomppE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>res1a__ res3 b. \<lbrakk>rel_resource A B res1a__ b; rel_resource A' B' b res3\<rbrakk> \<Longrightarrow> rel_fun (A OO A') (rel_spmf (rel_prod (B OO B') (\<lambda>res1 res2. (\<exists>res1a__ res3. res1 = res1a__ \<and> res2 = res3 \<and> (rel_resource A B OO rel_resource A' B') res1a__ res3) \<or> rel_resource (A OO A') (B OO B') res1 res2))) (run_resource res1a__) (run_resource res3)
[PROOF STEP]
apply(drule rel_resourceD)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>res1a__ res3 b. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3)\<rbrakk> \<Longrightarrow> rel_fun (A OO A') (rel_spmf (rel_prod (B OO B') (\<lambda>res1 res2. (\<exists>res1a__ res3. res1 = res1a__ \<and> res2 = res3 \<and> (rel_resource A B OO rel_resource A' B') res1a__ res3) \<or> rel_resource (A OO A') (B OO B') res1 res2))) (run_resource res1a__) (run_resource res3)
[PROOF STEP]
apply(rule rel_fun_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>res1a__ res3 b. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3)\<rbrakk> \<Longrightarrow> rel_fun (?X9 res1a__ res3 b) (?A9 res1a__ res3 b) (run_resource res1a__) (run_resource res3)
 2. \<And>res1a__ res3 b x y. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3)\<rbrakk> \<Longrightarrow> (A OO A') x y \<longrightarrow> ?X9 res1a__ res3 b x y
 3. \<And>res1a__ res3 b x y. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3); ?A9 res1a__ res3 b x y\<rbrakk> \<Longrightarrow> rel_spmf (rel_prod (B OO B') (\<lambda>res1 res2. (\<exists>res1a__ res3. res1 = res1a__ \<and> res2 = res3 \<and> (rel_resource A B OO rel_resource A' B') res1a__ res3) \<or> rel_resource (A OO A') (B OO B') res1 res2)) x y
[PROOF STEP]
apply(rule pos_fun_distr[THEN predicate2D])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>res1a__ res3 b. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3)\<rbrakk> \<Longrightarrow> (rel_fun (?R14 res1a__ res3 b) (?S14 res1a__ res3 b) OO rel_fun (?R'14 res1a__ res3 b) (?S'14 res1a__ res3 b)) (run_resource res1a__) (run_resource res3)
 2. \<And>res1a__ res3 b x y. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3)\<rbrakk> \<Longrightarrow> (A OO A') x y \<longrightarrow> (?R14 res1a__ res3 b OO ?R'14 res1a__ res3 b) x y
 3. \<And>res1a__ res3 b x y. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3); (?S14 res1a__ res3 b OO ?S'14 res1a__ res3 b) x y\<rbrakk> \<Longrightarrow> rel_spmf (rel_prod (B OO B') (\<lambda>res1 res2. (\<exists>res1a__ res3. res1 = res1a__ \<and> res2 = res3 \<and> (rel_resource A B OO rel_resource A' B') res1a__ res3) \<or> rel_resource (A OO A') (B OO B') res1 res2)) x y
[PROOF STEP]
apply(erule (1) relcomppI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>res1a__ res3 b x y. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3)\<rbrakk> \<Longrightarrow> (A OO A') x y \<longrightarrow> (A OO A') x y
 2. \<And>res1a__ res3 b x y. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3); (rel_spmf (rel_prod B (rel_resource A B)) OO rel_spmf (rel_prod B' (rel_resource A' B'))) x y\<rbrakk> \<Longrightarrow> rel_spmf (rel_prod (B OO B') (\<lambda>res1 res2. (\<exists>res1a__ res3. res1 = res1a__ \<and> res2 = res3 \<and> (rel_resource A B OO rel_resource A' B') res1a__ res3) \<or> rel_resource (A OO A') (B OO B') res1 res2)) x y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>res1a__ res3 b x y. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3); (rel_spmf (rel_prod B (rel_resource A B)) OO rel_spmf (rel_prod B' (rel_resource A' B'))) x y\<rbrakk> \<Longrightarrow> rel_spmf (rel_prod (B OO B') (\<lambda>res1 res2. (\<exists>res1a__ res3. res1 = res1a__ \<and> res2 = res3 \<and> (rel_resource A B OO rel_resource A' B') res1a__ res3) \<or> rel_resource (A OO A') (B OO B') res1 res2)) x y
[PROOF STEP]
apply(rule rel_spmf_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>res1a__ res3 b x y. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3); (rel_spmf (rel_prod B (rel_resource A B)) OO rel_spmf (rel_prod B' (rel_resource A' B'))) x y\<rbrakk> \<Longrightarrow> rel_spmf (?A18 res1a__ res3 b x y) x y
 2. \<And>res1a__ res3 b x y xa ya. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3); (rel_spmf (rel_prod B (rel_resource A B)) OO rel_spmf (rel_prod B' (rel_resource A' B'))) x y; ?A18 res1a__ res3 b x y xa ya\<rbrakk> \<Longrightarrow> rel_prod (B OO B') (\<lambda>res1 res2. (\<exists>res1a__ res3. res1 = res1a__ \<and> res2 = res3 \<and> (rel_resource A B OO rel_resource A' B') res1a__ res3) \<or> rel_resource (A OO A') (B OO B') res1 res2) xa ya
[PROOF STEP]
apply(erule rel_spmf_pos_distr[THEN predicate2D])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>res1a__ res3 b x y xa ya. \<lbrakk>rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1a__) (run_resource b); rel_fun A' (rel_spmf (rel_prod B' (rel_resource A' B'))) (run_resource b) (run_resource res3); (rel_spmf (rel_prod B (rel_resource A B)) OO rel_spmf (rel_prod B' (rel_resource A' B'))) x y; (rel_prod B (rel_resource A B) OO rel_prod B' (rel_resource A' B')) xa ya\<rbrakk> \<Longrightarrow> rel_prod (B OO B') (\<lambda>res1 res2. (\<exists>res1a__ res3. res1 = res1a__ \<and> res2 = res3 \<and> (rel_resource A B OO rel_resource A' B') res1a__ res3) \<or> rel_resource (A OO A') (B OO B') res1 res2) xa ya
[PROOF STEP]
apply(auto simp add: prod.rel_compp[symmetric] elim: prod.rel_mono[THEN predicate2D, rotated -1])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(rel_resource A B OO rel_resource A' B') ?res1.0 ?res3.0 \<Longrightarrow> rel_resource (A OO A') (B OO B') ?res1.0 ?res3.0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma left_unique_rel_resource:
  "\<lbrakk> left_total A; left_unique B \<rbrakk> \<Longrightarrow> left_unique (rel_resource A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (rel_resource A B)
[PROOF STEP]
unfolding left_unique_alt_def left_total_alt_def rel_resource_conversep[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(=) \<le> A OO A\<inverse>\<inverse>; B OO B\<inverse>\<inverse> \<le> (=)\<rbrakk> \<Longrightarrow> rel_resource A B OO rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> \<le> (=)
[PROOF STEP]
apply(subst rel_resource_eq[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(=) \<le> A OO A\<inverse>\<inverse>; B OO B\<inverse>\<inverse> \<le> (=)\<rbrakk> \<Longrightarrow> rel_resource A B OO rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> \<le> rel_resource (=) (=)
[PROOF STEP]
apply(rule order_trans[OF rel_resource_pos_distr])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(=) \<le> A OO A\<inverse>\<inverse>; B OO B\<inverse>\<inverse> \<le> (=)\<rbrakk> \<Longrightarrow> rel_resource (A OO A\<inverse>\<inverse>) (B OO B\<inverse>\<inverse>) \<le> rel_resource (=) (=)
[PROOF STEP]
apply(erule (1) rel_resource_mono)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma right_unique_rel_resource:
  "\<lbrakk> right_total A; right_unique B \<rbrakk> \<Longrightarrow> right_unique (rel_resource A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (rel_resource A B)
[PROOF STEP]
unfolding right_unique_alt_def right_total_alt_def rel_resource_conversep[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(=) \<le> A\<inverse>\<inverse> OO A; B\<inverse>\<inverse> OO B \<le> (=)\<rbrakk> \<Longrightarrow> rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> OO rel_resource A B \<le> (=)
[PROOF STEP]
apply(subst rel_resource_eq[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(=) \<le> A\<inverse>\<inverse> OO A; B\<inverse>\<inverse> OO B \<le> (=)\<rbrakk> \<Longrightarrow> rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> OO rel_resource A B \<le> rel_resource (=) (=)
[PROOF STEP]
apply(rule order_trans[OF rel_resource_pos_distr])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(=) \<le> A\<inverse>\<inverse> OO A; B\<inverse>\<inverse> OO B \<le> (=)\<rbrakk> \<Longrightarrow> rel_resource (A\<inverse>\<inverse> OO A) (B\<inverse>\<inverse> OO B) \<le> rel_resource (=) (=)
[PROOF STEP]
apply(erule (1) rel_resource_mono)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bi_unique_rel_resource [transfer_rule]:
  "\<lbrakk> bi_total A; bi_unique B \<rbrakk> \<Longrightarrow> bi_unique (rel_resource A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_resource A B)
[PROOF STEP]
unfolding bi_unique_alt_def bi_total_alt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>left_total A \<and> right_total A; left_unique B \<and> right_unique B\<rbrakk> \<Longrightarrow> left_unique (rel_resource A B) \<and> right_unique (rel_resource A B)
[PROOF STEP]
by(blast intro: left_unique_rel_resource right_unique_rel_resource)


[STATEMENT]
lemma rel_witness_resource_sel [simp]:
  "run_resource (rel_witness_resource A A' B (res1, res2)) =
   map_spmf (map_prod id (rel_witness_resource A A' B) \<circ> rel_witness_prod) \<circ>
   rel_witness_spmf (rel_prod B (rel_resource (A OO A') B)) \<circ>
   rel_witness_fun A A' (run_resource res1, run_resource res2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_resource (rel_witness_resource A A' B (res1, res2)) = map_spmf (map_prod id (rel_witness_resource A A' B) \<circ> rel_witness_prod) \<circ> rel_witness_spmf (rel_prod B (rel_resource (A OO A') B)) \<circ> rel_witness_fun A A' (run_resource res1, run_resource res2)
[PROOF STEP]
by(auto simp add: rel_witness_resource_def o_def fun_eq_iff spmf.map_comp intro!: map_spmf_cong)


[STATEMENT]
lemma assumes "rel_resource (A OO A') B res res'"
  and A: "left_unique A" "right_total A"
  and A': "right_unique A'" "left_total A'"
shows rel_witness_resource1: "rel_resource A (\<lambda>b (b', c). b = b' \<and> B b' c) res (rel_witness_resource A A' B (res, res'))" (is "?thesis1")
  and rel_witness_resource2: "rel_resource A' (\<lambda>(b, c') c. c = c' \<and> B b c') (rel_witness_resource A A' B (res, res')) res'" (is "?thesis2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A (\<lambda>b (b', c). b = b' \<and> B b' c) res (rel_witness_resource A A' B (res, res')) &&& rel_resource A' (\<lambda>(b, c') c. c = c' \<and> B b c') (rel_witness_resource A A' B (res, res')) res'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rel_resource A (\<lambda>b (b', c). b = b' \<and> B b' c) res (rel_witness_resource A A' B (res, res'))
 2. rel_resource A' (\<lambda>(b, c') c. c = c' \<and> B b c') (rel_witness_resource A A' B (res, res')) res'
[PROOF STEP]
show ?thesis1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A (\<lambda>b (b', c). b = b' \<and> B b' c) res (rel_witness_resource A A' B (res, res'))
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
rel_resource (A OO A') B res res'

goal (1 subgoal):
 1. rel_resource A (\<lambda>b (b', c). b = b' \<and> B b' c) res (rel_witness_resource A A' B (res, res'))
[PROOF STEP]
proof(coinduction arbitrary: res res')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>res res'. rel_resource (A OO A') B res res' \<Longrightarrow> rel_fun A (rel_spmf (rel_prod (\<lambda>b (b', c). b = b' \<and> B b' c) (\<lambda>res1 res2. (\<exists>res res'. res1 = res \<and> res2 = rel_witness_resource A A' B (res, res') \<and> rel_resource (A OO A') B res res') \<or> rel_resource A (\<lambda>b (b', c). b = b' \<and> B b' c) res1 res2))) (run_resource res) (run_resource (rel_witness_resource A A' B (res, res')))
[PROOF STEP]
case rel_resource
[PROOF STATE]
proof (state)
this:
rel_resource (A OO A') B res res'

goal (1 subgoal):
 1. \<And>res res'. rel_resource (A OO A') B res res' \<Longrightarrow> rel_fun A (rel_spmf (rel_prod (\<lambda>b (b', c). b = b' \<and> B b' c) (\<lambda>res1 res2. (\<exists>res res'. res1 = res \<and> res2 = rel_witness_resource A A' B (res, res') \<and> rel_resource (A OO A') B res res') \<or> rel_resource A (\<lambda>b (b', c). b = b' \<and> B b' c) res1 res2))) (run_resource res) (run_resource (rel_witness_resource A A' B (res, res')))
[PROOF STEP]
from this[THEN rel_resourceD]
[PROOF STATE]
proof (chain)
picking this:
rel_fun (A OO A') (rel_spmf (rel_prod B (rel_resource (A OO A') B))) (run_resource res) (run_resource res')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
rel_fun (A OO A') (rel_spmf (rel_prod B (rel_resource (A OO A') B))) (run_resource res) (run_resource res')

goal (1 subgoal):
 1. rel_fun A (rel_spmf (rel_prod (\<lambda>b (b', c). b = b' \<and> B b' c) (\<lambda>res1 res2. (\<exists>res res'. res1 = res \<and> res2 = rel_witness_resource A A' B (res, res') \<and> rel_resource (A OO A') B res res') \<or> rel_resource A (\<lambda>b (b', c). b = b' \<and> B b' c) res1 res2))) (run_resource res) (run_resource (rel_witness_resource A A' B (res, res')))
[PROOF STEP]
by(simp add: rel_fun_comp)
        (erule rel_fun_mono[OF rel_witness_fun1[OF _ A A']]
          , auto simp add: spmf_rel_map elim!: rel_spmf_mono[OF rel_witness_spmf1])
[PROOF STATE]
proof (state)
this:
rel_fun A (rel_spmf (rel_prod (\<lambda>b (b', c). b = b' \<and> B b' c) (\<lambda>res1 res2. (\<exists>res res'. res1 = res \<and> res2 = rel_witness_resource A A' B (res, res') \<and> rel_resource (A OO A') B res res') \<or> rel_resource A (\<lambda>b (b', c). b = b' \<and> B b' c) res1 res2))) (run_resource res) (run_resource (rel_witness_resource A A' B (res, res')))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_resource A (\<lambda>b (b', c). b = b' \<and> B b' c) res (rel_witness_resource A A' B (res, res'))

goal (1 subgoal):
 1. rel_resource A' (\<lambda>(b, c') c. c = c' \<and> B b c') (rel_witness_resource A A' B (res, res')) res'
[PROOF STEP]
show ?thesis2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A' (\<lambda>(b, c') c. c = c' \<and> B b c') (rel_witness_resource A A' B (res, res')) res'
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
rel_resource (A OO A') B res res'

goal (1 subgoal):
 1. rel_resource A' (\<lambda>(b, c') c. c = c' \<and> B b c') (rel_witness_resource A A' B (res, res')) res'
[PROOF STEP]
proof(coinduction arbitrary: res res')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>res res'. rel_resource (A OO A') B res res' \<Longrightarrow> rel_fun A' (rel_spmf (rel_prod (\<lambda>(b, c') c. c = c' \<and> B b c') (\<lambda>res1 res2. (\<exists>res res'. res1 = rel_witness_resource A A' B (res, res') \<and> res2 = res' \<and> rel_resource (A OO A') B res res') \<or> rel_resource A' (\<lambda>(b, c') c. c = c' \<and> B b c') res1 res2))) (run_resource (rel_witness_resource A A' B (res, res'))) (run_resource res')
[PROOF STEP]
case rel_resource
[PROOF STATE]
proof (state)
this:
rel_resource (A OO A') B res res'

goal (1 subgoal):
 1. \<And>res res'. rel_resource (A OO A') B res res' \<Longrightarrow> rel_fun A' (rel_spmf (rel_prod (\<lambda>(b, c') c. c = c' \<and> B b c') (\<lambda>res1 res2. (\<exists>res res'. res1 = rel_witness_resource A A' B (res, res') \<and> res2 = res' \<and> rel_resource (A OO A') B res res') \<or> rel_resource A' (\<lambda>(b, c') c. c = c' \<and> B b c') res1 res2))) (run_resource (rel_witness_resource A A' B (res, res'))) (run_resource res')
[PROOF STEP]
from this[THEN rel_resourceD]
[PROOF STATE]
proof (chain)
picking this:
rel_fun (A OO A') (rel_spmf (rel_prod B (rel_resource (A OO A') B))) (run_resource res) (run_resource res')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
rel_fun (A OO A') (rel_spmf (rel_prod B (rel_resource (A OO A') B))) (run_resource res) (run_resource res')

goal (1 subgoal):
 1. rel_fun A' (rel_spmf (rel_prod (\<lambda>(b, c') c. c = c' \<and> B b c') (\<lambda>res1 res2. (\<exists>res res'. res1 = rel_witness_resource A A' B (res, res') \<and> res2 = res' \<and> rel_resource (A OO A') B res res') \<or> rel_resource A' (\<lambda>(b, c') c. c = c' \<and> B b c') res1 res2))) (run_resource (rel_witness_resource A A' B (res, res'))) (run_resource res')
[PROOF STEP]
by(simp add: rel_fun_comp)
        (erule rel_fun_mono[OF rel_witness_fun2[OF _ A A']]
          , auto simp add: spmf_rel_map elim!: rel_spmf_mono[OF rel_witness_spmf2])
[PROOF STATE]
proof (state)
this:
rel_fun A' (rel_spmf (rel_prod (\<lambda>(b, c') c. c = c' \<and> B b c') (\<lambda>res1 res2. (\<exists>res res'. res1 = rel_witness_resource A A' B (res, res') \<and> res2 = res' \<and> rel_resource (A OO A') B res res') \<or> rel_resource A' (\<lambda>(b, c') c. c = c' \<and> B b c') res1 res2))) (run_resource (rel_witness_resource A A' B (res, res'))) (run_resource res')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_resource A' (\<lambda>(b, c') c. c = c' \<and> B b c') (rel_witness_resource A A' B (res, res')) res'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_resource_neg_distr:
  assumes A: "left_unique A" "right_total A"
    and A': "right_unique A'" "left_total A'"
  shows "rel_resource (A OO A') (B OO B') \<le> rel_resource A B OO rel_resource A' B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource (A OO A') (B OO B') \<le> rel_resource A B OO rel_resource A' B'
[PROOF STEP]
proof(rule predicate2I relcomppI)+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. rel_resource (A OO A') (B OO B') x y \<Longrightarrow> rel_resource A B x (?b2 x y)
 2. \<And>x y. rel_resource (A OO A') (B OO B') x y \<Longrightarrow> rel_resource A' B' (?b2 x y) y
[PROOF STEP]
fix res res''
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. rel_resource (A OO A') (B OO B') x y \<Longrightarrow> rel_resource A B x (?b2 x y)
 2. \<And>x y. rel_resource (A OO A') (B OO B') x y \<Longrightarrow> rel_resource A' B' (?b2 x y) y
[PROOF STEP]
assume *: "rel_resource (A OO A') (B OO B') res res''"
[PROOF STATE]
proof (state)
this:
rel_resource (A OO A') (B OO B') res res''

goal (2 subgoals):
 1. \<And>x y. rel_resource (A OO A') (B OO B') x y \<Longrightarrow> rel_resource A B x (?b2 x y)
 2. \<And>x y. rel_resource (A OO A') (B OO B') x y \<Longrightarrow> rel_resource A' B' (?b2 x y) y
[PROOF STEP]
let ?res' = "map_resource' (relcompp_witness B B') (rel_witness_resource A A' (B OO B') (res, res''))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. rel_resource (A OO A') (B OO B') x y \<Longrightarrow> rel_resource A B x (?b2 x y)
 2. \<And>x y. rel_resource (A OO A') (B OO B') x y \<Longrightarrow> rel_resource A' B' (?b2 x y) y
[PROOF STEP]
show "rel_resource A B res ?res'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A B res (map_resource' (relcompp_witness B B') (rel_witness_resource A A' (B OO B') (res, res'')))
[PROOF STEP]
using rel_witness_resource1[OF * A A']
[PROOF STATE]
proof (prove)
using this:
rel_resource A (\<lambda>b (b', c). b = b' \<and> (B OO B') b' c) res (rel_witness_resource A A' (B OO B') (res, res''))

goal (1 subgoal):
 1. rel_resource A B res (map_resource' (relcompp_witness B B') (rel_witness_resource A A' (B OO B') (res, res'')))
[PROOF STEP]
unfolding resource_rel_map'
[PROOF STATE]
proof (prove)
using this:
rel_resource A (\<lambda>b (b', c). b = b' \<and> (B OO B') b' c) res (rel_witness_resource A A' (B OO B') (res, res''))

goal (1 subgoal):
 1. rel_resource A (\<lambda>x y. B x (relcompp_witness B B' y)) res (rel_witness_resource A A' (B OO B') (res, res''))
[PROOF STEP]
by(rule rel_resource_mono[THEN predicate2D, rotated -1]; clarify del: relcomppE elim!: relcompp_witness)
[PROOF STATE]
proof (state)
this:
rel_resource A B res (map_resource' (relcompp_witness B B') (rel_witness_resource A A' (B OO B') (res, res'')))

goal (1 subgoal):
 1. \<And>x y. rel_resource (A OO A') (B OO B') x y \<Longrightarrow> rel_resource A' B' (map_resource' (relcompp_witness B B') (rel_witness_resource A A' (B OO B') (x, y))) y
[PROOF STEP]
show "rel_resource A' B' ?res' res''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A' B' (map_resource' (relcompp_witness B B') (rel_witness_resource A A' (B OO B') (res, res''))) res''
[PROOF STEP]
using rel_witness_resource2[OF * A A']
[PROOF STATE]
proof (prove)
using this:
rel_resource A' (\<lambda>(b, c') c. c = c' \<and> (B OO B') b c') (rel_witness_resource A A' (B OO B') (res, res'')) res''

goal (1 subgoal):
 1. rel_resource A' B' (map_resource' (relcompp_witness B B') (rel_witness_resource A A' (B OO B') (res, res''))) res''
[PROOF STEP]
unfolding resource_rel_map'
[PROOF STATE]
proof (prove)
using this:
rel_resource A' (\<lambda>(b, c') c. c = c' \<and> (B OO B') b c') (rel_witness_resource A A' (B OO B') (res, res'')) res''

goal (1 subgoal):
 1. rel_resource A' (\<lambda>x. B' (relcompp_witness B B' x)) (rel_witness_resource A A' (B OO B') (res, res'')) res''
[PROOF STEP]
by(rule rel_resource_mono[THEN predicate2D, rotated -1]; clarify del: relcomppE elim!: relcompp_witness)
[PROOF STATE]
proof (state)
this:
rel_resource A' B' (map_resource' (relcompp_witness B B') (rel_witness_resource A A' (B OO B') (res, res''))) res''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma left_total_rel_resource:
  "\<lbrakk> left_unique A; right_total A; left_total B \<rbrakk> \<Longrightarrow> left_total (rel_resource A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>left_unique A; right_total A; left_total B\<rbrakk> \<Longrightarrow> left_total (rel_resource A B)
[PROOF STEP]
unfolding left_unique_alt_def left_total_alt_def rel_resource_conversep[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A OO A\<inverse>\<inverse> \<le> (=); right_total A; (=) \<le> B OO B\<inverse>\<inverse>\<rbrakk> \<Longrightarrow> (=) \<le> rel_resource A B OO rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse>
[PROOF STEP]
apply(subst rel_resource_eq[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A OO A\<inverse>\<inverse> \<le> (=); right_total A; (=) \<le> B OO B\<inverse>\<inverse>\<rbrakk> \<Longrightarrow> rel_resource (=) (=) \<le> rel_resource A B OO rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse>
[PROOF STEP]
apply(rule order_trans[rotated])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A OO A\<inverse>\<inverse> \<le> (=); right_total A; (=) \<le> B OO B\<inverse>\<inverse>\<rbrakk> \<Longrightarrow> ?y \<le> rel_resource A B OO rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse>
 2. \<lbrakk>A OO A\<inverse>\<inverse> \<le> (=); right_total A; (=) \<le> B OO B\<inverse>\<inverse>\<rbrakk> \<Longrightarrow> rel_resource (=) (=) \<le> ?y
[PROOF STEP]
apply(rule rel_resource_neg_distr; simp add: left_unique_alt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A OO A\<inverse>\<inverse> \<le> (=); right_total A; (=) \<le> B OO B\<inverse>\<inverse>\<rbrakk> \<Longrightarrow> rel_resource (=) (=) \<le> rel_resource (A OO A\<inverse>\<inverse>) (B OO B\<inverse>\<inverse>)
[PROOF STEP]
apply(rule rel_resource_mono; assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma right_total_rel_resource:
  "\<lbrakk> right_unique A; left_total A; right_total B \<rbrakk> \<Longrightarrow> right_total (rel_resource A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>right_unique A; left_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (rel_resource A B)
[PROOF STEP]
unfolding right_unique_alt_def right_total_alt_def rel_resource_conversep[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A\<inverse>\<inverse> OO A \<le> (=); left_total A; (=) \<le> B\<inverse>\<inverse> OO B\<rbrakk> \<Longrightarrow> (=) \<le> rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> OO rel_resource A B
[PROOF STEP]
apply(subst rel_resource_eq[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A\<inverse>\<inverse> OO A \<le> (=); left_total A; (=) \<le> B\<inverse>\<inverse> OO B\<rbrakk> \<Longrightarrow> rel_resource (=) (=) \<le> rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> OO rel_resource A B
[PROOF STEP]
apply(rule order_trans[rotated])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A\<inverse>\<inverse> OO A \<le> (=); left_total A; (=) \<le> B\<inverse>\<inverse> OO B\<rbrakk> \<Longrightarrow> ?y \<le> rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> OO rel_resource A B
 2. \<lbrakk>A\<inverse>\<inverse> OO A \<le> (=); left_total A; (=) \<le> B\<inverse>\<inverse> OO B\<rbrakk> \<Longrightarrow> rel_resource (=) (=) \<le> ?y
[PROOF STEP]
apply(rule rel_resource_neg_distr; simp add: right_unique_alt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A\<inverse>\<inverse> OO A \<le> (=); left_total A; (=) \<le> B\<inverse>\<inverse> OO B\<rbrakk> \<Longrightarrow> rel_resource (=) (=) \<le> rel_resource (A\<inverse>\<inverse> OO A) (B\<inverse>\<inverse> OO B)
[PROOF STEP]
apply(rule rel_resource_mono; assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bi_total_rel_resource [transfer_rule]:
  "\<lbrakk> bi_total A; bi_unique A; bi_total B \<rbrakk> \<Longrightarrow> bi_total (rel_resource A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bi_total A; bi_unique A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (rel_resource A B)
[PROOF STEP]
unfolding bi_total_alt_def bi_unique_alt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>left_total A \<and> right_total A; left_unique A \<and> right_unique A; left_total B \<and> right_total B\<rbrakk> \<Longrightarrow> left_total (rel_resource A B) \<and> right_total (rel_resource A B)
[PROOF STEP]
by(blast intro: left_total_rel_resource right_total_rel_resource)


[STATEMENT]
lemma Resource_parametric [transfer_rule]:
  "((A ===> rel_spmf (rel_prod B (rel_resource A B))) ===> rel_resource A B) Resource Resource"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> rel_spmf (rel_prod B (rel_resource A B))) ===> rel_resource A B) Resource Resource
[PROOF STEP]
by(rule rel_funI)(simp)


[STATEMENT]
lemma run_resource_parametric [transfer_rule]:
  "(rel_resource A B ===> A ===> rel_spmf (rel_prod B (rel_resource A B))) run_resource run_resource"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_resource A B ===> A ===> rel_spmf (rel_prod B (rel_resource A B))) run_resource run_resource
[PROOF STEP]
by(rule rel_funI)(auto dest: rel_resourceD)


[STATEMENT]
lemma corec_resource_parametric [transfer_rule]:
  "((S ===> A ===> rel_spmf (rel_prod B (rel_sum (rel_resource A B) S))) ===> S ===> rel_resource A B)
   corec_resource corec_resource"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((S ===> A ===> rel_spmf (rel_prod B (rel_sum (rel_resource A B) S))) ===> S ===> rel_resource A B) corec_resource corec_resource
[PROOF STEP]
proof((rule rel_funI)+, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>(S ===> A ===> rel_spmf (rel_prod B (rel_sum (rel_resource A B) S))) x y; S xa ya\<rbrakk> \<Longrightarrow> rel_resource A B (corec_resource x xa) (corec_resource y ya)
[PROOF STEP]
case (1 f g s1 s2)
[PROOF STATE]
proof (state)
this:
(S ===> A ===> rel_spmf (rel_prod B (rel_sum (rel_resource A B) S))) f g
S s1 s2

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>(S ===> A ===> rel_spmf (rel_prod B (rel_sum (rel_resource A B) S))) x y; S xa ya\<rbrakk> \<Longrightarrow> rel_resource A B (corec_resource x xa) (corec_resource y ya)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(S ===> A ===> rel_spmf (rel_prod B (rel_sum (rel_resource A B) S))) f g
S s1 s2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(S ===> A ===> rel_spmf (rel_prod B (rel_sum (rel_resource A B) S))) f g
S s1 s2

goal (1 subgoal):
 1. rel_resource A B (corec_resource f s1) (corec_resource g s2)
[PROOF STEP]
using 1(2)
[PROOF STATE]
proof (prove)
using this:
(S ===> A ===> rel_spmf (rel_prod B (rel_sum (rel_resource A B) S))) f g
S s1 s2
S s1 s2

goal (1 subgoal):
 1. rel_resource A B (corec_resource f s1) (corec_resource g s2)
[PROOF STEP]
by (coinduction arbitrary: s1 s2)
      (drule 1(1)[THEN rel_funD], auto 4 4 simp add: rel_fun_comp spmf_rel_map prod.rel_map[abs_def] split: sum.split elim!: rel_fun_mono rel_spmf_mono elim: prod.rel_mono[THEN predicate2D, rotated -1])
[PROOF STATE]
proof (state)
this:
rel_resource A B (corec_resource f s1) (corec_resource g s2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_resource_parametric [transfer_rule]:
  "((A' ===> A) ===> (B ===> B') ===> rel_resource A B ===> rel_resource A' B') map_resource map_resource"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A' ===> A) ===> (B ===> B') ===> rel_resource A B ===> rel_resource A' B') map_resource map_resource
[PROOF STEP]
unfolding map_resource_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A' ===> A) ===> (B ===> B') ===> rel_resource A B ===> rel_resource A' B') (\<lambda>a b. corec_resource (\<lambda>res. map_spmf (map_prod b Inr) \<circ> run_resource res \<circ> a)) (\<lambda>a b. corec_resource (\<lambda>res. map_spmf (map_prod b Inr) \<circ> run_resource res \<circ> a))
[PROOF STEP]
by(transfer_prover)


[STATEMENT]
lemma map_resource'_parametric [transfer_rule]:
  "((B ===> B') ===> rel_resource (=) B ===> rel_resource (=) B') map_resource' map_resource'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((B ===> B') ===> rel_resource (=) B ===> rel_resource (=) B') map_resource' map_resource'
[PROOF STEP]
unfolding map_resource_id1[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((B ===> B') ===> rel_resource (=) B ===> rel_resource (=) B') (map_resource id) (map_resource id)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma case_resource_parametric [transfer_rule]:
  "(((A ===> rel_spmf (rel_prod B (rel_resource A B))) ===> C) ===> rel_resource A B ===> C)
  case_resource case_resource"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((A ===> rel_spmf (rel_prod B (rel_resource A B))) ===> C) ===> rel_resource A B ===> C) case_resource case_resource
[PROOF STEP]
unfolding case_resource_conv_run_resource
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((A ===> rel_spmf (rel_prod B (rel_resource A B))) ===> C) ===> rel_resource A B ===> C) (\<lambda>f res. f (run_resource res)) (\<lambda>f res. f (run_resource res))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma rel_resource_Grp:
  "rel_resource (conversep (BNF_Def.Grp UNIV f)) (BNF_Def.Grp UNIV g) = BNF_Def.Grp UNIV (map_resource f g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) = BNF_Def.Grp UNIV (map_resource f g)
[PROOF STEP]
proof((rule ext iffI)+, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) x xa \<Longrightarrow> BNF_Def.Grp UNIV (map_resource f g) x xa
 2. \<And>x xa. BNF_Def.Grp UNIV (map_resource f g) x xa \<Longrightarrow> rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) x xa
[PROOF STEP]
case (1 res res')
[PROOF STATE]
proof (state)
this:
rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) res res'

goal (2 subgoals):
 1. \<And>x xa. rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) x xa \<Longrightarrow> BNF_Def.Grp UNIV (map_resource f g) x xa
 2. \<And>x xa. BNF_Def.Grp UNIV (map_resource f g) x xa \<Longrightarrow> rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) x xa
[PROOF STEP]
have *: "rel_resource (\<lambda>a b. b = f a)\<inverse>\<inverse> (\<lambda>a b. b = g a) res res' \<Longrightarrow> res' = map_resource f g res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource (\<lambda>a b. b = f a)\<inverse>\<inverse> (\<lambda>a b. b = g a) res res' \<Longrightarrow> res' = map_resource f g res
[PROOF STEP]
by(rule sym, subst (3) map_resource_id[symmetric], subst rel_resource_eq[symmetric])
      (erule map_resource_parametric[THEN rel_funD, THEN rel_funD, THEN rel_funD, rotated -1]
        , auto simp add: rel_fun_def)
[PROOF STATE]
proof (state)
this:
rel_resource (\<lambda>a b. b = f a)\<inverse>\<inverse> (\<lambda>a b. b = g a) res res' \<Longrightarrow> res' = map_resource f g res

goal (2 subgoals):
 1. \<And>x xa. rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) x xa \<Longrightarrow> BNF_Def.Grp UNIV (map_resource f g) x xa
 2. \<And>x xa. BNF_Def.Grp UNIV (map_resource f g) x xa \<Longrightarrow> rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) x xa
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) res res'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) res res'

goal (1 subgoal):
 1. BNF_Def.Grp UNIV (map_resource f g) res res'
[PROOF STEP]
unfolding Grp_def
[PROOF STATE]
proof (prove)
using this:
rel_resource (\<lambda>a b. b = f a \<and> a \<in> UNIV)\<inverse>\<inverse> (\<lambda>a b. b = g a \<and> a \<in> UNIV) res res'

goal (1 subgoal):
 1. res' = map_resource f g res \<and> res \<in> UNIV
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
rel_resource (\<lambda>a b. b = f a \<and> a \<in> UNIV)\<inverse>\<inverse> (\<lambda>a b. b = g a \<and> a \<in> UNIV) res res'
rel_resource (\<lambda>a b. b = f a)\<inverse>\<inverse> (\<lambda>a b. b = g a) res res' \<Longrightarrow> res' = map_resource f g res

goal (1 subgoal):
 1. res' = map_resource f g res \<and> res \<in> UNIV
[PROOF STEP]
by (clarsimp simp add: * simp del: conversep_iff)
[PROOF STATE]
proof (state)
this:
BNF_Def.Grp UNIV (map_resource f g) res res'

goal (1 subgoal):
 1. \<And>x xa. BNF_Def.Grp UNIV (map_resource f g) x xa \<Longrightarrow> rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) x xa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. BNF_Def.Grp UNIV (map_resource f g) x xa \<Longrightarrow> rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) x xa
[PROOF STEP]
case (2 _ _)
[PROOF STATE]
proof (state)
this:
BNF_Def.Grp UNIV (map_resource f g) x_ xa_

goal (1 subgoal):
 1. \<And>x xa. BNF_Def.Grp UNIV (map_resource f g) x xa \<Longrightarrow> rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) x xa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
BNF_Def.Grp UNIV (map_resource f g) x_ xa_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
BNF_Def.Grp UNIV (map_resource f g) x_ xa_

goal (1 subgoal):
 1. rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) x_ xa_
[PROOF STEP]
by(clarsimp simp add: Grp_iff, subst map_resource_id[symmetric])
      (rule map_resource_parametric[THEN rel_funD, THEN rel_funD, THEN rel_funD, rotated -1]
        , subst rel_resource_eq, auto simp add: Grp_iff rel_fun_def)
[PROOF STATE]
proof (state)
this:
rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g) x_ xa_

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lossless_resourceD:
  "\<lbrakk> lossless_resource \<I> res; a \<in> outs_\<I> \<I> \<rbrakk>
  \<Longrightarrow> lossless_spmf (run_resource res a) \<and> (\<forall>(x, res')\<in>set_spmf (run_resource res a). lossless_resource \<I> res')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lossless_resource \<I> res; a \<in> outs_\<I> \<I>\<rbrakk> \<Longrightarrow> lossless_spmf (run_resource res a) \<and> (\<forall>(x, res')\<in>set_spmf (run_resource res a). lossless_resource \<I> res')
[PROOF STEP]
by(auto elim: lossless_resource.cases)


[STATEMENT]
lemma lossless_resource_mono:
  assumes "lossless_resource \<I>' res"
    and le: "outs_\<I> \<I> \<subseteq> outs_\<I> \<I>'"
  shows "lossless_resource \<I> res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_resource \<I> res
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
lossless_resource \<I>' res

goal (1 subgoal):
 1. lossless_resource \<I> res
[PROOF STEP]
by(coinduction arbitrary: res)(auto dest: lossless_resourceD intro: subsetD[OF le])


[STATEMENT]
lemma lossless_resource_mono':
  "\<lbrakk> lossless_resource \<I>' res; \<I> \<le> \<I>' \<rbrakk> \<Longrightarrow> lossless_resource \<I> res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lossless_resource \<I>' res; \<I> \<le> \<I>'\<rbrakk> \<Longrightarrow> lossless_resource \<I> res
[PROOF STEP]
by(erule lossless_resource_mono)(simp add: le_\<I>_def)


[STATEMENT]
lemma resource_of_oracle_parametric [transfer_rule]: includes lifting_syntax shows
  "((S ===> A ===> rel_spmf (rel_prod B S)) ===> S ===> rel_resource A B) resource_of_oracle resource_of_oracle"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((S ===> A ===> rel_spmf (rel_prod B S)) ===> S ===> rel_resource A B) resource_of_oracle resource_of_oracle
[PROOF STEP]
unfolding resource_of_oracle_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((S ===> A ===> rel_spmf (rel_prod B S)) ===> S ===> rel_resource A B) (\<lambda>oracle. corec_resource (\<lambda>s a. map_spmf (map_prod id Inr) (oracle s a))) (\<lambda>oracle. corec_resource (\<lambda>s a. map_spmf (map_prod id Inr) (oracle s a)))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma map_resource_resource_of_oracle:
  "map_resource f g (resource_of_oracle oracle s) = resource_of_oracle (map_fun id (map_fun f (map_spmf (map_prod g id))) oracle) s"
  for s :: 's
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_resource f g (resource_of_oracle oracle s) = resource_of_oracle (map_fun id (map_fun f (map_spmf (map_prod g id))) oracle) s
[PROOF STEP]
using resource_of_oracle_parametric[of "BNF_Def.Grp UNIV (id :: 's \<Rightarrow> _)" "conversep (BNF_Def.Grp UNIV f)" "BNF_Def.Grp UNIV g"]
[PROOF STATE]
proof (prove)
using this:
rel_fun (rel_fun (BNF_Def.Grp UNIV id) (rel_fun (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (rel_spmf (rel_prod (BNF_Def.Grp UNIV g) (BNF_Def.Grp UNIV id))))) (rel_fun (BNF_Def.Grp UNIV id) (rel_resource (BNF_Def.Grp UNIV f)\<inverse>\<inverse> (BNF_Def.Grp UNIV g))) resource_of_oracle resource_of_oracle

goal (1 subgoal):
 1. map_resource f g (resource_of_oracle oracle s) = resource_of_oracle (map_fun id (map_fun f (map_spmf (map_prod g id))) oracle) s
[PROOF STEP]
unfolding prod.rel_Grp option.rel_Grp pmf.rel_Grp rel_fun_Grp rel_resource_Grp
[PROOF STATE]
proof (prove)
using this:
rel_fun (rel_fun (BNF_Def.Grp UNIV id) (BNF_Def.Grp {fa. fa ` range f \<subseteq> {x. set_pmf x \<subseteq> {x. set_option x \<subseteq> {x. Basic_BNFs.fsts x \<subseteq> UNIV \<and> Basic_BNFs.snds x \<subseteq> UNIV}}}} (map_fun f (map_spmf (map_prod g id))))) (rel_fun (BNF_Def.Grp UNIV id) (BNF_Def.Grp UNIV (map_resource f g))) resource_of_oracle resource_of_oracle

goal (1 subgoal):
 1. map_resource f g (resource_of_oracle oracle s) = resource_of_oracle (map_fun id (map_fun f (map_spmf (map_prod g id))) oracle) s
[PROOF STEP]
by simp
    (subst (asm) (1 2) eq_alt[symmetric]
      , subst (asm) (1 2) conversep_eq[symmetric]
      , subst (asm) (1 2) eq_alt
      , unfold rel_fun_Grp, simp add: rel_fun_Grp rel_fun_def Grp_iff)


[STATEMENT]
lemma (in callee_invariant_on) lossless_resource_of_oracle:
  assumes *: "\<And>s x. \<lbrakk> x \<in> outs_\<I> \<I>; I s \<rbrakk> \<Longrightarrow> lossless_spmf (callee s x)"
    and "I s"
  shows "lossless_resource \<I> (resource_of_oracle callee s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_resource \<I> (resource_of_oracle callee s)
[PROOF STEP]
using \<open>I s\<close>
[PROOF STATE]
proof (prove)
using this:
I s

goal (1 subgoal):
 1. lossless_resource \<I> (resource_of_oracle callee s)
[PROOF STEP]
by(coinduction arbitrary: s)(auto intro: * dest: callee_invariant)


[STATEMENT]
lemma resource_of_oracle_rprodl: includes lifting_syntax shows
  "resource_of_oracle ((rprodl ---> id ---> map_spmf (map_prod id lprodr)) oracle) ((s1, s2), s3) =
    resource_of_oracle oracle (s1, s2, s3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resource_of_oracle ((rprodl ---> id ---> map_spmf (map_prod id lprodr)) oracle) ((s1, s2), s3) = resource_of_oracle oracle (s1, s2, s3)
[PROOF STEP]
by(rule resource_of_oracle_parametric[of "BNF_Def.Grp UNIV rprodl" "(=)" "(=)", THEN rel_funD, THEN rel_funD, unfolded rel_resource_eq])
    (auto simp add: Grp_iff rel_fun_def spmf_rel_map intro!: rel_spmf_reflI)


[STATEMENT]
lemma resource_of_oracle_extend_state_oracle [simp]:
  "resource_of_oracle (extend_state_oracle oracle) (s', s) = resource_of_oracle oracle s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resource_of_oracle \<dagger>oracle (s', s) = resource_of_oracle oracle s
[PROOF STEP]
by(rule resource_of_oracle_parametric[of "conversep (BNF_Def.Grp UNIV (\<lambda>s. (s', s)))" "(=)" "(=)", THEN rel_funD, THEN rel_funD, unfolded rel_resource_eq])
    (auto simp add: Grp_iff rel_fun_def spmf_rel_map intro!: rel_spmf_reflI)


[STATEMENT]
lemma exec_gpv_resource_of_oracle:
  "exec_gpv run_resource gpv (resource_of_oracle oracle s) = map_spmf (map_prod id (resource_of_oracle oracle)) (exec_gpv oracle gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_gpv run_resource gpv (resource_of_oracle oracle s) = map_spmf (map_prod id (resource_of_oracle oracle)) (exec_gpv oracle gpv s)
[PROOF STEP]
by(subst spmf.map_id[symmetric], fold pmf.rel_eq)
    (rule pmf.map_transfer[THEN rel_funD, THEN rel_funD, rotated]
      , rule exec_gpv_parametric[where S="\<lambda>res s. res = resource_of_oracle oracle s" and CALL="(=)" and A="(=)", THEN rel_funD, THEN rel_funD, THEN rel_funD]
      , auto simp add: gpv.rel_eq rel_fun_def spmf_rel_map elim: option.rel_cases intro!: rel_spmf_reflI)


[STATEMENT]
lemma parallel_resource_parametric [transfer_rule]: includes lifting_syntax shows
  "(rel_resource A B ===> rel_resource C D ===> rel_resource (rel_sum A C) (rel_sum B D))
   parallel_resource parallel_resource"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_resource A B ===> rel_resource C D ===> rel_resource (rel_sum A C) (rel_sum B D)) parallel_resource parallel_resource
[PROOF STEP]
unfolding parallel_resource_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_resource A B ===> rel_resource C D ===> rel_resource (rel_sum A C) (rel_sum B D)) (\<lambda>uu uua. corec_resource (\<lambda>(res1, res2) ac. case ac of Inl a \<Rightarrow> map_spmf (map_prod Inl (\<lambda>uu. Inr (uu, res2))) (run_resource res1 a) | Inr c \<Rightarrow> map_spmf (map_prod Inr (\<lambda>uu. Inr (res1, uu))) (run_resource res2 c)) (uu, uua)) (\<lambda>uu uua. corec_resource (\<lambda>(res1, res2) ac. case ac of Inl a \<Rightarrow> map_spmf (map_prod Inl (\<lambda>uu. Inr (uu, res2))) (run_resource res1 a) | Inr c \<Rightarrow> map_spmf (map_prod Inr (\<lambda>uu. Inr (res1, uu))) (run_resource res2 c)) (uu, uua))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma resource_of_parallel_oracle:
  "resource_of_oracle (parallel_oracle oracle1 oracle2) (s1, s2) =
   parallel_resource (resource_of_oracle oracle1 s1) (resource_of_oracle oracle2 s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resource_of_oracle (parallel_oracle oracle1 oracle2) (s1, s2) = parallel_resource (resource_of_oracle oracle1 s1) (resource_of_oracle oracle2 s2)
[PROOF STEP]
by(coinduction arbitrary: s1 s2)
    (auto 4 3 simp add: rel_fun_def spmf_rel_map split: sum.split intro!: rel_spmf_reflI)


[STATEMENT]
lemma parallel_resource_assoc: \<comment> \<open>There's still an ugly map operation in there to rebalance the interface trees, but well...\<close>
  "parallel_resource (parallel_resource res1 res2) res3 =
   map_resource rsuml lsumr (parallel_resource res1 (parallel_resource res2 res3))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parallel_resource (parallel_resource res1 res2) res3 = map_resource rsuml lsumr (parallel_resource res1 (parallel_resource res2 res3))
[PROOF STEP]
by(coinduction arbitrary: res1 res2 res3)
    (auto 4 5 intro!: rel_funI rel_spmf_reflI simp add: spmf_rel_map split: sum.split)


[STATEMENT]
lemma lossless_parallel_resource:
  assumes "lossless_resource \<I> res1" "lossless_resource \<I>' res2"
  shows "lossless_resource (\<I> \<oplus>\<^sub>\<I> \<I>') (parallel_resource res1 res2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_resource (\<I> \<oplus>\<^sub>\<I> \<I>') (parallel_resource res1 res2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lossless_resource \<I> res1
lossless_resource \<I>' res2

goal (1 subgoal):
 1. lossless_resource (\<I> \<oplus>\<^sub>\<I> \<I>') (parallel_resource res1 res2)
[PROOF STEP]
by(coinduction arbitrary: res1 res2)(clarsimp; erule PlusE; simp; frule (1) lossless_resourceD; auto 4 3)


[STATEMENT]
lemma WT_resource_coinduct [consumes 1, case_names WT_resource, case_conclusion WT_resource response WT_resource, coinduct pred: WT_resource]:
  assumes "X res"
    and "\<And>res q r res'. \<lbrakk> X res; q \<in> outs_\<I> \<I>; (r, res') \<in> set_spmf (run_resource res q) \<rbrakk>
       \<Longrightarrow> r \<in> responses_\<I> \<I> q \<and> (X res' \<or> \<I> \<turnstile>res res' \<surd>)"
  shows "\<I> \<turnstile>res res \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<turnstile>res res \<surd>
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
X res

goal (1 subgoal):
 1. \<I> \<turnstile>res res \<surd>
[PROOF STEP]
by(rule WT_resource.coinduct)(blast dest: assms(2))


[STATEMENT]
lemma WT_resourceD:
  assumes "\<I> \<turnstile>res res \<surd>" "q \<in> outs_\<I> \<I>" "(r, res') \<in> set_spmf (run_resource res q)"
  shows "r \<in> responses_\<I> \<I> q \<and> \<I> \<turnstile>res res' \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> responses_\<I> \<I> q \<and> \<I> \<turnstile>res res' \<surd>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<I> \<turnstile>res res \<surd>
q \<in> outs_\<I> \<I>
(r, res') \<in> set_spmf (run_resource res q)

goal (1 subgoal):
 1. r \<in> responses_\<I> \<I> q \<and> \<I> \<turnstile>res res' \<surd>
[PROOF STEP]
by(auto elim: WT_resource.cases)


[STATEMENT]
lemma WT_resource_of_oracle [simp]:
  assumes "\<And>s. \<I> \<turnstile>c oracle s \<surd>"
  shows "\<I> \<turnstile>res resource_of_oracle oracle s \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<turnstile>res resource_of_oracle oracle s \<surd>
[PROOF STEP]
by(coinduction arbitrary: s)(auto dest: WT_calleeD[OF assms])


[STATEMENT]
lemma WT_resource_bot [simp]: "bot \<turnstile>res res \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> \<turnstile>res res \<surd>
[PROOF STEP]
by(rule WT_resource.intros)auto


[STATEMENT]
lemma WT_resource_full: "\<I>_full \<turnstile>res res \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>_full \<turnstile>res res \<surd>
[PROOF STEP]
by(coinduction arbitrary: res)(auto)


[STATEMENT]
lemma (in callee_invariant_on) WT_resource_of_oracle:
  "I s \<Longrightarrow> \<I> \<turnstile>res resource_of_oracle callee s \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I s \<Longrightarrow> \<I> \<turnstile>res resource_of_oracle callee s \<surd>
[PROOF STEP]
by(coinduction arbitrary: s)(auto dest: callee_invariant')


[STATEMENT]
lemma WT_parallel_resource [WT_intro]:
  assumes "\<I>1 \<turnstile>res res1 \<surd>"
    and "\<I>2 \<turnstile>res res2 \<surd>"
  shows "\<I>1 \<oplus>\<^sub>\<I> \<I>2 \<turnstile>res parallel_resource res1 res2 \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> \<I>2 \<turnstile>res parallel_resource res1 res2 \<surd>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<I>1 \<turnstile>res res1 \<surd>
\<I>2 \<turnstile>res res2 \<surd>

goal (1 subgoal):
 1. \<I>1 \<oplus>\<^sub>\<I> \<I>2 \<turnstile>res parallel_resource res1 res2 \<surd>
[PROOF STEP]
by(coinduction arbitrary: res1 res2)(auto 4 4 intro!: imageI dest: WT_resourceD)


[STATEMENT]
lemma callee_invariant_run_resource: "callee_invariant_on run_resource (\<lambda>res.  \<I> \<turnstile>res res \<surd>) \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. callee_invariant_on run_resource (WT_resource \<I>) \<I>
[PROOF STEP]
by(unfold_locales)(auto dest: WT_resourceD intro: WT_calleeI)


[STATEMENT]
lemma callee_invariant_run_lossless_resource:
  "callee_invariant_on run_resource (\<lambda>res. lossless_resource \<I> res \<and> \<I> \<turnstile>res res \<surd>) \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. callee_invariant_on run_resource (\<lambda>res. lossless_resource \<I> res \<and> \<I> \<turnstile>res res \<surd>) \<I>
[PROOF STEP]
by(unfold_locales)(auto dest: WT_resourceD lossless_resourceD intro: WT_calleeI)


[STATEMENT]
lemma [simp]: "validTrans aid trn \<Longrightarrow> lreach aid (srcOf trn) \<Longrightarrow> \<phi> aid trn \<Longrightarrow> comOf aid trn = Internal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); \<phi> aid trn\<rbrakk> \<Longrightarrow> comOf aid trn = Internal
[PROOF STEP]
by (cases trn) (auto elim: Issuer.\<phi>E)


[STATEMENT]
theorem secure: "secure"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure
[PROOF STEP]
proof (intro preserve_source_secure ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
fix aid
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
assume "aid \<in> AIDs - {AID}"
[PROOF STATE]
proof (state)
this:
aid \<in> nodes'

goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
aid \<in> nodes'
[PROOF STEP]
show "Net.lsecure aid"
[PROOF STATE]
proof (prove)
using this:
aid \<in> nodes'

goal (1 subgoal):
 1. Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV aid) (Net.lO aid) (B aid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
by (intro Abstract_BD_Security.B_id_secure) (auto simp: B_id_def)
[PROOF STATE]
proof (state)
this:
Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV aid) (Net.lO aid) (B aid) (BD_Security_IO.never (\<lambda>a. False))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma size_eq_card_implies_surj_on:
  assumes "finite A" "finite B"
  assumes "size N = card B"
  assumes "f \<in> functions_of A B N"
  shows   "f ` A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
from \<open>f \<in> functions_of A B N\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in> Twelvefold_Way_Entry10.functions_of A B N
[PROOF STEP]
have "f \<in> A \<rightarrow>\<^sub>E B" and
    "N = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))"
[PROOF STATE]
proof (prove)
using this:
f \<in> Twelvefold_Way_Entry10.functions_of A B N

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B &&& N = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))
[PROOF STEP]
unfolding functions_of_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})) = N}

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B &&& N = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
N = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
from this \<open>size N = card B\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E B
N = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))
size N = card B
[PROOF STEP]
have "card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E B
N = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))
size N = card B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
from this \<open>finite B\<close> \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (chain)
picking this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
finite B
f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
show "f ` A = B"
[PROOF STATE]
proof (prove)
using this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
finite B
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
using card_eq_implies_surjective_on
[PROOF STATE]
proof (prove)
using this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
finite B
f \<in> A \<rightarrow>\<^sub>E B
\<lbrakk>finite ?B; ?f \<in> ?A \<rightarrow>\<^sub>E ?B; card ((\<lambda>b. {x \<in> ?A. ?f x = b}) ` ?B - {{}}) = card ?B\<rbrakk> \<Longrightarrow> ?f ` ?A = ?B

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f ` A = B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma surj_on_implies_size_eq_card:
  assumes "finite A" "finite B"
  assumes "F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B"
  assumes "univ (\<lambda>f. f ` A = B) F"
  shows "size (number_partition_of A B F) = card B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
from \<open>F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B\<close>
[PROOF STATE]
proof (chain)
picking this:
F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B
[PROOF STEP]
obtain f where "f \<in> A \<rightarrow>\<^sub>E B"
    and F_eq: "F = domain_and_range_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = domain_and_range_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using quotientE
[PROOF STATE]
proof (prove)
using this:
F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B
\<lbrakk>?X \<in> ?A // ?r; \<And>x. \<lbrakk>?X = ?r `` {x}; x \<in> ?A\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E B; F = domain_and_range_permutation A B `` {f}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B
F = domain_and_range_permutation A B `` {f}

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
have "number_partition_of A B F = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. number_partition_of A B F = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F
[PROOF STEP]
unfolding number_partition_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
number_partition_of A B F = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
number_partition_of A B F = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
have "\<dots> =  univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})
[PROOF STEP]
unfolding F_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f}) = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) F = univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
have "\<dots> = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f}) = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))
[PROOF STEP]
using \<open>finite B\<close> equiv_domain_and_range_permutation multiset_of_partition_cards_respects_domain_and_range_permutation \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (prove)
using this:
finite B
equiv (?A \<rightarrow>\<^sub>E ?B) (domain_and_range_permutation ?A ?B)
finite ?B \<Longrightarrow> (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> ?A. f x = b}) ` ?B - {{}}))) respects domain_and_range_permutation ?A ?B
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f}) = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))
[PROOF STEP]
by (subst univ_commute') auto
[PROOF STATE]
proof (state)
this:
univ (\<lambda>f. image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f}) = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
number_partition_of A B F = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))
[PROOF STEP]
have eq: "number_partition_of A B F = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))"
[PROOF STATE]
proof (prove)
using this:
number_partition_of A B F = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))

goal (1 subgoal):
 1. number_partition_of A B F = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
number_partition_of A B F = image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
from iffD1[OF univ_commute', OF equiv_domain_and_range_permutation, OF surjective_respects_domain_and_range_permutation, OF \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>]
    assms(4)
[PROOF STATE]
proof (chain)
picking this:
univ (\<lambda>f. f ` A = B) (domain_and_range_permutation A B `` {f}) \<Longrightarrow> f ` A = B
univ (\<lambda>f. f ` A = B) F
[PROOF STEP]
have "f ` A = B"
[PROOF STATE]
proof (prove)
using this:
univ (\<lambda>f. f ` A = B) (domain_and_range_permutation A B `` {f}) \<Longrightarrow> f ` A = B
univ (\<lambda>f. f ` A = B) F

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
by (simp add: F_eq)
[PROOF STATE]
proof (state)
this:
f ` A = B

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
have "size (number_partition_of A B F) = size (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (number_partition_of A B F) = size (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})))
[PROOF STEP]
unfolding eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) = size (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
size (number_partition_of A B F) = size (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})))

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
size (number_partition_of A B F) = size (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})))

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
have "\<dots> = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
size (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
size (image_mset card (mset_set ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}))) = card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}})

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
from \<open>f ` A = B\<close>
[PROOF STATE]
proof (chain)
picking this:
f ` A = B
[PROOF STEP]
have "\<dots> = card B"
[PROOF STATE]
proof (prove)
using this:
f ` A = B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
using surjective_on_implies_card_eq
[PROOF STATE]
proof (prove)
using this:
f ` A = B
?f ` ?A = ?B \<Longrightarrow> card ((\<lambda>b. {x \<in> ?A. ?f x = b}) ` ?B - {{}}) = card ?B

goal (1 subgoal):
 1. card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card ((\<lambda>b. {x \<in> A. f x = b}) ` B - {{}}) = card B

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
size (number_partition_of A B F) = card B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
size (number_partition_of A B F) = card B

goal (1 subgoal):
 1. size (number_partition_of A B F) = card B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
size (number_partition_of A B F) = card B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma functions_of_is_surj_on:
  assumes "finite A" "finite B"
  assumes "number_partition (card A) N" "size N = card B"
  shows "univ (\<lambda>f. f ` A = B) (functions_of A B N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (Twelvefold_Way_Entry10.functions_of A B N)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (Twelvefold_Way_Entry10.functions_of A B N)
[PROOF STEP]
have "functions_of A B N \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Twelvefold_Way_Entry10.functions_of A B N \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B
[PROOF STEP]
using functions_of \<open>finite A\<close> \<open>finite B\<close> \<open>number_partition (card A) N \<close> \<open>size N = card B\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; finite ?B; number_partition (card ?A) ?N; size ?N \<le> card ?B\<rbrakk> \<Longrightarrow> Twelvefold_Way_Entry10.functions_of ?A ?B ?N \<in> (?A \<rightarrow>\<^sub>E ?B) // domain_and_range_permutation ?A ?B
finite A
finite B
number_partition (card A) N
size N = card B

goal (1 subgoal):
 1. Twelvefold_Way_Entry10.functions_of A B N \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Twelvefold_Way_Entry10.functions_of A B N \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (Twelvefold_Way_Entry10.functions_of A B N)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
Twelvefold_Way_Entry10.functions_of A B N \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B
[PROOF STEP]
obtain f where eq_f: "functions_of A B N = domain_and_range_permutation A B `` {f}" and "f \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
Twelvefold_Way_Entry10.functions_of A B N \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>Twelvefold_Way_Entry10.functions_of A B N = domain_and_range_permutation A B `` {f}; f \<in> A \<rightarrow>\<^sub>E B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using quotientE
[PROOF STATE]
proof (prove)
using this:
Twelvefold_Way_Entry10.functions_of A B N \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B
\<lbrakk>?X \<in> ?A // ?r; \<And>x. \<lbrakk>?X = ?r `` {x}; x \<in> ?A\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>Twelvefold_Way_Entry10.functions_of A B N = domain_and_range_permutation A B `` {f}; f \<in> A \<rightarrow>\<^sub>E B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Twelvefold_Way_Entry10.functions_of A B N = domain_and_range_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (Twelvefold_Way_Entry10.functions_of A B N)
[PROOF STEP]
from eq_f
[PROOF STATE]
proof (chain)
picking this:
Twelvefold_Way_Entry10.functions_of A B N = domain_and_range_permutation A B `` {f}
[PROOF STEP]
have "f \<in> functions_of A B N"
[PROOF STATE]
proof (prove)
using this:
Twelvefold_Way_Entry10.functions_of A B N = domain_and_range_permutation A B `` {f}

goal (1 subgoal):
 1. f \<in> Twelvefold_Way_Entry10.functions_of A B N
[PROOF STEP]
using \<open>f \<in> A \<rightarrow>\<^sub>E B\<close> equiv_domain_and_range_permutation equiv_class_self
[PROOF STATE]
proof (prove)
using this:
Twelvefold_Way_Entry10.functions_of A B N = domain_and_range_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B
equiv (?A \<rightarrow>\<^sub>E ?B) (domain_and_range_permutation ?A ?B)
\<lbrakk>equiv ?A ?r; ?a \<in> ?A\<rbrakk> \<Longrightarrow> ?a \<in> ?r `` {?a}

goal (1 subgoal):
 1. f \<in> Twelvefold_Way_Entry10.functions_of A B N
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f \<in> Twelvefold_Way_Entry10.functions_of A B N

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (Twelvefold_Way_Entry10.functions_of A B N)
[PROOF STEP]
have "f ` A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
using \<open>f \<in> functions_of A B N\<close> assms size_eq_card_implies_surj_on
[PROOF STATE]
proof (prove)
using this:
f \<in> Twelvefold_Way_Entry10.functions_of A B N
finite A
finite B
number_partition (card A) N
size N = card B
\<lbrakk>finite ?A; finite ?B; size ?N = card ?B; ?f \<in> Twelvefold_Way_Entry10.functions_of ?A ?B ?N\<rbrakk> \<Longrightarrow> ?f ` ?A = ?B

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f ` A = B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (Twelvefold_Way_Entry10.functions_of A B N)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f ` A = B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f ` A = B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (Twelvefold_Way_Entry10.functions_of A B N)
[PROOF STEP]
unfolding eq_f
[PROOF STATE]
proof (prove)
using this:
f ` A = B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (domain_and_range_permutation A B `` {f})
[PROOF STEP]
using equiv_domain_and_range_permutation surjective_respects_domain_and_range_permutation \<open>f \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (prove)
using this:
f ` A = B
equiv (?A \<rightarrow>\<^sub>E ?B) (domain_and_range_permutation ?A ?B)
(\<lambda>f. f ` ?A = ?B) respects domain_and_range_permutation ?A ?B
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A = B) (domain_and_range_permutation A B `` {f})
[PROOF STEP]
by (subst univ_commute') assumption+
[PROOF STATE]
proof (state)
this:
univ (\<lambda>f. f ` A = B) (Twelvefold_Way_Entry10.functions_of A B N)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_number_partition_of:
   assumes "finite A" "finite B"
  shows "bij_betw (number_partition_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) {N. number_partition (card A) N \<and> size N = card B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (number_partition_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
proof (rule bij_betw_byWitness[where f'="functions_of A B"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>a\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B. Twelvefold_Way_Entry10.functions_of A B (number_partition_of A B a) = a
 2. \<forall>a'\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B a') = a'
 3. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
 4. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
[PROOF STEP]
have quotient_eq: "{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B = {F \<in> ((A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B). univ (\<lambda>f. f ` A = B) F}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. univ (\<lambda>f. f ` A = B) F}
[PROOF STEP]
using equiv_domain_and_range_permutation[of A B] surjective_respects_domain_and_range_permutation[of A B]
[PROOF STATE]
proof (prove)
using this:
equiv (A \<rightarrow>\<^sub>E B) (domain_and_range_permutation A B)
(\<lambda>f. f ` A = B) respects domain_and_range_permutation A B

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. univ (\<lambda>f. f ` A = B) F}
[PROOF STEP]
by (simp only: univ_preserves_predicate)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. univ (\<lambda>f. f ` A = B) F}

goal (4 subgoals):
 1. \<forall>a\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B. Twelvefold_Way_Entry10.functions_of A B (number_partition_of A B a) = a
 2. \<forall>a'\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B a') = a'
 3. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
 4. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
[PROOF STEP]
show "\<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B.
       functions_of A B (number_partition_of A B F) = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B. Twelvefold_Way_Entry10.functions_of A B (number_partition_of A B F) = F
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. \<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B. Twelvefold_Way_Entry10.functions_of A B (number_partition_of A B F) = F
[PROOF STEP]
by (auto simp only: quotient_eq functions_of_number_partition_of)
[PROOF STATE]
proof (state)
this:
\<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B. Twelvefold_Way_Entry10.functions_of A B (number_partition_of A B F) = F

goal (3 subgoals):
 1. \<forall>a'\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B a') = a'
 2. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
 3. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
[PROOF STEP]
show "\<forall>N\<in>{N. number_partition (card A) N  \<and> size N = card B}. number_partition_of A B (functions_of A B N) = N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>N\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B N) = N
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. \<forall>N\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B N) = N
[PROOF STEP]
by (simp add: number_partition_of_functions_of)
[PROOF STATE]
proof (state)
this:
\<forall>N\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B N) = N

goal (2 subgoals):
 1. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
 2. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
[PROOF STEP]
show "number_partition_of A B ` ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B)
    \<subseteq> {N. number_partition (card A) N  \<and> size N = card B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
by (auto simp add: quotient_eq number_partition_of surj_on_implies_size_eq_card)
[PROOF STATE]
proof (state)
this:
number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}

goal (1 subgoal):
 1. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
[PROOF STEP]
show "functions_of A B ` {N. number_partition (card A) N \<and> size N = card B}
    \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
[PROOF STEP]
by (auto simp add: quotient_eq intro: functions_of functions_of_is_surj_on)
[PROOF STATE]
proof (state)
this:
Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_functions_of:
   assumes "finite A" "finite B"
  shows "bij_betw (functions_of A B) {N. number_partition (card A) N \<and> size N = card B} ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (Twelvefold_Way_Entry10.functions_of A B) {N. number_partition (card A) N \<and> size N = card B} ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B)
[PROOF STEP]
proof (rule bij_betw_byWitness[where f'="number_partition_of A B"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>a\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B a) = a
 2. \<forall>a'\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B. Twelvefold_Way_Entry10.functions_of A B (number_partition_of A B a') = a'
 3. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
 4. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
have quotient_eq: "{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B = {F \<in> ((A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B). univ (\<lambda>f. f ` A = B) F}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. univ (\<lambda>f. f ` A = B) F}
[PROOF STEP]
using equiv_domain_and_range_permutation[of A B] surjective_respects_domain_and_range_permutation[of A B]
[PROOF STATE]
proof (prove)
using this:
equiv (A \<rightarrow>\<^sub>E B) (domain_and_range_permutation A B)
(\<lambda>f. f ` A = B) respects domain_and_range_permutation A B

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. univ (\<lambda>f. f ` A = B) F}
[PROOF STEP]
by (simp only: univ_preserves_predicate)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B = {F \<in> (A \<rightarrow>\<^sub>E B) // domain_and_range_permutation A B. univ (\<lambda>f. f ` A = B) F}

goal (4 subgoals):
 1. \<forall>a\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B a) = a
 2. \<forall>a'\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B. Twelvefold_Way_Entry10.functions_of A B (number_partition_of A B a') = a'
 3. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
 4. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
show "\<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B.
       functions_of A B (number_partition_of A B F) = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B. Twelvefold_Way_Entry10.functions_of A B (number_partition_of A B F) = F
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. \<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B. Twelvefold_Way_Entry10.functions_of A B (number_partition_of A B F) = F
[PROOF STEP]
by (auto simp only: quotient_eq functions_of_number_partition_of)
[PROOF STATE]
proof (state)
this:
\<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B. Twelvefold_Way_Entry10.functions_of A B (number_partition_of A B F) = F

goal (3 subgoals):
 1. \<forall>a\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B a) = a
 2. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
 3. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
show "\<forall>N\<in>{N. number_partition (card A) N  \<and> size N = card B}. number_partition_of A B (functions_of A B N) = N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>N\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B N) = N
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. \<forall>N\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B N) = N
[PROOF STEP]
by (simp add: number_partition_of_functions_of)
[PROOF STATE]
proof (state)
this:
\<forall>N\<in>{N. number_partition (card A) N \<and> size N = card B}. number_partition_of A B (Twelvefold_Way_Entry10.functions_of A B N) = N

goal (2 subgoals):
 1. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
 2. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
show "number_partition_of A B ` ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B)
    \<subseteq> {N. number_partition (card A) N  \<and> size N = card B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
by (auto simp add: quotient_eq number_partition_of surj_on_implies_size_eq_card)
[PROOF STATE]
proof (state)
this:
number_partition_of A B ` {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B \<subseteq> {N. number_partition (card A) N \<and> size N = card B}

goal (1 subgoal):
 1. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
[PROOF STEP]
show "functions_of A B ` {N. number_partition (card A) N \<and> size N = card B}
    \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B
[PROOF STEP]
by (auto simp add: quotient_eq intro: functions_of functions_of_is_surj_on)
[PROOF STATE]
proof (state)
this:
Twelvefold_Way_Entry10.functions_of A B ` {N. number_partition (card A) N \<and> size N = card B} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_surjective_functions_domain_and_range_permutation:
  assumes "finite A" "finite B"
  shows "card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)
[PROOF STEP]
have "bij_betw (number_partition_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) {N. number_partition (card A) N \<and> size N = card B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (number_partition_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. bij_betw (number_partition_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
by (rule bij_betw_number_partition_of)
[PROOF STATE]
proof (state)
this:
bij_betw (number_partition_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) {N. number_partition (card A) N \<and> size N = card B}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
bij_betw (number_partition_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
have "card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = card {N. number_partition (card A) N \<and> size N = card B}"
[PROOF STATE]
proof (prove)
using this:
bij_betw (number_partition_of A B) ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) {N. number_partition (card A) N \<and> size N = card B}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = card {N. number_partition (card A) N \<and> size N = card B}
[PROOF STEP]
by (rule bij_betw_same_card)
[PROOF STATE]
proof (state)
this:
card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = card {N. number_partition (card A) N \<and> size N = card B}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = card {N. number_partition (card A) N \<and> size N = card B}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)
[PROOF STEP]
have "card {N. number_partition (card A) N \<and> size N = card B} = Partition (card A) (card B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {N. number_partition (card A) N \<and> size N = card B} = Partition (card A) (card B)
[PROOF STEP]
by (rule card_partitions_with_k_parts)
[PROOF STATE]
proof (state)
this:
card {N. number_partition (card A) N \<and> size N = card B} = Partition (card A) (card B)

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card ({f \<in> A \<rightarrow>\<^sub>E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_fm_Equality_axP [simp]: "eval_fm e (Equality_axP x) \<longleftrightarrow> \<lbrakk>x\<rbrakk>e \<in> Equality_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fm e (Equality_axP x) = (\<lbrakk>x\<rbrakk>e \<in> Equality_ax)
[PROOF STEP]
by (auto simp: Equality_ax_def intro: eval_quot_fm_ignore)


[STATEMENT]
lemma eval_fm_HF_axP [simp]: "eval_fm e (HF_axP x) \<longleftrightarrow> \<lbrakk>x\<rbrakk>e \<in> HF_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fm e (HF_axP x) = (\<lbrakk>x\<rbrakk>e \<in> HF_ax)
[PROOF STEP]
by (auto simp: HF_ax_def intro: eval_quot_fm_ignore)


[STATEMENT]
lemma HF_axP_sf [iff]: "Sigma_fm (HF_axP t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_fm (HF_axP t)
[PROOF STEP]
by auto