tidying
authorpaulson
Thu Jan 28 10:21:45 1999 +0100 (1999-01-28)
changeset 6158981f96a598f5
parent 6157 29942d3a1818
child 6159 833b76d0e6dc
tidying
src/ZF/ex/Limit.ML
     1.1 --- a/src/ZF/ex/Limit.ML	Wed Jan 27 17:11:39 1999 +0100
     1.2 +++ b/src/ZF/ex/Limit.ML	Thu Jan 28 10:21:45 1999 +0100
     1.3 @@ -72,8 +72,10 @@
     1.4  Goal "[|cpo(D); x:set(D)|] ==> rel(D,x,x)";
     1.5  by (blast_tac (claset() addIs [po_refl, cpo_po]) 1);
     1.6  qed "cpo_refl";
     1.7 +
     1.8  Addsimps [cpo_refl];
     1.9  AddSIs   [cpo_refl];
    1.10 +AddTCs   [cpo_refl];
    1.11  
    1.12  Goal "[|cpo(D); rel(D,x,y); rel(D,y,z); x:set(D);  \
    1.13  \       y:set(D); z:set(D)|] ==> rel(D,x,z)";
    1.14 @@ -170,20 +172,15 @@
    1.15  qed "chain_rel";
    1.16  
    1.17  Addsimps [chain_in, chain_rel];
    1.18 +AddTCs   [chain_in, chain_rel];
    1.19  
    1.20  Goal "[|chain(D,X); cpo(D); n:nat; m:nat|] ==> rel(D,X`n,(X`(m #+ n)))";
    1.21  by (induct_tac "m" 1);
    1.22  by (ALLGOALS Simp_tac);
    1.23 -by (rtac cpo_trans 2); (* loops if repeated *)
    1.24 -by (REPEAT (ares_tac [cpo_refl,chain_in,chain_rel,nat_succI,add_type] 1));
    1.25 +by (rtac cpo_trans 1);
    1.26 +by Auto_tac;
    1.27  qed "chain_rel_gen_add";
    1.28  
    1.29 -Goal "[| n le succ(x); ~ n le x; x : nat; n:nat |] ==> n = succ(x)";
    1.30 -by (etac le_anti_sym 1);
    1.31 -by (asm_simp_tac (simpset() addsimps [not_le_iff_lt RS iff_sym, 
    1.32 -				      nat_into_Ord]) 1);
    1.33 -qed "le_succ_eq";
    1.34 -
    1.35  Goal  (* chain_rel_gen *)
    1.36      "[|n le m; chain(D,X); cpo(D); n:nat; m:nat|] ==> rel(D,X`n,X`m)";
    1.37  by (rtac impE 1);  (* The first three steps prepare for the induction proof *)
    1.38 @@ -193,9 +190,8 @@
    1.39  by Safe_tac;
    1.40  by (Asm_full_simp_tac 1);
    1.41  by (rtac cpo_trans 2);
    1.42 -by (rtac (le_succ_eq RS subst) 1);
    1.43 -by (auto_tac (claset() addIs [chain_in,chain_rel],
    1.44 -	      simpset()));
    1.45 +by (auto_tac (claset(),
    1.46 +	      simpset() addsimps [le_iff]));
    1.47  qed "chain_rel_gen";
    1.48  
    1.49  (*----------------------------------------------------------------------*)
    1.50 @@ -226,6 +222,8 @@
    1.51  by (best_tac (claset() addIs [pcpo_bot_ex1 RS theI2]) 1);
    1.52  qed "bot_in";
    1.53  
    1.54 +AddTCs [pcpo_cpo, bot_least, bot_in];
    1.55 +
    1.56  val prems = goal Limit.thy  (* bot_unique *)
    1.57      "[| pcpo(D); x:set(D); !!y. y:set(D) ==> rel(D,x,y)|] ==> x = bot(D)";
    1.58  by (rtac cpo_antisym 1);
    1.59 @@ -749,6 +747,8 @@
    1.60  
    1.61  qed "cpo_cf";
    1.62  
    1.63 +AddTCs [cpo_cf];
    1.64 +
    1.65  Goal "[| chain(cf(D,E),X); cpo(D); cpo(E)|] ==>   \
    1.66  \     lub(cf(D,E), X) = (lam x:set(D). lub(E,lam n:nat. X`n`x))";
    1.67  by (blast_tac (claset() addIs [islub_unique,cpo_lub,islub_cf,cpo_cf]) 1);
    1.68 @@ -1191,6 +1191,8 @@
    1.69  brr(islub_iprod::prems) 1;
    1.70  qed "cpo_iprod";
    1.71  
    1.72 +AddTCs [cpo_iprod];
    1.73 +
    1.74  val prems = Goalw [islub_def,isub_def]  (* lub_iprod *)
    1.75      "[|chain(iprod(DD),X);  !!n. n:nat ==> cpo(DD`n)|] ==>   \
    1.76  \    lub(iprod(DD),X) = (lam n:nat. lub(DD`n,lam m:nat. X`m`n))";
    1.77 @@ -1423,7 +1425,8 @@
    1.78  
    1.79  Goal "emb_chain(DD,ee) ==> cpo(Dinf(DD,ee))";
    1.80  by (rtac subcpo_cpo 1);
    1.81 -by (auto_tac (claset() addIs [subcpo_Dinf,cpo_iprod,emb_chain_cpo], simpset()));
    1.82 +be subcpo_Dinf 1;
    1.83 +by (auto_tac (claset() addIs [cpo_iprod, emb_chain_cpo], simpset()));
    1.84  qed "cpo_Dinf";
    1.85  
    1.86  (* Again and again the proofs are much easier to WRITE in Isabelle, but