--- a/src/ZF/AC/AC15_WO6.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/AC/AC15_WO6.thy Thu May 23 17:05:21 2002 +0200
@@ -174,12 +174,12 @@
apply (erule impE, fast)
apply (elim bexE conjE exE)
apply (rule bexI)
-apply (rule conjI, assumption)
-apply (rule_tac x = "LEAST i. HH (f,A,i) ={A}" in exI)
-apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
-apply simp
+ apply (rule conjI, assumption)
+ apply (rule_tac x = "LEAST i. HH (f,A,i) ={A}" in exI)
+ apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
+ apply (simp_all add: ltD)
apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
- elim!: less_Least_subset_x lemma1 lemma2, assumption)
+ elim!: less_Least_subset_x lemma1 lemma2)
done
--- a/src/ZF/AC/AC16_WO4.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/AC/AC16_WO4.thy Thu May 23 17:05:21 2002 +0200
@@ -22,8 +22,8 @@
apply (drule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]])
apply (erule exE)
apply (rule_tac x = "n" in exI)
-apply (rule_tac x = "\<lambda>i \<in> n. {f`i}" in exI, simp)
-apply (unfold bij_def surj_def)
+apply (rule_tac x = "\<lambda>i \<in> n. {f`i}" in exI)
+apply (simp add: ltD bij_def surj_def)
apply (fast intro!: ltI nat_into_Ord lam_funtype [THEN domain_of_fun]
singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
nat_1_lepoll_iff [THEN iffD2]
@@ -548,7 +548,7 @@
apply (rule_tac x = "ordertype (LL,S)" in exI)
apply (rule_tac x = "\<lambda>b \<in> ordertype(LL,S).
GG ` (converse (ordermap (LL,S)) ` b)" in exI)
-apply simp
+apply (simp add: ltD)
apply (blast intro: lam_funtype [THEN domain_of_fun]
Ord_ordertype OUN_eq_x all_in_lepoll_m [THEN ospec])
done
--- a/src/ZF/AC/DC.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/AC/DC.thy Thu May 23 17:05:21 2002 +0200
@@ -30,7 +30,7 @@
lemma range_subset_domain:
"[| R \<subseteq> X*X; !!g. g \<in> X ==> \<exists>u. <g,u> \<in> R |]
==> range(R) \<subseteq> domain(R)"
-by (blast );
+by blast
lemma cons_fun_type: "g \<in> n->X ==> cons(<n,x>, g) \<in> succ(n) -> cons(x, X)"
apply (unfold succ_def)
@@ -247,7 +247,8 @@
(** LEVEL 11: last subgoal **)
apply (subst DC0_imp.lemma3, assumption+)
apply (fast elim!: fun_weaken_type)
- apply (erule ltD, force)
+ apply (erule ltD)
+apply (force simp add: lt_def)
done
@@ -486,7 +487,7 @@
done
lemma value_in_image: "[| f \<in> X->Y; A \<subseteq> X; a \<in> A |] ==> f`a \<in> f``A"
-by (fast elim!: image_fun [THEN ssubst]);
+by (fast elim!: image_fun [THEN ssubst])
theorem DC_WO3: "(\<forall>K. Card(K) --> DC(K)) ==> WO3"
apply (unfold DC_def WO3_def)
--- a/src/ZF/AC/WO6_WO1.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/AC/WO6_WO1.thy Thu May 23 17:05:21 2002 +0200
@@ -92,7 +92,8 @@
apply (erule Ord_ordertype)
apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN lam_sets, THEN domain_of_fun])
apply (simp_all add: singleton_eqpoll_1 eqpoll_imp_lepoll Ord_ordertype
- ordermap_bij [THEN bij_converse_bij, THEN bij_is_surj, THEN surj_imp_eq])
+ ordermap_bij [THEN bij_converse_bij, THEN bij_is_surj, THEN surj_imp_eq]
+ ltD)
done
(* ********************************************************************** *)
@@ -218,14 +219,14 @@
domain(uu(f,b,g,d)) \<lesssim> m);
\<forall>b<a. f`b \<lesssim> succ(m); b<a++a |]
==> gg1(f,a,m)`b \<lesssim> m"
-apply (unfold gg1_def, simp)
+apply (simp add: gg1_def empty_lepollI)
apply (safe dest!: lt_oadd_odiff_disj)
(*Case b<a \<in> show vv1(f,m,b) \<lesssim> m *)
-apply (simp add: vv1_def Let_def)
-apply (fast intro: nested_Least_instance [THEN conjunct2]
- elim!: lt_Ord intro!: empty_lepollI)
+ apply (simp add: vv1_def Let_def empty_lepollI)
+ apply (fast intro: nested_Least_instance [THEN conjunct2]
+ elim!: lt_Ord)
(*Case a\<le>b \<in> show ww1(f,m,b--a) \<lesssim> m *)
-apply (simp add: ww1_def)
+apply (simp add: ww1_def empty_lepollI)
apply (case_tac "f` (b--a) = 0", simp add: empty_lepollI)
apply (rule Diff_lepoll, blast)
apply (rule vv1_subset)
@@ -321,8 +322,8 @@
(\<Union>b<a. f`b)=y; Ord(a); m \<in> nat; s \<in> f`b; b<a |]
==> (\<Union>g<a++a. gg2(f,a,b,s) ` g) = y"
apply (unfold gg2_def)
-apply (drule sym)
-apply (simp add: UN_oadd lt_oadd1 oadd_le_self [THEN le_imp_not_lt]
+apply (drule sym)
+apply (simp add: ltD UN_oadd oadd_le_self [THEN le_imp_not_lt]
lt_Ord odiff_oadd_inverse ww2_def
vv2_subset [THEN Diff_partition])
done
@@ -361,7 +362,7 @@
\<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
(\<Union>b<a. f`b)=y; b<a; s \<in> f`b; m \<in> nat; m\<noteq> 0; g<a++a |]
==> gg2(f,a,b,s) ` g \<lesssim> m"
-apply (unfold gg2_def, simp)
+apply (simp add: gg2_def empty_lepollI)
apply (safe elim!: lt_Ord2 dest!: lt_oadd_odiff_disj)
apply (simp add: vv2_lepoll)
apply (simp add: ww2_lepoll vv2_subset)
--- a/src/ZF/Epsilon.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/Epsilon.thy Thu May 23 17:05:21 2002 +0200
@@ -278,14 +278,14 @@
"P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"
by (simp add: the_0 the_equality2)
-(*The premise is needed not just to fix i but to ensure f~=0*)
-lemma rank_apply: "i : domain(f) ==> rank(f`i) < rank(f)"
-apply (unfold apply_def, clarify)
-apply (subgoal_tac "rank (y) < rank (f) ")
-prefer 2 apply (blast intro: lt_trans rank_lt rank_pair2)
-apply (subgoal_tac "0 < rank (f) ")
-apply (erule_tac [2] Ord_rank [THEN Ord_0_le, THEN lt_trans1])
-apply (simp add: the_equality_if)
+(*The first premise not only fixs i but ensures f~=0.
+ The second premise is now essential. Consider otherwise the relation
+ r = {<0,0>,<0,1>,<0,2>,...}. Then f`0 = Union(f``{0}) = Union(nat) = nat,
+ whose rank equals that of r.*)
+lemma rank_apply: "[|i : domain(f); function(f)|] ==> rank(f`i) < rank(f)"
+apply (clarify );
+apply (simp add: function_apply_equality);
+apply (blast intro: lt_trans rank_lt rank_pair2)
done
@@ -323,8 +323,8 @@
lemma transrec2_Limit:
"Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
-apply (rule transrec2_def [THEN def_transrec, THEN trans], simp)
-apply (blast dest!: Limit_has_0 elim!: succ_LimitE)
+apply (rule transrec2_def [THEN def_transrec, THEN trans])
+apply (auto simp add: OUnion_def);
done
--- a/src/ZF/Induct/Multiset.ML Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/Induct/Multiset.ML Thu May 23 17:05:21 2002 +0200
@@ -284,22 +284,18 @@
by (auto_tac (claset(), simpset()
addsimps [multiset_fun_iff, mset_of_def, funrestrict_def]));
qed "mdiff_0";
-Addsimps [mdiff_0];
+Addsimps [mdiff_0];
-Goalw [multiset_def] "multiset(M) ==> M +# {#a#} -# {#a#} = M";
-by (rewrite_goals_tac [munion_def, mdiff_def,
+Goal "multiset(M) ==> M +# {#a#} -# {#a#} = M";
+by (rewrite_goals_tac [multiset_def, munion_def, mdiff_def,
msingle_def, normalize_def, mset_of_def]);
-by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
+by (auto_tac (claset(),
+ simpset() addcongs [if_cong]
+ addsimps [ltD, multiset_fun_iff,
+ funrestrict_def, subset_Un_iff2 RS iffD1]));
+by (subgoal_tac "{x \\<in> A \\<union> {a} . x \\<noteq> a \\<and> x \\<in> A} = A" 2);
by (rtac fun_extension 1);
-by Auto_tac;
-by (res_inst_tac [("P", "%x. ?u : Pi(x, ?v)")] subst 1);
-by (rtac funrestrict_type 2);
-by (rtac equalityI 1);
-by (ALLGOALS(Clarify_tac));
-by Auto_tac;
-by (res_inst_tac [("Pa", "~(1<?u)")] swap 1);
-by (case_tac "x=a" 3);
-by (ALLGOALS(Asm_full_simp_tac));
+by Auto_tac;
qed "mdiff_union_inverse2";
Addsimps [mdiff_union_inverse2];
--- a/src/ZF/Induct/Ntree.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/Induct/Ntree.thy Thu May 23 17:05:21 2002 +0200
@@ -114,21 +114,21 @@
\medskip @{text ntree} recursion.
*}
-lemma ntree_rec_Branch: "ntree_rec(b, Branch(x,h))
- = b(x, h, \<lambda>i \<in> domain(h). ntree_rec(b, h`i))"
+lemma ntree_rec_Branch:
+ "function(h) ==>
+ ntree_rec(b, Branch(x,h)) = b(x, h, \<lambda>i \<in> domain(h). ntree_rec(b, h`i))"
apply (rule ntree_rec_def [THEN def_Vrecursor, THEN trans])
apply (simp add: ntree.con_defs rank_pair2 [THEN [2] lt_trans] rank_apply)
done
lemma ntree_copy_Branch [simp]:
- "ntree_copy (Branch(x, h)) = Branch(x, \<lambda>i \<in> domain(h). ntree_copy (h`i))"
- apply (unfold ntree_copy_def)
- apply (rule ntree_rec_Branch)
- done
+ "function(h) ==>
+ ntree_copy (Branch(x, h)) = Branch(x, \<lambda>i \<in> domain(h). ntree_copy (h`i))"
+ by (simp add: ntree_copy_def ntree_rec_Branch)
lemma ntree_copy_is_ident: "z \<in> ntree(A) ==> ntree_copy(z) = z"
apply (induct_tac z)
- apply (auto simp add: domain_of_fun Pi_Collect_iff)
+ apply (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function)
done
--- a/src/ZF/Integ/Bin.ML Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/Integ/Bin.ML Thu May 23 17:05:21 2002 +0200
@@ -7,6 +7,7 @@
*)
+Addsimps bin.intrs;
AddTCs bin.intrs;
Goal "NCons(Pls,0) = Pls";
--- a/src/ZF/Integ/IntDiv.ML Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/Integ/IntDiv.ML Thu May 23 17:05:21 2002 +0200
@@ -369,7 +369,7 @@
Addsimps [adjust_eq];
-Goal "[| #0 $< b; \\<not> a $< b |] \
+Goal "[| #0 $< b; ~ a $< b |] \
\ ==> nat_of(a $- #2 $\\<times> b $+ #1) < nat_of(a $- b $+ #1)";
by (simp_tac (simpset() addsimps [zless_nat_conj]) 1);
by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle,
@@ -382,8 +382,8 @@
\ posDivAlg(<a,b>) = \
\ (if a$<b then <#0,a> else adjust(b, posDivAlg (<a, #2$*b>)))";
by (rtac (posDivAlg_unfold RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
-by (asm_simp_tac (simpset() addsimps [vimage_iff, posDivAlg_termination]) 1);
+by (asm_simp_tac (simpset() addsimps [vimage_iff, not_zless_iff_zle RS iff_sym]) 1);
+by (blast_tac (claset() addIs [posDivAlg_termination]) 1);
qed "posDivAlg_eqn";
val [prem] =
@@ -529,8 +529,7 @@
(*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***)
-Goal "[| #0 $< b; \\<not> #0 $<= a $+ b |] \
-\ ==> nat_of($- a $- #2 $\\<times> b) < nat_of($- a $- b)";
+Goal "[| #0 $< b; a $+ b $< #0 |] ==> nat_of($- a $- #2 $* b) < nat_of($- a $- b)";
by (simp_tac (simpset() addsimps [zless_nat_conj]) 1);
by (asm_full_simp_tac (simpset() addsimps zcompare_rls @
[not_zle_iff_zless, zless_zdiff_iff RS iff_sym, zless_zminus]) 1);
@@ -538,14 +537,13 @@
val negDivAlg_unfold = wf_measure RS (negDivAlg_def RS def_wfrec);
-Goal "[| #0 $< b; a \\<in> int; b \\<in> int |] ==> \
+Goal "[| #0 $< b; a : int; b : int |] ==> \
\ negDivAlg(<a,b>) = \
\ (if #0 $<= a$+b then <#-1,a$+b> \
\ else adjust(b, negDivAlg (<a, #2$*b>)))";
by (rtac (negDivAlg_unfold RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
-by (asm_simp_tac (simpset() addsimps [not_zle_iff_zless, vimage_iff,
- negDivAlg_termination]) 1);
+by (asm_simp_tac (simpset() addsimps [vimage_iff, not_zless_iff_zle RS iff_sym]) 1);
+by (blast_tac (claset() addIs [negDivAlg_termination]) 1);
qed "negDivAlg_eqn";
val [prem] =
@@ -640,15 +638,17 @@
qed "posDivAlg_0";
Addsimps [posDivAlg_0];
-Goal "negDivAlg (<#-1,b>) = <#-1, b$-#1>";
-by (stac negDivAlg_unfold 1);
-by Auto_tac;
-(*ALL the rest is linear arithmetic: to notice the contradiction*)
+(*Needed below. Actually it's an equivalence.*)
+Goal "~ (#0 $<= #-1 $+ b) ==> (b $<= #0)";
by (asm_full_simp_tac (simpset() addsimps [not_zle_iff_zless]) 1);
by (dtac (zminus_zless_zminus RS iffD2) 1);
by (asm_full_simp_tac (simpset() addsimps [zadd_commute, zless_add1_iff_zle,
zle_zminus]) 1);
-by (asm_full_simp_tac (simpset() addsimps [not_zle_iff_zless RS iff_sym]) 1);
+qed "linear_arith_lemma";
+
+Goal "negDivAlg (<#-1,b>) = <#-1, b$-#1>";
+by (stac negDivAlg_unfold 1);
+by (asm_full_simp_tac (simpset() addsimps [linear_arith_lemma, integ_of_type, vimage_iff]) 1);
qed "negDivAlg_minus1";
Addsimps [negDivAlg_minus1];
--- a/src/ZF/List.ML Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/List.ML Thu May 23 17:05:21 2002 +0200
@@ -8,6 +8,8 @@
(*** Aspects of the datatype definition ***)
+Addsimps list.intrs;
+
(*An elimination rule, for type-checking*)
bind_thm ("ConsE", list.mk_cases "Cons(a,l) : list(A)");
--- a/src/ZF/OrdQuant.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/OrdQuant.thy Thu May 23 17:05:21 2002 +0200
@@ -182,8 +182,6 @@
"[| 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)
--- a/src/ZF/Perm.ML Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/Perm.ML Thu May 23 17:05:21 2002 +0200
@@ -146,7 +146,7 @@
bind_thm ("id_inj", subset_refl RS id_subset_inj);
Goalw [id_def,surj_def] "id(A): surj(A,A)";
-by (blast_tac (claset() addIs [lam_type, beta]) 1);
+by (Asm_simp_tac 1);
qed "id_surj";
Goalw [bij_def] "id(A): bij(A,A)";
@@ -342,7 +342,7 @@
by (rtac comp_fun 1);
by (rtac lam_funtype 2);
by (typecheck_tac (tcset() addTCs [prem]));
-by (asm_simp_tac (simpset()
+by (asm_simp_tac (simpset() addsimps [prem]
setSolver (mk_solver ""
(type_solver_tac (tcset() addTCs [prem, lam_funtype])))) 1);
qed "comp_lam";
--- a/src/ZF/Univ.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/Univ.thy Thu May 23 17:05:21 2002 +0200
@@ -488,7 +488,7 @@
apply (unfold Vrec_def)
apply (subst transrec)
apply simp
-apply (rule refl [THEN lam_cong, THEN subst_context], simp)
+apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
done
text{*This form avoids giant explosions in proofs. NOTE USE OF == *}
@@ -504,7 +504,7 @@
"Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x), a)"
apply (unfold Vrecursor_def)
apply (subst transrec, simp)
-apply (rule refl [THEN lam_cong, THEN subst_context], simp)
+apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
done
text{*This form avoids giant explosions in proofs. NOTE USE OF == *}
--- a/src/ZF/WF.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/WF.thy Thu May 23 17:05:21 2002 +0200
@@ -213,8 +213,9 @@
lemma apply_recfun:
"[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
apply (unfold is_recfun_def)
-apply (erule_tac P = "%x.?t (x) = (?u::i) " in ssubst)
-apply (erule underI [THEN beta])
+ txt{*replace f only on the left-hand side*}
+apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
+apply (simp add: underI);
done
lemma is_recfun_equal [rule_format]:
@@ -280,7 +281,7 @@
apply (frule spec [THEN mp], assumption)
apply (subgoal_tac "<xa,a1> : r")
apply (drule_tac x1 = "xa" in spec [THEN mp], assumption)
-apply (simp add: vimage_singleton_iff underI [THEN beta]
+apply (simp add: vimage_singleton_iff
apply_recfun is_recfun_cut)
apply (blast dest: transD)
done
--- a/src/ZF/ZF.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/ZF.thy Thu May 23 17:05:21 2002 +0200
@@ -145,11 +145,11 @@
syntax (xsymbols)
"op *" :: "[i, i] => i" (infixr "\\<times>" 80)
- "op Int" :: "[i, i] => i" (infixl "\\<inter>" 70)
- "op Un" :: "[i, i] => i" (infixl "\\<union>" 65)
+ "op Int" :: "[i, i] => i" (infixl "\\<inter>" 70)
+ "op Un" :: "[i, i] => i" (infixl "\\<union>" 65)
"op ->" :: "[i, i] => i" (infixr "\\<rightarrow>" 60)
- "op <=" :: "[i, i] => o" (infixl "\\<subseteq>" 50)
- "op :" :: "[i, i] => o" (infixl "\\<in>" 50)
+ "op <=" :: "[i, i] => o" (infixl "\\<subseteq>" 50)
+ "op :" :: "[i, i] => o" (infixl "\\<in>" 50)
"op ~:" :: "[i, i] => o" (infixl "\\<notin>" 50)
"@Collect" :: "[pttrn, i, o] => i" ("(1{_ \\<in> _ ./ _})")
"@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \\<in> _, _})")
@@ -261,7 +261,7 @@
(* Abstraction, application and Cartesian product of a family of sets *)
lam_def "Lambda(A,b) == {<x,b(x)> . x:A}"
- apply_def "f`a == THE y. <a,y> : f"
+ apply_def "f`a == Union(f``{a})"
Pi_def "Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
(* Restrict the relation r to the domain A *)
--- a/src/ZF/Zorn.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/Zorn.thy Thu May 23 17:05:21 2002 +0200
@@ -222,10 +222,10 @@
"ch: (PROD X: Pow(chain(S))-{0}. X) ==>
EX next: increasing(S). ALL X: Pow(S).
next`X = if(X: chain(S)-maxchain(S), ch`super(S,X), X)"
-apply (rule bexI)
-apply (rule ballI)
-apply (rule beta)
-apply assumption
+apply (rule_tac x="\<lambda>X\<in>Pow(S).
+ if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X"
+ in bexI)
+apply (force );
apply (unfold increasing_def)
apply (rule CollectI)
apply (rule lam_type)
@@ -236,7 +236,7 @@
apply safe
apply (drule choice_super)
apply (assumption+)
-apply (unfold super_def)
+apply (simp add: super_def)
apply blast
done
@@ -366,11 +366,10 @@
lemma Zermelo_next_exists:
"ch: (PROD X: Pow(S)-{0}. X) ==>
EX next: increasing(S). ALL X: Pow(S).
- next`X = if(X=S, S, cons(ch`(S-X), X))"
-apply (rule bexI)
-apply (rule ballI)
-apply (rule beta)
-apply assumption
+ next`X = (if X=S then S else cons(ch`(S-X), X))"
+apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
+ in bexI)
+apply (force );
apply (unfold increasing_def)
apply (rule CollectI)
apply (rule lam_type)
--- a/src/ZF/ex/Limit.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/ex/Limit.thy Thu May 23 17:05:21 2002 +0200
@@ -1066,7 +1066,7 @@
(*looks like something should be inserted into the assumptions!*)
apply (rule_tac P = "%t. rel (DD`na,t,lub (DD`na,\<lambda>x \<in> nat. X`x`na))"
and b1 = "%n. X`n`na" in beta [THEN subst])
-apply (simp del: beta
+apply (simp del: beta_if
add: chain_iprod [THEN cpo_lub, THEN islub_ub] iprodE
chain_in)+
apply (blast intro: iprodI lam_type chain_iprod [THEN cpo_lub, THEN islub_in])
@@ -2167,7 +2167,8 @@
((\<lambda>n \<in> nat. f(n) O Rp(DD ` n, E, r(n))) ` na)) =
(\<lambda>na \<in> nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))"
apply (rule fun_extension)
-apply (auto intro: lam_type)
+(*something wrong here*)
+apply (auto simp del: beta_if simp add: beta intro: lam_type)
done
lemma chain_lemma:
--- a/src/ZF/func.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/func.thy Thu May 23 17:05:21 2002 +0200
@@ -58,7 +58,7 @@
(*Applying a function outside its domain yields 0*)
lemma apply_0: "a ~: domain(f) ==> f`a = 0"
apply (unfold apply_def)
-apply (rule the_0, blast)
+apply (blast intro: elim:);
done
lemma Pi_memberD: "[| f: Pi(A,B); c: f |] ==> EX x:A. c = <x,f`x>"
@@ -67,8 +67,12 @@
done
lemma function_apply_Pair: "[| function(f); a : domain(f)|] ==> <a,f`a>: f"
-apply (simp add: function_def apply_def)
-apply (rule theI2, auto)
+apply (simp add: function_def)
+apply (clarify );
+apply (subgoal_tac "f`a = y")
+apply (blast intro: elim:);
+apply (simp add: apply_def);
+apply (blast intro: elim:);
done
lemma apply_Pair: "[| f: Pi(A,B); a:A |] ==> <a,f`a>: f"
@@ -145,8 +149,15 @@
lemma relation_lam: "relation (lam x:A. b(x))"
by (simp add: relation_def lam_def)
-lemma beta [simp]: "a : A ==> (lam x:A. b(x)) ` a = b(a)"
-by (blast intro: apply_equality lam_funtype lamI)
+lemma beta_if [simp]: "(lam x:A. b(x)) ` a = (if a : A then b(a) else 0)"
+apply (simp add: apply_def lam_def)
+apply (blast intro: elim:);
+done
+
+lemma beta: "a : A ==> (lam x:A. b(x)) ` a = b(a)"
+apply (simp add: apply_def lam_def)
+apply (blast intro: elim:);
+done
lemma lam_empty [simp]: "(lam x:0. b(x)) = 0"
by (simp add: lam_def)
@@ -161,9 +172,8 @@
lemma lam_theI:
"(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)"
-apply (rule_tac x = "lam x: A. THE y. Q (x,y) " in exI)
-apply (rule ballI)
-apply (subst beta, assumption)
+apply (rule_tac x = "lam x: A. THE y. Q (x,y)" in exI)
+apply (simp add: );
apply (blast intro: theI)
done
@@ -263,7 +273,9 @@
by (simp add: Pi_iff function_def restrict_def, blast)
lemma restrict: "a : A ==> restrict(f,A) ` a = f`a"
-by (simp add: apply_def restrict_def)
+apply (simp add: apply_def restrict_def)
+apply (blast intro: elim:);
+done
lemma restrict_empty [simp]: "restrict(f,0) = 0"
apply (unfold restrict_def)