[STATEMENT]
lemma bij_finite_ground_subst_exists:
  assumes "finite (S::'v set)" "infinite (U::('f,'v) term set)" "ground U"
  shows "\<exists>\<sigma>::('f,'v) subst. subst_domain \<sigma> = S
                          \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>)
                          \<and> subst_range \<sigma> \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
obtain T' where "T' \<subseteq> U" "card T' = card S" "finite T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>T' \<subseteq> U; card T' = card S; finite T'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms(2) finite_Diff2 infinite_arbitrarily_large)
[PROOF STATE]
proof (state)
this:
T' \<subseteq> U
card T' = card S
finite T'

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T' \<subseteq> U
card T' = card S
finite T'
[PROOF STEP]
obtain f::"'v \<Rightarrow> ('f,'v) term" where f_bij: "bij_betw f S T'"
[PROOF STATE]
proof (prove)
using this:
T' \<subseteq> U
card T' = card S
finite T'

goal (1 subgoal):
 1. (\<And>f. bij_betw f S T' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_same_card_bij[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
T' \<subseteq> U
card T' = card S
finite T'
\<lbrakk>finite ?B; card S = card ?B\<rbrakk> \<Longrightarrow> \<exists>h. bij_betw h S ?B

goal (1 subgoal):
 1. (\<And>f. bij_betw f S T' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
bij_betw f S T'

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
hence *: "\<And>v. v \<in> S \<Longrightarrow> f v \<noteq> Var v"
[PROOF STATE]
proof (prove)
using this:
bij_betw f S T'

goal (1 subgoal):
 1. \<And>v. v \<in> S \<Longrightarrow> f v \<noteq> Var v
[PROOF STEP]
using \<open>ground U\<close> \<open>T' \<subseteq> U\<close> bij_betwE
[PROOF STATE]
proof (prove)
using this:
bij_betw f S T'
ground U
T' \<subseteq> U
bij_betw ?f ?A ?B \<Longrightarrow> \<forall>a\<in>?A. ?f a \<in> ?B

goal (1 subgoal):
 1. \<And>v. v \<in> S \<Longrightarrow> f v \<noteq> Var v
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?v \<in> S \<Longrightarrow> f ?v \<noteq> Var ?v

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
let ?\<sigma> = "\<lambda>v. if v \<in> S then f v else Var v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
have "subst_domain ?\<sigma> = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subst_domain (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> S
 2. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
show "subst_domain ?\<sigma> \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_domain (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> S
[PROOF STEP]
by (auto simp add: subst_domain_def)
[PROOF STATE]
proof (state)
this:
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> S

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> S

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
assume "v \<in> S" "v \<notin> subst_domain ?\<sigma>"
[PROOF STATE]
proof (state)
this:
v \<in> S
v \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
hence "f v = Var v"
[PROOF STATE]
proof (prove)
using this:
v \<in> S
v \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)

goal (1 subgoal):
 1. f v = Var v
[PROOF STEP]
by (simp add: subst_domain_def)
[PROOF STATE]
proof (state)
this:
f v = Var v

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
f v = Var v

goal (1 subgoal):
 1. False
[PROOF STEP]
using *[OF \<open>v \<in> S\<close>]
[PROOF STATE]
proof (prove)
using this:
f v = Var v
f v \<noteq> Var v

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

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v2 \<in> S; ?v2 \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
thus "S \<subseteq> subst_domain ?\<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v2 \<in> S; ?v2 \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
hence "\<And>v w. \<lbrakk>v \<in> subst_domain ?\<sigma>; w \<notin> subst_domain ?\<sigma>\<rbrakk> \<Longrightarrow> ?\<sigma> w \<noteq> ?\<sigma> v"
[PROOF STATE]
proof (prove)
using this:
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if w \<in> S then f w else Var w) \<noteq> (if v \<in> S then f v else Var v)
[PROOF STEP]
using \<open>ground U\<close> bij_betwE[OF f_bij] set_rev_mp[OF _ \<open>T' \<subseteq> U\<close>]
[PROOF STATE]
proof (prove)
using this:
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S
ground U
\<forall>a\<in>S. f a \<in> T'
?c \<in> T' \<Longrightarrow> ?c \<in> U

goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if w \<in> S then f w else Var w) \<noteq> (if v \<in> S then f v else Var v)
[PROOF STEP]
by (metis (no_types, lifting) UN_iff empty_iff vars_iff_subterm_or_eq fv\<^sub>s\<^sub>e\<^sub>t.simps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); ?w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if ?w \<in> S then f ?w else Var ?w) \<noteq> (if ?v \<in> S then f ?v else Var ?v)

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
hence "inj_on ?\<sigma> (subst_domain ?\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); ?w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if ?w \<in> S then f ?w else Var ?w) \<noteq> (if ?v \<in> S then f ?v else Var ?v)

goal (1 subgoal):
 1. inj_on (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v))
[PROOF STEP]
using f_bij \<open>subst_domain ?\<sigma> = S\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); ?w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if ?w \<in> S then f ?w else Var ?w) \<noteq> (if ?v \<in> S then f ?v else Var ?v)
bij_betw f S T'
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. inj_on (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v))
[PROOF STEP]
unfolding bij_betw_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); ?w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if ?w \<in> S then f ?w else Var ?w) \<noteq> (if ?v \<in> S then f ?v else Var ?v)
(\<forall>x\<in>S. \<forall>y\<in>S. f x = f y \<longrightarrow> x = y) \<and> f ` S = T'
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. \<forall>x\<in>subst_domain (\<lambda>v. if v \<in> S then f v else Var v). \<forall>y\<in>subst_domain (\<lambda>v. if v \<in> S then f v else Var v). (if x \<in> S then f x else Var x) = (if y \<in> S then f y else Var y) \<longrightarrow> x = y
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v))

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
hence "bij_betw ?\<sigma> (subst_domain ?\<sigma>) (subst_range ?\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v))

goal (1 subgoal):
 1. bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))
[PROOF STEP]
using inj_on_imp_bij_betw[of ?\<sigma>]
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v))
inj_on (\<lambda>v. if v \<in> S then f v else Var v) ?A \<Longrightarrow> bij_betw (\<lambda>v. if v \<in> S then f v else Var v) ?A ((\<lambda>v. if v \<in> S then f v else Var v) ` ?A)

goal (1 subgoal):
 1. bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
have "subst_range ?\<sigma> = T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'
[PROOF STEP]
using \<open>bij_betw f S T'\<close> \<open>subst_domain ?\<sigma> = S\<close>
[PROOF STATE]
proof (prove)
using this:
bij_betw f S T'
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
using this:
inj_on f S \<and> f ` S = T'
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
hence "subst_range ?\<sigma> \<subseteq> U"
[PROOF STATE]
proof (prove)
using this:
subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'

goal (1 subgoal):
 1. subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U
[PROOF STEP]
using \<open>T' \<subseteq> U\<close>
[PROOF STATE]
proof (prove)
using this:
subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'
T' \<subseteq> U

goal (1 subgoal):
 1. subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))
subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))
subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
using \<open>subst_domain ?\<sigma> = S\<close>
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))
subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
by (metis (lifting))
[PROOF STATE]
proof (state)
this:
\<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U

goal:
No subgoals!
[PROOF STEP]
qed