Theory TAO_98_ArtificialTheorems

(*<*)
theory TAO_98_ArtificialTheorems
imports TAO_7_Axioms
begin
(*>*)

section‹Artificial Theorems›
text‹\label{TAO_ArtificialTheorems}›

text‹
\begin{remark}
  Some examples of theorems that can be derived from the model structure, but which
  are not derivable from the deductive system PLM itself.
\end{remark}
›

locale ArtificialTheorems
begin

  lemma lambda_enc_1:
    "[⦇❙λx . ⦃x⇧^P, F⦄ ❙≡ ⦃x⇧^P, F⦄, y⇧^P⦈ in v]"
    by (auto simp: meta_defs meta_aux conn_defs forall_Π⇩₁_def)

  lemma lambda_enc_2:
    "[⦇❙λ x . ⦃y⇧^P, G⦄, x⇧^P⦈ ❙≡ ⦃y⇧^P, G⦄ in v]"
    by (auto simp: meta_defs meta_aux conn_defs forall_Π⇩₁_def)

text‹
\begin{remark}
  The following is \emph{not} a theorem and nitpick can
  find a countermodel. This is expected and important.
  If this were a theorem, the theory would become inconsistent.
\end{remark}
›

  lemma lambda_enc_3:
    "[(⦇❙λ x . ⦃x⇧^P, F⦄, x⇧^P⦈ ❙→ ⦃x⇧^P, F⦄) in v]"
    apply (simp add: meta_defs meta_aux conn_defs forall_Π⇩₁_def)
    nitpick[user_axioms, expect=genuine]
    oops ― ‹countermodel by nitpick›

text‹
\begin{remark}
  Instead the following two statements hold.
\end{remark}
›

  lemma lambda_enc_4:
    "[⦇(❙λ x . ⦃x⇧^P, F⦄), x⇧^P⦈ in v] = (∃ y . νυ y = νυ x ∧ [⦃y⇧^P, F⦄ in v])"
    by (simp add: meta_defs meta_aux)

  lemma lambda_ex:
    "[⦇(❙λ x . φ (x⇧^P)), x⇧^P⦈ in v] = (∃ y . νυ y = νυ x ∧ [φ (y⇧^P) in v])"
    by (simp add: meta_defs meta_aux)

text‹
\begin{remark}
  These statements can be translated to statements in the embedded logic.
\end{remark}
›

  lemma lambda_ex_emb:
    "[⦇(❙λ x . φ (x⇧^P)), x⇧^P⦈ ❙≡ (❙∃ y . (❙∀ F . ⦇F,x⇧^P⦈ ❙≡ ⦇F,y⇧^P⦈) ❙& φ (y⇧^P)) in v]"
    proof(rule MetaSolver.EquivI)
      interpret MetaSolver .
      {
        assume "[⦇(❙λ x . φ (x⇧^P)), x⇧^P⦈ in v]"
        then obtain y where "νυ y = νυ x ∧ [φ (y⇧^P) in v]"
          using lambda_ex by blast
        moreover hence "[(❙∀ F . ⦇F,x⇧^P⦈ ❙≡ ⦇F,y⇧^P⦈) in v]"
          apply - apply meta_solver
          by (simp add: Semantics.d⇩_κ_proper Semantics.ex1_def)
        ultimately have "[❙∃ y . (❙∀ F . ⦇F,x⇧^P⦈ ❙≡ ⦇F,y⇧^P⦈) ❙& φ (y⇧^P) in v]"
          using ExIRule ConjI by fast
      }
      moreover {
        assume "[❙∃ y . (❙∀ F . ⦇F,x⇧^P⦈ ❙≡ ⦇F,y⇧^P⦈) ❙& φ (y⇧^P) in v]"
        then obtain y where y_def: "[(❙∀ F . ⦇F,x⇧^P⦈ ❙≡ ⦇F,y⇧^P⦈) ❙& φ (y⇧^P) in v]"
          by (rule ExERule)
        hence "⋀ F . [⦇F,x⇧^P⦈ in v] = [⦇F,y⇧^P⦈ in v]"
          apply - apply (drule ConjE) apply (drule conjunct1)
          apply (drule AllE) apply (drule EquivE) by simp
        hence "[⦇makeΠ⇩₁ (λ u s w . νυ y = u),x⇧^P⦈ in v]
             = [⦇makeΠ⇩₁ (λ u s w . νυ y = u),y⇧^P⦈ in v]" by auto
        hence "νυ y = νυ x" by (simp add: meta_defs meta_aux)
        moreover have "[φ (y⇧^P) in v]" using y_def ConjE by blast
        ultimately have "[⦇(❙λ x . φ (x⇧^P)), x⇧^P⦈ in v]"
          using lambda_ex by blast
      }
      ultimately show "[⦇❙λx. φ (x⇧^P),x⇧^P⦈ in v]
          = [❙∃y. (❙∀F. ⦇F,x⇧^P⦈ ❙≡ ⦇F,y⇧^P⦈) ❙& φ (y⇧^P) in v]"
        by auto
    qed

  lemma lambda_enc_emb:
    "[⦇(❙λ x . ⦃x⇧^P, F⦄), x⇧^P⦈ ❙≡ (❙∃ y . (❙∀ F . ⦇F,x⇧^P⦈ ❙≡ ⦇F,y⇧^P⦈) ❙& ⦃y⇧^P, F⦄) in v]"
    using lambda_ex_emb by fast

text‹
\begin{remark}
  In the case of proper maps, the generalized ‹β›-conversion reduces to
  classical ‹β›-conversion.
\end{remark}
›

  lemma proper_beta:
    assumes "IsProperInX φ"
    shows "[(❙∃ y . (❙∀ F . ⦇F,x⇧^P⦈ ❙≡ ⦇F,y⇧^P⦈) ❙& φ (y⇧^P)) ❙≡ φ (x⇧^P) in v]"
  proof (rule MetaSolver.EquivI; rule)
    interpret MetaSolver .
    assume "[❙∃y. (❙∀F. ⦇F,x⇧^P⦈ ❙≡ ⦇F,y⇧^P⦈) ❙& φ (y⇧^P) in v]"
    then obtain y where y_def: "[(❙∀F. ⦇F,x⇧^P⦈ ❙≡ ⦇F,y⇧^P⦈) ❙& φ (y⇧^P) in v]" by (rule ExERule)
    hence "[⦇makeΠ⇩₁ (λ u s w . νυ y = u), x⇧^P⦈ in v] = [⦇makeΠ⇩₁ (λ u s w . νυ y = u), y⇧^P⦈ in v]"
      using EquivS AllE ConjE by blast
    hence "νυ y = νυ x" by (simp add: meta_defs meta_aux)
    thus "[φ (x⇧^P) in v]"
      using y_def[THEN ConjE[THEN conjunct2]]
            assms IsProperInX.rep_eq valid_in.rep_eq
      by blast
  next
    interpret MetaSolver .
    assume "[φ (x⇧^P) in v]"
    moreover have "[❙∀F. ⦇F,x⇧^P⦈ ❙≡ ⦇F,x⇧^P⦈ in v]" apply meta_solver by blast
    ultimately show "[❙∃y. (❙∀F. ⦇F,x⇧^P⦈ ❙≡ ⦇F,y⇧^P⦈) ❙& φ (y⇧^P) in v]"
      by (meson ConjI ExI)
  qed
      
text‹
\begin{remark}
  The following theorem is a consequence of the constructed Aczel-model, but not
  part of PLM. Separate research on possible modifications of the embedding suggest
  that this artificial theorem can be avoided by introducing a dependency on states
  for the mapping from abstract objects to special urelements.
\end{remark}
›

  lemma lambda_rel_extensional:
    assumes "[❙∀F . ⦇F,a⇧^P⦈ ❙≡ ⦇F,b⇧^P⦈ in v]"
    shows "(❙λx. ⦇R,x⇧^P,a⇧^P⦈) = (❙λx . ⦇R,x⇧^P, b⇧^P⦈)"
  proof -
    interpret MetaSolver .
    obtain F where F_def: "F = makeΠ⇩₁ (λ u s w . u = νυ a)" by auto
    have "[⦇F, a⇧^P⦈ ❙≡ ⦇F, b⇧^P⦈ in v]" using assms by (rule AllE)
    moreover have "[⦇F, a⇧^P⦈ in v]"
      unfolding F_def by (simp add: meta_defs meta_aux)
    ultimately have "[⦇F, b⇧^P⦈ in v]" using EquivE by auto
    hence "νυ a = νυ b" using F_def by (simp add: meta_defs meta_aux)
    thus ?thesis by (simp add: meta_defs meta_aux)
  qed

      
end

(*<*)
end
(*>*)