Quelle  Detects.thy   Sprache: Isabelle

(*  Title:      HOL/UNITY/Detects.thy
    Author:     Tanja Vos, Cambridge University Computer Laboratory
    Copyright   2000  University of Cambridge

Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
*)

section‹The Detects Relation›

theory Detects imports FP SubstAx begin

definition Detects :: "['a set, 'a set] => 'a program set"  (infixl ‹Detects› 60)
  where "A Detects B = (Always (-A \ B)) \ (B LeadsTo A)"

definition Equality :: "['a set, 'a set] => 'a set"  (infixl ‹<==>› 60)
  where "A <==> B = (-A \ B) \ (A \ -B)"


(* Corollary from Sectiom 3.6.4 *)

lemma Always_at_FP:
     "[|F \ A LeadsTo B; all_total F|] ==> F \ Always (-((FP F) \ A \ -B))"
supply [[simproc del: boolean_algebra_cancel_inf]] inf_compl_bot_right[simp del] 
apply (rule LeadsTo_empty)
apply (subgoal_tac "F \ (FP F \ A \ - B) LeadsTo (B \ (FP F \ -B))")
apply (subgoal_tac [2] " (FP F \ A \ - B) = (A \ (FP F \ -B))")
apply (subgoal_tac "(B \ (FP F \ -B)) = {}")
apply auto
apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
done


lemma Detects_Trans: 
     "[| F \ A Detects B; F \ B Detects C |] ==> F \ A Detects C"
apply (unfold Detects_def Int_def)
apply (simp (no_asm))
apply safe
apply (rule_tac [2] LeadsTo_Trans, auto)
apply (subgoal_tac "F \ Always ((-A \ B) \ (-B \ C))")
 apply (blast intro: Always_weaken)
apply (simp add: Always_Int_distrib)
done

lemma Detects_refl: "F \ A Detects A"
apply (unfold Detects_def)
apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
done

lemma Detects_eq_Un: "(A<==>B) = (A \ B) \ (-A \ -B)"
by (unfold Equality_def, blast)

(*Not quite antisymmetry: sets A and B agree in all reachable states *)
lemma Detects_antisym: 
     "[| F \ A Detects B; F \ B Detects A|] ==> F \ Always (A <==> B)"
apply (unfold Detects_def Equality_def)
apply (simp add: Always_Int_I Un_commute)
done


(* Theorem from Section 3.8 *)

lemma Detects_Always: 
     "[|F \ A Detects B; all_total F|] ==> F \ Always (-(FP F) \ (A <==> B))"
apply (unfold Detects_def Equality_def)
apply (simp add: Un_Int_distrib Always_Int_distrib)
apply (blast dest: Always_at_FP intro: Always_weaken)
done

(* Theorem from exercise 11.1 Section 11.3.1 *)

lemma Detects_Imp_LeadstoEQ: 
     "F \ A Detects B ==> F \ UNIV LeadsTo (A <==> B)"
apply (unfold Detects_def Equality_def)
apply (rule_tac B = B in LeadsTo_Diff)
 apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
apply (blast intro: Always_LeadsTo_weaken)
done


end