expanded tabs; renamed subtype to typedef;
authorclasohm
Mon Feb 05 21:27:16 1996 +0100 (1996-02-05)
changeset 14757f5a4cd08209
parent 1474 3f7d67927fe2
child 1476 608483c2122a
expanded tabs; renamed subtype to typedef;
incorporated Konrad's changes
src/HOL/Arith.ML
src/HOL/Arith.thy
src/HOL/Finite.thy
src/HOL/Fun.thy
src/HOL/Gfp.thy
src/HOL/Lfp.thy
src/HOL/List.thy
src/HOL/Nat.ML
src/HOL/Nat.thy
src/HOL/Prod.thy
src/HOL/Relation.thy
src/HOL/Sexp.ML
src/HOL/Sexp.thy
src/HOL/Sum.thy
src/HOL/Trancl.thy
src/HOL/Univ.thy
src/HOL/WF.ML
src/HOL/WF.thy
src/HOL/equalities.thy
src/HOL/mono.thy
src/HOL/subset.thy
src/HOL/thy_syntax.ML
src/HOL/typedef.ML
     1.1 --- a/src/HOL/Arith.ML	Mon Feb 05 14:44:09 1996 +0100
     1.2 +++ b/src/HOL/Arith.ML	Mon Feb 05 21:27:16 1996 +0100
     1.3 @@ -197,26 +197,36 @@
     1.4  by (rtac refl 1);
     1.5  qed "less_eq";
     1.6  
     1.7 +goal Arith.thy "(%m. m mod n) = wfrec (trancl pred_nat) \
     1.8 +             \                      (%f j. if j<n then j else f (j-n))";
     1.9 +by (simp_tac (HOL_ss addsimps [mod_def]) 1);
    1.10 +val mod_def1 = result() RS eq_reflection;
    1.11 +
    1.12  goal Arith.thy "!!m. m<n ==> m mod n = m";
    1.13 -by (rtac (mod_def RS wf_less_trans) 1);
    1.14 +by (rtac (mod_def1 RS wf_less_trans) 1);
    1.15  by(Asm_simp_tac 1);
    1.16  qed "mod_less";
    1.17  
    1.18  goal Arith.thy "!!m. [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
    1.19 -by (rtac (mod_def RS wf_less_trans) 1);
    1.20 +by (rtac (mod_def1 RS wf_less_trans) 1);
    1.21  by(asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
    1.22  qed "mod_geq";
    1.23  
    1.24  
    1.25  (*** Quotient ***)
    1.26  
    1.27 +goal Arith.thy "(%m. m div n) = wfrec (trancl pred_nat) \
    1.28 +                        \            (%f j. if j<n then 0 else Suc (f (j-n)))";
    1.29 +by (simp_tac (HOL_ss addsimps [div_def]) 1);
    1.30 +val div_def1 = result() RS eq_reflection;
    1.31 +
    1.32  goal Arith.thy "!!m. m<n ==> m div n = 0";
    1.33 -by (rtac (div_def RS wf_less_trans) 1);
    1.34 +by (rtac (div_def1 RS wf_less_trans) 1);
    1.35  by(Asm_simp_tac 1);
    1.36  qed "div_less";
    1.37  
    1.38  goal Arith.thy "!!M. [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
    1.39 -by (rtac (div_def RS wf_less_trans) 1);
    1.40 +by (rtac (div_def1 RS wf_less_trans) 1);
    1.41  by(asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
    1.42  qed "div_geq";
    1.43  
    1.44 @@ -322,20 +332,20 @@
    1.45  bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
    1.46  
    1.47  goal Arith.thy "!!i. i+j < (k::nat) ==> i<k";
    1.48 -by (etac rev_mp 1);
    1.49 +be rev_mp 1;
    1.50  by(nat_ind_tac "j" 1);
    1.51  by (ALLGOALS Asm_simp_tac);
    1.52  by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
    1.53  qed "add_lessD1";
    1.54  
    1.55  goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
    1.56 -by (etac le_trans 1);
    1.57 -by (rtac le_add1 1);
    1.58 +by (eresolve_tac [le_trans] 1);
    1.59 +by (resolve_tac [le_add1] 1);
    1.60  qed "le_imp_add_le";
    1.61  
    1.62  goal Arith.thy "!!k::nat. m < n ==> m < n+k";
    1.63 -by (etac less_le_trans 1);
    1.64 -by (rtac le_add1 1);
    1.65 +by (eresolve_tac [less_le_trans] 1);
    1.66 +by (resolve_tac [le_add1] 1);
    1.67  qed "less_imp_add_less";
    1.68  
    1.69  goal Arith.thy "m+k<=n --> m<=(n::nat)";
    1.70 @@ -350,7 +360,7 @@
    1.71  by (asm_full_simp_tac
    1.72      (!simpset delsimps [add_Suc_right]
    1.73                  addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
    1.74 -by (etac subst 1);
    1.75 +by (eresolve_tac [subst] 1);
    1.76  by (simp_tac (!simpset addsimps [less_add_Suc1]) 1);
    1.77  qed "less_add_eq_less";
    1.78  
    1.79 @@ -386,7 +396,7 @@
    1.80  (*non-strict, in 1st argument*)
    1.81  goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k";
    1.82  by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1);
    1.83 -by (etac add_less_mono1 1);
    1.84 +by (eresolve_tac [add_less_mono1] 1);
    1.85  by (assume_tac 1);
    1.86  qed "add_le_mono1";
    1.87  
    1.88 @@ -395,5 +405,5 @@
    1.89  by (etac (add_le_mono1 RS le_trans) 1);
    1.90  by (simp_tac (!simpset addsimps [add_commute]) 1);
    1.91  (*j moves to the end because it is free while k, l are bound*)
    1.92 -by (etac add_le_mono1 1);
    1.93 +by (eresolve_tac [add_le_mono1] 1);
    1.94  qed "add_le_mono";
     2.1 --- a/src/HOL/Arith.thy	Mon Feb 05 14:44:09 1996 +0100
     2.2 +++ b/src/HOL/Arith.thy	Mon Feb 05 21:27:16 1996 +0100
     2.3 @@ -20,8 +20,10 @@
     2.4    add_def   "m+n == nat_rec m n (%u v. Suc(v))"
     2.5    diff_def  "m-n == nat_rec n m (%u v. pred(v))"
     2.6    mult_def  "m*n == nat_rec m 0 (%u v. n + v)"
     2.7 -  mod_def   "m mod n == wfrec (trancl pred_nat) m (%j f.if j<n then j else f (j-n))"
     2.8 -  div_def   "m div n == wfrec (trancl pred_nat) m (%j f.if j<n then 0 else Suc (f (j-n)))"
     2.9 +mod_def "m mod n == wfrec (trancl pred_nat)
    2.10 +                          (%f j. if j<n then j else f (j-n)) m"
    2.11 +div_def "m div n == wfrec (trancl pred_nat) 
    2.12 +                          (%f j. if j<n then 0 else Suc (f (j-n))) m"
    2.13  end
    2.14  
    2.15  (*"Difference" is subtraction of natural numbers.
     3.1 --- a/src/HOL/Finite.thy	Mon Feb 05 14:44:09 1996 +0100
     3.2 +++ b/src/HOL/Finite.thy	Mon Feb 05 21:27:16 1996 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4 -(*  Title: 	HOL/Finite.thy
     3.5 +(*  Title:      HOL/Finite.thy
     3.6      ID:         $Id$
     3.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.9      Copyright   1994  University of Cambridge
    3.10  
    3.11  Finite powerset operator
     4.1 --- a/src/HOL/Fun.thy	Mon Feb 05 14:44:09 1996 +0100
     4.2 +++ b/src/HOL/Fun.thy	Mon Feb 05 21:27:16 1996 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4 -(*  Title: 	HOL/Fun.thy
     4.5 +(*  Title:      HOL/Fun.thy
     4.6      ID:         $Id$
     4.7 -    Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
     4.8 +    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4.9      Copyright   1994  University of Cambridge
    4.10  
    4.11  Lemmas about functions.
     5.1 --- a/src/HOL/Gfp.thy	Mon Feb 05 14:44:09 1996 +0100
     5.2 +++ b/src/HOL/Gfp.thy	Mon Feb 05 21:27:16 1996 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4 -(*  Title: 	HOL/gfp.thy
     5.5 +(*  Title:      HOL/gfp.thy
     5.6      ID:         $Id$
     5.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     5.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.9      Copyright   1994  University of Cambridge
    5.10  
    5.11  Greatest fixed points (requires Lfp too!)
     6.1 --- a/src/HOL/Lfp.thy	Mon Feb 05 14:44:09 1996 +0100
     6.2 +++ b/src/HOL/Lfp.thy	Mon Feb 05 21:27:16 1996 +0100
     6.3 @@ -1,6 +1,6 @@
     6.4 -(*  Title: 	HOL/Lfp.thy
     6.5 +(*  Title:      HOL/Lfp.thy
     6.6      ID:         $Id$
     6.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     6.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.9      Copyright   1992  University of Cambridge
    6.10  
    6.11  The Knaster-Tarski Theorem
     7.1 --- a/src/HOL/List.thy	Mon Feb 05 14:44:09 1996 +0100
     7.2 +++ b/src/HOL/List.thy	Mon Feb 05 21:27:16 1996 +0100
     7.3 @@ -13,7 +13,7 @@
     7.4  
     7.5  consts
     7.6  
     7.7 -  "@"	    :: ['a list, 'a list] => 'a list		(infixr 65)
     7.8 +  "@"       :: ['a list, 'a list] => 'a list            (infixr 65)
     7.9    drop      :: [nat, 'a list] => 'a list
    7.10    filter    :: ['a => bool, 'a list] => 'a list
    7.11    flat      :: 'a list list => 'a list
    7.12 @@ -22,7 +22,7 @@
    7.13    length    :: 'a list => nat
    7.14    list_all  :: ('a => bool) => ('a list => bool)
    7.15    map       :: ('a=>'b) => ('a list => 'b list)
    7.16 -  mem       :: ['a, 'a list] => bool			(infixl 55)
    7.17 +  mem       :: ['a, 'a list] => bool                    (infixl 55)
    7.18    nth       :: [nat, 'a list] => 'a
    7.19    take      :: [nat, 'a list] => 'a list
    7.20    tl,ttl    :: 'a list => 'a list
    7.21 @@ -33,15 +33,15 @@
    7.22    "@list"   :: args => 'a list                        ("[(_)]")
    7.23  
    7.24    (* Special syntax for list_all and filter *)
    7.25 -  "@Alls"	:: [idt, 'a list, bool] => bool	("(2Alls _:_./ _)" 10)
    7.26 -  "@filter"	:: [idt, 'a list, bool] => 'a list	("(1[_:_ ./ _])")
    7.27 +  "@Alls"       :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
    7.28 +  "@filter"     :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
    7.29  
    7.30  translations
    7.31    "[x, xs]"     == "x#[xs]"
    7.32    "[x]"         == "x#[]"
    7.33  
    7.34 -  "[x:xs . P]"	== "filter (%x.P) xs"
    7.35 -  "Alls x:xs.P"	== "list_all (%x.P) xs"
    7.36 +  "[x:xs . P]"  == "filter (%x.P) xs"
    7.37 +  "Alls x:xs.P" == "list_all (%x.P) xs"
    7.38  
    7.39  primrec hd list
    7.40    hd_Nil  "hd([]) = (@x.False)"
     8.1 --- a/src/HOL/Nat.ML	Mon Feb 05 14:44:09 1996 +0100
     8.2 +++ b/src/HOL/Nat.ML	Mon Feb 05 21:27:16 1996 +0100
     8.3 @@ -160,7 +160,17 @@
     8.4  
     8.5  (*** nat_rec -- by wf recursion on pred_nat ***)
     8.6  
     8.7 -bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec)));
     8.8 +(* The unrolling rule for nat_rec *)
     8.9 +goal Nat.thy
    8.10 +   "(%n. nat_rec n c d) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))";
    8.11 +  by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1);
    8.12 +bind_thm("nat_rec_unfold", wf_pred_nat RS 
    8.13 +                            ((result() RS eq_reflection) RS def_wfrec));
    8.14 +
    8.15 +(*---------------------------------------------------------------------------
    8.16 + * Old:
    8.17 + * bind_thm ("nat_rec_unfold", (wf_pred_nat RS (nat_rec_def RS def_wfrec))); 
    8.18 + *---------------------------------------------------------------------------*)
    8.19  
    8.20  (** conversion rules **)
    8.21  
     9.1 --- a/src/HOL/Nat.thy	Mon Feb 05 14:44:09 1996 +0100
     9.2 +++ b/src/HOL/Nat.thy	Mon Feb 05 21:27:16 1996 +0100
     9.3 @@ -33,7 +33,7 @@
     9.4  
     9.5  (* type definition *)
     9.6  
     9.7 -subtype (Nat)
     9.8 +typedef (Nat)
     9.9    nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
    9.10  
    9.11  instance
    9.12 @@ -65,6 +65,5 @@
    9.13  
    9.14    le_def   "m<=(n::nat) == ~(n<m)"
    9.15  
    9.16 -  nat_rec_def   "nat_rec n c d == wfrec pred_nat n  
    9.17 -                        (nat_case (%g.c) (%m g.(d m (g m))))"
    9.18 +nat_rec_def"nat_rec n c d == wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
    9.19  end
    10.1 --- a/src/HOL/Prod.thy	Mon Feb 05 14:44:09 1996 +0100
    10.2 +++ b/src/HOL/Prod.thy	Mon Feb 05 21:27:16 1996 +0100
    10.3 @@ -19,7 +19,7 @@
    10.4  defs
    10.5    Pair_Rep_def  "Pair_Rep == (%a b. %x y. x=a & y=b)"
    10.6  
    10.7 -subtype (Prod)
    10.8 +typedef (Prod)
    10.9    ('a, 'b) "*"          (infixr 20)
   10.10      = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
   10.11  
   10.12 @@ -61,7 +61,7 @@
   10.13  
   10.14  (** Unit **)
   10.15  
   10.16 -subtype (Unit)
   10.17 +typedef (Unit)
   10.18    unit = "{p. p = True}"
   10.19  
   10.20  consts
    11.1 --- a/src/HOL/Relation.thy	Mon Feb 05 14:44:09 1996 +0100
    11.2 +++ b/src/HOL/Relation.thy	Mon Feb 05 21:27:16 1996 +0100
    11.3 @@ -1,24 +1,24 @@
    11.4 -(*  Title: 	Relation.thy
    11.5 +(*  Title:      Relation.thy
    11.6      ID:         $Id$
    11.7 -    Author: 	Riccardo Mattolini, Dip. Sistemi e Informatica
    11.8 -        and	Lawrence C Paulson, Cambridge University Computer Laboratory
    11.9 +    Author:     Riccardo Mattolini, Dip. Sistemi e Informatica
   11.10 +        and     Lawrence C Paulson, Cambridge University Computer Laboratory
   11.11      Copyright   1994 Universita' di Firenze
   11.12      Copyright   1993  University of Cambridge
   11.13  *)
   11.14  
   11.15  Relation = Prod +
   11.16  consts
   11.17 -    id	        :: "('a * 'a)set"               (*the identity relation*)
   11.18 -    O	        :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
   11.19 -    trans       :: "('a * 'a)set => bool" 	(*transitivity predicate*)
   11.20 +    id          :: "('a * 'a)set"               (*the identity relation*)
   11.21 +    O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
   11.22 +    trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
   11.23      converse    :: "('a * 'b)set => ('b * 'a)set"
   11.24      "^^"        :: "[('a * 'b) set, 'a set] => 'b set" (infixl 90)
   11.25      Domain      :: "('a * 'b) set => 'a set"
   11.26      Range       :: "('a * 'b) set => 'b set"
   11.27  defs
   11.28 -    id_def	"id == {p. ? x. p = (x,x)}"
   11.29 -    comp_def	"r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
   11.30 -    trans_def	  "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
   11.31 +    id_def      "id == {p. ? x. p = (x,x)}"
   11.32 +    comp_def    "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
   11.33 +    trans_def     "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
   11.34      converse_def  "converse(r) == {(y,x). (x,y):r}"
   11.35      Domain_def    "Domain(r) == {x. ? y. (x,y):r}"
   11.36      Range_def     "Range(r) == Domain(converse(r))"
    12.1 --- a/src/HOL/Sexp.ML	Mon Feb 05 14:44:09 1996 +0100
    12.2 +++ b/src/HOL/Sexp.ML	Mon Feb 05 21:27:16 1996 +0100
    12.3 @@ -17,17 +17,17 @@
    12.4                     Scons_neq_Leaf, Scons_neq_Numb];
    12.5  
    12.6  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
    12.7 -by (rtac select_equality 1);
    12.8 +by (resolve_tac [select_equality] 1);
    12.9  by (ALLGOALS (fast_tac sexp_free_cs));
   12.10  qed "sexp_case_Leaf";
   12.11  
   12.12  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
   12.13 -by (rtac select_equality 1);
   12.14 +by (resolve_tac [select_equality] 1);
   12.15  by (ALLGOALS (fast_tac sexp_free_cs));
   12.16  qed "sexp_case_Numb";
   12.17  
   12.18  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
   12.19 -by (rtac select_equality 1);
   12.20 +by (resolve_tac [select_equality] 1);
   12.21  by (ALLGOALS (fast_tac sexp_free_cs));
   12.22  qed "sexp_case_Scons";
   12.23  
   12.24 @@ -109,9 +109,18 @@
   12.25  
   12.26  (*** sexp_rec -- by wf recursion on pred_sexp ***)
   12.27  
   12.28 +goal Sexp.thy
   12.29 +   "(%M. sexp_rec M c d e) = wfrec pred_sexp \
   12.30 +                       \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
   12.31 +by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
   12.32 +bind_thm("sexp_rec_unfold", wf_pred_sexp RS 
   12.33 +                            ((result() RS eq_reflection) RS def_wfrec));
   12.34  (** conversion rules **)
   12.35  
   12.36 -val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
   12.37 +(*---------------------------------------------------------------------------
   12.38 + * Old:
   12.39 + * val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
   12.40 + *---------------------------------------------------------------------------*)
   12.41  
   12.42  
   12.43  goal Sexp.thy "sexp_rec (Leaf a) c d h = c(a)";
    13.1 --- a/src/HOL/Sexp.thy	Mon Feb 05 14:44:09 1996 +0100
    13.2 +++ b/src/HOL/Sexp.thy	Mon Feb 05 21:27:16 1996 +0100
    13.3 @@ -1,6 +1,6 @@
    13.4 -(*  Title: 	HOL/Sexp
    13.5 +(*  Title:      HOL/Sexp
    13.6      ID:         $Id$
    13.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    13.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.9      Copyright   1992  University of Cambridge
   13.10  
   13.11  S-expressions, general binary trees for defining recursive data structures
   13.12 @@ -13,7 +13,7 @@
   13.13    sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
   13.14                  'a item] => 'b"
   13.15  
   13.16 -  sexp_rec  :: "['a item, 'a=>'b, nat=>'b, 	
   13.17 +  sexp_rec  :: "['a item, 'a=>'b, nat=>'b,      
   13.18                  ['a item, 'a item, 'b, 'b]=>'b] => 'b"
   13.19    
   13.20    pred_sexp :: "('a item * 'a item)set"
   13.21 @@ -26,7 +26,7 @@
   13.22  
   13.23  defs
   13.24  
   13.25 -  sexp_case_def	
   13.26 +  sexp_case_def 
   13.27     "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
   13.28                              | (? k.   M=Numb(k) & z=d(k))  
   13.29                              | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
   13.30 @@ -35,6 +35,6 @@
   13.31       "pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"
   13.32  
   13.33    sexp_rec_def
   13.34 -   "sexp_rec M c d e == wfrec pred_sexp M  
   13.35 -             (%M g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)) M)"
   13.36 +   "sexp_rec M c d e == wfrec pred_sexp
   13.37 +             (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
   13.38  end
    14.1 --- a/src/HOL/Sum.thy	Mon Feb 05 14:44:09 1996 +0100
    14.2 +++ b/src/HOL/Sum.thy	Mon Feb 05 21:27:16 1996 +0100
    14.3 @@ -18,7 +18,7 @@
    14.4    Inl_Rep_def   "Inl_Rep == (%a. %x y p. x=a & p)"
    14.5    Inr_Rep_def   "Inr_Rep == (%b. %x y p. y=b & ~p)"
    14.6  
    14.7 -subtype (Sum)
    14.8 +typedef (Sum)
    14.9    ('a, 'b) "+"          (infixr 10)
   14.10      = "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}"
   14.11  
    15.1 --- a/src/HOL/Trancl.thy	Mon Feb 05 14:44:09 1996 +0100
    15.2 +++ b/src/HOL/Trancl.thy	Mon Feb 05 21:27:16 1996 +0100
    15.3 @@ -1,6 +1,6 @@
    15.4 -(*  Title: 	HOL/Trancl.thy
    15.5 +(*  Title:      HOL/Trancl.thy
    15.6      ID:         $Id$
    15.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    15.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.9      Copyright   1992  University of Cambridge
   15.10  
   15.11  Relfexive and Transitive closure of a relation
   15.12 @@ -12,13 +12,13 @@
   15.13  
   15.14  Trancl = Lfp + Relation + 
   15.15  consts
   15.16 -    rtrancl :: "('a * 'a)set => ('a * 'a)set"	("(_^*)" [100] 100)
   15.17 -    trancl  :: "('a * 'a)set => ('a * 'a)set"	("(_^+)" [100] 100)  
   15.18 +    rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [100] 100)
   15.19 +    trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [100] 100)  
   15.20  syntax
   15.21      reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [100] 100)
   15.22  defs   
   15.23 -  rtrancl_def	"r^*  ==  lfp(%s. id Un (r O s))"
   15.24 -  trancl_def	"r^+  ==  r O rtrancl(r)"
   15.25 +  rtrancl_def   "r^*  ==  lfp(%s. id Un (r O s))"
   15.26 +  trancl_def    "r^+  ==  r O rtrancl(r)"
   15.27  translations
   15.28                  "r^=" == "r Un id"
   15.29  end
    16.1 --- a/src/HOL/Univ.thy	Mon Feb 05 14:44:09 1996 +0100
    16.2 +++ b/src/HOL/Univ.thy	Mon Feb 05 21:27:16 1996 +0100
    16.3 @@ -15,7 +15,7 @@
    16.4  
    16.5  (** lists, trees will be sets of nodes **)
    16.6  
    16.7 -subtype (Node)
    16.8 +typedef (Node)
    16.9    'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
   16.10  
   16.11  types
    17.1 --- a/src/HOL/WF.ML	Mon Feb 05 14:44:09 1996 +0100
    17.2 +++ b/src/HOL/WF.ML	Mon Feb 05 21:27:16 1996 +0100
    17.3 @@ -1,9 +1,9 @@
    17.4 -(*  Title:      HOL/WF.ML
    17.5 +(*  Title:      HOL/wf.ML
    17.6      ID:         $Id$
    17.7 -    Author:     Tobias Nipkow
    17.8 -    Copyright   1992  University of Cambridge
    17.9 +    Author:     Tobias Nipkow, with minor changes by Konrad Slind
   17.10 +    Copyright   1992  University of Cambridge/1995 TU Munich
   17.11  
   17.12 -For WF.thy.  Well-founded Recursion
   17.13 +For WF.thy.  Wellfoundedness, induction, and  recursion
   17.14  *)
   17.15  
   17.16  open WF;
   17.17 @@ -48,7 +48,7 @@
   17.18  by (REPEAT (resolve_tac prems 1));
   17.19  qed "wf_anti_refl";
   17.20  
   17.21 -(*transitive closure of a WF relation is WF!*)
   17.22 +(*transitive closure of a wf relation is wf! *)
   17.23  val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
   17.24  by (rewtac wf_def);
   17.25  by (strip_tac 1);
   17.26 @@ -69,41 +69,32 @@
   17.27    H_cong to expose the equality*)
   17.28  goalw WF.thy [cut_def]
   17.29      "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
   17.30 -by(simp_tac (!simpset addsimps [expand_fun_eq]
   17.31 -                        setloop (split_tac [expand_if])) 1);
   17.32 -qed "cut_cut_eq";
   17.33 +by(simp_tac (HOL_ss addsimps [expand_fun_eq]
   17.34 +                    setloop (split_tac [expand_if])) 1);
   17.35 +qed "cuts_eq";
   17.36  
   17.37  goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
   17.38 -by(Asm_simp_tac 1);
   17.39 +by(asm_simp_tac HOL_ss 1);
   17.40  qed "cut_apply";
   17.41  
   17.42 -
   17.43  (*** is_recfun ***)
   17.44  
   17.45  goalw WF.thy [is_recfun_def,cut_def]
   17.46 -    "!!f. [| is_recfun r a H f;  ~(b,a):r |] ==> f(b) = (@z.True)";
   17.47 +    "!!f. [| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = (@z.True)";
   17.48  by (etac ssubst 1);
   17.49 -by(Asm_simp_tac 1);
   17.50 +by(asm_simp_tac HOL_ss 1);
   17.51  qed "is_recfun_undef";
   17.52  
   17.53 -(*eresolve_tac transD solves (a,b):r using transitivity AT MOST ONCE
   17.54 -  mp amd allE  instantiate induction hypotheses*)
   17.55 -fun indhyp_tac hyps =
   17.56 -    ares_tac (TrueI::hyps) ORELSE' 
   17.57 -    (cut_facts_tac hyps THEN'
   17.58 -       DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
   17.59 -                        eresolve_tac [transD, mp, allE]));
   17.60 -
   17.61  (*** NOTE! some simplifications need a different finish_tac!! ***)
   17.62  fun indhyp_tac hyps =
   17.63      resolve_tac (TrueI::refl::hyps) ORELSE' 
   17.64      (cut_facts_tac hyps THEN'
   17.65         DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
   17.66                          eresolve_tac [transD, mp, allE]));
   17.67 -val wf_super_ss = !simpset setsolver indhyp_tac;
   17.68 +val wf_super_ss = HOL_ss setsolver indhyp_tac;
   17.69  
   17.70  val prems = goalw WF.thy [is_recfun_def,cut_def]
   17.71 -    "[| wf(r);  trans(r);  is_recfun r a H f;  is_recfun r b H g |] ==> \
   17.72 +    "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \
   17.73      \ (x,a):r --> (x,b):r --> f(x)=g(x)";
   17.74  by (cut_facts_tac prems 1);
   17.75  by (etac wf_induct 1);
   17.76 @@ -115,7 +106,7 @@
   17.77  
   17.78  val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]
   17.79      "[| wf(r);  trans(r); \
   17.80 -\       is_recfun r a H f;  is_recfun r b H g;  (b,a):r |] ==> \
   17.81 +\       is_recfun r H a f;  is_recfun r H b g;  (b,a):r |] ==> \
   17.82  \    cut f r b = g";
   17.83  val gundef = recgb RS is_recfun_undef
   17.84  and fisg   = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
   17.85 @@ -128,70 +119,112 @@
   17.86  (*** Main Existence Lemma -- Basic Properties of the_recfun ***)
   17.87  
   17.88  val prems = goalw WF.thy [the_recfun_def]
   17.89 -    "is_recfun r a H f ==> is_recfun r a H (the_recfun r a H)";
   17.90 -by (res_inst_tac [("P", "is_recfun r a H")] selectI 1);
   17.91 +    "is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)";
   17.92 +by (res_inst_tac [("P", "is_recfun r H a")] selectI 1);
   17.93  by (resolve_tac prems 1);
   17.94  qed "is_the_recfun";
   17.95  
   17.96  val prems = goal WF.thy
   17.97 -    "[| wf(r);  trans(r) |] ==> is_recfun r a H (the_recfun r a H)";
   17.98 -by (cut_facts_tac prems 1);
   17.99 -by (wf_ind_tac "a" prems 1);
  17.100 -by (res_inst_tac [("f", "cut (%y. wftrec r y H) r a1")] is_the_recfun 1);
  17.101 -by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
  17.102 -by (rtac (cut_cut_eq RS ssubst) 1);
  17.103 -(*Applying the substitution: must keep the quantified assumption!!*)
  17.104 -by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac,
  17.105 -            etac (mp RS ssubst), atac]);
  17.106 -by (fold_tac [is_recfun_def]);
  17.107 -by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cut_cut_eq]) 1);
  17.108 + "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
  17.109 +  by (cut_facts_tac prems 1);
  17.110 +  by (wf_ind_tac "a" prems 1);
  17.111 +  by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
  17.112 +                   is_the_recfun 1);
  17.113 +  by (rewrite_goals_tac [is_recfun_def]);
  17.114 +  by (rtac (cuts_eq RS ssubst) 1);
  17.115 +  by (rtac allI 1);
  17.116 +  by (rtac impI 1);
  17.117 +  by (res_inst_tac [("f1","H"),("x","y")](arg_cong RS fun_cong) 1);
  17.118 +  by (subgoal_tac
  17.119 +         "the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1);
  17.120 +  by (etac allE 2);
  17.121 +  by (dtac impE 2);
  17.122 +  by (atac 2);
  17.123 +  by (atac 3);
  17.124 +  by (atac 2);
  17.125 +  by (etac ssubst 1);
  17.126 +  by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
  17.127 +  by (rtac allI 1);
  17.128 +  by (rtac impI 1);
  17.129 +  by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
  17.130 +  by (res_inst_tac [("f1","H"),("x","ya")](arg_cong RS fun_cong) 1);
  17.131 +  by (fold_tac [is_recfun_def]);
  17.132 +  by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
  17.133  qed "unfold_the_recfun";
  17.134  
  17.135 -
  17.136 -(*Beware incompleteness of unification!*)
  17.137 -val prems = goal WF.thy
  17.138 -    "[| wf(r);  trans(r);  (c,a):r;  (c,b):r |] \
  17.139 -\    ==> the_recfun r a H c = the_recfun r b H c";
  17.140 -by (DEPTH_SOLVE (ares_tac (prems@[is_recfun_equal,unfold_the_recfun]) 1));
  17.141 -qed "the_recfun_equal";
  17.142 -
  17.143 -val prems = goal WF.thy
  17.144 -    "[| wf(r); trans(r); (b,a):r |] \
  17.145 -\    ==> cut (the_recfun r a H) r b = the_recfun r b H";
  17.146 -by (REPEAT (ares_tac (prems@[is_recfun_cut,unfold_the_recfun]) 1));
  17.147 -qed "the_recfun_cut";
  17.148 -
  17.149 -(*** Unfolding wftrec ***)
  17.150 +val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun;
  17.151  
  17.152 -goalw WF.thy [wftrec_def]
  17.153 -    "!!r. [| wf(r);  trans(r) |] ==> \
  17.154 -\    wftrec r a H = H a (cut (%x.wftrec r x H) r a)";
  17.155 -by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun),
  17.156 -            REPEAT o atac, rtac H_cong1]);
  17.157 -by (asm_simp_tac (!simpset addsimps [cut_cut_eq,the_recfun_cut]) 1);
  17.158 -qed "wftrec";
  17.159 -
  17.160 -(*Unused but perhaps interesting*)
  17.161 +(*--------------Old proof-----------------------------------------------------
  17.162  val prems = goal WF.thy
  17.163 -    "[| wf(r);  trans(r);  !!f x. H x (cut f r x) = H x f |] ==> \
  17.164 -\               wftrec r a H = H a (%x.wftrec r x H)";
  17.165 -by (rtac (wftrec RS trans) 1);
  17.166 -by (REPEAT (resolve_tac prems 1));
  17.167 -qed "wftrec2";
  17.168 +    "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
  17.169 +by (cut_facts_tac prems 1);
  17.170 +by (wf_ind_tac "a" prems 1);
  17.171 +by (res_inst_tac [("f", "cut (%y. wftrec r H y) r a1")] is_the_recfun 1); 
  17.172 +by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
  17.173 +by (rtac (cuts_eq RS ssubst) 1);
  17.174 +(*Applying the substitution: must keep the quantified assumption!!*)
  17.175 +by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac,
  17.176 +            etac (mp RS ssubst), atac]); 
  17.177 +by (fold_tac [is_recfun_def]);
  17.178 +by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1);
  17.179 +qed "unfold_the_recfun";
  17.180 +---------------------------------------------------------------------------*)
  17.181  
  17.182  (** Removal of the premise trans(r) **)
  17.183 +val th = rewrite_rule[is_recfun_def]
  17.184 +                     (trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun)));
  17.185  
  17.186  goalw WF.thy [wfrec_def]
  17.187 -    "!!r. wf(r) ==> wfrec r a H = H a (cut (%x.wfrec r x H) r a)";
  17.188 +    "!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
  17.189 +by (rtac H_cong 1);
  17.190 +by (rtac refl 2);
  17.191 +by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
  17.192 +by (rtac allI 1);
  17.193 +by (rtac impI 1);
  17.194 +by (simp_tac(HOL_ss addsimps [wfrec_def]) 1);
  17.195 +by (res_inst_tac [("a1","a")] (th RS ssubst) 1);
  17.196 +by (atac 1);
  17.197 +by (forward_tac[wf_trancl] 1);
  17.198 +by (forward_tac[r_into_trancl] 1);
  17.199 +by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1);
  17.200 +by (rtac H_cong 1);    (*expose the equality of cuts*)
  17.201 +by (rtac refl 2);
  17.202 +by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1);
  17.203 +by (strip_tac 1);
  17.204 +by (res_inst_tac [("r2","r^+")] (is_recfun_equal_lemma RS mp RS mp) 1);
  17.205 +by (atac 1);
  17.206 +by (rtac trans_trancl 1);
  17.207 +by (rtac unfold_the_recfun 1);
  17.208 +by (atac 1);
  17.209 +by (rtac trans_trancl 1);
  17.210 +by (rtac unfold_the_recfun 1);
  17.211 +by (atac 1);
  17.212 +by (rtac trans_trancl 1);
  17.213 +by (rtac transD 1);
  17.214 +by (rtac trans_trancl 1);
  17.215 +by (forw_inst_tac [("a","ya")] r_into_trancl 1);
  17.216 +by (atac 1);
  17.217 +by (atac 1);
  17.218 +by (forw_inst_tac [("a","ya")] r_into_trancl 1);
  17.219 +by (atac 1);
  17.220 +qed "wfrec";
  17.221 +
  17.222 +(*--------------Old proof-----------------------------------------------------
  17.223 +goalw WF.thy [wfrec_def]
  17.224 +    "!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
  17.225  by (etac (wf_trancl RS wftrec RS ssubst) 1);
  17.226  by (rtac trans_trancl 1);
  17.227  by (rtac (refl RS H_cong) 1);    (*expose the equality of cuts*)
  17.228 -by (simp_tac (!simpset addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1);
  17.229 +by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1);
  17.230  qed "wfrec";
  17.231 +---------------------------------------------------------------------------*)
  17.232  
  17.233 -(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
  17.234 +(*---------------------------------------------------------------------------
  17.235 + * This form avoids giant explosions in proofs.  NOTE USE OF == 
  17.236 + *---------------------------------------------------------------------------*)
  17.237  val rew::prems = goal WF.thy
  17.238 -    "[| !!x. f(x)==wfrec r x H;  wf(r) |] ==> f(a) = H a (cut (%x.f(x)) r a)";
  17.239 +    "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a";
  17.240  by (rewtac rew);
  17.241  by (REPEAT (resolve_tac (prems@[wfrec]) 1));
  17.242  qed "def_wfrec";
  17.243 +
    18.1 --- a/src/HOL/WF.thy	Mon Feb 05 14:44:09 1996 +0100
    18.2 +++ b/src/HOL/WF.thy	Mon Feb 05 21:27:16 1996 +0100
    18.3 @@ -1,6 +1,6 @@
    18.4 -(*  Title: 	HOL/WF.thy
    18.5 +(*  Title:      HOL/wf.ML
    18.6      ID:         $Id$
    18.7 -    Author: 	Tobias Nipkow
    18.8 +    Author:     Tobias Nipkow
    18.9      Copyright   1992  University of Cambridge
   18.10  
   18.11  Well-founded Recursion
   18.12 @@ -8,23 +8,22 @@
   18.13  
   18.14  WF = Trancl +
   18.15  consts
   18.16 -   wf		:: "('a * 'a)set => bool"
   18.17 -   cut		:: "['a => 'b, ('a * 'a)set, 'a] => 'a => 'b"
   18.18 -   wftrec,wfrec	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'b"
   18.19 -   is_recfun	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b, 'a=>'b] => bool"
   18.20 -   the_recfun	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b"
   18.21 + wf         :: "('a * 'a)set => bool"
   18.22 + cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
   18.23 + is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
   18.24 + the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
   18.25 + wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
   18.26  
   18.27  defs
   18.28    wf_def  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
   18.29    
   18.30 -  cut_def 	 "cut f r x == (%y. if (y,x):r then f y else @z.True)"
   18.31 +  cut_def        "cut f r x == (%y. if (y,x):r then f y else @z.True)"
   18.32  
   18.33 -  is_recfun_def  "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)"
   18.34 -
   18.35 -  the_recfun_def "the_recfun r a H == (@f.is_recfun r a H f)"
   18.36 +  is_recfun_def  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
   18.37  
   18.38 -  wftrec_def     "wftrec r a H == H a (the_recfun r a H)"
   18.39 +  the_recfun_def "the_recfun r H a  == (@f. is_recfun r H a f)"
   18.40  
   18.41 -  (*version not requiring transitivity*)
   18.42 -  wfrec_def	"wfrec r a H == wftrec (trancl r) a (%x f.(H x (cut f r x)))"
   18.43 +  wfrec_def
   18.44 +    "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
   18.45 +                              r x)  x)"
   18.46  end
    19.1 --- a/src/HOL/equalities.thy	Mon Feb 05 14:44:09 1996 +0100
    19.2 +++ b/src/HOL/equalities.thy	Mon Feb 05 21:27:16 1996 +0100
    19.3 @@ -1,6 +1,6 @@
    19.4 -(*  Title: 	HOL/equalities
    19.5 +(*  Title:      HOL/equalities
    19.6      ID:         $Id$
    19.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    19.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.9      Copyright   1994  University of Cambridge
   19.10  
   19.11  Equalities involving union, intersection, inclusion, etc.
    20.1 --- a/src/HOL/mono.thy	Mon Feb 05 14:44:09 1996 +0100
    20.2 +++ b/src/HOL/mono.thy	Mon Feb 05 21:27:16 1996 +0100
    20.3 @@ -1,6 +1,6 @@
    20.4 -(*  Title: 	HOL/mono.thy
    20.5 +(*  Title:      HOL/mono.thy
    20.6      ID:         $Id$
    20.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    20.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    20.9      Copyright   1991  University of Cambridge
   20.10  
   20.11  *)
    21.1 --- a/src/HOL/subset.thy	Mon Feb 05 14:44:09 1996 +0100
    21.2 +++ b/src/HOL/subset.thy	Mon Feb 05 21:27:16 1996 +0100
    21.3 @@ -1,6 +1,6 @@
    21.4 -(*  Title: 	HOL/subset.thy
    21.5 +(*  Title:      HOL/subset.thy
    21.6      ID:         $Id$
    21.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    21.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    21.9      Copyright   1994  University of Cambridge
   21.10  *)
   21.11  
    22.1 --- a/src/HOL/thy_syntax.ML	Mon Feb 05 14:44:09 1996 +0100
    22.2 +++ b/src/HOL/thy_syntax.ML	Mon Feb 05 21:27:16 1996 +0100
    22.3 @@ -17,9 +17,9 @@
    22.4  open ThyParse;
    22.5  
    22.6  
    22.7 -(** subtype **)
    22.8 +(** typedef **)
    22.9  
   22.10 -fun mk_subtype_decl (((((opt_name, vs), t), mx), rhs), wt) =
   22.11 +fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
   22.12    let
   22.13      val name' = if_none opt_name t;
   22.14      val name = strip_quotes name';
   22.15 @@ -29,10 +29,10 @@
   22.16          "Abs_" ^ name ^ "_inverse"])
   22.17    end;
   22.18  
   22.19 -val subtype_decl =
   22.20 +val typedef_decl =
   22.21    optional ("(" $$-- name --$$ ")" >> Some) None --
   22.22    type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
   22.23 -  >> mk_subtype_decl;
   22.24 +  >> mk_typedef_decl;
   22.25  
   22.26  
   22.27  
   22.28 @@ -191,7 +191,7 @@
   22.29  val user_keywords = ["intrs", "monos", "con_defs", "|"];
   22.30  
   22.31  val user_sections =
   22.32 - [axm_section "subtype" "|> Subtype.add_subtype" subtype_decl,
   22.33 + [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
   22.34    ("inductive", inductive_decl ""),
   22.35    ("coinductive", inductive_decl "Co"),
   22.36    ("datatype", datatype_decl),
    23.1 --- a/src/HOL/typedef.ML	Mon Feb 05 14:44:09 1996 +0100
    23.2 +++ b/src/HOL/typedef.ML	Mon Feb 05 21:27:16 1996 +0100
    23.3 @@ -1,20 +1,20 @@
    23.4 -(*  Title:      HOL/subtype.ML
    23.5 +(*  Title:      HOL/typedef.ML
    23.6      ID:         $Id$
    23.7      Author:     Markus Wenzel, TU Muenchen
    23.8  
    23.9 -Internal interface for subtype definitions.
   23.10 +Internal interface for typedef definitions.
   23.11  *)
   23.12  
   23.13 -signature SUBTYPE =
   23.14 +signature TYPEDEF =
   23.15  sig
   23.16    val prove_nonempty: cterm -> thm list -> tactic option -> thm
   23.17 -  val add_subtype: string -> string * string list * mixfix ->
   23.18 +  val add_typedef: string -> string * string list * mixfix ->
   23.19      string -> string list -> thm list -> tactic option -> theory -> theory
   23.20 -  val add_subtype_i: string -> string * string list * mixfix ->
   23.21 +  val add_typedef_i: string -> string * string list * mixfix ->
   23.22      term -> string list -> thm list -> tactic option -> theory -> theory
   23.23  end;
   23.24  
   23.25 -structure Subtype: SUBTYPE =
   23.26 +structure Typedef: TYPEDEF =
   23.27  struct
   23.28  
   23.29  open Syntax Logic HOLogic;
   23.30 @@ -41,11 +41,11 @@
   23.31      error ("Failed to prove non-emptyness of " ^ quote (string_of_cterm cset));
   23.32  
   23.33  
   23.34 -(* ext_subtype *)
   23.35 +(* ext_typedef *)
   23.36  
   23.37 -fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
   23.38 +fun ext_typedef prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
   23.39    let
   23.40 -    val dummy = require_thy thy "Set" "subtype definitions";
   23.41 +    val dummy = require_thy thy "Set" "typedef definitions";
   23.42      val sign = sign_of thy;
   23.43  
   23.44      (*rhs*)
   23.45 @@ -122,7 +122,7 @@
   23.46        (Abs_name ^ "_inverse", abs_type_inv)]
   23.47    end
   23.48    handle ERROR =>
   23.49 -    error ("The error(s) above occurred in subtype definition " ^ quote name);
   23.50 +    error ("The error(s) above occurred in typedef definition " ^ quote name);
   23.51  
   23.52  
   23.53  (* external interfaces *)
   23.54 @@ -133,8 +133,8 @@
   23.55  fun read_term sg str =
   23.56    read_cterm sg (str, termTVar);
   23.57  
   23.58 -val add_subtype = ext_subtype read_term;
   23.59 -val add_subtype_i = ext_subtype cert_term;
   23.60 +val add_typedef = ext_typedef read_term;
   23.61 +val add_typedef_i = ext_typedef cert_term;
   23.62  
   23.63  
   23.64  end;