src/ZF/UNITY/WFair.ML

 by (subgoal_tac "P(zb) --> P(za)" 1);
 (*now solve first subgoal: this formula is sufficient*)
 by (blast_tac (claset() addIs leadsTo_refl::prems) 1);
 by (rtac (major RS leadsTo_induct) 1);
 by (REPEAT (blast_tac (claset() addIs prems) 1));
-qed "lemma";
+qed "leadsTo_induct_pre_aux";
 
 
 val [major, zb_prem, basis_prem, union_prem] = Goal
   "[| F : za leadsTo zb;  \
 \     P(zb); \

 \     !!S. ALL A:S. F : A leadsTo zb & P(A) & st_set(A) ==> P(Union(S)) \
 \  |] ==> P(za)";
 by (cut_facts_tac [major] 1);
 by (subgoal_tac "(F : za leadsTo zb) & P(za)" 1);
 by (etac conjunct2 1);
-by (rtac (major RS lemma) 1);
+by (rtac (major RS leadsTo_induct_pre_aux) 1);
 by (blast_tac (claset() addDs [leadsToD2]
                         addIs [leadsTo_Union,union_prem]) 3);
 by (blast_tac (claset() addIs [leadsTo_Trans,basis_prem, leadsTo_Basis]) 2);
 by (blast_tac (claset() addIs [leadsTo_refl,zb_prem] 
                         addDs [leadsToD2]) 1);

 by (asm_simp_tac (simpset() delsimps UN_simps
 			    addsimps [Int_UN_distrib]) 2);
 by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
 by (auto_tac (claset() addIs [leadsTo_UN], 
               simpset()  delsimps UN_simps addsimps [Int_UN_distrib]));
-qed "lemma1";
+qed "leadsTo_wf_induct_aux";
 
 (** Meta or object quantifier ? **)
 Goal "[| wf(r); \
 \        field(r)<=I; \
 \        A<=f-``I;\ 

 \     ==> F : A leadsTo B";
 by (res_inst_tac [("b", "A")] subst 1);
 by (res_inst_tac [("I", "I")] leadsTo_UN 2);
 by (REPEAT (assume_tac 2));
 by (Clarify_tac 2);
-by (eres_inst_tac [("I", "I")] lemma1 2);
+by (eres_inst_tac [("I", "I")] leadsTo_wf_induct_aux 2);
 by (REPEAT (assume_tac 2));
 by (rtac equalityI 1);
 by Safe_tac;
 by (thin_tac "field(r)<=I" 1);
 by (dres_inst_tac [("c", "x")] subsetD 1);

 \      F : (A1 - B) co (A1 Un B); \
 \      F : (A2 - C) co (A2 Un C) |] \
 \   ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)";
 by (Clarify_tac 1);
 by (Blast_tac 1);
-qed "lemma1";
+qed "leadsTo_123_aux";
 
 (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
 (* slightly different from the HOL one: B here is bounded *)
 Goal "F : A leadsTo A' \
 \     ==> EX B:Pow(state). A<=B & F:B leadsTo A' & F : (B-A') co (B Un A')";

 (*Basis*)
 by (blast_tac (claset() addDs [ensuresD, constrainsD2, st_setD]) 1);
 (*Trans*)
 by (Clarify_tac 1);
 by (res_inst_tac [("x", "Ba Un Bb")] bexI 1);
-by (blast_tac (claset() addIs [lemma1,leadsTo_Un_Un, leadsTo_cancel1,
+by (blast_tac (claset() addIs [leadsTo_123_aux,leadsTo_Un_Un, leadsTo_cancel1,
                                leadsTo_Un_duplicate]) 1);
 by (Blast_tac 1);
 (*Union*)
 by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1]) 1);
 by (subgoal_tac "EX y. y:Pi(S, %A. {Ba:Pow(state). A<=Ba & \