Theory TAO_98_ArtificialTheorems

theory TAO_98_ArtificialTheorems
imports TAO_7_Axioms
(*<*)
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 . ⦃xP, F⦄  ⦃xP, F⦄, yP⦈ in v]"
    by (auto simp: meta_defs meta_aux conn_defs forall_Π1_def)

  lemma lambda_enc_2:
    "[⦇λ x . ⦃yP, G⦄, xP ⦃yP, G⦄ in v]"
    by (auto simp: meta_defs meta_aux conn_defs forall_Π1_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 . ⦃xP, F⦄, xP ⦃xP, F⦄) in v]"
    apply (simp add: meta_defs meta_aux conn_defs forall_Π1_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 . ⦃xP, F⦄), xP⦈ in v] = (∃ y . νυ y = νυ x ∧ [⦃yP, F⦄ in v])"
    by (simp add: meta_defs meta_aux)

  lemma lambda_ex:
    "[⦇(λ x . φ (xP)), xP⦈ in v] = (∃ y . νυ y = νυ x ∧ [φ (yP) 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 . φ (xP)), xP ( y . ( F . ⦇F,xP ⦇F,yP⦈) & φ (yP)) in v]"
    proof(rule MetaSolver.EquivI)
      interpret MetaSolver .
      {
        assume "[⦇(λ x . φ (xP)), xP⦈ in v]"
        then obtain y where "νυ y = νυ x ∧ [φ (yP) in v]"
          using lambda_ex by blast
        moreover hence "[( F . ⦇F,xP ⦇F,yP⦈) in v]"
          apply - apply meta_solver
          by (simp add: Semantics.dκ_proper Semantics.ex1_def)
        ultimately have "[ y . ( F . ⦇F,xP ⦇F,yP⦈) & φ (yP) in v]"
          using ExIRule ConjI by fast
      }
      moreover {
        assume "[ y . ( F . ⦇F,xP ⦇F,yP⦈) & φ (yP) in v]"
        then obtain y where y_def: "[( F . ⦇F,xP ⦇F,yP⦈) & φ (yP) in v]"
          by (rule ExERule)
        hence "⋀ F . [⦇F,xP⦈ in v] = [⦇F,yP⦈ in v]"
          apply - apply (drule ConjE) apply (drule conjunct1)
          apply (drule AllE) apply (drule EquivE) by simp
        hence "[⦇makeΠ1 (λ u s w . νυ y = u),xP⦈ in v]
             = [⦇makeΠ1 (λ u s w . νυ y = u),yP⦈ in v]" by auto
        hence "νυ y = νυ x" by (simp add: meta_defs meta_aux)
        moreover have "[φ (yP) in v]" using y_def ConjE by blast
        ultimately have "[⦇(λ x . φ (xP)), xP⦈ in v]"
          using lambda_ex by blast
      }
      ultimately show "[⦇λx. φ (xP),xP⦈ in v]
          = [y. (F. ⦇F,xP ⦇F,yP⦈) & φ (yP) in v]"
        by auto
    qed

  lemma lambda_enc_emb:
    "[⦇(λ x . ⦃xP, F⦄), xP ( y . ( F . ⦇F,xP ⦇F,yP⦈) & ⦃yP, 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,xP ⦇F,yP⦈) & φ (yP))  φ (xP) in v]"
  proof (rule MetaSolver.EquivI; rule)
    interpret MetaSolver .
    assume "[y. (F. ⦇F,xP ⦇F,yP⦈) & φ (yP) in v]"
    then obtain y where y_def: "[(F. ⦇F,xP ⦇F,yP⦈) & φ (yP) in v]" by (rule ExERule)
    hence "[⦇makeΠ1 (λ u s w . νυ y = u), xP⦈ in v] = [⦇makeΠ1 (λ u s w . νυ y = u), yP⦈ in v]"
      using EquivS AllE ConjE by blast
    hence "νυ y = νυ x" by (simp add: meta_defs meta_aux)
    thus "[φ (xP) in v]"
      using y_def[THEN ConjE[THEN conjunct2]]
            assms IsProperInX.rep_eq valid_in.rep_eq
      by blast
  next
    interpret MetaSolver .
    assume "[φ (xP) in v]"
    moreover have "[F. ⦇F,xP ⦇F,xP⦈ in v]" apply meta_solver by blast
    ultimately show "[y. (F. ⦇F,xP ⦇F,yP⦈) & φ (yP) 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,aP ⦇F,bP⦈ in v]"
    shows "(λx. ⦇R,xP,aP⦈) = (λx . ⦇R,xP, bP⦈)"
  proof -
    interpret MetaSolver .
    obtain F where F_def: "F = makeΠ1 (λ u s w . u = νυ a)" by auto
    have "[⦇F, aP ⦇F, bP⦈ in v]" using assms by (rule AllE)
    moreover have "[⦇F, aP⦈ in v]"
      unfolding F_def by (simp add: meta_defs meta_aux)
    ultimately have "[⦇F, bP⦈ 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
(*>*)