# HG changeset patch # User wenzelm # Date 1126904489 -7200 # Node ID 5b5feca0344a34a9ec862daa7d562d14c7c12eda # Parent df77edc4f5d0c83dc319559fb9f2a3cce7f7ac56 converted to Isar theory format; diff -r df77edc4f5d0 -r 5b5feca0344a src/CTT/Arith.ML --- a/src/CTT/Arith.ML Fri Sep 16 21:02:15 2005 +0200 +++ b/src/CTT/Arith.ML Fri Sep 16 23:01:29 2005 +0200 @@ -1,4 +1,4 @@ -(* Title: CTT/Arith +(* Title: CTT/Arith.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge @@ -31,7 +31,7 @@ Goalw arith_defs "[| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"; by (rew_tac []) ; -qed "addC_succ"; +qed "addC_succ"; (** Multiplication *) @@ -144,7 +144,7 @@ (*Commutative law for addition. Can be proved using three inductions. - Must simplify after first induction! Orientation of rewrites is delicate*) + Must simplify after first induction! Orientation of rewrites is delicate*) Goal "[| a:N; b:N |] ==> a #+ b = b #+ a : N"; by (NE_tac "a" 1); by (hyp_arith_rew_tac []); @@ -182,7 +182,7 @@ by (hyp_arith_rew_tac [add_assoc RS sym_elem]); by (REPEAT (assume_tac 1 ORELSE resolve_tac ([add_commute,mult_typingL,add_typingL]@ intrL_rls@ - [refl_elem]) 1)) ; + [refl_elem]) 1)) ; qed "mult_succ_right"; (*Commutative law for multiplication*) @@ -227,18 +227,18 @@ Goal "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"; by (NE_tac "b" 1); (*strip one "universal quantifier" but not the "implication"*) -by (resolve_tac intr_rls 3); +by (resolve_tac intr_rls 3); (*case analysis on x in (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *) -by (NE_tac "x" 4 THEN assume_tac 4); +by (NE_tac "x" 4 THEN assume_tac 4); (*Prepare for simplification of types -- the antecedent succ(u)<=x *) by (rtac replace_type 5); by (rtac replace_type 4); -by (arith_rew_tac []); +by (arith_rew_tac []); (*Solves first 0 goal, simplifies others. Two sugbgoals remain. Both follow by rewriting, (2) using quantified induction hyp*) by (intr_tac[]); (*strips remaining PRODs*) -by (hyp_arith_rew_tac [add_0_right]); +by (hyp_arith_rew_tac [add_0_right]); by (assume_tac 1); qed "add_diff_inverse_lemma"; @@ -319,7 +319,7 @@ by (typechk_tac [diff_typing]); qed "absdiff_eq0_lem"; -(*if a |-| b = 0 then a = b +(*if a |-| b = 0 then a = b proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*) Goal "[| a |-| b = 0 : N; a:N; b:N |] ==> a = b : N"; by (rtac EqE 1); @@ -340,11 +340,11 @@ Goalw [mod_def] "[| a:N; b:N |] ==> a mod b : N"; by (typechk_tac [absdiff_typing]) ; qed "mod_typing"; - + Goalw [mod_def] "[| a=c:N; b=d:N |] ==> a mod b = c mod d : N"; by (equal_tac [absdiff_typingL]) ; qed "mod_typingL"; - + (*computation for mod : 0 and successor cases*) @@ -352,7 +352,7 @@ by (rew_tac [absdiff_typing]) ; qed "modC0"; -Goalw [mod_def] +Goalw [mod_def] "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"; by (rew_tac [absdiff_typing]) ; qed "modC_succ"; @@ -377,7 +377,7 @@ by (rew_tac [mod_typing, absdiff_typing]) ; qed "divC0"; -Goalw [div_def] +Goalw [div_def] "[| a:N; b:N |] ==> succ(a) div b = \ \ rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"; by (rew_tac [mod_typing]) ; @@ -406,19 +406,17 @@ (*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *) Goal "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N"; by (NE_tac "a" 1); -by (arith_rew_tac (div_typing_rls@[modC0,modC_succ,divC0,divC_succ2])); +by (arith_rew_tac (div_typing_rls@[modC0,modC_succ,divC0,divC_succ2])); by (rtac EqE 1); (*case analysis on succ(u mod b)|-|b *) -by (res_inst_tac [("a1", "succ(u mod b) |-| b")] +by (res_inst_tac [("a1", "succ(u mod b) |-| b")] (iszero_decidable RS PlusE) 1); by (etac SumE 3); by (hyp_arith_rew_tac (div_typing_rls @ - [modC0,modC_succ, divC0, divC_succ2])); + [modC0,modC_succ, divC0, divC_succ2])); (*Replace one occurence of b by succ(u mod b). Clumsy!*) by (resolve_tac [ add_typingL RS trans_elem ] 1); by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1); by (rtac refl_elem 3); -by (hyp_arith_rew_tac (div_typing_rls)); +by (hyp_arith_rew_tac (div_typing_rls)); qed "mod_div_equality"; - -writeln"Reached end of file."; diff -r df77edc4f5d0 -r 5b5feca0344a src/CTT/Arith.thy --- a/src/CTT/Arith.thy Fri Sep 16 21:02:15 2005 +0200 +++ b/src/CTT/Arith.thy Fri Sep 16 23:01:29 2005 +0200 @@ -1,30 +1,42 @@ -(* Title: CTT/arith +(* Title: CTT/Arith.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge - -Arithmetic operators and their definitions - -Proves about elementary arithmetic: addition, multiplication, etc. -Tests definitions and simplifier. *) -Arith = CTT + +header {* Arithmetic operators and their definitions *} + +theory Arith +imports Bool +begin -consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65) - "#*",div,mod :: "[i,i]=>i" (infixr 70) +text {* + Proves about elementary arithmetic: addition, multiplication, etc. + Tests definitions and simplifier. +*} + +consts + "#+" :: "[i,i]=>i" (infixr 65) + "-" :: "[i,i]=>i" (infixr 65) + "|-|" :: "[i,i]=>i" (infixr 65) + "#*" :: "[i,i]=>i" (infixr 70) + div :: "[i,i]=>i" (infixr 70) + mod :: "[i,i]=>i" (infixr 70) syntax (xsymbols) - "op #*" :: [i, i] => i (infixr "#\\" 70) + "op #*" :: "[i, i] => i" (infixr "#\" 70) syntax (HTML output) - "op #*" :: [i, i] => i (infixr "#\\" 70) + "op #*" :: "[i, i] => i" (infixr "#\" 70) -rules - add_def "a#+b == rec(a, b, %u v. succ(v))" - diff_def "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))" - absdiff_def "a|-|b == (a-b) #+ (b-a)" - mult_def "a#*b == rec(a, 0, %u v. b #+ v)" - mod_def "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))" - div_def "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" +defs + add_def: "a#+b == rec(a, b, %u v. succ(v))" + diff_def: "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))" + absdiff_def: "a|-|b == (a-b) #+ (b-a)" + mult_def: "a#*b == rec(a, 0, %u v. b #+ v)" + mod_def: "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))" + div_def: "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" + +ML {* use_legacy_bindings (the_context ()) *} + end diff -r df77edc4f5d0 -r 5b5feca0344a src/CTT/Bool.ML --- a/src/CTT/Bool.ML Fri Sep 16 21:02:15 2005 +0200 +++ b/src/CTT/Bool.ML Fri Sep 16 23:01:29 2005 +0200 @@ -2,8 +2,6 @@ ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge - -The two-element type (booleans and conditionals) *) val bool_defs = [Bool_def,true_def,false_def,cond_def]; @@ -27,7 +25,7 @@ qed "boolI_false"; (*elimination rule: typing of cond*) -Goalw bool_defs +Goalw bool_defs "[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)"; by (typechk_tac []); by (ALLGOALS (etac TE)); @@ -43,7 +41,7 @@ (*computation rules for true, false*) -Goalw bool_defs +Goalw bool_defs "[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)"; by (resolve_tac comp_rls 1); by (typechk_tac []); @@ -58,6 +56,3 @@ by (ALLGOALS (etac TE)); by (typechk_tac []) ; qed "boolC_false"; - -writeln"Reached end of file."; - diff -r df77edc4f5d0 -r 5b5feca0344a src/CTT/Bool.thy --- a/src/CTT/Bool.thy Fri Sep 16 21:02:15 2005 +0200 +++ b/src/CTT/Bool.thy Fri Sep 16 23:01:29 2005 +0200 @@ -2,18 +2,26 @@ ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge - -The two-element type (booleans and conditionals) *) -Bool = CTT + +header {* The two-element type (booleans and conditionals) *} + +theory Bool +imports CTT +uses "~~/src/Provers/typedsimp.ML" "rew.ML" +begin -consts Bool :: "t" - true,false :: "i" - cond :: "[i,i,i]=>i" -rules - Bool_def "Bool == T+T" - true_def "true == inl(tt)" - false_def "false == inr(tt)" - cond_def "cond(a,b,c) == when(a, %u. b, %u. c)" +consts + Bool :: "t" + true :: "i" + false :: "i" + cond :: "[i,i,i]=>i" +defs + Bool_def: "Bool == T+T" + true_def: "true == inl(tt)" + false_def: "false == inr(tt)" + cond_def: "cond(a,b,c) == when(a, %u. b, %u. c)" + +ML {* use_legacy_bindings (the_context ()) *} + end diff -r df77edc4f5d0 -r 5b5feca0344a src/CTT/CTT.ML --- a/src/CTT/CTT.ML Fri Sep 16 21:02:15 2005 +0200 +++ b/src/CTT/CTT.ML Fri Sep 16 23:01:29 2005 +0200 @@ -10,7 +10,7 @@ val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF] and formL_rls = [ProdFL, SumFL, PlusFL, EqFL]; - + (*Introduction rules OMITTED: EqI, because its premise is an eqelem, not an elem*) val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI] @@ -42,7 +42,7 @@ val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL]; -(*Exploit p:Prod(A,B) to create the assumption z:B(a). +(*Exploit p:Prod(A,B) to create the assumption z:B(a). A more natural form of product elimination. *) val prems = Goal "[| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) \ \ |] ==> c(p`a): C(p`a)"; @@ -56,7 +56,7 @@ | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a)) | is_rigid_elem _ = false; -(*Try solving a:A or a=b:A by assumption provided a is rigid!*) +(*Try solving a:A or a=b:A by assumption provided a is rigid!*) val test_assume_tac = SUBGOAL(fn (prem,i) => if is_rigid_elem (Logic.strip_assums_concl prem) then assume_tac i else no_tac); @@ -81,7 +81,7 @@ in REPEAT_FIRST (ASSUME tac) end; -(*Solve a:A (a flexible, A rigid) by introduction rules. +(*Solve a:A (a flexible, A rigid) by introduction rules. Cannot use stringtrees (filt_resolve_tac) since goals like ?a:SUM(A,B) have a trivial head-string *) fun intr_tac thms = @@ -125,22 +125,22 @@ val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1)); (** Tactics that instantiate CTT-rules. - Vars in the given terms will be incremented! + Vars in the given terms will be incremented! The (rtac EqE i) lets them apply to equality judgements. **) -fun NE_tac (sp: string) i = +fun NE_tac (sp: string) i = TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i; -fun SumE_tac (sp: string) i = +fun SumE_tac (sp: string) i = TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i; -fun PlusE_tac (sp: string) i = +fun PlusE_tac (sp: string) i = TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i; (** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **) (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *) -fun add_mp_tac i = +fun add_mp_tac i = rtac subst_prodE i THEN assume_tac i THEN assume_tac i; (*Finds P-->Q and P in the assumptions, replaces implication by Q *) @@ -148,11 +148,11 @@ (*"safe" when regarded as predicate calculus rules*) val safe_brls = sort (make_ord lessb) - [ (true,FE), (true,asm_rl), + [ (true,FE), (true,asm_rl), (false,ProdI), (true,SumE), (true,PlusE) ]; val unsafe_brls = - [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), + [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), (true,subst_prodE) ]; (*0 subgoals vs 1 or more*) @@ -160,12 +160,12 @@ List.partition (apl(0,op=) o subgoals_of_brl) safe_brls; fun safestep_tac thms i = - form_tac ORELSE + form_tac ORELSE resolve_tac thms i ORELSE biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE DETERM (biresolve_tac safep_brls i); -fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i); +fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i); fun step_tac thms = safestep_tac thms ORELSE' biresolve_tac unsafe_brls; diff -r df77edc4f5d0 -r 5b5feca0344a src/CTT/CTT.thy --- a/src/CTT/CTT.thy Fri Sep 16 21:02:15 2005 +0200 +++ b/src/CTT/CTT.thy Fri Sep 16 23:01:29 2005 +0200 @@ -1,21 +1,23 @@ -(* Title: CTT/ctt.thy +(* Title: CTT/CTT.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -Constructive Type Theory *) -CTT = Pure + +header {* Constructive Type Theory *} -types - i - t - o +theory CTT +imports Pure +begin + +typedecl i +typedecl t +typedecl o consts (*Types*) - F,T :: "t" (*F is empty, T contains one element*) + F :: "t" + T :: "t" (*F is empty, T contains one element*) contr :: "i=>i" tt :: "i" (*Natural numbers*) @@ -23,11 +25,13 @@ succ :: "i=>i" rec :: "[i, i, [i,i]=>i] => i" (*Unions*) - inl,inr :: "i=>i" + inl :: "i=>i" + inr :: "i=>i" when :: "[i, i=>i, i=>i]=>i" (*General Sum and Binary Product*) Sum :: "[t, i=>t]=>t" - fst,snd :: "i=>i" + fst :: "i=>i" + snd :: "i=>i" split :: "[i, [i,i]=>i] =>i" (*General Product and Function Space*) Prod :: "[t, i=>t]=>t" @@ -64,24 +68,30 @@ "SUM x:A. B" => "Sum(A, %x. B)" "A * B" => "Sum(A, _K(B))" +print_translation {* + [("Prod", dependent_tr' ("@PROD", "@-->")), + ("Sum", dependent_tr' ("@SUM", "@*"))] +*} + + syntax (xsymbols) - "@-->" :: "[t,t]=>t" ("(_ \\/ _)" [31,30] 30) - "@*" :: "[t,t]=>t" ("(_ \\/ _)" [51,50] 50) - Elem :: "[i, t]=>prop" ("(_ /\\ _)" [10,10] 5) - Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \\/ _)" [10,10,10] 5) - "@SUM" :: "[idt,t,t] => t" ("(3\\ _\\_./ _)" 10) - "@PROD" :: "[idt,t,t] => t" ("(3\\ _\\_./ _)" 10) - "lam " :: "[idts, i] => i" ("(3\\\\_./ _)" 10) + "@-->" :: "[t,t]=>t" ("(_ \/ _)" [31,30] 30) + "@*" :: "[t,t]=>t" ("(_ \/ _)" [51,50] 50) + Elem :: "[i, t]=>prop" ("(_ /\ _)" [10,10] 5) + Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \/ _)" [10,10,10] 5) + "@SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) + "@PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) + "lam " :: "[idts, i] => i" ("(3\\_./ _)" 10) syntax (HTML output) - "@*" :: "[t,t]=>t" ("(_ \\/ _)" [51,50] 50) - Elem :: "[i, t]=>prop" ("(_ /\\ _)" [10,10] 5) - Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \\/ _)" [10,10,10] 5) - "@SUM" :: "[idt,t,t] => t" ("(3\\ _\\_./ _)" 10) - "@PROD" :: "[idt,t,t] => t" ("(3\\ _\\_./ _)" 10) - "lam " :: "[idts, i] => i" ("(3\\\\_./ _)" 10) + "@*" :: "[t,t]=>t" ("(_ \/ _)" [51,50] 50) + Elem :: "[i, t]=>prop" ("(_ /\ _)" [10,10] 5) + Eqelem :: "[i,i,t]=>prop" ("(2_ =/ _ \/ _)" [10,10,10] 5) + "@SUM" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) + "@PROD" :: "[idt,t,t] => t" ("(3\ _\_./ _)" 10) + "lam " :: "[idts, i] => i" ("(3\\_./ _)" 10) -rules +axioms (*Reduction: a weaker notion than equality; a hack for simplification. Reduce[a,b] means either that a=b:A for some A or else that "a" and "b" @@ -89,167 +99,167 @@ (*does not verify a:A! Sound because only trans_red uses a Reduce premise No new theorems can be proved about the standard judgements.*) - refl_red "Reduce[a,a]" - red_if_equal "a = b : A ==> Reduce[a,b]" - trans_red "[| a = b : A; Reduce[b,c] |] ==> a = c : A" + refl_red: "Reduce[a,a]" + red_if_equal: "a = b : A ==> Reduce[a,b]" + trans_red: "[| a = b : A; Reduce[b,c] |] ==> a = c : A" (*Reflexivity*) - refl_type "A type ==> A = A" - refl_elem "a : A ==> a = a : A" + refl_type: "A type ==> A = A" + refl_elem: "a : A ==> a = a : A" (*Symmetry*) - sym_type "A = B ==> B = A" - sym_elem "a = b : A ==> b = a : A" + sym_type: "A = B ==> B = A" + sym_elem: "a = b : A ==> b = a : A" (*Transitivity*) - trans_type "[| A = B; B = C |] ==> A = C" - trans_elem "[| a = b : A; b = c : A |] ==> a = c : A" + trans_type: "[| A = B; B = C |] ==> A = C" + trans_elem: "[| a = b : A; b = c : A |] ==> a = c : A" - equal_types "[| a : A; A = B |] ==> a : B" - equal_typesL "[| a = b : A; A = B |] ==> a = b : B" + equal_types: "[| a : A; A = B |] ==> a : B" + equal_typesL: "[| a = b : A; A = B |] ==> a = b : B" (*Substitution*) - subst_type "[| a : A; !!z. z:A ==> B(z) type |] ==> B(a) type" - subst_typeL "[| a = c : A; !!z. z:A ==> B(z) = D(z) |] ==> B(a) = D(c)" + subst_type: "[| a : A; !!z. z:A ==> B(z) type |] ==> B(a) type" + subst_typeL: "[| a = c : A; !!z. z:A ==> B(z) = D(z) |] ==> B(a) = D(c)" - subst_elem "[| a : A; !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)" - subst_elemL + subst_elem: "[| a : A; !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)" + subst_elemL: "[| a=c : A; !!z. z:A ==> b(z)=d(z) : B(z) |] ==> b(a)=d(c) : B(a)" (*The type N -- natural numbers*) - NF "N type" - NI0 "0 : N" - NI_succ "a : N ==> succ(a) : N" - NI_succL "a = b : N ==> succ(a) = succ(b) : N" + NF: "N type" + NI0: "0 : N" + NI_succ: "a : N ==> succ(a) : N" + NI_succL: "a = b : N ==> succ(a) = succ(b) : N" - NE - "[| p: N; a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] + NE: + "[| p: N; a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==> rec(p, a, %u v. b(u,v)) : C(p)" - NEL - "[| p = q : N; a = c : C(0); - !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] + NEL: + "[| p = q : N; a = c : C(0); + !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] ==> rec(p, a, %u v. b(u,v)) = rec(q,c,d) : C(p)" - NC0 - "[| a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] + NC0: + "[| a: C(0); !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==> rec(0, a, %u v. b(u,v)) = a : C(0)" - NC_succ - "[| p: N; a: C(0); - !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==> + NC_succ: + "[| p: N; a: C(0); + !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==> rec(succ(p), a, %u v. b(u,v)) = b(p, rec(p, a, %u v. b(u,v))) : C(succ(p))" (*The fourth Peano axiom. See page 91 of Martin-Lof's book*) - zero_ne_succ + zero_ne_succ: "[| a: N; 0 = succ(a) : N |] ==> 0: F" (*The Product of a family of types*) - ProdF "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type" + ProdF: "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type" - ProdFL - "[| A = C; !!x. x:A ==> B(x) = D(x) |] ==> + ProdFL: + "[| A = C; !!x. x:A ==> B(x) = D(x) |] ==> PROD x:A. B(x) = PROD x:C. D(x)" - ProdI + ProdI: "[| A type; !!x. x:A ==> b(x):B(x)|] ==> lam x. b(x) : PROD x:A. B(x)" - ProdIL - "[| A type; !!x. x:A ==> b(x) = c(x) : B(x)|] ==> + ProdIL: + "[| A type; !!x. x:A ==> b(x) = c(x) : B(x)|] ==> lam x. b(x) = lam x. c(x) : PROD x:A. B(x)" - ProdE "[| p : PROD x:A. B(x); a : A |] ==> p`a : B(a)" - ProdEL "[| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a)" + ProdE: "[| p : PROD x:A. B(x); a : A |] ==> p`a : B(a)" + ProdEL: "[| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a)" - ProdC - "[| a : A; !!x. x:A ==> b(x) : B(x)|] ==> + ProdC: + "[| a : A; !!x. x:A ==> b(x) : B(x)|] ==> (lam x. b(x)) ` a = b(a) : B(a)" - ProdC2 + ProdC2: "p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)" (*The Sum of a family of types*) - SumF "[| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type" - SumFL + SumF: "[| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type" + SumFL: "[| A = C; !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A. B(x) = SUM x:C. D(x)" - SumI "[| a : A; b : B(a) |] ==> : SUM x:A. B(x)" - SumIL "[| a=c:A; b=d:B(a) |] ==> = : SUM x:A. B(x)" + SumI: "[| a : A; b : B(a) |] ==> : SUM x:A. B(x)" + SumIL: "[| a=c:A; b=d:B(a) |] ==> = : SUM x:A. B(x)" - SumE - "[| p: SUM x:A. B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C() |] + SumE: + "[| p: SUM x:A. B(x); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C() |] ==> split(p, %x y. c(x,y)) : C(p)" - SumEL - "[| p=q : SUM x:A. B(x); - !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C()|] + SumEL: + "[| p=q : SUM x:A. B(x); + !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C()|] ==> split(p, %x y. c(x,y)) = split(q, % x y. d(x,y)) : C(p)" - SumC - "[| a: A; b: B(a); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C() |] + SumC: + "[| a: A; b: B(a); !!x y. [| x:A; y:B(x) |] ==> c(x,y): C() |] ==> split(, %x y. c(x,y)) = c(a,b) : C()" - fst_def "fst(a) == split(a, %x y. x)" - snd_def "snd(a) == split(a, %x y. y)" + fst_def: "fst(a) == split(a, %x y. x)" + snd_def: "snd(a) == split(a, %x y. y)" (*The sum of two types*) - PlusF "[| A type; B type |] ==> A+B type" - PlusFL "[| A = C; B = D |] ==> A+B = C+D" + PlusF: "[| A type; B type |] ==> A+B type" + PlusFL: "[| A = C; B = D |] ==> A+B = C+D" - PlusI_inl "[| a : A; B type |] ==> inl(a) : A+B" - PlusI_inlL "[| a = c : A; B type |] ==> inl(a) = inl(c) : A+B" + PlusI_inl: "[| a : A; B type |] ==> inl(a) : A+B" + PlusI_inlL: "[| a = c : A; B type |] ==> inl(a) = inl(c) : A+B" - PlusI_inr "[| A type; b : B |] ==> inr(b) : A+B" - PlusI_inrL "[| A type; b = d : B |] ==> inr(b) = inr(d) : A+B" + PlusI_inr: "[| A type; b : B |] ==> inr(b) : A+B" + PlusI_inrL: "[| A type; b = d : B |] ==> inr(b) = inr(d) : A+B" - PlusE - "[| p: A+B; !!x. x:A ==> c(x): C(inl(x)); - !!y. y:B ==> d(y): C(inr(y)) |] + PlusE: + "[| p: A+B; !!x. x:A ==> c(x): C(inl(x)); + !!y. y:B ==> d(y): C(inr(y)) |] ==> when(p, %x. c(x), %y. d(y)) : C(p)" - PlusEL - "[| p = q : A+B; !!x. x: A ==> c(x) = e(x) : C(inl(x)); - !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] + PlusEL: + "[| p = q : A+B; !!x. x: A ==> c(x) = e(x) : C(inl(x)); + !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] ==> when(p, %x. c(x), %y. d(y)) = when(q, %x. e(x), %y. f(y)) : C(p)" - PlusC_inl - "[| a: A; !!x. x:A ==> c(x): C(inl(x)); - !!y. y:B ==> d(y): C(inr(y)) |] + PlusC_inl: + "[| a: A; !!x. x:A ==> c(x): C(inl(x)); + !!y. y:B ==> d(y): C(inr(y)) |] ==> when(inl(a), %x. c(x), %y. d(y)) = c(a) : C(inl(a))" - PlusC_inr - "[| b: B; !!x. x:A ==> c(x): C(inl(x)); - !!y. y:B ==> d(y): C(inr(y)) |] + PlusC_inr: + "[| b: B; !!x. x:A ==> c(x): C(inl(x)); + !!y. y:B ==> d(y): C(inr(y)) |] ==> when(inr(b), %x. c(x), %y. d(y)) = d(b) : C(inr(b))" (*The type Eq*) - EqF "[| A type; a : A; b : A |] ==> Eq(A,a,b) type" - EqFL "[| A=B; a=c: A; b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)" - EqI "a = b : A ==> eq : Eq(A,a,b)" - EqE "p : Eq(A,a,b) ==> a = b : A" + EqF: "[| A type; a : A; b : A |] ==> Eq(A,a,b) type" + EqFL: "[| A=B; a=c: A; b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)" + EqI: "a = b : A ==> eq : Eq(A,a,b)" + EqE: "p : Eq(A,a,b) ==> a = b : A" (*By equality of types, can prove C(p) from C(eq), an elimination rule*) - EqC "p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)" + EqC: "p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)" (*The type F*) - FF "F type" - FE "[| p: F; C type |] ==> contr(p) : C" - FEL "[| p = q : F; C type |] ==> contr(p) = contr(q) : C" + FF: "F type" + FE: "[| p: F; C type |] ==> contr(p) : C" + FEL: "[| p = q : F; C type |] ==> contr(p) = contr(q) : C" (*The type T Martin-Lof's book (page 68) discusses elimination and computation. @@ -257,17 +267,12 @@ but with an extra premise C(x) type x:T. Also computation can be derived from elimination. *) - TF "T type" - TI "tt : T" - TE "[| p : T; c : C(tt) |] ==> c : C(p)" - TEL "[| p = q : T; c = d : C(tt) |] ==> c = d : C(p)" - TC "p : T ==> p = tt : T" -end + TF: "T type" + TI: "tt : T" + TE: "[| p : T; c : C(tt) |] ==> c : C(p)" + TEL: "[| p = q : T; c = d : C(tt) |] ==> c = d : C(p)" + TC: "p : T ==> p = tt : T" - -ML +ML {* use_legacy_bindings (the_context ()) *} -val print_translation = - [("Prod", dependent_tr' ("@PROD", "@-->")), - ("Sum", dependent_tr' ("@SUM", "@*"))]; - +end diff -r df77edc4f5d0 -r 5b5feca0344a src/CTT/Main.thy --- a/src/CTT/Main.thy Fri Sep 16 21:02:15 2005 +0200 +++ b/src/CTT/Main.thy Fri Sep 16 23:01:29 2005 +0200 @@ -1,6 +1,9 @@ -(*theory Main includes everything*) +(* $Id$ *) + +header {* Main includes everything *} -theory Main imports CTT Arith Bool begin - +theory Main +imports CTT Arith Bool +begin end diff -r df77edc4f5d0 -r 5b5feca0344a src/CTT/ROOT.ML --- a/src/CTT/ROOT.ML Fri Sep 16 21:02:15 2005 +0200 +++ b/src/CTT/ROOT.ML Fri Sep 16 23:01:29 2005 +0200 @@ -10,13 +10,6 @@ val banner = "Constructive Type Theory"; writeln banner; -print_depth 1; - -use_thy "CTT"; -use "~~/src/Provers/typedsimp.ML"; -use "rew.ML"; use_thy "Main"; -print_depth 8; - Goal "tt : T"; (*leave subgoal package empty*) diff -r df77edc4f5d0 -r 5b5feca0344a src/CTT/ex/synth.ML --- a/src/CTT/ex/synth.ML Fri Sep 16 21:02:15 2005 +0200 +++ b/src/CTT/ex/synth.ML Fri Sep 16 23:01:29 2005 +0200 @@ -6,7 +6,7 @@ writeln"Synthesis examples, using a crude form of narrowing"; -context Arith.thy; +context (theory "Arith"); writeln"discovery of predecessor function"; Goal