| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/AOT/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 542 kB |
|
Impressum AOT_PLM.thy
Interaktion und
|
|
|
(*<*) 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 phi = hd (Term.add_vars (Thm.prop_of allthm) []) allthm = Drule.instantiate_normalize (TVars.empty, Vars.make [(phi,trm)]) allth 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 blas 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↓ & 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↓ & [λ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↓ & [λ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 leng java.lang.StringIndexOutOfBoundsException: Range [8, 7) out of bounds for length proof java.lang.StringIndexOutOfBoundsException: Range [12, 10) out of bounds for leng by (rule GEN) (metis "id-eq:1") AOT_thus \openτ = τ using assms "\<ll qed AOT_theorem "rule=I[java.lang.StringIndexOutOfBoundsException: Range [32, 31) ou 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 ad 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_in "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_in "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_in →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.s "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) = "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_in "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_in "cqt:5:b[4]"[axiom_inst] "→I" "∃ java.lang.StringIndexOutOfBoundsException: Range [12, 11) out of bounds for leng \open([Π>kappa> \or> κ1κ2κ3κ4[Π]) → ∃β (β = κ2) by (metis "rule=I:1" "&E" "∨E"(1) "cqt:5:a[4]"[axiom_in "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_in "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_in 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 ♯ (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 (rule "→I") AOT_assume ‹τsection ‹ moreover AOT_have ‹∀\Rig> v 🚫 \>s A ix ) 🚫 java.lang.StringIndexOutOfBoundsException: Range [23, 22) out of bounds for leng using "∀E" by blast "term-out:3": ‹(φ{α} & ∀β(φ{β} → β = α)) ≡ ∀β(φ{ apply (rule "≡I"; rule "→I") java.lang.StringIndexOutOfBoundsException: Range [9, 8) out of bounds for length 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 leng (‹∃!_...∃!_ _› [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]c › 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 leng "uiquenes:2: \open\<!alpha> \ \e>\al>\fo>\be>(🚫 (rule "≡I"; rule "→I") AOT_assume ‹∃!α φ{α}› AOT_hence ‹∃α (φ{α} & ∀βmoreover have "c[z::=V_var cb]cv 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 b using "instantiation"[rotated] by blast AOT_hence ‹∀βultima show "c[xa:=va]\^sub>v = ca[xa::=va]cv[za::=V_var cb]cv" by s 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 leng 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_ (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 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 (simp add: " -conj-act:4" "∀I") "closure-act:3": ‹\A∀ java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "b "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 | T 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 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_neut (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 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 leng 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 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.sim "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 = 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 leng by (metis "rule=I:1" "existential:1") java.lang.StringIndexOutOfBoundsException: Range [42, 41) out of bounds for leng 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_ using "≡sharp> (x,v) ==> subst_sv (AS_var u τ v' s) x v = AS_var u (subst_tv τ 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) & &psi 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 leng 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 "m 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_t 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, 1 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 leng (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 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 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 leng 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 "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_ (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' 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 = 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 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_ 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 using b "∀E" by blast AOT_have ‹\Aφ{b} & ∀z(\Aφ{z} → z = b)› and j: ‹ subst_ using g "&E" by blast+ AOT_hence ‹b = \ιx φ{x}› using h "≡defer 11 (* Sometim defering hard goals to the end makes it easier t 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 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 leng 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 blas 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, 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 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 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>\< 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))\<cl 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))\<cl 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\<clos 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\<clos 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>\< 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>\< 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> \<righta 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> \<righta 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> \<right 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> \<right 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>(\<p 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>(\<n 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>\< proof - AOT_have \<open>\<diamond>(\<phi> \<or> \<psi>) \<equiv> \<diamond>\<not>(\<not>\<phi> & \<not>\<psi>)\<clos 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>\<bo 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> & 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> \<rightar 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>\<cl ()\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> 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>) si 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> \< 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" "\<rightar 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 bl 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>\< by (metis "Act-Sub:2" "Act-Sub:3" "Act-Sub:4" "\<rightarrow>I" "\<equiv>E"(1) "\<equiv>E"(2) " 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>)\<clo 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> 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-e 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> &&n proof - AOT_have \<open>\<diamond>(\<phi> & \<diamond>\<psi>) \<equiv> \<diamond>\<not>(\<not>\<phi> \<or> \<not>\<d by (AOT_subst \<open>\<phi> & \<diamond>\<psi>\<close> \<open>\<not>(\<not>\<phi> \<or> \<not>\<diamond>\<ps (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>\<bo (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> & 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> & 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>\<ph proof (rule "\<equiv>I") AOT_modally_strict { AOT_have \<open>\<box>(\<phi> \<rightarrow> \<box>\<psi>) \<rightarrow> (\<diamond>\<phi> \<rightarrow> \<ps by (meson "KBasic:13" "B\<diamond>" "Hypothetical Syllogism" "\<rightarrow>I") } AOT_hence \<open>\<box>\<box>(\<phi> \<rightarrow> \<box>\<psi>) \<rightarrow> \<box>(\<diamond>\<phi> \<righ by (rule RM) AOT_thus \<open>\<box>(\<phi> \<rightarrow> \<box>\<psi>) \<rightarrow> \<box>(\<diamond>\<phi> \<rightarro using "4" "Hypothetical Syllogism" by blast next AOT_modally_strict { AOT_have \<open>\<box>(\<diamond>\<phi> \<rightarrow> \<psi>) \<rightarrow> (\<phi> \<rightarrow> \<box>\<ps by (meson "B" "Hypothetical Syllogism" "\<rightarrow>I" "qml:1"[axiom_inst]) } AOT_hence \<open>\<box>\<box>(\<diamond>\<phi> \<rightarrow> \<psi>) \<rightarrow> \<box>(\<phi> \<rightarr by (rule RM) AOT_thus \<open>\<box>(\<diamond>\<phi> \<rightarrow> \<psi>) \<rightarrow> \<box>(\<phi> \<rightarrow> \<bo 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>\< 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>\< using assms by (rule "RM:2[prem]") AOT_thus \<open>\<box>\<Gamma> \<^bold>\<turnstile>\<^sub>\<box> \<diamond>\<phi> \<rightarrow> \<psi>\<clos using "B\<diamond>" "Hypothetical Syllogism" by blast qed AOT_theorem "BFs:1": \<open>\<forall>\<alpha> \<box>\<phi>{\<alpha>} \<rightarrow> \<box>\<forall>\<alph proof - AOT_modally_strict { AOT_have \<open>\<diamond>\<forall>\<alpha> \<box>\<phi>{\<alpha>} \<rightarrow> \<diamond>\<box>\<phi>{\<a using "cqt-orig:3" by (rule "RM\<diamond>") AOT_hence \<open>\<diamond>\<forall>\<alpha> \<box>\<phi>{\<alpha>} \<rightarrow> \<forall>\<alpha> \<phi>{ 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> \<bo proof - AOT_have \<open>\<box>\<forall>\<alpha> \<phi>{\<alpha>} \<rightarrow> \<box>\<phi>{\<alpha>}\<close> for \<a 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>\<alph proof(rule "\<rightarrow>I") AOT_modally_strict { AOT_have \<open>\<box>\<forall>\<alpha> \<not>\<phi>{\<alpha>} \<equiv> \<forall>\<alpha> \<box>\<not>\<phi>{\<a 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> \<p 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>\<fo 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>{\<a (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> fo qed lemmas "BF\<diamond>" = "BFs:3" AOT_theorem "BFs:4": \<open>\<exists>\<alpha> \<diamond>\<phi>{\<alpha>} \<rightarrow> \<diamond>\<exi 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> fo moreover AOT_have \<open>\<forall>\<alpha> \<box>\<not>\<phi>{\<alpha>} \<equiv> \<box>\<forall>\<alpha> \<no 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>\<ph apply (simp add: "conventions:4" "\<equiv>Df") apply (AOT_subst \<open>\<not>\<not>\<forall>\<alpha> \<not>\<phi>{\<alpha>}\<close> \<open>\<forall>\<alph 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>\<exi 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>\<e proof - AOT_have \<open>\<phi>{\<tau>}, \<tau>\<down> \<^bold>\<turnstile>\<^sub>\<box> \<exists>\<alpha> \<phi>{\<alp AOT_thus \<open>\<box>\<phi>{\<tau>}, \<box>\<tau>\<down> \<^bold>\<turnstile>\<^sub>\<box> \<box>\<exists>\<al using "RN[prem]"[where \<Gamma>="{\<phi> \<tau>, \<guillemotleft>\<tau>\<down>\<guillemotright>}", 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> \<for proof - AOT_have \<open>\<forall>\<alpha> (\<diamond>\<forall>\<alpha> \<phi>{\<alpha>} \<rightarrow> \<diamond>\< by (simp add: "RM\<diamond>" "cqt-orig:3" "\<forall>I") AOT_thus \<open>\<diamond>\<forall>\<alpha> \<phi>{\<alpha>} \<rightarrow> \<forall>\<alpha> \<diamond>\<p 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>(\<ex apply (rule "RM:2") by (metis (no_types, lifting) "\<exists>E" "&I" "&E"(1) "&E"(2) "\<rightarrow>I" "\<e AOT_theorem "sign-S5-thm:4": \<open>\<diamond>\<exists>\<alpha> (\<phi>{\<alpha>} & \<psi>{\<alp 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>\<alp 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>(\<p 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>\<clo 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>\<cl 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> \<bet 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" "\<rightarr AOT_theorem "id-nec2:4": \<open>\<diamond>\<alpha> = \<beta> \<rightarrow> \<box>\<alpha> = \<beta>\<clos 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> 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>\<p 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> 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>\< 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> 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>)) \<rightarro proof(rule "\<rightarrow>I"; rule "\<rightarrow>I") AOT_assume \<theta>: \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>) & \<box>(\<psi> \<rightarrow> \<box> 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> \<eq 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>)) \<rightarro proof (rule "\<rightarrow>I") AOT_assume \<open>(\<box>(\<phi> \<rightarrow> \<box>\<phi>) & \<box>(\<psi> \<rightarrow> \<box>\<psi>)) AOT_hence \<open>\<box>(\<box>(\<phi> \<rightarrow> \<box>\<phi>) & \<box>(\<psi> \<rightarrow> \<box>\<ps 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> 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> 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>)\<clo 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>))\<clo qed AOT_theorem "sc-eq-box-box:6": \<open>\<box>(\<phi> \<rightarrow> \<box>\<phi>) \<rightarrow> ((\<phi> 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> 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>\< 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} \<rig 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 = using "&I" by blast AOT_hence \<open>\<exists>x (\<^bold>\<A>\<phi>{x} & \<forall>y (\<^bold>\<A>\<phi>{y} \<rightarrow> y = 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 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> 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)\<clos 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>\<clos 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>!\<al proof - AOT_have \<open>\<^bold>\<A>\<exists>!\<alpha> \<phi>{\<alpha>} \<equiv> \<^bold>\<A>\<exists>\<alpha>\<foral by (AOT_subst \<open>\<exists>!\<alpha> \<phi>{\<alpha>}\<close> \<open>\<exists>\<alpha>\<forall>\<beta> ( (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> \< by (simp add: "Act-Basic:10") also AOT_have \<open>\<dots> \<equiv> \<exists>\<alpha>\<forall>\<beta> \<^bold>\<A>(\<phi>{\<beta>} \<equiv> \< by (AOT_subst \<open>\<^bold>\<A>\<forall>\<beta> (\<phi>{\<beta>} \<equiv> \<beta> = \<alpha>)\<close> \<open>\< (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> \< 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> \< by (AOT_subst (reverse) \<open>\<^bold>\<A>\<beta> = \<alpha>\<close> \<open>\<beta> = \<alpha>\<close> for: \< (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> by (AOT_subst \<open>\<^bold>\<A>\<exists>!x \<phi>{x}\<close> \<open>\<exists>!x \<^bold>\<A>\<phi>{x}\<clo (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[ 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\<^su 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 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] 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 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 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 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]\<clo 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>1 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"< qed AOT_theorem "pre-en-eq:2[3]": \<open>\<not>x\<^sub>1x\<^sub>2x\<^sub>3[F] \<rightarrow> \<box>\<not> 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] qed AOT_theorem "pre-en-eq:2[4]": \<open>\<not>x\<^sub>1x\<^sub>2x\<^sub>3x\<^sub>4[F] \<rightarrow> \< 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\<^ 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 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\< 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\< 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\<^ 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\<^ 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]\<cl 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> 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> 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])\<clos 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] \<equi 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 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]) \<equi 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])\< 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] \< 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>\ java.lang.StringIndexOutOfBoundsException: Range [7, 6) out of bounds for length * s-box-box:"THEN"<>E" THEN "<rightarrowE] &[ -1]T ]OFpre-eneq13"THENRN]java.lang.StringIndexOutOfBoundsException: Index 7 java.lang.StringIndexOutOfBoundsException: Range [13, 11) out of bounds for leng <>x<sub1x\sub2x\^3\<>F] \<equiv \^1\^>y<^ub3\^sub>4[G] <equiv \boxx<sub1\^sub>x\<^sub>x<sub4F < \<ox>y<^1 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] \<equi 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 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]) \<equi 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 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\< 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\< 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\<^su 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\<^su 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> \<n 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]\<clos 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 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 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> \<b 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]\<c 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\<^su 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\<^su 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 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>\<^su ([\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n, \<nu>\<^sub>1...\<nu>\<^sub>n}] 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>\< \<forall>\<nu>\<^sub>1...\<forall>\<nu>\<^sub>n ([\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1. 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. 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> shows \<open>[v \<Turnstile> \<forall>\<nu>\<^sub>1...\<forall>\<nu>\<^sub>n ([\<lambda>\<mu>\<^sub>1...\<m \<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>\<^s proof - AOT_modally_strict { AOT_assume \<open>[\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<kappa>\<^ moreover AOT_have \<open>[\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<d using calculation "cqt:5:a"[axiom_inst, THEN "\<rightarrow>E"] "&E" by blast+ ultimately AOT_show \<open>\<phi>{\<kappa>\<^sub>1...\<kappa>\<^sub>n}\<close> using "beta-C-cor:2"[THEN "\<rightarrow>E", THEN "\<forall>E"(1), THEN "\<equiv>E"(1)] by blas } qed AOT_theorem "betaC:1:b": \<open>\<not>\<phi>{\<kappa>\<^sub>1...\<kappa>\<^sub>n} \<^bold>\<turnstil using "betaC:1:a" "raa-cor:3" by blast lemmas "\<beta>\<rightarrow>C" = "betaC:1:a" "betaC:1:b" AOT_theorem "betaC:2:a": \<open>[\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<down>, \<kappa>\<^sub>1 [\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<kappa>\<^sub>1...\<kappa>\<^ proof - AOT_modally_strict { AOT_assume 1: \<open>[\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<down>\< and 2: \<open>\<kappa>\<^sub>1...\<kappa>\<^sub>n\<down>\<close> and 3: \<open>\<phi>{\<kappa>\<^sub>1...\<kappa>\<^sub>n}\<close> AOT_hence \<open>[\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<kappa>\<^s using "beta-C-cor:2"[THEN "\<rightarrow>E", OF 1, THEN "\<forall>E"(1), THEN "\<equiv>E"(2)] by blast } AOT_thus \<open>[\<lambda>\<mu>\<^sub>1...\<mu>\<^sub>n \<phi>{\<mu>\<^sub>1...\<mu>\<^sub>n}]\<down>, \<kap |