Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
--- a/src/ZF/Arith.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Arith.ML Fri Sep 17 16:16:38 1993 +0200
@@ -29,10 +29,9 @@
goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
val rec_ss = ZF_ss
- addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")])
- addrews [nat_case_succ, nat_succI];
+ addsimps [nat_case_succ, nat_succI];
by (rtac rec_trans 1);
-by (SIMP_TAC rec_ss 1);
+by (simp_tac rec_ss 1);
val rec_succ = result();
val major::prems = goal Arith.thy
@@ -42,20 +41,12 @@
\ |] ==> rec(n,a,b) : C(n)";
by (rtac (major RS nat_induct) 1);
by (ALLGOALS
- (ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ]))));
+ (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
val rec_type = result();
-val prems = goalw Arith.thy [rec_def]
- "[| n=n'; a=a'; !!m z. b(m,z)=b'(m,z) \
-\ |] ==> rec(n,a,b)=rec(n',a',b')";
-by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong]
- addrews (prems RL [sym])) 1);
-val rec_cong = result();
-
val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
-val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong]
- addrews ([rec_0,rec_succ] @ nat_typechecks);
+val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
(** Addition **)
@@ -101,16 +92,16 @@
"n:nat ==> 0 #- n = 0"
(fn [prem]=>
[ (rtac (prem RS nat_induct) 1),
- (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]);
+ (ALLGOALS (asm_simp_tac nat_ss)) ]);
(*Must simplify BEFORE the induction!! (Else we get a critical pair)
succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *)
val diff_succ_succ = prove_goalw Arith.thy [diff_def]
"[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n"
(fn prems=>
- [ (ASM_SIMP_TAC (nat_ss addrews prems) 1),
+ [ (asm_simp_tac (nat_ss addsimps prems) 1),
(nat_ind_tac "n" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
val prems = goal Arith.thy
"[| m:nat; n:nat |] ==> m #- n : succ(m)";
@@ -119,8 +110,8 @@
by (resolve_tac prems 1);
by (etac succE 3);
by (ALLGOALS
- (ASM_SIMP_TAC
- (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
+ (asm_simp_tac
+ (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
val diff_leq = result();
(*** Simplification over add, mult, diff ***)
@@ -130,10 +121,7 @@
mult_0, mult_succ,
diff_0, diff_0_eq_0, diff_succ_succ];
-val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"];
-
-val arith_ss = nat_ss addcongs arith_congs
- addrews (arith_rews@arith_typechecks);
+val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
(*** Addition ***)
@@ -142,7 +130,7 @@
"m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*The following two lemmas are used for add_commute and sometimes
elsewhere, since they are safe for rewriting.*)
@@ -150,13 +138,13 @@
"m:nat ==> m #+ 0 = m"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
val add_succ_right = prove_goal Arith.thy
"m:nat ==> m #+ succ(n) = succ(m #+ n)"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*Commutative law for addition*)
val add_commute = prove_goal Arith.thy
@@ -164,15 +152,15 @@
(fn prems=>
[ (nat_ind_tac "n" prems 1),
(ALLGOALS
- (ASM_SIMP_TAC
- (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]);
+ (asm_simp_tac
+ (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
(*Cancellation law on the left*)
val [knat,eqn] = goal Arith.thy
"[| k:nat; k #+ m = k #+ n |] ==> m=n";
by (rtac (eqn RS rev_mp) 1);
by (nat_ind_tac "k" [knat] 1);
-by (ALLGOALS (SIMP_TAC arith_ss));
+by (ALLGOALS (simp_tac arith_ss));
by (fast_tac ZF_cs 1);
val add_left_cancel = result();
@@ -183,39 +171,40 @@
"m:nat ==> m #* 0 = 0"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*right successor law for multiplication*)
val mult_succ_right = prove_goal Arith.thy
- "[| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))),
+ "!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
+ (fn _=>
+ [ (nat_ind_tac "m" [] 1),
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
(*The final goal requires the commutative law for addition*)
- (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1)) ]);
+ (rtac (add_commute RS subst_context) 1),
+ (REPEAT (assume_tac 1)) ]);
(*Commutative law for multiplication*)
val mult_commute = prove_goal Arith.thy
"[| m:nat; n:nat |] ==> m #* n = n #* m"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC
- (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]);
+ (ALLGOALS (asm_simp_tac
+ (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
(*addition distributes over multiplication*)
val add_mult_distrib = prove_goal Arith.thy
"[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
(*Distributive law on the left; requires an extra typing premise*)
val add_mult_distrib_left = prove_goal Arith.thy
"[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
(fn prems=>
let val mult_commute' = read_instantiate [("m","k")] mult_commute
- val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems)
- in [ (SIMP_TAC ss 1) ]
+ val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
+ in [ (simp_tac ss 1) ]
end);
(*Associative law for multiplication*)
@@ -223,7 +212,7 @@
"[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
(*** Difference ***)
@@ -232,7 +221,7 @@
"m:nat ==> m #- m = 0"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
val notless::prems = goal Arith.thy
@@ -241,8 +230,8 @@
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (resolve_tac prems 1);
by (resolve_tac prems 1);
-by (ALLGOALS (ASM_SIMP_TAC
- (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
+by (ALLGOALS (asm_simp_tac
+ (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
naturals_are_ordinals]))));
val add_diff_inverse = result();
@@ -251,29 +240,24 @@
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 (arith_ss addrews [mnat])));
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
val diff_add_inverse = result();
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 (arith_ss addrews [mnat])));
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
val diff_add_0 = result();
(*** Remainder ***)
(*In ordinary notation: if 0<n and n<=m then m-n < m *)
-val prems = goal Arith.thy
- "[| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m";
-by (cut_facts_tac prems 1);
+goal Arith.thy "!!m n. [| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m";
by (etac rev_mp 1);
by (etac rev_mp 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-by (ALLGOALS (ASM_SIMP_TAC
- (nat_ss addrews (prems@[diff_leq,diff_succ_succ]))));
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
val div_termination = result();
val div_rls =
@@ -286,17 +270,17 @@
by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
val mod_type = result();
-val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination];
+val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
val prems = goal Arith.thy "[| 0:n; m:n; m:nat; n:nat |] ==> m mod n = m";
by (rtac (mod_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val mod_less = result();
val prems = goal Arith.thy
"[| 0:n; ~m:n; m:nat; n:nat |] ==> m mod n = (m#-n) mod n";
by (rtac (mod_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val mod_geq = result();
(*** Quotient ***)
@@ -310,13 +294,13 @@
val prems = goal Arith.thy
"[| 0:n; m:n; m:nat; n:nat |] ==> m div n = 0";
by (rtac (div_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val div_less = result();
val prems = goal Arith.thy
"[| 0:n; ~m:n; m:nat; n:nat |] ==> m div n = succ((m#-n) div n)";
by (rtac (div_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val div_geq = result();
(*Main Result.*)
@@ -326,8 +310,8 @@
by (resolve_tac prems 1);
by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
by (ALLGOALS
- (ASM_SIMP_TAC
- (arith_ss addrews ([mod_type,div_type] @ prems @
+ (asm_simp_tac
+ (arith_ss addsimps ([mod_type,div_type] @ prems @
[mod_less,mod_geq, div_less, div_geq,
add_assoc, add_diff_inverse, div_termination]))));
val mod_div_equality = result();
@@ -338,7 +322,7 @@
val [mnat,nnat] = goal Arith.thy
"[| m:nat; n:nat |] ==> ~ (m #+ n) : n";
by (rtac (mnat RS nat_induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl])));
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
by (rtac notI 1);
by (etac notE 1);
by (etac (succI1 RS Ord_trans) 1);
--- a/src/ZF/Arith.thy Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Arith.thy Fri Sep 17 16:16:38 1993 +0200
@@ -16,7 +16,7 @@
"#-" :: "[i,i]=>i" (infixl 65)
rules
- rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(n, a, %m. b(m, f`m)))"
+ rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`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))"
--- a/src/ZF/Bool.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Bool.ML Fri Sep 17 16:16:38 1993 +0200
@@ -53,9 +53,6 @@
by (resolve_tac prems 1);
val cond_type = result();
-val [cond_cong] = mk_congs Bool.thy ["cond"];
-val bool_congs = mk_congs Bool.thy ["cond","not","op and","op or","op xor"];
-
val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
by (rewtac rew);
by (rtac cond_1 1);
--- a/src/ZF/Epsilon.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Epsilon.ML Fri Sep 17 16:16:38 1993 +0200
@@ -64,8 +64,8 @@
"!!X A n. [| Transset(X); A<=X; n: nat |] ==> \
\ nat_rec(n, A, %m r. Union(r)) <= X";
by (etac nat_induct 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_0]) 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_succ]) 1);
+by (asm_simp_tac (ZF_ss addsimps [nat_rec_0]) 1);
+by (asm_simp_tac (ZF_ss addsimps [nat_rec_succ]) 1);
by (fast_tac ZF_cs 1);
val eclose_least_lemma = result();
@@ -126,8 +126,8 @@
by (rtac (kmemj RS eclose_induct) 1);
by (rtac wfrec_ssubst 1);
by (rtac wfrec_ssubst 1);
-by (ASM_SIMP_TAC (wf_ss addrews [under_Memrel_eclose,
- jmemi RSN (2,mem_eclose_sing_trans)]) 1);
+by (asm_simp_tac (ZF_ss addsimps [under_Memrel_eclose,
+ jmemi RSN (2,mem_eclose_sing_trans)]) 1);
val wfrec_eclose_eq = result();
val [prem] = goal Epsilon.thy
@@ -139,8 +139,8 @@
goalw Epsilon.thy [transrec_def]
"transrec(a,H) = H(a, lam x:a. transrec(x,H))";
by (rtac wfrec_ssubst 1);
-by (SIMP_TAC (wf_ss addrews [wfrec_eclose_eq2,
- arg_in_eclose_sing, under_Memrel_eclose]) 1);
+by (simp_tac (ZF_ss addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
+ under_Memrel_eclose]) 1);
val transrec = result();
(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
@@ -173,23 +173,12 @@
by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
val Ord_transrec_type = result();
-(*Congruence*)
-val prems = goalw Epsilon.thy [transrec_def,Memrel_def]
- "[| a=a'; !!x u. H(x,u)=H'(x,u) |] ==> transrec(a,H)=transrec(a',H')";
-val transrec_ss =
- ZF_ss addcongs ([wfrec_cong] @ mk_congs Epsilon.thy ["eclose"])
- addrews (prems RL [sym]);
-by (SIMP_TAC transrec_ss 1);
-val transrec_cong = result();
-
(*** Rank ***)
-val ord_ss = ZF_ss addcongs (mk_congs Ord.thy ["Ord"]);
-
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
by (rtac (rank_def RS def_transrec RS ssubst) 1);
-by (SIMP_TAC ZF_ss 1);
+by (simp_tac ZF_ss 1);
val rank = result();
goal Epsilon.thy "Ord(rank(a))";
@@ -203,7 +192,7 @@
val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
by (rtac (major RS trans_induct) 1);
by (rtac (rank RS ssubst) 1);
-by (ASM_SIMP_TAC (ord_ss addrews [Ord_equality]) 1);
+by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
val rank_of_Ord = result();
val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
--- a/src/ZF/List.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/List.ML Fri Sep 17 16:16:38 1993 +0200
@@ -62,7 +62,7 @@
\ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(<x,y>) \
\ |] ==> list_case(l,c,h) : C(l)";
by (rtac (major RS list_induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
([list_case_0,list_case_Pair]@prems))));
val list_case_type = result();
****)
@@ -71,10 +71,10 @@
(** For recursion **)
goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val rank_Cons1 = result();
goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val rank_Cons2 = result();
--- a/src/ZF/ListFn.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/ListFn.ML Fri Sep 17 16:16:38 1993 +0200
@@ -11,19 +11,14 @@
(** list_rec -- by Vset recursion **)
-(*Used to verify list_rec*)
-val list_rec_ss = ZF_ss
- addcongs (mk_typed_congs ListFn.thy [("h", "[i,i,i]=>i")])
- addrews List.case_eqns;
-
goal ListFn.thy "list_rec(Nil,c,h) = c";
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
-by (SIMP_TAC list_rec_ss 1);
+by (simp_tac (ZF_ss addsimps List.case_eqns) 1);
val list_rec_Nil = result();
goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
-by (SIMP_TAC (list_rec_ss addrews [Vset_rankI, rank_Cons2]) 1);
+by (simp_tac (ZF_ss addsimps (List.case_eqns @ [Vset_rankI, rank_Cons2])) 1);
val list_rec_Cons = result();
(*Type checking -- proved by induction, as usual*)
@@ -33,8 +28,8 @@
\ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \
\ |] ==> list_rec(l,c,h) : C(l)";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC
- (ZF_ss addrews (prems@[list_rec_Nil,list_rec_Cons]))));
+by (ALLGOALS (asm_simp_tac
+ (ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons]))));
val list_rec_type = result();
(** Versions for use with definitions **)
@@ -122,47 +117,42 @@
map_type, map_type2, app_type, length_type, rev_type, flat_type,
list_add_type];
-val list_congs =
- List.congs @
- mk_congs ListFn.thy
- ["list_rec","map","op @","length","rev","flat","list_add"];
-
val list_ss = arith_ss
- addcongs list_congs
- addrews List.case_eqns
- addrews list_typechecks
- addrews [list_rec_Nil, list_rec_Cons,
+ addsimps List.case_eqns
+ addsimps [list_rec_Nil, list_rec_Cons,
map_Nil, map_Cons,
app_Nil, app_Cons,
length_Nil, length_Cons,
rev_Nil, rev_Cons,
flat_Nil, flat_Cons,
- list_add_Nil, list_add_Cons];
+ list_add_Nil, list_add_Cons]
+ setsolver (type_auto_tac list_typechecks);
+(*Could also rewrite using the list_typechecks...*)
(*** theorems about map ***)
val prems = goal ListFn.thy
"l: list(A) ==> map(%u.u, l) = l";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val map_ident = result();
val prems = goal ListFn.thy
"l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val map_compose = result();
val prems = goal ListFn.thy
"xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val map_app_distrib = result();
val prems = goal ListFn.thy
"ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
by (list_ind_tac "ls" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
val map_flat = result();
val prems = goal ListFn.thy
@@ -170,9 +160,7 @@
\ list_rec(map(h,l), c, d) = \
\ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS
- (ASM_SIMP_TAC
- (list_ss addcongs (mk_typed_congs ListFn.thy [("d", "[i,i,i]=>i")]))));
+by (ALLGOALS (asm_simp_tac list_ss));
val list_rec_map = result();
(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
@@ -183,7 +171,7 @@
val prems = goal ListFn.thy
"l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val map_list_Collect = result();
(*** theorems about length ***)
@@ -191,13 +179,13 @@
val prems = goal ListFn.thy
"xs: list(A) ==> length(map(h,xs)) = length(xs)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val length_map = result();
val prems = goal ListFn.thy
"xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val length_app = result();
(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m
@@ -207,60 +195,59 @@
val prems = goal ListFn.thy
"xs: list(A) ==> length(rev(xs)) = length(xs)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app, add_commute_succ])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ])));
val length_rev = result();
val prems = goal ListFn.thy
"ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
by (list_ind_tac "ls" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
val length_flat = result();
(*** theorems about app ***)
val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
by (rtac (major RS List.induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val app_right_Nil = result();
val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val app_assoc = result();
val prems = goal ListFn.thy
"ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
by (list_ind_tac "ls" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_assoc])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc])));
val flat_app_distrib = result();
(*** theorems about rev ***)
val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
val rev_map_distrib = result();
(*Simplifier needs the premises as assumptions because rewriting will not
instantiate the variable ?A in the rules' typing conditions; note that
rev_type does not instantiate ?A. Only the premises do.
*)
-val prems = goal ListFn.thy
- "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
-by (cut_facts_tac prems 1);
+goal ListFn.thy
+ "!!xs. [| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
by (etac List.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_right_Nil,app_assoc])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc])));
val rev_app_distrib = result();
val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [rev_app_distrib])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib])));
val rev_rev_ident = result();
val prems = goal ListFn.thy
"ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
by (list_ind_tac "ls" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews
+by (ALLGOALS (asm_simp_tac (list_ss addsimps
[map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
val rev_flat = result();
@@ -273,22 +260,22 @@
by (cut_facts_tac prems 1);
by (list_ind_tac "xs" prems 1);
by (ALLGOALS
- (ASM_SIMP_TAC (list_ss addrews [add_0_right, add_assoc RS sym])));
-by (resolve_tac arith_congs 1);
-by (REPEAT (ares_tac [refl, list_add_type, add_commute] 1));
+ (asm_simp_tac (list_ss addsimps [add_0_right, add_assoc RS sym])));
+by (rtac (add_commute RS subst_context) 1);
+by (REPEAT (ares_tac [refl, list_add_type] 1));
val list_add_app = result();
val prems = goal ListFn.thy
"l: list(nat) ==> list_add(rev(l)) = list_add(l)";
by (list_ind_tac "l" prems 1);
by (ALLGOALS
- (ASM_SIMP_TAC (list_ss addrews [list_add_app, add_0_right])));
+ (asm_simp_tac (list_ss addsimps [list_add_app, add_0_right])));
val list_add_rev = result();
val prems = goal ListFn.thy
"ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
by (list_ind_tac "ls" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [list_add_app])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app])));
by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
val list_add_flat = result();
@@ -301,6 +288,6 @@
\ |] ==> P(l)";
by (rtac (major RS rev_rev_ident RS subst) 1);
by (rtac (major RS rev_type RS List.induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews prems)));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps prems)));
val list_append_induct = result();
--- a/src/ZF/Nat.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Nat.ML Fri Sep 17 16:16:38 1993 +0200
@@ -95,8 +95,8 @@
\ |] ==> m <= n --> P(m) --> P(n)";
by (nat_ind_tac "n" prems 1);
by (ALLGOALS
- (ASM_SIMP_TAC
- (ZF_ss addrews (prems@distrib_rews@[subset_empty_iff, subset_succ_iff,
+ (asm_simp_tac
+ (ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff,
Ord_nat RS Ord_in_Ord]))));
val nat_induct_from_lemma = result();
@@ -127,17 +127,17 @@
(** nat_case **)
-goalw Nat.thy [nat_case_def] "nat_case(0,a,b) = a";
+goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
by (fast_tac (ZF_cs addIs [the_equality]) 1);
val nat_case_0 = result();
-goalw Nat.thy [nat_case_def] "nat_case(succ(m),a,b) = b(m)";
+goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
by (fast_tac (ZF_cs addIs [the_equality]) 1);
val nat_case_succ = result();
val major::prems = goal Nat.thy
"[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) \
-\ |] ==> nat_case(n,a,b) : C(n)";
+\ |] ==> nat_case(a,b,n) : C(n)";
by (rtac (major RS nat_induct) 1);
by (REPEAT (resolve_tac [nat_case_0 RS ssubst,
nat_case_succ RS ssubst] 1
@@ -145,13 +145,6 @@
by (assume_tac 1);
val nat_case_type = result();
-val prems = goalw Nat.thy [nat_case_def]
- "[| n=n'; a=a'; !!m z. b(m)=b'(m) \
-\ |] ==> nat_case(n,a,b)=nat_case(n',a',b')";
-by (REPEAT (resolve_tac [the_cong,disj_cong,ex_cong] 1
- ORELSE EVERY1 (map rtac ((prems RL [ssubst]) @ [iff_refl]))));
-val nat_case_cong = result();
-
(** nat_rec -- used to define eclose and transrec, then obsolete **)
@@ -165,11 +158,10 @@
val [prem] = goal Nat.thy
"m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
val nat_rec_ss = ZF_ss
- addcongs (mk_typed_congs Nat.thy [("b", "[i,i]=>i")])
- addrews [prem, nat_case_succ, nat_succI, Memrel_iff,
- vimage_singleton_iff];
+ addsimps [prem, nat_case_succ, nat_succI, Memrel_iff,
+ vimage_singleton_iff];
by (rtac nat_rec_trans 1);
-by (SIMP_TAC nat_rec_ss 1);
+by (simp_tac nat_rec_ss 1);
val nat_rec_succ = result();
(** The union of two natural numbers is a natural number -- their maximum **)
--- a/src/ZF/Nat.thy Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Nat.thy Fri Sep 17 16:16:38 1993 +0200
@@ -9,7 +9,7 @@
Nat = Ord + Bool +
consts
nat :: "i"
- nat_case :: "[i, i, i=>i]=>i"
+ nat_case :: "[i, i=>i, i]=>i"
nat_rec :: "[i, i, [i,i]=>i]=>i"
rules
@@ -17,10 +17,10 @@
nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
nat_case_def
- "nat_case(k,a,b) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
+ "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
nat_rec_def
"nat_rec(k,a,b) == \
-\ wfrec(Memrel(nat), k, %n f. nat_case(n, a, %m. b(m, f`m)))"
+\ wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
end
--- a/src/ZF/Ord.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Ord.ML Fri Sep 17 16:16:38 1993 +0200
@@ -318,7 +318,7 @@
goal Ord.thy
"!!i j. [| Ord(i); Ord(j) |] ==> i<=succ(j) <-> i<=j | i=succ(j)";
-by (ASM_SIMP_TAC (ZF_ss addrews [member_succ_iff RS iff_sym, Ord_succ]) 1);
+by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1);
by (fast_tac ZF_cs 1);
val subset_succ_iff = result();
@@ -356,17 +356,17 @@
goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Un j : k";
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
-by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
+by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
by (rtac (Un_commute RS ssubst) 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
+by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
val Ord_member_UnI = result();
goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Int j : k";
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
-by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
+by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
by (rtac (Int_commute RS ssubst) 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
+by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
val Ord_member_IntI = result();
--- a/src/ZF/Pair.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Pair.ML Fri Sep 17 16:16:38 1993 +0200
@@ -15,7 +15,7 @@
val Pair_iff = prove_goalw ZF.thy [Pair_def]
"<a,b> = <c,d> <-> a=c & b=d"
- (fn _=> [ (SIMP_TAC (FOL_ss addrews [doubleton_iff]) 1),
+ (fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_iff]) 1),
(fast_tac FOL_cs 1) ]);
val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
@@ -89,7 +89,7 @@
val Sigma_cong = prove_goalw ZF.thy [Sigma_def]
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
\ Sigma(A,B) = Sigma(A',B')"
- (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
+ (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1) ]);
val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"
(fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
@@ -114,13 +114,6 @@
(etac ssubst 1),
(REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
-(*This congruence rule uses NO typing information...*)
-val split_cong = prove_goalw ZF.thy [split_def]
- "[| p=p'; !!x y.c(x,y) = c'(x,y) |] ==> \
-\ split(%x y.c(x,y), p) = split(%x y.c'(x,y), p')"
- (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
-
-
(*** conversions for fst and snd ***)
val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
--- a/src/ZF/Perm.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Perm.ML Fri Sep 17 16:16:38 1993 +0200
@@ -52,6 +52,7 @@
(* f: bij(A,B) ==> f: A->B *)
val bij_is_fun = standard (bij_is_inj RS inj_is_fun);
+
(** Identity function **)
val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";
@@ -76,7 +77,7 @@
goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)";
by (REPEAT (ares_tac [CollectI,lam_type] 1));
-by (SIMP_TAC ZF_ss 1);
+by (simp_tac ZF_ss 1);
val id_inj = result();
goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
@@ -262,7 +263,7 @@
"!!f g. [| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)";
by (safe_tac comp_cs);
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
-by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
+by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
val comp_mem_injD1 = result();
goalw Perm.thy [inj_def,surj_def]
@@ -271,9 +272,10 @@
by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
by (REPEAT (assume_tac 1));
-by (safe_tac (comp_cs addSIs ZF_congs));
+by (safe_tac comp_cs);
+by (res_inst_tac [("t", "op `(g)")] subst_context 1);
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
-by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
+by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
val comp_mem_injD2 = result();
goalw Perm.thy [surj_def]
@@ -427,7 +429,9 @@
by (etac fun_extend 1);
by (REPEAT (ares_tac [ballI] 1));
by (REPEAT_FIRST (eresolve_tac [consE,ssubst]));
-(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x makes ASM_SIMP_TAC loop!*)
-by (ALLGOALS (SIMP_TAC (ZF_ss addrews [fun_extend_apply2,fun_extend_apply1])));
+(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x would make asm_simp_tac loop
+ using ZF_ss! But FOL_ss ignores the assumption...*)
+by (ALLGOALS (asm_simp_tac
+ (FOL_ss addsimps [fun_extend_apply2,fun_extend_apply1])));
by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type])));
val inj_extend = result();
--- a/src/ZF/QPair.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/QPair.ML Fri Sep 17 16:16:38 1993 +0200
@@ -74,7 +74,7 @@
val QSigma_cong = prove_goalw QPair.thy [QSigma_def]
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
\ QSigma(A,B) = QSigma(A',B')"
- (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
+ (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]);
val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0"
(fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
@@ -98,12 +98,6 @@
(etac ssubst 1),
(REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]);
-(*This congruence rule uses NO typing information...*)
-val qsplit_cong = prove_goalw QPair.thy [qsplit_def]
- "[| p=p'; !!x y.c(x,y) = c'(x,y) |] ==> \
-\ qsplit(%x y.c(x,y), p) = qsplit(%x y.c'(x,y), p')"
- (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
-
val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
@@ -243,7 +237,7 @@
val qsum_subset_iff = result();
goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D";
-by (SIMP_TAC (ZF_ss addrews [extension,qsum_subset_iff]) 1);
+by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1);
by (fast_tac ZF_cs 1);
val qsum_equal_iff = result();
@@ -259,12 +253,6 @@
by (rtac cond_1 1);
val qcase_QInr = result();
-val prems = goalw QPair.thy [qcase_def]
- "[| u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) |] ==> \
-\ qcase(c,d,u)=qcase(c',d',u')";
-by (REPEAT (resolve_tac ([refl,qsplit_cong,cond_cong] @ prems) 1));
-val qcase_cong = result();
-
val major::prems = goal QPair.thy
"[| u: A <+> B; \
\ !!x. x: A ==> c(x): C(QInl(x)); \
@@ -272,7 +260,7 @@
\ |] ==> qcase(c,d,u) : C(u)";
by (rtac (major RS qsumE) 1);
by (ALLGOALS (etac ssubst));
-by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
(prems@[qcase_QInl,qcase_QInr]))));
val qcase_type = result();
--- a/src/ZF/QUniv.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/QUniv.ML Fri Sep 17 16:16:38 1993 +0200
@@ -205,7 +205,7 @@
goalw QUniv.thy [QPair_def,sum_def]
"<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))";
-by (SIMP_TAC (ZF_ss addrews [Int_Un_distrib, product_Int_quniv_eq]) 1);
+by (simp_tac (ZF_ss addsimps [Int_Un_distrib, product_Int_quniv_eq]) 1);
val QPair_Int_quniv_eq = result();
(**** "Take-lemma" rules for proving c: quniv(A) ****)
--- a/src/ZF/ROOT.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/ROOT.ML Fri Sep 17 16:16:38 1993 +0200
@@ -1,4 +1,5 @@
(* Title: ZF/ROOT
+ ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
--- a/src/ZF/Sum.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Sum.ML Fri Sep 17 16:16:38 1993 +0200
@@ -83,7 +83,7 @@
val sum_subset_iff = result();
goal Sum.thy "A+B = C+D <-> A=C & B=D";
-by (SIMP_TAC (ZF_ss addrews [extension,sum_subset_iff]) 1);
+by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1);
by (fast_tac ZF_cs 1);
val sum_equal_iff = result();
@@ -99,12 +99,6 @@
by (rtac cond_1 1);
val case_Inr = result();
-val prems = goalw Sum.thy [case_def]
- "[| u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) |] ==> \
-\ case(c,d,u)=case(c',d',u')";
-by (REPEAT (resolve_tac ([refl,split_cong,cond_cong] @ prems) 1));
-val case_cong = result();
-
val major::prems = goal Sum.thy
"[| u: A+B; \
\ !!x. x: A ==> c(x): C(Inl(x)); \
@@ -112,7 +106,7 @@
\ |] ==> case(c,d,u) : C(u)";
by (rtac (major RS sumE) 1);
by (ALLGOALS (etac ssubst));
-by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
(prems@[case_Inl,case_Inr]))));
val case_type = result();
--- a/src/ZF/Univ.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/Univ.ML Fri Sep 17 16:16:38 1993 +0200
@@ -11,7 +11,7 @@
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
-by (SIMP_TAC ZF_ss 1);
+by (simp_tac ZF_ss 1);
val Vfrom = result();
(** Monotonicity **)
@@ -122,9 +122,8 @@
goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
by (rtac (Vfrom RS trans) 1);
-brs ([refl] RL ZF_congs) 1;
-by (rtac equalityI 1);
-by (rtac (succI1 RS RepFunI RS Union_upper) 2);
+by (rtac (succI1 RS RepFunI RS Union_upper RSN
+ (2, equalityI RS subst_context)) 1);
by (rtac UN_least 1);
by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
by (etac member_succD 1);
@@ -473,16 +472,16 @@
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans]));
val rank_ss = ZF_ss
- addrews [split, case_Inl, case_Inr, Vset_rankI]
- addrews rank_trans_rls;
+ addsimps [case_Inl, case_Inr, Vset_rankI]
+ addsimps rank_trans_rls;
(** Recursion over Vset levels! **)
(*NOT SUITABLE FOR REWRITING: recursive!*)
goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
by (rtac (transrec RS ssubst) 1);
-by (SIMP_TAC (wf_ss addrews [Ord_rank, Ord_succ, Vset_D RS beta,
- VsetI RS beta]) 1);
+by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, Vset_D RS beta,
+ VsetI RS beta]) 1);
val Vrec = result();
(*This form avoids giant explosions in proofs. NOTE USE OF == *)
@@ -493,13 +492,6 @@
by (rtac Vrec 1);
val def_Vrec = result();
-val prems = goalw Univ.thy [Vrec_def]
- "[| a=a'; !!x u. H(x,u)=H'(x,u) |] ==> Vrec(a,H)=Vrec(a',H')";
-val Vrec_ss = ZF_ss addcongs ([transrec_cong] @ mk_congs Univ.thy ["rank"])
- addrews (prems RL [sym]);
-by (SIMP_TAC Vrec_ss 1);
-val Vrec_cong = result();
-
(*** univ(A) ***)
--- a/src/ZF/WF.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/WF.ML Fri Sep 17 16:16:38 1993 +0200
@@ -19,10 +19,6 @@
open WF;
-val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")];
-
-val wf_ss = ZF_ss addcongs [H_cong];
-
(*** Well-founded relations ***)
@@ -138,13 +134,13 @@
(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
spec RS mp instantiates induction hypotheses*)
fun indhyp_tac hyps =
- ares_tac (TrueI::hyps) ORELSE'
+ resolve_tac (TrueI::refl::hyps) ORELSE'
(cut_facts_tac hyps THEN'
DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
eresolve_tac [underD, transD, spec RS mp]));
-(*** NOTE! some simplifications need a different auto_tac!! ***)
-val wf_super_ss = wf_ss setauto indhyp_tac;
+(*** NOTE! some simplifications need a different solver!! ***)
+val wf_super_ss = ZF_ss setsolver indhyp_tac;
val prems = goalw WF.thy [is_recfun_def]
"[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \
@@ -153,7 +149,7 @@
by (wf_ind_tac "x" prems 1);
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
by (rewtac restrict_def);
-by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1);
+by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
val is_recfun_equal_lemma = result();
val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
@@ -165,7 +161,7 @@
by (rtac (consI1 RS restrict_type RS fun_extension) 1);
by (etac is_recfun_type 1);
by (ALLGOALS
- (ASM_SIMP_TAC (wf_super_ss addrews
+ (asm_simp_tac (wf_super_ss addsimps
[ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
val is_recfun_cut = result();
@@ -195,13 +191,13 @@
by (REPEAT (assume_tac 2));
by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
(*Applying the substitution: must keep the quantified assumption!!*)
-by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1));
+by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
by (fold_tac [is_recfun_def]);
-by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1);
+by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
by (rtac is_recfun_type 1);
by (ALLGOALS
- (ASM_SIMP_TAC
- (wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut])));
+ (asm_simp_tac
+ (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
val unfold_the_recfun = result();
@@ -214,13 +210,12 @@
val the_recfun_cut = result();
(*NOT SUITABLE FOR REWRITING since it is recursive!*)
-val prems = goalw WF.thy [wftrec_def]
- "[| wf(r); trans(r) |] ==> \
-\ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
+goalw WF.thy [wftrec_def]
+ "!!r. [| wf(r); trans(r) |] ==> \
+\ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
-by (ALLGOALS (ASM_SIMP_TAC
- (wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym,
- the_recfun_cut]))));
+by (ALLGOALS (asm_simp_tac
+ (ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
val wftrec = result();
(** Removal of the premise trans(r) **)
@@ -230,8 +225,7 @@
"wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
by (rtac trans_trancl 1);
-by (rtac (refl RS H_cong) 1);
-by (rtac (vimage_pair_mono RS restrict_lam_eq) 1);
+by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
by (etac r_into_trancl 1);
by (rtac subset_refl 1);
val wfrec = result();
@@ -253,10 +247,3 @@
by (REPEAT (ares_tac (prems@[lam_type]) 1
ORELSE eresolve_tac [spec RS mp, underD] 1));
val wfrec_type = result();
-
-val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def]
- "[| r=r'; !!x u. H(x,u)=H'(x,u); a=a' |] \
-\ ==> wfrec(r,a,H)=wfrec(r',a',H')";
-by (EVERY1 (map rtac (prems RL [subst])));
-by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1);
-val wfrec_cong = result();
--- a/src/ZF/ZF.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/ZF.ML Fri Sep 17 16:16:38 1993 +0200
@@ -13,9 +13,8 @@
val ballE : thm
val ballI : thm
val ball_cong : thm
- val ball_rew : thm
+ val ball_simp : thm
val ball_tac : int -> tactic
- val basic_ZF_congs : thm list
val bexCI : thm
val bexE : thm
val bexI : thm
@@ -45,7 +44,6 @@
val lemmas_cs : claset
val PowD : thm
val PowI : thm
- val prove_cong_tac : thm list -> int -> tactic
val RepFunE : thm
val RepFunI : thm
val RepFun_eqI : thm
@@ -75,14 +73,6 @@
structure ZF_Lemmas : ZF_LEMMAS =
struct
-val basic_ZF_congs = mk_congs ZF.thy
- ["op `", "op ``", "op Int", "op Un", "op -", "op <=", "op :",
- "Pow", "Union", "Inter", "fst", "snd", "succ", "Pair", "Upair", "cons",
- "domain", "range", "restrict"];
-
-fun prove_cong_tac prems i =
- REPEAT (ares_tac (prems@[refl]@FOL_congs@basic_ZF_congs) i);
-
(*** Bounded universal quantifier ***)
val ballI = prove_goalw ZF.thy [Ball_def]
@@ -118,14 +108,13 @@
val ball_tac = dtac bspec THEN' assume_tac;
(*Trival rewrite rule; (ALL x:A.P)<->P holds only if A is nonempty!*)
-val ball_rew = prove_goal ZF.thy "(ALL x:A. True) <-> True"
- (fn prems=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
+val ball_simp = prove_goal ZF.thy "(ALL x:A. True) <-> True"
+ (fn _=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
(*Congruence rule for rewriting*)
val ball_cong = prove_goalw ZF.thy [Ball_def]
- "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) \
-\ |] ==> (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
- (fn prems=> [ (prove_cong_tac prems 1) ]);
+ "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
+ (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
(*** Bounded existential quantifier ***)
@@ -151,8 +140,8 @@
val bex_cong = prove_goalw ZF.thy [Bex_def]
"[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) \
-\ |] ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
- (fn prems=> [ (prove_cong_tac prems 1) ]);
+\ |] ==> Bex(A,P) <-> Bex(A',P')"
+ (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
(*** Rules for subsets ***)
@@ -265,7 +254,7 @@
val Replace_cong = prove_goal ZF.thy
"[| A=B; !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
-\ {y. x:A, P(x,y)} = {y. x:B, Q(x,y)}"
+\ Replace(A,P) = Replace(B,Q)"
(fn prems=>
let val substprems = prems RL [subst, ssubst]
and iffprems = prems RL [iffD1,iffD2]
@@ -275,7 +264,6 @@
ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]
end);
-
(*** Rules for RepFun ***)
val RepFunI = prove_goalw ZF.thy [RepFun_def]
@@ -296,9 +284,8 @@
(REPEAT (ares_tac prems 1)) ]);
val RepFun_cong = prove_goalw ZF.thy [RepFun_def]
- "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> \
-\ {f(x). x:A} = {g(x). x:B}"
- (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
+ "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
+ (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
(*** Rules for Collect -- forming a subset by separation ***)
@@ -332,9 +319,8 @@
(assume_tac 1) ]);
val Collect_cong = prove_goalw ZF.thy [Collect_def]
- "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> \
-\ {x:A. P(x)} = {x:B. Q(x)}"
- (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
+ "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
+ (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
(*** Rules for Unions ***)
--- a/src/ZF/arith.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/arith.ML Fri Sep 17 16:16:38 1993 +0200
@@ -29,10 +29,9 @@
goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
val rec_ss = ZF_ss
- addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")])
- addrews [nat_case_succ, nat_succI];
+ addsimps [nat_case_succ, nat_succI];
by (rtac rec_trans 1);
-by (SIMP_TAC rec_ss 1);
+by (simp_tac rec_ss 1);
val rec_succ = result();
val major::prems = goal Arith.thy
@@ -42,20 +41,12 @@
\ |] ==> rec(n,a,b) : C(n)";
by (rtac (major RS nat_induct) 1);
by (ALLGOALS
- (ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ]))));
+ (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
val rec_type = result();
-val prems = goalw Arith.thy [rec_def]
- "[| n=n'; a=a'; !!m z. b(m,z)=b'(m,z) \
-\ |] ==> rec(n,a,b)=rec(n',a',b')";
-by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong]
- addrews (prems RL [sym])) 1);
-val rec_cong = result();
-
val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
-val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong]
- addrews ([rec_0,rec_succ] @ nat_typechecks);
+val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
(** Addition **)
@@ -101,16 +92,16 @@
"n:nat ==> 0 #- n = 0"
(fn [prem]=>
[ (rtac (prem RS nat_induct) 1),
- (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]);
+ (ALLGOALS (asm_simp_tac nat_ss)) ]);
(*Must simplify BEFORE the induction!! (Else we get a critical pair)
succ(m) #- succ(n) rewrites to pred(succ(m) #- n) *)
val diff_succ_succ = prove_goalw Arith.thy [diff_def]
"[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n"
(fn prems=>
- [ (ASM_SIMP_TAC (nat_ss addrews prems) 1),
+ [ (asm_simp_tac (nat_ss addsimps prems) 1),
(nat_ind_tac "n" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
val prems = goal Arith.thy
"[| m:nat; n:nat |] ==> m #- n : succ(m)";
@@ -119,8 +110,8 @@
by (resolve_tac prems 1);
by (etac succE 3);
by (ALLGOALS
- (ASM_SIMP_TAC
- (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
+ (asm_simp_tac
+ (nat_ss addsimps (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
val diff_leq = result();
(*** Simplification over add, mult, diff ***)
@@ -130,10 +121,7 @@
mult_0, mult_succ,
diff_0, diff_0_eq_0, diff_succ_succ];
-val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"];
-
-val arith_ss = nat_ss addcongs arith_congs
- addrews (arith_rews@arith_typechecks);
+val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
(*** Addition ***)
@@ -142,7 +130,7 @@
"m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*The following two lemmas are used for add_commute and sometimes
elsewhere, since they are safe for rewriting.*)
@@ -150,13 +138,13 @@
"m:nat ==> m #+ 0 = m"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
val add_succ_right = prove_goal Arith.thy
"m:nat ==> m #+ succ(n) = succ(m #+ n)"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*Commutative law for addition*)
val add_commute = prove_goal Arith.thy
@@ -164,15 +152,15 @@
(fn prems=>
[ (nat_ind_tac "n" prems 1),
(ALLGOALS
- (ASM_SIMP_TAC
- (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]);
+ (asm_simp_tac
+ (arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]);
(*Cancellation law on the left*)
val [knat,eqn] = goal Arith.thy
"[| k:nat; k #+ m = k #+ n |] ==> m=n";
by (rtac (eqn RS rev_mp) 1);
by (nat_ind_tac "k" [knat] 1);
-by (ALLGOALS (SIMP_TAC arith_ss));
+by (ALLGOALS (simp_tac arith_ss));
by (fast_tac ZF_cs 1);
val add_left_cancel = result();
@@ -183,39 +171,40 @@
"m:nat ==> m #* 0 = 0"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*right successor law for multiplication*)
val mult_succ_right = prove_goal Arith.thy
- "[| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
- (fn prems=>
- [ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))),
+ "!!m n. [| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
+ (fn _=>
+ [ (nat_ind_tac "m" [] 1),
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))),
(*The final goal requires the commutative law for addition*)
- (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1)) ]);
+ (rtac (add_commute RS subst_context) 1),
+ (REPEAT (assume_tac 1)) ]);
(*Commutative law for multiplication*)
val mult_commute = prove_goal Arith.thy
"[| m:nat; n:nat |] ==> m #* n = n #* m"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC
- (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]);
+ (ALLGOALS (asm_simp_tac
+ (arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]);
(*addition distributes over multiplication*)
val add_mult_distrib = prove_goal Arith.thy
"[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps ([add_assoc RS sym]@prems)))) ]);
(*Distributive law on the left; requires an extra typing premise*)
val add_mult_distrib_left = prove_goal Arith.thy
"[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
(fn prems=>
let val mult_commute' = read_instantiate [("m","k")] mult_commute
- val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems)
- in [ (SIMP_TAC ss 1) ]
+ val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems)
+ in [ (simp_tac ss 1) ]
end);
(*Associative law for multiplication*)
@@ -223,7 +212,7 @@
"[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps (prems@[add_mult_distrib])))) ]);
(*** Difference ***)
@@ -232,7 +221,7 @@
"m:nat ==> m #- m = 0"
(fn prems=>
[ (nat_ind_tac "m" prems 1),
- (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
+ (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
val notless::prems = goal Arith.thy
@@ -241,8 +230,8 @@
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (resolve_tac prems 1);
by (resolve_tac prems 1);
-by (ALLGOALS (ASM_SIMP_TAC
- (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
+by (ALLGOALS (asm_simp_tac
+ (arith_ss addsimps (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
naturals_are_ordinals]))));
val add_diff_inverse = result();
@@ -251,29 +240,24 @@
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 (arith_ss addrews [mnat])));
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
val diff_add_inverse = result();
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 (arith_ss addrews [mnat])));
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
val diff_add_0 = result();
(*** Remainder ***)
(*In ordinary notation: if 0<n and n<=m then m-n < m *)
-val prems = goal Arith.thy
- "[| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m";
-by (cut_facts_tac prems 1);
+goal Arith.thy "!!m n. [| 0:n; ~ m:n; m:nat; n:nat |] ==> m #- n : m";
by (etac rev_mp 1);
by (etac rev_mp 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-by (ALLGOALS (ASM_SIMP_TAC
- (nat_ss addrews (prems@[diff_leq,diff_succ_succ]))));
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_leq,diff_succ_succ])));
val div_termination = result();
val div_rls =
@@ -286,17 +270,17 @@
by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
val mod_type = result();
-val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination];
+val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
val prems = goal Arith.thy "[| 0:n; m:n; m:nat; n:nat |] ==> m mod n = m";
by (rtac (mod_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val mod_less = result();
val prems = goal Arith.thy
"[| 0:n; ~m:n; m:nat; n:nat |] ==> m mod n = (m#-n) mod n";
by (rtac (mod_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val mod_geq = result();
(*** Quotient ***)
@@ -310,13 +294,13 @@
val prems = goal Arith.thy
"[| 0:n; m:n; m:nat; n:nat |] ==> m div n = 0";
by (rtac (div_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val div_less = result();
val prems = goal Arith.thy
"[| 0:n; ~m:n; m:nat; n:nat |] ==> m div n = succ((m#-n) div n)";
by (rtac (div_def RS def_transrec RS trans) 1);
-by (SIMP_TAC (div_ss addrews prems) 1);
+by (simp_tac (div_ss addsimps prems) 1);
val div_geq = result();
(*Main Result.*)
@@ -326,8 +310,8 @@
by (resolve_tac prems 1);
by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
by (ALLGOALS
- (ASM_SIMP_TAC
- (arith_ss addrews ([mod_type,div_type] @ prems @
+ (asm_simp_tac
+ (arith_ss addsimps ([mod_type,div_type] @ prems @
[mod_less,mod_geq, div_less, div_geq,
add_assoc, add_diff_inverse, div_termination]))));
val mod_div_equality = result();
@@ -338,7 +322,7 @@
val [mnat,nnat] = goal Arith.thy
"[| m:nat; n:nat |] ==> ~ (m #+ n) : n";
by (rtac (mnat RS nat_induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl])));
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
by (rtac notI 1);
by (etac notE 1);
by (etac (succI1 RS Ord_trans) 1);
--- a/src/ZF/arith.thy Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/arith.thy Fri Sep 17 16:16:38 1993 +0200
@@ -16,7 +16,7 @@
"#-" :: "[i,i]=>i" (infixl 65)
rules
- rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(n, a, %m. b(m, f`m)))"
+ rec_def "rec(k,a,b) == transrec(k, %n f. nat_case(a, %m. b(m, f`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))"
--- a/src/ZF/bool.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/bool.ML Fri Sep 17 16:16:38 1993 +0200
@@ -53,9 +53,6 @@
by (resolve_tac prems 1);
val cond_type = result();
-val [cond_cong] = mk_congs Bool.thy ["cond"];
-val bool_congs = mk_congs Bool.thy ["cond","not","op and","op or","op xor"];
-
val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
by (rewtac rew);
by (rtac cond_1 1);
--- a/src/ZF/constructor.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/constructor.ML Fri Sep 17 16:16:38 1993 +0200
@@ -40,7 +40,6 @@
val free_iffs : thm list (*freeness rewrite rules*)
val free_SEs : thm list (*freeness destruct rules*)
val mk_free : string -> thm (*makes freeness theorems*)
- val congs : thm list (*congruence rules for simplifier*)
end;
@@ -194,7 +193,6 @@
val case_eqns = map prove_case_equation
(flat con_ty_lists ~~ big_case_args ~~ tl con_defs);
-val congs = mk_congs con_thy (flat (map #1 (const_decs @ ext_constants ext)));
end;
--- a/src/ZF/epsilon.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/epsilon.ML Fri Sep 17 16:16:38 1993 +0200
@@ -64,8 +64,8 @@
"!!X A n. [| Transset(X); A<=X; n: nat |] ==> \
\ nat_rec(n, A, %m r. Union(r)) <= X";
by (etac nat_induct 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_0]) 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [nat_rec_succ]) 1);
+by (asm_simp_tac (ZF_ss addsimps [nat_rec_0]) 1);
+by (asm_simp_tac (ZF_ss addsimps [nat_rec_succ]) 1);
by (fast_tac ZF_cs 1);
val eclose_least_lemma = result();
@@ -126,8 +126,8 @@
by (rtac (kmemj RS eclose_induct) 1);
by (rtac wfrec_ssubst 1);
by (rtac wfrec_ssubst 1);
-by (ASM_SIMP_TAC (wf_ss addrews [under_Memrel_eclose,
- jmemi RSN (2,mem_eclose_sing_trans)]) 1);
+by (asm_simp_tac (ZF_ss addsimps [under_Memrel_eclose,
+ jmemi RSN (2,mem_eclose_sing_trans)]) 1);
val wfrec_eclose_eq = result();
val [prem] = goal Epsilon.thy
@@ -139,8 +139,8 @@
goalw Epsilon.thy [transrec_def]
"transrec(a,H) = H(a, lam x:a. transrec(x,H))";
by (rtac wfrec_ssubst 1);
-by (SIMP_TAC (wf_ss addrews [wfrec_eclose_eq2,
- arg_in_eclose_sing, under_Memrel_eclose]) 1);
+by (simp_tac (ZF_ss addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
+ under_Memrel_eclose]) 1);
val transrec = result();
(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
@@ -173,23 +173,12 @@
by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
val Ord_transrec_type = result();
-(*Congruence*)
-val prems = goalw Epsilon.thy [transrec_def,Memrel_def]
- "[| a=a'; !!x u. H(x,u)=H'(x,u) |] ==> transrec(a,H)=transrec(a',H')";
-val transrec_ss =
- ZF_ss addcongs ([wfrec_cong] @ mk_congs Epsilon.thy ["eclose"])
- addrews (prems RL [sym]);
-by (SIMP_TAC transrec_ss 1);
-val transrec_cong = result();
-
(*** Rank ***)
-val ord_ss = ZF_ss addcongs (mk_congs Ord.thy ["Ord"]);
-
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
by (rtac (rank_def RS def_transrec RS ssubst) 1);
-by (SIMP_TAC ZF_ss 1);
+by (simp_tac ZF_ss 1);
val rank = result();
goal Epsilon.thy "Ord(rank(a))";
@@ -203,7 +192,7 @@
val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
by (rtac (major RS trans_induct) 1);
by (rtac (rank RS ssubst) 1);
-by (ASM_SIMP_TAC (ord_ss addrews [Ord_equality]) 1);
+by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
val rank_of_Ord = result();
val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
--- a/src/ZF/fin.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/fin.ML Fri Sep 17 16:16:38 1993 +0200
@@ -55,19 +55,19 @@
val Fin_induct = result();
(** Simplification for Fin **)
-val Fin_ss = arith_ss addcongs mk_congs Fin.thy ["Fin"] addrews Fin.intrs;
+val Fin_ss = arith_ss addsimps Fin.intrs;
(*The union of two finite sets is fin*)
val major::prems = goal Fin.thy
"[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)";
by (rtac (major RS Fin_induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews (prems@[Un_0, Un_cons]))));
+by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
val Fin_UnI = result();
(*The union of a set of finite sets is fin*)
val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
by (rtac (major RS Fin_induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews [Union_0, Union_cons, Fin_UnI])));
+by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
val Fin_UnionI = result();
(*Every subset of a finite set is fin*)
@@ -76,10 +76,10 @@
etac (spec RS mp),
rtac subs]);
by (rtac (fin RS Fin_induct) 1);
-by (SIMP_TAC (Fin_ss addrews [subset_empty_iff]) 1);
+by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
-by (ALLGOALS (ASM_SIMP_TAC Fin_ss));
+by (ALLGOALS (asm_simp_tac Fin_ss));
val Fin_subset = result();
val major::prems = goal Fin.thy
@@ -89,7 +89,7 @@
\ |] ==> c<=b --> P(b-c)";
by (rtac (major RS Fin_induct) 1);
by (rtac (Diff_cons RS ssubst) 2);
-by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews (prems@[Diff_0, cons_subset_iff,
+by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff,
Diff_subset RS Fin_subset]))));
val Fin_0_induct_lemma = result();
--- a/src/ZF/func.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/func.ML Fri Sep 17 16:16:38 1993 +0200
@@ -37,7 +37,7 @@
val prems = goalw ZF.thy [Pi_def]
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> Pi(A,B) = Pi(A',B')";
-by (prove_cong_tac (prems@[Collect_cong,Sigma_cong,ball_cong]) 1);
+by (simp_tac (FOL_ss addsimps prems addcongs [Sigma_cong]) 1);
val Pi_cong = result();
(*Weaking one function type to another*)
@@ -84,8 +84,7 @@
by (rtac refl 1);
val memberPiE = result();
-(*Conclusion is flexible -- use res_inst_tac or else RS with a theorem
- of the form f:A->B *)
+(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> f`a : B(a)";
by (rtac (fun_unique_Pair RS ex1E) 1);
by (REPEAT (assume_tac 1));
@@ -94,6 +93,11 @@
by (REPEAT (assume_tac 1));
val apply_type = result();
+(*This version is acceptable to the simplifier*)
+goal ZF.thy "!!f. [| f: A->B; a:A |] ==> f`a : B";
+by (REPEAT (ares_tac [apply_type] 1));
+val apply_funtype = result();
+
goal ZF.thy "!!f. [| f: Pi(A,B); a:A |] ==> <a,f`a>: f";
by (rtac (fun_unique_Pair RS ex1E) 1);
by (resolve_tac [apply_equality RS ssubst] 3);
@@ -169,11 +173,8 @@
(*congruence rule for lambda abstraction*)
val prems = goalw ZF.thy [lam_def]
- "[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> \
-\ (lam x:A.b(x)) = (lam x:A'.b'(x))";
-by (rtac RepFun_cong 1);
-by (res_inst_tac [("t","Pair")] subst_context2 2);
-by (REPEAT (ares_tac (prems@[refl]) 1));
+ "[| A=A'; !!x. x:A' ==> b(x)=b'(x) |] ==> Lambda(A,b) = Lambda(A',b')";
+by (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1);
val lam_cong = result();
val [major] = goal ZF.thy
@@ -259,7 +260,7 @@
val [prem] = goalw ZF.thy [restrict_def]
"A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
by (rtac (refl RS lam_cong) 1);
-be (prem RS subsetD RS beta) 1; (*easier than calling SIMP_TAC*)
+be (prem RS subsetD RS beta) 1; (*easier than calling simp_tac*)
val restrict_lam_eq = result();
--- a/src/ZF/ind-syntax.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/ind-syntax.ML Fri Sep 17 16:16:38 1993 +0200
@@ -37,7 +37,6 @@
flatten_term sign (Logic.mk_equals (lhs,rhs)))
end;
-(*export to Pure/sign? Used in Provers/simp.ML...*)
fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
(*export to Pure/library? *)
--- a/src/ZF/ind_syntax.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/ind_syntax.ML Fri Sep 17 16:16:38 1993 +0200
@@ -37,7 +37,6 @@
flatten_term sign (Logic.mk_equals (lhs,rhs)))
end;
-(*export to Pure/sign? Used in Provers/simp.ML...*)
fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
(*export to Pure/library? *)
--- a/src/ZF/list.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/list.ML Fri Sep 17 16:16:38 1993 +0200
@@ -62,7 +62,7 @@
\ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(<x,y>) \
\ |] ==> list_case(l,c,h) : C(l)";
by (rtac (major RS list_induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
([list_case_0,list_case_Pair]@prems))));
val list_case_type = result();
****)
@@ -71,10 +71,10 @@
(** For recursion **)
goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val rank_Cons1 = result();
goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
-by (SIMP_TAC rank_ss 1);
+by (simp_tac rank_ss 1);
val rank_Cons2 = result();
--- a/src/ZF/listfn.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/listfn.ML Fri Sep 17 16:16:38 1993 +0200
@@ -11,19 +11,14 @@
(** list_rec -- by Vset recursion **)
-(*Used to verify list_rec*)
-val list_rec_ss = ZF_ss
- addcongs (mk_typed_congs ListFn.thy [("h", "[i,i,i]=>i")])
- addrews List.case_eqns;
-
goal ListFn.thy "list_rec(Nil,c,h) = c";
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
-by (SIMP_TAC list_rec_ss 1);
+by (simp_tac (ZF_ss addsimps List.case_eqns) 1);
val list_rec_Nil = result();
goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
by (rtac (list_rec_def RS def_Vrec RS trans) 1);
-by (SIMP_TAC (list_rec_ss addrews [Vset_rankI, rank_Cons2]) 1);
+by (simp_tac (ZF_ss addsimps (List.case_eqns @ [Vset_rankI, rank_Cons2])) 1);
val list_rec_Cons = result();
(*Type checking -- proved by induction, as usual*)
@@ -33,8 +28,8 @@
\ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \
\ |] ==> list_rec(l,c,h) : C(l)";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC
- (ZF_ss addrews (prems@[list_rec_Nil,list_rec_Cons]))));
+by (ALLGOALS (asm_simp_tac
+ (ZF_ss addsimps (prems@[list_rec_Nil,list_rec_Cons]))));
val list_rec_type = result();
(** Versions for use with definitions **)
@@ -122,47 +117,42 @@
map_type, map_type2, app_type, length_type, rev_type, flat_type,
list_add_type];
-val list_congs =
- List.congs @
- mk_congs ListFn.thy
- ["list_rec","map","op @","length","rev","flat","list_add"];
-
val list_ss = arith_ss
- addcongs list_congs
- addrews List.case_eqns
- addrews list_typechecks
- addrews [list_rec_Nil, list_rec_Cons,
+ addsimps List.case_eqns
+ addsimps [list_rec_Nil, list_rec_Cons,
map_Nil, map_Cons,
app_Nil, app_Cons,
length_Nil, length_Cons,
rev_Nil, rev_Cons,
flat_Nil, flat_Cons,
- list_add_Nil, list_add_Cons];
+ list_add_Nil, list_add_Cons]
+ setsolver (type_auto_tac list_typechecks);
+(*Could also rewrite using the list_typechecks...*)
(*** theorems about map ***)
val prems = goal ListFn.thy
"l: list(A) ==> map(%u.u, l) = l";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val map_ident = result();
val prems = goal ListFn.thy
"l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val map_compose = result();
val prems = goal ListFn.thy
"xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val map_app_distrib = result();
val prems = goal ListFn.thy
"ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
by (list_ind_tac "ls" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
val map_flat = result();
val prems = goal ListFn.thy
@@ -170,9 +160,7 @@
\ list_rec(map(h,l), c, d) = \
\ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS
- (ASM_SIMP_TAC
- (list_ss addcongs (mk_typed_congs ListFn.thy [("d", "[i,i,i]=>i")]))));
+by (ALLGOALS (asm_simp_tac list_ss));
val list_rec_map = result();
(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
@@ -183,7 +171,7 @@
val prems = goal ListFn.thy
"l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val map_list_Collect = result();
(*** theorems about length ***)
@@ -191,13 +179,13 @@
val prems = goal ListFn.thy
"xs: list(A) ==> length(map(h,xs)) = length(xs)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val length_map = result();
val prems = goal ListFn.thy
"xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val length_app = result();
(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m
@@ -207,60 +195,59 @@
val prems = goal ListFn.thy
"xs: list(A) ==> length(rev(xs)) = length(xs)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app, add_commute_succ])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app, add_commute_succ])));
val length_rev = result();
val prems = goal ListFn.thy
"ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
by (list_ind_tac "ls" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [length_app])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app])));
val length_flat = result();
(*** theorems about app ***)
val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs";
by (rtac (major RS List.induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val app_right_Nil = result();
val prems = goal ListFn.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val app_assoc = result();
val prems = goal ListFn.thy
"ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
by (list_ind_tac "ls" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_assoc])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_assoc])));
val flat_app_distrib = result();
(*** theorems about rev ***)
val prems = goal ListFn.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [map_app_distrib])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_app_distrib])));
val rev_map_distrib = result();
(*Simplifier needs the premises as assumptions because rewriting will not
instantiate the variable ?A in the rules' typing conditions; note that
rev_type does not instantiate ?A. Only the premises do.
*)
-val prems = goal ListFn.thy
- "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
-by (cut_facts_tac prems 1);
+goal ListFn.thy
+ "!!xs. [| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
by (etac List.induct 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [app_right_Nil,app_assoc])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [app_right_Nil,app_assoc])));
val rev_app_distrib = result();
val prems = goal ListFn.thy "l: list(A) ==> rev(rev(l))=l";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [rev_app_distrib])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_app_distrib])));
val rev_rev_ident = result();
val prems = goal ListFn.thy
"ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
by (list_ind_tac "ls" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews
+by (ALLGOALS (asm_simp_tac (list_ss addsimps
[map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
val rev_flat = result();
@@ -273,22 +260,22 @@
by (cut_facts_tac prems 1);
by (list_ind_tac "xs" prems 1);
by (ALLGOALS
- (ASM_SIMP_TAC (list_ss addrews [add_0_right, add_assoc RS sym])));
-by (resolve_tac arith_congs 1);
-by (REPEAT (ares_tac [refl, list_add_type, add_commute] 1));
+ (asm_simp_tac (list_ss addsimps [add_0_right, add_assoc RS sym])));
+by (rtac (add_commute RS subst_context) 1);
+by (REPEAT (ares_tac [refl, list_add_type] 1));
val list_add_app = result();
val prems = goal ListFn.thy
"l: list(nat) ==> list_add(rev(l)) = list_add(l)";
by (list_ind_tac "l" prems 1);
by (ALLGOALS
- (ASM_SIMP_TAC (list_ss addrews [list_add_app, add_0_right])));
+ (asm_simp_tac (list_ss addsimps [list_add_app, add_0_right])));
val list_add_rev = result();
val prems = goal ListFn.thy
"ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
by (list_ind_tac "ls" prems 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [list_add_app])));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [list_add_app])));
by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
val list_add_flat = result();
@@ -301,6 +288,6 @@
\ |] ==> P(l)";
by (rtac (major RS rev_rev_ident RS subst) 1);
by (rtac (major RS rev_type RS List.induct) 1);
-by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews prems)));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps prems)));
val list_append_induct = result();
--- a/src/ZF/nat.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/nat.ML Fri Sep 17 16:16:38 1993 +0200
@@ -95,8 +95,8 @@
\ |] ==> m <= n --> P(m) --> P(n)";
by (nat_ind_tac "n" prems 1);
by (ALLGOALS
- (ASM_SIMP_TAC
- (ZF_ss addrews (prems@distrib_rews@[subset_empty_iff, subset_succ_iff,
+ (asm_simp_tac
+ (ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff,
Ord_nat RS Ord_in_Ord]))));
val nat_induct_from_lemma = result();
@@ -127,17 +127,17 @@
(** nat_case **)
-goalw Nat.thy [nat_case_def] "nat_case(0,a,b) = a";
+goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
by (fast_tac (ZF_cs addIs [the_equality]) 1);
val nat_case_0 = result();
-goalw Nat.thy [nat_case_def] "nat_case(succ(m),a,b) = b(m)";
+goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
by (fast_tac (ZF_cs addIs [the_equality]) 1);
val nat_case_succ = result();
val major::prems = goal Nat.thy
"[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) \
-\ |] ==> nat_case(n,a,b) : C(n)";
+\ |] ==> nat_case(a,b,n) : C(n)";
by (rtac (major RS nat_induct) 1);
by (REPEAT (resolve_tac [nat_case_0 RS ssubst,
nat_case_succ RS ssubst] 1
@@ -145,13 +145,6 @@
by (assume_tac 1);
val nat_case_type = result();
-val prems = goalw Nat.thy [nat_case_def]
- "[| n=n'; a=a'; !!m z. b(m)=b'(m) \
-\ |] ==> nat_case(n,a,b)=nat_case(n',a',b')";
-by (REPEAT (resolve_tac [the_cong,disj_cong,ex_cong] 1
- ORELSE EVERY1 (map rtac ((prems RL [ssubst]) @ [iff_refl]))));
-val nat_case_cong = result();
-
(** nat_rec -- used to define eclose and transrec, then obsolete **)
@@ -165,11 +158,10 @@
val [prem] = goal Nat.thy
"m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
val nat_rec_ss = ZF_ss
- addcongs (mk_typed_congs Nat.thy [("b", "[i,i]=>i")])
- addrews [prem, nat_case_succ, nat_succI, Memrel_iff,
- vimage_singleton_iff];
+ addsimps [prem, nat_case_succ, nat_succI, Memrel_iff,
+ vimage_singleton_iff];
by (rtac nat_rec_trans 1);
-by (SIMP_TAC nat_rec_ss 1);
+by (simp_tac nat_rec_ss 1);
val nat_rec_succ = result();
(** The union of two natural numbers is a natural number -- their maximum **)
--- a/src/ZF/nat.thy Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/nat.thy Fri Sep 17 16:16:38 1993 +0200
@@ -9,7 +9,7 @@
Nat = Ord + Bool +
consts
nat :: "i"
- nat_case :: "[i, i, i=>i]=>i"
+ nat_case :: "[i, i=>i, i]=>i"
nat_rec :: "[i, i, [i,i]=>i]=>i"
rules
@@ -17,10 +17,10 @@
nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
nat_case_def
- "nat_case(k,a,b) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
+ "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
nat_rec_def
"nat_rec(k,a,b) == \
-\ wfrec(Memrel(nat), k, %n f. nat_case(n, a, %m. b(m, f`m)))"
+\ wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
end
--- a/src/ZF/ord.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/ord.ML Fri Sep 17 16:16:38 1993 +0200
@@ -318,7 +318,7 @@
goal Ord.thy
"!!i j. [| Ord(i); Ord(j) |] ==> i<=succ(j) <-> i<=j | i=succ(j)";
-by (ASM_SIMP_TAC (ZF_ss addrews [member_succ_iff RS iff_sym, Ord_succ]) 1);
+by (asm_simp_tac (ZF_ss addsimps [member_succ_iff RS iff_sym, Ord_succ]) 1);
by (fast_tac ZF_cs 1);
val subset_succ_iff = result();
@@ -356,17 +356,17 @@
goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Un j : k";
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
-by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
+by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
by (rtac (Un_commute RS ssubst) 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [subset_Un_iff RS iffD1]) 1);
+by (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iffD1]) 1);
val Ord_member_UnI = result();
goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Int j : k";
by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1);
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
-by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
+by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
by (rtac (Int_commute RS ssubst) 1);
-by (ASM_SIMP_TAC (ZF_ss addrews [subset_Int_iff RS iffD1]) 1);
+by (asm_simp_tac (ZF_ss addsimps [subset_Int_iff RS iffD1]) 1);
val Ord_member_IntI = result();
--- a/src/ZF/pair.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/pair.ML Fri Sep 17 16:16:38 1993 +0200
@@ -15,7 +15,7 @@
val Pair_iff = prove_goalw ZF.thy [Pair_def]
"<a,b> = <c,d> <-> a=c & b=d"
- (fn _=> [ (SIMP_TAC (FOL_ss addrews [doubleton_iff]) 1),
+ (fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_iff]) 1),
(fast_tac FOL_cs 1) ]);
val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
@@ -89,7 +89,7 @@
val Sigma_cong = prove_goalw ZF.thy [Sigma_def]
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
\ Sigma(A,B) = Sigma(A',B')"
- (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
+ (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1) ]);
val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"
(fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
@@ -114,13 +114,6 @@
(etac ssubst 1),
(REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
-(*This congruence rule uses NO typing information...*)
-val split_cong = prove_goalw ZF.thy [split_def]
- "[| p=p'; !!x y.c(x,y) = c'(x,y) |] ==> \
-\ split(%x y.c(x,y), p) = split(%x y.c'(x,y), p')"
- (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
-
-
(*** conversions for fst and snd ***)
val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
--- a/src/ZF/perm.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/perm.ML Fri Sep 17 16:16:38 1993 +0200
@@ -52,6 +52,7 @@
(* f: bij(A,B) ==> f: A->B *)
val bij_is_fun = standard (bij_is_inj RS inj_is_fun);
+
(** Identity function **)
val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";
@@ -76,7 +77,7 @@
goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)";
by (REPEAT (ares_tac [CollectI,lam_type] 1));
-by (SIMP_TAC ZF_ss 1);
+by (simp_tac ZF_ss 1);
val id_inj = result();
goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
@@ -262,7 +263,7 @@
"!!f g. [| (f O g): inj(A,C); g: A->B; f: B->C |] ==> g: inj(A,B)";
by (safe_tac comp_cs);
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
-by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
+by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
val comp_mem_injD1 = result();
goalw Perm.thy [inj_def,surj_def]
@@ -271,9 +272,10 @@
by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
by (REPEAT (assume_tac 1));
-by (safe_tac (comp_cs addSIs ZF_congs));
+by (safe_tac comp_cs);
+by (res_inst_tac [("t", "op `(g)")] subst_context 1);
by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
-by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
+by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
val comp_mem_injD2 = result();
goalw Perm.thy [surj_def]
@@ -427,7 +429,9 @@
by (etac fun_extend 1);
by (REPEAT (ares_tac [ballI] 1));
by (REPEAT_FIRST (eresolve_tac [consE,ssubst]));
-(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x makes ASM_SIMP_TAC loop!*)
-by (ALLGOALS (SIMP_TAC (ZF_ss addrews [fun_extend_apply2,fun_extend_apply1])));
+(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x would make asm_simp_tac loop
+ using ZF_ss! But FOL_ss ignores the assumption...*)
+by (ALLGOALS (asm_simp_tac
+ (FOL_ss addsimps [fun_extend_apply2,fun_extend_apply1])));
by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type])));
val inj_extend = result();
--- a/src/ZF/qpair.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/qpair.ML Fri Sep 17 16:16:38 1993 +0200
@@ -74,7 +74,7 @@
val QSigma_cong = prove_goalw QPair.thy [QSigma_def]
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
\ QSigma(A,B) = QSigma(A',B')"
- (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
+ (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]);
val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0"
(fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
@@ -98,12 +98,6 @@
(etac ssubst 1),
(REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]);
-(*This congruence rule uses NO typing information...*)
-val qsplit_cong = prove_goalw QPair.thy [qsplit_def]
- "[| p=p'; !!x y.c(x,y) = c'(x,y) |] ==> \
-\ qsplit(%x y.c(x,y), p) = qsplit(%x y.c'(x,y), p')"
- (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
-
val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
@@ -243,7 +237,7 @@
val qsum_subset_iff = result();
goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D";
-by (SIMP_TAC (ZF_ss addrews [extension,qsum_subset_iff]) 1);
+by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1);
by (fast_tac ZF_cs 1);
val qsum_equal_iff = result();
@@ -259,12 +253,6 @@
by (rtac cond_1 1);
val qcase_QInr = result();
-val prems = goalw QPair.thy [qcase_def]
- "[| u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) |] ==> \
-\ qcase(c,d,u)=qcase(c',d',u')";
-by (REPEAT (resolve_tac ([refl,qsplit_cong,cond_cong] @ prems) 1));
-val qcase_cong = result();
-
val major::prems = goal QPair.thy
"[| u: A <+> B; \
\ !!x. x: A ==> c(x): C(QInl(x)); \
@@ -272,7 +260,7 @@
\ |] ==> qcase(c,d,u) : C(u)";
by (rtac (major RS qsumE) 1);
by (ALLGOALS (etac ssubst));
-by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
(prems@[qcase_QInl,qcase_QInr]))));
val qcase_type = result();
--- a/src/ZF/quniv.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/quniv.ML Fri Sep 17 16:16:38 1993 +0200
@@ -205,7 +205,7 @@
goalw QUniv.thy [QPair_def,sum_def]
"<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))";
-by (SIMP_TAC (ZF_ss addrews [Int_Un_distrib, product_Int_quniv_eq]) 1);
+by (simp_tac (ZF_ss addsimps [Int_Un_distrib, product_Int_quniv_eq]) 1);
val QPair_Int_quniv_eq = result();
(**** "Take-lemma" rules for proving c: quniv(A) ****)
--- a/src/ZF/simpdata.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/simpdata.ML Fri Sep 17 16:16:38 1993 +0200
@@ -10,7 +10,7 @@
(writeln s; prove_goal ZF.thy s
(fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));
-val mem_rews = map prove_fun
+val mem_simps = map prove_fun
[ "a:0 <-> False",
"a : A Un B <-> a:A | a:B",
"a : A Int B <-> a:A & a:B",
@@ -45,7 +45,7 @@
NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
fun type_auto_tac tyrls hyps = SELECT_GOAL
(DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
- ORELSE ares_tac [TrueI,ballI,allI,conjI,impI] 1));
+ ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
(** New version of mk_rew_rules **)
@@ -80,41 +80,19 @@
| _ $ A => tryrules atomize_pairs A
end;
-fun ZF_mk_rew_rules th = map mk_eq (atomize th);
+fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
-fun auto_tac rls hyps = SELECT_GOAL (DEPTH_SOLVE_1 (ares_tac (rls@hyps) 1));
-
-structure ZF_SimpData : SIMP_DATA =
- struct
- val refl_thms = FOL_SimpData.refl_thms
- val trans_thms = FOL_SimpData.trans_thms
- val red1 = FOL_SimpData.red1
- val red2 = FOL_SimpData.red2
- val mk_rew_rules = ZF_mk_rew_rules
- val norm_thms = FOL_SimpData.norm_thms
- val subst_thms = FOL_SimpData.subst_thms
- val dest_red = FOL_SimpData.dest_red
- end;
-
-structure ZF_Simp = SimpFun(ZF_SimpData);
-
-open ZF_Simp;
+val ZF_simps = [empty_subsetI, ball_simp, if_true, if_false,
+ beta, eta, restrict, fst_conv, snd_conv, split];
-(*Redeclared because the previous FOL_ss belongs to a different instance
- of type simpset*)
-val FOL_ss = empty_ss addcongs FOL_congs addrews FOL_rews
- setauto auto_tac[TrueI,ballI];
-
-(** Basic congruence and rewrite rules for ZF set theory **)
+(*Sigma_cong, Pi_cong NOT included by default since they cause
+ flex-flex pairs and the "Check your prover" error -- because most
+ Sigma's and Pi's are abbreviated as * or -> *)
+val ZF_congs =
+ [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
-val ZF_congs =
- [ball_cong,bex_cong,Replace_cong,RepFun_cong,Collect_cong,the_cong,
- if_cong,Sigma_cong,split_cong,Pi_cong,lam_cong] @ basic_ZF_congs;
-
-val ZF_rews = [empty_subsetI, ball_rew, if_true, if_false,
- beta, eta, restrict,
- fst_conv, snd_conv, split];
-
-val ZF_ss = FOL_ss addcongs ZF_congs addrews (ZF_rews@mem_rews);
-
+val ZF_ss = FOL_ss
+ setmksimps ZF_mk_rew_rules
+ addsimps (ZF_simps@mem_simps)
+ addcongs ZF_congs;
--- a/src/ZF/sum.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/sum.ML Fri Sep 17 16:16:38 1993 +0200
@@ -83,7 +83,7 @@
val sum_subset_iff = result();
goal Sum.thy "A+B = C+D <-> A=C & B=D";
-by (SIMP_TAC (ZF_ss addrews [extension,sum_subset_iff]) 1);
+by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1);
by (fast_tac ZF_cs 1);
val sum_equal_iff = result();
@@ -99,12 +99,6 @@
by (rtac cond_1 1);
val case_Inr = result();
-val prems = goalw Sum.thy [case_def]
- "[| u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) |] ==> \
-\ case(c,d,u)=case(c',d',u')";
-by (REPEAT (resolve_tac ([refl,split_cong,cond_cong] @ prems) 1));
-val case_cong = result();
-
val major::prems = goal Sum.thy
"[| u: A+B; \
\ !!x. x: A ==> c(x): C(Inl(x)); \
@@ -112,7 +106,7 @@
\ |] ==> case(c,d,u) : C(u)";
by (rtac (major RS sumE) 1);
by (ALLGOALS (etac ssubst));
-by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
(prems@[case_Inl,case_Inr]))));
val case_type = result();
--- a/src/ZF/univ.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/univ.ML Fri Sep 17 16:16:38 1993 +0200
@@ -11,7 +11,7 @@
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
-by (SIMP_TAC ZF_ss 1);
+by (simp_tac ZF_ss 1);
val Vfrom = result();
(** Monotonicity **)
@@ -122,9 +122,8 @@
goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
by (rtac (Vfrom RS trans) 1);
-brs ([refl] RL ZF_congs) 1;
-by (rtac equalityI 1);
-by (rtac (succI1 RS RepFunI RS Union_upper) 2);
+by (rtac (succI1 RS RepFunI RS Union_upper RSN
+ (2, equalityI RS subst_context)) 1);
by (rtac UN_least 1);
by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
by (etac member_succD 1);
@@ -473,16 +472,16 @@
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans]));
val rank_ss = ZF_ss
- addrews [split, case_Inl, case_Inr, Vset_rankI]
- addrews rank_trans_rls;
+ addsimps [case_Inl, case_Inr, Vset_rankI]
+ addsimps rank_trans_rls;
(** Recursion over Vset levels! **)
(*NOT SUITABLE FOR REWRITING: recursive!*)
goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
by (rtac (transrec RS ssubst) 1);
-by (SIMP_TAC (wf_ss addrews [Ord_rank, Ord_succ, Vset_D RS beta,
- VsetI RS beta]) 1);
+by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, Vset_D RS beta,
+ VsetI RS beta]) 1);
val Vrec = result();
(*This form avoids giant explosions in proofs. NOTE USE OF == *)
@@ -493,13 +492,6 @@
by (rtac Vrec 1);
val def_Vrec = result();
-val prems = goalw Univ.thy [Vrec_def]
- "[| a=a'; !!x u. H(x,u)=H'(x,u) |] ==> Vrec(a,H)=Vrec(a',H')";
-val Vrec_ss = ZF_ss addcongs ([transrec_cong] @ mk_congs Univ.thy ["rank"])
- addrews (prems RL [sym]);
-by (SIMP_TAC Vrec_ss 1);
-val Vrec_cong = result();
-
(*** univ(A) ***)
--- a/src/ZF/upair.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/upair.ML Fri Sep 17 16:16:38 1993 +0200
@@ -167,10 +167,6 @@
(resolve_tac [major RS the_equality2 RS ssubst] 1),
(REPEAT (assume_tac 1)) ]);
-val the_cong = prove_goalw ZF.thy [the_def]
- "[| !!y. P(y) <-> Q(y) |] ==> (THE x. P(x)) = (THE x. Q(x))"
- (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
-
(*** if -- a conditional expression for formulae ***)
@@ -182,38 +178,34 @@
by (fast_tac (lemmas_cs addIs [the_equality]) 1);
val if_false = result();
+(*Never use with case splitting, or if P is known to be true or false*)
val prems = goalw ZF.thy [if_def]
- "[| P<->Q; a=c; b=d |] ==> if(P,a,b) = if(Q,c,d)";
-by (REPEAT (resolve_tac (prems@[refl,the_cong]@FOL_congs) 1));
+ "[| P<->Q; Q ==> a=c; ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
+by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1);
val if_cong = result();
(*Not needed for rewriting, since P would rewrite to True anyway*)
-val prems = goalw ZF.thy [if_def] "P ==> if(P,a,b) = a";
-by (cut_facts_tac prems 1);
+goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
val if_P = result();
(*Not needed for rewriting, since P would rewrite to False anyway*)
-val prems = goalw ZF.thy [if_def] "~P ==> if(P,a,b) = b";
-by (cut_facts_tac prems 1);
+goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
val if_not_P = result();
-val if_ss =
- FOL_ss addcongs (if_cong :: mk_typed_congs ZF.thy [("P", "i=>o")]
- @ basic_ZF_congs)
- addrews [if_true,if_false];
+val if_ss = FOL_ss addsimps [if_true,if_false];
val expand_if = prove_goal ZF.thy
"P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
(fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
- (ASM_SIMP_TAC if_ss 1),
- (ASM_SIMP_TAC if_ss 1) ]);
+ (asm_simp_tac if_ss 1),
+ (asm_simp_tac if_ss 1) ]);
val prems = goal ZF.thy
"[| P ==> a: A; ~P ==> b: A |] ==> if(P,a,b): A";
by (res_inst_tac [("Q","P")] (excluded_middle RS disjE) 1);
-by (ALLGOALS (ASM_SIMP_TAC (if_ss addrews prems)));
+by (ALLGOALS (asm_simp_tac (if_ss addsimps prems)));
val if_type = result();
--- a/src/ZF/wf.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/wf.ML Fri Sep 17 16:16:38 1993 +0200
@@ -19,10 +19,6 @@
open WF;
-val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")];
-
-val wf_ss = ZF_ss addcongs [H_cong];
-
(*** Well-founded relations ***)
@@ -138,13 +134,13 @@
(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
spec RS mp instantiates induction hypotheses*)
fun indhyp_tac hyps =
- ares_tac (TrueI::hyps) ORELSE'
+ resolve_tac (TrueI::refl::hyps) ORELSE'
(cut_facts_tac hyps THEN'
DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
eresolve_tac [underD, transD, spec RS mp]));
-(*** NOTE! some simplifications need a different auto_tac!! ***)
-val wf_super_ss = wf_ss setauto indhyp_tac;
+(*** NOTE! some simplifications need a different solver!! ***)
+val wf_super_ss = ZF_ss setsolver indhyp_tac;
val prems = goalw WF.thy [is_recfun_def]
"[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \
@@ -153,7 +149,7 @@
by (wf_ind_tac "x" prems 1);
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
by (rewtac restrict_def);
-by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1);
+by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
val is_recfun_equal_lemma = result();
val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
@@ -165,7 +161,7 @@
by (rtac (consI1 RS restrict_type RS fun_extension) 1);
by (etac is_recfun_type 1);
by (ALLGOALS
- (ASM_SIMP_TAC (wf_super_ss addrews
+ (asm_simp_tac (wf_super_ss addsimps
[ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
val is_recfun_cut = result();
@@ -195,13 +191,13 @@
by (REPEAT (assume_tac 2));
by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
(*Applying the substitution: must keep the quantified assumption!!*)
-by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1));
+by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1));
by (fold_tac [is_recfun_def]);
-by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1);
+by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1);
by (rtac is_recfun_type 1);
by (ALLGOALS
- (ASM_SIMP_TAC
- (wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut])));
+ (asm_simp_tac
+ (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
val unfold_the_recfun = result();
@@ -214,13 +210,12 @@
val the_recfun_cut = result();
(*NOT SUITABLE FOR REWRITING since it is recursive!*)
-val prems = goalw WF.thy [wftrec_def]
- "[| wf(r); trans(r) |] ==> \
-\ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
+goalw WF.thy [wftrec_def]
+ "!!r. [| wf(r); trans(r) |] ==> \
+\ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
-by (ALLGOALS (ASM_SIMP_TAC
- (wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym,
- the_recfun_cut]))));
+by (ALLGOALS (asm_simp_tac
+ (ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
val wftrec = result();
(** Removal of the premise trans(r) **)
@@ -230,8 +225,7 @@
"wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
by (rtac trans_trancl 1);
-by (rtac (refl RS H_cong) 1);
-by (rtac (vimage_pair_mono RS restrict_lam_eq) 1);
+by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
by (etac r_into_trancl 1);
by (rtac subset_refl 1);
val wfrec = result();
@@ -253,10 +247,3 @@
by (REPEAT (ares_tac (prems@[lam_type]) 1
ORELSE eresolve_tac [spec RS mp, underD] 1));
val wfrec_type = result();
-
-val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def]
- "[| r=r'; !!x u. H(x,u)=H'(x,u); a=a' |] \
-\ ==> wfrec(r,a,H)=wfrec(r',a',H')";
-by (EVERY1 (map rtac (prems RL [subst])));
-by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1);
-val wfrec_cong = result();
--- a/src/ZF/zf.ML Fri Sep 17 12:53:53 1993 +0200
+++ b/src/ZF/zf.ML Fri Sep 17 16:16:38 1993 +0200
@@ -13,9 +13,8 @@
val ballE : thm
val ballI : thm
val ball_cong : thm
- val ball_rew : thm
+ val ball_simp : thm
val ball_tac : int -> tactic
- val basic_ZF_congs : thm list
val bexCI : thm
val bexE : thm
val bexI : thm
@@ -45,7 +44,6 @@
val lemmas_cs : claset
val PowD : thm
val PowI : thm
- val prove_cong_tac : thm list -> int -> tactic
val RepFunE : thm
val RepFunI : thm
val RepFun_eqI : thm
@@ -75,14 +73,6 @@
structure ZF_Lemmas : ZF_LEMMAS =
struct
-val basic_ZF_congs = mk_congs ZF.thy
- ["op `", "op ``", "op Int", "op Un", "op -", "op <=", "op :",
- "Pow", "Union", "Inter", "fst", "snd", "succ", "Pair", "Upair", "cons",
- "domain", "range", "restrict"];
-
-fun prove_cong_tac prems i =
- REPEAT (ares_tac (prems@[refl]@FOL_congs@basic_ZF_congs) i);
-
(*** Bounded universal quantifier ***)
val ballI = prove_goalw ZF.thy [Ball_def]
@@ -118,14 +108,13 @@
val ball_tac = dtac bspec THEN' assume_tac;
(*Trival rewrite rule; (ALL x:A.P)<->P holds only if A is nonempty!*)
-val ball_rew = prove_goal ZF.thy "(ALL x:A. True) <-> True"
- (fn prems=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
+val ball_simp = prove_goal ZF.thy "(ALL x:A. True) <-> True"
+ (fn _=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
(*Congruence rule for rewriting*)
val ball_cong = prove_goalw ZF.thy [Ball_def]
- "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) \
-\ |] ==> (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
- (fn prems=> [ (prove_cong_tac prems 1) ]);
+ "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
+ (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
(*** Bounded existential quantifier ***)
@@ -151,8 +140,8 @@
val bex_cong = prove_goalw ZF.thy [Bex_def]
"[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) \
-\ |] ==> (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
- (fn prems=> [ (prove_cong_tac prems 1) ]);
+\ |] ==> Bex(A,P) <-> Bex(A',P')"
+ (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
(*** Rules for subsets ***)
@@ -265,7 +254,7 @@
val Replace_cong = prove_goal ZF.thy
"[| A=B; !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
-\ {y. x:A, P(x,y)} = {y. x:B, Q(x,y)}"
+\ Replace(A,P) = Replace(B,Q)"
(fn prems=>
let val substprems = prems RL [subst, ssubst]
and iffprems = prems RL [iffD1,iffD2]
@@ -275,7 +264,6 @@
ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]
end);
-
(*** Rules for RepFun ***)
val RepFunI = prove_goalw ZF.thy [RepFun_def]
@@ -296,9 +284,8 @@
(REPEAT (ares_tac prems 1)) ]);
val RepFun_cong = prove_goalw ZF.thy [RepFun_def]
- "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> \
-\ {f(x). x:A} = {g(x). x:B}"
- (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
+ "[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
+ (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
(*** Rules for Collect -- forming a subset by separation ***)
@@ -332,9 +319,8 @@
(assume_tac 1) ]);
val Collect_cong = prove_goalw ZF.thy [Collect_def]
- "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> \
-\ {x:A. P(x)} = {x:B. Q(x)}"
- (fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);
+ "[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
+ (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
(*** Rules for Unions ***)