src/HOL/UNITY/WFair.ML
changeset 10064 1a77667b21ef
parent 9084 090d450af656
child 10797 028d22926a41
equal deleted inserted replaced
10063:947ee8608b90 10064:1a77667b21ef
   235 by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
   235 by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
   236 			       leadsTo_Trans]) 1);
   236 			       leadsTo_Trans]) 1);
   237 qed "leadsTo_weaken";
   237 qed "leadsTo_weaken";
   238 
   238 
   239 
   239 
   240 (*Set difference: maybe combine with leadsTo_weaken_L??*)
   240 (*Set difference: maybe combine with leadsTo_weaken_L?*)
   241 Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |]   ==> F : A leadsTo C";
   241 Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |]   ==> F : A leadsTo C";
   242 by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
   242 by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
   243 qed "leadsTo_Diff";
   243 qed "leadsTo_Diff";
   244 
   244 
   245 val prems = goal thy
   245 val prems = goal thy
   371 by (blast_tac (claset() addIs [leadsTo_UN]) 2);
   371 by (blast_tac (claset() addIs [leadsTo_UN]) 2);
   372 by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
   372 by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
   373 val lemma = result();
   373 val lemma = result();
   374 
   374 
   375 
   375 
   376 (** Meta or object quantifier ????? **)
   376 (** Meta or object quantifier ? **)
   377 Goal "[| wf r;     \
   377 Goal "[| wf r;     \
   378 \        ALL m. F : (A Int f-``{m}) leadsTo                     \
   378 \        ALL m. F : (A Int f-``{m}) leadsTo                     \
   379 \                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
   379 \                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \
   380 \     ==> F : A leadsTo B";
   380 \     ==> F : A leadsTo B";
   381 by (res_inst_tac [("t", "A")] subst 1);
   381 by (res_inst_tac [("t", "A")] subst 1);