From: Ferruccio Guidi Date: Tue, 7 Jun 2011 21:37:47 +0000 (+0000) Subject: - we removed the reduction-related item categorization X-Git-Tag: make_still_working~2452 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ec897a47d5c194a068ee76f9251958950371876b;p=helm.git - we removed the reduction-related item categorization - some renaming --- diff --git a/matita/matita/lib/lambda-delta/language/item.ma b/matita/matita/lib/lambda-delta/language/item.ma deleted file mode 100644 index 60a115dc0..000000000 --- a/matita/matita/lib/lambda-delta/language/item.ma +++ /dev/null @@ -1,59 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) - -(* THE FORMAL SYSTEM λδ - MATITA SOURCE SCRIPTS - * Specification started: 2011 April 17 - * - Patience on me so that I gain peace and perfection! - - * [ suggested invocation to start formal specifications with ] - *) - -include "lambda-delta/ground.ma". - -(* BINARY ITEMS *************************************************************) - -(* binary binding items *) -inductive bind2: Type[0] ≝ -| Abbr: bind2 (* abbreviation *) -| Abst: bind2 (* abstraction *) -. - -(* binary non-binding items *) -inductive flat2: Type[0] ≝ -| Appl: flat2 (* application *) -| Cast: flat2 (* explicit type annotation *) -. - -(* binary items *) -inductive item2: Type[0] ≝ -| Bind: bind2 → item2 (* binding item *) -| Flat: flat2 → item2 (* non-binding item *) -. - -coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2. - -coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2. - -(* reduction-related categorization *****************************************) - -(* binding items entitled for zeta-reduction *) -definition zable ≝ λI. I = Abbr. - -interpretation "is entitled for zeta-reduction" 'Zeta I = (zable I). - -(* non-binding items entitled for zeta-reduction *) -definition table ≝ λI. I = Cast. - -interpretation "is entitled for tau-reduction" 'Tau I = (table I). - -(* binding items entitled for theta-reduction *) -definition thable ≝ λI. I = Abbr. - -interpretation "is entitled for theta-reduction" 'Theta I = (thable I). diff --git a/matita/matita/lib/lambda-delta/language/lenv.ma b/matita/matita/lib/lambda-delta/language/lenv.ma deleted file mode 100644 index 3398de4ee..000000000 --- a/matita/matita/lib/lambda-delta/language/lenv.ma +++ /dev/null @@ -1,24 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) - -include "lambda-delta/language/term.ma". - -(* LOCAL ENVIRONMENTS *******************************************************) - -(* local environments *) -inductive lenv: Type[0] ≝ -| LSort: lenv (* empty *) -| LPair: lenv → bind2 → term → lenv (* binary binding construction *) -. - -interpretation "sort (local environment)" 'Star = LSort. - -interpretation "environment binding construction (binary)" 'DBind L I T = (LPair L I T). diff --git a/matita/matita/lib/lambda-delta/language/sh.ma b/matita/matita/lib/lambda-delta/language/sh.ma deleted file mode 100644 index 32840edff..000000000 --- a/matita/matita/lib/lambda-delta/language/sh.ma +++ /dev/null @@ -1,20 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) - -include "lambda-delta/ground.ma". - -(* SORT HIERARCHY ***********************************************************) - -(* sort hierarchy specifications *) -record sh: Type[0] ≝ { - next: nat → nat; (* next sort in the hierarchy *) - next_lt: ∀k. k < next k (* strict monotonicity condition *) -}. diff --git a/matita/matita/lib/lambda-delta/language/term.ma b/matita/matita/lib/lambda-delta/language/term.ma deleted file mode 100644 index ac3b8fa5e..000000000 --- a/matita/matita/lib/lambda-delta/language/term.ma +++ /dev/null @@ -1,31 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) - -include "lambda-delta/language/item.ma". - -(* TERMS ********************************************************************) - -(* terms *) -inductive term: Type[0] ≝ -| TSort: nat → term (* sort: starting at 0 *) -| TLRef: nat → term (* reference by index: starting at 0 *) -| TPair: item2 → term → term → term (* binary item construction *) -. - -interpretation "sort (term)" 'Star k = (TSort k). - -interpretation "local reference (term)" 'Weight i = (TLRef i). - -interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2). - -interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2). - -interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2). diff --git a/matita/matita/lib/lambda-delta/language/weight.ma b/matita/matita/lib/lambda-delta/language/weight.ma deleted file mode 100644 index f0021be9e..000000000 --- a/matita/matita/lib/lambda-delta/language/weight.ma +++ /dev/null @@ -1,40 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) - -include "lambda-delta/language/lenv.ma". - -(* WEIGHTS ******************************************************************) - -(* the weight of a term *) -let rec tw T ≝ match T with -[ TSort _ ⇒ 1 -| TLRef _ ⇒ 1 -| TPair _ V T ⇒ tw V + tw T + 1 -]. - -interpretation "weight (term)" 'Weight T = (tw T). - -(* the weight of a local environment *) -let rec lw L ≝ match L with -[ LSort ⇒ 0 -| LPair L _ V ⇒ lw L + #V -]. - -interpretation "weight (local environment)" 'Weight L = (lw L). - -(* the weight of a closure *) -definition cw: lenv → term → ? ≝ λL,T. #L + #T. - -interpretation "weight (closure)" 'Weight L T = (cw L T). - -axiom cw_wf_ind: ∀P:lenv→term→Prop. - (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) → - ∀L,T. P L T. diff --git a/matita/matita/lib/lambda-delta/notation.ma b/matita/matita/lib/lambda-delta/notation.ma index 7f5fabf28..09960abe3 100644 --- a/matita/matita/lib/lambda-delta/notation.ma +++ b/matita/matita/lib/lambda-delta/notation.ma @@ -13,18 +13,6 @@ (* language *****************************************************************) -notation "hvbox( ζ I )" - non associative with precedence 45 - for @{ 'Zeta $I }. - -notation "hvbox( τ I )" - non associative with precedence 45 - for @{ 'Tau $I }. - -notation "hvbox( θ I )" - non associative with precedence 45 - for @{ 'Theta $I }. - notation "hvbox( ⋆ )" non associative with precedence 90 for @{ 'Star }. diff --git a/matita/matita/lib/lambda-delta/substitution/lift.ma b/matita/matita/lib/lambda-delta/substitution/lift.ma index 656946171..6b97f502c 100644 --- a/matita/matita/lib/lambda-delta/substitution/lift.ma +++ b/matita/matita/lib/lambda-delta/substitution/lift.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/language/term.ma". +include "lambda-delta/syntax/term.ma". (* RELOCATION ***************************************************************) diff --git a/matita/matita/lib/lambda-delta/substitution/subst.ma b/matita/matita/lib/lambda-delta/substitution/subst.ma index 5989693c5..a9732529d 100644 --- a/matita/matita/lib/lambda-delta/substitution/subst.ma +++ b/matita/matita/lib/lambda-delta/substitution/subst.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/language/lenv.ma". +include "lambda-delta/syntax/lenv.ma". include "lambda-delta/substitution/lift.ma". (* TELESCOPIC SUBSTITUTION **************************************************) diff --git a/matita/matita/lib/lambda-delta/syntax/item.ma b/matita/matita/lib/lambda-delta/syntax/item.ma new file mode 100644 index 000000000..742ff2272 --- /dev/null +++ b/matita/matita/lib/lambda-delta/syntax/item.ma @@ -0,0 +1,42 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +(* THE FORMAL SYSTEM λδ - MATITA SOURCE SCRIPTS + * Specification started: 2011 April 17 + * - Patience on me so that I gain peace and perfection! - + * [ suggested invocation to start formal specifications with ] + *) + +include "lambda-delta/ground.ma". + +(* BINARY ITEMS *************************************************************) + +(* binary binding items *) +inductive bind2: Type[0] ≝ +| Abbr: bind2 (* abbreviation *) +| Abst: bind2 (* abstraction *) +. + +(* binary non-binding items *) +inductive flat2: Type[0] ≝ +| Appl: flat2 (* application *) +| Cast: flat2 (* explicit type annotation *) +. + +(* binary items *) +inductive item2: Type[0] ≝ +| Bind: bind2 → item2 (* binding item *) +| Flat: flat2 → item2 (* non-binding item *) +. + +coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2. + +coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2. diff --git a/matita/matita/lib/lambda-delta/syntax/lenv.ma b/matita/matita/lib/lambda-delta/syntax/lenv.ma new file mode 100644 index 000000000..c3aab910b --- /dev/null +++ b/matita/matita/lib/lambda-delta/syntax/lenv.ma @@ -0,0 +1,24 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda-delta/syntax/term.ma". + +(* LOCAL ENVIRONMENTS *******************************************************) + +(* local environments *) +inductive lenv: Type[0] ≝ +| LSort: lenv (* empty *) +| LPair: lenv → bind2 → term → lenv (* binary binding construction *) +. + +interpretation "sort (local environment)" 'Star = LSort. + +interpretation "environment binding construction (binary)" 'DBind L I T = (LPair L I T). diff --git a/matita/matita/lib/lambda-delta/syntax/sh.ma b/matita/matita/lib/lambda-delta/syntax/sh.ma new file mode 100644 index 000000000..32840edff --- /dev/null +++ b/matita/matita/lib/lambda-delta/syntax/sh.ma @@ -0,0 +1,20 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda-delta/ground.ma". + +(* SORT HIERARCHY ***********************************************************) + +(* sort hierarchy specifications *) +record sh: Type[0] ≝ { + next: nat → nat; (* next sort in the hierarchy *) + next_lt: ∀k. k < next k (* strict monotonicity condition *) +}. diff --git a/matita/matita/lib/lambda-delta/syntax/term.ma b/matita/matita/lib/lambda-delta/syntax/term.ma new file mode 100644 index 000000000..fe84e54b4 --- /dev/null +++ b/matita/matita/lib/lambda-delta/syntax/term.ma @@ -0,0 +1,31 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda-delta/syntax/item.ma". + +(* TERMS ********************************************************************) + +(* terms *) +inductive term: Type[0] ≝ +| TSort: nat → term (* sort: starting at 0 *) +| TLRef: nat → term (* reference by index: starting at 0 *) +| TPair: item2 → term → term → term (* binary item construction *) +. + +interpretation "sort (term)" 'Star k = (TSort k). + +interpretation "local reference (term)" 'Weight i = (TLRef i). + +interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2). + +interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2). + +interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2). diff --git a/matita/matita/lib/lambda-delta/syntax/weight.ma b/matita/matita/lib/lambda-delta/syntax/weight.ma new file mode 100644 index 000000000..8d5ed6835 --- /dev/null +++ b/matita/matita/lib/lambda-delta/syntax/weight.ma @@ -0,0 +1,40 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda-delta/syntax/lenv.ma". + +(* WEIGHTS ******************************************************************) + +(* the weight of a term *) +let rec tw T ≝ match T with +[ TSort _ ⇒ 1 +| TLRef _ ⇒ 1 +| TPair _ V T ⇒ tw V + tw T + 1 +]. + +interpretation "weight (term)" 'Weight T = (tw T). + +(* the weight of a local environment *) +let rec lw L ≝ match L with +[ LSort ⇒ 0 +| LPair L _ V ⇒ lw L + #V +]. + +interpretation "weight (local environment)" 'Weight L = (lw L). + +(* the weight of a closure *) +definition cw: lenv → term → ? ≝ λL,T. #L + #T. + +interpretation "weight (closure)" 'Weight L T = (cw L T). + +axiom cw_wf_ind: ∀P:lenv→term→Prop. + (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) → + ∀L,T. P L T.