From 2e1bf37296c12dd256cb346a31559aa9bdb8acd9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 18 Aug 2011 22:09:54 +0000 Subject: [PATCH] refactoring completed --- .../lambda-delta/Basic-2/syntax/item.ma | 43 ------------------ .../lambda-delta/Basic-2/syntax/length.ma | 22 ---------- .../lambda-delta/Basic-2/syntax/lenv.ma | 24 ---------- .../lambda-delta/Basic-2/syntax/sh.ma | 20 --------- .../lambda-delta/Basic-2/syntax/term.ma | 31 ------------- .../lambda-delta/Basic-2/syntax/weight.ma | 44 ------------------- 6 files changed, 184 deletions(-) delete mode 100644 matita/matita/contribs/lambda-delta/Basic-2/syntax/item.ma delete mode 100644 matita/matita/contribs/lambda-delta/Basic-2/syntax/length.ma delete mode 100644 matita/matita/contribs/lambda-delta/Basic-2/syntax/lenv.ma delete mode 100644 matita/matita/contribs/lambda-delta/Basic-2/syntax/sh.ma delete mode 100644 matita/matita/contribs/lambda-delta/Basic-2/syntax/term.ma delete mode 100644 matita/matita/contribs/lambda-delta/Basic-2/syntax/weight.ma diff --git a/matita/matita/contribs/lambda-delta/Basic-2/syntax/item.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/item.ma deleted file mode 100644 index c3613eb0c..000000000 --- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/item.ma +++ /dev/null @@ -1,43 +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 "Ground-2/ground.ma". -include "Basic-2/notation.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/contribs/lambda-delta/Basic-2/syntax/length.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/length.ma deleted file mode 100644 index dfe1261cd..000000000 --- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/length.ma +++ /dev/null @@ -1,22 +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 "Basic-2/syntax/lenv.ma". - -(* LENGTH *******************************************************************) - -(* the length of a local environment *) -let rec length L ≝ match L with -[ LSort ⇒ 0 -| LPair L _ _ ⇒ length L + 1 -]. - -interpretation "length (local environment)" 'card L = (length L). diff --git a/matita/matita/contribs/lambda-delta/Basic-2/syntax/lenv.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/lenv.ma deleted file mode 100644 index f8fc80668..000000000 --- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/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 "Basic-2/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/contribs/lambda-delta/Basic-2/syntax/sh.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/sh.ma deleted file mode 100644 index 99d1848fb..000000000 --- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/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 "Ground-2/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/contribs/lambda-delta/Basic-2/syntax/term.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/term.ma deleted file mode 100644 index b1c18e6e7..000000000 --- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/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 "Basic-2/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/contribs/lambda-delta/Basic-2/syntax/weight.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/weight.ma deleted file mode 100644 index 82bd97aa0..000000000 --- a/matita/matita/contribs/lambda-delta/Basic-2/syntax/weight.ma +++ /dev/null @@ -1,44 +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 "Basic-2/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 tw_wf_ind: ∀P:term→Prop. - (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) → - ∀T. P 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. -- 2.39.2