Quellcode-Bibliothek Detects.thy Sprache: Isabelle

(*  Title:      HOL/UNITY/Detects.thy
    Author:     Tanja Vos, Cambridge University Computer Laboratory
    Copyright   2000  University of Cambridge

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

section\<open>The Detects Relation\<close>

theory Detects imports FP SubstAx begin

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

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

(* Corollary from Sectiom 3.6.4 *)

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

lemma Detects_Trans:
     "[| F \ A Detects B; F \ B Detects C |] ==> F \ A Detects C"
apply (unfold Detects_def Int_def)
apply (simp (no_asm))
apply safe
apply (rule_tac [2] LeadsTo_Trans, auto)
apply (subgoal_tac "F \ Always ((-A \ B) \ (-B \ C))")
apply (blast intro: Always_weaken)
apply (simp add: Always_Int_distrib)
done

lemma Detects_refl: "F \ A Detects A"
apply (unfold Detects_def)
apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
done

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

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

(* Theorem from Section 3.8 *)

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

(* Theorem from exercise 11.1 Section 11.3.1 *)

lemma Detects_Imp_LeadstoEQ:
     "F \ A Detects B ==> F \ UNIV LeadsTo (A <==> B)"
apply (unfold Detects_def Equality_def)
apply (rule_tac B = B in LeadsTo_Diff)
apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
apply (blast intro: Always_LeadsTo_weaken)
done

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.15Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.