src/HOL/UNITY/Detects.thy
 author hoelzl Thu Sep 02 10:14:32 2010 +0200 (2010-09-02) changeset 39072 1030b1a166ef parent 37936 1e4c5015a72e child 57488 58db442609ac permissions -rw-r--r--
```     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 header{*The Detects Relation*}
```
```     9
```
```    10 theory Detects imports FP SubstAx begin
```
```    11
```
```    12 consts
```
```    13    op_Detects  :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
```
```    14    op_Equality :: "['a set, 'a set] => 'a set"          (infixl "<==>" 60)
```
```    15
```
```    16 defs
```
```    17   Detects_def:  "A Detects B == (Always (-A \<union> B)) \<inter> (B LeadsTo A)"
```
```    18   Equality_def: "A <==> B == (-A \<union> B) \<inter> (A \<union> -B)"
```
```    19
```
```    20
```
```    21 (* Corollary from Sectiom 3.6.4 *)
```
```    22
```
```    23 lemma Always_at_FP:
```
```    24      "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
```
```    25 apply (rule LeadsTo_empty)
```
```    26 apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
```
```    27 apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
```
```    28 apply (subgoal_tac "(B \<inter> (FP F \<inter> -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 \<in> A Detects B; F \<in> B Detects C |] ==> F \<in> 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, auto)
```
```    40 apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
```
```    41  apply (blast intro: Always_weaken)
```
```    42 apply (simp add: Always_Int_distrib)
```
```    43 done
```
```    44
```
```    45 lemma Detects_refl: "F \<in> A Detects A"
```
```    46 apply (unfold Detects_def)
```
```    47 apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
```
```    48 done
```
```    49
```
```    50 lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
```
```    51 by (unfold Equality_def, blast)
```
```    52
```
```    53 (*Not quite antisymmetry: sets A and B agree in all reachable states *)
```
```    54 lemma Detects_antisym:
```
```    55      "[| F \<in> A Detects B;  F \<in> B Detects A|] ==> F \<in> Always (A <==> B)"
```
```    56 apply (unfold Detects_def Equality_def)
```
```    57 apply (simp add: Always_Int_I Un_commute)
```
```    58 done
```
```    59
```
```    60
```
```    61 (* Theorem from Section 3.8 *)
```
```    62
```
```    63 lemma Detects_Always:
```
```    64      "[|F \<in> A Detects B; all_total F|] ==> F \<in> Always (-(FP F) \<union> (A <==> B))"
```
```    65 apply (unfold Detects_def Equality_def)
```
```    66 apply (simp add: Un_Int_distrib Always_Int_distrib)
```
```    67 apply (blast dest: Always_at_FP intro: Always_weaken)
```
```    68 done
```
```    69
```
```    70 (* Theorem from exercise 11.1 Section 11.3.1 *)
```
```    71
```
```    72 lemma Detects_Imp_LeadstoEQ:
```
```    73      "F \<in> A Detects B ==> F \<in> UNIV LeadsTo (A <==> B)"
```
```    74 apply (unfold Detects_def Equality_def)
```
```    75 apply (rule_tac B = B in LeadsTo_Diff)
```
```    76  apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
```
```    77 apply (blast intro: Always_LeadsTo_weaken)
```
```    78 done
```
```    79
```
```    80
```
```    81 end
```
```    82
```