--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/Base.ML Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/Base.thy Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,62 @@
+(* Title: Cube/Base.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1993 University of Cambridge
+
+Barendregt's Lambda-Cube.
+*)
+
+Base = Pure +
+
+types
+ term context typing
+
+arities
+ term :: logic
+
+consts
+ Abs, Prod :: "[term, term => term] => term"
+ Trueprop :: "[context, typing] => prop" ("(_/ |- _)")
+ MT_context :: "context" ("")
+ Context :: "[typing, context] => context" ("_ _")
+ star :: "term" ("*")
+ box :: "term" ("[]")
+ "^" :: "[term, term] => term" (infixl 20)
+ Has_type :: "[term, term] => typing" ("(_:/ _)" [0, 0] 5)
+
+syntax
+ Trueprop1 :: "typing => prop" ("(_)")
+ "" :: "id => context" ("_ ")
+ "" :: "var => context" ("_ ")
+ Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
+ Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
+ "->" :: "[term, term] => term" (infixr 10)
+
+translations
+ (prop) "x:X" == (prop) "|- x:X"
+ "Lam x:A. B" == "Abs(A, %x. B)"
+ "Pi x:A. B" => "Prod(A, %x. B)"
+ "A -> B" => "Prod(A, _K(B))"
+
+rules
+ s_b "*: []"
+
+ strip_s "[| A:*; a:A ==> G |- x:X |] ==> a:A G |- x:X"
+ strip_b "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"
+
+ app "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"
+
+ pi_ss "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
+
+ lam_ss "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
+ ==> Abs(A, f) : Prod(A, B)"
+
+ beta "Abs(A, f)^a == f(a)"
+
+end
+
+
+ML
+
+val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/CC.ML Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+val CC = simple @ [lam_bs,pi_bs,lam_bb,pi_bb,lam_sb,pi_sb];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/CC.thy Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,3 @@
+
+CC = L2 + LP + Lomega
+
--- a/src/Cube/Cube.ML Mon Jan 19 16:26:11 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: Cube/Cube.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1990 University of Cambridge
-
-For Cube.thy. The systems of the Lambda-cube that extend simple types
-*)
-
-open Cube;
-
-val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];
-
-val L2_thy =
- Cube.thy
- |> PureThy.add_store_axioms
- [("pi_bs", "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
- ("lam_bs", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
- \ ==> Abs(A,f) : Prod(A,B)")]
- |> Theory.add_name "L2";
-
-val lam_bs = get_axiom L2_thy "lam_bs";
-val pi_bs = get_axiom L2_thy "pi_bs";
-
-val L2 = simple @ [lam_bs,pi_bs];
-
-val Lomega_thy =
- Cube.thy
- |> PureThy.add_store_axioms
- [("pi_bb", "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
- ("lam_bb", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
- \ ==> Abs(A,f) : Prod(A,B)")]
- |> Theory.add_name "Lomega";
-
-val lam_bb = get_axiom Lomega_thy "lam_bb";
-val pi_bb = get_axiom Lomega_thy "pi_bb";
-val Lomega = simple @ [lam_bb,pi_bb];
-
-val LOmega_thy = merge_theories "LOmega" (L2_thy,Lomega_thy);
-val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
-
-val LP_thy =
- Cube.thy
- |> PureThy.add_store_axioms
- [("pi_sb", "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
- ("lam_sb", "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
- \ ==> Abs(A,f) : Prod(A,B)")]
- |> Theory.add_name "LP";
-
-val lam_sb = get_axiom LP_thy "lam_sb";
-val pi_sb = get_axiom LP_thy "pi_sb";
-val LP = simple @ [lam_sb,pi_sb];
-
-val LP2_thy = merge_theories "LP2" (L2_thy,LP_thy);
-val LP2 = simple @ [lam_bs,pi_bs,lam_sb,pi_sb];
-
-val LPomega_thy = merge_theories "LPomega" (LP_thy,Lomega_thy);
-val LPomega = simple @ [lam_bb,pi_bb,lam_sb,pi_sb];
-
-val CC_thy = merge_theories "CC" (L2_thy,LPomega_thy);
-val CC = simple @ [lam_bs,pi_bs,lam_bb,pi_bb,lam_sb,pi_sb];
--- a/src/Cube/Cube.thy Mon Jan 19 16:26:11 1998 +0100
+++ b/src/Cube/Cube.thy Tue Jan 20 18:26:26 1998 +0100
@@ -1,62 +1,3 @@
-(* Title: Cube/Cube.thy
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1993 University of Cambridge
-
-Barendregt's Lambda-Cube
-*)
-
-Cube = Pure +
-
-types
- term context typing
-
-arities
- term :: logic
-
-consts
- Abs, Prod :: "[term, term => term] => term"
- Trueprop :: "[context, typing] => prop" ("(_/ |- _)")
- MT_context :: "context" ("")
- Context :: "[typing, context] => context" ("_ _")
- star :: "term" ("*")
- box :: "term" ("[]")
- "^" :: "[term, term] => term" (infixl 20)
- Has_type :: "[term, term] => typing" ("(_:/ _)" [0, 0] 5)
-syntax
- Trueprop1 :: "typing => prop" ("(_)")
- "" :: "id => context" ("_ ")
- "" :: "var => context" ("_ ")
- Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
- Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
- "->" :: "[term, term] => term" (infixr 10)
-
-translations
- (prop) "x:X" == (prop) "|- x:X"
- "Lam x:A. B" == "Abs(A, %x. B)"
- "Pi x:A. B" => "Prod(A, %x. B)"
- "A -> B" => "Prod(A, _K(B))"
-
-rules
- s_b "*: []"
+Cube = Base + L2 + Lomega + LP + LP2 + LOmega + LPomega + CC
- strip_s "[| A:*; a:A ==> G |- x:X |] ==> a:A G |- x:X"
- strip_b "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"
-
- app "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"
-
- pi_ss "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
-
- lam_ss "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
- ==> Abs(A, f) : Prod(A, B)"
-
- beta "Abs(A, f)^a == f(a)"
-
-end
-
-
-ML
-
-val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
-
--- a/src/Cube/IsaMakefile Mon Jan 19 16:26:11 1998 +0100
+++ b/src/Cube/IsaMakefile Tue Jan 20 18:26:26 1998 +0100
@@ -26,7 +26,9 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/Cube: $(OUT)/Pure Cube.ML Cube.thy ROOT.ML
+$(OUT)/Cube: $(OUT)/Pure Base.ML Base.thy CC.ML CC.thy Cube.thy L2.ML \
+ L2.thy LOmega.ML LOmega.thy LP.ML LP.thy LP2.ML LP2.thy LPomega.ML \
+ LPomega.thy Lomega.ML Lomega.thy ROOT.ML
@$(ISATOOL) usedir -b $(OUT)/Pure Cube
@@ -34,7 +36,7 @@
Cube-ex: Cube $(LOG)/Cube-ex.gz
-$(LOG)/Cube-ex.gz: $(OUT)/Cube ex/ex.ML ex/ROOT.ML
+$(LOG)/Cube-ex.gz: $(OUT)/Cube ex/ex.ML ex/ex.thy ex/ROOT.ML
@$(ISATOOL) usedir $(OUT)/Cube ex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/L2.ML Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+val L2 = simple @ [lam_bs,pi_bs];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/L2.thy Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,9 @@
+
+L2 = Base +
+
+rules
+ pi_bs "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"
+ lam_bs "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
+ ==> Abs(A,f) : Prod(A,B)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/LOmega.ML Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/LOmega.thy Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+LOmega = L2 + Lomega
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/LP.ML Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+val LP = simple @ [lam_sb,pi_sb];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/LP.thy Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,9 @@
+
+LP = Base +
+
+rules
+ pi_sb "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
+ lam_sb "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
+ ==> Abs(A,f) : Prod(A,B)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/LP2.ML Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+val LP2 = simple @ [lam_bs,pi_bs,lam_sb,pi_sb];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/LP2.thy Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+LP2 = LP + L2
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/LPomega.ML Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+val LPomega = simple @ [lam_bb,pi_bb,lam_sb,pi_sb];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/LPomega.thy Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+LPomega = LP + Lomega
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/Lomega.ML Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+val Lomega = simple @ [lam_bb,pi_bb];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/Lomega.thy Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,9 @@
+
+Lomega = Base +
+
+rules
+ pi_bb "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
+ lam_bb "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
+ ==> Abs(A,f) : Prod(A,B)"
+
+end
--- a/src/Cube/ex/ROOT.ML Mon Jan 19 16:26:11 1998 +0100
+++ b/src/Cube/ex/ROOT.ML Tue Jan 20 18:26:26 1998 +0100
@@ -4,4 +4,4 @@
set proof_timing;
-use "ex.ML";
+use_thy "ex";
--- a/src/Cube/ex/ex.ML Mon Jan 19 16:26:11 1998 +0100
+++ b/src/Cube/ex/ex.ML Tue Jan 20 18:26:26 1998 +0100
@@ -6,129 +6,129 @@
fun strip_asms_tac thms i =
REPEAT(resolve_tac[strip_b,strip_s]i THEN DEPTH_SOLVE_1(ares_tac thms i));
-val imp_elim = prove_goal thy "[| f:A->B; a:A; f^a:B ==> PROP P |] ==> PROP P"
+val imp_elim = prove_goal Base.thy "[| f:A->B; a:A; f^a:B ==> PROP P |] ==> PROP P"
(fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
-val pi_elim = prove_goal thy
+val pi_elim = prove_goal Base.thy
"[| F:Prod(A,B); a:A; F^a:B(a) ==> PROP P |] ==> PROP P"
(fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
(* SIMPLE TYPES *)
-goal thy "A:* |- A->A : ?T";
+goal Base.thy "A:* |- A->A : ?T";
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
-goal thy "A:* |- Lam a:A. a : ?T";
+goal Base.thy "A:* |- Lam a:A. a : ?T";
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
-goal thy "A:* B:* b:B |- Lam x:A. b : ?T";
+goal Base.thy "A:* B:* b:B |- Lam x:A. b : ?T";
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
-goal thy "A:* b:A |- (Lam a:A. a)^b: ?T";
+goal Base.thy "A:* b:A |- (Lam a:A. a)^b: ?T";
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
-goal thy "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T";
+goal Base.thy "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T";
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
-goal thy "A:* B:* |- Lam a:A. Lam b:B. a : ?T";
+goal Base.thy "A:* B:* |- Lam a:A. Lam b:B. a : ?T";
by (DEPTH_SOLVE (ares_tac simple 1));
uresult();
(* SECOND-ORDER TYPES *)
-goal L2_thy "|- Lam A:*. Lam a:A. a : ?T";
+goal L2.thy "|- Lam A:*. Lam a:A. a : ?T";
by (DEPTH_SOLVE (ares_tac L2 1));
uresult();
-goal L2_thy "A:* |- (Lam B:*.Lam b:B. b)^A : ?T";
+goal L2.thy "A:* |- (Lam B:*.Lam b:B. b)^A : ?T";
by (DEPTH_SOLVE (ares_tac L2 1));
uresult();
-goal L2_thy "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T";
+goal L2.thy "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T";
by (DEPTH_SOLVE (ares_tac L2 1));
uresult();
-goal L2_thy "|- Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)->B) ^ a: ?T";
+goal L2.thy "|- Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)->B) ^ a: ?T";
by (DEPTH_SOLVE (ares_tac L2 1));
uresult();
(* Weakly higher-order proposiional logic *)
-goal Lomega_thy "|- Lam A:*.A->A : ?T";
+goal Lomega.thy "|- Lam A:*.A->A : ?T";
by (DEPTH_SOLVE (ares_tac Lomega 1));
uresult();
-goal Lomega_thy "B:* |- (Lam A:*.A->A) ^ B : ?T";
+goal Lomega.thy "B:* |- (Lam A:*.A->A) ^ B : ?T";
by (DEPTH_SOLVE (ares_tac Lomega 1));
uresult();
-goal Lomega_thy "B:* b:B |- (Lam y:B. b): ?T";
+goal Lomega.thy "B:* b:B |- (Lam y:B. b): ?T";
by (DEPTH_SOLVE (ares_tac Lomega 1));
uresult();
-goal Lomega_thy "A:* F:*->* |- F^(F^A): ?T";
+goal Lomega.thy "A:* F:*->* |- F^(F^A): ?T";
by (DEPTH_SOLVE (ares_tac Lomega 1));
uresult();
-goal Lomega_thy "A:* |- Lam F:*->*.F^(F^A): ?T";
+goal Lomega.thy "A:* |- Lam F:*->*.F^(F^A): ?T";
by (DEPTH_SOLVE (ares_tac Lomega 1));
uresult();
(* LF *)
-goal LP_thy "A:* |- A -> * : ?T";
+goal LP.thy "A:* |- A -> * : ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->* a:A |- P^a: ?T";
+goal LP.thy "A:* P:A->* a:A |- P^a: ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T";
+goal LP.thy "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T";
+goal LP.thy "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T";
+goal LP.thy "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T";
+goal LP.thy "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T";
+goal LP.thy "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
-goal LP_thy "A:* P:A->* Q:* a0:A |- \
+goal LP.thy "A:* P:A->* Q:* a0:A |- \
\ Lam x:Pi a:A. P^a->Q. Lam y:Pi a:A. P^a. x^a0^(y^a0): ?T";
by (DEPTH_SOLVE (ares_tac LP 1));
uresult();
(* OMEGA-ORDER TYPES *)
-goal L2_thy "A:* B:* |- Pi C:*.(A->B->C)->C : ?T";
+goal L2.thy "A:* B:* |- Pi C:*.(A->B->C)->C : ?T";
by (DEPTH_SOLVE (ares_tac L2 1));
uresult();
-goal LOmega_thy "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T";
+goal LOmega.thy "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T";
by (DEPTH_SOLVE (ares_tac LOmega 1));
uresult();
-goal LOmega_thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T";
+goal LOmega.thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T";
by (DEPTH_SOLVE (ares_tac LOmega 1));
uresult();
-goal LOmega_thy "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))";
+goal LOmega.thy "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))";
by (strip_asms_tac LOmega 1);
by (rtac lam_ss 1);
by (DEPTH_SOLVE_1(ares_tac LOmega 1));
@@ -148,17 +148,17 @@
(* Second-order Predicate Logic *)
-goal LP2_thy "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T";
+goal LP2.thy "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T";
by (DEPTH_SOLVE (ares_tac LP2 1));
uresult();
-goal LP2_thy "A:* P:A->A->* |- \
+goal LP2.thy "A:* P:A->A->* |- \
\ (Pi a:A. Pi b:A. P^a^b->P^b^a->Pi P:*.P) -> Pi a:A. P^a^a->Pi P:*.P : ?T";
by (DEPTH_SOLVE (ares_tac LP2 1));
uresult();
(* Antisymmetry implies irreflexivity: *)
-goal LP2_thy "A:* P:A->A->* |- \
+goal LP2.thy "A:* P:A->A->* |- \
\ ?p: (Pi a:A. Pi b:A. P^a^b->P^b^a->Pi P:*.P) -> Pi a:A. P^a^a->Pi P:*.P";
by (strip_asms_tac LP2 1);
by (rtac lam_ss 1);
@@ -175,25 +175,25 @@
(* LPomega *)
-goal LPomega_thy "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T";
+goal LPomega.thy "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T";
by (DEPTH_SOLVE (ares_tac LPomega 1));
uresult();
-goal LPomega_thy "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T";
+goal LPomega.thy "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T";
by (DEPTH_SOLVE (ares_tac LPomega 1));
uresult();
(* CONSTRUCTIONS *)
-goal CC_thy "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T";
+goal CC.thy "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T";
by (DEPTH_SOLVE (ares_tac CC 1));
uresult();
-goal CC_thy "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T";
+goal CC.thy "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T";
by (DEPTH_SOLVE (ares_tac CC 1));
uresult();
-goal CC_thy "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a";
+goal CC.thy "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a";
by (strip_asms_tac CC 1);
by (rtac lam_ss 1);
by (DEPTH_SOLVE_1(ares_tac CC 1));
@@ -203,18 +203,18 @@
(* Some random examples *)
-goal LP2_thy "A:* c:A f:A->A |- \
+goal LP2.thy "A:* c:A f:A->A |- \
\ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
by (DEPTH_SOLVE(ares_tac LP2 1));
uresult();
-goal CC_thy "Lam A:*.Lam c:A. Lam f:A->A. \
+goal CC.thy "Lam A:*.Lam c:A. Lam f:A->A. \
\ Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
by (DEPTH_SOLVE(ares_tac CC 1));
uresult();
(* Symmetry of Leibnitz equality *)
-goal LP2_thy "A:* a:A b:A |- ?p: (Pi P:A->*.P^a->P^b) -> (Pi P:A->*.P^b->P^a)";
+goal LP2.thy "A:* a:A b:A |- ?p: (Pi P:A->*.P^a->P^b) -> (Pi P:A->*.P^b->P^a)";
by (strip_asms_tac LP2 1);
by (rtac lam_ss 1);
by (DEPTH_SOLVE_1(ares_tac LP2 1));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/ex/ex.thy Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,2 @@
+
+ex = Cube