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