limits: we set up a different foundation

lambdadelta: Makefile updated for new version of probe

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 064c24db90690fd984793c9c88a7b922f0963174..f3d8b3232ad8e33d4e84f8c98851de01ee8d8a01 100644 (file)
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -25,7 +25,7 @@ MAC_OPTS     :=
 
 PRB_DIR      := ../../../components/binaries/probe
 PRB          := probe.native
-PRB_OPTS     := $(XOA_OPTS) -g 
+PRB_OPTS     := $(XOA_OPTS) -g -i
 
 ORIG         := . ./orig.sh 
 ORIGS        := basic_2/basic_1.orig
@@ -52,7 +52,7 @@ define MAS_TEMPLATE
 
 $(1)/$(1)_probe.txt: $$(MAS_$(1))
        @echo "  PROBE $(1)"
-       $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -on -i > $$@
+       $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -on -c > $$@
 
 $(1)/$(1)_mac.txt: $$(MAS_$(1))
        @echo "  MAC $(1)"

diff --git a/matita/matita/contribs/limits/Makefile b/matita/matita/contribs/limits/Makefile
new file mode 100644 (file)
index 0000000..c5a88d1
--- /dev/null
+++ b/matita/matita/contribs/limits/Makefile
@@ -0,0 +1,30 @@
+H    := @
+
+ALPHA_DIR ?= $(HOME)/mps/ocamlbuild/alpha
+ALPHA      = alpha.native
+
+MATITAC = ../../matitac.opt
+
+PRB_DIR      := ../../../components/binaries/probe
+PRB          := probe.native
+PRB_OPTS     := ../../matita.conf.xml -g -i
+
+AMAS = $(wildcard *.ama)
+
+all: $(AMAS:%.ama=%.ma)
+       @$(MATITAC)
+
+clean:
+       $(H)$(RM) *~
+
+clean_all: clean
+       $(H)$(RM) $(AMAS:%.ama=%.ma)
+
+probe:
+       @echo PROBE .
+       $(H)$(PRB_DIR)/$(PRB) $(PRB_OPTS) .
+
+.PHONY: all clean clean_all probe
+
+%.ma: %.ama
+       $(H)$(ALPHA_DIR)/$(ALPHA) < $< > $@ 

diff --git a/matita/matita/contribs/limits/u0_class.ma b/matita/matita/contribs/limits/u0_class.ma
new file mode 100644 (file)
index 0000000..49c715a
--- /dev/null
+++ b/matita/matita/contribs/limits/u0_class.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "u0_predicates.ma".
+
+(* CLASSES ************************************************************)
+
+record u0_class: Type[1] ≝ {
+   u0_class_t :> Type[0];
+   u0_class_in:  u0_predicate1 u0_class_t;
+   u0_class_eq:  u0_predicate2 u0_class_t
+}.
+
+interpretation "u0 class membership" 'mem a C = (u0_class_in C a).
+
+definition u0_class_all: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∀a. a ∈ C → P a.
+
+definition u0_class_ex: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∃a. a ∈ C ∧ P a.
+
+record is_u0_class (C:u0_class): Prop ≝ {
+   u0_class_repl1: can_u0_replace1 C (u0_class_all C) (u0_class_eq C) (u0_class_in C);
+   u0_class_refl : is_u0_reflexive C (u0_class_all C) (u0_class_eq C)
+}.

diff --git a/matita/matita/contribs/limits/u0_predicates.ma b/matita/matita/contribs/limits/u0_predicates.ma
new file mode 100644 (file)
index 0000000..13650cf
--- /dev/null
+++ b/matita/matita/contribs/limits/u0_predicates.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "preamble.ma".
+
+(* RELATIONS **********************************************************)
+
+definition u0_predicate1: Type[0] → Type[1] ≝ λT.T → Prop.
+
+definition u0_predicate2: Type[0] → Type[1] ≝ λT.T → u0_predicate1 T.
+
+definition u1_predicate1: Type[1] → Type[2] ≝ λT.T → Prop.
+
+definition u0_quantifier: Type[0] → Type[2] ≝ λT. u1_predicate1 (u0_predicate1 T).
+
+record is_u0_reflexive (T:Type[0]) (All:u0_quantifier T) (R:u0_predicate2 T): Prop ≝
+{
+   u0_refl: All (λa. R a a)
+}.
+
+record can_u0_replace1 (T:Type[0]) (All:u0_quantifier T) (Q:u0_predicate2 T) (R:u0_predicate1 T): Prop ≝
+{
+   u0_repl1: All (λa. R a → All (λb. Q b a → R b))
+}.
+(*
+record can_u0_replac2 (T:Type[0]) (All:u0_quantifier T) (Q:u0_predicate2 T) (R:u0_predicate2 T): Prop ≝
+{
+   u0_reflexivity: All (λa. R a a)
+}.
+*)