src/Pure/Pure.thy
 author haftmann Fri Nov 10 07:44:47 2006 +0100 (2006-11-10) changeset 21286 b5e7b80caa6a parent 20627 30da2841553e child 21625 fa8a7de5da28 permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
1 (*  Title:      Pure/Pure.thy
2     ID:         \$Id\$
3 *)
5 header {* The Pure theory *}
7 theory Pure
8 imports ProtoPure
9 begin
11 setup  -- {* Common setup of internal components *}
14 subsection {* Meta-level connectives in assumptions *}
16 lemma meta_mp:
17   assumes "PROP P ==> PROP Q" and "PROP P"
18   shows "PROP Q"
19     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
21 lemma meta_spec:
22   assumes "!!x. PROP P(x)"
23   shows "PROP P(x)"
24     by (rule `!!x. PROP P(x)`)
26 lemmas meta_allE = meta_spec [elim_format]
29 subsection {* Meta-level conjunction *}
31 locale (open) meta_conjunction_syntax =
32   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
34 parse_translation {*
35   [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
36 *}
38 lemma all_conjunction:
39   includes meta_conjunction_syntax
40   shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
41 proof
42   assume conj: "!!x. PROP A(x) && PROP B(x)"
43   show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
44   proof -
45     fix x
46     from conj show "PROP A(x)" by (rule conjunctionD1)
47     from conj show "PROP B(x)" by (rule conjunctionD2)
48   qed
49 next
50   assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
51   fix x
52   show "PROP A(x) && PROP B(x)"
53   proof -
54     show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
55     show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
56   qed
57 qed
59 lemma imp_conjunction:
60   includes meta_conjunction_syntax
61   shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
62 proof
63   assume conj: "PROP A ==> PROP B && PROP C"
64   show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
65   proof -
66     assume "PROP A"
67     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
68     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
69   qed
70 next
71   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
72   assume "PROP A"
73   show "PROP B && PROP C"
74   proof -
75     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
76     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
77   qed
78 qed
80 lemma conjunction_imp:
81   includes meta_conjunction_syntax
82   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
83 proof
84   assume r: "PROP A && PROP B ==> PROP C"
85   assume "PROP A" and "PROP B"
86   show "PROP C" by (rule r) -
87 next
88   assume r: "PROP A ==> PROP B ==> PROP C"
89   assume conj: "PROP A && PROP B"
90   show "PROP C"
91   proof (rule r)
92     from conj show "PROP A" by (rule conjunctionD1)
93     from conj show "PROP B" by (rule conjunctionD2)
94   qed
95 qed
97 end