src/HOL/UNITY/Detects.thy
author paulson
Fri Jan 31 20:12:44 2003 +0100 (2003-01-31)
changeset 13798 4c1a53627500
parent 13785 e2fcd88be55d
child 13805 3786b2fd6808
permissions -rw-r--r--
conversion to new-style theories and tidying
     1 (*  Title:      HOL/UNITY/Detects
     2     ID:         $Id$
     3     Author:     Tanja Vos, Cambridge University Computer Laboratory
     4     Copyright   2000  University of Cambridge
     5 
     6 Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
     7 *)
     8 
     9 header{*The Detects Relation*}
    10 
    11 theory Detects = FP + SubstAx:
    12 
    13 consts
    14    op_Detects  :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
    15    op_Equality :: "['a set, 'a set] => 'a set"          (infixl "<==>" 60)
    16    
    17 defs
    18   Detects_def:  "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
    19   Equality_def: "A <==> B == (-A Un B) Int (A Un -B)"
    20 
    21 
    22 (* Corollary from Sectiom 3.6.4 *)
    23 
    24 lemma Always_at_FP: "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))"
    25 apply (rule LeadsTo_empty)
    26 apply (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))")
    27 apply (subgoal_tac [2] " (FP F Int A Int - B) = (A Int (FP F Int -B))")
    28 apply (subgoal_tac "(B Int (FP F Int -B)) = {}")
    29 apply auto
    30 apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
    31 done
    32 
    33 
    34 lemma Detects_Trans: 
    35      "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C"
    36 apply (unfold Detects_def Int_def)
    37 apply (simp (no_asm))
    38 apply safe
    39 apply (rule_tac [2] LeadsTo_Trans)
    40 apply auto
    41 apply (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))")
    42  apply (blast intro: Always_weaken)
    43 apply (simp add: Always_Int_distrib)
    44 done
    45 
    46 lemma Detects_refl: "F : A Detects A"
    47 apply (unfold Detects_def)
    48 apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
    49 done
    50 
    51 lemma Detects_eq_Un: "(A<==>B) = (A Int B) Un (-A Int -B)"
    52 apply (unfold Equality_def)
    53 apply blast
    54 done
    55 
    56 (*Not quite antisymmetry: sets A and B agree in all reachable states *)
    57 lemma Detects_antisym: 
    58      "[| F : A Detects B;  F : B Detects A|] ==> F : Always (A <==> B)"
    59 apply (unfold Detects_def Equality_def)
    60 apply (simp add: Always_Int_I Un_commute)
    61 done
    62 
    63 
    64 (* Theorem from Section 3.8 *)
    65 
    66 lemma Detects_Always: 
    67      "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))"
    68 apply (unfold Detects_def Equality_def)
    69 apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib)
    70 apply (blast dest: Always_at_FP intro: Always_weaken)
    71 done
    72 
    73 (* Theorem from exercise 11.1 Section 11.3.1 *)
    74 
    75 lemma Detects_Imp_LeadstoEQ: 
    76      "F : A Detects B ==> F : UNIV LeadsTo (A <==> B)"
    77 apply (unfold Detects_def Equality_def)
    78 apply (rule_tac B = "B" in LeadsTo_Diff)
    79 prefer 2 apply (blast intro: Always_LeadsTo_weaken)
    80 apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
    81 done
    82 
    83 
    84 end
    85