From 2ff23d9306837c14c9d1a3b935a66bc71ffe87c3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 5 Sep 2005 10:15:21 +0000 Subject: [PATCH] LAMBDA-TYPES moved under contribs --- .../contribs/LAMBDA-TYPES/lref_map_defs.ma | 22 ++++++++ .../contribs/LAMBDA-TYPES/terms_defs.ma | 38 ++++++++++++++ helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma | 51 +++++++++++++++++++ 3 files changed, 111 insertions(+) create mode 100644 helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma create mode 100644 helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma create mode 100644 helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma diff --git a/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma new file mode 100644 index 000000000..f2994f9b7 --- /dev/null +++ b/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/LAMBDA-TYPES/lref_map_defs". + +include "terms_defs.ma". + +inductive tlref_map (A: Set) (N: Set) (map: nat \to nat): nat \to (T A N) \to (T A N) \to Prop \def + | tlref_map_sort: \forall i. \forall k. \forall y. (tlref_map A N map i (TSort A N y k) (TSort A N y k)) + | tlref_map_lref_lt: \forall j. \forall i. \forall y. (lt j i) \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y j)) + | tlref_map_lref_ge: \forall j. \forall i. \forall y. (le i j) \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y (map j))). \ No newline at end of file diff --git a/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma new file mode 100644 index 000000000..3f93fc13d --- /dev/null +++ b/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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/LAMBDA-TYPES/terms_defs". + +inductive B : Set \def + | Void: B + | Abbr: B + | Abst: B. + +inductive F : Set \def + | Appl: F + | Cast: F. + +inductive W : Set \def + | Bind: B \to W + | Flat: F \to W. + +inductive T (A:Set) (N:Set) : Set \def + | TSort: A \to nat \to (T A N) + | TLRef: A \to nat \to (T A N) + | TWag : A \to W \to (T A N) \to (T A N) \to (T A N) + | TGRef: A \to N \to (T A N). + +record X (A:Set) (N:Set) : Type \def { + get_gref: N \to B \to (T A N) \to Prop +}. diff --git a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma new file mode 100644 index 000000000..f2bf3660d --- /dev/null +++ b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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/LAMBDA-TYPES/tlt_defs". + +include "terms_defs.ma". + +definition wadd: (nat \to nat) \to nat \to (nat \to nat) \def + \lambda map,w,n. + match n with [ + O \Rightarrow w + | (S m) \Rightarrow (map m) + ]. + +let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T) : nat \def + match t with [ + (TSort A N y k) \Rightarrow O + | (TLRef A N y i) \Rightarrow (map i) + | (TWag A N y z w u) \Rightarrow + match z with [ + (Bind b) \Rightarrow + match b with [ + Abbr \Rightarrow + (S (plus (weight_map A N map w) (weight_map A N (wadd map (S (weight_map A N map w))) u))) + | Abst \Rightarrow + (S (plus (weight_map A N map w) (weight_map A N (wadd map O) u))) + | Void \Rightarrow + (S (plus (weight_map A N map w) (weight_map A N (wadd map O) u))) + ] + | (Flat a) \Rightarrow + (S (plus (weight_map A N map w) (weight_map A N map u))) + ]].(* + | (TGRef A N y n) \Rightarrow O + ].*) +(* + Definition weight : T \to nat := (weight_map [_](0)). + + Definition tlt : T \to T \to Prop := [t1,t2](lt (weight t1) (weight t2)). + +*) -- 2.39.2