equal
deleted
inserted
replaced
11 |
11 |
12 syntax (xsymbols) |
12 syntax (xsymbols) |
13 "?? " :: "[idts, o] => o" ("(3\<Or>_./ _)" [0, 0] 0) |
13 "?? " :: "[idts, o] => o" ("(3\<Or>_./ _)" [0, 0] 0) |
14 |
14 |
15 lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))" |
15 lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))" |
16 proof - |
16 proof (unfold ex_def) |
17 assume P: "PROP P(x)" |
17 assume P: "PROP P(x)" |
18 show "?? x. PROP P(x)" |
18 fix Q |
19 apply (unfold ex_def) |
19 assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q" |
20 proof - |
20 from P show "PROP Q" by (rule PQ) |
21 fix Q |
|
22 assume PQ: "\<And>x. PROP P(x) \<Longrightarrow> PROP Q" |
|
23 from P show "PROP Q" by (rule PQ) |
|
24 qed |
|
25 qed |
21 qed |
26 |
22 |
27 lemma meta_exE: "[| ?? x. PROP P(x); !!x. PROP P(x) ==> PROP R |] ==> PROP R" |
23 lemma meta_exE: "[| ?? x. PROP P(x); !!x. PROP P(x) ==> PROP R |] ==> PROP R" |
28 apply (unfold ex_def) |
24 proof (unfold ex_def) |
29 proof - |
|
30 assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q" |
25 assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q" |
31 assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R" |
26 assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R" |
32 from PR show "PROP R" by (rule QPQ) |
27 from PR show "PROP R" by (rule QPQ) |
33 qed |
28 qed |
34 |
29 |