author | wenzelm |
Fri, 20 Jul 2007 17:54:17 +0200 | |
changeset 23885 | 09254a1622e3 |
parent 23824 | 8ad7131dbfcf |
child 26426 | ddac7ef1e991 |
permissions | -rw-r--r-- |
15803 | 1 |
(* Title: Pure/Pure.thy |
2 |
ID: $Id$ |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
3 |
*) |
15803 | 4 |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
5 |
header {* The Pure theory *} |
15803 | 6 |
|
7 |
theory Pure |
|
8 |
imports ProtoPure |
|
9 |
begin |
|
19800 | 10 |
|
19048 | 11 |
setup -- {* Common setup of internal components *} |
15803 | 12 |
|
20627 | 13 |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
14 |
subsection {* Meta-level connectives in assumptions *} |
15803 | 15 |
|
16 |
lemma meta_mp: |
|
18019 | 17 |
assumes "PROP P ==> PROP Q" and "PROP P" |
15803 | 18 |
shows "PROP Q" |
18019 | 19 |
by (rule `PROP P ==> PROP Q` [OF `PROP P`]) |
15803 | 20 |
|
23432 | 21 |
lemmas meta_impE = meta_mp [elim_format] |
22 |
||
15803 | 23 |
lemma meta_spec: |
18019 | 24 |
assumes "!!x. PROP P(x)" |
15803 | 25 |
shows "PROP P(x)" |
18019 | 26 |
by (rule `!!x. PROP P(x)`) |
15803 | 27 |
|
28 |
lemmas meta_allE = meta_spec [elim_format] |
|
29 |
||
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
30 |
|
21625 | 31 |
subsection {* Embedded terms *} |
32 |
||
33 |
locale (open) meta_term_syntax = |
|
34 |
fixes meta_term :: "'a => prop" ("TERM _") |
|
35 |
||
36 |
lemmas [intro?] = termI |
|
37 |
||
38 |
||
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
39 |
subsection {* Meta-level conjunction *} |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
40 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
41 |
locale (open) meta_conjunction_syntax = |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
42 |
fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
43 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
44 |
lemma all_conjunction: |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
45 |
includes meta_conjunction_syntax |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
46 |
shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))" |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
47 |
proof |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
48 |
assume conj: "!!x. PROP A(x) && PROP B(x)" |
19121 | 49 |
show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))" |
50 |
proof - |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
51 |
fix x |
19121 | 52 |
from conj show "PROP A(x)" by (rule conjunctionD1) |
53 |
from conj show "PROP B(x)" by (rule conjunctionD2) |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
54 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
55 |
next |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
56 |
assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))" |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
57 |
fix x |
19121 | 58 |
show "PROP A(x) && PROP B(x)" |
59 |
proof - |
|
60 |
show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format]) |
|
61 |
show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format]) |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
62 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
63 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
64 |
|
19121 | 65 |
lemma imp_conjunction: |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
66 |
includes meta_conjunction_syntax |
19121 | 67 |
shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)" |
18836 | 68 |
proof |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
69 |
assume conj: "PROP A ==> PROP B && PROP C" |
19121 | 70 |
show "(PROP A ==> PROP B) && (PROP A ==> PROP C)" |
71 |
proof - |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
72 |
assume "PROP A" |
19121 | 73 |
from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1) |
74 |
from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2) |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
75 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
76 |
next |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
77 |
assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)" |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
78 |
assume "PROP A" |
19121 | 79 |
show "PROP B && PROP C" |
80 |
proof - |
|
81 |
from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1]) |
|
82 |
from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2]) |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
83 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
84 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
85 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
86 |
lemma conjunction_imp: |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
87 |
includes meta_conjunction_syntax |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
88 |
shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)" |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
89 |
proof |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
90 |
assume r: "PROP A && PROP B ==> PROP C" |
22933 | 91 |
assume ab: "PROP A" "PROP B" |
92 |
show "PROP C" |
|
93 |
proof (rule r) |
|
94 |
from ab show "PROP A && PROP B" . |
|
95 |
qed |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
96 |
next |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
97 |
assume r: "PROP A ==> PROP B ==> PROP C" |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
98 |
assume conj: "PROP A && PROP B" |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
99 |
show "PROP C" |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
100 |
proof (rule r) |
19121 | 101 |
from conj show "PROP A" by (rule conjunctionD1) |
102 |
from conj show "PROP B" by (rule conjunctionD2) |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
103 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
104 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
105 |
|
15803 | 106 |
end |