From 214b87039cc59cc6ecb5a54cf68b296b0a3ada92 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 15 Nov 2008 14:33:49 +0000 Subject: [PATCH] rules fixed --- .../matita/library/demo/natural_deduction.ma | 126 +++---- helm/software/matita/library/depends | 11 +- .../didactic/support/natural_deduction.ma | 329 +++++++++++------- helm/software/matita/matita.glade | 119 ++++--- helm/software/matita/matitaGui.ml | 23 +- 5 files changed, 336 insertions(+), 272 deletions(-) diff --git a/helm/software/matita/library/demo/natural_deduction.ma b/helm/software/matita/library/demo/natural_deduction.ma index 64b3daccb..14359325b 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 diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index 27032d916..aa370ab69 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -19,12 +19,13 @@ Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma datatypes/compare.ma +didactic/exercises/substitution.ma nat/minus.ma nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma formal_topology/basic_topologies.ma datatypes/categories.ma formal_topology/relations.ma formal_topology/saturations_reductions.ma logic/connectives.ma Q/nat_fact/times.ma nat/factorization.ma decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma -demo/natural_deduction_support.ma +didactic/exercises/duality.ma nat/minus.ma nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma nat/times.ma nat/plus.ma @@ -50,10 +51,12 @@ nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma demo/realisability.ma datatypes/constructors.ma logic/connectives.ma list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma +didactic/support/natural_deduction.ma nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma formal_topology/basic_pairs.ma datatypes/categories.ma formal_topology/relations.ma Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/factorization.ma nat/nat.ma +didactic/exercises/shannon.ma nat/minus.ma Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma formal_topology/concrete_spaces.ma formal_topology/basic_pairs.ma nat/minus.ma nat/compare.ma nat/le_arith.ma @@ -69,8 +72,8 @@ formal_topology/relations.ma datatypes/subsets.ma nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma Z/moebius.ma Z/sigma_p.ma nat/factorization.ma demo/toolbox.ma logic/cprop_connectives.ma -nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma logic/coimplication.ma logic/connectives.ma +nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma nat/minimization.ma nat/minus.ma logic/connectives2.ma higher_order_defs/relations.ma datatypes/subsets.ma datatypes/categories.ma logic/cprop_connectives.ma @@ -80,10 +83,10 @@ Q/q/q.ma Q/fraction/numerator_denominator.ma Q/ratio/ratio.ma nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sieve.ma nat/sqrt.ma nat/nat.ma higher_order_defs/functions.ma Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma -demo/natural_deduction.ma +demo/natural_deduction.ma didactic/support/natural_deduction.ma higher_order_defs/ordering.ma logic/equality.ma -nat/congruence.ma nat/primes.ma nat/relevant_equations.ma logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma +nat/congruence.ma nat/primes.ma nat/relevant_equations.ma nat/gcd.ma nat/lt_arith.ma nat/primes.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma Z/compare.ma Z/orders.ma nat/compare.ma diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma index 3969197e9..99e047a9d 100644 --- a/helm/software/matita/library/didactic/support/natural_deduction.ma +++ b/helm/software/matita/library/didactic/support/natural_deduction.ma @@ -40,7 +40,7 @@ definition Not_intro : ∀A.(A → Bot) → Not A ≝ λA. definition Not_elim : ∀A.Not A → A → Bot ≝ λA. Imply_elim ? Bot. -definition assumpt := λA:CProp.λa:A. +definition Discharge := λA:CProp.λa:A. a. axiom Raa : ∀A.(Not A → Bot) → A. @@ -90,36 +90,52 @@ axiom X : CProp. axiom Y : CProp. axiom Z : CProp. -(* Every formula user provided annotates its proof A becomes (show A ?) *) +(* Every formula user provided annotates its proof: + `A` becomes `(show A ?)` *) 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. +(* 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 _). -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)). - -notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 for @{ 'assumpt_ko $a $H }. -interpretation "assumption_ko 1" 'assumpt_ko a H = (show a (cast _ _ (assumpt _ H))). -interpretation "assumption_ko 2" 'assumpt_ko a H = (cast _ _ (show a (cast _ _ (assumpt _ H)))). - -notation < "[ a ] \sup H" with precedence 19 for @{ 'assumpt_ok $a $H }. -interpretation "assumption_ok 1" 'assumpt_ok a H = (show a (assumpt a H)). -notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 for @{ 'assumpt_ok_2 $a $H }. -interpretation "assumption_ok 2" 'assumpt_ok_2 a H = (cast _ _ (show a (assumpt a H))). - -notation > "[H]" with precedence 90 for @{ 'assumpt $H }. -interpretation "assumpt KO" 'assumpt H = (cast _ _ (assumpt _ H)). -interpretation "assumpt OK" 'assumpt H = (assumpt _ H). - +(* discharging *) +notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 +for @{ 'discharge_ko_1 $a $H }. +interpretation "discharge_ko_1" 'discharge_ko_1 a H = + (show a (cast _ _ (Discharge _ H))). +notation < "[ mstyle color #ff0000 (a) ] \sup mstyle color #ff0000 (H)" with precedence 19 +for @{ 'discharge_ko_2 $a $H }. +interpretation "discharge_ko_2" 'discharge_ko_2 a H = + (cast _ _ (show a (cast _ _ (Discharge _ H)))). + +notation < "[ a ] \sup H" with precedence 19 +for @{ 'discharge_ok_1 $a $H }. +interpretation "discharge_ok_1" 'discharge_ok_1 a H = + (show a (Discharge _ H)). +notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 +for @{ 'discharge_ok_2 $a $H }. +interpretation "discharge_ok_2" 'discharge_ok_2 a H = + (cast _ _ (show a (Discharge _ H))). + +notation > "'discharge' [H]" with precedence 19 +for @{ 'discharge $H }. +interpretation "discharge KO" 'discharge H = (cast _ _ (Discharge _ H)). +interpretation "discharge OK" 'discharge H = (Discharge _ H). + +(* ⇒ introduction *) notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19 for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }. interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b = @@ -127,7 +143,7 @@ interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b = notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19 for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }. -interpretation "Imply_intro_ko_1" 'Imply_intro_ko_2 ab \eta.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 @@ -142,15 +158,21 @@ interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b = notation > "⇒_'i' [ident H] term 90 b" with precedence 19 for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }. -interpretation "Imply_intro KO" 'Imply_intro b pb = (cast _ (Imply unit b) (Imply_intro _ b pb)). -interpretation "Imply_intro OK" 'Imply_intro b pb = (Imply_intro _ b pb). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_1 $ab $a $b }. +interpretation "Imply_intro KO" 'Imply_intro b pb = + (cast _ (Imply unit b) (Imply_intro _ b pb)). +interpretation "Imply_intro OK" 'Imply_intro b pb = + (Imply_intro _ b pb). + +(* ⇒ elimination *) +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19 +for @{ 'Imply_elim_ko_1 $ab $a $b }. interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b = - (show b (cast _ _ (Imply_elim _ _ ab a))). -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_2 $ab $a $b }. + (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a)))). + +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19 +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 _ _ ab a)))). + (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 for @{ 'Imply_elim_ok_1 $ab $a $b }. @@ -162,14 +184,21 @@ for @{ 'Imply_elim_ok_2 $ab $a $b }. interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b = (cast _ _ (show b (Imply_elim _ _ ab a))). -notation > "⇒_'e' term 90 ab term 90 a" with precedence 19 for @{ 'Imply_elim (show $ab ?) (show $a ?) }. -interpretation "Imply_elim KO" 'Imply_elim ab a = (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))). -interpretation "Imply_elim OK" 'Imply_elim ab a = (Imply_elim _ _ ab a). +notation > "⇒_'e' term 90 ab term 90 a" with precedence 19 +for @{ 'Imply_elim (show $ab ?) (show $a ?) }. +interpretation "Imply_elim KO" 'Imply_elim ab a = + (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))). +interpretation "Imply_elim OK" 'Imply_elim ab a = + (Imply_elim _ _ ab a). -notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_1 $a $b $ab }. +(* ∧ introduction *) +notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19 +for @{ 'And_intro_ko_1 $a $b $ab }. interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab = (show ab (cast _ _ (And_intro _ _ a b))). -notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_2 $a $b $ab }. + +notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19 +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)))). @@ -183,19 +212,21 @@ for @{ 'And_intro_ok_2 $a $b $ab }. interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab = (cast _ _ (show ab (And_intro _ _ a b))). -notation > "∧_'i' term 90 a term 90 b" with precedence 19 for @{ 'And_intro (show $a ?) (show $b ?) }. +notation > "∧_'i' term 90 a term 90 b" with precedence 19 +for @{ 'And_intro (show $a ?) (show $b ?) }. interpretation "And_intro KO" 'And_intro a b = (cast _ _ (And_intro _ _ a b)). interpretation "And_intro OK" 'And_intro a b = (And_intro _ _ a b). +(* ∧ elimination *) notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 for @{ 'And_elim_l_ko_1 $ab $a }. interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a = - (show a (cast _ _ (And_elim_l _ _ ab))). + (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab)))). notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 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 _ _ ab)))). + (cast _ _ (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab))))). notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19 for @{ 'And_elim_l_ok_1 $ab $a }. @@ -209,18 +240,18 @@ interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a = notation > "∧_'e_l' term 90 ab" with precedence 19 for @{ 'And_elim_l (show $ab ?) }. -interpretation "And_elim_l KO" 'And_elim_l a = (And_elim_l _ _ (cast (And _ unit) _ a)). +interpretation "And_elim_l KO" 'And_elim_l a = (cast _ _ (And_elim_l _ _ (cast (And unit unit) _ a))). interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l _ _ a). notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 for @{ 'And_elim_r_ko_1 $ab $a }. interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a = - (show a (cast _ _ (And_elim_r _ _ ab))). + (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab)))). notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 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 _ _ ab)))). + (cast _ _ (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab))))). notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))" with precedence 19 for @{ 'And_elim_r_ok_1 $ab $a }. @@ -234,19 +265,10 @@ interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a = notation > "∧_'e_r' term 90 ab" with precedence 19 for @{ 'And_elim_r (show $ab ?) }. -interpretation "And_elim_r KO" 'And_elim_r a = (And_elim_r _ _ (cast (And unit _) _ a)). +interpretation "And_elim_r KO" 'And_elim_r a = (cast _ _ (And_elim_r _ _ (cast (And unit unit) _ a))). interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r _ _ a). -notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" 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)). - -notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 -for @{ 'Or_intro_l_ok_1 $a $ab }. -interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = - (cast _ _ (show ab (Or_intro_l _ _ a))). - +(* ∨ introduction *) notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 for @{ 'Or_intro_l_ko_1 $a $ab }. interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab = @@ -257,21 +279,21 @@ 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 +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)). + +notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 +for @{ 'Or_intro_l_ok_1 $a $ab }. +interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = + (cast _ _ (show ab (Or_intro_l _ _ a))). + notation > "∨_'i_l' term 90 a" with precedence 19 for @{ 'Or_intro_l (show $a ?) }. interpretation "Or_intro_l KO" 'Or_intro_l a = (cast _ (Or _ unit) (Or_intro_l _ _ a)). interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l _ _ a). -notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" 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)). - -notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19 -for @{ 'Or_intro_r_ok_1 $a $ab }. -interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = - (cast _ _ (show ab (Or_intro_r _ _ a))). - notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 for @{ 'Or_intro_r_ko_1 $a $ab }. interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab = @@ -282,11 +304,32 @@ 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 +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)). + +notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19 +for @{ 'Or_intro_r_ok_1 $a $ab }. +interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = + (cast _ _ (show ab (Or_intro_r _ _ a))). + notation > "∨_'i_r' term 90 a" with precedence 19 for @{ 'Or_intro_r (show $a ?) }. interpretation "Or_intro_r KO" 'Or_intro_r a = (cast _ (Or unit _) (Or_intro_r _ _ a)). interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r _ _ a). +(* ∨ elimination *) +notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19 +for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }. +interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc = + (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) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19 +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 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 = @@ -297,49 +340,67 @@ for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }. interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c = (cast _ _ (show c (Or_elim _ _ _ ab ac bc))). -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19 -for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }. -interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc = - (show c (cast _ _ (Or_elim _ _ _ ab (cast _ _ ac) (cast _ _ bc)))). - -notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19 -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 _ _ _ ab (cast _ _ ac) (cast _ _ bc))))). - definition unit_to ≝ λx:CProp.unit → x. notation > "∨_'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19 -for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) $cl $cr }. -interpretation "Or_elim KO" 'Or_elim ab ac bc c1 c2 = - (cast _ _ (Or_elim _ _ _ (cast (Or unit unit) _ ab) (cast (unit_to unit) (unit_to _) ac) (cast (unit_to unit) (unit_to _) bc))). -interpretation "Or_elim OK" 'Or_elim ab ac bc c1 c2 = (Or_elim _ _ _ ab ac bc). - +for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }. +interpretation "Or_elim KO" 'Or_elim ab ac bc = + (cast _ _ (Or_elim _ _ _ + (cast (Or unit unit) _ ab) + (cast (unit_to unit) (unit_to _) ac) + (cast (unit_to unit) (unit_to _) bc))). +interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim _ _ _ ab ac bc). + +(* ⊤ introduction *) notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19 for @{'Top_intro_ko_1}. -interpretation "Top_intro_ko_1" 'Top_intro_ko_1 = (show _ (cast _ _ Top_intro)). +interpretation "Top_intro_ko_1" 'Top_intro_ko_1 = + (show _ (cast _ _ Top_intro)). + +notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19 +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 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 +for @{'Top_intro_ok_2 }. +interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast _ _ (show _ Top_intro)). + notation > "⊤_'i'" with precedence 19 for @{ 'Top_intro }. interpretation "Top_intro KO" 'Top_intro = (cast _ _ Top_intro). interpretation "Top_intro OK" 'Top_intro = Top_intro. -notation < "\infrule b a (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ok_1 $a $b}. +(* ⊥ introduction *) +notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19 +for @{'Bot_elim_ko_1 $a $b}. +interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b = + (show a (Bot_elim _ (cast _ _ b))). + +notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19 +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 +for @{'Bot_elim_ok_1 $a $b}. interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b = - (show a (Bot_elim a b)). + (show a (Bot_elim _ b)). -notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ko_1 $a $b}. -interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b = - (show a (Bot_elim a (cast _ _ b))). +notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19 +for @{'Bot_elim_ok_2 $a $b}. +interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b = + (cast _ _ (show a (Bot_elim _ b))). notation > "⊥_'e' term 90 b" with precedence 19 for @{ 'Bot_elim (show $b ?) }. interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)). interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a). +(* ¬ introduction *) notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }. interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b = @@ -365,6 +426,17 @@ for @{ 'Not_intro (λ${ident H}.show $b ?) }. interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a))). interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a). +(* ¬ elimination *) +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))). + +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)))). + 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 }. interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b = @@ -375,21 +447,22 @@ for @{ 'Not_elim_ok_2 $ab $a $b }. interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b = (cast _ _ (show b (Not_elim _ ab 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 (Not_elim _ (cast _ _ ab) 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 (Not_elim _ (cast _ _ ab) a))). - 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 = (Not_elim _ (cast _ _ ab) 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). +(* RAA *) +notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19 +for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }. +interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn = + (show Pn (cast _ _ (Raa _ (cast _ _ Px)))). + +notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19 +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 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }. interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn = @@ -400,37 +473,57 @@ for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }. interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn = (cast _ _ (show Pn (Raa _ Px))). -notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19 -for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }. -interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn = - (show Pn (Raa _ (cast _ _ Px))). - -notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19 -for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }. -interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn = - (cast _ _ (show Pn (Raa _ (cast _ _ Px)))). - notation > "'RAA' [ident H] term 90 b" with precedence 19 for @{ 'Raa (λ${ident H}.show $b ?) }. -interpretation "RAA KO" 'Raa p = (Raa _ (cast _ (unit_to _) p)). +interpretation "RAA KO" 'Raa p = (cast _ unit (Raa _ (cast _ (unit_to _) p))). interpretation "RAA OK" 'Raa p = (Raa _ p). (*DOCBEGIN -Templates for rules -⇒_i […] (…) -∧_i (…) (…) -∨_i_l (…) -∨_i_r (…) -¬_i […] (…) -⊤_i -⇒_e (…) (…) -∧_e_l (…) -∧_e_r (…) -∨_e (…) […] (…) […] (…) -¬_e (…) (…) -⊥_e (…) -prove (…) -RAA […] (…) +Templates for rules: + + apply rule (⇒_i […] (…)). + + apply rule (∧_i (…) (…)); + [ + | + ] + + apply rule (∨_i_l (…)). + + apply rule (∨_i_r (…)). + + apply rule (¬_i […] (…)). + + apply rule (⊤_i). + + apply rule (⇒_e (…) (…)); + [ + | + ] + + apply rule (∧_e_l (…)). + + apply rule (∧_e_r (…)). + + apply rule (∨_e (…) […] (…) […] (…)); + [ + | + | + ] + + apply rule (¬_e (…) (…)); + [ + | + ] + + apply rule (⊥_e (…)). + + apply rule (prove (…)). + + apply rule (RAA […] (…)). + + apply rule (discharge […]). + DOCEND*) diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 2b239b4e5..2447b2881 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -1387,6 +1387,7 @@ True + 2 True @@ -1608,6 +1609,18 @@ 1 + + + True + True + True + Discharge (discharge [ ]) + 0 + + + 2 + + @@ -2337,6 +2350,59 @@ 3 2 5 + + + True + 0 + Find: + + + + + + + + + True + 0 + Replace with: + + + 1 + 2 + + + + + + + True + True + True + True + True + * + + + 1 + 2 + + + + + + True + True + * + + + 1 + 2 + 1 + 2 + + + True @@ -2435,59 +2501,6 @@ 5 - - - True - True - * - - - 1 - 2 - 1 - 2 - - - - - - True - True - True - True - True - * - - - 1 - 2 - - - - - - True - 0 - Replace with: - - - 1 - 2 - - - - - - - True - 0 - Find: - - - - - - diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 393da7cef..6acf7357a 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -762,25 +762,25 @@ class gui () = else main#tacticsButtonsHandlebox#misc#hide ()) ~check:main#menuitemPalette; connect_button main#butImpl_intro - (fun () -> source_buffer#insert "apply rule (⇒_i […] (…));\n"); + (fun () -> source_buffer#insert "apply rule (⇒_i […] (…)).\n"); connect_button main#butAnd_intro (fun () -> source_buffer#insert "apply rule (∧_i (…) (…));\n\t[\n\t|\n\t]\n"); connect_button main#butOr_intro_left - (fun () -> source_buffer#insert "apply rule (∨_i_l (…));\n"); + (fun () -> source_buffer#insert "apply rule (∨_i_l (…)).\n"); connect_button main#butOr_intro_right - (fun () -> source_buffer#insert "apply rule (∨_i_r (…));\n"); + (fun () -> source_buffer#insert "apply rule (∨_i_r (…)).\n"); connect_button main#butNot_intro - (fun () -> source_buffer#insert "apply rule (¬_i […] (…));\n"); + (fun () -> source_buffer#insert "apply rule (¬_i […] (…)).\n"); connect_button main#butTop_intro - (fun () -> source_buffer#insert "apply rule (⊤_i);\n"); + (fun () -> source_buffer#insert "apply rule (⊤_i).\n"); connect_button main#butImpl_elim (fun () -> source_buffer#insert "apply rule (⇒_e (…) (…));\n\t[\n\t|\n\t]\n"); connect_button main#butAnd_elim_left - (fun () -> source_buffer#insert "apply rule (∧_e_l (…));\n"); + (fun () -> source_buffer#insert "apply rule (∧_e_l (…)).\n"); connect_button main#butAnd_elim_right - (fun () -> source_buffer#insert "apply rule (∧_e_r (…));\n"); + (fun () -> source_buffer#insert "apply rule (∧_e_r (…)).\n"); connect_button main#butOr_elim (fun () -> source_buffer#insert "apply rule (∨_e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n"); @@ -788,11 +788,14 @@ class gui () = (fun () -> source_buffer#insert "apply rule (¬_e (…) (…));\n\t[\n\t|\n\t]\n"); connect_button main#butBot_elim - (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n"); + (fun () -> source_buffer#insert "apply rule (⊥_e (…)).\n"); connect_button main#butRAA - (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n"); + (fun () -> source_buffer#insert "apply rule (RAA […] (…)).\n"); connect_button main#butStart - (fun () -> source_buffer#insert "apply rule (prove (…));\n"); + (fun () -> source_buffer#insert "apply rule (prove (…)).\n"); + connect_button main#butDischarge + (fun () -> source_buffer#insert "apply rule (discharge […]).\n"); + (* TO BE REMOVED *) main#scriptNotebook#remove_page 1; -- 2.39.2