Theory AOT_PLM

(*<*)
theory AOT_PLM
  imports AOT_Axioms
begin
(*>*)

section‹The Deductive System PLM›
text‹\label{PLM: 9}›

(* constrain sledgehammer to the abstraction layer *)
unbundle AOT_no_atp

subsection‹Primitive Rule of PLM: Modus Ponens›
text‹\label{PLM: 9.1}›

AOT_theorem "modus-ponens":
  assumes ‹φ› and ‹φ → ψ›
  shows ‹ψ›
  (* NOTE: semantics needed *)
  using assms by (simp add: AOT_sem_imp)
lemmas MP = "modus-ponens"

subsection‹(Modally Strict) Proofs and Derivations›
text‹\label{PLM: 9.2}›

AOT_theorem "non-con-thm-thm":
  assumes ‹❙⊢⇩_□ φ›
  shows ‹❙⊢ φ›
  using assms by simp

AOT_theorem "vdash-properties:1[1]":
  assumes ‹φ ∈ Λ›
  shows ‹❙⊢ φ›
  (* NOTE: semantics needed *)
  using assms unfolding AOT_model_act_axiom_def by blast

text‹Convenience attribute for instantiating modally-fragile axioms.›
attribute_setup act_axiom_inst =
  ‹Scan.succeed (Thm.rule_attribute []
    (K (fn thm => thm RS @{thm "vdash-properties:1[1]"})))›
  "Instantiate modally fragile axiom as modally fragile theorem."

AOT_theorem "vdash-properties:1[2]":
  assumes ‹φ ∈ Λ⇩_□›
  shows ‹❙⊢⇩_□ φ›
  (* NOTE: semantics needed *)
  using assms unfolding AOT_model_axiom_def by blast

text‹Convenience attribute for instantiating modally-strict axioms.›
attribute_setup axiom_inst =
  ‹Scan.succeed (Thm.rule_attribute []
    (K (fn thm => thm RS @{thm "vdash-properties:1[2]"})))›
  "Instantiate axiom as theorem."

text‹Convenience methods and theorem sets for applying "cqt:2".›
method cqt_2_lambda_inst_prover =
  (fast intro: AOT_instance_of_cqt_2_intro)
method "cqt:2[lambda]" =
  (rule "cqt:2[lambda]"[axiom_inst]; cqt_2_lambda_inst_prover)
lemmas "cqt:2" =
  "cqt:2[const_var]"[axiom_inst] "cqt:2[lambda]"[axiom_inst]
  AOT_instance_of_cqt_2_intro
method "cqt:2" = (safe intro!: "cqt:2")

AOT_theorem "vdash-properties:3":
  assumes ‹❙⊢⇩_□ φ›
  shows ‹Γ ❙⊢ φ›
  using assms by blast

AOT_theorem "vdash-properties:5":
  assumes ‹Γ⇩₁ ❙⊢ φ› and ‹Γ⇩₂ ❙⊢ φ → ψ›
  shows ‹Γ⇩₁, Γ⇩₂ ❙⊢ ψ›
  using MP assms by blast

AOT_theorem "vdash-properties:6":
  assumes ‹φ› and ‹φ → ψ›
  shows ‹ψ›
  using MP assms by blast

AOT_theorem "vdash-properties:8":
  assumes ‹Γ ❙⊢ φ› and ‹φ ❙⊢ ψ›
  shows ‹Γ ❙⊢ ψ›
  using assms by argo

AOT_theorem "vdash-properties:9":
  assumes ‹φ›
  shows ‹ψ → φ›
  using MP "pl:1"[axiom_inst] assms by blast

AOT_theorem "vdash-properties:10":
  assumes ‹φ → ψ› and ‹φ›
  shows ‹ψ›
  using MP assms by blast
lemmas "→E" = "vdash-properties:10"

subsection‹Two Fundamental Metarules: GEN and RN›
text‹\label{PLM: 9.3}›

AOT_theorem "rule-gen":
  assumes ‹for arbitrary α: φ{α}›
  shows ‹∀α φ{α}›
  (* NOTE: semantics needed *)
  using assms by (metis AOT_var_of_term_inverse AOT_sem_denotes AOT_sem_forall)
lemmas GEN = "rule-gen"

AOT_theorem "RN[prem]":
  assumes ‹Γ ❙⊢⇩_□ φ›
  shows ‹□Γ ❙⊢⇩_□ □φ›
  by (meson AOT_sem_box assms image_iff) (* NOTE: semantics needed *)
AOT_theorem RN:
  assumes ‹❙⊢⇩_□ φ›
  shows ‹□φ›
  using "RN[prem]" assms by blast

subsection‹The Inferential Role of Definitions›
text‹\label{PLM: 9.4}›

AOT_axiom "df-rules-formulas[1]":
  assumes ‹φ ≡⇩_d⇩_f ψ›
  shows ‹φ → ψ›
  (* NOTE: semantics needed *)
  using assms
  by (auto simp: assms AOT_model_axiomI AOT_model_equiv_def AOT_sem_imp)
AOT_axiom "df-rules-formulas[2]":
  assumes ‹φ ≡⇩_d⇩_f ψ›
  shows ‹ψ → φ›
  (* NOTE: semantics needed *)
  using assms
  by (auto simp: AOT_model_axiomI AOT_model_equiv_def AOT_sem_imp)
(* NOTE: for convenience also state the above as regular theorems *)
AOT_theorem "df-rules-formulas[3]":
  assumes ‹φ ≡⇩_d⇩_f ψ›
  shows ‹φ → ψ›
  using "df-rules-formulas[1]"[axiom_inst, OF assms].
AOT_theorem "df-rules-formulas[4]":
  assumes ‹φ ≡⇩_d⇩_f ψ›
  shows ‹ψ → φ›
  using "df-rules-formulas[2]"[axiom_inst, OF assms].


AOT_axiom "df-rules-terms[1]":
  assumes ‹τ{α⇩₁...α⇩_n} =⇩_d⇩_f σ{α⇩₁...α⇩_n}›
  shows ‹(σ{τ⇩₁...τ⇩_n}↓ → τ{τ⇩₁...τ⇩_n} = σ{τ⇩₁...τ⇩_n}) &
         (¬σ{τ⇩₁...τ⇩_n}↓ → ¬τ{τ⇩₁...τ⇩_n}↓)›
  (* NOTE: semantics needed *)
  using assms
  by (simp add: AOT_model_axiomI AOT_sem_conj AOT_sem_imp AOT_sem_eq
                AOT_sem_not AOT_sem_denotes AOT_model_id_def)
AOT_axiom "df-rules-terms[2]":
  assumes ‹τ =⇩_d⇩_f σ›
  shows ‹(σ↓ → τ = σ) & (¬σ↓ → ¬τ↓)›
  by (metis "df-rules-terms[1]" case_unit_Unity assms)
(* NOTE: for convenience also state the above as regular theorems *)
AOT_theorem "df-rules-terms[3]":
  assumes ‹τ{α⇩₁...α⇩_n} =⇩_d⇩_f σ{α⇩₁...α⇩_n}›
  shows ‹(σ{τ⇩₁...τ⇩_n}↓ → τ{τ⇩₁...τ⇩_n} = σ{τ⇩₁...τ⇩_n}) &
         (¬σ{τ⇩₁...τ⇩_n}↓ → ¬τ{τ⇩₁...τ⇩_n}↓)›
  using "df-rules-terms[1]"[axiom_inst, OF assms].
AOT_theorem "df-rules-terms[4]":
  assumes ‹τ =⇩_d⇩_f σ›
  shows ‹(σ↓ → τ = σ) & (¬σ↓ → ¬τ↓)›
  using "df-rules-terms[2]"[axiom_inst, OF assms].

subsection‹The Theory of Negations and Conditionals›
text‹\label{PLM: 9.5}›

AOT_theorem "if-p-then-p": ‹φ → φ›
  by (meson "pl:1"[axiom_inst] "pl:2"[axiom_inst] MP)

AOT_theorem "deduction-theorem":
  assumes ‹φ ❙⊢ ψ›
  shows ‹φ → ψ›
  (* NOTE: semantics needed *)
  using assms by (simp add: AOT_sem_imp)
lemmas CP = "deduction-theorem"
lemmas "→I" = "deduction-theorem"

AOT_theorem "ded-thm-cor:1":
  assumes ‹Γ⇩₁ ❙⊢ φ → ψ› and ‹Γ⇩₂ ❙⊢ ψ → χ›
  shows ‹Γ⇩₁, Γ⇩₂ ❙⊢ φ → χ›
  using "→E" "→I" assms by blast
AOT_theorem "ded-thm-cor:2":
  assumes ‹Γ⇩₁ ❙⊢ φ → (ψ → χ)› and ‹Γ⇩₂ ❙⊢ ψ›
  shows ‹Γ⇩₁, Γ⇩₂ ❙⊢ φ → χ›
  using "→E" "→I" assms by blast

AOT_theorem "ded-thm-cor:3":
  assumes ‹φ → ψ› and ‹ψ → χ›
  shows ‹φ → χ›
  using "→E" "→I" assms by blast
declare "ded-thm-cor:3"[trans]
AOT_theorem "ded-thm-cor:4":
  assumes ‹φ → (ψ → χ)› and ‹ψ›
  shows ‹φ → χ›
  using "→E" "→I" assms by blast

lemmas "Hypothetical Syllogism" = "ded-thm-cor:3"

AOT_theorem "useful-tautologies:1": ‹¬¬φ → φ›
  by (metis "pl:3"[axiom_inst] "→I" "Hypothetical Syllogism")
AOT_theorem "useful-tautologies:2": ‹φ → ¬¬φ›
  by (metis "pl:3"[axiom_inst] "→I" "ded-thm-cor:4")
AOT_theorem "useful-tautologies:3": ‹¬φ → (φ → ψ)›
  by (meson "ded-thm-cor:4" "pl:3"[axiom_inst] "→I")
AOT_theorem "useful-tautologies:4": ‹(¬ψ → ¬φ) → (φ → ψ)›
  by (meson "pl:3"[axiom_inst] "Hypothetical Syllogism" "→I")
AOT_theorem "useful-tautologies:5": ‹(φ → ψ) → (¬ψ → ¬φ)›
  by (metis "useful-tautologies:4" "Hypothetical Syllogism" "→I")

AOT_theorem "useful-tautologies:6": ‹(φ → ¬ψ) → (ψ → ¬φ)›
  by (metis "→I" MP "useful-tautologies:4")

AOT_theorem "useful-tautologies:7": ‹(¬φ → ψ) → (¬ψ → φ)›
  by (metis "→I" MP "useful-tautologies:3" "useful-tautologies:5")

AOT_theorem "useful-tautologies:8": ‹φ → (¬ψ → ¬(φ → ψ))›
  by (metis "→I" MP "useful-tautologies:5")

AOT_theorem "useful-tautologies:9": ‹(φ → ψ) → ((¬φ → ψ) → ψ)›
  by (metis "→I" MP "useful-tautologies:6")

AOT_theorem "useful-tautologies:10": ‹(φ → ¬ψ) → ((φ → ψ) → ¬φ)›
  by (metis "→I" MP "pl:3"[axiom_inst])

AOT_theorem "dn-i-e:1":
  assumes ‹φ›
  shows ‹¬¬φ›
  using MP "useful-tautologies:2" assms by blast
lemmas "¬¬I" = "dn-i-e:1"
AOT_theorem "dn-i-e:2":
  assumes ‹¬¬φ›
  shows ‹φ›
  using MP "useful-tautologies:1" assms by blast
lemmas "¬¬E" = "dn-i-e:2"

AOT_theorem "modus-tollens:1":
  assumes ‹φ → ψ› and ‹¬ψ›
  shows ‹¬φ›
  using MP "useful-tautologies:5" assms by blast
AOT_theorem "modus-tollens:2":
  assumes ‹φ → ¬ψ› and ‹ψ›
  shows ‹¬φ›
  using "¬¬I" "modus-tollens:1" assms by blast
lemmas MT = "modus-tollens:1" "modus-tollens:2"

AOT_theorem "contraposition:1[1]":
  assumes ‹φ → ψ›
  shows ‹¬ψ → ¬φ›
  using "→I" MT(1) assms by blast
AOT_theorem "contraposition:1[2]":
  assumes ‹¬ψ → ¬φ›
  shows ‹φ → ψ›
  using "→I" "¬¬E" MT(2) assms by blast

AOT_theorem "contraposition:2":
  assumes ‹φ → ¬ψ›
  shows ‹ψ → ¬φ›
  using "→I" MT(2) assms by blast

AOT_theorem "reductio-aa:1":
  assumes ‹¬φ ❙⊢ ¬ψ› and ‹¬φ ❙⊢ ψ›
  shows ‹φ›
  using "→I" "¬¬E" MT(2) assms by blast
AOT_theorem "reductio-aa:2":
  assumes ‹φ ❙⊢ ¬ψ› and ‹φ ❙⊢ ψ›
  shows ‹¬φ›
  using "reductio-aa:1" assms by blast
lemmas "RAA" = "reductio-aa:1" "reductio-aa:2"

AOT_theorem "exc-mid": ‹φ ∨ ¬φ›
  using "df-rules-formulas[4]" "if-p-then-p" MP
        "conventions:2" by blast

AOT_theorem "non-contradiction": ‹¬(φ & ¬φ)›
  using "df-rules-formulas[3]" MT(2) "useful-tautologies:2"
        "conventions:1" by blast

AOT_theorem "con-dis-taut:1": ‹(φ & ψ) → φ›
  by (meson "→I" "df-rules-formulas[3]" MP RAA(1) "conventions:1")
AOT_theorem "con-dis-taut:2": ‹(φ & ψ) → ψ›
  by (metis "→I" "df-rules-formulas[3]" MT(2) RAA(2)
            "¬¬E" "conventions:1")
lemmas "Conjunction Simplification" = "con-dis-taut:1" "con-dis-taut:2"

AOT_theorem "con-dis-taut:3": ‹φ → (φ ∨ ψ)›
  by (meson "contraposition:1[2]" "df-rules-formulas[4]"
            MP "→I" "conventions:2")
AOT_theorem "con-dis-taut:4": ‹ψ → (φ ∨ ψ)›
  using "Hypothetical Syllogism" "df-rules-formulas[4]"
        "pl:1"[axiom_inst] "conventions:2" by blast
lemmas "Disjunction Addition" = "con-dis-taut:3" "con-dis-taut:4"

AOT_theorem "con-dis-taut:5": ‹φ → (ψ → (φ & ψ))›
  by (metis "contraposition:2" "Hypothetical Syllogism" "→I"
            "df-rules-formulas[4]" "conventions:1")
lemmas Adjunction = "con-dis-taut:5"

AOT_theorem "con-dis-taut:6": ‹(φ & φ) ≡ φ›
  by (metis Adjunction "→I" "df-rules-formulas[4]" MP
            "Conjunction Simplification"(1) "conventions:3")
lemmas "Idempotence of &" = "con-dis-taut:6"

AOT_theorem "con-dis-taut:7": ‹(φ ∨ φ) ≡ φ›
proof -
  {
    AOT_assume ‹φ ∨ φ›
    AOT_hence ‹¬φ → φ›
      using "conventions:2"[THEN "df-rules-formulas[3]"] MP by blast
    AOT_hence ‹φ› using "if-p-then-p" RAA(1) MP by blast
  }
  moreover {
    AOT_assume ‹φ›
    AOT_hence ‹φ ∨ φ› using "Disjunction Addition"(1) MP by blast
  }
  ultimately AOT_show ‹(φ ∨ φ) ≡ φ›
    using "conventions:3"[THEN "df-rules-formulas[4]"] MP
    by (metis Adjunction "→I")
qed
lemmas "Idempotence of ∨" = "con-dis-taut:7"


AOT_theorem "con-dis-i-e:1":
  assumes ‹φ› and ‹ψ›
  shows ‹φ & ψ›
  using Adjunction MP assms by blast
lemmas "&I" = "con-dis-i-e:1"

AOT_theorem "con-dis-i-e:2:a":
  assumes ‹φ & ψ›
  shows ‹φ›
  using "Conjunction Simplification"(1) MP assms by blast
AOT_theorem "con-dis-i-e:2:b":
  assumes ‹φ & ψ›
  shows ‹ψ›
  using "Conjunction Simplification"(2) MP assms by blast
lemmas "&E" = "con-dis-i-e:2:a" "con-dis-i-e:2:b"

AOT_theorem "con-dis-i-e:3:a":
  assumes ‹φ›
  shows ‹φ ∨ ψ›
  using "Disjunction Addition"(1) MP assms by blast
AOT_theorem "con-dis-i-e:3:b":
  assumes ‹ψ›
  shows ‹φ ∨ ψ›
  using "Disjunction Addition"(2) MP assms by blast
AOT_theorem "con-dis-i-e:3:c":
  assumes ‹φ ∨ ψ› and ‹φ → χ› and ‹ψ → Θ›
  shows ‹χ ∨ Θ›
  by (metis "con-dis-i-e:3:a" "Disjunction Addition"(2)
            "df-rules-formulas[3]" MT(1) RAA(1)
            "conventions:2" assms)
lemmas "∨I" = "con-dis-i-e:3:a" "con-dis-i-e:3:b" "con-dis-i-e:3:c"

AOT_theorem "con-dis-i-e:4:a":
  assumes ‹φ ∨ ψ› and ‹φ → χ› and ‹ψ → χ›
  shows ‹χ›
  by (metis MP RAA(2) "df-rules-formulas[3]" "conventions:2" assms)
AOT_theorem "con-dis-i-e:4:b":
  assumes ‹φ ∨ ψ› and ‹¬φ›
  shows ‹ψ›
  using "con-dis-i-e:4:a" RAA(1) "→I" assms by blast
AOT_theorem "con-dis-i-e:4:c":
  assumes ‹φ ∨ ψ› and ‹¬ψ›
  shows ‹φ›
  using "con-dis-i-e:4:a" RAA(1) "→I" assms by blast
lemmas "∨E" = "con-dis-i-e:4:a" "con-dis-i-e:4:b" "con-dis-i-e:4:c"

AOT_theorem "raa-cor:1":
  assumes ‹¬φ ❙⊢ ψ & ¬ψ›
  shows ‹φ›
  using "&E" "∨E"(3) "∨I"(2) RAA(2) assms by blast
AOT_theorem "raa-cor:2":
  assumes ‹φ ❙⊢ ψ & ¬ψ›
  shows ‹¬φ›
  using "raa-cor:1" assms by blast
AOT_theorem "raa-cor:3":
  assumes ‹φ› and ‹¬ψ ❙⊢ ¬φ›
  shows ‹ψ›
  using RAA assms by blast
AOT_theorem "raa-cor:4":
  assumes ‹¬φ› and ‹¬ψ ❙⊢ φ›
  shows ‹ψ›
  using RAA assms by blast
AOT_theorem "raa-cor:5":
  assumes ‹φ› and ‹ψ ❙⊢ ¬φ›
  shows ‹¬ψ›
  using RAA assms by blast
AOT_theorem "raa-cor:6":
  assumes ‹¬φ› and ‹ψ ❙⊢ φ›
  shows ‹¬ψ›
  using RAA assms by blast

AOT_theorem "oth-class-taut:1:a": ‹(φ → ψ) ≡ ¬(φ & ¬ψ)›
  by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
     (metis "&E" "&I" "raa-cor:3" "→I" MP)
AOT_theorem "oth-class-taut:1:b": ‹¬(φ → ψ) ≡ (φ & ¬ψ)›
  by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
     (metis "&E" "&I" "raa-cor:3" "→I" MP)
AOT_theorem "oth-class-taut:1:c": ‹(φ → ψ) ≡ (¬φ ∨ ψ)›
  by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
     (metis "&I" "∨I"(1, 2) "∨E"(3) "→I" MP "raa-cor:1")

AOT_theorem "oth-class-taut:2:a": ‹(φ & ψ) ≡ (ψ & φ)›
  by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
     (meson "&I" "&E" "→I")
lemmas "Commutativity of &" = "oth-class-taut:2:a"
AOT_theorem "oth-class-taut:2:b": ‹(φ & (ψ & χ)) ≡ ((φ & ψ) & χ)›
  by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
     (metis "&I" "&E" "→I")
lemmas "Associativity of &" = "oth-class-taut:2:b"
AOT_theorem "oth-class-taut:2:c": ‹(φ ∨ ψ) ≡ (ψ ∨ φ)›
  by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
     (metis "&I" "∨I"(1, 2) "∨E"(1) "→I")
lemmas "Commutativity of ∨" = "oth-class-taut:2:c"
AOT_theorem "oth-class-taut:2:d": ‹(φ ∨ (ψ ∨ χ)) ≡ ((φ ∨ ψ) ∨ χ)›
  by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"])
     (metis "&I" "∨I"(1, 2) "∨E"(1) "→I")
lemmas "Associativity of ∨" = "oth-class-taut:2:d"
AOT_theorem "oth-class-taut:2:e": ‹(φ ≡ ψ) ≡ (ψ ≡ φ)›
  by (rule "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"]; rule "&I";
      metis "&I" "df-rules-formulas[4]" "conventions:3" "&E"
            "Hypothetical Syllogism" "→I" "df-rules-formulas[3]")
lemmas "Commutativity of ≡" = "oth-class-taut:2:e"
AOT_theorem "oth-class-taut:2:f": ‹(φ ≡ (ψ ≡ χ)) ≡ ((φ ≡ ψ) ≡ χ)›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "conventions:3"[THEN "df-rules-formulas[3]"]
        "→I" "→E" "&E" "&I"
  by metis
lemmas "Associativity of ≡" = "oth-class-taut:2:f"

AOT_theorem "oth-class-taut:3:a": ‹φ ≡ φ›
  using "&I" "vdash-properties:6" "if-p-then-p"
        "df-rules-formulas[4]" "conventions:3" by blast
AOT_theorem "oth-class-taut:3:b": ‹φ ≡ ¬¬φ›
  using "&I" "useful-tautologies:1" "useful-tautologies:2" "→E"
        "df-rules-formulas[4]" "conventions:3" by blast
AOT_theorem "oth-class-taut:3:c": ‹¬(φ ≡ ¬φ)›
  by (metis "&E" "→E" RAA "df-rules-formulas[3]" "conventions:3")

AOT_theorem "oth-class-taut:4:a": ‹(φ → ψ) → ((ψ → χ) → (φ → χ))›
  by (metis "→E" "→I")
AOT_theorem "oth-class-taut:4:b": ‹(φ ≡ ψ) ≡ (¬φ ≡ ¬ψ)›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "conventions:3"[THEN "df-rules-formulas[3]"]
        "→I" "→E" "&E" "&I" RAA by metis
AOT_theorem "oth-class-taut:4:c": ‹(φ ≡ ψ) → ((φ → χ) ≡ (ψ → χ))›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "conventions:3"[THEN "df-rules-formulas[3]"]
        "→I" "→E" "&E" "&I" by metis
AOT_theorem "oth-class-taut:4:d": ‹(φ ≡ ψ) → ((χ → φ) ≡ (χ → ψ))›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "conventions:3"[THEN "df-rules-formulas[3]"]
        "→I" "→E" "&E" "&I" by metis
AOT_theorem "oth-class-taut:4:e": ‹(φ ≡ ψ) → ((φ & χ) ≡ (ψ & χ))›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "conventions:3"[THEN "df-rules-formulas[3]"]
        "→I" "→E" "&E" "&I" by metis
AOT_theorem "oth-class-taut:4:f": ‹(φ ≡ ψ) → ((χ & φ) ≡ (χ & ψ))›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "conventions:3"[THEN "df-rules-formulas[3]"]
        "→I" "→E" "&E" "&I" by metis
AOT_theorem "oth-class-taut:4:g": ‹(φ ≡ ψ) ≡ ((φ & ψ) ∨ (¬φ & ¬ψ))›
proof(safe intro!: "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"]
                   "&I" "→I"
           dest!: "conventions:3"[THEN "df-rules-formulas[3]", THEN "→E"])
  AOT_show ‹φ & ψ ∨ (¬φ & ¬ψ)› if ‹(φ → ψ) & (ψ → φ)›
    using "&E" "∨I" "→E" "&I" "raa-cor:1" "→I" "∨E" that by metis
next
  AOT_show ‹ψ› if ‹φ & ψ ∨ (¬φ & ¬ψ)› and ‹φ›
    using that "∨E" "&E" "raa-cor:3" by blast
next
  AOT_show ‹φ› if ‹φ & ψ ∨ (¬φ & ¬ψ)› and ‹ψ›
    using that "∨E" "&E" "raa-cor:3" by blast
qed
AOT_theorem "oth-class-taut:4:h": ‹¬(φ ≡ ψ) ≡ ((φ & ¬ψ) ∨ (¬φ & ψ))›
proof (safe intro!: "conventions:3"[THEN "df-rules-formulas[4]", THEN "→E"]
                    "&I" "→I")
  AOT_show ‹φ & ¬ψ ∨ (¬φ & ψ)› if ‹¬(φ ≡ ψ)›
    by (metis that "&I" "∨I"(1, 2) "→I" MT(1) "df-rules-formulas[4]"
              "raa-cor:3" "conventions:3")
next
  AOT_show ‹¬(φ ≡ ψ)› if ‹φ & ¬ψ ∨ (¬φ & ψ)›
    by (metis that "&E" "∨E"(2) "→E" "df-rules-formulas[3]"
              "raa-cor:3" "conventions:3")
qed
AOT_theorem "oth-class-taut:5:a": ‹(φ & ψ) ≡ ¬(¬φ ∨ ¬ψ)›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis
AOT_theorem "oth-class-taut:5:b": ‹(φ ∨ ψ) ≡ ¬(¬φ & ¬ψ)›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis
AOT_theorem "oth-class-taut:5:c": ‹¬(φ & ψ) ≡ (¬φ ∨ ¬ψ)›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis
AOT_theorem "oth-class-taut:5:d": ‹¬(φ ∨ ψ) ≡ (¬φ & ¬ψ)›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis

lemmas DeMorgan = "oth-class-taut:5:c" "oth-class-taut:5:d"

AOT_theorem "oth-class-taut:6:a":
  ‹(φ & (ψ ∨ χ)) ≡ ((φ & ψ) ∨ (φ & χ))›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis
AOT_theorem "oth-class-taut:6:b":
  ‹(φ ∨ (ψ & χ)) ≡ ((φ ∨ ψ) & (φ ∨ χ))›
  using "conventions:3"[THEN "df-rules-formulas[4]"]
        "→I" "→E" "&E" "&I" "∨I" "∨E" RAA by metis

AOT_theorem "oth-class-taut:7:a": ‹((φ & ψ) → χ) → (φ → (ψ → χ))›
  by (metis "&I" "→E" "→I")
lemmas Exportation = "oth-class-taut:7:a"
AOT_theorem "oth-class-taut:7:b": ‹(φ → (ψ →χ)) → ((φ & ψ) → χ)›
  by (metis "&E" "→E" "→I")
lemmas Importation = "oth-class-taut:7:b"

AOT_theorem "oth-class-taut:8:a":
  ‹(φ → (ψ → χ)) ≡ (ψ → (φ → χ))›
  using "conventions:3"[THEN "df-rules-formulas[4]"] "→I" "→E" "&E" "&I"
  by metis
lemmas Permutation = "oth-class-taut:8:a"
AOT_theorem "oth-class-taut:8:b":
  ‹(φ → ψ) → ((φ → χ) → (φ → (ψ & χ)))›
  by (metis "&I" "→E" "→I")
lemmas Composition = "oth-class-taut:8:b"
AOT_theorem "oth-class-taut:8:c":
  ‹(φ → χ) → ((ψ → χ) → ((φ ∨ ψ) → χ))›
  by (metis "∨E"(2) "→E" "→I" RAA(1))
AOT_theorem "oth-class-taut:8:d":
  ‹((φ → ψ) & (χ → Θ)) → ((φ & χ) → (ψ & Θ))›
  by (metis "&E" "&I" "→E" "→I")
lemmas "Double Composition" = "oth-class-taut:8:d"
AOT_theorem "oth-class-taut:8:e":
  ‹((φ & ψ) ≡ (φ & χ)) ≡ (φ → (ψ ≡ χ))›
  by (metis "conventions:3"[THEN "df-rules-formulas[4]"]
            "conventions:3"[THEN "df-rules-formulas[3]"]
            "→I" "→E" "&E" "&I")
AOT_theorem "oth-class-taut:8:f":
  ‹((φ & ψ) ≡ (χ & ψ)) ≡ (ψ → (φ ≡ χ))›
  by (metis "conventions:3"[THEN "df-rules-formulas[4]"]
            "conventions:3"[THEN "df-rules-formulas[3]"]
            "→I" "→E" "&E" "&I")
AOT_theorem "oth-class-taut:8:g":
  ‹(ψ ≡ χ) → ((φ ∨ ψ) ≡ (φ ∨ χ))›
  by (metis "conventions:3"[THEN "df-rules-formulas[4]"]
            "conventions:3"[THEN "df-rules-formulas[3]"]
            "→I" "→E" "&E" "&I" "∨I" "∨E"(1))
AOT_theorem "oth-class-taut:8:h":
  ‹(ψ ≡ χ) → ((ψ ∨ φ) ≡ (χ ∨ φ))›
  by (metis "conventions:3"[THEN "df-rules-formulas[4]"]
            "conventions:3"[THEN "df-rules-formulas[3]"]
            "→I" "→E" "&E" "&I" "∨I" "∨E"(1))
AOT_theorem "oth-class-taut:8:i":
  ‹(φ ≡ (ψ & χ)) → (ψ → (φ ≡ χ))›
  by (metis "conventions:3"[THEN "df-rules-formulas[4]"]
            "conventions:3"[THEN "df-rules-formulas[3]"]
            "→I" "→E" "&E" "&I")

AOT_theorem "intro-elim:1":
  assumes ‹φ ∨ ψ› and ‹φ ≡ χ› and ‹ψ ≡ Θ›
  shows ‹χ ∨ Θ›
  by (metis assms "∨I"(1, 2) "∨E"(1) "→I" "→E" "&E"(1)
            "conventions:3"[THEN "df-rules-formulas[3]"])

AOT_theorem "intro-elim:2":
  assumes ‹φ → ψ› and ‹ψ → φ›
  shows ‹φ ≡ ψ›
  by (meson "&I" "conventions:3" "df-rules-formulas[4]" MP assms)
lemmas "≡I" = "intro-elim:2"

AOT_theorem "intro-elim:3:a":
  assumes ‹φ ≡ ψ› and ‹φ›
  shows ‹ψ›
  by (metis "∨I"(1) "→I" "∨E"(1) "intro-elim:1" assms)
AOT_theorem "intro-elim:3:b":
  assumes ‹φ ≡ ψ› and ‹ψ›
  shows ‹φ›
  using "intro-elim:3:a" "Commutativity of ≡" assms by blast
AOT_theorem "intro-elim:3:c":
  assumes ‹φ ≡ ψ› and ‹¬φ›
  shows ‹¬ψ›
  using "intro-elim:3:b" "raa-cor:3" assms by blast
AOT_theorem "intro-elim:3:d":
  assumes ‹φ ≡ ψ› and ‹¬ψ›
  shows ‹¬φ›
  using "intro-elim:3:a" "raa-cor:3" assms by blast
AOT_theorem "intro-elim:3:e":
  assumes ‹φ ≡ ψ› and ‹ψ ≡ χ›
  shows ‹φ ≡ χ›
  by (metis "≡I" "→I" "intro-elim:3:a" "intro-elim:3:b" assms)
declare "intro-elim:3:e"[trans]
AOT_theorem "intro-elim:3:f":
  assumes ‹φ ≡ ψ› and ‹φ ≡ χ›
  shows ‹χ ≡ ψ›
  by (metis "≡I" "→I" "intro-elim:3:a" "intro-elim:3:b" assms)
lemmas "≡E" = "intro-elim:3:a" "intro-elim:3:b" "intro-elim:3:c"
              "intro-elim:3:d" "intro-elim:3:e" "intro-elim:3:f"

declare "Commutativity of ≡"[THEN "≡E"(1), sym]

AOT_theorem "rule-eq-df:1":
  assumes ‹φ ≡⇩_d⇩_f ψ›
  shows ‹φ ≡ ψ›
  by (simp add: "≡I" "df-rules-formulas[3]" "df-rules-formulas[4]" assms)
lemmas "≡Df" = "rule-eq-df:1"
AOT_theorem "rule-eq-df:2":
  assumes ‹φ ≡⇩_d⇩_f ψ› and ‹φ›
  shows ‹ψ›
  using "≡Df" "≡E"(1) assms by blast
lemmas "≡⇩_d⇩_fE" = "rule-eq-df:2"
AOT_theorem "rule-eq-df:3":
  assumes ‹φ ≡⇩_d⇩_f ψ› and ‹ψ›
  shows ‹φ›
  using "≡Df" "≡E"(2) assms by blast
lemmas "≡⇩_d⇩_fI" = "rule-eq-df:3"

AOT_theorem  "df-simplify:1":
  assumes ‹φ ≡ (ψ & χ)› and ‹ψ›
  shows ‹φ ≡ χ›
  by (metis "&E"(2) "&I" "≡E"(1, 2) "≡I" "→I" assms)
(* Note: this is a slight variation from PLM *)
AOT_theorem  "df-simplify:2":
  assumes ‹φ ≡ (ψ & χ)› and ‹χ›
  shows ‹φ ≡ ψ›
  by (metis "&E"(1) "&I" "≡E"(1, 2) "≡I" "→I" assms)
lemmas "≡S" = "df-simplify:1"  "df-simplify:2"

subsection‹The Theory of Quantification›
text‹\label{PLM: 9.6}›

AOT_theorem "rule-ui:1":
  assumes ‹∀α φ{α}› and ‹τ↓›
  shows ‹φ{τ}›
  using "→E" "cqt:1"[axiom_inst] assms by blast
AOT_theorem "rule-ui:2[const_var]":
  assumes ‹∀α φ{α}›
  shows ‹φ{β}›
  by (simp add: "rule-ui:1" "cqt:2[const_var]"[axiom_inst] assms)
AOT_theorem "rule-ui:2[lambda]":
  assumes ‹∀F φ{F}› and ‹INSTANCE_OF_CQT_2(ψ)›
  shows ‹φ{[λν⇩₁...ν⇩_n ψ{ν⇩₁...ν⇩_n}]}›
  by (simp add: "rule-ui:1" "cqt:2[lambda]"[axiom_inst] assms)
AOT_theorem "rule-ui:3":
  assumes ‹∀α φ{α}›
  shows ‹φ{α}›
  by (simp add: "rule-ui:2[const_var]" assms)
lemmas "∀E" = "rule-ui:1" "rule-ui:2[const_var]"
              "rule-ui:2[lambda]" "rule-ui:3"

AOT_theorem "cqt-orig:1[const_var]": ‹∀α φ{α} → φ{β}›
  by (simp add: "∀E"(2) "→I")
AOT_theorem "cqt-orig:1[lambda]":
  assumes ‹INSTANCE_OF_CQT_2(ψ)›
  shows ‹∀F φ{F} → φ{[λν⇩₁...ν⇩_n ψ{ν⇩₁...ν⇩_n}]}›
  by (simp add: "∀E"(3) "→I" assms)
AOT_theorem "cqt-orig:2": ‹∀α (φ → ψ{α}) → (φ → ∀α ψ{α})›
  by (metis "→I" GEN "vdash-properties:6" "∀E"(4))
AOT_theorem "cqt-orig:3": ‹∀α φ{α} → φ{α}›
  using "cqt-orig:1[const_var]".

AOT_theorem universal:
  assumes ‹for arbitrary β: φ{β}›
  shows ‹∀α φ{α}›
  using GEN assms .
lemmas "∀I" = universal

(* Generalized mechanism for ∀I followed by ∀E *)
ML‹
fun get_instantiated_allI ctxt varname thm = let
val trm = Thm.concl_of thm
val trm =
  case trm of (@{const Trueprop} $ (@{const AOT_model_valid_in} $ _ $ x)) => x
  | _ => raise Term.TERM ("Expected simple theorem.", [trm])
fun extractVars (Const (\<^const_name>‹AOT_term_of_var›, _) $ Var v) =
    (if fst (fst v) = fst varname then [Var v] else [])
  | extractVars (t1 $ t2) = extractVars t1 @ extractVars t2
  | extractVars (Abs (_, _, t)) = extractVars t
  | extractVars _ = []
val vars = extractVars trm
val vars = fold Term.add_vars vars []
val var = hd vars
val trmty =
  case (snd var) of (Type (\<^type_name>‹AOT_var›, [t])) => (t)
  | _ => raise Term.TYPE ("Expected variable type.", [snd var], [Var var])
val trm = Abs (Term.string_of_vname (fst var), trmty, Term.abstract_over (
      Const (\<^const_name>‹AOT_term_of_var›, Type ("fun", [snd var, trmty]))
       $ Var var, trm))
val trm = Thm.cterm_of (Context.proof_of ctxt) trm
val ty = hd (Term.add_tvars (Thm.prop_of @{thm "∀I"}) [])
val typ = Thm.ctyp_of (Context.proof_of ctxt) trmty
val allthm = Drule.instantiate_normalize (TVars.make [(ty, typ)], Vars.empty) @{thm "∀I"}
val phi = hd (Term.add_vars (Thm.prop_of allthm) [])
val allthm = Drule.instantiate_normalize (TVars.empty, Vars.make [(phi,trm)]) allthm
in
allthm
end
›

attribute_setup "∀I" =
  ‹Scan.lift (Scan.repeat1 Args.var) >> (fn args => Thm.rule_attribute []
  (fn ctxt => fn thm => fold (fn arg => fn thm =>
    thm RS get_instantiated_allI ctxt arg thm) args thm))›
  "Quantify over a variable in a theorem using GEN."

attribute_setup "unvarify" =
  ‹Scan.lift (Scan.repeat1 Args.var) >> (fn args => Thm.rule_attribute []
  (fn ctxt => fn thm =>
    let
      fun get_inst_allI arg thm = thm RS get_instantiated_allI ctxt arg thm
      val thm = fold get_inst_allI args thm
      val thm = fold (K (fn thm => thm RS @{thm "∀E"(1)})) args thm
    in
     thm
    end))›
  "Generalize a statement about variables to a statement about denoting terms."

(* Note: rereplace-lem does not apply to the embedding *)

AOT_theorem "cqt-basic:1": ‹∀α∀β φ{α,β} ≡ ∀β∀α φ{α,β}›
  by (metis "≡I" "∀E"(2) "∀I" "→I")

AOT_theorem "cqt-basic:2":
  ‹∀α(φ{α} ≡ ψ{α}) ≡ (∀α(φ{α} → ψ{α}) & ∀α(ψ{α} → φ{α}))›
proof (rule "≡I"; rule "→I")
  AOT_assume ‹∀α(φ{α} ≡ ψ{α})›
  AOT_hence ‹φ{α} ≡ ψ{α}› for α using "∀E"(2) by blast
  AOT_hence ‹φ{α} → ψ{α}› and ‹ψ{α} → φ{α}› for α
    using "≡E"(1,2) "→I" by blast+
  AOT_thus ‹∀α(φ{α} → ψ{α}) & ∀α(ψ{α} → φ{α})›
    by (auto intro: "&I" "∀I")
next
  AOT_assume ‹∀α(φ{α} → ψ{α}) & ∀α(ψ{α} → φ{α})›
  AOT_hence ‹φ{α} → ψ{α}› and ‹ψ{α} → φ{α}› for α
    using "∀E"(2) "&E" by blast+
  AOT_hence ‹φ{α} ≡ ψ{α}› for α
    using "≡I" by blast
  AOT_thus ‹∀α(φ{α} ≡ ψ{α})› by (auto intro: "∀I")
qed

AOT_theorem "cqt-basic:3": ‹∀α(φ{α} ≡ ψ{α}) → (∀α φ{α} ≡ ∀α ψ{α})›
proof(rule "→I")
  AOT_assume ‹∀α(φ{α} ≡ ψ{α})›
  AOT_hence 1: ‹φ{α} ≡ ψ{α}› for α using "∀E"(2) by blast
  {
    AOT_assume ‹∀α φ{α}›
    AOT_hence ‹∀α ψ{α}› using 1 "∀I" "∀E"(4) "≡E" by metis
  }
  moreover {
    AOT_assume ‹∀α ψ{α}›
    AOT_hence ‹∀α φ{α}› using 1 "∀I" "∀E"(4) "≡E" by metis
  }
  ultimately AOT_show ‹∀α φ{α} ≡ ∀α ψ{α}›
    using "≡I" "→I" by auto
qed

AOT_theorem "cqt-basic:4": ‹∀α(φ{α} & ψ{α}) → (∀α φ{α} & ∀α ψ{α})›
proof(rule "→I")
  AOT_assume 0: ‹∀α(φ{α} & ψ{α})›
  AOT_have ‹φ{α}› and ‹ψ{α}› for α using "∀E"(2) 0 "&E" by blast+
  AOT_thus ‹∀α φ{α} & ∀α ψ{α}›
    by (auto intro: "∀I" "&I")
qed

AOT_theorem "cqt-basic:5": ‹(∀α⇩₁...∀α⇩_n(φ{α⇩₁...α⇩_n})) → φ{α⇩₁...α⇩_n}›
  using "cqt-orig:3" by blast

AOT_theorem "cqt-basic:6": ‹∀α∀α φ{α} ≡ ∀α φ{α}›
  by (meson "≡I" "→I" GEN "cqt-orig:1[const_var]")

AOT_theorem "cqt-basic:7": ‹(φ → ∀α ψ{α}) ≡ ∀α(φ → ψ{α})›
  by (metis "→I" "vdash-properties:6" "rule-ui:3" "≡I" GEN)

AOT_theorem "cqt-basic:8": ‹(∀α φ{α} ∨ ∀α ψ{α}) → ∀α (φ{α} ∨ ψ{α})›
  by (simp add: "∨I"(3) "→I" GEN "cqt-orig:1[const_var]")

AOT_theorem "cqt-basic:9":
  ‹(∀α (φ{α} → ψ{α}) & ∀α (ψ{α} → χ{α})) → ∀α(φ{α} → χ{α})›
proof -
  {
    AOT_assume ‹∀α (φ{α} → ψ{α})›
    moreover AOT_assume ‹∀α (ψ{α} → χ{α})›
    ultimately AOT_have ‹φ{α} → ψ{α}› and ‹ψ{α} → χ{α}› for α
      using "∀E" by blast+
    AOT_hence ‹φ{α} → χ{α}› for α by (metis "→E" "→I")
    AOT_hence ‹∀α(φ{α} → χ{α})› using "∀I" by fast
  }
  thus ?thesis using "&I" "→I" "&E" by meson
qed

AOT_theorem "cqt-basic:10":
  ‹(∀α(φ{α} ≡ ψ{α}) & ∀α(ψ{α} ≡ χ{α})) → ∀α (φ{α} ≡ χ{α})›
proof(rule "→I"; rule "∀I")
  fix β
  AOT_assume ‹∀α(φ{α} ≡ ψ{α}) & ∀α(ψ{α} ≡ χ{α})›
  AOT_hence ‹φ{β} ≡ ψ{β}› and ‹ψ{β} ≡ χ{β}› using "&E" "∀E" by blast+
  AOT_thus ‹φ{β} ≡ χ{β}› using "≡I" "≡E" by blast
qed

AOT_theorem "cqt-basic:11": ‹∀α(φ{α} ≡ ψ{α}) ≡ ∀α (ψ{α} ≡ φ{α})›
proof (rule "≡I"; rule "→I")
  AOT_assume 0: ‹∀α(φ{α} ≡ ψ{α})›
  {
    fix α
    AOT_have ‹φ{α} ≡ ψ{α}› using 0 "∀E" by blast
    AOT_hence ‹ψ{α} ≡ φ{α}› using "≡I" "≡E" "→I" "→E" by metis
  }
  AOT_thus ‹∀α(ψ{α} ≡ φ{α})› using "∀I" by fast
next
  AOT_assume 0: ‹∀α(ψ{α} ≡ φ{α})›
  {
    fix α
    AOT_have ‹ψ{α} ≡ φ{α}› using 0 "∀E" by blast
    AOT_hence ‹φ{α} ≡ ψ{α}› using "≡I" "≡E" "→I" "→E" by metis
  }
  AOT_thus ‹∀α(φ{α} ≡ ψ{α})› using "∀I" by fast
qed

AOT_theorem "cqt-basic:12": ‹∀α φ{α} → ∀α (ψ{α} → φ{α})›
  by (simp add: "∀E"(2) "→I" GEN)

AOT_theorem "cqt-basic:13": ‹∀α φ{α} ≡ ∀β φ{β}›
  using "≡I" "→I" by blast

AOT_theorem "cqt-basic:14":
  ‹(∀α⇩₁...∀α⇩_n (φ{α⇩₁...α⇩_n} → ψ{α⇩₁...α⇩_n})) →
   ((∀α⇩₁...∀α⇩_n φ{α⇩₁...α⇩_n}) → (∀α⇩₁...∀α⇩_n ψ{α⇩₁...α⇩_n}))›
  using "cqt:3"[axiom_inst] by auto

AOT_theorem "cqt-basic:15":
  ‹(∀α⇩₁...∀α⇩_n (φ → ψ{α⇩₁...α⇩_n})) → (φ → (∀α⇩₁...∀α⇩_n ψ{α⇩₁...α⇩_n}))›
  using "cqt-orig:2" by auto

AOT_theorem "universal-cor":
  assumes ‹for arbitrary β: φ{β}›
  shows ‹∀α φ{α}›
  using GEN assms .

AOT_theorem "existential:1":
  assumes ‹φ{τ}› and ‹τ↓›
  shows ‹∃α φ{α}›
proof(rule "raa-cor:1")
  AOT_assume ‹¬∃α φ{α}›
  AOT_hence ‹∀α ¬φ{α}›
    using "≡⇩_d⇩_fI" "conventions:4" RAA "&I" by blast
  AOT_hence ‹¬φ{τ}› using assms(2) "∀E"(1) "→E" by blast
  AOT_thus ‹φ{τ} & ¬φ{τ}› using assms(1) "&I" by blast
qed

AOT_theorem "existential:2[const_var]":
  assumes ‹φ{β}›
  shows ‹∃α φ{α}›
  using "existential:1" "cqt:2[const_var]"[axiom_inst] assms by blast

AOT_theorem "existential:2[lambda]":
  assumes ‹φ{[λν⇩₁...ν⇩_n ψ{ν⇩₁...ν⇩_n}]}› and ‹INSTANCE_OF_CQT_2(ψ)›
  shows ‹∃α φ{α}›
  using "existential:1" "cqt:2[lambda]"[axiom_inst] assms by blast
lemmas "∃I" = "existential:1" "existential:2[const_var]"
              "existential:2[lambda]" 

AOT_theorem "instantiation":
  assumes ‹for arbitrary β: φ{β} ❙⊢ ψ› and ‹∃α φ{α}›
  shows ‹ψ›
  by (metis (no_types, lifting) "≡⇩_d⇩_fE" GEN "raa-cor:3" "conventions:4" assms)
lemmas "∃E" = "instantiation"

AOT_theorem "cqt-further:1": ‹∀α φ{α} → ∃α φ{α}›
  using "∀E"(4) "∃I"(2) "→I" by metis

AOT_theorem "cqt-further:2": ‹¬∀α φ{α} → ∃α ¬φ{α}›
  using "∀I" "∃I"(2) "→I" RAA by metis

AOT_theorem "cqt-further:3": ‹∀α φ{α} ≡ ¬∃α ¬φ{α}›
  using "∀E"(4) "∃E" "→I" RAA
  by (metis "cqt-further:2" "≡I" "modus-tollens:1")

AOT_theorem "cqt-further:4": ‹¬∃α φ{α} → ∀α ¬φ{α}›
  using "∀I" "∃I"(2)"→I" RAA by metis

AOT_theorem "cqt-further:5": ‹∃α (φ{α} & ψ{α}) → (∃α φ{α} & ∃α ψ{α})›
  by (metis (no_types, lifting) "&E" "&I" "∃E" "∃I"(2) "→I")

AOT_theorem "cqt-further:6": ‹∃α (φ{α} ∨ ψ{α}) → (∃α φ{α} ∨ ∃α ψ{α})›
  by (metis (mono_tags, lifting) "∃E" "∃I"(2) "∨E"(3) "∨I"(1, 2) "→I" RAA(2))

(* NOTE: vacuous in the embedding *)
AOT_theorem "cqt-further:7": ‹∃α φ{α} ≡ ∃β φ{β}›
  by (simp add: "oth-class-taut:3:a")

AOT_theorem "cqt-further:8":
  ‹(∀α φ{α} & ∀α ψ{α}) → ∀α (φ{α} ≡ ψ{α})›
  by (metis (mono_tags, lifting) "&E" "≡I" "∀E"(2) "→I" GEN)

AOT_theorem "cqt-further:9":
  ‹(¬∃α φ{α} & ¬∃α ψ{α}) → ∀α (φ{α} ≡ ψ{α})›
  by (metis (mono_tags, lifting) "&E" "≡I" "∃I"(2) "→I" GEN "raa-cor:4")

AOT_theorem "cqt-further:10":
  ‹(∃α φ{α} & ¬∃α ψ{α}) → ¬∀α (φ{α} ≡ ψ{α})›
proof(rule "→I"; rule "raa-cor:2")
  AOT_assume 0: ‹∃α φ{α} & ¬∃α ψ{α}›
  then AOT_obtain α where ‹φ{α}› using "∃E" "&E"(1) by metis
  moreover AOT_assume ‹∀α (φ{α} ≡ ψ{α})›
  ultimately AOT_have ‹ψ{α}› using "∀E"(4) "≡E"(1) by blast
  AOT_hence ‹∃α ψ{α}› using "∃I" by blast
  AOT_thus ‹∃α ψ{α} & ¬∃α ψ{α}› using 0 "&E"(2) "&I" by blast
qed

AOT_theorem "cqt-further:11": ‹∃α∃β φ{α,β} ≡ ∃β∃α φ{α,β}›
  using "≡I" "→I" "∃I"(2) "∃E" by metis

subsection‹Logical Existence, Identity, and Truth›
text‹\label{PLM: 9.7}›

AOT_theorem "log-prop-prop:1": ‹[λ φ]↓›
  using "cqt:2[lambda0]"[axiom_inst] by auto

AOT_theorem "log-prop-prop:2": ‹φ↓›
  by (rule "≡⇩_d⇩_fI"[OF "existence:3"]) "cqt:2[lambda]"

AOT_theorem "exist-nec": ‹τ↓ → □τ↓›
proof -
  AOT_have ‹∀β □β↓›
    by (simp add: GEN RN "cqt:2[const_var]"[axiom_inst])
  AOT_thus ‹τ↓ → □τ↓›
    using "cqt:1"[axiom_inst] "→E" by blast
qed

(* TODO: replace this mechanism by a "proof by types" command *)
class AOT_Term_id = AOT_Term +
  assumes "t=t-proper:1"[AOT]: ‹[v ⊨ τ = τ' → τ↓]›
      and "t=t-proper:2"[AOT]: ‹[v ⊨ τ = τ' → τ'↓]›

instance κ :: AOT_Term_id
proof
  AOT_modally_strict {
    AOT_show ‹κ = κ' → κ↓› for κ κ'
    proof(rule "→I")
      AOT_assume ‹κ = κ'›
      AOT_hence ‹O!κ ∨ A!κ›
        by (rule "∨I"(3)[OF "≡⇩_d⇩_fE"[OF "identity:1"]])
           (meson "→I" "∨I"(1) "&E"(1))+
      AOT_thus ‹κ↓›
        by (rule "∨E"(1))
           (metis "cqt:5:a"[axiom_inst] "→I" "→E" "&E"(2))+
    qed
  }
next
  AOT_modally_strict {
    AOT_show ‹κ = κ' → κ'↓› for κ κ'
    proof(rule "→I")
      AOT_assume ‹κ = κ'›
      AOT_hence ‹O!κ' ∨ A!κ'›
        by (rule "∨I"(3)[OF "≡⇩_d⇩_fE"[OF "identity:1"]])
           (meson "→I" "∨I" "&E")+
      AOT_thus ‹κ'↓›
        by (rule "∨E"(1))
           (metis "cqt:5:a"[axiom_inst] "→I" "→E" "&E"(2))+
    qed
  }
qed

instance rel :: (AOT_κs) AOT_Term_id
proof
  AOT_modally_strict {
    AOT_show ‹Π = Π' → Π↓› for Π Π' :: ‹<'a>›
    proof(rule "→I")
      AOT_assume ‹Π = Π'›
      AOT_thus ‹Π↓› using "≡⇩_d⇩_fE"[OF "identity:3"[of Π Π']] "&E" by blast
    qed
  }
next
  AOT_modally_strict {
    AOT_show ‹Π = Π' → Π'↓› for Π Π' :: ‹<'a>›
    proof(rule "→I")
      AOT_assume ‹Π = Π'›
      AOT_thus ‹Π'↓› using "≡⇩_d⇩_fE"[OF "identity:3"[of Π Π']] "&E" by blast
    qed
  }
qed

instance 𝗈 :: AOT_Term_id
proof
  AOT_modally_strict {
    fix φ ψ
    AOT_show ‹φ = ψ → φ↓›
    proof(rule "→I")
      AOT_assume ‹φ = ψ›
      AOT_thus ‹φ↓› using "≡⇩_d⇩_fE"[OF "identity:4"[of φ ψ]] "&E" by blast
    qed
  }
next
  AOT_modally_strict {
    fix φ ψ
    AOT_show ‹φ = ψ → ψ↓›
    proof(rule "→I")
      AOT_assume ‹φ = ψ›
      AOT_thus ‹ψ↓› using "≡⇩_d⇩_fE"[OF "identity:4"[of φ ψ]] "&E" by blast
    qed
  }
qed

instance prod :: (AOT_Term_id, AOT_Term_id) AOT_Term_id
proof
  AOT_modally_strict {
    fix τ τ' :: ‹'a×'b›
    AOT_show ‹τ = τ' → τ↓›
    proof (induct τ; induct τ'; rule "→I")
      fix τ⇩₁ τ⇩₁' :: 'a and τ⇩₂  τ⇩₂' :: 'b
      AOT_assume ‹«(τ⇩₁, τ⇩₂)» = «(τ⇩₁', τ⇩₂')»›
      AOT_hence ‹(τ⇩₁ = τ⇩₁') & (τ⇩₂ = τ⇩₂')› by (metis "≡⇩_d⇩_fE" tuple_identity_1)
      AOT_hence ‹τ⇩₁↓› and ‹τ⇩₂↓›
        using "t=t-proper:1" "&E" "vdash-properties:10" by blast+
      AOT_thus ‹«(τ⇩₁, τ⇩₂)»↓› by (metis "≡⇩_d⇩_fI" "&I" tuple_denotes)
    qed
  }
next
  AOT_modally_strict {
    fix τ τ' :: ‹'a×'b›
    AOT_show ‹τ = τ' → τ'↓›
    proof (induct τ; induct τ'; rule "→I")
      fix τ⇩₁ τ⇩₁' :: 'a and τ⇩₂  τ⇩₂' :: 'b
      AOT_assume ‹«(τ⇩₁, τ⇩₂)» = «(τ⇩₁', τ⇩₂')»›
      AOT_hence ‹(τ⇩₁ = τ⇩₁') & (τ⇩₂ = τ⇩₂')› by (metis "≡⇩_d⇩_fE" tuple_identity_1)
      AOT_hence ‹τ⇩₁'↓› and ‹τ⇩₂'↓›
        using "t=t-proper:2" "&E" "vdash-properties:10" by blast+
      AOT_thus ‹«(τ⇩₁', τ⇩₂')»↓› by (metis "≡⇩_d⇩_fI" "&I" tuple_denotes)
    qed
  }
qed

(* This is the end of the "proof by types" and
   makes the results available on new theorems *)
AOT_register_type_constraints
  Term: ‹_::AOT_Term_id› ‹_::AOT_Term_id›
AOT_register_type_constraints
  Individual: ‹κ› ‹_::{AOT_κs, AOT_Term_id}›
AOT_register_type_constraints
  Relation: ‹<_::{AOT_κs, AOT_Term_id}>›

AOT_theorem "id-rel-nec-equiv:1":
  ‹Π = Π' → □∀x⇩₁...∀x⇩_n ([Π]x⇩₁...x⇩_n ≡ [Π']x⇩₁...x⇩_n)›
proof(rule "→I")
  AOT_assume assumption: ‹Π = Π'›
  AOT_hence ‹Π↓› and ‹Π'↓›
    using "t=t-proper:1" "t=t-proper:2" MP by blast+
  moreover AOT_have ‹∀F∀G (F = G → ((□∀x⇩₁...∀x⇩_n ([F]x⇩₁...x⇩_n ≡ [F]x⇩₁...x⇩_n)) →
                                     □∀x⇩₁...∀x⇩_n ([F]x⇩₁...x⇩_n ≡ [G]x⇩₁...x⇩_n)))›
    apply (rule GEN)+ using "l-identity"[axiom_inst] by force
  ultimately AOT_have ‹Π = Π' → ((□∀x⇩₁...∀x⇩_n ([Π]x⇩₁...x⇩_n ≡ [Π]x⇩₁...x⇩_n)) →
                                   □∀x⇩₁...∀x⇩_n ([Π]x⇩₁...x⇩_n ≡ [Π']x⇩₁...x⇩_n))›
    using "∀E"(1) by blast
  AOT_hence ‹(□∀x⇩₁...∀x⇩_n ([Π]x⇩₁...x⇩_n ≡ [Π]x⇩₁...x⇩_n)) →
             □∀x⇩₁...∀x⇩_n ([Π]x⇩₁...x⇩_n ≡ [Π']x⇩₁...x⇩_n)›
    using assumption "→E" by blast
  moreover AOT_have ‹□∀x⇩₁...∀x⇩_n ([Π]x⇩₁...x⇩_n ≡ [Π]x⇩₁...x⇩_n)›
    by (simp add: RN "oth-class-taut:3:a" "universal-cor")
  ultimately AOT_show ‹□∀x⇩₁...∀x⇩_n ([Π]x⇩₁...x⇩_n ≡ [Π']x⇩₁...x⇩_n)›
    using "→E" by blast
qed

AOT_theorem "id-rel-nec-equiv:2": ‹φ = ψ → □(φ ≡ ψ)›
proof(rule "→I")
  AOT_assume assumption: ‹φ = ψ›
  AOT_hence ‹φ↓› and ‹ψ↓›
    using "t=t-proper:1" "t=t-proper:2" MP by blast+
  moreover AOT_have ‹∀p∀q (p = q → ((□(p ≡ p) → □(p ≡ q))))›
    apply (rule GEN)+ using "l-identity"[axiom_inst] by force
  ultimately AOT_have ‹φ = ψ → (□(φ ≡ φ) → □(φ ≡ ψ))›
    using "∀E"(1) by blast
  AOT_hence ‹□(φ ≡ φ) → □(φ ≡ ψ)›
    using assumption "→E" by blast
  moreover AOT_have ‹□(φ ≡ φ)›
    by (simp add: RN "oth-class-taut:3:a" "universal-cor")
  ultimately AOT_show ‹□(φ ≡ ψ)›
    using "→E" by blast
qed

AOT_theorem "rule=E":
  assumes ‹φ{τ}› and ‹τ = σ›
  shows ‹φ{σ}›
proof -
  AOT_have ‹τ↓› and ‹σ↓›
    using assms(2) "t=t-proper:1" "t=t-proper:2" "→E" by blast+
  moreover AOT_have ‹∀α∀β(α = β → (φ{α} → φ{β}))›
    apply (rule GEN)+ using "l-identity"[axiom_inst] by blast
  ultimately AOT_have ‹τ = σ → (φ{τ} → φ{σ})›
    using "∀E"(1) by blast
  AOT_thus ‹φ{σ}› using assms "→E" by blast
qed

AOT_theorem "propositions-lemma:1": ‹[λ φ] = φ›
proof -
  AOT_have ‹φ↓› by (simp add: "log-prop-prop:2")
  moreover AOT_have ‹∀p [λ p] = p›
    using "lambda-predicates:3[zero]"[axiom_inst] "∀I" by fast
  ultimately AOT_show ‹[λ φ] = φ›
    using "∀E" by blast
qed

AOT_theorem "propositions-lemma:2": ‹[λ φ] ≡ φ›
proof -
  AOT_have ‹[λ φ] ≡ [λ φ]› by (simp add: "oth-class-taut:3:a")
  AOT_thus ‹[λ φ] ≡ φ› using "propositions-lemma:1" "rule=E" by blast
qed

text‹propositions-lemma:3 through propositions-lemma:5 hold implicitly›

AOT_theorem "propositions-lemma:6": ‹(φ ≡ ψ) ≡ ([λ φ] ≡ [λ ψ])›
  by (metis "≡E"(1) "≡E"(5) "Associativity of ≡" "propositions-lemma:2")

text‹dr-alphabetic-rules holds implicitly›

AOT_theorem "oa-exist:1": ‹O!↓›
proof -
  AOT_have ‹[λx ◇[E!]x]↓› by "cqt:2[lambda]"
  AOT_hence 1: ‹O! = [λx ◇[E!]x]›
    using "df-rules-terms[4]"[OF "oa:1", THEN "&E"(1)] "→E" by blast
  AOT_show ‹O!↓› using "t=t-proper:1"[THEN "→E", OF 1] by simp
qed

AOT_theorem "oa-exist:2": ‹A!↓›
proof -
  AOT_have ‹[λx ¬◇[E!]x]↓› by "cqt:2[lambda]"
  AOT_hence 1: ‹A! = [λx ¬◇[E!]x]›
    using "df-rules-terms[4]"[OF "oa:2", THEN "&E"(1)] "→E" by blast
  AOT_show ‹A!↓› using "t=t-proper:1"[THEN "→E", OF 1] by simp
qed

AOT_theorem "oa-exist:3": ‹O!x ∨ A!x›
proof(rule "raa-cor:1")
  AOT_assume ‹¬(O!x ∨ A!x)›
  AOT_hence A: ‹¬O!x› and B: ‹¬A!x›
    using "Disjunction Addition"(1) "modus-tollens:1"
          "∨I"(2) "raa-cor:5" by blast+
  AOT_have C: ‹O! = [λx ◇[E!]x]›
    by (rule "df-rules-terms[4]"[OF "oa:1", THEN "&E"(1), THEN "→E"]) "cqt:2"
  AOT_have D: ‹A! = [λx ¬◇[E!]x]›
    by (rule "df-rules-terms[4]"[OF "oa:2", THEN "&E"(1), THEN "→E"]) "cqt:2"
  AOT_have E: ‹¬[λx ◇[E!]x]x›
    using A C "rule=E" by fast
  AOT_have F: ‹¬[λx ¬◇[E!]x]x›
    using B D "rule=E" by fast
  AOT_have G: ‹[λx ◇[E!]x]x ≡ ◇[E!]x›
    by (rule "lambda-predicates:2"[axiom_inst, THEN "→E"]) "cqt:2"
  AOT_have H: ‹[λx ¬◇[E!]x]x ≡ ¬◇[E!]x›
    by (rule "lambda-predicates:2"[axiom_inst, THEN "→E"]) "cqt:2"
  AOT_show ‹¬◇[E!]x & ¬¬◇[E!]x› using G E "≡E" H F "≡E" "&I" by metis
qed

AOT_theorem "p-identity-thm2:1": ‹F = G ≡ □∀x(x[F] ≡ x[G])›
proof -
  AOT_have ‹F = G ≡ F↓ & G↓ & □∀x(x[F] ≡ x[G])›
    using "identity:2" "df-rules-formulas[3]" "df-rules-formulas[4]"
          "→E" "&E" "≡I" "→I" by blast
  moreover AOT_have ‹F↓› and ‹G↓›
    by (auto simp: "cqt:2[const_var]"[axiom_inst])
  ultimately AOT_show ‹F = G ≡ □∀x(x[F] ≡ x[G])›
    using "≡S"(1) "&I" by blast
qed

AOT_theorem "p-identity-thm2:2[2]":
  ‹F = G ≡ ∀y⇩₁([λx [F]xy⇩₁] = [λx [G]xy⇩₁] & [λx [F]y⇩₁x] = [λx [G]y⇩₁x])›
proof -
  AOT_have ‹F = G ≡ F↓ & G↓ &
              ∀y⇩₁([λx [F]xy⇩₁] = [λx [G]xy⇩₁] & [λx [F]y⇩₁x] = [λx [G]y⇩₁x])›
    using "identity:3[2]" "df-rules-formulas[3]" "df-rules-formulas[4]"
          "→E" "&E" "≡I" "→I" by blast
  moreover AOT_have ‹F↓› and ‹G↓›
    by (auto simp: "cqt:2[const_var]"[axiom_inst])
  ultimately show ?thesis
    using "≡S"(1) "&I" by blast
qed
    
AOT_theorem "p-identity-thm2:2[3]":
  ‹F = G ≡ ∀y⇩₁∀y⇩₂([λx [F]xy⇩₁y⇩₂] = [λx [G]xy⇩₁y⇩₂] &
                  [λx [F]y⇩₁xy⇩₂] = [λx [G]y⇩₁xy⇩₂] &
                  [λx [F]y⇩₁y⇩₂x] = [λx [G]y⇩₁y⇩₂x])›
proof -
  AOT_have ‹F = G ≡ F↓ & G↓ & ∀y⇩₁∀y⇩₂([λx [F]xy⇩₁y⇩₂] = [λx [G]xy⇩₁y⇩₂] &
                                     [λx [F]y⇩₁xy⇩₂] = [λx [G]y⇩₁xy⇩₂] &
                                     [λx [F]y⇩₁y⇩₂x] = [λx [G]y⇩₁y⇩₂x])›
    using "identity:3[3]" "df-rules-formulas[3]" "df-rules-formulas[4]"
          "→E" "&E" "≡I" "→I" by blast
  moreover AOT_have ‹F↓› and ‹G↓›
    by (auto simp: "cqt:2[const_var]"[axiom_inst])
  ultimately show ?thesis
    using "≡S"(1) "&I" by blast
qed

AOT_theorem "p-identity-thm2:2[4]":
  ‹F = G ≡ ∀y⇩₁∀y⇩₂∀y⇩₃([λx [F]xy⇩₁y⇩₂y⇩₃] = [λx [G]xy⇩₁y⇩₂y⇩₃] &
                     [λx [F]y⇩₁xy⇩₂y⇩₃] = [λx [G]y⇩₁xy⇩₂y⇩₃] &
                     [λx [F]y⇩₁y⇩₂xy⇩₃] = [λx [G]y⇩₁y⇩₂xy⇩₃] &
                     [λx [F]y⇩₁y⇩₂y⇩₃x] = [λx [G]y⇩₁y⇩₂y⇩₃x])›
proof -
  AOT_have ‹F = G ≡ F↓ & G↓ & ∀y⇩₁∀y⇩₂∀y⇩₃([λx [F]xy⇩₁y⇩₂y⇩₃] = [λx [G]xy⇩₁y⇩₂y⇩₃] &
                                        [λx [F]y⇩₁xy⇩₂y⇩₃] = [λx [G]y⇩₁xy⇩₂y⇩₃] &
                                        [λx [F]y⇩₁y⇩₂xy⇩₃] = [λx [G]y⇩₁y⇩₂xy⇩₃] &
                                        [λx [F]y⇩₁y⇩₂y⇩₃x] = [λx [G]y⇩₁y⇩₂y⇩₃x])›
    using "identity:3[4]" "df-rules-formulas[3]" "df-rules-formulas[4]"
          "→E" "&E" "≡I" "→I" by blast
  moreover AOT_have ‹F↓› and ‹G↓›
    by (auto simp: "cqt:2[const_var]"[axiom_inst])
  ultimately show ?thesis
    using "≡S"(1) "&I" by blast
qed

AOT_theorem "p-identity-thm2:2":
  ‹F = G ≡ ∀x⇩₁...∀x⇩_n «AOT_sem_proj_id x⇩₁x⇩_n (λ τ . «[F]τ») (λ τ . «[G]τ»)»›
proof -
  AOT_have ‹F = G ≡ F↓ & G↓ &
              ∀x⇩₁...∀x⇩_n «AOT_sem_proj_id x⇩₁x⇩_n (λ τ . «[F]τ») (λ τ . «[G]τ»)»›
    using "identity:3" "df-rules-formulas[3]" "df-rules-formulas[4]"
          "→E" "&E" "≡I" "→I" by blast
  moreover AOT_have ‹F↓› and ‹G↓›
    by (auto simp: "cqt:2[const_var]"[axiom_inst])
  ultimately show ?thesis
    using "≡S"(1) "&I" by blast
qed

AOT_theorem "p-identity-thm2:3":
  ‹p = q ≡ [λx p] = [λx q]›
proof -
  AOT_have ‹p = q ≡ p↓ & q↓ & [λx p] = [λx q]›
    using "identity:4" "df-rules-formulas[3]" "df-rules-formulas[4]"
          "→E" "&E" "≡I" "→I" by blast
  moreover AOT_have ‹p↓› and ‹q↓›
    by (auto simp: "cqt:2[const_var]"[axiom_inst])
  ultimately show ?thesis
    using "≡S"(1) "&I" by blast
qed

class AOT_Term_id_2 = AOT_Term_id + assumes "id-eq:1": ‹[v ⊨ α = α]›

instance κ :: AOT_Term_id_2
proof
  AOT_modally_strict {
    fix x
    {
      AOT_assume ‹O!x›
      moreover AOT_have ‹□∀F([F]x ≡ [F]x)›
        using RN GEN "oth-class-taut:3:a" by fast
      ultimately AOT_have ‹O!x & O!x & □∀F([F]x ≡ [F]x)› using "&I" by simp
    }
    moreover {
      AOT_assume ‹A!x›
      moreover AOT_have ‹□∀F(x[F] ≡ x[F])›
        using RN GEN "oth-class-taut:3:a" by fast
      ultimately AOT_have ‹A!x & A!x & □∀F(x[F] ≡ x[F])› using "&I" by simp
    }
    ultimately AOT_have ‹(O!x & O!x & □∀F([F]x ≡ [F]x)) ∨
                         (A!x & A!x & □∀F(x[F] ≡ x[F]))›
      using "oa-exist:3" "∨I"(1) "∨I"(2) "∨E"(3) "raa-cor:1" by blast
    AOT_thus ‹x = x›
      using "identity:1"[THEN "df-rules-formulas[4]"] "→E" by blast
  }
qed

instance rel :: ("{AOT_κs,AOT_Term_id_2}") AOT_Term_id_2
proof
  AOT_modally_strict {
    fix F :: "<'a> AOT_var"
    AOT_have 0: ‹[λx⇩₁...x⇩_n [F]x⇩₁...x⇩_n] = F›
      by (simp add: "lambda-predicates:3"[axiom_inst])
    AOT_have ‹[λx⇩₁...x⇩_n [F]x⇩₁...x⇩_n]↓›
      by "cqt:2[lambda]"
    AOT_hence ‹[λx⇩₁...x⇩_n [F]x⇩₁...x⇩_n] = [λx⇩₁...x⇩_n [F]x⇩₁...x⇩_n]›
      using "lambda-predicates:1"[axiom_inst] "→E" by blast
    AOT_show ‹F = F› using "rule=E" 0 by force 
  }
qed

instance 𝗈 :: AOT_Term_id_2
proof
  AOT_modally_strict {
    fix p
    AOT_have 0: ‹[λ p] = p›
      by (simp add: "lambda-predicates:3[zero]"[axiom_inst])
    AOT_have ‹[λ p]↓›
      by (rule "cqt:2[lambda0]"[axiom_inst])
    AOT_hence ‹[λ p] = [λ p]›
      using "lambda-predicates:1[zero]"[axiom_inst] "→E" by blast
    AOT_show ‹p = p› using "rule=E" 0 by force
  }
qed

instance prod :: (AOT_Term_id_2, AOT_Term_id_2) AOT_Term_id_2
proof
  AOT_modally_strict {
    fix α :: ‹('a×'b) AOT_var›
    AOT_show ‹α = α›
    proof (induct)
      AOT_show ‹τ = τ› if ‹τ↓› for τ :: ‹'a×'b›
        using that
      proof (induct τ)
        fix τ⇩₁ :: 'a and τ⇩₂ :: 'b
        AOT_assume ‹«(τ⇩₁,τ⇩₂)»↓›
        AOT_hence ‹τ⇩₁↓› and ‹τ⇩₂↓›
          using "≡⇩_d⇩_fE" "&E" tuple_denotes by blast+
        AOT_hence ‹τ⇩₁ = τ⇩₁› and ‹τ⇩₂ = τ⇩₂›
          using "id-eq:1"[unvarify α] by blast+
        AOT_thus ‹«(τ⇩₁, τ⇩₂)» = «(τ⇩₁, τ⇩₂)»›
          by (metis "≡⇩_d⇩_fI" "&I" tuple_identity_1)
      qed
    qed
  }
qed

AOT_register_type_constraints
  Term: ‹_::AOT_Term_id_2› ‹_::AOT_Term_id_2›
AOT_register_type_constraints
  Individual: ‹κ› ‹_::{AOT_κs, AOT_Term_id_2}›
AOT_register_type_constraints
  Relation: ‹<_::{AOT_κs, AOT_Term_id_2}>›

AOT_theorem "id-eq:2": ‹α = β → β = α›
  by (meson "rule=E" "deduction-theorem")

AOT_theorem "id-eq:3": ‹α = β & β = γ → α = γ›
  using "rule=E" "→I" "&E" by blast

AOT_theorem "id-eq:4": ‹α = β ≡ ∀γ (α = γ ≡ β = γ)›
proof (rule "≡I"; rule "→I")
  AOT_assume 0: ‹α = β›
  AOT_hence 1: ‹β = α› using "id-eq:2" "→E" by blast
  AOT_show ‹∀γ (α = γ ≡ β = γ)›
    by (rule GEN) (metis "≡I" "→I" 0 "1" "rule=E")
next
  AOT_assume ‹∀γ (α = γ ≡ β = γ)›
  AOT_hence ‹α = α ≡ β = α› using "∀E"(2) by blast
  AOT_hence ‹α = α → β = α› using "≡E"(1) "→I" by blast
  AOT_hence ‹β = α› using "id-eq:1" "→E" by blast
  AOT_thus ‹α = β› using "id-eq:2" "→E" by blast
qed

AOT_theorem "rule=I:1":
  assumes ‹τ↓›
  shows ‹τ = τ›
proof -
  AOT_have ‹∀α (α = α)›
    by (rule GEN) (metis "id-eq:1")
  AOT_thus ‹τ = τ› using assms "∀E" by blast
qed

AOT_theorem "rule=I:2[const_var]": "α = α"
  using "id-eq:1".

AOT_theorem "rule=I:2[lambda]":
  assumes ‹INSTANCE_OF_CQT_2(φ)›
  shows "[λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}] = [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}]"
proof -
  AOT_have ‹∀α (α = α)›
    by (rule GEN) (metis "id-eq:1")
  moreover AOT_have ‹[λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}]↓›
    using assms by (rule "cqt:2[lambda]"[axiom_inst])
  ultimately AOT_show ‹[λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}] = [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}]›
    using assms "∀E" by blast
qed

lemmas "=I" = "rule=I:1" "rule=I:2[const_var]" "rule=I:2[lambda]"

AOT_theorem "rule-id-df:1":
  assumes ‹τ{α⇩₁...α⇩_n} =⇩_d⇩_f σ{α⇩₁...α⇩_n}› and ‹σ{τ⇩₁...τ⇩_n}↓›
  shows ‹τ{τ⇩₁...τ⇩_n} = σ{τ⇩₁...τ⇩_n}›
proof -
  AOT_have ‹σ{τ⇩₁...τ⇩_n}↓ → τ{τ⇩₁...τ⇩_n} = σ{τ⇩₁...τ⇩_n}›
    using "df-rules-terms[3]" assms(1) "&E" by blast
  AOT_thus ‹τ{τ⇩₁...τ⇩_n} = σ{τ⇩₁...τ⇩_n}›
    using assms(2) "→E" by blast
qed

AOT_theorem "rule-id-df:1[zero]":
  assumes ‹τ =⇩_d⇩_f σ› and ‹σ↓›
  shows ‹τ = σ›
proof -
  AOT_have ‹σ↓ → τ = σ›
    using "df-rules-terms[4]" assms(1) "&E" by blast
  AOT_thus ‹τ = σ›
    using assms(2) "→E" by blast
qed

AOT_theorem "rule-id-df:2:a":
  assumes ‹τ{α⇩₁...α⇩_n} =⇩_d⇩_f σ{α⇩₁...α⇩_n}› and ‹σ{τ⇩₁...τ⇩_n}↓› and ‹φ{τ{τ⇩₁...τ⇩_n}}›
  shows ‹φ{σ{τ⇩₁...τ⇩_n}}›
proof -
  AOT_have ‹τ{τ⇩₁...τ⇩_n} = σ{τ⇩₁...τ⇩_n}› using "rule-id-df:1" assms(1,2) by blast
  AOT_thus ‹φ{σ{τ⇩₁...τ⇩_n}}› using assms(3) "rule=E" by blast
qed

AOT_theorem "rule-id-df:2:a[2]":
  assumes ‹τ{«(α⇩₁,α⇩₂)»} =⇩_d⇩_f σ{«(α⇩₁,α⇩₂)»}›
    and ‹σ{«(τ⇩₁,τ⇩₂)»}↓›
      and ‹φ{τ{«(τ⇩₁,τ⇩₂)»}}›
  shows ‹φ{σ{«(τ⇩₁::'a::AOT_Term_id_2,τ⇩₂::'b::AOT_Term_id_2)»}}›
proof -
  AOT_have ‹τ{«(τ⇩₁,τ⇩₂)»} = σ{«(τ⇩₁,τ⇩₂)»}›
    using "rule-id-df:1" assms(1,2) by auto
  AOT_thus ‹φ{σ{«(τ⇩₁,τ⇩₂)»}}› using assms(3) "rule=E" by blast
qed

AOT_theorem "rule-id-df:2:a[zero]":
  assumes ‹τ =⇩_d⇩_f σ› and ‹σ↓› and ‹φ{τ}›
  shows ‹φ{σ}›
proof -
  AOT_have ‹τ = σ› using "rule-id-df:1[zero]" assms(1,2) by blast
  AOT_thus ‹φ{σ}› using assms(3) "rule=E" by blast
qed

lemmas "=⇩_d⇩_fE" = "rule-id-df:2:a" "rule-id-df:2:a[zero]"

AOT_theorem "rule-id-df:2:b":
  assumes ‹τ{α⇩₁...α⇩_n} =⇩_d⇩_f σ{α⇩₁...α⇩_n}› and ‹σ{τ⇩₁...τ⇩_n}↓› and ‹φ{σ{τ⇩₁...τ⇩_n}}›
  shows ‹φ{τ{τ⇩₁...τ⇩_n}}›
proof -
  AOT_have ‹τ{τ⇩₁...τ⇩_n} = σ{τ⇩₁...τ⇩_n}›
    using "rule-id-df:1" assms(1,2) by blast
  AOT_hence ‹σ{τ⇩₁...τ⇩_n} = τ{τ⇩₁...τ⇩_n}›
    using "rule=E" "=I"(1) "t=t-proper:1" "→E" by fast
  AOT_thus ‹φ{τ{τ⇩₁...τ⇩_n}}› using assms(3) "rule=E" by blast
qed

AOT_theorem "rule-id-df:2:b[2]":
  assumes ‹τ{«(α⇩₁,α⇩₂)»} =⇩_d⇩_f σ{«(α⇩₁,α⇩₂)»}›
      and ‹σ{«(τ⇩₁,τ⇩₂)»}↓›
      and ‹φ{σ{«(τ⇩₁,τ⇩₂)»}}›
  shows ‹φ{τ{«(τ⇩₁::'a::AOT_Term_id_2,τ⇩₂::'b::AOT_Term_id_2)»}}›
proof -
  AOT_have ‹τ{«(τ⇩₁,τ⇩₂)»} = σ{«(τ⇩₁,τ⇩₂)»}›
    using "=I"(1) "rule-id-df:2:a[2]" RAA(1) assms(1,2) "→I" by metis
  AOT_hence ‹σ{«(τ⇩₁,τ⇩₂)»} = τ{«(τ⇩₁,τ⇩₂)»}›
    using "rule=E" "=I"(1) "t=t-proper:1" "→E" by fast
  AOT_thus ‹φ{τ{«(τ⇩₁,τ⇩₂)»}}› using assms(3) "rule=E" by blast
qed

AOT_theorem "rule-id-df:2:b[zero]":
  assumes ‹τ =⇩_d⇩_f σ› and ‹σ↓› and ‹φ{σ}›
  shows ‹φ{τ}›
proof -
  AOT_have ‹τ = σ› using "rule-id-df:1[zero]" assms(1,2) by blast
  AOT_hence ‹σ = τ›
    using "rule=E" "=I"(1) "t=t-proper:1" "→E" by fast
  AOT_thus ‹φ{τ}› using assms(3) "rule=E" by blast
qed

lemmas "=⇩_d⇩_fI" = "rule-id-df:2:b" "rule-id-df:2:b[zero]"

AOT_theorem "free-thms:1": ‹τ↓ ≡ ∃β (β = τ)›
  by (metis "∃E" "rule=I:1" "t=t-proper:2" "→I" "∃I"(1) "≡I" "→E")

AOT_theorem "free-thms:2": ‹∀α φ{α} → (∃β (β = τ) → φ{τ})›
  by (metis "∃E" "rule=E" "cqt:2[const_var]"[axiom_inst] "→I" "∀E"(1))

AOT_theorem "free-thms:3[const_var]": ‹∃β (β = α)›
  by (meson "∃I"(2) "id-eq:1")

AOT_theorem "free-thms:3[lambda]":
  assumes ‹INSTANCE_OF_CQT_2(φ)›
  shows ‹∃β (β = [λν⇩₁...ν⇩_n φ{ν⇩₁...ν⇩_n}])›
  by (meson "=I"(3) assms "cqt:2[lambda]"[axiom_inst] "existential:1")

AOT_theorem "free-thms:4[rel]":
  ‹([Π]κ⇩₁...κ⇩_n ∨ κ⇩₁...κ⇩_n[Π]) → ∃β (β = Π)›
  by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a"[axiom_inst]
            "cqt:5:b"[axiom_inst] "→I" "∃I"(1))

AOT_theorem "free-thms:4[vars]":
  ‹([Π]κ⇩₁...κ⇩_n ∨ κ⇩₁...κ⇩_n[Π]) → ∃β⇩₁...∃β⇩_n (β⇩₁...β⇩_n = κ⇩₁...κ⇩_n)›
  by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a"[axiom_inst]
            "cqt:5:b"[axiom_inst] "→I" "∃I"(1))

AOT_theorem "free-thms:4[1,rel]":
  ‹([Π]κ ∨ κ[Π]) → ∃β (β = Π)›
  by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a"[axiom_inst]
            "cqt:5:b"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[1,1]":
  ‹([Π]κ ∨ κ[Π]) → ∃β (β = κ)›
  by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a"[axiom_inst]
            "cqt:5:b"[axiom_inst] "→I" "∃I"(1))

AOT_theorem "free-thms:4[2,rel]":
  ‹([Π]κ⇩₁κ⇩₂ ∨ κ⇩₁κ⇩₂[Π]) → ∃β (β = Π)›
  by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a[2]"[axiom_inst]
            "cqt:5:b[2]"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[2,1]":
  ‹([Π]κ⇩₁κ⇩₂ ∨ κ⇩₁κ⇩₂[Π]) → ∃β (β = κ⇩₁)›
  by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[2]"[axiom_inst]
            "cqt:5:b[2]"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[2,2]":
  ‹([Π]κ⇩₁κ⇩₂ ∨ κ⇩₁κ⇩₂[Π]) → ∃β (β = κ⇩₂)›
  by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a[2]"[axiom_inst]
            "cqt:5:b[2]"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[3,rel]":
  ‹([Π]κ⇩₁κ⇩₂κ⇩₃ ∨ κ⇩₁κ⇩₂κ⇩₃[Π]) → ∃β (β = Π)›
  by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a[3]"[axiom_inst]
            "cqt:5:b[3]"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[3,1]":
  ‹([Π]κ⇩₁κ⇩₂κ⇩₃ ∨ κ⇩₁κ⇩₂κ⇩₃[Π]) → ∃β (β = κ⇩₁)›
  by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[3]"[axiom_inst]
            "cqt:5:b[3]"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[3,2]":
  ‹([Π]κ⇩₁κ⇩₂κ⇩₃ ∨ κ⇩₁κ⇩₂κ⇩₃[Π]) → ∃β (β = κ⇩₂)›
  by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[3]"[axiom_inst]
            "cqt:5:b[3]"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[3,3]":
  ‹([Π]κ⇩₁κ⇩₂κ⇩₃ ∨ κ⇩₁κ⇩₂κ⇩₃[Π]) → ∃β (β = κ⇩₃)›
  by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a[3]"[axiom_inst]
            "cqt:5:b[3]"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[4,rel]":
  ‹([Π]κ⇩₁κ⇩₂κ⇩₃κ⇩₄ ∨ κ⇩₁κ⇩₂κ⇩₃κ⇩₄[Π]) → ∃β (β = Π)›
  by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a[4]"[axiom_inst]
            "cqt:5:b[4]"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[4,1]":
  ‹([Π]κ⇩₁κ⇩₂κ⇩₃κ⇩₄ ∨ κ⇩₁κ⇩₂κ⇩₃κ⇩₄[Π]) → ∃β (β = κ⇩₁)›
  by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[4]"[axiom_inst]
            "cqt:5:b[4]"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[4,2]":
  ‹([Π]κ⇩₁κ⇩₂κ⇩₃κ⇩₄ ∨ κ⇩₁κ⇩₂κ⇩₃κ⇩₄[Π]) → ∃β (β = κ⇩₂)›
  by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[4]"[axiom_inst]
            "cqt:5:b[4]"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[4,3]":
  ‹([Π]κ⇩₁κ⇩₂κ⇩₃κ⇩₄ ∨ κ⇩₁κ⇩₂κ⇩₃κ⇩₄[Π]) → ∃β (β = κ⇩₃)›
  by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[4]"[axiom_inst]
            "cqt:5:b[4]"[axiom_inst] "→I" "∃I"(1))
AOT_theorem "free-thms:4[4,4]":
  ‹([Π]κ⇩₁κ⇩₂κ⇩₃κ⇩₄ ∨ κ⇩₁κ⇩₂κ⇩₃κ⇩₄[Π]) → ∃β (β = κ⇩₄)›
  by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a[4]"[axiom_inst]
            "cqt:5:b[4]"[axiom_inst] "→I" "∃I"(1))

AOT_theorem "ex:1:a": ‹∀α α↓›
  by (rule GEN) (fact "cqt:2[const_var]"[axiom_inst])
AOT_theorem "ex:1:b": ‹∀α∃β(β = α)›
  by (rule GEN) (fact "free-thms:3[const_var]")

AOT_theorem "ex:2:a": ‹□α↓›
  by (rule RN) (fact "cqt:2[const_var]"[axiom_inst])
AOT_theorem "ex:2:b": ‹□∃β(β = α)›
  by (rule RN) (fact "free-thms:3[const_var]")

AOT_theorem "ex:3:a": ‹□∀α α↓›
  by (rule RN) (fact "ex:1:a")
AOT_theorem "ex:3:b": ‹□∀α∃β(β = α)›
  by (rule RN) (fact "ex:1:b")

AOT_theorem "ex:4:a": ‹∀α □α↓›
  by (rule GEN; rule RN) (fact "cqt:2[const_var]"[axiom_inst])
AOT_theorem "ex:4:b": ‹∀α□∃β(β = α)›
  by (rule GEN; rule RN) (fact "free-thms:3[const_var]")

AOT_theorem "ex:5:a": ‹□∀α □α↓›
  by (rule RN) (simp add: "ex:4:a")
AOT_theorem "ex:5:b": ‹□∀α□∃β(β = α)›
  by (rule RN) (simp add: "ex:4:b")

AOT_theorem "all-self=:1": ‹□∀α(α = α)›
  by (rule RN; rule GEN) (fact "id-eq:1")
AOT_theorem "all-self=:2": ‹∀α□(α = α)›
  by (rule GEN; rule RN) (fact "id-eq:1")

AOT_theorem "id-nec:1": ‹α = β → □(α = β)›
proof(rule "→I")
  AOT_assume ‹α = β›
  moreover AOT_have ‹□(α = α)›
    by (rule RN) (fact "id-eq:1")
  ultimately AOT_show ‹□(α = β)› using "rule=E" by fast
qed

AOT_theorem "id-nec:2": ‹τ = σ → □(τ = σ)›
proof(rule "→I")
  AOT_assume asm: ‹τ = σ›
  moreover AOT_have ‹τ↓›
    using calculation "t=t-proper:1" "→E" by blast
  moreover AOT_have ‹□(τ = τ)›
    using calculation "all-self=:2" "∀E"(1) by blast
  ultimately AOT_show ‹□(τ = σ)› using "rule=E" by fast
qed

AOT_theorem "term-out:1": ‹φ{α} ≡ ∃β (β = α & φ{β})›
proof (rule "≡I"; rule "→I")
  AOT_assume asm: ‹φ{α}›
  AOT_show ‹∃β (β = α & φ{β})›
    by (rule "∃I"(2)[where β=α]; rule "&I")
       (auto simp: "id-eq:1" asm)
next
  AOT_assume 0: ‹∃β (β = α & φ{β})›
  AOT_obtain β where ‹β = α & φ{β}›
    using "∃E"[rotated, OF 0] by blast
  AOT_thus ‹φ{α}› using "&E" "rule=E" by blast
qed

AOT_theorem "term-out:2": ‹τ↓ → (φ{τ} ≡ ∃α(α = τ & φ{α}))›
proof(rule "→I")
  AOT_assume ‹τ↓›
  moreover AOT_have ‹∀α (φ{α} ≡ ∃β (β = α & φ{β}))›
    by (rule GEN) (fact "term-out:1")
  ultimately AOT_show ‹φ{τ} ≡ ∃α(α = τ & φ{α})›
    using "∀E" by blast
qed

AOT_theorem "term-out:3":
  ‹(φ{α} & ∀β(φ{β} → β = α)) ≡ ∀β(φ{β} ≡ β = α)›
  apply (rule "≡I"; rule "→I")
   apply (frule "&E"(1))
   apply (drule "&E"(2))
   apply (rule GEN; rule "≡I"; rule "→I")
  using "rule-ui:2[const_var]" "vdash-properties:5"
    apply blast
   apply (meson "rule=E" "id-eq:1")
  apply (rule "&I")
  using "id-eq:1" "≡E"(2) "rule-ui:3"
   apply blast
  apply (rule GEN; rule "→I")
  using "≡E"(1) "rule-ui:2[const_var]"
  by blast

(* Note: generalized alphabetic variant of the last theorem. *)
AOT_theorem "term-out:4":
  ‹(φ{β} & ∀α(φ{α} → α = β)) ≡ ∀α(φ{α} ≡ α = β)›
  using "term-out:3" .

(* TODO: Provide a nicer mechanism for introducing custom binders. *)
AOT_define AOT_exists_unique :: ‹α ⇒ φ ⇒ φ› "uniqueness:1":
  ‹«AOT_exists_unique φ» ≡⇩_d⇩_f ∃α (φ{α} & ∀β (φ{β} → β = α))›
syntax (input) "_AOT_exists_unique" :: ‹α ⇒ φ ⇒ φ› ("∃!_ _" [1,40])
syntax (output) "_AOT_exists_unique" :: ‹α ⇒ φ ⇒ φ› ("∃!_'(_')" [1,40])
AOT_syntax_print_translations
  "_AOT_exists_unique τ φ" <= "CONST AOT_exists_unique (_abs τ φ)"
syntax
   "_AOT_exists_unique_ellipse" :: ‹id_position ⇒ id_position ⇒ φ ⇒ φ›
   (‹∃!_...∃!_ _› [1,40])
parse_ast_translation‹
[(\<^syntax_const>‹_AOT_exists_unique_ellipse›,
  fn ctx => fn [a,b,c] => Ast.mk_appl (Ast.Constant "AOT_exists_unique")
  [parseEllipseList "_AOT_vars" ctx [a,b],c]),
 (\<^syntax_const>‹_AOT_exists_unique›,
  AOT_restricted_binder
    \<^const_name>‹AOT_exists_unique›
    \<^const_syntax>‹AOT_conj›)]›
print_translation‹AOT_syntax_print_translations [
  AOT_preserve_binder_abs_tr'
    \<^const_syntax>‹AOT_exists_unique›
    \<^syntax_const>‹_AOT_exists_unique›
    (\<^syntax_const>‹_AOT_exists_unique_ellipse›, true)
    \<^const_name>‹AOT_conj›,
  AOT_binder_trans
    @{theory}
    @{binding "AOT_exists_unique_binder"}
    \<^syntax_const>‹_AOT_exists_unique›
]›


context AOT_meta_syntax
begin
notation AOT_exists_unique (binder "❙∃❙!" 20)
end
context AOT_no_meta_syntax
begin
no_notation AOT_exists_unique (binder "❙∃❙!" 20)
end

AOT_theorem "uniqueness:2": ‹∃!α φ{α} ≡ ∃α∀β(φ{β} ≡ β = α)›
proof(rule "≡I"; rule "→I")
    AOT_assume ‹∃!α φ{α}›
    AOT_hence ‹∃α (φ{α} & ∀β (φ{β} → β = α))›
      using "uniqueness:1" "≡⇩_d⇩_fE" by blast
    then AOT_obtain α where ‹φ{α} & ∀β (φ{β} → β = α)›
      using "instantiation"[rotated] by blast
    AOT_hence ‹∀β(φ{β} ≡ β = α)›
      using