apply rule (lem EM) works

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 7d4e1ff11ca5ae0a0828c707933425c04217347e..de1c1f482cf91cd1cafbd54565cd119ae9c974df 100644 (file)
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -24,7 +24,8 @@ apply rule (prove (A ∨ ¬A));
 apply rule (RAA [H] (⊥)).
 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
        [ apply rule (discharge [H]).
-       | apply rule (¬_e (¬¬A) (¬A));
+       | apply rule (⊥_e (⊥));
+         apply rule (¬_e (¬¬A) (¬A));
           [ apply rule (¬_i [K] (⊥)).
        apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
              [ apply rule (discharge [H]).
@@ -58,6 +59,14 @@ apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
                 | apply rule (discharge [M]).
                 ]
              ]
-          | apply rule EM;
+          | apply rule (∨_e (B ∨ ¬B) [h1] (B) [h2] (B));
+              [ apply rule (lem EM);
+              
+
+              | apply rule (discharge [h1]);
+              |
+              ]
+ 
+          apply rule (show EM);
           ]
        ]

diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index 8a7399167dbad84a2cf4a8002e14aed19e035597..9ae03f502df8200fd670e8b8802a74c967545e10 100644 (file)
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -111,6 +111,43 @@ notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19
 for @{ 'leaf_ko $a $t }.
 interpretation "leaf KO" 'leaf_ko a t = (cast _ _ (show a t)).
 
+(* already proved lemma *)
+definition Lemma : ∀A.A→A ≝ λA:CProp.λa:A.a.
+
+notation < "\infrule \nbsp p mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19
+for @{ 'lemma_ko_1 $p $H }.
+interpretation "lemma_ko_1" 'lemma_ko_1 p H = 
+  (show p (cast _ _ (Lemma _ H))). 
+
+notation < "\infrule \nbsp mstyle color #ff0000 (p) mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19
+for @{ 'lemma_ko_2 $p $H }.
+interpretation "lemma_ko_2" 'lemma_ko_2 p H = 
+  (cast _ _ (show p (cast _ _ (Lemma _ H)))). 
+
+notation < "\infrule \nbsp p (\lem\emsp H)" non associative with precedence 19
+for @{ 'lemma_ok_1 $p $H }.
+interpretation "lemma_ok_1" 'lemma_ok_1 p H = 
+  (show p (Lemma _ H)). 
+interpretation "lemma_ok_11" 'lemma_ok_1 p H = 
+  (show p (Lemma _ H _)). 
+interpretation "lemma_ok_111" 'lemma_ok_1 p H = 
+  (show p (Lemma _ H _ _)). 
+
+notation < "\infrule \nbsp mstyle color #ff0000 (p) (\lem\emsp H)" non associative with precedence 19
+for @{ 'lemma_ok_2 $p $H }.
+interpretation "lemma_ok_2" 'lemma_ok_2 p H = 
+  (cast _ _ (show p (Lemma _ H))). 
+interpretation "lemma_ok_22" 'lemma_ok_2 p H = 
+  (cast _ _ (show p (Lemma _ H _))). 
+interpretation "lemma_ok_22" 'lemma_ok_2 p H = 
+  (cast _ _ (show p (Lemma _ H _ _))). 
+
+notation > "'lem' term 90 p" non associative with precedence 19
+for @{ 'Lemma $p  }.
+interpretation "lemma KO" 'Lemma p = (cast _ _ (Lemma _ p)).
+interpretation "lemma OK" 'Lemma p = (Lemma _ p).
+
+
 (* discharging *)
 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 
 for @{ 'discharge_ko_1 $a $H }.
@@ -310,7 +347,7 @@ 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 }.
+for @{ 'Or_intro_r_ok_2 $a $ab }.
 interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = 
   (cast _ _ (show ab (Or_intro_r _ _ a))).
 
@@ -427,22 +464,22 @@ 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 
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub(\emsp\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) (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 
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub(\emsp\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) (cast _ _ a))))).
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub\e) " with precedence 19 
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub(\emsp\e)) " 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)).
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub\e) " with precedence 19 
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub(\emsp\e)) " with precedence 19 
 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))).

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 62eefcfd7cf31625053a6ef4c8f71fbec9cd1991..a14858d9109cdf8381fa57947a395e70a961c8e2 100644 (file)
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1597,12 +1597,24 @@
                                             <property name="response_id">0</property>
                                           </widget>
                                         </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butUseLemma">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Use lemma (lem)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">1</property>
+                                          </packing>
+                                        </child>
                                         <child>
                                           <widget class="GtkButton" id="butDischarge">
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Discharge (discharge [  ])</property>
+                                            <property name="label" translatable="yes">Discharge (discharge)</property>
                                             <property name="response_id">0</property>
                                           </widget>
                                           <packing>
@@ -2338,59 +2350,6 @@
         <property name="n_rows">3</property>
         <property name="n_columns">2</property>
         <property name="row_spacing">5</property>
-        <child>
-          <widget class="GtkLabel" id="label17">
-            <property name="visible">True</property>
-            <property name="xalign">0</property>
-            <property name="label" translatable="yes">Find:</property>
-          </widget>
-          <packing>
-            <property name="x_options"></property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkLabel" id="label18">
-            <property name="visible">True</property>
-            <property name="xalign">0</property>
-            <property name="label" translatable="yes">Replace with: </property>
-          </widget>
-          <packing>
-            <property name="top_attach">1</property>
-            <property name="bottom_attach">2</property>
-            <property name="x_options"></property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkEntry" id="findEntry">
-            <property name="visible">True</property>
-            <property name="can_focus">True</property>
-            <property name="has_focus">True</property>
-            <property name="can_default">True</property>
-            <property name="has_default">True</property>
-            <property name="invisible_char">*</property>
-          </widget>
-          <packing>
-            <property name="left_attach">1</property>
-            <property name="right_attach">2</property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkEntry" id="replaceEntry">
-            <property name="visible">True</property>
-            <property name="can_focus">True</property>
-            <property name="invisible_char">*</property>
-          </widget>
-          <packing>
-            <property name="left_attach">1</property>
-            <property name="right_attach">2</property>
-            <property name="top_attach">1</property>
-            <property name="bottom_attach">2</property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
         <child>
           <widget class="GtkHBox" id="hbox19">
             <property name="visible">True</property>
@@ -2489,6 +2448,59 @@
             <property name="y_padding">5</property>
           </packing>
         </child>
+        <child>
+          <widget class="GtkEntry" id="replaceEntry">
+            <property name="visible">True</property>
+            <property name="can_focus">True</property>
+            <property name="invisible_char">*</property>
+          </widget>
+          <packing>
+            <property name="left_attach">1</property>
+            <property name="right_attach">2</property>
+            <property name="top_attach">1</property>
+            <property name="bottom_attach">2</property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkEntry" id="findEntry">
+            <property name="visible">True</property>
+            <property name="can_focus">True</property>
+            <property name="has_focus">True</property>
+            <property name="can_default">True</property>
+            <property name="has_default">True</property>
+            <property name="invisible_char">*</property>
+          </widget>
+          <packing>
+            <property name="left_attach">1</property>
+            <property name="right_attach">2</property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkLabel" id="label18">
+            <property name="visible">True</property>
+            <property name="xalign">0</property>
+            <property name="label" translatable="yes">Replace with: </property>
+          </widget>
+          <packing>
+            <property name="top_attach">1</property>
+            <property name="bottom_attach">2</property>
+            <property name="x_options"></property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkLabel" id="label17">
+            <property name="visible">True</property>
+            <property name="xalign">0</property>
+            <property name="label" translatable="yes">Find:</property>
+          </widget>
+          <packing>
+            <property name="x_options"></property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
       </widget>
     </child>
   </widget>

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 84909e95bd99d12738cec8c54f1e1fcac128ea36..db26ba20a55d7575e54f6b9932e5c0d71aa1404e 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -791,6 +791,8 @@ class gui () =
         (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n");
       connect_button main#butRAA
         (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
+      connect_button main#butUseLemma
+        (fun () -> source_buffer#insert "apply rule (lem …);\n");
       connect_button main#butDischarge
         (fun () -> source_buffer#insert "apply rule (discharge […]);\n");