]> matita.cs.unibo.it Git - helm.git/commitdiff
- we removed the reduction-related item categorization
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 7 Jun 2011 21:37:47 +0000 (21:37 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 7 Jun 2011 21:37:47 +0000 (21:37 +0000)
- some renaming

13 files changed:
matita/matita/lib/lambda-delta/language/item.ma [deleted file]
matita/matita/lib/lambda-delta/language/lenv.ma [deleted file]
matita/matita/lib/lambda-delta/language/sh.ma [deleted file]
matita/matita/lib/lambda-delta/language/term.ma [deleted file]
matita/matita/lib/lambda-delta/language/weight.ma [deleted file]
matita/matita/lib/lambda-delta/notation.ma
matita/matita/lib/lambda-delta/substitution/lift.ma
matita/matita/lib/lambda-delta/substitution/subst.ma
matita/matita/lib/lambda-delta/syntax/item.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/syntax/lenv.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/syntax/sh.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/syntax/term.ma [new file with mode: 0644]
matita/matita/lib/lambda-delta/syntax/weight.ma [new file with mode: 0644]

diff --git a/matita/matita/lib/lambda-delta/language/item.ma b/matita/matita/lib/lambda-delta/language/item.ma
deleted file mode 100644 (file)
index 60a115d..0000000
+++ /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 (file)
index 3398de4..0000000
+++ /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 (file)
index 32840ed..0000000
+++ /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 (file)
index ac3b8fa..0000000
+++ /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 (file)
index f0021be..0000000
+++ /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.
index 7f5fabf28821582db43d4a35fc376bcd553d46a8..09960abe3facdd73b4759958cf037e5e57af533d 100644 (file)
 
 (* 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 }.
index 6569461718d2e46e81c9f40cd1d34e260203ba5f..6b97f502cea4b1653286f82812009699ad2ffc64 100644 (file)
@@ -9,7 +9,7 @@
      \ /
       V_______________________________________________________________ *)
 
-include "lambda-delta/language/term.ma".
+include "lambda-delta/syntax/term.ma".
 
 (* RELOCATION ***************************************************************)
 
index 5989693c5059a987e6e77a8a0c0b0fee9d4c8d71..a9732529ddcc0bb4f1f34ceef5fffc508303f5b6 100644 (file)
@@ -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 (file)
index 0000000..742ff22
--- /dev/null
@@ -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 (file)
index 0000000..c3aab91
--- /dev/null
@@ -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 (file)
index 0000000..32840ed
--- /dev/null
@@ -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 (file)
index 0000000..fe84e54
--- /dev/null
@@ -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 (file)
index 0000000..8d5ed68
--- /dev/null
@@ -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.