Theory Ordinals_In_MG

sectionOrdinals in generic extensions
theory Ordinals_In_MG
  imports
    Forcing_Theorems
begin

context G_generic1
begin

lemma rank_val: "rank(val(G,x))  rank(x)" (is "?Q(x)")
proof (induct rule:ed_induction[of ?Q])
  case (1 x)
  have "val(G,x) = {val(G,u). u{tdomain(x). pG . t,px }}"
    using def_val[of G x] by auto
  then
  have "rank(val(G,x)) = (u{tdomain(x). pG . t,px }. succ(rank(val(G,u))))"
    using rank[of "val(G,x)"] by simp
  moreover
  have "succ(rank(val(G, y)))  rank(x)" if "ed(y, x)" for y
    using 1[OF that] rank_ed[OF that] by (auto intro:lt_trans1)
  moreover from this
  have "(u{tdomain(x). pG . t,px }. succ(rank(val(G,u))))  rank(x)"
    by (rule_tac UN_least_le) (auto)
  ultimately
  show ?case
    by simp
qed

lemma Ord_MG_iff:
  assumes "Ord(α)"
  shows "α  M  α  M[G]"
proof
  show "α  M[G]" if "α  M"
    using M_subset_MG[OF one_in_G] that ..
next
  assume "α  M[G]"
  then
  obtain x where "xM" "val(G,x) = α"
    using GenExtD by auto
  then
  have "rank(α)  rank(x)"
    using rank_val by blast
  with assms
  have "α  rank(x)"
    using rank_of_Ord by simp
  then
  have "α  succ(rank(x))"
    using ltD by simp
  with xM
  show "α  M"
    using cons_closed transitivity[of α "succ(rank(x))"] rank_closed
    unfolding succ_def by simp
qed

end ― ‹localeG_generic1

end