src/HOL/UNITY/Detects.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 61635 c657ee4f59b7
child 63146 f1ecba0272f9
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/UNITY/Detects.thy
     2     Author:     Tanja Vos, Cambridge University Computer Laboratory
     3     Copyright   2000  University of Cambridge
     4 
     5 Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
     6 *)
     7 
     8 section{*The Detects Relation*}
     9 
    10 theory Detects imports FP SubstAx begin
    11 
    12 definition 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 
    15 definition 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 
    21 lemma Always_at_FP:
    22      "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
    23 supply [[simproc del: boolean_algebra_cancel_inf]] inf_compl_bot_right[simp del] 
    24 apply (rule LeadsTo_empty)
    25 apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
    26 apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
    27 apply (subgoal_tac "(B \<inter> (FP F \<inter> -B)) = {}")
    28 apply auto
    29 apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
    30 done
    31 
    32 
    33 lemma Detects_Trans: 
    34      "[| F \<in> A Detects B; F \<in> B Detects C |] ==> F \<in> A Detects C"
    35 apply (unfold Detects_def Int_def)
    36 apply (simp (no_asm))
    37 apply safe
    38 apply (rule_tac [2] LeadsTo_Trans, auto)
    39 apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
    40  apply (blast intro: Always_weaken)
    41 apply (simp add: Always_Int_distrib)
    42 done
    43 
    44 lemma Detects_refl: "F \<in> A Detects A"
    45 apply (unfold Detects_def)
    46 apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
    47 done
    48 
    49 lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
    50 by (unfold Equality_def, blast)
    51 
    52 (*Not quite antisymmetry: sets A and B agree in all reachable states *)
    53 lemma Detects_antisym: 
    54      "[| F \<in> A Detects B;  F \<in> B Detects A|] ==> F \<in> Always (A <==> B)"
    55 apply (unfold Detects_def Equality_def)
    56 apply (simp add: Always_Int_I Un_commute)
    57 done
    58 
    59 
    60 (* Theorem from Section 3.8 *)
    61 
    62 lemma Detects_Always: 
    63      "[|F \<in> A Detects B; all_total F|] ==> F \<in> Always (-(FP F) \<union> (A <==> B))"
    64 apply (unfold Detects_def Equality_def)
    65 apply (simp add: Un_Int_distrib Always_Int_distrib)
    66 apply (blast dest: Always_at_FP intro: Always_weaken)
    67 done
    68 
    69 (* Theorem from exercise 11.1 Section 11.3.1 *)
    70 
    71 lemma Detects_Imp_LeadstoEQ: 
    72      "F \<in> A Detects B ==> F \<in> UNIV LeadsTo (A <==> B)"
    73 apply (unfold Detects_def Equality_def)
    74 apply (rule_tac B = B in LeadsTo_Diff)
    75  apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
    76 apply (blast intro: Always_LeadsTo_weaken)
    77 done
    78 
    79 
    80 end
    81