From 046dadc88aaa639e4efe54acdc35b564ca189cce Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 18 Jul 2008 14:47:29 +0000
Subject: [PATCH] New input notation for bottom-up tree construction finished.

---
 .../matita/library/demo/natural_deduction.ma  | 32 ++++++++++++-------
 1 file changed, 20 insertions(+), 12 deletions(-)

diff --git a/helm/software/matita/library/demo/natural_deduction.ma b/helm/software/matita/library/demo/natural_deduction.ma
index e0c689720..68d7327fd 100644
--- a/helm/software/matita/library/demo/natural_deduction.ma
+++ b/helm/software/matita/library/demo/natural_deduction.ma
@@ -130,7 +130,14 @@ notation > "∨\sub\i\sup\r term 90 a" with precedence 19
 for @{ Or_intro_r ?? (cast $a ?) }.
 notation > "∨\sub\e term 90 ab [ident Ha] term 90 c1 [ident Hb] term 90 c2" with precedence 19
 for @{ Or_elim ??? (cast $ab ?) (λ${ident Ha}.cast $c1 ?) (λ${ident Hb}.cast $c2 ?) }.
-
+notation > "∀\sub\i [ident z] term 90 a" with precedence 19
+for @{ Forall_intro ?? (λ${ident z}.cast $a ?) }.
+notation > "∀\sub\e term 90 ab" with precedence 19
+for @{ Forall_elim ?? ? (cast $ab ?) }.
+notation > "∃\sub\e term 90 enpn [ident z] [ident pz] term 90 c" with precedence 19
+for @{ Exists_elim ??? (cast $enpn ?) (λ${ident z}.λ${ident pz}.cast $c ?) }.
+notation > "∃\sub\i term 90 n term 90 pn" with precedence 19
+for @{ Exists_intro ? (λ_.?) $n (cast $pn ?) }.
 
 lemma ex1 : (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
  apply cast;
@@ -157,17 +164,18 @@ axiom N: Type.
 axiom R: N → N → CProp.
 
 lemma ex2: (∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y.
- apply cast; apply Imply_intro; intro;
- apply cast; apply Forall_intro; intro z;
- apply cast; apply Imply_intro; intro;
- apply cast; apply (Exists_elim N (λy.R y z)); try intros (n);
-  [ apply cast; assumption
-  | apply cast; apply (Exists_intro ? ? n);
-    apply cast; apply (Imply_elim (R n z) (R z n));
-     [ apply cast; apply (Forall_elim N (λb:N.R n b ⇒ R b n) z);
-       apply cast; apply (Forall_elim N (λa:N.∀b:N.R a b ⇒ R b a) n);
-       apply cast; assumption
-     | apply cast; assumption
+ apply cast;
+ apply (⇒\sub\i [H] (∀z:N.(∃x:N.R x z)⇒∃y:N.R z y));
+ apply (∀\sub\i [z] ((∃x:N.R x z)⇒∃y:N.R z y));
+ apply (⇒\sub\i [H2] (∃y:N.R z y));
+ apply (∃\sub\e (∃x:N.R x z) [n] [H3] (∃y:N.R z y));
+  [ apply [H2]
+  | apply (∃\sub\i n (R z n));
+    apply (⇒\sub\e (R n z ⇒ R z n) (R n z));
+     [ apply (∀\sub\e (∀b:N.R n b ⇒ R b n));
+       apply (∀\sub\e (∀a:N.∀b:N.R a b ⇒ R b a));
+       apply [H]
+     | apply [H3]
      ]
   ]
 qed.
\ No newline at end of file
-- 
2.39.2