almost ready

diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index aa370ab695e073a90d1cbab8f14e7a24eec4e1cd..f98e795f219b0966b8d395954edbf4c9e975dba6 100644 (file)
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -108,6 +108,7 @@ Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma
 nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma
 nat/gcd_properties1.ma nat/gcd.ma
 list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma
+didactic/exercises/natural_deduction.ma didactic/support/natural_deduction.ma
 Z/times.ma Z/plus.ma nat/lt_arith.ma
 Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
 nat/o.ma nat/binomial.ma nat/sqrt.ma

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
new file mode 100644 (file)
index 0000000..8ec8d6f
--- /dev/null
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -0,0 +1,26 @@
+(* Esercizio 0
+   ===========
+
+   Compilare i seguenti campi:
+
+   Nome1: ...
+   Cognome1: ...
+   Matricola1: ...
+   Account1: ...
+
+   Nome2: ...
+   Cognome2: ...
+   Matricola2: ...
+   Account2: ...
+
+*)
+
+
+include "didactic/support/natural_deduction.ma".
+
+
+
+theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
+
+
+

diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index 99e047a9dcf64d2d42b5c5b0c26ec0aae4eb7b96..3e7c54d5cbbd6873921b72b9fc6060a6f774ac43 100644 (file)
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -97,19 +97,19 @@ definition show : ∀A.A→A ≝ λA:CProp.λa:A.a.
 (* When something does not fit, this daemon is used *)
 axiom cast: ∀A,B:CProp.B → A.
 
+(* begin a proof: draws the root *)
+notation > "'prove' p" non associative with precedence 19 
+for @{ 'prove $p }.
+interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
+interpretation "prove OK" 'prove p = (show p _).
+
 (* Leaves *)
 notation < "\infrule (t\atop ⋮) a ?" with precedence 19
 for @{ 'leaf_ok $a $t }.
 interpretation "leaf OK" 'leaf_ok a t = (show a t).
 notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 
 for @{ 'leaf_ko $a $t }.
-interpretation "leaf KO" 'leaf_ko a t = (cast _ a (show _ t)).
-
-(* begin a proof: draws the root *)
-notation > "'prove' p" non associative with precedence 19 
-for @{ 'prove $p }.
-interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
-interpretation "prove OK" 'prove p = (show p _).
+interpretation "leaf KO" 'leaf_ko a t = (cast _ _ (show a t)).
 
 (* discharging *)
 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 
@@ -430,12 +430,12 @@ interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a).
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 
 for @{ 'Not_elim_ko_1 $ab $a $b }.
 interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b = 
-  (show b (cast _ _ (Not_elim _ (cast _ _ ab) a))).
+  (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a)))).
 
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 
 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) a)))).
+  (cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))))).
 
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub\e) " with precedence 19 
 for @{ 'Not_elim_ok_1 $ab $a $b }.
@@ -449,8 +449,10 @@ interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b =
 
 notation > "¬_'e' term 90 ab term 90 a" with precedence 19
 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
-interpretation "Not_elim KO" 'Not_elim ab a = (cast _ unit (Not_elim _ (cast _ _ ab) a)).
-interpretation "Not_elim OK" 'Not_elim ab a = (Not_elim _ ab a).
+interpretation "Not_elim KO" 'Not_elim ab a = 
+  (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))).
+interpretation "Not_elim OK" 'Not_elim ab a = 
+  (Not_elim _ ab a).
 
 (* RAA *)
 notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 2447b28817684fd33d0d5398ea3f38e055e09416..d33743edab5de52e6072e9ffca1eb977a9487be7 100644 (file)
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1453,7 +1453,7 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Negaton (¬_i)</property>
+                                            <property name="label" translatable="yes">Negation (¬_i)</property>
                                             <property name="response_id">0</property>
                                           </widget>
                                           <packing>
@@ -1545,7 +1545,7 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Negaton (¬_e)</property>
+                                            <property name="label" translatable="yes">Negation (¬_e)</property>
                                             <property name="response_id">0</property>
                                           </widget>
                                           <packing>