section‹The binder \<^term>‹Least›› theory Least imports "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 [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 context M_trivial begin subsection‹Uniqueness, absoluteness and closure under \<^term>‹Least›› lemma unique_least: assumes "M(a)" "M(b)" "least(M,Q,a)" "least(M,Q,b)" shows "a=b" proof - from assms have "Ord(a)" "Ord(b)" unfolding least_def by simp_all then consider (le) "a∈b" | "a=b" | (ge) "b∈a" using Ord_linear[OF ‹Ord(a)› ‹Ord(b)›] by auto then show ?thesis proof(cases) case le then show ?thesis using assms unfolding least_def by auto next case ge then show ?thesis using assms unfolding least_def by auto qed qed 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 ― ‹\<^locale>‹M_trivial›› end