equal
deleted
inserted
replaced
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 |