src/HOL/UNITY/Detects.thy
changeset 13785 e2fcd88be55d
parent 8334 7896bcbd8641
child 13798 4c1a53627500
     1.1 --- a/src/HOL/UNITY/Detects.thy	Thu Jan 23 10:30:14 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Detects.thy	Fri Jan 24 14:06:49 2003 +0100
     1.3 @@ -6,16 +6,78 @@
     1.4  Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
     1.5  *)
     1.6  
     1.7 -Detects = WFair + Reach + 
     1.8 -
     1.9 +theory Detects = FP + SubstAx:
    1.10  
    1.11  consts
    1.12     op_Detects  :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
    1.13     op_Equality :: "['a set, 'a set] => 'a set"          (infixl "<==>" 60)
    1.14     
    1.15  defs
    1.16 -  Detects_def "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
    1.17 -  Equality_def "A <==> B == (-A Un B) Int (A Un -B)"
    1.18 +  Detects_def:  "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
    1.19 +  Equality_def: "A <==> B == (-A Un B) Int (A Un -B)"
    1.20 +
    1.21 +
    1.22 +(* Corollary from Sectiom 3.6.4 *)
    1.23 +
    1.24 +lemma Always_at_FP: "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))"
    1.25 +apply (rule LeadsTo_empty)
    1.26 +apply (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))")
    1.27 +apply (subgoal_tac [2] " (FP F Int A Int - B) = (A Int (FP F Int -B))")
    1.28 +apply (subgoal_tac "(B Int (FP F Int -B)) = {}")
    1.29 +apply auto
    1.30 +apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
    1.31 +done
    1.32 +
    1.33 +
    1.34 +lemma Detects_Trans: 
    1.35 +     "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C"
    1.36 +apply (unfold Detects_def Int_def)
    1.37 +apply (simp (no_asm))
    1.38 +apply safe
    1.39 +apply (rule_tac [2] LeadsTo_Trans)
    1.40 +apply auto
    1.41 +apply (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))")
    1.42 + apply (blast intro: Always_weaken)
    1.43 +apply (simp add: Always_Int_distrib)
    1.44 +done
    1.45 +
    1.46 +lemma Detects_refl: "F : A Detects A"
    1.47 +apply (unfold Detects_def)
    1.48 +apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
    1.49 +done
    1.50 +
    1.51 +lemma Detects_eq_Un: "(A<==>B) = (A Int B) Un (-A Int -B)"
    1.52 +apply (unfold Equality_def)
    1.53 +apply blast
    1.54 +done
    1.55 +
    1.56 +(*Not quite antisymmetry: sets A and B agree in all reachable states *)
    1.57 +lemma Detects_antisym: 
    1.58 +     "[| F : A Detects B;  F : B Detects A|] ==> F : Always (A <==> B)"
    1.59 +apply (unfold Detects_def Equality_def)
    1.60 +apply (simp add: Always_Int_I Un_commute)
    1.61 +done
    1.62 +
    1.63 +
    1.64 +(* Theorem from Section 3.8 *)
    1.65 +
    1.66 +lemma Detects_Always: 
    1.67 +     "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))"
    1.68 +apply (unfold Detects_def Equality_def)
    1.69 +apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib)
    1.70 +apply (blast dest: Always_at_FP intro: Always_weaken)
    1.71 +done
    1.72 +
    1.73 +(* Theorem from exercise 11.1 Section 11.3.1 *)
    1.74 +
    1.75 +lemma Detects_Imp_LeadstoEQ: 
    1.76 +     "F : A Detects B ==> F : UNIV LeadsTo (A <==> B)"
    1.77 +apply (unfold Detects_def Equality_def)
    1.78 +apply (rule_tac B = "B" in LeadsTo_Diff)
    1.79 +prefer 2 apply (blast intro: Always_LeadsTo_weaken)
    1.80 +apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
    1.81 +done
    1.82 +
    1.83  
    1.84  end
    1.85