|
|
|
|
Impressum AOT_PLM.thy
Sprache: Isabelle
|
|
(*<*)
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 ‹Γ1 \⊨ φ› and ‹Γ2 \⊨ φ → ψ›
shows ‹Γ1, Γ2 \⊨ ψ›
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 ‹φ ≡df ψ›
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 ‹φ ≡df ψ›
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 ‹φ ≡df ψ›
shows ‹φ → ψ›
using "df-rules-formulas[1]"[axiom_inst, OF assms].
AOT_theorem "df-rules-formulas[4]":
assumes ‹φ ≡df ψ›
shows ‹ψ → φ›
using "df-rules-formulas[2]"[axiom_inst, OF assms].
AOT_axiom "df-rules-terms[1]":
assumes ‹τ{α1...αn} =df σ{α1...αn}›
shows ‹(σ{τ1...τn}↓ → τ{τ1...τn} = σ{τ1...τn}) &
(¬σ{τ1...τn}↓ → ¬τ{τ1...τ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 ‹τ =df σ›
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 ‹τ{α1...αn} =df σ{α1...αn}›
shows ‹(σ{τ1...τn}↓ → τ{τ1...τn} = σ{τ1...τn}) &
(¬σ{τ1...τn}↓ → ¬τ{τ1...τn}↓)›
using "df-rules-terms[1]"[axiom_inst, OF assms].
AOT_theorem "df-rules-terms[4]":
assumes ‹τ =df σ›
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 ‹Γ1 \⊨ φ → ψ› and ‹Γ2 \⊨ ψ → χ›
shows ‹Γ1, Γ2 \⊨ φ → χ›
using "→E" "→I" assms by blast
AOT_theorem "ded-thm-cor:2":
assumes ‹Γ1 \⊨ φ → (ψ → χ)› and ‹Γ2 \⊨ ψ›
shows ‹Γ1, Γ2 \⊨ φ → χ›
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 ‹φ ≡df ψ›
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 ‹φ ≡df ψ› and ‹φ›
shows ‹ψ›
using "≡Df" "≡E"(1) assms by blast
lemmas "≡dfE" = "rule-eq-df:2"
AOT_theorem "rule-eq-df:3":
assumes ‹φ ≡df ψ› and ‹ψ›
shows ‹φ›
using "≡Df" "≡E"(2) assms by blast
lemmas "≡dfI" = "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 ‹φ{[λν1...νn ψ{ν1...ν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} → φ{[λν1...νn ψ{ν1...ν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 \<forall>I followed by \<forall>E *)
ML‹
get_instantiated_allI ctxt varname thm = let
trm = Thm.concl_of thm
trm =
case trm of (@{const Trueprop} $ (@{const AOT_model_valid_in} $ _ $ x)) => x
| _ => raise Term.TERM ("Expected simple theorem.", [trm])
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 _ = []
vars = extractVars trm
vars = fold Term.add_vars vars []
var = hd vars
trmty =
case (snd var) of (Type (type_name‹AOT_var›, [t])) => (t)
| _ => raise Term.TYPE ("Expected variable type.", [snd var], [Var var])
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))
trm = Thm.cterm_of (Context.proof_of ctxt) trm
ty = hd (Term.add_tvars (Thm.prop_of @{thm "∀I"}) [])
typ = Thm.ctyp_of (Context.proof_of ctxt) trmty
allthm = Drule.instantiate_normalize (TVars.make [(ty, typ)], Vars.empty) @{thm "∀I"}
phi = hd (Term.add_vars (Thm.prop_of allthm) [])
allthm = Drule.instantiate_normalize (TVars.empty, Vars.make [(phi,trm)]) allthm
›
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": ‹(∀α1...∀αn(φ{α1...αn})) → φ{α1...α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":
‹(∀α1...∀αn (φ{α1...αn} → ψ{α1...αn})) →
((∀α1...∀αn φ{α1...αn}) → (∀α1...∀αn ψ{α1...αn}))›
using "cqt:3"[axiom_inst] by auto
AOT_theorem "cqt-basic:15":
‹(∀α1...∀αn (φ → ψ{α1...αn})) → (φ → (∀α1...∀αn ψ{α1...α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 "≡dfI" "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 ‹φ{[λν1...νn ψ{ν1...ν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) "≡dfE" 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 "≡dfI"[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 "≡dfE"[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 "≡dfE"[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 "≡dfE"[OF "identity:3"[of Π Π']] "&E" by blast
qed
}
next
AOT_modally_strict {
AOT_show ‹Π = Π' → Π'↓› for Π Π' :: ‹<'a>›
proof(rule "→I")
AOT_assume ‹Π = Π'›
AOT_thus ‹Π'↓› using "≡dfE"[OF "identity:3"[of Π Π']] "&E" by blast
qed
}
qed
instance o :: AOT_Term_id
proof
AOT_modally_strict {
fix φ ψ
AOT_show ‹φ = ψ → φ↓›
proof(rule "→I")
AOT_assume ‹φ = ψ›
AOT_thus ‹φ↓› using "≡dfE"[OF "identity:4"[of φ ψ]] "&E" by blast
qed
}
next
AOT_modally_strict {
fix φ ψ
AOT_show ‹φ = ψ → ψ↓›
proof(rule "→I")
AOT_assume ‹φ = ψ›
AOT_thus ‹ψ↓› using "≡dfE"[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 τ1 τ1' :: 'a and τ2 τ2' :: 'b
AOT_assume ‹«(τ1, τ2)¬ = «(τ1', τ2')¬›
AOT_hence ‹(τ1 = τ1') & (τ2 = τ2')› by (metis "≡dfE" tuple_identity_1)
AOT_hence ‹τ1↓› and ‹τ2↓›
using "t=t-proper:1" "&E" "vdash-properties:10" by blast+
AOT_thus ‹«(τ1, τ2)¬↓› by (metis "≡dfI" "&I" tuple_denotes)
qed
}
next
AOT_modally_strict {
fix τ τ' :: ‹'a×'b›
AOT_show ‹τ = τ' → τ'↓›
proof (induct τ; induct τ'; rule "→I")
fix τ1 τ1' :: 'a and τ2 τ2' :: 'b
AOT_assume ‹«(τ1, τ2)¬ = «(τ1', τ2')¬›
AOT_hence ‹(τ1 = τ1') & (τ2 = τ2')› by (metis "≡dfE" tuple_identity_1)
AOT_hence ‹τ1'↓› and ‹τ2'↓›
using "t=t-proper:2" "&E" "vdash-properties:10" by blast+
AOT_thus ‹«(τ1', τ2')¬↓› by (metis "≡dfI" "&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":
‹Π = Π' → ◻∀x1...∀xn ([Π]x1...xn ≡ [Π']x1...xn)›
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 → ((◻∀x1...∀xn ([F]x1...xn ≡ [F]x1...xn)) →
◻∀x1...∀xn ([F]x1...xn ≡ [G]x1...xn)))›
apply (rule GEN)+ using "l-identity"[axiom_inst] by force
ultimately AOT_have ‹Π = Π' → ((◻∀x1...∀xn ([Π]x1...xn ≡ [Π]x1...xn)) →
◻∀x1...∀xn ([Π]x1...xn ≡ [Π']x1...xn))›
using "∀E"(1) by blast
AOT_hence ‹(◻∀x1...∀xn ([Π]x1...xn ≡ [Π]x1...xn)) →
◻∀x1...∀xn ([Π]x1...xn ≡ [Π']x1...xn)›
using assumption "→E" by blast
moreover AOT_have ‹◻∀x1...∀xn ([Π]x1...xn ≡ [Π]x1...xn)›
by (simp add: RN "oth-class-taut:3:a" "universal-cor")
ultimately AOT_show ‹◻∀x1...∀xn ([Π]x1...xn ≡ [Π']x1...xn)›
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 ≡ ∀y1([λx [F]xy1] = [λx [G]xy1] & [λx [F]y1x] = [λx [G]y1x])›
proof -
AOT_have ‹F = G ≡ F↓ & G↓ &
∀y1([λx [F]xy1] = [λx [G]xy1] & [λx [F]y1x] = [λx [G]y1x])›
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 ≡ ∀y1∀y2([λx [F]xy1y2] = [λx [G]xy1y2] &
[λx [F]y1xy2] = [λx [G]y1xy2] &
[λx [F]y1y2x] = [λx [G]y1y2x])›
proof -
AOT_have ‹F = G ≡ F↓ & G↓ & ∀y1∀y2([λx [F]xy1y2] = [λx [G]xy1y2] &
[λx [F]y1xy2] = [λx [G]y1xy2] &
[λx [F]y1y2x] = [λx [G]y1y2x])›
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 ≡ ∀y1∀y2∀y3([λx [F]xy1y2y3] = [λx [G]xy1y2y3] &
[λx [F]y1xy2y3] = [λx [G]y1xy2y3] &
[λx [F]y1y2xy3] = [λx [G]y1y2xy3] &
[λx [F]y1y2y3x] = [λx [G]y1y2y3x])›
proof -
AOT_have ‹F = G ≡ F↓ & G↓ & ∀y1∀y2∀y3([λx [F]xy1y2y3] = [λx [G]xy1y2y3] &
[λx [F]y1xy2y3] = [λx [G]y1xy2y3] &
[λx [F]y1y2xy3] = [λx [G]y1y2xy3] &
[λx [F]y1y2y3x] = [λx [G]y1y2y3x])›
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 ≡ ∀x1...∀xn «AOT_sem_proj_id x1xn (λ τ . «[F]τ¬) (λ τ . «[G]τ¬)¬›
proof -
AOT_have ‹F = G ≡ F↓ & G↓ &
∀x1...∀xn «AOT_sem_proj_id x1xn (λ τ . «[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: ‹[λx1...xn [F]x1...xn] = F›
by (simp add: "lambda-predicates:3"[axiom_inst])
AOT_have ‹[λx1...xn [F]x1...xn]↓›
by "cqt:2[lambda]"
AOT_hence ‹[λx1...xn [F]x1...xn] = [λx1...xn [F]x1...xn]›
using "lambda-predicates:1"[axiom_inst] "→E" by blast
AOT_show ‹F = F› using "rule=E" 0 by force
}
qed
instance o :: 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 τ1 :: 'a and τ2 :: 'b
AOT_assume ‹«(τ1,τ2)¬↓›
AOT_hence ‹τ1↓› and ‹τ2↓›
using "≡dfE" "&E" tuple_denotes by blast+
AOT_hence ‹τ1 = τ1› and ‹τ2 = τ2›
using "id-eq:1"[unvarify α] by blast+
AOT_thus ‹«(τ1, τ2)¬ = «(τ1, τ2)¬›
by (metis "≡dfI" "&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":
java.lang.StringIndexOutOfBoundsException: Range [17, 16) out of bounds for length 38
java.lang.StringIndexOutOfBoundsException: Range [8, 7) out of bounds for length 38
proof
java.lang.StringIndexOutOfBoundsException: Range [12, 10) out of bounds for length 65
by (rule GEN) (metis "id-eq:1")
AOT_thus \openτ = τ using assms "\<ll
qed
AOT_theorem "rule=I[java.lang.StringIndexOutOfBoundsException: Range [32, 31) out of bounds for length 56
using "id-eq:1".
AOT_theorem "l=:[aba:
assumes ‹)<close>
shows " \lν1...νn φ{ν1...νn}] = [λν1...νn φ{ν1...νn}]"
-
AOT_have ‹∀α (α = α)›
by (rule GEN) (metis "id-eq:1")
moreover AOT_have ‹[λν1...νn φ{ν1...νn}]↓›
using assms by (rule "cqt:2[lambda]"[axiom_inst])
ultimately AOT_show ‹[λν1...νn φ{ν1...νn}] = [λν1...νn φ{ν1...νn}]›
using assms "∀E" by blast
"=I" = "rule=I:1" "rule=I:2[const_var]" "rule=I:2[lambda]"
"rule-id-df:1":
assumes ‹τ{α1...αn} =df σ{α1...αn}› and ‹σ{τ1...τn}↓›
shows ‹τ{τ1...τn} = σ{τ1...τn}›
-
AOT_have ‹σ{τ1...τn}↓ → τ{τ1...τn} = σ{τ1...τn}›
using "df-rules-terms[3]" assms(1) "&E" by blast
AOT_thus ‹τ{τ1...τn} = σ{τ1...τn}›
using assms(2) "→E" by blast
"rule-id-df:1[zero]":
assumes ‹τ =df σ› and ‹σ↓›
shows ‹τ = σ›
-
AOT_have ‹σ↓ → τ = σ›
using "df-rules-terms[4]" assms(1) "&E" by blast
AOT_thus ‹τ = σ›
using assms(2) "→E" by blast
"rule-id-df:2:a":
java.lang.NullPointerException
lemma subst_v_flip_eq_three:
-
\openτ{τ1...τn} = σ{τ1...τn}› using "rule-id-df:1" assms(1,2) by blast
AOT_thus ‹φ{σ{τ1...τn}}› using assms(3) "rule=E" by blast
"rule-id-df:2:a[2]":
assumes ‹τ{«(α1,α2)¬} =df σ{«(α1,αproof -
and ‹σ{«(τ1,τ2)¬}↓›
\open>φ>(τ,\<\>}}🚫
shows ‹φ{σ{«(τ1::'a::AOT_Term_id_2,τ2::'b::AOT_Term_id_2)¬}}›
-
AOT_have ‹τ{«(τ1,τ2)¬} = σ{«(τ1,τ2)¬}›
using "rule-id-df:1" assms(1,2) by auto
AOT_thus ‹φ{σ{«(τ1,τ2)¬}}› using assms(3) "rule=E" by blast
"rule-id-df:2:a[zero]":
assumes ‹τ =dby (sim add: supp_at_base |mtis b.suppsupp_b_em )+
shows ‹φ{σ}›
-
AOT_have ‹τ = σ› using "rule-id-df:1[zeroy (induct tm rule: v.induct) (simp_all add: fresh_at_base)
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
"=\<^lemma t:v
"rule-id-df:2:b":
assumes ‹τ "a"atom x 🚫
shows ‹φ{τ{τ1...τn}}›
-
AOT_have ‹τ{τ1...τn} = σ{τ1...τwher
using "rule-id-df:1" assms(1,2) by blast
AOT_hence ‹σ{τ1...τn}
using "rule=E" "=I"(1) "t=t-proper:1" "→E" by fast
java.lang.NullPointerException
"rule-id-df:2:b[2]":
assumes ‹τ{«by (auto simp: fresh_at_base)
and ‹σ
and ‹φ{σ{«(τ1,τ avo: r: e.trong_indu) (auto si: fresh)
shows ‹φ{τ{« Ai x ) =((tom i \sharpA \and j \sharp>A r>A ∨
-
AOT_have ‹τ{«(τ1,τ2)¬} = σ{«(τ1,τ2)¬}›
using "=I"(1) "rule-id-df:2:a[2]" RAA(1) assms(1,2) "→I" by metis
AOT_hence ‹apply m
using "rule=E" "=I"(1) "t=t-proper:1" "→E" by fast
AOT_thus ‹
"rule-id-df:2:b[zero]":
assumes ‹τ =df σ› and ‹
shows ‹φ{τ}›
AOT_have ‹τ = σ› using "rule-id-df:1[zero]" assms(1,2) by blast
AOT_hence ‹σ = τ›appl (sim ad subst_)
using "rule=E" "=I"(1) "t=t-proper:1" "→E" by fast
AOT_thus ‹φ{τ}› using assms(3) "rule=E" by blast
java.lang.NullPointerException
"free-thms:1": ‹τ↓ ≡ ∃β (β = τ)› flip_dfby (si add:flip_d permute_)+
(metis"🚫
"free-thms:2": ‹∀α φ show ?thesis b aut
by (metis "∃E" "rule=E" "cqt:2[const_var]"[axiom_inst] "→:
"free-thms:3[const_var]": ‹∃β (β = α)›
by (meson "∃I"(2) "id-eq:1")
"free-thms:3[lambda]":
assumes ‹
shows ‹∃
by (meson "=I"(3) assms "cqt:2[lambda]"[axiom_inst] "existential:1")
-tms:4[rel]":
‹([Π]κ1...κn ∨ κ1...κn[Π]) → ∃β (β = Π)›
by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a"[axiom_inst]
"cqt:5:b"[axiom_inst] "→I" "∃I"(1))
"free-thms:4[vars]":
java.lang.NullPointerException
by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a"[axiom_inst]
"cqt:5:b"[axiom_inst] "→I" "∃I"(1))
"free-thms:4[1,rel]":
‹([Π]κ:x and tm::e
by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a"[axiom_inst]
cqt:5:b"[axiom_inst] "→I" "∃I"(1))
"free-thms:4[1,1]":
‹([Π]κ ∨ κ[Π🚫
by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a"[axiom_inst]
">I" "∃
"free-thms:4[2,rel]":
‹([Π]κ1κ2 ∨ κ1κ:eqvt_def subst_,auto
by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a[2]"[axiom_inst]
"cqt:5:b[2]"[axiom_inst] "→I" "∃I"(1))
-thms:4[2,1]":
‹([Π]κ1κ2 ∨ κ :: "ce \Right> x →o>_[_::=_]cev› [1000,50,50] 500)
by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[2]"[axiom_inst]
"cqt:5:b[2]"[axiom_inst] "→I" "∃I"(1))
"free-thms:4[2,2]":
‹
(metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a[2]"[axiom_inst]
"cqt:5:b[2]"[axiom_inst] "→I" "∃I"(1))
"free-thms:4[3,rel]":
java.lang.NullPointerException
(mtis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a[3]"[axiom_inst]
"cqt:5:b[3]"[axiom_inst] "→I" "∃I"(1))
"free-thms:4[3,1]":
‹([Π]κ1κ2κ3 ∨
by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[3]"[axiom_inst]
→I" "∃I"(1))
"free-thms:4[3,2]":
‹([Π]κ(ubst_cev A i x ) = ((atom i ♯ A ∧ j ♯ A) ∨ (j ♯ x ∧ (j ♯ce.strong_)
by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[3]"[axis e.supp pure_fresh opp.fresh
"cqt:5:b[3]"[axiom_inst] "→I" "∃I"(1))
"free-thms:4qed(auto)+
‹([Π]κ[simp]:
by (metis "rule=I:1" "&E"(2) "∨subst_cev A A i t ) j u) = subst_cev A i (sbst_vv t j u )"
"cqt:5:b[3]"[axiom_inst] "→I" "∃I"(1))
"free-thms:4[4,rel]":
java.lang.NullPointerException
by (metis "rule=I:1" "&E"(1) "∨E"(1) "cqt:5:a[4]"[axiom_inst]
"cqt:5:b[4]"[axiom_inst] "→I" "∃I"(1))
"free-thms:4[4,1]":
‹([Π]κ1κ2κ3κ4 ∨ κ1κ2κ3κ4[Π]) → ∃β (β = κce.strong)
by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[4]"[axiom_inst]
"cqt:5:b[4]"[axiom_inst] "→I" "∃
java.lang.StringIndexOutOfBoundsException: Range [12, 11) out of bounds for length 31
\open([Π>kappa> \or> κ1κ2κ3κ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))
"free-thms:4[4,3]":
‹([Π]κ1κ2κ3κ4 ∨ κ1κ2κ3κ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))
"free-thms:4[4,4]":
‹([Π]κ1κperm_simps ce.perm_simps permute_pur ce.fresh oppstrong_exhau by presburger
by (metis "rule=I:1" "&E"(2) "∨E"(1) "cqt:5:a[4]"[axiom_inst]
cqt:5:b[4]"[axiom_inst] "→I" "∃I"(1))
"ex:11:": foral>🚫.= ea[xa::=v']cev" using subst_ev_var_flip assms by simp
by (rule GEN) (fact "cqt:2[const_var]"[axiom_inst])
"ex:1:b": ‹∀α
by (rule GEN) (fact "free-thms:3[const_var]")
"ex:2:a": ‹◻and x::x
by (rule RN) (fact "cqt:2[const_var]"[axiom_inst])
"ex:2:b": ‹◻∃β(β = α)›
by (rule RN) (fact "free-thms:3[const_var]")
"ex:3:a": ‹◻∀α α↓›
by (rule RN) (fact "ex:1:a")
"ex:3:b": ‹
by (rule RN) (fact "ex:1:b")
"ex:4:a": ‹∀α ◻\Aefinition
by (rule GEN; rule RN) (fact "cqt:2[const_var]"[axiom_inst])
"ex:4:b": ‹∀α◻
by (rule GEN; rule RN) (fact "free-thms:3[const_var]")
"ex:5:a": ‹◻show "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨x subst by met
(rule RN) simp add:: "e:4:a")
"ex:5:b show"atom a \sharp> tm \Longrightarrow subst_v tm a x = tm"
by (rule RN) (simp add: "ex:4:b")
"all-self=:1": ‹
by (rule RN; rule GEN) (fact "id-eq:1")
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
by (rule GEN; rule RN) (fact "id-eq:1")
"id-nec:1": ‹α = β → ◻(α = β)›
(rule "→I")
AOT_assume ‹α = β:xand c:ce and z::x
‹
by (rule RN) (fact "id-eq:1")
ultimately AOT_show ‹◻(α = β)› using "rule=E" by fast
"id-nec:2": ‹τ = σ → ◻(τ = σ)›
(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 ‹
out:1": \open<{>} \equiv> β>& \ph>{\beta>})
(rule "≡I"; rule "→I")
AOT_assume asm: ‹φ{α}›
AOT_show ‹∃z::=w]\^>c ssub>ev) z w "
by (rule "∃I"(2)[where β=α]; rule "&I")
(auto simp: "id-eq:1" asm)
AOT_assume 0: ‹∃β (β = α & φ{β})›
AOT_obtain β where ‹
using "∃E"[rotated, OF 0] by blast
AOT_thusfi e::ce
"term-out:2": shows"(z1 ↔ z1') ∙ e[z::=v]cev = e[z::= ((z1 ↔ z1') ∙ v)]ce(ominal_indu e ru:ce.strong_induct)
(rule "→I")
AOT_assume ‹τsection ‹
moreover AOT_have ‹∀\Rig> v 🚫
\>s A ix ) 🚫
java.lang.StringIndexOutOfBoundsException: Range [23, 22) out of bounds for length 66
using "∀E" by blast
"term-out:3":
‹(φ{α} & ∀β(φ{β} → β = α)) ≡ ∀β(φ{
apply (rule "≡I"; rule "→I")
java.lang.StringIndexOutOfBoundsException: Range [9, 8) out of bounds for length 24
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")
) "rule-ui:-ui:2[const_var]"
by blast
(* Note: generalized alphabetic variant of the last theorem. *)
AOT_theorem "term-out:4":
‹(φ{β} & ∀L> c[z::=[]\^>v]\^s>v[x::v]\<^v= c[z::=v]v"
using "term-out:3" .
(* TODO: Provide a nicer mechanism for introducing custom binders. *)
<\guillemotleft
syntax (input) "_AOT_exists_unique" :: ‹α →
(output) "_AOT_exists_unique" :: ‹α → φ → φ›
"_AOT_exists_unique τ φ" <=
java.lang.StringIndexOutOfBoundsException: Range [31, 30) out of bounds for length 129
(‹∃!_...∃!_ _› [1,40])
‹
(syntax_const‹>x \Rightarrow v 🚫
fn ctx => fn [a,b,c] => Ast.mk_appl (Ast.Constant "AOT_exists_unique")
[parseEllipseList "_AOT_vars" ctx [a,b],c]),
(syntax_const
AOT_restricted_binder
const_name‹AOT_exists_unique›
\<^assumes "atom
‹AOT_syntax_print_translations [
AOT_preserve_binder_abs_tr'
const_syntax‹AOT_exists_unique›
syntax_const y›
(syntax_const‹_AOT_exists_unique_ellipse›, true)
const_name‹AOT_conj›,
AOT_binder_trans
{theory}
@{binding "AOT_exists_unique_binder"}
syntax_const \sharp (x,v) ==> subst_tv { z : b | c } x v = { z : b | c[x::=v]cv }"
›
AOT_meta_syntax
AOT_exists_unique (binder \ apply(rule_tac y=a and c="(aa,b)" in τ.strong_exhaust)
AOT_no_meta_syntax
java.lang.StringIndexOutOfBoundsException: Range [32, 31) out of bounds for length 72
"uiquenes:2: \open\<!alpha> \ \e>\al>\fo>\be>(🚫
(rule "≡I"; rule "→I")
AOT_assume ‹∃!α φ{α}›
AOT_hence ‹∃α (φ{α} & ∀βmoreover have "c[z::=V_var cb]cv[xa::=va]cv = c[xa::=va]cv[z::=V_var cb]cv" using subst_cv_commute_full[of z va xa "V_var cb" ] assms fresh_def v.supp by fastforce
moreover have "ca[za::=V_var cb]cv[xa::=va]cv = ca[xa::=va]cv[za::=V_var cb]cv"
using subst_cv_commute_full[of za va xa "V_var cb" ] assms fresh_def v.supp by fastforce
using "instantiation"[rotated] by blast
AOT_hence ‹∀βultima show "c[xa:=va]\^sub>v = ca[xa::=va]cv[za::=V_var cb]cv" by simp
using "term-out:3" "≡E" by blast
AOT_thus ‹∃α∀β(φ
using "∃I" by fast
AOT_assume ‹∃α∀β(φ{β} ≡ β = α)›
AOT_obtain 🚫
java.lang.StringIndexOutOfBoundsException: Range [36, 35) out of bounds for length 115
using "term-out:3" "≡E" by blast
AOT_hence ‹
using "∃>\t"
AOT_thus ‹∃!α φ"(x 🚫
using "uniqueness:1" "≡dfI" by blast
"uni-most": ‹∃!α φ{α} → ∀β∀γ((φ{β} & φ{γ}) → β = γ)›
(ule "🚫
fix \< show
AOT_assume ‹∃!α φ{α}›nominal_nduct c avoi: xv zw rul: \t.strong_ind)
AOT_hence ‹∃α∀β(φ{β} ≡ β = α)›
using "uniqueness:2" "≡E" by blast
then AOT_obtain α where ‹ subst_cv_commute_full by simp
using "instantiation"[rotated] by blast
moreover AOT_assume ‹
ultimately AOT_have ‹β
"∀E"(1,2) by blast+
AOT_thus ‹β = γ›
by (metis "rule=E" "id-eq:2" "→E")
"nec-exist-!": ‹∀α(φ{α} → ◻φ{α}) → (∃!αusubst_v_fli[of z1 c1 z2 c2 v] eq_i ass subst__c_def by simp
(rule "→I"; rule "→I")
AOT_assume a: ‹∀α(φ{α} → ◻φ{α})›
AOT_assume ‹∃!α φ{α}›
AOT_hence ‹∃α (φ{α} & ∀β (φ
using "uniqueness:1" "≡d:"τ x →
then AOT_obtain α where ξ: ‹φ{α} & ∀β ♯T_r z b c) x = c[z::=[x]]cv"
using "instantiation"[rotated] by blast
AOT_have ‹◻φ{α}›
using ξ a "&E" "∀E" "→E" by fast
moreover AOT_have ‹∀β (◻φ{β} → β = α)›
apply (rule GEN; rule "→I")
using ξ[THEN "&E"(2), THEN "∀E"(2), THEN "→E"]
"qml:2"[axiom_inst, THEN "→E"] by blast
ultimately AOT_have ‹(◻φ{α} & ∀β (◻φ{β} → β = α))›
using "&I" by blast
AOT_thus ‹∃!α ◻φ{α}›
using "uniqueness:1" "≡dfI" "∃I" by fast
‹The Theory of Actuality and Descriptions›
‹\label{PLM: 9.8}›
"act-cond": ‹\A(φ → ψ) → (\Aφ → \Aψ)›
using "→I" "≡E"(1) "logic-actual-nec:2"[axiom_inst] by blast
"nec-imp-act": ‹◻φ → \Aφ›
by (metis "act-cond" "contraposition:1[2]" "≡E"(4)
"qml:2"[THEN act_closure, axiom_inst]
"qml-act:2"[axiom_inst] RAA(1) "→E" "→I")
"act-conj-act:1": ‹\A(\Aφ → φ)›
using "→I" "≡E"(2) "logic-actual-nec:2"[axiom_inst]
"logic-actual-nec:4"[axiom_inst] by blast
"act-conj-act:2": ‹\A(φ → \Aφ)›
by (metis "→I" "≡E"(2, 4) "logic-actual-nec:2"[axiom_inst]
"logic-actual-nec:4"[axiom_inst] RAA(1))
"act-conj-act:3": ‹(\Aφ & \Aψ) → \A(φ & ψ)›
-
AOT_have ‹◻(φ → (ψ → (φ & ψ)))›
by (rule RN) (fact Adjunction)
AOT_hence ‹\A(φ → (ψ → (φ & ψ)))›
using "nec-imp-act" "→E" by blast
AOT_hence ‹\Aφ → \A(ψ → (φ & ψ))›
using "act-cond" "→E" by blast
moreover AOT_have ‹\A(ψ → (φ & ψ)) → (\Aψ → \A(φ & ψ))›
by (fact "act-cond")
ultimately AOT_have ‹\Aφ → (\Aψ → \A(φ & ψ))›
using "→I" "→E" by metis
AOT_thus ‹(\Aφ & \Aψ) → \A(φ & ψ)›
by (metis Importation "→E")
"act-conj-act:4": ‹\A(\Aφ ≡ φ)›
-
AOT_have ‹(\A(\Aφ → φ) & \A(φ → \Aφ)) → \A((\Aφ → φ) & (φ → \Aφ))›
by (fact "act-conj-act:3")
moreover AOT_have ‹\A(\Aφ → φ) & \A(φ → \Aφ)›
using "&I" "act-conj-act:1" "act-conj-act:2" by simp
ultimately AOT_have ζ: ‹\A((A>φ → φ) & (φ → \Aφ))›
using "→E" by blast
AOT_have ‹\A(((\Aφ → φ) & (φ → \Aφ)) → (\Aφ ≡ φ))›
using "conventions:3"[THEN "df-rules-formulas[2]",
THEN act_closure, axiom_inst] by blast
AOT_hence ‹\A((\Aφ → φ) & (φ → \Aφ)) → \A(\Aφ ≡ φ)›
using "act-cond" "→E" by blast
AOT_thus ‹\A(\Aφ ≡ φ)› using ζ "→E" by blast
(* TODO: Consider introducing AOT_inductive. *)
inductive arbitrary_actualization for φ where
‹arbitrary_actualization φ «\Aφ¬›
| ‹arbitrary_actualization φ «\Aψ¬› if ‹arbitrary_actualization φ ψ›
declare arbitrary_actualization.cases[AOT]
arbitrary_actualization.induct[AOT]
arbitrary_actualization.simps[AOT]
arbitrary_actualization.intros[AOT]
syntax arbitrary_actualization :: ‹φ' → φ' → AOT_prop›
(‹ARBITRARY'_ACTUALIZATION'(_,_')›)
notepad
begin
AOT_modally_strict {
fix φ
AOT_have ‹ARBITRARY_ACTUALIZATION(\Aφ ≡ φ, \A(\Aφ ≡ φ))›
using AOT_PLM.arbitrary_actualization.intros by metis
AOT_have ‹ARBITRARY_ACTUALIZATION(\Aφ ≡ φ, \A\A(\Aφ ≡ φ))›
using AOT_PLM.arbitrary_actualization.intros by metis
AOT_have ‹ARBITRARY_ACTUALIZATION(\Aφ ≡ φ, \A\A\A(\Aφ ≡ φ))›
using AOT_PLM.arbitrary_actualization.intros by metis
}
end
AOT_theorem "closure-act:1":
assumes ‹ARBITRARY_ACTUALIZATION(\Aφ ≡ φ, ψ)›
shows ‹ψ›
using assms proof(induct)
case 1
AOT_show ‹\A(\Aφ ≡ φ)›
by (simp add: "act-conj-act:4")
next
case (2 ψ)
AOT_thus ‹\Aψ›
by (metis arbitrary_actualization.simps "≡
"logic-actual-nec:4"[axiom_inst])
qed
AOT_theorem "closure-act:2": ‹\ then obtain x1::\tau and x2:: where *:"x= (x1,x2)" by forc
by (simp add: " -conj-act:4" "∀I")
"closure-act:3": ‹\A∀
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "brackoff" is null
"logic-actual-nec:3"[axiom_inst]
"logic-actual-nec:4"[axiom_inst])
"closure-act:4": ‹\A\<moreover have " atom z \<notin> set [atom z']" using z
using "closure-act:3" .
"RA[1]":
assumes ‹\⊨ φ›
shows ‹using \tauAb_qifass
― ‹While this proof is rejected in PLM,
we merely state it as modally-fragile rule,
which addresses the concern in PLM.›
using "¬¬E" assms "≡E"(3) "logic-actual"[act_axiom_inst]
"logic-actual-nec:1"[axiom_inst] "modus-tollens:2" by blast
"RA[2]":
assumes ‹\⊨\◻ φ›
shows ‹\⊨\◻lbrace> > z' : B_bool | TRUE } x1a : B_bool | x3a }.e_f ei
― \<hen show ?case usingv<>(
does not require an appeal to the semantics itself.›
using RN assms "nec-imp-act" "vdash-properties:5" by blast
"RA[3]":
assumes ‹Γ \⊨\◻moreover have "{ za : B_id tid | TRUE } = { za : B_id tid | TRUE }[x::=v]\τv"
shows ‹\AΓ subst_cv.simps subst_tv.simps by (simp add: ‹atom za ♯ (x, v)›)
text‹This rule is only derivable from the semantics,
but apparently no proof actually relies on it.
If this turns out to be required, it is valid to derive it from the
semantics just like RN, but we refrain from doing so, unless necessary.›
(* using assms by (meson AOT_sem_act imageI) *)
oops ― ‹discard the rule›
AOT_act_theorem "ANeg:1": ‹¬ atom z } = supp c1 - { atom z1 }"
by (simp add: "RA[1]" "contraposition:1[1]" "deduction-theorem"
"≡I" "logic-actual"[act_axiom_inst])
"ANeg:2": ‹¬\A¬φ ≡ list.set(1) list.simps(15) sup_bot.right_neutral supp_b_empty)
using "ANeg:1" "≡I" "≡E"(5) "useful-tautologies:1"
"useful-tautologies:2" by blast
"Act-Basic:1": ‹\Aφ ∨ \A¬ "atom z1 \notin>supp b1 ∧ atom z ∉ supp b" using supp_b_empty by simp
by (meson "∨I"(1,2) "≡E"(2) "logic-actual-nec:1"[axiom_inst] "raa-cor:1")
"Act-Basic:2": ‹.eq_iff τass b.supp(1) list.se(1) list.set(2) sup_bot.right_neutral)
(rule "≡I"; rule "→I")
AOT_assumeqed
moreover AOT_have ‹\A((φ & ψ
by (simp add: "RA[2]" "Conjunction Simplification"(1))
moreover AOT_have ‹\A((φ & ψ) → ψ)›
by (simp add: "RA[2]" "Conjunction Simplification"(2))
ultimately AOT_show ‹ assumes "({ z : b | c }) = ({ zz : b | cc })" and "atom x ♯ c" and "x ≠ zz"
using "act-cond"[THEN "→E", THEN "→E"] "&I" by metis
AOT_assume ‹\Aφ & \Aψ›
AOT_thus ‹A(φ)›
using "act-conj-act:3" "vdash-properties:6" by blast
"Act-Basic:3": ‹ supp c" using assms fresh_def by blast
(rule "≡I"; rule "→I")
AOT_assume ‹A(φ ψ)›
moreover AOT_have ‹\A((φ ≡>supp cc" using assms by simp
by (simp add: "RA[2]" "deduction-theorem" "≡E"(1))
moreover AOT_have ‹\A((φ ≡ ψ) → (ψ → φ))›
by (simp add: "RA[2]" "deduction-theorem" "≡E"(2))
ultimately AOT_show ‹\A(φ → ψ) & \A(ψ → φ)›Mutable Variable Context›
using "act-cond"[THEN "→E", THEN "→
java.lang.StringIndexOutOfBoundsException: Range [13, 12) out of bounds for length 113
AOT_hence ‹\A((φ → ψ) & (ψ → φ))›
by (metis "act-conj-act:3" "vdash-properties:10")
moreover AOT_have ‹\A(((φ → ψ) & (ψ → φ)) → (φ ≡ ψ))›
by (simp add: "conventions:3" "RA[2]" "df-rules-formulas[2]"
"vdash-properties:1[2]")
ultimately AOT_show ‹\A(φ ≡ ψ)›
using "act-cond"[THEN "→E", THEN "→E"] by metis
"Act-Basic:4": ‹(\A(φ → ψ) & \A(ψ → φ)) ≡ (\Aφ ≡ \Aψ)›
(rule "≡I"; rule "→I")
AOT_assume 0: ‹\A(φ → ψ) & \A(ψ → φ)›
AOT_show ‹\Aφ ≡ \Aψ›
using 0 "&E" "act-cond"[THEN "→E", THEN "→# SPX-License-Identifier: GPL-2.0-only
AOT_assume ‹\Aφ ≡ \Aψ›
AOT_thus ‹\A(φ → ψ) & \A(ψ → φ)›
by (metis "→I" "logic-actual-nec:2"[axiom_inst] "≡E"(1,2) "&I")
"Act-Basic:5": ‹\A(φ ≡ ψ) ≡ (\Aφ ≡ \Aψ)›
using "Act-Basic:3" "Act-Basic:4" "≡E"(5) by blast
"Act-Basic:6": ‹\Aφ ≡ ◻\Aφ›
by (simp add: "≡I" "qml:2"[axiom_inst] "qml-act:1"[axiom_inst])
"Act-Basic:7": ‹\A◻φ → ◻\Aφ›
by (metis "Act-Basic:6" "→I" "→E" "≡E"(1,2) "nec-imp-act"
"qml-act:2"[axiom_inst])
"Act-Basic:8": ‹◻φ → ◻\Aφ›
using "Hypothetical Syllogism" "nec-imp-act" "qml-act:1"[axiom_inst] by blast
"Act-Basic:9": ‹\A(φ ∨ ψ) ≡ (\Aφ ∨ \Aψ)›
(rule "≡I"; rule "→
AOT_assume ‹vl Nl
AOT_thus ‹\Δ Δ x v = (,[:=]v) # (subst_dv\D>x v ))"
proof (rule "raa-cor:3")
AOT_assume ‹¬(\Aφ ∨ \Aψ)›
AOT_hence ‹¬\Aφ & ¬\Aψ›
by (metis "≡E"(1) "oth-class-taut:5:d")
AOT_hence ‹\A¬φ & \A¬ψ›
using "logic-actual-nec:1"[axiom_inst, THEN "≡E"(2)] "&E" "&I" by metis
AOT_hence ‹\A(¬φ & ¬ψ)›
using "≡E" "Act-Basic:2" by metis
moreover AOT_have ‹\A((¬φ & ¬ψ) ≡ ¬(φ ∨ ψ))›
using "RA[2]" "≡E"(6) "oth-class-taut:3:a" "oth-class-taut:5:d" by blast
moreover AOT_have ‹\A(¬φ & ¬ψ) ≡ \A(¬(φ ∨ ψ))›
using calculation(2) by (metis "Act-Basic:5" "≡E"(1))
ultimately AOT_have ‹\A(¬(φ ∨ ψ))› using "≡E" by blast
AOT_thus ‹¬\A(φ ∨ ψ)›
using "logic-actual-nec:1"[axiom_inst, THEN "≡E"(1)] by auto
qed
AOT_assume ‹\Aφ ∨ \Aψ›
AOT_thus ‹\A(φ ∨ ψ)›
by (meson "RA[2]" "act-cond" "∨I"(1) "∨E"(1) "Disjunction Addition"(1,2))
"Act-Basic:10": ‹\A∃α φ{α} ≡ ∃α \Aφ{α}›
-
AOT_have θ: ‹¬\A∀α ¬φ{α} ≡ ¬∀α \A¬φ{α}›
by (rule "oth-class-taut:4:b"[THEN "≡E"(1)])
(metis "logic-actual-nec:3"[axiom_inst])
AOT_have ξ: ‹¬∀α \A¬φ{α} ≡ ¬∀α ¬\Aφ{α}›
by (rule "oth-class-taut:4:b"[THEN "≡E"(1)])
(rule "logic-actual-nec:1"[THEN universal_closure,
axiom_inst, THEN "cqt-basic:3"[THEN "→E"]])
AOT_have ‹\A(∃α φ{α}) ≡ \A(¬∀α ¬φ{α})›
using "conventions:4"[THEN "df-rules-formulas[1]",
THEN act_closure, axiom_inst]
"conventions:4"[THEN "df-rules-formulas[2]",
THEN act_closure, axiom_inst]
"Act-Basic:4"[THEN "≡E"(1)] "&I" "Act-Basic:5"[THEN "≡E"(2)] by metis
also AOT_have ‹… ≡ ¬\A∀α ¬φ{α}›
by (simp add: "logic-actual-nec:1" "vdash-properties:1[2]")
also AOT_have ‹… ≡ ¬∀α \A ¬φ{α}› using θ by blast
also AOT_have ‹… ≡ ¬∀α ¬\A φ{α}› using ξ by blast
also AOT_have ‹… ≡ ∃α \A φ{α}›
using "conventions:4"[THEN "≡Df"] by (metis "≡E"(6) "oth-class-taut:3:a")
finally AOT_show ‹\A∃α φ{α} ≡ ∃α \Aφ{α}› .
"Act-Basic:11":
‹\A∀α(φ{α} ≡ ψ{α}) ≡ ∀α(\Aφ{α} ≡ \Aψ{α})›
(rule "≡I"; rule "→I")
AOT_assume ‹\A∀α(φ{α} ≡ ψ{α})›
AOT_hence ‹∀α\A(φ{α} ≡ ψ{α})›
using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] by blast
AOT_hence ‹\A(φ{α} ≡ ψ{α})› for α using "∀E" by blast
AOT_hence ‹\Aφ{α} ≡ \Aψ{α}› for α by (metis "Act-Basic:5" "≡E"(1))
AOT_thus ‹∀α(\Aφ{α} ≡ \Aψ{α})› by (rule "∀I")
AOT_assume ‹∀α(\Aφ{α} ≡ \Aψ{α})›
AOT_hence ‹\Aφ{α} ≡ \Aψ{α}› for α using "∀E" by blast
AOT_hence ‹\A(φ{α} ≡ ψ{α})› for α by (metis "Act-Basic:5" "≡E"(2))
AOT_hence ‹∀α \A(φ{α} ≡ ψ{α})› by (rule "∀I")
AOT_thus ‹\A∀α(φ{α} ≡ ψ{α})›
using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(2)] by fast
"act-quant-uniq":
‹∀β(\Aφ{β} ≡ β = α) ≡ ∀β(φ{β} ≡ β = α)›
(rule "≡I"; rule "→I")
AOT_assume ‹∀β(\Aφ{β} ≡ β = α)›
AOT_hence ‹\Aφ{β} ≡ β = α› for β using "∀E" by blast
AOT_hence ‹φ{β} ≡ β = α› for β
using "≡I" "→I" "RA[1]" "≡E"(1,2) "logic-actual"[act_axiom_inst] "→E"
by metis
AOT_thus ‹∀β(φ{β} ≡ β = α)› by (rule "∀I")
AOT_assume ‹∀β(φ{β} ≡ β = α)›
AOT_hence ‹φ{β} ≡ β = α› for β using "∀E" by blast
AOT_hence ‹\Aφ{β} ≡ β = α› for β
using "≡I" "→I" "RA[1]" "≡E"(1,2) "logic-actual"[act_axiom_inst] "→E"
by metis
java.lang.NullPointerException
"fund-cont-desc": ‹x = subst_dv_abbrev🚫cas Nl
using descriptions[axiom_inst] "act-quant-uniq" "≡E"(5) by fast
hintikka: ‹
using "Commutativity of ≡"[THEN "≡E"(1)] then show ?case unfolding subst_dv.simps using fresh_DCons fresh_subst_tv_if fresh_Pair by metis
"fund-cont-desc" "≡E"(5) by blast
russell_axiom =
fixes ψ
assumes ψ_denotes_asm: "[v ⊨ ψ{κ}] ==> [v ⊨ κ↓]"
"russell-axiom":
‹ψ{\ιx φ{x}} ≡ ∃x(φ{x} & ∀z(φ{z} → z = x) & ψ{x})›pysl of.
java.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 0
AOT_have b: ‹x (x \^old>ιx φequiv> (φ{x} & ∀z(φ{z} → z = x)))›
using hintikka "∀I" by fast
show ?thesis
proof(rule "≡I"; rule "→I")
AOT_assume c: ‹ψ{\ιx φ{x}}›
AOT_hence d: ‹\ιx φ{x}↓›
using ψ_denotes_asm by blast
java.lang.StringIndexOutOfBoundsException: Range [15, 13) out of bounds for length 72
by (metis "rule=I:1" "existential:1")
java.lang.StringIndexOutOfBoundsException: Range [42, 41) out of bounds for length 80
using "instantiation"[rotated] by blast
moreover AOT_have ‹a = \ιx φ{x} ≡ (φ" us_v(S_thv c)xv=A_mc ('x:=\^>v (sbs_rnhvcs "
using b "∀E" by blast
ultimately AOT_have ‹φ{a} & ∀z(φ{z} →_f 's12)xv=(Sf(us_vv v) suts 1x (sssv2xv))
using "≡sharp> (x,v) ==> subst_sv (AS_var u τ v' s) x v = AS_var u (subst_tv τ x v ) (subst_vv v' x v ) (subst_sv s x v ) "
moreover AOT_have ‹ψ{a}›
proof -
AOT_have 1: ‹
by (simp add: "id-eq:2" "universal-cor")
AOT_have ‹a = \ιx φ{x} → \ιx φ{x} = a›
by (rule "∀E"(1)[where τ="«\ιx φ{x}¬"]; rule "∀E"(2)[where β=a])
(auto simp: 1 d "universal-cor")
AOT_thus ‹ψ{a}›
using a_def c "rule=E" "→E" by blast
qed
ultimately AOT_have ‹φ{a} & ∀z(φ{z} → z = a) & ψ{a}›
AOT_thus ‹∃x(φ{x} & ∀z(φ{z} → z
next
AOT_assume ‹∃x(φ{x} & ∀z(φ{z} → z = x) & ψ{x})›
then AOT_obtain b where g: ‹φ{b} & ∀z(φ{z} → z = b) & ψ{b}›
using "instantiation"[rotated] by blast
java.lang.NullPointerException
usingapply(subst Projl_permute)
AOT_have ‹φ{b} & ∀z(φ{z} → z = b)› and j: ‹ψ{b}›
using g "&E" by blast+
AOT_hence ‹b = \ιx φ{x}› using h "≡E" by blast
AOT_thus ‹ψ{\ιx φ{x}}›1ss_s_ustbacvsbstbrnhvgap Il(,av)))")
qed
java.lang.StringIndexOutOfBoundsException: Range [15, 11) out of bounds for length 37
by standard (metis "cqt:5:a[1]"[axiom_inst, THEN "→E"] "&E"(2))
"russell-axiom[exe,2,1,1]": russell_axiom ‹λ κ . «[Π]κκ'¬›
by standard (metis "cqt:5:a[2]"[axiom_inst, THEN "→E"] "&E")
"russell-axiom[exe,2,1,2]": russell_axiom ‹λ κ . «[Π]κ'꬛
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
by standard (metis "cqt:5:a[2]"[axiom_inst, THEN "→E"] "&E"(2))
"russell-axiom[exe,3,1,1]": rui case (1 P '
by standard (metis "cqt:5:a[3]"[axiom_inst, THEN "→E"] "&E")
"russell-axiom[exe,3,1,2]": russell_axiom ‹λ κ . «[Π]κ'κκ''¬
by standard (metis "cqt:5:a[3]"[axiom_inst, THEN "→cassa
"russell-axiom[exe,3,1,3]": russell_axiom ‹λ κied a c
by standard (metis "cqt:5:a[3]"[axiom_inst, THEN "→E"] "&E"(2))
"russell-axiom[exe,3,2,1]": russell_axiom ‹λ κ
by standard (metis "cqt:5:a[3]"[axiom_inst, THEN "→E"] "&E")
"russell-axiom[exe,3,2,2]": russell_axiom ‹λ κ . «
by sta proof(asesb)
"russell-axiom[exe,3,2,3]": russell_axiom ‹λ κ . «
by standard (metis "cqt:5:a[3]"[axiom_inst, THEN "→E"] "&E"(2))
"russell-axiom[exe,3,3]": russell_axiom ‹λ κ . «[Π]κκ꬛
by standard (metis "cqt:5:a[3]"[axiom_inst, THEN "→
"russell-axiom[enc,1]": russell_axiom ‹λ κ . «κ[Π]¬ n2 Irb)thuPpofb
by standard (metis "cqt:5:b[1]"[axiom_inst, THEN "\ s ab cc
"russell-axiom[enc,2,1]": russell_axiom ‹λ κ uingn n s_an__bachlis.togehas rs_trisr ymets
by standard (metis "cqt:5:b[2]"[axiom_inst, THEN "→E"] "&E")
"russell-axiom[enc,2,2]": russell_axiom ‹λ κ . «κ'κ[Π]¬›
by standard (metis "cqt:5:b[2]"[axiom_inst, THEN "→E"] "&E"(2))
"russell-axiom[enc,2,3]": russell_axiom ‹λ κ . «κκ[Π]¬›
by standard (metis "cqt:5:b[2]"[axiom_inst, THEN "→E"] "&E"(2))
"russell-axiom[enc,3,1,1]": russell_axiom ‹λ κ . «κκ'κ''[Π]¬
by standard (metis "cqt:5:b[3]"[axiom_inst, THEN "→E"] "&E")
"russell-axiom[enc,3,1,2]": russell_axiom ‹λ κ . «κ'κκ''[Π]¬›
by standard (metis "cqt:5:b[3]"[axiom_inst, THEN "→E"] "&E")
"russell-axiom[enc,3,1,3]": russell_axiom ‹λ κ . «κ'κ''κ[Π]¬tpob lat
by standard (metis "cqt:5:b[3]"[axiom_inst, THEN "→next
"russell-axiom[enc,3,2,1]": russell_axiom ‹λ κ . «(4 u a asuas )
by standard (metis "cqt:5:b[3]"[axiom_inst, THEN "→E"] "&E")
"russell-axiom[enc,3,2,2]": russell_axiom ‹λ κ . «κκ'κ[Π]¬›
by standard (metis "cqt:5:b[3]"[axiom_inst, THEN "→E"] "&E"(2))
"russell-axiom[enc,3,2,3]": russell_axiom ‹λ κ . «κ'κκ[Π]¬›
by standard (metis "cqt:5:b[3]"[axiom_inst, THEN "→E"] "&E"(2))
"russell-axiom[enc,3,3]": russell_axiom ‹λ κ . «κκκ[Π]¬›
by standard (metis "cqt:5:b[3]"[axiom_inst, THEN "→E"] "&E"(2))
"!-exists:1": ‹\ιx φ{x}↓ ≡
(rule "≡
java.lang.NullPointerException
AOT_hence ‹
then AOT_obtain a where ‹a = x →Rightar> s" (\" (‹_[_::=_]sv› [1000,50,50] 1000)
using "instantiation"[rotated] by blast
AOT_hence ‹φ{a} & ∀z (φ{z} → z = a)›
using hintikka "≡E" by blast
AOT_hence ‹∃x (φ{x} & ∀z (φ{z} → z = x))›
by (rule "∃I")
AOT_thus ‹∃!x φ{x}›
using "uniqueness:1"[THEN "≡dfI"] by blast
AOT_assume ‹∃!x φ{x}›
AOT_hence ‹∃x (φ{x} & ∀z (φ{z} → z = x))›
using "uniqueness:1"[THEN "≡dfE"] by blast
then AOT_obtain b where ‹φ{b} & ∀z (φ{z} → z = b)›
using "instantiation"[rotated] by blast
AOT_hence ‹b = \ιx φ{x}›
using hintikka "≡E" by blast
AOT_thus ‹\ιx φ{x}↓›
by (metis "t=t-proper:2" "vdash-properties:6")
"!-exists:2": ‹∃y(y=\ιx φ{x}) ≡ ∃!x φ{x}›
using "!-exists:1" "free-thms:1" "≡E"(6) by blast
"y-in:1": ‹x = \ιx φ{x} → φ{x}›
using "&E"(1) "→I" hintikka "≡E"(1) by blast
(* Note: generalized alphabetic variant of the last theorem *)
AOT_act_theorem "y-in:2": ‹z = \ιx φ{x} → φ{z}› using "y-in:1".
AOT_act_theorem "y-in:3": ‹\ιx φ{x}↓ → φ{\ιx φ{x}}›
proof(rule "→I")
AOT_assume ‹\ιx φ{x}↓›
AOT_hence ‹∃y (y = \ιx φ{x})›
by (metis "rule=I:1" "existential:1")
then AOT_obtain a where ‹a = \ιx φ{x}›
using "instantiation"[rotated] by blast
moreover AOT_have ‹φ{a}›
using calculation hintikka "≡E"(1) "&E" by blast
ultimately AOT_show ‹φ{\ιx φ{x}}› using "rule=E" by blast
qed
AOT_act_theorem "y-in:4": java.lang.StringIndexOutOfBoundsException: Range [106, 105) out of bounds for length 133
using "y-in:3"[THEN "→E"] "free-thms:1"[THEN "≡E"(2)] "→I" by blast
"act-quant-nec":
java.lang.StringIndexOutOfBoundsException: Range [49, 48) out of bounds for length 151
(rule "≡I"; rule "→I")
AOT_assume ‹∀β (s subst_branchv s x v"
java.lang.NullPointerException
AOT_hence ‹\Av[ip: "ie(us_vAix) ieA nd "ie(sbt_ach ix =sz " n szesbtbacl ieC
by (metis "Act-Basic:5" "act-conj-act:4" "≡E"(1) "≡E"(5))
AOT_thus ‹∀β(\A\Aφ{β} ≡ β = α)›
by (rule "∀I")
AOT_assume ‹∀β(\A\<A c a nCin l s_rnh__rn_issrn_ncatsm:rhtae
AOT_hence ‹
AOT_hence ‹\Aφsm]:"us_vAa(_a )=A n"ustbrnh _a )=B n sbtbrnhvC Va ) C
by (metis "Act-Basic:5" "act-conj-act:4" "≡E"(1) "≡E"(6))
AOT_thus ‹∀β (\Aφ{β} ≡ β = α)›
by (rule "∀I")
"equi-desc-descA:1": ‹
java.lang.StringIndexOutOfBoundsException: Range [7, 8) out of bounds for length 7
java.lang.NullPointerException
using descriptions[axiom_inst] by blast
also AOT_have ‹... ≡
proof(rule "≡shows
java.lang.StringIndexOutOfBoundsException: Range [42, 40) out of bounds for length 156
AOT_hence ‹\Aamx 🚫
using "∀Nn)
AOT_thus ‹tei uig S_e feho rs_ubs_v_i lt.ic is.st_csssbac__rnhlitrs e_nD
by (metis "Act-Basic:5" "act-conj-act: by ei
next
AOT_assume ‹∀z (\A\Aφ{z} ≡
AOT_hence ‹\A\Aφtau> s1 s2)
using "∀E" by blast
AOT_thus ‹\Aφ{a} ≡ a = x› for a
by (metis "Act-Basic:5" "act-conj-act:4" "≡E"(1) "≡E"(6))
qed
also AOT_have ‹... ≡ x = \ιx(\Aφhence "subst_s (Set \taus 2 xv= (Slt2y\tau s1 s2)" using forget_subst_sv by simp
using "Commutativity of ≡ (AS_let2 y τ s1 s2)" using AS_let2 by argo
finally show ?thesis .
"equi-desc-descA:2": ‹\ιx φ{x}↓ → [x::=v]v) (s1[x::=v]v) (s2[x::=v]v)" using subst_sv.simps AS_let2 y oc
(rule "\< then]<sv" using assms by presburger
AOT_assume ‹\ιx φ{x}↓›
AOT_hence ‹∃y (y = \ιx φ{x})›
by (metis "rule=I:1" "existential:1")
then AOT_obtain a where ‹a = \ιx φ{x}›
using "instantiation"[rotated] by blast
moreover AOT_have ‹a = \ιx(\Aφ{x})›
using calculation "equi-desc-descA:1"[THEN "≡E"(1)] by blast
ultimately AOT_show ‹\ιx φ{x} = \ιx(\Aφ{x})›
using "rule=E" by fast
"nec-hintikka-scheme":
‹x = \ιx φ{x} ≡ \Aφ{x} & ∀z(\Aφ{z} → z = x)›
-
AOT_have ‹x = \ιx φ{x} ≡ ∀z(\Aφ{z} ≡ z = x)›
using descriptions[axiom_inst] by blast
also AOT_have ‹… ≡ (\Aφ{x} & ∀z(\Aφ{z} → z = x))›
using "Commutativity of ≡"[THEN "≡E"(1)] "term-out:3" by fast
finally show ?thesis.
"equiv-desc-eq:1":
‹\A∀x(φ{x} ≡ ψ{x}) → ∀x (x = \ιx φ{x} ≡ x = \ιx ψ{x})›
(rule "→I"; rule "∀I")
fix β
AOT_assume ‹\A∀x(φ{x} ≡ ψ{x})›
AOT_hence ‹\A(φ{x} ≡ ψ{x})› for x
using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(1)] "∀E"(2) by blast
AOT_hence 0: ‹\Aφ{x} ≡ \Aψ{x}› for x
by (metis "Act-Basic:5" "≡E"(1))
AOT_have ‹β = \ιx φ{x} ≡ \Aφ{β} & ∀z(\Aφ{z} → z = β)›
using "nec-hintikka-scheme" by blast
also AOT_have ‹... ≡ c) ∙le> c) ∙ xa) ::= ((xa ↔ c) ∙ v') ]sv" using assms
proof (rule "≡I"; rule "→I")
AOT_assume 1: ‹\Aφ{β} & ∀z(\Aφ{z} → z = β)›
AOT_hence ‹\Aφ{z} → z = β› for z
using "&E" "∀E" by blast
AOT_hence ‹\Aψ{z} → z = β› for z
using 0 "≡E" "→I" "→E" by metis
AOT_hence ‹∀z(\Aψ{z} → z = β)›
using "∀I" by fast
moreover AOT_have ‹\Aψ{β}›
using "&E" 0[THEN "≡E"(1)] 1 by blast
ultimately AOT_show ‹\Aψ{β} & ∀z(\Aψ{z} → z = β)›
using "&I" by blast
next
AOT_assume 1: ‹\Aψ{β} & ∀z(\Aψ{z} → z = β)›
AOT_hence ‹\Aψ{z} → z = β› for z
using "&E" "∀E" by blast
AOT_hence ‹\Aφ{z} → z = β› for z
using 0 "≡E" "→I" "→E" by metis
AOT_hence ‹∀z(\Aφ{z} → z = β)›
using "∀I" by fast
moreover AOT_have ‹\Aφ{β}›
using "&E" 0[THEN "≡E"(2)] 1 by blast
ultimately AOT_show ‹\Aφ{β} & ∀z(\Aφ{z} → z = β)›
using "&I" by blast
qed
also AOT_have ‹... ≡ β = \ιx ψ{x}›
using "Commutativity of ≡"[THEN "≡E"(1)] "nec-hintikka-scheme" by blast
finally AOT_show ‹β = \ιx φ{x} ≡ β = \ιx ψ{x}› .
"equiv-desc-eq:2":
‹\ιx φ{x}↓ & \A∀x(φ{x} ≡ ψ{x}) → \ιx φ{x} = \ιx ψ{x}›
(rule "→I")
AOT_assume ‹\ιx φ{x}↓ & \A∀x(φ{x} ≡ ψ{x})›
AOT_hence 0: ‹∃y (y = \ιx φ{x})› and
1: ‹∀x (x = \ιx φ{x} ≡ x = \ιx ψ{x})›
using "&E" "free-thms:1"[THEN "≡E"(1)] "equiv-desc-eq:1" "→E" by blast+
then AOT_obtain a where ‹a = \ιx φ{x}›
using "instantiation"[rotated] by blast
moreover AOT_have ‹a = \ιx ψ{x}›
using calculation 1 "∀E" "≡E"(1) by fast
ultimately AOT_show ‹\ιx φ{x} = \ιx ψ{x}›
using "rule=E" by fast
"equiv-desc-eq:3":
‹\ιx φ{x}↓ & ◻∀x(φ{x} ≡ ψ{x}) → \ιx φ{x} = \ιx ψ{x}›
using "→I" "equiv-desc-eq:2"[THEN "→E", OF "&I"] "&E"
"nec-imp-act"[THEN "→E"] by metis
(* Note: this is a special case of "exist-nec" *)
AOT_theorem "equiv-desc-eq:4": ‹\ιx φ{x}↓ → ◻\ιx φ{x}↓›
proof(rule "→I")
AOT_assume ‹\ιx φ{x}↓›
AOT_hence ‹∃y (y = \ιx φ{x})›
by (metis "rule=I:1" "existential:1")
then AOT_obtain a where ‹a = \ιx φ{x}›
using "instantiation"[rotated] by blast
AOT_thus ‹by (metis flip_at_simps(1) flip_fresh_fresh fresh_PairD(1))
using "ex:2:a" "rule=E" by fast
"equiv-desc-eq:5": ‹\ιx φsub>sshres_i)
(rule "→I")
AOT_assume ‹qed
AOT_hence ‹∃y (y = \ιx φ{x})›
by (metis "rule=I:1" "existential:1")
then AOT_obtain a where ‹a = \ιx φ{x}\< assumesusing \t.eq_iff Abs1_eq_iff(3)[of z1' "CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1']v]cv"
using "instantiation"[rotated] by blast
AOT_hence ‹◻(a = \ιx φ{x})›
by (metis "id-nec:2" "vdash-properties:10")
AOT_thus ‹∃y ◻(y = \ιx φ{x})›
by (rule "∃I")
"equiv-desc-eq2:1":
‹∀x (φ{x} ≡ ψ{x}) → ∀x (x = \ιx φ{x} ≡ x = \ιx ψ{x})›
using "→I" "logic-actual"[act_axiom_inst, THEN "→E"]
"equiv-desc-eq:1"[THEN "→E"]
"RA[1]" "deduction-theorem" by blast
"equiv-desc-eq2:2":
‹\ιx φ{x}↓ & ∀x (φ{x} ≡ ψ{x}) → \ιx φ{x} = \ιx ψ{x}›
using "→I" "logic-actual"[act_axiom_inst, THEN "→E"]
"equiv-desc-eq:2"[THEN "→E", OF "&I"]
"RA[1]" "deduction-theorem" "&E" by metis
russell_axiom
"nec-russell-axiom":
‹ψ{\ιx φ{x}} ≡ ∃x(\Aφ{x} & ∀z(\Aφ{z} → z = x) & ψ{x})›
-
AOT_have b: ‹∀x (x = \ιx φ{x} ≡ (\Aφ{x} & ∀z(\Aφ{z} → z = x)))›
using "nec-hintikka-scheme" "∀I" by fast
show ?thesis
proof(rule "≡I"; rule "→I")
AOT_assume c: ‹ψ{\ιx φ{x}}›
AOT_hence d: ‹\ιx φ{x}↓›
using ψ_denotes_asm by blast
AOT_hence ‹∃y (y = \ιx φ{x})›
by (metis "rule=I:1" "existential:1")
then AOT_obtain a where a_def: ‹a = \ιx φ{x}›
using "instantiation"[rotated] by blast
moreover AOT_have ‹a = \ιx φ{x} ≡ (\Aφ{a} & ∀z(\Aφ{z} → z = a))›
using b "∀E" by blast
ultimately AOT_have ‹\Aφ{a} & ∀z(\Aφ{z} → z = a)›
using "≡E" by blast
moreover AOT_have ‹ψ{a}›
proof -
AOT_have 1: ‹∀x∀y(x = y → y = x)›
by (simp add: "id-eq:2" "universal-cor")
AOT_have ‹a = \ιx φ{x} → \ιx φ{x} = a›
by (rule "∀E"(1)[where τ="«\ιx φ{x}¬"]; rule "∀E"(2)[where β=a])
(auto simp: d "universal-cor" 1)
java.lang.NullPointerException
using a_def c "rule=E" "→E" by metis
qed
ultimately AOT_have ‹\Aφ{a} & ∀z(\lemma subst_sv_var_flip:
by (rule "&I")
java.lang.NullPointerException
java.lang.NullPointerException
next
AOT_assume ‹x({x} & ∀Aφ{z} →{x})›
then AOT_obtain b where g: ‹\Aφ"aom ♯ z) ∙v"
using "instantiation"[rotated] by blast
AOT_hence h: ‹b = \ιx φ{x} ≡ (\Aφ{b} & ∀using [[simproc del: alpha_lst]]
using b "∀E" by blast
AOT_have ‹\Aφ{b} & ∀z(\Aφ{z} → z = b)› and j: ‹ subst_tv_var_flip flip_fresh_freh v.fresh s_branch_s_branch_list.fresh
using g "&E" by blast+
AOT_hence ‹b = \ιx φ{x}›
using h "≡defer 11 (* Sometim defering hard goals to the end makes it easier to finish *)
AOT_thus ‹ψ{\ιx φ{x}}›
using j "rule=E" by blast
qed
java.lang.NullPointerException
(rule "≡
AOT_assume ‹\ιx_f Abs1_eq_iff'(3) flip_fresh_fresh
AOT_hence ‹∃flip_fresh_fresh)
by (metis "rule=I:1" "existential:1")
then AOT_obtain a where ‹a = \ιx φ{x}›instantiatis :: has_subst_v
using "instantiation"[rotated] by blast
moreover AOT_have ‹a = \ιx φ{x} ≡ ∀z(\Aφ{z} ≡ z = a)›
using descriptions[axiom_inst] by blast
ultimately AOT_have ‹ubst_v ubts"
using "≡E" by blast
AOT_hence ‹∃x∀ proof
AOT_thus ‹∃fix j:atmad :xad :vadt:
using "uniqueness:2"[THEN "≡E"(2) shw (j 🚫
java.lang.NullPointerException
AOT_hence \<open_
using "uniqueness:2"[THEN "≡E"(1)] by f hence "c[z::=[ b ]↑v]cv[xa::=va]cv = ca[za::=[ cb ]v]cv[xa::=va]cv" by auto
OT_obtain a where ‹∀z(\Aφ{z} ≡ z = a)›
using "instantiation"[rotated] by blast
java.lang.NullPointerException
using descriptions[axiom_inst] by blast
java.lang.StringIndexOutOfBoundsException: Range [13, 12) out of bounds for length 67
using "≡E" by blast
AOT_thus ‹{x}↓
by (metis "t=t-proper:2" "vdash-properties:6")
"actual-desc:2": \< then
using "&E"(1) "contraposition:1[2]" "≡E"(1) "nec-hintikka-scheme"
"reductio-aa:2" "vdash-properties:9" by blast
(* Note: generalized alphabetic variant of the last theorem *)
AOT_theoremactual-:3" \openz = phi{x} →bold>\A>\<{clos>
using "actual-desc:2".
AOT_theorem "actual-desc:4": ‹\<iota>x φ{x}↓ → \<A>φ{\<iota>x φ{x}}›
proof(rule "→I")
AOT_assume ‹\<iota>x φ{x}↓›
AOT_hence ‹∃y (y = \<iota>x φ{x})› by (metis "rule=I:1" "existential:1")
then AOT_obtain a where ‹a = \<iota>x φ{x}› using "instantiation"[rotated] by blast
AOT_thus ‹\<A>φ{\<iota>x φ{x}}›
using "actual-desc:2" "rule=E" "→E" by fast
qed
AOT_theorem "actual-desc:5": ‹\<iota>x φ{x} = \<iota>x ψ{x} → \<A>∀x(φ{x} ≡ ψ{x})›
proof(rule "→I")
AOT_assume 0: ‹\<iota>x φ{x} = \<iota>x ψ{x}›
AOT_hence φ_down: ‹\<iota>x φ{x}↓› and ψ_down: ‹\<iota>x ψ{x}↓›
using "t=t-proper:1" "t=t-proper:2" "vdash-properties:6" by blast+
AOT_hence ‹∃y (y = \<iota>x φ{x})› and ‹∃y (y = \<iota>x ψ{x})›
by (metis "rule=I:1" "existential:1")+
then AOT_obtain a and b where a_eq: ‹a = \<iota>x φ{x}› and b_eq: ‹b = \<iota>x ψ{x}›
using "instantiation"[rotated] by metis
AOT_have ‹∀α∀β (α = β → β = α)›
by (rule "∀I"; rule "∀I"; rule "id-eq:2")
AOT_hence ‹∀β (\<iota>x φ{x} = β → β = \<iota>x φ{x})›
using "∀E" φ_down by blast
AOT_hence ‹\<iota>x φ{x} = \<iota>x ψ{x} → \<iota>x ψ{x} = \<iota>x φ{x}›
using "∀E" ψ_down by blast
AOT_hence 1: ‹\<iota>x ψ{x} = \<iota>x φ{x}› using 0
"→E" by blast
AOT_have ‹\<A>φ{x} ≡ \<A>ψ{x}› for x
proof(rule "≡I"; rule "→I")
AOT_assume ‹\<A>φ{x}›
moreover AOT_have ‹\<A>φ{x} → x = a› for x
using "nec-hintikka-scheme"[THEN "≡E"(1), OF a_eq, THEN "&E>"(2)]
"∀E" by blast
ultimately AOT_have ‹x = a›
using "→E" by blast
AOT_hence ‹x = \<iota>x φ{x}›
using a_eq "rule=E" by blast
AOT_hence ‹x = \<iota>x ψ{x}›
using 0 "rule=E" by blast
AOT_thus ‹\<A>ψ{x}›
by (metis "actual-desc:3" "vdash-properties:6")
next
AOT_assume ‹\<A>ψ{x}›
moreover AOT_have ‹\<A>ψ{x} → x = b› for x
using "nec-hintikka-scheme"[THEN "≡E"(1), OF b_eq, THEN "&E>"(2)]
"∀E" by blast
ultimately AOT_have ‹x = b›
using "→E" by blast
AOT_hence ‹x = \<iota>x ψ{x}›
using b_eq "rule=E" by blast
AOT_hence ‹x = \<iota>x φ{x}›
using 1 "rule=E" by blast
AOT_thus ‹\<A>φ{x}›
by (metis "actual-desc:3" "vdash-properties:6")
qed
AOT_hence ‹\<A>(φ{x} ≡ ψ{x})› for x
by (metis "Act-Basic:5" "≡E"(2))
AOT_hence ‹∀x \<A>(φ{x} ≡ ψ{x})›
by (rule "∀I")
AOT_thus ‹\<A>∀x (φ{x} ≡ ψ{x})›
using "logic-actual-nec:3"[axiom_inst, THEN "≡E"(2)] by fast
qed
AOT_theorem "!box-desc:1": ‹∃!x ◻φ{x} → ∀y (y = \<iota>x φ{x} → φ{y})›
proof(rule "→I")
AOT_assume ‹∃!x ◻φ{x}›
AOT_hence ζ: ‹∃x (◻φ{x} & ∀z (◻φ{z} → z = x))›
using "uniqueness:1"[THEN "≡dfE"] by blast
then AOT_obtain b where θ: ‹◻φ{b} & ∀z (◻φ{z} → z = b)›
using "instantiation"[rotated] by blast
AOT_show ‹∀y (y = \<iota>x φ{x} → φ{y})›
proof(rule GEN; rule "→applyjava.lang.StringIndexOutOfBoundsException: Range [25, 24) out of bounds for length 68
fix y
AOT_assume < using
AOT_hence java.lang.NullPointerException
using "nec-hintikka-scheme"[THEN "≡E"(1)] by blast
AOT_hence ‹\Aφ{b} → b = y›
using "&E" "∀E" by blast
moreover AOT_have ‹:fun and z::x
using θ[THEN "&E"(1)] by (metis "nec-imp-act" "→E")
ultimately AOT_have ‹b = y›
using "→E" by blast
moreover AOT_have ‹φ{b}›
using θ[THEN "&E"(1)] by (metis "qml:2"[axiom_inst] "→E")
ultimately AOT_show ‹φ(ominal_induct c avoidin:z x v rule:fun_t.strong_induct)
using "rule=E" by blast
qed
"!box-desc:2":
‹∀
(rule "→I"; rule "→
AOT_assume ‹\<forall
moreover AOT_assume ‹ fun_typ_q : has_subst_v
ultimately AOT_have ‹∃
using "nec-exist-!"[THEN "→E", THEN "→E"] by blast
AOT_thus ‹∀
using "!box-desc:1" "→E" by blast
(* Note: vacuous in the embedding. *)
AOT_theorem "dr-alphabetic-thm": ‹\< fix
by (simp add: "rule=I:1" "→I")
‹The Theory of Necessity›
‹\label{PLM: 9.9}›
"RM:1[prem]":
assumes ‹x::::x nd c::un_typ_ and z::x
shows ‹◻Γ \⊨\◻ ◻φ → ◻ψ›
-
AOT_have ‹◻Γ \⊨\◻ ◻(φ → ψ)›
using "RN[prem]" assms by blast
AOT_thus ‹◻Γ \⊨\◻ ◻φ → ◻ψ›c avoidi: x z ru
by (metis "qml:1"[axiom_inst] "→E")
"RM:1":
assumes ‹\⊨\◻ φ → ψ›
shows ‹\⊨\◻ ◻φ → ◻ψ›
using "RM:1[prem]" assms by blast
RM = "RM:1"
"RM:2[prem]":
assumes ‹Γ \⊨\◻ φ → ψ›
shows ‹◻Γ \⊨\◻ ♢φ →
-
AOT_have ‹Γ \⊨\◻ ¬ψ →
using assms
by (simp add: "contraposition:1[1]")
AOT_hence ‹◻Γ \⊨\◻ ◻¬ψ → ◻¬φ›
using "RM:1[prem]" by blast subst_dv_f:
AOT_thus ‹\<box <v= fst ` setD Δ"
by (meson "≡dfE" "≡dfI" "conventions:5" "→I" "modus-tollens:1")
"RM:2":
assumes ‹\⊨
shows ‹x':: and x::x and v::v and c':c
using "RM:2[prem]" assms by blast
"RM♢" = "RM:2"
"RM:3[prem]":
assumes ‹Γ \⊨\◻ φ ≡ ψ›
shows ‹◻\proof-
-
AOT_have ‹Γ \⊨\◻ φ → ψ› ?hes usi as pro(ind \Gammarul: 🚫
using assms "≡E" "→I" by metis+
AOT_hence ‹◻Γ \⊨x', b', c')∈False toSet.simps by auto
using "RM:1[prem]" by metis+
AOT_thus ‹◻Γ \⊨\◻ ◻φ ≡ ◻ψ›
by (simp add: "≡I")
RM:3":
assumes ‹\⊨\◻ φ ≡ ψ›
shows ‹\⊨\◻ ◻φ ≡ ◻ψ›
using "RM:3[prem]" assms by blast
RE = "RM:3"
"RM:4[prem]":
assumes ‹Γ \⊨\◻ φ ≡ ψ›
shows ‹◻Γ \⊨\◻ ♢φ ≡ ♢ψ›
-
AOT_have ‹Γ \⊨\◻ φ → ψ› and ‹Γ \⊨\◻ ψ → φ›
using assms "≡E" "→I" by metis+
AOT_hence ‹◻Γ \⊨\◻ ♢
using "RM:2[prem]" by metis+
java.lang.NullPointerException
by (simp add: "≡
"RM:4":
assumes ‹\⊨\◻ φassum "j \s t \and> j \<x
shows ‹\⊨( \s> subs ti x)
using "RM:4[prem]" assms by blast
"RE♢" = "RM:4"
"KBasic:1": ‹◻φ → ◻(ψ → φ)›
by (simp add: RM "pl:1"[axiom_inst])
"KBasic:2": ‹◻¬φ → ◻(φ → ψ)›
by (simp add: RM "useful-tautologies:3")
"KBasic:3": ‹◻(φ & ψ) ≡ (◻φ
(rule "≡I"; rule "→I")
AOT_assume ‹◻(φ & ψ)›
AOT_thus ‹◻φ & ◻ψ›
by (meson RM "&I" "Conjunction Simplification"(1, 2) "→E")
AOT_have ‹◻φ → ◻(ψ → (φ & ψ
by (simp add: "RM:1" Adjunction)
AOT_hence ‹◻φ → (◻ψ → ◻(φ & ψ subst_g_ass:
by (metis "Hypothetical Syllogism" "qml:1"[axiom_inst])
moreover AOT_assume ‹◻φ & ◻ψ›
ultimately AOT_show ‹◻(φ & ψ)›
using "→E" "&E" by blast
"KBasic:4": ‹◻(φ ≡ ψ) ≡ (◻(φ → ψ) & ◻(ψ → φ))›
-
AOT_have θ: ‹◻((φ → ψ) & (ψ → φ)) ≡ (◻(φ → ψ) & ◻(ψ → φ))›
by (fact "KBasic:3")
AOT_modally_strict {
AOT_have ‹(φ ≡ ψ) ≡ ((φ → ψ) & (ψ → φ))›
>Df"])
}
AOT_hence ξ: ‹◻(φ ≡ ψ) ≡ ◻((φ → ψ) & (ψ →
by (rule RE)
with ξ and θ AOT_show ‹◻(φ ≡ ψ) ≡ (◻(φ → ψ) & ◻(ψ → φ))›
using "≡E"(5) by blast
"KBasic:5": ‹(◻(φ → ψ) & ◻(ψ → φ)) → (◻φ ≡ ◻ψ)›
-
AOT_have ‹◻(φ → ψ) → (◻φ → ◻ψ)›
by (fact "qml:1"[axiom_inst])
moreover AOT_have ‹◻(ψ → φ) → (◻ψ → ◻φ)›
by (fact "qml:1"[axiom_inst])
ultimately AOT_have ‹(◻(φ → ψ) & ◻(ψ → φ)) → ((◻φ → ◻ψ) & (tyle='font-size: 18px;'>◻ψ → ◻φ))›
by (metis "&I" MP "Double Composition")
moreover AOT_have ‹((◻φ → ◻ψ) & (◻ψ → ◻φ)) → (◻φ ≡ ◻ψ)›
using "conventions:3"[THEN "≡dfI"] "→I" by blast
ultimately AOT_show ‹(◻(φ → ψ) & ◻(ψ → φ)) → (◻φ ≡ ◻ψ)›
by (metis "Hypothetical Syllogism")
"KBasic:6": ‹◻(φ ≡ ψ) → (◻φ ≡ ◻ψ)›
using "KBasic:4" "KBasic:5" "deduction-theorem" "≡E"(1) "→E" by blast
"KBasic:7": ‹((◻φ & ◻ψ) ∨ (◻¬φ & ◻¬ψ)) → ◻(φ ≡ ψ)›
(rule "→I"; drule "∨E"(1); (rule "→I")?)
AOT_assume ‹◻φ & ◻ψ›
AOT_hence ‹◻φ› and ‹◻ψ› using "&E" by blast+
AOT_hence ‹◻(φ → ψ)› and ‹◻(ψ → φ)› using "KBasic:1" "→E" by blast+
AOT_hence ‹◻(φ → ψ) & ◻(ψ → φ)› using "&I" by blast
AOT_thus ‹◻(φ ≡ ψ)› by (metis "KBasic:4" "≡E"(2))
AOT_assume ‹◻¬φ & ◻¬ψ›
AOT_hence 0: ‹◻(¬φ & ¬ψ)› using "KBasic:3"[THEN "≡E"(2)] by blast
AOT_modally_strict {
AOT_have ‹(¬φ & ¬ψ) → (φ ≡ ψ)›
by (metis "&E"(1) "&E"(2) "deduction-theorem" "≡I" "reductio-aa:1")
}
AOT_hence ‹◻(¬φ & ¬ψ) → ◻(φ ≡ ψ)›
by (rule RM)
AOT_thus ‹◻(φ ≡ ψ)› using 0 "→E" by blast
(auto)
"KBasic:8": ‹◻(φ & ψ) → ◻(φ ≡ ψ)›
by (meson "RM:1" "&E"(1) "&E"(2) "deduction-theorem" "≡I")
"KBasic:9": ‹◻(¬φ & ¬ψ) → ◻(φ ≡ ψ)›
by (metis "RM:1" "&E"(1) "&E"(2) "deduction-theorem" "≡I" "raa-cor:4")
"KBasic:10": ‹◻φ ≡ ◻¬¬φ›
by (simp add: "RM:3" "oth-class-taut:3:b")
"KBasic:11": ‹¬◻φ ≡ ♢¬φ›
(rule "≡I"; rule "→I")
AOT_show ‹♢¬φ› if ‹¬◻φ›
using that "≡dfI" "conventions:5" "KBasic:10" "≡E"(3) by blast
AOT_show ‹¬◻φ› if ‹♢¬φ›
using "≡dfE" "conventions:5" "KBasic:10" "≡E"(4) that by blast
"KBasic:12": ‹◻φ ≡ ¬♢¬φ›
(rule "≡I"; rule "→I")
AOT_show ‹¬♢¬φ› if ‹◻φ›
using "¬¬I" "KBasic:11" "≡E"(3) that by blast
AOT_show ‹◻φ› if ‹¬♢¬φ›
using "KBasic:11" "≡E"(1) "reductio-aa:1" that by blast
"KBasic:13": ‹◻(φ → ψ) → (♢φ → ♢ψ)›
-
AOT_have ‹φ → ψ \⊨\◻ φ → ψ› by blast
AOT_hence ‹◻(φ → ψ) \⊨\◻ ♢φ → ♢ψ›
using "RM:2[prem]" by blast
AOT_thus ‹◻(φ → ψ) → (♢φ → ♢ψ)› using "→I" by blast
"K♢" = "KBasic:13"
"KBasic:14": ‹♢◻φ ≡ ¬◻♢¬φ›
by (meson "RE♢" "KBasic:11" "KBasic:12" "≡E"(6) "oth-class-taut:3:a")
"KBasic:15": ‹(◻φ ∨ ◻ψ) → ◻(φ ∨ ψ)›
-
AOT_modally_strict {
AOT_have ‹φ → (φ ∨ ψ)› and ‹ψ → (φ ∨ ψ)›
by (auto simp: "Disjunction Addition"(1) "Disjunction Addition"(2))
}
AOT_hence ‹◻φ → ◻(φ ∨ ψ)› and ‹◻ψ → ◻(φ ∨ ψ)›
using RM by blast+
AOT_thus ‹(◻φ ∨ ◻ψ) → ◻(φ ∨ ψ)›
by (metis "∨E"(1) "deduction-theorem")
"KBasic:16": ‹(◻φ & ♢ψ) → ♢(φ & ψ)›
by (meson "KBasic:13" "RM:1" Adjunction "Hypothetical Syllogism"
Importation "→E")
"rule-sub-lem:1:a":
assumes ‹\⊨\◻ ◻(ψ ≡ χ)›
shows ‹\⊨\◻ ¬ψ ≡ ¬χ›
using "qml:2"[axiom_inst, THEN "→E", OF assms]
"≡E"(1) "oth-class-taut:4:b" by blast
"rule-sub-lem:1:b":
assumes ‹\⊨\◻ ◻(ψ ≡ χ)›
shows ‹\⊨\◻ (ψ → Θ) ≡ (χ → Θ)›
using "qml:2"[axiom_inst, THEN "→E", OF assms]
using "oth-class-taut:4:c" "vdash-properties:6" by blast
"rule-sub-lem:1:c":
assumes ‹\⊨\◻ ◻(ψ ≡ χ)›
shows ‹\⊨\◻ (Θ → ψ) ≡ (Θ → χ)›
using "qml:2"[axiom_inst, THEN "→E", OF assms]
using "oth-class-taut:4:d" "vdash-properties:6" by blast
"rule-sub-lem:1:d":
assumes ‹for arbitrary α: \⊨\◻ ◻(ψ{α} ≡ χ{α})›
shows ‹\⊨\◻ ∀α ψ{α} ≡ ∀α χ{α}›
-
AOT_modally_strict {
AOT_have ‹∀α (ψ{α} ≡ χ{α})›
using "qml:2"[axiom_inst, THEN "→E", OF assms] "∀I" by fast
AOT_hence 0: ‹ψ{α} ≡ χ{α}› for α using "∀E" by blast
AOT_show ‹∀α ψ{α} ≡ ∀α χ{α}›
proof (rule "≡I"; rule "→I")
AOT_assume ‹∀α ψ{α}›
AOT_hence ‹ψ{α}› for α using "∀E" by blast
AOT_hence ‹χ{α}› for α using 0 "≡E" by blast
AOT_thus ‹∀α χ{α}› by (rule "∀I")
next
AOT_assume ‹∀α χ{α}›
AOT_hence ‹χ{α}› for α using "∀E" by blast
AOT_hence ‹ψ{α}› for α using 0 "≡E" by blast
AOT_thus ‹∀α ψ{α}› by (rule "∀I")
qed
}
"rule-sub-lem:1:e":
assumes ‹\⊨\◻ ◻(ψ ≡ χ)›
shows ‹\⊨\◻ [λ ψ] ≡ [λ χ]›
using "qml:2"[axiom_inst, THEN "→E", OF assms]
using "≡E"(1) "propositions-lemma:6" by blast
"rule-sub-lem:1:f":
assumes ‹\⊨\◻ ◻(ψ ≡ χ)›
shows ‹\⊨\◻ \Aψ ≡ \Aχ›
using "qml:2"[axiom_inst, THEN "→E", OF assms, THEN "RA[2]"]
by (metis "Act-Basic:5" "≡E"(1))
"rule-sub-lem:1:g":
assumes ‹\⊨\◻ ◻(ψ ≡ χ)›
shows ‹\⊨\◻ ◻ψ ≡ ◻χ›
using "KBasic:6" assms "vdash-properties:6" by blast
‹Note that instead of deriving @{text "rule-sub-lem:2"},
@{text "rule-sub-lem:3"}, @{text "rule-sub-lem:4"},
and @{text "rule-sub-nec"}, we construct substitution methods instead.›
AOT_subst =
fixes AOT_subst :: "('a → o) → bool"
and AOT_subst_cond :: "'a → 'a → bool"
assumes AOT_subst:
"AOT_subst φ ==> AOT_subst_cond ψ χ ==> [v ⊨ «φ ψ¬ ≡ «φ χ¬]"
AOT_substI
o :: AOT_subst
AOT_subst_o where
AOT_subst_o_id[AOT_substI]:
‹AOT_subst_o (λφ. φ)›
| AOT_subst_o_const[AOT_substI]:
‹AOT_subst_o (λφ. ψ)›
| AOT_subst_o_not[AOT_substI]:
‹AOT_subst_o Θ ==> AOT_subst_o (λ φ. «¬Θ{φ}¬)›
| AOT_subst_o_imp[AOT_substI]:
‹AOT_subst_o Θ ==> AOT_subst_o Ξ ==> AOT_subst_o (λ φ. «Θ{φ} → Ξ{φ}¬)›
| AOT_subst_o_lambda0[AOT_substI]:
‹AOT_subst_o Θ ==> AOT_subst_o (λ φ. (AOT_lambda0 (Θ φ)))›
| AOT_subst_o_act[AOT_substI]:
‹AOT_subst_o Θ ==> AOT_subst_o (λ φ. «\AΘ{φ}¬)›
| AOT_subst_o_box[AOT_substI]:
‹AOT_subst_o Θ ==> AOT_subst_o (λ φ. «◻Θ{φ}¬)›
| AOT_subst_o_by_def[AOT_substI]:
‹(∧ ψ . AOT_model_equiv_def (Θ ψ) (Ξ ψ)) ==>
AOT_subst_o Ξ ==> AOT_subst_o Θ›
AOT_subst_cond_o where
‹AOT_subst_cond_o ≡ λ ψ χ . ∀ v . [v ⊨ ψ ≡ χ]›
fix ψ χ :: o and φ :: ‹o → o›
assume cond: ‹AOT_subst_cond ψ χ›
assume ‹AOT_subst φ›
moreover AOT_have ‹\⊨\◻ ψ ≡ χ›
using cond unfolding AOT_subst_cond_o_def by blast
ultimately AOT_show ‹\⊨\◻ φ{ψ} ≡ φ{χ}›
proof (induct arbitrary: ψ χ)
case AOT_subst_o_id
thus ?case
using "≡E"(2) "oth-class-taut:4:b" "rule-sub-lem:1:a" by blast
next
case (AOT_subst_o_const ψ)
thus ?case
by (simp add: "oth-class-taut:3:a")
next
case (AOT_subst_o_not Θ)
thus ?case
by (simp add: RN "rule-sub-lem:1:a")
next
case (AOT_subst_o_imp Θ Ξ)
thus ?case
by (meson RN "≡E"(5) "rule-sub-lem:1:b" "rule-sub-lem:1:c")
next
case (AOT_subst_o_lambda0 Θ)
thus ?case
by (simp add: RN "rule-sub-lem:1:e")
next
case (AOT_subst_o_act Θ)
thus ?case
by (simp add: RN "rule-sub-lem:1:f")
next
case (AOT_subst_o_box Θ)
thus ?case
by (simp add: RN "rule-sub-lem:1:g")
next
case (AOT_subst_o_by_def Θ Ξ)
AOT_modally_strict {
AOT_have ‹Ξ{ψ} ≡ Ξ{χ}›
using AOT_subst_o_by_def by simp
AOT_thus ‹Θ{ψ} ≡ Θ{χ}›
using "≡Df"[OF AOT_subst_o_by_def(1), of _ ψ]
"≡Df"[OF AOT_subst_o_by_def(1), of _ χ]
by (metis "≡E"(6) "oth-class-taut:3:a")
}
qed
"fun" :: (AOT_Term_id_2, AOT_subst) AOT_subst
AOT_subst_cond_fun :: ‹('a → 'b) → ('a → 'b) → bool› where
‹AOT_subst_cond_fun ≡ λ φ ψ . ∀ α . AOT_subst_cond (φ (AOT_term_of_var α))
(ψ (AOT_term_of_var α))›
AOT_subst_fun :: ‹(('a → 'b) → o) → bool› where
AOT_subst_fun_const[AOT_substI]:
‹AOT_subst_fun (λφ. ψ)›
| AOT_subst_fun_id[AOT_substI]:
‹AOT_subst Ψ ==> AOT_subst_fun (λφ. Ψ (φ (AOT_term_of_var α)))›
| AOT_subst_fun_all[AOT_substI]:
‹AOT_subst Ψ ==> (∧ α . AOT_subst_fun (Θ (AOT_term_of_var α))) ==>
AOT_subst_fun (λφ :: 'a → 'b. Ψ «∀α «Θ (α::'a) φ¬¬)›
| AOT_subst_fun_not[AOT_substI]:
‹AOT_subst Ψ ==> AOT_subst_fun (λφ. «¬«Ψ φ¬¬)›
| AOT_subst_fun_imp[AOT_substI]:
‹AOT_subst Ψ ==> AOT_subst Θ ==> AOT_subst_fun (λφ. ««Ψ φ¬ → «Θ φ¬¬)›
| AOT_subst_fun_lambda0[AOT_substI]:
‹AOT_subst Θ ==> AOT_subst_fun (λ φ. (AOT_lambda0 (Θ φ)))›
| AOT_subst_fun_act[AOT_substI]:
‹AOT_subst Θ ==> AOT_subst_fun (λ φ. «\A«Θ φ¬¬)›
| AOT_subst_fun_box[AOT_substI]:
‹AOT_subst Θ ==> AOT_subst_fun (λ φ. «◻«Θ φ¬¬)›
| AOT_subst_fun_def[AOT_substI]:
‹(∧ φ . AOT_model_equiv_def (Θ φ) (Ψ φ)) ==>
AOT_subst_fun Ψ ==> AOT_subst_fun Θ›
proof
fix ψ χ :: ‹'a → 'b› and φ :: ‹('a → 'b) → o›
assume ‹AOT_subst φ›
moreover assume cond: ‹AOT_subst_cond ψ χ›
ultimately AOT_show ‹\⊨\◻ «φ ψ¬ ≡ «φ χ¬›
proof(induct)
case (AOT_subst_fun_const ψ)
then show ?case by (simp add: "oth-class-taut:3:a")
next
case (AOT_subst_fun_id Ψ x)
then show ?case by (simp add: AOT_subst AOT_subst_cond_fun_def)
next
next
case (AOT_subst_fun_all Ψ Θ)
AOT_have ‹\⊨\◻ ◻(Θ{α, «ψ¬} ≡ Θ{α, «χ¬})› for α
using AOT_subst_fun_all.hyps(3) AOT_subst_fun_all.prems RN by presburger
thus ?case using AOT_subst[OF AOT_subst_fun_all(1)]
by (simp add: RN "rule-sub-lem:1:d"
AOT_subst_cond_fun_def AOT_subst_cond_o_def)
next
case (AOT_subst_fun_not Ψ)
then show ?case by (simp add: RN "rule-sub-lem:1:a")
next
case (AOT_subst_fun_imp Ψ Θ)
then show ?case
unfolding AOT_subst_cond_fun_def AOT_subst_cond_o_def
by (meson "≡E"(5) "oth-class-taut:4:c" "oth-class-taut:4:d" "→E")
next
case (AOT_subst_fun_lambda0 Θ)
then show ?case by (simp add: RN "rule-sub-lem:1:e")
next
case (AOT_subst_fun_act Θ)
then show ?case by (simp add: RN "rule-sub-lem:1:f")
next
case (AOT_subst_fun_box Θ)
then show ?case by (simp add: RN "rule-sub-lem:1:g")
next
case (AOT_subst_fun_def Θ Ψ)
then show ?case
by (meson "df-rules-formulas[3]" "df-rules-formulas[4]" "≡I" "≡E"(5))
qed
‹
prove_AOT_subst_tac ctxt = REPEAT (SUBGOAL (fn (trm,_) => let
fun findHeadConst (Const x) = SOME x
| findHeadConst (A $ _) = findHeadConst A
| findHeadConst _ = NONE
fun findDef (Const (const_name‹AOT_model_equiv_def›, _) $ lhs $ _)
= findHeadConst lhs
| findDef (A $ B) = (case findDef A of SOME x => SOME x | _ => findDef B)
| findDef (Abs (_,_,c)) = findDef c
| findDef _ = NONE
val const_opt = (findDef trm)
val defs = case const_opt of SOME const => List.filter (fn thm => let
val concl = Thm.concl_of thm
val thmconst = (findDef concl)
in case thmconst of SOME (c,_) => fst const = c | _ => false end)
(AOT_Definitions.get ctxt)
| _ => []
val tac = case defs of
[] => safe_step_tac (ctxt addSIs @{thms AOT_substI}) 1
| _ => resolve_tac ctxt defs 1
in tac end) 1)
getSubstThm ctxt reversed phi p q = let
p_ty = Term.type_of p
abs = HOLogic.mk_Trueprop (@{const AOT_subst(_)} $ phi)
abs = Syntax.check_term ctxt abs
substThm = Goal.prove ctxt [] [] abs
(fn {context=ctxt, prems=_} => prove_AOT_subst_tac ctxt)
substThm = substThm RS @{thm AOT_subst}
if reversed then let
val substThm = Drule.instantiate_normalize
(TVars.empty, Vars.make [((("χ", 0), p_ty), Thm.cterm_of ctxt p),
((("ψ", 0), p_ty), Thm.cterm_of ctxt q)]) substThm
val substThm = substThm RS @{thm "≡E"(1)}
in substThm end
let
val substThm = Drule.instantiate_normalize
(TVars.empty, Vars.make [((("ψ", 0), p_ty), Thm.cterm_of ctxt p),
((("χ", 0), p_ty), Thm.cterm_of ctxt q)]) substThm
val substThm = substThm RS @{thm "≡E"(2)}
in substThm end end
›
AOT_subst = ‹
.option (Scan.lift (Args.parens (Args.$$$ "reverse"))) --
.lift (Parse.embedded_inner_syntax -- Parse.embedded_inner_syntax) --
.option (Scan.lift (Args.$$$ "for" -- Args.colon) |--
.repeat1 (Scan.lift (Parse.embedded_inner_syntax) --
.option (Scan.lift (Args.$$$ "::" |-- Parse.embedded_inner_syntax))))
> (fn ((reversed,(raw_p,raw_q)),raw_bounds) => (fn ctxt =>
Method.SIMPLE_METHOD (Subgoal.FOCUS (fn {context = ctxt, params = _,
prems = prems, asms = asms, concl = concl, schematics = _} =>
thms = prems
ctxt' = ctxt
ctxt = Context_Position.set_visible false ctxt
raw_bounds = case raw_bounds of SOME bounds => bounds | _ => []
ctxt = (fold (fn (bound, ty) => fn ctxt =>
let
val bound = AOT_read_term @{nonterminal τ'} ctxt bound
val ty = Option.map (Syntax.read_typ ctxt) ty
val ctxt = case ty of SOME ty => let
val bound = Const ("_type_constraint_", Type ("fun", [ty,ty])) $ bound
val bound = Syntax.check_term ctxt bound
in Variable.declare_term bound ctxt end | _ => ctxt
in ctxt end)) raw_bounds ctxt
p = AOT_read_term @{nonterminal φ'} ctxt raw_p
p = Syntax.check_term ctxt p
ctxt = Variable.declare_term p ctxt
q = AOT_read_term @{nonterminal φ'} ctxt raw_q
q = Syntax.check_term ctxt q
ctxt = Variable.declare_term q ctxt
bounds = (map (fn (bound, _) =>
Syntax.check_term ctxt (AOT_read_term @{nonterminal τ'} ctxt bound)
) raw_bounds
p = fold (fn bound => fn p =>
Term.abs ("α", Term.type_of bound) (Term.abstract_over (bound,p)))
bounds p
p = Syntax.check_term ctxt p
p_ty = Term.type_of p
pat = @{const Trueprop} $
(@{const AOT_model_valid_in} $ Var (("w",0), @{typ w}) $
(Var (("φ",0), Type (type_name‹fun›, [p_ty, @{typ o}])) $ p))
univ = Unify.matchers (Context.Proof ctxt) [(pat, Thm.term_of concl)]
val univ = hd (Seq.list_of univ) (* TODO: consider all matches *)
val phi = the (Envir.lookup univ
(("φ",0), Type (type_name‹fun›, [p_ty, @{typ o}])))
val q = fold (fn bound => fn q =>
Term.abs ("α", Term.type_of bound) (Term.abstract_over (bound,q))) bounds q
val q = Syntax.check_term ctxt q
(* Reparse to report bounds as fixes. *)
val ctxt = Context_Position.restore_visible ctxt' ctxt
val ctxt' = ctxt
fun unsource str = fst (Input.source_content (Syntax.read_input str))
val (_,ctxt') = Proof_Context.add_fixes (map (fn (str,_) =>
(Binding.make (unsource str, Position.none), NONE, Mixfix.NoSyn)) raw_bounds)
ctxt'
val _ = (map (fn (x,_) =>
Syntax.check_term ctxt (AOT_read_term @{nonterminal τ'} ctxt' x)))
raw_bounds
val _ = AOT_read_term @{nonterminal φ'} ctxt' raw_p
val _ = AOT_read_term @{nonterminal \<phi>'} ctxt' raw_q
val reversed = case reversed of SOME _ => true | _ => false
val simpThms = [@{thm AOT_subst_cond_\<o>_def}, @{thm AOT_subst_cond_fun_def}]
in
resolve_tac ctxt [getSubstThm ctxt reversed phi p q] 1
THEN simp_tac (ctxt addsimps simpThms) 1
THEN (REPEAT (resolve_tac ctxt [@{thm allI}] 1))
THEN (TRY (resolve_tac ctxt thms 1))
end
) ctxt 1))))
\<close>
method_setup AOT_subst_def = \<open>
Scan.option (Scan.lift (Args.parens (Args.$$$ "reverse"))) --
Attrib.thm
>> (fn (reversed,fact) => (fn ctxt =>
(Method.SIMPLE_METHOD (Subgoal.FOCUS (fn {context = ctxt, params = _,
prems = prems, asms = asms, concl = concl, schematics = _} =>
let
val c = Thm.concl_of fact
val (lhs, rhs) = case c of (\<^const>\<open>Trueprop\<close> $
(\<^const>\<open>AOT_model_equiv_def\<close> $ lhs $ rhs)) => (lhs, rhs)
| _ => raise Fail "Definition expected."
val substCond = HOLogic.mk_Trueprop
(Const (\<^const_name>\<open>AOT_subst_cond\<close>, dummyT) $ lhs $ rhs)
val substCond = Syntax.check_term
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
substCond
val simpThms = [@{thm AOT_subst_cond_\<o>_def},
@{thm AOT_subst_cond_fun_def},
fact RS @{thm "\<equiv>Df"}]
val substCondThm = Goal.prove ctxt [] [] substCond
(fn {context=ctxt, prems=prems} =>
(SUBGOAL (fn (trm,int) =>
auto_tac (ctxt addsimps simpThms)) 1))
val substThm = substCondThm RSN (2,@{thm AOT_subst})
in
resolve_tac ctxt [substThm RS
(case reversed of NONE => @{thm "\<equiv>E"(2)} | _ => @{thm "\<equiv>E"(1)})] 1
THEN prove_AOT_subst_tac ctxt
THEN (TRY (resolve_tac ctxt prems 1))
end
) ctxt 1))))
\<close>
method_setup AOT_subst_thm = \<open>
Scan.option (Scan.lift (Args.parens (Args.$$$ "reverse"))) --
Attrib.thm
>> (fn (reversed,fact) => (fn ctxt =>
(Method.SIMPLE_METHOD (Subgoal.FOCUS (fn {context = ctxt, params = _,
prems = prems, asms = asms, concl = concl, schematics = _} =>
let
val c = Thm.concl_of fact
val (lhs, rhs) = case c of
(\<^const>\<open>Trueprop\<close> $
(\<^const>\<open>AOT_model_valid_in\<close> $ _ $
(\<^const>\<open>AOT_equiv\<close> $ lhs $ rhs))) => (lhs, rhs)
| _ => raise Fail "Equivalence expected."
val substCond = HOLogic.mk_Trueprop
(Const (\<^const_name>\<open>AOT_subst_cond\<close>, dummyT) $ lhs $ rhs)
val substCond = Syntax.check_term
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
substCond
val simpThms = [@{thm AOT_subst_cond_\<o>_def},
@{thm AOT_subst_cond_fun_def},
fact]
val substCondThm = Goal.prove ctxt [] [] substCond
(fn {context=ctxt, prems=prems} =>
(SUBGOAL (fn (trm,int) => auto_tac (ctxt addsimps simpThms)) 1))
val substThm = substCondThm RSN (2,@{thm AOT_subst})
in
resolve_tac ctxt [substThm RS
(case reversed of NONE => @{thm "\<equiv>E"(2)} | _ => @{thm "\<equiv>E"(1)})] 1
THEN prove_AOT_subst_tac ctxt
THEN (TRY (resolve_tac ctxt prems 1))
end
) ctxt 1))))
\<close>
AOT_theorem "rule-sub-remark:1[1]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> A!x \<equiv> \<not>\<diamond>E!x\<close> and \<open>\<not>A!x\<close>
shows \<open>\<not>\<not>\<diamond>E!x\<close>
by (AOT_subst (reverse) \<open>\<not>\<diamond>E!x\<close> \<open>A!x\<close>)
(auto simp: assms)
AOT_theorem "rule-sub-remark:1[2]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> A!x \<equiv> \<not>\<diamond>E!x\<close> and \<open>\<not>\<not>\<diamond>E!x\<close>
shows \<open>\<not>A!x\<close>
by (AOT_subst \<open>A!x\<close> \<open>\<not>\<diamond>E!x\<close>)
(auto simp: assms)
AOT_theorem "rule-sub-remark:2[1]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> [R]xy \<equiv> ([R]xy & ([Q]a \<or> \<not>[Q]a))\<close>
and \<open>p \<rightarrow> [R]xy\<close>
shows \<open>p \<rightarrow> [R]xy & ([Q]a \<or> \<not>[Q]a)\<close>
by (AOT_subst_thm (reverse) assms(1)) (simp add: assms(2))
AOT_theorem "rule-sub-remark:2[2]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> [R]xy \<equiv> ([R]xy & ([Q]a \<or> \<not>[Q]a))\<close>
and \<open>p \<rightarrow> [R]xy & ([Q]a \<or> \<not>[Q]a)\<close>
shows \<open>p \<rightarrow> [R]xy\<close>
by (AOT_subst_thm assms(1)) (simp add: assms(2))
AOT_theorem "rule-sub-remark:3[1]":
assumes \<open>for arbitrary x: \<^bold>\<turnstile>\<^sub>\<box> A!x \<equiv> \<not>\<diamond>E!x\<close>
and \<open>\<exists>x A!x\<close>
shows \<open>\<exists>x \<not>\<diamond>E!x\<close>
by (AOT_subst (reverse) \<open>\<not>\<diamond>E!x\<close> \<open>A!x\<close> for: x)
(auto simp: assms)
AOT_theorem "rule-sub-remark:3[2]":
assumes \<open>for arbitrary x: \<^bold>\<turnstile>\<^sub>\<box> A!x \<equiv> \<not>\<diamond>E!x\<close>
and \<open>\<exists>x \<not>\<diamond>E!x\<close>
shows \<open>\<exists>x A!x\<close>
by (AOT_subst \<open>A!x\<close> \<open>\<not>\<diamond>E!x\<close> for: x)
(auto simp: assms)
AOT_theorem "rule-sub-remark:4[1]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> \<not>\<not>[P]x \<equiv> [P]x\<close> and \<open>\<^bold>\<A>\<not>\<not>[P]x\<close>
shows \<open>\<^bold>\<A>[P]x\<close>
by (AOT_subst_thm (reverse) assms(1)) (simp add: assms(2))
AOT_theorem "rule-sub-remark:4[2]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> \<not>\<not>[P]x \<equiv> [P]x\<close> and \<open>\<^bold>\<A>[P]x\<close>
shows \<open>\<^bold>\<A>\<not>\<not>[P]x\<close>
by (AOT_subst_thm assms(1)) (simp add: assms(2))
AOT_theorem "rule-sub-remark:5[1]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> (\<phi> \<rightarrow> \<psi>) \<equiv> (\<not>\<psi> \<rightarrow> \<not>\<phi>)\<close> and \<open>\<box>(\<phi> \<rightarrow> \<psi>)\<close>
shows \<open>\<box>(\<not>\<psi> \<rightarrow> \<not>\<phi>)\<close>
by (AOT_subst_thm (reverse) assms(1)) (simp add: assms(2))
AOT_theorem "rule-sub-remark:5[2]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> (\<phi> \<rightarrow> \<psi>) \<equiv> (\<not>\<psi> \<rightarrow> \<not>\<phi>)\<close> and \<open>\<box>(\<not>\<psi> \<rightarrow> \<not>\<phi>)\<close>
shows \<open>\<box>(\<phi> \<rightarrow> \<psi>)\<close>
by (AOT_subst_thm assms(1)) (simp add: assms(2))
AOT_theorem "rule-sub-remark:6[1]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> \<psi> \<equiv> \<chi>\<close> and \<open>\<box>(\<phi> \<rightarrow> \<psi>)\<close>
shows \<open>\<box>(\<phi> \<rightarrow> \<chi>)\<close>
by (AOT_subst_thm (reverse) assms(1)) (simp add: assms(2))
AOT_theorem "rule-sub-remark:6[2]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> \<psi> \<equiv> \<chi>\<close> and \<open>\<box>(\<phi> \<rightarrow> \<chi>)\<close>
shows \<open>\<box>(\<phi> \<rightarrow> \<psi>)\<close>
by (AOT_subst_thm assms(1)) (simp add: assms(2))
AOT_theorem "rule-sub-remark:7[1]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> \<phi> \<equiv> \<not>\<not>\<phi>\<close> and \<open>\<box>(\<phi> \<rightarrow> \<phi>)\<close>
shows \<open>\<box>(\<not>\<not>\<phi> \<rightarrow> \<phi>)\<close>
by (AOT_subst_thm (reverse) assms(1)) (simp add: assms(2))
AOT_theorem "rule-sub-remark:7[2]":
assumes \<open>\<^bold>\<turnstile>\<^sub>\<box> \<phi> \<equiv> \<not>\<not>\<phi>\<close> and \<open>\<box>(\<not>\<not>\<phi> \<rightarrow> \<phi>)\<close>
shows \<open>\<box>(\<phi> \<rightarrow> \<phi>)\<close>
by (AOT_subst_thm assms(1)) (simp add: assms(2))
AOT_theorem "KBasic2:1": \<open>\<box>\<not>\<phi> \<equiv> \<not>\<diamond>\<phi>\<close>
by (meson "conventions:5" "contraposition:2"
"Hypothetical Syllogism" "df-rules-formulas[3]"
"df-rules-formulas[4]" "\<equiv>I" "useful-tautologies:1")
AOT_theorem "KBasic2:2": \<open>\<diamond>(\<phi> \<or> \<psi>) \<equiv> (\<diamond>\<phi> \<or> \<diamond>\<psi>)\<close>
proof -
AOT_have \<open>\<diamond>(\<phi> \<or> \<psi>) \<equiv> \<diamond>\<not>(\<not>\<phi> & \<not>\<psi>)\<close>
by (simp add: "RE\<diamond>" "oth-class-taut:5:b")
also AOT_have \<open>\<dots> \<equiv> \<not>\<box>(\<not>\<phi> & \<not>\<psi>)\<close>
using "KBasic:11" "\<equiv>E"(6) "oth-class-taut:3:a" by blast
also AOT_have \<open>\<dots> \<equiv> \<not>(\<box>\<not>\<phi> & \<box>\<not>\<psi>)\<close>
using "KBasic:3" "\<equiv>E"(1) "oth-class-taut:4:b" by blast
also AOT_have \<open>\<dots> \<equiv> \<not>(\<not>\<diamond>\<phi> & \<not>\<diamond>\<psi>)\<close>
using "KBasic2:1"
by (AOT_subst \<open>\<box>\<not>\<phi>\<close> \<open>\<not>\<diamond>\<phi>\<close>; AOT_subst \<open>\<box>\<not>\<psi>\<close> \<open>\<not>\<diamond>\<psi>\<close>;
auto simp: "oth-class-taut:3:a")
also AOT_have \<open>\<dots> \<equiv> \<not>\<not>(\<diamond>\<phi> \<or> \<diamond>\<psi>)\<close>
using "\<equiv>E"(6) "oth-class-taut:3:b" "oth-class-taut:5:b" by blast
also AOT_have \<open>\<dots> \<equiv> \<diamond>\<phi> \<or> \<diamond>\<psi>\<close>
by (simp add: "\<equiv>I" "useful-tautologies:1" "useful-tautologies:2")
finally show ?thesis .
qed
AOT_theorem "KBasic2:3": \<open>\<diamond>(\<phi> & \<psi>) \<rightarrow> (\<diamond>\<phi> & \<diamond>\<psi>)\<close>
by (metis "RM\<diamond>" "&I" "Conjunction Simplification"(1,2)
"\<rightarrow>I" "modus-tollens:1" "reductio-aa:1")
AOT_theorem "KBasic2:4": \<open>\<diamond>(\<phi> \<rightarrow> \<psi>) \<equiv> (\<box>\<phi> \<rightarrow> \<diamond>\<psi>)\<close>
proof -
AOT_have \<open>\<diamond>(\<phi> \<rightarrow> \<psi>) \<equiv> \<diamond>(\<not>\<phi> \<or> \<psi>)\<close>
by (AOT_subst \<open>\<phi> \<rightarrow> \<psi>\<close> \<open>\<not>\<phi> \<or> \<psi>\<close>)
(auto simp: "oth-class-taut:1:c" "oth-class-taut:3:a")
also AOT_have \<open>... \<equiv> \<diamond>\<not>\<phi> \<or> \<diamond>\<psi>\<close>
by (simp add: "KBasic2:2")
also AOT_have \<open>... \<equiv> \<not>\<box>\<phi> \<or> \<diamond>\<psi>\<close>
by (AOT_subst \<open>\<not>\<box>\<phi>\<close> \<open>\<diamond>\<not>\<phi>\<close>)
(auto simp: "KBasic:11" "oth-class-taut:3:a")
also AOT_have \<open>... \<equiv> \<box>\<phi> \<rightarrow> \<diamond>\<psi>\<close>
using "\<equiv>E"(6) "oth-class-taut:1:c" "oth-class-taut:3:a" by blast
finally show ?thesis .
qed
AOT_theorem "KBasic2:5": \<open>\<diamond>\<diamond>\<phi> \<equiv> \<not>\<box>\<box>\<not>\<phi>\<close>
using "conventions:5"[THEN "\<equiv>Df"]
by (AOT_subst \<open>\<diamond>\<phi>\<close> \<open>\<not>\<box>\<not>\<phi>\<close>;
AOT_subst \<open>\<diamond>\<not>\<box>\<not>\<phi>\<close> \<open>\<not>\<box>\<not>\<not>\<box>\<not>\<phi>\<close>;
()\open><ot\not\<box><><>\<close>\open><ox>\not>\phi\<>
bch_inode_unpacked
AOT_theorem "KBasic2:6": \<open>\<box>(\<phi> \<or> \<psi>) \<rightarrow> (\<box>\<phi> \<or> \<diamond>\<psi>)\<close>
proof(rule "\<rightarrow>I"; rule "raa-cor:1")
AOT_assume \<open>\<box>(\<phi> \<or> \<psi>)\<close>
AOT_hence \<open>\<box>(\<not>\<phi> \<rightarrow> \<psi>)\<close>
using "conventions:2"[THEN "\<equiv>Df"]
by (AOT_subst (reverse) \<open>\<not>\<phi> \<rightarrow> \<psi>\<close> \<open>\<phi> \<or> \<psi>\<close>) simp
AOT_hence 1: \<open>\<diamond>\<not>\<phi> \<rightarrow> \<diamond>\<psi>\<close>
using "KBasic:13" "vdash-properties:10" by blast
AOT_assume \<open>\<not>(\<box>\<phi> \<or> \<diamond>\<psi>)\<close>
AOT_hence \<open>\<not>\<box>\<phi>\<close> and \<open>\<not>\<diamond>\<psi>\<close>
using "&E" "\<equiv>E"(1) "oth-class-taut:5:d" by blast+
AOT_thus \<open>\<diamond>\<psi> & \<not>\<diamond>\<psi>\<close>
using "&I"(1) 1[THEN "\<rightarrow>E"] "KBasic:11" "\<equiv>E"(4) "raa-cor:3" by blast
qed
AOT_theorem "KBasic2:7": \<open>(\<box>(\<phi> \<or> \<psi>) & \<diamond>\<not>\<phi>) \<rightarrow> \<diamond>\<psi>\<close>
proof(rule "\<rightarrow>I"; frule "&E"(1); drule "&E"(2))
AOT_assume \<open>\<box>(\<phi> \<or> \<psi>)\<close>
AOT_hence 1: \<open>\<box>\<phi> \<or> \<diamond>\<psi>\<close>
using "KBasic2:6" "\<or>I"(2) "\<or>E"(1) by blast
AOT_assume \<open>\<diamond>\<not>\<phi>\<close>
AOT_hence \<open>\<not>\<box>\<phi>\<close> using "KBasic:11" "\<equiv>E"(2) by blast
AOT_thus \<open>\<diamond>\<psi>\<close> using 1 "\<or>E"(2) by blast
qed
AOT_theorem "T-S5-fund:1": \<open>\<phi> \<rightarrow> \<diamond>\<phi>\<close>
by (meson "\<equiv>\<^sub>d\<^sub>fI" "conventions:5" "contraposition:2"
"Hypothetical Syllogism" "\<rightarrow>I" "qml:2"[axiom_inst])
lemmas "T\<diamond>" = "T-S5-fund:1"
AOT_theorem "T-S5-fund:2": \<open>\<diamond>\<box>\<phi> \<rightarrow> \<box>\<phi>\<close>
proof(rule "\<rightarrow>I")
AOT_assume \<open>\<diamond>\<box>\<phi>\<close>
AOT_hence \<open>\<not>\<box>\<diamond>\<not>\<phi>\<close>
using "KBasic:14" "\<equiv>E"(4) "raa-cor:3" by blast
moreover AOT_have \<open>\<diamond>\<not>\<phi> \<rightarrow> \<box>\<diamond>\<not>\<phi>\<close>
by (fact "qml:3"[axiom_inst])
ultimately AOT_have \<open>\<not>\<diamond>\<not>\<phi>\<close>
using "modus-tollens:1" by blast
AOT_thus \<open>\<box>\<phi>\<close> using "KBasic:12" "\<equiv>E"(2) by blast
qed
lemmas "5\<diamond>" = "T-S5-fund:2"
AOT_theorem "Act-Sub:1": \<open>\<^bold>\<A>\<phi> \<equiv> \<not>\<^bold>\<A>\<not>\<phi>\<close>
by (AOT_subst \<open>\<^bold>\<A>\<not>\<phi>\<close> \<open>\<not>\<^bold>\<A>\<phi>\<close>)
(auto simp: "logic-actual-nec:1"[axiom_inst] "oth-class-taut:3:b")
AOT_theorem "Act-Sub:2": \<open>\<diamond>\<phi> \<equiv> \<^bold>\<A>\<diamond>\<phi>\<close>
using "conventions:5"[THEN "\<equiv>Df"]
by (AOT_subst \<open>\<diamond>\<phi>\<close> \<open>\<not>\<box>\<not>\<phi>\<close>)
(metis "deduction-theorem" "\<equiv>I" "\<equiv>E"(1) "\<equiv>E"(2) "\<equiv>E"(3)
"logic-actual-nec:1"[axiom_inst] "qml-act:2"[axiom_inst])
AOT_theorem "Act-Sub:3": \<open>\<^bold>\<A>\<phi> \<rightarrow> \<diamond>\<phi>\<close>
using "conventions:5"[THEN "\<equiv>Df"]
by (AOT_subst \<open>\<diamond>\<phi>\<close> \<open>\<not>\<box>\<not>\<phi>\<close>)
(metis "Act-Sub:1" "\<rightarrow>I" "\<equiv>E"(4) "nec-imp-act" "reductio-aa:2" "\<rightarrow>E")
AOT_theorem "Act-Sub:4": \<open>\<^bold>\<A>\<phi> \<equiv> \<diamond>\<^bold>\<A>\<phi>\<close>
proof (rule "\<equiv>I"; rule "\<rightarrow>I")
AOT_assume \<open>\<^bold>\<A>\<phi>\<close>
AOT_thus \<open>\<diamond>\<^bold>\<A>\<phi>\<close> using "T\<diamond>" "vdash-properties:10" by blast
next
AOT_assume \<open>\<diamond>\<^bold>\<A>\<phi>\<close>
AOT_hence \<open>\<not>\<box>\<not>\<^bold>\<A>\<phi>\<close>
using "\<equiv>\<^sub>d\<^sub>fE" "conventions:5" by blast
AOT_hence \<open>\<not>\<box>\<^bold>\<A>\<not>\<phi>\<close>
by (AOT_subst \<open>\<^bold>\<A>\<not>\<phi>\<close> \<open>\<not>\<^bold>\<A>\<phi>\<close>)
(simp add: "logic-actual-nec:1"[axiom_inst])
AOT_thus \<open>\<^bold>\<A>\<phi>\<close>
using "Act-Basic:1" "Act-Basic:6" "\<or>E"(3) "\<equiv>E"(4)
"reductio-aa:1" by blast
qed
AOT_theorem "Act-Sub:5": \<open>\<diamond>\<^bold>\<A>\<phi> \<rightarrow> \<^bold>\<A>\<diamond>\<phi>\<close>
by (metis "Act-Sub:2" "Act-Sub:3" "Act-Sub:4" "\<rightarrow>I" "\<equiv>E"(1) "\<equiv>E"(2) "\<rightarrow>E")
AOT_theorem "S5Basic:1": \<open>\<diamond>\<phi> \<equiv> \<box>\<diamond>\<phi>\<close>
by (simp add: "\<equiv>I" "qml:2"[axiom_inst] "qml:3"[axiom_inst])
AOT_theorem "S5Basic:2": \<open>\<box>\<phi> \<equiv> \<diamond>\<box>\<phi>\<close>
by (simp add: "T\<diamond>" "5\<diamond>" "\<equiv>I")
AOT_theorem "S5Basic:3": \<open>\<phi> \<rightarrow> \<box>\<diamond>\<phi>\<close>
using "T\<diamond>" "Hypothetical Syllogism" "qml:3"[axiom_inst] by blast
lemmas "B" = "S5Basic:3"
AOT_theorem "S5Basic:4": \<open>\<diamond>\<box>\<phi> \<rightarrow> \<phi>\<close>
using "5\<diamond>" "Hypothetical Syllogism" "qml:2"[axiom_inst] by blast
lemmas "B\<diamond>" = "S5Basic:4"
AOT_theorem "S5Basic:5": \<open>\<box>\<phi> \<rightarrow> \<box>\<box>\<phi>\<close>
using "RM:1" "B" "5\<diamond>" "Hypothetical Syllogism" by blast
lemmas "4" = "S5Basic:5"
AOT_theorem "S5Basic:6": \<open>\<box>\<phi> \<equiv> \<box>\<box>\<phi>\<close>
by (simp add: "4" "\<equiv>I" "qml:2"[axiom_inst])
AOT_theorem "S5Basic:7": \<open>\<diamond>\<diamond>\<phi> \<rightarrow> \<diamond>\<phi>\<close>
using "conventions:5"[THEN "\<equiv>Df"] "oth-class-taut:3:b"
by (AOT_subst \<open>\<diamond>\<diamond>\<phi>\<close> \<open>\<not>\<box>\<not>\<diamond>\<phi>\<close>;
AOT_subst \<open>\<diamond>\<phi>\<close> \<open>\<not>\<box>\<not>\<phi>\<close>;
AOT_subst (reverse) \<open>\<not>\<not>\<box>\<not>\<phi>\<close> \<open>\<box>\<not>\<phi>\<close>;
AOT_subst (reverse) \<open>\<box>\<box>\<not>\<phi>\<close> \<open>\<box>\<not>\<phi>\<close>)
(auto simp: "S5Basic:6" "if-p-then-p")
lemmas "4\<diamond>" = "S5Basic:7"
AOT_theorem "S5Basic:8": \<open>\<diamond>\<diamond>\<phi> \<equiv> \<diamond>\<phi>\<close>
by (simp add: "4\<diamond>" "T\<diamond>" "\<equiv>I")
AOT_theorem "S5Basic:9": \<open>\<box>(\<phi> \<or> \<box>\<psi>) \<equiv> (\<box>\<phi> \<or> \<box>\<psi>)\<close>
apply (rule "\<equiv>I"; rule "\<rightarrow>I")
using "KBasic2:6" "5\<diamond>" "\<or>I"(3) "if-p-then-p" "vdash-properties:10"
apply blast
by (meson "KBasic:15" "4" "\<or>I"(3) "\<or>E"(1) "Disjunction Addition"(1)
"con-dis-taut:7" "intro-elim:1" "Commutativity of \<or>")
AOT_theorem "S5Basic:10": \<open>\<box>(\<phi> \<or> \<diamond>\<psi>) \<equiv> (\<box>\<phi> \<or> \<diamond>\<psi>)\<close>
proof(rule "\<equiv>I"; rule "\<rightarrow>I")
AOT_assume \<open>\<box>(\<phi> \<or> \<diamond>\<psi>)\<close>
AOT_hence \<open>\<box>\<phi> \<or> \<diamond>\<diamond>\<psi>\<close>
by (meson "KBasic2:6" "\<or>I"(2) "\<or>E"(1))
AOT_thus \<open>\<box>\<phi> \<or> \<diamond>\<psi>\<close>
by (meson "B\<diamond>" "4" "4\<diamond>" "T\<diamond>" "\<or>I"(3))
next
AOT_assume \<open>\<box>\<phi> \<or> \<diamond>\<psi>\<close>
AOT_hence \<open>\<box>\<phi> \<or> \<box>\<diamond>\<psi>\<close>
by (meson "S5Basic:1" "B\<diamond>" "S5Basic:6" "T\<diamond>" "5\<diamond>" "\<or>I"(3) "intro-elim:1")
AOT_thus \<open>\<box>(\<phi> \<or> \<diamond>\<psi>)\<close>
by (meson "KBasic:15" "\<or>I"(3) "\<or>E"(1) "Disjunction Addition"(1,2))
qed
AOT_theorem "S5Basic:11": \<open>\<diamond>(\<phi> & \<diamond>\<psi>) \<equiv> (\<diamond>\<phi> & \<diamond>\<psi>)\<close>
proof -
AOT_have \<open>\<diamond>(\<phi> & \<diamond>\<psi>) \<equiv> \<diamond>\<not>(\<not>\<phi> \<or> \<not>\<diamond>\<psi>)\<close>
by (AOT_subst \<open>\<phi> & \<diamond>\<psi>\<close> \<open>\<not>(\<not>\<phi> \<or> \<not>\<diamond>\<psi>)\<close>)
(auto simp: "oth-class-taut:5:a" "oth-class-taut:3:a")
also AOT_have \<open>\<dots> \<equiv> \<diamond>\<not>(\<not>\<phi> \<or> \<box>\<not>\<psi>)\<close>
by (AOT_subst \<open>\<box>\<not>\<psi>\<close> \<open>\<not>\<diamond>\<psi>\<close>)
(auto simp: "KBasic2:1" "oth-class-taut:3:a")
also AOT_have \<open>\<dots> \<equiv> \<not>\<box>(\<not>\<phi> \<or> \<box>\<not>\<psi>)\<close>
using "KBasic:11" "\<equiv>E"(6) "oth-class-taut:3:a" by blast
also AOT_have \<open>\<dots> \<equiv> \<not>(\<box>\<not>\<phi> \<or> \<box>\<not>\<psi>)\<close>
using "S5Basic:9" "\<equiv>E"(1) "oth-class-taut:4:b" by blast
also AOT_have \<open>\<dots> \<equiv> \<not>(\<not>\<diamond>\<phi> \<or> \<not>\<diamond>\<psi>)\<close>
using "KBasic2:1"
by (AOT_subst \<open>\<box>\<not>\<phi>\<close> \<open>\<not>\<diamond>\<phi>\<close>; AOT_subst \<open>\<box>\<not>\<psi>\<close> \<open>\<not>\<diamond>\<psi>\<close>)
(auto simp: "oth-class-taut:3:a")
also AOT_have \<open>\<dots> \<equiv> \<diamond>\<phi> & \<diamond>\<psi>\<close>
using "\<equiv>E"(6) "oth-class-taut:3:a" "oth-class-taut:5:a" by blast
finally show ?thesis .
qed
AOT_theorem "S5Basic:12": \<open>\<diamond>(\<phi> & \<box>\<psi>) \<equiv> (\<diamond>\<phi> & \<box>\<psi>)\<close>
proof (rule "\<equiv>I"; rule "\<rightarrow>I")
AOT_assume \<open>\<diamond>(\<phi> & \<box>\<psi>)\<close>
AOT_hence \<open>\<diamond>\<phi> & \<diamond>\<box>\<psi>\<close>
using "KBasic2:3" "vdash-properties:6" by blast
AOT_thus \<open>\<diamond>\<phi> & \<box>\<psi>\<close>
using "5\<diamond>" "&I" "&E"(1) "&E"(2) "vdash-properties:6" by blast
next
AOT_assume \<open>\<diamond>\<phi> & \<box>\<psi>\<close>
moreover AOT_have \<open>(\<box>\<box>\<psi> & \<diamond>\<phi>) \<rightarrow> \<diamond>(\<phi> & \<box>\<psi>)\<close>
by (AOT_subst \<open>\<phi> & \<box>\<psi>\<close> \<open>\<box>\<psi> & \<phi>\<close>)
(auto simp: "Commutativity of &" "KBasic:16")
ultimately AOT_show \<open>\<diamond>(\<phi> & \<box>\<psi>)\<close>
by (metis "4" "&I" "Conjunction Simplification"(1,2) "\<rightarrow>E")
qed
AOT_theorem "S5Basic:13": \<open>\<box>(\<phi> \<rightarrow> \<box>\<psi>) \<equiv> \<box>(\<diamond>\<phi> \<rightarrow> \<psi>)\<close>
proof (rule "\<equiv>I")
AOT_modally_strict {
AOT_have \<open>\<box>(\<phi> \<rightarrow> \<box>\<psi>) \<rightarrow> (\<diamond>\<phi> \<rightarrow> \<psi>)\<close>
by (meson "KBasic:13" "B\<diamond>" "Hypothetical Syllogism" "\<rightarrow>I")
}
AOT_hence \<open>\<box>\<box>(\<phi> \<rightarrow> \<box>\<psi>) \<rightarrow> \<box>(\<diamond>\<phi> \<rightarrow> \<psi>)\<close>
by (rule RM)
AOT_thus \<open>\<box>(\<phi> \<rightarrow> \<box>\<psi>) \<rightarrow> \<box>(\<diamond>\<phi> \<rightarrow> \<psi>)\<close>
using "4" "Hypothetical Syllogism" by blast
next
AOT_modally_strict {
AOT_have \<open>\<box>(\<diamond>\<phi> \<rightarrow> \<psi>) \<rightarrow> (\<phi> \<rightarrow> \<box>\<psi>)\<close>
by (meson "B" "Hypothetical Syllogism" "\<rightarrow>I" "qml:1"[axiom_inst])
}
AOT_hence \<open>\<box>\<box>(\<diamond>\<phi> \<rightarrow> \<psi>) \<rightarrow> \<box>(\<phi> \<rightarrow> \<box>\<psi>)\<close>
by (rule RM)
AOT_thus \<open>\<box>(\<diamond>\<phi> \<rightarrow> \<psi>) \<rightarrow> \<box>(\<phi> \<rightarrow> \<box>\<psi>)\<close>
using "4" "Hypothetical Syllogism" by blast
qed
AOT_theorem "derived-S5-rules:1":
assumes \<open>\<Gamma> \<^bold>\<turnstile>\<^sub>\<box> \<diamond>\<phi> \<rightarrow> \<psi>\<close>
shows \<open>\<box>\<Gamma> \<^bold>\<turnstile>\<^sub>\<box> \<phi> \<rightarrow> \<box>\<psi>\<close>
proof -
AOT_have \<open>\<box>\<Gamma> \<^bold>\<turnstile>\<^sub>\<box> \<box>\<diamond>\<phi> \<rightarrow> \<box>\<psi>\<close>
using assms by (rule "RM:1[prem]")
AOT_thus \<open>\<box>\<Gamma> \<^bold>\<turnstile>\<^sub>\<box> \<phi> \<rightarrow> \<box>\<psi>\<close>
using "B" "Hypothetical Syllogism" by blast
qed
AOT_theorem "derived-S5-rules:2":
assumes \<open>\<Gamma> \<^bold>\<turnstile>\<^sub>\<box> \<phi> \<rightarrow> \<box>\<psi>\<close>
shows \<open>\<box>\<Gamma> \<^bold>\<turnstile>\<^sub>\<box> \<diamond>\<phi> \<rightarrow> \<psi>\<close>
proof -
AOT_have \<open>\<box>\<Gamma> \<^bold>\<turnstile>\<^sub>\<box> \<diamond>\<phi> \<rightarrow> \<diamond>\<box>\<psi>\<close>
using assms by (rule "RM:2[prem]")
AOT_thus \<open>\<box>\<Gamma> \<^bold>\<turnstile>\<^sub>\<box> \<diamond>\<phi> \<rightarrow> \<psi>\<close>
using "B\<diamond>" "Hypothetical Syllogism" by blast
qed
AOT_theorem "BFs:1": \<open>\<forall>\<alpha> \<box>\<phi>{\<alpha>} \<rightarrow> \<box>\<forall>\<alpha> \<phi>{\<alpha>}\<close>
proof -
AOT_modally_strict {
AOT_have \<open>\<diamond>\<forall>\<alpha> \<box>\<phi>{\<alpha>} \<rightarrow> \<diamond>\<box>\<phi>{\<alpha>}\<close> for \<alpha>
using "cqt-orig:3" by (rule "RM\<diamond>")
AOT_hence \<open>\<diamond>\<forall>\<alpha> \<box>\<phi>{\<alpha>} \<rightarrow> \<forall>\<alpha> \<phi>{\<alpha>}\<close>
using "B\<diamond>" "\<forall>I" "\<rightarrow>E" "\<rightarrow>I" by metis
}
thus ?thesis
using "derived-S5-rules:1" by blast
qed
lemmas "BF" = "BFs:1"
AOT_theorem "BFs:2": \<open>\<box>\<forall>\<alpha> \<phi>{\<alpha>} \<rightarrow> \<forall>\<alpha> \<box>\<phi>{\<alpha>}\<close>
proof -
AOT_have \<open>\<box>\<forall>\<alpha> \<phi>{\<alpha>} \<rightarrow> \<box>\<phi>{\<alpha>}\<close> for \<alpha>
using RM "cqt-orig:3" by metis
thus ?thesis
using "cqt-orig:2"[THEN "\<rightarrow>E"] "\<forall>I" by metis
qed
lemmas "CBF" = "BFs:2"
AOT_theorem "BFs:3": \<open>\<diamond>\<exists>\<alpha> \<phi>{\<alpha>} \<rightarrow> \<exists>\<alpha> \<diamond>\<phi>{\<alpha>}\<close>
proof(rule "\<rightarrow>I")
AOT_modally_strict {
AOT_have \<open>\<box>\<forall>\<alpha> \<not>\<phi>{\<alpha>} \<equiv> \<forall>\<alpha> \<box>\<not>\<phi>{\<alpha>}\<close>
using BF CBF "\<equiv>I" by blast
} note \<theta> = this
AOT_assume \<open>\<diamond>\<exists>\<alpha> \<phi>{\<alpha>}\<close>
AOT_hence \<open>\<not>\<box>\<not>(\<exists>\<alpha> \<phi>{\<alpha>})\<close>
using "\<equiv>\<^sub>d\<^sub>fE" "conventions:5" by blast
AOT_hence \<open>\<not>\<box>\<forall>\<alpha> \<not>\<phi>{\<alpha>}\<close>
apply (AOT_subst \<open>\<forall>\<alpha> \<not>\<phi>{\<alpha>}\<close> \<open>\<not>(\<exists>\<alpha> \<phi>{\<alpha>})\<close>)
using "\<equiv>\<^sub>d\<^sub>fI" "conventions:3" "conventions:4" "&I"
"contraposition:2" "cqt-further:4"
"df-rules-formulas[3]" by blast
AOT_hence \<open>\<not>\<forall>\<alpha> \<box>\<not>\<phi>{\<alpha>}\<close>
apply (AOT_subst (reverse) \<open>\<forall>\<alpha> \<box>\<not>\<phi>{\<alpha>}\<close> \<open>\<box>\<forall>\<alpha> \<not>\<phi>{\<alpha>}\<close>)
using \<theta> by blast
AOT_hence \<open>\<not>\<forall>\<alpha> \<not>\<not>\<box>\<not>\<phi>{\<alpha>}\<close>
by (AOT_subst (reverse) \<open>\<not>\<not>\<box>\<not>\<phi>{\<alpha>}\<close> \<open>\<box>\<not>\<phi>{\<alpha>}\<close> for: \<alpha>)
(simp add: "oth-class-taut:3:b")
AOT_hence \<open>\<exists>\<alpha> \<not>\<box>\<not>\<phi>{\<alpha>}\<close>
by (rule "conventions:4"[THEN "\<equiv>\<^sub>d\<^sub>fI"])
AOT_thus \<open>\<exists>\<alpha> \<diamond>\<phi>{\<alpha>}\<close>
using "conventions:5"[THEN "\<equiv>Df"]
by (AOT_subst \<open>\<diamond>\<phi>{\<alpha>}\<close> \<open>\<not>\<box>\<not>\<phi>{\<alpha>}\<close> for: \<alpha>)
qed
lemmas "BF\<diamond>" = "BFs:3"
AOT_theorem "BFs:4": \<open>\<exists>\<alpha> \<diamond>\<phi>{\<alpha>} \<rightarrow> \<diamond>\<exists>\<alpha> \<phi>{\<alpha>}\<close>
proof(rule "\<rightarrow>I")
AOT_assume \<open>\<exists>\<alpha> \<diamond>\<phi>{\<alpha>}\<close>
AOT_hence \<open>\<not>\<forall>\<alpha> \<not>\<diamond>\<phi>{\<alpha>}\<close>
using "conventions:4"[THEN "\<equiv>\<^sub>d\<^sub>fE"] by blast
AOT_hence \<open>\<not>\<forall>\<alpha> \<box>\<not>\<phi>{\<alpha>}\<close>
using "KBasic2:1"
by (AOT_subst \<open>\<box>\<not>\<phi>{\<alpha>}\<close> \<open>\<not>\<diamond>\<phi>{\<alpha>}\<close> for: \<alpha>)
moreover AOT_have \<open>\<forall>\<alpha> \<box>\<not>\<phi>{\<alpha>} \<equiv> \<box>\<forall>\<alpha> \<not>\<phi>{\<alpha>}\<close>
using "\<equiv>I" "BF" "CBF" by metis
ultimately AOT_have 1: \<open>\<not>\<box>\<forall>\<alpha> \<not>\<phi>{\<alpha>}\<close>
using "\<equiv>E"(3) by blast
AOT_show \<open>\<diamond>\<exists>\<alpha> \<phi>{\<alpha>}\<close>
apply (rule "conventions:5"[THEN "\<equiv>\<^sub>d\<^sub>fI"])
apply (AOT_subst \<open>\<exists>\<alpha> \<phi>{\<alpha>}\<close> \<open>\<not>\<forall>\<alpha> \<not>\<phi>{\<alpha>}\<close>)
apply (simp add: "conventions:4" "\<equiv>Df")
apply (AOT_subst \<open>\<not>\<not>\<forall>\<alpha> \<not>\<phi>{\<alpha>}\<close> \<open>\<forall>\<alpha> \<not>\<phi>{\<alpha>}\<close>)
by (auto simp: 1 "\<equiv>I" "useful-tautologies:1" "useful-tautologies:2")
qed
lemmas "CBF\<diamond>" = "BFs:4"
AOT_theorem "sign-S5-thm:1": \<open>\<exists>\<alpha> \<box>\<phi>{\<alpha>} \<rightarrow> \<box>\<exists>\<alpha> \<phi>{\<alpha>}\<close>
proof(rule "\<rightarrow>I")
AOT_assume \<open>\<exists>\<alpha> \<box>\<phi>{\<alpha>}\<close>
then AOT_obtain \<alpha> where \<open>\<box>\<phi>{\<alpha>}\<close> using "\<exists>E" by metis
moreover AOT_have \<open>\<box>\<alpha>\<down>\<close>
by (simp add: "ex:1:a" "rule-ui:2[const_var]" RN)
moreover AOT_have \<open>\<box>\<phi>{\<tau>}, \<box>\<tau>\<down> \<^bold>\<turnstile>\<^sub>\<box> \<box>\<exists>\<alpha> \<phi>{\<alpha>}\<close> for \<tau>
proof -
AOT_have \<open>\<phi>{\<tau>}, \<tau>\<down> \<^bold>\<turnstile>\<^sub>\<box> \<exists>\<alpha> \<phi>{\<alpha>}\<close> using "existential:1" by blast
AOT_thus \<open>\<box>\<phi>{\<tau>}, \<box>\<tau>\<down> \<^bold>\<turnstile>\<^sub>\<box> \<box>\<exists>\<alpha> \<phi>{\<alpha>}\<close>
using "RN[prem]"[where \<Gamma>="{\<phi> \<tau>, \<guillemotleft>\<tau>\<down>\<guillemotright>}", simplified] by blast
qed
ultimately AOT_show \<open>\<box>\<exists>\<alpha> \<phi>{\<alpha>}\<close> by blast
qed
lemmas Buridan = "sign-S5-thm:1"
AOT_theorem "sign-S5-thm:2": \<open>\<diamond>\<forall>\<alpha> \<phi>{\<alpha>} \<rightarrow> \<forall>\<alpha> \<diamond>\<phi>{\<alpha>}\<close>
proof -
AOT_have \<open>\<forall>\<alpha> (\<diamond>\<forall>\<alpha> \<phi>{\<alpha>} \<rightarrow> \<diamond>\<phi>{\<alpha>})\<close>
by (simp add: "RM\<diamond>" "cqt-orig:3" "\<forall>I")
AOT_thus \<open>\<diamond>\<forall>\<alpha> \<phi>{\<alpha>} \<rightarrow> \<forall>\<alpha> \<diamond>\<phi>{\<alpha>}\<close>
using "\<forall>E"(4) "\<forall>I" "\<rightarrow>E" "\<rightarrow>I" by metis
qed
lemmas "Buridan\<diamond>" = "sign-S5-thm:2"
AOT_theorem "sign-S5-thm:3":
\<open>\<diamond>\<exists>\<alpha> (\<phi>{\<alpha>} & \<psi>{\<alpha>}) \<rightarrow> \<diamond>(\<exists>\<alpha> \<phi>{\<alpha>} & \<exists>\<alpha> \<psi>{\<alpha>})\<close>
apply (rule "RM:2")
by (metis (no_types, lifting) "\<exists>E" "&I" "&E"(1) "&E"(2) "\<rightarrow>I" "\<exists>I"(2))
AOT_theorem "sign-S5-thm:4": \<open>\<diamond>\<exists>\<alpha> (\<phi>{\<alpha>} & \<psi>{\<alpha>}) \<rightarrow> \<diamond>\<exists>\<alpha> \<phi>{\<alpha>}\<close>
apply (rule "RM:2")
by (meson "instantiation" "&E"(1) "\<rightarrow>I" "\<exists>I"(2))
AOT_theorem "sign-S5-thm:5":
\<open>(\<box>\<forall>\<alpha> (\<phi>{\<alpha>} \<rightarrow> \<psi>{\<alpha>}) & \<box>\<forall>\<alpha> (\<psi>{\<alpha>} \<rightarrow> \<chi>{\<alpha>})) \<rightarrow> \<box>\<forall>\<alpha> (\<phi>{\<alpha>} \<rightarrow> \<chi>{\<alpha>})\<close>
proof -
{
fix \<phi>' \<psi>' \<chi>'
AOT_assume \<open>\<^bold>\<turnstile>\<^sub>\<box> \<phi>' & \<psi>' \<rightarrow> \<chi>'\<close>
AOT_hence \<open>\<box>\<phi>' & \<box>\<psi>' \<rightarrow> \<box>\<chi>'\<close>
using "RN[prem]"[where \<Gamma>="{\<phi>', \<psi>'}"] apply simp
using "&E" "&I" "\<rightarrow>E" "\<rightarrow>I" by metis
} note R = this
show ?thesis by (rule R; fact AOT)
qed
AOT_theorem "sign-S5-thm:6":
\<open>(\<box>\<forall>\<alpha> (\<phi>{\<alpha>} \<equiv> \<psi>{\<alpha>}) & \<box>\<forall>\<alpha>(\<psi>{\<alpha>} \<equiv> \<chi>{\<alpha>})) \<rightarrow> \<box>\<forall>\<alpha>(\<phi>{\<alpha>} \<equiv> \<chi>{\<alpha>})\<close>
proof -
{
fix \<phi>' \<psi>' \<chi>'
AOT_assume \<open>\<^bold>\<turnstile>\<^sub>\<box> \<phi>' & \<psi>' \<rightarrow> \<chi>'\<close>
AOT_hence \<open>\<box>\<phi>' & \<box>\<psi>' \<rightarrow> \<box>\<chi>'\<close>
using "RN[prem]"[where \<Gamma>="{\<phi>', \<psi>'}"] apply simp
using "&E" "&I" "\<rightarrow>E" "\<rightarrow>I" by metis
} note R = this
show ?thesis by (rule R; fact AOT)
qed
AOT_theorem "exist-nec2:1": \<open>\<diamond>\<tau>\<down> \<rightarrow> \<tau>\<down>\<close>
using "B\<diamond>" "RM\<diamond>" "Hypothetical Syllogism" "exist-nec" by blast
AOT_theorem "exists-nec2:2": \<open>\<diamond>\<tau>\<down> \<equiv> \<box>\<tau>\<down>\<close>
by (meson "Act-Sub:3" "Hypothetical Syllogism" "exist-nec"
"exist-nec2:1" "\<equiv>I" "nec-imp-act")
AOT_theorem "exists-nec2:3": \<open>\<not>\<tau>\<down> \<rightarrow> \<box>\<not>\<tau>\<down>\<close>
using "KBasic2:1" "\<rightarrow>I" "exist-nec2:1" "\<equiv>E"(2) "modus-tollens:1" by blast
AOT_theorem "exists-nec2:4": \<open>\<diamond>\<not>\<tau>\<down> \<equiv> \<box>\<not>\<tau>\<down>\<close>
by (metis "Act-Sub:3" "KBasic:12" "\<rightarrow>I" "exist-nec" "exists-nec2:3"
"\<equiv>I" "\<equiv>E"(4) "nec-imp-act" "reductio-aa:1")
AOT_theorem "id-nec2:1": \<open>\<diamond>\<alpha> = \<beta> \<rightarrow> \<alpha> = \<beta>\<close>
using "B\<diamond>" "RM\<diamond>" "Hypothetical Syllogism" "id-nec:1" by blast
AOT_theorem "id-nec2:2": \<open>\<alpha> \<noteq> \<beta> \<rightarrow> \<box>\<alpha> \<noteq> \<beta>\<close>
apply (AOT_subst \<open>\<alpha> \<noteq> \<beta>\<close> \<open>\<not>(\<alpha> = \<beta>)\<close>)
using "=-infix"[THEN "\<equiv>Df"] apply blast
using "KBasic2:1" "\<rightarrow>I" "id-nec2:1" "\<equiv>E"(2) "modus-tollens:1" by blast
AOT_theorem "id-nec2:3": \<open>\<diamond>\<alpha> \<noteq> \<beta> \<rightarrow> \<alpha> \<noteq> \<beta>\<close>
apply (AOT_subst \<open>\<alpha> \<noteq> \<beta>\<close> \<open>\<not>(\<alpha> = \<beta>)\<close>)
using "=-infix"[THEN "\<equiv>Df"] apply blast
by (metis "KBasic:11" "\<rightarrow>I" "id-nec:2" "\<equiv>E"(3) "reductio-aa:2" "\<rightarrow>E")
AOT_theorem "id-nec2:4": \<open>\<diamond>\<alpha> = \<beta> \<rightarrow> \<box>\<alpha> = \<beta>\<close>
using "Hypothetical Syllogism" "id-nec2:1" "id-nec:1" by blast
AOT_theorem "id-nec2:5": \<open>\<diamond>\<alpha> \<noteq> \<beta> \<rightarrow> \<box>\<alpha> \<noteq> \<beta>\<close>
using "id-nec2:3" "id-nec2:2" "\<rightarrow>I" "\<rightarrow>E" by metis
AOT_theorem "sc-eq-box-box:1": \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>) \<equiv> (\<diamond>\<phi> \<rightarrow> \<box>\<phi>)\<close>
apply (rule "\<equiv>I"; rule "\<rightarrow>I")
using "KBasic:13" "5\<diamond>" "Hypothetical Syllogism" "\<rightarrow>E" apply blast
by (metis "KBasic2:1" "KBasic:1" "KBasic:2" "S5Basic:13" "\<equiv>E"(2)
"raa-cor:5" "\<rightarrow>E")
AOT_theorem "sc-eq-box-box:2": \<open>(\<box>(\<phi> \<rightarrow> \<box>\<phi>) \<or> (\<diamond>\<phi> \<rightarrow> \<box>\<phi>)) \<rightarrow> (\<diamond>\<phi> \<equiv> \<box>\<phi>)\<close>
by (metis "Act-Sub:3" "KBasic:13" "5\<diamond>" "\<or>E"(2) "\<rightarrow>I" "\<equiv>I"
"nec-imp-act" "raa-cor:2" "\<rightarrow>E")
AOT_theorem "sc-eq-box-box:3": \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>) \<rightarrow> (\<not>\<box>\<phi> \<equiv> \<box>\<not>\<phi>)\<close>
proof (rule "\<rightarrow>I"; rule "\<equiv>I"; rule "\<rightarrow>I")
AOT_assume \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>)\<close>
AOT_hence \<open>\<diamond>\<phi> \<rightarrow> \<box>\<phi>\<close> using "sc-eq-box-box:1" "\<equiv>E" by blast
moreover AOT_assume \<open>\<not>\<box>\<phi>\<close>
ultimately AOT_have \<open>\<not>\<diamond>\<phi>\<close>
using "modus-tollens:1" by blast
AOT_thus \<open>\<box>\<not>\<phi>\<close>
using "KBasic2:1" "\<equiv>E"(2) by blast
next
AOT_assume \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>)\<close>
moreover AOT_assume \<open>\<box>\<not>\<phi>\<close>
ultimately AOT_show \<open>\<not>\<box>\<phi>\<close>
using "modus-tollens:1" "qml:2"[axiom_inst] "\<rightarrow>E" by blast
qed
AOT_theorem "sc-eq-box-box:4":
\<open>(\<box>(\<phi> \<rightarrow> \<box>\<phi>) & \<box>(\<psi> \<rightarrow> \<box>\<psi>)) \<rightarrow> ((\<box>\<phi> \<equiv> \<box>\<psi>) \<rightarrow> \<box>(\<phi> \<equiv> \<psi>))\<close>
proof(rule "\<rightarrow>I"; rule "\<rightarrow>I")
AOT_assume \<theta>: \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>) & \<box>(\<psi> \<rightarrow> \<box>\<psi>)\<close>
AOT_assume \<xi>: \<open>\<box>\<phi> \<equiv> \<box>\<psi>\<close>
AOT_hence \<open>(\<box>\<phi> & \<box>\<psi>) \<or> (\<not>\<box>\<phi> & \<not>\<box>\<psi>)\<close>
using "\<equiv>E"(4) "oth-class-taut:4:g" "raa-cor:3" by blast
moreover {
AOT_assume \<open>\<box>\<phi> & \<box>\<psi>\<close>
AOT_hence \<open>\<box>(\<phi> \<equiv> \<psi>)\<close>
using "KBasic:3" "KBasic:8" "\<equiv>E"(2) "vdash-properties:10" by blast
}
moreover {
AOT_assume \<open>\<not>\<box>\<phi> & \<not>\<box>\<psi>\<close>
moreover AOT_have \<open>\<not>\<box>\<phi> \<equiv> \<box>\<not>\<phi>\<close> and \<open>\<not>\<box>\<psi> \<equiv> \<box>\<not>\<psi>\<close>
using \<theta> "Conjunction Simplification"(1,2)
"sc-eq-box-box:3" "\<rightarrow>E" by metis+
ultimately AOT_have \<open>\<box>\<not>\<phi> & \<box>\<not>\<psi>\<close>
by (metis "&I" "Conjunction Simplification"(1,2)
"\<equiv>E"(4) "modus-tollens:1" "raa-cor:3")
AOT_hence \<open>\<box>(\<phi> \<equiv> \<psi>)\<close>
using "KBasic:3" "KBasic:9" "\<equiv>E"(2) "\<rightarrow>E" by blast
}
ultimately AOT_show \<open>\<box>(\<phi> \<equiv> \<psi>)\<close>
using "\<or>E"(2) "reductio-aa:1" by blast
qed
AOT_theorem "sc-eq-box-box:5":
\<open>(\<box>(\<phi> \<rightarrow> \<box>\<phi>) & \<box>(\<psi> \<rightarrow> \<box>\<psi>)) \<rightarrow> \<box>((\<phi> \<equiv> \<psi>) \<rightarrow> \<box>(\<phi> \<equiv> \<psi>))\<close>
proof (rule "\<rightarrow>I")
AOT_assume \<open>(\<box>(\<phi> \<rightarrow> \<box>\<phi>) & \<box>(\<psi> \<rightarrow> \<box>\<psi>))\<close>
AOT_hence \<open>\<box>(\<box>(\<phi> \<rightarrow> \<box>\<phi>) & \<box>(\<psi> \<rightarrow> \<box>\<psi>))\<close>
using 4[THEN "\<rightarrow>E"] "&E" "&I" "KBasic:3" "\<equiv>E"(2) by metis
moreover AOT_have \<open>\<box>(\<box>(\<phi> \<rightarrow> \<box>\<phi>) & \<box>(\<psi> \<rightarrow> \<box>\<psi>)) \<rightarrow> \<box>((\<phi> \<equiv> \<psi>) \<rightarrow> \<box>(\<phi> \<equiv> \<psi>))\<close>
proof (rule RM; rule "\<rightarrow>I"; rule "\<rightarrow>I")
AOT_modally_strict {
AOT_assume A: \<open>(\<box>(\<phi> \<rightarrow> \<box>\<phi>) & \<box>(\<psi> \<rightarrow> \<box>\<psi>))\<close>
AOT_hence \<open>\<phi> \<rightarrow> \<box>\<phi>\<close> and \<open>\<psi> \<rightarrow> \<box>\<psi>\<close>
using "&E" "qml:2"[axiom_inst] "\<rightarrow>E" by blast+
moreover AOT_assume \<open>\<phi> \<equiv> \<psi>\<close>
ultimately AOT_have \<open>\<box>\<phi> \<equiv> \<box>\<psi>\<close>
using "\<rightarrow>E" "qml:2"[axiom_inst] "\<equiv>E" "\<equiv>I" by meson
moreover AOT_have \<open>(\<box>\<phi> \<equiv> \<box>\<psi>) \<rightarrow> \<box>(\<phi> \<equiv> \<psi>)\<close>
using A "sc-eq-box-box:4" "\<rightarrow>E" by blast
ultimately AOT_show \<open>\<box>(\<phi> \<equiv> \<psi>)\<close> using "\<rightarrow>E" by blast
}
qed
ultimately AOT_show \<open>\<box>((\<phi> \<equiv> \<psi>) \<rightarrow> \<box>(\<phi> \<equiv> \<psi>))\<close> using "\<rightarrow>E" by blast
qed
AOT_theorem "sc-eq-box-box:6": \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>) \<rightarrow> ((\<phi> \<rightarrow> \<box>\<psi>) \<rightarrow> \<box>(\<phi> \<rightarrow> \<psi>))\<close>
proof (rule "\<rightarrow>I"; rule "\<rightarrow>I"; rule "raa-cor:1")
AOT_assume \<open>\<not>\<box>(\<phi> \<rightarrow> \<psi>)\<close>
AOT_hence \<open>\<diamond>\<not>(\<phi> \<rightarrow> \<psi>)\<close>
by (metis "KBasic:11" "\<equiv>E"(1))
AOT_hence \<open>\<diamond>(\<phi> & \<not>\<psi>)\<close>
by (AOT_subst \<open>\<phi> & \<not>\<psi>\<close> \<open>\<not>(\<phi> \<rightarrow> \<psi>)\<close>)
(meson "Commutativity of \<equiv>" "\<equiv>E"(1) "oth-class-taut:1:b")
AOT_hence \<open>\<diamond>\<phi>\<close> and 2: \<open>\<diamond>\<not>\<psi>\<close>
using "KBasic2:3"[THEN "\<rightarrow>E"] "&E" by blast+
moreover AOT_assume \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>)\<close>
ultimately AOT_have \<open>\<box>\<phi>\<close>
by (metis "\<equiv>E"(1) "sc-eq-box-box:1" "\<rightarrow>E")
AOT_hence \<phi>
using "qml:2"[axiom_inst, THEN "\<rightarrow>E"] by blast
moreover AOT_assume \<open>\<phi> \<rightarrow> \<box>\<psi>\<close>
ultimately AOT_have \<open>\<box>\<psi>\<close>
using "\<rightarrow>E" by blast
moreover AOT_have \<open>\<not>\<box>\<psi>\<close>
using 2 "KBasic:12" "\<not>\<not>I" "intro-elim:3:d" by blast
ultimately AOT_show \<open>\<box>\<psi> & \<not>\<box>\<psi>\<close>
using "&I" by blast
qed
AOT_theorem "sc-eq-box-box:7": \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>) \<rightarrow> ((\<phi> \<rightarrow> \<^bold>\<A>\<psi>) \<rightarrow> \<^bold>\<A>(\<phi> \<rightarrow> \<psi>))\<close>
proof (rule "\<rightarrow>I"; rule "\<rightarrow>I"; rule "raa-cor:1")
AOT_assume \<open>\<not>\<^bold>\<A>(\<phi> \<rightarrow> \<psi>)\<close>
AOT_hence \<open>\<^bold>\<A>\<not>(\<phi> \<rightarrow> \<psi>)\<close>
by (metis "Act-Basic:1" "\<or>E"(2))
AOT_hence \<open>\<^bold>\<A>(\<phi> & \<not>\<psi>)\<close>
by (AOT_subst \<open>\<phi> & \<not>\<psi>\<close> \<open>\<not>(\<phi> \<rightarrow> \<psi>)\<close>)
(meson "Commutativity of \<equiv>" "\<equiv>E"(1) "oth-class-taut:1:b")
AOT_hence \<open>\<^bold>\<A>\<phi>\<close> and 2: \<open>\<^bold>\<A>\<not>\<psi>\<close>
using "Act-Basic:2"[THEN "\<equiv>E"(1)] "&E" by blast+
AOT_hence \<open>\<diamond>\<phi>\<close>
by (metis "Act-Sub:3" "\<rightarrow>E")
moreover AOT_assume \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>)\<close>
ultimately AOT_have \<open>\<box>\<phi>\<close>
by (metis "\<equiv>E"(1) "sc-eq-box-box:1" "\<rightarrow>E")
AOT_hence \<phi>
using "qml:2"[axiom_inst, THEN "\<rightarrow>E"] by blast
moreover AOT_assume \<open>\<phi> \<rightarrow> \<^bold>\<A>\<psi>\<close>
ultimately AOT_have \<open>\<^bold>\<A>\<psi>\<close>
using "\<rightarrow>E" by blast
moreover AOT_have \<open>\<not>\<^bold>\<A>\<psi>\<close>
using 2 by (meson "Act-Sub:1" "\<equiv>E"(4) "raa-cor:3")
ultimately AOT_show \<open>\<^bold>\<A>\<psi> & \<not>\<^bold>\<A>\<psi>\<close>
using "&I" by blast
qed
AOT_theorem "sc-eq-fur:1": \<open>\<diamond>\<^bold>\<A>\<phi> \<equiv> \<box>\<^bold>\<A>\<phi>\<close>
using "Act-Basic:6" "Act-Sub:4" "\<equiv>E"(6) by blast
AOT_theorem "sc-eq-fur:2": \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>) \<rightarrow> (\<^bold>\<A>\<phi> \<equiv> \<phi>)\<close>
by (metis "B\<diamond>" "Act-Sub:3" "KBasic:13" "T\<diamond>" "Hypothetical Syllogism"
"\<rightarrow>I" "\<equiv>I" "nec-imp-act")
AOT_theorem "sc-eq-fur:3":
\<open>\<box>\<forall>x (\<phi>{x} \<rightarrow> \<box>\<phi>{x}) \<rightarrow> (\<exists>!x \<phi>{x} \<rightarrow> \<^bold>\<iota>x \<phi>{x}\<down>)\<close>
proof (rule "\<rightarrow>I"; rule "\<rightarrow>I")
AOT_assume \<open>\<box>\<forall>x (\<phi>{x} \<rightarrow> \<box>\<phi>{x})\<close>
AOT_hence A: \<open>\<forall>x \<box>(\<phi>{x} \<rightarrow> \<box>\<phi>{x})\<close>
using CBF "\<rightarrow>E" by blast
AOT_assume \<open>\<exists>!x \<phi>{x}\<close>
then AOT_obtain a where a_def: \<open>\<phi>{a} & \<forall>y (\<phi>{y} \<rightarrow> y = a)\<close>
using "\<exists>E"[rotated 1, OF "uniqueness:1"[THEN "\<equiv>\<^sub>d\<^sub>fE"]] by blast
moreover AOT_have \<open>\<box>\<phi>{a}\<close>
using calculation A "\<forall>E"(2) "qml:2"[axiom_inst] "\<rightarrow>E" "&E"(1) by blast
AOT_hence \<open>\<^bold>\<A>\<phi>{a}\<close>
using "nec-imp-act" "\<rightarrow>E" by blast
moreover AOT_have \<open>\<forall>y (\<^bold>\<A>\<phi>{y} \<rightarrow> y = a)\<close>
proof (rule "\<forall>I"; rule "\<rightarrow>I")
fix b
AOT_assume \<open>\<^bold>\<A>\<phi>{b}\<close>
AOT_hence \<open>\<diamond>\<phi>{b}\<close>
using "Act-Sub:3" "\<rightarrow>E" by blast
moreover {
AOT_have \<open>\<box>(\<phi>{b} \<rightarrow> \<box>\<phi>{b})\<close>
using A "\<forall>E"(2) by blast
AOT_hence \<open>\<diamond>\<phi>{b} \<rightarrow> \<box>\<phi>{b}\<close>
using "KBasic:13" "5\<diamond>" "Hypothetical Syllogism" "\<rightarrow>E" by blast
}
ultimately AOT_have \<open>\<box>\<phi>{b}\<close>
using "\<rightarrow>E" by blast
AOT_hence \<open>\<phi>{b}\<close>
using "qml:2"[axiom_inst] "\<rightarrow>E" by blast
AOT_thus \<open>b = a\<close>
using a_def[THEN "&E"(2)] "\<forall>E"(2) "\<rightarrow>E" by blast
qed
ultimately AOT_have \<open>\<^bold>\<A>\<phi>{a} & \<forall>y (\<^bold>\<A>\<phi>{y} \<rightarrow> y = a)\<close>
using "&I" by blast
AOT_hence \<open>\<exists>x (\<^bold>\<A>\<phi>{x} & \<forall>y (\<^bold>\<A>\<phi>{y} \<rightarrow> y = x))\<close>
using "\<exists>I" by fast
AOT_hence \<open>\<exists>!x \<^bold>\<A>\<phi>{x}\<close>
using "uniqueness:1"[THEN "\<equiv>\<^sub>d\<^sub>fI"] by fast
AOT_thus \<open>\<^bold>\<iota>x \<phi>{x}\<down>\<close>
using "actual-desc:1"[THEN "\<equiv>E"(2)] by blast
qed
AOT_theorem "sc-eq-fur:4":
\<open>\<box>\<forall>x (\<phi>{x} \<rightarrow> \<box>\<phi>{x}) \<rightarrow> (x = \<^bold>\<iota>x \<phi>{x} \<equiv> (\<phi>{x} & \<forall>z (\<phi>{z} \<rightarrow> z = x)))\<close>
proof (rule "\<rightarrow>I")
AOT_assume \<open>\<box>\<forall>x (\<phi>{x} \<rightarrow> \<box>\<phi>{x})\<close>
AOT_hence \<open>\<forall>x \<box>(\<phi>{x} \<rightarrow> \<box>\<phi>{x})\<close>
using CBF "\<rightarrow>E" by blast
AOT_hence A: \<open>\<^bold>\<A>\<phi>{\<alpha>} \<equiv> \<phi>{\<alpha>}\<close> for \<alpha>
using "sc-eq-fur:2" "\<forall>E" "\<rightarrow>E" by fast
AOT_show \<open>x = \<^bold>\<iota>x \<phi>{x} \<equiv> (\<phi>{x} & \<forall>z (\<phi>{z} \<rightarrow> z = x))\<close>
proof (rule "\<equiv>I"; rule "\<rightarrow>I")
AOT_assume \<open>x = \<^bold>\<iota>x \<phi>{x}\<close>
AOT_hence B: \<open>\<^bold>\<A>\<phi>{x} & \<forall>z (\<^bold>\<A>\<phi>{z} \<rightarrow> z = x)\<close>
using "nec-hintikka-scheme"[THEN "\<equiv>E"(1)] by blast
AOT_show \<open>\<phi>{x} & \<forall>z (\<phi>{z} \<rightarrow> z = x)\<close>
proof (rule "&I"; (rule "\<forall>I"; rule "\<rightarrow>I")?)
AOT_show \<open>\<phi>{x}\<close>
using A B[THEN "&E"(1)] "\<equiv>E"(1) by blast
next
AOT_show \<open>z = x\<close> if \<open>\<phi>{z}\<close> for z
using that B[THEN "&E"(2)] "\<forall>E"(2) "\<rightarrow>E" A[THEN "\<equiv>E"(2)] by blast
qed
next
AOT_assume B: \<open>\<phi>{x} & \<forall>z (\<phi>{z} \<rightarrow> z = x)\<close>
AOT_have \<open>\<^bold>\<A>\<phi>{x} & \<forall>z (\<^bold>\<A>\<phi>{z} \<rightarrow> z = x)\<close>
proof(rule "&I"; (rule "\<forall>I"; rule "\<rightarrow>I")?)
AOT_show \<open>\<^bold>\<A>\<phi>{x}\<close>
using B[THEN "&E"(1)] A[THEN "\<equiv>E"(2)] by blast
next
AOT_show \<open>b = x\<close> if \<open>\<^bold>\<A>\<phi>{b}\<close> for b
using A[THEN "\<equiv>E"(1)] that
B[THEN "&E"(2), THEN "\<forall>E"(2), THEN "\<rightarrow>E"] by blast
qed
AOT_thus \<open>x = \<^bold>\<iota>x \<phi>{x}\<close>
using "nec-hintikka-scheme"[THEN "\<equiv>E"(2)] by blast
qed
qed
AOT_theorem "id-act:1": \<open>\<alpha> = \<beta> \<equiv> \<^bold>\<A>\<alpha> = \<beta>\<close>
by (meson "Act-Sub:3" "Hypothetical Syllogism"
"id-nec2:1" "id-nec:2" "\<equiv>I" "nec-imp-act")
AOT_theorem "id-act:2": \<open>\<alpha> \<noteq> \<beta> \<equiv> \<^bold>\<A>\<alpha> \<noteq> \<beta>\<close>
proof (AOT_subst \<open>\<alpha> \<noteq> \<beta>\<close> \<open>\<not>(\<alpha> = \<beta>)\<close>)
AOT_modally_strict {
AOT_show \<open>\<alpha> \<noteq> \<beta> \<equiv> \<not>(\<alpha> = \<beta>)\<close>
by (simp add: "=-infix" "\<equiv>Df")
}
next
AOT_show \<open>\<not>(\<alpha> = \<beta>) \<equiv> \<^bold>\<A>\<not>(\<alpha> = \<beta>)\<close>
proof (safe intro!: "\<equiv>I" "\<rightarrow>I")
AOT_assume \<open>\<not>\<alpha> = \<beta>\<close>
AOT_hence \<open>\<not>\<^bold>\<A>\<alpha> = \<beta>\<close> using "id-act:1" "\<equiv>E"(3) by blast
AOT_thus \<open>\<^bold>\<A>\<not>\<alpha> = \<beta>\<close>
using "\<not>\<not>E" "Act-Sub:1" "\<equiv>E"(3) by blast
next
AOT_assume \<open>\<^bold>\<A>\<not>\<alpha> = \<beta>\<close>
AOT_hence \<open>\<not>\<^bold>\<A>\<alpha> = \<beta>\<close>
using "\<not>\<not>I" "Act-Sub:1" "\<equiv>E"(4) by blast
AOT_thus \<open>\<not>\<alpha> = \<beta>\<close>
using "id-act:1" "\<equiv>E"(4) by blast
qed
qed
AOT_theorem "A-Exists:1": \<open>\<^bold>\<A>\<exists>!\<alpha> \<phi>{\<alpha>} \<equiv> \<exists>!\<alpha> \<^bold>\<A>\<phi>{\<alpha>}\<close>
proof -
AOT_have \<open>\<^bold>\<A>\<exists>!\<alpha> \<phi>{\<alpha>} \<equiv> \<^bold>\<A>\<exists>\<alpha>\<forall>\<beta> (\<phi>{\<beta>} \<equiv> \<beta> = \<alpha>)\<close>
by (AOT_subst \<open>\<exists>!\<alpha> \<phi>{\<alpha>}\<close> \<open>\<exists>\<alpha>\<forall>\<beta> (\<phi>{\<beta>} \<equiv> \<beta> = \<alpha>)\<close>)
(auto simp add: "oth-class-taut:3:a" "uniqueness:2")
also AOT_have \<open>\<dots> \<equiv> \<exists>\<alpha> \<^bold>\<A>\<forall>\<beta> (\<phi>{\<beta>} \<equiv> \<beta> = \<alpha>)\<close>
by (simp add: "Act-Basic:10")
also AOT_have \<open>\<dots> \<equiv> \<exists>\<alpha>\<forall>\<beta> \<^bold>\<A>(\<phi>{\<beta>} \<equiv> \<beta> = \<alpha>)\<close>
by (AOT_subst \<open>\<^bold>\<A>\<forall>\<beta> (\<phi>{\<beta>} \<equiv> \<beta> = \<alpha>)\<close> \<open>\<forall>\<beta> \<^bold>\<A>(\<phi>{\<beta>} \<equiv> \<beta> = \<alpha>)\<close> for: \<alpha>)
(auto simp: "logic-actual-nec:3"[axiom_inst] "oth-class-taut:3:a")
also AOT_have \<open>\<dots> \<equiv> \<exists>\<alpha>\<forall>\<beta> (\<^bold>\<A>\<phi>{\<beta>} \<equiv> \<^bold>\<A>\<beta> = \<alpha>)\<close>
by (AOT_subst (reverse) \<open>\<^bold>\<A>\<phi>{\<beta>} \<equiv> \<^bold>\<A>\<beta> = \<alpha>\<close>
\<open>\<^bold>\<A>(\<phi>{\<beta>} \<equiv> \<beta> = \<alpha>)\<close> for: \<alpha> \<beta> :: 'a)
(auto simp: "Act-Basic:5" "cqt-further:7")
also AOT_have \<open>\<dots> \<equiv> \<exists>\<alpha>\<forall>\<beta> (\<^bold>\<A>\<phi>{\<beta>} \<equiv> \<beta> = \<alpha>)\<close>
by (AOT_subst (reverse) \<open>\<^bold>\<A>\<beta> = \<alpha>\<close> \<open>\<beta> = \<alpha>\<close> for: \<alpha> \<beta> :: 'a)
(auto simp: "id-act:1" "cqt-further:7")
also AOT_have \<open>... \<equiv> \<exists>!\<alpha> \<^bold>\<A>\<phi>{\<alpha>}\<close>
using "uniqueness:2" "Commutativity of \<equiv>"[THEN "\<equiv>E"(1)] by fast
finally show ?thesis.
qed
AOT_theorem "A-Exists:2": \<open>\<^bold>\<iota>x \<phi>{x}\<down> \<equiv> \<^bold>\<A>\<exists>!x \<phi>{x}\<close>
by (AOT_subst \<open>\<^bold>\<A>\<exists>!x \<phi>{x}\<close> \<open>\<exists>!x \<^bold>\<A>\<phi>{x}\<close>)
(auto simp: "actual-desc:1" "A-Exists:1")
AOT_theorem "id-act-desc:1": \<open>\<^bold>\<iota>x (x = y)\<down>\<close>
proof(rule "existence:1"[THEN "\<equiv>\<^sub>d\<^sub>fI"]; rule "\<exists>I")
AOT_show \<open>[\<lambda>x E!x \<rightarrow> E!x]\<^bold>\<iota>x (x = y)\<close>
proof (rule "russell-axiom[exe,1].nec-russell-axiom"[THEN "\<equiv>E"(2)];
rule "\<exists>I"; (rule "&I")+)
AOT_show \<open>\<^bold>\<A>y = y\<close> by (simp add: "RA[2]" "id-eq:1")
next
AOT_show \<open>\<forall>z (\<^bold>\<A>z = y \<rightarrow> z = y)\<close>
apply (rule "\<forall>I")
using "id-act:1"[THEN "\<equiv>E"(2)] "\<rightarrow>I" by blast
next
AOT_show \<open>[\<lambda>x E!x \<rightarrow> E!x]y\<close>
proof (rule "lambda-predicates:2"[axiom_inst, THEN "\<rightarrow>E", THEN "\<equiv>E"(2)])
AOT_show \<open>[\<lambda>x E!x \<rightarrow> E!x]\<down>\<close>
by "cqt:2[lambda]"
next
AOT_show \<open>E!y \<rightarrow> E!y\<close>
by (simp add: "if-p-then-p")
qed
qed
next
AOT_show \<open>[\<lambda>x E!x \<rightarrow> E!x]\<down>\<close>
by "cqt:2[lambda]"
qed
AOT_theorem "id-act-desc:2": \<open>y = \<^bold>\<iota>x (x = y)\<close>
by (rule descriptions[axiom_inst, THEN "\<equiv>E"(2)];
rule "\<forall>I"; rule "id-act:1"[symmetric])
AOT_theorem "pre-en-eq:1[1]": \<open>x\<^sub>1[F] \<rightarrow> \<box>x\<^sub>1[F]\<close>
by (simp add: encoding "vdash-properties:1[2]")
AOT_theorem "pre-en-eq:1[2]": \<open>x\<^sub>1x\<^sub>2[F] \<rightarrow> \<box>x\<^sub>1x\<^sub>2[F]\<close>
proof (rule "\<rightarrow>I")
AOT_assume \<open>x\<^sub>1x\<^sub>2[F]\<close>
AOT_hence \<open>x\<^sub>1[\<lambda>y [F]yx\<^sub>2]\<close> and \<open>x\<^sub>2[\<lambda>y [F]x\<^sub>1y]\<close>
using "nary-encoding[2]"[axiom_inst, THEN "\<equiv>E"(1)] "&E" by blast+
moreover AOT_have \<open>[\<lambda>y [F]yx\<^sub>2]\<down>\<close> by "cqt:2"
moreover AOT_have \<open>[\<lambda>y [F]x\<^sub>1y]\<down>\<close> by "cqt:2"
ultimately AOT_have \<open>\<box>x\<^sub>1[\<lambda>y [F]yx\<^sub>2]\<close> and \<open>\<box>x\<^sub>2[\<lambda>y [F]x\<^sub>1y]\<close>
using encoding[axiom_inst, unvarify F] "\<rightarrow>E" "&I" by blast+
note A = this
AOT_hence \<open>\<box>(x\<^sub>1[\<lambda>y [F]yx\<^sub>2] & x\<^sub>2[\<lambda>y [F]x\<^sub>1y])\<close>
using "KBasic:3"[THEN "\<equiv>E"(2)] "&I" by blast
AOT_thus \<open>\<box>x\<^sub>1x\<^sub>2[F]\<close>
by (rule "nary-encoding[2]"[axiom_inst, THEN RN,
THEN "KBasic:6"[THEN "\<rightarrow>E"],
THEN "\<equiv>E"(2)])
qed
AOT_theorem "pre-en-eq:1[3]": \<open>x\<^sub>1x\<^sub>2x\<^sub>3[F] \<rightarrow> \<box>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
proof (rule "\<rightarrow>I")
AOT_assume \<open>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
AOT_hence \<open>x\<^sub>1[\<lambda>y [F]yx\<^sub>2x\<^sub>3]\<close>
and \<open>x\java.lang.ArrayIndexOutOfBoundsException
and \<open>x\<^sub>3[\<lambda>y [F]x\<^sub>1x\<^sub>2y]\<close>
using "nary-encoding[3]"[axiom_inst, THEN "\<equiv>E"(1)] "&E" by blast+
moreover AOT_have \<open>[\<lambda>y [F]yx\<^sub>2x\<^sub>3]\<down>\<close> by "cqt:2"
moreover AOT_have \<open>[\<lambda>y [F]x\<^sub>1yx\<^sub>3]\<down>\<close> by "cqt:2"
moreover AOT_have \<open>[\<lambda>y [F]x\<^sub>1x\<^sub>2y]\<down>\<close> by "cqt:2"
ultimately AOT_have \<open>\<box>x\<^sub>1[\<lambda>y [F]yx\<^sub>2x\<^sub>3]\<close>
and \<open>\<box>x\<^sub>2[\<lambda>y [F]x\<^sub>1yx\<^sub>3]\<close>
and \<open>\<box>x\<^sub>3[\<lambda>y [F]x\<^sub>1x\<^sub>2y]\<close>
using encoding[axiom_inst, unvarify F] "\<rightarrow>E" by blast+
note A = this
AOT_have B: \<open>\<box>(x\<^sub>1[\<lambda>y [F]yx\<^sub>2x\<^sub>3] & x\<^sub>2[\<lambda>y [F]x\<^sub>1yx\<^sub>3] & x\<^sub>3[\<lambda>y [F]x\<^sub>1x\<^sub>2y])\<close>
by (rule "KBasic:3"[THEN "\<equiv>E"(2)] "&I" A)+
AOT_thus \<open>\<box>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
by (rule "nary-encoding[3]"[axiom_inst, THEN RN,
THEN "KBasic:6"[THEN "\<rightarrow>E"], THEN "\<equiv>E"(2)])
qed
AOT_theorem "pre-en-eq:1[4]": \<open>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<rightarrow> \<box>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
proof (rule "\<rightarrow>I")
AOT_assume \<open>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
AOT_hence \<open>x\<^sub>1[\<lambda>y [F]yx\<^sub>2x\<^sub>3x\<^sub>4]\<close>
and \<open>x\<^sub>2[\<lambda>y [F]x\<^sub>1yx\<^sub>3x\<^sub>4]\<close>
and \<open>x\<^sub>3[\<lambda>y [F]x\<^sub>1x\<^sub>2yx\<^sub>4]\<close>
and \<open>x\<^sub>4[\<lambda>y [F]x\<^sub>1x\<^sub>2x\<^sub>3y]\<close>
using "nary-encoding[4]"[axiom_inst, THEN "\<equiv>E"(1)] "&E" by metis+
moreover AOT_have \<open>[\<lambda>y [F]yx\<^sub>2x\<^sub>3x\<^sub>4]\<down>\<close> by "cqt:2"
moreover AOT_have \<open>[\<lambda>y [F]x\<^sub>1yx\<^sub>3x\<^sub>4]\<down>\<close> by "cqt:2"
moreover AOT_have \<open>[\<lambda>y [F]x\<^sub>1x\<^sub>2yx\<^sub>4]\<down>\<close> by "cqt:2"
moreover AOT_have \<open>[\<lambda>y [F]x\<^sub>1x\<^sub>2x\<^sub>3y]\<down>\<close> by "cqt:2"
ultimately AOT_have \<open>\<box>x\<^sub>1[\<lambda>y [F]yx\<^sub>2x\<^sub>3x\<^sub>4]\<close>
and \<open>\<box>x\<^sub>2[\<lambda>y [F]x\<^sub>1yx\<^sub>3x\<^sub>4]\<close>
and \<open>\<box>x\<^sub>3[\<lambda>y [F]x\<^sub>1x\<^sub>2yx\<^sub>4]\<close>
and \<open>\<box>x\<^sub>4[\<lambda>y [F]x\<^sub>1x\<^sub>2x\<^sub>3y]\<close>
using "\<rightarrow>E" encoding[axiom_inst, unvarify F] by blast+
note A = this
AOT_have B: \<open>\<box>(x\<^sub>1[\<lambda>y [F]yx\<^sub>2x\<^sub>3x\<^sub>4] &
x\<^sub>2[\<lambda>y [F]x\<^sub>1yx\<^sub>3x\<^sub>4] &
x\<^sub>3[\<lambda>y [F]x\<^sub>1x\<^sub>2yx\<^sub>4] &
x\<^sub>4[\<lambda>y [F]x\<^sub>1x\<^sub>2x\<^sub>3y])\<close>
by (rule "KBasic:3"[THEN "\<equiv>E"(2)] "&I" A)+
AOT_thus \<open>\<box>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
by (rule "nary-encoding[4]"[axiom_inst, THEN RN,
THEN "KBasic:6"[THEN "\<rightarrow>E"], THEN "\<equiv>E"(2)])
qed
AOT_theorem "pre-en-eq:2[1]": \<open>\<not>x\<^sub>1[F] \<rightarrow> \<box>\<not>x\<^sub>1[F]\<close>
proof (rule "\<rightarrow>I"; rule "raa-cor:1")
AOT_assume \<open>\<not>\<box>\<not>x\<^sub>1[F]\<close>
AOT_hence \<open>\<diamond>x\<^sub>1[F]\<close>
by (rule "conventions:5"[THEN "\<equiv>\<^sub>d\<^sub>fI"])
AOT_hence \<open>x\<^sub>1[F]\<close>
by(rule "S5Basic:13"[THEN "\<equiv>E"(1), OF "pre-en-eq:1[1]"[THEN RN],
THEN "qml:2"[axiom_inst, THEN "\<rightarrow>E"], THEN "\<rightarrow>E"])
moreover AOT_assume \<open>\<not>x\<^sub>1[F]\<close>
ultimately AOT_show \<open>x\<^sub>1[F] & \<not>x\<^sub>1[F]\<close> by (rule "&I")
qed
AOT_theorem "pre-en-eq:2[2]": \<open>\<not>x\<^sub>1x\<^sub>2[F] \<rightarrow> \<box>\<not>x\<^sub>1x\<^sub>2[F]\<close>
proof (rule "\<rightarrow>I"; rule "raa-cor:1")
AOT_assume \<open>\<not>\<box>\<not>x\<^sub>1x\<^sub>2[F]\<close>
AOT_hence \<open>\<diamond>x\<^sub>1x\<^sub>2[F]\<close>
by (rule "conventions:5"[THEN "\<equiv>\<^sub>d\<^sub>fI"])
AOT_hence \<open>x\<^sub>1x\<^sub>2[F]\<close>
by(rule "S5Basic:13"[THEN "\<equiv>E"(1), OF "pre-en-eq:1[2]"[THEN RN],
THEN "qml:2"[axiom_inst, THEN "\<rightarrow>E"], THEN "\<rightarrow>E"])
moreover AOT_assume \<open>\<not>x\<^sub>1x\<^sub>2[F]\<close>
ultimately AOT_show \<open>x\<^sub>1x\<^sub>2[F] & \<not>x\<^sub>1x\<^sub>2[F]\<close> by (rule "&I"</span>)
qed
AOT_theorem "pre-en-eq:2[3]": \<open>\<not>x\<^sub>1x\<^sub>2x\<^sub>3[F] \<rightarrow> \<box>\<not>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
proof (rule "\<rightarrow>I"; rule "raa-cor:1")
AOT_assume \<open>\<not>\<box>\<not>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
AOT_hence \<open>\<diamond>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
by (rule "conventions:5"[THEN "\<equiv>\<^sub>d\<^sub>fI"])
AOT_hence \<open>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
by(rule "S5Basic:13"[THEN "\<equiv>E"(1), OF "pre-en-eq:1[3]"[THEN RN],
THEN "qml:2"[axiom_inst, THEN "\<rightarrow>E"], THEN "\<rightarrow>E"])
moreover AOT_assume \<open>\<not>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
ultimately AOT_show \<open>x\<^sub>1x\<^sub>2x\<^sub>3[F] & \<not>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close> by (rule "&I")
qed
AOT_theorem "pre-en-eq:2[4]": \<open>\<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<rightarrow> \<box>\<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
proof (rule "\<rightarrow>I"; rule "raa-cor:1")
AOT_assume \<open>\<not>\<box>\<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
AOT_hence \<open>\<diamond>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
by (rule "conventions:5"[THEN "\<equiv>\<^sub>d\<^sub>fI"])
AOT_hence \<open>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
by(rule "S5Basic:13"[THEN "\<equiv>E"(1), OF "pre-en-eq:1[4]"[THEN RN],
THEN "qml:2"[axiom_inst, THEN "\<rightarrow>E"], THEN "\<rightarrow>E"])
moreover AOT_assume \<open>\<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
ultimately AOT_show \<open>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] & \<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close> by (rule "&I")
qed
AOT_theorem "en-eq:1[1]": \<open>\<diamond>x\<^sub>1[F] \<equiv> \<box>x\<^sub>1[F]\<close>
using "pre-en-eq:1[1]"[THEN RN] "sc-eq-box-box:2" "\<or>I" "\<rightarrow>E" by metis
AOT_theorem "en-eq:1[2]": \<open>\<diamond>x\<^sub>1x\<^sub>2[F] \<equiv> \<box>x\<^sub>1x\<^sub>2[F]\<close>
using "pre-en-eq:1[2]"[THEN RN] "sc-eq-box-box:2" "\<or>I" "\<rightarrow>E" by metis
AOT_theorem "en-eq:1[3]": \<open>\<diamond>x\<^sub>1x\<^sub>2x\<^sub>3[F] \<equiv> \<box>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
using "pre-en-eq:1[3]"[THEN RN] "sc-eq-box-box:2" "\<or>I" "\<rightarrow>E" by fast
AOT_theorem "en-eq:1[4]": \<open>\<diamond>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<equiv> \<box>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
using "pre-en-eq:1[4]"[THEN RN] "sc-eq-box-box:2" "\<or>I" "\<rightarrow>E" by fast
AOT_theorem "en-eq:2[1]": \<open>x\<^sub>1[F] \<equiv> \<box>x\<^sub>1[F]\<close>
by (simp add: "\<equiv>I" "pre-en-eq:1[1]" "qml:2"[axiom_inst])
AOT_theorem "en-eq:2[2]": \<open>x\<^sub>1x\<^sub>2[F] \<equiv> \<box>x\<^sub>1x\<^sub>2[F]\<close>
by (simp add: "\<equiv>I" "pre-en-eq:1[2]" "qml:2"[axiom_inst])
AOT_theorem "en-eq:2[3]": \<open>x\<^sub>1x\<^sub>2x\<^sub>3[F] \<equiv> \<box>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
by (simp add: "\<equiv>I" "pre-en-eq:1[3]" "qml:2"[axiom_inst])
AOT_theorem "en-eq:2[4]": \<open>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<equiv> \<box>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
by (simp add: "\<equiv>I" "pre-en-eq:1[4]" "qml:2"[axiom_inst])
AOT_theorem "en-eq:3[1]": \<open>\<diamond>x\<^sub>1[F] \<equiv> x\<^sub>1[F]\<close>
using "T\<diamond>" "derived-S5-rules:2"[OF "pre-en-eq:1[1]"] "\<equiv>I" by blast
AOT_theorem "en-eq:3[2]": \<open>\<diamond>x\<^sub>1x\<^sub>2[F] \<equiv> x\<^sub>1x\<^sub>2[F]\<close>
using "T\<diamond>" "derived-S5-rules:2"[OF "pre-en-eq:1[2]"] "\<equiv>I" by blast
AOT_theorem "en-eq:3[3]": \<open>\<diamond>x\<^sub>1x\<^sub>2x\<^sub>3[F] \<equiv> x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
using "T\<diamond>" "derived-S5-rules:2"[OF "pre-en-eq:1[3]"] "\<equiv>I" by blast
AOT_theorem "en-eq:3[4]": \<open>\<diamond>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<equiv> x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
using "T\<diamond>" "derived-S5-rules:2"[OF "pre-en-eq:1[4]"] "\<equiv>I" by blast
AOT_theorem "en-eq:4[1]":
\<open>(x\<^sub>1[F] \<equiv> y\<^sub>1[G]) \<equiv> (\<box>x\<^sub>1[F] \<equiv> \<box>y\<^sub>1[G])\<close>
apply (rule "\<equiv>I"; rule "\<rightarrow>I"; rule "\<equiv>I"; rule "\<rightarrow>I")
using "qml:2"[axiom_inst, THEN "\<rightarrow>E"] "\<equiv>E"(1,2) "en-eq:2[1]" by blast+
AOT_theorem "en-eq:4[2]":
\<open>(x\<^sub>1x\<^sub>2[F] \<equiv> y\<^sub>1y\<^sub>2[G]) \<equiv> (\<box>x\<^sub>1x\<^sub>2[F] \<equiv> \<box>y\<^sub>1y\<^sub>2[G])\<close>
apply (rule "\<equiv>I"; rule "\<rightarrow>I"; rule "\<equiv>I"; rule "\<rightarrow>I")
using "qml:2"[axiom_inst, THEN "\<rightarrow>E"] "\<equiv>E"(1,2) "en-eq:2[2]" by blast+
AOT_theorem "en-eq:4[3]":
\<open>(x\<^sub>1x\<^sub>2x\<^sub>3[F] \<equiv> y\<^sub>1y\<^sub>2y\<^sub>3[G]) \<equiv> (\<box>x\<^sub>1x\<^sub>2x\<^sub>3[F] \<equiv> \<box>y\<^sub>1y\<^sub>2y\<^sub>3[G])\<close>
apply (rule "\<equiv>I"; rule "\<rightarrow>I"; rule "\<equiv>I"; rule "\<rightarrow>I")
using "qml:2"[axiom_inst, THEN "\<rightarrow>E"] "\<equiv>E"(1,2) "en-eq:2[3]" by blast+
AOT_theorem "en-eq:4[4]":
\<open>(x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<equiv> y\<^sub>1y\<^sub>2y\<^sub>3y\<^sub>4[G]) \<equiv> (\<box>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<equiv> \<box>y\<^sub>1y\<^sub>2y\<^sub>3y\<^sub>4[G])\<close>
apply (rule "\<equiv>I"; rule "\<rightarrow>I"; rule "\<equiv>I"; rule "\<rightarrow>I")
using "qml:2"[axiom_inst, THEN "\<rightarrow>E"] "\<equiv>E"(1,2) "en-eq:2[4]" by blast+
AOT_theorem "en-eq:5[1]":
\<open>\<box>(x\<^sub>1[F] \<equiv> y\<^sub>1[G]) \<equiv> (\<box>x\<^sub>1[F] \<equiv> \<box>y\<^sub>1[G])\<close>
apply (rule "\<equiv>I"; rule "\<rightarrow>I")
using "en-eq:4[1]"[THEN "\<equiv>E"(1)] "qml:2"[axiom_inst, THEN "\<rightarrow>E"]
apply blast
using "sc-eq-box-box:4"[THEN "\<rightarrow>E", THEN "\<rightarrow>E"]
"&I"[OF "pre-en-eq:1[1]"[THEN RN], OF "pre-en-eq:1[1]"[THEN RN]]
by blast
AOT_theorem "en-eq:5[2]":
\<open>\<box>(x\<^sub>1x\<^sub>2[F] \<equiv> y\<^sub>1y\<^sub>2[G]) \<equiv> (\<box>x\<^sub>1x\<^sub>2[F] \<equiv> \<box>y\<^sub>1y\<^sub>2[G])\<close>
apply (rule "\<equiv>I"; rule "\<rightarrow>I")
using "en-eq:4[2]"[THEN "\<equiv>E"(1)] "qml:2"[axiom_inst, THEN "\<rightarrow>E"]
apply blast
using "sc-eq-box-box:4"[THEN "\<rightarrow>E", THEN "\<rightarrow>E"]
"&I"[OF "pre-en-eq:1[2]" Copyright (C)20042006RedHat,IncAllrights reserved.
by blast
AOT_theorem"n-eq:53]:
(x<sub\^sub>x\^sub>3F \equiv y<^uby<sub>2\sub[])\<equiv>(<box>\^sub>x\<sub2\^sub>3[]\<equiv>\box>\^sub>y<^sub>2y<^sub[G)\close>
java.lang.StringIndexOutOfBoundsException: Range [7, 6) out of bounds for length 43
*
s-box-box:"THEN"<>E" THEN "<rightarrowE]
&[ -1]T ]OFpre-eneq13"THENRN]java.lang.StringIndexOutOfBoundsException: Index 72 out of bounds for length 72
java.lang.StringIndexOutOfBoundsException: Range [13, 11) out of bounds for length 25
<>x<sub1x\sub2x\^3\<>F] \<equiv \^1\^>y<^ub3\^sub>4[G] <equiv \boxx<sub1\^sub>x\<^sub>x<sub4F < \<ox>y<^1y\^2y\^>y<^ub4[]\<lose
apply (rule "\<equiv>I"; rule "\<rightarrow>I")
using "en-eq:4[4]"[THEN "\<equiv>E"(1)] "qml:2"[axiom_inst, THEN "\<rightarrow>E"]
apply blast
box[ \E "rightarrow>E"
"I[F eq14" RN eq14"THENRN]
by blast
AOT_theorem "en-eq:6[1]":
\<open>(x\<^sub>1[F] \<equiv> y\<^sub>1[G]) \<equiv> \<box>(x\<^sub>1[F] \<equiv> y\<^sub>1[G])\<close>
using "en-eq:5[1]"[symmetric] "en-eq:4[1]" "\<equiv>E"(5) by fast
AOT_theorem "en-eq:6[2]":
\<open>(x\<^sub>1x\<^sub>2[F] \<equiv> y\<^sub>1y\<^sub>2[G]) \<equiv> \<box>(x\<^sub>1x\<^sub>2[F] \<equiv> y\<^sub>1y\<^sub>2[G])\<close>
using "en-eq:5[2]"[symmetric] "en-eq:4[2]" "\<equiv>E"(5) by fast
AOT_theorem "en-eq:6[3]":
\<open>(x\<^sub>1x\<^sub>2x\<^sub>3[F] \<equiv> y\<^sub>1y\<^sub>2y\<^sub>3[G]) \<equiv> \<box>(x\<^sub>1x\<^sub>2x\<^sub>3[F] \<equiv> y\<^sub>1y\<^sub>2y\<^sub>3[G])\<close>
using "en-eq:5[3]"[symmetric] "en-eq:4[3]" "\<equiv>E"(5) by fast
AOT_theorem "en-eq:6[4]":
\<open>(x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<equiv> y\<^sub>1y\<^sub>2y\<^sub>3y\<^sub>4[G]) \<equiv> \<box>(x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<equiv> y\<^sub>1y\<^sub>2y\<^sub>3y\<^sub>4[G])\<close>
using "en-eq:5[4]"[symmetric] "en-eq:4[4]" "\<equiv>E"(5) by fast
AOT_theorem "en-eq:7[1]": \<open>\<not>x\<^sub>1[F] \<equiv> \<box>\<not>x\<^sub>1[F]\<close>
using "pre-en-eq:2[1]" "qml:2"[axiom_inst] "\<equiv>I" by blast
AOT_theorem "en-eq:7[2]": \<open>\<not>x\<^sub>1x\<^sub>2[F] \<equiv> \<box>\<not>x\<^sub>1x\<^sub>2[F]\<close>
using "pre-en-eq:2[2]" "qml:2"[axiom_inst] "\<equiv>I" by blast
AOT_theorem "en-eq:7[3]": \<open>\<not>x\<^sub>1x\<^sub>2x\<^sub>3[F] \<equiv> \<box>\<not>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
using "pre-en-eq:2[3]" "qml:2"[axiom_inst] "\<equiv>I" by blast
AOT_theorem "en-eq:7[4]": \<open>\<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<equiv> \<box>\<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
using "pre-en-eq:2[4]" "qml:2"[axiom_inst] "\<equiv>I" by blast
AOT_theorem "en-eq:8[1]": \<open>\<diamond>\<not>x\<^sub>1[F] \<equiv> \<not>x\<^sub>1[F]\<close>
using "en-eq:2[1]"[THEN "oth-class-taut:4:b"[THEN "\<equiv>E"(1)]]
"KBasic:11" "\<equiv>E"(5)[symmetric] by blast
AOT_theorem "en-eq:8[2]": \<open>\<diamond>\<not>x\<^sub>1x\<^sub>2[F] \<equiv> \<not>x\<^sub>1x\<^sub>2[F]\<close>
using "en-eq:2[2]"[THEN "oth-class-taut:4:b"[THEN "\<equiv>E"(1)]]
"KBasic:11" "\<equiv>E"(5)[symmetric] by blast
AOT_theorem "en-eq:8[3]": \<open>\<diamond>\<not>x\<^sub>1x\<^sub>2x\<^sub>3[F] \<equiv> \<not>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
using "en-eq:2[3]"[THEN "oth-class-taut:4:b"[THEN "\<equiv>E"(1)]]
"KBasic:11" "\<equiv>E"(5)[symmetric] by blast
AOT_theorem "en-eq:8[4]": \<open>\<diamond>\<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<equiv> \<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
using "en-eq:2[4]"[THEN "oth-class-taut:4:b"[THEN "\<equiv>E"(1)]]
"KBasic:11" "\<equiv>E"(5)[symmetric] by blast
AOT_theorem "en-eq:9[1]": \<open>\<diamond>\<not>x\<^sub>1[F] \<equiv> \<box>\<not>x\<^sub>1[F]\<close>
using "en-eq:7[1]" "en-eq:8[1]" "\<equiv>E"(5) by blast
AOT_theorem "en-eq:9[2]": \<open>\<diamond>\<not>x\<^sub>1x\<^sub>2[F] \<equiv> \<box>\<not>x\<^sub>1x\<^sub>2[F]\<close>
using "en-eq:7[2]" "en-eq:8[2]" "\<equiv>E"(5) by blast
AOT_theorem "en-eq:9[3]": \<open>\<diamond>\<not>x\<^sub>1x\<^sub>2x\<^sub>3[F] \<equiv> \<box>\<not>x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
using "en-eq:7[3]" "en-eq:8[3]" "\<equiv>E"(5) by blast
AOT_theorem "en-eq:9[4]": \<open>\<diamond>\<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<equiv> \<box>\<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
using "en-eq:7[4]" "en-eq:8[4]" "\<equiv>E"(5) by blast
AOT_theorem "en-eq:10[1]": \<open>\<^bold>\<A>x\<^sub>1[F] \<equiv> x\<^sub>1[F]\<close>
by (metis "Act-Sub:3" "deduction-theorem" "\<equiv>I" "\<equiv>E"(1)
"nec-imp-act" "en-eq:3[1]" "pre-en-eq:1[1]")
AOT_theorem "en-eq:10[2]": \<open>\<^bold>\<A>x\<^sub>1x\<^sub>2[F] \<equiv> x\<^sub>1x\<^sub>2[F]\<close>
by (metis "Act-Sub:3" "deduction-theorem" "\<equiv>I" "\<equiv>E"(1)
"nec-imp-act" "en-eq:3[2]" "pre-en-eq:1[2]")
AOT_theorem "en-eq:10[3]": \<open>\<^bold>\<A>x\<^sub>1x\<^sub>2x\<^sub>3[F] \<equiv> x\<^sub>1x\<^sub>2x\<^sub>3[F]\<close>
by (metis "Act-Sub:3" "deduction-theorem" "\<equiv>I" "\<equiv>E"(1)
"nec-imp-act" "en-eq:3[3]" "pre-en-eq:1[3]")
AOT_theorem "en-eq:10[4]": \<open>\<^bold>\<A>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<equiv> x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F]\<close>
by (metis "Act-Sub:3" "deduction-theorem" "\<equiv>I" "\<equiv>E"(1)
"nec-imp-act" "en-eq:3[4]" "pre-en-eq:1[4]")
AOT_theorem "oa-facts:1": \<open>O!x \<rightarrow> \<box>O!x\<close>
proof(rule "\<rightarrow>I")
AOT_modally_strict {
AOT_have \<open>[\<lambda>x \<diamond>E!x]x \<equiv> \<diamond>E!x\<close>
by (rule "lambda-predicates:2"[axiom_inst, THEN "\<rightarrow>E"]) "cqt:2"
} note \<theta> = this
AOT_assume \<open>O!x\<close>
AOT_hence \<open>[\<lambda>x \<diamond>E!x]x\<close>
by (rule "=\<^sub>d\<^sub>fE"(2)[OF AOT_ordinary, rotated 1]) "cqt:2"
AOT_hence \<open>\<diamond>E!x\<close> using \<theta>[THEN "\<equiv>E"(1)] by blast
AOT_hence \<open>\<box>\<diamond>E!x\<close> using "qml:3"[axiom_inst, THEN "\<rightarrow>E"] by blast
AOT_hence \<open>\<box>[\<lambda>x \<diamond>E!x]x\<close>
by (AOT_subst \<open>[\<lambda>x \<diamond>E!x]x\<close> \<open>\<diamond>E!x\<close>)
(auto simp: \<theta>)
AOT_thus \<open>\<box>O!x\<close>
by (rule "=\<^sub>d\<^sub>fI"(2)[OF AOT_ordinary, rotated 1]) "cqt:2"
qed
AOT_theorem "oa-facts:2": \<open>A!x \<rightarrow> \<box>A!x\<close>
proof(rule "\<rightarrow>I")
AOT_modally_strict {
AOT_have \<open>[\<lambda>x \<not>\<diamond>E!x]x \<equiv> \<not>\<diamond>E!x\<close>
by (rule "lambda-predicates:2"[axiom_inst, THEN "\<rightarrow>E"]) "cqt:2"
} note \<theta> = this
AOT_assume \<open>A!x\<close>
AOT_hence \<open>[\<lambda>x \<not>\<diamond>E!x]x\<close>
by (rule "=\<^sub>d\<^sub>fE"(2)[OF AOT_abstract, rotated 1]) "cqt:2"
AOT_hence \<open>\<not>\<diamond>E!x\<close> using \<theta>[THEN "\<equiv>E"(1)] by blast
AOT_hence \<open>\<box>\<not>E!x\<close> using "KBasic2:1"[THEN "\<equiv>E"(2)] by blast
AOT_hence \<open>\<box>\<box>\<not>E!x\<close> using "4"[THEN "\<rightarrow>E"] by blast
AOT_hence \<open>\<box>\<not>\<diamond>E!x\<close>
using "KBasic2:1"
by (AOT_subst (reverse) \<open>\<not>\<diamond>E!x\<close> \<open>\<box>\<not>E!x\<close>) blast
AOT_hence \<open>\<box>[\<lambda>x \<not>\<diamond>E!x]x\<close>
by (AOT_subst \<open>[\<lambda>x \<not>\<diamond>E!x]x\<close> \<open>\<not>\<diamond>E!x\<close>)
(auto simp: \<theta>)
AOT_thus \<open>\<box>A!x\<close>
by (rule "=\<^sub>d\<^sub>fI"(2)[OF AOT_abstract, rotated 1]) "cqt:2[lambda]"
qed
AOT_theorem "oa-facts:3": \<open>\<diamond>O!x \<rightarrow> O!x\<close>
using "oa-facts:1" "B\<diamond>" "RM\<diamond>" "Hypothetical Syllogism" by blast
AOT_theorem "oa-facts:4": \<open>\<diamond>A!x \<rightarrow> A!x\<close>
using "oa-facts:2" "B\<diamond>" "RM\<diamond>" "Hypothetical Syllogism" by blast
AOT_theorem "oa-facts:5": \<open>\<diamond>O!x \<equiv> \<box>O!x\<close>
by (meson "Act-Sub:3" "Hypothetical Syllogism" "\<equiv>I" "nec-imp-act"
"oa-facts:1" "oa-facts:3")
AOT_theorem "oa-facts:6": \<open>\<diamond>A!x \<equiv> \<box>A!x\<close>
by (meson "Act-Sub:3" "Hypothetical Syllogism" "\<equiv>I" "nec-imp-act"
"oa-facts:2" "oa-facts:4")
AOT_theorem "oa-facts:7": \<open>O!x \<equiv> \<^bold>\<A>O!x\<close>
by (meson "Act-Sub:3" "Hypothetical Syllogism" "\<equiv>I" "nec-imp-act"
"oa-facts:1" "oa-facts:3")
AOT_theorem "oa-facts:8": \<open>A!x \<equiv> \<^bold>\<A>A!x\<close>
by (meson "Act-Sub:3" "Hypothetical Syllogism" "\<equiv>I" "nec-imp-act"
"oa-facts:2" "oa-facts:4")
subsection\<open>The Theory of Relations\<close>
text\<open>\label{PLM: 9.10}\<close>
AOT_theorem "beta-C-meta":
\<open>[\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n, \<nu>\<^sub>1...\<nu>\<^sub>n}]\<down> \<rightarrow>
([\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n, \<nu>\<^sub>1...\<nu>\<^sub>n}]\<nu>\<^sub>1...\<nu>\<^sub>n \<equiv> \<phi>{\<nu>\<^sub>1...\<nu>\<^sub>n, \<nu>\<^sub>1...\<nu>\<^sub>n})\<close>
using "lambda-predicates:2"[axiom_inst] by blast
AOT_theorem "beta-C-cor:1":
\<open>(\<forall>\<nu>\<^sub>1...\<forall>\<nu>\<^sub>n([\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n, \<nu>\<^sub>1...\<nu>\<^sub>n}]\<down>)) \<rightarrow>
\<forall>\<nu>\<^sub>1...\<forall>\<nu>\<^sub>n ([\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n, \<nu>\<^sub>1...\<nu>\<^sub>n}]\<nu>\<^sub>1...\<nu>\<^sub>n \<equiv> \<phi>{\<nu>\<^sub>1...\<nu>\<^sub>n, \<nu>\<^sub>1...\<nu>\<^sub>n})\<close>
apply (rule "cqt-basic:14"[where 'a='a, THEN "\<rightarrow>E"])
using "beta-C-meta" "\<forall>I" by fast
AOT_theorem "beta-C-cor:2":
\<open>[\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<down> \<rightarrow>
\<forall>\<nu>\<^sub>1...\<forall>\<nu>\<^sub>n ([\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<nu>\<^sub>1...\<nu>\<^sub>n \<equiv> \<phi>{\<nu>\<^sub>1...\<nu>\<^sub>n})\<close>
apply (rule "\<rightarrow>I"; rule "\<forall>I")
using "beta-C-meta"[THEN "\<rightarrow>E"] by fast
(* TODO: add better syntax parsing for INSTANCE_OF_CQT_2 *)
theorem "beta-C-cor:3":
assumes \<open>\<And>\<nu>\<^sub>1\<nu>\<^sub>n. AOT_instance_of_cqt_2 (\<phi> (AOT_term_of_var \<nu>\<^sub>1\<nu>\<^sub>n))\<close>
shows \<open>[v \<Turnstile> \<forall>\<nu>\<^sub>1...\<forall>\<nu>\<^sub>n ([\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<nu>\<^sub>1...\<nu>\<^sub>n, \<mu>\<^sub>1...\<mu>\<^sub>n}]\<nu>\<^sub>1...\<nu>\<^sub>n \<equiv>
\<phi>{\<nu>\<^sub>1...\<nu>\<^sub>n, \<nu>\<^sub>1...\<nu>\<^sub>n})]\<close>
using "cqt:2[lambda]"[axiom_inst, OF assms]
"beta-C-cor:1"[THEN "\<rightarrow>E"] "\<forall>I" by fast
AOT_theorem "betaC:1:a": \<open>[\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<kappa>\<^sub>1...\<kappa>\<^sub>n \<^bold>\<turnstile>\<^sub>\<box> \<phi>{\<kappa>\<^sub>1...\<kappa>\<^sub>n}\<close>
proof -
AOT_modally_strict {
AOT_assume \<open>[\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<kappa>\<^sub>1...\<kappa>\<^sub>n\<close>
moreover AOT_have \<open>[\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<down>\<close> | | |