new definition of "apply" and new simprule "beta_if"
authorpaulson
Thu May 23 17:05:21 2002 +0200 (2002-05-23)
changeset 1317581082cfa5618
parent 13174 85d3c0981a16
child 13176 312bd350579b
new definition of "apply" and new simprule "beta_if"
src/ZF/AC/AC15_WO6.thy
src/ZF/AC/AC16_WO4.thy
src/ZF/AC/DC.thy
src/ZF/AC/WO6_WO1.thy
src/ZF/Epsilon.thy
src/ZF/Induct/Multiset.ML
src/ZF/Induct/Ntree.thy
src/ZF/Integ/Bin.ML
src/ZF/Integ/IntDiv.ML
src/ZF/List.ML
src/ZF/OrdQuant.thy
src/ZF/Perm.ML
src/ZF/Univ.thy
src/ZF/WF.thy
src/ZF/ZF.thy
src/ZF/Zorn.thy
src/ZF/ex/Limit.thy
src/ZF/func.thy
     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)