X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fnatural_deduction.ma;h=9a7fd3671656547cb68fb7adfacc4e52c7cd2315;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=64b3daccbb5fd4f687a421fc7c0c92c123cc5f71;hpb=88f24d23df67d88bf98c2ca32ac0d9854f3d9b00;p=helm.git

diff --git a/helm/software/matita/library/demo/natural_deduction.ma b/helm/software/matita/library/demo/natural_deduction.ma
index 64b3daccb..9a7fd3671 100644
--- a/helm/software/matita/library/demo/natural_deduction.ma
+++ b/helm/software/matita/library/demo/natural_deduction.ma
@@ -12,115 +12,67 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "demo/natural_deduction_support.ma".
+include "didactic/support/natural_deduction.ma".
 
 lemma RAA_to_EM : A ∨ ¬ A.
 
-  apply (prove (A ∨ ¬ A));
+  apply rule (prove (A ∨ ¬ A));
   
-  apply (RAA [H] ⊥);
-  apply (¬_e (¬A) A);
-    [ apply (¬_i [H1] ⊥);
-      apply (¬_e (¬(A∨¬A)) (A∨¬A));
-      [ apply [H];
-      | apply (∨_i_l A);
-        apply [H1];
+  apply rule (RAA [H] ⊥);
+  apply rule (¬#e (¬A) A);
+    [ apply rule (¬#i [H1] ⊥);
+      apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
+      [ apply rule (discharge [H]);
+      | apply rule (∨#i_l A);
+        apply rule (discharge [H1]);
       ]
-    | apply (RAA [H2] ⊥);
-      apply (¬_e (¬(A∨¬A)) (A∨¬A));
-      [ apply [H];
-      | apply (∨_i_r (¬A));
-        apply [H2];
+    | apply rule (RAA [H2] ⊥);
+      apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
+      [ apply rule (discharge [H]);
+      | apply rule (∨#i_r (¬A));
+        apply rule (discharge [H2]);
       ]
     ]
 qed.
 
 lemma RA_to_EM1 : A ∨ ¬ A.
 
-  apply (prove (A ∨ ¬ A));
+  apply rule (prove (A ∨ ¬ A));
   
-  apply (RAA [H] ⊥);
-  apply (¬_e (¬¬A) (¬A));
-    [ apply (¬_i [H2] ⊥);
-      apply (¬_e (¬(A∨¬A)) (A∨¬A));
-      [ apply [H];
-      | apply (∨_i_r (¬A));
-        apply [H2];
+  apply rule (RAA [H] ⊥);
+  apply rule (¬#e (¬¬A) (¬A));
+    [ apply rule (¬#i [H2] ⊥);
+      apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
+      [ apply rule (discharge [H]);
+      | apply rule (∨#i_r (¬A));
+        apply rule (discharge [H2]);
       ]
-    | apply (¬_i [H1] ⊥);
-      apply (¬_e (¬(A∨¬A)) (A∨¬A));
-      [ apply [H];
-      | apply (∨_i_l A);
-        apply [H1];
+    | apply rule (¬#i [H1] ⊥);
+      apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
+      [ apply rule (discharge [H]);
+      | apply rule (∨#i_l A);
+        apply rule (discharge [H1]);
       ]
     ]
 qed.
 
-lemma ex0 : (A ⇒ ⊥) ⇒ A ⇒ B ∧ ⊤. 
- 
-  apply (prove ((A ⇒ ⊥) ⇒ A ⇒ B∧⊤));
-  
-  apply (⇒_i [H] (A ⇒ B∧⊤));
-  apply (⇒_i [H1] (B∧⊤));
-  apply (∧_i B ⊤);
-  [ apply (⊥_e ⊥);
-    apply (⇒_e (A ⇒ ⊥) A); 
-    [ apply [H];
-    | apply [H1];
-    ]
-  | apply (⊤_i);
-  ]
-qed.
-
 lemma ex1 : (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
 
- apply (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
+ apply rule (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
    
- apply (⇒_i [H] (A∧C⇒E∧C∨B));
- apply (⇒_i [K] (E∧C∨B));
- apply (∨_e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
-[ apply [H];
-| apply (∨_i_l (E∧C));
-  apply (∧_i E C);
-  [ apply (⇒_e (A⇒E) A);
-    [ apply [C1];
-    | apply (∧_e_l (A∧C)); apply [K];
+ apply rule (⇒#i [H] (A∧C⇒E∧C∨B));
+ apply rule (⇒#i [K] (E∧C∨B));
+ apply rule (∨#e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
+[ apply rule (discharge [H]);
+| apply rule (∨#i_l (E∧C));
+  apply rule (∧#i E C);
+  [ apply rule (⇒#e (A⇒E) A);
+    [ apply rule (discharge [C1]);
+    | apply rule (∧#e_l (A∧C)); apply rule (discharge [K]);
     ]
-  | apply (∧_e_r (A∧C)); apply [K];
+  | apply rule (∧#e_r (A∧C)); apply rule (discharge [K]);
   ]
-| apply (∨_i_r B); apply [C2];
+| apply rule (∨#i_r B); apply rule (discharge [C2]);
 ]
 qed.
 
-lemma dmg : ¬(A ∨ B) ⇒ ¬A ∧ ¬B.
-
-  apply (prove (¬(A ∨ B) ⇒ ¬A ∧ ¬B));
-  apply (⇒_i [H] (¬A ∧ ¬B));
-  
-  apply (¬_e (¬A) A);
-  
-  
-
-
-(*
-lemma ex2: ΠN:Type.ΠR:N→N→CProp.
-
-   (∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y.
-   
- intros (N R);apply (prove ((∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y));
- 
- apply (⇒_i [H] (∀z:N.(∃x:N.R x z)⇒∃y:N.R z y));
- apply (∀_i [z] ((∃x:N.R x z)⇒∃y:N.R z y));
- apply (⇒_i [H2] (∃y:N.R z y));
- apply (∃_e (∃x:N.R x z) [n] [H3] (∃y:N.R z y));
-  [ apply [H2]
-  | apply (∃_i n (R z n));
-    apply (⇒_e (R n z ⇒ R z n) (R n z));
-     [ apply (∀_e (∀b:N.R n b ⇒ R b n) z);
-       apply (∀_e (∀a:N.∀b:N.R a b ⇒ R b a) n);
-       apply [H]
-     | apply [H3]
-     ]
-  ]
-qed.
-*)
\ No newline at end of file