From: Enrico Tassi Date: Sat, 15 Nov 2008 14:56:05 +0000 (+0000) Subject: almost ready X-Git-Tag: make_still_working~4556 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b14d3611e67633ffa5b661e38331db4ea83ca429;p=helm.git almost ready --- diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index aa370ab69..f98e795f2 100644 --- 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 index 000000000..8ec8d6fd7 --- /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 99e047a9d..3e7c54d5c 100644 --- 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 2447b2881..d33743eda 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -1453,7 +1453,7 @@ True True True - Negaton (¬_i) + Negation (¬_i) 0 @@ -1545,7 +1545,7 @@ True True True - Negaton (¬_e) + Negation (¬_e) 0