src/HOL/UNITY/WFair.ML
changeset 8948 b797cfa3548d
parent 8835 56187238220d
child 9084 090d450af656
equal deleted inserted replaced
8947:971aedd340e4 8948:b797cfa3548d
   398 qed "bounded_induct";
   398 qed "bounded_induct";
   399 
   399 
   400 
   400 
   401 (*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
   401 (*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
   402 val prems = 
   402 val prems = 
   403 Goal "[| !!m. F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
   403 Goal "[| !!m::nat. F : (A Int f-``{m}) leadsTo ((A Int f-``{..m(}) Un B) |] \
   404 \     ==> F : A leadsTo B";
   404 \     ==> F : A leadsTo B";
   405 by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
   405 by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
   406 by (Asm_simp_tac 1);
   406 by (Asm_simp_tac 1);
   407 by (blast_tac (claset() addIs prems) 1);
   407 by (blast_tac (claset() addIs prems) 1);
   408 qed "lessThan_induct";
   408 qed "lessThan_induct";
   409 
   409 
   410 Goal "[| ALL m:(greaterThan l).    \
   410 Goal "!!l::nat. [| ALL m:(greaterThan l).    \
   411 \           F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
   411 \           F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
   412 \     ==> F : A leadsTo ((A Int (f-``(atMost l))) Un B)";
   412 \     ==> F : A leadsTo ((A Int (f-``(atMost l))) Un B)";
   413 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
   413 by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, 
   414 			       Compl_greaterThan RS sym]) 1);
   414 			       Compl_greaterThan RS sym]) 1);
   415 by (rtac (wf_less_than RS bounded_induct) 1);
   415 by (rtac (wf_less_than RS bounded_induct) 1);
   416 by (Asm_simp_tac 1);
   416 by (Asm_simp_tac 1);
   417 qed "lessThan_bounded_induct";
   417 qed "lessThan_bounded_induct";
   418 
   418 
   419 Goal "[| ALL m:(lessThan l).    \
   419 Goal "!!l::nat. [| ALL m:(lessThan l).    \
   420 \           F : (A Int f-``{m}) leadsTo ((A Int f-``(greaterThan m)) Un B) |] \
   420 \           F : (A Int f-``{m}) leadsTo ((A Int f-``(greaterThan m)) Un B) |] \
   421 \     ==> F : A leadsTo ((A Int (f-``(atLeast l))) Un B)";
   421 \     ==> F : A leadsTo ((A Int (f-``(atLeast l))) Un B)";
   422 by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
   422 by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
   423     (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
   423     (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
   424 by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
   424 by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);