# HG changeset patch # User wenzelm # Date 1319294674 -7200 # Node ID 87950f7520996eb718dcaa3b9e3c46af2cb5bb27 # Parent 9d97bd3c086abfeb06cf1c6aa80c139aa2e0f8e9 modernized specifications; diff -r 9d97bd3c086a -r 87950f752099 src/Cube/Cube.thy --- a/src/Cube/Cube.thy Fri Oct 21 22:44:55 2011 +0200 +++ b/src/Cube/Cube.thy Sat Oct 22 16:44:34 2011 +0200 @@ -14,40 +14,46 @@ typedecl "context" typedecl typing -nonterminal context' and typing' +axiomatization + Abs :: "[term, term => term] => term" and + Prod :: "[term, term => term] => term" and + Trueprop :: "[context, typing] => prop" and + MT_context :: "context" and + Context :: "[typing, context] => context" and + star :: "term" ("*") and + box :: "term" ("[]") and + app :: "[term, term] => term" (infixl "^" 20) and + Has_type :: "[term, term] => 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" +notation (xsymbols) + box ("\") + +nonterminal context' and typing' syntax - "\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ |- _)") - "_Trueprop1" :: "typing' => prop" ("(_)") - "" :: "id => context'" ("_") - "" :: "var => context'" ("_") - "\<^const>Cube.MT_context" :: "context'" ("") - "\<^const>Cube.Context" :: "[typing', context'] => context'" ("_ _") - "\<^const>Cube.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) + "_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 + "_Trueprop(G, t)" == "CONST Trueprop(G, t)" ("prop") "x:X" == ("prop") "|- x:X" + "_MT_context" == "CONST MT_context" + "_Context" == "CONST Context" + "_Has_type" == "CONST Has_type" "Lam x:A. B" == "CONST Abs(A, %x. B)" "Pi x:A. B" => "CONST Prod(A, %x. B)" "A -> B" => "CONST Prod(A, %_. B)" syntax (xsymbols) - "\<^const>Cube.Trueprop" :: "[context', typing'] => prop" ("(_/ \ _)") - "\<^const>Cube.box" :: "term" ("\") + "_Trueprop" :: "[context', typing'] => prop" ("(_/ \ _)") "_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) @@ -57,20 +63,20 @@ Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] *} -axioms - s_b: "*: []" +axiomatization where + s_b: "*: []" and - 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" + strip_s: "[| A:*; a:A ==> G |- x:X |] ==> a:A G |- x:X" and + strip_b: "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X" and - app: "[| F:Prod(A, B); C:A |] ==> F^C: B(C)" + app: "[| F:Prod(A, B); C:A |] ==> F^C: B(C)" and - pi_ss: "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*" + pi_ss: "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*" and - lam_ss: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] - ==> Abs(A, f) : Prod(A, B)" + lam_ss: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] + ==> Abs(A, f) : Prod(A, B)" and - beta: "Abs(A, f)^a == f(a)" + beta: "Abs(A, f)^a == f(a)" lemmas simple = s_b strip_s strip_b app lam_ss pi_ss lemmas rules = simple @@ -105,27 +111,42 @@ 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)" +begin -lemmas (in LP) rules = simple lam_sb pi_sb +lemmas rules = simple lam_sb pi_sb + +end locale LP2 = LP + L2 +begin -lemmas (in LP2) rules = simple lam_bs pi_bs lam_sb pi_sb +lemmas rules = simple lam_bs pi_bs lam_sb pi_sb + +end locale Lomega2 = L2 + Lomega +begin -lemmas (in Lomega2) rules = simple lam_bs pi_bs lam_bb pi_bb +lemmas rules = simple lam_bs pi_bs lam_bb pi_bb + +end locale LPomega = LP + Lomega +begin -lemmas (in LPomega) rules = simple lam_bb pi_bb lam_sb pi_sb +lemmas rules = simple lam_bb pi_bb lam_sb pi_sb + +end locale CC = L2 + LP + Lomega +begin -lemmas (in CC) rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb +lemmas rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb end + +end diff -r 9d97bd3c086a -r 87950f752099 src/Cube/ROOT.ML --- a/src/Cube/ROOT.ML Fri Oct 21 22:44:55 2011 +0200 +++ b/src/Cube/ROOT.ML Sat Oct 22 16:44:34 2011 +0200 @@ -5,4 +5,4 @@ The Lambda-Cube a la Barendregt. *) -use_thys ["Cube", "Example"]; +use_thys ["Example"];