Theory TAO_10_PossibleWorlds

theory TAO_10_PossibleWorlds
imports TAO_9_PLM
(*<*)
theory TAO_10_PossibleWorlds
imports TAO_9_PLM
begin
(*>*)

section‹Possible Worlds›
text‹\label{TAO_PossibleWorlds}›

locale PossibleWorlds = PLM
begin

subsection‹Definitions›
text‹\label{TAO_PossibleWorlds_Definitions}›

  definition Situation where
    "Situation x ≡ ⦇A!,x⦈ & ( F. ⦃x,F⦄  Propositional F)"

  definition EncodeProposition (infixl "Σ" 70) where
    "xΣp ≡ ⦇A!,x⦈ & ⦃x, λ x . p⦄"
  definition TrueInSituation (infixl "" 10) where
    "x  p ≡ Situation x & xΣp"
  definition PossibleWorld where
    "PossibleWorld x ≡ Situation x & ( p . xΣp  p)"

subsection‹Auxiliary Lemmas›
text‹\label{TAO_PossibleWorlds_Aux}›

  lemma possit_sit_1:
    "[Situation (xP)  (Situation (xP)) in v]"
    proof (rule "I"; rule CP)
      assume "[Situation (xP) in v]"
      hence 1: "[⦇A!,xP& ( F. ⦃xP,F⦄  Propositional F) in v]"
        unfolding Situation_def by auto
      have "[⦇A!,xP⦈ in v]"
        using 1[conj1, THEN oa_facts_2[deduction]] .
      moreover have "[( F. ⦃xP,F⦄  Propositional F) in v]"
         using 1[conj2] unfolding Propositional_def
         by (rule enc_prop_nec_2[deduction])
      ultimately show "[Situation (xP) in v]"
        unfolding Situation_def
        apply cut_tac apply (rule KBasic_3[equiv_rl])
        by (rule intro_elim_1)
    next
      assume "[Situation (xP) in v]"
      thus "[Situation (xP) in v]"
        using qml_2[axiom_instance, deduction] by auto
    qed

  lemma possworld_nec:
    "[PossibleWorld (xP)  (PossibleWorld (xP)) in v]"
    apply (rule "I"; rule CP)
     subgoal unfolding PossibleWorld_def
     apply (rule KBasic_3[equiv_rl])
     apply (rule intro_elim_1)
      using possit_sit_1[equiv_lr] "&E"(1) apply blast
     using qml_3[axiom_instance, deduction] "&E"(2) by blast
    using qml_2[axiom_instance,deduction] by auto

  lemma TrueInWorldNecc:
    "[((xP)  p)  ((xP)  p) in v]"
    proof (rule "I"; rule CP)
      assume "[xP  p in v]"
      hence "[Situation (xP) & (⦇A!,xP& ⦃xP,λx. p⦄) in v]"
        unfolding TrueInSituation_def EncodeProposition_def .
      hence "[(Situation (xP) & ⦇A!,xP⦈) & ⦃xP, λx. p⦄ in v]"
        using "&I" "&E" possit_sit_1[equiv_lr] oa_facts_2[deduction]
              encoding[axiom_instance,deduction] by metis
      thus "[((xP)  p) in v]"
        unfolding TrueInSituation_def EncodeProposition_def
        using KBasic_3[equiv_rl] "&I" "&E" by metis
    next
      assume "[(xP  p) in v]"
      thus "[xP  p in v]"
        using qml_2[axiom_instance,deduction] by auto
    qed


  lemma PossWorldAux:
    "[(⦇A!,xP& ( F . (⦃xP,F⦄  ( p . p & (F = (λ x . p))))))
        (PossibleWorld (xP)) in v]"
    proof (rule CP)
      assume DefX: "[⦇A!,xP& ( F . (⦃xP,F⦄ 
            ( p . p & (F = (λ x . p))))) in v]"
    
      have "[Situation (xP) in v]"
      proof -
        have "[⦇A!,xP⦈ in v]"
          using DefX[conj1] .
        moreover have "[(F. ⦃xP,F⦄  Propositional F) in v]"
          proof (rule "I"; rule CP)
            fix F
            assume "[⦃xP,F⦄ in v]"
            moreover have "[⦃xP,F⦄  ( p . p & (F = (λ x . p))) in v]"
              using DefX[conj2] cqt_1[axiom_instance, deduction] by auto
            ultimately have "[( p . p & (F = (λ x . p))) in v]"
              using "E"(1) by blast
            then obtain p where "[p & (F = (λ x . p)) in v]"
              by (rule "E")
            hence "[(F = (λ x . p)) in v]"
              by (rule "&E"(2))
            hence "[( p . (F = (λ x . p))) in v]"
              by PLM_solver
            thus "[Propositional F in v]"
              unfolding Propositional_def .
          qed
        ultimately show "[Situation (xP) in v]"
          unfolding Situation_def by (rule "&I")
      qed
      moreover have "[(p. xP Σ p  p) in v]"
        unfolding EncodeProposition_def
        proof (rule TBasic[deduction]; rule "I")
          fix q
          have EncodeLambda:
            "[⦃xP, λx. q⦄  ( p . p & ((λx. q) = (λ x . p))) in v]"
            using DefX[conj2] by (rule cqt_1[axiom_instance, deduction])
          moreover {
             assume "[q in v]"
             moreover have "[(λx. q) = (λ x . q) in v]"
              using id_eq_prop_prop_1 by auto
             ultimately have "[q & ((λx. q) = (λ x . q)) in v]"
               by (rule "&I")
             hence "[ p . p & ((λx. q) = (λ x . p)) in v]"
               by PLM_solver
             moreover have "[⦇A!,xP⦈ in v]"
               using DefX[conj1] .
             ultimately have "[⦇A!,xP& ⦃xP, λx. q⦄ in v]"
               using EncodeLambda[equiv_rl] "&I" by auto
          }
          moreover {
            assume "[⦇A!,xP& ⦃xP, λx. q⦄ in v]"
            hence "[⦃xP, λx. q⦄ in v]"
              using "&E"(2) by auto
            hence "[ p . p & ((λx. q) = (λ x . p)) in v]"
              using EncodeLambda[equiv_lr] by auto
            then obtain p where p_and_lambda_q_is_lambda_p:
              "[p & ((λx. q) = (λ x . p)) in v]"
              by (rule "E")
            have "[⦇(λ x . p), xP p in v]"
              apply (rule beta_C_meta_1)
              by show_proper
            hence "[⦇(λ x . p), xP⦈ in v]"
              using p_and_lambda_q_is_lambda_p[conj1] "E"(2) by auto
            hence "[⦇(λ x . q), xP⦈ in v]"
              using p_and_lambda_q_is_lambda_p[conj2, THEN id_eq_prop_prop_2[deduction]]
                l_identity[axiom_instance, deduction, deduction] by fast
            moreover have "[⦇(λ x . q), xP q in v]"
              apply (rule beta_C_meta_1) by show_proper
            ultimately have "[q in v]"
              using "E"(1) by blast
          }
          ultimately show "[⦇A!,xP& ⦃xP,λx. q⦄  q in v]"
            using "&I" "I" CP by auto
        qed
    
      ultimately show "[PossibleWorld (xP) in v]"
        unfolding PossibleWorld_def by (rule "&I")
    qed

subsection‹For every syntactic Possible World there is a semantic Possible World›
text‹\label{TAO_PossibleWorlds_SyntacticSemantic}›

  theorem SemanticPossibleWorldForSyntacticPossibleWorlds:
    "∀ x . [PossibleWorld (xP) in w] ⟶
     (∃ v . ∀ p . [(xP  p) in w] ⟷ [p in v])"
    proof
      fix x
      {
        assume PossWorldX: "[PossibleWorld (xP) in w]"
        hence SituationX: "[Situation (xP) in w]"
          unfolding PossibleWorld_def apply cut_tac by PLM_solver
        have PossWorldExpanded:
          "[⦇A!,xP& (F. ⦃xP,F⦄  (p. F = (λx. p)))
            & (p. ⦇A!,xP& ⦃xP,λx. p⦄  p) in w]"
           using PossWorldX
           unfolding PossibleWorld_def Situation_def
                     Propositional_def EncodeProposition_def .
        have AbstractX: "[⦇A!,xP⦈ in w]"
          using PossWorldExpanded[conj1,conj1] .
        
        have "[(p. ⦃xP,λx. p⦄  p) in w]"
          apply (PLM_subst_method
                 "λp. ⦇A!,xP& ⦃xP,λx. p⦄"
                 "λ p . ⦃xP,λx. p⦄")
           subgoal using PossWorldExpanded[conj1,conj1,THEN oa_facts_2[deduction]]
                   using Semantics.T6 apply cut_tac by PLM_solver
          using PossWorldExpanded[conj2] .
    
        hence "∃v. ∀p. ([⦃xP,λx. p⦄ in v])
                        = [p in v]"
         unfolding diamond_def equiv_def conj_def
         apply (simp add: Semantics.T4 Semantics.T6 Semantics.T5
                          Semantics.T8)
         by auto
    
        then obtain v where PropsTrueInSemWorld:
          "∀p. ([⦃xP,λx. p⦄ in v]) = [p in v]"
          by auto
        {
          fix p
          {
            assume "[((xP)  p) in w]"
            hence "[((xP)  p) in v]"
              using TrueInWorldNecc[equiv_lr] Semantics.T6 by simp
            hence "[Situation (xP) & (⦇A!,xP& ⦃xP,λx. p⦄) in v]"
              unfolding TrueInSituation_def EncodeProposition_def .
            hence "[⦃xP,λx. p⦄ in v]"
              using "&E"(2) by blast
            hence "[p in v]"
              using PropsTrueInSemWorld by blast
          }
          moreover {
            assume "[p in v]"
            hence "[⦃xP,λx. p⦄ in v]"
              using PropsTrueInSemWorld by blast
            hence "[(xP)  p in v]"
              apply cut_tac unfolding TrueInSituation_def EncodeProposition_def
              apply (rule "&I") using SituationX[THEN possit_sit_1[equiv_lr]]
              subgoal using Semantics.T6 by auto
              apply (rule "&I")
              subgoal using AbstractX[THEN oa_facts_2[deduction]]
                using Semantics.T6 by auto
              by assumption
            hence "[((xP)  p) in v]"
              using TrueInWorldNecc[equiv_lr] by simp
            hence "[(xP)  p in w]"
              using Semantics.T6 by simp
          }
          ultimately have "[p in v] ⟷ [(xP)  p in w]"
            by auto
        }
        hence "(∃ v . ∀ p . [p in v] ⟷ [(xP)  p in w])"
          by blast
      }
      thus "[PossibleWorld (xP) in w] ⟶
            (∃v. ∀ p . [(xP)  p in w] ⟷ [p in v])"
        by blast
    qed

subsection‹For every semantic Possible World there is a syntactic Possible World›
text‹\label{TAO_PossibleWorlds_SemanticSyntactic}›

  theorem SyntacticPossibleWorldForSemanticPossibleWorlds:
    "∀ v . ∃ x . [PossibleWorld (xP) in w] ∧
     (∀ p . [p in v] ⟷ [((xP)  p) in w])"
    proof
      fix v
      have "[x. ⦇A!,xP& ( F . (⦃xP,F⦄ 
            ( p . p & (F = (λ x . p))))) in v]"
        using A_objects[axiom_instance] by fast
      then obtain x where DefX:
        "[⦇A!,xP& ( F . (⦃xP,F⦄  ( p . p & (F = (λ x . p))))) in v]"
        by (rule "E")
      hence PossWorldX: "[PossibleWorld (xP) in v]"
        using PossWorldAux[deduction] by blast
      hence "[PossibleWorld (xP) in w]"
        using possworld_nec[equiv_lr] Semantics.T6 by auto
      moreover have "(∀ p . [p in v] ⟷ [(xP)  p in w])"
      proof
        fix q
        {
           assume "[q in v]"
           moreover have "[(λ x . q) = (λ x . q) in v]"
             using id_eq_prop_prop_1 by auto
           ultimately have "[q & (λ x . q) = (λ x . q) in v]"
             using "&I" by auto
           hence "[( p . p & ((λ x . q) = (λ x . p))) in v]"
             by PLM_solver
           hence 4: "[⦃xP, (λ x . q)⦄ in v]"
             using cqt_1[axiom_instance,deduction, OF DefX[conj2], equiv_rl]
             by blast
           have "[(xP  q) in v]"
             unfolding TrueInSituation_def apply (rule "&I")
              using PossWorldX unfolding PossibleWorld_def
              using "&E"(1) apply blast
             unfolding EncodeProposition_def apply (rule "&I")
              using DefX[conj1] apply simp
             using 4 .
          hence "[(xP  q) in w]"
            using TrueInWorldNecc[equiv_lr] Semantics.T6 by auto
        }
        moreover {
          assume "[(xP  q) in w]"
          hence "[(xP  q) in v]"
             using TrueInWorldNecc[equiv_lr] Semantics.T6
             by auto
          hence "[⦃xP, (λ x . q)⦄ in v]"
            unfolding TrueInSituation_def EncodeProposition_def
            using "&E"(2) by blast
          hence "[( p . p & ((λ x . q) = (λ x . p))) in v]"
            using cqt_1[axiom_instance,deduction, OF DefX[conj2], equiv_lr]
            by blast
          then obtain p where 4:
            "[(p & ((λ x . q) = (λ x . p))) in v]"
            by (rule "E")
          have "[⦇(λ x . p),xP p in v]"
            apply (rule beta_C_meta_1)
            by show_proper
          hence "[⦇(λ x . q),xP p in v]"
              using l_identity[where β="(λ x . q)" and α="(λ x . p)",
                               axiom_instance, deduction, deduction]
              using 4[conj2,THEN id_eq_prop_prop_2[deduction]] by meson
          hence "[⦇(λ x . q),xP⦈ in v]" using 4[conj1] "E"(2) by blast
          moreover have "[⦇(λ x . q),xP q in v]"
            apply (rule beta_C_meta_1)
            by show_proper
          ultimately have "[q in v]"
            using "E"(1) by blast
        }
        ultimately show "[q in v] ⟷ [(xP)  q in w]"
          by blast
      qed
      ultimately show "∃ x . [PossibleWorld (xP) in w]
                           ∧ (∀ p . [p in v] ⟷ [(xP)  p in w])"
        by auto
    qed
end

(*<*)
end
(*>*)