# HG changeset patch # User berghofe # Date 901278200 -7200 # Node ID 89f162de39cf44c7dacef48b49b8aa84a85c2c69 # Parent 69917bbbce457832c1db23514da8ceaa00367361 Adapted to new datatype package. diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Arith.ML --- 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 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 - 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); diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Arith.thy --- 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)" diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Auth/Event.thy --- 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 diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Auth/Message.thy --- 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?*) diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Auth/Public.thy --- 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)" diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Auth/Shared.thy --- 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))}" diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Divides.ML --- 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 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]; diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Finite.ML --- 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 \ \ ? m::nat. m 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 diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Hoare/Examples.ML --- 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]))); diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Hoare/Hoare.ML --- 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, diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Hoare/Hoare.thy --- 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')" diff -r 69917bbbce45 -r 89f162de39cf src/HOL/IMP/Com.thy --- 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 diff -r 69917bbbce45 -r 89f162de39cf src/HOL/IMP/Denotation.ML --- 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-> t"; -by (com.induct_tac "c" 1); +by (induct_tac "c" 1); by (ALLGOALS Full_simp_tac); by (ALLGOALS (TRY o Fast_tac)); diff -r 69917bbbce45 -r 89f162de39cf src/HOL/IMP/Denotation.thy --- 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)" diff -r 69917bbbce45 -r 89f162de39cf src/HOL/IMP/Expr.ML --- 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))))); diff -r 69917bbbce45 -r 89f162de39cf src/HOL/IMP/Expr.thy --- 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))" diff -r 69917bbbce45 -r 89f162de39cf src/HOL/IMP/Hoare.ML --- 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); diff -r 69917bbbce45 -r 89f162de39cf src/HOL/IMP/Transition.ML --- 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"; diff -r 69917bbbce45 -r 89f162de39cf src/HOL/IMP/VC.ML --- 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"; diff -r 69917bbbce45 -r 89f162de39cf src/HOL/IMP/VC.thy --- 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; diff -r 69917bbbce45 -r 89f162de39cf src/HOL/IsaMakefile --- 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 diff -r 69917bbbce45 -r 89f162de39cf src/HOL/List.ML --- 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]) diff -r 69917bbbce45 -r 89f162de39cf src/HOL/List.thy --- 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 diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Map.ML --- 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]); diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Map.thy --- 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 diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Option.ML --- 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"; diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Option.thy --- 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}" diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Power.thy --- 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) = diff -r 69917bbbce45 -r 89f162de39cf src/HOL/ROOT.ML --- 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"; diff -r 69917bbbce45 -r 89f162de39cf src/HOL/RelPow.ML --- 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); diff -r 69917bbbce45 -r 89f162de39cf src/HOL/RelPow.thy --- 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)" diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Sum.ML --- 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, diff -r 69917bbbce45 -r 89f162de39cf src/HOL/thy_syntax.ML --- 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;