From 658d76a1961418ee20d610bccff04b1d38cf206e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 12 Nov 2007 12:35:56 +0000 Subject: [PATCH] refactoring --- .../matita/contribs/LOGIC/Track/pred.ma | 5 ++++- .../{datatypes => datatypes_defs}/Context.ma | 8 ++++---- .../{datatypes => datatypes_defs}/Formula.ma | 2 +- .../{datatypes => datatypes_defs}/Proof.ma | 2 +- .../{datatypes => datatypes_defs}/Sequent.ma | 8 ++++---- .../contribs/LOGIC/datatypes_props/Sequent.ma | 19 +++++++++++++++++++ 6 files changed, 33 insertions(+), 11 deletions(-) rename helm/software/matita/contribs/LOGIC/{datatypes => datatypes_defs}/Context.ma (86%) rename helm/software/matita/contribs/LOGIC/{datatypes => datatypes_defs}/Formula.ma (95%) rename helm/software/matita/contribs/LOGIC/{datatypes => datatypes_defs}/Proof.ma (96%) rename helm/software/matita/contribs/LOGIC/{datatypes => datatypes_defs}/Sequent.ma (87%) create mode 100644 helm/software/matita/contribs/LOGIC/datatypes_props/Sequent.ma diff --git a/helm/software/matita/contribs/LOGIC/Track/pred.ma b/helm/software/matita/contribs/LOGIC/Track/pred.ma index c4e65c05d..d190f17fd 100644 --- a/helm/software/matita/contribs/LOGIC/Track/pred.ma +++ b/helm/software/matita/contribs/LOGIC/Track/pred.ma @@ -33,7 +33,10 @@ theorem track_pred: \forall Q1,Q2,p1,p2,S1,S2. [Q1, p1, S1] => [Q2, p2, S2] \to | lapply linear track_inv_scut to H4; decompose; destruct; lapply linear track_inv_lref to H5; decompose; autobatch | lapply linear track_inv_scut to H3; decompose; destruct; - lapply linear track_inv_prin to H5; destruct; autobatch + lapply linear track_inv_prin to H5; destruct; + lapply linear rinj_inj to Hcut1; + rewrite < Hcut1 in H4; clear Hcut1 a2; + autobatch | lapply linear track_inv_scut to H3; decompose; destruct; lapply linear track_inv_prin to H4; destruct; autobatch | lapply linear track_inv_scut to H3; decompose; destruct; diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Context.ma b/helm/software/matita/contribs/LOGIC/datatypes_defs/Context.ma similarity index 86% rename from helm/software/matita/contribs/LOGIC/datatypes/Context.ma rename to helm/software/matita/contribs/LOGIC/datatypes_defs/Context.ma index 44d626648..e5dba4aaf 100644 --- a/helm/software/matita/contribs/LOGIC/datatypes/Context.ma +++ b/helm/software/matita/contribs/LOGIC/datatypes_defs/Context.ma @@ -12,15 +12,15 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LOGIC/datatypes/Context". +set "baseuri" "cic:/matita/LOGIC/datatypes_defs/Context". (* FLAT CONTEXTS - Naming policy: - contexts: P Q *) -include "datatypes/Proof.ma". -include "datatypes/Sequent.ma". +include "datatypes_defs/Proof.ma". +include "datatypes_defs/Sequent.ma". inductive Context: Type \def | leaf: Context @@ -29,5 +29,5 @@ inductive Context: Type \def (* definition inj: Sequent \to Context \def abst leaf. -coercion cic:/matita/LOGIC/datatypes/Context/inj.con. +coercion cic:/matita/LOGIC/datatypes_defs/Context/inj.con. *) diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Formula.ma b/helm/software/matita/contribs/LOGIC/datatypes_defs/Formula.ma similarity index 95% rename from helm/software/matita/contribs/LOGIC/datatypes/Formula.ma rename to helm/software/matita/contribs/LOGIC/datatypes_defs/Formula.ma index 64025957e..ec6441dd1 100644 --- a/helm/software/matita/contribs/LOGIC/datatypes/Formula.ma +++ b/helm/software/matita/contribs/LOGIC/datatypes_defs/Formula.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LOGIC/datatypes/Formula". +set "baseuri" "cic:/matita/LOGIC/datatypes_defs/Formula". (* FORMULAE - Naming policy: diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma b/helm/software/matita/contribs/LOGIC/datatypes_defs/Proof.ma similarity index 96% rename from helm/software/matita/contribs/LOGIC/datatypes/Proof.ma rename to helm/software/matita/contribs/LOGIC/datatypes_defs/Proof.ma index f6260b026..fa2c29ffa 100644 --- a/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma +++ b/helm/software/matita/contribs/LOGIC/datatypes_defs/Proof.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LOGIC/datatypes/Proof". +set "baseuri" "cic:/matita/LOGIC/datatypes_defs/Proof". (* PROOFS - Naming policy: diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Sequent.ma b/helm/software/matita/contribs/LOGIC/datatypes_defs/Sequent.ma similarity index 87% rename from helm/software/matita/contribs/LOGIC/datatypes/Sequent.ma rename to helm/software/matita/contribs/LOGIC/datatypes_defs/Sequent.ma index d78ac503a..09d826991 100644 --- a/helm/software/matita/contribs/LOGIC/datatypes/Sequent.ma +++ b/helm/software/matita/contribs/LOGIC/datatypes_defs/Sequent.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LOGIC/datatypes/Sequent". +set "baseuri" "cic:/matita/LOGIC/datatypes_defs/Sequent". (* SEQUENTS - Naming policy: @@ -21,7 +21,7 @@ set "baseuri" "cic:/matita/LOGIC/datatypes/Sequent". - sequents : R S *) -include "datatypes/Formula.ma". +include "datatypes_defs/Formula.ma". inductive LHS: Type \def | lleaf: LHS @@ -41,6 +41,6 @@ definition linj: Formula \to LHS \def labst lleaf. definition rinj: Formula \to RHS \def \lambda b. rabst b rleaf. -coercion cic:/matita/LOGIC/datatypes/Sequent/linj.con. +coercion cic:/matita/LOGIC/datatypes_defs/Sequent/linj.con. -coercion cic:/matita/LOGIC/datatypes/Sequent/rinj.con. +coercion cic:/matita/LOGIC/datatypes_defs/Sequent/rinj.con. diff --git a/helm/software/matita/contribs/LOGIC/datatypes_props/Sequent.ma b/helm/software/matita/contribs/LOGIC/datatypes_props/Sequent.ma new file mode 100644 index 000000000..1b0ea6cf8 --- /dev/null +++ b/helm/software/matita/contribs/LOGIC/datatypes_props/Sequent.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/LOGIC/datatypes_props/Sequent". + +include "datatypes_defs/Sequent.ma". + +theorem rinj_inj: \forall b,d. rinj b = rinj d \to b = d. -- 2.39.2