Theory AOT_misc

theory AOT_misc
  imports AOT_NaturalNumbers
begin

section‹Miscellaneous Theorems›

AOT_theorem PossiblyNumbersEmptyPropertyImpliesZero:
  Numbers(x,z O!z & z E z])  x = 0
proof(rule "→I")
  AOT_have Rigid(z O!z & z E z])
  proof (safe intro!: "df-rigid-rel:1"[THEN "dfI"] "&I" "cqt:2";
         rule RN; safe intro!: GEN "→I")
    AOT_modally_strict {
      fix x
      AOT_assume z O!z & z E z]x
      AOT_hence O!x & x E x by (rule "β→C")
      moreover AOT_have x =E x using calculation[THEN "&E"(1)] 
        by (metis "ord=Eequiv:1" "vdash-properties:10")
      ultimately AOT_have x =E x & ¬x =E x
        by (metis "con-dis-i-e:1" "con-dis-i-e:2:b" "intro-elim:3:a" "thm-neg=E")
      AOT_thus z O!z & z E z]x using "raa-cor:1" by blast
    }
  qed
  AOT_hence x (Numbers(x,z O!z & z E z])  Numbers(x,z O!z & z E z]))
    by (safe intro!: "num-cont:2"[unvarify G, THEN "→E"] "cqt:2")
  AOT_hence x (Numbers(x,z O!z & z E z])  Numbers(x,z O!z & z E z]))
    using "BFs:2"[THEN "→E"] by blast
  AOT_hence (Numbers(x,z O!z & z E z])  Numbers(x,z O!z & z E z]))
    using "∀E"(2) by auto
  moreover AOT_assume Numbers(x,z O!z & z E z])
  ultimately AOT_have 𝒜Numbers(x,z O!z & z E z])
    using "sc-eq-box-box:1"[THEN "≡E"(1), THEN "→E", THEN "nec-imp-act"[THEN "→E"]]
    by blast
  AOT_hence Numbers(x,z 𝒜z O!z & z E z]z])
    by (safe intro!: "eq-num:1"[unvarify G, THEN "≡E"(1)] "cqt:2")
  AOT_hence x = #z O!z & z E z]
    by (safe intro!: "eq-num:2"[unvarify G, THEN "≡E"(1)] "cqt:2")
  AOT_thus x = 0
    using "cqt:2"(1) "rule-id-df:2:b[zero]" "rule=E" "zero:1" by blast
qed

AOT_define Numbers' :: τ  τ  φ (Numbers'''(_,_'))
  Numbers'(x, G) df A!x & G & F (x[F]  F E G)
AOT_theorem Numbers'equiv: Numbers'(x,G)  A!x & F (x[F]  F E G)
  by (AOT_subst_def Numbers')
     (auto intro!: "≡I" "→I" "&I" "cqt:2" dest: "&E")

AOT_theorem Numbers'DistinctZeroes:
  xy (Numbers'(x,z O!z & z E z]) & Numbers'(y,z O!z & z E z]) & x  y)
proof -
  AOT_obtain w1 where w w1  w
    using "two-worlds-exist:4" "PossibleWorld.∃E"[rotated] by fast
  then AOT_obtain w2 where distinct_worlds: w1  w2
    using "PossibleWorld.∃E"[rotated] by blast
  AOT_obtain x where x_prop:
    A!x & F (x[F]  w1  F E z O!z & z E z])
    using "A-objects"[axiom_inst] "∃E"[rotated] by fast
  moreover AOT_obtain y where y_prop:
    A!y & F (y[F]  w2  F E z O!z & z E z])
    using "A-objects"[axiom_inst] "∃E"[rotated] by fast
  moreover {
    fix x w
    AOT_assume x_prop: A!x & F (x[F]  w  F E z O!z & z E z])
    AOT_have F w  (x[F]  F E z O!z & z E z])
    proof(safe intro!: GEN "conj-dist-w:4"[unvarify p q, OF "log-prop-prop:2",
                              OF "log-prop-prop:2",THEN "≡E"(2)] "≡I" "→I")
      fix F
      AOT_assume w  x[F]
      AOT_hence x[F]
        using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2),
                       OF "PossibleWorld.∃I"] by blast
      AOT_hence x[F]
        by (metis "en-eq:3[1]" "intro-elim:3:a")
      AOT_thus w  (F E z O!z & z E z])
        using x_prop[THEN "&E"(2), THEN "∀E"(2), THEN "≡E"(1)] by blast
    next
      fix F
      AOT_assume w  (F E z O!z & z E z])
      AOT_hence x[F]
        using x_prop[THEN "&E"(2), THEN "∀E"(2), THEN "≡E"(2)] by blast
      AOT_hence x[F]
        using "pre-en-eq:1[1]"[THEN "→E"] by blast
      AOT_thus w  x[F]
        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
              "PossibleWorld.∀E" by fast
    qed
    AOT_hence w  F (x[F]  F E z O!z & z E z])
      using "conj-dist-w:5"[THEN "≡E"(2)] by fast
    moreover {
      AOT_have z O!z & z E z]
        by (safe intro!: RN "cqt:2")
      AOT_hence w  z O!z & z E z]
        using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1),
                       THEN "PossibleWorld.∀E"] by blast
    }
    moreover {
      AOT_have A!x
        using x_prop[THEN "&E"(1)] by (metis "oa-facts:2" "→E")
      AOT_hence w  A!x
        using "fund:2"[unvarify p, OF "log-prop-prop:2",
                       THEN "≡E"(1), THEN "PossibleWorld.∀E"] by blast
    }
    ultimately AOT_have w  (A!x & z O!z & z E z] &
                               F (x[F]  F E z O!z & z E z]))
      using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
              OF "log-prop-prop:2", THEN "≡E"(2), OF "&I"] by auto
    AOT_hence w w  (A!x & z O!z & z E z] &
                        F (x[F]  F E z O!z & z E z]))
      using "PossibleWorld.∃I" by auto
    AOT_hence (A!x & z O!z & z E z] & F (x[F]  F E z O!z & z E z]))
      using "fund:1"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(2)] by blast
    AOT_hence Numbers'(x,z O!z & z E z])
      by (AOT_subst_def Numbers')
  }
  ultimately AOT_have Numbers'(x,z O!z & z E z])
                  and Numbers'(y,z O!z & z E z])
    by auto
  moreover AOT_have x  y
  proof (rule "ab-obey:2"[THEN "→E"])
    AOT_have ¬u z O!z & z E z]u
    proof (safe intro!: RN "raa-cor:2")
      AOT_modally_strict {
        AOT_assume u z O!z & z E z]u
        then AOT_obtain u where z O!z & z E z]u
          using "Ordinary.∃E"[rotated] by blast
        AOT_hence O!u & u E u
          by (rule "β→C")
        AOT_hence ¬(u =E u)
          by (metis "con-dis-taut:2" "intro-elim:3:d" "modus-tollens:1"
                    "raa-cor:3" "thm-neg=E")
        AOT_hence u =E u & ¬u =E u
          by (metis "modus-tollens:1" "ord=Eequiv:1" "raa-cor:3" Ordinary.ψ)
        AOT_thus p & ¬p for p
          by (metis "raa-cor:1")
      }
    qed
    AOT_hence nec_not_ex: w w  ¬u z O!z & z E z]u
      using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
    AOT_have (y p]x  p) for x p
      by (safe intro!: RN "beta-C-meta"[THEN "→E"] "cqt:2")
    AOT_hence w w  (y p]x  p) for x p
      using "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
    AOT_hence world_prop_beta: w (w  y p]x  w  p) for x p
      using "conj-dist-w:4"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)]
            "PossibleWorld.∀E" "PossibleWorld.∀I" by meson

    AOT_have p (w1  p & ¬w2  p)
    proof(rule "raa-cor:1")
      AOT_assume 0: ¬p (w1  p & ¬w2  p)
      AOT_have 1: w1  p  w2  p for p
      proof(safe intro!: GEN "→I")
        AOT_assume w1  p
        AOT_thus w2  p
          using 0 "con-dis-i-e:1" "∃I"(2) "raa-cor:4" by fast
      qed
      moreover AOT_have w2  p  w1  p for p
      proof(safe intro!: GEN "→I")
        AOT_assume w2  p
        AOT_hence ¬w2  ¬p
          using "coherent:2" "intro-elim:3:a" by blast
        AOT_hence ¬w1  ¬p
          using 1["∀I" p, THEN "∀E"(1), OF "log-prop-prop:2"]
          by (metis "modus-tollens:1")
        AOT_thus w1  p
          using "coherent:1" "intro-elim:3:b" "reductio-aa:1" by blast
      qed
      ultimately AOT_have w1  p  w2  p for p
        by (metis "intro-elim:2")
      AOT_hence w1 = w2
        using "sit-identity"[unconstrain s, THEN "→E",
            OF PossibleWorld.ψ[THEN "world:1"[THEN "dfE"], THEN "&E"(1)],
            unconstrain s', THEN "→E",
            OF PossibleWorld.ψ[THEN "world:1"[THEN "dfE"], THEN "&E"(1)],
            THEN "≡E"(2)] GEN by fast
      AOT_thus w1 = w2 & ¬w1 = w2
        using  "=-infix" "dfE" "con-dis-i-e:1" distinct_worlds by blast
    qed
    then AOT_obtain p where 0: w1  p & ¬w2  p
      using "∃E"[rotated] by blast
    AOT_have yy p]
    proof (safe intro!: y_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(2)] "cqt:2")
      AOT_show w2  y p] E z O!z & z E z]
      proof (safe intro!:  "cqt:2" "empty-approx:1"[unvarify F H, THEN RN,
                  THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
                  THEN "PossibleWorld.∀E",
                  THEN "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2",
                                       OF "log-prop-prop:2", THEN "≡E"(1)],
                                       THEN "→E"]
                  "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
                                  OF "log-prop-prop:2", THEN "≡E"(2)] "&I")
        AOT_have ¬w2  u y p]u
        proof (rule "raa-cor:2")
          AOT_assume w2  u y p]u
          AOT_hence x w2  (O!x & y p]x)
            by (metis "conj-dist-w:6" "intro-elim:3:a")
          then AOT_obtain x where w2  (O!x & y p]x)
            using "∃E"[rotated] by blast
          AOT_hence w2  y p]x
            using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
                    OF "log-prop-prop:2", THEN "≡E"(1), THEN "&E"(2)] by blast
          AOT_hence w2  p
            using world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(1)] by blast
          AOT_thus w2  p & ¬w2  p
            using 0[THEN "&E"(2)] "&I" by blast
        qed
        AOT_thus w2  ¬u y p]u
          by (safe intro!: "coherent:1"[unvarify p, OF "log-prop-prop:2",
                                        THEN "≡E"(2)])
      next
        AOT_show w2  ¬v z O!z & z E z]v
          using nec_not_ex[THEN "PossibleWorld.∀E"] by blast
      qed
    qed
    moreover AOT_have ¬xy p]
    proof(rule "raa-cor:2")
      AOT_assume xy p]
      AOT_hence "w1  y p] E z O!z & z E z]"
        using x_prop[THEN "&E"(2), THEN "∀E"(1), THEN "≡E"(1)]
              "prop-prop2:2" by blast
      AOT_hence "¬w1  ¬y p] E z O!z & z E z]"
        using "coherent:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)] by blast
      moreover AOT_have "w1  ¬(y p] E z O!z & z E z])"
      proof (safe intro!: "cqt:2" "empty-approx:2"[unvarify F H, THEN RN,
                    THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
                    THEN "PossibleWorld.∀E",
                    THEN "conj-dist-w:2"[unvarify p q, OF "log-prop-prop:2",
                        OF "log-prop-prop:2", THEN "≡E"(1)], THEN "→E"]
                    "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
                                    OF "log-prop-prop:2", THEN "≡E"(2)] "&I")
        fix u
        AOT_have w1  O!u
          using Ordinary.ψ[THEN RN,
                  THEN "fund:2"[unvarify p, OF "log-prop-prop:2", THEN "≡E"(1)],
                  THEN "PossibleWorld.∀E"] by simp
        moreover AOT_have w1  y p]u
          by (safe intro!: world_prop_beta[THEN "PossibleWorld.∀E", THEN "≡E"(2)]
                           0[THEN "&E"(1)])
        ultimately AOT_have w1  (O!u & y p]u)
          using "conj-dist-w:1"[unvarify p q, OF "log-prop-prop:2",
                                OF "log-prop-prop:2", THEN "≡E"(2),
                                OF "&I"] by blast
        AOT_hence x w1  (O!x & y p]x)
          by (rule "∃I")
        AOT_thus w1  u y p]u
          by (metis "conj-dist-w:6" "intro-elim:3:b")
      next
        AOT_show w1  ¬v z O!z & z E z]v
          using "PossibleWorld.∀E" nec_not_ex by fastforce
      qed
      ultimately AOT_show p & ¬p for p
        using "raa-cor:3" by blast
    qed
    ultimately AOT_have yy p] & ¬xy p]
      using "&I" by blast
    AOT_hence F (y[F] & ¬x[F])
      by (metis "existential:1" "prop-prop2:2")
    AOT_thus F (x[F] & ¬y[F])  F (y[F] & ¬x[F])
      by (rule "∨I")
  qed
  ultimately AOT_have Numbers'(x,z O!z & z E z]) &
                       Numbers'(y,z O!z & z E z]) & x  y
    using "&I" by blast
  AOT_thus xy (Numbers'(x,z O!z & z E z]) &
                  Numbers'(y,z O!z & z E z]) & x  y)
    using "∃I"(2)[where β=x] "∃I"(2)[where β=y] by auto
qed

AOT_theorem restricted_identity:
  x =⇩ y  (InDomainOf(x,) & InDomainOf(y,) & x = y)
  by (auto intro!: "≡I" "→I" "&I"
             dest: "id-R-thm:2"[THEN "→E"] "&E"
                   "id-R-thm:3"[THEN "→E"]
                   "id-R-thm:4"[THEN "→E", OF "∨I"(1), THEN "≡E"(2)])

AOT_theorem induction': F ([F]0 & n([F]n  [F]n')  n [F]n)
proof(rule GEN; rule "→I")
  fix F n
  AOT_assume A: [F]0 & n([F]n  [F]n')
  AOT_have nm([]nm  ([F]n  [F]m))
  proof(safe intro!: "Number.GEN" "→I")
    fix n m
    AOT_assume []nm
    moreover AOT_have []n n'
      using "suc-thm".
    ultimately AOT_have m_eq_suc_n: m = n'
      using "pred-func:1"[unvarify z, OF "def-suc[den2]", THEN "→E", OF "&I"]
      by blast
    AOT_assume [F]n
    AOT_hence [F]n'
      using A[THEN "&E"(2), THEN "Number.∀E", THEN "→E"] by blast
    AOT_thus [F]m
      using m_eq_suc_n[symmetric] "rule=E" by fast
  qed
  AOT_thus n[F]n
    using induction[THEN "∀E"(2), THEN "→E", OF "&I", OF A[THEN "&E"(1)]]
    by simp
qed

AOT_define ExtensionOf :: τ  Π  φ (ExtensionOf'(_,_'))
  "exten-property:1": ExtensionOf(x,[G]) df A!x & G & F(x[F]  z([F]z  [G]z))

AOT_define OrdinaryExtensionOf :: τ  Π  φ (OrdinaryExtensionOf'(_,_'))
   OrdinaryExtensionOf(x,[G]) df A!x & G & F(x[F]  z(O!z  ([F]z  [G]z)))

AOT_theorem BeingOrdinaryExtensionOfDenotes:
  x OrdinaryExtensionOf(x,[G])]
proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
  AOT_show x A!x & G & x F(x[F]  z(O!z  ([F]z  [G]z)))]x]
    by "cqt:2"
next
  AOT_show x (A!x & G & x F (x[F]  z (O!z  ([F]z  [G]z)))]x 
            OrdinaryExtensionOf(x,[G]))
  proof(safe intro!: RN GEN)
    AOT_modally_strict {
      fix x
      AOT_modally_strict {
        AOT_have x F (x[F]  z (O!z  ([F]z  [G]z)))]
        proof (safe intro!: "Comprehension_3"[THEN "→E"] RN GEN
                            "→I" "≡I" Ordinary.GEN)
          AOT_modally_strict {
            fix F H u
            AOT_assume H E F
            AOT_hence u([H]u  [F]u)
              using eqE[THEN "dfE", THEN "&E"(2)] "qml:2"[axiom_inst, THEN "→E"]
              by blast
            AOT_hence 0: [H]u  [F]u using "Ordinary.∀E" by fast
            {
              AOT_assume u([F]u  [G]u)
              AOT_hence 1: [F]u  [G]u using "Ordinary.∀E" by fast
              AOT_show [G]u if [H]u using 0 1 "≡E"(1) that by blast
              AOT_show [H]u if [G]u using 0 1 "≡E"(2) that by blast
            }
            {
              AOT_assume u([H]u  [G]u)
              AOT_hence 1: [H]u  [G]u using "Ordinary.∀E" by fast
              AOT_show [G]u if [F]u using 0 1 "≡E"(1,2) that by blast 
              AOT_show [F]u if [G]u using 0 1 "≡E"(1,2) that by blast 
            }
          }
        qed
      }
      AOT_thus (A!x & G & x F (x[F]  z (O!z  ([F]z  [G]z)))]x) 
                OrdinaryExtensionOf(x,[G])
        apply (AOT_subst_def OrdinaryExtensionOf)
        apply (AOT_subst x F (x[F]  z (O!z  ([F]z  [G]z)))]x
                         F (x[F]  z (O!z  ([F]z  [G]z))))
        by (auto intro!: "beta-C-meta"[THEN "→E"] simp: "oth-class-taut:3:a")
    }
  qed
qed

text‹Fragments of PLM's theory of Concepts.›

AOT_define FimpG :: Π  Π  φ (infixl  50)
  "F-imp-G": [G]  [F] df F & G & x ([G]x  [F]x)

AOT_define concept :: Π (C!)
  concepts: C! =df A!

AOT_register_rigid_restricted_type
  Concept: C!κ
proof
  AOT_modally_strict {
    AOT_have x A!x
      using "o-objects-exist:2" "qml:2"[axiom_inst] "→E" by blast
    AOT_thus x C!x
      using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"] "rule=E" id_sym
      by fast
  }
next
  AOT_modally_strict {
    AOT_show C!κ  κ for κ
      using "cqt:5:a"[axiom_inst, THEN "→E", THEN "&E"(2)] "→I"
      by blast
  }
next
  AOT_modally_strict {
    AOT_have x(A!x  A!x)
      by (simp add: "oa-facts:2" GEN)
    AOT_thus x(C!x  C!x)
      using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"] "rule=E" id_sym
      by fast
  }
qed

AOT_register_variable_names
  Concept: c d e

AOT_theorem "concept-comp:1": x(C!x & F(x[F]  φ{F}))
    using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
          "A-objects"[axiom_inst]
          "rule=E" by fast

AOT_theorem "concept-comp:2": ∃!x(C!x & F(x[F]  φ{F}))
    using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
          "A-objects!"
          "rule=E" by fast

AOT_theorem "concept-comp:3": ιx(C!x & F(x[F]  φ{F}))
  using "concept-comp:2" "A-Exists:2"[THEN "≡E"(2)] "RA[2]" by blast

AOT_theorem "concept-comp:4":
  ιx(C!x & F(x[F]  φ{F})) = ιx(A!x & F(x[F]  φ{F}))
    using "=I"(1)[OF "concept-comp:3"]
          "rule=E"[rotated]
          concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2"]
          by fast

AOT_define conceptInclusion :: τ  τ  φ (infixl  100)
  "con:1": c  d df F(c[F]  d[F])


AOT_define conceptOf :: τ  τ  φ (ConceptOf'(_,_'))
  "concept-of-G": ConceptOf(c,G) df G & F (c[F]  [G]  [F])

AOT_theorem ConceptOfOrdinaryProperty: ([H]  O!)  x ConceptOf(x,H)]
proof(rule "→I")
  AOT_assume [H]  O!
  AOT_hence x([H]x  O!x)
    using "F-imp-G"[THEN "dfE"] "&E" by blast
  AOT_hence x([H]x  O!x)
    using "S5Basic:6"[THEN "≡E"(1)] by blast
  moreover AOT_have x([H]x  O!x) 
                     FG((G E F)  ([H]  [F]  [H]  [G]))
  proof(rule RM; safe intro!: "→I" GEN "≡I")
    AOT_modally_strict {
      fix F G
      AOT_assume 0: x([H]x  O!x)
      AOT_assume G E F
      AOT_hence 1: u([G]u  [F]u)
        by (AOT_subst_thm eqE[THEN "≡Df", THEN "≡S"(1), OF "&I",
              OF "cqt:2[const_var]"[axiom_inst],
              OF "cqt:2[const_var]"[axiom_inst], symmetric])
      {
        AOT_assume [H]  [F]
        AOT_hence x([H]x  [F]x)
          using "F-imp-G"[THEN "dfE"] "&E" by blast
        moreover AOT_modally_strict {
          AOT_assume x([H]x  O!x)
          moreover AOT_assume u([G]u  [F]u)
          moreover AOT_assume x([H]x  [F]x)
          ultimately AOT_have [H]x  [G]x for x
            by (auto intro!: "→I" dest!: "∀E"(2) dest: "→E" "≡E")
          AOT_hence x([H]x  [G]x)
            by (rule GEN)
        }
        ultimately AOT_have x([H]x  [G]x)
          using "RN[prem]"[where
              Γ="{«x([H]x  O!x)», «u([G]u  [F]u)», «x([H]x  [F]x)»}"]
          using 0 1 by fast
        AOT_thus [H]  [G]
          by (AOT_subst_def "F-imp-G")
             (safe intro!: "cqt:2" "&I")
      }
      {
        AOT_assume [H]  [G]
        AOT_hence x([H]x  [G]x)
          using "F-imp-G"[THEN "dfE"] "&E" by blast
        moreover AOT_modally_strict {
          AOT_assume x([H]x  O!x)
          moreover AOT_assume u([G]u  [F]u)
          moreover AOT_assume x([H]x  [G]x)
          ultimately AOT_have [H]x  [F]x for x
            by (auto intro!: "→I" dest!: "∀E"(2) dest: "→E" "≡E")
          AOT_hence x([H]x  [F]x)
            by (rule GEN)
        }
        ultimately AOT_have x([H]x  [F]x)
          using "RN[prem]"[where
              Γ="{«x([H]x  O!x)», «u([G]u  [F]u)», «x([H]x  [G]x)»}"]
          using 0 1 by fast
        AOT_thus [H]  [F]
          by (AOT_subst_def "F-imp-G")
             (safe intro!: "cqt:2" "&I")
      }
    }
  qed
  ultimately AOT_have FG((G E F)  ([H]  [F]  [H]  [G]))
    using "→E" by blast
  AOT_hence 0: x F(x[F]  ([H]  [F]))]
    using Comprehension_3[THEN "→E"] by blast
  AOT_show x ConceptOf(x,H)]
  proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show x C!x & x F(x[F]  ([H]  [F]))]x] by "cqt:2"
  next
    AOT_show x (C!x & x F (x[F]  [H]  [F])]x  ConceptOf(x,H))
    proof (rule "RN[prem]"[where Γ={«x F(x[F]  ([H]  [F]))]»}, simplified])
      AOT_modally_strict {
        AOT_assume 0: x F (x[F]  [H]  [F])]
        AOT_show x (C!x & x F (x[F]  [H]  [F])]x  ConceptOf(x,H))
        proof(safe intro!: GEN "≡I" "→I" "&I")
          fix x
          AOT_assume C!x & x F (x[F]  [H]  [F])]x
          AOT_thus ConceptOf(x,H)
            by (AOT_subst_def "concept-of-G")
               (auto intro!: "&I" "cqt:2" dest: "&E" "β→C")
        next
          fix x
          AOT_assume ConceptOf(x,H)
          AOT_hence C!x & (H & F(x[F]  [H]  [F]))
            by (AOT_subst_def (reverse) "concept-of-G")
          AOT_thus C!x and x F(x[F]  [H]  [F])]x
            by (auto intro!: "β←C" 0 "cqt:2" dest: "&E")
        qed
      }
    next
      AOT_show x F(x[F]  ([H]  [F]))]
        using "exist-nec"[THEN "→E"] 0 by blast
    qed
  qed
qed

AOT_theorem "con-exists:1": c ConceptOf(c,G)
proof -
  AOT_obtain c where F (c[F]  [G]  [F])
    using "concept-comp:1" "Concept.∃E"[rotated] by meson
  AOT_hence ConceptOf(c,G)
    by (auto intro!: "concept-of-G"[THEN "dfI"] "&I" "cqt:2" Concept.ψ)
  thus ?thesis by (rule "Concept.∃I")
qed

AOT_theorem "con-exists:2": ∃!c ConceptOf(c,G)
proof -
  AOT_have ∃!c F (c[F]  [G]  [F])
    using "concept-comp:2" by simp
  moreover {
    AOT_modally_strict {
      fix x
      AOT_assume F (x[F]  [G]  [F])
      moreover AOT_have [G]  [G]
        by (safe intro!: "F-imp-G"[THEN "dfI"] "&I" "cqt:2" RN GEN "→I")
      ultimately AOT_have x[G]
        using "∀E"(2) "≡E" by blast
      AOT_hence A!x
        using "encoders-are-abstract"[THEN "→E", OF "∃I"(2)] by simp
      AOT_hence C!x
        using concepts[THEN "rule-id-df:1[zero]", OF "oa-exist:2", symmetric]
              "rule=E"[rotated]
        by fast
    }
  }
  ultimately show ?thesis
    by (AOT_subst ConceptOf(c,G) F (c[F]  [G]  [F]) for: c;
           AOT_subst_def "concept-of-G")
       (auto intro!: "≡I" "→I" "&I" "cqt:2" Concept.ψ dest: "&E")
qed

AOT_theorem "con-exists:3": ιc ConceptOf(c,G)
  by (safe intro!: "A-Exists:2"[THEN "≡E"(2)] "con-exists:2"[THEN "RA[2]"])


AOT_define theConceptOfG :: τ  κs (c_›)
  "concept-G": cG =df ιc ConceptOf(c, G)

AOT_theorem "concept-G[den]": cG
  by (auto intro!: "rule-id-df:1"[OF "concept-G"]
                   "t=t-proper:1"[THEN "→E"]
                   "con-exists:3")


AOT_theorem "concept-G[concept]": C!cG
proof -
  AOT_have 𝒜(C!cG & ConceptOf(cG, G))
    by (auto intro!: "actual-desc:2"[unvarify x, THEN "→E"]
                     "rule-id-df:1"[OF "concept-G"]
                     "concept-G[den]"
                     "con-exists:3")
  AOT_hence 𝒜C!cG
    by (metis "Act-Basic:2" "con-dis-i-e:2:a" "intro-elim:3:a")
  AOT_hence 𝒜A!cG
    using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"]
          "rule=E" by fast
  AOT_hence A!cG
    using "oa-facts:8"[unvarify x, THEN "≡E"(2)] "concept-G[den]" by blast
  thus ?thesis
    using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2", symmetric]
          "rule=E" by fast
qed

AOT_theorem "conG-strict": cG = ιc F(c[F]  [G]  [F])
proof (rule "id-eq:3"[unvarify α β γ, THEN "→E"])
  AOT_have x (C!x & ConceptOf(x,G)  C!x & F (x[F]  [G]  [F]))
    by (auto intro!: "concept-of-G"[THEN "dfI"] RN GEN "≡I" "→I" "&I" "cqt:2"
               dest: "&E";
        auto dest: "∀E"(2) "≡E"(1,2) dest!: "&E"(2) "concept-of-G"[THEN "dfE"])
  AOT_thus cG = ιc ConceptOf(c, G) & ιc ConceptOf(c, G) = ιc F(c[F]  [G]  [F])
    by (auto intro!: "&I" "rule-id-df:1"[OF "concept-G"] "con-exists:3"
                      "equiv-desc-eq:3"[THEN "→E"])
qed(auto simp: "concept-G[den]" "con-exists:3" "concept-comp:3")


AOT_theorem "conG-lemma:1": F(cG[F]  [G]  [F])
proof(safe intro!: GEN "≡I" "→I")
  fix F
  AOT_have 𝒜F(cG[F]  [G]  [F])
    using "actual-desc:4"[THEN "→E", OF "concept-comp:3",
                          THEN "Act-Basic:2"[THEN "≡E"(1)],
                          THEN "&E"(2)]
          "conG-strict"[symmetric] "rule=E" by fast
  AOT_hence 𝒜(cG[F]  [G]  [F])
    using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] "∀E"(2)
    by blast
  AOT_hence 0: 𝒜cG[F]  𝒜[G]  [F]
    using "Act-Basic:5"[THEN "≡E"(1)] by blast
  {
    AOT_assume cG[F]
    AOT_hence 𝒜cG[F]
      by(safe intro!: "en-eq:10[1]"[unvarify x1, THEN "≡E"(2)]
                      "concept-G[den]")
    AOT_hence 𝒜[G]  [F]
      using 0[THEN "≡E"(1)] by blast
    AOT_hence 𝒜(F & G & x([G]x  [F]x))
      by (AOT_subst_def (reverse) "F-imp-G")
    AOT_hence 𝒜x([G]x  [F]x)
      using "Act-Basic:2"[THEN "≡E"(1)] "&E" by blast
    AOT_hence x([G]x  [F]x)
      using "qml-act:2"[axiom_inst, THEN "≡E"(2)] by simp
    AOT_thus [G]  [F]
      by (AOT_subst_def "F-imp-G"; auto intro!: "&I" "cqt:2")
  }
  {
    AOT_assume [G]  [F]
    AOT_hence x([G]x  [F]x)
      by (safe dest!: "F-imp-G"[THEN "dfE"] "&E"(2))
    AOT_hence 𝒜x([G]x  [F]x)
      using "qml-act:2"[axiom_inst, THEN "≡E"(1)] by simp
    AOT_hence 𝒜(F & G & x([G]x  [F]x))
      by (auto intro!: "Act-Basic:2"[THEN "≡E"(2)] "&I" "cqt:2"
               intro: "RA[2]")
    AOT_hence 𝒜([G]  [F])
      by (AOT_subst_def "F-imp-G")
    AOT_hence 𝒜cG[F]
      using 0[THEN "≡E"(2)] by blast
    AOT_thus cG[F]
      by(safe intro!: "en-eq:10[1]"[unvarify x1, THEN "≡E"(1)]
                      "concept-G[den]")
  }
qed

AOT_theorem conH_enc_ord:
  ([H]  O!)  F G (G E F  (cH[F]  cH[G]))
proof(rule "→I")
  AOT_assume 0: [H]  O!
  AOT_have 0: ([H]  O!)
    apply (AOT_subst_def "F-imp-G")
    using 0[THEN "dfE"[OF "F-imp-G"]]
    by (auto intro!: "KBasic:3"[THEN "≡E"(2)] "&I" "exist-nec"[THEN "→E"]
               dest: "&E" 4[THEN "→E"])
  moreover AOT_have ([H]  O!)  F G (G E F  (cH[F]  cH[G]))
  proof(rule RM; safe intro!: "→I" GEN)
    AOT_modally_strict {
      fix F G
      AOT_assume [H]  O!
      AOT_hence 0: x ([H]x  O!x)
        by (safe dest!: "F-imp-G"[THEN "dfE"] "&E"(2))
      AOT_assume 1: G E F
      AOT_assume cH[F]
      AOT_hence [H]  [F]
        using "conG-lemma:1"[THEN "∀E"(2), THEN "≡E"(1)] by simp
      AOT_hence 2: x ([H]x  [F]x)
        by (safe dest!: "F-imp-G"[THEN "dfE"] "&E"(2))
      AOT_modally_strict {
        AOT_assume 0: x ([H]x  O!x)
        AOT_assume 1: x ([H]x  [F]x)
        AOT_assume 2: G E F
        AOT_have x ([H]x  [G]x)
        proof(safe intro!: GEN "→I")
          fix x
          AOT_assume [H]x
          AOT_hence O!x and [F]x
            using 0 1 "∀E"(2) "→E" by blast+
          AOT_thus [G]x
            using 2[THEN eqE[THEN "dfE"], THEN "&E"(2)]
                  "∀E"(2) "→E" "≡E"(2) calculation by blast
        qed
      }
      AOT_hence x ([H]x  [G]x)
        using "RN[prem]"[where Γ={«x ([H]x  O!x)»,
                               «x ([H]x  [F]x)»,
                               «G E F»}, simplified] 0 1 2 by fast
      AOT_hence [H]  [G]
        by (safe intro!: "F-imp-G"[THEN "dfI"] "&I" "cqt:2")
      AOT_hence cH[G]
        using "conG-lemma:1"[THEN "∀E"(2), THEN "≡E"(2)] by simp
    } note 0 = this
    AOT_modally_strict {
      fix F G
      AOT_assume [H]  O!
      moreover AOT_assume G E F
      moreover AOT_have F E G
        by (AOT_subst F E G G E F)
            (auto intro!: calculation(2)
                          eqE[THEN "dfI"]
                          "≡I" "→I" "&I" "cqt:2" Ordinary.GEN
                  dest!: eqE[THEN "dfE"] "&E"(2)
                  dest: "≡E"(1,2) "Ordinary.∀E")
      ultimately AOT_show (cH[F]  cH[G])
        using 0 "≡I" "→I" by auto
    }
  qed
  ultimately AOT_show F G (G E F  (cH[F]  cH[G]))
    using "→E" by blast
qed

AOT_theorem concept_inclusion_denotes_1:
  ([H]  O!)  x cH  x]
proof(rule "→I")
  AOT_assume 0: [H]  O!
  AOT_show x cH  x]
  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show x C!x & F(cH[F]  x[F])]
      by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
                       Comprehension_2'[THEN "→E"]
                       conH_enc_ord[THEN "→E", OF 0]) "cqt:2"
  next
    AOT_show x (C!x & F (cH[F]  x[F])  cH  x)
      by (safe intro!: RN GEN; AOT_subst_def "con:1")
         (auto intro!: "≡I" "→I" "&I" "concept-G[concept]" dest: "&E")
  qed
qed

AOT_theorem concept_inclusion_denotes_2:
  ([H]  O!)  x x  cH]
proof(rule "→I")
  AOT_assume 0: [H]  O!
  AOT_show x x  cH]
  proof(rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show x C!x & F(x[F]  cH[F])]
      by (safe intro!: conjunction_denotes[THEN "→E", OF "&I"]
                       Comprehension_1'[THEN "→E"]
                       conH_enc_ord[THEN "→E", OF 0]) "cqt:2"
  next
    AOT_show x (C!x & F (x[F]  cH[F])  x  cH)
      by (safe intro!: RN GEN; AOT_subst_def "con:1")
         (auto intro!: "≡I" "→I" "&I" "concept-G[concept]" dest: "&E")
  qed
qed

AOT_define ThickForm :: τ  τ  φ (FormOf'(_,_'))
  "tform-of": FormOf(x,G) df A!x & G & F(x[F]  [G]  [F])

AOT_theorem FormOfOrdinaryProperty: ([H]  O!)  x FormOf(x,H)]
proof(rule "→I")
  AOT_assume 0: [H]  [O!]
  AOT_show x FormOf(x,H)]
  proof (rule "safe-ext"[axiom_inst, THEN "→E", OF "&I"])
    AOT_show x ConceptOf(x,H)]
      using 0 ConceptOfOrdinaryProperty[THEN "→E"] by blast
    AOT_show x (ConceptOf(x,H)  FormOf(x,H))
    proof(safe intro!: RN GEN)
      AOT_modally_strict {
        fix x
        AOT_modally_strict {
          AOT_have A!x  A!x
            by (simp add: "oth-class-taut:3:a")
          AOT_hence C!x  A!x
            using "rule-id-df:1[zero]"[OF concepts, OF "oa-exist:2"]
                  "rule=E" id_sym by fast
        }
        AOT_thus ConceptOf(x,H)  FormOf(x,H)
          by (AOT_subst_def "tform-of";
              AOT_subst_def "concept-of-G";
              AOT_subst C!x A!x)
             (auto intro!: "≡I" "→I" "&I" dest: "&E")
      }
    qed
  qed
qed

AOT_theorem equal_E_rigid_one_to_one: Rigid1-1((=E))
proof (safe intro!: "df-1-1:2"[THEN "dfI"] "&I" "df-1-1:1"[THEN "dfI"]
                    GEN "→I" "df-rigid-rel:1"[THEN "dfI"] "=E[denotes]")
  fix x y z
  AOT_assume x =E z & y =E z
  AOT_thus x = y
    by (metis "rule=E" "&E"(1) "Conjunction Simplification"(2)
              "=E-simple:2" id_sym "→E")
next
  AOT_have xy (x =E y  x =E y)
  proof(rule GEN; rule GEN)
    AOT_show (x =E y  x =E y) for x y
      by (meson RN "deduction-theorem" "id-nec3:1" "≡E"(1))
  qed
  AOT_hence x1...∀xn ([(=E)]x1...xn  [(=E)]x1...xn)
    by (rule tuple_forall[THEN "dfI"])
  AOT_thus x1...∀xn ([(=E)]x1...xn  [(=E)]x1...xn)
    using BF[THEN "→E"] by fast
qed

AOT_theorem equal_E_domain: InDomainOf(x,(=E))  O!x
proof(safe intro!: "≡I" "→I")
  AOT_assume InDomainOf(x,(=E))
  AOT_hence y x =E y
    by (metis "dfE" "df-1-1:5")
  then AOT_obtain y where x =E y
    using "∃E"[rotated] by blast
  AOT_thus O!x
    using "=E-simple:1"[THEN "≡E"(1)] "&E" by blast
next
  AOT_assume O!x
  AOT_hence x =E x   
    by (metis "ord=Eequiv:1"[THEN "→E"])
  AOT_hence y x =E y
    using "∃I"(2) by fast
  AOT_thus InDomainOf(x,(=E))
    by (metis "dfI" "df-1-1:5")
qed

AOT_theorem shared_urelement_projection_identity:
  assumes y x (yz [R]zx])]
  shows F([F]a  [F]b)  z [R]za] = z [R]zb]
proof(rule "→I")
  AOT_assume 0: F([F]a  [F]b)
  {
    fix z
    AOT_have x (zz [R]zx])]
      using assms[THEN "∀E"(2)].
    AOT_hence 1: x y (F ([F]x  [F]y)  (zz [R]zx]  zz [R]zy]))
      using "kirchner-thm-cor:1"[THEN "→E"]
      by blast
    AOT_have (zz [R]za]  zz [R]zb])
      using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
  }
  AOT_hence z (zz [R]za]  zz [R]zb])
    by (rule GEN)
  AOT_hence z(zz [R]za]  zz [R]zb])
    by (rule BF[THEN "→E"])
  AOT_thus z [R]za] = z [R]zb]
    by (AOT_subst_def "identity:2")
       (auto intro!: "&I" "cqt:2")
qed

AOT_theorem shared_urelement_exemplification_identity:
  assumes y x (yz [G]x])]
  shows F([F]a  [F]b)  ([G]a) = ([G]b)
proof(rule "→I")
  AOT_assume 0: F([F]a  [F]b)
  {
    fix z
    AOT_have x (zz [G]x])]
      using assms[THEN "∀E"(2)].
    AOT_hence 1: x y (F ([F]x  [F]y)  (zz [G]x]  zz [G]y]))
      using "kirchner-thm-cor:1"[THEN "→E"]
      by blast
    AOT_have (zz [G]a]  zz [G]b])
      using 1[THEN "∀E"(2), THEN "∀E"(2), THEN "→E", OF 0] by blast
  }
  AOT_hence z (zz [G]a]  zz [G]b])
    by (rule GEN)
  AOT_hence z(zz [G]a]  zz [G]b])
    by (rule BF[THEN "→E"])
  AOT_hence z [G]a] = z [G]b]
    by (AOT_subst_def "identity:2")
       (auto intro!: "&I" "cqt:2")
  AOT_thus ([G]a) = ([G]b)
    by (safe intro!: "identity:4"[THEN "dfI"] "&I" "log-prop-prop:2")
qed

text‹The assumptions of the theorems above are derivable, if the additional
     introduction rules for the upcoming extension of @{thm "cqt:2[lambda]"}
     are explicitly allowed (while they are currently not part of the
     abstraction layer).›
notepad
begin
  AOT_modally_strict {
    AOT_have Ry x (yz [R]zx])]
      by (safe intro!: GEN "cqt:2" AOT_instance_of_cqt_2_intro_next)
    AOT_have Gy x (yz [G]x])]
      by (safe intro!: GEN "cqt:2" AOT_instance_of_cqt_2_intro_next)
  }
end

end