paulson@8334: (*  Title:      HOL/UNITY/Detects
paulson@8334:     ID:         $Id$
paulson@8334:     Author:     Tanja Vos, Cambridge University Computer Laboratory
paulson@8334:     Copyright   2000  University of Cambridge
paulson@8334: 
paulson@8334: Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
paulson@8334: *)
paulson@8334: 
paulson@13798: header{*The Detects Relation*}
paulson@13798: 
haftmann@16417: theory Detects imports FP SubstAx begin
paulson@8334: 
paulson@8334: consts
paulson@8334:    op_Detects  :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
paulson@8334:    op_Equality :: "['a set, 'a set] => 'a set"          (infixl "<==>" 60)
paulson@8334:    
paulson@8334: defs
paulson@13805:   Detects_def:  "A Detects B == (Always (-A \<union> B)) \<inter> (B LeadsTo A)"
paulson@13805:   Equality_def: "A <==> B == (-A \<union> B) \<inter> (A \<union> -B)"
paulson@13785: 
paulson@13785: 
paulson@13785: (* Corollary from Sectiom 3.6.4 *)
paulson@13785: 
paulson@13812: lemma Always_at_FP:
paulson@13812:      "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
paulson@13785: apply (rule LeadsTo_empty)
paulson@13805: apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
paulson@13805: apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
paulson@13805: apply (subgoal_tac "(B \<inter> (FP F \<inter> -B)) = {}")
paulson@13785: apply auto
paulson@13785: apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
paulson@13785: done
paulson@13785: 
paulson@13785: 
paulson@13785: lemma Detects_Trans: 
paulson@13805:      "[| F \<in> A Detects B; F \<in> B Detects C |] ==> F \<in> A Detects C"
paulson@13785: apply (unfold Detects_def Int_def)
paulson@13785: apply (simp (no_asm))
paulson@13785: apply safe
paulson@13812: apply (rule_tac [2] LeadsTo_Trans, auto)
paulson@13805: apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
paulson@13785:  apply (blast intro: Always_weaken)
paulson@13785: apply (simp add: Always_Int_distrib)
paulson@13785: done
paulson@13785: 
paulson@13805: lemma Detects_refl: "F \<in> A Detects A"
paulson@13785: apply (unfold Detects_def)
paulson@13785: apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
paulson@13785: done
paulson@13785: 
paulson@13805: lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
paulson@13812: by (unfold Equality_def, blast)
paulson@13785: 
paulson@13785: (*Not quite antisymmetry: sets A and B agree in all reachable states *)
paulson@13785: lemma Detects_antisym: 
paulson@13805:      "[| F \<in> A Detects B;  F \<in> B Detects A|] ==> F \<in> Always (A <==> B)"
paulson@13785: apply (unfold Detects_def Equality_def)
paulson@13785: apply (simp add: Always_Int_I Un_commute)
paulson@13785: done
paulson@13785: 
paulson@13785: 
paulson@13785: (* Theorem from Section 3.8 *)
paulson@13785: 
paulson@13785: lemma Detects_Always: 
paulson@13812:      "[|F \<in> A Detects B; all_total F|] ==> F \<in> Always (-(FP F) \<union> (A <==> B))"
paulson@13785: apply (unfold Detects_def Equality_def)
paulson@13812: apply (simp add: Un_Int_distrib Always_Int_distrib)
paulson@13785: apply (blast dest: Always_at_FP intro: Always_weaken)
paulson@13785: done
paulson@13785: 
paulson@13785: (* Theorem from exercise 11.1 Section 11.3.1 *)
paulson@13785: 
paulson@13785: lemma Detects_Imp_LeadstoEQ: 
paulson@13805:      "F \<in> A Detects B ==> F \<in> UNIV LeadsTo (A <==> B)"
paulson@13785: apply (unfold Detects_def Equality_def)
paulson@13812: apply (rule_tac B = B in LeadsTo_Diff)
paulson@13805:  apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
paulson@13805: apply (blast intro: Always_LeadsTo_weaken)
paulson@13785: done
paulson@13785: 
paulson@8334: 
paulson@8334: end
paulson@8334: