# HG changeset patch # User wenzelm # Date 1125776630 -7200 # Node ID e352f65d58935b377706fb84b98f74190e01db04 # Parent 84fcead1f20b2871d408f23af6b04955294770d1 converted to Isar theory format; diff -r 84fcead1f20b -r e352f65d5893 src/Cube/Cube.thy --- 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" ("(_/ \ _)") + box :: "term" ("\") + Lam :: "[idt, term, term] => term" ("(3\ _:_./ _)" [0, 0, 0] 10) + Pi :: "[idt, term, term] => term" ("(3\ _:_./ _)" [0, 0] 10) + arrow :: "[term, term] => term" (infixr "\" 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 diff -r 84fcead1f20b -r e352f65d5893 src/Cube/IsaMakefile --- 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 diff -r 84fcead1f20b -r e352f65d5893 src/Cube/ROOT.ML --- 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; diff -r 84fcead1f20b -r e352f65d5893 src/Cube/ex/ex.thy --- 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