Theory Replacement_Lepoll
section‹Lambda-replacements required for cardinal inequalities›
theory Replacement_Lepoll
imports
ZF_Library_Relative
begin
definition
lepoll_assumptions1 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions1(M,A,F,S,fa,K,x,f,r) ≡ ∀x∈S. strong_replacement(M, λy z. y ∈ F(A, x) ∧ z = {⟨x, y⟩})"
definition
lepoll_assumptions2 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions2(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement(M, λx z. z = Sigfun(x, F(A)))"
definition
lepoll_assumptions3 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions3(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement(M, λx y. y = F(A, x))"
definition
lepoll_assumptions4 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions4(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement(M, λx y. y = ⟨x, minimum(r, F(A, x))⟩)"
definition
lepoll_assumptions5 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions5(M,A,F,S,fa,K,x,f,r) ≡
strong_replacement(M, λx y. y = ⟨x, μ i. x ∈ F(A, i), f ` (μ i. x ∈ F(A, i)) ` x⟩)"
definition
lepoll_assumptions6 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions6(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement(M, λy z. y ∈ inj⇗M⇖(F(A, x),S) ∧ z = {⟨x, y⟩})"
definition
lepoll_assumptions7 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions7(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement(M, λx y. y = inj⇗M⇖(F(A, x),S))"
definition
lepoll_assumptions8 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions8(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement(M, λx z. z = Sigfun(x, λi. inj⇗M⇖(F(A, i),S)))"
definition
lepoll_assumptions9 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions9(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement(M, λx y. y = ⟨x, minimum(r, inj⇗M⇖(F(A, x),S))⟩)"
definition
lepoll_assumptions10 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions10(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement
(M, λx z. z = Sigfun(x, λk. if k ∈ range(f) then F(A, converse(f) ` k) else 0))"
definition
lepoll_assumptions11 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions11(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement(M, λx y. y = (if x ∈ range(f) then F(A, converse(f) ` x) else 0))"
definition
lepoll_assumptions12 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions12(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement(M, λy z. y ∈ F(A, converse(f) ` x) ∧ z = {⟨x, y⟩})"
definition
lepoll_assumptions13 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions13(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement
(M, λx y. y = ⟨x, minimum(r, if x ∈ range(f) then F(A,converse(f) ` x) else 0)⟩)"
definition
lepoll_assumptions14 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions14(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement
(M, λx y. y = ⟨x, μ i. x ∈ (if i ∈ range(f) then F(A, converse(f) ` i) else 0),
fa ` (μ i. x ∈ (if i ∈ range(f) then F(A, converse(f) ` i) else 0)) ` x⟩)"
definition
lepoll_assumptions15 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions15(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement
(M, λy z. y ∈ inj⇗M⇖(if x ∈ range(f) then F(A, converse(f) ` x) else 0,K) ∧ z = {⟨x, y⟩})"
definition
lepoll_assumptions16 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions16(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement(M, λx y. y = inj⇗M⇖(if x ∈ range(f) then F(A, converse(f) ` x) else 0,K))"
definition
lepoll_assumptions17 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions17(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement
(M, λx z. z = Sigfun(x, λi. inj⇗M⇖(if i ∈ range(f) then F(A, converse(f) ` i) else 0,K)))"
definition
lepoll_assumptions18 :: "[i⇒o,i,[i,i]⇒i,i,i,i,i,i,i] ⇒ o" where
"lepoll_assumptions18(M,A,F,S,fa,K,x,f,r) ≡ strong_replacement
(M, λx y. y = ⟨x, minimum(r, inj⇗M⇖(if x ∈ range(f) then F(A, converse(f) ` x) else 0,K))⟩)"
lemmas lepoll_assumptions_defs[simp] = lepoll_assumptions1_def
lepoll_assumptions2_def lepoll_assumptions3_def lepoll_assumptions4_def
lepoll_assumptions5_def lepoll_assumptions6_def lepoll_assumptions7_def
lepoll_assumptions8_def lepoll_assumptions9_def lepoll_assumptions10_def
lepoll_assumptions11_def lepoll_assumptions12_def lepoll_assumptions13_def
lepoll_assumptions14_def lepoll_assumptions15_def lepoll_assumptions16_def
lepoll_assumptions17_def lepoll_assumptions18_def
definition if_range_F where
[simp]: "if_range_F(H,f,i) ≡ if i ∈ range(f) then H(converse(f) ` i) else 0"
definition if_range_F_else_F where
"if_range_F_else_F(H,b,f,i) ≡ if b=0 then if_range_F(H,f,i) else H(i)"
lemma (in M_basic) lam_Least_assumption_general:
assumes
separations:
"∀A'[M]. separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(F(A),b,f,i)⟩)"
and
mem_F_bound:"⋀x c. x∈F(A,c) ⟹ c ∈ range(f) ∪ U(A)"
and
types:"M(A)" "M(b)" "M(f)" "M(U(A))"
shows "lam_replacement(M,λx . μ i. x ∈ if_range_F_else_F(F(A),b,f,i))"
proof -
have "∀x∈X. (μ i. x ∈ if_range_F_else_F(F(A),b,f,i)) ∈
Pow⇗M⇖(⋃(X ∪ range(f) ∪ U(A)))" if "M(X)" for X
proof
fix x
assume "x∈X"
moreover
note ‹M(X)›
moreover from calculation
have "M(x)" by (auto dest:transM)
moreover
note assms
ultimately
show "(μ i. x ∈ if_range_F_else_F(F(A),b,f,i)) ∈
Pow⇗M⇖(⋃(X ∪ range(f) ∪ U(A)))"
proof (rule_tac Least_in_Pow_rel_Union, cases "b=0", simp_all)
case True
fix c
assume asm:"x ∈ if_range_F_else_F(F(A), 0, f, c)"
with mem_F_bound
show "c∈X ∨ c ∈ range(f) ∨ c ∈ U(A)"
unfolding if_range_F_else_F_def if_range_F_def by (cases "c∈range(f)") auto
next
case False
fix c
assume "x ∈ if_range_F_else_F(F(A), b, f, c)"
with False mem_F_bound[of x c]
show "c∈X ∨ c ∈ range(f) ∨ c∈U(A)"
unfolding if_range_F_else_F_def if_range_F_def by auto
qed
qed
with assms
show ?thesis
using bounded_lam_replacement[of "λx.(μ i. x ∈ if_range_F_else_F(F(A),b,f,i))"
"λX. Pow⇗M⇖(⋃(X ∪ range(f) ∪ U(A)))"] by simp
qed
lemma (in M_basic) lam_Least_assumption_ifM_b0:
fixes F
defines "F ≡ λ_ x. if M(x) then x else 0"
assumes
separations:
"∀A'[M]. separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(F(A),0,f,i)⟩)"
and
types:"M(A)" "M(f)"
shows "lam_replacement(M,λx . μ i. x ∈ if_range_F_else_F(F(A),0,f,i))"
(is "lam_replacement(M,λx . Least(?P(x)))")
proof -
{
fix x X
assume "M(X)" "x∈X" "(μ i. ?P(x,i)) ≠ 0"
moreover from this
obtain m where "Ord(m)" "?P(x,m)"
using Least_0[of "?P(_)"] by auto
moreover
note assms
moreover
have "?P(x,i) ⟷ (M(converse(f) ` i) ∧ i ∈ range(f) ∧ x ∈ converse(f) ` i)" for i
unfolding F_def if_range_F_else_F_def if_range_F_def by auto
ultimately
have "(μ i. ?P(x,i)) ∈ range (f)"
unfolding F_def if_range_F_else_F_def if_range_F_def
by (rule_tac LeastI2) auto
}
with assms
show ?thesis
by (rule_tac bounded_lam_replacement[of _ "λX. range(f) ∪ {0}"]) auto
qed
lemma (in M_replacement) lam_Least_assumption_ifM_bnot0:
fixes F
defines "F ≡ λ_ x. if M(x) then x else 0"
assumes
lam_replacement_minimum:"lam_replacement(M, λp. minimum(fst(p),snd(p)))"
and
separations:
"∀A'[M]. separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(F(A),b,f,i)⟩)"
"separation(M,Ord)"
and
types:"M(A)" "M(f)"
and
"b≠0"
shows "lam_replacement(M,λx . μ i. x ∈ if_range_F_else_F(F(A),b,f,i))"
(is "lam_replacement(M,λx . Least(?P(x)))")
proof -
have "M(x) ⟹(μ i. (M(i) ⟶ x ∈ i) ∧ M(i)) = (if Ord(x) then succ(x) else 0)" for x
using Ord_in_Ord
apply (auto intro:Least_0, rule_tac Least_equality, simp_all)
by (frule lt_Ord) (auto dest:le_imp_not_lt[of _ x] intro:ltI[of x])
moreover
have "lam_replacement(M, λx. if Ord(x) then succ(x) else 0)"
using lam_replacement_if[OF _ _ separations(2)] lam_replacement_identity
lam_replacement_constant lam_replacement_hcomp lam_replacement_succ
by simp
moreover
note types ‹b≠0›
ultimately
show ?thesis
using lam_replacement_cong
unfolding F_def if_range_F_else_F_def if_range_F_def
by auto
qed
lemma (in M_replacement) lam_Least_assumption_drSR_Y:
fixes F r' D
defines "F ≡ drSR_Y(r',D)"
assumes "∀A'[M]. separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(F(A),b,f,i)⟩)"
"M(A)" "M(b)" "M(f)" "M(r')"
and
lam_replacement_minimum:"lam_replacement(M, λp. minimum(fst(p),snd(p)))"
shows "lam_replacement(M,λx . μ i. x ∈ if_range_F_else_F(F(A),b,f,i))"
proof -
from assms(2-)
have [simp]: "M(X) ⟹ M(X ∪ range(f) ∪ {domain(x) . x ∈ A})"
"M(r') ⟹ M(X) ⟹ M({restrict(x,r') . x ∈ A})"
for X r'
using lam_replacement_domain[THEN lam_replacement_imp_strong_replacement,
THEN RepFun_closed, of A]
lam_replacement_restrict'[THEN lam_replacement_imp_strong_replacement,
THEN RepFun_closed, of r' A] by (auto dest:transM)
have "∀x∈X. (μ i. x ∈ if_range_F_else_F(F(A),b,f,i)) ∈
Pow⇗M⇖(⋃(X ∪ range(f) ∪ {domain(x). x∈A} ∪ {restrict(x,r'). x∈A} ∪ domain(A) ∪ range(A) ∪ ⋃A))" if "M(X)" for X
proof
fix x
assume "x∈X"
moreover
note ‹M(X)›
moreover from calculation
have "M(x)" by (auto dest:transM)
moreover
note assms(2-)
ultimately
show "(μ i. x ∈ if_range_F_else_F(F(A),b,f,i)) ∈
Pow⇗M⇖(⋃(X ∪ range(f) ∪ {domain(x). x∈A} ∪ {restrict(x,r'). x∈A} ∪ domain(A) ∪ range(A) ∪ ⋃A))"
unfolding if_range_F_else_F_def if_range_F_def
proof (rule_tac Least_in_Pow_rel_Union, simp_all,cases "b=0", simp_all)
case True
fix c
assume asm:"x ∈ (if c ∈ range(f) then F(A, converse(f) ` c) else 0)"
then
show "c∈X ∨ c∈range(f) ∨ (∃x∈A. c = domain(x)) ∨ (∃x∈A. c = restrict(x,r')) ∨ c ∈ domain(A) ∨ c ∈ range(A) ∨ (∃x∈A. c∈x)" by auto
next
case False
fix c
assume "x ∈ F(A, c)"
then
show "c∈X ∨ c∈range(f) ∨ (∃x∈A. c = domain(x)) ∨ (∃x∈A. c = restrict(x,r')) ∨ c ∈ domain(A) ∨ c ∈ range(A) ∨ (∃x∈A. c∈x)"
using apply_0
by (cases "M(c)", auto simp:F_def drSR_Y_def dC_F_def)
qed
qed
with assms(2-)
show ?thesis
using bounded_lam_replacement[of "λx.(μ i. x ∈ if_range_F_else_F(F(A),b,f,i))"
"λX. Pow⇗M⇖(⋃(X ∪ range(f) ∪ {domain(x). x∈A} ∪ {restrict(x,r'). x∈A} ∪ domain(A) ∪ range(A) ∪ ⋃A))"] by simp
qed
locale M_replacement_lepoll = M_replacement + M_inj +
fixes F
assumes
F_type[simp]: "M(A) ⟹ ∀x[M]. M(F(A,x))"
and
lam_lepoll_assumption_F:"M(A) ⟹ lam_replacement(M,F(A))"
and
lam_Least_assumption:"M(A) ⟹ M(b) ⟹ M(f) ⟹
lam_replacement(M,λx . μ i. x ∈ if_range_F_else_F(F(A),b,f,i))"
and
F_args_closed: "M(A) ⟹ M(x) ⟹ x ∈ F(A,i) ⟹ M(i)"
and
lam_replacement_inj_rel:"lam_replacement(M, λp. inj⇗M⇖(fst(p),snd(p)))"
and
lam_replacement_minimum:"lam_replacement(M, λp. minimum(fst(p),snd(p)))"
begin
declare if_range_F_else_F_def[simp]
lemma lepoll_assumptions1:
assumes types[simp]:"M(A)" "M(S)"
shows "lepoll_assumptions1(M,A,F,S,fa,K,x,f,r)"
using strong_replacement_separation[OF lam_replacement_sing_const_id separation_in_constant]
transM[of _ S]
by simp
lemma lepoll_assumptions2:
assumes types[simp]:"M(A)" "M(S)"
shows "lepoll_assumptions2(M,A,F,S,fa,K,x,f,r)"
using lam_replacement_Sigfun lam_replacement_imp_strong_replacement
assms lam_lepoll_assumption_F
by simp
lemma lepoll_assumptions3:
assumes types[simp]:"M(A)"
shows "lepoll_assumptions3(M,A,F,S,fa,K,x,f,r)"
using lam_lepoll_assumption_F[THEN lam_replacement_imp_strong_replacement]
by simp
lemma lepoll_assumptions4:
assumes types[simp]:"M(A)" "M(r)"
shows "lepoll_assumptions4(M,A,F,S,fa,K,x,f,r)"
using lam_replacement_minimum lam_replacement_constant lam_lepoll_assumption_F
unfolding lepoll_assumptions_defs
lam_replacement_def[symmetric]
by (rule_tac lam_replacement_hcomp2[of _ _ minimum])
(force intro: lam_replacement_identity)+
lemma lam_Least_closed :
assumes "M(A)" "M(b)" "M(f)"
shows "∀x[M]. M(μ i. x ∈ if_range_F_else_F(F(A),b,f,i))"
proof -
have "x ∈ (if i ∈ range(f) then F(A, converse(f) ` i) else 0) ⟹ M(i)" for x i
proof (cases "i∈range(f)")
case True
with ‹M(f)›
show ?thesis by (auto dest:transM)
next
case False
moreover
assume "x ∈ (if i ∈ range(f) then F(A, converse(f) ` i) else 0)"
ultimately
show ?thesis
by auto
qed
with assms
show ?thesis
using F_args_closed[of A] unfolding if_range_F_else_F_def if_range_F_def
by (clarify, rule_tac Least_closed', cases "b=0") simp_all
qed
lemma lepoll_assumptions5:
assumes
types[simp]:"M(A)" "M(f)"
shows "lepoll_assumptions5(M,A,F,S,fa,K,x,f,r)"
using
lam_replacement_apply2[THEN [5] lam_replacement_hcomp2]
lam_replacement_hcomp[OF _ lam_replacement_apply[of f]]
lam_replacement_identity
lam_replacement_product lam_Least_closed[where b=1]
assms lam_Least_assumption[where b=1,OF ‹M(A)› _ ‹M(f)›]
unfolding lepoll_assumptions_defs
lam_replacement_def[symmetric]
by simp
lemma lepoll_assumptions6:
assumes types[simp]:"M(A)" "M(S)" "M(x)"
shows "lepoll_assumptions6(M,A,F,S,fa,K,x,f,r)"
using strong_replacement_separation[OF lam_replacement_sing_const_id separation_in_constant]
lam_replacement_inj_rel
by simp
lemma lepoll_assumptions7:
assumes types[simp]:"M(A)" "M(S)" "M(x)"
shows "lepoll_assumptions7(M,A,F,S,fa,K,x,f,r)"
using lam_replacement_constant lam_lepoll_assumption_F lam_replacement_inj_rel
unfolding lepoll_assumptions_defs
by (rule_tac lam_replacement_imp_strong_replacement)
(rule_tac lam_replacement_hcomp2[of _ _ "inj_rel(M)"], simp_all)
lemma lepoll_assumptions8:
assumes types[simp]:"M(A)" "M(S)"
shows "lepoll_assumptions8(M,A,F,S,fa,K,x,f,r)"
using lam_replacement_Sigfun lam_replacement_imp_strong_replacement
lam_replacement_inj_rel lam_replacement_constant
lam_replacement_hcomp2[of _ _ "inj_rel(M)",OF lam_lepoll_assumption_F[of A]]
by simp
lemma lepoll_assumptions9:
assumes types[simp]:"M(A)" "M(S)" "M(r)"
shows "lepoll_assumptions9(M,A,F,S,fa,K,x,f,r)"
using lam_replacement_minimum lam_replacement_constant lam_lepoll_assumption_F
lam_replacement_hcomp2[of _ _ "inj_rel(M)"] lam_replacement_inj_rel lepoll_assumptions4
unfolding lepoll_assumptions_defs lam_replacement_def[symmetric]
by (rule_tac lam_replacement_hcomp2[of _ _ minimum])
(force intro: lam_replacement_identity)+
lemma lepoll_assumptions10:
assumes types[simp]:"M(A)" "M(f)"
shows "lepoll_assumptions10(M,A,F,S,fa,K,x,f,r)"
using lam_replacement_Sigfun lam_replacement_imp_strong_replacement
lam_replacement_constant[OF nonempty]
lam_replacement_if[OF _ _ separation_in_constant]
lam_replacement_hcomp
lam_replacement_apply[OF converse_closed[OF ‹M(f)›]]
lam_lepoll_assumption_F[of A]
by simp
lemma lepoll_assumptions11:
assumes types[simp]:"M(A)" "M(f)"
shows "lepoll_assumptions11(M, A, F, S, fa, K, x, f, r)"
using lam_replacement_imp_strong_replacement
lam_replacement_if[OF _ _ separation_in_constant[of "range(f)"]]
lam_replacement_constant
lam_replacement_hcomp lam_replacement_apply
lam_lepoll_assumption_F
by simp
lemma lepoll_assumptions12:
assumes types[simp]:"M(A)" "M(x)" "M(f)"
shows "lepoll_assumptions12(M,A,F,S,fa,K,x,f,r)"
using strong_replacement_separation[OF lam_replacement_sing_const_id separation_in_constant]
by simp
lemma lepoll_assumptions13:
assumes types[simp]:"M(A)" "M(r)" "M(f)"
shows "lepoll_assumptions13(M,A,F,S,fa,K,x,f,r)"
using lam_replacement_constant[OF nonempty] lam_lepoll_assumption_F
lam_replacement_hcomp lam_replacement_apply
lam_replacement_hcomp2[OF lam_replacement_constant[OF ‹M(r)›]
lam_replacement_if[OF _ _ separation_in_constant[of "range(f)"]] _ _
lam_replacement_minimum] assms
unfolding lepoll_assumptions_defs
lam_replacement_def[symmetric]
by simp
lemma lepoll_assumptions14:
assumes types[simp]:"M(A)" "M(f)" "M(fa)"
shows "lepoll_assumptions14(M,A,F,S,fa,K,x,f,r)"
using
lam_replacement_apply2[THEN [5] lam_replacement_hcomp2]
lam_replacement_hcomp[OF _ lam_replacement_apply[of fa]]
lam_replacement_identity
lam_replacement_product lam_Least_closed[where b=0]
assms lam_Least_assumption[where b=0,OF ‹M(A)› _ ‹M(f)›]
unfolding lepoll_assumptions_defs
lam_replacement_def[symmetric]
by simp
lemma lepoll_assumptions15:
assumes types[simp]:"M(A)" "M(x)" "M(f)" "M(K)"
shows "lepoll_assumptions15(M,A,F,S,fa,K,x,f,r)"
using strong_replacement_separation[OF lam_replacement_sing_const_id separation_in_constant]
by simp
lemma lepoll_assumptions16:
assumes types[simp]:"M(A)" "M(f)" "M(K)"
shows "lepoll_assumptions16(M,A,F,S,fa,K,x,f,r)"
using lam_replacement_imp_strong_replacement
lam_replacement_inj_rel lam_replacement_constant
lam_replacement_hcomp2[of _ _ "inj_rel(M)"]
lam_replacement_constant[OF nonempty]
lam_replacement_if[OF _ _ separation_in_constant]
lam_replacement_hcomp
lam_replacement_apply[OF converse_closed[OF ‹M(f)›]]
lam_lepoll_assumption_F[of A]
by simp
lemma lepoll_assumptions17:
assumes types[simp]:"M(A)" "M(f)" "M(K)"
shows "lepoll_assumptions17(M,A,F,S,fa,K,x,f,r)"
using lam_replacement_Sigfun lam_replacement_imp_strong_replacement
lam_replacement_inj_rel lam_replacement_constant
lam_replacement_hcomp2[of _ _ "inj_rel(M)"]
lam_replacement_constant[OF nonempty]
lam_replacement_if[OF _ _ separation_in_constant]
lam_replacement_hcomp
lam_replacement_apply[OF converse_closed[OF ‹M(f)›]]
lam_lepoll_assumption_F[of A]
by simp
lemma lepoll_assumptions18:
assumes types[simp]:"M(A)" "M(K)" "M(f)" "M(r)"
shows "lepoll_assumptions18(M,A,F,S,fa,K,x,f,r)"
using lam_replacement_constant lam_replacement_inj_rel lam_lepoll_assumption_F
lam_replacement_minimum lam_replacement_identity lam_replacement_apply2 separation_in_constant
unfolding lepoll_assumptions18_def lam_replacement_def[symmetric]
by (rule_tac lam_replacement_hcomp2[of _ _ minimum], simp_all,
rule_tac lam_replacement_hcomp2[of _ _ "inj_rel(M)"], simp_all)
(rule_tac lam_replacement_if, rule_tac lam_replacement_hcomp[of _ "F(A)"],
rule_tac lam_replacement_hcomp2[of _ _ "(`)"], simp_all)
lemmas lepoll_assumptions = lepoll_assumptions1 lepoll_assumptions2
lepoll_assumptions3 lepoll_assumptions4 lepoll_assumptions5
lepoll_assumptions6 lepoll_assumptions7 lepoll_assumptions8
lepoll_assumptions9 lepoll_assumptions10 lepoll_assumptions11
lepoll_assumptions12 lepoll_assumptions13 lepoll_assumptions14
lepoll_assumptions15 lepoll_assumptions16
lepoll_assumptions17 lepoll_assumptions18
end
end