--- a/src/ZF/IsaMakefile Tue May 21 13:06:36 2002 +0200
+++ b/src/ZF/IsaMakefile Tue May 21 18:25:28 2002 +0200
@@ -39,7 +39,7 @@
Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy \
Main_ZFC.ML Main_ZFC.thy \
Nat.ML Nat.thy Order.thy OrderArith.thy \
- OrderType.thy Ordinal.thy OrdQuant.ML OrdQuant.thy Perm.ML Perm.thy \
+ OrderType.thy Ordinal.thy OrdQuant.thy Perm.ML Perm.thy \
QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML \
Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \
Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \
--- a/src/ZF/OrdQuant.ML Tue May 21 13:06:36 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,116 +0,0 @@
-(* Title: ZF/OrdQuant.ML
- ID: $Id$
- Authors: Krzysztof Grabczewski and L C Paulson
-
-Quantifiers and union operator for ordinals.
-*)
-
-val oall_def = thm "oall_def";
-val oex_def = thm "oex_def";
-val OUnion_def = thm "OUnion_def";
-
-(*** universal quantifier for ordinals ***)
-
-val prems = Goalw [oall_def]
- "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)";
-by (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ;
-qed "oallI";
-
-Goalw [oall_def] "[| ALL x<A. P(x); x<A |] ==> P(x)";
-by (etac (spec RS mp) 1);
-by (assume_tac 1) ;
-qed "ospec";
-
-val major::prems = Goalw [oall_def]
- "[| ALL x<A. P(x); P(x) ==> Q; ~x<A ==> Q |] ==> Q";
-by (rtac (major RS allE) 1);
-by (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ;
-qed "oallE";
-
-val major::prems = Goal
- "[| ALL x<A. P(x); ~x<A ==> Q; P(x) ==> Q |] ==> Q";
-by (rtac (major RS oallE) 1);
-by (REPEAT (eresolve_tac prems 1)) ;
-qed "rev_oallE";
-
-(*Trival rewrite rule; (ALL x<a.P)<->P holds only if a is not 0!*)
-Goal "(ALL x<a. True) <-> True";
-by (REPEAT (ares_tac [TrueI,oallI,iffI] 1)) ;
-qed "oall_simp";
-
-(*Congruence rule for rewriting*)
-val prems = Goalw [oall_def]
- "[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')";
-by (simp_tac (simpset() addsimps prems) 1) ;
-qed "oall_cong";
-
-
-(*** existential quantifier for ordinals ***)
-
-val prems = Goalw [oex_def]
- "[| P(x); x<A |] ==> EX x<A. P(x)";
-by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ;
-qed "oexI";
-
-(*Not of the general form for such rules; ~EX has become ALL~ *)
-val prems = Goal
- "[| ALL x<A. ~P(x) ==> P(a); a<A |] ==> EX x<A. P(x)";
-by (rtac classical 1);
-by (REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ;
-qed "oexCI";
-
-val major::prems = Goalw [oex_def]
- "[| EX x<A. P(x); !!x. [| x<A; P(x) |] ==> Q \
-\ |] ==> Q";
-by (rtac (major RS exE) 1);
-by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ;
-qed "oexE";
-
-val prems = Goalw [oex_def]
- "[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) \
-\ |] ==> oex(a,P) <-> oex(a',P')";
-by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1) ;
-qed "oex_cong";
-
-
-(*** Rules for Ordinal-Indexed Unions ***)
-
-Goalw [OUnion_def] "[| a<i; b: B(a) |] ==> b: (UN z<i. B(z))";
-by (blast_tac (claset() addSEs [ltE]) 1);
-qed "OUN_I";
-
-val major::prems = Goalw [OUnion_def]
- "[| b : (UN z<i. B(z)); !!a.[| b: B(a); a<i |] ==> R |] ==> R";
-by (rtac (major RS CollectE) 1);
-by (rtac UN_E 1);
-by (REPEAT (ares_tac (ltI::prems) 1)) ;
-qed "OUN_E";
-
-Goalw [oex_def] "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))";
-by (fast_tac (claset() addIs [OUN_I] addSEs [OUN_E]) 1) ;
-qed "OUN_iff";
-
-val prems = Goal
- "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))";
-by (rtac equality_iffI 1);
-by (simp_tac (simpset() addcongs [oex_cong] addsimps OUN_iff::prems) 1) ;
-qed "OUN_cong";
-
-AddSIs [oallI];
-AddIs [oexI, OUN_I];
-AddSEs [oexE, OUN_E];
-AddEs [rev_oallE];
-
-val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
-
-simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
- addsimps [oall_simp, ltD RS beta]
- addcongs [oall_cong, oex_cong, OUN_cong];
-
-val major::prems = Goalw [lt_def, oall_def]
- "[| i<k; !!x.[| x<k; ALL y<x. P(y) |] ==> P(x) \
-\ |] ==> P(i)";
-by (rtac (major RS conjE) 1);
-by (etac Ord_induct 1 THEN assume_tac 1);
-by (fast_tac (claset() addIs prems) 1);
-qed "lt_induct";
--- a/src/ZF/OrdQuant.thy Tue May 21 13:06:36 2002 +0200
+++ b/src/ZF/OrdQuant.thy Tue May 21 18:25:28 2002 +0200
@@ -39,8 +39,8 @@
(** simplification of the new quantifiers **)
-(*MOST IMPORTANT that this is added to the simpset BEFORE OrdQuant.ML
- is loaded: it's Ord_atomize would convert this rule to
+(*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize
+ is proved. Ord_atomize would convert this rule to
x < 0 ==> P(x) == True, which causes dire effects!*)
lemma [simp]: "(ALL x<0. P(x))"
by (simp add: oall_def)
@@ -199,4 +199,124 @@
"(!!x. x<A ==> P(x)) == Trueprop (ALL x<A. P(x))"
by (simp add: oall_def atomize_all atomize_imp)
+(*** universal quantifier for ordinals ***)
+
+lemma oallI [intro!]:
+ "[| !!x. x<A ==> P(x) |] ==> ALL x<A. P(x)"
+by (simp add: oall_def);
+
+lemma ospec: "[| ALL x<A. P(x); x<A |] ==> P(x)"
+by (simp add: oall_def);
+
+lemma oallE:
+ "[| ALL x<A. P(x); P(x) ==> Q; ~x<A ==> Q |] ==> Q"
+apply (simp add: oall_def);
+apply (blast intro: elim:);
+done
+
+lemma rev_oallE [elim]:
+ "[| ALL x<A. P(x); ~x<A ==> Q; P(x) ==> Q |] ==> Q"
+apply (simp add: oall_def);
+apply (blast intro: elim:);
+done
+
+
+(*Trival rewrite rule; (ALL x<a.P)<->P holds only if a is not 0!*)
+lemma oall_simp [simp]: "(ALL x<a. True) <-> True"
+apply (blast intro: elim:);
+done
+
+(*Congruence rule for rewriting*)
+lemma oall_cong [cong]:
+ "[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) |] ==> oall(a,P) <-> oall(a',P')"
+by (simp add: oall_def)
+
+
+(*** existential quantifier for ordinals ***)
+
+lemma oexI [intro]:
+ "[| P(x); x<A |] ==> EX x<A. P(x)"
+apply (simp add: oex_def);
+apply (blast intro: elim:);
+done
+
+(*Not of the general form for such rules; ~EX has become ALL~ *)
+lemma oexCI:
+ "[| ALL x<A. ~P(x) ==> P(a); a<A |] ==> EX x<A. P(x)"
+apply (simp add: oex_def);
+apply (blast intro: elim:);
+done
+
+lemma oexE [elim!]:
+ "[| EX x<A. P(x); !!x. [| x<A; P(x) |] ==> Q |] ==> Q"
+apply (simp add: oex_def);
+apply (blast intro: elim:);
+done
+
+lemma oex_cong [cong]:
+ "[| a=a'; !!x. x<a' ==> P(x) <-> P'(x) |] ==> oex(a,P) <-> oex(a',P')"
+apply (simp add: oex_def cong add: conj_cong)
+done
+
+
+(*** Rules for Ordinal-Indexed Unions ***)
+
+lemma OUN_I [intro]: "[| a<i; b: B(a) |] ==> b: (UN z<i. B(z))"
+apply (unfold OUnion_def lt_def)
+apply (blast)
+done
+
+lemma OUN_E [elim!]:
+ "[| b : (UN z<i. B(z)); !!a.[| b: B(a); a<i |] ==> R |] ==> R"
+apply (unfold OUnion_def lt_def)
+apply (blast)
+done
+
+lemma OUN_iff: "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
+apply (unfold OUnion_def oex_def lt_def)
+apply (blast intro: elim:);
+done
+
+lemma OUN_cong [cong]:
+ "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
+by (simp add: OUnion_def lt_def OUN_iff)
+
+declare ltD [THEN beta, simp]
+
+
+lemma lt_induct:
+ "[| i<k; !!x.[| x<k; ALL y<x. P(y) |] ==> P(x) |] ==> P(i)"
+apply (simp add: lt_def oall_def)
+apply (erule conjE)
+apply (erule Ord_induct, assumption)
+apply (blast intro: elim:);
+done
+
+ML
+{*
+val oall_def = thm "oall_def"
+val oex_def = thm "oex_def"
+val OUnion_def = thm "OUnion_def"
+
+val oallI = thm "oallI";
+val ospec = thm "ospec";
+val oallE = thm "oallE";
+val rev_oallE = thm "rev_oallE";
+val oall_simp = thm "oall_simp";
+val oall_cong = thm "oall_cong";
+val oexI = thm "oexI";
+val oexCI = thm "oexCI";
+val oexE = thm "oexE";
+val oex_cong = thm "oex_cong";
+val OUN_I = thm "OUN_I";
+val OUN_E = thm "OUN_E";
+val OUN_iff = thm "OUN_iff";
+val OUN_cong = thm "OUN_cong";
+val lt_induct = thm "lt_induct";
+
+val Ord_atomize =
+ atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs);
+simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
+*}
+
end
--- a/src/ZF/domrange.ML Tue May 21 13:06:36 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,233 +0,0 @@
-(* Title: ZF/domrange
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Converse, domain, range of a relation or function
-*)
-
-(*** converse ***)
-
-Goalw [converse_def] "<a,b>: converse(r) <-> <b,a>:r";
-by (Blast_tac 1) ;
-qed "converse_iff";
-
-Goalw [converse_def] "<a,b>:r ==> <b,a>:converse(r)";
-by (Blast_tac 1) ;
-qed "converseI";
-
-Goalw [converse_def] "<a,b> : converse(r) ==> <b,a> : r";
-by (Blast_tac 1) ;
-qed "converseD";
-
-val [major,minor]= Goalw [converse_def]
- "[| yx : converse(r); \
-\ !!x y. [| yx=<y,x>; <x,y>:r |] ==> P \
-\ |] ==> P";
-by (rtac (major RS ReplaceE) 1);
-by (REPEAT (eresolve_tac [exE, conjE, minor] 1));
-by (hyp_subst_tac 1);
-by (assume_tac 1) ;
-qed "converseE";
-
-Addsimps [converse_iff];
-AddSIs [converseI];
-AddSEs [converseD,converseE];
-
-Goal "r<=Sigma(A,B) ==> converse(converse(r)) = r";
-by (Blast_tac 1) ;
-qed "converse_converse";
-
-Goal "r<=A*B ==> converse(r)<=B*A";
-by (Blast_tac 1) ;
-qed "converse_type";
-
-Goal "converse(A*B) = B*A";
-by (Blast_tac 1) ;
-qed "converse_prod";
-
-Goal "converse(0) = 0";
-by (Blast_tac 1) ;
-qed "converse_empty";
-
-Addsimps [converse_prod, converse_empty];
-
-Goal "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B";
-by (Blast_tac 1) ;
-qed "converse_subset_iff";
-
-
-(*** domain ***)
-
-Goalw [domain_def] "a: domain(r) <-> (EX y. <a,y>: r)";
-by (Blast_tac 1) ;
-qed "domain_iff";
-
-Goal "<a,b>: r ==> a: domain(r)";
-by (etac (exI RS (domain_iff RS iffD2)) 1) ;
-qed "domainI";
-
-val prems= Goal
- "[| a : domain(r); !!y. <a,y>: r ==> P |] ==> P";
-by (rtac (domain_iff RS iffD1 RS exE) 1);
-by (REPEAT (ares_tac prems 1)) ;
-qed "domainE";
-
-AddIs [domainI];
-AddSEs [domainE];
-
-Goal "domain(Sigma(A,B)) <= A";
-by (Blast_tac 1) ;
-qed "domain_subset";
-
-(*** range ***)
-
-Goalw [range_def] "<a,b>: r ==> b : range(r)";
-by (etac (converseI RS domainI) 1) ;
-qed "rangeI";
-
-val major::prems= Goalw [range_def]
- "[| b : range(r); !!x. <x,b>: r ==> P |] ==> P";
-by (rtac (major RS domainE) 1);
-by (resolve_tac prems 1);
-by (etac converseD 1) ;
-qed "rangeE";
-
-AddIs [rangeI];
-AddSEs [rangeE];
-
-Goalw [range_def] "range(A*B) <= B";
-by (stac converse_prod 1);
-by (rtac domain_subset 1) ;
-qed "range_subset";
-
-
-(*** field ***)
-
-Goalw [field_def] "<a,b>: r ==> a : field(r)";
-by (Blast_tac 1) ;
-qed "fieldI1";
-
-Goalw [field_def] "<a,b>: r ==> b : field(r)";
-by (Blast_tac 1) ;
-qed "fieldI2";
-
-val [prem]= Goalw [field_def]
- "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)";
-by (blast_tac (claset() addIs [prem]) 1) ;
-qed "fieldCI";
-
-val major::prems= Goalw [field_def]
- "[| a : field(r); \
-\ !!x. <a,x>: r ==> P; \
-\ !!x. <x,a>: r ==> P |] ==> P";
-by (rtac (major RS UnE) 1);
-by (REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ;
-qed "fieldE";
-
-AddIs [fieldCI];
-AddSEs [fieldE];
-
-Goal "field(A*B) <= A Un B";
-by (Blast_tac 1) ;
-qed "field_subset";
-
-Goalw [field_def] "domain(r) <= field(r)";
-by (rtac Un_upper1 1) ;
-qed "domain_subset_field";
-
-Goalw [field_def] "range(r) <= field(r)";
-by (rtac Un_upper2 1) ;
-qed "range_subset_field";
-
-Goal "r <= Sigma(A,B) ==> r <= domain(r)*range(r)";
-by (Blast_tac 1) ;
-qed "domain_times_range";
-
-Goal "r <= Sigma(A,B) ==> r <= field(r)*field(r)";
-by (Blast_tac 1) ;
-qed "field_times_field";
-
-
-(*** Image of a set under a function/relation ***)
-
-Goalw [image_def] "b : r``A <-> (EX x:A. <x,b>:r)";
-by (Blast_tac 1);
-qed "image_iff";
-
-Goal "b : r``{a} <-> <a,b>:r";
-by (rtac (image_iff RS iff_trans) 1);
-by (Blast_tac 1) ;
-qed "image_singleton_iff";
-
-Goalw [image_def] "[| <a,b>: r; a:A |] ==> b : r``A";
-by (Blast_tac 1) ;
-qed "imageI";
-
-val major::prems= Goalw [image_def]
- "[| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P";
-by (rtac (major RS CollectE) 1);
-by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ;
-qed "imageE";
-
-AddIs [imageI];
-AddSEs [imageE];
-
-Goal "r <= A*B ==> r``C <= B";
-by (Blast_tac 1) ;
-qed "image_subset";
-
-
-(*** Inverse image of a set under a function/relation ***)
-
-Goalw [vimage_def,image_def,converse_def]
- "a : r-``B <-> (EX y:B. <a,y>:r)";
-by (Blast_tac 1) ;
-qed "vimage_iff";
-
-Goal "a : r-``{b} <-> <a,b>:r";
-by (rtac (vimage_iff RS iff_trans) 1);
-by (Blast_tac 1) ;
-qed "vimage_singleton_iff";
-
-Goalw [vimage_def] "[| <a,b>: r; b:B |] ==> a : r-``B";
-by (Blast_tac 1) ;
-qed "vimageI";
-
-val major::prems= Goalw [vimage_def]
- "[| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P";
-by (rtac (major RS imageE) 1);
-by (REPEAT (etac converseD 1 ORELSE ares_tac prems 1)) ;
-qed "vimageE";
-
-Goalw [vimage_def] "r <= A*B ==> r-``C <= A";
-by (etac (converse_type RS image_subset) 1) ;
-qed "vimage_subset";
-
-
-(** Theorem-proving for ZF set theory **)
-
-AddIs [vimageI];
-AddSEs [vimageE];
-
-val ZF_cs = claset() delrules [equalityI];
-
-(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
-Goal "(ALL x:S. EX A B. x <= A*B) ==> \
-\ Union(S) <= domain(Union(S)) * range(Union(S))";
-by (Blast_tac 1);
-qed "rel_Union";
-
-(** The Union of 2 relations is a relation (Lemma for fun_Un) **)
-Goal "[| r <= A*B; s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)";
-by (Blast_tac 1) ;
-qed "rel_Un";
-
-Goal "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
-by (Blast_tac 1);
-qed "domain_Diff_eq";
-
-Goal "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
-by (Blast_tac 1);
-qed "range_Diff_eq";
-
--- a/src/ZF/domrange.thy Tue May 21 13:06:36 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-domrange = pair + subset
-
--- a/src/ZF/equalities.thy Tue May 21 13:06:36 2002 +0200
+++ b/src/ZF/equalities.thy Tue May 21 18:25:28 2002 +0200
@@ -15,70 +15,52 @@
(*** converse ***)
lemma converse_iff [iff]: "<a,b>: converse(r) <-> <b,a>:r"
-apply (unfold converse_def)
-apply blast
-done
+by (unfold converse_def, blast)
lemma converseI: "<a,b>:r ==> <b,a>:converse(r)"
-apply (unfold converse_def)
-apply blast
-done
+by (unfold converse_def, blast)
lemma converseD: "<a,b> : converse(r) ==> <b,a> : r"
-apply (unfold converse_def)
-apply blast
-done
+by (unfold converse_def, blast)
lemma converseE [elim!]:
"[| yx : converse(r);
!!x y. [| yx=<y,x>; <x,y>:r |] ==> P |]
==> P"
-apply (unfold converse_def)
-apply (blast intro: elim:);
+apply (unfold converse_def, blast)
done
lemma converse_converse: "r<=Sigma(A,B) ==> converse(converse(r)) = r"
-apply blast
-done
+by blast
lemma converse_type: "r<=A*B ==> converse(r)<=B*A"
-apply blast
-done
+by blast
lemma converse_prod [simp]: "converse(A*B) = B*A"
-apply blast
-done
+by blast
lemma converse_empty [simp]: "converse(0) = 0"
-apply blast
-done
+by blast
lemma converse_subset_iff: "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
-apply blast
-done
+by blast
(*** domain ***)
lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>: r)"
-apply (unfold domain_def)
-apply blast
-done
+by (unfold domain_def, blast)
lemma domainI [intro]: "<a,b>: r ==> a: domain(r)"
-apply (unfold domain_def)
-apply blast
-done
+by (unfold domain_def, blast)
lemma domainE [elim!]:
"[| a : domain(r); !!y. <a,y>: r ==> P |] ==> P"
-apply (unfold domain_def)
-apply blast
+apply (unfold domain_def, blast)
done
lemma domain_subset: "domain(Sigma(A,B)) <= A"
-apply blast
-done
+by blast
(*** range ***)
@@ -88,9 +70,7 @@
done
lemma rangeE [elim!]: "[| b : range(r); !!x. <x,b>: r ==> P |] ==> P"
-apply (unfold range_def)
-apply (blast intro: elim:);
-done
+by (unfold range_def, blast)
lemma range_subset: "range(A*B) <= B"
apply (unfold range_def)
@@ -102,32 +82,25 @@
(*** field ***)
lemma fieldI1: "<a,b>: r ==> a : field(r)"
-apply (unfold field_def)
-apply blast
-done
+by (unfold field_def, blast)
lemma fieldI2: "<a,b>: r ==> b : field(r)"
-apply (unfold field_def)
-apply blast
-done
+by (unfold field_def, blast)
lemma fieldCI [intro]:
"(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)"
-apply (unfold field_def)
-apply blast
+apply (unfold field_def, blast)
done
lemma fieldE [elim!]:
"[| a : field(r);
!!x. <a,x>: r ==> P;
!!x. <x,a>: r ==> P |] ==> P"
-apply (unfold field_def)
-apply blast
+apply (unfold field_def, blast)
done
lemma field_subset: "field(A*B) <= A Un B"
-apply blast
-done
+by blast
lemma domain_subset_field: "domain(r) <= field(r)"
apply (unfold field_def)
@@ -140,64 +113,48 @@
done
lemma domain_times_range: "r <= Sigma(A,B) ==> r <= domain(r)*range(r)"
-apply blast
-done
+by blast
lemma field_times_field: "r <= Sigma(A,B) ==> r <= field(r)*field(r)"
-apply blast
-done
+by blast
(*** Image of a set under a function/relation ***)
lemma image_iff: "b : r``A <-> (EX x:A. <x,b>:r)"
-apply (unfold image_def)
-apply blast
-done
+by (unfold image_def, blast)
lemma image_singleton_iff: "b : r``{a} <-> <a,b>:r"
-apply (rule image_iff [THEN iff_trans])
-apply blast
-done
+by (rule image_iff [THEN iff_trans], blast)
lemma imageI [intro]: "[| <a,b>: r; a:A |] ==> b : r``A"
-apply (unfold image_def)
-apply blast
-done
+by (unfold image_def, blast)
lemma imageE [elim!]:
"[| b: r``A; !!x.[| <x,b>: r; x:A |] ==> P |] ==> P"
-apply (unfold image_def)
-apply blast
+apply (unfold image_def, blast)
done
lemma image_subset: "r <= A*B ==> r``C <= B"
-apply blast
-done
+by blast
(*** Inverse image of a set under a function/relation ***)
lemma vimage_iff:
"a : r-``B <-> (EX y:B. <a,y>:r)"
-apply (unfold vimage_def image_def converse_def)
-apply blast
+apply (unfold vimage_def image_def converse_def, blast)
done
lemma vimage_singleton_iff: "a : r-``{b} <-> <a,b>:r"
-apply (rule vimage_iff [THEN iff_trans])
-apply blast
-done
+by (rule vimage_iff [THEN iff_trans], blast)
lemma vimageI [intro]: "[| <a,b>: r; b:B |] ==> a : r-``B"
-apply (unfold vimage_def)
-apply blast
-done
+by (unfold vimage_def, blast)
lemma vimageE [elim!]:
"[| a: r-``B; !!x.[| <a,x>: r; x:B |] ==> P |] ==> P"
-apply (unfold vimage_def)
-apply blast
+apply (unfold vimage_def, blast)
done
lemma vimage_subset: "r <= A*B ==> r-``C <= A"
@@ -213,16 +170,13 @@
(** The Union of 2 relations is a relation (Lemma for fun_Un) **)
lemma rel_Un: "[| r <= A*B; s <= C*D |] ==> (r Un s) <= (A Un C) * (B Un D)"
-apply blast
-done
+by blast
lemma domain_Diff_eq: "[| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
-apply blast
-done
+by blast
lemma range_Diff_eq: "[| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)"
-apply blast
-done
+by blast