update in ground_2

set up for equality insertion lemmas

diff --git a/matita/matita/contribs/lambdadelta/ground_2/insert_eq/insert_eq_0.ma b/matita/matita/contribs/lambdadelta/ground_2/insert_eq/insert_eq_0.ma
new file mode 100644 (file)
index 0000000..6a3788e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/insert_eq/insert_eq_0.ma
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basics/relations.ma".
+
+(* GENERATED LIBRARY ********************************************************)
+
+lemma insert_eq_0: ∀A,a. ∀Q1,Q2:predicate A. (∀a0. Q1 a0 → a = a0 → Q2 a0) → Q1 a → Q2 a.
+/2 width=1 by/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
index 27ef34de4a87509def939141ac20c87ba8def7ae..4bfd5c7c7fa1a867409da82b14622d09c7e94151 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
 (*                                                                        *)
 (**************************************************************************)
 

+include "ground_2/insert_eq/insert_eq_0.ma".

 include "ground_2/lib/functions.ma".
 
 (* LABELLED TRANSITIVE CLOSURE **********************************************)
 include "ground_2/lib/functions.ma".
 
 (* LABELLED TRANSITIVE CLOSURE **********************************************)


@@ -37,7 +38,7 @@ lemma ltc_ind_sn (A) (f) (B) (R) (Q:relation2 A B) (b2): associative … f →
                  (∀a,b1. R a b1 b2 → Q a b1) →
                  (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
                  ∀a,b1. ltc … f … R a b1 b2 → Q a b1.
                  (∀a,b1. R a b1 b2 → Q a b1) →
                  (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
                  ∀a,b1. ltc … f … R a b1 b2 → Q a b1.

-#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq … b2)
+#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq_0 … b2)

 #b0 #H elim H -a -b1 -b0 /2 width=2 by/
 #a1 #a2 #b1 #b #b0 #H #Hb2 #_
 generalize in match Hb2; generalize in match a2; -Hb2 -a2
 #b0 #H elim H -a -b1 -b0 /2 width=2 by/
 #a1 #a2 #b1 #b #b0 #H #Hb2 #_
 generalize in match Hb2; generalize in match a2; -Hb2 -a2


@@ -48,7 +49,7 @@ lemma ltc_ind_dx (A) (f) (B) (R) (Q:A→predicate B) (b1): associative … f →
                  (∀a,b2. R a b1 b2 → Q a b2) →
                  (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) →
                  ∀a,b2. ltc … f … R a b1 b2 → Q a b2.
                  (∀a,b2. R a b1 b2 → Q a b2) →
                  (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) →
                  ∀a,b2. ltc … f … R a b1 b2 → Q a b2.

-#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq … b1)
+#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq_0 … b1)

 #b0 #H elim H -a -b0 -b2 /2 width=2 by/
 #a1 #a2 #b0 #b #b2 #Hb0 #H #IHb0 #_
 generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0 -Hb0 -a1
 #b0 #H elim H -a -b0 -b2 /2 width=2 by/
 #a1 #a2 #b0 #b #b2 #Hb0 #H #IHb0 #_
 generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0 -Hb0 -a1

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
index 7c63b469f36ecaa02c2f6c11f11e6fb7a9e4e9a9..fa8bae34356880363acc0a6369876121b7bbe6d9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
@@ -17,9 +17,6 @@ include "ground_2/lib/logic.ma".
 
 (* GENERIC RELATIONS ********************************************************)
 
 
 (* GENERIC RELATIONS ********************************************************)
 

-lemma insert_eq: ∀A,a. ∀Q1,Q2:predicate A. (∀a0. Q1 a0 → a = a0 → Q2 a0) → Q1 a → Q2 a.
-/2 width=1 by/ qed-.
-

 definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B) ≝
                               λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2.
 
 definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B) ≝
                               λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2.
 

diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
index 06ff4be72bc290ad957976750c9ef53c66bc2de6..77174d94ba00845e5c198cfc28ecadffa057e2ce 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -62,8 +62,12 @@ table {
      }
    ]
    class "orange"
      }
    ]
    class "orange"

-   [ { "generated logical decomposables" * } {
-        [ { "" * } {
+   [ { "generated library" * } {
+        [ { "equality insertion" * } {
+             [ "insert_eq" * ]
+          }
+        ]
+        [ { "logical decomposables" * } {

              [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" * ]
           }
         ]
              [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" * ]
           }
         ]