--- a/src/ZF/AC.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/AC.ML Fri Aug 14 18:37:28 1998 +0200
@@ -61,3 +61,9 @@
by (REPEAT (ares_tac [non_empty_family] 1));
qed "AC_Pi0";
+(*Used in Zorn.ML*)
+Goal "[| ch : (PROD X:Pow(S) - {0}. X); X<=S; X~=S |] ==> ch ` (S-X) : S-X";
+by (etac apply_type 1);
+by (blast_tac (claset() addSEs [equalityE]) 1);
+qed "choice_Diff";
+
--- a/src/ZF/Fixedpt.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Fixedpt.ML Fri Aug 14 18:37:28 1998 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-For fixedpt.thy. Least and greatest fixed points; the Knaster-Tarski Theorem
+Least and greatest fixed points; the Knaster-Tarski Theorem
Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
*)
@@ -12,7 +12,7 @@
(*** Monotone operators ***)
-val prems = goalw Fixedpt.thy [bnd_mono_def]
+val prems = Goalw [bnd_mono_def]
"[| h(D)<=D; \
\ !!W X. [| W<=D; X<=D; W<=X |] ==> h(W) <= h(X) \
\ |] ==> bnd_mono(D,h)";
@@ -20,14 +20,12 @@
ORELSE etac subset_trans 1));
qed "bnd_monoI";
-val [major] = goalw Fixedpt.thy [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D";
-by (rtac (major RS conjunct1) 1);
+Goalw [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D";
+by (etac conjunct1 1);
qed "bnd_monoD1";
-val major::prems = goalw Fixedpt.thy [bnd_mono_def]
- "[| bnd_mono(D,h); W<=X; X<=D |] ==> h(W) <= h(X)";
-by (rtac (major RS conjunct2 RS spec RS spec RS mp RS mp) 1);
-by (REPEAT (resolve_tac prems 1));
+Goalw [bnd_mono_def] "[| bnd_mono(D,h); W<=X; X<=D |] ==> h(W) <= h(X)";
+by (Blast_tac 1);
qed "bnd_monoD2";
val [major,minor] = goal Fixedpt.thy
@@ -71,7 +69,7 @@
by (rtac lfp_subset 1);
qed "def_lfp_subset";
-val prems = goalw Fixedpt.thy [lfp_def]
+val prems = Goalw [lfp_def]
"[| h(D) <= D; !!X. [| h(X) <= X; X<=D |] ==> A<=X |] ==> \
\ A <= lfp(D,h)";
by (rtac (Pow_top RS CollectI RS Inter_greatest) 1);
@@ -85,11 +83,10 @@
by (REPEAT (resolve_tac prems 1));
qed "lfp_lemma1";
-val [hmono] = goal Fixedpt.thy
- "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)";
+Goal "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)";
by (rtac (bnd_monoD1 RS lfp_greatest) 1);
by (rtac lfp_lemma1 2);
-by (REPEAT (ares_tac [hmono] 1));
+by (REPEAT (assume_tac 1));
qed "lfp_lemma2";
val [hmono] = goal Fixedpt.thy
@@ -101,9 +98,8 @@
by (REPEAT (rtac lfp_subset 1));
qed "lfp_lemma3";
-val prems = goal Fixedpt.thy
- "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
-by (REPEAT (resolve_tac (prems@[equalityI,lfp_lemma2,lfp_lemma3]) 1));
+Goal "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
+by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
qed "lfp_Tarski";
(*Definition form, to control unfolding*)
@@ -115,7 +111,7 @@
(*** General induction rule for least fixedpoints ***)
-val [hmono,indstep] = goal Fixedpt.thy
+val [hmono,indstep] = Goal
"[| bnd_mono(D,h); !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \
\ |] ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)";
by (rtac subsetI 1);
@@ -128,7 +124,7 @@
(*This rule yields an induction hypothesis in which the components of a
data structure may be assumed to be elements of lfp(D,h)*)
-val prems = goal Fixedpt.thy
+val prems = Goal
"[| bnd_mono(D,h); a : lfp(D,h); \
\ !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \
\ |] ==> P(a)";
@@ -138,7 +134,7 @@
qed "induct";
(*Definition form, to control unfolding*)
-val rew::prems = goal Fixedpt.thy
+val rew::prems = Goal
"[| A == lfp(D,h); bnd_mono(D,h); a:A; \
\ !!x. x : h(Collect(A,P)) ==> P(x) \
\ |] ==> P(a)";
@@ -157,7 +153,7 @@
(*Monotonicity of lfp, where h precedes i under a domain-like partial order
monotonicity of h is not strictly necessary; h must be bounded by D*)
-val [hmono,imono,subhi] = goal Fixedpt.thy
+val [hmono,imono,subhi] = Goal
"[| bnd_mono(D,h); bnd_mono(E,i); \
\ !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(E,i)";
by (rtac (bnd_monoD1 RS lfp_greatest) 1);
@@ -170,7 +166,7 @@
(*This (unused) version illustrates that monotonicity is not really needed,
but both lfp's must be over the SAME set D; Inter is anti-monotonic!*)
-val [isubD,subhi] = goal Fixedpt.thy
+val [isubD,subhi] = Goal
"[| i(D) <= D; !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(D,i)";
by (rtac lfp_greatest 1);
by (rtac isubD 1);
@@ -183,10 +179,9 @@
(**** Proof of Knaster-Tarski Theorem for the gfp ****)
(*gfp contains each post-fixedpoint that is contained in D*)
-val prems = goalw Fixedpt.thy [gfp_def]
- "[| A <= h(A); A<=D |] ==> A <= gfp(D,h)";
+Goalw [gfp_def] "[| A <= h(A); A<=D |] ==> A <= gfp(D,h)";
by (rtac (PowI RS CollectI RS Union_upper) 1);
-by (REPEAT (resolve_tac prems 1));
+by (REPEAT (assume_tac 1));
qed "gfp_upperbound";
Goalw [gfp_def] "gfp(D,h) <= D";
@@ -199,7 +194,7 @@
by (rtac gfp_subset 1);
qed "def_gfp_subset";
-val hmono::prems = goalw Fixedpt.thy [gfp_def]
+val hmono::prems = Goalw [gfp_def]
"[| bnd_mono(D,h); !!X. [| X <= h(X); X<=D |] ==> X<=A |] ==> \
\ gfp(D,h) <= A";
by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1);
@@ -213,11 +208,10 @@
by (REPEAT (resolve_tac prems 1));
qed "gfp_lemma1";
-val [hmono] = goal Fixedpt.thy
- "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))";
+Goal "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))";
by (rtac gfp_least 1);
by (rtac gfp_lemma1 2);
-by (REPEAT (ares_tac [hmono] 1));
+by (REPEAT (assume_tac 1));
qed "gfp_lemma2";
val [hmono] = goal Fixedpt.thy
@@ -228,9 +222,8 @@
by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1));
qed "gfp_lemma3";
-val prems = goal Fixedpt.thy
- "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
-by (REPEAT (resolve_tac (prems@[equalityI,gfp_lemma2,gfp_lemma3]) 1));
+Goal "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
+by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
qed "gfp_Tarski";
(*Definition form, to control unfolding*)
@@ -275,7 +268,7 @@
qed "def_coinduct";
(*Lemma used immediately below!*)
-val [subsA,XimpP] = goal ZF.thy
+val [subsA,XimpP] = Goal
"[| X <= A; !!z. z:X ==> P(z) |] ==> X <= Collect(A,P)";
by (rtac (subsA RS subsetD RS CollectI RS subsetI) 1);
by (assume_tac 1);
@@ -283,7 +276,7 @@
qed "subset_Collect";
(*The version used in the induction/coinduction package*)
-val prems = goal Fixedpt.thy
+val prems = Goal
"[| A == gfp(D, %w. Collect(D,P(w))); bnd_mono(D, %w. Collect(D,P(w))); \
\ a: X; X <= D; !!z. z: X ==> P(X Un A, z) |] ==> \
\ a : A";
@@ -292,7 +285,7 @@
qed "def_Collect_coinduct";
(*Monotonicity of gfp!*)
-val [hmono,subde,subhi] = goal Fixedpt.thy
+val [hmono,subde,subhi] = Goal
"[| bnd_mono(D,h); D <= E; \
\ !!X. X<=D ==> h(X) <= i(X) |] ==> gfp(D,h) <= gfp(E,i)";
by (rtac gfp_upperbound 1);
--- a/src/ZF/List.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/List.ML Fri Aug 14 18:37:28 1998 +0200
@@ -55,7 +55,7 @@
by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
qed "list_into_univ";
-val major::prems = goal List.thy
+val major::prems = Goal
"[| l: list(A); \
\ c: C(Nil); \
\ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \
@@ -142,7 +142,7 @@
(*Type checking -- proved by induction, as usual*)
-val prems = goal List.thy
+val prems = Goal
"[| l: list(A); \
\ c: C(Nil); \
\ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \
@@ -153,14 +153,12 @@
(** Versions for use with definitions **)
-val [rew] = goal List.thy
- "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
+val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Nil) = c";
by (rewtac rew);
by (rtac list_rec_Nil 1);
qed "def_list_rec_Nil";
-val [rew] = goal List.thy
- "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
+val [rew] = Goal "[| !!l. j(l)==list_rec(l, c, h) |] ==> j(Cons(a,l)) = h(a,l,j(l))";
by (rewtac rew);
by (rtac list_rec_Cons 1);
qed "def_list_rec_Cons";
@@ -173,13 +171,13 @@
val [map_Nil,map_Cons] = list_recs map_def;
Addsimps [map_Nil, map_Cons];
-val prems = goalw List.thy [map_def]
+val prems = Goalw [map_def]
"[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
qed "map_type";
-val [major] = goal List.thy "l: list(A) ==> map(h,l) : list({h(u). u:A})";
-by (rtac (major RS map_type) 1);
+Goal "l: list(A) ==> map(h,l) : list({h(u). u:A})";
+by (etac map_type 1);
by (etac RepFunI 1);
qed "map_type2";
@@ -263,35 +261,30 @@
(*** theorems about map ***)
-val prems = goal List.thy
- "l: list(A) ==> map(%u. u, l) = l";
-by (list_ind_tac "l" prems 1);
+Goal "l: list(A) ==> map(%u. u, l) = l";
+by (list_ind_tac "l" [] 1);
by (ALLGOALS Asm_simp_tac);
qed "map_ident";
-val prems = goal List.thy
- "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
-by (list_ind_tac "l" prems 1);
+Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
+by (list_ind_tac "l" [] 1);
by (ALLGOALS Asm_simp_tac);
qed "map_compose";
-val prems = goal List.thy
- "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
-by (list_ind_tac "xs" prems 1);
+Goal "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
+by (list_ind_tac "xs" [] 1);
by (ALLGOALS Asm_simp_tac);
qed "map_app_distrib";
-val prems = goal List.thy
- "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
-by (list_ind_tac "ls" prems 1);
+Goal "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
+by (list_ind_tac "ls" [] 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
qed "map_flat";
-val prems = goal List.thy
- "l: list(A) ==> \
+Goal "l: list(A) ==> \
\ 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 (list_ind_tac "l" [] 1);
by (ALLGOALS Asm_simp_tac);
qed "list_rec_map";
@@ -300,23 +293,20 @@
(* c : list(Collect(B,P)) ==> c : list(B) *)
bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD));
-val prems = goal List.thy
- "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
-by (list_ind_tac "l" prems 1);
+Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
+by (list_ind_tac "l" [] 1);
by (ALLGOALS Asm_simp_tac);
qed "map_list_Collect";
(*** theorems about length ***)
-val prems = goal List.thy
- "xs: list(A) ==> length(map(h,xs)) = length(xs)";
-by (list_ind_tac "xs" prems 1);
+Goal "xs: list(A) ==> length(map(h,xs)) = length(xs)";
+by (list_ind_tac "xs" [] 1);
by (ALLGOALS Asm_simp_tac);
qed "length_map";
-val prems = goal List.thy
- "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
-by (list_ind_tac "xs" prems 1);
+Goal "xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
+by (list_ind_tac "xs" [] 1);
by (ALLGOALS Asm_simp_tac);
qed "length_app";
@@ -324,15 +314,13 @@
Used for rewriting below*)
val add_commute_succ = nat_succI RSN (2,add_commute);
-val prems = goal List.thy
- "xs: list(A) ==> length(rev(xs)) = length(xs)";
-by (list_ind_tac "xs" prems 1);
+Goal "xs: list(A) ==> length(rev(xs)) = length(xs)";
+by (list_ind_tac "xs" [] 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app, add_commute_succ])));
qed "length_rev";
-val prems = goal List.thy
- "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
-by (list_ind_tac "ls" prems 1);
+Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
+by (list_ind_tac "ls" [] 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
qed "length_flat";
@@ -364,26 +352,25 @@
(*** theorems about app ***)
-val [major] = goal List.thy "xs: list(A) ==> xs@Nil=xs";
-by (rtac (major RS list.induct) 1);
+Goal "xs: list(A) ==> xs@Nil=xs";
+by (etac list.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "app_right_Nil";
-val prems = goal List.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
-by (list_ind_tac "xs" prems 1);
+Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
+by (list_ind_tac "xs" [] 1);
by (ALLGOALS Asm_simp_tac);
qed "app_assoc";
-val prems = goal List.thy
- "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
-by (list_ind_tac "ls" prems 1);
+Goal "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
+by (list_ind_tac "ls" [] 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
qed "flat_app_distrib";
(*** theorems about rev ***)
-val prems = goal List.thy "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
-by (list_ind_tac "l" prems 1);
+Goal "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
+by (list_ind_tac "l" [] 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
qed "rev_map_distrib";
@@ -396,14 +383,13 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_right_Nil,app_assoc])));
qed "rev_app_distrib";
-val prems = goal List.thy "l: list(A) ==> rev(rev(l))=l";
-by (list_ind_tac "l" prems 1);
+Goal "l: list(A) ==> rev(rev(l))=l";
+by (list_ind_tac "l" [] 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib])));
qed "rev_rev_ident";
-val prems = goal List.thy
- "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
-by (list_ind_tac "ls" prems 1);
+Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
+by (list_ind_tac "ls" [] 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps
[map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
qed "rev_flat";
@@ -411,34 +397,30 @@
(*** theorems about list_add ***)
-val prems = goal List.thy
- "[| xs: list(nat); ys: list(nat) |] ==> \
+Goal "[| xs: list(nat); ys: list(nat) |] ==> \
\ list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
-by (cut_facts_tac prems 1);
-by (list_ind_tac "xs" prems 1);
+by (list_ind_tac "xs" [] 1);
by (ALLGOALS
(asm_simp_tac (simpset() 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));
qed "list_add_app";
-val prems = goal List.thy
- "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
-by (list_ind_tac "l" prems 1);
+Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
+by (list_ind_tac "l" [] 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [list_add_app, add_0_right])));
qed "list_add_rev";
-val prems = goal List.thy
- "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
-by (list_ind_tac "ls" prems 1);
+Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
+by (list_ind_tac "ls" [] 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
qed "list_add_flat";
(** New induction rule **)
-val major::prems = goal List.thy
+val major::prems = Goal
"[| l: list(A); \
\ P(Nil); \
\ !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) \
--- a/src/ZF/Ordinal.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Ordinal.ML Fri Aug 14 18:37:28 1998 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-For Ordinal.thy. Ordinals in Zermelo-Fraenkel Set Theory
+Ordinals in Zermelo-Fraenkel Set Theory
*)
open Ordinal;
@@ -73,12 +73,12 @@
by (Blast_tac 1);
qed "Transset_Union";
-val [Transprem] = goalw Ordinal.thy [Transset_def]
+val [Transprem] = Goalw [Transset_def]
"[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))";
by (blast_tac (claset() addDs [Transprem RS bspec RS subsetD]) 1);
qed "Transset_Union_family";
-val [prem,Transprem] = goalw Ordinal.thy [Transset_def]
+val [prem,Transprem] = Goalw [Transset_def]
"[| j:A; !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))";
by (cut_facts_tac [prem] 1);
by (blast_tac (claset() addDs [Transprem RS bspec RS subsetD]) 1);
@@ -86,19 +86,18 @@
(*** Natural Deduction rules for Ord ***)
-val prems = goalw Ordinal.thy [Ord_def]
+val prems = Goalw [Ord_def]
"[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i)";
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
qed "OrdI";
-val [major] = goalw Ordinal.thy [Ord_def]
- "Ord(i) ==> Transset(i)";
-by (rtac (major RS conjunct1) 1);
+Goalw [Ord_def] "Ord(i) ==> Transset(i)";
+by (Blast_tac 1);
qed "Ord_is_Transset";
-val [major,minor] = goalw Ordinal.thy [Ord_def]
+Goalw [Ord_def]
"[| Ord(i); j:i |] ==> Transset(j) ";
-by (rtac (minor RS (major RS conjunct2 RS bspec)) 1);
+by (Blast_tac 1);
qed "Ord_contains_Transset";
(*** Lemmas for ordinals ***)
@@ -159,7 +158,7 @@
by (blast_tac (claset() addSIs [Transset_Int]) 1);
qed "Ord_Int";
-val nonempty::prems = goal Ordinal.thy
+val nonempty::prems = Goal
"[| j:A; !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
by (rtac Ord_is_Transset 1);
@@ -167,7 +166,7 @@
ORELSE etac InterD 1));
qed "Ord_Inter";
-val jmemA::prems = goal Ordinal.thy
+val jmemA::prems = Goal
"[| j:A; !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))";
by (rtac (jmemA RS RepFunI RS Ord_Inter) 1);
by (etac RepFunE 1);
@@ -194,7 +193,7 @@
by (REPEAT (ares_tac [conjI] 1));
qed "ltI";
-val major::prems = goalw Ordinal.thy [lt_def]
+val major::prems = Goalw [lt_def]
"[| i<j; [| i:j; Ord(i); Ord(j) |] ==> P |] ==> P";
by (rtac (major RS conjE) 1);
by (REPEAT (ares_tac (prems@[Ord_in_Ord]) 1));
@@ -258,12 +257,12 @@
val le_refl = refl RS le_eqI;
-val [prem] = goal Ordinal.thy "(~ (i=j & Ord(j)) ==> i<j) ==> i le j";
+val [prem] = Goal "(~ (i=j & Ord(j)) ==> i<j) ==> i le j";
by (rtac (disjCI RS (le_iff RS iffD2)) 1);
by (etac prem 1);
qed "leCI";
-val major::prems = goal Ordinal.thy
+val major::prems = Goal
"[| i le j; i<j ==> P; [| i=j; Ord(j) |] ==> P |] ==> P";
by (rtac (major RS (le_iff RS iffD1 RS disjE)) 1);
by (DEPTH_SOLVE (ares_tac prems 1 ORELSE etac conjE 1));
@@ -298,7 +297,7 @@
by (REPEAT (ares_tac [conjI, Memrel_iff RS iffD2] 1));
qed "MemrelI";
-val [major,minor] = goal Ordinal.thy
+val [major,minor] = Goal
"[| <a,b> : Memrel(A); \
\ [| a: A; b: A; a:b |] ==> P \
\ |] ==> P";
@@ -357,7 +356,7 @@
(*** Transfinite induction ***)
(*Epsilon induction over a transitive set*)
-val major::prems = goalw Ordinal.thy [Transset_def]
+val major::prems = Goalw [Transset_def]
"[| i: k; Transset(k); \
\ !!x.[| x: k; ALL y:x. P(y) |] ==> P(x) \
\ |] ==> P(i)";
@@ -373,7 +372,7 @@
val Ord_induct = Ord_is_Transset RSN (2, Transset_induct);
(*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
-val [major,indhyp] = goal Ordinal.thy
+val [major,indhyp] = Goal
"[| Ord(i); \
\ !!x.[| Ord(x); ALL y:x. P(y) |] ==> P(x) \
\ |] ==> P(i)";
@@ -397,29 +396,28 @@
(** Proving that < is a linear ordering on the ordinals **)
-val prems = goal Ordinal.thy
- "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)";
-by (trans_ind_tac "i" prems 1);
+Goal "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)";
+by (etac trans_induct 1);
by (rtac (impI RS allI) 1);
by (trans_ind_tac "j" [] 1);
by (DEPTH_SOLVE (Step_tac 1 ORELSE Ord_trans_tac 1));
qed_spec_mp "Ord_linear";
(*The trichotomy law for ordinals!*)
-val ordi::ordj::prems = goalw Ordinal.thy [lt_def]
+val ordi::ordj::prems = Goalw [lt_def]
"[| Ord(i); Ord(j); i<j ==> P; i=j ==> P; j<i ==> P |] ==> P";
by (rtac ([ordi,ordj] MRS Ord_linear RS disjE) 1);
by (etac disjE 2);
by (DEPTH_SOLVE (ares_tac ([ordi,ordj,conjI] @ prems) 1));
qed "Ord_linear_lt";
-val prems = goal Ordinal.thy
+val prems = Goal
"[| Ord(i); Ord(j); i<j ==> P; j le i ==> P |] ==> P";
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
by (DEPTH_SOLVE (ares_tac ([leI, sym RS le_eqI] @ prems) 1));
qed "Ord_linear2";
-val prems = goal Ordinal.thy
+val prems = Goal
"[| Ord(i); Ord(j); i le j ==> P; j le i ==> P |] ==> P";
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
by (DEPTH_SOLVE (ares_tac ([leI,le_eqI] @ prems) 1));
@@ -489,7 +487,7 @@
qed "le_succ_iff";
(*Just a variant of subset_imp_le*)
-val [ordi,ordj,minor] = goal Ordinal.thy
+val [ordi,ordj,minor] = Goal
"[| Ord(i); Ord(j); !!x. x<j ==> x<i |] ==> j le i";
by (REPEAT_FIRST (ares_tac [notI RS not_lt_imp_le, ordi, ordj]));
by (etac (minor RS lt_irrefl) 1);
@@ -581,12 +579,12 @@
(*** Results about limits ***)
-val prems = goal Ordinal.thy "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))";
+val prems = Goal "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))";
by (rtac (Ord_is_Transset RS Transset_Union_family RS OrdI) 1);
by (REPEAT (etac UnionE 1 ORELSE ares_tac ([Ord_contains_Transset]@prems) 1));
qed "Ord_Union";
-val prems = goal Ordinal.thy
+val prems = Goal
"[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))";
by (rtac Ord_Union 1);
by (etac RepFunE 1);
@@ -595,27 +593,27 @@
qed "Ord_UN";
(* No < version; consider (UN i:nat.i)=nat *)
-val [ordi,limit] = goal Ordinal.thy
+val [ordi,limit] = Goal
"[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i";
by (rtac (le_imp_subset RS UN_least RS subset_imp_le) 1);
by (REPEAT (ares_tac [ordi, Ord_UN, limit] 1 ORELSE etac (limit RS ltE) 1));
qed "UN_least_le";
-val [jlti,limit] = goal Ordinal.thy
+val [jlti,limit] = Goal
"[| j<i; !!x. x:A ==> b(x)<j |] ==> (UN x:A. succ(b(x))) < i";
by (rtac (jlti RS ltE) 1);
by (rtac (UN_least_le RS lt_trans2) 1);
by (REPEAT (ares_tac [jlti, succ_leI, limit] 1));
qed "UN_succ_least_lt";
-val prems = goal Ordinal.thy
+val prems = Goal
"[| a: A; i le b(a); !!x. x:A ==> Ord(b(x)) |] ==> i le (UN x:A. b(x))";
by (resolve_tac (prems RL [ltE]) 1);
by (rtac (le_imp_subset RS subset_trans RS subset_imp_le) 1);
by (REPEAT (ares_tac (prems @ [UN_upper, Ord_UN]) 1));
qed "UN_upper_le";
-val [leprem] = goal Ordinal.thy
+val [leprem] = Goal
"[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))";
by (rtac UN_least_le 1);
by (rtac UN_upper_le 2);
@@ -679,7 +677,7 @@
addSDs [Ord_succD]) 1);
qed "Ord_cases_disj";
-val major::prems = goal Ordinal.thy
+val major::prems = Goal
"[| Ord(i); \
\ i=0 ==> P; \
\ !!j. [| Ord(j); i=succ(j) |] ==> P; \
@@ -689,7 +687,7 @@
by (REPEAT (eresolve_tac (prems@[asm_rl, disjE, exE, conjE]) 1));
qed "Ord_cases";
-val major::prems = goal Ordinal.thy
+val major::prems = Goal
"[| Ord(i); \
\ P(0); \
\ !!x. [| Ord(x); P(x) |] ==> P(succ(x)); \
--- a/src/ZF/Perm.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Perm.ML Fri Aug 14 18:37:28 1998 +0200
@@ -33,7 +33,7 @@
by (blast_tac (claset() addIs prems) 1);
qed "f_imp_surjective";
-val prems = goal Perm.thy
+val prems = Goal
"[| !!x. x:A ==> c(x): B; \
\ !!y. y:B ==> d(y): A; \
\ !!y. y:B ==> c(d(y)) = y \
@@ -74,7 +74,7 @@
by (deepen_tac (claset() addEs [subst_context RS box_equals]) 0 1);
bind_thm ("f_imp_injective", ballI RSN (2,result()));
-val prems = goal Perm.thy
+val prems = Goal
"[| !!x. x:A ==> c(x): B; \
\ !!x. x:A ==> d(c(x)) = x \
\ |] ==> (lam x:A. c(x)) : inj(A,B)";
@@ -185,10 +185,9 @@
val left_inverse_bij = bij_is_inj RS left_inverse;
-val prems = goal Perm.thy
- "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b";
+Goal "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b";
by (rtac (apply_Pair RS (converseD RS apply_equality)) 1);
-by (REPEAT (resolve_tac prems 1));
+by (REPEAT (assume_tac 1));
qed "right_inverse_lemma";
(*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
@@ -337,7 +336,7 @@
Addsimps [comp_fun_apply];
(*Simplifies compositions of lambda-abstractions*)
-val [prem] = goal Perm.thy
+val [prem] = Goal
"[| !!x. x:A ==> b(x): B \
\ |] ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))";
by (rtac fun_extension 1);
@@ -513,11 +512,10 @@
box_equals, restrict] 1));
qed "restrict_inj";
-val prems = goal Perm.thy
- "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)";
+Goal "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)";
by (rtac (restrict_image RS subst) 1);
by (rtac (restrict_type2 RS surj_image) 3);
-by (REPEAT (resolve_tac prems 1));
+by (REPEAT (assume_tac 1));
qed "restrict_surj";
Goalw [inj_def,bij_def]
--- a/src/ZF/QUniv.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/QUniv.ML Fri Aug 14 18:37:28 1998 +0200
@@ -160,42 +160,6 @@
bind_thm ("bool_into_quniv", bool_subset_quniv RS subsetD);
-(**** Properties of Vfrom analogous to the "take-lemma" ****)
-
-(*** Intersecting a*b with Vfrom... ***)
-
-(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
-goal Univ.thy
- "!!X. [| {a,b} : Vfrom(X,succ(i)); Transset(X) |] ==> \
-\ a: Vfrom(X,i) & b: Vfrom(X,i)";
-by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
-by (assume_tac 1);
-by (Fast_tac 1);
-qed "doubleton_in_Vfrom_D";
-
-(*This weaker version says a, b exist at the same level*)
-bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D);
-
-(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
- implies a, b : Vfrom(X,i), which is useless for induction.
- Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
- implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
- The combination gives a reduction by precisely one level, which is
- most convenient for proofs.
-**)
-
-goalw Univ.thy [Pair_def]
- "!!X. [| <a,b> : Vfrom(X,succ(i)); Transset(X) |] ==> \
-\ a: Vfrom(X,i) & b: Vfrom(X,i)";
-by (blast_tac (claset() addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
-qed "Pair_in_Vfrom_D";
-
-goal Univ.thy
- "!!X. Transset(X) ==> \
-\ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
-by (blast_tac (claset() addSDs [Pair_in_Vfrom_D]) 1);
-qed "product_Int_Vfrom_subset";
-
(*** Intersecting <a;b> with Vfrom... ***)
Goalw [QPair_def,sum_def]
--- a/src/ZF/Rel.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Rel.ML Fri Aug 14 18:37:28 1998 +0200
@@ -12,19 +12,18 @@
(* irreflexivity *)
-val prems = goalw Rel.thy [irrefl_def]
+val prems = Goalw [irrefl_def]
"[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)";
by (REPEAT (ares_tac (prems @ [ballI]) 1));
qed "irreflI";
-val prems = goalw Rel.thy [irrefl_def]
- "[| irrefl(A,r); x:A |] ==> <x,x> ~: r";
-by (rtac (prems MRS bspec) 1);
+Goalw [irrefl_def] "[| irrefl(A,r); x:A |] ==> <x,x> ~: r";
+by (Blast_tac 1);
qed "irreflE";
(* symmetry *)
-val prems = goalw Rel.thy [sym_def]
+val prems = Goalw [sym_def]
"[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)";
by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
qed "symI";
@@ -35,21 +34,19 @@
(* antisymmetry *)
-val prems = goalw Rel.thy [antisym_def]
+val prems = Goalw [antisym_def]
"[| !!x y.[| <x,y>: r; <y,x>: r |] ==> x=y |] ==> \
\ antisym(r)";
by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
qed "antisymI";
-val prems = goalw Rel.thy [antisym_def]
- "!!r. [| antisym(r); <x,y>: r; <y,x>: r |] ==> x=y";
+Goalw [antisym_def] "[| antisym(r); <x,y>: r; <y,x>: r |] ==> x=y";
by (Blast_tac 1);
qed "antisymE";
(* transitivity *)
-Goalw [trans_def]
- "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
+Goalw [trans_def] "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
by (Blast_tac 1);
qed "transD";
--- a/src/ZF/Sum.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Sum.ML Fri Aug 14 18:37:28 1998 +0200
@@ -22,7 +22,7 @@
val PartI = refl RSN (2,Part_eqI);
-val major::prems = goalw Sum.thy [Part_def]
+val major::prems = Goalw [Part_def]
"[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P \
\ |] ==> P";
by (rtac (major RS CollectE) 1);
@@ -58,7 +58,7 @@
(** Elimination rules **)
-val major::prems = goalw Sum.thy sum_defs
+val major::prems = Goalw sum_defs
"[| u: A+B; \
\ !!x. [| x:A; u=Inl(x) |] ==> P; \
\ !!y. [| y:B; u=Inr(y) |] ==> P \
@@ -141,7 +141,7 @@
Addsimps [case_Inl, case_Inr];
-val major::prems = goal Sum.thy
+val major::prems = Goal
"[| u: A+B; \
\ !!x. x: A ==> c(x): C(Inl(x)); \
\ !!y. y: B ==> d(y): C(Inr(y)) \
@@ -158,7 +158,7 @@
by Auto_tac;
qed "expand_case";
-val major::prems = goal Sum.thy
+val major::prems = Goal
"[| z: A+B; \
\ !!x. x:A ==> c(x)=c'(x); \
\ !!y. y:B ==> d(y)=d'(y) \
--- a/src/ZF/Trancl.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Trancl.ML Fri Aug 14 18:37:28 1998 +0200
@@ -14,9 +14,9 @@
by (Blast_tac 1);
qed "rtrancl_bnd_mono";
-val [prem] = goalw Trancl.thy [rtrancl_def] "r<=s ==> r^* <= s^*";
+Goalw [rtrancl_def] "r<=s ==> r^* <= s^*";
by (rtac lfp_mono 1);
-by (REPEAT (resolve_tac [rtrancl_bnd_mono, prem, subset_refl, id_mono,
+by (REPEAT (ares_tac [rtrancl_bnd_mono, subset_refl, id_mono,
comp_mono, Un_mono, field_mono, Sigma_mono] 1));
qed "rtrancl_mono";
@@ -28,29 +28,27 @@
bind_thm ("rtrancl_type", (rtrancl_def RS def_lfp_subset));
(*Reflexivity of rtrancl*)
-val [prem] = goal Trancl.thy "[| a: field(r) |] ==> <a,a> : r^*";
+Goal "[| a: field(r) |] ==> <a,a> : r^*";
by (resolve_tac [rtrancl_unfold RS ssubst] 1);
-by (rtac (prem RS idI RS UnI1) 1);
+by (etac (idI RS UnI1) 1);
qed "rtrancl_refl";
(*Closure under composition with r *)
-val prems = goal Trancl.thy
- "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*";
+Goal "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*";
by (resolve_tac [rtrancl_unfold RS ssubst] 1);
by (rtac (compI RS UnI2) 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
+by (assume_tac 1);
+by (assume_tac 1);
qed "rtrancl_into_rtrancl";
(*rtrancl of r contains all pairs in r *)
-val prems = goal Trancl.thy "<a,b> : r ==> <a,b> : r^*";
+Goal "<a,b> : r ==> <a,b> : r^*";
by (resolve_tac [rtrancl_refl RS rtrancl_into_rtrancl] 1);
-by (REPEAT (resolve_tac (prems@[fieldI1]) 1));
+by (REPEAT (ares_tac [fieldI1] 1));
qed "r_into_rtrancl";
(*The premise ensures that r consists entirely of pairs*)
-val prems = goal Trancl.thy "r <= Sigma(A,B) ==> r <= r^*";
-by (cut_facts_tac prems 1);
+Goal "r <= Sigma(A,B) ==> r <= r^*";
by (blast_tac (claset() addIs [r_into_rtrancl]) 1);
qed "r_subset_rtrancl";
@@ -62,7 +60,7 @@
(** standard induction rule **)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| <a,b> : r^*; \
\ !!x. x: field(r) ==> P(<x,x>); \
\ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] \
@@ -74,7 +72,7 @@
(*nice induction rule.
Tried adding the typing hypotheses y,z:field(r), but these
caused expensive case splits!*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| <a,b> : r^*; \
\ P(a); \
\ !!y z.[| <a,y> : r^*; <y,z> : r; P(y) |] ==> P(z) \
@@ -96,7 +94,7 @@
qed "trans_rtrancl";
(*elimination of rtrancl -- by induction on a special formula*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| <a,b> : r^*; (a=b) ==> P; \
\ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |] \
\ ==> P";
@@ -147,7 +145,7 @@
qed "rtrancl_into_trancl2";
(*Nice induction rule for trancl*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| <a,b> : r^+; \
\ !!y. [| <a,y> : r |] ==> P(y); \
\ !!y z.[| <a,y> : r^+; <y,z> : r; P(y) |] ==> P(z) \
@@ -162,7 +160,7 @@
qed "trancl_induct";
(*elimination of r^+ -- NOT an induction rule*)
-val major::prems = goal Trancl.thy
+val major::prems = Goal
"[| <a,b> : r^+; \
\ <a,b> : r ==> P; \
\ !!y.[| <a,y> : r^+; <y,b> : r |] ==> P \
@@ -178,7 +176,7 @@
by (blast_tac (claset() addEs [rtrancl_type RS subsetD RS SigmaE2]) 1);
qed "trancl_type";
-val [prem] = goalw Trancl.thy [trancl_def] "r<=s ==> r^+ <= s^+";
-by (REPEAT (resolve_tac [prem, comp_mono, rtrancl_mono] 1));
+Goalw [trancl_def] "r<=s ==> r^+ <= s^+";
+by (REPEAT (ares_tac [comp_mono, rtrancl_mono] 1));
qed "trancl_mono";
--- a/src/ZF/Univ.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Univ.ML Fri Aug 14 18:37:28 1998 +0200
@@ -107,11 +107,10 @@
by (REPEAT (ares_tac [doubleton_in_Vfrom] 1));
qed "Pair_in_Vfrom";
-val [prem] = goal Univ.thy
- "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
+Goal "a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))";
by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1));
by (rtac (Vfrom_mono RSN (2,subset_trans)) 2);
-by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1));
+by (REPEAT (ares_tac [subset_refl, subset_succI] 1));
qed "succ_in_Vfrom";
(*** 0, successor and limit equations fof Vfrom ***)
@@ -140,12 +139,32 @@
(*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces
the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
+Goal "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
+by (stac Vfrom 1);
+by (rtac equalityI 1);
+(*first inclusion*)
+by (rtac Un_least 1);
+by (rtac (A_subset_Vfrom RS subset_trans) 1);
+by (rtac UN_upper 1);
+by (assume_tac 1);
+by (rtac UN_least 1);
+by (etac UnionE 1);
+by (rtac subset_trans 1);
+by (etac UN_upper 2 THEN stac Vfrom 1 THEN
+ etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
+(*opposite inclusion*)
+by (rtac UN_least 1);
+by (stac Vfrom 1);
+by (Blast_tac 1);
+qed "Vfrom_Union";
+
val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
by (stac Vfrom 1);
by (rtac equalityI 1);
(*first inclusion*)
by (rtac Un_least 1);
by (rtac (A_subset_Vfrom RS subset_trans) 1);
+
by (rtac (prem RS UN_upper) 1);
by (rtac UN_least 1);
by (etac UnionE 1);
@@ -175,7 +194,7 @@
by (REPEAT (ares_tac [ltD RS UN_I] 1));
qed "Limit_VfromI";
-val prems = goal Univ.thy
+val prems = Goal
"[| a: Vfrom(A,i); Limit(i); \
\ !!x. [| x<i; a: Vfrom(A,x) |] ==> R \
\ |] ==> R";
@@ -278,8 +297,7 @@
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1);
qed "Transset_Vfrom_succ";
-goalw Ordinal.thy [Pair_def,Transset_def]
- "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
+Goalw [Pair_def,Transset_def] "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
by (Blast_tac 1);
qed "Transset_Pair_subset";
@@ -297,7 +315,7 @@
***)
(*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*)
-val [aprem,bprem,limiti,step] = goal Univ.thy
+val [aprem,bprem,limiti,step] = Goal
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); \
\ !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) \
\ |] ==> EX k. h(x,y): Vfrom(A,k) & k<i |] ==> \
@@ -377,8 +395,7 @@
qed "fun_in_VLimit";
Goalw [Pi_def]
- "[| a: Vfrom(A,j); Transset(A) |] ==> \
-\ Pow(a) : Vfrom(A, succ(succ(j)))";
+ "[| a: Vfrom(A,j); Transset(A) |] ==> Pow(a) : Vfrom(A, succ(succ(j)))";
by (dtac Transset_Vfrom 1);
by (rtac subset_mem_Vfrom 1);
by (rewtac Transset_def);
@@ -406,8 +423,8 @@
(** Characterisation of the elements of Vset(i) **)
-val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
-by (rtac (ordi RS trans_induct) 1);
+Goal "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
+by (etac trans_induct 1);
by (stac Vset 1);
by Safe_tac;
by (stac rank 1);
@@ -416,8 +433,8 @@
by (REPEAT (ares_tac [ltI] 1));
qed_spec_mp "VsetD";
-val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
-by (rtac (ordi RS trans_induct) 1);
+Goal "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
+by (etac trans_induct 1);
by (rtac allI 1);
by (stac Vset 1);
by (blast_tac (claset() addSIs [rank_lt RS ltD]) 1);
@@ -458,7 +475,7 @@
by (etac (rank_lt RS VsetI) 1);
qed "arg_subset_Vset_rank";
-val [iprem] = goal Univ.thy
+val [iprem] = Goal
"[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b";
by (rtac ([subset_refl, arg_subset_Vset_rank] MRS
Int_greatest RS subset_trans) 1);
@@ -490,7 +507,7 @@
qed "Vrec";
(*This form avoids giant explosions in proofs. NOTE USE OF == *)
-val rew::prems = goal Univ.thy
+val rew::prems = Goal
"[| !!x. h(x)==Vrec(x,H) |] ==> \
\ h(a) = H(a, lam x: Vset(rank(a)). h(x))";
by (rewtac rew);
@@ -520,7 +537,7 @@
by (etac (univ_eq_UN RS subst) 1);
qed "subset_univ_eq_Int";
-val [aprem, iprem] = goal Univ.thy
+val [aprem, iprem] = Goal
"[| a <= univ(X); \
\ !!i. i:nat ==> a Int Vfrom(X,i) <= b \
\ |] ==> a <= b";
@@ -529,7 +546,7 @@
by (etac iprem 1);
qed "univ_Int_Vfrom_subset";
-val prems = goal Univ.thy
+val prems = Goal
"[| a <= univ(X); b <= univ(X); \
\ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \
\ |] ==> a = b";
@@ -696,3 +713,37 @@
val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ);
+(**** For QUniv. Properties of Vfrom analogous to the "take-lemma" ****)
+
+(*** Intersecting a*b with Vfrom... ***)
+
+(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
+Goal "[| {a,b} : Vfrom(X,succ(i)); Transset(X) |] \
+\ ==> a: Vfrom(X,i) & b: Vfrom(X,i)";
+by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1);
+by (assume_tac 1);
+by (Fast_tac 1);
+qed "doubleton_in_Vfrom_D";
+
+(*This weaker version says a, b exist at the same level*)
+bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D);
+
+(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
+ implies a, b : Vfrom(X,i), which is useless for induction.
+ Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
+ implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
+ The combination gives a reduction by precisely one level, which is
+ most convenient for proofs.
+**)
+
+Goalw [Pair_def]
+ "[| <a,b> : Vfrom(X,succ(i)); Transset(X) |] \
+\ ==> a: Vfrom(X,i) & b: Vfrom(X,i)";
+by (blast_tac (claset() addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
+qed "Pair_in_Vfrom_D";
+
+Goal "Transset(X) ==> \
+\ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
+by (blast_tac (claset() addSDs [Pair_in_Vfrom_D]) 1);
+qed "product_Int_Vfrom_subset";
+
--- a/src/ZF/WF.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/WF.ML Fri Aug 14 18:37:28 1998 +0200
@@ -48,7 +48,7 @@
(** Introduction rules for wf_on **)
(*If every non-empty subset of A has an r-minimal element then wf[A](r).*)
-val [prem] = goalw WF.thy [wf_on_def, wf_def]
+val [prem] = Goalw [wf_on_def, wf_def]
"[| !!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \
\ ==> wf[A](r)";
by (rtac (equals0I RS disjCI RS allI) 1);
@@ -59,7 +59,7 @@
(*If r allows well-founded induction over A then wf[A](r)
Premise is equivalent to
!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B *)
-val [prem] = goal WF.thy
+val [prem] = Goal
"[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A \
\ |] ==> y:B |] \
\ ==> wf[A](r)";
@@ -74,7 +74,7 @@
(** Well-founded Induction **)
(*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)
-val [major,minor] = goalw WF.thy [wf_def]
+val [major,minor] = Goalw [wf_def]
"[| wf(r); \
\ !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \
\ |] ==> P(a)";
@@ -92,7 +92,7 @@
ares_tac prems i];
(*The form of this rule is designed to match wfI*)
-val wfr::amem::prems = goal WF.thy
+val wfr::amem::prems = Goal
"[| wf(r); a:A; field(r)<=A; \
\ !!x.[| x: A; ALL y. <y,x>: r --> P(y) |] ==> P(x) \
\ |] ==> P(a)";
@@ -103,11 +103,11 @@
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
qed "wf_induct2";
-goal domrange.thy "!!r A. field(r Int A*A) <= A";
+Goal "!!r A. field(r Int A*A) <= A";
by (Blast_tac 1);
qed "field_Int_square";
-val wfr::amem::prems = goalw WF.thy [wf_on_def]
+val wfr::amem::prems = Goalw [wf_on_def]
"[| wf[A](r); a:A; \
\ !!x.[| x: A; ALL y:A. <y,x>: r --> P(y) |] ==> P(x) \
\ |] ==> P(a)";
@@ -122,7 +122,7 @@
REPEAT (ares_tac prems i)];
(*If r allows well-founded induction then wf(r)*)
-val [subs,indhyp] = goal WF.thy
+val [subs,indhyp] = Goal
"[| field(r)<=A; \
\ !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A \
\ |] ==> y:B |] \
@@ -197,9 +197,8 @@
(** is_recfun **)
-val [major] = goalw WF.thy [is_recfun_def]
- "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
-by (stac major 1);
+Goalw [is_recfun_def] "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
+by (etac ssubst 1);
by (rtac (lamI RS rangeI RS lam_type) 1);
by (assume_tac 1);
qed "is_recfun_type";
@@ -245,26 +244,22 @@
(*** Main Existence Lemma ***)
-val prems = goal WF.thy
- "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g";
-by (cut_facts_tac prems 1);
+Goal "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g";
by (rtac fun_extension 1);
by (REPEAT (ares_tac [is_recfun_equal] 1
ORELSE eresolve_tac [is_recfun_type,underD] 1));
qed "is_recfun_functional";
(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
-val prems = goalw WF.thy [the_recfun_def]
+Goalw [the_recfun_def]
"[| is_recfun(r,a,H,f); wf(r); trans(r) |] \
\ ==> is_recfun(r, a, H, the_recfun(r,a,H))";
by (rtac (ex1I RS theI) 1);
-by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1));
+by (REPEAT (ares_tac [is_recfun_functional] 1));
qed "is_the_recfun";
-val prems = goal WF.thy
- "[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
-by (cut_facts_tac prems 1);
-by (wf_ind_tac "a" prems 1);
+Goal "[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
+by (wf_ind_tac "a" [] 1);
by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1);
by (REPEAT (assume_tac 2));
by (rewrite_goals_tac [is_recfun_def, wftrec_def]);
@@ -309,14 +304,14 @@
qed "wfrec";
(*This form avoids giant explosions in proofs. NOTE USE OF == *)
-val rew::prems = goal WF.thy
+val rew::prems = Goal
"[| !!x. h(x)==wfrec(r,x,H); wf(r) |] ==> \
\ h(a) = H(a, lam x: r-``{a}. h(x))";
by (rewtac rew);
by (REPEAT (resolve_tac (prems@[wfrec]) 1));
qed "def_wfrec";
-val prems = goal WF.thy
+val prems = Goal
"[| wf(r); a:A; field(r)<=A; \
\ !!x u. [| x: A; u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x) \
\ |] ==> wfrec(r,a,H) : B(a)";
--- a/src/ZF/Zorn.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/Zorn.ML Fri Aug 14 18:37:28 1998 +0200
@@ -13,11 +13,11 @@
(*** Section 1. Mathematical Preamble ***)
-goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
+Goal "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
by (Blast_tac 1);
qed "Union_lemma0";
-goal ZF.thy
+Goal
"!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
by (Blast_tac 1);
qed "Inter_lemma0";
@@ -45,7 +45,7 @@
(** Structural induction on TFin(S,next) **)
-val major::prems = goal Zorn.thy
+val major::prems = Goal
"[| n: TFin(S,next); \
\ !!x. [| x : TFin(S,next); P(x); next: increasing(S) |] ==> P(next`x); \
\ !!Y. [| Y <= TFin(S,next); ALL y:Y. P(y) |] ==> P(Union(Y)) \
@@ -67,12 +67,10 @@
TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans)));
(*Lemma 1 of section 3.1*)
-val major::prems = goal Zorn.thy
- "[| n: TFin(S,next); m: TFin(S,next); \
-\ ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m \
-\ |] ==> n<=m | next`m<=n";
-by (cut_facts_tac prems 1);
-by (rtac (major RS TFin_induct) 1);
+Goal "[| n: TFin(S,next); m: TFin(S,next); \
+\ ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m \
+\ |] ==> n<=m | next`m<=n";
+by (etac TFin_induct 1);
by (etac Union_lemma0 2); (*or just Blast_tac*)
by (blast_tac (subset_cs addIs [increasing_trans]) 1);
qed "TFin_linear_lemma1";
@@ -123,10 +121,8 @@
(*Lemma 3 of section 3.3*)
-val major::prems = goal Zorn.thy
- "[| n: TFin(S,next); m: TFin(S,next); m = next`m |] ==> n<=m";
-by (cut_facts_tac prems 1);
-by (rtac (major RS TFin_induct) 1);
+Goal "[| n: TFin(S,next); m: TFin(S,next); m = next`m |] ==> n<=m";
+by (etac TFin_induct 1);
by (dtac TFin_subsetD 1);
by (REPEAT (assume_tac 1));
by (fast_tac (claset() addEs [ssubst]) 1);
@@ -276,11 +272,10 @@
(*** Section 6. Zermelo's Theorem: every set can be well-ordered ***)
(*Lemma 5*)
-val major::prems = goal Zorn.thy
+Goal
"[| n: TFin(S,next); Z <= TFin(S,next); z:Z; ~ Inter(Z) : Z \
\ |] ==> ALL m:Z. n<=m";
-by (cut_facts_tac prems 1);
-by (rtac (major RS TFin_induct) 1);
+by (etac TFin_induct 1);
by (Blast_tac 2); (*second induction step is easy*)
by (rtac ballI 1);
by (rtac (bspec RS TFin_subsetD RS disjE) 1);
@@ -324,13 +319,6 @@
(** Defining the "next" operation for Zermelo's Theorem **)
-goal AC.thy
- "!!S. [| ch : (PROD X:Pow(S) - {0}. X); X<=S; X~=S \
-\ |] ==> ch ` (S-X) : S-X";
-by (etac apply_type 1);
-by (blast_tac (claset() addSEs [equalityE]) 1);
-qed "choice_Diff";
-
(*This justifies Definition 6.1*)
Goal "ch: (PROD X: Pow(S)-{0}. X) ==> \
\ EX next: increasing(S). ALL X: Pow(S). \
--- a/src/ZF/equalities.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/equalities.ML Fri Aug 14 18:37:28 1998 +0200
@@ -10,23 +10,23 @@
(** Finite Sets **)
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
-goal ZF.thy "{a} Un B = cons(a,B)";
+Goal "{a} Un B = cons(a,B)";
by (Blast_tac 1);
qed "cons_eq";
-goal ZF.thy "cons(a, cons(b, C)) = cons(b, cons(a, C))";
+Goal "cons(a, cons(b, C)) = cons(b, cons(a, C))";
by (Blast_tac 1);
qed "cons_commute";
-goal ZF.thy "!!B. a: B ==> cons(a,B) = B";
+Goal "a: B ==> cons(a,B) = B";
by (Blast_tac 1);
qed "cons_absorb";
-goal ZF.thy "!!B. a: B ==> cons(a, B-{a}) = B";
+Goal "a: B ==> cons(a, B-{a}) = B";
by (Blast_tac 1);
qed "cons_Diff";
-goal ZF.thy "!!C. [| a: C; ALL y:C. y=b |] ==> C = {b}";
+Goal "[| a: C; ALL y:C. y=b |] ==> C = {b}";
by (Blast_tac 1);
qed "equal_singleton_lemma";
val equal_singleton = ballI RSN (2,equal_singleton_lemma);
@@ -35,150 +35,150 @@
(** Binary Intersection **)
(*NOT an equality, but it seems to belong here...*)
-goal ZF.thy "cons(a,B) Int C <= cons(a, B Int C)";
+Goal "cons(a,B) Int C <= cons(a, B Int C)";
by (Blast_tac 1);
qed "Int_cons";
-goal ZF.thy "A Int A = A";
+Goal "A Int A = A";
by (Blast_tac 1);
qed "Int_absorb";
-goal ZF.thy "A Int B = B Int A";
+Goal "A Int B = B Int A";
by (Blast_tac 1);
qed "Int_commute";
-goal ZF.thy "(A Int B) Int C = A Int (B Int C)";
+Goal "(A Int B) Int C = A Int (B Int C)";
by (Blast_tac 1);
qed "Int_assoc";
-goal ZF.thy "(A Un B) Int C = (A Int C) Un (B Int C)";
+Goal "(A Un B) Int C = (A Int C) Un (B Int C)";
by (Blast_tac 1);
qed "Int_Un_distrib";
-goal ZF.thy "A<=B <-> A Int B = A";
+Goal "A<=B <-> A Int B = A";
by (blast_tac (claset() addSEs [equalityE]) 1);
qed "subset_Int_iff";
-goal ZF.thy "A<=B <-> B Int A = A";
+Goal "A<=B <-> B Int A = A";
by (blast_tac (claset() addSEs [equalityE]) 1);
qed "subset_Int_iff2";
-goal ZF.thy "!!A B C. C<=A ==> (A-B) Int C = C-B";
+Goal "C<=A ==> (A-B) Int C = C-B";
by (Blast_tac 1);
qed "Int_Diff_eq";
(** Binary Union **)
-goal ZF.thy "cons(a,B) Un C = cons(a, B Un C)";
+Goal "cons(a,B) Un C = cons(a, B Un C)";
by (Blast_tac 1);
qed "Un_cons";
-goal ZF.thy "A Un A = A";
+Goal "A Un A = A";
by (Blast_tac 1);
qed "Un_absorb";
-goal ZF.thy "A Un B = B Un A";
+Goal "A Un B = B Un A";
by (Blast_tac 1);
qed "Un_commute";
-goal ZF.thy "(A Un B) Un C = A Un (B Un C)";
+Goal "(A Un B) Un C = A Un (B Un C)";
by (Blast_tac 1);
qed "Un_assoc";
-goal ZF.thy "(A Int B) Un C = (A Un C) Int (B Un C)";
+Goal "(A Int B) Un C = (A Un C) Int (B Un C)";
by (Blast_tac 1);
qed "Un_Int_distrib";
-goal ZF.thy "A<=B <-> A Un B = B";
+Goal "A<=B <-> A Un B = B";
by (blast_tac (claset() addSEs [equalityE]) 1);
qed "subset_Un_iff";
-goal ZF.thy "A<=B <-> B Un A = B";
+Goal "A<=B <-> B Un A = B";
by (blast_tac (claset() addSEs [equalityE]) 1);
qed "subset_Un_iff2";
(** Simple properties of Diff -- set difference **)
-goal ZF.thy "A-A = 0";
+Goal "A-A = 0";
by (Blast_tac 1);
qed "Diff_cancel";
-goal ZF.thy "0-A = 0";
+Goal "0-A = 0";
by (Blast_tac 1);
qed "empty_Diff";
-goal ZF.thy "A-0 = A";
+Goal "A-0 = A";
by (Blast_tac 1);
qed "Diff_0";
-goal ZF.thy "A-B=0 <-> A<=B";
+Goal "A-B=0 <-> A<=B";
by (blast_tac (claset() addEs [equalityE]) 1);
qed "Diff_eq_0_iff";
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
-goal ZF.thy "A - cons(a,B) = A - B - {a}";
+Goal "A - cons(a,B) = A - B - {a}";
by (Blast_tac 1);
qed "Diff_cons";
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
-goal ZF.thy "A - cons(a,B) = A - {a} - B";
+Goal "A - cons(a,B) = A - {a} - B";
by (Blast_tac 1);
qed "Diff_cons2";
-goal ZF.thy "A Int (B-A) = 0";
+Goal "A Int (B-A) = 0";
by (Blast_tac 1);
qed "Diff_disjoint";
-goal ZF.thy "!!A B. A<=B ==> A Un (B-A) = B";
+Goal "A<=B ==> A Un (B-A) = B";
by (Blast_tac 1);
qed "Diff_partition";
-goal ZF.thy "A <= B Un (A - B)";
+Goal "A <= B Un (A - B)";
by (Blast_tac 1);
qed "subset_Un_Diff";
-goal ZF.thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A";
+Goal "[| A<=B; B<=C |] ==> B-(C-A) = A";
by (Blast_tac 1);
qed "double_complement";
-goal ZF.thy "(A Un B) - (B-A) = A";
+Goal "(A Un B) - (B-A) = A";
by (Blast_tac 1);
qed "double_complement_Un";
-goal ZF.thy
+Goal
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
by (Blast_tac 1);
qed "Un_Int_crazy";
-goal ZF.thy "A - (B Un C) = (A-B) Int (A-C)";
+Goal "A - (B Un C) = (A-B) Int (A-C)";
by (Blast_tac 1);
qed "Diff_Un";
-goal ZF.thy "A - (B Int C) = (A-B) Un (A-C)";
+Goal "A - (B Int C) = (A-B) Un (A-C)";
by (Blast_tac 1);
qed "Diff_Int";
(*Halmos, Naive Set Theory, page 16.*)
-goal ZF.thy "(A Int B) Un C = A Int (B Un C) <-> C<=A";
+Goal "(A Int B) Un C = A Int (B Un C) <-> C<=A";
by (blast_tac (claset() addSEs [equalityE]) 1);
qed "Un_Int_assoc_iff";
(** Big Union and Intersection **)
-goal ZF.thy "Union(cons(a,B)) = a Un Union(B)";
+Goal "Union(cons(a,B)) = a Un Union(B)";
by (Blast_tac 1);
qed "Union_cons";
-goal ZF.thy "Union(A Un B) = Union(A) Un Union(B)";
+Goal "Union(A Un B) = Union(A) Un Union(B)";
by (Blast_tac 1);
qed "Union_Un_distrib";
-goal ZF.thy "Union(A Int B) <= Union(A) Int Union(B)";
+Goal "Union(A Int B) <= Union(A) Int Union(B)";
by (Blast_tac 1);
qed "Union_Int_subset";
-goal ZF.thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
+Goal "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
by (blast_tac (claset() addSEs [equalityE]) 1);
qed "Union_disjoint";
@@ -186,26 +186,26 @@
by (Blast_tac 1);
qed "Inter_0";
-goal ZF.thy "!!A B. [| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
+Goal "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
by (Blast_tac 1);
qed "Inter_Un_subset";
(* A good challenge: Inter is ill-behaved on the empty set *)
-goal ZF.thy "!!A B. [| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
+Goal "[| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
by (Blast_tac 1);
qed "Inter_Un_distrib";
-goal ZF.thy "Union({b}) = b";
+Goal "Union({b}) = b";
by (Blast_tac 1);
qed "Union_singleton";
-goal ZF.thy "Inter({b}) = b";
+Goal "Inter({b}) = b";
by (Blast_tac 1);
qed "Inter_singleton";
(** Unions and Intersections of Families **)
-goal ZF.thy "Union(A) = (UN x:A. x)";
+Goal "Union(A) = (UN x:A. x)";
by (Blast_tac 1);
qed "Union_eq_UN";
@@ -213,43 +213,41 @@
by (Blast_tac 1);
qed "Inter_eq_INT";
-goal ZF.thy "(UN i:0. A(i)) = 0";
+Goal "(UN i:0. A(i)) = 0";
by (Blast_tac 1);
qed "UN_0";
(*Halmos, Naive Set Theory, page 35.*)
-goal ZF.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
+Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
by (Blast_tac 1);
qed "Int_UN_distrib";
-goal ZF.thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
+Goal "i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
by (Blast_tac 1);
qed "Un_INT_distrib";
-goal ZF.thy
- "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
+Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
by (Blast_tac 1);
qed "Int_UN_distrib2";
-goal ZF.thy
- "!!I J. [| i:I; j:J |] ==> \
-\ (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
+Goal "[| i:I; j:J |] ==> \
+\ (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
by (Blast_tac 1);
qed "Un_INT_distrib2";
-goal ZF.thy "!!A. a: A ==> (UN y:A. c) = c";
+Goal "a: A ==> (UN y:A. c) = c";
by (Blast_tac 1);
qed "UN_constant";
-goal ZF.thy "!!A. a: A ==> (INT y:A. c) = c";
+Goal "a: A ==> (INT y:A. c) = c";
by (Blast_tac 1);
qed "INT_constant";
-goal ZF.thy "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))";
+Goal "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))";
by (Blast_tac 1);
qed "UN_RepFun";
-goal ZF.thy "!!x. x:A ==> (INT y: RepFun(A,f). B(y)) = (INT x:A. B(f(x)))";
+Goal "x:A ==> (INT y: RepFun(A,f). B(y)) = (INT x:A. B(f(x)))";
by (Blast_tac 1);
qed "INT_RepFun";
@@ -259,94 +257,92 @@
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
Union of a family of unions **)
-goal ZF.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))";
+Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))";
by (Blast_tac 1);
qed "UN_Un_distrib";
-goal ZF.thy
- "!!A B. i:I ==> \
-\ (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
+Goal "i:I ==> (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
by (Blast_tac 1);
qed "INT_Int_distrib";
-goal ZF.thy "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))";
+Goal "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))";
by (Blast_tac 1);
qed "UN_Int_subset";
(** Devlin, page 12, exercise 5: Complements **)
-goal ZF.thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
+Goal "i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
by (Blast_tac 1);
qed "Diff_UN";
-goal ZF.thy "!!A B. i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))";
+Goal "i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))";
by (Blast_tac 1);
qed "Diff_INT";
(** Unions and Intersections with General Sum **)
(*Not suitable for rewriting: LOOPS!*)
-goal ZF.thy "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)";
+Goal "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)";
by (Blast_tac 1);
qed "Sigma_cons1";
(*Not suitable for rewriting: LOOPS!*)
-goal ZF.thy "A * cons(b,B) = A*{b} Un A*B";
+Goal "A * cons(b,B) = A*{b} Un A*B";
by (Blast_tac 1);
qed "Sigma_cons2";
-goal ZF.thy "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)";
+Goal "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)";
by (Blast_tac 1);
qed "Sigma_succ1";
-goal ZF.thy "A * succ(B) = A*{B} Un A*B";
+Goal "A * succ(B) = A*{B} Un A*B";
by (Blast_tac 1);
qed "Sigma_succ2";
-goal ZF.thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
+Goal "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
by (Blast_tac 1);
qed "SUM_UN_distrib1";
-goal ZF.thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
+Goal "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
by (Blast_tac 1);
qed "SUM_UN_distrib2";
-goal ZF.thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
+Goal "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
by (Blast_tac 1);
qed "SUM_Un_distrib1";
-goal ZF.thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
+Goal "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
by (Blast_tac 1);
qed "SUM_Un_distrib2";
(*First-order version of the above, for rewriting*)
-goal ZF.thy "I * (A Un B) = I*A Un I*B";
+Goal "I * (A Un B) = I*A Un I*B";
by (rtac SUM_Un_distrib2 1);
qed "prod_Un_distrib2";
-goal ZF.thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
+Goal "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
by (Blast_tac 1);
qed "SUM_Int_distrib1";
-goal ZF.thy
- "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
+Goal "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
by (Blast_tac 1);
qed "SUM_Int_distrib2";
(*First-order version of the above, for rewriting*)
-goal ZF.thy "I * (A Int B) = I*A Int I*B";
+Goal "I * (A Int B) = I*A Int I*B";
by (rtac SUM_Int_distrib2 1);
qed "prod_Int_distrib2";
(*Cf Aczel, Non-Well-Founded Sets, page 115*)
-goal ZF.thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
+Goal "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
by (Blast_tac 1);
qed "SUM_eq_UN";
(** Domain **)
-qed_goal "domain_of_prod" ZF.thy "!!A B. b:B ==> domain(A*B) = A"
- (fn _ => [ Blast_tac 1 ]);
+Goal "b:B ==> domain(A*B) = A";
+by (Blast_tac 1);
+qed "domain_of_prod";
qed_goal "domain_0" ZF.thy "domain(0) = 0"
(fn _ => [ Blast_tac 1 ]);
@@ -355,19 +351,19 @@
"domain(cons(<a,b>,r)) = cons(a, domain(r))"
(fn _ => [ Blast_tac 1 ]);
-goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";
+Goal "domain(A Un B) = domain(A) Un domain(B)";
by (Blast_tac 1);
qed "domain_Un_eq";
-goal ZF.thy "domain(A Int B) <= domain(A) Int domain(B)";
+Goal "domain(A Int B) <= domain(A) Int domain(B)";
by (Blast_tac 1);
qed "domain_Int_subset";
-goal ZF.thy "domain(A) - domain(B) <= domain(A - B)";
+Goal "domain(A) - domain(B) <= domain(A - B)";
by (Blast_tac 1);
qed "domain_Diff_subset";
-goal ZF.thy "domain(converse(r)) = range(r)";
+Goal "domain(converse(r)) = range(r)";
by (Blast_tac 1);
qed "domain_converse";
@@ -376,9 +372,9 @@
(** Range **)
-qed_goal "range_of_prod" ZF.thy
- "!!a A B. a:A ==> range(A*B) = B"
- (fn _ => [ Blast_tac 1 ]);
+Goal "a:A ==> range(A*B) = B";
+by (Blast_tac 1);
+qed "range_of_prod";
qed_goal "range_0" ZF.thy "range(0) = 0"
(fn _ => [ Blast_tac 1 ]);
@@ -387,19 +383,19 @@
"range(cons(<a,b>,r)) = cons(b, range(r))"
(fn _ => [ Blast_tac 1 ]);
-goal ZF.thy "range(A Un B) = range(A) Un range(B)";
+Goal "range(A Un B) = range(A) Un range(B)";
by (Blast_tac 1);
qed "range_Un_eq";
-goal ZF.thy "range(A Int B) <= range(A) Int range(B)";
+Goal "range(A Int B) <= range(A) Int range(B)";
by (Blast_tac 1);
qed "range_Int_subset";
-goal ZF.thy "range(A) - range(B) <= range(A - B)";
+Goal "range(A) - range(B) <= range(A - B)";
by (Blast_tac 1);
qed "range_Diff_subset";
-goal ZF.thy "range(converse(r)) = domain(r)";
+Goal "range(converse(r)) = domain(r)";
by (Blast_tac 1);
qed "range_converse";
@@ -418,19 +414,19 @@
"field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
(fn _ => [ rtac equalityI 1, ALLGOALS (Blast_tac) ]);
-goal ZF.thy "field(A Un B) = field(A) Un field(B)";
+Goal "field(A Un B) = field(A) Un field(B)";
by (Blast_tac 1);
qed "field_Un_eq";
-goal ZF.thy "field(A Int B) <= field(A) Int field(B)";
+Goal "field(A Int B) <= field(A) Int field(B)";
by (Blast_tac 1);
qed "field_Int_subset";
-goal ZF.thy "field(A) - field(B) <= field(A - B)";
+Goal "field(A) - field(B) <= field(A - B)";
by (Blast_tac 1);
qed "field_Diff_subset";
-goal ZF.thy "field(converse(r)) = field(r)";
+Goal "field(converse(r)) = field(r)";
by (Blast_tac 1);
qed "field_converse";
@@ -439,72 +435,74 @@
(** Image **)
-goal ZF.thy "r``0 = 0";
+Goal "r``0 = 0";
by (Blast_tac 1);
qed "image_0";
-goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)";
+Goal "r``(A Un B) = (r``A) Un (r``B)";
by (Blast_tac 1);
qed "image_Un";
-goal ZF.thy "r``(A Int B) <= (r``A) Int (r``B)";
+Goal "r``(A Int B) <= (r``A) Int (r``B)";
by (Blast_tac 1);
qed "image_Int_subset";
-goal ZF.thy "(r Int A*A)``B <= (r``B) Int A";
+Goal "(r Int A*A)``B <= (r``B) Int A";
by (Blast_tac 1);
qed "image_Int_square_subset";
-goal ZF.thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";
+Goal "B<=A ==> (r Int A*A)``B = (r``B) Int A";
by (Blast_tac 1);
qed "image_Int_square";
Addsimps [image_0, image_Un];
(*Image laws for special relations*)
-goal ZF.thy "0``A = 0";
+Goal "0``A = 0";
by (Blast_tac 1);
qed "image_0_left";
Addsimps [image_0_left];
-goal ZF.thy "(r Un s)``A = (r``A) Un (s``A)";
+Goal "(r Un s)``A = (r``A) Un (s``A)";
by (Blast_tac 1);
qed "image_Un_left";
-goal ZF.thy "(r Int s)``A <= (r``A) Int (s``A)";
+Goal "(r Int s)``A <= (r``A) Int (s``A)";
by (Blast_tac 1);
qed "image_Int_subset_left";
(** Inverse Image **)
-goal ZF.thy "r-``0 = 0";
+Goal "r-``0 = 0";
by (Blast_tac 1);
qed "vimage_0";
-goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)";
+Goal "r-``(A Un B) = (r-``A) Un (r-``B)";
by (Blast_tac 1);
qed "vimage_Un";
-goal ZF.thy "r-``(A Int B) <= (r-``A) Int (r-``B)";
+Goal "r-``(A Int B) <= (r-``A) Int (r-``B)";
by (Blast_tac 1);
qed "vimage_Int_subset";
-Goalw [function_def]
- "function(f) ==> f-``(A Int B) = (f-``A) Int (f-``B)";
+Goalw [function_def] "function(f) ==> f-``(A Int B) = (f-``A) Int (f-``B)";
by (Blast_tac 1);
qed "function_vimage_Int";
-Goalw [function_def]
- "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)";
+Goalw [function_def] "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)";
by (Blast_tac 1);
qed "function_vimage_Diff";
-goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A";
+Goalw [function_def] "function(f) ==> f `` (f-`` A) <= A";
+by (Blast_tac 1);
+qed "function_image_vimage";
+
+Goal "(r Int A*A)-``B <= (r-``B) Int A";
by (Blast_tac 1);
qed "vimage_Int_square_subset";
-goal ZF.thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
+Goal "B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
by (Blast_tac 1);
qed "vimage_Int_square";
@@ -512,35 +510,35 @@
(*Invese image laws for special relations*)
-goal ZF.thy "0-``A = 0";
+Goal "0-``A = 0";
by (Blast_tac 1);
qed "vimage_0_left";
Addsimps [vimage_0_left];
-goal ZF.thy "(r Un s)-``A = (r-``A) Un (s-``A)";
+Goal "(r Un s)-``A = (r-``A) Un (s-``A)";
by (Blast_tac 1);
qed "vimage_Un_left";
-goal ZF.thy "(r Int s)-``A <= (r-``A) Int (s-``A)";
+Goal "(r Int s)-``A <= (r-``A) Int (s-``A)";
by (Blast_tac 1);
qed "vimage_Int_subset_left";
(** Converse **)
-goal ZF.thy "converse(A Un B) = converse(A) Un converse(B)";
+Goal "converse(A Un B) = converse(A) Un converse(B)";
by (Blast_tac 1);
qed "converse_Un";
-goal ZF.thy "converse(A Int B) = converse(A) Int converse(B)";
+Goal "converse(A Int B) = converse(A) Int converse(B)";
by (Blast_tac 1);
qed "converse_Int";
-goal ZF.thy "converse(A - B) = converse(A) - converse(B)";
+Goal "converse(A - B) = converse(A) - converse(B)";
by (Blast_tac 1);
qed "converse_Diff";
-goal ZF.thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
+Goal "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
by (Blast_tac 1);
qed "converse_UN";
@@ -553,27 +551,27 @@
(** Pow **)
-goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";
+Goal "Pow(A) Un Pow(B) <= Pow(A Un B)";
by (Blast_tac 1);
qed "Un_Pow_subset";
-goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
+Goal "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
by (Blast_tac 1);
qed "UN_Pow_subset";
-goal ZF.thy "A <= Pow(Union(A))";
+Goal "A <= Pow(Union(A))";
by (Blast_tac 1);
qed "subset_Pow_Union";
-goal ZF.thy "Union(Pow(A)) = A";
+Goal "Union(Pow(A)) = A";
by (Blast_tac 1);
qed "Union_Pow_eq";
-goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
+Goal "Pow(A Int B) = Pow(A) Int Pow(B)";
by (Blast_tac 1);
qed "Int_Pow_eq";
-goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
+Goal "x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
by (Blast_tac 1);
qed "INT_Pow_subset";
@@ -581,26 +579,26 @@
(** RepFun **)
-goal ZF.thy "{f(x).x:A}=0 <-> A=0";
+Goal "{f(x).x:A}=0 <-> A=0";
(*blast_tac takes too long to find a good depth*)
by (Blast.depth_tac (claset() addSEs [equalityE]) 10 1);
qed "RepFun_eq_0_iff";
(** Collect **)
-goal ZF.thy "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
+Goal "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
by (Blast_tac 1);
qed "Collect_Un";
-goal ZF.thy "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)";
+Goal "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)";
by (Blast_tac 1);
qed "Collect_Int";
-goal ZF.thy "Collect(A - B, P) = Collect(A,P) - Collect(B,P)";
+Goal "Collect(A - B, P) = Collect(A,P) - Collect(B,P)";
by (Blast_tac 1);
qed "Collect_Diff";
-goal ZF.thy "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
+Goal "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
by (simp_tac (simpset() addsplits [split_if]) 1);
by (Blast_tac 1);
qed "Collect_cons";
--- a/src/ZF/func.ML Fri Aug 14 13:52:42 1998 +0200
+++ b/src/ZF/func.ML Fri Aug 14 18:37:28 1998 +0200
@@ -389,25 +389,23 @@
(*** Extensions of functions ***)
-goal ZF.thy
- "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
+Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
by (forward_tac [singleton_fun RS fun_disjoint_Un] 1);
by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2);
by (Blast_tac 1);
qed "fun_extend";
-goal ZF.thy
- "!!f A B. [| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
+Goal "[| f: A->B; c~:A; b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
by (blast_tac (claset() addIs [fun_extend RS fun_weaken_type]) 1);
qed "fun_extend3";
-goal ZF.thy "!!f A B. [| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a";
+Goal "[| f: A->B; a:A; c~:A |] ==> cons(<c,b>,f)`a = f`a";
by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
by (rtac fun_extend 3);
by (REPEAT (assume_tac 1));
qed "fun_extend_apply1";
-goal ZF.thy "!!f A B. [| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b";
+Goal "[| f: A->B; c~:A |] ==> cons(<c,b>,f)`c = b";
by (rtac (consI1 RS apply_equality) 1);
by (rtac fun_extend 1);
by (REPEAT (assume_tac 1));
@@ -417,8 +415,7 @@
Addsimps [singleton_apply];
(*For Finite.ML. Inclusion of right into left is easy*)
-goal ZF.thy
- "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
+Goal "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
by (rtac equalityI 1);
by (safe_tac (claset() addSEs [fun_extend3]));
(*Inclusion of left into right*)