Theory Least

section‹The binder termLeast
theory Least
  imports
    Names

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 :: "[io,io,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)  bi ¬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  qformula  least_fm(q,i)  formula"
  unfolding least_fm_def
  by simp

(* Refactorize Formula and Relative to include the following three lemmas *)
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) ; 0A
     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); 0A
    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: "aM  least(##M, λx. xM  Q(x),a)  least(##M,Q,a)"
  unfolding least_def by simp

(* Better to have this in M_basic or similar *)
lemma (in M_ctm) unique_least: "aM  bM  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 termLeast

lemma least_abs:
  assumes "x. Q(x)  M(x)" "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 x. Q(x)  M(x)
  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 x. Q(x)  M(x)
  have "Ord(b)  b  a  ¬ Q(b)" for b
    by blast
  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)  M(x)"
  shows "M(μ x. Q(x))"
  using assms LeastI[of Q] Least_0 by (cases "(i. Ord(i)  Q(i))", auto)

end (* M_trivial *)

end