1.1 --- a/src/ZF/AC/AC15_WO6.thy Wed May 22 19:34:01 2002 +0200
1.2 +++ b/src/ZF/AC/AC15_WO6.thy Thu May 23 17:05:21 2002 +0200
1.3 @@ -174,12 +174,12 @@
1.4 apply (erule impE, fast)
1.5 apply (elim bexE conjE exE)
1.6 apply (rule bexI)
1.7 -apply (rule conjI, assumption)
1.8 -apply (rule_tac x = "LEAST i. HH (f,A,i) ={A}" in exI)
1.9 -apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
1.10 -apply simp
1.11 + apply (rule conjI, assumption)
1.12 + apply (rule_tac x = "LEAST i. HH (f,A,i) ={A}" in exI)
1.13 + apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
1.14 + apply (simp_all add: ltD)
1.15 apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
1.16 - elim!: less_Least_subset_x lemma1 lemma2, assumption)
1.17 + elim!: less_Least_subset_x lemma1 lemma2)
1.18 done
1.19
1.20
2.1 --- a/src/ZF/AC/AC16_WO4.thy Wed May 22 19:34:01 2002 +0200
2.2 +++ b/src/ZF/AC/AC16_WO4.thy Thu May 23 17:05:21 2002 +0200
2.3 @@ -22,8 +22,8 @@
2.4 apply (drule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]])
2.5 apply (erule exE)
2.6 apply (rule_tac x = "n" in exI)
2.7 -apply (rule_tac x = "\<lambda>i \<in> n. {f`i}" in exI, simp)
2.8 -apply (unfold bij_def surj_def)
2.9 +apply (rule_tac x = "\<lambda>i \<in> n. {f`i}" in exI)
2.10 +apply (simp add: ltD bij_def surj_def)
2.11 apply (fast intro!: ltI nat_into_Ord lam_funtype [THEN domain_of_fun]
2.12 singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
2.13 nat_1_lepoll_iff [THEN iffD2]
2.14 @@ -548,7 +548,7 @@
2.15 apply (rule_tac x = "ordertype (LL,S)" in exI)
2.16 apply (rule_tac x = "\<lambda>b \<in> ordertype(LL,S).
2.17 GG ` (converse (ordermap (LL,S)) ` b)" in exI)
2.18 -apply simp
2.19 +apply (simp add: ltD)
2.20 apply (blast intro: lam_funtype [THEN domain_of_fun]
2.21 Ord_ordertype OUN_eq_x all_in_lepoll_m [THEN ospec])
2.22 done
3.1 --- a/src/ZF/AC/DC.thy Wed May 22 19:34:01 2002 +0200
3.2 +++ b/src/ZF/AC/DC.thy Thu May 23 17:05:21 2002 +0200
3.3 @@ -30,7 +30,7 @@
3.4 lemma range_subset_domain:
3.5 "[| R \<subseteq> X*X; !!g. g \<in> X ==> \<exists>u. <g,u> \<in> R |]
3.6 ==> range(R) \<subseteq> domain(R)"
3.7 -by (blast );
3.8 +by blast
3.9
3.10 lemma cons_fun_type: "g \<in> n->X ==> cons(<n,x>, g) \<in> succ(n) -> cons(x, X)"
3.11 apply (unfold succ_def)
3.12 @@ -247,7 +247,8 @@
3.13 (** LEVEL 11: last subgoal **)
3.14 apply (subst DC0_imp.lemma3, assumption+)
3.15 apply (fast elim!: fun_weaken_type)
3.16 - apply (erule ltD, force)
3.17 + apply (erule ltD)
3.18 +apply (force simp add: lt_def)
3.19 done
3.20
3.21
3.22 @@ -486,7 +487,7 @@
3.23 done
3.24
3.25 lemma value_in_image: "[| f \<in> X->Y; A \<subseteq> X; a \<in> A |] ==> f`a \<in> f``A"
3.26 -by (fast elim!: image_fun [THEN ssubst]);
3.27 +by (fast elim!: image_fun [THEN ssubst])
3.28
3.29 theorem DC_WO3: "(\<forall>K. Card(K) --> DC(K)) ==> WO3"
3.30 apply (unfold DC_def WO3_def)
4.1 --- a/src/ZF/AC/WO6_WO1.thy Wed May 22 19:34:01 2002 +0200
4.2 +++ b/src/ZF/AC/WO6_WO1.thy Thu May 23 17:05:21 2002 +0200
4.3 @@ -92,7 +92,8 @@
4.4 apply (erule Ord_ordertype)
4.5 apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN lam_sets, THEN domain_of_fun])
4.6 apply (simp_all add: singleton_eqpoll_1 eqpoll_imp_lepoll Ord_ordertype
4.7 - ordermap_bij [THEN bij_converse_bij, THEN bij_is_surj, THEN surj_imp_eq])
4.8 + ordermap_bij [THEN bij_converse_bij, THEN bij_is_surj, THEN surj_imp_eq]
4.9 + ltD)
4.10 done
4.11
4.12 (* ********************************************************************** *)
4.13 @@ -218,14 +219,14 @@
4.14 domain(uu(f,b,g,d)) \<lesssim> m);
4.15 \<forall>b<a. f`b \<lesssim> succ(m); b<a++a |]
4.16 ==> gg1(f,a,m)`b \<lesssim> m"
4.17 -apply (unfold gg1_def, simp)
4.18 +apply (simp add: gg1_def empty_lepollI)
4.19 apply (safe dest!: lt_oadd_odiff_disj)
4.20 (*Case b<a \<in> show vv1(f,m,b) \<lesssim> m *)
4.21 -apply (simp add: vv1_def Let_def)
4.22 -apply (fast intro: nested_Least_instance [THEN conjunct2]
4.23 - elim!: lt_Ord intro!: empty_lepollI)
4.24 + apply (simp add: vv1_def Let_def empty_lepollI)
4.25 + apply (fast intro: nested_Least_instance [THEN conjunct2]
4.26 + elim!: lt_Ord)
4.27 (*Case a\<le>b \<in> show ww1(f,m,b--a) \<lesssim> m *)
4.28 -apply (simp add: ww1_def)
4.29 +apply (simp add: ww1_def empty_lepollI)
4.30 apply (case_tac "f` (b--a) = 0", simp add: empty_lepollI)
4.31 apply (rule Diff_lepoll, blast)
4.32 apply (rule vv1_subset)
4.33 @@ -321,8 +322,8 @@
4.34 (\<Union>b<a. f`b)=y; Ord(a); m \<in> nat; s \<in> f`b; b<a |]
4.35 ==> (\<Union>g<a++a. gg2(f,a,b,s) ` g) = y"
4.36 apply (unfold gg2_def)
4.37 -apply (drule sym)
4.38 -apply (simp add: UN_oadd lt_oadd1 oadd_le_self [THEN le_imp_not_lt]
4.39 +apply (drule sym)
4.40 +apply (simp add: ltD UN_oadd oadd_le_self [THEN le_imp_not_lt]
4.41 lt_Ord odiff_oadd_inverse ww2_def
4.42 vv2_subset [THEN Diff_partition])
4.43 done
4.44 @@ -361,7 +362,7 @@
4.45 \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
4.46 (\<Union>b<a. f`b)=y; b<a; s \<in> f`b; m \<in> nat; m\<noteq> 0; g<a++a |]
4.47 ==> gg2(f,a,b,s) ` g \<lesssim> m"
4.48 -apply (unfold gg2_def, simp)
4.49 +apply (simp add: gg2_def empty_lepollI)
4.50 apply (safe elim!: lt_Ord2 dest!: lt_oadd_odiff_disj)
4.51 apply (simp add: vv2_lepoll)
4.52 apply (simp add: ww2_lepoll vv2_subset)
5.1 --- a/src/ZF/Epsilon.thy Wed May 22 19:34:01 2002 +0200
5.2 +++ b/src/ZF/Epsilon.thy Thu May 23 17:05:21 2002 +0200
5.3 @@ -278,14 +278,14 @@
5.4 "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"
5.5 by (simp add: the_0 the_equality2)
5.6
5.7 -(*The premise is needed not just to fix i but to ensure f~=0*)
5.8 -lemma rank_apply: "i : domain(f) ==> rank(f`i) < rank(f)"
5.9 -apply (unfold apply_def, clarify)
5.10 -apply (subgoal_tac "rank (y) < rank (f) ")
5.11 -prefer 2 apply (blast intro: lt_trans rank_lt rank_pair2)
5.12 -apply (subgoal_tac "0 < rank (f) ")
5.13 -apply (erule_tac [2] Ord_rank [THEN Ord_0_le, THEN lt_trans1])
5.14 -apply (simp add: the_equality_if)
5.15 +(*The first premise not only fixs i but ensures f~=0.
5.16 + The second premise is now essential. Consider otherwise the relation
5.17 + r = {<0,0>,<0,1>,<0,2>,...}. Then f`0 = Union(f``{0}) = Union(nat) = nat,
5.18 + whose rank equals that of r.*)
5.19 +lemma rank_apply: "[|i : domain(f); function(f)|] ==> rank(f`i) < rank(f)"
5.20 +apply (clarify );
5.21 +apply (simp add: function_apply_equality);
5.22 +apply (blast intro: lt_trans rank_lt rank_pair2)
5.23 done
5.24
5.25
5.26 @@ -323,8 +323,8 @@
5.27
5.28 lemma transrec2_Limit:
5.29 "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
5.30 -apply (rule transrec2_def [THEN def_transrec, THEN trans], simp)
5.31 -apply (blast dest!: Limit_has_0 elim!: succ_LimitE)
5.32 +apply (rule transrec2_def [THEN def_transrec, THEN trans])
5.33 +apply (auto simp add: OUnion_def);
5.34 done
5.35
5.36
6.1 --- a/src/ZF/Induct/Multiset.ML Wed May 22 19:34:01 2002 +0200
6.2 +++ b/src/ZF/Induct/Multiset.ML Thu May 23 17:05:21 2002 +0200
6.3 @@ -284,22 +284,18 @@
6.4 by (auto_tac (claset(), simpset()
6.5 addsimps [multiset_fun_iff, mset_of_def, funrestrict_def]));
6.6 qed "mdiff_0";
6.7 -Addsimps [mdiff_0];
6.8 +Addsimps [mdiff_0];
6.9
6.10 -Goalw [multiset_def] "multiset(M) ==> M +# {#a#} -# {#a#} = M";
6.11 -by (rewrite_goals_tac [munion_def, mdiff_def,
6.12 +Goal "multiset(M) ==> M +# {#a#} -# {#a#} = M";
6.13 +by (rewrite_goals_tac [multiset_def, munion_def, mdiff_def,
6.14 msingle_def, normalize_def, mset_of_def]);
6.15 -by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
6.16 +by (auto_tac (claset(),
6.17 + simpset() addcongs [if_cong]
6.18 + addsimps [ltD, multiset_fun_iff,
6.19 + funrestrict_def, subset_Un_iff2 RS iffD1]));
6.20 +by (subgoal_tac "{x \\<in> A \\<union> {a} . x \\<noteq> a \\<and> x \\<in> A} = A" 2);
6.21 by (rtac fun_extension 1);
6.22 -by Auto_tac;
6.23 -by (res_inst_tac [("P", "%x. ?u : Pi(x, ?v)")] subst 1);
6.24 -by (rtac funrestrict_type 2);
6.25 -by (rtac equalityI 1);
6.26 -by (ALLGOALS(Clarify_tac));
6.27 -by Auto_tac;
6.28 -by (res_inst_tac [("Pa", "~(1<?u)")] swap 1);
6.29 -by (case_tac "x=a" 3);
6.30 -by (ALLGOALS(Asm_full_simp_tac));
6.31 +by Auto_tac;
6.32 qed "mdiff_union_inverse2";
6.33 Addsimps [mdiff_union_inverse2];
6.34
7.1 --- a/src/ZF/Induct/Ntree.thy Wed May 22 19:34:01 2002 +0200
7.2 +++ b/src/ZF/Induct/Ntree.thy Thu May 23 17:05:21 2002 +0200
7.3 @@ -114,21 +114,21 @@
7.4 \medskip @{text ntree} recursion.
7.5 *}
7.6
7.7 -lemma ntree_rec_Branch: "ntree_rec(b, Branch(x,h))
7.8 - = b(x, h, \<lambda>i \<in> domain(h). ntree_rec(b, h`i))"
7.9 +lemma ntree_rec_Branch:
7.10 + "function(h) ==>
7.11 + ntree_rec(b, Branch(x,h)) = b(x, h, \<lambda>i \<in> domain(h). ntree_rec(b, h`i))"
7.12 apply (rule ntree_rec_def [THEN def_Vrecursor, THEN trans])
7.13 apply (simp add: ntree.con_defs rank_pair2 [THEN [2] lt_trans] rank_apply)
7.14 done
7.15
7.16 lemma ntree_copy_Branch [simp]:
7.17 - "ntree_copy (Branch(x, h)) = Branch(x, \<lambda>i \<in> domain(h). ntree_copy (h`i))"
7.18 - apply (unfold ntree_copy_def)
7.19 - apply (rule ntree_rec_Branch)
7.20 - done
7.21 + "function(h) ==>
7.22 + ntree_copy (Branch(x, h)) = Branch(x, \<lambda>i \<in> domain(h). ntree_copy (h`i))"
7.23 + by (simp add: ntree_copy_def ntree_rec_Branch)
7.24
7.25 lemma ntree_copy_is_ident: "z \<in> ntree(A) ==> ntree_copy(z) = z"
7.26 apply (induct_tac z)
7.27 - apply (auto simp add: domain_of_fun Pi_Collect_iff)
7.28 + apply (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function)
7.29 done
7.30
7.31
8.1 --- a/src/ZF/Integ/Bin.ML Wed May 22 19:34:01 2002 +0200
8.2 +++ b/src/ZF/Integ/Bin.ML Thu May 23 17:05:21 2002 +0200
8.3 @@ -7,6 +7,7 @@
8.4 *)
8.5
8.6
8.7 +Addsimps bin.intrs;
8.8 AddTCs bin.intrs;
8.9
8.10 Goal "NCons(Pls,0) = Pls";
9.1 --- a/src/ZF/Integ/IntDiv.ML Wed May 22 19:34:01 2002 +0200
9.2 +++ b/src/ZF/Integ/IntDiv.ML Thu May 23 17:05:21 2002 +0200
9.3 @@ -369,7 +369,7 @@
9.4 Addsimps [adjust_eq];
9.5
9.6
9.7 -Goal "[| #0 $< b; \\<not> a $< b |] \
9.8 +Goal "[| #0 $< b; ~ a $< b |] \
9.9 \ ==> nat_of(a $- #2 $\\<times> b $+ #1) < nat_of(a $- b $+ #1)";
9.10 by (simp_tac (simpset() addsimps [zless_nat_conj]) 1);
9.11 by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle,
9.12 @@ -382,8 +382,8 @@
9.13 \ posDivAlg(<a,b>) = \
9.14 \ (if a$<b then <#0,a> else adjust(b, posDivAlg (<a, #2$*b>)))";
9.15 by (rtac (posDivAlg_unfold RS trans) 1);
9.16 -by (asm_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
9.17 -by (asm_simp_tac (simpset() addsimps [vimage_iff, posDivAlg_termination]) 1);
9.18 +by (asm_simp_tac (simpset() addsimps [vimage_iff, not_zless_iff_zle RS iff_sym]) 1);
9.19 +by (blast_tac (claset() addIs [posDivAlg_termination]) 1);
9.20 qed "posDivAlg_eqn";
9.21
9.22 val [prem] =
9.23 @@ -529,8 +529,7 @@
9.24
9.25 (*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***)
9.26
9.27 -Goal "[| #0 $< b; \\<not> #0 $<= a $+ b |] \
9.28 -\ ==> nat_of($- a $- #2 $\\<times> b) < nat_of($- a $- b)";
9.29 +Goal "[| #0 $< b; a $+ b $< #0 |] ==> nat_of($- a $- #2 $* b) < nat_of($- a $- b)";
9.30 by (simp_tac (simpset() addsimps [zless_nat_conj]) 1);
9.31 by (asm_full_simp_tac (simpset() addsimps zcompare_rls @
9.32 [not_zle_iff_zless, zless_zdiff_iff RS iff_sym, zless_zminus]) 1);
9.33 @@ -538,14 +537,13 @@
9.34
9.35 val negDivAlg_unfold = wf_measure RS (negDivAlg_def RS def_wfrec);
9.36
9.37 -Goal "[| #0 $< b; a \\<in> int; b \\<in> int |] ==> \
9.38 +Goal "[| #0 $< b; a : int; b : int |] ==> \
9.39 \ negDivAlg(<a,b>) = \
9.40 \ (if #0 $<= a$+b then <#-1,a$+b> \
9.41 \ else adjust(b, negDivAlg (<a, #2$*b>)))";
9.42 by (rtac (negDivAlg_unfold RS trans) 1);
9.43 -by (asm_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
9.44 -by (asm_simp_tac (simpset() addsimps [not_zle_iff_zless, vimage_iff,
9.45 - negDivAlg_termination]) 1);
9.46 +by (asm_simp_tac (simpset() addsimps [vimage_iff, not_zless_iff_zle RS iff_sym]) 1);
9.47 +by (blast_tac (claset() addIs [negDivAlg_termination]) 1);
9.48 qed "negDivAlg_eqn";
9.49
9.50 val [prem] =
9.51 @@ -640,15 +638,17 @@
9.52 qed "posDivAlg_0";
9.53 Addsimps [posDivAlg_0];
9.54
9.55 -Goal "negDivAlg (<#-1,b>) = <#-1, b$-#1>";
9.56 -by (stac negDivAlg_unfold 1);
9.57 -by Auto_tac;
9.58 -(*ALL the rest is linear arithmetic: to notice the contradiction*)
9.59 +(*Needed below. Actually it's an equivalence.*)
9.60 +Goal "~ (#0 $<= #-1 $+ b) ==> (b $<= #0)";
9.61 by (asm_full_simp_tac (simpset() addsimps [not_zle_iff_zless]) 1);
9.62 by (dtac (zminus_zless_zminus RS iffD2) 1);
9.63 by (asm_full_simp_tac (simpset() addsimps [zadd_commute, zless_add1_iff_zle,
9.64 zle_zminus]) 1);
9.65 -by (asm_full_simp_tac (simpset() addsimps [not_zle_iff_zless RS iff_sym]) 1);
9.66 +qed "linear_arith_lemma";
9.67 +
9.68 +Goal "negDivAlg (<#-1,b>) = <#-1, b$-#1>";
9.69 +by (stac negDivAlg_unfold 1);
9.70 +by (asm_full_simp_tac (simpset() addsimps [linear_arith_lemma, integ_of_type, vimage_iff]) 1);
9.71 qed "negDivAlg_minus1";
9.72 Addsimps [negDivAlg_minus1];
9.73
10.1 --- a/src/ZF/List.ML Wed May 22 19:34:01 2002 +0200
10.2 +++ b/src/ZF/List.ML Thu May 23 17:05:21 2002 +0200
10.3 @@ -8,6 +8,8 @@
10.4
10.5 (*** Aspects of the datatype definition ***)
10.6
10.7 +Addsimps list.intrs;
10.8 +
10.9 (*An elimination rule, for type-checking*)
10.10 bind_thm ("ConsE", list.mk_cases "Cons(a,l) : list(A)");
10.11
11.1 --- a/src/ZF/OrdQuant.thy Wed May 22 19:34:01 2002 +0200
11.2 +++ b/src/ZF/OrdQuant.thy Thu May 23 17:05:21 2002 +0200
11.3 @@ -182,8 +182,6 @@
11.4 "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
11.5 by (simp add: OUnion_def lt_def OUN_iff)
11.6
11.7 -declare ltD [THEN beta, simp]
11.8 -
11.9 lemma lt_induct:
11.10 "[| i<k; !!x.[| x<k; ALL y<x. P(y) |] ==> P(x) |] ==> P(i)"
11.11 apply (simp add: lt_def oall_def)
12.1 --- a/src/ZF/Perm.ML Wed May 22 19:34:01 2002 +0200
12.2 +++ b/src/ZF/Perm.ML Thu May 23 17:05:21 2002 +0200
12.3 @@ -146,7 +146,7 @@
12.4 bind_thm ("id_inj", subset_refl RS id_subset_inj);
12.5
12.6 Goalw [id_def,surj_def] "id(A): surj(A,A)";
12.7 -by (blast_tac (claset() addIs [lam_type, beta]) 1);
12.8 +by (Asm_simp_tac 1);
12.9 qed "id_surj";
12.10
12.11 Goalw [bij_def] "id(A): bij(A,A)";
12.12 @@ -342,7 +342,7 @@
12.13 by (rtac comp_fun 1);
12.14 by (rtac lam_funtype 2);
12.15 by (typecheck_tac (tcset() addTCs [prem]));
12.16 -by (asm_simp_tac (simpset()
12.17 +by (asm_simp_tac (simpset() addsimps [prem]
12.18 setSolver (mk_solver ""
12.19 (type_solver_tac (tcset() addTCs [prem, lam_funtype])))) 1);
12.20 qed "comp_lam";
13.1 --- a/src/ZF/Univ.thy Wed May 22 19:34:01 2002 +0200
13.2 +++ b/src/ZF/Univ.thy Thu May 23 17:05:21 2002 +0200
13.3 @@ -488,7 +488,7 @@
13.4 apply (unfold Vrec_def)
13.5 apply (subst transrec)
13.6 apply simp
13.7 -apply (rule refl [THEN lam_cong, THEN subst_context], simp)
13.8 +apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
13.9 done
13.10
13.11 text{*This form avoids giant explosions in proofs. NOTE USE OF == *}
13.12 @@ -504,7 +504,7 @@
13.13 "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x), a)"
13.14 apply (unfold Vrecursor_def)
13.15 apply (subst transrec, simp)
13.16 -apply (rule refl [THEN lam_cong, THEN subst_context], simp)
13.17 +apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
13.18 done
13.19
13.20 text{*This form avoids giant explosions in proofs. NOTE USE OF == *}
14.1 --- a/src/ZF/WF.thy Wed May 22 19:34:01 2002 +0200
14.2 +++ b/src/ZF/WF.thy Thu May 23 17:05:21 2002 +0200
14.3 @@ -213,8 +213,9 @@
14.4 lemma apply_recfun:
14.5 "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
14.6 apply (unfold is_recfun_def)
14.7 -apply (erule_tac P = "%x.?t (x) = (?u::i) " in ssubst)
14.8 -apply (erule underI [THEN beta])
14.9 + txt{*replace f only on the left-hand side*}
14.10 +apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
14.11 +apply (simp add: underI);
14.12 done
14.13
14.14 lemma is_recfun_equal [rule_format]:
14.15 @@ -280,7 +281,7 @@
14.16 apply (frule spec [THEN mp], assumption)
14.17 apply (subgoal_tac "<xa,a1> : r")
14.18 apply (drule_tac x1 = "xa" in spec [THEN mp], assumption)
14.19 -apply (simp add: vimage_singleton_iff underI [THEN beta]
14.20 +apply (simp add: vimage_singleton_iff
14.21 apply_recfun is_recfun_cut)
14.22 apply (blast dest: transD)
14.23 done
15.1 --- a/src/ZF/ZF.thy Wed May 22 19:34:01 2002 +0200
15.2 +++ b/src/ZF/ZF.thy Thu May 23 17:05:21 2002 +0200
15.3 @@ -145,11 +145,11 @@
15.4
15.5 syntax (xsymbols)
15.6 "op *" :: "[i, i] => i" (infixr "\\<times>" 80)
15.7 - "op Int" :: "[i, i] => i" (infixl "\\<inter>" 70)
15.8 - "op Un" :: "[i, i] => i" (infixl "\\<union>" 65)
15.9 + "op Int" :: "[i, i] => i" (infixl "\\<inter>" 70)
15.10 + "op Un" :: "[i, i] => i" (infixl "\\<union>" 65)
15.11 "op ->" :: "[i, i] => i" (infixr "\\<rightarrow>" 60)
15.12 - "op <=" :: "[i, i] => o" (infixl "\\<subseteq>" 50)
15.13 - "op :" :: "[i, i] => o" (infixl "\\<in>" 50)
15.14 + "op <=" :: "[i, i] => o" (infixl "\\<subseteq>" 50)
15.15 + "op :" :: "[i, i] => o" (infixl "\\<in>" 50)
15.16 "op ~:" :: "[i, i] => o" (infixl "\\<notin>" 50)
15.17 "@Collect" :: "[pttrn, i, o] => i" ("(1{_ \\<in> _ ./ _})")
15.18 "@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \\<in> _, _})")
15.19 @@ -261,7 +261,7 @@
15.20 (* Abstraction, application and Cartesian product of a family of sets *)
15.21
15.22 lam_def "Lambda(A,b) == {<x,b(x)> . x:A}"
15.23 - apply_def "f`a == THE y. <a,y> : f"
15.24 + apply_def "f`a == Union(f``{a})"
15.25 Pi_def "Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
15.26
15.27 (* Restrict the relation r to the domain A *)
16.1 --- a/src/ZF/Zorn.thy Wed May 22 19:34:01 2002 +0200
16.2 +++ b/src/ZF/Zorn.thy Thu May 23 17:05:21 2002 +0200
16.3 @@ -222,10 +222,10 @@
16.4 "ch: (PROD X: Pow(chain(S))-{0}. X) ==>
16.5 EX next: increasing(S). ALL X: Pow(S).
16.6 next`X = if(X: chain(S)-maxchain(S), ch`super(S,X), X)"
16.7 -apply (rule bexI)
16.8 -apply (rule ballI)
16.9 -apply (rule beta)
16.10 -apply assumption
16.11 +apply (rule_tac x="\<lambda>X\<in>Pow(S).
16.12 + if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X"
16.13 + in bexI)
16.14 +apply (force );
16.15 apply (unfold increasing_def)
16.16 apply (rule CollectI)
16.17 apply (rule lam_type)
16.18 @@ -236,7 +236,7 @@
16.19 apply safe
16.20 apply (drule choice_super)
16.21 apply (assumption+)
16.22 -apply (unfold super_def)
16.23 +apply (simp add: super_def)
16.24 apply blast
16.25 done
16.26
16.27 @@ -366,11 +366,10 @@
16.28 lemma Zermelo_next_exists:
16.29 "ch: (PROD X: Pow(S)-{0}. X) ==>
16.30 EX next: increasing(S). ALL X: Pow(S).
16.31 - next`X = if(X=S, S, cons(ch`(S-X), X))"
16.32 -apply (rule bexI)
16.33 -apply (rule ballI)
16.34 -apply (rule beta)
16.35 -apply assumption
16.36 + next`X = (if X=S then S else cons(ch`(S-X), X))"
16.37 +apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
16.38 + in bexI)
16.39 +apply (force );
16.40 apply (unfold increasing_def)
16.41 apply (rule CollectI)
16.42 apply (rule lam_type)
17.1 --- a/src/ZF/ex/Limit.thy Wed May 22 19:34:01 2002 +0200
17.2 +++ b/src/ZF/ex/Limit.thy Thu May 23 17:05:21 2002 +0200
17.3 @@ -1066,7 +1066,7 @@
17.4 (*looks like something should be inserted into the assumptions!*)
17.5 apply (rule_tac P = "%t. rel (DD`na,t,lub (DD`na,\<lambda>x \<in> nat. X`x`na))"
17.6 and b1 = "%n. X`n`na" in beta [THEN subst])
17.7 -apply (simp del: beta
17.8 +apply (simp del: beta_if
17.9 add: chain_iprod [THEN cpo_lub, THEN islub_ub] iprodE
17.10 chain_in)+
17.11 apply (blast intro: iprodI lam_type chain_iprod [THEN cpo_lub, THEN islub_in])
17.12 @@ -2167,7 +2167,8 @@
17.13 ((\<lambda>n \<in> nat. f(n) O Rp(DD ` n, E, r(n))) ` na)) =
17.14 (\<lambda>na \<in> nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))"
17.15 apply (rule fun_extension)
17.16 -apply (auto intro: lam_type)
17.17 +(*something wrong here*)
17.18 +apply (auto simp del: beta_if simp add: beta intro: lam_type)
17.19 done
17.20
17.21 lemma chain_lemma:
18.1 --- a/src/ZF/func.thy Wed May 22 19:34:01 2002 +0200
18.2 +++ b/src/ZF/func.thy Thu May 23 17:05:21 2002 +0200
18.3 @@ -58,7 +58,7 @@
18.4 (*Applying a function outside its domain yields 0*)
18.5 lemma apply_0: "a ~: domain(f) ==> f`a = 0"
18.6 apply (unfold apply_def)
18.7 -apply (rule the_0, blast)
18.8 +apply (blast intro: elim:);
18.9 done
18.10
18.11 lemma Pi_memberD: "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>"
18.12 @@ -67,8 +67,12 @@
18.13 done
18.14
18.15 lemma function_apply_Pair: "[| function(f); a : domain(f)|] ==> <a,f`a>: f"
18.16 -apply (simp add: function_def apply_def)
18.17 -apply (rule theI2, auto)
18.18 +apply (simp add: function_def)
18.19 +apply (clarify );
18.20 +apply (subgoal_tac "f`a = y")
18.21 +apply (blast intro: elim:);
18.22 +apply (simp add: apply_def);
18.23 +apply (blast intro: elim:);
18.24 done
18.25
18.26 lemma apply_Pair: "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f"
18.27 @@ -145,8 +149,15 @@
18.28 lemma relation_lam: "relation (lam x:A. b(x))"
18.29 by (simp add: relation_def lam_def)
18.30
18.31 -lemma beta [simp]: "a : A ==> (lam x:A. b(x)) ` a = b(a)"
18.32 -by (blast intro: apply_equality lam_funtype lamI)
18.33 +lemma beta_if [simp]: "(lam x:A. b(x)) ` a = (if a : A then b(a) else 0)"
18.34 +apply (simp add: apply_def lam_def)
18.35 +apply (blast intro: elim:);
18.36 +done
18.37 +
18.38 +lemma beta: "a : A ==> (lam x:A. b(x)) ` a = b(a)"
18.39 +apply (simp add: apply_def lam_def)
18.40 +apply (blast intro: elim:);
18.41 +done
18.42
18.43 lemma lam_empty [simp]: "(lam x:0. b(x)) = 0"
18.44 by (simp add: lam_def)
18.45 @@ -161,9 +172,8 @@
18.46
18.47 lemma lam_theI:
18.48 "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)"
18.49 -apply (rule_tac x = "lam x: A. THE y. Q (x,y) " in exI)
18.50 -apply (rule ballI)
18.51 -apply (subst beta, assumption)
18.52 +apply (rule_tac x = "lam x: A. THE y. Q (x,y)" in exI)
18.53 +apply (simp add: );
18.54 apply (blast intro: theI)
18.55 done
18.56
18.57 @@ -263,7 +273,9 @@
18.58 by (simp add: Pi_iff function_def restrict_def, blast)
18.59
18.60 lemma restrict: "a : A ==> restrict(f,A) ` a = f`a"
18.61 -by (simp add: apply_def restrict_def)
18.62 +apply (simp add: apply_def restrict_def)
18.63 +apply (blast intro: elim:);
18.64 +done
18.65
18.66 lemma restrict_empty [simp]: "restrict(f,0) = 0"
18.67 apply (unfold restrict_def)