header{*\isaheader{Metamath\_interface.thy}*}
theory Metamath_interface imports Complex_ZF MMI_prelude
begin
text{*This theory contains some lemmas that make it possible to use
the theorems translated from Metamath in a the @{text "complex0"}
context.*}
section{*MMisar0 and complex0 contexts.*}
text{*In the section we show a lemma that the assumptions in
@{text "complex0"} context imply the assumptions of the @{text "MMIsar0"}
context. The @{text "Metamath_sampler"} theory provides examples
how this lemma can be used.*}
text{*The next lemma states that we can use
the theorems proven in the @{text "MMIsar0"} context in
the @{text "complex0"} context. Unfortunately we have to
use low level Isabelle methods "rule" and "unfold" in the proof, simp
and blast fail on the order axioms.
*}
lemma (in complex0) MMIsar_valid:
shows "MMIsar0(ℝ,ℂ,𝟭,𝟬,𝗂,CplxAdd(R,A),CplxMul(R,A,M),
StrictVersion(CplxROrder(R,A,r)))"
proof -
let ?real = "ℝ"
let ?complex = "ℂ"
let ?zero = "𝟬"
let ?one = "𝟭"
let ?iunit = "𝗂"
let ?caddset = "CplxAdd(R,A)"
let ?cmulset = "CplxMul(R,A,M)"
let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
have "(∀a b. a ∈ ?real ∧ b ∈ ?real ⟶
⟨a, b⟩ ∈ ?lessrrel ⟷ ¬ (a = b ∨ ⟨b, a⟩ ∈ ?lessrrel))"
proof -
have I:
"∀a b. a ∈ ℝ ∧ b ∈ ℝ ⟶ (a \<lsr> b ⟷ ¬(a=b ∨ b \<lsr> a))"
using pre_axlttri by blast
{ fix a b assume "a ∈ ?real ∧ b ∈ ?real"
with I have "(a \<lsr> b ⟷ ¬(a=b ∨ b \<lsr> a))"
by blast
hence
"⟨a, b⟩ ∈ ?lessrrel ⟷ ¬ (a = b ∨ ⟨b, a⟩ ∈ ?lessrrel)"
by simp
} thus "(∀a b. a ∈ ?real ∧ b ∈ ?real ⟶
(⟨a, b⟩ ∈ ?lessrrel ⟷ ¬ (a = b ∨ ⟨b, a⟩ ∈ ?lessrrel)))"
by blast
qed
moreover
have "(∀a b c.
a ∈ ?real ∧ b ∈ ?real ∧ c ∈ ?real ⟶
⟨a, b⟩ ∈ ?lessrrel ∧ ⟨b, c⟩ ∈ ?lessrrel ⟶ ⟨a, c⟩ ∈ ?lessrrel)"
proof -
have II: "∀a b c. a ∈ ℝ ∧ b ∈ ℝ ∧ c ∈ ℝ ⟶
((a \<lsr> b ∧ b \<lsr> c) ⟶ a \<lsr> c)"
using pre_axlttrn by blast
{ fix a b c assume "a ∈ ?real ∧ b ∈ ?real ∧ c ∈ ?real"
with II have "(a \<lsr> b ∧ b \<lsr> c) ⟶ a \<lsr> c"
by blast
hence
"⟨a, b⟩ ∈ ?lessrrel ∧ ⟨b, c⟩ ∈ ?lessrrel ⟶ ⟨a, c⟩ ∈ ?lessrrel"
by simp
} thus "(∀a b c.
a ∈ ?real ∧ b ∈ ?real ∧ c ∈ ?real ⟶
⟨a, b⟩ ∈ ?lessrrel ∧ ⟨b, c⟩ ∈ ?lessrrel ⟶ ⟨a, c⟩ ∈ ?lessrrel)"
by blast
qed
moreover have "(∀A B C.
A ∈ ?real ∧ B ∈ ?real ∧ C ∈ ?real ⟶
⟨A, B⟩ ∈ ?lessrrel ⟶
⟨?caddset ` ⟨C, A⟩, ?caddset ` ⟨C, B⟩⟩ ∈ ?lessrrel)"
using pre_axltadd by simp
moreover have "(∀A B. A ∈ ?real ∧ B ∈ ?real ⟶
⟨?zero, A⟩ ∈ ?lessrrel ∧ ⟨?zero, B⟩ ∈ ?lessrrel ⟶
⟨?zero, ?cmulset ` ⟨A, B⟩⟩ ∈ ?lessrrel)"
using pre_axmulgt0 by simp
moreover have
"(∀S. S ⊆ ?real ∧ S ≠ 0 ∧ (∃x∈?real. ∀y∈S. ⟨y, x⟩ ∈ ?lessrrel) ⟶
(∃x∈?real.
(∀y∈S. ⟨x, y⟩ ∉ ?lessrrel) ∧
(∀y∈?real. ⟨y, x⟩ ∈ ?lessrrel ⟶ (∃z∈S. ⟨y, z⟩ ∈ ?lessrrel))))"
using pre_axsup by simp
moreover have "ℝ ⊆ ℂ" using axresscn by simp
moreover have "𝟭 ≠ 𝟬" using ax1ne0 by simp
moreover have "ℂ isASet" by simp
moreover have " CplxAdd(R,A) : ℂ × ℂ → ℂ"
using axaddopr by simp
moreover have "CplxMul(R,A,M) : ℂ × ℂ → ℂ"
using axmulopr by simp
moreover have
"∀a b. a ∈ ℂ ∧ b ∈ ℂ ⟶ a⋅ b = b ⋅ a"
using axmulcom by simp
hence "(∀a b. a ∈ ℂ ∧ b ∈ ℂ ⟶
?cmulset ` ⟨a, b⟩ = ?cmulset ` ⟨b, a⟩
)" by simp
moreover have "∀a b. a ∈ ℂ ∧ b ∈ ℂ ⟶ a \<ca> b ∈ ℂ"
using axaddcl by simp
hence "(∀a b. a ∈ ℂ ∧ b ∈ ℂ ⟶
?caddset ` ⟨a, b⟩ ∈ ℂ
)" by simp
moreover have "∀a b. a ∈ ℂ ∧ b ∈ ℂ ⟶ a ⋅ b ∈ ℂ"
using axmulcl by simp
hence "(∀a b. a ∈ ℂ ∧ b ∈ ℂ ⟶
?cmulset ` ⟨a, b⟩ ∈ ℂ )" by simp
moreover have
"∀a b C. a ∈ ℂ ∧ b ∈ ℂ ∧ C ∈ ℂ ⟶
a ⋅ (b \<ca> C) = a ⋅ b \<ca> a ⋅ C"
using axdistr by simp
hence "∀a b C.
a ∈ ℂ ∧ b ∈ ℂ ∧ C ∈ ℂ ⟶
?cmulset ` ⟨a, ?caddset ` ⟨b, C⟩⟩ =
?caddset `
⟨?cmulset ` ⟨a, b⟩, ?cmulset ` ⟨a, C⟩⟩"
by simp
moreover have "∀a b. a ∈ ℂ ∧ b ∈ ℂ ⟶
a \<ca> b = b \<ca> a"
using axaddcom by simp
hence "∀a b.
a ∈ ℂ ∧ b ∈ ℂ ⟶
?caddset ` ⟨a, b⟩ = ?caddset ` ⟨b, a⟩" by simp
moreover have "∀a b C. a ∈ ℂ ∧ b ∈ ℂ ∧ C ∈ ℂ ⟶
a \<ca> b \<ca> C = a \<ca> (b \<ca> C)"
using axaddass by simp
hence "∀a b C.
a ∈ ℂ ∧ b ∈ ℂ ∧ C ∈ ℂ ⟶
?caddset ` ⟨?caddset ` ⟨a, b⟩, C⟩ =
?caddset ` ⟨a, ?caddset ` ⟨b, C⟩⟩" by simp
moreover have
"∀a b c. a ∈ ℂ ∧ b ∈ ℂ ∧ c ∈ ℂ ⟶ a⋅b⋅c = a⋅(b⋅c)"
using axmulass by simp
hence "∀a b C.
a ∈ ℂ ∧ b ∈ ℂ ∧ C ∈ ℂ ⟶
?cmulset ` ⟨?cmulset ` ⟨a, b⟩, C⟩ =
?cmulset ` ⟨a, ?cmulset ` ⟨b, C⟩⟩" by simp
moreover have "𝟭 ∈ ℝ" using ax1re by simp
moreover have "𝗂⋅𝗂 \<ca> 𝟭 = 𝟬"
using axi2m1 by simp
hence "?caddset ` ⟨?cmulset ` ⟨𝗂, 𝗂⟩, 𝟭⟩ = 𝟬" by simp
moreover have "∀a. a ∈ ℂ ⟶ a \<ca> 𝟬 = a"
using ax0id by simp
hence "∀a. a ∈ ℂ ⟶ ?caddset ` ⟨a, 𝟬⟩ = a" by simp
moreover have "𝗂 ∈ ℂ" using axicn by simp
moreover have "∀a. a ∈ ℂ ⟶ (∃x∈ℂ. a \<ca> x = 𝟬)"
using axnegex by simp
hence "∀a. a ∈ ℂ ⟶
(∃x∈ℂ. ?caddset ` ⟨a, x⟩ = 𝟬)" by simp
moreover have "∀a. a ∈ ℂ ∧ a ≠ 𝟬 ⟶ (∃x∈ℂ. a ⋅ x = 𝟭)"
using axrecex by simp
hence "∀a. a ∈ ℂ ∧ a ≠ 𝟬 ⟶
( ∃x∈ℂ. ?cmulset ` ⟨a, x⟩ = 𝟭 )" by simp
moreover have "∀a. a ∈ ℂ ⟶ a⋅𝟭 = a"
using ax1id by simp
hence " ∀a. a ∈ ℂ ⟶
?cmulset ` ⟨a, 𝟭⟩ = a" by simp
moreover have "∀a b. a ∈ ℝ ∧ b ∈ ℝ ⟶ a \<ca> b ∈ ℝ"
using axaddrcl by simp
hence "∀a b. a ∈ ℝ ∧ b ∈ ℝ ⟶
?caddset ` ⟨a, b⟩ ∈ ℝ" by simp
moreover have "∀a b. a ∈ ℝ ∧ b ∈ ℝ ⟶ a ⋅ b ∈ ℝ"
using axmulrcl by simp
hence "∀a b. a ∈ ℝ ∧ b ∈ ℝ ⟶
?cmulset ` ⟨a, b⟩ ∈ ℝ" by simp
moreover have "∀a. a ∈ ℝ ⟶ (∃x∈ℝ. a \<ca> x = 𝟬)"
using axrnegex by simp
hence "∀a. a ∈ ℝ ⟶
( ∃x∈ℝ. ?caddset ` ⟨a, x⟩ = 𝟬 )" by simp
moreover have "∀a. a ∈ ℝ ∧ a≠𝟬 ⟶ (∃x∈ℝ. a ⋅ x = 𝟭)"
using axrrecex by simp
hence "∀a. a ∈ ℝ ∧ a ≠ 𝟬 ⟶
( ∃x∈ℝ. ?cmulset ` ⟨a, x⟩ = 𝟭)" by simp
ultimately have
"(
(
(
( ∀a b.
a ∈ ℝ ∧ b ∈ ℝ ⟶
⟨a, b⟩ ∈ ?lessrrel ⟷
¬ (a = b ∨ ⟨b, a⟩ ∈ ?lessrrel)
) ∧
( ∀a b C.
a ∈ ℝ ∧ b ∈ ℝ ∧ C ∈ ℝ ⟶
⟨a, b⟩ ∈ ?lessrrel ∧
⟨b, C⟩ ∈ ?lessrrel ⟶
⟨a, C⟩ ∈ ?lessrrel
) ∧
(∀a b C.
a ∈ ℝ ∧ b ∈ ℝ ∧ C ∈ ℝ ⟶
⟨a, b⟩ ∈ ?lessrrel ⟶
⟨?caddset ` ⟨C, a⟩, ?caddset ` ⟨C, b⟩⟩ ∈
?lessrrel
)
) ∧
(
( ∀a b.
a ∈ ℝ ∧ b ∈ ℝ ⟶
⟨𝟬, a⟩ ∈ ?lessrrel ∧
⟨𝟬, b⟩ ∈ ?lessrrel ⟶
⟨𝟬, ?cmulset ` ⟨a, b⟩⟩ ∈
?lessrrel
) ∧
( ∀S. S ⊆ ℝ ∧ S ≠ 0 ∧
( ∃x∈ℝ. ∀y∈S. ⟨y, x⟩ ∈ ?lessrrel
) ⟶
( ∃x∈ℝ.
( ∀y∈S. ⟨x, y⟩ ∉ ?lessrrel
) ∧
( ∀y∈ℝ. ⟨y, x⟩ ∈ ?lessrrel ⟶
( ∃z∈S. ⟨y, z⟩ ∈ ?lessrrel
)
)
)
)
) ∧
ℝ ⊆ ℂ ∧
𝟭 ≠ 𝟬
) ∧
( ℂ isASet ∧ ?caddset ∈ ℂ × ℂ → ℂ ∧
?cmulset ∈ ℂ × ℂ → ℂ
) ∧
(
(∀a b.
a ∈ ℂ ∧ b ∈ ℂ ⟶
?cmulset ` ⟨a, b⟩ = ?cmulset ` ⟨b, a⟩
) ∧
(∀a b. a ∈ ℂ ∧ b ∈ ℂ ⟶
?caddset ` ⟨a, b⟩ ∈ ℂ
)
) ∧
(∀a b. a ∈ ℂ ∧ b ∈ ℂ ⟶
?cmulset ` ⟨a, b⟩ ∈ ℂ
) ∧
(∀a b C.
a ∈ ℂ ∧ b ∈ ℂ ∧ C ∈ ℂ ⟶
?cmulset ` ⟨a, ?caddset ` ⟨b, C⟩⟩ =
?caddset `
⟨?cmulset ` ⟨a, b⟩, ?cmulset ` ⟨a, C⟩⟩
)
) ∧
(
(
(∀a b.
a ∈ ℂ ∧ b ∈ ℂ ⟶
?caddset ` ⟨a, b⟩ = ?caddset ` ⟨b, a⟩
) ∧
(∀a b C.
a ∈ ℂ ∧ b ∈ ℂ ∧ C ∈ ℂ ⟶
?caddset ` ⟨?caddset ` ⟨a, b⟩, C⟩ =
?caddset ` ⟨a, ?caddset ` ⟨b, C⟩⟩
) ∧
(∀a b C.
a ∈ ℂ ∧ b ∈ ℂ ∧ C ∈ ℂ ⟶
?cmulset ` ⟨?cmulset ` ⟨a, b⟩, C⟩ =
?cmulset ` ⟨a, ?cmulset ` ⟨b, C⟩⟩
)
) ∧
(𝟭 ∈ ℝ ∧
?caddset ` ⟨?cmulset ` ⟨𝗂, 𝗂⟩, 𝟭⟩ = 𝟬
) ∧
(∀a. a ∈ ℂ ⟶ ?caddset ` ⟨a, 𝟬⟩ = a
) ∧
𝗂 ∈ ℂ
) ∧
(
(∀a. a ∈ ℂ ⟶
(∃x∈ℂ. ?caddset ` ⟨a, x⟩ = 𝟬
)
) ∧
( ∀a. a ∈ ℂ ∧ a ≠ 𝟬 ⟶
( ∃x∈ℂ. ?cmulset ` ⟨a, x⟩ = 𝟭
)
) ∧
( ∀a. a ∈ ℂ ⟶
?cmulset ` ⟨a, 𝟭⟩ = a
)
) ∧
(
( ∀a b. a ∈ ℝ ∧ b ∈ ℝ ⟶
?caddset ` ⟨a, b⟩ ∈ ℝ
) ∧
( ∀a b. a ∈ ℝ ∧ b ∈ ℝ ⟶
?cmulset ` ⟨a, b⟩ ∈ ℝ
)
) ∧
( ∀a. a ∈ ℝ ⟶
( ∃x∈ℝ. ?caddset ` ⟨a, x⟩ = 𝟬
)
) ∧
( ∀a. a ∈ ℝ ∧ a ≠ 𝟬 ⟶
( ∃x∈ℝ. ?cmulset ` ⟨a, x⟩ = 𝟭
)
)"
by blast
then show "MMIsar0(ℝ,ℂ,𝟭,𝟬,𝗂,CplxAdd(R,A),CplxMul(R,A,M),
StrictVersion(CplxROrder(R,A,r)))" unfolding MMIsar0_def by blast
qed
end