src/Pure/Pure.thy
 author wenzelm Sun Mar 01 23:36:12 2009 +0100 (2009-03-01) changeset 30190 479806475f3c parent 29606 fedb8be05f24 child 48638 22d65e375c01 permissions -rw-r--r--
use long names for old-style fold combinators;
2 section {* Further content for the Pure theory *}
4 subsection {* Meta-level connectives in assumptions *}
6 lemma meta_mp:
7   assumes "PROP P ==> PROP Q" and "PROP P"
8   shows "PROP Q"
9     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
11 lemmas meta_impE = meta_mp [elim_format]
13 lemma meta_spec:
14   assumes "!!x. PROP P x"
15   shows "PROP P x"
16     by (rule `!!x. PROP P x`)
18 lemmas meta_allE = meta_spec [elim_format]
20 lemma swap_params:
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))"
28 proof
29   assume conj: "!!x. PROP A x &&& PROP B x"
30   show "(!!x. PROP A x) &&& (!!x. PROP B x)"
31   proof -
32     fix x
33     from conj show "PROP A x" by (rule conjunctionD1)
34     from conj show "PROP B x" by (rule conjunctionD2)
35   qed
36 next
37   assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
38   fix x
39   show "PROP A x &&& PROP B x"
40   proof -
41     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
42     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
43   qed
44 qed
46 lemma imp_conjunction:
47   "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
48 proof
49   assume conj: "PROP A ==> PROP B &&& PROP C"
50   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
51   proof -
52     assume "PROP A"
53     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
54     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
55   qed
56 next
57   assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
58   assume "PROP A"
59   show "PROP B &&& PROP C"
60   proof -
61     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
62     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
63   qed
64 qed
66 lemma conjunction_imp:
67   "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
68 proof
69   assume r: "PROP A &&& PROP B ==> PROP C"
70   assume ab: "PROP A" "PROP B"
71   show "PROP C"
72   proof (rule r)
73     from ab show "PROP A &&& PROP B" .
74   qed
75 next
76   assume r: "PROP A ==> PROP B ==> PROP C"
77   assume conj: "PROP A &&& PROP B"
78   show "PROP C"
79   proof (rule r)
80     from conj show "PROP A" by (rule conjunctionD1)
81     from conj show "PROP B" by (rule conjunctionD2)
82   qed
83 qed