X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpropositional_sequent_calculus.ma;h=42ae9682532ce8f65811f23944ec7e0f2a83cf0c;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=d647830bff9e938afb1446cf670dab4e647fdcf3;hpb=b671a48a8cdce63bd7b15af656a75a91463c0e31;p=helm.git

diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
index d647830bf..42ae96825 100644
--- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma
+++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/demo/propositional_sequent_calculus/".
-
 include "nat/plus.ma".
 include "nat/compare.ma".
 include "list/sort.ma".
@@ -183,6 +181,8 @@ axiom symm_andb: symmetric ? andb.
 axiom associative_andb: associative ? andb.
 axiom distributive_andb_orb: distributive ? andb orb.
 
+lemma andb_true: ∀x.(true ∧ x) = x. intro; reflexivity. qed. 
+
 lemma and_of_list_permut:
  ∀i,f,l1,l2. eval i (and_of_list (l1 @ (f::l2))) = eval i (and_of_list (f :: l1 @ l2)).
  intros;
@@ -244,11 +244,20 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F).
     lapply (H4 i); clear H4;
     rewrite > symm_orb in ⊢ (? ? (? ? %) ?);
     rewrite > distributive_orb_andb;
+    demodulate.
+    reflexivity.
+    (*
     autobatch paramodulation
+      by distributive_orb_andb,symm_orb,symm_orb, 
+         Hletin, Hletin1,andb_true.
+    *)
   | simplify in H2 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
-    autobatch
+    pump 100. pump 100.
+    demodulate.
+    reflexivity. 
+    (* autobatch paramodulation by andb_assoc, Hletin. *) 
   | simplify in H2 H4 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
@@ -258,11 +267,13 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F).
     rewrite > demorgan2;
     rewrite > symm_orb;
     rewrite > distributive_orb_andb;
-    autobatch paramodulation
+    demodulate.
+    reflexivity.
+    (* autobatch paramodulation by symm_andb,symm_orb,andb_true,Hletin,Hletin1. *)
   | simplify in H2 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
-    autobatch
+    autobatch paramodulation;
   | simplify in H2 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
@@ -422,8 +433,7 @@ lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2.
   [1,2:
     simplify in H;
     destruct H
-  | generalize in match H; clear H;
-    elim f2;
+  | elim f2 in H ⊢ %;
      [1,2:
        simplify in H;
        destruct H
@@ -511,7 +521,7 @@ lemma look_for_axiom:
           simplify;
           apply (ex_intro ? ? a3);
           apply (ex_intro ? ? a4);
-          autobatch
+          autobatch depth=4
         | right;
           intro;
           apply (bool_elim ? (same_atom a (FAtom n1)));
@@ -588,16 +598,10 @@ lemma sizel_0_no_axiom_is_tautology:
  intros;
  lapply (H1 (λn.mem ? same_atom (FAtom n) l1)); clear H1;
  simplify in Hletin;  
- generalize in match Hletin; clear Hletin;
- generalize in match H2; clear H2;
- generalize in match H; clear H;
- elim l1 0;
+ elim l1 in Hletin H2 H ⊢ % 0;
   [ intros;
     simplify in H2;
-    generalize in match H2; clear H2;
-    generalize in match H1; clear H1;
-    generalize in match H; clear H;
-    elim l2 0;
+    elim l2 in H2 H1 H ⊢ % 0;
      [ intros;
        simplify in H2;
        destruct H2
@@ -677,8 +681,7 @@ lemma sizel_0_no_axiom_is_tautology:
         | assumption
         | lapply (H2 n1); clear H2;
           simplify in Hletin;
-          generalize in match Hletin; clear Hletin;
-          elim (eqb n1 n);
+          elim (eqb n1 n) in Hletin ⊢ %;
            [ simplify in H2;
              rewrite > H2;
              autobatch
@@ -693,10 +696,7 @@ lemma sizel_0_no_axiom_is_tautology:
           rewrite > eqb_n_n in H3;
           simplify in H3;
 (*
-          generalize in match H3;
-          generalize in match H1; clear H1;
-          generalize in match H; clear H;
-          elim l 0;
+          elim l in H3 H1 H ⊢ % 0;
            [ elim l2 0;
               [ intros;
                 simplify in H2;
@@ -714,9 +714,7 @@ lemma sizel_0_no_axiom_is_tautology:
                  ]
                     
                  [ autobatch
-                 | generalize in match H4; clear H4;
-                   generalize in match H2; clear H2;
-                   elim t1;
+                 | elim t1 in H4 H2 ⊢ %;
                     [
                     |
                     |