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