helm/software/matita/library/demo/natural_deduction.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 "didactic/support/natural_deduction.ma".
  16
  17 lemma RAA_to_EM : A ∨ ¬ A.
  18
  19   apply rule (prove (A ∨ ¬ A));
  20
  21   apply rule (RAA [H] ⊥);
  22   apply rule (¬#e (¬A) A);
  23     [ apply rule (¬#i [H1] ⊥);
  24       apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
  25       [ apply rule (discharge [H]);
  26       | apply rule (∨#i_l A);
  27         apply rule (discharge [H1]);
  28       ]
  29     | apply rule (RAA [H2] ⊥);
  30       apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
  31       [ apply rule (discharge [H]);
  32       | apply rule (∨#i_r (¬A));
  33         apply rule (discharge [H2]);
  34       ]
  35     ]
  36 qed.
  37
  38 lemma RA_to_EM1 : A ∨ ¬ A.
  39
  40   apply rule (prove (A ∨ ¬ A));
  41
  42   apply rule (RAA [H] ⊥);
  43   apply rule (¬#e (¬¬A) (¬A));
  44     [ apply rule (¬#i [H2] ⊥);
  45       apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
  46       [ apply rule (discharge [H]);
  47       | apply rule (∨#i_r (¬A));
  48         apply rule (discharge [H2]);
  49       ]
  50     | apply rule (¬#i [H1] ⊥);
  51       apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
  52       [ apply rule (discharge [H]);
  53       | apply rule (∨#i_l A);
  54         apply rule (discharge [H1]);
  55       ]
  56     ]
  57 qed.
  58
  59 lemma ex1 : (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
  60
  61  apply rule (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
  62
  63  apply rule (⇒#i [H] (A∧C⇒E∧C∨B));
  64  apply rule (⇒#i [K] (E∧C∨B));
  65  apply rule (∨#e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
  66 [ apply rule (discharge [H]);
  67 | apply rule (∨#i_l (E∧C));
  68   apply rule (∧#i E C);
  69   [ apply rule (⇒#e (A⇒E) A);
  70     [ apply rule (discharge [C1]);
  71     | apply rule (∧#e_l (A∧C)); apply rule (discharge [K]);
  72     ]
  73   | apply rule (∧#e_r (A∧C)); apply rule (discharge [K]);
  74   ]
  75 | apply rule (∨#i_r B); apply rule (discharge [C2]);
  76 ]
  77 qed.
  78