From: Ferruccio Guidi Date: Mon, 12 Nov 2007 12:35:56 +0000 (+0000) Subject: refactoring X-Git-Tag: 0.4.95@7852~25 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f14e9248d0f76d1f366325b5ef74c1c03f485c2f;p=helm.git refactoring --- diff --git a/matita/contribs/LOGIC/Track/pred.ma b/matita/contribs/LOGIC/Track/pred.ma index c4e65c05d..d190f17fd 100644 --- a/matita/contribs/LOGIC/Track/pred.ma +++ b/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/matita/contribs/LOGIC/datatypes/Context.ma b/matita/contribs/LOGIC/datatypes/Context.ma deleted file mode 100644 index 44d626648..000000000 --- a/matita/contribs/LOGIC/datatypes/Context.ma +++ /dev/null @@ -1,33 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/Context". - -(* FLAT CONTEXTS - - Naming policy: - - contexts: P Q -*) - -include "datatypes/Proof.ma". -include "datatypes/Sequent.ma". - -inductive Context: Type \def - | leaf: Context - | abst: Context \to Proof \to Proof \to Sequent \to Context -. -(* -definition inj: Sequent \to Context \def abst leaf. - -coercion cic:/matita/LOGIC/datatypes/Context/inj.con. -*) diff --git a/matita/contribs/LOGIC/datatypes/Formula.ma b/matita/contribs/LOGIC/datatypes/Formula.ma deleted file mode 100644 index 64025957e..000000000 --- a/matita/contribs/LOGIC/datatypes/Formula.ma +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/Formula". - -(* FORMULAE - - Naming policy: - - formulae: a b c d -*) - -include "preamble.ma". - -inductive Formula: Type \def - | posr: Nat \to Formula - | impl: Formula \to Formula \to Formula -. diff --git a/matita/contribs/LOGIC/datatypes/Proof.ma b/matita/contribs/LOGIC/datatypes/Proof.ma deleted file mode 100644 index f6260b026..000000000 --- a/matita/contribs/LOGIC/datatypes/Proof.ma +++ /dev/null @@ -1,31 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/Proof". - -(* PROOFS - - Naming policy: - - proofs: p q r s -*) - -include "preamble.ma". - -inductive Proof: Type \def - | lref: Nat \to Proof (* projection *) - | prin: Nat \to Proof (* pos rel inhabitant *) - | impw: Proof \to Proof (* weakening *) - | impr: Proof \to Proof (* right introduction *) - | impi: Proof \to Proof \to Proof \to Proof (* left introduction *) - | scut: Proof \to Proof \to Proof (* symmetric cut *) -. diff --git a/matita/contribs/LOGIC/datatypes/Sequent.ma b/matita/contribs/LOGIC/datatypes/Sequent.ma deleted file mode 100644 index d78ac503a..000000000 --- a/matita/contribs/LOGIC/datatypes/Sequent.ma +++ /dev/null @@ -1,46 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/Sequent". - -(* SEQUENTS - - Naming policy: - - left hand sides (lhs): A C - - right hand sides (rhs): B D - - sequents : R S -*) - -include "datatypes/Formula.ma". - -inductive LHS: Type \def - | lleaf: LHS - | labst: LHS \to Formula \to LHS -. - -inductive RHS: Type \def - | rleaf: RHS - | rabst: Formula \to RHS \to RHS -. - -inductive Sequent: Type \def - | pair: LHS \to RHS \to Sequent -. - -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/Sequent/rinj.con. diff --git a/matita/contribs/LOGIC/datatypes_defs/Context.ma b/matita/contribs/LOGIC/datatypes_defs/Context.ma new file mode 100644 index 000000000..e5dba4aaf --- /dev/null +++ b/matita/contribs/LOGIC/datatypes_defs/Context.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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_defs/Context". + +(* FLAT CONTEXTS + - Naming policy: + - contexts: P Q +*) + +include "datatypes_defs/Proof.ma". +include "datatypes_defs/Sequent.ma". + +inductive Context: Type \def + | leaf: Context + | abst: Context \to Proof \to Proof \to Sequent \to Context +. +(* +definition inj: Sequent \to Context \def abst leaf. + +coercion cic:/matita/LOGIC/datatypes_defs/Context/inj.con. +*) diff --git a/matita/contribs/LOGIC/datatypes_defs/Formula.ma b/matita/contribs/LOGIC/datatypes_defs/Formula.ma new file mode 100644 index 000000000..ec6441dd1 --- /dev/null +++ b/matita/contribs/LOGIC/datatypes_defs/Formula.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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_defs/Formula". + +(* FORMULAE + - Naming policy: + - formulae: a b c d +*) + +include "preamble.ma". + +inductive Formula: Type \def + | posr: Nat \to Formula + | impl: Formula \to Formula \to Formula +. diff --git a/matita/contribs/LOGIC/datatypes_defs/Proof.ma b/matita/contribs/LOGIC/datatypes_defs/Proof.ma new file mode 100644 index 000000000..fa2c29ffa --- /dev/null +++ b/matita/contribs/LOGIC/datatypes_defs/Proof.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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_defs/Proof". + +(* PROOFS + - Naming policy: + - proofs: p q r s +*) + +include "preamble.ma". + +inductive Proof: Type \def + | lref: Nat \to Proof (* projection *) + | prin: Nat \to Proof (* pos rel inhabitant *) + | impw: Proof \to Proof (* weakening *) + | impr: Proof \to Proof (* right introduction *) + | impi: Proof \to Proof \to Proof \to Proof (* left introduction *) + | scut: Proof \to Proof \to Proof (* symmetric cut *) +. diff --git a/matita/contribs/LOGIC/datatypes_defs/Sequent.ma b/matita/contribs/LOGIC/datatypes_defs/Sequent.ma new file mode 100644 index 000000000..09d826991 --- /dev/null +++ b/matita/contribs/LOGIC/datatypes_defs/Sequent.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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_defs/Sequent". + +(* SEQUENTS + - Naming policy: + - left hand sides (lhs): A C + - right hand sides (rhs): B D + - sequents : R S +*) + +include "datatypes_defs/Formula.ma". + +inductive LHS: Type \def + | lleaf: LHS + | labst: LHS \to Formula \to LHS +. + +inductive RHS: Type \def + | rleaf: RHS + | rabst: Formula \to RHS \to RHS +. + +inductive Sequent: Type \def + | pair: LHS \to RHS \to Sequent +. + +definition linj: Formula \to LHS \def labst lleaf. + +definition rinj: Formula \to RHS \def \lambda b. rabst b rleaf. + +coercion cic:/matita/LOGIC/datatypes_defs/Sequent/linj.con. + +coercion cic:/matita/LOGIC/datatypes_defs/Sequent/rinj.con. diff --git a/matita/contribs/LOGIC/datatypes_props/Sequent.ma b/matita/contribs/LOGIC/datatypes_props/Sequent.ma new file mode 100644 index 000000000..1b0ea6cf8 --- /dev/null +++ b/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.