# Theory Replacement_Lepoll

section‹Lambda-replacements required for cardinal inequalities›

theory Replacement_Lepoll
imports
ZF_Library_Relative
begin

definition
lepoll_assumptions1 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
"lepoll_assumptions1(M,A,F,S,fa,K,x,f,r)  xS. strong_replacement(M, λy z. y  F(A, x)  z = {x, y})"

definition
lepoll_assumptions2 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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 :: "[io,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. xA'. y = x, μ i. x  if_range_F_else_F(F(A),b,f,i))"
and
mem_F_bound:"x c. xF(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 "xX. (μ 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 "xX"
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 "cX  c  range(f)  c  U(A)"
unfolding if_range_F_else_F_def if_range_F_def by (cases "crange(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 "cX  c  range(f)  cU(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. xA'. 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)" "xX" "(μ 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)  {}"]) 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. xA'. y = x, μ i. x  if_range_F_else_F(F(A),b,f,i))"
"separation(M,Ord)"
and
types:"M(A)" "M(f)"
and
"b0"
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 b0
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. xA'. 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 "xX. (μ i. x  if_range_F_else_F(F(A),b,f,i))
Pow⇗M⇖((X  range(f)  {domain(x). xA}  {restrict(x,r'). xA}  domain(A)  range(A)  A))" if "M(X)" for X
proof
fix x
assume "xX"
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). xA}  {restrict(x,r'). xA}  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 "cX  crange(f)  (xA. c = domain(x))  (xA. c = restrict(x,r'))  c  domain(A)  c  range(A)  (xA. cx)" by auto
next
case False
fix c
assume "x  F(A, c)"
then
show "cX  crange(f)  (xA. c = domain(x))  (xA. c = restrict(x,r'))  c  domain(A)  c  range(A)  (xA. cx)"
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). xA}  {restrict(x,r'). xA}  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
― ‹Here b is a Boolean.›
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 _ _ ])
(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 "irange(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 _ _ ])
(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 _ _ ], 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 ― ‹localeM_replacement_lepoll

end