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