X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdidactic%2Fsupport%2Fnatural_deduction.ma;h=c592b5254a3df4469f5af82c49e1fb9b0f6c6276;hb=6090d3df71fdd405d231981c8bf2aedff01612c5;hp=f5799b90e3a9435a90253876ed4903e42296fc52;hpb=2030cae5f1a588fa6bbea50927030f83a2156d67;p=helm.git

diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index f5799b90e..c592b5254 100644
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -103,13 +103,10 @@ axiom L : CProp.
 axiom M : CProp.
 axiom N : CProp.
 axiom O : CProp.
-axiom P : sort →CProp.
-axiom Q : sort →CProp.
-axiom R : sort →sort →CProp.
-axiom S : sort →sort →CProp.
-axiom f : sort → sort.
-axiom g : sort → sort.
-axiom h : sort → sort → sort.
+axiom  x: sort.
+axiom  y: sort.
+axiom  z: sort.
+axiom  w: sort.
 
 (* Every formula user provided annotates its proof:
    `A` becomes `(show A ?)` *)
@@ -167,7 +164,7 @@ for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 interpretation "Imply_intro_ko_2" 'Imply_intro_ko_2 ab \eta.b = 
   (cast _ _ (show ab (cast _ _ (Imply_intro _ _ b)))).
 
-notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19
+notation < "maction (\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) ) (\vdots)" with precedence 19
 for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b = 
   (show ab (Imply_intro _ _ b)).
@@ -195,7 +192,7 @@ for @{ 'Imply_elim_ko_2 $ab $a $b }.
 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b = 
   (cast _ _ (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a))))).
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) " with precedence 19 
+notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) ) (\vdots)" with precedence 19 
 for @{ 'Imply_elim_ok_1 $ab $a $b }.
 interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b = 
   (show b (Imply_elim _ _ ab a)).
@@ -223,7 +220,7 @@ for @{ 'And_intro_ko_2 $a $b $ab }.
 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab = 
   (cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))).
 
-notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)" with precedence 19 
+notation < "maction (\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)) (\vdots)" with precedence 19 
 for @{ 'And_intro_ok_1 $a $b $ab }.
 interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab = 
   (show ab (And_intro _ _ a b)).
@@ -249,7 +246,7 @@ for @{ 'And_elim_l_ko_2 $ab $a }.
 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a = 
   (cast _ _ (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab))))).
 
-notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19 
+notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))) (\vdots)" with precedence 19 
 for @{ 'And_elim_l_ok_1 $ab $a }.
 interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a = 
   (show a (And_elim_l _ _ ab)).
@@ -274,7 +271,7 @@ for @{ 'And_elim_r_ko_2 $ab $a }.
 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a = 
   (cast _ _ (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab))))).
 
-notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))" with precedence 19 
+notation < "maction (\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))) (\vdots)" with precedence 19 
 for @{ 'And_elim_r_ok_1 $ab $a }.
 interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a = 
   (show a (And_elim_r _ _ ab)).
@@ -300,7 +297,7 @@ for @{ 'Or_intro_l_ko_2 $a $ab }.
 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab = 
   (cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))).
 
-notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19 
+notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))) (\vdots)" with precedence 19 
 for @{ 'Or_intro_l_ok_1 $a $ab }.
 interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab = 
   (show ab (Or_intro_l _ _ a)).
@@ -325,7 +322,7 @@ for @{ 'Or_intro_r_ko_2 $a $ab }.
 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab = 
   (cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))).
 
-notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" with precedence 19 
+notation < "maction (\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))) (\vdots)" with precedence 19 
 for @{ 'Or_intro_r_ok_1 $a $ab }.
 interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab = 
   (show ab (Or_intro_r _ _ a)).
@@ -351,7 +348,7 @@ for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c = 
   (cast _ _ (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc))))).
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
+notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)) (\vdots)" with precedence 19
 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c = 
   (show c (Or_elim _ _ _ ab ac bc)).
@@ -383,11 +380,11 @@ for @{'Top_intro_ko_2}.
 interpretation "Top_intro_ko_2" 'Top_intro_ko_2 = 
   (cast _ _ (show _ (cast _ _ Top_intro))).
 
-notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19 
+notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19 
 for @{'Top_intro_ok_1}.
 interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro).
 
-notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19 
+notation < "maction (\infrule \nbsp ⊤ (⊤\sub\i)) (\vdots)" with precedence 19 
 for @{'Top_intro_ok_2 }.
 interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast _ _ (show _ Top_intro)).
 
@@ -406,7 +403,7 @@ for @{'Bot_elim_ko_2 $a $b}.
 interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b = 
   (cast _ _ (show a (Bot_elim _ (cast _ _ b)))).
 
-notation < "\infrule b a (⊥\sub\e)" with precedence 19 
+notation < "maction (\infrule b a (⊥\sub\e)) (\vdots)" with precedence 19 
 for @{'Bot_elim_ok_1 $a $b}.
 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b = 
   (show a (Bot_elim _ b)).
@@ -432,7 +429,7 @@ for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
 interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b = 
   (cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))).
 
-notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) " with precedence 19
+notation < "maction (\infrule hbox(\emsp b \emsp) ab (\lnot\sub(\emsp\i) \emsp ident H) ) (\vdots)" with precedence 19
 for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
 interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b = 
   (show ab (Not_intro _ b)).
@@ -458,7 +455,7 @@ for @{ 'Not_elim_ko_2 $ab $a $b }.
 interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b = 
   (cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))))).
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) " with precedence 19 
+notation < "maction (\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) ) (\vdots)" with precedence 19 
 for @{ 'Not_elim_ok_1 $ab $a $b }.
 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b = 
   (show b (Not_elim _ ab a)).
@@ -486,7 +483,7 @@ for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn = 
   (cast _ _ (show Pn (cast _ _ (Raa _ (cast _ _ Px))))).
 
-notation < "\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)) (\vdots)" with precedence 19
 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn = 
   (show Pn (Raa _ Px)).
@@ -512,7 +509,7 @@ for @{ 'Exists_intro_ko_2 $Pn $Px }.
 interpretation "Exists_intro_ko_2" 'Exists_intro_ko_2 Pn Px = 
   (cast _ _ (show Px (cast _ _ (Exists_intro _ _ _ (cast _ _ Pn))))).
 
-notation < "\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)) (\vdots)" with precedence 19
 for @{ 'Exists_intro_ok_1 $Pn $Px }.
 interpretation "Exists_intro_ok_1" 'Exists_intro_ok_1 Pn Px = 
   (show Px (Exists_intro _ _ _ Pn)).
@@ -523,7 +520,7 @@ interpretation "Exists_intro_ok_2" 'Exists_intro_ok_2 Pn Px =
   (cast _ _ (show Px (Exists_intro _ _ _ Pn))).
 
 notation >"∃_'i' {term 90 t} term 90 Pt" non associative with precedence 19
-for @{'Exists_intro $t (λ_.?) (show $Pt ?)}. 
+for @{'Exists_intro $t (λw.? w) (show $Pt ?)}. 
 interpretation "Exists_intro KO" 'Exists_intro t P Pt =
  (cast _ _ (Exists_intro sort P t (cast _ _ Pt))).
 interpretation "Exists_intro OK" 'Exists_intro t P Pt =
@@ -540,7 +537,7 @@ for @{ 'Exists_elim_ko_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 interpretation "Exists_elim_ko_2" 'Exists_elim_ko_2 ExPx Pc c =
     (cast _ _ (show c (cast _ _ (Exists_elim _ _ _ (cast _ _ ExPx) (cast _ _ Pc))))).
 
-notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19
+notation < "maction (\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)) (\vdots)" with precedence 19
 for @{ 'Exists_elim_ok_1 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 interpretation "Exists_elim_ok_1" 'Exists_elim_ok_1 ExPx Pc c =
     (show c (Exists_elim _ _ _ ExPx Pc)).
@@ -550,14 +547,16 @@ for @{ 'Exists_elim_ok_2 $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
 interpretation "Exists_elim_ok_2" 'Exists_elim_ok_2 ExPx Pc c =
     (cast _ _ (show c (Exists_elim _ _ _ ExPx Pc))).
 
-definition ex_concl := λx:CProp.sort → unit → x.
+definition ex_concl := λx:sort → CProp.∀y:sort.unit → x y.
+definition ex_concl_dummy := ∀y:sort.unit → unit.
 definition fake_pred := λx:sort.unit.
 
 notation >"∃_'e' term 90 ExPt {ident t} [ident H] term 90 c" non associative with precedence 19
-for @{'Exists_elim (λ_.?) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}. 
+for @{'Exists_elim (λx.? x) (show $ExPt ?) (λ${ident t}:sort.λ${ident H}.show $c ?)}. 
 interpretation "Exists_elim KO" 'Exists_elim P ExPt c =
  (cast _ _ (Exists_elim sort P _ 
-   (cast (Exists _ P)  _ ExPt) (cast (ex_concl unit) (ex_concl _) c))).
+   (cast (Exists _ P)  _ ExPt) 
+   (cast ex_concl_dummy (ex_concl _) c))).
 interpretation "Exists_elim OK" 'Exists_elim P ExPt c =
  (Exists_elim sort P _ ExPt c).
 
@@ -573,7 +572,7 @@ for @{ 'Forall_intro_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "Forall_intro_ko_2" 'Forall_intro_ko_2 Px Pn = 
   (cast _ _ (show Pn (cast _ _ (Forall_intro _ _ (cast _ _ Px))))).
 
-notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)) (\vdots)" with precedence 19
 for @{ 'Forall_intro_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "Forall_intro_ok_1" 'Forall_intro_ok_1 Px Pn = 
   (show Pn (Forall_intro _ _ Px)).
@@ -601,7 +600,7 @@ for @{ 'Forall_elim_ko_2 $Px $Pn }.
 interpretation "Forall_elim_ko_2" 'Forall_elim_ko_2 Px Pn = 
   (cast _ _ (show Pn (cast _ _ (Forall_elim _ _ _ (cast _ _ Px))))).
 
-notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)" with precedence 19
+notation < "maction (\infrule hbox(\emsp Px \emsp) Pn (∀\sub\e)) (\vdots)" with precedence 19
 for @{ 'Forall_elim_ok_1 $Px $Pn }.
 interpretation "Forall_elim_ok_1" 'Forall_elim_ok_1 Px Pn = 
   (show Pn (Forall_elim _ _ _ Px)).