src/HOL/UNITY/Detects.thy
 author Andreas Lochbihler Wed, 11 Nov 2015 12:57:01 +0100 changeset 61635 c657ee4f59b7 parent 58889 5b7a9633cfa8 child 63146 f1ecba0272f9 permissions -rw-r--r--
```
(*  Title:      HOL/UNITY/Detects.thy
Author:     Tanja Vos, Cambridge University Computer Laboratory

Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
*)

section{*The Detects Relation*}

theory Detects imports FP SubstAx begin

definition Detects :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
where "A Detects B = (Always (-A \<union> B)) \<inter> (B LeadsTo A)"

definition Equality :: "['a set, 'a set] => 'a set"  (infixl "<==>" 60)
where "A <==> B = (-A \<union> B) \<inter> (A \<union> -B)"

(* Corollary from Sectiom 3.6.4 *)

lemma Always_at_FP:
"[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
supply [[simproc del: boolean_algebra_cancel_inf]] inf_compl_bot_right[simp del]
apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
apply (subgoal_tac "(B \<inter> (FP F \<inter> -B)) = {}")
apply auto
apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
done

lemma Detects_Trans:
"[| F \<in> A Detects B; F \<in> B Detects C |] ==> F \<in> A Detects C"
apply (unfold Detects_def Int_def)
apply (simp (no_asm))
apply safe
apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
apply (blast intro: Always_weaken)
done

lemma Detects_refl: "F \<in> A Detects A"
apply (unfold Detects_def)
done

lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
by (unfold Equality_def, blast)

(*Not quite antisymmetry: sets A and B agree in all reachable states *)
lemma Detects_antisym:
"[| F \<in> A Detects B;  F \<in> B Detects A|] ==> F \<in> Always (A <==> B)"
apply (unfold Detects_def Equality_def)
done

(* Theorem from Section 3.8 *)

lemma Detects_Always:
"[|F \<in> A Detects B; all_total F|] ==> F \<in> Always (-(FP F) \<union> (A <==> B))"
apply (unfold Detects_def Equality_def)
apply (blast dest: Always_at_FP intro: Always_weaken)
done

(* Theorem from exercise 11.1 Section 11.3.1 *)