section {* Further content for the Pure theory *}
subsection {* Meta-level connectives in assumptions *}
lemma meta_mp:
assumes "PROP P ==> PROP Q" and "PROP P"
shows "PROP Q"
by (rule `PROP P ==> PROP Q` [OF `PROP P`])
lemmas meta_impE = meta_mp [elim_format]
lemma meta_spec:
assumes "!!x. PROP P x"
shows "PROP P x"
by (rule `!!x. PROP P x`)
lemmas meta_allE = meta_spec [elim_format]
lemma swap_params:
"(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
subsection {* Meta-level conjunction *}
lemma all_conjunction:
"(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
proof
assume conj: "!!x. PROP A x &&& PROP B x"
show "(!!x. PROP A x) &&& (!!x. PROP B x)"
proof -
fix x
from conj show "PROP A x" by (rule conjunctionD1)
from conj show "PROP B x" by (rule conjunctionD2)
qed
next
assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
fix x
show "PROP A x &&& PROP B x"
proof -
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
qed
qed
lemma imp_conjunction:
"(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
proof
assume conj: "PROP A ==> PROP B &&& PROP C"
show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
proof -
assume "PROP A"
from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
qed
next
assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
assume "PROP A"
show "PROP B &&& PROP C"
proof -
from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
qed
qed
lemma conjunction_imp:
"(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
proof
assume r: "PROP A &&& PROP B ==> PROP C"
assume ab: "PROP A" "PROP B"
show "PROP C"
proof (rule r)
from ab show "PROP A &&& PROP B" .
qed
next
assume r: "PROP A ==> PROP B ==> PROP C"
assume conj: "PROP A &&& PROP B"
show "PROP C"
proof (rule r)
from conj show "PROP A" by (rule conjunctionD1)
from conj show "PROP B" by (rule conjunctionD2)
qed
qed