--- a/src/Cube/Cube.thy Sat Sep 03 21:43:12 2005 +0200
+++ b/src/Cube/Cube.thy Sat Sep 03 21:43:50 2005 +0200
@@ -1,3 +1,119 @@
-Cube = Base + L2 + Lomega + LP + LP2 + Lomega2 + LPomega + CC
+header {* Barendregt's Lambda-Cube *}
+
+theory Cube
+imports Pure
+begin
+
+typedecl "term"
+typedecl "context"
+typedecl typing
+
+nonterminals
+ context_ typing_
+
+consts
+ Abs :: "[term, term => term] => term"
+ Prod :: "[term, term => term] => term"
+ Trueprop :: "[context, typing] => prop"
+ MT_context :: "context"
+ Context :: "[typing, context] => context"
+ star :: "term" ("*")
+ box :: "term" ("[]")
+ app :: "[term, term] => term" (infixl "^" 20)
+ Has_type :: "[term, term] => typing"
+
+syntax
+ Trueprop :: "[context_, typing_] => prop" ("(_/ |- _)")
+ Trueprop1 :: "typing_ => prop" ("(_)")
+ "" :: "id => context_" ("_")
+ "" :: "var => context_" ("_")
+ MT_context :: "context_" ("")
+ Context :: "[typing_, context_] => context_" ("_ _")
+ Has_type :: "[term, term] => typing_" ("(_:/ _)" [0, 0] 5)
+ Lam :: "[idt, term, term] => term" ("(3Lam _:_./ _)" [0, 0, 0] 10)
+ Pi :: "[idt, term, term] => term" ("(3Pi _:_./ _)" [0, 0] 10)
+ arrow :: "[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))"
+
+syntax (xsymbols)
+ Trueprop :: "[context_, typing_] => prop" ("(_/ \<turnstile> _)")
+ box :: "term" ("\<box>")
+ Lam :: "[idt, term, term] => term" ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
+ Pi :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10)
+ arrow :: "[term, term] => term" (infixr "\<rightarrow>" 10)
+
+print_translation {* [("Prod", dependent_tr' ("Pi", "arrow"))] *}
+
+axioms
+ 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)"
+
+lemmas simple = s_b strip_s strip_b app lam_ss pi_ss
+lemmas rules = simple
+
+lemma imp_elim:
+ assumes "f:A->B" and "a:A" and "f^a:B ==> PROP P"
+ shows "PROP P" by (rule app prems)+
+
+lemma pi_elim:
+ assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P"
+ shows "PROP P" by (rule app prems)+
+
+
+locale L2 =
+ assumes pi_bs: "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"
+ and lam_bs: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
+ ==> Abs(A,f) : Prod(A,B)"
+
+lemmas (in L2) rules = simple lam_bs pi_bs
+
+locale Lomega =
+ assumes
+ pi_bb: "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
+ and lam_bb: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
+ ==> Abs(A,f) : Prod(A,B)"
+
+lemmas (in Lomega) rules = simple lam_bb pi_bb
+
+
+locale LP =
+ assumes pi_sb: "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
+ and lam_sb: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
+ ==> Abs(A,f) : Prod(A,B)"
+
+lemmas (in LP) rules = simple lam_sb pi_sb
+
+locale LP2 = LP + L2
+
+lemmas (in LP2) rules = simple lam_bs pi_bs lam_sb pi_sb
+
+locale Lomega2 = L2 + Lomega
+
+lemmas (in Lomega2) rules = simple lam_bs pi_bs lam_bb pi_bb
+
+locale LPomega = LP + Lomega
+
+lemmas (in LPomega) rules = simple lam_bb pi_bb lam_sb pi_sb
+
+locale CC = L2 + LP + Lomega
+
+lemmas (in CC) rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
+
+end
--- a/src/Cube/IsaMakefile Sat Sep 03 21:43:12 2005 +0200
+++ b/src/Cube/IsaMakefile Sat Sep 03 21:43:50 2005 +0200
@@ -26,9 +26,7 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/Cube: $(OUT)/Pure Base.ML Base.thy CC.ML CC.thy Cube.thy L2.ML \
- L2.thy Lomega2.ML Lomega2.thy LP.ML LP.thy LP2.ML LP2.thy LPomega.ML \
- LPomega.thy Lomega.ML Lomega.thy ROOT.ML
+$(OUT)/Cube: $(OUT)/Pure Cube.thy ROOT.ML
@$(ISATOOL) usedir -b $(OUT)/Pure Cube
@@ -36,7 +34,7 @@
Cube-ex: Cube $(LOG)/Cube-ex.gz
-$(LOG)/Cube-ex.gz: $(OUT)/Cube ex/ex.ML ex/ex.thy ex/ROOT.ML
+$(LOG)/Cube-ex.gz: $(OUT)/Cube ex/ex.thy ex/ROOT.ML
@$(ISATOOL) usedir $(OUT)/Cube ex
--- a/src/Cube/ROOT.ML Sat Sep 03 21:43:12 2005 +0200
+++ b/src/Cube/ROOT.ML Sat Sep 03 21:43:50 2005 +0200
@@ -9,8 +9,4 @@
val banner = "Barendregt's Lambda-Cube";
writeln banner;
-print_depth 1;
-
use_thy "Cube";
-
-print_depth 8;
--- a/src/Cube/ex/ex.thy Sat Sep 03 21:43:12 2005 +0200
+++ b/src/Cube/ex/ex.thy Sat Sep 03 21:43:50 2005 +0200
@@ -1,2 +1,236 @@
-ex = Cube
+theory ex
+imports Cube
+begin
+
+text {*
+ Examples taken from:
+
+ H. Barendregt. Introduction to Generalised Type Systems.
+ J. Functional Programming.
+*}
+
+method_setup depth_solve = {*
+ Method.thms_args (fn thms => Method.METHOD (fn facts =>
+ (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
+*} ""
+
+method_setup depth_solve1 = {*
+ Method.thms_args (fn thms => Method.METHOD (fn facts =>
+ (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))
+*} ""
+
+ML {*
+local val strip_b = thm "strip_b" and strip_s = thm "strip_s" in
+fun strip_asms_tac thms i =
+ REPEAT (resolve_tac [strip_b, strip_s] i THEN DEPTH_SOLVE_1 (ares_tac thms i))
+end
+*}
+
+
+subsection {* Simple types *}
+
+lemma "A:* |- A->A : ?T"
+ by (depth_solve rules)
+
+lemma "A:* |- Lam a:A. a : ?T"
+ by (depth_solve rules)
+
+lemma "A:* B:* b:B |- Lam x:A. b : ?T"
+ by (depth_solve rules)
+
+lemma "A:* b:A |- (Lam a:A. a)^b: ?T"
+ by (depth_solve rules)
+
+lemma "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T"
+ by (depth_solve rules)
+
+lemma "A:* B:* |- Lam a:A. Lam b:B. a : ?T"
+ by (depth_solve rules)
+
+
+subsection {* Second-order types *}
+
+lemma (in L2) "|- Lam A:*. Lam a:A. a : ?T"
+ by (depth_solve rules)
+
+lemma (in L2) "A:* |- (Lam B:*.Lam b:B. b)^A : ?T"
+ by (depth_solve rules)
+
+lemma (in L2) "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T"
+ by (depth_solve rules)
+
+lemma (in L2) "|- Lam B:*.Lam a:(Pi A:*.A).a ^ ((Pi A:*.A)->B) ^ a: ?T"
+ by (depth_solve rules)
+
+
+subsection {* Weakly higher-order propositional logic *}
+
+lemma (in Lomega) "|- Lam A:*.A->A : ?T"
+ by (depth_solve rules)
+
+lemma (in Lomega) "B:* |- (Lam A:*.A->A) ^ B : ?T"
+ by (depth_solve rules)
+
+lemma (in Lomega) "B:* b:B |- (Lam y:B. b): ?T"
+ by (depth_solve rules)
+
+lemma (in Lomega) "A:* F:*->* |- F^(F^A): ?T"
+ by (depth_solve rules)
+
+lemma (in Lomega) "A:* |- Lam F:*->*.F^(F^A): ?T"
+ by (depth_solve rules)
+
+
+subsection {* LP *}
+
+lemma (in LP) "A:* |- A -> * : ?T"
+ by (depth_solve rules)
+
+lemma (in LP) "A:* P:A->* a:A |- P^a: ?T"
+ by (depth_solve rules)
+
+lemma (in LP) "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T"
+ by (depth_solve rules)
+
+lemma (in LP) "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T"
+ by (depth_solve rules)
+
+lemma (in LP) "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T"
+ by (depth_solve rules)
+
+lemma (in LP) "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T"
+ by (depth_solve rules)
+
+lemma (in LP) "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T"
+ by (depth_solve rules)
+
+lemma (in LP) "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 rules)
+
+
+subsection {* Omega-order types *}
+
+lemma (in L2) "A:* B:* |- Pi C:*.(A->B->C)->C : ?T"
+ by (depth_solve rules)
+
+lemma (in Lomega2) "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T"
+ by (depth_solve rules)
+
+lemma (in Lomega2) "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T"
+ by (depth_solve rules)
+
+lemma (in Lomega2) "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))"
+ apply (tactic {* strip_asms_tac (thms "rules") 1 *})
+ apply (rule lam_ss)
+ apply (depth_solve1 rules)
+ prefer 2
+ apply (depth_solve1 rules)
+ apply (rule lam_ss)
+ apply (depth_solve1 rules)
+ prefer 2
+ apply (depth_solve1 rules)
+ apply (rule lam_ss)
+ apply assumption
+ prefer 2
+ apply (depth_solve1 rules)
+ apply (erule pi_elim)
+ apply assumption
+ apply (erule pi_elim)
+ apply assumption
+ apply assumption
+ done
+
+
+subsection {* Second-order Predicate Logic *}
+
+lemma (in LP2) "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T"
+ by (depth_solve rules)
+
+lemma (in LP2) "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 rules)
+
+lemma (in LP2) "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"
+ -- {* Antisymmetry implies irreflexivity: *}
+ apply (tactic {* strip_asms_tac (thms "rules") 1 *})
+ apply (rule lam_ss)
+ apply (depth_solve1 rules)
+ prefer 2
+ apply (depth_solve1 rules)
+ apply (rule lam_ss)
+ apply assumption
+ prefer 2
+ apply (depth_solve1 rules)
+ apply (rule lam_ss)
+ apply (depth_solve1 rules)
+ prefer 2
+ apply (depth_solve1 rules)
+ apply (erule pi_elim, assumption, assumption?)+
+ done
+
+
+subsection {* LPomega *}
+
+lemma (in LPomega) "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T"
+ by (depth_solve rules)
+
+lemma (in LPomega) "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T"
+ by (depth_solve rules)
+
+
+subsection {* Constructions *}
+
+lemma (in CC) "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T"
+ by (depth_solve rules)
+
+lemma (in CC) "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T"
+ by (depth_solve rules)
+
+lemma (in CC) "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a"
+ apply (tactic {* strip_asms_tac (thms "rules") 1 *})
+ apply (rule lam_ss)
+ apply (depth_solve1 rules)
+ prefer 2
+ apply (depth_solve1 rules)
+ apply (erule pi_elim, assumption, assumption)
+ done
+
+
+subsection {* Some random examples *}
+
+lemma (in LP2) "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 rules)
+
+lemma (in CC) "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 rules)
+
+lemma (in LP2)
+ "A:* a:A b:A |- ?p: (Pi P:A->*.P^a->P^b) -> (Pi P:A->*.P^b->P^a)"
+ -- {* Symmetry of Leibnitz equality *}
+ apply (tactic {* strip_asms_tac (thms "rules") 1 *})
+ apply (rule lam_ss)
+ apply (depth_solve1 rules)
+ prefer 2
+ apply (depth_solve1 rules)
+ apply (erule_tac a = "Lam x:A. Pi Q:A->*.Q^x->Q^a" in pi_elim)
+ apply (depth_solve1 rules)
+ apply (unfold beta)
+ apply (erule imp_elim)
+ apply (rule lam_bs)
+ apply (depth_solve1 rules)
+ prefer 2
+ apply (depth_solve1 rules)
+ apply (rule lam_ss)
+ apply (depth_solve1 rules)
+ prefer 2
+ apply (depth_solve1 rules)
+ apply assumption
+ apply assumption
+ done
+
+end