--- a/NEWS Thu Jan 07 11:08:29 1999 +0100
+++ b/NEWS Thu Jan 07 18:30:55 1999 +0100
@@ -61,10 +61,10 @@
*** ZF ***
* new primrec section allows primitive recursive functions to be given
- directly, as in HOL;
+ directly (as in HOL) over datatypes and the natural numbers;
* new tactics induct_tac and exhaust_tac for induction (or case analysis)
- on a datatype;
+ over datatypes and the natural numbers;
* the datatype declaration of type T now defines the recursor T_rec;
--- a/src/ZF/AC/AC10_AC15.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/AC10_AC15.ML Thu Jan 07 18:30:55 1999 +0100
@@ -197,8 +197,8 @@
(* AC13(m) ==> AC13(n) for m <= n *)
(* ********************************************************************** *)
-Goalw AC_defs "[| m:nat; n:nat; m le n; AC13(m) |] ==> AC13(n)";
-by (dtac nat_le_imp_lepoll 1 THEN REPEAT (assume_tac 1));
+Goalw AC_defs "[| m le n; AC13(m) |] ==> AC13(n)";
+by (dtac le_imp_lepoll 1);
by (fast_tac (claset() addSEs [lepoll_trans]) 1);
qed "AC13_mono";
--- a/src/ZF/AC/AC16_WO4.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/AC16_WO4.ML Thu Jan 07 18:30:55 1999 +0100
@@ -5,8 +5,6 @@
The proof of AC16(n, k) ==> WO4(n-k)
*)
-open AC16_WO4;
-
(* ********************************************************************** *)
(* The case of finite set *)
(* ********************************************************************** *)
@@ -150,7 +148,7 @@
Goal "[| k:nat; m:nat |] ==> \
\ ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m";
-by (eres_inst_tac [("n","k")] nat_induct 1);
+by (induct_tac "k" 1);
by (simp_tac (simpset() addsimps [add_0]) 1);
by (fast_tac (claset() addIs [eqpoll_imp_lepoll RS
(Diff_subset RS subset_imp_lepoll RS lepoll_trans)]) 1);
@@ -180,7 +178,7 @@
Goal "[| k:nat; m:nat |] ==> \
\ ALL A B. A eqpoll k #+ m & k eqpoll B & B<=A --> A-B eqpoll m";
-by (eres_inst_tac [("n","k")] nat_induct 1);
+by (induct_tac "k" 1);
by (fast_tac (claset() addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0]
addss (simpset() addsimps [add_0])) 1);
by (REPEAT (resolve_tac [allI,impI] 1));
@@ -419,9 +417,9 @@
qed "well_ord_subsets_eqpoll_n";
Goal "n:nat ==> EX R. well_ord({z:Pow(y). z lepoll n}, R)";
-by (etac nat_induct 1);
-by (fast_tac (claset() addSIs [well_ord_unit]
- addss (simpset() addsimps [subsets_lepoll_0_eq_unit])) 1);
+by (induct_tac "n" 1);
+by (force_tac (claset() addSIs [well_ord_unit],
+ simpset() addsimps [subsets_lepoll_0_eq_unit]) 1);
by (etac exE 1);
by (resolve_tac [well_ord_subsets_eqpoll_n RS exE] 1 THEN assume_tac 1);
by (asm_simp_tac (simpset() addsimps [subsets_lepoll_succ]) 1);
--- a/src/ZF/AC/AC16_lemmas.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/AC16_lemmas.ML Thu Jan 07 18:30:55 1999 +0100
@@ -5,8 +5,6 @@
Lemmas used in the proofs concerning AC16
*)
-open AC16_lemmas;
-
Goal "a~:A ==> cons(a,A)-{a}=A";
by (Fast_tac 1);
qed "cons_Diff_eq";
@@ -126,7 +124,7 @@
Goal "n:nat ==> \
\ ALL z. (ALL y:z. Ord(y)) & z eqpoll n & z~=0 --> Union(z) : z";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1);
by (REPEAT (resolve_tac [allI, impI] 1));
by (etac natE 1);
@@ -189,7 +187,7 @@
Goal "[| InfCard(X); n:nat |] \
\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
by (rtac subsets_eqpoll_1_eqpoll 1);
by (rtac eqpollI 1);
by (resolve_tac [subsets_lepoll_lemma1 RS lepoll_trans] 1
--- a/src/ZF/AC/AC_Equiv.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/AC_Equiv.ML Thu Jan 07 18:30:55 1999 +0100
@@ -16,23 +16,6 @@
val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def];
-(* ******************************************** *)
-
-(* Theorems analogous to ones presented in "ZF/Ordinal.ML" *)
-
-(* lemma for nat_le_imp_lepoll *)
-val [prem] = goalw Cardinal.thy [lepoll_def]
- "m:nat ==> ALL n: nat. m le n --> m lepoll n";
-by (nat_ind_tac "m" [prem] 1);
-by (fast_tac (claset() addSIs [le_imp_subset RS id_subset_inj]) 1);
-by (rtac ballI 1);
-by (eres_inst_tac [("n","n")] natE 1);
-by (asm_simp_tac (simpset() addsimps [inj_def, succI1 RS Pi_empty2]) 1);
-by (fast_tac (claset() addSIs [le_imp_subset RS id_subset_inj]) 1);
-qed "nat_le_imp_lepoll_lemma";
-
-(* used in : AC10-AC15.ML WO1-WO6.ML WO6WO1.ML*)
-val nat_le_imp_lepoll = nat_le_imp_lepoll_lemma RS bspec RS mp |> standard;
(* ********************************************************************** *)
(* lemmas concerning FOL and pure ZF theory *)
--- a/src/ZF/AC/Cardinal_aux.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/Cardinal_aux.ML Thu Jan 07 18:30:55 1999 +0100
@@ -5,8 +5,6 @@
Auxiliary lemmas concerning cardinalities
*)
-open Cardinal_aux;
-
(* ********************************************************************** *)
(* Lemmas involving ordinals and cardinalities used in the proofs *)
(* concerning AC16 and DC *)
@@ -113,7 +111,7 @@
Goal "[| well_ord(T, R); ~Finite(a); Ord(a); n:nat |] ==> \
\ ALL f. (ALL b:a. f`b lepoll n & f`b <= T) --> (UN b:a. f`b) lepoll a";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
by (rtac allI 1);
by (rtac impI 1);
by (res_inst_tac [("b","UN b:a. f`b")] subst 1);
--- a/src/ZF/AC/DC.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/DC.ML Thu Jan 07 18:30:55 1999 +0100
@@ -5,8 +5,6 @@
The proofs concerning the Axiom of Dependent Choice
*)
-open DC;
-
(* ********************************************************************** *)
(* DC ==> DC(omega) *)
(* *)
@@ -80,7 +78,7 @@
Goal "[| ALL n:nat. <f`n, f`succ(n)> : RR; f: nat -> XX; n:nat |] \
\ ==> EX k:nat. f`succ(n) : k -> X & n:k \
\ & <f`succ(n)``n, f`succ(n)`n> : R";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
by (dresolve_tac [nat_1I RSN (2, apply_type)] 1);
by (dresolve_tac [nat_0I RSN (2, bspec)] 1);
by (asm_full_simp_tac (simpset() addsimps [XX_def]) 1);
@@ -112,7 +110,7 @@
\ ==> {f`succ(x)`x. x:m} = {f`succ(m)`x. x:m}";
by (subgoal_tac "ALL x:m. f`succ(m)`x = f`succ(x)`x" 1);
by (Asm_full_simp_tac 1);
-by (etac nat_induct 1);
+by (induct_tac "m" 1);
by (Fast_tac 1);
by (rtac ballI 1);
by (etac succE 1);
@@ -207,7 +205,7 @@
qed "lesspoll_nat_is_Finite";
Goal "n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
by (rtac allI 1);
by (fast_tac (claset() addSIs [Fin.emptyI]
addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1);
--- a/src/ZF/AC/WO1_WO6.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/WO1_WO6.ML Thu Jan 07 18:30:55 1999 +0100
@@ -61,10 +61,9 @@
(* ********************************************************************** *)
-Goalw WO_defs "[| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)";
-by (rtac allI 1);
-by (dtac spec 1);
-by (blast_tac (claset() addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1);
+Goalw WO_defs "[| m le n; WO4(m) |] ==> WO4(n)";
+by (blast_tac (claset() addSDs [spec]
+ addIs [le_imp_lepoll RSN (2, lepoll_trans)]) 1);
qed "WO4_mono";
(* ********************************************************************** *)
--- a/src/ZF/AC/WO2_AC16.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/WO2_AC16.ML Thu Jan 07 18:30:55 1999 +0100
@@ -137,7 +137,7 @@
Goal "n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x)) \
\ --> Finite(Union(X))";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]
addSIs [nat_0I RS nat_into_Finite] addss (simpset())) 1);
by (REPEAT (resolve_tac [allI, impI] 1));
@@ -396,7 +396,7 @@
Goal "m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
-by (etac nat_induct 1);
+by (induct_tac "m" 1);
by (fast_tac (claset() addSDs [lepoll_0_is_0]) 1);
by (REPEAT (resolve_tac [allI, impI] 1));
by (REPEAT (etac conjE 1));
--- a/src/ZF/AC/WO6_WO1.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/AC/WO6_WO1.ML Thu Jan 07 18:30:55 1999 +0100
@@ -411,8 +411,7 @@
val [prem1, prem2] = goal thy
"[| n:nat; !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
\ ==> n~=0 --> P(n) --> P(1)";
-by (res_inst_tac [("n","n")] nat_induct 1);
-by (rtac prem1 1);
+by (rtac (prem1 RS nat_induct) 1);
by (Blast_tac 1);
by (excluded_middle_tac "x=0" 1);
by (Blast_tac 2);
--- a/src/ZF/Arith.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Arith.ML Thu Jan 07 18:30:55 1999 +0100
@@ -6,50 +6,20 @@
Arithmetic operators and their definitions
Proofs about elementary arithmetic: addition, multiplication, etc.
-
-Could prove def_rec_0, def_rec_succ...
*)
-open Arith;
-
(*"Difference" is subtraction of natural numbers.
There are no negative numbers; we have
m #- n = 0 iff m<=n and m #- n = succ(k) iff m>n.
Also, rec(m, 0, %z w.z) is pred(m).
*)
-(** rec -- better than nat_rec; the succ case has no type requirement! **)
-
-val rec_trans = rec_def RS def_transrec RS trans;
-
-Goal "rec(0,a,b) = a";
-by (rtac rec_trans 1);
-by (rtac nat_case_0 1);
-qed "rec_0";
-
-Goal "rec(succ(m),a,b) = b(m, rec(m,a,b))";
-by (rtac rec_trans 1);
-by (Simp_tac 1);
-qed "rec_succ";
-
-Addsimps [rec_0, rec_succ];
-
-val major::prems = Goal
- "[| n: nat; \
-\ a: C(0); \
-\ !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) \
-\ |] ==> rec(n,a,b) : C(n)";
-by (rtac (major RS nat_induct) 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps prems)));
-qed "rec_type";
-
Addsimps [rec_type, nat_0_le, nat_le_refl];
val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
Goal "[| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
by (etac rev_mp 1);
-by (etac nat_induct 1);
+by (induct_tac "k" 1);
by (Simp_tac 1);
by (Blast_tac 1);
val lemma = result();
@@ -60,63 +30,46 @@
(** Addition **)
-qed_goalw "add_type" Arith.thy [add_def]
- "[| m:nat; n:nat |] ==> m #+ n : nat"
- (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
-
-qed_goalw "add_0" Arith.thy [add_def]
- "0 #+ n = n"
- (fn _ => [ (rtac rec_0 1) ]);
-
-qed_goalw "add_succ" Arith.thy [add_def]
- "succ(m) #+ n = succ(m #+ n)"
- (fn _=> [ (rtac rec_succ 1) ]);
-
-Addsimps [add_0, add_succ];
+Goal "[| m:nat; n:nat |] ==> m #+ n : nat";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "add_type";
+Addsimps [add_type];
(** Multiplication **)
-qed_goalw "mult_type" Arith.thy [mult_def]
- "[| m:nat; n:nat |] ==> m #* n : nat"
- (fn prems=>
- [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);
+Goal "[| m:nat; n:nat |] ==> m #* n : nat";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "mult_type";
+Addsimps [mult_type];
-qed_goalw "mult_0" Arith.thy [mult_def]
- "0 #* n = 0"
- (fn _ => [ (rtac rec_0 1) ]);
-
-qed_goalw "mult_succ" Arith.thy [mult_def]
- "succ(m) #* n = n #+ (m #* n)"
- (fn _ => [ (rtac rec_succ 1) ]);
-
-Addsimps [mult_0, mult_succ];
(** Difference **)
-qed_goalw "diff_type" Arith.thy [diff_def]
- "[| m:nat; n:nat |] ==> m #- n : nat"
- (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
+Goal "[| m:nat; n:nat |] ==> m #- n : nat";
+by (induct_tac "n" 1);
+by Auto_tac;
+by (fast_tac (claset() addIs [nat_case_type]) 1);
+qed "diff_type";
+Addsimps [diff_type];
-qed_goalw "diff_0" Arith.thy [diff_def]
- "m #- 0 = m"
- (fn _ => [ (rtac rec_0 1) ]);
+Goal "n:nat ==> 0 #- n = 0";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "diff_0_eq_0";
-qed_goalw "diff_0_eq_0" Arith.thy [diff_def]
- "n:nat ==> 0 #- n = 0"
- (fn [prem]=>
- [ (rtac (prem RS nat_induct) 1),
- (ALLGOALS (Asm_simp_tac)) ]);
+(*Must simplify BEFORE the induction: else we get a critical pair*)
+Goal "[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n";
+by (Asm_simp_tac 1);
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "diff_succ_succ";
-(*Must simplify BEFORE the induction!! (Else we get a critical pair)
- succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *)
-qed_goalw "diff_succ_succ" Arith.thy [diff_def]
- "[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n"
- (fn prems=>
- [ (asm_simp_tac (simpset() addsimps prems) 1),
- (nat_ind_tac "n" prems 1),
- (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
+Addsimps [diff_0_eq_0, diff_succ_succ];
-Addsimps [diff_0, diff_0_eq_0, diff_succ_succ];
+(*This defining property is no longer wanted*)
+Delsimps [diff_SUCC];
val prems = goal Arith.thy
"[| m:nat; n:nat |] ==> m #- n le m";
@@ -129,72 +82,64 @@
(*** Simplification over add, mult, diff ***)
val arith_typechecks = [add_type, mult_type, diff_type];
-Addsimps arith_typechecks;
(*** Addition ***)
(*Associative law for addition*)
-qed_goal "add_assoc" Arith.thy
- "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
+Goal "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "add_assoc";
(*The following two lemmas are used for add_commute and sometimes
elsewhere, since they are safe for rewriting.*)
-qed_goal "add_0_right" Arith.thy
- "m:nat ==> m #+ 0 = m"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
+Goal "m:nat ==> m #+ 0 = m";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "add_0_right";
-qed_goal "add_succ_right" Arith.thy
- "m:nat ==> m #+ succ(n) = succ(m #+ n)"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
+Goal "m:nat ==> m #+ succ(n) = succ(m #+ n)";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "add_succ_right";
Addsimps [add_0_right, add_succ_right];
(*Commutative law for addition*)
-qed_goal "add_commute" Arith.thy
- "!!m n. [| m:nat; n:nat |] ==> m #+ n = n #+ m"
- (fn _ =>
- [ (nat_ind_tac "n" [] 1),
- (ALLGOALS Asm_simp_tac) ]);
+Goal "[| m:nat; n:nat |] ==> m #+ n = n #+ m";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "add_commute";
(*for a/c rewriting*)
-qed_goal "add_left_commute" Arith.thy
- "!!m n k. [| m:nat; n:nat |] ==> m#+(n#+k)=n#+(m#+k)"
- (fn _ => [asm_simp_tac(simpset() addsimps [add_assoc RS sym, add_commute]) 1]);
+Goal "[| m:nat; n:nat |] ==> m#+(n#+k)=n#+(m#+k)";
+by (asm_simp_tac (simpset() addsimps [add_assoc RS sym, add_commute]) 1);
+qed "add_left_commute";
(*Addition is an AC-operator*)
val add_ac = [add_assoc, add_commute, add_left_commute];
(*Cancellation law on the left*)
-val [eqn,knat] = goal Arith.thy
- "[| k #+ m = k #+ n; k:nat |] ==> m=n";
-by (rtac (eqn RS rev_mp) 1);
-by (nat_ind_tac "k" [knat] 1);
-by (ALLGOALS (Simp_tac));
+Goal "[| k #+ m = k #+ n; k:nat |] ==> m=n";
+by (etac rev_mp 1);
+by (induct_tac "k" 1);
+by Auto_tac;
qed "add_left_cancel";
(*** Multiplication ***)
(*right annihilation in product*)
-qed_goal "mult_0_right" Arith.thy
- "!!m. m:nat ==> m #* 0 = 0"
- (fn _=>
- [ (nat_ind_tac "m" [] 1),
- (ALLGOALS (Asm_simp_tac)) ]);
+Goal "m:nat ==> m #* 0 = 0";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "mult_0_right";
(*right successor law for multiplication*)
-qed_goal "mult_succ_right" Arith.thy
- "!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
- (fn _ =>
- [ (nat_ind_tac "m" [] 1),
- (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac))) ]);
+Goal "[| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)";
+by (induct_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
+qed "mult_succ_right";
Addsimps [mult_0_right, mult_succ_right];
@@ -206,53 +151,49 @@
by (Asm_simp_tac 1);
qed "mult_1_right";
+Addsimps [mult_1, mult_1_right];
+
(*Commutative law for multiplication*)
-qed_goal "mult_commute" Arith.thy
- "!!m n. [| m:nat; n:nat |] ==> m #* n = n #* m"
- (fn _=>
- [ (nat_ind_tac "m" [] 1),
- (ALLGOALS Asm_simp_tac) ]);
+Goal "[| m:nat; n:nat |] ==> m #* n = n #* m";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "mult_commute";
(*addition distributes over multiplication*)
-qed_goal "add_mult_distrib" Arith.thy
- "!!m n. [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
- (fn _=>
- [ (etac nat_induct 1),
- (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym]))) ]);
+Goal "[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)";
+by (induct_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
+qed "add_mult_distrib";
(*Distributive law on the left; requires an extra typing premise*)
-qed_goal "add_mult_distrib_left" Arith.thy
- "!!m. [| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
- (fn prems=>
- [ (nat_ind_tac "m" [] 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (simpset() addsimps add_ac) 1) ]);
+Goal "[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)";
+by (induct_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
+qed "add_mult_distrib_left";
(*Associative law for multiplication*)
-qed_goal "mult_assoc" Arith.thy
- "!!m n k. [| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
- (fn _=>
- [ (etac nat_induct 1),
- (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))) ]);
+Goal "[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)";
+by (induct_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
+qed "mult_assoc";
(*for a/c rewriting*)
-qed_goal "mult_left_commute" Arith.thy
- "!!m n k. [| m:nat; n:nat; k:nat |] ==> m #* (n #* k) = n #* (m #* k)"
- (fn _ => [rtac (mult_commute RS trans) 1,
- rtac (mult_assoc RS trans) 3,
- rtac (mult_commute RS subst_context) 6,
- REPEAT (ares_tac [mult_type] 1)]);
+Goal "[| m:nat; n:nat; k:nat |] ==> m #* (n #* k) = n #* (m #* k)";
+by (rtac (mult_commute RS trans) 1);
+by (rtac (mult_assoc RS trans) 3);
+by (rtac (mult_commute RS subst_context) 6);
+by (REPEAT (ares_tac [mult_type] 1));
+qed "mult_left_commute";
val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
(*** Difference ***)
-qed_goal "diff_self_eq_0" Arith.thy
- "m:nat ==> m #- m = 0"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
+Goal "m:nat ==> m #- m = 0";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "diff_self_eq_0";
(*Addition is the inverse of subtraction*)
Goal "[| n le m; m:nat |] ==> n #+ (m#-n) = m";
@@ -287,10 +228,9 @@
(** Subtraction is the inverse of addition. **)
-val [mnat,nnat] = goal Arith.thy
- "[| m:nat; n:nat |] ==> (n#+m) #- n = m";
-by (rtac (nnat RS nat_induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [mnat])));
+Goal "[| m:nat; n:nat |] ==> (n#+m) #- n = m";
+by (induct_tac "n" 1);
+by Auto_tac;
qed "diff_add_inverse";
Goal "[| m:nat; n:nat |] ==> (m#+n) #- n = m";
@@ -299,7 +239,7 @@
qed "diff_add_inverse2";
Goal "[| k:nat; m: nat; n: nat |] ==> (k#+m) #- (k#+n) = m #- n";
-by (nat_ind_tac "k" [] 1);
+by (induct_tac "k" 1);
by (ALLGOALS Asm_simp_tac);
qed "diff_cancel";
@@ -308,10 +248,9 @@
by (asm_simp_tac (simpset() addsimps [add_commute_k, diff_cancel]) 1);
qed "diff_cancel2";
-val [mnat,nnat] = goal Arith.thy
- "[| m:nat; n:nat |] ==> n #- (n#+m) = 0";
-by (rtac (nnat RS nat_induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [mnat])));
+Goal "[| m:nat; n:nat |] ==> n #- (n#+m) = 0";
+by (induct_tac "n" 1);
+by Auto_tac;
qed "diff_add_0";
(** Difference distributes over multiplication **)
@@ -334,7 +273,7 @@
by (etac rev_mp 1);
by (etac rev_mp 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self,diff_succ_succ])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self])));
qed "div_termination";
val div_rls = (*for mod and div*)
@@ -342,8 +281,8 @@
[Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
nat_into_Ord, not_lt_iff_le RS iffD1];
-val div_ss = (simpset()) addsimps [nat_into_Ord, div_termination RS ltD,
- not_lt_iff_le RS iffD2];
+val div_ss = simpset() addsimps [nat_into_Ord, div_termination RS ltD,
+ not_lt_iff_le RS iffD2];
(*Type checking depends upon termination!*)
Goalw [mod_def] "[| 0<n; m:nat; n:nat |] ==> m mod n : nat";
@@ -442,7 +381,7 @@
qed "mod2_succ_succ";
Goal "m:nat ==> (m#+m) mod 2 = 0";
-by (etac nat_induct 1);
+by (induct_tac "m" 1);
by (simp_tac (simpset() addsimps [mod_less]) 1);
by (asm_simp_tac (simpset() addsimps [mod2_succ_succ, add_succ_right]) 1);
qed "mod2_add_self";
@@ -451,7 +390,7 @@
(**** Additional theorems about "le" ****)
Goal "[| m:nat; n:nat |] ==> m le m #+ n";
-by (etac nat_induct 1);
+by (induct_tac "m" 1);
by (ALLGOALS Asm_simp_tac);
qed "add_le_self";
@@ -510,7 +449,7 @@
Goal "[| i le j; j:nat; k:nat |] ==> i#*k le j#*k";
by (forward_tac [lt_nat_in_nat] 1);
-by (nat_ind_tac "k" [] 2);
+by (induct_tac "k" 2);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
qed "mult_le_mono1";
@@ -529,7 +468,7 @@
by (etac zero_lt_natE 1);
by (forward_tac [lt_nat_in_nat] 2);
by (ALLGOALS Asm_simp_tac);
-by (nat_ind_tac "x" [] 1);
+by (induct_tac "x" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
qed "mult_lt_mono2";
@@ -571,38 +510,28 @@
div_termination RS ltD]) 1);
qed "mult_mod_distrib";
-(** Lemma for gcd **)
-
-val mono_lemma = (nat_into_Ord RS Ord_0_lt) RSN (2,mult_lt_mono2);
-
+(*Lemma for gcd*)
Goal "[| m = m#*n; m: nat; n: nat |] ==> n=1 | m=0";
by (rtac disjCI 1);
by (dtac sym 1);
by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
-by (fast_tac (claset() addss (simpset())) 1);
-by (fast_tac (le_cs addDs [mono_lemma]
- addss (simpset() addsimps [mult_1_right])) 1);
+by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 2);
+by Auto_tac;
qed "mult_eq_self_implies_10";
-
(*Thanks to Sten Agerholm*)
Goal "[|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
by (etac rev_mp 1);
-by (eres_inst_tac [("n","n")] nat_induct 1);
+by (induct_tac "m" 1);
by (Asm_simp_tac 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt,nat_into_Ord]) 1);
-by (etac lt_asym 1);
-by (assume_tac 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [le_iff, nat_into_Ord]) 1);
-by (Blast_tac 1);
qed "add_le_elim1";
Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
be rev_mp 1;
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
by (blast_tac (claset() addSEs [leE]
addSIs [add_0_right RS sym, add_succ_right RS sym]) 1);
--- a/src/ZF/Arith.thy Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Arith.thy Thu Jan 07 18:30:55 1999 +0100
@@ -7,20 +7,37 @@
*)
Arith = Epsilon +
+
+setup setup_datatypes
+
+(*The natural numbers as a datatype*)
+rep_datatype
+ elim natE
+ induct nat_induct
+ case_eqns nat_case_0, nat_case_succ
+ recursor_eqns recursor_0, recursor_succ
+
+
consts
- rec :: [i, i, [i,i]=>i]=>i
"#*" :: [i,i]=>i (infixl 70)
div :: [i,i]=>i (infixl 70)
mod :: [i,i]=>i (infixl 70)
"#+" :: [i,i]=>i (infixl 65)
"#-" :: [i,i]=>i (infixl 65)
-defs
- rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
+primrec
+ add_0 "0 #+ n = n"
+ add_succ "succ(m) #+ n = succ(m #+ n)"
+
+primrec
+ diff_0 "m #- 0 = m"
+ diff_SUCC "m #- succ(n) = nat_case(0, %x. x, m #- n)"
- add_def "m#+n == rec(m, n, %u v. succ(v))"
- diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y. x))"
- mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
- mod_def "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))"
- div_def "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-n))))"
+primrec
+ mult_0 "0 #* n = 0"
+ mult_succ "succ(m) #* n = n #+ (m #* n)"
+
+defs
+ mod_def "m mod n == transrec(m, %j f. if j<n then j else f`(j#-n))"
+ div_def "m div n == transrec(m, %j f. if j<n then 0 else succ(f`(j#-n)))"
end
--- a/src/ZF/CardinalArith.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/CardinalArith.ML Thu Jan 07 18:30:55 1999 +0100
@@ -59,6 +59,7 @@
by (asm_simp_tac (simpset() addsimps [sum_0_eqpoll RS cardinal_cong,
Card_cardinal_eq]) 1);
qed "cadd_0";
+Addsimps [cadd_0];
(** Addition by another cardinal **)
@@ -120,10 +121,8 @@
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1));
qed "cadd_succ_lemma";
-val [mnat,nnat] = goal CardinalArith.thy
- "[| m: nat; n: nat |] ==> m |+| n = m#+n";
-by (cut_facts_tac [nnat] 1);
-by (nat_ind_tac "m" [mnat] 1);
+Goal "[| m: nat; n: nat |] ==> m |+| n = m#+n";
+by (induct_tac "m" 1);
by (asm_simp_tac (simpset() addsimps [nat_into_Card RS cadd_0]) 1);
by (asm_simp_tac (simpset() addsimps [nat_into_Ord, cadd_succ_lemma,
nat_into_Card RS Card_cardinal_eq]) 1);
@@ -198,6 +197,7 @@
by (asm_simp_tac (simpset() addsimps [prod_0_eqpoll RS cardinal_cong,
Card_0 RS Card_cardinal_eq]) 1);
qed "cmult_0";
+Addsimps [cmult_0];
(** 1 is the identity for multiplication **)
@@ -210,6 +210,7 @@
by (asm_simp_tac (simpset() addsimps [prod_singleton_eqpoll RS cardinal_cong,
Card_cardinal_eq]) 1);
qed "cmult_1";
+Addsimps [cmult_1];
(*** Some inequalities for multiplication ***)
@@ -285,19 +286,16 @@
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
qed "cmult_succ_lemma";
-val [mnat,nnat] = goal CardinalArith.thy
- "[| m: nat; n: nat |] ==> m |*| n = m#*n";
-by (cut_facts_tac [nnat] 1);
-by (nat_ind_tac "m" [mnat] 1);
-by (asm_simp_tac (simpset() addsimps [cmult_0]) 1);
+Goal "[| m: nat; n: nat |] ==> m |*| n = m#*n";
+by (induct_tac "m" 1);
+by (Asm_simp_tac 1);
by (asm_simp_tac (simpset() addsimps [nat_into_Ord, cmult_succ_lemma,
nat_cadd_eq_add]) 1);
qed "nat_cmult_eq_mult";
Goal "Card(n) ==> 2 |*| n = n |+| n";
by (asm_simp_tac
- (simpset() addsimps [Ord_0, Ord_succ, cmult_0, cmult_succ_lemma,
- Card_is_Ord, cadd_0,
+ (simpset() addsimps [Ord_0, Ord_succ, cmult_succ_lemma, Card_is_Ord,
read_instantiate [("j","0")] cadd_commute]) 1);
qed "cmult_2";
@@ -708,7 +706,7 @@
(*** Finite sets ***)
Goal "n: nat ==> ALL A. A eqpoll n --> A : Fin(A)";
-by (etac nat_induct 1);
+by (induct_tac "n" 1);
by (simp_tac (simpset() addsimps eqpoll_0_iff::Fin.intrs) 1);
by (Clarify_tac 1);
by (subgoal_tac "EX u. u:A" 1);
--- a/src/ZF/Datatype.thy Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Datatype.thy Thu Jan 07 18:30:55 1999 +0100
@@ -8,9 +8,4 @@
"Datatype" must be capital to avoid conflicts with ML's "datatype"
*)
-Datatype = Inductive + Univ + QUniv +
-
-setup setup_datatypes
-
-end
-
+Datatype = Inductive + Univ + QUniv
--- a/src/ZF/Epsilon.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Epsilon.ML Thu Jan 07 18:30:55 1999 +0100
@@ -287,7 +287,8 @@
by (rtac arg_subset_eclose 1);
qed "eclose_idem";
-(*Transfinite recursion for definitions based on the three cases of ordinals*)
+(** Transfinite recursion for definitions based on the
+ three cases of ordinals **)
Goal "transrec2(0,a,b) = a";
by (rtac (transrec2_def RS def_transrec RS trans) 1);
@@ -312,3 +313,40 @@
Addsimps [transrec2_0, transrec2_succ];
+
+(** recursor -- better than nat_rec; the succ case has no type requirement! **)
+
+(*NOT suitable for rewriting*)
+val lemma = recursor_def RS def_transrec RS trans;
+
+Goal "recursor(a,b,0) = a";
+by (rtac (nat_case_0 RS lemma) 1);
+qed "recursor_0";
+
+Goal "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))";
+by (rtac lemma 1);
+by (Simp_tac 1);
+qed "recursor_succ";
+
+
+(** rec: old version for compatibility **)
+
+Goalw [rec_def] "rec(0,a,b) = a";
+by (rtac recursor_0 1);
+qed "rec_0";
+
+Goalw [rec_def] "rec(succ(m),a,b) = b(m, rec(m,a,b))";
+by (rtac recursor_succ 1);
+qed "rec_succ";
+
+Addsimps [rec_0, rec_succ];
+
+val major::prems = Goal
+ "[| n: nat; \
+\ a: C(0); \
+\ !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) \
+\ |] ==> rec(n,a,b) : C(n)";
+by (rtac (major RS nat_induct) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
+qed "rec_type";
+
--- a/src/ZF/Epsilon.thy Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Epsilon.thy Thu Jan 07 18:30:55 1999 +0100
@@ -25,4 +25,10 @@
b(THE j. i=succ(j), r`(THE j. i=succ(j))),
UN j<i. r`j)))"
+ recursor :: [i, [i,i]=>i, i]=>i
+ "recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
+
+ rec :: [i, i, [i,i]=>i]=>i
+ "rec(k,a,b) == recursor(a,b,k)"
+
end
--- a/src/ZF/Finite.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Finite.ML Thu Jan 07 18:30:55 1999 +0100
@@ -10,8 +10,6 @@
prove: b: Fin(A) ==> inj(b,b)<=surj(b,b)
*)
-open Finite;
-
(*** Finite powerset operator ***)
Goalw Fin.defs "A<=B ==> Fin(A) <= Fin(B)";
@@ -104,7 +102,7 @@
(*Functions from a finite ordinal*)
Goal "n: nat ==> n->A <= Fin(nat*A)";
-by (nat_ind_tac "n" [] 1);
+by (induct_tac "n" 1);
by (simp_tac (simpset() addsimps [Pi_empty1, subset_iff, cons_iff]) 1);
by (asm_simp_tac
(simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1);
--- a/src/ZF/List.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/List.ML Thu Jan 07 18:30:55 1999 +0100
@@ -63,31 +63,27 @@
(** drop **)
-Goalw [drop_def] "drop(0, l) = l";
-by (rtac rec_0 1);
-qed "drop_0";
-
-Goalw [drop_def] "i:nat ==> drop(i, Nil) = Nil";
-by (etac nat_induct 1);
+Goal "i:nat ==> drop(i, Nil) = Nil";
+by (induct_tac "i" 1);
by (ALLGOALS Asm_simp_tac);
qed "drop_Nil";
-Goalw [drop_def]
- "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
+Goal "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
by (rtac sym 1);
-by (etac nat_induct 1);
+by (induct_tac "i" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "drop_succ_Cons";
-Addsimps [drop_0, drop_Nil, drop_succ_Cons];
+Addsimps [drop_Nil, drop_succ_Cons];
-Goalw [drop_def]
- "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
-by (etac nat_induct 1);
+Goal "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
+by (induct_tac "i" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [tl_type])));
qed "drop_type";
+Delsimps [drop_SUCC];
+
(** Type checking -- proved by induction, as usual **)
--- a/src/ZF/List.thy Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/List.thy Thu Jan 07 18:30:55 1999 +0100
@@ -33,12 +33,6 @@
length :: i=>i
hd :: i=>i
tl :: i=>i
- map :: [i=>i, i] => i
- set_of_list :: i=>i
- "@" :: [i,i]=>i (infixr 60)
- rev :: i=>i
- flat :: i=>i
- list_add :: i=>i
primrec
"length([]) = 0"
@@ -51,6 +45,12 @@
"tl([]) = []"
"tl(Cons(a,l)) = l"
+
+consts
+ map :: [i=>i, i] => i
+ set_of_list :: i=>i
+ "@" :: [i,i]=>i (infixr 60)
+
primrec
"map(f,[]) = []"
"map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
@@ -63,6 +63,12 @@
"[] @ ys = ys"
"(Cons(a,l)) @ ys = Cons(a, l @ ys)"
+
+consts
+ rev :: i=>i
+ flat :: i=>i
+ list_add :: i=>i
+
primrec
"rev([]) = []"
"rev(Cons(a,l)) = rev(l) @ [a]"
@@ -75,8 +81,11 @@
"list_add([]) = 0"
"list_add(Cons(a,l)) = a #+ list_add(l)"
-constdefs
+consts
drop :: [i,i]=>i
- "drop(i,l) == rec(i, l, %j r. tl(r))"
+
+primrec
+ drop_0 "drop(0,l) = l"
+ drop_SUCC "drop(succ(i), l) = tl (drop(i,l))"
end
--- a/src/ZF/Nat.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Nat.ML Thu Jan 07 18:30:55 1999 +0100
@@ -213,17 +213,16 @@
(** nat_rec -- used to define eclose and transrec, then obsolete;
rec, from arith.ML, has fewer typing conditions **)
-val nat_rec_trans = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans);
+val lemma = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans);
Goal "nat_rec(0,a,b) = a";
-by (rtac nat_rec_trans 1);
+by (rtac lemma 1);
by (rtac nat_case_0 1);
qed "nat_rec_0";
-val [prem] = goal Nat.thy
- "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
-by (rtac nat_rec_trans 1);
-by (simp_tac (simpset() addsimps [prem, Memrel_iff, vimage_singleton_iff]) 1);
+Goal "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
+by (rtac lemma 1);
+by (asm_simp_tac (simpset() addsimps [Memrel_iff, vimage_singleton_iff]) 1);
qed "nat_rec_succ";
(** The union of two natural numbers is a natural number -- their maximum **)
--- a/src/ZF/QUniv.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/QUniv.ML Thu Jan 07 18:30:55 1999 +0100
@@ -193,6 +193,6 @@
by (rtac (succI1 RS UN_upper) 1);
(*Limit(i) case*)
by (asm_simp_tac
- (simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl,
+ (simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib,
UN_mono, QPair_Int_Vset_subset_trans]) 1);
qed "QPair_Int_Vset_subset_UN";
--- a/src/ZF/ROOT.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/ROOT.ML Thu Jan 07 18:30:55 1999 +0100
@@ -42,11 +42,11 @@
use_thy "Fixedpt";
use "Tools/inductive_package";
use_thy "Inductive";
+use "Tools/induct_tacs";
+use "Tools/primrec_package";
use_thy "QUniv";
use "Tools/datatype_package";
-use "Tools/primrec_package";
use_thy "Datatype";
-use "Tools/induct_tacs";
use_thy "InfDatatype";
use_thy "List";
--- a/src/ZF/Resid/Substitution.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Resid/Substitution.ML Thu Jan 07 18:30:55 1999 +0100
@@ -16,7 +16,7 @@
val succ_pred = prove_goal Arith.thy
"!!i.[|j:nat; i:nat|] ==> i < j --> succ(j #- 1) = j"
- (fn prems =>[(etac nat_induct 1),
+ (fn prems =>[(induct_tac "j" 1),
(Fast_tac 1),
(Asm_simp_tac 1)]);
--- a/src/ZF/Tools/datatype_package.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Tools/datatype_package.ML Thu Jan 07 18:30:55 1999 +0100
@@ -13,59 +13,6 @@
*)
-(** Datatype information, e.g. associated theorems **)
-
-type datatype_info =
- {inductive: bool, (*true if inductive, not coinductive*)
- constructors : term list, (*the constructors, as Consts*)
- rec_rewrites : thm list, (*recursor equations*)
- case_rewrites : thm list, (*case equations*)
- induct : thm,
- mutual_induct : thm,
- exhaustion : thm};
-
-structure DatatypesArgs =
- struct
- val name = "ZF/datatypes";
- type T = datatype_info Symtab.table;
-
- val empty = Symtab.empty;
- val prep_ext = I;
- val merge: T * T -> T = Symtab.merge (K true);
-
- fun print sg tab =
- Pretty.writeln (Pretty.strs ("datatypes:" ::
- map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
- end;
-
-structure DatatypesData = TheoryDataFun(DatatypesArgs);
-
-
-(** Constructor information: needed to map constructors to datatypes **)
-
-type constructor_info =
- {big_rec_name : string, (*name of the mutually recursive set*)
- constructors : term list, (*the constructors, as Consts*)
- rec_rewrites : thm list}; (*recursor equations*)
-
-
-structure ConstructorsArgs =
-struct
- val name = "ZF/constructors"
- type T = constructor_info Symtab.table
-
- val empty = Symtab.empty
- val prep_ext = I
- val merge: T * T -> T = Symtab.merge (K true)
-
- fun print sg tab = () (*nothing extra to print*)
-end;
-
-structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
-
-val setup_datatypes = [DatatypesData.init, ConstructorsData.init];
-
-
type datatype_result =
{con_defs : thm list, (*definitions made in thy*)
case_eqns : thm list, (*equations for case operator*)
--- a/src/ZF/Tools/induct_tacs.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Thu Jan 07 18:30:55 1999 +0100
@@ -1,9 +1,13 @@
-(* Title: HOL/Tools/induct_tacs.ML
+(* Title: ZF/Tools/induct_tacs.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Induction and exhaustion tactics for Isabelle/ZF
+
+The theory information needed to support them (and to support primrec)
+
+Also, a function to install other sets as if they were datatypes
*)
@@ -11,9 +15,65 @@
sig
val induct_tac : string -> int -> tactic
val exhaust_tac : string -> int -> tactic
+ val rep_datatype_i : thm -> thm -> thm list -> thm list -> theory -> theory
end;
+
+(** Datatype information, e.g. associated theorems **)
+
+type datatype_info =
+ {inductive: bool, (*true if inductive, not coinductive*)
+ constructors : term list, (*the constructors, as Consts*)
+ rec_rewrites : thm list, (*recursor equations*)
+ case_rewrites : thm list, (*case equations*)
+ induct : thm,
+ mutual_induct : thm,
+ exhaustion : thm};
+
+structure DatatypesArgs =
+ struct
+ val name = "ZF/datatypes";
+ type T = datatype_info Symtab.table;
+
+ val empty = Symtab.empty;
+ val prep_ext = I;
+ val merge: T * T -> T = Symtab.merge (K true);
+
+ fun print sg tab =
+ Pretty.writeln (Pretty.strs ("datatypes:" ::
+ map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
+ end;
+
+structure DatatypesData = TheoryDataFun(DatatypesArgs);
+
+
+(** Constructor information: needed to map constructors to datatypes **)
+
+type constructor_info =
+ {big_rec_name : string, (*name of the mutually recursive set*)
+ constructors : term list, (*the constructors, as Consts*)
+ rec_rewrites : thm list}; (*recursor equations*)
+
+
+structure ConstructorsArgs =
+struct
+ val name = "ZF/constructors"
+ type T = constructor_info Symtab.table
+
+ val empty = Symtab.empty
+ val prep_ext = I
+ val merge: T * T -> T = Symtab.merge (K true)
+
+ fun print sg tab = () (*nothing extra to print*)
+end;
+
+structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
+
+val setup_datatypes = [DatatypesData.init, ConstructorsData.init];
+
+
+
structure DatatypeTactics : DATATYPE_TACTICS =
struct
@@ -62,7 +122,62 @@
val exhaust_tac = exhaust_induct_tac true;
val induct_tac = exhaust_induct_tac false;
+
+
+(**** declare non-datatype as datatype ****)
+
+fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
+ let
+ val sign = sign_of thy;
+
+ (*analyze the LHS of a case equation to get a constructor*)
+ fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
+ | const_of eqn = error ("Ill-formed case equation: " ^
+ Sign.string_of_term sign eqn);
+
+ val constructors =
+ map (head_of o const_of o FOLogic.dest_Trueprop o
+ #prop o rep_thm) case_eqns;
+
+ val Const ("op :", _) $ _ $ Const(big_rec_name, _) =
+ FOLogic.dest_Trueprop (hd (prems_of elim));
+
+ val simps = case_eqns @ recursor_eqns;
+
+ val dt_info =
+ {inductive = true,
+ constructors = constructors,
+ rec_rewrites = recursor_eqns,
+ case_rewrites = case_eqns,
+ induct = induct,
+ mutual_induct = TrueI, (*No need for mutual induction*)
+ exhaustion = elim};
+
+ val con_info =
+ {big_rec_name = big_rec_name,
+ constructors = constructors,
+ (*let primrec handle definition by cases*)
+ rec_rewrites = (case recursor_eqns of
+ [] => case_eqns | _ => recursor_eqns)};
+
+ (*associate with each constructor the datatype name and rewrites*)
+ val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
+
+ in
+ thy |> Theory.add_path (Sign.base_name big_rec_name)
+ |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps),
+ [Simplifier.simp_add_global])]
+ |> DatatypesData.put
+ (Symtab.update
+ ((big_rec_name, dt_info), DatatypesData.get thy))
+ |> ConstructorsData.put
+ (foldr Symtab.update (con_pairs, ConstructorsData.get thy))
+ |> Theory.parent_path
+ end
+ handle _ => error "Failure in rep_datatype";
+
end;
-open DatatypeTactics;
+val exhaust_tac = DatatypeTactics.exhaust_tac;
+val induct_tac = DatatypeTactics.induct_tac;
--- a/src/ZF/ex/Limit.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/ex/Limit.ML Thu Jan 07 18:30:55 1999 +0100
@@ -174,7 +174,7 @@
Addsimps [chain_in, chain_rel];
Goal "[|chain(D,X); cpo(D); n:nat; m:nat|] ==> rel(D,X`n,(X`(m #+ n)))";
-by (res_inst_tac [("n","m")] nat_induct 1);
+by (induct_tac "m" 1);
by (ALLGOALS Simp_tac);
by (rtac cpo_trans 2); (* loops if repeated *)
by (REPEAT (ares_tac [cpo_refl,chain_in,chain_rel,nat_succI,add_type] 1));
@@ -191,7 +191,7 @@
by (rtac impE 1); (* The first three steps prepare for the induction proof *)
by (assume_tac 3);
by (assume_tac 2);
-by (res_inst_tac [("n","m")] nat_induct 1);
+by (induct_tac "m" 1);
by Safe_tac;
by (Asm_full_simp_tac 1);
by (rtac cpo_trans 2);
@@ -1456,36 +1456,25 @@
qed "e_less_add";
(* Again, would like more theorems about arithmetic. *)
-(* Well, HOL has much better support and automation of natural numbers. *)
val add1 = prove_goal Limit.thy
"!!x. n:nat ==> succ(n) = n #+ 1"
- (fn prems =>
- [asm_simp_tac (simpset() addsimps[add_succ_right,add_0_right]) 1]);
+ (fn prems => [Asm_simp_tac 1]);
Goal (* succ_sub1 *)
"x:nat ==> 0 < x --> succ(x #- 1)=x";
-by (res_inst_tac[("n","x")]nat_induct 1);
-by (assume_tac 1);
-by (Fast_tac 1);
-by Safe_tac;
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
+by (induct_tac "x" 1);
+by Auto_tac;
qed "succ_sub1";
Goal (* succ_le_pos *)
"[|m:nat; k:nat|] ==> succ(m) le m #+ k --> 0 < k";
-by (res_inst_tac[("n","m")]nat_induct 1);
-by (assume_tac 1);
-by (rtac impI 1);
-by (Asm_full_simp_tac 1);
-by Safe_tac;
-by (Asm_full_simp_tac 1); (* Surprise, surprise. *)
+by (induct_tac "m" 1);
+by Auto_tac;
qed "succ_le_pos";
Goal "[|n:nat; m:nat|] ==> m le n --> (EX k:nat. n = m #+ k)";
-by (res_inst_tac[("n","m")]nat_induct 1);
-by (assume_tac 1);
+by (induct_tac "m" 1);
by Safe_tac;
by (rtac bexI 1);
by (rtac (add_0 RS sym) 1);
@@ -1539,11 +1528,10 @@
Goal "[|emb_chain(DD,ee); m:nat; k:nat|] ==> \
\ emb(DD`m,DD`(m#+k),e_less(DD,ee,m,m#+k))";
-by (res_inst_tac[("n","k")]nat_induct 1);
-by (assume_tac 1);
-by (asm_simp_tac(simpset() addsimps[add_0_right,e_less_eq]) 1);
+by (induct_tac "k" 1);
+by (asm_simp_tac(simpset() addsimps[e_less_eq]) 1);
brr[emb_id,emb_chain_cpo] 1;
-by (asm_simp_tac(simpset() addsimps[add_succ_right,e_less_add]) 1);
+by (asm_simp_tac(simpset() addsimps[e_less_add]) 1);
by (auto_tac (claset() addIs [emb_comp,emb_chain_emb,emb_chain_cpo,add_type],
simpset()));
qed "emb_e_less_add";
@@ -1571,7 +1559,7 @@
"[| emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==> \
\ n le k --> \
\ e_less(DD,ee,m,m#+k) = e_less(DD,ee,m#+n,m#+k) O e_less(DD,ee,m,m#+n)";
-by (eres_inst_tac[("n","k")]nat_induct 1);
+by (induct_tac "k" 1);
by (asm_full_simp_tac(simpset() addsimps [e_less_eq, id_type RS id_comp]) 1);
by (asm_simp_tac(ZF_ss addsimps[le_succ_iff]) 1);
by (rtac impI 1);
@@ -1631,10 +1619,9 @@
Goal (* e_gr_fun_add *)
"[|emb_chain(DD,ee); n:nat; k:nat|] ==> \
\ e_gr(DD,ee,n#+k,n): set(DD`(n#+k))->set(DD`n)";
-by (res_inst_tac[("n","k")]nat_induct 1);
-by (assume_tac 1);
-by (asm_simp_tac(simpset() addsimps[add_0_right,e_gr_eq,id_type]) 1);
-by (asm_simp_tac(simpset() addsimps[add_succ_right,e_gr_add]) 1);
+by (induct_tac "k" 1);
+by (asm_simp_tac(simpset() addsimps[e_gr_eq,id_type]) 1);
+by (asm_simp_tac(simpset() addsimps[e_gr_add]) 1);
brr[comp_fun, Rp_cont, cont_fun, emb_chain_emb, emb_chain_cpo, add_type, nat_succI] 1;
qed "e_gr_fun_add";
@@ -1651,11 +1638,10 @@
"[| emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==> \
\ m le k --> \
\ e_gr(DD,ee,n#+k,n) = e_gr(DD,ee,n#+m,n) O e_gr(DD,ee,n#+k,n#+m)";
-by (res_inst_tac[("n","k")]nat_induct 1);
-by (assume_tac 1);
+by (induct_tac "k" 1);
by (rtac impI 1);
-by (asm_full_simp_tac(ZF_ss addsimps
- [le0_iff, add_0_right, e_gr_eq, id_type RS comp_id]) 1);
+by (asm_full_simp_tac(simpset() addsimps
+ [le0_iff, e_gr_eq, id_type RS comp_id]) 1);
by (asm_simp_tac(ZF_ss addsimps[le_succ_iff]) 1);
by (rtac impI 1);
by (etac disjE 1);
@@ -1683,13 +1669,12 @@
by (blast_tac (claset() addIs [emb_cont, emb_e_less]) 1);
qed "e_less_cont";
-Goal (* e_gr_cont_lemma *)
- "[|emb_chain(DD,ee); m:nat; n:nat|] ==> \
-\ n le m --> e_gr(DD,ee,m,n):cont(DD`m,DD`n)";
-by (res_inst_tac[("n","m")]nat_induct 1);
-by (assume_tac 1);
-by (asm_full_simp_tac(simpset() addsimps
- [le0_iff,e_gr_eq,nat_0I]) 1);
+Goal (* e_gr_cont *)
+ "[|n le m; emb_chain(DD,ee); m:nat; n:nat|] ==> \
+\ e_gr(DD,ee,m,n):cont(DD`m,DD`n)";
+by (etac rev_mp 1);
+by (induct_tac "m" 1);
+by (asm_full_simp_tac(simpset() addsimps [le0_iff,e_gr_eq,nat_0I]) 1);
brr[impI,id_cont,emb_chain_cpo,nat_0I] 1;
by (asm_full_simp_tac(simpset() addsimps[le_succ_iff]) 1);
by (etac disjE 1);
@@ -1699,12 +1684,6 @@
brr[comp_pres_cont,Rp_cont,emb_chain_cpo,emb_chain_emb,nat_succI] 1;
by (asm_simp_tac(simpset() addsimps[e_gr_eq,nat_succI]) 1);
by (auto_tac (claset() addIs [id_cont,emb_chain_cpo], simpset()));
-qed "e_gr_cont_lemma";
-
-Goal (* e_gr_cont *)
- "[|n le m; emb_chain(DD,ee); m:nat; n:nat|] ==> \
-\ e_gr(DD,ee,m,n):cont(DD`m,DD`n)";
-brr[e_gr_cont_lemma RS mp] 1;
qed "e_gr_cont";
(* Considerably shorter.... 57 against 26 *)
@@ -1713,12 +1692,11 @@
"[|n le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==> \
\ e_less(DD,ee,m,m#+n) = e_gr(DD,ee,m#+k,m#+n) O e_less(DD,ee,m,m#+k)";
(* Use mp to prepare for induction. *)
-by (rtac mp 1);
-by (assume_tac 2);
-by (res_inst_tac[("n","k")]nat_induct 1);
-by (assume_tac 1);
-by (asm_full_simp_tac(ZF_ss addsimps
- [le0_iff, add_0_right, e_gr_eq, e_less_eq, id_type RS id_comp]) 1);by (simp_tac(ZF_ss addsimps[le_succ_iff]) 1);
+by (etac rev_mp 1);
+by (induct_tac "k" 1);
+by (asm_full_simp_tac(simpset() addsimps
+ [e_gr_eq, e_less_eq, id_type RS id_comp]) 1);
+by (simp_tac(ZF_ss addsimps[le_succ_iff]) 1);
by (rtac impI 1);
by (etac disjE 1);
by (etac impE 1);
@@ -1742,12 +1720,10 @@
"[|m le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==> \
\ e_gr(DD,ee,n#+m,n) = e_gr(DD,ee,n#+k,n) O e_less(DD,ee,n#+m,n#+k)";
(* Use mp to prepare for induction. *)
-by (rtac mp 1);
-by (assume_tac 2);
-by (res_inst_tac[("n","k")]nat_induct 1);
-by (assume_tac 1);
+by (etac rev_mp 1);
+by (induct_tac "k" 1);
by (asm_full_simp_tac(simpset() addsimps
- [add_0_right, e_gr_eq, e_less_eq, id_type RS id_comp]) 1);
+ [e_gr_eq, e_less_eq, id_type RS id_comp]) 1);
by (simp_tac(ZF_ss addsimps[le_succ_iff]) 1);
by (rtac impI 1);
by (etac disjE 1);
@@ -2042,10 +2018,10 @@
"[|m le n; emb_chain(DD,ee); x:set(Dinf(DD,ee)); m:nat; n:nat|] ==> \
\ rel(DD`n,e_less(DD,ee,m,n)`(x`m),x`n)";
by (etac rev_mp 1); (* For induction proof *)
-by (res_inst_tac[("n","n")]nat_induct 1);
-by (rtac impI 2);
-by (asm_full_simp_tac (simpset() addsimps [e_less_eq]) 2);
-by (stac id_thm 2);
+by (induct_tac "n" 1);
+by (rtac impI 1);
+by (asm_full_simp_tac (simpset() addsimps [e_less_eq]) 1);
+by (stac id_thm 1);
brr[apply_type,Dinf_prod,cpo_refl,emb_chain_cpo,nat_0I] 1;
by (asm_full_simp_tac (simpset() addsimps [le_succ_iff]) 1);
by (rtac impI 1);
@@ -2080,10 +2056,10 @@
"[|n le m; emb_chain(DD,ee); x:set(Dinf(DD,ee)); m:nat; n:nat|] ==> \
\ rel(DD`n,e_gr(DD,ee,m,n)`(x`m),x`n)";
by (etac rev_mp 1); (* For induction proof *)
-by (res_inst_tac[("n","m")]nat_induct 1);
-by (rtac impI 2);
-by (asm_full_simp_tac (simpset() addsimps [e_gr_eq]) 2);
-by (stac id_thm 2);
+by (induct_tac "m" 1);
+by (rtac impI 1);
+by (asm_full_simp_tac (simpset() addsimps [e_gr_eq]) 1);
+by (stac id_thm 1);
brr[apply_type,Dinf_prod,cpo_refl,emb_chain_cpo,nat_0I] 1;
by (asm_full_simp_tac (simpset() addsimps [le_succ_iff]) 1);
by (rtac impI 1);
@@ -2429,22 +2405,17 @@
simpset()));
qed "mono_lemma";
-(* PAINFUL: wish condrew with difficult conds on term bound in lam-abs. *)
-(* Introduces need for lemmas. *)
-
Goal "[| commute(DD,ee,E,r); commute(DD,ee,G,f); \
\ emb_chain(DD,ee); cpo(E); cpo(G); n:nat |] ==> \
\ (lam na:nat. (lam f:cont(E, G). f O r(n)) ` \
\ ((lam n:nat. f(n) O Rp(DD ` n, E, r(n))) ` na)) = \
\ (lam na:nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))";
by (rtac fun_extension 1);
-by (stac beta 3);
-by (stac beta 4);
-by (stac beta 5);
-by (rtac lam_type 1);
-by (stac beta 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (fast_tac (claset() addIs [lam_type, comp_pres_cont, Rp_cont, emb_cont, commute_emb, emb_chain_cpo])));
+by (fast_tac (claset() addIs [lam_type]) 1);
+by (ALLGOALS
+ (asm_simp_tac
+ (simpset() setSolver (type_auto_tac [lam_type, comp_pres_cont, Rp_cont,
+ emb_cont, commute_emb, emb_chain_cpo]))));
val lemma = result();
Goal "[| commute(DD,ee,E,r); commute(DD,ee,G,f); \
--- a/src/ZF/ex/Mutil.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/ex/Mutil.ML Thu Jan 07 18:30:55 1999 +0100
@@ -96,20 +96,21 @@
qed "tiling_domino_0_1";
Goal "[| i: nat; n: nat |] ==> {i} * (n #+ n) : tiling(domino)";
-by (nat_ind_tac "n" [] 1);
+by (induct_tac "n" 1);
by (simp_tac (simpset() addsimps tiling.intrs) 1);
by (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_succ2]) 1);
by (resolve_tac tiling.intrs 1);
by (assume_tac 2);
+by (rename_tac "n'" 1);
by (subgoal_tac (*seems the easiest way of turning one to the other*)
- "{i}*{succ(n1#+n1)} Un {i}*{n1#+n1} = {<i,n1#+n1>, <i,succ(n1#+n1)>}" 1);
+ "{i}*{succ(n'#+n')} Un {i}*{n'#+n'} = {<i,n'#+n'>, <i,succ(n'#+n')>}" 1);
by (Blast_tac 2);
by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1);
by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 1);
qed "dominoes_tile_row";
Goal "[| m: nat; n: nat |] ==> m * (n #+ n) : tiling(domino)";
-by (nat_ind_tac "m" [] 1);
+by (induct_tac "m" 1);
by (simp_tac (simpset() addsimps tiling.intrs) 1);
by (asm_simp_tac (simpset() addsimps [Sigma_succ1]) 1);
by (blast_tac (claset() addIs [tiling_UnI, dominoes_tile_row]
--- a/src/ZF/ex/Primrec.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/ex/Primrec.ML Thu Jan 07 18:30:55 1999 +0100
@@ -23,7 +23,7 @@
pr_typechecks @ prim_rec.intrs));
Goalw [ACK_def] "i:nat ==> ACK(i): prim_rec";
-by (etac nat_induct 1);
+by (induct_tac "i" 1);
by (ALLGOALS Asm_simp_tac);
qed "ACK_in_prim_rec";
@@ -64,10 +64,10 @@
(*PROPERTY A 4*)
Goal "i:nat ==> ALL j:nat. j < ack(i,j)";
-by (etac nat_induct 1);
+by (induct_tac "i" 1);
by (Asm_simp_tac 1);
by (rtac ballI 1);
-by (eres_inst_tac [("n","j")] nat_induct 1);
+by (induct_tac "j" 1);
by (DO_GOAL [rtac (nat_0I RS nat_0_le RS lt_trans),
Asm_simp_tac] 1);
by (DO_GOAL [etac (succ_leI RS lt_trans1),
@@ -77,7 +77,7 @@
(*PROPERTY A 5-, the single-step lemma*)
Goal "[| i:nat; j:nat |] ==> ack(i,j) < ack(i, succ(j))";
-by (etac nat_induct 1);
+by (induct_tac "i" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack2])));
qed "ack_lt_ack_succ2";
@@ -98,7 +98,7 @@
(*PROPERTY A 6*)
Goal "[| i:nat; j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)";
-by (nat_ind_tac "j" [] 1);
+by (induct_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
by (rtac ack_le_mono2 1);
by (rtac (lt_ack2 RS succ_leI RS le_trans) 1);
@@ -129,13 +129,13 @@
(*PROPERTY A 8*)
Goal "j:nat ==> ack(1,j) = succ(succ(j))";
-by (etac nat_induct 1);
+by (induct_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
qed "ack_1";
(*PROPERTY A 9*)
Goal "j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
-by (etac nat_induct 1);
+by (induct_tac "j" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ack_1, add_succ_right])));
qed "ack_2";
@@ -183,7 +183,7 @@
(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
Goal "[| i:nat; j:nat |] ==> i < ack(i,j)";
-by (etac nat_induct 1);
+by (induct_tac "i" 1);
by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
by (tc_tac []);
@@ -261,7 +261,7 @@
by (asm_simp_tac (simpset() addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
by (Asm_simp_tac 1);
by (etac ssubst 1); (*get rid of the needless assumption*)
-by (eres_inst_tac [("n","a")] nat_induct 1);
+by (induct_tac "a" 1);
(*base case*)
by (DO_GOAL [Asm_simp_tac, rtac lt_trans, etac bspec,
assume_tac, rtac (add_le_self RS ack_lt_mono1),
--- a/src/ZF/ex/Ramsey.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/ex/Ramsey.ML Thu Jan 07 18:30:55 1999 +0100
@@ -18,16 +18,13 @@
Available from the author: kaufmann@cli.com
*)
-open Ramsey;
-
(*** Cliques and Independent sets ***)
Goalw [Clique_def] "Clique(0,V,E)";
by (Fast_tac 1);
qed "Clique0";
-Goalw [Clique_def]
- "[| Clique(C,V',E); V'<=V |] ==> Clique(C,V,E)";
+Goalw [Clique_def] "[| Clique(C,V',E); V'<=V |] ==> Clique(C,V,E)";
by (Fast_tac 1);
qed "Clique_superset";
@@ -74,37 +71,37 @@
(*The #-succ(0) strengthens the original theorem statement, but precisely
the same proof could be used!!*)
-val prems = goal Ramsey.thy
- "m: nat ==> \
-\ ALL n: nat. ALL A B. Atleast((m#+n) #- succ(0), A Un B) --> \
-\ Atleast(m,A) | Atleast(n,B)";
-by (nat_ind_tac "m" prems 1);
+Goal "m: nat ==> \
+\ ALL n: nat. ALL A B. Atleast((m#+n) #- succ(0), A Un B) --> \
+\ Atleast(m,A) | Atleast(n,B)";
+by (induct_tac "m" 1);
by (fast_tac (claset() addSIs [Atleast0]) 1);
by (Asm_simp_tac 1);
by (rtac ballI 1);
-by (rename_tac "n" 1); (*simplifier does NOT preserve bound names!*)
-by (nat_ind_tac "n" [] 1);
+by (rename_tac "m' n" 1); (*simplifier does NOT preserve bound names!*)
+by (induct_tac "n" 1);
by (fast_tac (claset() addSIs [Atleast0]) 1);
-by (asm_simp_tac (simpset() addsimps [add_succ_right]) 1);
+by (Asm_simp_tac 1);
by Safe_tac;
by (etac (Atleast_succD RS bexE) 1);
+by (rename_tac "n' A B z" 1);
by (etac UnE 1);
-(**case x:B. Instantiate the 'ALL A B' induction hypothesis. **)
-by (dres_inst_tac [("x1","A"), ("x","B-{x}")] (spec RS spec) 2);
+(**case z:B. Instantiate the 'ALL A B' induction hypothesis. **)
+by (dres_inst_tac [("x1","A"), ("x","B-{z}")] (spec RS spec) 2);
by (etac (mp RS disjE) 2);
-(*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
+(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
by (REPEAT (eresolve_tac [asm_rl, notE, Atleast_Diff_succI] 3));
(*proving the condition*)
by (etac Atleast_superset 2 THEN Fast_tac 2);
-(**case x:A. Instantiate the 'ALL n:nat. ALL A B' induction hypothesis. **)
-by (dres_inst_tac [("x2","succ(n1)"), ("x1","A-{x}"), ("x","B")]
+(**case z:A. Instantiate the 'ALL n:nat. ALL A B' induction hypothesis. **)
+by (dres_inst_tac [("x2","succ(n')"), ("x1","A-{z}"), ("x","B")]
(bspec RS spec RS spec) 1);
by (etac nat_succI 1);
by (etac (mp RS disjE) 1);
-(*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
+(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
(*proving the condition*)
-by (asm_simp_tac (simpset() addsimps [add_succ_right]) 1);
+by (Asm_simp_tac 1);
by (etac Atleast_superset 1 THEN Fast_tac 1);
qed "pigeon2_lemma";
@@ -129,31 +126,27 @@
(*The use of succ(m) here, rather than #-succ(0), simplifies the proof of
Ramsey_step_lemma.*)
-val prems = goal Ramsey.thy
- "[| Atleast(m #+ n, A); m: nat; n: nat |] ==> \
-\ Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
+Goal "[| Atleast(m #+ n, A); m: nat; n: nat |] \
+\ ==> Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
by (rtac (nat_succI RS pigeon2) 1);
-by (simp_tac (simpset() addsimps prems) 3);
+by (Asm_simp_tac 3);
by (rtac Atleast_superset 3);
-by (REPEAT (resolve_tac prems 1));
-by (Fast_tac 1);
+by Auto_tac;
qed "Atleast_partition";
(*For the Atleast part, proves ~(a:I) from the second premise!*)
-val prems = goalw Ramsey.thy [Symmetric_def,Indept_def]
+Goalw [Symmetric_def,Indept_def]
"[| Symmetric(E); Indept(I, {z: V-{a}. <a,z> ~: E}, E); a: V; \
\ Atleast(j,I) |] ==> \
\ Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
-by (cut_facts_tac prems 1);
-by (fast_tac (claset() addSEs [Atleast_succI]) 1); (*34 secs*)
+by (blast_tac (claset() addSIs [Atleast_succI]) 1);
qed "Indept_succ";
-val prems = goalw Ramsey.thy [Symmetric_def,Clique_def]
+Goalw [Symmetric_def,Clique_def]
"[| Symmetric(E); Clique(C, {z: V-{a}. <a,z>:E}, E); a: V; \
\ Atleast(j,C) |] ==> \
\ Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))";
-by (cut_facts_tac prems 1);
-by (fast_tac (claset() addSEs [Atleast_succI]) 1); (*41 secs*)
+by (blast_tac (claset() addSIs [Atleast_succI]) 1);
qed "Clique_succ";
(** Induction step **)
@@ -187,12 +180,11 @@
(** The actual proof **)
(*Again, the induction requires Ramsey numbers to be positive.*)
-val prems = goal Ramsey.thy
- "i: nat ==> ALL j: nat. EX n:nat. Ramsey(succ(n), i, j)";
-by (nat_ind_tac "i" prems 1);
+Goal "i: nat ==> ALL j: nat. EX n:nat. Ramsey(succ(n), i, j)";
+by (induct_tac "i" 1);
by (fast_tac (claset() addSIs [Ramsey0j]) 1);
by (rtac ballI 1);
-by (nat_ind_tac "j" [] 1);
+by (induct_tac "j" 1);
by (fast_tac (claset() addSIs [Ramseyi0]) 1);
by (fast_tac (claset() addSDs [bspec]
addSIs [add_type,Ramsey_step_lemma]) 1);
--- a/src/ZF/thy_syntax.ML Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/thy_syntax.ML Thu Jan 07 18:30:55 1999 +0100
@@ -130,6 +130,19 @@
end;
+(** rep_datatype **)
+
+fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) =
+ "|> DatatypeTactics.rep_datatype_i " ^ elim ^ " " ^ induct ^ "\n " ^
+ mk_list case_eqns ^ " " ^ mk_list recursor_eqns;
+
+val rep_datatype_decl =
+ (("elim" $$-- ident) --
+ ("induct" $$-- ident) --
+ ("case_eqns" $$-- list1 ident) --
+ ("recursor_eqns" $$-- list1 ident)) >> mk_rep_dt_string;
+
+
(** primrec **)
fun mk_primrec_decl eqns =
@@ -154,12 +167,14 @@
val _ = ThySyn.add_syntax
["inductive", "coinductive", "datatype", "codatatype", "and", "|",
- "<=", "domains", "intrs", "monos", "con_defs", "type_intrs",
- "type_elims"]
- [section "inductive" "" (inductive_decl false),
- section "coinductive" "" (inductive_decl true),
- section "datatype" "" (datatype_decl false),
- section "codatatype" "" (datatype_decl true),
- section "primrec" "" primrec_decl];
+ "<=", "domains", "intrs", "monos", "con_defs", "type_intrs", "type_elims",
+ (*rep_datatype*)
+ "elim", "induct", "case_eqns", "recursor_eqns"]
+ [section "inductive" "" (inductive_decl false),
+ section "coinductive" "" (inductive_decl true),
+ section "datatype" "" (datatype_decl false),
+ section "codatatype" "" (datatype_decl true),
+ section "rep_datatype" "" rep_datatype_decl,
+ section "primrec" "" primrec_decl];
end;