section‹The binder \<^term>‹Least››
theory Least
imports
"Forcing_Data"
"Internalizations"
begin
text‹We have some basic results on the least ordinal satisfying
a predicate.›
lemma Least_Ord: "(μ α. R(α)) = (μ α. Ord(α) ∧ R(α))"
unfolding Least_def by (simp add:lt_Ord)
lemma Ord_Least_cong:
assumes "⋀y. Ord(y) ⟹ R(y) ⟷ Q(y)"
shows "(μ α. R(α)) = (μ α. Q(α))"
proof -
from assms
have "(μ α. Ord(α) ∧ R(α)) = (μ α. Ord(α) ∧ Q(α))"
by simp
then
show ?thesis using Least_Ord by simp
qed
definition
least :: "[i⇒o,i⇒o,i] ⇒ o" where
"least(M,Q,i) ≡ ordinal(M,i) ∧ (
(empty(M,i) ∧ (∀b[M]. ordinal(M,b) ⟶ ¬Q(b)))
∨ (Q(i) ∧ (∀b[M]. ordinal(M,b) ∧ b∈i⟶ ¬Q(b))))"
definition
least_fm :: "[i,i] ⇒ i" where
"least_fm(q,i) ≡ And(ordinal_fm(i),
Or(And(empty_fm(i),Forall(Implies(ordinal_fm(0),Neg(q)))),
And(Exists(And(q,Equal(0,succ(i)))),
Forall(Implies(And(ordinal_fm(0),Member(0,succ(i))),Neg(q))))))"
lemma least_fm_type[TC] :"i ∈ nat ⟹ q∈formula ⟹ least_fm(q,i) ∈ formula"
unfolding least_fm_def
by simp
lemmas basic_fm_simps = sats_subset_fm' sats_transset_fm' sats_ordinal_fm'
lemma sats_least_fm :
assumes p_iff_sats:
"⋀a. a ∈ A ⟹ P(a) ⟷ sats(A, p, Cons(a, env))"
shows
"⟦y ∈ nat; env ∈ list(A) ; 0∈A⟧
⟹ sats(A, least_fm(p,y), env) ⟷
least(##A, P, nth(y,env))"
using nth_closed p_iff_sats unfolding least_def least_fm_def
by (simp add:basic_fm_simps)
lemma least_iff_sats:
assumes is_Q_iff_sats:
"⋀a. a ∈ A ⟹ is_Q(a) ⟷ sats(A, q, Cons(a,env))"
shows
"⟦nth(j,env) = y; j ∈ nat; env ∈ list(A); 0∈A⟧
⟹ least(##A, is_Q, y) ⟷ sats(A, least_fm(q,j), env)"
using sats_least_fm [OF is_Q_iff_sats, of j , symmetric]
by simp
lemma least_conj: "a∈M ⟹ least(##M, λx. x∈M ∧ Q(x),a) ⟷ least(##M,Q,a)"
unfolding least_def by simp
lemma (in M_ctm) unique_least: "a∈M ⟹ b∈M ⟹ least(##M,Q,a) ⟹ least(##M,Q,b) ⟹ a=b"
unfolding least_def
by (auto, erule_tac i=a and j=b in Ord_linear_lt; (drule ltD | simp); auto intro:Ord_in_Ord)
context M_trivial
begin
subsection‹Absoluteness and closure under \<^term>‹Least››
lemma least_abs:
assumes "⋀x. Q(x) ⟹ Ord(x) ⟹ ∃y[M]. Q(y) ∧ Ord(y)" "M(a)"
shows "least(M,Q,a) ⟷ a = (μ x. Q(x))"
unfolding least_def
proof (cases "∀b[M]. Ord(b) ⟶ ¬ Q(b)"; intro iffI; simp add:assms)
case True
with assms
have "¬ (∃i. Ord(i) ∧ Q(i)) " by blast
then
show "0 =(μ x. Q(x))" using Least_0 by simp
then
show "ordinal(M, μ x. Q(x)) ∧ (empty(M, Least(Q)) ∨ Q(Least(Q)))"
by simp
next
assume "∃b[M]. Ord(b) ∧ Q(b)"
then
obtain i where "M(i)" "Ord(i)" "Q(i)" by blast
assume "a = (μ x. Q(x))"
moreover
note ‹M(a)›
moreover from ‹Q(i)› ‹Ord(i)›
have "Q(μ x. Q(x))" (is ?G)
by (blast intro:LeastI)
moreover
have "(∀b[M]. Ord(b) ∧ b ∈ (μ x. Q(x)) ⟶ ¬ Q(b))" (is "?H")
using less_LeastE[of Q _ False]
by (auto, drule_tac ltI, simp, blast)
ultimately
show "ordinal(M, μ x. Q(x)) ∧ (empty(M, μ x. Q(x)) ∧ (∀b[M]. Ord(b) ⟶ ¬ Q(b)) ∨ ?G ∧ ?H)"
by simp
next
assume 1:"∃b[M]. Ord(b) ∧ Q(b)"
then
obtain i where "M(i)" "Ord(i)" "Q(i)" by blast
assume "Ord(a) ∧ (a = 0 ∧ (∀b[M]. Ord(b) ⟶ ¬ Q(b)) ∨ Q(a) ∧ (∀b[M]. Ord(b) ∧ b ∈ a ⟶ ¬ Q(b)))"
with 1
have "Ord(a)" "Q(a)" "∀b[M]. Ord(b) ∧ b ∈ a ⟶ ¬ Q(b)"
by blast+
moreover from this and assms
have "Ord(b) ⟹ b ∈ a ⟹ ¬ Q(b)" for b
by (auto dest:transM)
moreover from this and ‹Ord(a)›
have "b < a ⟹ ¬ Q(b)" for b
unfolding lt_def using Ord_in_Ord by blast
ultimately
show "a = (μ x. Q(x))"
using Least_equality by simp
qed
lemma Least_closed:
assumes "⋀x. Q(x) ⟹ Ord(x) ⟹ ∃y[M]. Q(y) ∧ Ord(y)"
shows "M(μ x. Q(x))"
using assms Least_le[of Q] Least_0[of Q]
by (cases "(∃i[M]. Ord(i) ∧ Q(i))") (force dest:transM ltD)+
text‹Older, easier to apply versions (with a simpler assumption
on \<^term>‹Q›).›
lemma least_abs':
assumes "⋀x. Q(x) ⟹ M(x)" "M(a)"
shows "least(M,Q,a) ⟷ a = (μ x. Q(x))"
using assms least_abs[of Q] by auto
lemma Least_closed':
assumes "⋀x. Q(x) ⟹ M(x)"
shows "M(μ x. Q(x))"
using assms Least_closed[of Q] by auto
end
end