1(*  Title:      HOL/UNITY/Detects.thy
2    Author:     Tanja Vos, Cambridge University Computer Laboratory
3    Copyright   2000  University of Cambridge
4
5Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
6*)
7
8section\<open>The Detects Relation\<close>
9
10theory Detects imports FP SubstAx begin
11
12definition Detects :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
13  where "A Detects B = (Always (-A \<union> B)) \<inter> (B LeadsTo A)"
14
15definition Equality :: "['a set, 'a set] => 'a set"  (infixl "<==>" 60)
16  where "A <==> B = (-A \<union> B) \<inter> (A \<union> -B)"
17
18
19(* Corollary from Sectiom 3.6.4 *)
20
21lemma Always_at_FP:
22     "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
23supply [[simproc del: boolean_algebra_cancel_inf]] inf_compl_bot_right[simp del] 
24apply (rule LeadsTo_empty)
25apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
26apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
27apply (subgoal_tac "(B \<inter> (FP F \<inter> -B)) = {}")
28apply auto
29apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
30done
31
32
33lemma Detects_Trans: 
34     "[| F \<in> A Detects B; F \<in> B Detects C |] ==> F \<in> A Detects C"
35apply (unfold Detects_def Int_def)
36apply (simp (no_asm))
37apply safe
38apply (rule_tac [2] LeadsTo_Trans, auto)
39apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
40 apply (blast intro: Always_weaken)
41apply (simp add: Always_Int_distrib)
42done
43
44lemma Detects_refl: "F \<in> A Detects A"
45apply (unfold Detects_def)
46apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
47done
48
49lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
50by (unfold Equality_def, blast)
51
52(*Not quite antisymmetry: sets A and B agree in all reachable states *)
53lemma Detects_antisym: 
54     "[| F \<in> A Detects B;  F \<in> B Detects A|] ==> F \<in> Always (A <==> B)"
55apply (unfold Detects_def Equality_def)
56apply (simp add: Always_Int_I Un_commute)
57done
58
59
60(* Theorem from Section 3.8 *)
61
62lemma Detects_Always: 
63     "[|F \<in> A Detects B; all_total F|] ==> F \<in> Always (-(FP F) \<union> (A <==> B))"
64apply (unfold Detects_def Equality_def)
65apply (simp add: Un_Int_distrib Always_Int_distrib)
66apply (blast dest: Always_at_FP intro: Always_weaken)
67done
68
69(* Theorem from exercise 11.1 Section 11.3.1 *)
70
71lemma Detects_Imp_LeadstoEQ: 
72     "F \<in> A Detects B ==> F \<in> UNIV LeadsTo (A <==> B)"
73apply (unfold Detects_def Equality_def)
74apply (rule_tac B = B in LeadsTo_Diff)
75 apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
76apply (blast intro: Always_LeadsTo_weaken)
77done
78
79
80end
81
82