Adapted to new datatype package.
--- a/src/HOL/IOA/IOA.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/IOA/IOA.ML Fri Jul 24 13:19:38 1998 +0200
@@ -83,10 +83,10 @@
by (rename_tac "ex1 ex2 n" 1);
by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1);
by (Asm_full_simp_tac 1);
- by (nat_ind_tac "n" 1);
+ by (induct_tac "n" 1);
by (fast_tac (claset() addIs [p1,reachable_0]) 1);
- by (eres_inst_tac[("x","n")] allE 1);
- by (exhaust_tac "ex1 n" 1 THEN ALLGOALS Asm_full_simp_tac);
+ by (eres_inst_tac[("x","na")] allE 1);
+ by (exhaust_tac "ex1 na" 1 THEN ALLGOALS Asm_full_simp_tac);
by Safe_tac;
by (etac (p2 RS mp) 1);
by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
--- a/src/HOL/IOA/Solve.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/IOA/Solve.ML Fri Jul 24 13:19:38 1998 +0200
@@ -79,7 +79,7 @@
by (asm_full_simp_tac
(simpset() addsimps [executions_def,is_execution_fragment_def,
par_def,starts_of_def,trans_of_def,filter_oseq_def]
- addsplits [split_option_case]) 1);
+ addsplits [option.split]) 1);
qed"comp1_reachable";
@@ -99,7 +99,7 @@
by (asm_full_simp_tac
(simpset() addsimps [executions_def,is_execution_fragment_def,
par_def,starts_of_def,trans_of_def,filter_oseq_def]
- addsplits [split_option_case]) 1);
+ addsplits [option.split]) 1);
qed"comp2_reachable";
Delsplits [split_if];
@@ -161,7 +161,7 @@
by (asm_full_simp_tac
(simpset() addsimps [executions_def,is_execution_fragment_def,
par_def,starts_of_def,trans_of_def,rename_def]
- addsplits [split_option_case]) 1);
+ addsplits [option.split]) 1);
by (best_tac (claset() addSDs [spec] addDs [sym] addss (simpset())) 1);
qed"reachable_rename_ioa";
--- a/src/HOL/Induct/Com.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/Com.thy Fri Jul 24 13:19:38 1998 +0200
@@ -6,7 +6,7 @@
Example of Mutual Induction via Iteratived Inductive Definitions: Commands
*)
-Com = Arith + Inductive +
+Com = Datatype +
types loc
state = "loc => nat"
--- a/src/HOL/Induct/Comb.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/Comb.thy Fri Jul 24 13:19:38 1998 +0200
@@ -13,7 +13,7 @@
*)
-Comb = Arith + Inductive +
+Comb = Datatype +
(** Datatype definition of combinators S and K, with infixed application **)
datatype comb = K
--- a/src/HOL/Induct/LList.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/LList.ML Fri Jul 24 13:19:38 1998 +0200
@@ -155,10 +155,10 @@
by (safe_tac ((claset_of Fun.thy) delrules [equalityI]));
by (etac LListD.elim 1);
by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE]));
-by (res_inst_tac [("n", "n")] natE 1);
+by (exhaust_tac "n" 1);
by (Asm_simp_tac 1);
by (rename_tac "n'" 1);
-by (res_inst_tac [("n", "n'")] natE 1);
+by (exhaust_tac "n'" 1);
by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
qed "LListD_implies_ntrunc_equality";
@@ -317,9 +317,9 @@
by (stac prem2 1);
by (Simp_tac 1);
by (strip_tac 1);
-by (res_inst_tac [("n", "n")] natE 1);
+by (exhaust_tac "n" 1);
by (rename_tac "m" 2);
-by (res_inst_tac [("n", "m")] natE 2);
+by (exhaust_tac "m" 2);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
result();
@@ -782,12 +782,12 @@
Goal
"nat_rec (LCons b l) (%m. lmap(f)) n = \
\ LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "fun_power_lmap";
goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "fun_power_Suc";
--- a/src/HOL/Induct/Mutil.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/Mutil.ML Fri Jul 24 13:19:38 1998 +0200
@@ -44,7 +44,7 @@
qed "Sigma_Suc2";
Goal "{i} Times below(n+n) : tiling domino";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_Suc2])));
by (resolve_tac tiling.intrs 1);
by (assume_tac 2);
@@ -57,7 +57,7 @@
qed "dominoes_tile_row";
Goal "(below m) Times below(n+n) : tiling domino";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Sigma_Suc1])));
by (blast_tac (claset() addSIs [tiling_UnI, dominoes_tile_row]
addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
--- a/src/HOL/Induct/Perm.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/Perm.ML Fri Jul 24 13:19:38 1998 +0200
@@ -14,7 +14,7 @@
open Perm;
Goal "l <~~> l";
-by (list.induct_tac "l" 1);
+by (induct_tac "l" 1);
by (REPEAT (ares_tac perm.intrs 1));
qed "perm_refl";
@@ -50,7 +50,7 @@
(*We can insert the head anywhere in the list*)
Goal "a # xs @ ys <~~> xs @ a # ys";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (simp_tac (simpset() addsimps [perm_refl]) 1);
by (Simp_tac 1);
by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1);
@@ -63,7 +63,7 @@
*)
Goal "xs@ys <~~> ys@xs";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (simp_tac (simpset() addsimps [perm_refl]) 1);
by (Simp_tac 1);
by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1);
@@ -77,7 +77,7 @@
qed "perm_append_single";
Goal "rev xs <~~> xs";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (simp_tac (simpset() addsimps [perm_refl]) 1);
by (Simp_tac 1);
by (rtac (perm_append_single RS perm_sym RS perm.trans) 1);
@@ -85,7 +85,7 @@
qed "perm_rev";
Goal "xs <~~> ys ==> l@xs <~~> l@ys";
-by (list.induct_tac "l" 1);
+by (induct_tac "l" 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [perm.Cons]) 1);
qed "perm_append1";
--- a/src/HOL/Induct/PropLog.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/PropLog.ML Fri Jul 24 13:19:38 1998 +0200
@@ -102,7 +102,7 @@
(*This formulation is required for strong induction hypotheses*)
Goal "hyps p tt |- (if tt[p] then p else p->false)";
by (rtac (split_if RS iffD2) 1);
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H])));
by (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2,
weaken_right, imp_false]
@@ -140,7 +140,7 @@
(*For the case hyps(p,t)-insert(#v,Y) |- p;
we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
Goal "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
by (ALLGOALS Simp_tac);
by (Fast_tac 1);
qed "hyps_Diff";
@@ -148,7 +148,7 @@
(*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
Goal "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
by (ALLGOALS Simp_tac);
by (Fast_tac 1);
qed "hyps_insert";
@@ -169,7 +169,7 @@
qed "hyps_finite";
Goal "hyps p t <= (UN v. {#v, #v->false})";
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
by (ALLGOALS Simp_tac);
by (Blast_tac 1);
qed "hyps_subset";
--- a/src/HOL/Induct/PropLog.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/PropLog.thy Fri Jul 24 13:19:38 1998 +0200
@@ -6,7 +6,8 @@
Inductive definition of propositional logic.
*)
-PropLog = Finite +
+PropLog = Finite + Datatype +
+
datatype
'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
consts
@@ -32,12 +33,12 @@
sat_def "H |= p == (!tt. (!q:H. tt[q]) --> tt[p])"
eval_def "tt[p] == eval2 p tt"
-primrec eval2 pl
+primrec
"eval2(false) = (%x. False)"
"eval2(#v) = (%tt. v:tt)"
"eval2(p->q) = (%tt. eval2 p tt-->eval2 q tt)"
-primrec hyps pl
+primrec
"hyps(false) = (%tt.{})"
"hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
"hyps(p->q) = (%tt. hyps p tt Un hyps q tt)"
--- a/src/HOL/Integ/Bin.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Integ/Bin.ML Fri Jul 24 13:19:38 1998 +0200
@@ -106,7 +106,7 @@
qed_goal "integ_of_bin_norm_Bcons" Bin.thy
"integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
- (fn _ =>[(bin.induct_tac "w" 1),
+ (fn _ =>[(induct_tac "w" 1),
(ALLGOALS Simp_tac) ]);
qed_goal "integ_of_bin_succ" Bin.thy
@@ -140,11 +140,11 @@
Goal
"! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
-by (bin.induct_tac "v" 1);
+by (induct_tac "v" 1);
by (simp_tac (simpset() addsimps bin_add_simps) 1);
by (simp_tac (simpset() addsimps bin_add_simps) 1);
by (rtac allI 1);
-by (bin.induct_tac "w" 1);
+by (induct_tac "w" 1);
by (asm_simp_tac (simpset() addsimps (bin_add_simps)) 1);
by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
by (cut_inst_tac [("P","bool")] True_or_False 1);
@@ -162,7 +162,7 @@
integ_of_bin_norm_Bcons];
Goal "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
-by (bin.induct_tac "v" 1);
+by (induct_tac "v" 1);
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
by (cut_inst_tac [("P","bool")] True_or_False 1);
--- a/src/HOL/Integ/Bin.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Integ/Bin.thy Fri Jul 24 13:19:38 1998 +0200
@@ -22,7 +22,7 @@
quoting the previously computed values. (Or code an oracle...)
*)
-Bin = Integ +
+Bin = Integ + Datatype +
syntax
"_Int" :: xnum => int ("_")
@@ -43,42 +43,42 @@
(*norm_Bcons adds a bit, suppressing leading 0s and 1s*)
-primrec norm_Bcons bin
+primrec
norm_Plus "norm_Bcons PlusSign b = (if b then (Bcons PlusSign b) else PlusSign)"
norm_Minus "norm_Bcons MinusSign b = (if b then MinusSign else (Bcons MinusSign b))"
norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b"
-primrec integ_of_bin bin
+primrec
iob_Plus "integ_of_bin PlusSign = $#0"
iob_Minus "integ_of_bin MinusSign = $~($#1)"
iob_Bcons "integ_of_bin(Bcons w x) = (if x then $#1 else $#0) + (integ_of_bin w) + (integ_of_bin w)"
-primrec bin_succ bin
+primrec
succ_Plus "bin_succ PlusSign = Bcons PlusSign True"
succ_Minus "bin_succ MinusSign = PlusSign"
succ_Bcons "bin_succ(Bcons w x) = (if x then (Bcons (bin_succ w) False) else (norm_Bcons w True))"
-primrec bin_pred bin
+primrec
pred_Plus "bin_pred(PlusSign) = MinusSign"
pred_Minus "bin_pred(MinusSign) = Bcons MinusSign False"
pred_Bcons "bin_pred(Bcons w x) = (if x then (norm_Bcons w False) else (Bcons (bin_pred w) True))"
-primrec bin_minus bin
+primrec
min_Plus "bin_minus PlusSign = PlusSign"
min_Minus "bin_minus MinusSign = Bcons PlusSign True"
min_Bcons "bin_minus(Bcons w x) = (if x then (bin_pred (Bcons (bin_minus w) False)) else (Bcons (bin_minus w) False))"
-primrec bin_add bin
+primrec
add_Plus "bin_add PlusSign w = w"
add_Minus "bin_add MinusSign w = bin_pred w"
add_Bcons "bin_add (Bcons v x) w = h_bin v x w"
-primrec bin_mult bin
+primrec
mult_Plus "bin_mult PlusSign w = PlusSign"
mult_Minus "bin_mult MinusSign w = bin_minus w"
mult_Bcons "bin_mult (Bcons v x) w = (if x then (bin_add (norm_Bcons (bin_mult v w) False) w) else (norm_Bcons (bin_mult v w) False))"
-primrec h_bin bin
+primrec
h_Plus "h_bin v x PlusSign = Bcons v x"
h_Minus "h_bin v x MinusSign = bin_pred (Bcons v x)"
h_BCons "h_bin v x (Bcons w y) = norm_Bcons (bin_add v (if (x & y) then bin_succ w else w)) (x~=y)"
--- a/src/HOL/Integ/Integ.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Integ/Integ.ML Fri Jul 24 13:19:38 1998 +0200
@@ -173,12 +173,12 @@
(**** zmagnitude: magnitide of an integer, as a natural number ****)
goal Arith.thy "!!n::nat. n - Suc(n+m)=0";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "diff_Suc_add_0";
goal Arith.thy "Suc((n::nat)+m)-n=Suc(m)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "diff_Suc_add_inverse";
@@ -785,7 +785,7 @@
Goal "$~ $# n <= $#0";
by (rtac zless_or_eq_imp_zle 1);
- by (nat_ind_tac "n" 1);
+ by (induct_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "negative_zle_0";
Addsimps[negative_zle_0];
--- a/src/HOL/Lambda/Eta.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lambda/Eta.ML Fri Jul 24 13:19:38 1998 +0200
@@ -25,7 +25,7 @@
section "eta, subst and free";
Goal "!i t u. ~free s i --> s[t/i] = s[u/i]";
-by (dB.induct_tac "s" 1);
+by (induct_tac "s" 1);
by (ALLGOALS(simp_tac (addsplit (simpset()))));
by (Blast_tac 1);
by (Blast_tac 1);
@@ -33,10 +33,10 @@
Addsimps [subst_not_free RS eqTrueI];
Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
by (Blast_tac 2);
-by (simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1);
+by (simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
qed "free_lift";
@@ -44,12 +44,12 @@
Goal "!i k t. free (s[t/k]) i = \
\ (free s k & free t i | free s (if i<k then i else Suc i))";
-by (dB.induct_tac "s" 1);
+by (induct_tac "s" 1);
by (Asm_simp_tac 2);
by (Blast_tac 2);
by (asm_full_simp_tac (addsplit (simpset())) 2);
by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
- addsplits [split_nat_case]) 1);
+ addsplits [nat.split]) 1);
by (safe_tac (HOL_cs addSEs [nat_neqE]));
by (ALLGOALS trans_tac);
qed "free_subst";
@@ -123,7 +123,7 @@
AddIs [beta_subst];
Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS (asm_simp_tac (addsplit (simpset()))));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
by (ALLGOALS trans_tac);
@@ -137,7 +137,7 @@
Addsimps [eta_lift];
Goal "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
-by (dB.induct_tac "u" 1);
+by (induct_tac "u" 1);
by (ALLGOALS(asm_simp_tac (addsplit (simpset()))));
by (blast_tac (claset() addIs [r_into_rtrancl]) 1);
by (blast_tac (claset() addSIs [rtrancl_eta_App]) 1);
@@ -166,7 +166,7 @@
section "Implicit definition of -e>: Abs(lift s 0 $ Var 0) -e> s";
Goal "!i. (~free s i) = (? t. s = lift t i)";
-by (dB.induct_tac "s" 1);
+by (induct_tac "s" 1);
by (Simp_tac 1);
by (SELECT_GOAL(safe_tac HOL_cs)1);
by (etac nat_neqE 1);
--- a/src/HOL/Lambda/Eta.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lambda/Eta.thy Fri Jul 24 13:19:38 1998 +0200
@@ -19,7 +19,7 @@
"s -e>= t" == "(s,t) : eta^="
"s ->= t" == "(s,t) : beta^="
-primrec free Lambda.dB
+primrec
"free (Var j) i = (j=i)"
"free (s $ t) i = (free s i | free t i)"
"free (Abs s) i = free s (Suc i)"
--- a/src/HOL/Lambda/Lambda.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lambda/Lambda.ML Fri Jul 24 13:19:38 1998 +0200
@@ -66,16 +66,16 @@
Goal
"!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
qed_spec_mp "lift_lift";
Goal "!i j s. j < Suc i --> lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
- addsplits [split_nat_case]
+ addsplits [nat.split]
addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
@@ -84,7 +84,7 @@
Goal
"!i j s. i < Suc j --> lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift]
addSolver cut_trans_tac)));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
@@ -92,18 +92,18 @@
qed "lift_subst_lt";
Goal "!k s. (lift t k)[s/k] = t";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "subst_lift";
Addsimps [subst_lift];
Goal "!i j u v. i < Suc j --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac
(simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
delsplits [split_if]
- addsplits [split_nat_case]
+ addsplits [nat.split]
addloop ("if",split_inside_tac[split_if])
addSolver cut_trans_tac)));
by (safe_tac (HOL_cs addSEs [nat_neqE]));
@@ -114,20 +114,20 @@
(*** Equivalence proof for optimized substitution ***)
Goal "!k. liftn 0 t k = t";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
qed "liftn_0";
Addsimps [liftn_0];
Goal "!k. liftn (Suc n) t k = lift (liftn n t k) k";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
by (blast_tac (claset() addDs [add_lessD1]) 1);
qed "liftn_lift";
Addsimps [liftn_lift];
Goal "!n. substn t s n = t[liftn n s 0 / n]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
qed "substn_subst_n";
Addsimps [substn_subst_n];
--- a/src/HOL/Lambda/Lambda.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lambda/Lambda.thy Fri Jul 24 13:19:38 1998 +0200
@@ -7,7 +7,7 @@
substitution and beta-reduction.
*)
-Lambda = Arith + Inductive +
+Lambda = Datatype +
datatype dB = Var nat | "$" dB dB (infixl 200) | Abs dB
@@ -18,23 +18,23 @@
substn :: [dB,dB,nat] => dB
liftn :: [nat,dB,nat] => dB
-primrec lift dB
+primrec
"lift (Var i) k = (if i < k then Var i else Var(Suc i))"
"lift (s $ t) k = (lift s k) $ (lift t k)"
"lift (Abs s) k = Abs(lift s (Suc k))"
-primrec subst dB
+primrec
subst_Var "(Var i)[s/k] = (if k < i then Var(i-1)
else if i = k then s else Var i)"
subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]"
subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])"
-primrec liftn dB
+primrec
"liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
"liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)"
"liftn n (Abs s) k = Abs(liftn n s (Suc k))"
-primrec substn dB
+primrec
"substn (Var i) s k = (if k < i then Var(i-1)
else if i = k then liftn k s 0 else Var i)"
"substn (t $ u) s k = (substn t s k) $ (substn u s k)"
--- a/src/HOL/Lambda/ParRed.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lambda/ParRed.ML Fri Jul 24 13:19:38 1998 +0200
@@ -26,7 +26,7 @@
Addsimps [par_beta_varL];
Goal "t => t";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed"par_beta_refl";
Addsimps [par_beta_refl];
@@ -52,14 +52,14 @@
(*** => ***)
Goal "!t' n. t => t' --> lift t n => lift t' n";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS(fast_tac (claset() addss (simpset()))));
qed_spec_mp "par_beta_lift";
Addsimps [par_beta_lift];
Goal
"!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (asm_simp_tac (addsplit(simpset())) 1);
by (strip_tac 1);
by (eresolve_tac par_beta_cases 1);
--- a/src/HOL/Lex/AutoChopper.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/AutoChopper.thy Fri Jul 24 13:19:38 1998 +0200
@@ -29,7 +29,8 @@
consts
acc :: "[('a,'s)da, 's, 'a list list*'a list, 'a list, 'a list, 'a list]
=> 'a list list * 'a list"
-primrec acc List.list
+
+primrec
"acc A s r ps [] zs = (if ps=[] then r else (ps#fst(r),snd(r)))"
"acc A s r ps (x#xs) zs =
(let t = next A x s
--- a/src/HOL/Lex/AutoMaxChop.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/AutoMaxChop.thy Fri Jul 24 13:19:38 1998 +0200
@@ -8,7 +8,7 @@
consts
auto_split :: "('a,'s)da => 's => 'a list * 'a list => 'a list => 'a splitter"
-primrec auto_split list
+primrec
"auto_split A q res ps [] = (if fin A q then (ps,[]) else res)"
"auto_split A q res ps (x#xs) =
auto_split A (next A x q) (if fin A q then (ps,x#xs) else res) (ps@[x]) xs"
--- a/src/HOL/Lex/MaxChop.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/MaxChop.ML Fri Jul 24 13:19:38 1998 +0200
@@ -84,7 +84,7 @@
addsplits [split_split]) 1);
by (Clarify_tac 1);
by (rename_tac "xs1 ys1 xss1 ys" 1);
-by (split_asm_tac [split_list_case_asm] 1);
+by (split_asm_tac [list.split_asm] 1);
by (Asm_full_simp_tac 1);
by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
--- a/src/HOL/Lex/MaxPrefix.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/MaxPrefix.thy Fri Jul 24 13:19:38 1998 +0200
@@ -19,7 +19,7 @@
consts
maxsplit :: "('a list => bool) => 'a list * 'a list => 'a list => 'a splitter"
-primrec maxsplit list
+primrec
"maxsplit P res ps [] = (if P ps then (ps,[]) else res)"
"maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res)
(ps@[q]) qs"
--- a/src/HOL/Lex/NA.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/NA.thy Fri Jul 24 13:19:38 1998 +0200
@@ -11,7 +11,7 @@
types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)"
consts delta :: "('a,'s)na => 'a list => 's => 's set"
-primrec delta list
+primrec
"delta A [] p = {p}"
"delta A (a#w) p = Union(delta A w `` next A a p)"
--- a/src/HOL/Lex/NAe.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/NAe.thy Fri Jul 24 13:19:38 1998 +0200
@@ -18,7 +18,7 @@
translations "eps A" == "step A None"
consts steps :: "('a,'s)nae => 'a list => ('s * 's)set"
-primrec steps list
+primrec
"steps A [] = (eps A)^*"
"steps A (a#w) = steps A w O step A (Some a) O (eps A)^*"
@@ -28,7 +28,7 @@
(* not really used:
consts delta :: "('a,'s)nae => 'a list => 's => 's set"
-primrec delta list
+primrec
"delta A [] s = (eps A)^* ^^ {s}"
"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ^^ {s}))"
*)
--- a/src/HOL/Lex/Prefix.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/Prefix.ML Fri Jul 24 13:19:38 1998 +0200
@@ -7,7 +7,7 @@
(* Junk: *)
val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)";
by (rtac allI 1);
-by (list.induct_tac "l" 1);
+by (induct_tac "l" 1);
by (rtac maj 1);
by (rtac min 1);
val list_cases = result();
@@ -37,7 +37,7 @@
AddIffs[Nil_prefix];
Goalw [prefix_def] "(xs <= []) = (xs = [])";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (Simp_tac 1);
by (Simp_tac 1);
qed "prefix_Nil";
@@ -83,7 +83,7 @@
(* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
Goalw [prefix_def]
"(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Fast_tac 1);
--- a/src/HOL/Lex/RegExp.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/RegExp.thy Fri Jul 24 13:19:38 1998 +0200
@@ -15,7 +15,7 @@
| Star ('a rexp)
consts lang :: 'a rexp => 'a list set
-primrec lang rexp
+primrec
lang_Emp "lang Empty = {}"
lang_Atom "lang (Atom a) = {[a]}"
lang_Un "lang (Union el er) = (lang el) Un (lang er)"
--- a/src/HOL/Lex/RegExp2NAe.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML Fri Jul 24 13:19:38 1998 +0200
@@ -446,7 +446,7 @@
Goalw [conc_def]
"!L R. fin(conc L R) p = (? s. p = False#s & fin R s)";
-by (simp_tac (simpset() addsplits [split_list_case]) 1);
+by (simp_tac (simpset() addsplits [list.split]) 1);
qed_spec_mp "final_conc";
Goal
--- a/src/HOL/Lex/RegExp2NAe.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/RegExp2NAe.thy Fri Jul 24 13:19:38 1998 +0200
@@ -50,7 +50,7 @@
%s. case s of [] => True | left#s => left & f s)"
consts rexp2nae :: 'a rexp => 'a bitsNAe
-primrec rexp2nae rexp
+primrec
"rexp2nae Empty = ([], %a s. {}, %s. False)"
"rexp2nae(Atom a) = atom a"
"rexp2nae(Union r s) = union (rexp2nae r) (rexp2nae s)"
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML Fri Jul 24 13:19:38 1998 +0200
@@ -140,7 +140,7 @@
"!i j xs. xs : regset d i j k = \
\ ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)";
by (induct_tac "k" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [split_list_case]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong] addsplits [list.split]) 1);
by (strip_tac 1);
by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
by (rtac iffI 1);
@@ -149,12 +149,12 @@
by (REPEAT(eresolve_tac[exE,conjE] 1));
by (Asm_full_simp_tac 1);
by (subgoal_tac
- "(!n:set(butlast(trace d k xsb)). n < Suc k) & deltas d xsb k = k" 1);
+ "(!m:set(butlast(trace d n xsb)). m < Suc n) & deltas d xsb n = n" 1);
by (asm_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
by (etac star.induct 1);
by (Simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
-by (case_tac "k : set(butlast(trace d i xs))" 1);
+by (case_tac "n : set(butlast(trace d i xs))" 1);
by (rtac disjI1 2);
by (blast_tac (claset() addIs [lemma]) 2);
by (rtac disjI2 1);
--- a/src/HOL/Lex/RegSet_of_nat_DA.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.thy Fri Jul 24 13:19:38 1998 +0200
@@ -23,14 +23,14 @@
translations "deltas" == "foldl2"
consts trace :: 'a nat_next => nat => 'a list => nat list
-primrec trace list
+primrec
"trace d i [] = []"
"trace d i (x#xs) = d x i # trace d (d x i) xs"
(* conversion a la Warshall *)
consts regset :: 'a nat_next => nat => nat => nat => 'a list set
-primrec regset nat
+primrec
"regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j}
else {[a] | a. d a i = j})"
"regset d i j (Suc k) = regset d i j k Un
--- a/src/HOL/MiniML/Generalize.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Generalize.ML Fri Jul 24 13:19:38 1998 +0200
@@ -7,12 +7,12 @@
AddSEs [equalityE];
Goal "free_tv A = free_tv B ==> gen A t = gen B t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "gen_eq_on_free_tv";
Goal "(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Asm_simp_tac 1);
by (Simp_tac 1);
by (Fast_tac 1);
@@ -21,7 +21,7 @@
Addsimps [gen_without_effect];
Goal "free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Simp_tac 1);
by (case_tac "nat : free_tv ($ S A)" 1);
by (Asm_simp_tac 1);
@@ -42,7 +42,7 @@
Addsimps [free_tv_gen_cons];
Goal "bound_tv (gen A t1) = (free_tv t1) - (free_tv A)";
-by (typ.induct_tac "t1" 1);
+by (induct_tac "t1" 1);
by (Simp_tac 1);
by (case_tac "nat : free_tv A" 1);
by (Asm_simp_tac 1);
@@ -55,7 +55,7 @@
Addsimps [bound_tv_gen];
Goal "new_tv n t --> new_tv n (gen A t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Simp_tac 1);
by (case_tac "nat : free_tv A" 1);
by (Asm_simp_tac 1);
@@ -63,7 +63,7 @@
qed_spec_mp "new_tv_compatible_gen";
Goalw [gen_ML_def] "gen A t = gen_ML A t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
qed "gen_eq_gen_ML";
@@ -85,7 +85,7 @@
qed_spec_mp "gen_subst_commutes";
Goal "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
by (Fast_tac 1);
qed_spec_mp "bound_typ_inst_gen";
@@ -96,7 +96,7 @@
by Safe_tac;
by (rename_tac "R" 1);
by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "gen_bound_typ_instance";
@@ -106,7 +106,7 @@
by Safe_tac;
by (rename_tac "S" 1);
by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Asm_simp_tac 1);
by (Fast_tac 1);
by (Asm_simp_tac 1);
@@ -119,7 +119,7 @@
by (etac exE 1);
by (hyp_subst_tac 1);
by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Simp_tac 1);
by (case_tac "nat : free_tv A" 1);
by (Asm_simp_tac 1);
--- a/src/HOL/MiniML/Generalize.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Generalize.thy Fri Jul 24 13:19:38 1998 +0200
@@ -16,7 +16,7 @@
consts
gen :: [ctxt, typ] => type_scheme
-primrec gen typ
+primrec
"gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
"gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
@@ -25,7 +25,7 @@
consts
gen_ML_aux :: [nat list, typ] => type_scheme
-primrec gen_ML_aux typ
+primrec
"gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
"gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
--- a/src/HOL/MiniML/Instance.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Instance.ML Fri Jul 24 13:19:38 1998 +0200
@@ -10,14 +10,14 @@
(* lemmatas for bound_typ_inst *)
Goal "bound_typ_inst S (mk_scheme t) = t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "bound_typ_inst_mk_scheme";
Addsimps [bound_typ_inst_mk_scheme];
Goal "bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "bound_typ_inst_composed_subst";
@@ -32,7 +32,7 @@
(* lemmatas for bound_scheme_inst *)
Goal "bound_scheme_inst B (mk_scheme t) = mk_scheme t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "bound_scheme_inst_mk_scheme";
@@ -40,7 +40,7 @@
Addsimps [bound_scheme_inst_mk_scheme];
Goal "$S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
@@ -48,7 +48,7 @@
Goal "!t. mk_scheme t = bound_scheme_inst B sch --> \
\ (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (Simp_tac 1);
by Safe_tac;
by (rtac exI 1);
@@ -81,7 +81,7 @@
Goal "new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
\ (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (simp_tac (simpset() addsimps [leD]) 1);
by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1);
by (Asm_simp_tac 1);
@@ -96,7 +96,7 @@
Goal "new_tv n sch --> \
\ subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
\ bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (simp_tac (simpset() addsimps [leD]) 1);
by (Asm_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [leD]) 1);
@@ -127,7 +127,7 @@
by (asm_simp_tac (simpset() addsimps [aux2]) 1);
by Safe_tac;
by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
@@ -145,7 +145,7 @@
by (rotate_tac 1 1);
by (rtac mp 1);
by (assume_tac 2);
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
by (Fast_tac 1);
@@ -154,7 +154,7 @@
by (etac exE 1);
by (Asm_full_simp_tac 1);
by (rtac exI 1);
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
@@ -172,7 +172,7 @@
by (rtac conjI 1);
by (Fast_tac 1);
by (rtac allI 1);
-by (nat_ind_tac "i" 1);
+by (induct_tac "i" 1);
by (ALLGOALS Asm_simp_tac);
qed "le_env_Cons";
AddIffs [le_env_Cons];
@@ -221,7 +221,7 @@
Goalw [le_type_scheme_def,is_bound_typ_instance]
"(sch <= FVar n) = (sch = FVar n)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Fast_tac 1);
@@ -249,26 +249,26 @@
qed "Fun_le_FunD";
Goal "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
-by (type_scheme.induct_tac "sch'" 1);
+by (induct_tac "sch'" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
by (Fast_tac 1);
qed_spec_mp "scheme_le_Fun";
Goal "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (rtac allI 1);
- by (type_scheme.induct_tac "sch'" 1);
+ by (induct_tac "sch'" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (rtac allI 1);
- by (type_scheme.induct_tac "sch'" 1);
+ by (induct_tac "sch'" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (rtac allI 1);
-by (type_scheme.induct_tac "sch'" 1);
+by (induct_tac "sch'" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
@@ -278,10 +278,10 @@
qed_spec_mp "le_type_scheme_free_tv";
Goal "!A::type_scheme list. A <= B --> free_tv B <= free_tv A";
-by (list.induct_tac "B" 1);
+by (induct_tac "B" 1);
by (Simp_tac 1);
by (rtac allI 1);
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (simp_tac (simpset() addsimps [le_env_def]) 1);
by (Simp_tac 1);
by (fast_tac (claset() addDs [le_type_scheme_free_tv]) 1);
--- a/src/HOL/MiniML/Instance.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Instance.thy Fri Jul 24 13:19:38 1998 +0200
@@ -14,7 +14,7 @@
consts
bound_typ_inst :: [subst, type_scheme] => typ
-primrec bound_typ_inst type_scheme
+primrec
"bound_typ_inst S (FVar n) = (TVar n)"
"bound_typ_inst S (BVar n) = (S n)"
"bound_typ_inst S (sch1 =-> sch2) = ((bound_typ_inst S sch1) -> (bound_typ_inst S sch2))"
@@ -22,7 +22,7 @@
consts
bound_scheme_inst :: [nat => type_scheme, type_scheme] => type_scheme
-primrec bound_scheme_inst type_scheme
+primrec
"bound_scheme_inst S (FVar n) = (FVar n)"
"bound_scheme_inst S (BVar n) = (S n)"
"bound_scheme_inst S (sch1 =-> sch2) = ((bound_scheme_inst S sch1) =-> (bound_scheme_inst S sch2))"
@@ -38,7 +38,7 @@
consts
subst_to_scheme :: [nat => type_scheme, typ] => type_scheme
-primrec subst_to_scheme typ
+primrec
"subst_to_scheme B (TVar n) = (B n)"
"subst_to_scheme B (t1 -> t2) = ((subst_to_scheme B t1) =-> (subst_to_scheme B t2))"
--- a/src/HOL/MiniML/Maybe.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Maybe.ML Fri Jul 24 13:19:38 1998 +0200
@@ -18,7 +18,7 @@
(* expansion of option_bind *)
Goalw [option_bind_def] "P(option_bind res f) = \
\ ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
-by (rtac split_option_case 1);
+by (rtac option.split 1);
qed "split_option_bind";
Goal
--- a/src/HOL/MiniML/MiniML.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/MiniML.ML Fri Jul 24 13:19:38 1998 +0200
@@ -47,22 +47,22 @@
qed "alpha_A";
Goal "$ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS (Asm_full_simp_tac));
qed "S_o_alpha_typ";
Goal "$ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS (Asm_full_simp_tac));
val S_o_alpha_typ' = result ();
Goal "$ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (ALLGOALS (Asm_full_simp_tac));
qed "S_o_alpha_type_scheme";
Goal "$ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (ALLGOALS (Asm_full_simp_tac));
by (rtac (rewrite_rule [o_def] S_o_alpha_type_scheme) 1);
qed "S_o_alpha_type_scheme_list";
@@ -106,7 +106,7 @@
Goal "!!t1::typ. \
\ (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
\ {x. ? y. x = n + y}";
-by (typ.induct_tac "t1" 1);
+by (induct_tac "t1" 1);
by (Simp_tac 1);
by (Fast_tac 1);
by (Simp_tac 1);
@@ -143,7 +143,7 @@
Goal "!A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}";
by (rtac allI 1);
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (fast_tac (claset() addDs [new_tv_Int_free_tv_empty_scheme ]) 1);
@@ -155,7 +155,7 @@
by (etac exE 1);
by (hyp_subst_tac 1);
by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Simp_tac 1);
by (case_tac "nat : free_tv A" 1);
by (Asm_simp_tac 1);
--- a/src/HOL/MiniML/Type.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Type.ML Fri Jul 24 13:19:38 1998 +0200
@@ -10,33 +10,33 @@
(* lemmata for make scheme *)
Goal "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
by (Fast_tac 1);
qed_spec_mp "mk_scheme_Fun";
Goal "!t'. mk_scheme t = mk_scheme t' --> t=t'";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (rtac allI 1);
- by (typ.induct_tac "t'" 1);
+ by (induct_tac "t'" 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
-by (typ.induct_tac "t'" 1);
+by (induct_tac "t'" 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
qed_spec_mp "mk_scheme_injective";
Goal "free_tv (mk_scheme t) = free_tv t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "free_tv_mk_scheme";
Addsimps [free_tv_mk_scheme];
Goal "$ S (mk_scheme t) = mk_scheme ($ S t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "subst_mk_scheme";
@@ -110,14 +110,14 @@
Goal "new_tv n (sch::type_scheme) --> \
\ $(%k. if k<n then S k else S' k) sch = $S sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (ALLGOALS Asm_simp_tac);
qed "new_if_subst_type_scheme";
Addsimps [new_if_subst_type_scheme];
Goal "new_tv n (A::type_scheme list) --> \
\ $(%k. if k<n then S k else S' k) A = $S A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (ALLGOALS Asm_simp_tac);
qed "new_if_subst_type_scheme_list";
Addsimps [new_if_subst_type_scheme_list];
@@ -147,7 +147,7 @@
Addsimps [free_tv_id_subst];
Goal "!n. n < length A --> x : free_tv (A!n) --> x : free_tv A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
by (res_inst_tac [("n","n")] nat_induct 1);
@@ -158,7 +158,7 @@
Addsimps [free_tv_nth_A_impl_free_tv_A];
Goal "!nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
by (res_inst_tac [("n","nat")] nat_induct 1);
@@ -173,7 +173,7 @@
occurring in the type structure *)
Goal "(!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
qed_spec_mp "typ_substitutions_only_on_free_variables";
@@ -184,7 +184,7 @@
qed "eq_free_eq_subst_te";
Goal "(!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
@@ -198,7 +198,7 @@
Goal
"(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
(* case [] *)
by (fast_tac (HOL_cs addss simpset()) 1);
(* case x#xl *)
@@ -210,7 +210,7 @@
val weaken_asm_Un = result ();
Goal "(!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
by (rtac weaken_asm_Un 1);
@@ -220,7 +220,7 @@
Goal
"$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
(* case TVar n *)
by (fast_tac (HOL_cs addss simpset()) 1);
(* case Fun t1 t2 *)
@@ -229,7 +229,7 @@
Goal
"$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
(* case TVar n *)
by (Asm_simp_tac 1);
(* case BVar n *)
@@ -242,7 +242,7 @@
Goal
"$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
(* case [] *)
by (fast_tac (HOL_cs addss simpset()) 1);
(* case x#xl *)
@@ -281,7 +281,7 @@
qed "free_tv_subst_var";
Goal "free_tv ($ S (t::typ)) <= cod S Un free_tv t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
(* case TVar n *)
by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
(* case Fun t1 t2 *)
@@ -289,7 +289,7 @@
qed "free_tv_app_subst_te";
Goal "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
(* case FVar n *)
by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
(* case BVar n *)
@@ -299,7 +299,7 @@
qed "free_tv_app_subst_type_scheme";
Goal "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
(* case [] *)
by (Simp_tac 1);
(* case a#al *)
@@ -322,14 +322,14 @@
qed "free_tv_o_subst";
Goal "n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Fast_tac 1);
qed_spec_mp "free_tv_of_substitutions_extend_to_types";
Goal "n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (Simp_tac 1);
@@ -337,7 +337,7 @@
qed_spec_mp "free_tv_of_substitutions_extend_to_schemes";
Goal "n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_schemes]) 1);
@@ -346,14 +346,14 @@
Addsimps [free_tv_of_substitutions_extend_to_scheme_lists];
Goal "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (ALLGOALS Asm_simp_tac);
by (strip_tac 1);
by (Fast_tac 1);
qed "free_tv_ML_scheme";
Goal "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme]) 1);
qed "free_tv_ML_scheme_list";
@@ -362,14 +362,14 @@
(* lemmata for bound_tv *)
Goal "bound_tv (mk_scheme t) = {}";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "bound_tv_mk_scheme";
Addsimps [bound_tv_mk_scheme];
Goal "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (ALLGOALS Asm_simp_tac);
qed "bound_tv_subst_scheme";
@@ -410,28 +410,28 @@
Goal
"new_tv n = list_all (new_tv n)";
by (rtac ext 1);
-by (list.induct_tac "x" 1);
+by (induct_tac "x" 1);
by (ALLGOALS Asm_simp_tac);
qed "new_tv_list";
(* substitution affects only variables occurring freely *)
Goal
"new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "subst_te_new_tv";
Addsimps [subst_te_new_tv];
Goal
"new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (ALLGOALS Asm_simp_tac);
qed_spec_mp "subst_te_new_type_scheme";
Addsimps [subst_te_new_type_scheme];
Goal
"new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (ALLGOALS Asm_full_simp_tac);
qed_spec_mp "subst_tel_new_scheme_list";
Addsimps [subst_tel_new_scheme_list];
@@ -466,13 +466,13 @@
Goal
"new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
qed_spec_mp "new_tv_subst_te";
Addsimps [new_tv_subst_te];
Goal "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (ALLGOALS (Asm_full_simp_tac));
by (rewtac new_tv_def);
by (simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1);
@@ -487,7 +487,7 @@
Goal
"new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (ALLGOALS(fast_tac (HOL_cs addss (simpset()))));
qed_spec_mp "new_tv_subst_scheme_list";
Addsimps [new_tv_subst_scheme_list];
@@ -495,7 +495,7 @@
Goal
"new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
by (simp_tac (simpset() addsimps [new_tv_list]) 1);
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "new_tv_Suc_list";
@@ -509,7 +509,7 @@
Goalw [new_tv_def]
"!nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
by (res_inst_tac [("n","nat")] nat_induct 1);
@@ -549,7 +549,7 @@
val less_maxR = result();
Goalw [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (res_inst_tac [("x","Suc nat")] exI 1);
by (Asm_simp_tac 1);
by (REPEAT (etac exE 1));
@@ -562,7 +562,7 @@
Addsimps [fresh_variable_types];
Goalw [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (res_inst_tac [("x","Suc nat")] exI 1);
by (Simp_tac 1);
by (res_inst_tac [("x","Suc nat")] exI 1);
@@ -586,7 +586,7 @@
val le_maxR = result();
Goal "!!A::type_scheme list. ? n. (new_tv n A)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (etac exE 1);
@@ -648,7 +648,7 @@
Addsimps [length_app_subst_list];
Goal "!!sch::type_scheme. $ TVar sch = sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (ALLGOALS Asm_simp_tac);
qed "subst_TVar_scheme";
@@ -665,7 +665,7 @@
Goalw [id_subst_def]
"$ id_subst = (%t::typ. t)";
by (rtac ext 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "app_subst_id_te";
Addsimps [app_subst_id_te];
@@ -673,7 +673,7 @@
Goalw [id_subst_def]
"$ id_subst = (%sch::type_scheme. sch)";
by (rtac ext 1);
-by (type_scheme.induct_tac "t" 1);
+by (induct_tac "sch" 1);
by (ALLGOALS Asm_simp_tac);
qed "app_subst_id_type_scheme";
Addsimps [app_subst_id_type_scheme];
@@ -682,20 +682,20 @@
Goalw [app_subst_list]
"$ id_subst = (%A::type_scheme list. A)";
by (rtac ext 1);
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (ALLGOALS Asm_simp_tac);
qed "app_subst_id_tel";
Addsimps [app_subst_id_tel];
Goal "!!sch::type_scheme. $ id_subst sch = sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [id_subst_def])));
qed "id_subst_sch";
Addsimps [id_subst_sch];
Goal "!!A::type_scheme list. $ id_subst A = A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "id_subst_A";
@@ -710,18 +710,18 @@
Addsimps[o_id_subst];
Goal "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "subst_comp_te";
Goal "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "subst_comp_type_scheme";
Goalw [app_subst_list]
"$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
(* case [] *)
by (Simp_tac 1);
(* case x#xl *)
@@ -740,7 +740,7 @@
qed "subst_id_on_type_scheme_list";
Goal "!n. n < length A --> ($ S A)!n = $S (A!n)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
by (rename_tac "n1" 1);
--- a/src/HOL/MiniML/Type.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Type.thy Fri Jul 24 13:19:38 1998 +0200
@@ -25,7 +25,7 @@
consts
mk_scheme :: typ => type_scheme
-primrec mk_scheme typ
+primrec
"mk_scheme (TVar n) = (FVar n)"
"mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"
@@ -41,16 +41,16 @@
consts
free_tv :: ['a::type_struct] => nat set
-primrec free_tv typ
+primrec
free_tv_TVar "free_tv (TVar m) = {m}"
free_tv_Fun "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
-primrec free_tv type_scheme
+primrec
"free_tv (FVar m) = {m}"
"free_tv (BVar m) = {}"
"free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
-primrec free_tv list
+primrec
"free_tv [] = {}"
"free_tv (x#l) = (free_tv x) Un (free_tv l)"
@@ -59,12 +59,12 @@
consts
free_tv_ML :: ['a::type_struct] => nat list
-primrec free_tv_ML type_scheme
+primrec
"free_tv_ML (FVar m) = [m]"
"free_tv_ML (BVar m) = []"
"free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
-primrec free_tv_ML list
+primrec
"free_tv_ML [] = []"
"free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
@@ -82,12 +82,12 @@
consts
bound_tv :: ['a::type_struct] => nat set
-primrec bound_tv type_scheme
+primrec
"bound_tv (FVar m) = {}"
"bound_tv (BVar m) = {m}"
"bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
-primrec bound_tv list
+primrec
"bound_tv [] = {}"
"bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
@@ -97,7 +97,7 @@
consts
min_new_bound_tv :: 'a::type_struct => nat
-primrec min_new_bound_tv type_scheme
+primrec
"min_new_bound_tv (FVar n) = 0"
"min_new_bound_tv (BVar n) = Suc n"
"min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
@@ -118,11 +118,11 @@
consts
app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
-primrec app_subst typ
+primrec
app_subst_TVar "$ S (TVar n) = S n"
app_subst_Fun "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)"
-primrec app_subst type_scheme
+primrec
"$ S (FVar n) = mk_scheme (S n)"
"$ S (BVar n) = (BVar n)"
"$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
--- a/src/HOL/MiniML/W.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/W.ML Fri Jul 24 13:19:38 1998 +0200
@@ -16,7 +16,7 @@
(* the resulting type variable is always greater or equal than the given one *)
Goal
"!A n S t m. W e A n = Some (S,t,m) --> n<=m";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
(* case Var(n) *)
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
(* case Abs e *)
@@ -45,7 +45,7 @@
qed "new_tv_compatible_W";
Goal "new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
by (strip_tac 1);
@@ -74,7 +74,7 @@
Goal
"!n A S t m. new_tv n A --> W e A n = Some (S,t,m) --> \
\ new_tv m S & new_tv m t";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
(* case Var n *)
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
by (strip_tac 1);
@@ -156,7 +156,7 @@
qed_spec_mp "new_tv_W";
Goal "(v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (strip_tac 1);
@@ -170,7 +170,7 @@
Goal
"!n A S t m v. W e A n = Some (S,t,m) --> \
\ (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
(* case Var n *)
by (simp_tac (simpset() addsimps
[free_tv_subst] addsplits [split_option_bind]) 1);
@@ -265,7 +265,7 @@
(* correctness of W with respect to has_type *)
Goal
"!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
(* case Var n *)
by (Asm_full_simp_tac 1);
by (strip_tac 1);
@@ -388,7 +388,7 @@
"!S' A t' n. $S' A |- e :: t' --> new_tv n A --> \
\ (? S t. (? m. W e A n = Some (S,t,m)) & \
\ (? R. $S' A = $R ($S A) & t' = $R t))";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
(* case Var n *)
by (strip_tac 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
--- a/src/HOL/MiniML/W.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/W.thy Fri Jul 24 13:19:38 1998 +0200
@@ -17,7 +17,7 @@
consts
W :: [expr, ctxt, nat] => result_W
-primrec W expr
+primrec
"W (Var i) A n =
(if i < length A then Some( id_subst,
bound_typ_inst (%b. TVar(b+n)) (A!i),
--- a/src/HOL/Quot/NPAIR.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Quot/NPAIR.thy Fri Jul 24 13:19:38 1998 +0200
@@ -6,11 +6,9 @@
Example: define a PER on pairs of natural numbers (with embedding)
*)
-NPAIR = PER + Arith + (* representation for rational numbers *)
+NPAIR = PER + Datatype + (* representation for rational numbers *)
-types np = "(nat * nat)" (* is needed for datatype *)
-
-datatype NP = abs_NP np
+datatype NP = abs_NP "(nat * nat)"
consts rep_NP :: "NP => nat * nat"
@@ -23,4 +21,4 @@
(* for proves of this rule see [Slo97diss] *)
rules
per_trans_NP "[| eqv (x::NP) y;eqv y z |] ==> eqv x z"
-end
\ No newline at end of file
+end
--- a/src/HOL/Real/PNat.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Real/PNat.ML Fri Jul 24 13:19:38 1998 +0200
@@ -48,11 +48,8 @@
qed "pnat_induct";
(*Perform induction on n. *)
-local fun raw_pnat_ind_tac a i =
- res_inst_tac [("n",a)] pnat_induct i THEN rename_last_tac a [""] (i+1)
-in
-val pnat_ind_tac = Datatype.occs_in_prems raw_pnat_ind_tac
-end;
+fun pnat_ind_tac a i =
+ res_inst_tac [("n",a)] pnat_induct i THEN rename_last_tac a [""] (i+1);
val prems = goal thy
"[| !!x. P x 1p; \
--- a/src/HOL/Real/Real.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Real/Real.ML Fri Jul 24 13:19:38 1998 +0200
@@ -1267,7 +1267,7 @@
Goal "1r <= %%#n";
by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1);
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
by (auto_tac (claset(),simpset ()
addsimps [real_nat_Suc,real_le_refl,real_nat_one]));
by (res_inst_tac [("t","1r")] (real_add_zero_left RS subst) 1);
--- a/src/HOL/Subst/Subst.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Subst/Subst.thy Fri Jul 24 13:19:38 1998 +0200
@@ -18,7 +18,7 @@
srange :: "('a*('a uterm)) list => 'a set"
-primrec "op <|" uterm
+primrec
subst_Var "(Var v <| s) = assoc v (Var v) s"
subst_Const "(Const c <| s) = Const c"
subst_Comb "(Comb M N <| s) = Comb (M <| s) (N <| s)"
--- a/src/HOL/Subst/UTerm.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Subst/UTerm.thy Fri Jul 24 13:19:38 1998 +0200
@@ -7,7 +7,7 @@
Binary trees with leaves that are constants or variables.
*)
-UTerm = Finite +
+UTerm = Finite + Datatype +
datatype 'a uterm = Var ('a)
| Const ('a)
@@ -19,20 +19,20 @@
uterm_size :: 'a uterm => nat
-primrec vars_of uterm
-vars_of_Var "vars_of (Var v) = {v}"
-vars_of_Const "vars_of (Const c) = {}"
-vars_of_Comb "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
+primrec
+ vars_of_Var "vars_of (Var v) = {v}"
+ vars_of_Const "vars_of (Const c) = {}"
+ vars_of_Comb "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
-primrec "op <:" uterm
-occs_Var "u <: (Var v) = False"
-occs_Const "u <: (Const c) = False"
-occs_Comb "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
+primrec
+ occs_Var "u <: (Var v) = False"
+ occs_Const "u <: (Const c) = False"
+ occs_Comb "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
-primrec uterm_size uterm
-uterm_size_Var "uterm_size (Var v) = 0"
-uterm_size_Const "uterm_size (Const c) = 0"
-uterm_size_Comb "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
+primrec
+ uterm_size_Var "uterm_size (Var v) = 0"
+ uterm_size_Const "uterm_size (Const c) = 0"
+ uterm_size_Comb "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
end
--- a/src/HOL/Subst/Unify.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Subst/Unify.ML Fri Jul 24 13:19:38 1998 +0200
@@ -160,7 +160,7 @@
inv_image_def, less_eq]) 1);
(** LEVEL 7 **)
(*Comb-Comb case*)
-by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
+by (asm_simp_tac (simpset() addsplits [option.split]) 1);
by (strip_tac 1);
by (rtac (trans_unifyRel RS transD) 1);
by (Blast_tac 1);
@@ -183,7 +183,7 @@
\ of None => None \
\ | Some sigma => Some (theta <> sigma)))";
by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0)
- addsplits [split_option_case]) 1);
+ addsplits [option.split]) 1);
qed "unifyCombComb";
@@ -219,7 +219,7 @@
by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
(** LEVEL 8 **)
(*Comb-Comb case*)
-by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
+by (asm_simp_tac (simpset() addsplits [option.split]) 1);
by (strip_tac 1);
by (rotate_tac ~2 1);
by (asm_full_simp_tac
@@ -244,7 +244,7 @@
by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
by (ALLGOALS
(asm_simp_tac
- (simpset() addsimps [Var_Idem] addsplits [split_option_case])));
+ (simpset() addsimps [Var_Idem] addsplits [option.split])));
(*Comb-Comb case*)
by Safe_tac;
by (REPEAT (dtac spec 1 THEN mp_tac 1));
--- a/src/HOL/TLA/Inc/Pcount.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/TLA/Inc/Pcount.thy Fri Jul 24 13:19:38 1998 +0200
@@ -11,7 +11,7 @@
and case distinction tactics.
*)
-Pcount = HOL + Arith +
+Pcount = Datatype +
datatype pcount = a | b | g
--- a/src/HOL/TLA/Memory/MIParameters.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/TLA/Memory/MIParameters.thy Fri Jul 24 13:19:38 1998 +0200
@@ -9,7 +9,7 @@
RPC-Memory example: Parameters of the memory implementation.
*)
-MIParameters = Arith +
+MIParameters = Datatype +
datatype histState = histA | histB
--- a/src/HOL/TLA/Memory/Memory.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/TLA/Memory/Memory.ML Fri Jul 24 13:19:38 1998 +0200
@@ -148,13 +148,13 @@
res_inst_tac [("s","arg(ch s p)")] sumE 1,
action_simp_tac (simpset()addsimps[Read_def,enabled_ex,base_pair])
[action_mp ReadInner_enabled,exI] [] 1,
- split_all_tac 1, rename_tac "a b" 1, Rd.induct_tac "a" 1,
+ split_all_tac 1, rename_tac "a b" 1, induct_tac "a" 1,
(* introduce a trivial subgoal to solve flex-flex constraint?! *)
subgoal_tac "b = snd(a,b)" 1,
TRYALL Simp_tac, (* solves "read" case *)
etac swap 1,
action_simp_tac (simpset()addsimps[Write_def,enabled_ex,base_pair])
[action_mp WriteInner_enabled,exI] [] 1,
- split_all_tac 1, rename_tac "a aa b" 1, Wr.induct_tac "a" 1,
+ split_all_tac 1, rename_tac "a aa b" 1, induct_tac "a" 1,
subgoal_tac "(aa = fst(snd(a,aa,b))) & (b = snd(snd(a,aa,b)))" 1,
ALLGOALS Simp_tac ]);
--- a/src/HOL/TLA/Memory/MemoryParameters.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy Fri Jul 24 13:19:38 1998 +0200
@@ -9,7 +9,7 @@
RPC-Memory example: Memory parameters
*)
-MemoryParameters = Prod + Sum + Arith + RPCMemoryParams +
+MemoryParameters = Datatype + RPCMemoryParams +
(* the memory operations. nb: data types must be defined in theories
that do not include Intensional -- otherwise the induction rule
--- a/src/HOL/W0/I.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/I.ML Fri Jul 24 13:19:38 1998 +0200
@@ -12,7 +12,7 @@
"! a m s s' t n. \
\ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \
\ ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
(* case Var n *)
by (simp_tac (simpset() addsimps [app_subst_list]
@@ -143,7 +143,7 @@
Goal "!a m s. \
\ new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
by (simp_tac (simpset() addsimps [app_subst_list]) 1);
by (Simp_tac 1);
by (strip_tac 1);
--- a/src/HOL/W0/I.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/I.thy Fri Jul 24 13:19:38 1998 +0200
@@ -11,7 +11,7 @@
consts
I :: [expr, typ list, nat, subst] => result_W
-primrec I expr
+primrec
"I (Var i) a n s = (if i < length a then Ok(s, a!i, n)
else Fail)"
"I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
--- a/src/HOL/W0/Type.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/Type.ML Fri Jul 24 13:19:38 1998 +0200
@@ -17,7 +17,7 @@
Goalw [id_subst_def]
"$ id_subst = (%t::typ. t)";
by (rtac ext 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "app_subst_id_te";
Addsimps [app_subst_id_te];
@@ -26,7 +26,7 @@
Goalw [app_subst_list]
"$ id_subst = (%ts::typ list. ts)";
by (rtac ext 1);
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
by (ALLGOALS Asm_simp_tac);
qed "app_subst_id_tel";
Addsimps [app_subst_id_tel];
@@ -69,13 +69,13 @@
(* composition of substitutions *)
Goal
"$ g ($ f t::typ) = $ (%x. $ g (f x) ) t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "subst_comp_te";
Goalw [app_subst_list]
"$ g ($ f ts::typ list) = $ (%x. $ g (f x)) ts";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
(* case [] *)
by (Simp_tac 1);
(* case x#xl *)
@@ -149,21 +149,21 @@
Goal
"new_tv n = list_all (new_tv n)";
by (rtac ext 1);
-by (list.induct_tac "x" 1);
+by (induct_tac "x" 1);
by (ALLGOALS Asm_simp_tac);
qed "new_tv_list";
(* substitution affects only variables occurring freely *)
Goal
"new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "subst_te_new_tv";
Addsimps [subst_te_new_tv];
Goal
"new_tv n (ts::typ list) --> $(%x. if x=n then t else s x) ts = $s ts";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "subst_tel_new_tv";
Addsimps [subst_tel_new_tv];
@@ -171,7 +171,7 @@
(* all greater variables are also new *)
Goal
"n<=m --> new_tv n (t::typ) --> new_tv m t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
(* case TVar n *)
by (fast_tac (HOL_cs addIs [less_le_trans] addss simpset()) 1);
(* case Fun t1 t2 *)
@@ -181,7 +181,7 @@
Goal
"n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
(* case [] *)
by (Simp_tac 1);
(* case a#al *)
@@ -209,7 +209,7 @@
Goal
"new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
qed_spec_mp "new_tv_subst_te";
Addsimps [new_tv_subst_te];
@@ -217,7 +217,7 @@
Goal
"new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
by (simp_tac (simpset() addsimps [new_tv_list]) 1);
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
qed_spec_mp "new_tv_subst_tel";
Addsimps [new_tv_subst_tel];
@@ -226,7 +226,7 @@
Goal
"new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
by (simp_tac (simpset() addsimps [new_tv_list]) 1);
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "new_tv_Suc_list";
@@ -255,7 +255,7 @@
Goal
"(t::typ) mem ts --> free_tv t <= free_tv ts";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
(* case [] *)
by (Simp_tac 1);
(* case x#xl *)
@@ -269,7 +269,7 @@
occurring in the type structure *)
Goal
"$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
(* case TVar n *)
by (fast_tac (HOL_cs addss simpset()) 1);
(* case Fun t1 t2 *)
@@ -278,7 +278,7 @@
Goal
"(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
(* case TVar n *)
by (fast_tac (HOL_cs addss simpset()) 1);
(* case Fun t1 t2 *)
@@ -286,7 +286,7 @@
qed_spec_mp "eq_free_eq_subst_te";
Goal "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
(* case [] *)
by (fast_tac (HOL_cs addss simpset()) 1);
(* case x#xl *)
@@ -294,7 +294,7 @@
qed_spec_mp "eq_subst_tel_eq_free";
Goal "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
(* case [] *)
by (fast_tac (HOL_cs addss simpset()) 1);
(* case x#xl *)
@@ -323,7 +323,7 @@
qed "free_tv_subst_var";
Goal "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
(* case TVar n *)
by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
(* case Fun t1 t2 *)
@@ -331,7 +331,7 @@
qed "free_tv_app_subst_te";
Goal "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
(* case [] *)
by (Simp_tac 1);
(* case a#al *)
--- a/src/HOL/W0/Type.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/Type.thy Fri Jul 24 13:19:38 1998 +0200
@@ -36,7 +36,7 @@
consts
app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
-primrec app_subst typ
+primrec
app_subst_TVar "$ s (TVar n) = s n"
app_subst_Fun "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)"
@@ -47,11 +47,11 @@
consts
free_tv :: ['a::type_struct] => nat set
-primrec free_tv typ
+primrec
"free_tv (TVar m) = {m}"
"free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
-primrec free_tv List.list
+primrec
"free_tv [] = {}"
"free_tv (x#l) = (free_tv x) Un (free_tv l)"
--- a/src/HOL/W0/W.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/W.ML Fri Jul 24 13:19:38 1998 +0200
@@ -11,7 +11,7 @@
(* correctness of W with respect to has_type *)
Goal "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
(* case Var n *)
by (Asm_simp_tac 1);
(* case Abs e *)
@@ -41,7 +41,7 @@
(* the resulting type variable is always greater or equal than the given one *)
Goal "!a n s t m. W e a n = Ok (s,t,m) --> n<=m";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
(* case Var(n) *)
by (fast_tac (HOL_cs addss simpset()) 1);
(* case Abs e *)
@@ -85,7 +85,7 @@
Goal
"!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) --> \
\ new_tv m s & new_tv m t";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
(* case Var n *)
by (fast_tac (HOL_cs addDs [list_all_nth] addss (simpset()
addsimps [id_subst_def,new_tv_list,new_tv_subst])) 1);
@@ -151,7 +151,7 @@
Goal "!n a s t m v. W e a n = Ok (s,t,m) --> \
\ (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
(* case Var n *)
by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list]
addss simpset()) 1);
@@ -217,7 +217,7 @@
"!s' a t' n. $s' a |- e :: t' --> new_tv n a --> \
\ (? s t. (? m. W e a n = Ok (s,t,m)) & \
\ (? r. $s' a = $r ($s a) & t' = $r t))";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
(* case Var n *)
by (strip_tac 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
--- a/src/HOL/W0/W.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/W.thy Fri Jul 24 13:19:38 1998 +0200
@@ -15,7 +15,7 @@
consts
W :: [expr, typ list, nat] => result_W
-primrec W expr
+primrec
"W (Var i) a n = (if i < length a then Ok(id_subst, a!i, n)
else Fail)"
"W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
--- a/src/HOL/ex/BT.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/BT.ML Fri Jul 24 13:19:38 1998 +0200
@@ -11,48 +11,48 @@
(** BT simplification **)
Goal "n_leaves(reflect(t)) = n_leaves(t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
qed "n_leaves_reflect";
Goal "n_nodes(reflect(t)) = n_nodes(t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
qed "n_nodes_reflect";
(*The famous relationship between the numbers of leaves and nodes*)
Goal "n_leaves(t) = Suc(n_nodes(t))";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "n_leaves_nodes";
Goal "reflect(reflect(t))=t";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "reflect_reflect_ident";
Goal "bt_map f (reflect t) = reflect (bt_map f t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "bt_map_reflect";
Goal "inorder (bt_map f t) = map f (inorder t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "inorder_bt_map";
Goal "preorder (reflect t) = rev (postorder t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "preorder_reflect";
Goal "inorder (reflect t) = rev (inorder t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "inorder_reflect";
Goal "postorder (reflect t) = rev (preorder t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
qed "postorder_reflect";
--- a/src/HOL/ex/BT.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/BT.thy Fri Jul 24 13:19:38 1998 +0200
@@ -19,31 +19,31 @@
inorder :: 'a bt => 'a list
postorder :: 'a bt => 'a list
-primrec n_nodes bt
+primrec
"n_nodes (Lf) = 0"
"n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
-primrec n_leaves bt
+primrec
"n_leaves (Lf) = Suc 0"
"n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
-primrec reflect bt
+primrec
"reflect (Lf) = Lf"
"reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
-primrec bt_map bt
+primrec
"bt_map f Lf = Lf"
"bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
-primrec preorder bt
+primrec
"preorder (Lf) = []"
"preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
-primrec inorder bt
+primrec
"inorder (Lf) = []"
"inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
-primrec postorder bt
+primrec
"postorder (Lf) = []"
"postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
--- a/src/HOL/ex/InSort.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/InSort.ML Fri Jul 24 13:19:38 1998 +0200
@@ -7,13 +7,13 @@
*)
Goal "!y. mset(ins f x xs) y = mset (x#xs) y";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "mset_ins";
Addsimps [mset_ins];
Goal "!x. mset(insort f xs) x = mset xs x";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "insort_permutes";
@@ -25,7 +25,7 @@
val prems = goalw InSort.thy [total_def,transf_def]
"[| total(f); transf(f) |] ==> sorted f (ins f x xs) = sorted f xs";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
by (cut_facts_tac prems 1);
by (Fast_tac 1);
@@ -33,6 +33,6 @@
Addsimps [sorted_ins];
Goal "[| total(f); transf(f) |] ==> sorted f (insort f xs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "sorted_insort";
--- a/src/HOL/ex/InSort.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/InSort.thy Fri Jul 24 13:19:38 1998 +0200
@@ -12,10 +12,10 @@
ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list
insort :: [['a,'a]=>bool, 'a list] => 'a list
-primrec ins List.list
+primrec
"ins f x [] = [x]"
"ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))"
-primrec insort List.list
+primrec
"insort f [] = []"
"insort f (x#xs) = ins f x (insort f xs)"
end
--- a/src/HOL/ex/NatSum.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/NatSum.thy Fri Jul 24 13:19:38 1998 +0200
@@ -8,7 +8,7 @@
NatSum = Arith +
consts sum :: [nat=>nat, nat] => nat
-primrec "sum" nat
+primrec
"sum f 0 = 0"
"sum f (Suc n) = f(n) + sum f n"
--- a/src/HOL/ex/Primes.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/Primes.thy Fri Jul 24 13:19:38 1998 +0200
@@ -11,7 +11,7 @@
Isabelle prove those conditions.
*)
-Primes = Divides + WF_Rel +
+Primes = Divides + Recdef + Datatype +
consts
is_gcd :: [nat,nat,nat]=>bool (*gcd as a relation*)
gcd :: "nat*nat=>nat" (*Euclid's algorithm *)
--- a/src/HOL/ex/Primrec.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/Primrec.thy Fri Jul 24 13:19:38 1998 +0200
@@ -25,12 +25,12 @@
"ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"
consts list_add :: nat list => nat
-primrec list_add list
+primrec
"list_add [] = 0"
"list_add (m#ms) = m + list_add ms"
consts zeroHd :: nat list => nat
-primrec zeroHd list
+primrec
"zeroHd [] = 0"
"zeroHd (m#ms) = m"
--- a/src/HOL/ex/Qsort.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/Qsort.ML Fri Jul 24 13:19:38 1998 +0200
@@ -36,7 +36,7 @@
goal List.thy
"(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed"Ball_set_filter";
Addsimps [Ball_set_filter];
@@ -44,7 +44,7 @@
Goal
"sorted le (xs@ys) = (sorted le xs & sorted le ys & \
\ (!x:set xs. !y:set ys. le x y))";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "sorted_append";
Addsimps [sorted_append];
--- a/src/HOL/ex/Sorting.ML Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/Sorting.ML Fri Jul 24 13:19:38 1998 +0200
@@ -7,20 +7,20 @@
*)
Goal "!x. mset (xs@ys) x = mset xs x + mset ys x";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "mset_append";
Goal "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
\ mset xs x";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "mset_compl_add";
Addsimps [mset_append, mset_compl_add];
Goal "set xs = {x. mset xs x ~= 0}";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
by (Fast_tac 1);
qed "set_via_mset";
@@ -29,8 +29,8 @@
val prems = goalw Sorting.thy [transf_def]
"transf(le) ==> sorted1 le xs = sorted le xs";
-by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [split_list_case])));
+by (induct_tac "xs" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsplits [list.split])));
by (cut_facts_tac prems 1);
by (Fast_tac 1);
qed "sorted1_is_sorted";
--- a/src/HOL/ex/Sorting.thy Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/Sorting.thy Fri Jul 24 13:19:38 1998 +0200
@@ -14,16 +14,16 @@
total :: (['a,'a] => bool) => bool
transf :: (['a,'a] => bool) => bool
-primrec sorted1 list
+primrec
"sorted1 le [] = True"
"sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
sorted1 le xs)"
-primrec sorted list
+primrec
"sorted le [] = True"
"sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
-primrec mset list
+primrec
"mset [] y = 0"
"mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"