src/HOL/UNITY/Detects.thy
changeset 61635 c657ee4f59b7
parent 58889 5b7a9633cfa8
child 63146 f1ecba0272f9
equal deleted inserted replaced
61634:48e2de1b1df5 61635:c657ee4f59b7
    18 
    18 
    19 (* Corollary from Sectiom 3.6.4 *)
    19 (* Corollary from Sectiom 3.6.4 *)
    20 
    20 
    21 lemma Always_at_FP:
    21 lemma Always_at_FP:
    22      "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
    22      "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
       
    23 supply [[simproc del: boolean_algebra_cancel_inf]] inf_compl_bot_right[simp del] 
    23 apply (rule LeadsTo_empty)
    24 apply (rule LeadsTo_empty)
    24 apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
    25 apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
    25 apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
    26 apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
    26 apply (subgoal_tac "(B \<inter> (FP F \<inter> -B)) = {}")
    27 apply (subgoal_tac "(B \<inter> (FP F \<inter> -B)) = {}")
    27 apply auto
    28 apply auto