# 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_Π⇩1_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_Π⇩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 . ⦃x⇧P, F⦄, x⇧P⦈ ❙→ ⦃x⇧P, 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 . ⦃x⇧P, F⦄), x⇧P⦈ in v] = (∃ y . νυ y = νυ x ∧ [⦃y⇧P, F⦄ in v])"

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

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
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Π⇩1 (λ u s w . νυ y = u),x⇧P⦈ in v]
= [⦇makeΠ⇩1 (λ 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Π⇩1 (λ u s w . νυ y = u), x⇧P⦈ in v] = [⦇makeΠ⇩1 (λ 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Π⇩1 (λ 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
(*>*)