]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/demo/cantor.ma
apply rule (lem EM) works
[helm.git] / helm / software / matita / library / demo / cantor.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "demo/formal_topology.ma".
16 include "datatypes/constructors.ma".
17
18 axiom A: Type.
19 axiom S: A → Ω \sup A.
20
21 definition axs: axiom_set.
22  constructor 1;
23   [ apply A;
24   | intro; apply unit;
25   | intros; apply (S a)]
26 qed.
27
28 definition S' : axs → Ω \sup axs ≝ S.
29
30 definition emptyset: Ω \sup axs ≝ {x | False}.
31
32 definition Z: Ω \sup axs ≝ {x | x ◃ emptyset}.
33
34 theorem cantor: ∀a:axs. ¬ (Z ⊆ S' a ∧ S' a ⊆ Z).
35  intros 2; cases H; clear H;
36  cut (a ◃ S' a);
37   [2: constructor 2; [constructor 1 | whd in ⊢ (? ? ? % ?); autobatch]]
38  cut (a ◃ emptyset);
39   [2: apply transitivity; [apply (S' a)]
40        [ assumption
41        | constructor 1; intros;
42          lapply (H2 ? H); whd in Hletin; assumption]]
43  cut (a ∈ S' a);
44   [2: apply H1; whd; assumption]
45  generalize in match Hcut2; clear Hcut2;
46  change with (a ∈ {a | a ∈ S' a → False});
47  apply (covers_elim ?????? Hcut1);
48   [ intros 2; simplify; intros; assumption;
49   | intros; simplify; intros; whd in H3; simplify in H3; apply (H3 a1);
50      [ assumption
51      | assumption
52      ]]
53 qed.