2 section {* Further content for the Pure theory *}
4 subsection {* Meta-level connectives in assumptions *}
7 assumes "PROP P ==> PROP Q" and "PROP P"
9 by (rule `PROP P ==> PROP Q` [OF `PROP P`])
11 lemmas meta_impE = meta_mp [elim_format]
14 assumes "!!x. PROP P x"
16 by (rule `!!x. PROP P x`)
18 lemmas meta_allE = meta_spec [elim_format]
21 "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
24 subsection {* Meta-level conjunction *}
26 lemma all_conjunction:
27 "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
29 assume conj: "!!x. PROP A x &&& PROP B x"
30 show "(!!x. PROP A x) &&& (!!x. PROP B x)"
33 from conj show "PROP A x" by (rule conjunctionD1)
34 from conj show "PROP B x" by (rule conjunctionD2)
37 assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
39 show "PROP A x &&& PROP B x"
41 show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
42 show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
46 lemma imp_conjunction:
47 "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
49 assume conj: "PROP A ==> PROP B &&& PROP C"
50 show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
53 from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
54 from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
57 assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
59 show "PROP B &&& PROP C"
61 from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
62 from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
66 lemma conjunction_imp:
67 "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
69 assume r: "PROP A &&& PROP B ==> PROP C"
70 assume ab: "PROP A" "PROP B"
73 from ab show "PROP A &&& PROP B" .
76 assume r: "PROP A ==> PROP B ==> PROP C"
77 assume conj: "PROP A &&& PROP B"
80 from conj show "PROP A" by (rule conjunctionD1)
81 from conj show "PROP B" by (rule conjunctionD2)