author | wenzelm |
Wed, 01 Aug 2012 19:53:20 +0200 | |
changeset 48638 | 22d65e375c01 |
parent 29606 | fedb8be05f24 |
child 48641 | 92b48b8abfe4 |
permissions | -rw-r--r-- |
48638 | 1 |
theory Pure |
2 |
begin |
|
15803 | 3 |
|
26435 | 4 |
section {* Further content for the Pure theory *} |
20627 | 5 |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
6 |
subsection {* Meta-level connectives in assumptions *} |
15803 | 7 |
|
8 |
lemma meta_mp: |
|
18019 | 9 |
assumes "PROP P ==> PROP Q" and "PROP P" |
15803 | 10 |
shows "PROP Q" |
18019 | 11 |
by (rule `PROP P ==> PROP Q` [OF `PROP P`]) |
15803 | 12 |
|
23432 | 13 |
lemmas meta_impE = meta_mp [elim_format] |
14 |
||
15803 | 15 |
lemma meta_spec: |
26958 | 16 |
assumes "!!x. PROP P x" |
17 |
shows "PROP P x" |
|
18 |
by (rule `!!x. PROP P x`) |
|
15803 | 19 |
|
20 |
lemmas meta_allE = meta_spec [elim_format] |
|
21 |
||
26570 | 22 |
lemma swap_params: |
26958 | 23 |
"(!!x y. PROP P x y) == (!!y x. PROP P x y)" .. |
26570 | 24 |
|
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
25 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
26 |
subsection {* Meta-level conjunction *} |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
27 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
28 |
lemma all_conjunction: |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
29 |
"(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
30 |
proof |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
31 |
assume conj: "!!x. PROP A x &&& PROP B x" |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
32 |
show "(!!x. PROP A x) &&& (!!x. PROP B x)" |
19121 | 33 |
proof - |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
34 |
fix x |
26958 | 35 |
from conj show "PROP A x" by (rule conjunctionD1) |
36 |
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
|
37 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
38 |
next |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
39 |
assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
40 |
fix x |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
41 |
show "PROP A x &&& PROP B x" |
19121 | 42 |
proof - |
26958 | 43 |
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) |
44 |
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
|
45 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
46 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
47 |
|
19121 | 48 |
lemma imp_conjunction: |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
49 |
"(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
18836 | 50 |
proof |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
51 |
assume conj: "PROP A ==> PROP B &&& PROP C" |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
52 |
show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
19121 | 53 |
proof - |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
54 |
assume "PROP A" |
19121 | 55 |
from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1) |
56 |
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
|
57 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
58 |
next |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
59 |
assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
60 |
assume "PROP A" |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
61 |
show "PROP B &&& PROP C" |
19121 | 62 |
proof - |
63 |
from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1]) |
|
64 |
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
|
65 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
66 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
67 |
|
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
68 |
lemma conjunction_imp: |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
69 |
"(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
70 |
proof |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
71 |
assume r: "PROP A &&& PROP B ==> PROP C" |
22933 | 72 |
assume ab: "PROP A" "PROP B" |
73 |
show "PROP C" |
|
74 |
proof (rule r) |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
75 |
from ab show "PROP A &&& PROP B" . |
22933 | 76 |
qed |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
77 |
next |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
78 |
assume r: "PROP A ==> PROP B ==> PROP C" |
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset
|
79 |
assume conj: "PROP A &&& PROP B" |
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
80 |
show "PROP C" |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
81 |
proof (rule r) |
19121 | 82 |
from conj show "PROP A" by (rule conjunctionD1) |
83 |
from conj show "PROP B" by (rule conjunctionD2) |
|
18466
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 |
qed |
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset
|
86 |
|
48638 | 87 |
end |
88 |