(* 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 \<open>The Detects Relation\<close> theory Detects imports FP SubstAx begin definition Detects :: "['a set, 'a set] => 'a program set" (infixl \<open>Detects\<close> 60) where "A Detects B = (Always (-A \ B)) \ (B LeadsTo A)" definition Equality :: "['a set, 'a set] => 'a set" (infixl \<open><==>\<close> 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))" 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 autoapply (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 safeapply (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 quality 100%
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
