equal
deleted
inserted
replaced
54 val disj_exD = prove_fun "(? x. P(x)) | (? x. Q(x)) ==> ? x. P(x) | Q(x)"; |
54 val disj_exD = prove_fun "(? x. P(x)) | (? x. Q(x)) ==> ? x. P(x) | Q(x)"; |
55 |
55 |
56 val disj_exD1 = prove_fun "(? x. P(x)) | Q ==> ? x. P(x) | Q"; |
56 val disj_exD1 = prove_fun "(? x. P(x)) | Q ==> ? x. P(x) | Q"; |
57 val disj_exD2 = prove_fun "P | (? x. Q(x)) ==> ? x. P | Q(x)"; |
57 val disj_exD2 = prove_fun "P | (? x. Q(x)) ==> ? x. P | Q(x)"; |
58 |
58 |
59 |
|
60 (**** Skolemization -- pulling "?" over "!" ****) |
|
61 |
|
62 (*"Axiom" of Choice, proved using the description operator*) |
|
63 val [major] = goal HOL.thy |
|
64 "! x. ? y. Q x y ==> ? f. ! x. Q x (f x)"; |
|
65 by (cut_facts_tac [major] 1); |
|
66 by (fast_tac (claset() addEs [selectI]) 1); |
|
67 qed "choice"; |
|
68 |
59 |
69 |
60 |
70 (***** Generating clauses for the Meson Proof Procedure *****) |
61 (***** Generating clauses for the Meson Proof Procedure *****) |
71 |
62 |
72 (*** Disjunctions ***) |
63 (*** Disjunctions ***) |