converted to Isar theory format;
authorwenzelm
Fri Sep 16 23:01:29 2005 +0200 (2005-09-16)
changeset 174415b5feca0344a
parent 17440 df77edc4f5d0
child 17442 c0f0b92c198c
converted to Isar theory format;
src/CTT/Arith.ML
src/CTT/Arith.thy
src/CTT/Bool.ML
src/CTT/Bool.thy
src/CTT/CTT.ML
src/CTT/CTT.thy
src/CTT/Main.thy
src/CTT/ROOT.ML
src/CTT/ex/synth.ML
     1.1 --- a/src/CTT/Arith.ML	Fri Sep 16 21:02:15 2005 +0200
     1.2 +++ b/src/CTT/Arith.ML	Fri Sep 16 23:01:29 2005 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      CTT/Arith
     1.5 +(*  Title:      CTT/Arith.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1991  University of Cambridge
     1.9 @@ -31,7 +31,7 @@
    1.10  
    1.11  Goalw arith_defs "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N";
    1.12  by (rew_tac []) ;
    1.13 -qed "addC_succ"; 
    1.14 +qed "addC_succ";
    1.15  
    1.16  
    1.17  (** Multiplication *)
    1.18 @@ -144,7 +144,7 @@
    1.19  
    1.20  
    1.21  (*Commutative law for addition.  Can be proved using three inductions.
    1.22 -  Must simplify after first induction!  Orientation of rewrites is delicate*)  
    1.23 +  Must simplify after first induction!  Orientation of rewrites is delicate*)
    1.24  Goal "[| a:N;  b:N |] ==> a #+ b = b #+ a : N";
    1.25  by (NE_tac "a" 1);
    1.26  by (hyp_arith_rew_tac []);
    1.27 @@ -182,7 +182,7 @@
    1.28  by (hyp_arith_rew_tac [add_assoc RS sym_elem]);
    1.29  by (REPEAT (assume_tac 1
    1.30       ORELSE resolve_tac ([add_commute,mult_typingL,add_typingL]@ intrL_rls@
    1.31 -			 [refl_elem])   1)) ;
    1.32 +                         [refl_elem])   1)) ;
    1.33  qed "mult_succ_right";
    1.34  
    1.35  (*Commutative law for multiplication*)
    1.36 @@ -227,18 +227,18 @@
    1.37  Goal "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)";
    1.38  by (NE_tac "b" 1);
    1.39  (*strip one "universal quantifier" but not the "implication"*)
    1.40 -by (resolve_tac intr_rls 3);  
    1.41 +by (resolve_tac intr_rls 3);
    1.42  (*case analysis on x in
    1.43      (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
    1.44 -by (NE_tac "x" 4 THEN assume_tac 4); 
    1.45 +by (NE_tac "x" 4 THEN assume_tac 4);
    1.46  (*Prepare for simplification of types -- the antecedent succ(u)<=x *)
    1.47  by (rtac replace_type 5);
    1.48  by (rtac replace_type 4);
    1.49 -by (arith_rew_tac []); 
    1.50 +by (arith_rew_tac []);
    1.51  (*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
    1.52    Both follow by rewriting, (2) using quantified induction hyp*)
    1.53  by (intr_tac[]);  (*strips remaining PRODs*)
    1.54 -by (hyp_arith_rew_tac [add_0_right]);  
    1.55 +by (hyp_arith_rew_tac [add_0_right]);
    1.56  by (assume_tac 1);
    1.57  qed "add_diff_inverse_lemma";
    1.58  
    1.59 @@ -319,7 +319,7 @@
    1.60  by (typechk_tac [diff_typing]);
    1.61  qed "absdiff_eq0_lem";
    1.62  
    1.63 -(*if  a |-| b = 0  then  a = b  
    1.64 +(*if  a |-| b = 0  then  a = b
    1.65    proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
    1.66  Goal "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N";
    1.67  by (rtac EqE 1);
    1.68 @@ -340,11 +340,11 @@
    1.69  Goalw [mod_def] "[| a:N;  b:N |] ==> a mod b : N";
    1.70  by (typechk_tac [absdiff_typing]) ;
    1.71  qed "mod_typing";
    1.72 - 
    1.73 +
    1.74  Goalw [mod_def] "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N";
    1.75  by (equal_tac [absdiff_typingL]) ;
    1.76  qed "mod_typingL";
    1.77 - 
    1.78 +
    1.79  
    1.80  (*computation for  mod : 0 and successor cases*)
    1.81  
    1.82 @@ -352,7 +352,7 @@
    1.83  by (rew_tac [absdiff_typing]) ;
    1.84  qed "modC0";
    1.85  
    1.86 -Goalw [mod_def]   
    1.87 +Goalw [mod_def]
    1.88  "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N";
    1.89  by (rew_tac [absdiff_typing]) ;
    1.90  qed "modC_succ";
    1.91 @@ -377,7 +377,7 @@
    1.92  by (rew_tac [mod_typing, absdiff_typing]) ;
    1.93  qed "divC0";
    1.94  
    1.95 -Goalw [div_def] 
    1.96 +Goalw [div_def]
    1.97   "[| a:N;  b:N |] ==> succ(a) div b = \
    1.98  \    rec(succ(a) mod b, succ(a div b), %x y. a div b) : N";
    1.99  by (rew_tac [mod_typing]) ;
   1.100 @@ -406,19 +406,17 @@
   1.101  (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
   1.102  Goal "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N";
   1.103  by (NE_tac "a" 1);
   1.104 -by (arith_rew_tac (div_typing_rls@[modC0,modC_succ,divC0,divC_succ2])); 
   1.105 +by (arith_rew_tac (div_typing_rls@[modC0,modC_succ,divC0,divC_succ2]));
   1.106  by (rtac EqE 1);
   1.107  (*case analysis on   succ(u mod b)|-|b  *)
   1.108 -by (res_inst_tac [("a1", "succ(u mod b) |-| b")] 
   1.109 +by (res_inst_tac [("a1", "succ(u mod b) |-| b")]
   1.110                   (iszero_decidable RS PlusE) 1);
   1.111  by (etac SumE 3);
   1.112  by (hyp_arith_rew_tac (div_typing_rls @
   1.113 -        [modC0,modC_succ, divC0, divC_succ2])); 
   1.114 +        [modC0,modC_succ, divC0, divC_succ2]));
   1.115  (*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
   1.116  by (resolve_tac [ add_typingL RS trans_elem ] 1);
   1.117  by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);
   1.118  by (rtac refl_elem 3);
   1.119 -by (hyp_arith_rew_tac (div_typing_rls)); 
   1.120 +by (hyp_arith_rew_tac (div_typing_rls));
   1.121  qed "mod_div_equality";
   1.122 -
   1.123 -writeln"Reached end of file.";
     2.1 --- a/src/CTT/Arith.thy	Fri Sep 16 21:02:15 2005 +0200
     2.2 +++ b/src/CTT/Arith.thy	Fri Sep 16 23:01:29 2005 +0200
     2.3 @@ -1,30 +1,42 @@
     2.4 -(*  Title:      CTT/arith
     2.5 +(*  Title:      CTT/Arith.thy
     2.6      ID:         $Id$
     2.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8      Copyright   1991  University of Cambridge
     2.9 -
    2.10 -Arithmetic operators and their definitions
    2.11 -
    2.12 -Proves about elementary arithmetic: addition, multiplication, etc.
    2.13 -Tests definitions and simplifier.
    2.14  *)
    2.15  
    2.16 -Arith = CTT +
    2.17 +header {* Arithmetic operators and their definitions *}
    2.18 +
    2.19 +theory Arith
    2.20 +imports Bool
    2.21 +begin
    2.22  
    2.23 -consts "#+","-","|-|"   :: "[i,i]=>i"   (infixr 65)
    2.24 -       "#*",div,mod     :: "[i,i]=>i"   (infixr 70)
    2.25 +text {*
    2.26 +  Proves about elementary arithmetic: addition, multiplication, etc.
    2.27 +  Tests definitions and simplifier.
    2.28 +*}
    2.29 +
    2.30 +consts
    2.31 +  "#+"  :: "[i,i]=>i"   (infixr 65)
    2.32 +  "-"   :: "[i,i]=>i"   (infixr 65)
    2.33 +  "|-|" :: "[i,i]=>i"   (infixr 65)
    2.34 +  "#*"  :: "[i,i]=>i"   (infixr 70)
    2.35 +  div   :: "[i,i]=>i"   (infixr 70)
    2.36 +  mod   :: "[i,i]=>i"   (infixr 70)
    2.37  
    2.38  syntax (xsymbols)
    2.39 -  "op #*"      :: [i, i] => i   (infixr "#\\<times>" 70)
    2.40 +  "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)
    2.41  
    2.42  syntax (HTML output)
    2.43 -  "op #*"      :: [i, i] => i   (infixr "#\\<times>" 70)
    2.44 +  "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)
    2.45  
    2.46 -rules
    2.47 -  add_def     "a#+b == rec(a, b, %u v. succ(v))"  
    2.48 -  diff_def    "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"  
    2.49 -  absdiff_def "a|-|b == (a-b) #+ (b-a)"  
    2.50 -  mult_def    "a#*b == rec(a, 0, %u v. b #+ v)"  
    2.51 -  mod_def     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
    2.52 -  div_def     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
    2.53 +defs
    2.54 +  add_def:     "a#+b == rec(a, b, %u v. succ(v))"
    2.55 +  diff_def:    "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
    2.56 +  absdiff_def: "a|-|b == (a-b) #+ (b-a)"
    2.57 +  mult_def:    "a#*b == rec(a, 0, %u v. b #+ v)"
    2.58 +  mod_def:     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
    2.59 +  div_def:     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
    2.60 +
    2.61 +ML {* use_legacy_bindings (the_context ()) *}
    2.62 +
    2.63  end
     3.1 --- a/src/CTT/Bool.ML	Fri Sep 16 21:02:15 2005 +0200
     3.2 +++ b/src/CTT/Bool.ML	Fri Sep 16 23:01:29 2005 +0200
     3.3 @@ -2,8 +2,6 @@
     3.4      ID:         $Id$
     3.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.6      Copyright   1991  University of Cambridge
     3.7 -
     3.8 -The two-element type (booleans and conditionals)
     3.9  *)
    3.10  
    3.11  val bool_defs = [Bool_def,true_def,false_def,cond_def];
    3.12 @@ -27,7 +25,7 @@
    3.13  qed "boolI_false";
    3.14  
    3.15  (*elimination rule: typing of cond*)
    3.16 -Goalw bool_defs 
    3.17 +Goalw bool_defs
    3.18      "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)";
    3.19  by (typechk_tac []);
    3.20  by (ALLGOALS (etac TE));
    3.21 @@ -43,7 +41,7 @@
    3.22  
    3.23  (*computation rules for true, false*)
    3.24  
    3.25 -Goalw bool_defs 
    3.26 +Goalw bool_defs
    3.27      "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)";
    3.28  by (resolve_tac comp_rls 1);
    3.29  by (typechk_tac []);
    3.30 @@ -58,6 +56,3 @@
    3.31  by (ALLGOALS (etac TE));
    3.32  by (typechk_tac []) ;
    3.33  qed "boolC_false";
    3.34 -
    3.35 -writeln"Reached end of file.";
    3.36 -
     4.1 --- a/src/CTT/Bool.thy	Fri Sep 16 21:02:15 2005 +0200
     4.2 +++ b/src/CTT/Bool.thy	Fri Sep 16 23:01:29 2005 +0200
     4.3 @@ -2,18 +2,26 @@
     4.4      ID:         $Id$
     4.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.6      Copyright   1991  University of Cambridge
     4.7 -
     4.8 -The two-element type (booleans and conditionals)
     4.9  *)
    4.10  
    4.11 -Bool = CTT +
    4.12 +header {* The two-element type (booleans and conditionals) *}
    4.13 +
    4.14 +theory Bool
    4.15 +imports CTT
    4.16 +uses "~~/src/Provers/typedsimp.ML" "rew.ML"
    4.17 +begin
    4.18  
    4.19 -consts Bool             :: "t"
    4.20 -       true,false       :: "i"
    4.21 -       cond             :: "[i,i,i]=>i"
    4.22 -rules
    4.23 -  Bool_def      "Bool == T+T"
    4.24 -  true_def      "true == inl(tt)"
    4.25 -  false_def     "false == inr(tt)"
    4.26 -  cond_def      "cond(a,b,c) == when(a, %u. b, %u. c)"
    4.27 +consts
    4.28 +  Bool        :: "t"
    4.29 +  true        :: "i"
    4.30 +  false       :: "i"
    4.31 +  cond        :: "[i,i,i]=>i"
    4.32 +defs
    4.33 +  Bool_def:   "Bool == T+T"
    4.34 +  true_def:   "true == inl(tt)"
    4.35 +  false_def:  "false == inr(tt)"
    4.36 +  cond_def:   "cond(a,b,c) == when(a, %u. b, %u. c)"
    4.37 +
    4.38 +ML {* use_legacy_bindings (the_context ()) *}
    4.39 +
    4.40  end
     5.1 --- a/src/CTT/CTT.ML	Fri Sep 16 21:02:15 2005 +0200
     5.2 +++ b/src/CTT/CTT.ML	Fri Sep 16 23:01:29 2005 +0200
     5.3 @@ -10,7 +10,7 @@
     5.4  val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
     5.5  and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
     5.6  
     5.7 - 
     5.8 +
     5.9  (*Introduction rules
    5.10    OMITTED: EqI, because its premise is an eqelem, not an elem*)
    5.11  val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI]
    5.12 @@ -42,7 +42,7 @@
    5.13  
    5.14  val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
    5.15  
    5.16 -(*Exploit p:Prod(A,B) to create the assumption z:B(a).  
    5.17 +(*Exploit p:Prod(A,B) to create the assumption z:B(a).
    5.18    A more natural form of product elimination. *)
    5.19  val prems = Goal "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
    5.20  \    |] ==> c(p`a): C(p`a)";
    5.21 @@ -56,7 +56,7 @@
    5.22    | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
    5.23    | is_rigid_elem _ = false;
    5.24  
    5.25 -(*Try solving a:A or a=b:A by assumption provided a is rigid!*) 
    5.26 +(*Try solving a:A or a=b:A by assumption provided a is rigid!*)
    5.27  val test_assume_tac = SUBGOAL(fn (prem,i) =>
    5.28      if is_rigid_elem (Logic.strip_assums_concl prem)
    5.29      then  assume_tac i  else  no_tac);
    5.30 @@ -81,7 +81,7 @@
    5.31    in  REPEAT_FIRST (ASSUME tac)  end;
    5.32  
    5.33  
    5.34 -(*Solve a:A (a flexible, A rigid) by introduction rules. 
    5.35 +(*Solve a:A (a flexible, A rigid) by introduction rules.
    5.36    Cannot use stringtrees (filt_resolve_tac) since
    5.37    goals like ?a:SUM(A,B) have a trivial head-string *)
    5.38  fun intr_tac thms =
    5.39 @@ -125,22 +125,22 @@
    5.40  val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1));
    5.41  
    5.42  (** Tactics that instantiate CTT-rules.
    5.43 -    Vars in the given terms will be incremented! 
    5.44 +    Vars in the given terms will be incremented!
    5.45      The (rtac EqE i) lets them apply to equality judgements. **)
    5.46  
    5.47 -fun NE_tac (sp: string) i = 
    5.48 +fun NE_tac (sp: string) i =
    5.49    TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i;
    5.50  
    5.51 -fun SumE_tac (sp: string) i = 
    5.52 +fun SumE_tac (sp: string) i =
    5.53    TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i;
    5.54  
    5.55 -fun PlusE_tac (sp: string) i = 
    5.56 +fun PlusE_tac (sp: string) i =
    5.57    TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
    5.58  
    5.59  (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
    5.60  
    5.61  (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
    5.62 -fun add_mp_tac i = 
    5.63 +fun add_mp_tac i =
    5.64      rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i;
    5.65  
    5.66  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    5.67 @@ -148,11 +148,11 @@
    5.68  
    5.69  (*"safe" when regarded as predicate calculus rules*)
    5.70  val safe_brls = sort (make_ord lessb)
    5.71 -    [ (true,FE), (true,asm_rl), 
    5.72 +    [ (true,FE), (true,asm_rl),
    5.73        (false,ProdI), (true,SumE), (true,PlusE) ];
    5.74  
    5.75  val unsafe_brls =
    5.76 -    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), 
    5.77 +    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
    5.78        (true,subst_prodE) ];
    5.79  
    5.80  (*0 subgoals vs 1 or more*)
    5.81 @@ -160,12 +160,12 @@
    5.82      List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
    5.83  
    5.84  fun safestep_tac thms i =
    5.85 -    form_tac  ORELSE  
    5.86 +    form_tac  ORELSE
    5.87      resolve_tac thms i  ORELSE
    5.88      biresolve_tac safe0_brls i  ORELSE  mp_tac i  ORELSE
    5.89      DETERM (biresolve_tac safep_brls i);
    5.90  
    5.91 -fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i); 
    5.92 +fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i);
    5.93  
    5.94  fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls;
    5.95  
     6.1 --- a/src/CTT/CTT.thy	Fri Sep 16 21:02:15 2005 +0200
     6.2 +++ b/src/CTT/CTT.thy	Fri Sep 16 23:01:29 2005 +0200
     6.3 @@ -1,21 +1,23 @@
     6.4 -(*  Title:      CTT/ctt.thy
     6.5 +(*  Title:      CTT/CTT.thy
     6.6      ID:         $Id$
     6.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.8      Copyright   1993  University of Cambridge
     6.9 -
    6.10 -Constructive Type Theory
    6.11  *)
    6.12  
    6.13 -CTT = Pure +
    6.14 +header {* Constructive Type Theory *}
    6.15  
    6.16 -types
    6.17 -  i
    6.18 -  t
    6.19 -  o
    6.20 +theory CTT
    6.21 +imports Pure
    6.22 +begin
    6.23 +
    6.24 +typedecl i
    6.25 +typedecl t
    6.26 +typedecl o
    6.27  
    6.28  consts
    6.29    (*Types*)
    6.30 -  F,T       :: "t"          (*F is empty, T contains one element*)
    6.31 +  F         :: "t"
    6.32 +  T         :: "t"          (*F is empty, T contains one element*)
    6.33    contr     :: "i=>i"
    6.34    tt        :: "i"
    6.35    (*Natural numbers*)
    6.36 @@ -23,11 +25,13 @@
    6.37    succ      :: "i=>i"
    6.38    rec       :: "[i, i, [i,i]=>i] => i"
    6.39    (*Unions*)
    6.40 -  inl,inr   :: "i=>i"
    6.41 +  inl       :: "i=>i"
    6.42 +  inr       :: "i=>i"
    6.43    when      :: "[i, i=>i, i=>i]=>i"
    6.44    (*General Sum and Binary Product*)
    6.45    Sum       :: "[t, i=>t]=>t"
    6.46 -  fst,snd   :: "i=>i"
    6.47 +  fst       :: "i=>i"
    6.48 +  snd       :: "i=>i"
    6.49    split     :: "[i, [i,i]=>i] =>i"
    6.50    (*General Product and Function Space*)
    6.51    Prod      :: "[t, i=>t]=>t"
    6.52 @@ -64,24 +68,30 @@
    6.53    "SUM x:A. B"  => "Sum(A, %x. B)"
    6.54    "A * B"       => "Sum(A, _K(B))"
    6.55  
    6.56 +print_translation {*
    6.57 +  [("Prod", dependent_tr' ("@PROD", "@-->")),
    6.58 +   ("Sum", dependent_tr' ("@SUM", "@*"))]
    6.59 +*}
    6.60 +
    6.61 +
    6.62  syntax (xsymbols)
    6.63 -  "@-->"    :: "[t,t]=>t"           ("(_ \\<longrightarrow>/ _)" [31,30] 30)
    6.64 -  "@*"      :: "[t,t]=>t"           ("(_ \\<times>/ _)"          [51,50] 50)
    6.65 -  Elem      :: "[i, t]=>prop"       ("(_ /\\<in> _)" [10,10] 5)
    6.66 -  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
    6.67 -  "@SUM"    :: "[idt,t,t] => t"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
    6.68 -  "@PROD"   :: "[idt,t,t] => t"     ("(3\\<Pi> _\\<in>_./ _)"    10)
    6.69 -  "lam "    :: "[idts, i] => i"     ("(3\\<lambda>\\<lambda>_./ _)" 10)
    6.70 +  "@-->"    :: "[t,t]=>t"           ("(_ \<longrightarrow>/ _)" [31,30] 30)
    6.71 +  "@*"      :: "[t,t]=>t"           ("(_ \<times>/ _)"          [51,50] 50)
    6.72 +  Elem      :: "[i, t]=>prop"       ("(_ /\<in> _)" [10,10] 5)
    6.73 +  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    6.74 +  "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    6.75 +  "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    6.76 +  "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
    6.77  
    6.78  syntax (HTML output)
    6.79 -  "@*"      :: "[t,t]=>t"           ("(_ \\<times>/ _)"          [51,50] 50)
    6.80 -  Elem      :: "[i, t]=>prop"       ("(_ /\\<in> _)" [10,10] 5)
    6.81 -  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
    6.82 -  "@SUM"    :: "[idt,t,t] => t"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
    6.83 -  "@PROD"   :: "[idt,t,t] => t"     ("(3\\<Pi> _\\<in>_./ _)"    10)
    6.84 -  "lam "    :: "[idts, i] => i"     ("(3\\<lambda>\\<lambda>_./ _)" 10)
    6.85 +  "@*"      :: "[t,t]=>t"           ("(_ \<times>/ _)"          [51,50] 50)
    6.86 +  Elem      :: "[i, t]=>prop"       ("(_ /\<in> _)" [10,10] 5)
    6.87 +  Eqelem    :: "[i,i,t]=>prop"      ("(2_ =/ _ \<in>/ _)" [10,10,10] 5)
    6.88 +  "@SUM"    :: "[idt,t,t] => t"     ("(3\<Sigma> _\<in>_./ _)" 10)
    6.89 +  "@PROD"   :: "[idt,t,t] => t"     ("(3\<Pi> _\<in>_./ _)"    10)
    6.90 +  "lam "    :: "[idts, i] => i"     ("(3\<lambda>\<lambda>_./ _)" 10)
    6.91  
    6.92 -rules
    6.93 +axioms
    6.94  
    6.95    (*Reduction: a weaker notion than equality;  a hack for simplification.
    6.96      Reduce[a,b] means either that  a=b:A  for some A or else that "a" and "b"
    6.97 @@ -89,167 +99,167 @@
    6.98  
    6.99    (*does not verify a:A!  Sound because only trans_red uses a Reduce premise
   6.100      No new theorems can be proved about the standard judgements.*)
   6.101 -  refl_red "Reduce[a,a]"
   6.102 -  red_if_equal "a = b : A ==> Reduce[a,b]"
   6.103 -  trans_red "[| a = b : A;  Reduce[b,c] |] ==> a = c : A"
   6.104 +  refl_red: "Reduce[a,a]"
   6.105 +  red_if_equal: "a = b : A ==> Reduce[a,b]"
   6.106 +  trans_red: "[| a = b : A;  Reduce[b,c] |] ==> a = c : A"
   6.107  
   6.108    (*Reflexivity*)
   6.109  
   6.110 -  refl_type "A type ==> A = A"
   6.111 -  refl_elem "a : A ==> a = a : A"
   6.112 +  refl_type: "A type ==> A = A"
   6.113 +  refl_elem: "a : A ==> a = a : A"
   6.114  
   6.115    (*Symmetry*)
   6.116  
   6.117 -  sym_type  "A = B ==> B = A"
   6.118 -  sym_elem  "a = b : A ==> b = a : A"
   6.119 +  sym_type:  "A = B ==> B = A"
   6.120 +  sym_elem:  "a = b : A ==> b = a : A"
   6.121  
   6.122    (*Transitivity*)
   6.123  
   6.124 -  trans_type   "[| A = B;  B = C |] ==> A = C"
   6.125 -  trans_elem   "[| a = b : A;  b = c : A |] ==> a = c : A"
   6.126 +  trans_type:   "[| A = B;  B = C |] ==> A = C"
   6.127 +  trans_elem:   "[| a = b : A;  b = c : A |] ==> a = c : A"
   6.128  
   6.129 -  equal_types  "[| a : A;  A = B |] ==> a : B"
   6.130 -  equal_typesL "[| a = b : A;  A = B |] ==> a = b : B"
   6.131 +  equal_types:  "[| a : A;  A = B |] ==> a : B"
   6.132 +  equal_typesL: "[| a = b : A;  A = B |] ==> a = b : B"
   6.133  
   6.134    (*Substitution*)
   6.135  
   6.136 -  subst_type   "[| a : A;  !!z. z:A ==> B(z) type |] ==> B(a) type"
   6.137 -  subst_typeL  "[| a = c : A;  !!z. z:A ==> B(z) = D(z) |] ==> B(a) = D(c)"
   6.138 +  subst_type:   "[| a : A;  !!z. z:A ==> B(z) type |] ==> B(a) type"
   6.139 +  subst_typeL:  "[| a = c : A;  !!z. z:A ==> B(z) = D(z) |] ==> B(a) = D(c)"
   6.140  
   6.141 -  subst_elem   "[| a : A;  !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)"
   6.142 -  subst_elemL
   6.143 +  subst_elem:   "[| a : A;  !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)"
   6.144 +  subst_elemL:
   6.145      "[| a=c : A;  !!z. z:A ==> b(z)=d(z) : B(z) |] ==> b(a)=d(c) : B(a)"
   6.146  
   6.147  
   6.148    (*The type N -- natural numbers*)
   6.149  
   6.150 -  NF "N type"
   6.151 -  NI0 "0 : N"
   6.152 -  NI_succ "a : N ==> succ(a) : N"
   6.153 -  NI_succL  "a = b : N ==> succ(a) = succ(b) : N"
   6.154 +  NF: "N type"
   6.155 +  NI0: "0 : N"
   6.156 +  NI_succ: "a : N ==> succ(a) : N"
   6.157 +  NI_succL:  "a = b : N ==> succ(a) = succ(b) : N"
   6.158  
   6.159 -  NE
   6.160 -   "[| p: N;  a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] 
   6.161 +  NE:
   6.162 +   "[| p: N;  a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |]
   6.163     ==> rec(p, a, %u v. b(u,v)) : C(p)"
   6.164  
   6.165 -  NEL
   6.166 -   "[| p = q : N;  a = c : C(0);  
   6.167 -      !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] 
   6.168 +  NEL:
   6.169 +   "[| p = q : N;  a = c : C(0);
   6.170 +      !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |]
   6.171     ==> rec(p, a, %u v. b(u,v)) = rec(q,c,d) : C(p)"
   6.172  
   6.173 -  NC0
   6.174 -   "[| a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] 
   6.175 +  NC0:
   6.176 +   "[| a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |]
   6.177     ==> rec(0, a, %u v. b(u,v)) = a : C(0)"
   6.178  
   6.179 -  NC_succ
   6.180 -   "[| p: N;  a: C(0);  
   6.181 -       !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==>  
   6.182 +  NC_succ:
   6.183 +   "[| p: N;  a: C(0);
   6.184 +       !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==>
   6.185     rec(succ(p), a, %u v. b(u,v)) = b(p, rec(p, a, %u v. b(u,v))) : C(succ(p))"
   6.186  
   6.187    (*The fourth Peano axiom.  See page 91 of Martin-Lof's book*)
   6.188 -  zero_ne_succ
   6.189 +  zero_ne_succ:
   6.190      "[| a: N;  0 = succ(a) : N |] ==> 0: F"
   6.191  
   6.192  
   6.193    (*The Product of a family of types*)
   6.194  
   6.195 -  ProdF  "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type"
   6.196 +  ProdF:  "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type"
   6.197  
   6.198 -  ProdFL
   6.199 -   "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> 
   6.200 +  ProdFL:
   6.201 +   "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==>
   6.202     PROD x:A. B(x) = PROD x:C. D(x)"
   6.203  
   6.204 -  ProdI
   6.205 +  ProdI:
   6.206     "[| A type;  !!x. x:A ==> b(x):B(x)|] ==> lam x. b(x) : PROD x:A. B(x)"
   6.207  
   6.208 -  ProdIL
   6.209 -   "[| A type;  !!x. x:A ==> b(x) = c(x) : B(x)|] ==> 
   6.210 +  ProdIL:
   6.211 +   "[| A type;  !!x. x:A ==> b(x) = c(x) : B(x)|] ==>
   6.212     lam x. b(x) = lam x. c(x) : PROD x:A. B(x)"
   6.213  
   6.214 -  ProdE  "[| p : PROD x:A. B(x);  a : A |] ==> p`a : B(a)"
   6.215 -  ProdEL "[| p=q: PROD x:A. B(x);  a=b : A |] ==> p`a = q`b : B(a)"
   6.216 +  ProdE:  "[| p : PROD x:A. B(x);  a : A |] ==> p`a : B(a)"
   6.217 +  ProdEL: "[| p=q: PROD x:A. B(x);  a=b : A |] ==> p`a = q`b : B(a)"
   6.218  
   6.219 -  ProdC
   6.220 -   "[| a : A;  !!x. x:A ==> b(x) : B(x)|] ==> 
   6.221 +  ProdC:
   6.222 +   "[| a : A;  !!x. x:A ==> b(x) : B(x)|] ==>
   6.223     (lam x. b(x)) ` a = b(a) : B(a)"
   6.224  
   6.225 -  ProdC2
   6.226 +  ProdC2:
   6.227     "p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)"
   6.228  
   6.229  
   6.230    (*The Sum of a family of types*)
   6.231  
   6.232 -  SumF  "[| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type"
   6.233 -  SumFL
   6.234 +  SumF:  "[| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type"
   6.235 +  SumFL:
   6.236      "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A. B(x) = SUM x:C. D(x)"
   6.237  
   6.238 -  SumI  "[| a : A;  b : B(a) |] ==> <a,b> : SUM x:A. B(x)"
   6.239 -  SumIL "[| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)"
   6.240 +  SumI:  "[| a : A;  b : B(a) |] ==> <a,b> : SUM x:A. B(x)"
   6.241 +  SumIL: "[| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)"
   6.242  
   6.243 -  SumE
   6.244 -    "[| p: SUM x:A. B(x);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
   6.245 +  SumE:
   6.246 +    "[| p: SUM x:A. B(x);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |]
   6.247      ==> split(p, %x y. c(x,y)) : C(p)"
   6.248  
   6.249 -  SumEL
   6.250 -    "[| p=q : SUM x:A. B(x); 
   6.251 -       !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|] 
   6.252 +  SumEL:
   6.253 +    "[| p=q : SUM x:A. B(x);
   6.254 +       !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|]
   6.255      ==> split(p, %x y. c(x,y)) = split(q, % x y. d(x,y)) : C(p)"
   6.256  
   6.257 -  SumC
   6.258 -    "[| a: A;  b: B(a);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
   6.259 +  SumC:
   6.260 +    "[| a: A;  b: B(a);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |]
   6.261      ==> split(<a,b>, %x y. c(x,y)) = c(a,b) : C(<a,b>)"
   6.262  
   6.263 -  fst_def   "fst(a) == split(a, %x y. x)"
   6.264 -  snd_def   "snd(a) == split(a, %x y. y)"
   6.265 +  fst_def:   "fst(a) == split(a, %x y. x)"
   6.266 +  snd_def:   "snd(a) == split(a, %x y. y)"
   6.267  
   6.268  
   6.269    (*The sum of two types*)
   6.270  
   6.271 -  PlusF   "[| A type;  B type |] ==> A+B type"
   6.272 -  PlusFL  "[| A = C;  B = D |] ==> A+B = C+D"
   6.273 +  PlusF:   "[| A type;  B type |] ==> A+B type"
   6.274 +  PlusFL:  "[| A = C;  B = D |] ==> A+B = C+D"
   6.275  
   6.276 -  PlusI_inl   "[| a : A;  B type |] ==> inl(a) : A+B"
   6.277 -  PlusI_inlL "[| a = c : A;  B type |] ==> inl(a) = inl(c) : A+B"
   6.278 +  PlusI_inl:   "[| a : A;  B type |] ==> inl(a) : A+B"
   6.279 +  PlusI_inlL: "[| a = c : A;  B type |] ==> inl(a) = inl(c) : A+B"
   6.280  
   6.281 -  PlusI_inr   "[| A type;  b : B |] ==> inr(b) : A+B"
   6.282 -  PlusI_inrL "[| A type;  b = d : B |] ==> inr(b) = inr(d) : A+B"
   6.283 +  PlusI_inr:   "[| A type;  b : B |] ==> inr(b) : A+B"
   6.284 +  PlusI_inrL: "[| A type;  b = d : B |] ==> inr(b) = inr(d) : A+B"
   6.285  
   6.286 -  PlusE
   6.287 -    "[| p: A+B;  !!x. x:A ==> c(x): C(inl(x));  
   6.288 -                !!y. y:B ==> d(y): C(inr(y)) |] 
   6.289 +  PlusE:
   6.290 +    "[| p: A+B;  !!x. x:A ==> c(x): C(inl(x));
   6.291 +                !!y. y:B ==> d(y): C(inr(y)) |]
   6.292      ==> when(p, %x. c(x), %y. d(y)) : C(p)"
   6.293  
   6.294 -  PlusEL
   6.295 -    "[| p = q : A+B;  !!x. x: A ==> c(x) = e(x) : C(inl(x));   
   6.296 -                     !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] 
   6.297 +  PlusEL:
   6.298 +    "[| p = q : A+B;  !!x. x: A ==> c(x) = e(x) : C(inl(x));
   6.299 +                     !!y. y: B ==> d(y) = f(y) : C(inr(y)) |]
   6.300      ==> when(p, %x. c(x), %y. d(y)) = when(q, %x. e(x), %y. f(y)) : C(p)"
   6.301  
   6.302 -  PlusC_inl
   6.303 -    "[| a: A;  !!x. x:A ==> c(x): C(inl(x));  
   6.304 -              !!y. y:B ==> d(y): C(inr(y)) |] 
   6.305 +  PlusC_inl:
   6.306 +    "[| a: A;  !!x. x:A ==> c(x): C(inl(x));
   6.307 +              !!y. y:B ==> d(y): C(inr(y)) |]
   6.308      ==> when(inl(a), %x. c(x), %y. d(y)) = c(a) : C(inl(a))"
   6.309  
   6.310 -  PlusC_inr
   6.311 -    "[| b: B;  !!x. x:A ==> c(x): C(inl(x));  
   6.312 -              !!y. y:B ==> d(y): C(inr(y)) |] 
   6.313 +  PlusC_inr:
   6.314 +    "[| b: B;  !!x. x:A ==> c(x): C(inl(x));
   6.315 +              !!y. y:B ==> d(y): C(inr(y)) |]
   6.316      ==> when(inr(b), %x. c(x), %y. d(y)) = d(b) : C(inr(b))"
   6.317  
   6.318  
   6.319    (*The type Eq*)
   6.320  
   6.321 -  EqF    "[| A type;  a : A;  b : A |] ==> Eq(A,a,b) type"
   6.322 -  EqFL "[| A=B;  a=c: A;  b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)"
   6.323 -  EqI "a = b : A ==> eq : Eq(A,a,b)"
   6.324 -  EqE "p : Eq(A,a,b) ==> a = b : A"
   6.325 +  EqF:    "[| A type;  a : A;  b : A |] ==> Eq(A,a,b) type"
   6.326 +  EqFL: "[| A=B;  a=c: A;  b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)"
   6.327 +  EqI: "a = b : A ==> eq : Eq(A,a,b)"
   6.328 +  EqE: "p : Eq(A,a,b) ==> a = b : A"
   6.329  
   6.330    (*By equality of types, can prove C(p) from C(eq), an elimination rule*)
   6.331 -  EqC "p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)"
   6.332 +  EqC: "p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)"
   6.333  
   6.334    (*The type F*)
   6.335  
   6.336 -  FF "F type"
   6.337 -  FE "[| p: F;  C type |] ==> contr(p) : C"
   6.338 -  FEL  "[| p = q : F;  C type |] ==> contr(p) = contr(q) : C"
   6.339 +  FF: "F type"
   6.340 +  FE: "[| p: F;  C type |] ==> contr(p) : C"
   6.341 +  FEL:  "[| p = q : F;  C type |] ==> contr(p) = contr(q) : C"
   6.342  
   6.343    (*The type T
   6.344       Martin-Lof's book (page 68) discusses elimination and computation.
   6.345 @@ -257,17 +267,12 @@
   6.346       but with an extra premise C(x) type x:T.
   6.347       Also computation can be derived from elimination. *)
   6.348  
   6.349 -  TF "T type"
   6.350 -  TI "tt : T"
   6.351 -  TE "[| p : T;  c : C(tt) |] ==> c : C(p)"
   6.352 -  TEL "[| p = q : T;  c = d : C(tt) |] ==> c = d : C(p)"
   6.353 -  TC "p : T ==> p = tt : T"
   6.354 -end
   6.355 +  TF: "T type"
   6.356 +  TI: "tt : T"
   6.357 +  TE: "[| p : T;  c : C(tt) |] ==> c : C(p)"
   6.358 +  TEL: "[| p = q : T;  c = d : C(tt) |] ==> c = d : C(p)"
   6.359 +  TC: "p : T ==> p = tt : T"
   6.360  
   6.361 -
   6.362 -ML
   6.363 +ML {* use_legacy_bindings (the_context ()) *}
   6.364  
   6.365 -val print_translation =
   6.366 -  [("Prod", dependent_tr' ("@PROD", "@-->")),
   6.367 -   ("Sum", dependent_tr' ("@SUM", "@*"))];
   6.368 -
   6.369 +end
     7.1 --- a/src/CTT/Main.thy	Fri Sep 16 21:02:15 2005 +0200
     7.2 +++ b/src/CTT/Main.thy	Fri Sep 16 23:01:29 2005 +0200
     7.3 @@ -1,6 +1,9 @@
     7.4  
     7.5 -(*theory Main includes everything*)
     7.6 +(* $Id$ *)
     7.7 +
     7.8 +header {* Main includes everything *}
     7.9  
    7.10 -theory Main imports CTT Arith Bool begin
    7.11 -
    7.12 +theory Main
    7.13 +imports CTT Arith Bool
    7.14 +begin
    7.15  end
     8.1 --- a/src/CTT/ROOT.ML	Fri Sep 16 21:02:15 2005 +0200
     8.2 +++ b/src/CTT/ROOT.ML	Fri Sep 16 23:01:29 2005 +0200
     8.3 @@ -10,13 +10,6 @@
     8.4  val banner = "Constructive Type Theory";
     8.5  writeln banner;
     8.6  
     8.7 -print_depth 1;  
     8.8 -
     8.9 -use_thy "CTT";
    8.10 -use "~~/src/Provers/typedsimp.ML";
    8.11 -use "rew.ML";
    8.12  use_thy "Main";
    8.13  
    8.14 -print_depth 8;
    8.15 -
    8.16  Goal "tt : T";  (*leave subgoal package empty*)
     9.1 --- a/src/CTT/ex/synth.ML	Fri Sep 16 21:02:15 2005 +0200
     9.2 +++ b/src/CTT/ex/synth.ML	Fri Sep 16 23:01:29 2005 +0200
     9.3 @@ -6,7 +6,7 @@
     9.4  
     9.5  writeln"Synthesis examples, using a crude form of narrowing";
     9.6  
     9.7 -context Arith.thy;
     9.8 +context (theory "Arith");
     9.9  
    9.10  writeln"discovery of predecessor function";
    9.11  Goal