Theory AOT_ExtendedRelationComprehension

theory AOT_ExtendedRelationComprehension
  imports AOT_RestrictedVariables
begin

section‹Extended Relation Comprehension›

text‹This theory depends on choosing extended models.›
interpretation AOT_ExtendedModel by (standard; auto)

text‹Auxiliary lemma: negations of denoting relations denote.›
AOT_theorem negation_denotes: ‹[λx φ{x}]↓ → [λx ¬φ{x}]↓›
proof(rule "→I")
  AOT_assume 0: ‹[λx φ{x}]↓›
  AOT_show ‹[λx ¬φ{x}]↓›
  proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show ‹[λx ¬[λx φ{x}]x]↓› by "cqt:2"
  next
    AOT_have ‹□[λx φ{x}]↓›
      using 0 "exist-nec"[THEN "→E"] by blast
    moreover AOT_have ‹□[λx φ{x}]↓ → □∀x (¬[λx φ{x}]x ≡ ¬φ{x})›
      by(rule RM; safe intro!: GEN "≡I" "→I" "β→C"(2) "β←C"(2) "cqt:2")
    ultimately AOT_show ‹□∀x (¬[λx φ{x}]x ≡ ¬φ{x})›
      using "→E" by blast
  qed
qed

text‹Auxiliary lemma: conjunctions of denoting relations denote.›
AOT_theorem conjunction_denotes: ‹[λx φ{x}]↓ & [λx ψ{x}]↓ → [λx φ{x} & ψ{x}]↓›
proof(rule "→I")
  AOT_assume 0: ‹[λx φ{x}]↓ & [λx ψ{x}]↓›
  AOT_show ‹[λx φ{x} & ψ{x}]↓›
  proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show ‹[λx [λx φ{x}]x & [λx ψ{x}]x]↓› by "cqt:2"
  next
    AOT_have ‹□([λx φ{x}]↓ & [λx ψ{x}]↓)›
      using 0 "exist-nec"[THEN "→E"] "&E"
            "KBasic:3" "df-simplify:2" "intro-elim:3:b" by blast
    moreover AOT_have
      ‹□([λx φ{x}]↓ & [λx ψ{x}]↓) → □∀x ([λx φ{x}]x & [λx ψ{x}]x ≡ φ{x} & ψ{x})›
      by(rule RM; auto intro!: GEN "≡I" "→I" "cqt:2" "&I"
                        intro: "β←C"
                         dest: "&E" "β→C")
    ultimately AOT_show ‹□∀x ([λx φ{x}]x & [λx ψ{x}]x ≡ φ{x} & ψ{x})›
      using "→E" by blast
  qed
qed

AOT_register_rigid_restricted_type
  Ordinary: ‹O!κ›
proof
  AOT_modally_strict {
    AOT_show ‹∃x O!x›
      by (meson "B◇" "T◇" "o-objects-exist:1" "→E")
  }
next
  AOT_modally_strict {
    AOT_show ‹O!κ → κ↓› for κ
      by (simp add: "→I" "cqt:5:a[1]"[axiom_inst, THEN "→E", THEN "&E"(2)])
  }
next
  AOT_modally_strict {
    AOT_show ‹∀α(O!α → □O!α)›
      by (simp add: GEN "oa-facts:1")
  }
qed

AOT_register_variable_names
  Ordinary: u v r t s

text‹In PLM this is defined in the Natural Numbers chapter,
     but since it is helpful for stating the comprehension principles,
     we already define it here.›
AOT_define eqE :: ‹τ ⇒ τ ⇒ φ› (infixl ‹≡⇩E› 50)
  eqE: ‹F ≡⇩E G ≡⇩d⇩f F↓ & G↓ & ∀u ([F]u ≡ [G]u)›

text‹Derive existence claims about relations from the axioms.›
AOT_theorem denotes_all: ‹[λx ∀G (□G ≡⇩E F → x[G])]↓›
    and denotes_all_neg: ‹[λx ∀G (□G ≡⇩E F → ¬x[G])]↓›
proof -
  AOT_have Aux: ‹∀F (□F ≡⇩E G → (x[F] ≡ x[G])), ¬(x[G] ≡ y[G])
    ❙⊢⇩□ ∃F([F]x & ¬[F]y)› for x y G
  proof -
    AOT_modally_strict {
    AOT_assume 0: ‹∀F (□F ≡⇩E G → (x[F] ≡ x[G]))›
    AOT_assume G_prop: ‹¬(x[G] ≡ y[G])›
    {
      AOT_assume ‹¬∃F([F]x & ¬[F]y)›
      AOT_hence 0: ‹∀F ¬([F]x & ¬[F]y)›
        by (metis "cqt-further:4" "→E")
      AOT_have ‹∀F ([F]x ≡ [F]y)›
      proof (rule GEN; rule "≡I"; rule "→I")
        fix F
        AOT_assume ‹[F]x›
        moreover AOT_have ‹¬([F]x & ¬[F]y)›
          using 0[THEN "∀E"(2)] by blast
        ultimately AOT_show ‹[F]y›
          by (metis "&I" "raa-cor:1") 
      next
        fix F
        AOT_assume ‹[F]y›
        AOT_hence ‹¬[λx ¬[F]x]y›
          by (metis "¬¬I" "β→C"(2))
        moreover AOT_have ‹¬([λx ¬[F]x]x & ¬[λx ¬[F]x]y)›
          apply (rule 0[THEN "∀E"(1)]) by "cqt:2[lambda]"
        ultimately AOT_have 1: ‹¬[λx ¬[F]x]x›
          by (metis "&I" "raa-cor:3")
        {
          AOT_assume ‹¬[F]x›
          AOT_hence ‹[λx ¬[F]x]x›
            by (auto intro!: "β←C"(1) "cqt:2")
          AOT_hence ‹p & ¬p› for p
            using 1 by (metis "raa-cor:3")
        }
        AOT_thus ‹[F]x› by (metis "raa-cor:1")
      qed
      AOT_hence ‹□∀F ([F]x ≡ [F]y)›
        using "ind-nec"[THEN "→E"] by blast
      AOT_hence ‹∀F □([F]x ≡ [F]y)›
        by (metis "CBF" "→E")
    } note indistI = this
    {
      AOT_assume G_prop: ‹x[G] & ¬y[G]›
      AOT_hence Ax: ‹A!x›
        using "&E"(1) "∃I"(2) "→E" "encoders-are-abstract" by blast
  
      {
        AOT_assume Ay: ‹A!y›
        {
          fix F
          {
            AOT_assume ‹∀u□([F]u ≡ [G]u)›
            AOT_hence ‹□∀u([F]u ≡ [G]u)›
              using "Ordinary.res-var-bound-reas[BF]"[THEN "→E"] by simp
            AOT_hence ‹□F ≡⇩E G›
              by (AOT_subst ‹F ≡⇩E G› ‹∀u ([F]u ≡ [G]u)›)
                 (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
            AOT_hence ‹x[F] ≡ x[G]›
              using 0[THEN "∀E"(2)] "≡E" "→E" by meson
            AOT_hence ‹x[F]›
              using G_prop "&E" "≡E" by blast
          }
          AOT_hence ‹∀u□([F]u ≡ [G]u) → x[F]›
            by (rule "→I")
        }
        AOT_hence xprop: ‹∀F(∀u□([F]u ≡ [G]u) → x[F])›
          by (rule GEN)
        moreover AOT_have yprop: ‹¬∀F(∀u□([F]u ≡ [G]u) → y[F])›
        proof (rule "raa-cor:2")
          AOT_assume ‹∀F(∀u□([F]u ≡ [G]u) → y[F])›
          AOT_hence ‹∀F(□∀u([F]u ≡ [G]u) → y[F])›
            apply (AOT_subst ‹□∀u([F]u ≡ [G]u)› ‹∀u□([F]u ≡ [G]u)› for: F)
            using "Ordinary.res-var-bound-reas[BF]"
                  "Ordinary.res-var-bound-reas[CBF]"
                  "intro-elim:2" apply presburger
            by simp
          AOT_hence A: ‹∀F(□F ≡⇩E G → y[F])›
            by (AOT_subst ‹F ≡⇩E G› ‹∀u ([F]u ≡ [G]u)› for: F)
               (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
          moreover AOT_have ‹□G ≡⇩E G›
            by (auto intro!: "eqE"[THEN "≡⇩d⇩fI"] "cqt:2" RN "&I" GEN "→I" "≡I")
          ultimately AOT_have ‹y[G]› using "∀E"(2) "→E" by blast
          AOT_thus ‹p & ¬p› for p using G_prop "&E" by (metis "raa-cor:3")
        qed
        AOT_have ‹∃F([F]x & ¬[F]y)›
        proof(rule "raa-cor:1")
          AOT_assume ‹¬∃F([F]x & ¬[F]y)›
          AOT_hence indist: ‹∀F □([F]x ≡ [F]y)› using indistI by blast
          AOT_have ‹∀F(∀u□([F]u ≡ [G]u) → y[F])›
            using indistinguishable_ord_enc_all[axiom_inst, THEN "→E", OF "&I",
                      OF "&I", OF "&I", OF "cqt:2[const_var]"[axiom_inst],
                      OF Ax, OF Ay, OF indist, THEN "≡E"(1), OF xprop].
          AOT_thus ‹∀F(∀u□([F]u ≡ [G]u) → y[F]) & ¬∀F(∀u□([F]u ≡ [G]u) → y[F])›
            using yprop "&I" by blast
        qed
      }
      moreover {
        AOT_assume notAy: ‹¬A!y›
        AOT_have ‹∃F([F]x & ¬[F]y)›
          apply (rule "∃I"(1)[where τ=‹«A!»›])
          using Ax notAy "&I" apply blast
          by (simp add: "oa-exist:2")
      }
      ultimately AOT_have ‹∃F([F]x & ¬[F]y)›
        by (metis "raa-cor:1")
    }
    moreover {
      AOT_assume G_prop: ‹¬x[G] & y[G]›
      AOT_hence Ay: ‹A!y›
        by (meson "&E"(2) "encoders-are-abstract" "existential:2[const_var]" "→E")
      AOT_hence notOy: ‹¬O!y›
        using "≡E"(1) "oa-contingent:3" by blast
      {
        AOT_assume Ax: ‹A!x›
        {
          fix F
          {
            AOT_assume ‹□∀u([F]u ≡ [G]u)›
            AOT_hence ‹□F ≡⇩E G›
              by (AOT_subst ‹F ≡⇩E G› ‹∀u([F]u ≡ [G]u)›)
                 (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
            AOT_hence ‹x[F] ≡ x[G]›
              using 0[THEN "∀E"(2)] "≡E" "→E" by meson
            AOT_hence ‹¬x[F]›
              using G_prop "&E" "≡E" by blast
          }
          AOT_hence ‹□∀u([F]u ≡ [G]u) → ¬x[F]›
            by (rule "→I")
        }
        AOT_hence x_prop: ‹∀F(□∀u([F]u ≡ [G]u) → ¬x[F])›
          by (rule GEN)
        AOT_have x_prop: ‹¬∃F(∀u□([F]u ≡ [G]u) & x[F])› 
        proof (rule "raa-cor:2")
          AOT_assume ‹∃F(∀u □([F]u ≡ [G]u) & x[F])›
          then AOT_obtain F where F_prop: ‹∀u □([F]u ≡ [G]u) & x[F]›
            using "∃E"[rotated] by blast
          AOT_have ‹□([F]u ≡ [G]u)› for u
            using F_prop[THEN "&E"(1), THEN "Ordinary.∀E"].
          AOT_hence ‹∀u □([F]u ≡ [G]u)›
            by (rule Ordinary.GEN)
          AOT_hence ‹□∀u([F]u ≡ [G]u)›
            by (metis "Ordinary.res-var-bound-reas[BF]" "→E")
          AOT_hence ‹¬x[F]›
            using x_prop[THEN "∀E"(2), THEN "→E"] by blast
          AOT_thus ‹p & ¬p› for p
            using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
        qed
        AOT_have y_prop: ‹∃F(∀u □([F]u ≡ [G]u) & y[F])›
        proof (rule "raa-cor:1")
          AOT_assume ‹¬∃F (∀u □([F]u ≡ [G]u) & y[F])›
          AOT_hence 0: ‹∀F ¬(∀u □([F]u ≡ [G]u) & y[F])›
            using "cqt-further:4"[THEN "→E"] by blast
          {
            fix F
            {
              AOT_assume ‹∀u □([F]u ≡ [G]u)›
              AOT_hence ‹¬y[F]›
                using 0[THEN "∀E"(2)] "&I" "raa-cor:1" by meson
            }
            AOT_hence ‹(∀u □([F]u ≡ [G]u) → ¬y[F])›
              by (rule "→I")
          }
          AOT_hence A: ‹∀F(∀u □([F]u ≡ [G]u) → ¬y[F])›
            by (rule GEN)
          moreover AOT_have ‹∀u □([G]u ≡ [G]u)›
            by (simp add: RN "oth-class-taut:3:a" "universal-cor" "→I")
          ultimately AOT_have ‹¬y[G]›
            using "∀E"(2) "→E" by blast
          AOT_thus ‹p & ¬p› for p
            using G_prop "&E" by (metis "raa-cor:3")
        qed
        AOT_have ‹∃F([F]x & ¬[F]y)›
        proof(rule "raa-cor:1")
          AOT_assume ‹¬∃F([F]x & ¬[F]y)›
          AOT_hence indist: ‹∀F □([F]x ≡ [F]y)›
            using indistI by blast
          AOT_thus ‹∃F(∀u □([F]u ≡ [G]u) & x[F]) & ¬∃F(∀u □([F]u ≡ [G]u) & x[F])›
            using indistinguishable_ord_enc_ex[axiom_inst, THEN "→E", OF "&I",
                    OF "&I", OF "&I", OF "cqt:2[const_var]"[axiom_inst],
                    OF Ax, OF Ay, OF indist, THEN "≡E"(2), OF y_prop]
                x_prop "&I" by blast
        qed
      }
      moreover {
        AOT_assume notAx: ‹¬A!x›
        AOT_hence Ox: ‹O!x›
          using "∨E"(3) "oa-exist:3" by blast
        AOT_have ‹∃F([F]x & ¬[F]y)›
          apply (rule "∃I"(1)[where τ=‹«O!»›])
          using Ox notOy "&I" apply blast
          by (simp add: "oa-exist:1")
      }
      ultimately AOT_have ‹∃F([F]x & ¬[F]y)›
        by (metis "raa-cor:1")
    }
    ultimately AOT_show ‹∃F([F]x & ¬[F]y)›
      using G_prop by (metis "&I" "→I" "≡I" "raa-cor:1")
  }
  qed

  AOT_modally_strict {
    fix x y
    AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
    AOT_hence nec_indist: ‹□∀F ([F]x ≡ [F]y)› 
      using "ind-nec" "vdash-properties:10" by blast
    AOT_hence indist_nec: ‹∀F □([F]x ≡ [F]y)›
      using "CBF" "vdash-properties:10" by blast
    AOT_assume 0: ‹∀G (□G ≡⇩E F → x[G])›
    AOT_hence 1: ‹∀G (□∀u ([G]u ≡ [F]u) → x[G])›
      by (AOT_subst (reverse) ‹∀u ([G]u ≡ [F]u)› ‹G ≡⇩E F› for: G)
         (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
    AOT_have ‹x[F]›
      by (safe intro!: 1[THEN "∀E"(2), THEN "→E"] GEN "→I" RN "≡I")
    AOT_have ‹∀G (□G ≡⇩E F → y[G])›
    proof(rule "raa-cor:1")
      AOT_assume ‹¬∀G (□G ≡⇩E F → y[G])›
      AOT_hence ‹∃G ¬(□G ≡⇩E F → y[G])›
        using "cqt-further:2" "→E" by blast
      then AOT_obtain G where G_prop: ‹¬(□G ≡⇩E F → y[G])›
        using "∃E"[rotated] by blast
      AOT_hence 1: ‹□G ≡⇩E F & ¬y[G]›
        by (metis "≡E"(1) "oth-class-taut:1:b")
      AOT_have xG: ‹x[G]›
        using 0[THEN "∀E"(2), THEN "→E"] 1[THEN "&E"(1)] by blast
      AOT_hence ‹x[G] & ¬y[G]›
        using 1[THEN "&E"(2)] "&I" by blast
      AOT_hence B: ‹¬(x[G] ≡ y[G])›
        using "&E"(2) "≡E"(1) "reductio-aa:1" xG by blast
      {
        fix H
        {
          AOT_assume ‹□H ≡⇩E G›
          AOT_hence ‹□(H ≡⇩E G & G ≡⇩E F)›
            using 1 by (metis "KBasic:3" "con-dis-i-e:1" "con-dis-i-e:2:a"
                              "intro-elim:3:b")
          moreover AOT_have ‹□(H ≡⇩E G & G ≡⇩E F) → □(H ≡⇩E F)›
          proof(rule RM)
            AOT_modally_strict {
              AOT_show ‹H ≡⇩E G & G ≡⇩E F → H ≡⇩E F›
              proof (safe intro!: "→I" "eqE"[THEN "≡⇩d⇩fI"] "&I" "cqt:2" Ordinary.GEN)
                fix u
                AOT_assume ‹H ≡⇩E G & G ≡⇩E F›
                AOT_hence ‹∀u ([H]u ≡ [G]u)› and ‹∀u ([G]u ≡ [F]u)›
                  using "eqE"[THEN "≡⇩d⇩fE"] "&E" by blast+
                AOT_thus ‹[H]u ≡ [F]u›
                  by (auto dest!: "Ordinary.∀E" dest: "≡E")
              qed
            }
          qed
          ultimately AOT_have ‹□(H ≡⇩E F)›
            using "→E" by blast
          AOT_hence ‹x[H]›
            using 0[THEN "∀E"(2)] "→E" by blast
          AOT_hence ‹x[H] ≡ x[G]›
            using xG "≡I" "→I" by blast
        }
        AOT_hence ‹□H ≡⇩E G → (x[H] ≡ x[G])› by (rule "→I")
      }
      AOT_hence A: ‹∀H(□H ≡⇩E G → (x[H] ≡ x[G]))›
        by (rule GEN)
      then AOT_obtain F where F_prop: ‹[F]x & ¬[F]y›
        using Aux[OF A, OF B] "∃E"[rotated] by blast
      moreover AOT_have ‹[F]y›
        using indist[THEN "∀E"(2), THEN "≡E"(1), OF F_prop[THEN "&E"(1)]].
      AOT_thus ‹p & ¬p› for p
        using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
    qed
  } note 0 = this
  AOT_modally_strict {
    fix x y
    AOT_assume ‹∀F ([F]x ≡ [F]y)›
    moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
      by (metis calculation "cqt-basic:11" "≡E"(2))
    ultimately AOT_have ‹∀G (□G ≡⇩E F → x[G]) ≡ ∀G (□G ≡⇩E F → y[G])›
      using 0 "≡I" "→I" by auto
  } note 1 = this
  AOT_show ‹[λx ∀G (□G ≡⇩E F → x[G])]↓›
    by (safe intro!: RN GEN "→I" 1 "kirchner-thm:2"[THEN "≡E"(2)])

  AOT_modally_strict {
    fix x y
    AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
    AOT_hence nec_indist: ‹□∀F ([F]x ≡ [F]y)› 
      using "ind-nec" "vdash-properties:10" by blast
    AOT_hence indist_nec: ‹∀F □([F]x ≡ [F]y)›
      using "CBF" "vdash-properties:10" by blast
    AOT_assume 0: ‹∀G (□G ≡⇩E F → ¬x[G])›
    AOT_hence 1: ‹∀G (□∀u ([G]u ≡ [F]u) → ¬x[G])›
      by (AOT_subst (reverse) ‹∀u ([G]u ≡ [F]u)› ‹G ≡⇩E F› for: G)
         (auto intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
    AOT_have ‹¬x[F]›
      by (safe intro!: 1[THEN "∀E"(2), THEN "→E"] GEN "→I" RN "≡I")
    AOT_have ‹∀G (□G ≡⇩E F → ¬y[G])›
    proof(rule "raa-cor:1")
      AOT_assume ‹¬∀G (□G ≡⇩E F → ¬y[G])›
      AOT_hence ‹∃G ¬(□G ≡⇩E F → ¬y[G])›
        using "cqt-further:2" "→E" by blast
      then AOT_obtain G where G_prop: ‹¬(□G ≡⇩E F → ¬y[G])›
        using "∃E"[rotated] by blast
      AOT_hence 1: ‹□G ≡⇩E F & ¬¬y[G]›
        by (metis "≡E"(1) "oth-class-taut:1:b")
      AOT_hence yG: ‹y[G]›
        using G_prop "→I" "raa-cor:3" by blast
      moreover AOT_hence 12: ‹¬x[G]›
        using 0[THEN "∀E"(2), THEN "→E"] 1[THEN "&E"(1)] by blast
      ultimately AOT_have ‹¬x[G] & y[G]›
        using "&I" by blast
      AOT_hence B: ‹¬(x[G] ≡ y[G])›
        by (metis "12" "≡E"(3) "raa-cor:3" yG)
      {
        fix H
        {
          AOT_assume 3: ‹□H ≡⇩E G›
          AOT_hence ‹□(H ≡⇩E G & G ≡⇩E F)›
            using 1
            by (metis "KBasic:3" "con-dis-i-e:1" "→I" "intro-elim:3:b"
                      "reductio-aa:1" G_prop)
          moreover AOT_have ‹□(H ≡⇩E G & G ≡⇩E F) → □(H ≡⇩E F)›
          proof (rule RM)
            AOT_modally_strict {
              AOT_show ‹H ≡⇩E G & G ≡⇩E F → H ≡⇩E F›
              proof (safe intro!: "→I" "eqE"[THEN "≡⇩d⇩fI"] "&I" "cqt:2" Ordinary.GEN)
                fix u
                AOT_assume ‹H ≡⇩E G & G ≡⇩E F›
                AOT_hence ‹∀u ([H]u ≡ [G]u)› and ‹∀u ([G]u ≡ [F]u)›
                  using "eqE"[THEN "≡⇩d⇩fE"] "&E" by blast+
                AOT_thus ‹[H]u ≡ [F]u›
                  by (auto dest!: "Ordinary.∀E" dest: "≡E")
              qed
            }
          qed
          ultimately AOT_have ‹□(H ≡⇩E F)›
            using "→E" by blast
          AOT_hence ‹¬x[H]›
            using 0[THEN "∀E"(2)] "→E" by blast
          AOT_hence ‹x[H] ≡ x[G]›
            using 12 "≡I" "→I" by (metis "raa-cor:3")
        }
        AOT_hence ‹□H ≡⇩E G → (x[H] ≡ x[G])›
          by (rule "→I")
      }
      AOT_hence A: ‹∀H(□H ≡⇩E G → (x[H] ≡ x[G]))›
        by (rule GEN)
      then AOT_obtain F where F_prop: ‹[F]x & ¬[F]y›
        using Aux[OF A, OF B] "∃E"[rotated] by blast
      moreover AOT_have ‹[F]y›
        using indist[THEN "∀E"(2), THEN "≡E"(1), OF F_prop[THEN "&E"(1)]].
      AOT_thus ‹p & ¬p› for p
        using F_prop[THEN "&E"(2)] by (metis "raa-cor:3")
    qed
  } note 0 = this
  AOT_modally_strict {
    fix x y
    AOT_assume ‹∀F ([F]x ≡ [F]y)›
    moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
      by (metis calculation "cqt-basic:11" "≡E"(2))
    ultimately AOT_have ‹∀G (□G ≡⇩E F → ¬x[G]) ≡ ∀G (□G ≡⇩E F → ¬y[G])›
      using 0 "≡I" "→I" by auto
  } note 1 = this
  AOT_show ‹[λx ∀G (□G ≡⇩E F → ¬x[G])]↓›
    by (safe intro!: RN GEN "→I" 1 "kirchner-thm:2"[THEN "≡E"(2)])
qed

text‹Reformulate the existence claims in terms of their negations.›

AOT_theorem denotes_ex: ‹[λx ∃G (□G ≡⇩E F & x[G])]↓›
proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
  AOT_show ‹[λx ¬∀G (□G ≡⇩E F → ¬x[G])]↓›
    using denotes_all_neg[THEN negation_denotes[THEN "→E"]].
next
  AOT_show ‹□∀x (¬∀G (□G ≡⇩E F → ¬x[G]) ≡ ∃G (□G ≡⇩E F & x[G]))›
    by (AOT_subst  ‹□G ≡⇩E F & x[G]› ‹¬(□G ≡⇩E F → ¬x[G])› for: G x)
       (auto simp: "conventions:1" "rule-eq-df:1"
             intro: "oth-class-taut:4:b"[THEN "≡E"(2)]
                    "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:b"]
             intro!: RN GEN)
qed

AOT_theorem denotes_ex_neg: ‹[λx ∃G (□G ≡⇩E F & ¬x[G])]↓›
proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
  AOT_show ‹[λx ¬∀G (□G ≡⇩E F → x[G])]↓›
    using denotes_all[THEN negation_denotes[THEN "→E"]].
next
  AOT_show ‹□∀x (¬∀G (□G ≡⇩E F → x[G]) ≡ ∃G (□G ≡⇩E F & ¬x[G]))›
    by (AOT_subst (reverse) ‹□G ≡⇩E F & ¬x[G]› ‹¬(□G ≡⇩E F → x[G])› for: G x)
       (auto simp: "oth-class-taut:1:b"
             intro: "oth-class-taut:4:b"[THEN "≡E"(2)]
                    "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:b"]
             intro!: RN GEN)
qed

text‹Derive comprehension principles.›

AOT_theorem Comprehension_1:
  shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∃F (φ{F} & x[F])]↓›
proof(rule "→I")
  AOT_assume assm: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
  AOT_modally_strict {
    fix x y
    AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
    AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
    AOT_assume x_prop: ‹∃F (φ{F} & x[F])›
    then AOT_obtain F where F_prop: ‹φ{F} & x[F]›
      using "∃E"[rotated] by blast
    AOT_hence ‹□F ≡⇩E F & x[F]›
      by (auto intro!: RN eqE[THEN "≡⇩d⇩fI"] "&I" "cqt:2" GEN "≡I" "→I" dest: "&E")
    AOT_hence ‹∃G(□G ≡⇩E F & x[G])›
      by (rule "∃I")
    AOT_hence ‹[λx ∃G(□G ≡⇩E F & x[G])]x›
      by (safe intro!: "β←C" denotes_ex "cqt:2")
    AOT_hence ‹[λx ∃G(□G ≡⇩E F & x[G])]y›
      using indist[THEN "∀E"(1), OF denotes_ex, THEN "≡E"(1)] by blast
    AOT_hence ‹∃G(□G ≡⇩E F & y[G])›
      using "β→C" by blast
    then AOT_obtain G where ‹□G ≡⇩E F & y[G]›
      using "∃E"[rotated] by blast
    AOT_hence ‹φ{G} & y[G]›
      using 0[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", THEN "≡E"(1)]
            F_prop[THEN "&E"(1)] "&E" "&I" by blast
    AOT_hence ‹∃F (φ{F} & y[F])›
      by (rule "∃I")
  } note 1 = this
  AOT_modally_strict {
    AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
    {
      fix x y
      {
        AOT_assume ‹∀F ([F]x ≡ [F]y)›
        moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
          by (metis calculation "cqt-basic:11" "≡E"(1))
        ultimately AOT_have ‹∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])›
          using 0 1[OF 0] "≡I" "→I" by simp
      }
      AOT_hence ‹∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F]))›
        using "→I" by blast
    }
    AOT_hence ‹∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡  ∃F (φ{F} & y[F])))›
      by (auto intro!: GEN)
  } note 1 = this
  AOT_hence ‹❙⊢⇩□ ∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
                ∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])))›
    by (rule "→I")
  AOT_hence ‹□∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
             □∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])))›
    by (rule RM)
  AOT_hence ‹□∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & x[F]) ≡ ∃F (φ{F} & y[F])))›
    using "→E" assm by blast
  AOT_thus ‹[λx ∃F (φ{F} & x[F])]↓›
    by (safe intro!: "kirchner-thm:2"[THEN "≡E"(2)])
qed

AOT_theorem Comprehension_2:
  shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∃F (φ{F} & ¬x[F])]↓›
proof(rule "→I")
  AOT_assume assm: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
  AOT_modally_strict {
    fix x y
    AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
    AOT_assume indist: ‹∀F ([F]x ≡ [F]y)›
    AOT_assume x_prop: ‹∃F (φ{F} & ¬x[F])›
    then AOT_obtain F where F_prop: ‹φ{F} & ¬x[F]›
      using "∃E"[rotated] by blast
    AOT_hence ‹□F ≡⇩E F & ¬x[F]›
      by (auto intro!: RN eqE[THEN "≡⇩d⇩fI"] "&I" "cqt:2" GEN "≡I" "→I" dest: "&E")
    AOT_hence ‹∃G(□G ≡⇩E F & ¬x[G])›
      by (rule "∃I")
    AOT_hence ‹[λx ∃G(□G ≡⇩E F & ¬x[G])]x›
      by (safe intro!: "β←C" denotes_ex_neg "cqt:2")
    AOT_hence ‹[λx ∃G(□G ≡⇩E F & ¬x[G])]y›
      using indist[THEN "∀E"(1), OF denotes_ex_neg, THEN "≡E"(1)] by blast
    AOT_hence ‹∃G(□G ≡⇩E F & ¬y[G])›
      using "β→C" by blast
    then AOT_obtain G where ‹□G ≡⇩E F & ¬y[G]›
      using "∃E"[rotated] by blast
    AOT_hence ‹φ{G} & ¬y[G]›
      using 0[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", THEN "≡E"(1)]
            F_prop[THEN "&E"(1)] "&E" "&I" by blast
    AOT_hence ‹∃F (φ{F} & ¬y[F])›
      by (rule "∃I")
  } note 1 = this
  AOT_modally_strict {
    AOT_assume 0: ‹∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G}))›
    {
      fix x y
      {
        AOT_assume ‹∀F ([F]x ≡ [F]y)›
        moreover AOT_have ‹∀F ([F]y ≡ [F]x)›
          by (metis calculation "cqt-basic:11" "≡E"(1))
        ultimately AOT_have ‹∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])›
          using 0 1[OF 0] "≡I" "→I" by simp
      }
      AOT_hence ‹∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F]))›
        using "→I" by blast
    }
    AOT_hence ‹∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡  ∃F (φ{F} & ¬y[F])))›
      by (auto intro!: GEN)
  } note 1 = this
  AOT_hence ‹❙⊢⇩□ ∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
                ∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])))›
    by (rule "→I")
  AOT_hence ‹□∀F∀G (□G ≡⇩E F → (φ{F} ≡ φ{G})) →
             □∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])))›
    by (rule RM)
  AOT_hence ‹□∀x∀y(∀F ([F]x ≡ [F]y) → (∃F (φ{F} & ¬x[F]) ≡ ∃F (φ{F} & ¬y[F])))›
    using "→E" assm by blast
  AOT_thus ‹[λx ∃F (φ{F} & ¬x[F])]↓›
    by (safe intro!: "kirchner-thm:2"[THEN "≡E"(2)])
qed

text‹Derived variants of the comprehension principles above.›

AOT_theorem Comprehension_1':
  shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∀F (x[F] → φ{F})]↓›
proof(rule "→I")
  AOT_assume ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
  AOT_hence 0: ‹□∀F∀G(□G ≡⇩E F → (¬φ{F} ≡ ¬φ{G}))›
    by (AOT_subst (reverse) ‹¬φ{F} ≡ ¬φ{G}› ‹φ{F} ≡ φ{G}› for: F G)
       (auto simp: "oth-class-taut:4:b")
  AOT_show ‹[λx ∀F (x[F] → φ{F})]↓›
  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show ‹[λx ¬∃F(¬φ{F} & x[F])]↓›
      using Comprehension_1[THEN "→E", OF 0, THEN negation_denotes[THEN "→E"]].
  next
    AOT_show ‹□∀x (¬∃F (¬φ{F} & x[F]) ≡ ∀F (x[F] → φ{F}))›
      by (AOT_subst (reverse) ‹¬φ{F} & x[F]› ‹¬(x[F] → φ{F})› for: F x)
         (auto simp: "oth-class-taut:1:b"[THEN "intro-elim:3:e",
                                          OF "oth-class-taut:2:a"]
             intro: "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:a",
                                     symmetric]
             intro!: RN GEN)
  qed
qed

AOT_theorem Comprehension_2':
  shows ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∀F (φ{F} → x[F])]↓›
proof(rule "→I")
  AOT_assume 0: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
  AOT_show ‹[λx ∀F (φ{F} → x[F])]↓›
  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show ‹[λx ¬∃F(φ{F} & ¬x[F])]↓›
      using Comprehension_2[THEN "→E", OF 0, THEN negation_denotes[THEN "→E"]].
  next
    AOT_show ‹□∀x (¬∃F (φ{F} & ¬x[F]) ≡ ∀F (φ{F} → x[F]))›
      by (AOT_subst (reverse) ‹φ{F} & ¬x[F]› ‹¬(φ{F} → x[F])› for: F x)
         (auto simp: "oth-class-taut:1:b"
             intro: "intro-elim:3:f"[OF "cqt-further:3", OF "oth-class-taut:3:a",
                                     symmetric]
             intro!: RN GEN)
  qed
qed

text‹Derive a combined comprehension principles.›

AOT_theorem Comprehension_3:
  ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G})) → [λx ∀F (x[F] ≡ φ{F})]↓›
proof(rule "→I")
  AOT_assume 0: ‹□∀F∀G(□G ≡⇩E F → (φ{F} ≡ φ{G}))›
  AOT_show ‹[λx ∀F (x[F] ≡ φ{F})]↓›
  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show ‹[λx ∀F (x[F] → φ{F}) & ∀F (φ{F} → x[F])]↓›
      by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
                       Comprehension_1'[THEN "→E"]
                       Comprehension_2'[THEN "→E"] 0)
  next
    AOT_show ‹□∀x (∀F (x[F] → φ{F}) & ∀F (φ{F} → x[F]) ≡ ∀F (x[F] ≡ φ{F}))›
      by (auto intro!: RN GEN "≡I" "→I" "&I" dest: "&E" "∀E"(2) "→E" "≡E"(1,2))
  qed
qed

notepad
begin
text‹Verify that the original axioms are equivalent to @{thm denotes_ex}
     and @{thm denotes_ex_neg}.›
AOT_modally_strict {
  fix x y H
  AOT_have ‹A!x & A!y & ∀F □([F]x ≡ [F]y) →
  (∀G (∀z (O!z → □([G]z ≡ [H]z)) → x[G]) ≡
   ∀G (∀z (O!z → □([G]z ≡ [H]z)) → y[G]))›
  proof(rule "→I")
    {
      fix x y
      AOT_assume ‹A!x›
      AOT_assume ‹A!y›
      AOT_assume indist: ‹∀F □([F]x ≡ [F]y)›
      AOT_assume ‹∀G (∀u □([G]u ≡ [H]u) → x[G])›
      AOT_hence ‹∀G (□∀u ([G]u ≡ [H]u) → x[G])›
        using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
              "intro-elim:2"
        by (AOT_subst ‹□∀u ([G]u ≡ [H]u)› ‹∀u □([G]u ≡ [H]u)› for: G) auto
      AOT_hence ‹∀G (□G ≡⇩E H → x[G])›
        by (AOT_subst ‹G ≡⇩E H› ‹∀u ([G]u ≡ [H]u)› for: G)
            (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2")
      AOT_hence ‹¬∃G (□G ≡⇩E H & ¬x[G])›
        by (AOT_subst (reverse) ‹(□G ≡⇩E H & ¬x[G])› ‹¬(□G ≡⇩E H → x[G])› for: G)
           (auto simp: "oth-class-taut:1:b" "cqt-further:3"[THEN "≡E"(1)])
      AOT_hence ‹¬[λx ∃G (□G ≡⇩E H & ¬x[G])]x›
        by (auto intro: "β→C")
      AOT_hence ‹¬[λx ∃G (□G ≡⇩E H & ¬x[G])]y›
        using indist[THEN "∀E"(1), OF denotes_ex_neg,
                     THEN "qml:2"[axiom_inst, THEN "→E"],
                     THEN "≡E"(3)] by blast
      AOT_hence ‹¬∃G (□G ≡⇩E H & ¬y[G])›
        by (safe intro!: "β←C" denotes_ex_neg "cqt:2")
      AOT_hence ‹∀G ¬(□G ≡⇩E H & ¬y[G])›
        using "cqt-further:4"[THEN "→E"] by blast
      AOT_hence ‹∀G(□G ≡⇩E H → y[G])›
        by (AOT_subst ‹□G ≡⇩E H → y[G]› ‹¬(□G ≡⇩E H & ¬y[G])› for: G)
           (auto simp: "oth-class-taut:1:a")
      AOT_hence ‹∀G (□∀u([G]u ≡ [H]u) → y[G])›
        by (AOT_subst (reverse) ‹∀u ([G]u ≡ [H]u)› ‹G ≡⇩E H› for: G)
           (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2") 
      AOT_hence ‹∀G (∀u □([G]u ≡ [H]u) → y[G])›
        using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
              "intro-elim:2"
        by (AOT_subst ‹∀u □([G]u ≡ [H]u)› ‹□∀u ([G]u ≡ [H]u)› for: G) auto
    } note 0 = this
    AOT_assume ‹A!x & A!y & ∀F □([F]x ≡ [F]y)›
    AOT_hence ‹A!x› and ‹A!y› and ‹∀F □([F]x ≡ [F]y)›
      using "&E" by blast+
    moreover AOT_have ‹∀F □([F]y ≡ [F]x)›
      using calculation(3)
      apply (safe intro!: CBF[THEN "→E"] dest!: BF[THEN "→E"])
      using "RM:3" "cqt-basic:11" "intro-elim:3:b" by fast
    ultimately AOT_show ‹∀G (∀u □([G]u ≡ [H]u) → x[G]) ≡
                         ∀G (∀u □([G]u ≡ [H]u) → y[G])›
      using 0 by (auto intro!: "≡I" "→I")
  qed
  
  AOT_have ‹A!x & A!y & ∀F □([F]x ≡ [F]y) →
  (∃G (∀z (O!z → □([G]z ≡ [H]z)) & x[G]) ≡ ∃G (∀z (O!z → □([G]z ≡ [H]z)) & y[G]))›
  proof(rule "→I")
    {
      fix x y
      AOT_assume ‹A!x›
      AOT_assume ‹A!y›
      AOT_assume indist: ‹∀F □([F]x ≡ [F]y)›
      AOT_assume x_prop: ‹∃G (∀u □([G]u ≡ [H]u) & x[G])›
      AOT_hence ‹∃G (□∀u ([G]u ≡ [H]u) & x[G])›
        using "Ordinary.res-var-bound-reas[BF]" "Ordinary.res-var-bound-reas[CBF]"
              "intro-elim:2"
        by (AOT_subst ‹□∀u ([G]u ≡ [H]u)› ‹∀u □([G]u ≡ [H]u)› for: G) auto
      AOT_hence ‹∃G (□G ≡⇩E H & x[G])›
        by (AOT_subst ‹G ≡⇩E H› ‹∀u ([G]u ≡ [H]u)› for: G)
           (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2") 
      AOT_hence ‹[λx ∃G (□G ≡⇩E H & x[G])]x›
        by (safe intro!: "β←C" denotes_ex "cqt:2")
      AOT_hence ‹[λx ∃G (□G ≡⇩E H & x[G])]y›
        using indist[THEN "∀E"(1), OF denotes_ex,
                     THEN "qml:2"[axiom_inst, THEN "→E"],
                     THEN "≡E"(1)] by blast
      AOT_hence ‹∃G (□G ≡⇩E H & y[G])›
        by (rule "β→C")
      AOT_hence ‹∃G (□∀u ([G]u ≡ [H]u) & y[G])›
        by (AOT_subst (reverse) ‹∀u ([G]u ≡ [H]u)› ‹G ≡⇩E H› for: G)
           (safe intro!: "eqE"[THEN "≡Df", THEN "≡S"(1), OF "&I"] "cqt:2") 
      AOT_hence ‹∃G (∀u □([G]u ≡ [H]u) & y[G])›
        using "Ordinary.res-var-bound-reas[BF]"
              "Ordinary.res-var-bound-reas[CBF]"
              "intro-elim:2"
        by (AOT_subst ‹∀u □([G]u ≡ [H]u)› ‹□∀u ([G]u ≡ [H]u)› for: G) auto 
    } note 0 = this
    AOT_assume ‹A!x & A!y & ∀F □([F]x ≡ [F]y)›
    AOT_hence ‹A!x› and ‹A!y› and ‹∀F □([F]x ≡ [F]y)›
      using "&E" by blast+
    moreover AOT_have ‹∀F □([F]y ≡ [F]x)›
      using calculation(3)
      apply (safe intro!: CBF[THEN "→E"] dest!: BF[THEN "→E"])
      using "RM:3" "cqt-basic:11" "intro-elim:3:b" by fast
    ultimately AOT_show ‹∃G (∀u □([G]u ≡ [H]u) & x[G]) ≡
                         ∃G (∀u □([G]u ≡ [H]u) & y[G])›
      using 0 by (auto intro!: "≡I" "→I")
  qed
}
end
end