Adapted to new datatype package.
authorberghofe
Fri Jul 24 13:03:20 1998 +0200 (1998-07-24)
changeset 518389f162de39cf
parent 5182 69917bbbce45
child 5184 9b8547a9496a
Adapted to new datatype package.
src/HOL/Arith.ML
src/HOL/Arith.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/Hoare/Arith2.thy
src/HOL/Hoare/Examples.ML
src/HOL/Hoare/Hoare.ML
src/HOL/Hoare/Hoare.thy
src/HOL/IMP/Com.thy
src/HOL/IMP/Denotation.ML
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Expr.ML
src/HOL/IMP/Expr.thy
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Transition.ML
src/HOL/IMP/VC.ML
src/HOL/IMP/VC.thy
src/HOL/IsaMakefile
src/HOL/List.ML
src/HOL/List.thy
src/HOL/Map.ML
src/HOL/Map.thy
src/HOL/Option.ML
src/HOL/Option.thy
src/HOL/Power.thy
src/HOL/ROOT.ML
src/HOL/RelPow.ML
src/HOL/RelPow.thy
src/HOL/Sum.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Jul 24 13:02:01 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Jul 24 13:03:20 1998 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4     However, none of the generalizations are currently in the simpset,
     1.5     and I dread to think what happens if I put them in *)
     1.6  Goal "0 < n ==> Suc(n-1) = n";
     1.7 -by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1);
     1.8 +by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
     1.9  qed "Suc_pred";
    1.10  Addsimps [Suc_pred];
    1.11  
    1.12 @@ -114,7 +114,7 @@
    1.13  Goal "0<n ==> m + (n-1) = (m+n)-1";
    1.14  by (exhaust_tac "m" 1);
    1.15  by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
    1.16 -                                      addsplits [split_nat_case])));
    1.17 +                                      addsplits [nat.split])));
    1.18  qed "add_pred";
    1.19  Addsimps [add_pred];
    1.20  
    1.21 @@ -373,7 +373,7 @@
    1.22  Addsimps [Suc_diff_diff];
    1.23  
    1.24  Goal "0<n ==> n - Suc i < n";
    1.25 -by (res_inst_tac [("n","n")] natE 1);
    1.26 +by (exhaust_tac "n" 1);
    1.27  by Safe_tac;
    1.28  by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1);
    1.29  qed "diff_Suc_less";
    1.30 @@ -670,8 +670,8 @@
    1.31  Goal "!!n::nat. m<=n ==> (l-n) <= (l-m)";
    1.32  by (induct_tac "l" 1);
    1.33  by (Simp_tac 1);
    1.34 -by (case_tac "n <= l" 1);
    1.35 -by (subgoal_tac "m <= l" 1);
    1.36 +by (case_tac "n <= na" 1);
    1.37 +by (subgoal_tac "m <= na" 1);
    1.38  by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
    1.39  by (fast_tac (claset() addEs [le_trans]) 1);
    1.40  by (dtac not_leE 1);
     2.1 --- a/src/HOL/Arith.thy	Fri Jul 24 13:02:01 1998 +0200
     2.2 +++ b/src/HOL/Arith.thy	Fri Jul 24 13:03:20 1998 +0200
     2.3 @@ -14,15 +14,15 @@
     2.4  (* size of a datatype value; overloaded *)
     2.5  consts size :: 'a => nat
     2.6  
     2.7 -primrec "op +" nat 
     2.8 +primrec
     2.9    add_0    "0 + n = n"
    2.10    add_Suc  "Suc m + n = Suc(m + n)"
    2.11  
    2.12 -primrec "op -" nat 
    2.13 +primrec
    2.14    diff_0   "m - 0 = m"
    2.15    diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    2.16  
    2.17 -primrec "op *"  nat 
    2.18 +primrec
    2.19    mult_0   "0 * n = 0"
    2.20    mult_Suc "Suc m * n = n + (m * n)"
    2.21  
     3.1 --- a/src/HOL/Auth/Event.thy	Fri Jul 24 13:02:01 1998 +0200
     3.2 +++ b/src/HOL/Auth/Event.thy	Fri Jul 24 13:03:20 1998 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4    Spy_in_bad     "Spy: bad"
     3.5    Server_not_bad "Server ~: bad"
     3.6  
     3.7 -primrec spies list
     3.8 +primrec
     3.9             (*Spy reads all traffic whether addressed to him or not*)
    3.10    spies_Nil   "spies []       = initState Spy"
    3.11    spies_Cons  "spies (ev # evs) =
    3.12 @@ -43,7 +43,7 @@
    3.13      complement of the set of fresh items*)
    3.14    used :: event list => msg set
    3.15  
    3.16 -primrec used list
    3.17 +primrec
    3.18    used_Nil   "used []         = (UN B. parts (initState B))"
    3.19    used_Cons  "used (ev # evs) =
    3.20  	         (case ev of
     4.1 --- a/src/HOL/Auth/Message.thy	Fri Jul 24 13:02:01 1998 +0200
     4.2 +++ b/src/HOL/Auth/Message.thy	Fri Jul 24 13:03:20 1998 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  Inductive relations "parts", "analz" and "synth"
     4.5  *)
     4.6  
     4.7 -Message = Arith + Inductive +
     4.8 +Message = Datatype +
     4.9  
    4.10  (*Is there a difference between a nonce and arbitrary numerical data?
    4.11    Do we need a type of nonces?*)
     5.1 --- a/src/HOL/Auth/Public.thy	Fri Jul 24 13:02:01 1998 +0200
     5.2 +++ b/src/HOL/Auth/Public.thy	Fri Jul 24 13:03:20 1998 +0200
     5.3 @@ -19,7 +19,7 @@
     5.4  translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
     5.5    "priK x"  == "invKey(pubK x)"
     5.6  
     5.7 -primrec initState agent
     5.8 +primrec
     5.9          (*Agents know their private key and all public keys*)
    5.10    initState_Server  "initState Server     =    
    5.11   		         insert (Key (priK Server)) (Key `` range pubK)"
     6.1 --- a/src/HOL/Auth/Shared.thy	Fri Jul 24 13:02:01 1998 +0200
     6.2 +++ b/src/HOL/Auth/Shared.thy	Fri Jul 24 13:03:20 1998 +0200
     6.3 @@ -17,7 +17,7 @@
     6.4    isSym_keys "isSymKey K"	(*All keys are symmetric*)
     6.5    inj_shrK   "inj shrK"		(*No two agents have the same long-term key*)
     6.6  
     6.7 -primrec initState agent
     6.8 +primrec
     6.9          (*Server knows all long-term keys; other agents know only their own*)
    6.10    initState_Server  "initState Server     = Key `` range shrK"
    6.11    initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
     7.1 --- a/src/HOL/Divides.ML	Fri Jul 24 13:02:01 1998 +0200
     7.2 +++ b/src/HOL/Divides.ML	Fri Jul 24 13:03:20 1998 +0200
     7.3 @@ -92,7 +92,7 @@
     7.4  Goal "0<n ==> m*n mod n = 0";
     7.5  by (induct_tac "m" 1);
     7.6  by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
     7.7 -by (dres_inst_tac [("m","m*n")] mod_add_self2 1);
     7.8 +by (dres_inst_tac [("m","na*n")] mod_add_self2 1);
     7.9  by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
    7.10  qed "mod_mult_self_is_0";
    7.11  Addsimps [mod_mult_self_is_0];
     8.1 --- a/src/HOL/Finite.ML	Fri Jul 24 13:02:01 1998 +0200
     8.2 +++ b/src/HOL/Finite.ML	Fri Jul 24 13:03:20 1998 +0200
     8.3 @@ -214,7 +214,7 @@
     8.4  Goal
     8.5    "[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
     8.6  \  ? m::nat. m<n & (? g. A = {g i|i. i<m})";
     8.7 -by (res_inst_tac [("n","n")] natE 1);
     8.8 +by (exhaust_tac "n" 1);
     8.9   by (hyp_subst_tac 1);
    8.10   by (Asm_full_simp_tac 1);
    8.11  by (rename_tac "m" 1);
     9.1 --- a/src/HOL/Hoare/Arith2.thy	Fri Jul 24 13:02:01 1998 +0200
     9.2 +++ b/src/HOL/Hoare/Arith2.thy	Fri Jul 24 13:03:20 1998 +0200
     9.3 @@ -16,8 +16,9 @@
     9.4    "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
     9.5  
     9.6  consts fac     :: nat => nat
     9.7 -primrec fac nat
     9.8 -"fac 0 = Suc 0"
     9.9 -"fac(Suc n) = (Suc n)*fac(n)"
    9.10 +
    9.11 +primrec
    9.12 +  "fac 0 = Suc 0"
    9.13 +  "fac(Suc n) = (Suc n)*fac(n)"
    9.14  
    9.15  end
    10.1 --- a/src/HOL/Hoare/Examples.ML	Fri Jul 24 13:02:01 1998 +0200
    10.2 +++ b/src/HOL/Hoare/Examples.ML	Fri Jul 24 13:03:20 1998 +0200
    10.3 @@ -65,7 +65,7 @@
    10.4  
    10.5  by (hoare_tac 1);
    10.6  
    10.7 -by (res_inst_tac [("n","b")] natE 1);
    10.8 +by (exhaust_tac "b" 1);
    10.9  by (hyp_subst_tac 1);
   10.10  by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
   10.11  by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);
   10.12 @@ -86,7 +86,7 @@
   10.13  
   10.14  by (hoare_tac 1);
   10.15  by Safe_tac;
   10.16 -by (res_inst_tac [("n","a")] natE 1);
   10.17 +by (exhaust_tac "a" 1);
   10.18  by (ALLGOALS
   10.19      (asm_simp_tac
   10.20       (simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
    11.1 --- a/src/HOL/Hoare/Hoare.ML	Fri Jul 24 13:02:01 1998 +0200
    11.2 +++ b/src/HOL/Hoare/Hoare.ML	Fri Jul 24 13:03:20 1998 +0200
    11.3 @@ -44,7 +44,7 @@
    11.4    (fn [prem1,prem2] =>
    11.5       [REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2,
    11.6        etac thin_rl 1, res_inst_tac[("x","s")]spec 1,
    11.7 -      res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
    11.8 +      res_inst_tac[("x","s'")]spec 1, induct_tac "n" 1,
    11.9        Simp_tac 1,
   11.10        fast_tac (claset() addIs [prem2]) 1,
   11.11        simp_tac (simpset() addsimps [Seq_def]) 1,
    12.1 --- a/src/HOL/Hoare/Hoare.thy	Fri Jul 24 13:02:01 1998 +0200
    12.2 +++ b/src/HOL/Hoare/Hoare.thy	Fri Jul 24 13:03:20 1998 +0200
    12.3 @@ -47,7 +47,8 @@
    12.4  
    12.5  consts
    12.6    Iter          :: [nat, 'a bexp, 'a com] => 'a com
    12.7 -primrec Iter nat
    12.8 +
    12.9 +primrec
   12.10    "Iter 0 b c = (%s s'.~b(s) & (s=s'))"
   12.11    "Iter (Suc n) b c = (%s s'. b(s) & Seq c (Iter n b c) s s')"
   12.12  
    13.1 --- a/src/HOL/IMP/Com.thy	Fri Jul 24 13:02:01 1998 +0200
    13.2 +++ b/src/HOL/IMP/Com.thy	Fri Jul 24 13:03:20 1998 +0200
    13.3 @@ -7,7 +7,7 @@
    13.4  Syntax of commands
    13.5  *)
    13.6  
    13.7 -Com = Arith +
    13.8 +Com = Datatype +
    13.9  
   13.10  types 
   13.11        val
    14.1 --- a/src/HOL/IMP/Denotation.ML	Fri Jul 24 13:02:01 1998 +0200
    14.2 +++ b/src/HOL/IMP/Denotation.ML	Fri Jul 24 13:03:20 1998 +0200
    14.3 @@ -42,7 +42,7 @@
    14.4  (* Denotational Semantics implies Operational Semantics *)
    14.5  
    14.6  Goal "!s t. (s,t):C(c) --> <c,s> -c-> t";
    14.7 -by (com.induct_tac "c" 1);
    14.8 +by (induct_tac "c" 1);
    14.9  
   14.10  by (ALLGOALS Full_simp_tac);
   14.11  by (ALLGOALS (TRY o Fast_tac));
    15.1 --- a/src/HOL/IMP/Denotation.thy	Fri Jul 24 13:02:01 1998 +0200
    15.2 +++ b/src/HOL/IMP/Denotation.thy	Fri Jul 24 13:03:20 1998 +0200
    15.3 @@ -18,7 +18,7 @@
    15.4  consts
    15.5    C     :: com => com_den
    15.6  
    15.7 -primrec C com
    15.8 +primrec
    15.9    C_skip    "C(SKIP) = id"
   15.10    C_assign  "C(x := a) = {(s,t). t = s[x:=a(s)]}"
   15.11    C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    16.1 --- a/src/HOL/IMP/Expr.ML	Fri Jul 24 13:02:01 1998 +0200
    16.2 +++ b/src/HOL/IMP/Expr.ML	Fri Jul 24 13:03:20 1998 +0200
    16.3 @@ -33,14 +33,14 @@
    16.4  \   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"];
    16.5  
    16.6  Goal "!n. ((a,s) -a-> n) = (A a s = n)";
    16.7 -by (aexp.induct_tac "a" 1);
    16.8 +by (induct_tac "a" 1);
    16.9  by (ALLGOALS 
   16.10      (fast_tac (claset() addSIs evala.intrs
   16.11  	                addSEs evala_elim_cases addss (simpset()))));
   16.12  qed_spec_mp "aexp_iff";
   16.13  
   16.14  Goal "!w. ((b,s) -b-> w) = (B b s = w)";
   16.15 -by (bexp.induct_tac "b" 1);
   16.16 +by (induct_tac "b" 1);
   16.17  by (ALLGOALS 
   16.18      (fast_tac (claset() 
   16.19  	       addss (simpset() addsimps (aexp_iff::evalb_simps)))));
    17.1 --- a/src/HOL/IMP/Expr.thy	Fri Jul 24 13:02:01 1998 +0200
    17.2 +++ b/src/HOL/IMP/Expr.thy	Fri Jul 24 13:03:20 1998 +0200
    17.3 @@ -7,7 +7,7 @@
    17.4  Not used in the rest of the language, but included for completeness.
    17.5  *)
    17.6  
    17.7 -Expr = Arith + Inductive +
    17.8 +Expr = Datatype +
    17.9  
   17.10  (** Arithmetic expressions **)
   17.11  types loc
   17.12 @@ -72,13 +72,13 @@
   17.13    A     :: aexp => state => nat
   17.14    B     :: bexp => state => bool
   17.15  
   17.16 -primrec A aexp
   17.17 +primrec
   17.18    "A(N(n)) = (%s. n)"
   17.19    "A(X(x)) = (%s. s(x))"
   17.20    "A(Op1 f a) = (%s. f(A a s))"
   17.21    "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
   17.22  
   17.23 -primrec B bexp
   17.24 +primrec
   17.25    "B(true) = (%s. True)"
   17.26    "B(false) = (%s. False)"
   17.27    "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    18.1 --- a/src/HOL/IMP/Hoare.ML	Fri Jul 24 13:02:01 1998 +0200
    18.2 +++ b/src/HOL/IMP/Hoare.ML	Fri Jul 24 13:03:20 1998 +0200
    18.3 @@ -91,7 +91,7 @@
    18.4  AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
    18.5  
    18.6  Goal "!Q. |- {wp c Q} c {Q}";
    18.7 -by (com.induct_tac "c" 1);
    18.8 +by (induct_tac "c" 1);
    18.9  by (ALLGOALS Simp_tac);
   18.10  by (REPEAT_FIRST Fast_tac);
   18.11  by (blast_tac (claset() addIs [hoare.conseq]) 1);
    19.1 --- a/src/HOL/IMP/Transition.ML	Fri Jul 24 13:02:01 1998 +0200
    19.2 +++ b/src/HOL/IMP/Transition.ML	Fri Jul 24 13:03:20 1998 +0200
    19.3 @@ -32,7 +32,7 @@
    19.4  Goal
    19.5    "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
    19.6  \              (c;d, s) -*-> (SKIP, u)";
    19.7 -by (nat_ind_tac "n" 1);
    19.8 +by (induct_tac "n" 1);
    19.9   by (fast_tac (claset() addIs [rtrancl_into_rtrancl2])1);
   19.10  by (fast_tac  (claset() addIs [rtrancl_into_rtrancl2]addSDs [rel_pow_Suc_D2])1);
   19.11  qed_spec_mp "lemma1";
    20.1 --- a/src/HOL/IMP/VC.ML	Fri Jul 24 13:02:01 1998 +0200
    20.2 +++ b/src/HOL/IMP/VC.ML	Fri Jul 24 13:03:20 1998 +0200
    20.3 @@ -13,7 +13,7 @@
    20.4  val lemma = prove_goal HOL.thy "!s. P s --> P s" (K[Fast_tac 1]);
    20.5  
    20.6  Goal "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}";
    20.7 -by (acom.induct_tac "c" 1);
    20.8 +by (induct_tac "c" 1);
    20.9      by (ALLGOALS Simp_tac);
   20.10      by (Fast_tac 1);
   20.11     by (Fast_tac 1);
   20.12 @@ -30,7 +30,7 @@
   20.13  qed "vc_sound";
   20.14  
   20.15  Goal "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)";
   20.16 -by (acom.induct_tac "c" 1);
   20.17 +by (induct_tac "c" 1);
   20.18      by (ALLGOALS Asm_simp_tac);
   20.19  by (EVERY1[rtac allI, rtac allI, rtac impI]);
   20.20  by (EVERY1[etac allE, etac allE, etac mp]);
   20.21 @@ -38,7 +38,7 @@
   20.22  qed_spec_mp "awp_mono";
   20.23  
   20.24  Goal "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
   20.25 -by (acom.induct_tac "c" 1);
   20.26 +by (induct_tac "c" 1);
   20.27      by (ALLGOALS Asm_simp_tac);
   20.28  by (safe_tac HOL_cs);
   20.29  by (EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
   20.30 @@ -70,6 +70,6 @@
   20.31  qed "vc_complete";
   20.32  
   20.33  Goal "!Q. vcawp c Q = (vc c Q, awp c Q)";
   20.34 -by (acom.induct_tac "c" 1);
   20.35 +by (induct_tac "c" 1);
   20.36  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def])));
   20.37  qed "vcawp_vc_awp";
    21.1 --- a/src/HOL/IMP/VC.thy	Fri Jul 24 13:02:01 1998 +0200
    21.2 +++ b/src/HOL/IMP/VC.thy	Fri Jul 24 13:03:20 1998 +0200
    21.3 @@ -21,14 +21,14 @@
    21.4    vcawp :: "acom => assn => assn * assn"
    21.5    astrip :: acom => com
    21.6  
    21.7 -primrec awp acom
    21.8 +primrec
    21.9    "awp Askip Q = Q"
   21.10    "awp (Aass x a) Q = (%s. Q(s[x:=a s]))"
   21.11    "awp (Asemi c d) Q = awp c (awp d Q)"
   21.12    "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
   21.13    "awp (Awhile b I c) Q = I"
   21.14  
   21.15 -primrec vc acom
   21.16 +primrec
   21.17    "vc Askip Q = (%s. True)"
   21.18    "vc (Aass x a) Q = (%s. True)"
   21.19    "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
   21.20 @@ -36,7 +36,7 @@
   21.21    "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
   21.22                                (I s & b s --> awp c I s) & vc c I s)"
   21.23  
   21.24 -primrec astrip acom
   21.25 +primrec
   21.26    "astrip Askip = SKIP"
   21.27    "astrip (Aass x a) = (x:=a)"
   21.28    "astrip (Asemi c d) = (astrip c;astrip d)"
   21.29 @@ -44,7 +44,7 @@
   21.30    "astrip (Awhile b I c) = (WHILE b DO astrip c)"
   21.31  
   21.32  (* simultaneous computation of vc and awp: *)
   21.33 -primrec vcawp acom
   21.34 +primrec
   21.35    "vcawp Askip Q = (%s. True, Q)"
   21.36    "vcawp (Aass x a) Q = (%s. True, %s. Q(s[x:=a s]))"
   21.37    "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
    22.1 --- a/src/HOL/IsaMakefile	Fri Jul 24 13:02:01 1998 +0200
    22.2 +++ b/src/HOL/IsaMakefile	Fri Jul 24 13:03:20 1998 +0200
    22.3 @@ -39,19 +39,23 @@
    22.4    $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \
    22.5    $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \
    22.6    $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \
    22.7 -  Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
    22.8 +  Arith.ML Arith.thy Datatype.thy \
    22.9 +  Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
   22.10    Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \
   22.11    Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/Integ.ML \
   22.12    Integ/Integ.thy Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML \
   22.13    Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
   22.14    Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
   22.15    RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
   22.16 -  String.ML String.thy Sum.ML Sum.thy Tools/inductive_package.ML Tools/record_package.ML \
   22.17 +  String.ML String.thy Sum.ML Sum.thy \
   22.18 +  Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
   22.19 +  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
   22.20 +  Tools/inductive_package.ML Tools/primrec_package.ML Tools/record_package.ML \
   22.21    Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
   22.22    Update.ML Update.thy Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
   22.23 -  WF_Rel.thy arith_data.ML cladata.ML datatype.ML equalities.ML \
   22.24 +  WF_Rel.thy arith_data.ML cladata.ML equalities.ML \
   22.25    equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
   22.26 -  subset.thy thy_data.ML thy_syntax.ML
   22.27 +  subset.thy thy_syntax.ML
   22.28  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
   22.29  
   22.30  
    23.1 --- a/src/HOL/List.ML	Fri Jul 24 13:02:01 1998 +0200
    23.2 +++ b/src/HOL/List.ML	Fri Jul 24 13:03:20 1998 +0200
    23.3 @@ -208,17 +208,17 @@
    23.4  
    23.5  Goal "xs ~= [] ==> hd(xs @ ys) = hd xs";
    23.6  by (asm_simp_tac (simpset() addsimps [hd_append]
    23.7 -                           addsplits [split_list_case]) 1);
    23.8 +                           addsplits [list.split]) 1);
    23.9  qed "hd_append2";
   23.10  Addsimps [hd_append2];
   23.11  
   23.12  Goal "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
   23.13 -by (simp_tac (simpset() addsplits [split_list_case]) 1);
   23.14 +by (simp_tac (simpset() addsplits [list.split]) 1);
   23.15  qed "tl_append";
   23.16  
   23.17  Goal "xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
   23.18  by (asm_simp_tac (simpset() addsimps [tl_append]
   23.19 -                           addsplits [split_list_case]) 1);
   23.20 +                           addsplits [list.split]) 1);
   23.21  qed "tl_append2";
   23.22  Addsimps [tl_append2];
   23.23  
   23.24 @@ -482,7 +482,7 @@
   23.25  
   23.26  Goal
   23.27    "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
   23.28 -by (nat_ind_tac "n" 1);
   23.29 +by (induct_tac "n" 1);
   23.30   by (Asm_simp_tac 1);
   23.31   by (rtac allI 1);
   23.32   by (exhaust_tac "xs" 1);
   23.33 @@ -495,7 +495,7 @@
   23.34  by (Asm_full_simp_tac 1);
   23.35  (* case x#xl *)
   23.36  by (rtac allI 1);
   23.37 -by (nat_ind_tac "n" 1);
   23.38 +by (induct_tac "n" 1);
   23.39  by (Auto_tac);
   23.40  qed_spec_mp "nth_map";
   23.41  Addsimps [nth_map];
   23.42 @@ -506,7 +506,7 @@
   23.43  by (Simp_tac 1);
   23.44  (* case x#xl *)
   23.45  by (rtac allI 1);
   23.46 -by (nat_ind_tac "n" 1);
   23.47 +by (induct_tac "n" 1);
   23.48  by (Auto_tac);
   23.49  qed_spec_mp "list_all_nth";
   23.50  
   23.51 @@ -516,7 +516,7 @@
   23.52  by (Simp_tac 1);
   23.53  (* case x#xl *)
   23.54  by (rtac allI 1);
   23.55 -by (nat_ind_tac "n" 1);
   23.56 +by (induct_tac "n" 1);
   23.57  (* case 0 *)
   23.58  by (Asm_full_simp_tac 1);
   23.59  (* case Suc x *)
   23.60 @@ -531,7 +531,7 @@
   23.61  Goal "!i. length(xs[i:=x]) = length xs";
   23.62  by (induct_tac "xs" 1);
   23.63  by (Simp_tac 1);
   23.64 -by (asm_full_simp_tac (simpset() addsplits [split_nat_case]) 1);
   23.65 +by (asm_full_simp_tac (simpset() addsplits [nat.split]) 1);
   23.66  qed_spec_mp "length_list_update";
   23.67  Addsimps [length_list_update];
   23.68  
   23.69 @@ -603,7 +603,7 @@
   23.70  Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
   23.71  
   23.72  Goal "!xs. length(take n xs) = min (length xs) n";
   23.73 -by (nat_ind_tac "n" 1);
   23.74 +by (induct_tac "n" 1);
   23.75   by (Auto_tac);
   23.76  by (exhaust_tac "xs" 1);
   23.77   by (Auto_tac);
   23.78 @@ -611,7 +611,7 @@
   23.79  Addsimps [length_take];
   23.80  
   23.81  Goal "!xs. length(drop n xs) = (length xs - n)";
   23.82 -by (nat_ind_tac "n" 1);
   23.83 +by (induct_tac "n" 1);
   23.84   by (Auto_tac);
   23.85  by (exhaust_tac "xs" 1);
   23.86   by (Auto_tac);
   23.87 @@ -619,14 +619,14 @@
   23.88  Addsimps [length_drop];
   23.89  
   23.90  Goal "!xs. length xs <= n --> take n xs = xs";
   23.91 -by (nat_ind_tac "n" 1);
   23.92 +by (induct_tac "n" 1);
   23.93   by (Auto_tac);
   23.94  by (exhaust_tac "xs" 1);
   23.95   by (Auto_tac);
   23.96  qed_spec_mp "take_all";
   23.97  
   23.98  Goal "!xs. length xs <= n --> drop n xs = []";
   23.99 -by (nat_ind_tac "n" 1);
  23.100 +by (induct_tac "n" 1);
  23.101   by (Auto_tac);
  23.102  by (exhaust_tac "xs" 1);
  23.103   by (Auto_tac);
  23.104 @@ -634,7 +634,7 @@
  23.105  
  23.106  Goal 
  23.107    "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
  23.108 -by (nat_ind_tac "n" 1);
  23.109 +by (induct_tac "n" 1);
  23.110   by (Auto_tac);
  23.111  by (exhaust_tac "xs" 1);
  23.112   by (Auto_tac);
  23.113 @@ -642,7 +642,7 @@
  23.114  Addsimps [take_append];
  23.115  
  23.116  Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
  23.117 -by (nat_ind_tac "n" 1);
  23.118 +by (induct_tac "n" 1);
  23.119   by (Auto_tac);
  23.120  by (exhaust_tac "xs" 1);
  23.121   by (Auto_tac);
  23.122 @@ -650,37 +650,37 @@
  23.123  Addsimps [drop_append];
  23.124  
  23.125  Goal "!xs n. take n (take m xs) = take (min n m) xs"; 
  23.126 -by (nat_ind_tac "m" 1);
  23.127 +by (induct_tac "m" 1);
  23.128   by (Auto_tac);
  23.129  by (exhaust_tac "xs" 1);
  23.130   by (Auto_tac);
  23.131 -by (exhaust_tac "n" 1);
  23.132 +by (exhaust_tac "na" 1);
  23.133   by (Auto_tac);
  23.134  qed_spec_mp "take_take";
  23.135  
  23.136  Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
  23.137 -by (nat_ind_tac "m" 1);
  23.138 +by (induct_tac "m" 1);
  23.139   by (Auto_tac);
  23.140  by (exhaust_tac "xs" 1);
  23.141   by (Auto_tac);
  23.142  qed_spec_mp "drop_drop";
  23.143  
  23.144  Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
  23.145 -by (nat_ind_tac "m" 1);
  23.146 +by (induct_tac "m" 1);
  23.147   by (Auto_tac);
  23.148  by (exhaust_tac "xs" 1);
  23.149   by (Auto_tac);
  23.150  qed_spec_mp "take_drop";
  23.151  
  23.152  Goal "!xs. take n (map f xs) = map f (take n xs)"; 
  23.153 -by (nat_ind_tac "n" 1);
  23.154 +by (induct_tac "n" 1);
  23.155   by (Auto_tac);
  23.156  by (exhaust_tac "xs" 1);
  23.157   by (Auto_tac);
  23.158  qed_spec_mp "take_map"; 
  23.159  
  23.160  Goal "!xs. drop n (map f xs) = map f (drop n xs)"; 
  23.161 -by (nat_ind_tac "n" 1);
  23.162 +by (induct_tac "n" 1);
  23.163   by (Auto_tac);
  23.164  by (exhaust_tac "xs" 1);
  23.165   by (Auto_tac);
  23.166 @@ -697,7 +697,7 @@
  23.167  Addsimps [nth_take];
  23.168  
  23.169  Goal  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
  23.170 -by (nat_ind_tac "n" 1);
  23.171 +by (induct_tac "n" 1);
  23.172   by (Auto_tac);
  23.173  by (exhaust_tac "xs" 1);
  23.174   by (Auto_tac);
  23.175 @@ -792,18 +792,18 @@
  23.176  val list_eq_pattern =
  23.177    read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
  23.178  
  23.179 -fun last (cons as Const("List.op #",_) $ _ $ xs) =
  23.180 -      (case xs of Const("List.[]",_) => cons | _ => last xs)
  23.181 -  | last (Const("List.op @",_) $ _ $ ys) = last ys
  23.182 +fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
  23.183 +      (case xs of Const("List.list.[]",_) => cons | _ => last xs)
  23.184 +  | last (Const("List.list.op @",_) $ _ $ ys) = last ys
  23.185    | last t = t;
  23.186  
  23.187 -fun list1 (Const("List.op #",_) $ _ $ Const("List.[]",_)) = true
  23.188 +fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
  23.189    | list1 _ = false;
  23.190  
  23.191 -fun butlast ((cons as Const("List.op #",_) $ x) $ xs) =
  23.192 -      (case xs of Const("List.[]",_) => xs | _ => cons $ butlast xs)
  23.193 -  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
  23.194 -  | butlast xs = Const("List.[]",fastype_of xs);
  23.195 +fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
  23.196 +      (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
  23.197 +  | butlast ((app as Const("List.list.op @",_) $ xs) $ ys) = app $ butlast ys
  23.198 +  | butlast xs = Const("List.list.[]",fastype_of xs);
  23.199  
  23.200  val rearr_tac =
  23.201    simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
  23.202 @@ -815,7 +815,7 @@
  23.203        let val lhs1 = butlast lhs and rhs1 = butlast rhs
  23.204            val Type(_,listT::_) = eqT
  23.205            val appT = [listT,listT] ---> listT
  23.206 -          val app = Const("List.op @",appT)
  23.207 +          val app = Const("List.list.op @",appT)
  23.208            val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
  23.209            val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
  23.210            val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
    24.1 --- a/src/HOL/List.thy	Fri Jul 24 13:02:01 1998 +0200
    24.2 +++ b/src/HOL/List.thy	Fri Jul 24 13:03:20 1998 +0200
    24.3 @@ -6,7 +6,7 @@
    24.4  The datatype of finite lists.
    24.5  *)
    24.6  
    24.7 -List = WF_Rel +
    24.8 +List = WF_Rel + Datatype +
    24.9  
   24.10  datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
   24.11  
   24.12 @@ -74,76 +74,76 @@
   24.13  syntax   length :: 'a list => nat
   24.14  translations  "length"  =>  "size:: _ list => nat"
   24.15  
   24.16 -primrec hd list
   24.17 +primrec
   24.18    "hd([]) = arbitrary"
   24.19    "hd(x#xs) = x"
   24.20 -primrec tl list
   24.21 +primrec
   24.22    "tl([]) = []"
   24.23    "tl(x#xs) = xs"
   24.24 -primrec last list
   24.25 +primrec
   24.26    "last [] = arbitrary"
   24.27    "last(x#xs) = (if xs=[] then x else last xs)"
   24.28 -primrec butlast list
   24.29 +primrec
   24.30    "butlast [] = []"
   24.31    "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
   24.32 -primrec "op mem" list
   24.33 +primrec
   24.34    "x mem [] = False"
   24.35    "x mem (y#ys) = (if y=x then True else x mem ys)"
   24.36 -primrec set list
   24.37 +primrec
   24.38    "set [] = {}"
   24.39    "set (x#xs) = insert x (set xs)"
   24.40 -primrec list_all list
   24.41 +primrec
   24.42    list_all_Nil  "list_all P [] = True"
   24.43    list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
   24.44 -primrec map list
   24.45 +primrec
   24.46    "map f [] = []"
   24.47    "map f (x#xs) = f(x)#map f xs"
   24.48 -primrec "op @" list
   24.49 -append_Nil  "[]    @ys = ys"
   24.50 -append_Cons "(x#xs)@ys = x#(xs@ys)"
   24.51 -primrec rev list
   24.52 +primrec
   24.53 +  append_Nil  "[]    @ys = ys"
   24.54 +  append_Cons "(x#xs)@ys = x#(xs@ys)"
   24.55 +primrec
   24.56    "rev([]) = []"
   24.57    "rev(x#xs) = rev(xs) @ [x]"
   24.58 -primrec filter list
   24.59 +primrec
   24.60    "filter P [] = []"
   24.61    "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
   24.62 -primrec foldl list
   24.63 +primrec
   24.64    "foldl f a [] = a"
   24.65    "foldl f a (x#xs) = foldl f (f a x) xs"
   24.66 -primrec concat list
   24.67 +primrec
   24.68    "concat([]) = []"
   24.69    "concat(x#xs) = x @ concat(xs)"
   24.70 -primrec drop list
   24.71 +primrec
   24.72    drop_Nil  "drop n [] = []"
   24.73    drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
   24.74 -primrec take list
   24.75 +primrec
   24.76    take_Nil  "take n [] = []"
   24.77    take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
   24.78 -primrec nth nat
   24.79 +primrec
   24.80    "xs!0 = hd xs"
   24.81    "xs!(Suc n) = (tl xs)!n"
   24.82 -primrec list_update list
   24.83 +primrec
   24.84   "    [][i:=v] = []"
   24.85   "(x#xs)[i:=v] = (case i of 0     => v # xs 
   24.86  			  | Suc j => x # xs[j:=v])"
   24.87 -primrec takeWhile list
   24.88 +primrec
   24.89    "takeWhile P [] = []"
   24.90    "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
   24.91 -primrec dropWhile list
   24.92 +primrec
   24.93    "dropWhile P [] = []"
   24.94    "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
   24.95 -primrec zip list
   24.96 +primrec
   24.97    "zip xs []     = []"
   24.98    "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
   24.99 -primrec nodups list
  24.100 +primrec
  24.101    "nodups []     = True"
  24.102    "nodups (x#xs) = (x ~: set xs & nodups xs)"
  24.103 -primrec remdups list
  24.104 +primrec
  24.105    "remdups [] = []"
  24.106    "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
  24.107 -primrec replicate nat
  24.108 -replicate_0   "replicate 0 x       = []"
  24.109 -replicate_Suc "replicate (Suc n) x = x # replicate n x"
  24.110 +primrec
  24.111 +  replicate_0   "replicate 0 x       = []"
  24.112 +  replicate_Suc "replicate (Suc n) x = x # replicate n x"
  24.113  
  24.114  end
  24.115  
    25.1 --- a/src/HOL/Map.ML	Fri Jul 24 13:02:01 1998 +0200
    25.2 +++ b/src/HOL/Map.ML	Fri Jul 24 13:03:20 1998 +0200
    25.3 @@ -44,21 +44,21 @@
    25.4  Goalw [override_def] "empty ++ m = m";
    25.5  by (Simp_tac 1);
    25.6  by (rtac ext 1);
    25.7 -by (split_tac [split_option_case] 1);
    25.8 +by (split_tac [option.split] 1);
    25.9  by (Simp_tac 1);
   25.10  qed "empty_override";
   25.11  Addsimps [empty_override];
   25.12  
   25.13  Goalw [override_def]
   25.14   "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
   25.15 -by (simp_tac (simpset() addsplits [split_option_case]) 1);
   25.16 +by (simp_tac (simpset() addsplits [option.split]) 1);
   25.17  qed_spec_mp "override_Some_iff";
   25.18  
   25.19  bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
   25.20  
   25.21  Goalw [override_def]
   25.22   "((m ++ n) k = None) = (n k = None & m k = None)";
   25.23 -by (simp_tac (simpset() addsplits [split_option_case]) 1);
   25.24 +by (simp_tac (simpset() addsplits [option.split]) 1);
   25.25  qed "override_None";
   25.26  AddIffs [override_None];
   25.27  
   25.28 @@ -66,12 +66,12 @@
   25.29  by (induct_tac "xs" 1);
   25.30  by (Simp_tac 1);
   25.31  by (rtac ext 1);
   25.32 -by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
   25.33 +by (asm_simp_tac (simpset() addsplits [option.split]) 1);
   25.34  qed "map_of_append";
   25.35  Addsimps [map_of_append];
   25.36  
   25.37  Goal "map_of xs k = Some y --> (k,y):set xs";
   25.38 -by (list.induct_tac "xs" 1);
   25.39 +by (induct_tac "xs" 1);
   25.40  by  (Simp_tac 1);
   25.41  by (split_all_tac 1);
   25.42  by (Asm_simp_tac 1);
   25.43 @@ -91,7 +91,7 @@
   25.44  Addsimps [dom_update];
   25.45  
   25.46  qed_goalw "finite_dom_map_of" Map.thy [dom_def] "finite (dom (map_of l))" (K[
   25.47 -	list.induct_tac "l" 1,
   25.48 +	induct_tac "l" 1,
   25.49  	 ALLGOALS Simp_tac,
   25.50  	stac (insert_Collect RS sym) 1,
   25.51  	Asm_simp_tac 1]);
    26.1 --- a/src/HOL/Map.thy	Fri Jul 24 13:02:01 1998 +0200
    26.2 +++ b/src/HOL/Map.thy	Fri Jul 24 13:03:20 1998 +0200
    26.3 @@ -37,8 +37,8 @@
    26.4  dom_def "dom(m) == {a. m a ~= None}"
    26.5  ran_def "ran(m) == {b. ? a. m a = Some b}"
    26.6  
    26.7 -primrec map_of list
    26.8 -"map_of [] = empty"
    26.9 -"map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
   26.10 +primrec
   26.11 +  "map_of [] = empty"
   26.12 +  "map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
   26.13  
   26.14  end
    27.1 --- a/src/HOL/Option.ML	Fri Jul 24 13:02:01 1998 +0200
    27.2 +++ b/src/HOL/Option.ML	Fri Jul 24 13:03:20 1998 +0200
    27.3 @@ -8,7 +8,7 @@
    27.4  open Option;
    27.5  
    27.6  qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
    27.7 -	(K [option.induct_tac "x" 1, Auto_tac]);
    27.8 +	(K [induct_tac "x" 1, Auto_tac]);
    27.9  
   27.10  section "case analysis in premises";
   27.11  
   27.12 @@ -55,7 +55,7 @@
   27.13  
   27.14  val option_map_eq_Some = prove_goalw thy [option_map_def]
   27.15  	"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" 
   27.16 - (K [asm_full_simp_tac (simpset() addsplits [split_option_case]) 1]);
   27.17 + (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]);
   27.18  AddIffs[option_map_eq_Some];
   27.19  
   27.20  section "o2s";
    28.1 --- a/src/HOL/Option.thy	Fri Jul 24 13:02:01 1998 +0200
    28.2 +++ b/src/HOL/Option.thy	Fri Jul 24 13:03:20 1998 +0200
    28.3 @@ -6,7 +6,7 @@
    28.4  Datatype 'a option
    28.5  *)
    28.6  
    28.7 -Option = Arith +
    28.8 +Option = Datatype +
    28.9  
   28.10  datatype 'a option = None | Some 'a
   28.11  
   28.12 @@ -22,8 +22,7 @@
   28.13  
   28.14    o2s	   :: "'a option => 'a set"
   28.15  
   28.16 -primrec o2s option
   28.17 -
   28.18 +primrec
   28.19   "o2s  None    = {}"
   28.20   "o2s (Some x) = {x}"
   28.21  
    29.1 --- a/src/HOL/Power.thy	Fri Jul 24 13:02:01 1998 +0200
    29.2 +++ b/src/HOL/Power.thy	Fri Jul 24 13:03:20 1998 +0200
    29.3 @@ -11,11 +11,11 @@
    29.4  consts
    29.5    binomial :: "[nat,nat] => nat"      ("'(_ choose _')" [50,50])
    29.6  
    29.7 -primrec "op ^" nat
    29.8 +primrec
    29.9    "p ^ 0 = 1"
   29.10    "p ^ (Suc n) = (p::nat) * (p ^ n)"
   29.11    
   29.12 -primrec "binomial" nat
   29.13 +primrec
   29.14    binomial_0   "(0     choose k) = (if k = 0 then 1 else 0)"
   29.15  
   29.16    binomial_Suc "(Suc n choose k) =
    30.1 --- a/src/HOL/ROOT.ML	Fri Jul 24 13:02:01 1998 +0200
    30.2 +++ b/src/HOL/ROOT.ML	Fri Jul 24 13:03:20 1998 +0200
    30.3 @@ -26,8 +26,6 @@
    30.4  use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
    30.5  use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
    30.6  
    30.7 -use "thy_data.ML";
    30.8 -
    30.9  use_thy "HOL";
   30.10  use "hologic.ML";
   30.11  use "cladata.ML";
   30.12 @@ -42,13 +40,21 @@
   30.13  use "Tools/record_package.ML";
   30.14  use_thy "Record";
   30.15  
   30.16 -use "datatype.ML";
   30.17 -use_thy "Arith";
   30.18 -use "arith_data.ML";
   30.19 +use_thy "NatDef";
   30.20  
   30.21  use "Tools/inductive_package.ML";
   30.22  use_thy "Inductive";
   30.23  
   30.24 +use "Tools/datatype_aux.ML";
   30.25 +use "Tools/datatype_prop.ML";
   30.26 +use "Tools/datatype_rep_proofs.ML";
   30.27 +use "Tools/datatype_abs_proofs.ML";
   30.28 +use "Tools/datatype_package.ML";
   30.29 +use "Tools/primrec_package.ML";
   30.30 +
   30.31 +use_thy "Arith";
   30.32 +use "arith_data.ML";
   30.33 +
   30.34  use_thy "RelPow";
   30.35  use_thy "Finite";
   30.36  use_thy "Sexp";
    31.1 --- a/src/HOL/RelPow.ML	Fri Jul 24 13:02:01 1998 +0200
    31.2 +++ b/src/HOL/RelPow.ML	Fri Jul 24 13:03:20 1998 +0200
    31.3 @@ -42,10 +42,9 @@
    31.4      "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
    31.5  \       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
    31.6  \    |] ==> P";
    31.7 -by (res_inst_tac [("n","n")] natE 1);
    31.8  by (cut_facts_tac [p1] 1);
    31.9 +by (exhaust_tac "n" 1);
   31.10  by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
   31.11 -by (cut_facts_tac [p1] 1);
   31.12  by (Asm_full_simp_tac 1);
   31.13  by (etac compEpair 1);
   31.14  by (REPEAT(ares_tac [p3] 1));
   31.15 @@ -69,10 +68,9 @@
   31.16      "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
   31.17  \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
   31.18  \    |] ==> P";
   31.19 -by (res_inst_tac [("n","n")] natE 1);
   31.20  by (cut_facts_tac [p1] 1);
   31.21 +by (exhaust_tac "n" 1);
   31.22  by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
   31.23 -by (cut_facts_tac [p1] 1);
   31.24  by (Asm_full_simp_tac 1);
   31.25  by (etac compEpair 1);
   31.26  by (dtac (conjI RS rel_pow_Suc_D2') 1);
    32.1 --- a/src/HOL/RelPow.thy	Fri Jul 24 13:02:01 1998 +0200
    32.2 +++ b/src/HOL/RelPow.thy	Fri Jul 24 13:03:20 1998 +0200
    32.3 @@ -8,7 +8,7 @@
    32.4  
    32.5  RelPow = Nat +
    32.6  
    32.7 -primrec "op ^" nat
    32.8 +primrec
    32.9    "R^0 = id"
   32.10    "R^(Suc n) = R O (R^n)"
   32.11  
    33.1 --- a/src/HOL/Sum.ML	Fri Jul 24 13:02:01 1998 +0200
    33.2 +++ b/src/HOL/Sum.ML	Fri Jul 24 13:03:20 1998 +0200
    33.3 @@ -140,6 +140,11 @@
    33.4                      rtac (Rep_Sum_inverse RS sym)]));
    33.5  qed "sumE";
    33.6  
    33.7 +val prems = goal thy "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
    33.8 +by (res_inst_tac [("s","x")] sumE 1);
    33.9 +by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
   33.10 +qed "sum_induct";
   33.11 +
   33.12  Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
   33.13  by (EVERY1 [res_inst_tac [("s","s")] sumE, 
   33.14              etac ssubst, rtac sum_case_Inl,
    34.1 --- a/src/HOL/thy_syntax.ML	Fri Jul 24 13:02:01 1998 +0200
    34.2 +++ b/src/HOL/thy_syntax.ML	Fri Jul 24 13:03:20 1998 +0200
    34.3 @@ -5,10 +5,6 @@
    34.4  Additional theory file sections for HOL.
    34.5  *)
    34.6  
    34.7 -(*the kind of distinctiveness axioms depends on number of constructors*)
    34.8 -val dtK = 7;  (* FIXME rename?, move? *)
    34.9 -
   34.10 -
   34.11  local
   34.12  
   34.13  open ThyParse;
   34.14 @@ -86,159 +82,119 @@
   34.15  (** datatype **)
   34.16  
   34.17  local
   34.18 -  (* FIXME err -> add_datatype *)
   34.19 -  fun mk_cons cs =
   34.20 -    (case duplicates (map (fst o fst) cs) of
   34.21 -      [] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
   34.22 -    | dups => error ("Duplicate constructors: " ^ commas_quote dups));
   34.23 +  (*** generate string for calling add_datatype ***)
   34.24 +  (*** and bindig theorems to ML identifiers    ***)
   34.25  
   34.26 -  (*generate names of distinctiveness axioms*)
   34.27 -  fun mk_distinct_rules cs tname =
   34.28 +  fun mk_bind_thms_string names =
   34.29 +   (case find_first (not o Syntax.is_identifier) names of
   34.30 +      Some id => (warning (id ^ " is not a valid identifier"); "")
   34.31 +    | None =>
   34.32 +        let
   34.33 +          fun mk_dt_struct (s, (id, i)) =
   34.34 +            s ^ "structure " ^ id ^ " =\n\
   34.35 +            \struct\n\
   34.36 +            \  val distinct = nth_elem (" ^ i ^ ", distinct);\n\
   34.37 +            \  val inject = nth_elem (" ^ i ^ ", inject);\n\
   34.38 +            \  val exhaust = nth_elem (" ^ i ^ ", exhaustion);\n\
   34.39 +            \  val cases = nth_elem (" ^ i ^ ", case_thms);\n\
   34.40 +            \  val (split, split_asm) = nth_elem (" ^ i ^ ", split_thms);\n" ^
   34.41 +              (if length names = 1 then
   34.42 +                 "  val induct = induction;\n\
   34.43 +                 \  val recs = rec_thms;\n\
   34.44 +                 \  val simps = simps;\n\
   34.45 +                 \  val size = size;\n"
   34.46 +               else "") ^
   34.47 +            "end;\n";
   34.48 +
   34.49 +          val structs = foldl mk_dt_struct
   34.50 +            ("", (names ~~ (map string_of_int (0 upto length names - 1))));
   34.51 +
   34.52 +        in
   34.53 +          (if length names > 1 then
   34.54 +             "structure " ^ (space_implode "_" names) ^ " =\n\
   34.55 +             \struct\n\
   34.56 +             \val induct = induction;\n\
   34.57 +             \val recs = rec_thms;\n\
   34.58 +             \val simps = simps;\n\
   34.59 +             \val size = size;\n"
   34.60 +           else "") ^ structs ^
   34.61 +          (if length names > 1 then "end;\n" else "")
   34.62 +        end);
   34.63 +
   34.64 +  fun mk_dt_string dts =
   34.65      let
   34.66 -      val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
   34.67 -      (*combine all constructor names with all others w/o duplicates*)
   34.68 -      fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
   34.69 -      fun neg1 [] = []
   34.70 -        | neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
   34.71 +      val names = map (fn ((((alt_name, _), name), _), _) =>
   34.72 +        strip_quotes (if_none alt_name name)) dts;
   34.73 +
   34.74 +      val add_datatype_args = brackets (commas (map quote names)) ^ " " ^
   34.75 +        brackets (commas (map (fn ((((_, vs), name), mx), cs) =>
   34.76 +          parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^
   34.77 +            brackets (commas cs))) dts));
   34.78 +
   34.79      in
   34.80 -      if length uqcs < dtK then neg1 uqcs
   34.81 -      else quote (tname ^ "_ord_distinct") ::
   34.82 -        map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
   34.83 +      ";\nlocal\n\
   34.84 +      \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
   34.85 +      \  case_thms, split_thms, induction, size, simps}) =\n\
   34.86 +      \  DatatypePackage.add_datatype " ^ add_datatype_args ^ " thy;\n\
   34.87 +      \in\n" ^ mk_bind_thms_string names ^
   34.88 +      "val thy = thy;\nend;\nval thy = thy\n"
   34.89      end;
   34.90  
   34.91 -  fun mk_rules tname cons pre = " map (get_axiom thy) " ^
   34.92 -    mk_list (map (fn ((s,_), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
   34.93 +  fun mk_rep_dt_string (((names, distinct), inject), induct) =
   34.94 +    ";\nlocal\n\
   34.95 +    \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
   34.96 +    \  case_thms, split_thms, induction, size, simps}) =\n\
   34.97 +    \  DatatypePackage.add_rep_datatype " ^
   34.98 +    (case names of
   34.99 +        Some names => "(Some [" ^ commas (map quote names) ^ "]) (" ^
  34.100 +          distinct ^ ") (" ^ inject ^ ") (" ^ induct ^ ") thy;\nin\n" ^
  34.101 +            mk_bind_thms_string names
  34.102 +      | None => "None (" ^ distinct ^ ") (" ^ inject ^ ") (" ^ induct ^
  34.103 +          ") thy;\nin\n") ^
  34.104 +    "val thy = thy;\nend;\nval thy = thy\n";
  34.105  
  34.106 -  (*generate string for calling add_datatype and build_record*)
  34.107 -  fun mk_params ((ts, tname), cons) =
  34.108 -    "val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqns) =\n\
  34.109 -    \    Datatype.add_datatype\n"
  34.110 -    ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
  34.111 -    \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)\n\
  34.112 -    \val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
  34.113 -    \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
  34.114 -    \structure " ^ tname ^ " =\n\
  34.115 -    \struct\n\
  34.116 -    \ val inject = map (get_axiom thy) " ^
  34.117 -        mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
  34.118 -          (filter_out (null o snd o fst) cons)) ^ ";\n\
  34.119 -    \ val distinct = " ^
  34.120 -        (if length cons < dtK then "let val distinct' = " else "") ^
  34.121 -        "map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
  34.122 -        (if length cons < dtK then
  34.123 -          "  in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
  34.124 -          \ distinct') end"
  34.125 -         else "") ^ ";\n\
  34.126 -    \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
  34.127 -    \ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
  34.128 -    \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
  34.129 -    \ val simps = inject @ distinct @ cases @ recs;\n\
  34.130 -    \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
  34.131 -    \end;\n\
  34.132 -    \val thy = thy |> Dtype.add_record " ^
  34.133 -      mk_triple
  34.134 -        ("Sign.intern_tycon (sign_of thy) " ^ quote tname,
  34.135 -          mk_list (map (fst o fst) cons),
  34.136 -          tname ^ ".induct_tac") ^ ";\n\
  34.137 -    \val dummy = context thy;\n\
  34.138 -    \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
  34.139 -    \val dummy = AddIffs " ^ tname ^ ".inject;\n\
  34.140 -    \val dummy = " ^
  34.141 -      (if length cons < dtK then "AddIffs " else "Addsimps ") ^
  34.142 -      tname ^ ".distinct;\n\
  34.143 -    \val dummy = Addsimps(map (fn (_,eqn) =>\n\
  34.144 -    \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
  34.145 -                     "] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\
  34.146 -    \val split_"^tname^"_case = prove_goal thy (#1(split_"^tname^"_eqns))\n\
  34.147 -    \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
  34.148 -      ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
  34.149 -    \            ALLGOALS Asm_simp_tac]);\n\
  34.150 -    \val split_"^tname^"_case_asm = prove_goal thy (#2(split_"^tname^"_eqns))\n\
  34.151 -    \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
  34.152 -      ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
  34.153 -    \            ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex]))]);\n\
  34.154 -    \val thy = thy\n";
  34.155 +  (*** parsers ***)
  34.156  
  34.157 -(*
  34.158 -The #exhaust_tac(snd(hd(!datatypes))) in the proof of split_"^tname^"_case
  34.159 -is a hack. Ideally I would just write exhaust_tac, but the latter extracts the
  34.160 -specific exhaustion tactic from the theory associated with the proof
  34.161 -state. However, the exhaustion tactic for the current datatype has only just
  34.162 -been added to !datatypes (a few lines above) but is not yet associated with
  34.163 -the theory. Hope this can be simplified in the future.
  34.164 -*)
  34.165 -
  34.166 -  (*parsers*)
  34.167 -  val tvars = type_args >> map (cat "dtVar");
  34.168 -
  34.169 -  val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) ||
  34.170 -    type_var >> cat "dtVar";
  34.171 +  val simple_typ = ident || (type_var >> strip_quotes);
  34.172  
  34.173    fun complex_typ toks =
  34.174      let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
  34.175          val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
  34.176      in
  34.177 -     (typ -- repeat (ident>>quote) >>
  34.178 -        (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) ||
  34.179 -      "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >>
  34.180 -       (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^
  34.181 -                         mk_pair (brackets x, y)) (commas fst, ids))) toks
  34.182 +     (typ ^^ (repeat ident >> (cat "" o space_implode " ")) ||
  34.183 +      "(" $$-- !! (list1 typ2 >> (parens o commas)) --$$ ")" ^^ !!
  34.184 +        (repeat1 ident >> (cat "" o space_implode " "))) toks
  34.185      end;
  34.186  
  34.187 -  val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
  34.188 -  val constructor = name -- opt_typs -- opt_mixfix;
  34.189 +  val opt_typs = repeat ((string >> strip_quotes) ||
  34.190 +    simple_typ || ("(" $$-- complex_typ --$$ ")"));
  34.191 +  val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
  34.192 +    parens (n ^ ", " ^ mx ^ ", " ^ brackets (commas (map quote Ts))));
  34.193 +  val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None
  34.194 +
  34.195  in
  34.196    val datatype_decl =
  34.197 -    tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
  34.198 +    enum1 "and" (opt_name -- type_args -- name -- opt_infix --$$ "=" --
  34.199 +      enum1 "|" constructor) >> mk_dt_string;
  34.200 +  val rep_datatype_decl =
  34.201 +    ((optional ((repeat1 (name >> strip_quotes)) >> Some) None) --
  34.202 +      ("distinct" $$-- (name >> strip_quotes)) -- ("inject" $$--
  34.203 +        (name >> strip_quotes)) -- ("induct" $$-- (name >> strip_quotes))) >>
  34.204 +          mk_rep_dt_string;
  34.205  end;
  34.206  
  34.207  
  34.208 -
  34.209  (** primrec **)
  34.210  
  34.211 -(*recursion equations have user-supplied names*)
  34.212 -fun mk_primrec_decl_1 ((fname, tname), axms) =
  34.213 -  let
  34.214 -    (*Isolate type name from the structure's identifier it may be stored in*)
  34.215 -    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
  34.216 -
  34.217 -    fun mk_prove (name, eqn) =
  34.218 -      "val " ^ name ^ " = store_thm (" ^ quote name
  34.219 -      ^ ", prove_goalw thy [get_def thy "
  34.220 -      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\
  34.221 -      \  (fn _ => [Simp_tac 1]));";
  34.222 -
  34.223 -    val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
  34.224 -  in ("|> " ^ tname ^ "_add_primrec " ^ axs
  34.225 -      , 
  34.226 -      cat_lines (map mk_prove axms)
  34.227 -      ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
  34.228 -  end;
  34.229 +fun mk_primrec_decl (names, eqns) =
  34.230 +  ";\nval (thy, " ^ (if null names then "_" else brackets (commas names)) ^
  34.231 +  ") = PrimrecPackage.add_primrec " ^ brackets (commas eqns) ^ " thy;\n\
  34.232 +  \val thy = thy\n";
  34.233  
  34.234 -(*recursion equations have no names*)
  34.235 -fun mk_primrec_decl_2 ((fname, tname), axms) =
  34.236 -  let
  34.237 -    (*Isolate type name from the structure's identifier it may be stored in*)
  34.238 -    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
  34.239 -
  34.240 -    fun mk_prove eqn =
  34.241 -      "prove_goalw thy [get_def thy "
  34.242 -      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \
  34.243 -      \(fn _ => [Simp_tac 1])";
  34.244 -
  34.245 -    val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
  34.246 -  in ("|> " ^ tname ^ "_add_primrec " ^ axs
  34.247 -      ,
  34.248 -      "val dummy = Addsimps " ^
  34.249 -      brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
  34.250 -  end;
  34.251 -
  34.252 -(*function name, argument type and either (name,axiom) pairs or just axioms*)
  34.253 +(* either names and axioms or just axioms *)
  34.254  val primrec_decl =
  34.255 -  (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
  34.256 -  (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
  34.257 -
  34.258 -
  34.259 +  (repeat1 (ident -- string) >> (mk_primrec_decl o ListPair.unzip)) ||
  34.260 +  (repeat1 string >> (mk_primrec_decl o (pair [])));
  34.261  
  34.262  
  34.263  (** rec: interface to Slind's TFL **)
  34.264 @@ -278,13 +234,15 @@
  34.265  in
  34.266  
  34.267  val _ = ThySyn.add_syntax
  34.268 - ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
  34.269 + ["intrs", "monos", "con_defs", "congs", "simpset", "|",
  34.270 +  "and", "distinct", "inject", "induct"]
  34.271   [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
  34.272    section "record" "|> RecordPackage.add_record" record_decl,
  34.273    section "inductive" "" (inductive_decl false),
  34.274    section "coinductive" "" (inductive_decl true),
  34.275    section "datatype" "" datatype_decl,
  34.276 -  ("primrec", primrec_decl),
  34.277 +  section "rep_datatype" "" rep_datatype_decl,
  34.278 +  section "primrec" "" primrec_decl,
  34.279    ("recdef", rec_decl)];
  34.280  
  34.281  end;