Adapted to new datatype package.
--- a/src/HOL/Arith.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Arith.ML Fri Jul 24 13:03:20 1998 +0200
@@ -29,7 +29,7 @@
However, none of the generalizations are currently in the simpset,
and I dread to think what happens if I put them in *)
Goal "0 < n ==> Suc(n-1) = n";
-by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1);
+by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
qed "Suc_pred";
Addsimps [Suc_pred];
@@ -114,7 +114,7 @@
Goal "0<n ==> m + (n-1) = (m+n)-1";
by (exhaust_tac "m" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
- addsplits [split_nat_case])));
+ addsplits [nat.split])));
qed "add_pred";
Addsimps [add_pred];
@@ -373,7 +373,7 @@
Addsimps [Suc_diff_diff];
Goal "0<n ==> n - Suc i < n";
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
by Safe_tac;
by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1);
qed "diff_Suc_less";
@@ -670,8 +670,8 @@
Goal "!!n::nat. m<=n ==> (l-n) <= (l-m)";
by (induct_tac "l" 1);
by (Simp_tac 1);
-by (case_tac "n <= l" 1);
-by (subgoal_tac "m <= l" 1);
+by (case_tac "n <= na" 1);
+by (subgoal_tac "m <= na" 1);
by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
by (fast_tac (claset() addEs [le_trans]) 1);
by (dtac not_leE 1);
--- a/src/HOL/Arith.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Arith.thy Fri Jul 24 13:03:20 1998 +0200
@@ -14,15 +14,15 @@
(* size of a datatype value; overloaded *)
consts size :: 'a => nat
-primrec "op +" nat
+primrec
add_0 "0 + n = n"
add_Suc "Suc m + n = Suc(m + n)"
-primrec "op -" nat
+primrec
diff_0 "m - 0 = m"
diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
-primrec "op *" nat
+primrec
mult_0 "0 * n = 0"
mult_Suc "Suc m * n = n + (m * n)"
--- a/src/HOL/Auth/Event.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Auth/Event.thy Fri Jul 24 13:03:20 1998 +0200
@@ -29,7 +29,7 @@
Spy_in_bad "Spy: bad"
Server_not_bad "Server ~: bad"
-primrec spies list
+primrec
(*Spy reads all traffic whether addressed to him or not*)
spies_Nil "spies [] = initState Spy"
spies_Cons "spies (ev # evs) =
@@ -43,7 +43,7 @@
complement of the set of fresh items*)
used :: event list => msg set
-primrec used list
+primrec
used_Nil "used [] = (UN B. parts (initState B))"
used_Cons "used (ev # evs) =
(case ev of
--- a/src/HOL/Auth/Message.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Auth/Message.thy Fri Jul 24 13:03:20 1998 +0200
@@ -7,7 +7,7 @@
Inductive relations "parts", "analz" and "synth"
*)
-Message = Arith + Inductive +
+Message = Datatype +
(*Is there a difference between a nonce and arbitrary numerical data?
Do we need a type of nonces?*)
--- a/src/HOL/Auth/Public.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Auth/Public.thy Fri Jul 24 13:03:20 1998 +0200
@@ -19,7 +19,7 @@
translations (*BEWARE! expressions like (inj priK) will NOT work!*)
"priK x" == "invKey(pubK x)"
-primrec initState agent
+primrec
(*Agents know their private key and all public keys*)
initState_Server "initState Server =
insert (Key (priK Server)) (Key `` range pubK)"
--- a/src/HOL/Auth/Shared.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Auth/Shared.thy Fri Jul 24 13:03:20 1998 +0200
@@ -17,7 +17,7 @@
isSym_keys "isSymKey K" (*All keys are symmetric*)
inj_shrK "inj shrK" (*No two agents have the same long-term key*)
-primrec initState agent
+primrec
(*Server knows all long-term keys; other agents know only their own*)
initState_Server "initState Server = Key `` range shrK"
initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}"
--- a/src/HOL/Divides.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Divides.ML Fri Jul 24 13:03:20 1998 +0200
@@ -92,7 +92,7 @@
Goal "0<n ==> m*n mod n = 0";
by (induct_tac "m" 1);
by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
-by (dres_inst_tac [("m","m*n")] mod_add_self2 1);
+by (dres_inst_tac [("m","na*n")] mod_add_self2 1);
by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
qed "mod_mult_self_is_0";
Addsimps [mod_mult_self_is_0];
--- a/src/HOL/Finite.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Finite.ML Fri Jul 24 13:03:20 1998 +0200
@@ -214,7 +214,7 @@
Goal
"[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
\ ? m::nat. m<n & (? g. A = {g i|i. i<m})";
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
by (hyp_subst_tac 1);
by (Asm_full_simp_tac 1);
by (rename_tac "m" 1);
--- a/src/HOL/Hoare/Arith2.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Hoare/Arith2.thy Fri Jul 24 13:03:20 1998 +0200
@@ -16,8 +16,9 @@
"gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
consts fac :: nat => nat
-primrec fac nat
-"fac 0 = Suc 0"
-"fac(Suc n) = (Suc n)*fac(n)"
+
+primrec
+ "fac 0 = Suc 0"
+ "fac(Suc n) = (Suc n)*fac(n)"
end
--- a/src/HOL/Hoare/Examples.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Hoare/Examples.ML Fri Jul 24 13:03:20 1998 +0200
@@ -65,7 +65,7 @@
by (hoare_tac 1);
-by (res_inst_tac [("n","b")] natE 1);
+by (exhaust_tac "b" 1);
by (hyp_subst_tac 1);
by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);
@@ -86,7 +86,7 @@
by (hoare_tac 1);
by Safe_tac;
-by (res_inst_tac [("n","a")] natE 1);
+by (exhaust_tac "a" 1);
by (ALLGOALS
(asm_simp_tac
(simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
--- a/src/HOL/Hoare/Hoare.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Hoare/Hoare.ML Fri Jul 24 13:03:20 1998 +0200
@@ -44,7 +44,7 @@
(fn [prem1,prem2] =>
[REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2,
etac thin_rl 1, res_inst_tac[("x","s")]spec 1,
- res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
+ res_inst_tac[("x","s'")]spec 1, induct_tac "n" 1,
Simp_tac 1,
fast_tac (claset() addIs [prem2]) 1,
simp_tac (simpset() addsimps [Seq_def]) 1,
--- a/src/HOL/Hoare/Hoare.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Hoare/Hoare.thy Fri Jul 24 13:03:20 1998 +0200
@@ -47,7 +47,8 @@
consts
Iter :: [nat, 'a bexp, 'a com] => 'a com
-primrec Iter nat
+
+primrec
"Iter 0 b c = (%s s'.~b(s) & (s=s'))"
"Iter (Suc n) b c = (%s s'. b(s) & Seq c (Iter n b c) s s')"
--- a/src/HOL/IMP/Com.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IMP/Com.thy Fri Jul 24 13:03:20 1998 +0200
@@ -7,7 +7,7 @@
Syntax of commands
*)
-Com = Arith +
+Com = Datatype +
types
val
--- a/src/HOL/IMP/Denotation.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IMP/Denotation.ML Fri Jul 24 13:03:20 1998 +0200
@@ -42,7 +42,7 @@
(* Denotational Semantics implies Operational Semantics *)
Goal "!s t. (s,t):C(c) --> <c,s> -c-> t";
-by (com.induct_tac "c" 1);
+by (induct_tac "c" 1);
by (ALLGOALS Full_simp_tac);
by (ALLGOALS (TRY o Fast_tac));
--- a/src/HOL/IMP/Denotation.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IMP/Denotation.thy Fri Jul 24 13:03:20 1998 +0200
@@ -18,7 +18,7 @@
consts
C :: com => com_den
-primrec C com
+primrec
C_skip "C(SKIP) = id"
C_assign "C(x := a) = {(s,t). t = s[x:=a(s)]}"
C_comp "C(c0 ; c1) = C(c1) O C(c0)"
--- a/src/HOL/IMP/Expr.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IMP/Expr.ML Fri Jul 24 13:03:20 1998 +0200
@@ -33,14 +33,14 @@
\ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"];
Goal "!n. ((a,s) -a-> n) = (A a s = n)";
-by (aexp.induct_tac "a" 1);
+by (induct_tac "a" 1);
by (ALLGOALS
(fast_tac (claset() addSIs evala.intrs
addSEs evala_elim_cases addss (simpset()))));
qed_spec_mp "aexp_iff";
Goal "!w. ((b,s) -b-> w) = (B b s = w)";
-by (bexp.induct_tac "b" 1);
+by (induct_tac "b" 1);
by (ALLGOALS
(fast_tac (claset()
addss (simpset() addsimps (aexp_iff::evalb_simps)))));
--- a/src/HOL/IMP/Expr.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IMP/Expr.thy Fri Jul 24 13:03:20 1998 +0200
@@ -7,7 +7,7 @@
Not used in the rest of the language, but included for completeness.
*)
-Expr = Arith + Inductive +
+Expr = Datatype +
(** Arithmetic expressions **)
types loc
@@ -72,13 +72,13 @@
A :: aexp => state => nat
B :: bexp => state => bool
-primrec A aexp
+primrec
"A(N(n)) = (%s. n)"
"A(X(x)) = (%s. s(x))"
"A(Op1 f a) = (%s. f(A a s))"
"A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
-primrec B bexp
+primrec
"B(true) = (%s. True)"
"B(false) = (%s. False)"
"B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
--- a/src/HOL/IMP/Hoare.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IMP/Hoare.ML Fri Jul 24 13:03:20 1998 +0200
@@ -91,7 +91,7 @@
AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
Goal "!Q. |- {wp c Q} c {Q}";
-by (com.induct_tac "c" 1);
+by (induct_tac "c" 1);
by (ALLGOALS Simp_tac);
by (REPEAT_FIRST Fast_tac);
by (blast_tac (claset() addIs [hoare.conseq]) 1);
--- a/src/HOL/IMP/Transition.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IMP/Transition.ML Fri Jul 24 13:03:20 1998 +0200
@@ -32,7 +32,7 @@
Goal
"!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
\ (c;d, s) -*-> (SKIP, u)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2])1);
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]addSDs [rel_pow_Suc_D2])1);
qed_spec_mp "lemma1";
--- a/src/HOL/IMP/VC.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IMP/VC.ML Fri Jul 24 13:03:20 1998 +0200
@@ -13,7 +13,7 @@
val lemma = prove_goal HOL.thy "!s. P s --> P s" (K[Fast_tac 1]);
Goal "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}";
-by (acom.induct_tac "c" 1);
+by (induct_tac "c" 1);
by (ALLGOALS Simp_tac);
by (Fast_tac 1);
by (Fast_tac 1);
@@ -30,7 +30,7 @@
qed "vc_sound";
Goal "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)";
-by (acom.induct_tac "c" 1);
+by (induct_tac "c" 1);
by (ALLGOALS Asm_simp_tac);
by (EVERY1[rtac allI, rtac allI, rtac impI]);
by (EVERY1[etac allE, etac allE, etac mp]);
@@ -38,7 +38,7 @@
qed_spec_mp "awp_mono";
Goal "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
-by (acom.induct_tac "c" 1);
+by (induct_tac "c" 1);
by (ALLGOALS Asm_simp_tac);
by (safe_tac HOL_cs);
by (EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
@@ -70,6 +70,6 @@
qed "vc_complete";
Goal "!Q. vcawp c Q = (vc c Q, awp c Q)";
-by (acom.induct_tac "c" 1);
+by (induct_tac "c" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def])));
qed "vcawp_vc_awp";
--- a/src/HOL/IMP/VC.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IMP/VC.thy Fri Jul 24 13:03:20 1998 +0200
@@ -21,14 +21,14 @@
vcawp :: "acom => assn => assn * assn"
astrip :: acom => com
-primrec awp acom
+primrec
"awp Askip Q = Q"
"awp (Aass x a) Q = (%s. Q(s[x:=a s]))"
"awp (Asemi c d) Q = awp c (awp d Q)"
"awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
"awp (Awhile b I c) Q = I"
-primrec vc acom
+primrec
"vc Askip Q = (%s. True)"
"vc (Aass x a) Q = (%s. True)"
"vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
@@ -36,7 +36,7 @@
"vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
(I s & b s --> awp c I s) & vc c I s)"
-primrec astrip acom
+primrec
"astrip Askip = SKIP"
"astrip (Aass x a) = (x:=a)"
"astrip (Asemi c d) = (astrip c;astrip d)"
@@ -44,7 +44,7 @@
"astrip (Awhile b I c) = (WHILE b DO astrip c)"
(* simultaneous computation of vc and awp: *)
-primrec vcawp acom
+primrec
"vcawp Askip Q = (%s. True, Q)"
"vcawp (Aass x a) Q = (%s. True, %s. Q(s[x:=a s]))"
"vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
--- a/src/HOL/IsaMakefile Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IsaMakefile Fri Jul 24 13:03:20 1998 +0200
@@ -39,19 +39,23 @@
$(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \
$(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \
$(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \
- Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
+ Arith.ML Arith.thy Datatype.thy \
+ Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \
Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/Integ.ML \
Integ/Integ.thy Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML \
Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
Power.ML Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
- String.ML String.thy Sum.ML Sum.thy Tools/inductive_package.ML Tools/record_package.ML \
+ String.ML String.thy Sum.ML Sum.thy \
+ Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
+ Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
+ Tools/inductive_package.ML Tools/primrec_package.ML Tools/record_package.ML \
Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
Update.ML Update.thy Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
- WF_Rel.thy arith_data.ML cladata.ML datatype.ML equalities.ML \
+ WF_Rel.thy arith_data.ML cladata.ML equalities.ML \
equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
- subset.thy thy_data.ML thy_syntax.ML
+ subset.thy thy_syntax.ML
@$(ISATOOL) usedir -b $(OUT)/Pure HOL
--- a/src/HOL/List.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/List.ML Fri Jul 24 13:03:20 1998 +0200
@@ -208,17 +208,17 @@
Goal "xs ~= [] ==> hd(xs @ ys) = hd xs";
by (asm_simp_tac (simpset() addsimps [hd_append]
- addsplits [split_list_case]) 1);
+ addsplits [list.split]) 1);
qed "hd_append2";
Addsimps [hd_append2];
Goal "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
-by (simp_tac (simpset() addsplits [split_list_case]) 1);
+by (simp_tac (simpset() addsplits [list.split]) 1);
qed "tl_append";
Goal "xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
by (asm_simp_tac (simpset() addsimps [tl_append]
- addsplits [split_list_case]) 1);
+ addsplits [list.split]) 1);
qed "tl_append2";
Addsimps [tl_append2];
@@ -482,7 +482,7 @@
Goal
"!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Asm_simp_tac 1);
by (rtac allI 1);
by (exhaust_tac "xs" 1);
@@ -495,7 +495,7 @@
by (Asm_full_simp_tac 1);
(* case x#xl *)
by (rtac allI 1);
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Auto_tac);
qed_spec_mp "nth_map";
Addsimps [nth_map];
@@ -506,7 +506,7 @@
by (Simp_tac 1);
(* case x#xl *)
by (rtac allI 1);
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Auto_tac);
qed_spec_mp "list_all_nth";
@@ -516,7 +516,7 @@
by (Simp_tac 1);
(* case x#xl *)
by (rtac allI 1);
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
(* case 0 *)
by (Asm_full_simp_tac 1);
(* case Suc x *)
@@ -531,7 +531,7 @@
Goal "!i. length(xs[i:=x]) = length xs";
by (induct_tac "xs" 1);
by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [split_nat_case]) 1);
+by (asm_full_simp_tac (simpset() addsplits [nat.split]) 1);
qed_spec_mp "length_list_update";
Addsimps [length_list_update];
@@ -603,7 +603,7 @@
Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
Goal "!xs. length(take n xs) = min (length xs) n";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
@@ -611,7 +611,7 @@
Addsimps [length_take];
Goal "!xs. length(drop n xs) = (length xs - n)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
@@ -619,14 +619,14 @@
Addsimps [length_drop];
Goal "!xs. length xs <= n --> take n xs = xs";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
qed_spec_mp "take_all";
Goal "!xs. length xs <= n --> drop n xs = []";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
@@ -634,7 +634,7 @@
Goal
"!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
@@ -642,7 +642,7 @@
Addsimps [take_append];
Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
@@ -650,37 +650,37 @@
Addsimps [drop_append];
Goal "!xs n. take n (take m xs) = take (min n m) xs";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
-by (exhaust_tac "n" 1);
+by (exhaust_tac "na" 1);
by (Auto_tac);
qed_spec_mp "take_take";
Goal "!xs. drop n (drop m xs) = drop (n + m) xs";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
qed_spec_mp "drop_drop";
Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
qed_spec_mp "take_drop";
Goal "!xs. take n (map f xs) = map f (take n xs)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
qed_spec_mp "take_map";
Goal "!xs. drop n (map f xs) = map f (drop n xs)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
@@ -697,7 +697,7 @@
Addsimps [nth_take];
Goal "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (Auto_tac);
by (exhaust_tac "xs" 1);
by (Auto_tac);
@@ -792,18 +792,18 @@
val list_eq_pattern =
read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
-fun last (cons as Const("List.op #",_) $ _ $ xs) =
- (case xs of Const("List.[]",_) => cons | _ => last xs)
- | last (Const("List.op @",_) $ _ $ ys) = last ys
+fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
+ (case xs of Const("List.list.[]",_) => cons | _ => last xs)
+ | last (Const("List.list.op @",_) $ _ $ ys) = last ys
| last t = t;
-fun list1 (Const("List.op #",_) $ _ $ Const("List.[]",_)) = true
+fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
| list1 _ = false;
-fun butlast ((cons as Const("List.op #",_) $ x) $ xs) =
- (case xs of Const("List.[]",_) => xs | _ => cons $ butlast xs)
- | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
- | butlast xs = Const("List.[]",fastype_of xs);
+fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
+ (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
+ | butlast ((app as Const("List.list.op @",_) $ xs) $ ys) = app $ butlast ys
+ | butlast xs = Const("List.list.[]",fastype_of xs);
val rearr_tac =
simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
@@ -815,7 +815,7 @@
let val lhs1 = butlast lhs and rhs1 = butlast rhs
val Type(_,listT::_) = eqT
val appT = [listT,listT] ---> listT
- val app = Const("List.op @",appT)
+ val app = Const("List.list.op @",appT)
val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
--- a/src/HOL/List.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/List.thy Fri Jul 24 13:03:20 1998 +0200
@@ -6,7 +6,7 @@
The datatype of finite lists.
*)
-List = WF_Rel +
+List = WF_Rel + Datatype +
datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
@@ -74,76 +74,76 @@
syntax length :: 'a list => nat
translations "length" => "size:: _ list => nat"
-primrec hd list
+primrec
"hd([]) = arbitrary"
"hd(x#xs) = x"
-primrec tl list
+primrec
"tl([]) = []"
"tl(x#xs) = xs"
-primrec last list
+primrec
"last [] = arbitrary"
"last(x#xs) = (if xs=[] then x else last xs)"
-primrec butlast list
+primrec
"butlast [] = []"
"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
-primrec "op mem" list
+primrec
"x mem [] = False"
"x mem (y#ys) = (if y=x then True else x mem ys)"
-primrec set list
+primrec
"set [] = {}"
"set (x#xs) = insert x (set xs)"
-primrec list_all list
+primrec
list_all_Nil "list_all P [] = True"
list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
-primrec map list
+primrec
"map f [] = []"
"map f (x#xs) = f(x)#map f xs"
-primrec "op @" list
-append_Nil "[] @ys = ys"
-append_Cons "(x#xs)@ys = x#(xs@ys)"
-primrec rev list
+primrec
+ append_Nil "[] @ys = ys"
+ append_Cons "(x#xs)@ys = x#(xs@ys)"
+primrec
"rev([]) = []"
"rev(x#xs) = rev(xs) @ [x]"
-primrec filter list
+primrec
"filter P [] = []"
"filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
-primrec foldl list
+primrec
"foldl f a [] = a"
"foldl f a (x#xs) = foldl f (f a x) xs"
-primrec concat list
+primrec
"concat([]) = []"
"concat(x#xs) = x @ concat(xs)"
-primrec drop list
+primrec
drop_Nil "drop n [] = []"
drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
-primrec take list
+primrec
take_Nil "take n [] = []"
take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
-primrec nth nat
+primrec
"xs!0 = hd xs"
"xs!(Suc n) = (tl xs)!n"
-primrec list_update list
+primrec
" [][i:=v] = []"
"(x#xs)[i:=v] = (case i of 0 => v # xs
| Suc j => x # xs[j:=v])"
-primrec takeWhile list
+primrec
"takeWhile P [] = []"
"takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
-primrec dropWhile list
+primrec
"dropWhile P [] = []"
"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
-primrec zip list
+primrec
"zip xs [] = []"
"zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
-primrec nodups list
+primrec
"nodups [] = True"
"nodups (x#xs) = (x ~: set xs & nodups xs)"
-primrec remdups list
+primrec
"remdups [] = []"
"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
-primrec replicate nat
-replicate_0 "replicate 0 x = []"
-replicate_Suc "replicate (Suc n) x = x # replicate n x"
+primrec
+ replicate_0 "replicate 0 x = []"
+ replicate_Suc "replicate (Suc n) x = x # replicate n x"
end
--- a/src/HOL/Map.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Map.ML Fri Jul 24 13:03:20 1998 +0200
@@ -44,21 +44,21 @@
Goalw [override_def] "empty ++ m = m";
by (Simp_tac 1);
by (rtac ext 1);
-by (split_tac [split_option_case] 1);
+by (split_tac [option.split] 1);
by (Simp_tac 1);
qed "empty_override";
Addsimps [empty_override];
Goalw [override_def]
"((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
-by (simp_tac (simpset() addsplits [split_option_case]) 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
qed_spec_mp "override_Some_iff";
bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
Goalw [override_def]
"((m ++ n) k = None) = (n k = None & m k = None)";
-by (simp_tac (simpset() addsplits [split_option_case]) 1);
+by (simp_tac (simpset() addsplits [option.split]) 1);
qed "override_None";
AddIffs [override_None];
@@ -66,12 +66,12 @@
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (rtac ext 1);
-by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
+by (asm_simp_tac (simpset() addsplits [option.split]) 1);
qed "map_of_append";
Addsimps [map_of_append];
Goal "map_of xs k = Some y --> (k,y):set xs";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (Simp_tac 1);
by (split_all_tac 1);
by (Asm_simp_tac 1);
@@ -91,7 +91,7 @@
Addsimps [dom_update];
qed_goalw "finite_dom_map_of" Map.thy [dom_def] "finite (dom (map_of l))" (K[
- list.induct_tac "l" 1,
+ induct_tac "l" 1,
ALLGOALS Simp_tac,
stac (insert_Collect RS sym) 1,
Asm_simp_tac 1]);
--- a/src/HOL/Map.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Map.thy Fri Jul 24 13:03:20 1998 +0200
@@ -37,8 +37,8 @@
dom_def "dom(m) == {a. m a ~= None}"
ran_def "ran(m) == {b. ? a. m a = Some b}"
-primrec map_of list
-"map_of [] = empty"
-"map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
+primrec
+ "map_of [] = empty"
+ "map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
end
--- a/src/HOL/Option.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Option.ML Fri Jul 24 13:03:20 1998 +0200
@@ -8,7 +8,7 @@
open Option;
qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
- (K [option.induct_tac "x" 1, Auto_tac]);
+ (K [induct_tac "x" 1, Auto_tac]);
section "case analysis in premises";
@@ -55,7 +55,7 @@
val option_map_eq_Some = prove_goalw thy [option_map_def]
"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)"
- (K [asm_full_simp_tac (simpset() addsplits [split_option_case]) 1]);
+ (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]);
AddIffs[option_map_eq_Some];
section "o2s";
--- a/src/HOL/Option.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Option.thy Fri Jul 24 13:03:20 1998 +0200
@@ -6,7 +6,7 @@
Datatype 'a option
*)
-Option = Arith +
+Option = Datatype +
datatype 'a option = None | Some 'a
@@ -22,8 +22,7 @@
o2s :: "'a option => 'a set"
-primrec o2s option
-
+primrec
"o2s None = {}"
"o2s (Some x) = {x}"
--- a/src/HOL/Power.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Power.thy Fri Jul 24 13:03:20 1998 +0200
@@ -11,11 +11,11 @@
consts
binomial :: "[nat,nat] => nat" ("'(_ choose _')" [50,50])
-primrec "op ^" nat
+primrec
"p ^ 0 = 1"
"p ^ (Suc n) = (p::nat) * (p ^ n)"
-primrec "binomial" nat
+primrec
binomial_0 "(0 choose k) = (if k = 0 then 1 else 0)"
binomial_Suc "(Suc n choose k) =
--- a/src/HOL/ROOT.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/ROOT.ML Fri Jul 24 13:03:20 1998 +0200
@@ -26,8 +26,6 @@
use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
-use "thy_data.ML";
-
use_thy "HOL";
use "hologic.ML";
use "cladata.ML";
@@ -42,13 +40,21 @@
use "Tools/record_package.ML";
use_thy "Record";
-use "datatype.ML";
-use_thy "Arith";
-use "arith_data.ML";
+use_thy "NatDef";
use "Tools/inductive_package.ML";
use_thy "Inductive";
+use "Tools/datatype_aux.ML";
+use "Tools/datatype_prop.ML";
+use "Tools/datatype_rep_proofs.ML";
+use "Tools/datatype_abs_proofs.ML";
+use "Tools/datatype_package.ML";
+use "Tools/primrec_package.ML";
+
+use_thy "Arith";
+use "arith_data.ML";
+
use_thy "RelPow";
use_thy "Finite";
use_thy "Sexp";
--- a/src/HOL/RelPow.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/RelPow.ML Fri Jul 24 13:03:20 1998 +0200
@@ -42,10 +42,9 @@
"[| (x,z) : R^n; [| n=0; x = z |] ==> P; \
\ !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P \
\ |] ==> P";
-by (res_inst_tac [("n","n")] natE 1);
by (cut_facts_tac [p1] 1);
+by (exhaust_tac "n" 1);
by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
-by (cut_facts_tac [p1] 1);
by (Asm_full_simp_tac 1);
by (etac compEpair 1);
by (REPEAT(ares_tac [p3] 1));
@@ -69,10 +68,9 @@
"[| (x,z) : R^n; [| n=0; x = z |] ==> P; \
\ !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P \
\ |] ==> P";
-by (res_inst_tac [("n","n")] natE 1);
by (cut_facts_tac [p1] 1);
+by (exhaust_tac "n" 1);
by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
-by (cut_facts_tac [p1] 1);
by (Asm_full_simp_tac 1);
by (etac compEpair 1);
by (dtac (conjI RS rel_pow_Suc_D2') 1);
--- a/src/HOL/RelPow.thy Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/RelPow.thy Fri Jul 24 13:03:20 1998 +0200
@@ -8,7 +8,7 @@
RelPow = Nat +
-primrec "op ^" nat
+primrec
"R^0 = id"
"R^(Suc n) = R O (R^n)"
--- a/src/HOL/Sum.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Sum.ML Fri Jul 24 13:03:20 1998 +0200
@@ -140,6 +140,11 @@
rtac (Rep_Sum_inverse RS sym)]));
qed "sumE";
+val prems = goal thy "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
+by (res_inst_tac [("s","x")] sumE 1);
+by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
+qed "sum_induct";
+
Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
by (EVERY1 [res_inst_tac [("s","s")] sumE,
etac ssubst, rtac sum_case_Inl,
--- a/src/HOL/thy_syntax.ML Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/thy_syntax.ML Fri Jul 24 13:03:20 1998 +0200
@@ -5,10 +5,6 @@
Additional theory file sections for HOL.
*)
-(*the kind of distinctiveness axioms depends on number of constructors*)
-val dtK = 7; (* FIXME rename?, move? *)
-
-
local
open ThyParse;
@@ -86,159 +82,119 @@
(** datatype **)
local
- (* FIXME err -> add_datatype *)
- fun mk_cons cs =
- (case duplicates (map (fst o fst) cs) of
- [] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
- | dups => error ("Duplicate constructors: " ^ commas_quote dups));
+ (*** generate string for calling add_datatype ***)
+ (*** and bindig theorems to ML identifiers ***)
- (*generate names of distinctiveness axioms*)
- fun mk_distinct_rules cs tname =
+ fun mk_bind_thms_string names =
+ (case find_first (not o Syntax.is_identifier) names of
+ Some id => (warning (id ^ " is not a valid identifier"); "")
+ | None =>
+ let
+ fun mk_dt_struct (s, (id, i)) =
+ s ^ "structure " ^ id ^ " =\n\
+ \struct\n\
+ \ val distinct = nth_elem (" ^ i ^ ", distinct);\n\
+ \ val inject = nth_elem (" ^ i ^ ", inject);\n\
+ \ val exhaust = nth_elem (" ^ i ^ ", exhaustion);\n\
+ \ val cases = nth_elem (" ^ i ^ ", case_thms);\n\
+ \ val (split, split_asm) = nth_elem (" ^ i ^ ", split_thms);\n" ^
+ (if length names = 1 then
+ " val induct = induction;\n\
+ \ val recs = rec_thms;\n\
+ \ val simps = simps;\n\
+ \ val size = size;\n"
+ else "") ^
+ "end;\n";
+
+ val structs = foldl mk_dt_struct
+ ("", (names ~~ (map string_of_int (0 upto length names - 1))));
+
+ in
+ (if length names > 1 then
+ "structure " ^ (space_implode "_" names) ^ " =\n\
+ \struct\n\
+ \val induct = induction;\n\
+ \val recs = rec_thms;\n\
+ \val simps = simps;\n\
+ \val size = size;\n"
+ else "") ^ structs ^
+ (if length names > 1 then "end;\n" else "")
+ end);
+
+ fun mk_dt_string dts =
let
- val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
- (*combine all constructor names with all others w/o duplicates*)
- fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
- fun neg1 [] = []
- | neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
+ val names = map (fn ((((alt_name, _), name), _), _) =>
+ strip_quotes (if_none alt_name name)) dts;
+
+ val add_datatype_args = brackets (commas (map quote names)) ^ " " ^
+ brackets (commas (map (fn ((((_, vs), name), mx), cs) =>
+ parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^
+ brackets (commas cs))) dts));
+
in
- if length uqcs < dtK then neg1 uqcs
- else quote (tname ^ "_ord_distinct") ::
- map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
+ ";\nlocal\n\
+ \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
+ \ case_thms, split_thms, induction, size, simps}) =\n\
+ \ DatatypePackage.add_datatype " ^ add_datatype_args ^ " thy;\n\
+ \in\n" ^ mk_bind_thms_string names ^
+ "val thy = thy;\nend;\nval thy = thy\n"
end;
- fun mk_rules tname cons pre = " map (get_axiom thy) " ^
- mk_list (map (fn ((s,_), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
+ fun mk_rep_dt_string (((names, distinct), inject), induct) =
+ ";\nlocal\n\
+ \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
+ \ case_thms, split_thms, induction, size, simps}) =\n\
+ \ DatatypePackage.add_rep_datatype " ^
+ (case names of
+ Some names => "(Some [" ^ commas (map quote names) ^ "]) (" ^
+ distinct ^ ") (" ^ inject ^ ") (" ^ induct ^ ") thy;\nin\n" ^
+ mk_bind_thms_string names
+ | None => "None (" ^ distinct ^ ") (" ^ inject ^ ") (" ^ induct ^
+ ") thy;\nin\n") ^
+ "val thy = thy;\nend;\nval thy = thy\n";
- (*generate string for calling add_datatype and build_record*)
- fun mk_params ((ts, tname), cons) =
- "val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqns) =\n\
- \ Datatype.add_datatype\n"
- ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
- \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)\n\
- \val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
- \ (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
- \structure " ^ tname ^ " =\n\
- \struct\n\
- \ val inject = map (get_axiom thy) " ^
- mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
- (filter_out (null o snd o fst) cons)) ^ ";\n\
- \ val distinct = " ^
- (if length cons < dtK then "let val distinct' = " else "") ^
- "map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
- (if length cons < dtK then
- " in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
- \ distinct') end"
- else "") ^ ";\n\
- \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
- \ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
- \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
- \ val simps = inject @ distinct @ cases @ recs;\n\
- \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
- \end;\n\
- \val thy = thy |> Dtype.add_record " ^
- mk_triple
- ("Sign.intern_tycon (sign_of thy) " ^ quote tname,
- mk_list (map (fst o fst) cons),
- tname ^ ".induct_tac") ^ ";\n\
- \val dummy = context thy;\n\
- \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
- \val dummy = AddIffs " ^ tname ^ ".inject;\n\
- \val dummy = " ^
- (if length cons < dtK then "AddIffs " else "Addsimps ") ^
- tname ^ ".distinct;\n\
- \val dummy = Addsimps(map (fn (_,eqn) =>\n\
- \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
- "] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\
- \val split_"^tname^"_case = prove_goal thy (#1(split_"^tname^"_eqns))\n\
- \ (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
- ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
- \ ALLGOALS Asm_simp_tac]);\n\
- \val split_"^tname^"_case_asm = prove_goal thy (#2(split_"^tname^"_eqns))\n\
- \ (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
- ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
- \ ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex]))]);\n\
- \val thy = thy\n";
+ (*** parsers ***)
-(*
-The #exhaust_tac(snd(hd(!datatypes))) in the proof of split_"^tname^"_case
-is a hack. Ideally I would just write exhaust_tac, but the latter extracts the
-specific exhaustion tactic from the theory associated with the proof
-state. However, the exhaustion tactic for the current datatype has only just
-been added to !datatypes (a few lines above) but is not yet associated with
-the theory. Hope this can be simplified in the future.
-*)
-
- (*parsers*)
- val tvars = type_args >> map (cat "dtVar");
-
- val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) ||
- type_var >> cat "dtVar";
+ val simple_typ = ident || (type_var >> strip_quotes);
fun complex_typ toks =
let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
in
- (typ -- repeat (ident>>quote) >>
- (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) ||
- "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >>
- (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^
- mk_pair (brackets x, y)) (commas fst, ids))) toks
+ (typ ^^ (repeat ident >> (cat "" o space_implode " ")) ||
+ "(" $$-- !! (list1 typ2 >> (parens o commas)) --$$ ")" ^^ !!
+ (repeat1 ident >> (cat "" o space_implode " "))) toks
end;
- val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
- val constructor = name -- opt_typs -- opt_mixfix;
+ val opt_typs = repeat ((string >> strip_quotes) ||
+ simple_typ || ("(" $$-- complex_typ --$$ ")"));
+ val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
+ parens (n ^ ", " ^ mx ^ ", " ^ brackets (commas (map quote Ts))));
+ val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None
+
in
val datatype_decl =
- tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
+ enum1 "and" (opt_name -- type_args -- name -- opt_infix --$$ "=" --
+ enum1 "|" constructor) >> mk_dt_string;
+ val rep_datatype_decl =
+ ((optional ((repeat1 (name >> strip_quotes)) >> Some) None) --
+ ("distinct" $$-- (name >> strip_quotes)) -- ("inject" $$--
+ (name >> strip_quotes)) -- ("induct" $$-- (name >> strip_quotes))) >>
+ mk_rep_dt_string;
end;
-
(** primrec **)
-(*recursion equations have user-supplied names*)
-fun mk_primrec_decl_1 ((fname, tname), axms) =
- let
- (*Isolate type name from the structure's identifier it may be stored in*)
- val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
-
- fun mk_prove (name, eqn) =
- "val " ^ name ^ " = store_thm (" ^ quote name
- ^ ", prove_goalw thy [get_def thy "
- ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\
- \ (fn _ => [Simp_tac 1]));";
-
- val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
- in ("|> " ^ tname ^ "_add_primrec " ^ axs
- ,
- cat_lines (map mk_prove axms)
- ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
- end;
+fun mk_primrec_decl (names, eqns) =
+ ";\nval (thy, " ^ (if null names then "_" else brackets (commas names)) ^
+ ") = PrimrecPackage.add_primrec " ^ brackets (commas eqns) ^ " thy;\n\
+ \val thy = thy\n";
-(*recursion equations have no names*)
-fun mk_primrec_decl_2 ((fname, tname), axms) =
- let
- (*Isolate type name from the structure's identifier it may be stored in*)
- val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
-
- fun mk_prove eqn =
- "prove_goalw thy [get_def thy "
- ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \
- \(fn _ => [Simp_tac 1])";
-
- val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
- in ("|> " ^ tname ^ "_add_primrec " ^ axs
- ,
- "val dummy = Addsimps " ^
- brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
- end;
-
-(*function name, argument type and either (name,axiom) pairs or just axioms*)
+(* either names and axioms or just axioms *)
val primrec_decl =
- (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
- (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
-
-
+ (repeat1 (ident -- string) >> (mk_primrec_decl o ListPair.unzip)) ||
+ (repeat1 string >> (mk_primrec_decl o (pair [])));
(** rec: interface to Slind's TFL **)
@@ -278,13 +234,15 @@
in
val _ = ThySyn.add_syntax
- ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
+ ["intrs", "monos", "con_defs", "congs", "simpset", "|",
+ "and", "distinct", "inject", "induct"]
[axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
section "record" "|> RecordPackage.add_record" record_decl,
section "inductive" "" (inductive_decl false),
section "coinductive" "" (inductive_decl true),
section "datatype" "" datatype_decl,
- ("primrec", primrec_decl),
+ section "rep_datatype" "" rep_datatype_decl,
+ section "primrec" "" primrec_decl,
("recdef", rec_decl)];
end;