reorganized into individual theories;
authorwenzelm
Tue Jan 20 18:26:26 1998 +0100 (1998-01-20)
changeset 45836d9be46ea566
parent 4582 c5cfd00e4f28
child 4584 3588b8f9613f
reorganized into individual theories;
src/Cube/Base.ML
src/Cube/Base.thy
src/Cube/CC.ML
src/Cube/CC.thy
src/Cube/Cube.ML
src/Cube/Cube.thy
src/Cube/IsaMakefile
src/Cube/L2.ML
src/Cube/L2.thy
src/Cube/LOmega.ML
src/Cube/LOmega.thy
src/Cube/LP.ML
src/Cube/LP.thy
src/Cube/LP2.ML
src/Cube/LP2.thy
src/Cube/LPomega.ML
src/Cube/LPomega.thy
src/Cube/Lomega.ML
src/Cube/Lomega.thy
src/Cube/ex/ROOT.ML
src/Cube/ex/ex.ML
src/Cube/ex/ex.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Cube/Base.ML	Tue Jan 20 18:26:26 1998 +0100
     1.3 @@ -0,0 +1,2 @@
     1.4 +
     1.5 +val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Cube/Base.thy	Tue Jan 20 18:26:26 1998 +0100
     2.3 @@ -0,0 +1,62 @@
     2.4 +(*  Title:      Cube/Base.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow
     2.7 +    Copyright   1993  University of Cambridge
     2.8 +
     2.9 +Barendregt's Lambda-Cube.
    2.10 +*)
    2.11 +
    2.12 +Base = Pure +
    2.13 +
    2.14 +types
    2.15 +  term  context  typing
    2.16 +
    2.17 +arities
    2.18 +  term :: logic
    2.19 +
    2.20 +consts
    2.21 +  Abs, Prod     :: "[term, term => term] => term"
    2.22 +  Trueprop      :: "[context, typing] => prop"          ("(_/ |- _)")
    2.23 +  MT_context    :: "context"                            ("")
    2.24 +  Context       :: "[typing, context] => context"       ("_ _")
    2.25 +  star          :: "term"                               ("*")
    2.26 +  box           :: "term"                               ("[]")
    2.27 +  "^"           :: "[term, term] => term"               (infixl 20)
    2.28 +  Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
    2.29 +
    2.30 +syntax
    2.31 +  Trueprop1     :: "typing => prop"                     ("(_)")
    2.32 +  ""            :: "id => context"                      ("_ ")
    2.33 +  ""            :: "var => context"                     ("_ ")
    2.34 +  Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
    2.35 +  Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
    2.36 +  "->"          :: "[term, term] => term"               (infixr 10)
    2.37 +
    2.38 +translations
    2.39 +  (prop) "x:X"  == (prop) "|- x:X"
    2.40 +  "Lam x:A. B"  == "Abs(A, %x. B)"
    2.41 +  "Pi x:A. B"   => "Prod(A, %x. B)"
    2.42 +  "A -> B"      => "Prod(A, _K(B))"
    2.43 +
    2.44 +rules
    2.45 +  s_b           "*: []"
    2.46 +
    2.47 +  strip_s       "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
    2.48 +  strip_b       "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"
    2.49 +
    2.50 +  app           "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"
    2.51 +
    2.52 +  pi_ss         "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
    2.53 +
    2.54 +  lam_ss        "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
    2.55 +                   ==> Abs(A, f) : Prod(A, B)"
    2.56 +
    2.57 +  beta          "Abs(A, f)^a == f(a)"
    2.58 +
    2.59 +end
    2.60 +
    2.61 +
    2.62 +ML
    2.63 +
    2.64 +val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
    2.65 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Cube/CC.ML	Tue Jan 20 18:26:26 1998 +0100
     3.3 @@ -0,0 +1,2 @@
     3.4 +
     3.5 +val CC = simple @ [lam_bs,pi_bs,lam_bb,pi_bb,lam_sb,pi_sb];
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Cube/CC.thy	Tue Jan 20 18:26:26 1998 +0100
     4.3 @@ -0,0 +1,3 @@
     4.4 +
     4.5 +CC = L2 + LP + Lomega
     4.6 +
     5.1 --- a/src/Cube/Cube.ML	Mon Jan 19 16:26:11 1998 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,60 +0,0 @@
     5.4 -(*  Title:      Cube/Cube.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Tobias Nipkow
     5.7 -    Copyright   1990  University of Cambridge
     5.8 -
     5.9 -For Cube.thy.  The systems of the Lambda-cube that extend simple types
    5.10 -*)
    5.11 -
    5.12 -open Cube;
    5.13 -
    5.14 -val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];
    5.15 -
    5.16 -val L2_thy =
    5.17 -  Cube.thy
    5.18 -  |> PureThy.add_store_axioms
    5.19 -   [("pi_bs",  "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
    5.20 -    ("lam_bs", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
    5.21 -     \  ==> Abs(A,f) : Prod(A,B)")]
    5.22 -  |> Theory.add_name "L2";
    5.23 -
    5.24 -val lam_bs = get_axiom L2_thy "lam_bs";
    5.25 -val pi_bs = get_axiom L2_thy "pi_bs";
    5.26 -
    5.27 -val L2 = simple @ [lam_bs,pi_bs];
    5.28 -
    5.29 -val Lomega_thy =
    5.30 -  Cube.thy
    5.31 -  |> PureThy.add_store_axioms
    5.32 -   [("pi_bb",  "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
    5.33 -    ("lam_bb", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
    5.34 -     \  ==> Abs(A,f) : Prod(A,B)")]
    5.35 -  |> Theory.add_name "Lomega";
    5.36 -
    5.37 -val lam_bb = get_axiom Lomega_thy "lam_bb";
    5.38 -val pi_bb = get_axiom Lomega_thy "pi_bb";
    5.39 -val Lomega = simple @ [lam_bb,pi_bb];
    5.40 -
    5.41 -val LOmega_thy = merge_theories "LOmega" (L2_thy,Lomega_thy);
    5.42 -val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
    5.43 -
    5.44 -val LP_thy =
    5.45 -  Cube.thy
    5.46 -  |> PureThy.add_store_axioms
    5.47 -   [("pi_sb",  "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
    5.48 -    ("lam_sb", "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
    5.49 -     \  ==> Abs(A,f) : Prod(A,B)")]
    5.50 -  |> Theory.add_name "LP";
    5.51 -
    5.52 -val lam_sb = get_axiom LP_thy "lam_sb";
    5.53 -val pi_sb = get_axiom LP_thy "pi_sb";
    5.54 -val LP = simple @ [lam_sb,pi_sb];
    5.55 -
    5.56 -val LP2_thy = merge_theories "LP2" (L2_thy,LP_thy);
    5.57 -val LP2 = simple @ [lam_bs,pi_bs,lam_sb,pi_sb];
    5.58 -
    5.59 -val LPomega_thy = merge_theories "LPomega" (LP_thy,Lomega_thy);
    5.60 -val LPomega = simple @ [lam_bb,pi_bb,lam_sb,pi_sb];
    5.61 -
    5.62 -val CC_thy = merge_theories "CC" (L2_thy,LPomega_thy);
    5.63 -val CC = simple @ [lam_bs,pi_bs,lam_bb,pi_bb,lam_sb,pi_sb];
     6.1 --- a/src/Cube/Cube.thy	Mon Jan 19 16:26:11 1998 +0100
     6.2 +++ b/src/Cube/Cube.thy	Tue Jan 20 18:26:26 1998 +0100
     6.3 @@ -1,62 +1,3 @@
     6.4 -(*  Title:      Cube/Cube.thy
     6.5 -    ID:         $Id$
     6.6 -    Author:     Tobias Nipkow
     6.7 -    Copyright   1993  University of Cambridge
     6.8 -
     6.9 -Barendregt's Lambda-Cube
    6.10 -*)
    6.11 -
    6.12 -Cube = Pure +
    6.13 -
    6.14 -types
    6.15 -  term  context  typing
    6.16 -
    6.17 -arities
    6.18 -  term :: logic
    6.19 -
    6.20 -consts
    6.21 -  Abs, Prod     :: "[term, term => term] => term"
    6.22 -  Trueprop      :: "[context, typing] => prop"          ("(_/ |- _)")
    6.23 -  MT_context    :: "context"                            ("")
    6.24 -  Context       :: "[typing, context] => context"       ("_ _")
    6.25 -  star          :: "term"                               ("*")
    6.26 -  box           :: "term"                               ("[]")
    6.27 -  "^"           :: "[term, term] => term"               (infixl 20)
    6.28 -  Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
    6.29  
    6.30 -syntax
    6.31 -  Trueprop1     :: "typing => prop"                     ("(_)")
    6.32 -  ""            :: "id => context"                      ("_ ")
    6.33 -  ""            :: "var => context"                     ("_ ")
    6.34 -  Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
    6.35 -  Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
    6.36 -  "->"          :: "[term, term] => term"               (infixr 10)
    6.37 -
    6.38 -translations
    6.39 -  (prop) "x:X"  == (prop) "|- x:X"
    6.40 -  "Lam x:A. B"  == "Abs(A, %x. B)"
    6.41 -  "Pi x:A. B"   => "Prod(A, %x. B)"
    6.42 -  "A -> B"      => "Prod(A, _K(B))"
    6.43 -
    6.44 -rules
    6.45 -  s_b           "*: []"
    6.46 +Cube = Base + L2 + Lomega + LP + LP2 + LOmega + LPomega + CC
    6.47  
    6.48 -  strip_s       "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
    6.49 -  strip_b       "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"
    6.50 -
    6.51 -  app           "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"
    6.52 -
    6.53 -  pi_ss         "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
    6.54 -
    6.55 -  lam_ss        "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] 
    6.56 -                   ==> Abs(A, f) : Prod(A, B)"
    6.57 -
    6.58 -  beta          "Abs(A, f)^a == f(a)"
    6.59 -
    6.60 -end
    6.61 -
    6.62 -
    6.63 -ML
    6.64 -
    6.65 -val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
    6.66 -
     7.1 --- a/src/Cube/IsaMakefile	Mon Jan 19 16:26:11 1998 +0100
     7.2 +++ b/src/Cube/IsaMakefile	Tue Jan 20 18:26:26 1998 +0100
     7.3 @@ -26,7 +26,9 @@
     7.4  Pure:
     7.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     7.6  
     7.7 -$(OUT)/Cube: $(OUT)/Pure Cube.ML Cube.thy ROOT.ML
     7.8 +$(OUT)/Cube: $(OUT)/Pure Base.ML Base.thy CC.ML CC.thy Cube.thy L2.ML \
     7.9 +  L2.thy LOmega.ML LOmega.thy LP.ML LP.thy LP2.ML LP2.thy LPomega.ML \
    7.10 +  LPomega.thy Lomega.ML Lomega.thy ROOT.ML
    7.11  	@$(ISATOOL) usedir -b $(OUT)/Pure Cube
    7.12  
    7.13  
    7.14 @@ -34,7 +36,7 @@
    7.15  
    7.16  Cube-ex: Cube $(LOG)/Cube-ex.gz
    7.17  
    7.18 -$(LOG)/Cube-ex.gz: $(OUT)/Cube ex/ex.ML ex/ROOT.ML
    7.19 +$(LOG)/Cube-ex.gz: $(OUT)/Cube ex/ex.ML ex/ex.thy ex/ROOT.ML
    7.20  	@$(ISATOOL) usedir $(OUT)/Cube ex
    7.21  
    7.22  
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Cube/L2.ML	Tue Jan 20 18:26:26 1998 +0100
     8.3 @@ -0,0 +1,2 @@
     8.4 +
     8.5 +val L2 = simple @ [lam_bs,pi_bs];
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Cube/L2.thy	Tue Jan 20 18:26:26 1998 +0100
     9.3 @@ -0,0 +1,9 @@
     9.4 +
     9.5 +L2 = Base +
     9.6 +
     9.7 +rules
     9.8 +  pi_bs         "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"
     9.9 +  lam_bs        "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
    9.10 +                   ==> Abs(A,f) : Prod(A,B)"
    9.11 +
    9.12 +end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Cube/LOmega.ML	Tue Jan 20 18:26:26 1998 +0100
    10.3 @@ -0,0 +1,2 @@
    10.4 +
    10.5 +val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Cube/LOmega.thy	Tue Jan 20 18:26:26 1998 +0100
    11.3 @@ -0,0 +1,2 @@
    11.4 +
    11.5 +LOmega = L2 + Lomega
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Cube/LP.ML	Tue Jan 20 18:26:26 1998 +0100
    12.3 @@ -0,0 +1,2 @@
    12.4 +
    12.5 +val LP = simple @ [lam_sb,pi_sb];
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Cube/LP.thy	Tue Jan 20 18:26:26 1998 +0100
    13.3 @@ -0,0 +1,9 @@
    13.4 +
    13.5 +LP = Base +
    13.6 +
    13.7 +rules
    13.8 +  pi_sb         "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
    13.9 +  lam_sb        "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
   13.10 +                   ==> Abs(A,f) : Prod(A,B)"
   13.11 +
   13.12 +end
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Cube/LP2.ML	Tue Jan 20 18:26:26 1998 +0100
    14.3 @@ -0,0 +1,2 @@
    14.4 +
    14.5 +val LP2 = simple @ [lam_bs,pi_bs,lam_sb,pi_sb];
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/Cube/LP2.thy	Tue Jan 20 18:26:26 1998 +0100
    15.3 @@ -0,0 +1,2 @@
    15.4 +
    15.5 +LP2 = LP + L2
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/Cube/LPomega.ML	Tue Jan 20 18:26:26 1998 +0100
    16.3 @@ -0,0 +1,2 @@
    16.4 +
    16.5 +val LPomega = simple @ [lam_bb,pi_bb,lam_sb,pi_sb];
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/Cube/LPomega.thy	Tue Jan 20 18:26:26 1998 +0100
    17.3 @@ -0,0 +1,2 @@
    17.4 +
    17.5 +LPomega = LP + Lomega
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/Cube/Lomega.ML	Tue Jan 20 18:26:26 1998 +0100
    18.3 @@ -0,0 +1,2 @@
    18.4 +
    18.5 +val Lomega = simple @ [lam_bb,pi_bb];
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/Cube/Lomega.thy	Tue Jan 20 18:26:26 1998 +0100
    19.3 @@ -0,0 +1,9 @@
    19.4 +
    19.5 +Lomega = Base +
    19.6 +
    19.7 +rules
    19.8 +  pi_bb         "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
    19.9 +  lam_bb        "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
   19.10 +                   ==> Abs(A,f) : Prod(A,B)"
   19.11 +
   19.12 +end
    20.1 --- a/src/Cube/ex/ROOT.ML	Mon Jan 19 16:26:11 1998 +0100
    20.2 +++ b/src/Cube/ex/ROOT.ML	Tue Jan 20 18:26:26 1998 +0100
    20.3 @@ -4,4 +4,4 @@
    20.4  
    20.5  set proof_timing;
    20.6  
    20.7 -use "ex.ML";
    20.8 +use_thy "ex";
    21.1 --- a/src/Cube/ex/ex.ML	Mon Jan 19 16:26:11 1998 +0100
    21.2 +++ b/src/Cube/ex/ex.ML	Tue Jan 20 18:26:26 1998 +0100
    21.3 @@ -6,129 +6,129 @@
    21.4  fun strip_asms_tac thms  i =
    21.5      REPEAT(resolve_tac[strip_b,strip_s]i THEN DEPTH_SOLVE_1(ares_tac thms i));
    21.6  
    21.7 -val imp_elim = prove_goal thy "[| f:A->B; a:A; f^a:B ==> PROP P |] ==> PROP P"
    21.8 +val imp_elim = prove_goal Base.thy "[| f:A->B; a:A; f^a:B ==> PROP P |] ==> PROP P"
    21.9          (fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
   21.10  
   21.11 -val pi_elim = prove_goal thy
   21.12 +val pi_elim = prove_goal Base.thy
   21.13          "[| F:Prod(A,B); a:A; F^a:B(a) ==> PROP P |] ==> PROP P"
   21.14          (fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
   21.15  
   21.16  (* SIMPLE TYPES *)
   21.17  
   21.18 -goal thy "A:* |- A->A : ?T";
   21.19 +goal Base.thy "A:* |- A->A : ?T";
   21.20  by (DEPTH_SOLVE (ares_tac simple 1));
   21.21  uresult();
   21.22  
   21.23 -goal thy "A:* |- Lam a:A. a : ?T";
   21.24 +goal Base.thy "A:* |- Lam a:A. a : ?T";
   21.25  by (DEPTH_SOLVE (ares_tac simple 1));
   21.26  uresult();
   21.27  
   21.28 -goal thy "A:* B:* b:B |- Lam x:A. b : ?T";
   21.29 +goal Base.thy "A:* B:* b:B |- Lam x:A. b : ?T";
   21.30  by (DEPTH_SOLVE (ares_tac simple 1));
   21.31  uresult();
   21.32  
   21.33 -goal thy "A:* b:A |- (Lam a:A. a)^b: ?T";
   21.34 +goal Base.thy "A:* b:A |- (Lam a:A. a)^b: ?T";
   21.35  by (DEPTH_SOLVE (ares_tac simple 1));
   21.36  uresult();
   21.37  
   21.38 -goal thy "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T";
   21.39 +goal Base.thy "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T";
   21.40  by (DEPTH_SOLVE (ares_tac simple 1));
   21.41  uresult();
   21.42  
   21.43 -goal thy "A:* B:* |- Lam a:A. Lam b:B. a : ?T";
   21.44 +goal Base.thy "A:* B:* |- Lam a:A. Lam b:B. a : ?T";
   21.45  by (DEPTH_SOLVE (ares_tac simple 1));
   21.46  uresult();
   21.47  
   21.48  (* SECOND-ORDER TYPES *)
   21.49  
   21.50 -goal L2_thy "|- Lam A:*. Lam a:A. a : ?T";
   21.51 +goal L2.thy "|- Lam A:*. Lam a:A. a : ?T";
   21.52  by (DEPTH_SOLVE (ares_tac L2 1));
   21.53  uresult();
   21.54  
   21.55 -goal L2_thy "A:* |- (Lam B:*.Lam b:B. b)^A : ?T";
   21.56 +goal L2.thy "A:* |- (Lam B:*.Lam b:B. b)^A : ?T";
   21.57  by (DEPTH_SOLVE (ares_tac L2 1));
   21.58  uresult();
   21.59  
   21.60 -goal L2_thy "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T";
   21.61 +goal L2.thy "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T";
   21.62  by (DEPTH_SOLVE (ares_tac L2 1));
   21.63  uresult();
   21.64  
   21.65 -goal L2_thy "|- Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)->B) ^ a: ?T";
   21.66 +goal L2.thy "|- Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)->B) ^ a: ?T";
   21.67  by (DEPTH_SOLVE (ares_tac L2 1));
   21.68  uresult();
   21.69  
   21.70  (* Weakly higher-order proposiional logic *)
   21.71  
   21.72 -goal Lomega_thy "|- Lam A:*.A->A : ?T";
   21.73 +goal Lomega.thy "|- Lam A:*.A->A : ?T";
   21.74  by (DEPTH_SOLVE (ares_tac Lomega 1));
   21.75  uresult();
   21.76  
   21.77 -goal Lomega_thy "B:* |- (Lam A:*.A->A) ^ B : ?T";
   21.78 +goal Lomega.thy "B:* |- (Lam A:*.A->A) ^ B : ?T";
   21.79  by (DEPTH_SOLVE (ares_tac Lomega 1));
   21.80  uresult();
   21.81  
   21.82 -goal Lomega_thy "B:* b:B |- (Lam y:B. b): ?T";
   21.83 +goal Lomega.thy "B:* b:B |- (Lam y:B. b): ?T";
   21.84  by (DEPTH_SOLVE (ares_tac Lomega 1));
   21.85  uresult();
   21.86  
   21.87 -goal Lomega_thy "A:* F:*->* |- F^(F^A): ?T";
   21.88 +goal Lomega.thy "A:* F:*->* |- F^(F^A): ?T";
   21.89  by (DEPTH_SOLVE (ares_tac Lomega 1));
   21.90  uresult();
   21.91  
   21.92 -goal Lomega_thy "A:* |- Lam F:*->*.F^(F^A): ?T";
   21.93 +goal Lomega.thy "A:* |- Lam F:*->*.F^(F^A): ?T";
   21.94  by (DEPTH_SOLVE (ares_tac Lomega 1));
   21.95  uresult();
   21.96  
   21.97  (* LF *)
   21.98  
   21.99 -goal LP_thy "A:* |- A -> * : ?T";
  21.100 +goal LP.thy "A:* |- A -> * : ?T";
  21.101  by (DEPTH_SOLVE (ares_tac LP 1));
  21.102  uresult();
  21.103  
  21.104 -goal LP_thy "A:* P:A->* a:A |- P^a: ?T";
  21.105 +goal LP.thy "A:* P:A->* a:A |- P^a: ?T";
  21.106  by (DEPTH_SOLVE (ares_tac LP 1));
  21.107  uresult();
  21.108  
  21.109 -goal LP_thy "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T";
  21.110 +goal LP.thy "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T";
  21.111  by (DEPTH_SOLVE (ares_tac LP 1));
  21.112  uresult();
  21.113  
  21.114 -goal LP_thy "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T";
  21.115 +goal LP.thy "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T";
  21.116  by (DEPTH_SOLVE (ares_tac LP 1));
  21.117  uresult();
  21.118  
  21.119 -goal LP_thy "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T";
  21.120 +goal LP.thy "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T";
  21.121  by (DEPTH_SOLVE (ares_tac LP 1));
  21.122  uresult();
  21.123  
  21.124 -goal LP_thy "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T";
  21.125 +goal LP.thy "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T";
  21.126  by (DEPTH_SOLVE (ares_tac LP 1));
  21.127  uresult();
  21.128  
  21.129 -goal LP_thy "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T";
  21.130 +goal LP.thy "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T";
  21.131  by (DEPTH_SOLVE (ares_tac LP 1));
  21.132  uresult();
  21.133  
  21.134 -goal LP_thy "A:* P:A->* Q:* a0:A |- \
  21.135 +goal LP.thy "A:* P:A->* Q:* a0:A |- \
  21.136  \       Lam x:Pi a:A. P^a->Q. Lam y:Pi a:A. P^a. x^a0^(y^a0): ?T";
  21.137  by (DEPTH_SOLVE (ares_tac LP 1));
  21.138  uresult();
  21.139  
  21.140  (* OMEGA-ORDER TYPES *)
  21.141  
  21.142 -goal L2_thy "A:* B:* |- Pi C:*.(A->B->C)->C : ?T";
  21.143 +goal L2.thy "A:* B:* |- Pi C:*.(A->B->C)->C : ?T";
  21.144  by (DEPTH_SOLVE (ares_tac L2 1));
  21.145  uresult();
  21.146  
  21.147 -goal LOmega_thy "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T";
  21.148 +goal LOmega.thy "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T";
  21.149  by (DEPTH_SOLVE (ares_tac LOmega 1));
  21.150  uresult();
  21.151  
  21.152 -goal LOmega_thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T";
  21.153 +goal LOmega.thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T";
  21.154  by (DEPTH_SOLVE (ares_tac LOmega 1));
  21.155  uresult();
  21.156  
  21.157 -goal LOmega_thy "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))";
  21.158 +goal LOmega.thy "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))";
  21.159  by (strip_asms_tac LOmega 1);
  21.160  by (rtac lam_ss 1);
  21.161  by (DEPTH_SOLVE_1(ares_tac LOmega 1));
  21.162 @@ -148,17 +148,17 @@
  21.163  
  21.164  (* Second-order Predicate Logic *)
  21.165  
  21.166 -goal LP2_thy "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T";
  21.167 +goal LP2.thy "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T";
  21.168  by (DEPTH_SOLVE (ares_tac LP2 1));
  21.169  uresult();
  21.170  
  21.171 -goal LP2_thy "A:* P:A->A->* |- \
  21.172 +goal LP2.thy "A:* P:A->A->* |- \
  21.173  \       (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";
  21.174  by (DEPTH_SOLVE (ares_tac LP2 1));
  21.175  uresult();
  21.176  
  21.177  (* Antisymmetry implies irreflexivity: *)
  21.178 -goal LP2_thy "A:* P:A->A->* |- \
  21.179 +goal LP2.thy "A:* P:A->A->* |- \
  21.180  \       ?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";
  21.181  by (strip_asms_tac LP2 1);
  21.182  by (rtac lam_ss 1);
  21.183 @@ -175,25 +175,25 @@
  21.184  
  21.185  (* LPomega *)
  21.186  
  21.187 -goal LPomega_thy "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T";
  21.188 +goal LPomega.thy "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T";
  21.189  by (DEPTH_SOLVE (ares_tac LPomega 1));
  21.190  uresult();
  21.191  
  21.192 -goal LPomega_thy "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T";
  21.193 +goal LPomega.thy "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T";
  21.194  by (DEPTH_SOLVE (ares_tac LPomega 1));
  21.195  uresult();
  21.196  
  21.197  (* CONSTRUCTIONS *)
  21.198  
  21.199 -goal CC_thy "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T";
  21.200 +goal CC.thy "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T";
  21.201  by (DEPTH_SOLVE (ares_tac CC 1));
  21.202  uresult();
  21.203  
  21.204 -goal CC_thy "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T";
  21.205 +goal CC.thy "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T";
  21.206  by (DEPTH_SOLVE (ares_tac CC 1));
  21.207  uresult();
  21.208  
  21.209 -goal CC_thy "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a";
  21.210 +goal CC.thy "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a";
  21.211  by (strip_asms_tac CC 1);
  21.212  by (rtac lam_ss 1);
  21.213  by (DEPTH_SOLVE_1(ares_tac CC 1));
  21.214 @@ -203,18 +203,18 @@
  21.215  
  21.216  (* Some random examples *)
  21.217  
  21.218 -goal LP2_thy "A:* c:A f:A->A |- \
  21.219 +goal LP2.thy "A:* c:A f:A->A |- \
  21.220  \       Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
  21.221  by (DEPTH_SOLVE(ares_tac LP2 1));
  21.222  uresult();
  21.223  
  21.224 -goal CC_thy "Lam A:*.Lam c:A. Lam f:A->A. \
  21.225 +goal CC.thy "Lam A:*.Lam c:A. Lam f:A->A. \
  21.226  \       Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
  21.227  by (DEPTH_SOLVE(ares_tac CC 1));
  21.228  uresult();
  21.229  
  21.230  (* Symmetry of Leibnitz equality *)
  21.231 -goal LP2_thy "A:* a:A b:A |- ?p: (Pi P:A->*.P^a->P^b) -> (Pi P:A->*.P^b->P^a)";
  21.232 +goal LP2.thy "A:* a:A b:A |- ?p: (Pi P:A->*.P^a->P^b) -> (Pi P:A->*.P^b->P^a)";
  21.233  by (strip_asms_tac LP2 1);
  21.234  by (rtac lam_ss 1);
  21.235  by (DEPTH_SOLVE_1(ares_tac LP2 1));
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/Cube/ex/ex.thy	Tue Jan 20 18:26:26 1998 +0100
    22.3 @@ -0,0 +1,2 @@
    22.4 +
    22.5 +ex = Cube