equal
deleted
inserted
replaced
|
1 header{*The meta-existential quantifier*} |
|
2 |
|
3 theory MetaExists = Main: |
|
4 |
|
5 text{*Allows quantification over any term having sort @{text logic}. Used to |
|
6 quantify over classes. Yields a proposition rather than a FOL formula.*} |
|
7 |
|
8 constdefs |
|
9 ex :: "(('a::logic) => prop) => prop" (binder "?? " 0) |
|
10 "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)" |
|
11 |
|
12 syntax (xsymbols) |
|
13 "?? " :: "[idts, o] => o" ("(3\<Or>_./ _)" [0, 0] 0) |
|
14 |
|
15 lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))" |
|
16 proof - |
|
17 assume P: "PROP P(x)" |
|
18 show "?? x. PROP P(x)" |
|
19 apply (unfold ex_def) |
|
20 proof - |
|
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 |
|
26 |
|
27 lemma meta_exE: "[| ?? x. PROP P(x); !!x. PROP P(x) ==> PROP R |] ==> PROP R" |
|
28 apply (unfold ex_def) |
|
29 proof - |
|
30 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" |
|
32 from PR show "PROP R" by (rule QPQ) |
|
33 qed |
|
34 |
|
35 end |