[STATEMENT]
lemma wf_md'E:
  "\<lbrakk> wf_prog wf_md P;
     \<And>C S fs ms m.\<lbrakk>(C,S,fs,ms) \<in> set P; m \<in> set ms\<rbrakk> \<Longrightarrow> wf_md' P C m \<rbrakk>
  \<Longrightarrow> wf_prog wf_md' P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; \<And>C S fs ms m. \<lbrakk>(C, S, fs, ms) \<in> set P; m \<in> set ms\<rbrakk> \<Longrightarrow> wf_md' P C m\<rbrakk> \<Longrightarrow> wf_prog wf_md' P
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog wf_md P; \<And>C S fs ms m. \<lbrakk>(C, S, fs, ms) \<in> set P; m \<in> set ms\<rbrakk> \<Longrightarrow> wf_md' P C m\<rbrakk> \<Longrightarrow> wf_prog wf_md' P
[PROOF STEP]
apply (simp add: wf_prog_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_syscls P \<and> (\<forall>c\<in>set P. wf_cdecl wf_md P c) \<and> distinct_fst P; \<And>C S fs ms m. \<lbrakk>(C, S, fs, ms) \<in> set P; m \<in> set ms\<rbrakk> \<Longrightarrow> wf_md' P C m\<rbrakk> \<Longrightarrow> Ball (set P) (wf_cdecl wf_md' P)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b. \<lbrakk>\<And>C S fs ms a aa ab b. \<lbrakk>(C, S, fs, ms) \<in> set P; (a, aa, ab, b) \<in> set ms\<rbrakk> \<Longrightarrow> wf_md' P C (a, aa, ab, b); (a, aa, ab, b) \<in> set P; wf_syscls P; \<forall>x\<in>set P. wf_cdecl wf_md P x; distinct_fst P\<rbrakk> \<Longrightarrow> wf_cdecl wf_md' P (a, aa, ab, b)
[PROOF STEP]
apply (simp add: wf_cdecl_def wf_mdecl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab b. \<lbrakk>\<And>C S fs ms a aa ab b. \<lbrakk>(C, S, fs, ms) \<in> set P; (a, aa, ab, b) \<in> set ms\<rbrakk> \<Longrightarrow> wf_md' P C (a, aa, ab, b); (a, aa, ab, b) \<in> set P; wf_syscls P; \<forall>x\<in>set P. case x of (C, D, fs, ms) \<Rightarrow> (\<forall>f\<in>set fs. wf_fdecl P f) \<and> distinct_fst fs \<and> (\<forall>m\<in>set ms. case m of (M, Ts, ab) \<Rightarrow> Ball (set Ts) (is_type P) \<and> (case ab of (T, mb) \<Rightarrow> is_type P T \<and> wf_md P C (M, Ts, T, mb))) \<and> distinct_fst ms \<and> (C \<noteq> Object \<longrightarrow> (\<exists>a aa b. class P D = \<lfloor>(a, aa, b)\<rfloor>) \<and> (D, C) \<notin> (subcls1 P)\<^sup>* \<and> (\<forall>x\<in>set ms. case x of (M, Ts, T, m) \<Rightarrow> \<forall>D' Ts' T'. (\<exists>m'. P \<turnstile> D sees M: Ts'\<rightarrow>T' = m' in D') \<longrightarrow> P \<turnstile> Ts' [\<le>] Ts \<and> subtype P T T')); distinct_fst P\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set ab. wf_fdecl P x) \<and> distinct_fst ab \<and> (\<forall>x\<in>set b. case x of (M, Ts, ab) \<Rightarrow> (\<forall>x\<in>set Ts. is_type P x) \<and> (case ab of (T, mb) \<Rightarrow> is_type P T \<and> wf_md' P a (M, Ts, T, mb))) \<and> distinct_fst b \<and> (a \<noteq> Object \<longrightarrow> (\<exists>a ab b. class P aa = \<lfloor>(a, ab, b)\<rfloor>) \<and> (aa, a) \<notin> (subcls1 P)\<^sup>* \<and> (\<forall>x\<in>set b. case x of (M, Ts, T, m) \<Rightarrow> \<forall>D' Ts' T'. (\<exists>m'. P \<turnstile> aa sees M: Ts'\<rightarrow>T' = m' in D') \<longrightarrow> P \<turnstile> Ts' [\<le>] Ts \<and> subtype P T T'))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_prog:
  "wf_jvm_prog\<^bsub>\<Phi>\<^esub> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_jvm_prog\<^bsub>\<Phi>\<^esub> E
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_jvm_prog\<^bsub>\<Phi>\<^esub> E
[PROOF STEP]
apply (unfold wf_jvm_prog_phi_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) E
[PROOF STEP]
apply (rule wf_md'E [OF wf_struct])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C S fs ms m. \<lbrakk>(C, S, fs, ms) \<in> set E; m \<in> set ms\<rbrakk> \<Longrightarrow> case m of (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method E C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)
[PROOF STEP]
apply (simp add: E_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C S fs ms m. \<lbrakk>C = list_name \<and> (S, fs, ms) = list_class \<or> C = test_name \<and> (S, fs, ms) = test_class \<or> (C, S, fs, ms) \<in> set SystemClasses; m \<in> set ms\<rbrakk> \<Longrightarrow> case m of (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt) \<Rightarrow> wt_method (SystemClasses @ [(list_name, list_class), (test_name, test_class)]) C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C S fs ms a aa ab ac ad ae b. \<lbrakk>C = list_name \<and> (S, fs, ms) = list_class \<or> C = test_name \<and> (S, fs, ms) = test_class \<or> (C, S, fs, ms) \<in> set SystemClasses; (a, aa, ab, ac, ad, ae, b) \<in> set ms\<rbrakk> \<Longrightarrow> wt_method (SystemClasses @ [(list_name, list_class), (test_name, test_class)]) C aa ab ac ad ae b (\<Phi> C a)
[PROOF STEP]
apply (fold E_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C S fs ms a aa ab ac ad ae b. \<lbrakk>C = list_name \<and> (S, fs, ms) = list_class \<or> C = test_name \<and> (S, fs, ms) = test_class \<or> (C, S, fs, ms) \<in> set SystemClasses; (a, aa, ab, ac, ad, ae, b) \<in> set ms\<rbrakk> \<Longrightarrow> wt_method E C aa ab ac ad ae b (\<Phi> C a)
[PROOF STEP]
apply (simp add: system_defs class_defs Phi_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C S fs ms a aa ab ac ad ae b. \<lbrakk>C = list_name \<and> S = Object \<and> fs = [(val_name, Integer), (next_name, Clist)] \<and> ms = [(append_name, [Clist], Void, 3, 0, append_ins, [(Suc 0, 2, NullPointer, 7, 0)])] \<or> C = test_name \<and> S = Object \<and> fs = [] \<and> ms = [(makelist_name, [], Void, 3, 2, make_list_ins, [])] \<or> C = Object \<and> S = undefined \<and> fs = [] \<and> ms = [] \<or> C = NullPointer \<and> S = Object \<and> fs = [] \<and> ms = [] \<or> C = ClassCast \<and> S = Object \<and> fs = [] \<and> ms = [] \<or> C = OutOfMemory \<and> S = Object \<and> fs = [] \<and> ms = []; (a, aa, ab, ac, ad, ae, b) \<in> set ms\<rbrakk> \<Longrightarrow> (C = list_name \<and> a = append_name \<longrightarrow> (list_name = test_name \<and> append_name = makelist_name \<longrightarrow> wt_method E test_name aa ab ac ad ae b \<phi>\<^sub>m) \<and> ((list_name = test_name \<longrightarrow> append_name \<noteq> makelist_name) \<longrightarrow> wt_method E list_name aa ab ac ad ae b \<phi>\<^sub>a)) \<and> ((C = list_name \<longrightarrow> a \<noteq> append_name) \<longrightarrow> (C = test_name \<and> a = makelist_name \<longrightarrow> wt_method E test_name aa ab ac ad ae b \<phi>\<^sub>m) \<and> ((C = test_name \<longrightarrow> a \<noteq> makelist_name) \<longrightarrow> wt_method E C aa ab ac ad ae b []))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_name = test_name; append_name = makelist_name\<rbrakk> \<Longrightarrow> wt_method E test_name [Ctest] Void 3 0 append_ins [(Suc 0, 2, NullPointer, 7, 0)] \<phi>\<^sub>m
[PROOF STEP]
apply (simp add: distinct_classes)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "E,\<Phi> \<turnstile> start_state E test_name makelist_name \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E,\<Phi> |- start_state E test_name makelist_name [ok]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E,\<Phi> |- start_state E test_name makelist_name [ok]
[PROOF STEP]
apply (rule BV_correct_initial)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf_jvm_prog\<^bsub>\<Phi>\<^esub> E
 2. E \<turnstile> test_name sees makelist_name: []\<rightarrow>?T = ?m in test_name
[PROOF STEP]
apply (rule wf_prog)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<turnstile> test_name sees makelist_name: []\<rightarrow>?T = ?m in test_name
[PROOF STEP]
apply (fastforce simp add: test_class_def distinct_classes Method_def intro: Methods.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code]:
  "unstables r step ss =
   fold (\<lambda>p A. if \<not>stable r step ss p then insert p A else A) [0..<size ss] {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
have "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unstables r step ss = (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {})
[PROOF STEP]
apply (unfold unstables_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p} = (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {})
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p} \<subseteq> (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {})
 2. (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {}) \<subseteq> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p} \<Longrightarrow> x \<in> (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {})
 2. (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {}) \<subseteq> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p}
[PROOF STEP]
apply (erule CollectE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x < length ss \<and> \<not> Typing_Framework_1.stable r step ss x \<Longrightarrow> x \<in> (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {})
 2. (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {}) \<subseteq> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p}
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x < length ss; \<not> Typing_Framework_1.stable r step ss x\<rbrakk> \<Longrightarrow> x \<in> (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {})
 2. (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {}) \<subseteq> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p}
[PROOF STEP]
apply (rule UN_I)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x < length ss; \<not> Typing_Framework_1.stable r step ss x\<rbrakk> \<Longrightarrow> ?a9 x \<in> {..<length ss}
 2. \<And>x. \<lbrakk>x < length ss; \<not> Typing_Framework_1.stable r step ss x\<rbrakk> \<Longrightarrow> x \<in> (if \<not> Typing_Framework_1.stable r step ss (?a9 x) then {?a9 x} else {})
 3. (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {}) \<subseteq> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x < length ss; \<not> Typing_Framework_1.stable r step ss x\<rbrakk> \<Longrightarrow> x \<in> (if \<not> Typing_Framework_1.stable r step ss x then {x} else {})
 2. (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {}) \<subseteq> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {}) \<subseteq> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {}) \<Longrightarrow> x \<in> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p}
[PROOF STEP]
apply (erule UN_E)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x p. \<lbrakk>p \<in> {..<length ss}; x \<in> (if \<not> Typing_Framework_1.stable r step ss p then {p} else {})\<rbrakk> \<Longrightarrow> x \<in> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p}
[PROOF STEP]
apply (case_tac "\<not> stable r step ss p")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x p. \<lbrakk>p \<in> {..<length ss}; x \<in> (if \<not> Typing_Framework_1.stable r step ss p then {p} else {}); \<not> Typing_Framework_1.stable r step ss p\<rbrakk> \<Longrightarrow> x \<in> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p}
 2. \<And>x p. \<lbrakk>p \<in> {..<length ss}; x \<in> (if \<not> Typing_Framework_1.stable r step ss p then {p} else {}); \<not> \<not> Typing_Framework_1.stable r step ss p\<rbrakk> \<Longrightarrow> x \<in> {p. p < length ss \<and> \<not> Typing_Framework_1.stable r step ss p}
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unstables r step ss = (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {})

goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
unstables r step ss = (\<Union>p<length ss. if \<not> Typing_Framework_1.stable r step ss p then {p} else {})

goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<Union> (f ` {..<length ss}) = \<Union> (set (map f [0..<length ss]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (?f ` {..<length ss}) = \<Union> (set (map ?f [0..<length ss]))

goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Union> (?f ` {..<length ss}) = \<Union> (set (map ?f [0..<length ss]))

goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
note Sup_set_fold
[PROOF STATE]
proof (state)
this:
Sup (set ?xs) = fold sup_class.sup ?xs bot

goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Sup (set ?xs) = fold sup_class.sup ?xs bot

goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
note fold_map
[PROOF STATE]
proof (state)
this:
fold ?g (map ?f ?xs) = fold (?g \<circ> ?f) ?xs

goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fold ?g (map ?f ?xs) = fold (?g \<circ> ?f) ?xs

goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
have "(\<union>) \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) =
            (\<lambda>p A. if \<not>stable r step ss p then insert p A else A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<union>) \<circ> (\<lambda>p. if \<not> Typing_Framework_1.stable r step ss p then {p} else {}) = (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A)
[PROOF STEP]
by(auto simp add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
(\<union>) \<circ> (\<lambda>p. if \<not> Typing_Framework_1.stable r step ss p then {p} else {}) = (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A)

goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
unstables r step ss = fold (\<lambda>a b. if \<not> Typing_Framework_1.stable r step ss a then insert a b else b) [0..<length ss] {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
unstables r step ss = fold (\<lambda>a b. if \<not> Typing_Framework_1.stable r step ss a then insert a b else b) [0..<length ss] {}

goal (1 subgoal):
 1. unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
unstables r step ss = fold (\<lambda>p A. if \<not> Typing_Framework_1.stable r step ss p then insert p A else A) [0..<length ss] {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [code]:
  "iter f step ss w = while (\<lambda>(ss, w). \<not> Set.is_empty w)
    (\<lambda>(ss, w).
        let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
    (ss, w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iter f step ss w = while (\<lambda>(ss, w). \<not> Set.is_empty w) (\<lambda>(ss, w). let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p})) (ss, w)
[PROOF STEP]
unfolding iter_def Set.is_empty_def some_elem_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while (\<lambda>(\<tau>s, w). w \<noteq> {}) (\<lambda>(\<tau>s, w). let p = SOME p. p \<in> w in propa f (step p (\<tau>s ! p)) \<tau>s (w - {p})) (ss, w) = while (\<lambda>(ss, w). w \<noteq> {}) (\<lambda>(ss, w). let p = SOME x. x \<in> w in propa f (step p (ss ! p)) ss (w - {p})) (ss, w)
[PROOF STEP]
..


[STATEMENT]
lemma JVM_sup_unfold [code]:
 "JVM_SemiType.sup S m n = lift2 (Opt.sup
       (Product.sup (Listn.sup (SemiType.sup S))
         (\<lambda>x y. OK (map2 (lift2 (SemiType.sup S)) x y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.sup S m n = lift2 (Opt.sup (Product.sup (Listn.sup (SemiType.sup S)) (\<lambda>x y. OK (map2 (lift2 (SemiType.sup S)) x y))))
[PROOF STEP]
apply (unfold JVM_SemiType.sup_def JVM_SemiType.sl_def Opt.esl_def Err.sl_def
         stk_esl_def loc_sl_def Product.esl_def
         Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd (case case (case case (types S, subtype S, SemiType.sup S) of (A, r, f) \<Rightarrow> (\<Union> {nlists n A |n. n \<le> m}, Listn.le r, Listn.sup f) of (A, r\<^sub>A, f\<^sub>A) \<Rightarrow> \<lambda>(B, r\<^sub>B, f\<^sub>B). (A \<times> B, Product.le r\<^sub>A r\<^sub>B, Product.sup f\<^sub>A f\<^sub>B)) (case case case (types S, subtype S, SemiType.sup S) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f) of (A, r, f) \<Rightarrow> (nlists n A, Listn.le r, map2 f) of (A, r, f) \<Rightarrow> (A, r, \<lambda>x y. OK (f x y))) of (A, r, f) \<Rightarrow> (opt A, Opt.le r, Opt.sup f) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f))) = lift2 (Opt.sup (Product.sup (Listn.sup (SemiType.sup S)) (\<lambda>x y. OK (map2 (lift2 (SemiType.sup S)) x y))))
[PROOF STEP]
by simp


[STATEMENT]
lemma [code]:
  "is_refT T = (case T of NT \<Rightarrow> True | Class C \<Rightarrow> True | _ \<Rightarrow> False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_refT T = (case T of NT \<Rightarrow> True | Class C \<Rightarrow> True | _ \<Rightarrow> False)
[PROOF STEP]
by (simp add: is_refT_def split: ty.split)


[STATEMENT]
lemma [code]:
  "app\<^sub>i (Getfield F C, P, pc, mxs, T\<^sub>r, (T#ST, LT)) =
    Predicate.holds (Predicate.bind (sees_field_i_i_i_o_i P C F C) (\<lambda>T\<^sub>f. if P \<turnstile> T \<le> Class C then Predicate.single () else bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app\<^sub>i (Getfield F C, P, pc, mxs, T\<^sub>r, T # ST, LT) = Predicate.holds (Predicate.bind (sees_field_i_i_i_o_i P C F C) (\<lambda>T\<^sub>f. if subtype P T (Class C) then Predicate.single () else bot))
[PROOF STEP]
by(auto simp add: Predicate.holds_eq intro: sees_field_i_i_i_o_iI elim: sees_field_i_i_i_o_iE)


[STATEMENT]
lemma [code]:
  "app\<^sub>i (Putfield F C, P, pc, mxs, T\<^sub>r, (T\<^sub>1#T\<^sub>2#ST, LT)) =
     Predicate.holds (Predicate.bind (sees_field_i_i_i_o_i P C F C) (\<lambda>T\<^sub>f. if P \<turnstile> T\<^sub>2 \<le> (Class C) \<and> P \<turnstile> T\<^sub>1 \<le> T\<^sub>f then Predicate.single () else bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app\<^sub>i (Putfield F C, P, pc, mxs, T\<^sub>r, T\<^sub>1 # T\<^sub>2 # ST, LT) = Predicate.holds (Predicate.bind (sees_field_i_i_i_o_i P C F C) (\<lambda>T\<^sub>f. if subtype P T\<^sub>2 (Class C) \<and> subtype P T\<^sub>1 T\<^sub>f then Predicate.single () else bot))
[PROOF STEP]
by(auto simp add: Predicate.holds_eq simp del: eval_bind split: if_split_asm elim!: sees_field_i_i_i_o_iE Predicate.bindE intro: Predicate.bindI sees_field_i_i_i_o_iI)


[STATEMENT]
lemma [code]:
  "app\<^sub>i (Invoke M n, P, pc, mxs, T\<^sub>r, (ST,LT)) =
    (n < length ST \<and>
    (ST!n \<noteq> NT \<longrightarrow>
      (case ST!n of
         Class C \<Rightarrow> Predicate.holds (Predicate.bind (Method_i_i_i_o_o_o_o P C M) (\<lambda>(Ts, T, m, D). if P \<turnstile> rev (take n ST) [\<le>] Ts then Predicate.single () else bot))
       | _ \<Rightarrow> False)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app\<^sub>i (Invoke M n, P, pc, mxs, T\<^sub>r, ST, LT) = (n < length ST \<and> (ST ! n \<noteq> NT \<longrightarrow> (case ST ! n of Class C \<Rightarrow> Predicate.holds (Predicate.bind (Method_i_i_i_o_o_o_o P C M) (\<lambda>(Ts, T, m, D). if P \<turnstile> rev (take n ST) [\<le>] Ts then Predicate.single () else bot)) | _ \<Rightarrow> False)))
[PROOF STEP]
by (fastforce simp add: Predicate.holds_eq simp del: eval_bind split: ty.split_asm if_split_asm intro: bindI Method_i_i_i_o_o_o_oI elim!: bindE Method_i_i_i_o_o_o_oE)


[STATEMENT]
lemma functions_of_eq:
  assumes "finite A"
  assumes "f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}"
  shows "functions_of A (f ` A) = domain_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of A (f ` A) = domain_permutation A B `` {f}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. functions_of A (f ` A) \<subseteq> domain_permutation A B `` {f}
 2. domain_permutation A B `` {f} \<subseteq> functions_of A (f ` A)
[PROOF STEP]
have bij: "bij_betw f A (f ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f A (f ` A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}

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

goal (2 subgoals):
 1. functions_of A (f ` A) \<subseteq> domain_permutation A B `` {f}
 2. domain_permutation A B `` {f} \<subseteq> functions_of A (f ` A)
[PROOF STEP]
show "functions_of A (f ` A) \<subseteq> domain_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of A (f ` A) \<subseteq> domain_permutation A B `` {f}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> functions_of A (f ` A) \<Longrightarrow> x \<in> domain_permutation A B `` {f}
[PROOF STEP]
fix f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> functions_of A (f ` A) \<Longrightarrow> x \<in> domain_permutation A B `` {f}
[PROOF STEP]
assume "f' \<in> functions_of A (f ` A)"
[PROOF STATE]
proof (state)
this:
f' \<in> functions_of A (f ` A)

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of A (f ` A) \<Longrightarrow> x \<in> domain_permutation A B `` {f}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f' \<in> functions_of A (f ` A)
[PROOF STEP]
have "f' \<in> A \<rightarrow>\<^sub>E f ` A" and "f' ` A = f ` A"
[PROOF STATE]
proof (prove)
using this:
f' \<in> functions_of A (f ` A)

goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E f ` A &&& f' ` A = f ` A
[PROOF STEP]
unfolding functions_of_def
[PROOF STATE]
proof (prove)
using this:
f' \<in> {fa \<in> A \<rightarrow>\<^sub>E f ` A. fa ` A = f ` A}

goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E f ` A &&& f' ` A = f ` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' \<in> A \<rightarrow>\<^sub>E f ` A
f' ` A = f ` A

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of A (f ` A) \<Longrightarrow> x \<in> domain_permutation A B `` {f}
[PROOF STEP]
from this assms
[PROOF STATE]
proof (chain)
picking this:
f' \<in> A \<rightarrow>\<^sub>E f ` A
f' ` A = f ` A
finite A
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}
[PROOF STEP]
have "f' \<in> A \<rightarrow>\<^sub>E B" and "inj_on f A"
[PROOF STATE]
proof (prove)
using this:
f' \<in> A \<rightarrow>\<^sub>E f ` A
f' ` A = f ` A
finite A
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}

goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E B &&& inj_on f A
[PROOF STEP]
using PiE_mem
[PROOF STATE]
proof (prove)
using this:
f' \<in> A \<rightarrow>\<^sub>E f ` A
f' ` A = f ` A
finite A
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}
\<lbrakk>?f \<in> Pi\<^sub>E ?S ?T; ?x \<in> ?S\<rbrakk> \<Longrightarrow> ?f ?x \<in> ?T ?x

goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E B &&& inj_on f A
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
f' \<in> A \<rightarrow>\<^sub>E B
inj_on f A

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of A (f ` A) \<Longrightarrow> x \<in> domain_permutation A B `` {f}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f' \<in> A \<rightarrow>\<^sub>E B
inj_on f A

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of A (f ` A) \<Longrightarrow> x \<in> domain_permutation A B `` {f}
[PROOF STEP]
have "\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ?p permutes A \<and> (\<forall>x\<in>A. f x = f' (?p x))
[PROOF STEP]
let ?p = "\<lambda>x. if x \<in> A then inv_into A f' (f x) else x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ?p permutes A \<and> (\<forall>x\<in>A. f x = f' (?p x))
[PROOF STEP]
show "?p permutes A \<and> (\<forall>x\<in>A. f x = f' (?p x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) permutes A \<and> (\<forall>x\<in>A. f x = f' (if x \<in> A then inv_into A f' (f x) else x))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) permutes A
 2. \<forall>x\<in>A. f x = f' (if x \<in> A then inv_into A f' (f x) else x)
[PROOF STEP]
show "?p permutes A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) permutes A
[PROOF STEP]
proof (rule bij_imp_permutes)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bij_betw (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) A A
 2. \<And>x. x \<notin> A \<Longrightarrow> (if x \<in> A then inv_into A f' (f x) else x) = x
[PROOF STEP]
show "bij_betw ?p A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) A A
[PROOF STEP]
proof (rule bij_betw_imageI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) A
 2. (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A = A
[PROOF STEP]
show "inj_on ?p A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) A
[PROOF STEP]
proof (rule inj_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; (if x \<in> A then inv_into A f' (f x) else x) = (if y \<in> A then inv_into A f' (f y) else y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix a a'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; (if x \<in> A then inv_into A f' (f x) else x) = (if y \<in> A then inv_into A f' (f y) else y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "a \<in> A" "a' \<in> A" "?p a = ?p a'"
[PROOF STATE]
proof (state)
this:
a \<in> A
a' \<in> A
(if a \<in> A then inv_into A f' (f a) else a) = (if a' \<in> A then inv_into A f' (f a') else a')

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; (if x \<in> A then inv_into A f' (f x) else x) = (if y \<in> A then inv_into A f' (f y) else y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
a' \<in> A
(if a \<in> A then inv_into A f' (f a) else a) = (if a' \<in> A then inv_into A f' (f a') else a')
[PROOF STEP]
have "inv_into A f' (f a) = inv_into A f' (f a')"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
a' \<in> A
(if a \<in> A then inv_into A f' (f a) else a) = (if a' \<in> A then inv_into A f' (f a') else a')

goal (1 subgoal):
 1. inv_into A f' (f a) = inv_into A f' (f a')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_into A f' (f a) = inv_into A f' (f a')

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; (if x \<in> A then inv_into A f' (f x) else x) = (if y \<in> A then inv_into A f' (f y) else y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from this \<open>a \<in> A\<close> \<open>a' \<in> A\<close> \<open>f' ` A = f ` A\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_into A f' (f a) = inv_into A f' (f a')
a \<in> A
a' \<in> A
f' ` A = f ` A
[PROOF STEP]
have "f a = f a'"
[PROOF STATE]
proof (prove)
using this:
inv_into A f' (f a) = inv_into A f' (f a')
a \<in> A
a' \<in> A
f' ` A = f ` A

goal (1 subgoal):
 1. f a = f a'
[PROOF STEP]
using inv_into_injective
[PROOF STATE]
proof (prove)
using this:
inv_into A f' (f a) = inv_into A f' (f a')
a \<in> A
a' \<in> A
f' ` A = f ` A
\<lbrakk>inv_into ?A ?f ?x = inv_into ?A ?f ?y; ?x \<in> ?f ` ?A; ?y \<in> ?f ` ?A\<rbrakk> \<Longrightarrow> ?x = ?y

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A; (if x \<in> A then inv_into A f' (f x) else x) = (if y \<in> A then inv_into A f' (f y) else y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from this \<open>a \<in> A\<close> \<open>a' \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
f a = f a'
a \<in> A
a' \<in> A
[PROOF STEP]
show "a = a'"
[PROOF STATE]
proof (prove)
using this:
f a = f a'
a \<in> A
a' \<in> A

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) A

goal (1 subgoal):
 1. (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A = A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A = A
[PROOF STEP]
show "?p ` A = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A = A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A \<subseteq> A
 2. A \<subseteq> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
show "?p ` A \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A \<subseteq> A
[PROOF STEP]
using \<open>f' ` A = f ` A\<close>
[PROOF STATE]
proof (prove)
using this:
f' ` A = f ` A

goal (1 subgoal):
 1. (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A \<subseteq> A
[PROOF STEP]
by (simp add: image_subsetI inv_into_into)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A \<subseteq> A

goal (1 subgoal):
 1. A \<subseteq> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<subseteq> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
show "A \<subseteq> ?p ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
assume "a \<in> A"
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
have "inj_on f' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f' A
[PROOF STEP]
using \<open>finite A\<close> \<open>f' ` A = f ` A\<close> \<open>inj_on f A\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
f' ` A = f ` A
inj_on f A

goal (1 subgoal):
 1. inj_on f' A
[PROOF STEP]
by (simp add: card_image eq_card_imp_inj_on)
[PROOF STATE]
proof (state)
this:
inj_on f' A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
from \<open>a \<in> A\<close> \<open>f' ` A = f ` A\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
f' ` A = f ` A
[PROOF STEP]
have "inv_into A f (f' a) \<in> A"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
f' ` A = f ` A

goal (1 subgoal):
 1. inv_into A f (f' a) \<in> A
[PROOF STEP]
by (metis image_eqI inv_into_into)
[PROOF STATE]
proof (state)
this:
inv_into A f (f' a) \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv_into A f (f' a) \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
have "a = inv_into A f' (f (inv_into A f (f' a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = inv_into A f' (f (inv_into A f (f' a)))
[PROOF STEP]
using \<open>a \<in> A\<close> \<open>f' ` A = f ` A\<close> \<open>inj_on f' A\<close>
[PROOF STATE]
proof (prove)
using this:
a \<in> A
f' ` A = f ` A
inj_on f' A

goal (1 subgoal):
 1. a = inv_into A f' (f (inv_into A f (f' a)))
[PROOF STEP]
by (metis f_inv_into_f image_eqI inv_into_f_f)
[PROOF STATE]
proof (state)
this:
a = inv_into A f' (f (inv_into A f (f' a)))

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inv_into A f (f' a) \<in> A
a = inv_into A f' (f (inv_into A f (f' a)))
[PROOF STEP]
show "a \<in> ?p ` A"
[PROOF STATE]
proof (prove)
using this:
inv_into A f (f' a) \<in> A
a = inv_into A f' (f (inv_into A f (f' a)))

goal (1 subgoal):
 1. a \<in> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<subseteq> (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) ` A = A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bij_betw (\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) A A

goal (1 subgoal):
 1. \<And>x. x \<notin> A \<Longrightarrow> (if x \<in> A then inv_into A f' (f x) else x) = x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<notin> A \<Longrightarrow> (if x \<in> A then inv_into A f' (f x) else x) = x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<notin> A \<Longrightarrow> (if x \<in> A then inv_into A f' (f x) else x) = x
[PROOF STEP]
assume "x \<notin> A"
[PROOF STATE]
proof (state)
this:
x \<notin> A

goal (1 subgoal):
 1. \<And>x. x \<notin> A \<Longrightarrow> (if x \<in> A then inv_into A f' (f x) else x) = x
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<notin> A
[PROOF STEP]
show "?p x = x"
[PROOF STATE]
proof (prove)
using this:
x \<notin> A

goal (1 subgoal):
 1. (if x \<in> A then inv_into A f' (f x) else x) = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if x \<in> A then inv_into A f' (f x) else x) = x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) permutes A

goal (1 subgoal):
 1. \<forall>x\<in>A. f x = f' (if x \<in> A then inv_into A f' (f x) else x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>A. f x = f' (if x \<in> A then inv_into A f' (f x) else x)
[PROOF STEP]
from \<open>f' ` A = f ` A\<close>
[PROOF STATE]
proof (chain)
picking this:
f' ` A = f ` A
[PROOF STEP]
show "\<forall>x\<in>A. f x = f' (?p x)"
[PROOF STATE]
proof (prove)
using this:
f' ` A = f ` A

goal (1 subgoal):
 1. \<forall>x\<in>A. f x = f' (if x \<in> A then inv_into A f' (f x) else x)
[PROOF STEP]
by (simp add: f_inv_into_f)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>A. f x = f' (if x \<in> A then inv_into A f' (f x) else x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x \<in> A then inv_into A f' (f x) else x) permutes A \<and> (\<forall>x\<in>A. f x = f' (if x \<in> A then inv_into A f' (f x) else x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x))

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of A (f ` A) \<Longrightarrow> x \<in> domain_permutation A B `` {f}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x))

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of A (f ` A) \<Longrightarrow> x \<in> domain_permutation A B `` {f}
[PROOF STEP]
have "f \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}

goal (1 subgoal):
 1. f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x. x \<in> functions_of A (f ` A) \<Longrightarrow> x \<in> domain_permutation A B `` {f}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f' \<in> A \<rightarrow>\<^sub>E B
inj_on f A
\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x))
f \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
show "f' \<in> domain_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
using this:
f' \<in> A \<rightarrow>\<^sub>E B
inj_on f A
\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x))
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. f' \<in> domain_permutation A B `` {f}
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
f' \<in> A \<rightarrow>\<^sub>E B
inj_on f A
\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x))
f \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. f' \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))} `` {f}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' \<in> domain_permutation A B `` {f}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
functions_of A (f ` A) \<subseteq> domain_permutation A B `` {f}

goal (1 subgoal):
 1. domain_permutation A B `` {f} \<subseteq> functions_of A (f ` A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. domain_permutation A B `` {f} \<subseteq> functions_of A (f ` A)
[PROOF STEP]
show "domain_permutation A B `` {f} \<subseteq> functions_of A (f ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_permutation A B `` {f} \<subseteq> functions_of A (f ` A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> functions_of A (f ` A)
[PROOF STEP]
fix f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> functions_of A (f ` A)
[PROOF STEP]
assume "f' \<in> domain_permutation A B `` {f}"
[PROOF STATE]
proof (state)
this:
f' \<in> domain_permutation A B `` {f}

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> functions_of A (f ` A)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f' \<in> domain_permutation A B `` {f}
[PROOF STEP]
obtain p where p: "p permutes A" "\<forall>x\<in>A. f x = f' (p x)"
      and "f \<in> A \<rightarrow>\<^sub>E B" "f' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
using this:
f' \<in> domain_permutation A B `` {f}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x); f \<in> A \<rightarrow>\<^sub>E B; f' \<in> A \<rightarrow>\<^sub>E B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
f' \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))} `` {f}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f x = f' (p x); f \<in> A \<rightarrow>\<^sub>E B; f' \<in> A \<rightarrow>\<^sub>E B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
f \<in> A \<rightarrow>\<^sub>E B
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> functions_of A (f ` A)
[PROOF STEP]
have "f' ` A = f ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' ` A = f ` A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f' ` A \<subseteq> f ` A
 2. f ` A \<subseteq> f' ` A
[PROOF STEP]
show "f' ` A \<subseteq> f ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' ` A \<subseteq> f ` A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> f' ` A \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> f' ` A \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
assume "x \<in> f' ` A"
[PROOF STATE]
proof (state)
this:
x \<in> f' ` A

goal (1 subgoal):
 1. \<And>x. x \<in> f' ` A \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> f' ` A
[PROOF STEP]
obtain x' where "x = f' x'" and "x' \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> f' ` A

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x = f' x'; x' \<in> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x = f' x'
x' \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> f' ` A \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x = f' x'
x' \<in> A
[PROOF STEP]
have "x = f (inv p x')"
[PROOF STATE]
proof (prove)
using this:
x = f' x'
x' \<in> A

goal (1 subgoal):
 1. x = f (inv p x')
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
x = f' x'
x' \<in> A
p permutes A
\<forall>x\<in>A. f x = f' (p x)

goal (1 subgoal):
 1. x = f (inv p x')
[PROOF STEP]
by (metis (mono_tags, lifting) permutes_in_image permutes_inverses(1))
[PROOF STATE]
proof (state)
this:
x = f (inv p x')

goal (1 subgoal):
 1. \<And>x. x \<in> f' ` A \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = f (inv p x')

goal (1 subgoal):
 1. \<And>x. x \<in> f' ` A \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
have "inv p x' \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv p x' \<in> A
[PROOF STEP]
using p \<open>x' \<in> A\<close>
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
x' \<in> A

goal (1 subgoal):
 1. inv p x' \<in> A
[PROOF STEP]
by (simp add: permutes_in_image permutes_inv)
[PROOF STATE]
proof (state)
this:
inv p x' \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> f' ` A \<Longrightarrow> x \<in> f ` A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = f (inv p x')
inv p x' \<in> A
[PROOF STEP]
show "x \<in> f ` A"
[PROOF STATE]
proof (prove)
using this:
x = f (inv p x')
inv p x' \<in> A

goal (1 subgoal):
 1. x \<in> f ` A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x \<in> f ` A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f' ` A \<subseteq> f ` A

goal (1 subgoal):
 1. f ` A \<subseteq> f' ` A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f ` A \<subseteq> f' ` A
[PROOF STEP]
show "f ` A \<subseteq> f' ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` A \<subseteq> f' ` A
[PROOF STEP]
using p permutes_in_image
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f x = f' (p x)
?p permutes ?S \<Longrightarrow> (?p ?x \<in> ?S) = (?x \<in> ?S)

goal (1 subgoal):
 1. f ` A \<subseteq> f' ` A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f ` A \<subseteq> f' ` A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f' ` A = f ` A

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> functions_of A (f ` A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f' ` A = f ` A

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> functions_of A (f ` A)
[PROOF STEP]
from this \<open>f' \<in> A \<rightarrow>\<^sub>E B\<close>
[PROOF STATE]
proof (chain)
picking this:
f' ` A = f ` A
f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
have "f' \<in> A \<rightarrow>\<^sub>E f ` A"
[PROOF STATE]
proof (prove)
using this:
f' ` A = f ` A
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E f ` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' \<in> A \<rightarrow>\<^sub>E f ` A

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> functions_of A (f ` A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f' ` A = f ` A
f' \<in> A \<rightarrow>\<^sub>E f ` A
[PROOF STEP]
show "f' \<in> functions_of A (f ` A)"
[PROOF STATE]
proof (prove)
using this:
f' ` A = f ` A
f' \<in> A \<rightarrow>\<^sub>E f ` A

goal (1 subgoal):
 1. f' \<in> functions_of A (f ` A)
[PROOF STEP]
unfolding functions_of_def
[PROOF STATE]
proof (prove)
using this:
f' ` A = f ` A
f' \<in> A \<rightarrow>\<^sub>E f ` A

goal (1 subgoal):
 1. f' \<in> {fa \<in> A \<rightarrow>\<^sub>E f ` A. fa ` A = f ` A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' \<in> functions_of A (f ` A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
domain_permutation A B `` {f} \<subseteq> functions_of A (f ` A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subset_of:
  assumes "F \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B"
  shows "subset_of A F \<subseteq> B" and "card (subset_of A F) = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subset_of A F \<subseteq> B &&& card (subset_of A F) = card A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subset_of A F \<subseteq> B
 2. card (subset_of A F) = card A
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
obtain f where F_eq: "F = (domain_permutation A B) `` {f}"
    and f: "f \<in> A \<rightarrow>\<^sub>E B" "inj_on f A"
[PROOF STATE]
proof (prove)
using this:
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>F = domain_permutation A B `` {f}; f \<in> A \<rightarrow>\<^sub>E B; inj_on f A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mem_Collect_eq quotientE
[PROOF STATE]
proof (prove)
using this:
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
(?a \<in> Collect ?P) = ?P ?a
\<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 = domain_permutation A B `` {f}; f \<in> A \<rightarrow>\<^sub>E B; inj_on f A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
F = domain_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B
inj_on f A

goal (2 subgoals):
 1. subset_of A F \<subseteq> B
 2. card (subset_of A F) = card A
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
F = domain_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B
inj_on f A
[PROOF STEP]
have "subset_of A (domain_permutation A B `` {f}) = f ` A"
[PROOF STATE]
proof (prove)
using this:
F = domain_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B
inj_on f A

goal (1 subgoal):
 1. subset_of A (domain_permutation A B `` {f}) = f ` A
[PROOF STEP]
using equiv_domain_permutation image_respects_domain_permutation
[PROOF STATE]
proof (prove)
using this:
F = domain_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B
inj_on f A
equiv (?A \<rightarrow>\<^sub>E ?B) (domain_permutation ?A ?B)
(\<lambda>f. f ` ?A) respects domain_permutation ?A ?B

goal (1 subgoal):
 1. subset_of A (domain_permutation A B `` {f}) = f ` A
[PROOF STEP]
unfolding subset_of_def
[PROOF STATE]
proof (prove)
using this:
F = domain_permutation A B `` {f}
f \<in> A \<rightarrow>\<^sub>E B
inj_on f A
equiv (?A \<rightarrow>\<^sub>E ?B) (domain_permutation ?A ?B)
(\<lambda>f. f ` ?A) respects domain_permutation ?A ?B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A) (domain_permutation A B `` {f}) = f ` A
[PROOF STEP]
by (intro univ_commute') auto
[PROOF STATE]
proof (state)
this:
subset_of A (domain_permutation A B `` {f}) = f ` A

goal (2 subgoals):
 1. subset_of A F \<subseteq> B
 2. card (subset_of A F) = card A
[PROOF STEP]
from this f F_eq
[PROOF STATE]
proof (chain)
picking this:
subset_of A (domain_permutation A B `` {f}) = f ` A
f \<in> A \<rightarrow>\<^sub>E B
inj_on f A
F = domain_permutation A B `` {f}
[PROOF STEP]
show "subset_of A F \<subseteq> B" and "card (subset_of A F) = card A"
[PROOF STATE]
proof (prove)
using this:
subset_of A (domain_permutation A B `` {f}) = f ` A
f \<in> A \<rightarrow>\<^sub>E B
inj_on f A
F = domain_permutation A B `` {f}

goal (1 subgoal):
 1. subset_of A F \<subseteq> B &&& card (subset_of A F) = card A
[PROOF STEP]
by (auto simp add: card_image)
[PROOF STATE]
proof (state)
this:
subset_of A F \<subseteq> B
card (subset_of A F) = card A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma functions_of:
  assumes "finite A" "finite B" "X \<subseteq> B" "card X = card A"
  shows "functions_of A X \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of A X \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. functions_of A X \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
finite B
X \<subseteq> B
card X = card A
[PROOF STEP]
obtain f where f: "f \<in> A \<rightarrow>\<^sub>E X \<and> bij_betw f A X"
[PROOF STATE]
proof (prove)
using this:
finite A
finite B
X \<subseteq> B
card X = card A

goal (1 subgoal):
 1. (\<And>f. f \<in> A \<rightarrow>\<^sub>E X \<and> bij_betw f A X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
finite B
X \<subseteq> B
card X = card A
finite A
finite B

goal (1 subgoal):
 1. (\<And>f. f \<in> A \<rightarrow>\<^sub>E X \<and> bij_betw f A X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis finite_same_card_bij_on_ext_funcset finite_subset)
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E X \<and> bij_betw f A X

goal (1 subgoal):
 1. functions_of A X \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E X \<and> bij_betw f A X
[PROOF STEP]
have "X = f ` A"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E X \<and> bij_betw f A X

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

goal (1 subgoal):
 1. functions_of A X \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
from f \<open>X \<subseteq> B\<close>
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E X \<and> bij_betw f A X
X \<subseteq> B
[PROOF STEP]
have "f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E X \<and> bij_betw f A X
X \<subseteq> B

goal (1 subgoal):
 1. f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}
[PROOF STEP]
by (auto simp add: bij_betw_imp_inj_on)
[PROOF STATE]
proof (state)
this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}

goal (1 subgoal):
 1. functions_of A X \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
have "functions_of A X = domain_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of A X = domain_permutation A B `` {f}
[PROOF STEP]
using \<open>finite A\<close> \<open>X = f ` A\<close> \<open>f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
X = f ` A
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}

goal (1 subgoal):
 1. functions_of A X = domain_permutation A B `` {f}
[PROOF STEP]
by (simp add: functions_of_eq)
[PROOF STATE]
proof (state)
this:
functions_of A X = domain_permutation A B `` {f}

goal (1 subgoal):
 1. functions_of A X \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
functions_of A X = domain_permutation A B `` {f}
[PROOF STEP]
show "functions_of A X \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B"
[PROOF STATE]
proof (prove)
using this:
functions_of A X = domain_permutation A B `` {f}

goal (1 subgoal):
 1. functions_of A X \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
using \<open>f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}\<close>
[PROOF STATE]
proof (prove)
using this:
functions_of A X = domain_permutation A B `` {f}
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}

goal (1 subgoal):
 1. functions_of A X \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
by (auto intro: quotientI)
[PROOF STATE]
proof (state)
this:
functions_of A X \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subset_of_functions_of:
  assumes "finite A" "finite X" "card A = card X"
  shows "subset_of A (functions_of A X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
finite X
card A = card X
[PROOF STEP]
obtain f where "f \<in> A \<rightarrow>\<^sub>E X" and "bij_betw f A X"
[PROOF STATE]
proof (prove)
using this:
finite A
finite X
card A = card X

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E X; bij_betw f A X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_same_card_bij_on_ext_funcset
[PROOF STATE]
proof (prove)
using this:
finite A
finite X
card A = card X
\<lbrakk>finite ?A; finite ?B; card ?A = card ?B\<rbrakk> \<Longrightarrow> \<exists>f. f \<in> ?A \<rightarrow>\<^sub>E ?B \<and> bij_betw f ?A ?B

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> A \<rightarrow>\<^sub>E X; bij_betw f A X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> A \<rightarrow>\<^sub>E X
bij_betw f A X

goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f \<in> A \<rightarrow>\<^sub>E X
bij_betw f A X
[PROOF STEP]
have subset_of: "subset_of A (domain_permutation A X `` {f}) = f ` A"
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E X
bij_betw f A X

goal (1 subgoal):
 1. subset_of A (domain_permutation A X `` {f}) = f ` A
[PROOF STEP]
using equiv_domain_permutation image_respects_domain_permutation
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E X
bij_betw f A X
equiv (?A \<rightarrow>\<^sub>E ?B) (domain_permutation ?A ?B)
(\<lambda>f. f ` ?A) respects domain_permutation ?A ?B

goal (1 subgoal):
 1. subset_of A (domain_permutation A X `` {f}) = f ` A
[PROOF STEP]
unfolding subset_of_def
[PROOF STATE]
proof (prove)
using this:
f \<in> A \<rightarrow>\<^sub>E X
bij_betw f A X
equiv (?A \<rightarrow>\<^sub>E ?B) (domain_permutation ?A ?B)
(\<lambda>f. f ` ?A) respects domain_permutation ?A ?B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A) (domain_permutation A X `` {f}) = f ` A
[PROOF STEP]
by (intro univ_commute') auto
[PROOF STATE]
proof (state)
this:
subset_of A (domain_permutation A X `` {f}) = f ` A

goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
from \<open>bij_betw f A X\<close>
[PROOF STATE]
proof (chain)
picking this:
bij_betw f A X
[PROOF STEP]
have "inj_on f A" and "f ` A = X"
[PROOF STATE]
proof (prove)
using this:
bij_betw f A X

goal (1 subgoal):
 1. inj_on f A &&& f ` A = X
[PROOF STEP]
by (auto simp add: bij_betw_def)
[PROOF STATE]
proof (state)
this:
inj_on f A
f ` A = X

goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
have "subset_of A (functions_of A X) = subset_of A (functions_of A (f ` A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subset_of A (functions_of A X) = subset_of A (functions_of A (f ` A))
[PROOF STEP]
using \<open>f ` A = X\<close>
[PROOF STATE]
proof (prove)
using this:
f ` A = X

goal (1 subgoal):
 1. subset_of A (functions_of A X) = subset_of A (functions_of A (f ` A))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subset_of A (functions_of A X) = subset_of A (functions_of A (f ` A))

goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subset_of A (functions_of A X) = subset_of A (functions_of A (f ` A))

goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
have "\<dots> = subset_of A (domain_permutation A X `` {f})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subset_of A (functions_of A (f ` A)) = subset_of A (domain_permutation A X `` {f})
[PROOF STEP]
using \<open>finite A\<close> \<open>inj_on f A\<close> \<open>f \<in> A \<rightarrow>\<^sub>E X\<close>
[PROOF STATE]
proof (prove)
using this:
finite A
inj_on f A
f \<in> A \<rightarrow>\<^sub>E X

goal (1 subgoal):
 1. subset_of A (functions_of A (f ` A)) = subset_of A (domain_permutation A X `` {f})
[PROOF STEP]
by (auto simp add: functions_of_eq)
[PROOF STATE]
proof (state)
this:
subset_of A (functions_of A (f ` A)) = subset_of A (domain_permutation A X `` {f})

goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subset_of A (functions_of A (f ` A)) = subset_of A (domain_permutation A X `` {f})

goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
have "\<dots> = f ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subset_of A (domain_permutation A X `` {f}) = f ` A
[PROOF STEP]
using \<open>inj_on f A\<close> \<open>f \<in> A \<rightarrow>\<^sub>E X\<close>
[PROOF STATE]
proof (prove)
using this:
inj_on f A
f \<in> A \<rightarrow>\<^sub>E X

goal (1 subgoal):
 1. subset_of A (domain_permutation A X `` {f}) = f ` A
[PROOF STEP]
by (simp add: subset_of)
[PROOF STATE]
proof (state)
this:
subset_of A (domain_permutation A X `` {f}) = f ` A

goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subset_of A (domain_permutation A X `` {f}) = f ` A

goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
have "\<dots> = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` A = X
[PROOF STEP]
using \<open>f ` A = X\<close>
[PROOF STATE]
proof (prove)
using this:
f ` A = X

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

goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
subset_of A (functions_of A X) = X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subset_of A (functions_of A X) = X

goal (1 subgoal):
 1. subset_of A (functions_of A X) = X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
subset_of A (functions_of A X) = X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma functions_of_subset_of:
  assumes "finite A"
  assumes "F \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B"
  shows "functions_of A (subset_of A F) = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of A (subset_of A F) = F
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
F \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B

goal (1 subgoal):
 1. functions_of A (subset_of A F) = F
[PROOF STEP]
proof (rule quotientE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>F = domain_permutation A B `` {x}; x \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}\<rbrakk> \<Longrightarrow> functions_of A (subset_of A F) = F
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>F = domain_permutation A B `` {x}; x \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}\<rbrakk> \<Longrightarrow> functions_of A (subset_of A F) = F
[PROOF STEP]
assume f: "f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}"
    and F_eq: "F = domain_permutation A B `` {f}"
[PROOF STATE]
proof (state)
this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}
F = domain_permutation A B `` {f}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>F = domain_permutation A B `` {x}; x \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}\<rbrakk> \<Longrightarrow> functions_of A (subset_of A F) = F
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}
F = domain_permutation A B `` {f}
[PROOF STEP]
have "subset_of A (domain_permutation A B `` {f}) = f ` A"
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}
F = domain_permutation A B `` {f}

goal (1 subgoal):
 1. subset_of A (domain_permutation A B `` {f}) = f ` A
[PROOF STEP]
using equiv_domain_permutation image_respects_domain_permutation
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}
F = domain_permutation A B `` {f}
equiv (?A \<rightarrow>\<^sub>E ?B) (domain_permutation ?A ?B)
(\<lambda>f. f ` ?A) respects domain_permutation ?A ?B

goal (1 subgoal):
 1. subset_of A (domain_permutation A B `` {f}) = f ` A
[PROOF STEP]
unfolding subset_of_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}
F = domain_permutation A B `` {f}
equiv (?A \<rightarrow>\<^sub>E ?B) (domain_permutation ?A ?B)
(\<lambda>f. f ` ?A) respects domain_permutation ?A ?B

goal (1 subgoal):
 1. univ (\<lambda>f. f ` A) (domain_permutation A B `` {f}) = f ` A
[PROOF STEP]
by (intro univ_commute') auto
[PROOF STATE]
proof (state)
this:
subset_of A (domain_permutation A B `` {f}) = f ` A

goal (1 subgoal):
 1. \<And>x. \<lbrakk>F = domain_permutation A B `` {x}; x \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}\<rbrakk> \<Longrightarrow> functions_of A (subset_of A F) = F
[PROOF STEP]
from this f F_eq \<open>finite A\<close>
[PROOF STATE]
proof (chain)
picking this:
subset_of A (domain_permutation A B `` {f}) = f ` A
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}
F = domain_permutation A B `` {f}
finite A
[PROOF STEP]
show "functions_of A (subset_of A F) = F"
[PROOF STATE]
proof (prove)
using this:
subset_of A (domain_permutation A B `` {f}) = f ` A
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A}
F = domain_permutation A B `` {f}
finite A

goal (1 subgoal):
 1. functions_of A (subset_of A F) = F
[PROOF STEP]
by (simp add: functions_of_eq)
[PROOF STATE]
proof (state)
this:
functions_of A (subset_of A F) = F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_subset_of:
  assumes "finite A" "finite B"
  shows "bij_betw (subset_of A) ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) {X. X \<subseteq> B \<and> card X = card A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (subset_of A) ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) {X. X \<subseteq> B \<and> card X = card A}
[PROOF STEP]
proof (rule bij_betw_byWitness[where f'="functions_of A"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>a\<in>{f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A a) = a
 2. \<forall>a'\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A a') = a'
 3. subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}
 4. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
show "\<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A F) = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A F) = F
[PROOF STEP]
using \<open>finite A\<close> functions_of_subset_of
[PROOF STATE]
proof (prove)
using this:
finite A
\<lbrakk>finite ?A; ?F \<in> {f \<in> ?A \<rightarrow>\<^sub>E ?B. inj_on f ?A} // domain_permutation ?A ?B\<rbrakk> \<Longrightarrow> functions_of ?A (subset_of ?A ?F) = ?F

goal (1 subgoal):
 1. \<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A F) = F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A F) = F

goal (3 subgoals):
 1. \<forall>a'\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A a') = a'
 2. subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}
 3. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
show "\<forall>X\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A X) = X
[PROOF STEP]
using subset_of_functions_of \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; finite ?X; card ?A = card ?X\<rbrakk> \<Longrightarrow> subset_of ?A (functions_of ?A ?X) = ?X
finite A
finite B

goal (1 subgoal):
 1. \<forall>X\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A X) = X
[PROOF STEP]
by (metis (mono_tags) finite_subset mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A X) = X

goal (2 subgoals):
 1. subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}
 2. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
show "subset_of A ` ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) \<subseteq> {X. X \<subseteq> B \<and> card X = card A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}
[PROOF STEP]
using subset_of
[PROOF STATE]
proof (prove)
using this:
?F \<in> {f \<in> ?A \<rightarrow>\<^sub>E ?B. inj_on f ?A} // domain_permutation ?A ?B \<Longrightarrow> subset_of ?A ?F \<subseteq> ?B
?F \<in> {f \<in> ?A \<rightarrow>\<^sub>E ?B. inj_on f ?A} // domain_permutation ?A ?B \<Longrightarrow> card (subset_of ?A ?F) = card ?A

goal (1 subgoal):
 1. subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}

goal (1 subgoal):
 1. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
show "functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close> functions_of
[PROOF STATE]
proof (prove)
using this:
finite A
finite B
\<lbrakk>finite ?A; finite ?B; ?X \<subseteq> ?B; card ?X = card ?A\<rbrakk> \<Longrightarrow> functions_of ?A ?X \<in> {f \<in> ?A \<rightarrow>\<^sub>E ?B. inj_on f ?A} // domain_permutation ?A ?B

goal (1 subgoal):
 1. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_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) {X. X \<subseteq> B \<and> card X = card A} ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (functions_of A) {X. X \<subseteq> B \<and> card X = card A} ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B)
[PROOF STEP]
proof (rule bij_betw_byWitness[where f'="subset_of A"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>a\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A a) = a
 2. \<forall>a'\<in>{f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A a') = a'
 3. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
 4. subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}
[PROOF STEP]
show "\<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A F) = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A F) = F
[PROOF STEP]
using \<open>finite A\<close> functions_of_subset_of
[PROOF STATE]
proof (prove)
using this:
finite A
\<lbrakk>finite ?A; ?F \<in> {f \<in> ?A \<rightarrow>\<^sub>E ?B. inj_on f ?A} // domain_permutation ?A ?B\<rbrakk> \<Longrightarrow> functions_of ?A (subset_of ?A ?F) = ?F

goal (1 subgoal):
 1. \<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A F) = F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>F\<in>{f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A F) = F

goal (3 subgoals):
 1. \<forall>a\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A a) = a
 2. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
 3. subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}
[PROOF STEP]
show "\<forall>X\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A X) = X
[PROOF STEP]
using subset_of_functions_of \<open>finite A\<close> \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; finite ?X; card ?A = card ?X\<rbrakk> \<Longrightarrow> subset_of ?A (functions_of ?A ?X) = ?X
finite A
finite B

goal (1 subgoal):
 1. \<forall>X\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A X) = X
[PROOF STEP]
by (metis (mono_tags) finite_subset mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>{X. X \<subseteq> B \<and> card X = card A}. subset_of A (functions_of A X) = X

goal (2 subgoals):
 1. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
 2. subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}
[PROOF STEP]
show "subset_of A ` ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) \<subseteq> {X. X \<subseteq> B \<and> card X = card A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}
[PROOF STEP]
using subset_of
[PROOF STATE]
proof (prove)
using this:
?F \<in> {f \<in> ?A \<rightarrow>\<^sub>E ?B. inj_on f ?A} // domain_permutation ?A ?B \<Longrightarrow> subset_of ?A ?F \<subseteq> ?B
?F \<in> {f \<in> ?A \<rightarrow>\<^sub>E ?B. inj_on f ?A} // domain_permutation ?A ?B \<Longrightarrow> card (subset_of ?A ?F) = card ?A

goal (1 subgoal):
 1. subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
subset_of A ` {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B \<subseteq> {X. X \<subseteq> B \<and> card X = card A}

goal (1 subgoal):
 1. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
show "functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
using \<open>finite A\<close> \<open>finite B\<close> functions_of
[PROOF STATE]
proof (prove)
using this:
finite A
finite B
\<lbrakk>finite ?A; finite ?B; ?X \<subseteq> ?B; card ?X = card ?A\<rbrakk> \<Longrightarrow> functions_of ?A ?X \<in> {f \<in> ?A \<rightarrow>\<^sub>E ?B. inj_on f ?A} // domain_permutation ?A ?B

goal (1 subgoal):
 1. functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
functions_of A ` {X. X \<subseteq> B \<and> card X = card A} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_mset_set:
  shows "bij_betw mset_set {A. finite A} {M. \<forall>x. count M x \<le> 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw mset_set {A. finite A} {M. \<forall>x. count M x \<le> 1}
[PROOF STEP]
proof (rule bij_betw_byWitness[where f'="set_mset"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>a\<in>{A. finite A}. set_mset (mset_set a) = a
 2. \<forall>a'\<in>{M. \<forall>x. count M x \<le> 1}. mset_set (set_mset a') = a'
 3. mset_set ` {A. finite A} \<subseteq> {M. \<forall>x. count M x \<le> 1}
 4. set_mset ` {M. \<forall>x. count M x \<le> 1} \<subseteq> {A. finite A}
[PROOF STEP]
show "\<forall>A\<in>{A. finite A}. set_mset (mset_set A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>{A. finite A}. set_mset (mset_set A) = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>{A. finite A}. set_mset (mset_set A) = A

goal (3 subgoals):
 1. \<forall>a'\<in>{M. \<forall>x. count M x \<le> 1}. mset_set (set_mset a') = a'
 2. mset_set ` {A. finite A} \<subseteq> {M. \<forall>x. count M x \<le> 1}
 3. set_mset ` {M. \<forall>x. count M x \<le> 1} \<subseteq> {A. finite A}
[PROOF STEP]
show "\<forall>M\<in>{M. \<forall>x. count M x \<le> 1}. mset_set (set_mset M) = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>M\<in>{M. \<forall>x. count M x \<le> 1}. mset_set (set_mset M) = M
[PROOF STEP]
by (auto simp add: mset_set_set_mset')
[PROOF STATE]
proof (state)
this:
\<forall>M\<in>{M. \<forall>x. count M x \<le> 1}. mset_set (set_mset M) = M

goal (2 subgoals):
 1. mset_set ` {A. finite A} \<subseteq> {M. \<forall>x. count M x \<le> 1}
 2. set_mset ` {M. \<forall>x. count M x \<le> 1} \<subseteq> {A. finite A}
[PROOF STEP]
show "mset_set ` {A. finite A} \<subseteq> {M. \<forall>x. count M x \<le> 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_set ` {A. finite A} \<subseteq> {M. \<forall>x. count M x \<le> 1}
[PROOF STEP]
using nat_le_linear
[PROOF STATE]
proof (prove)
using this:
?m \<le> ?n \<or> ?n \<le> ?m

goal (1 subgoal):
 1. mset_set ` {A. finite A} \<subseteq> {M. \<forall>x. count M x \<le> 1}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
mset_set ` {A. finite A} \<subseteq> {M. \<forall>x. count M x \<le> 1}

goal (1 subgoal):
 1. set_mset ` {M. \<forall>x. count M x \<le> 1} \<subseteq> {A. finite A}
[PROOF STEP]
show "set_mset ` {M. \<forall>x. count M x \<le> 1} \<subseteq> {A. finite A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_mset ` {M. \<forall>x. count M x \<le> 1} \<subseteq> {A. finite A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_mset ` {M. \<forall>x. count M x \<le> 1} \<subseteq> {A. finite A}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_mset_set_card:
  assumes "finite A"
  shows "bij_betw mset_set {X. X \<subseteq> A \<and> card X = k} {M. M \<subseteq># mset_set A \<and> size M = k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw mset_set {X. X \<subseteq> A \<and> card X = k} {M. M \<subseteq># mset_set A \<and> size M = k}
[PROOF STEP]
proof (rule bij_betw_byWitness[where f'="set_mset"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>a\<in>{X. X \<subseteq> A \<and> card X = k}. set_mset (mset_set a) = a
 2. \<forall>a'\<in>{M. M \<subseteq># mset_set A \<and> size M = k}. mset_set (set_mset a') = a'
 3. mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. M \<subseteq># mset_set A \<and> size M = k}
 4. set_mset ` {M. M \<subseteq># mset_set A \<and> size M = k} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
show "\<forall>X\<in>{X. X \<subseteq> A \<and> card X = k}. set_mset (mset_set X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>{X. X \<subseteq> A \<and> card X = k}. set_mset (mset_set X) = X
[PROOF STEP]
using \<open>finite A\<close> rev_finite_subset[of A]
[PROOF STATE]
proof (prove)
using this:
finite A
\<lbrakk>finite A; ?A \<subseteq> A\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. \<forall>X\<in>{X. X \<subseteq> A \<and> card X = k}. set_mset (mset_set X) = X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>{X. X \<subseteq> A \<and> card X = k}. set_mset (mset_set X) = X

goal (3 subgoals):
 1. \<forall>a'\<in>{M. M \<subseteq># mset_set A \<and> size M = k}. mset_set (set_mset a') = a'
 2. mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. M \<subseteq># mset_set A \<and> size M = k}
 3. set_mset ` {M. M \<subseteq># mset_set A \<and> size M = k} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
show "\<forall>M\<in>{M. M \<subseteq># mset_set A \<and> size M = k}. mset_set (set_mset M) = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>M\<in>{M. M \<subseteq># mset_set A \<and> size M = k}. mset_set (set_mset M) = M
[PROOF STEP]
by (auto simp add: mset_set_set_mset)
[PROOF STATE]
proof (state)
this:
\<forall>M\<in>{M. M \<subseteq># mset_set A \<and> size M = k}. mset_set (set_mset M) = M

goal (2 subgoals):
 1. mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. M \<subseteq># mset_set A \<and> size M = k}
 2. set_mset ` {M. M \<subseteq># mset_set A \<and> size M = k} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
show "mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. M \<subseteq># mset_set A \<and> size M = k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. M \<subseteq># mset_set A \<and> size M = k}
[PROOF STEP]
using \<open>finite A\<close> rev_finite_subset[of A]
[PROOF STATE]
proof (prove)
using this:
finite A
\<lbrakk>finite A; ?A \<subseteq> A\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. M \<subseteq># mset_set A \<and> size M = k}
[PROOF STEP]
by (auto simp add: mset_set_subseteq_mset_set)
[PROOF STATE]
proof (state)
this:
mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. M \<subseteq># mset_set A \<and> size M = k}

goal (1 subgoal):
 1. set_mset ` {M. M \<subseteq># mset_set A \<and> size M = k} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
show "set_mset ` {M. M \<subseteq># mset_set A \<and> size M = k} \<subseteq> {X. X \<subseteq> A \<and> card X = k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_mset ` {M. M \<subseteq># mset_set A \<and> size M = k} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
using assms mset_subset_eqD card_set_mset
[PROOF STATE]
proof (prove)
using this:
finite A
\<lbrakk>?A \<subseteq># ?B; ?x \<in># ?A\<rbrakk> \<Longrightarrow> ?x \<in># ?B
?M \<subseteq># mset_set ?A \<Longrightarrow> card (set_mset ?M) = size ?M

goal (1 subgoal):
 1. set_mset ` {M. M \<subseteq># mset_set A \<and> size M = k} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set_mset ` {M. M \<subseteq># mset_set A \<and> size M = k} \<subseteq> {X. X \<subseteq> A \<and> card X = k}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_betw_mset_set_card':
  assumes "finite A"
  shows "bij_betw mset_set {X. X \<subseteq> A \<and> card X = k} {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw mset_set {X. X \<subseteq> A \<and> card X = k} {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}
[PROOF STEP]
proof (rule bij_betw_byWitness[where f'="set_mset"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>a\<in>{X. X \<subseteq> A \<and> card X = k}. set_mset (mset_set a) = a
 2. \<forall>a'\<in>{M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}. mset_set (set_mset a') = a'
 3. mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}
 4. set_mset ` {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
show "\<forall>X\<in>{X. X \<subseteq> A \<and> card X = k}. set_mset (mset_set X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>{X. X \<subseteq> A \<and> card X = k}. set_mset (mset_set X) = X
[PROOF STEP]
using \<open>finite A\<close> rev_finite_subset[of A]
[PROOF STATE]
proof (prove)
using this:
finite A
\<lbrakk>finite A; ?A \<subseteq> A\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. \<forall>X\<in>{X. X \<subseteq> A \<and> card X = k}. set_mset (mset_set X) = X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>X\<in>{X. X \<subseteq> A \<and> card X = k}. set_mset (mset_set X) = X

goal (3 subgoals):
 1. \<forall>a'\<in>{M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}. mset_set (set_mset a') = a'
 2. mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}
 3. set_mset ` {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
show "\<forall>M\<in>{M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}. mset_set (set_mset M) = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>M\<in>{M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}. mset_set (set_mset M) = M
[PROOF STEP]
by (auto simp add: mset_set_set_mset')
[PROOF STATE]
proof (state)
this:
\<forall>M\<in>{M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}. mset_set (set_mset M) = M

goal (2 subgoals):
 1. mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}
 2. set_mset ` {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
show "mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}
[PROOF STEP]
using \<open>finite A\<close> rev_finite_subset[of A]
[PROOF STATE]
proof (prove)
using this:
finite A
\<lbrakk>finite A; ?A \<subseteq> A\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}
[PROOF STEP]
by (auto simp add: count_mset_set_leq')
[PROOF STATE]
proof (state)
this:
mset_set ` {X. X \<subseteq> A \<and> card X = k} \<subseteq> {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)}

goal (1 subgoal):
 1. set_mset ` {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
show "set_mset ` {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} \<subseteq> {X. X \<subseteq> A \<and> card X = k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_mset ` {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
by (auto simp add: card_set_mset')
[PROOF STATE]
proof (state)
this:
set_mset ` {M. set_mset M \<subseteq> A \<and> size M = k \<and> (\<forall>x. count M x \<le> 1)} \<subseteq> {X. X \<subseteq> A \<and> card X = k}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_injective_functions_domain_permutation:
  assumes "finite A" "finite B"
  shows "card ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) = card B choose card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) = card B choose card A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) = card B choose card A
[PROOF STEP]
have "bij_betw (subset_of A) ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) {X. X \<subseteq> B \<and> card X = card A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (subset_of A) ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) {X. X \<subseteq> B \<and> card X = card A}
[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 (subset_of A) ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) {X. X \<subseteq> B \<and> card X = card A}
[PROOF STEP]
by (rule bij_betw_subset_of)
[PROOF STATE]
proof (state)
this:
bij_betw (subset_of A) ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) {X. X \<subseteq> B \<and> card X = card A}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) = card B choose card A
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
bij_betw (subset_of A) ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) {X. X \<subseteq> B \<and> card X = card A}
[PROOF STEP]
have "card ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) = card {X. X \<subseteq> B \<and> card X = card A}"
[PROOF STATE]
proof (prove)
using this:
bij_betw (subset_of A) ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) {X. X \<subseteq> B \<and> card X = card A}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) = card {X. X \<subseteq> B \<and> card X = card A}
[PROOF STEP]
by (rule bij_betw_same_card)
[PROOF STATE]
proof (state)
this:
card ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) = card {X. X \<subseteq> B \<and> card X = card A}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) = card B choose card A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) = card {X. X \<subseteq> B \<and> card X = card A}

goal (1 subgoal):
 1. card ({f \<in> A \<rightarrow>\<^sub>E B. inj_on f A} // domain_permutation A B) = card B choose card A
[PROOF STEP]
have "card {X. X \<subseteq> B \<and> card X = card A} = card B choose card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {X. X \<subseteq> B \<and> card X = card A} = card B choose card A
[PROOF STEP]
using \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
finite B

goal (1 subgoal):
 1. card {X. X \<subseteq> B \<and> card X = card A} = card B choose card A
[PROOF STEP]
by (rule n_subsets)
[PROOF STATE]
proof (state)
this:
card {X. X \<subseteq> B \<and> card X = card A} = card B choose card A

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_multiset_only_sets:
  assumes "finite A"
  shows "card {M. M \<subseteq># mset_set A \<and> size M = k} = card A choose k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {M. M \<subseteq># mset_set A \<and> size M = k} = card A choose k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {M. M \<subseteq># mset_set A \<and> size M = k} = card A choose k
[PROOF STEP]
have "bij_betw mset_set {X. X \<subseteq> A \<and> card X = k} {M. M \<subseteq># mset_set A \<and> size M = k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw mset_set {X. X \<subseteq> A \<and> card X = k} {M. M \<subseteq># mset_set A \<and> size M = k}
[PROOF STEP]
using \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. bij_betw mset_set {X. X \<subseteq> A \<and> card X = k} {M. M \<subseteq># mset_set A \<and> size M = k}
[PROOF STEP]
by (rule bij_betw_mset_set_card)
[PROOF STATE]
proof (state)
this:
bij_betw mset_set {X. X \<subseteq> A \<and> card X = k} {M. M \<subseteq># mset_set A \<and> size M = k}

goal (1 subgoal):
 1. card {M. M \<subseteq># mset_set A \<and> size M = k} = card A choose k
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
bij_betw mset_set {X. X \<subseteq> A \<and> card X = k} {M. M \<subseteq># mset_set A \<and> size M = k}
[PROOF STEP]
have "card {M. M \<subseteq># mset_set A \<and> size M = k} = card {X. X \<subseteq> A \<and> card X = k}"
[PROOF STATE]
proof (prove)
using this:
bij_betw mset_set {X. X \<subseteq> A \<and> card X = k} {M. M \<subseteq># mset_set A \<and> size M = k}

goal (1 subgoal):
 1. card {M. M \<subseteq># mset_set A \<and> size M = k} = card {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
by (simp add: bij_betw_same_card)
[PROOF STATE]
proof (state)
this:
card {M. M \<subseteq># mset_set A \<and> size M = k} = card {X. X \<subseteq> A \<and> card X = k}

goal (1 subgoal):
 1. card {M. M \<subseteq># mset_set A \<and> size M = k} = card A choose k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {M. M \<subseteq># mset_set A \<and> size M = k} = card {X. X \<subseteq> A \<and> card X = k}

goal (1 subgoal):
 1. card {M. M \<subseteq># mset_set A \<and> size M = k} = card A choose k
[PROOF STEP]
have " card {X. X \<subseteq> A \<and> card X = k} = card A choose k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {X. X \<subseteq> A \<and> card X = k} = card A choose k
[PROOF STEP]
using \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. card {X. X \<subseteq> A \<and> card X = k} = card A choose k
[PROOF STEP]
by (rule n_subsets)
[PROOF STATE]
proof (state)
this:
card {X. X \<subseteq> A \<and> card X = k} = card A choose k

goal (1 subgoal):
 1. card {M. M \<subseteq># mset_set A \<and> size M = k} = card A choose k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card {M. M \<subseteq># mset_set A \<and> size M = k} = card A choose k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card {M. M \<subseteq># mset_set A \<and> size M = k} = card A choose k

goal (1 subgoal):
 1. card {M. M \<subseteq># mset_set A \<and> size M = k} = card A choose k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
card {M. M \<subseteq># mset_set A \<and> size M = k} = card A choose k

goal:
No subgoals!
[PROOF STEP]
qed