src/HOL/UNITY/Constrains.thy

     Copyright   1998  University of Cambridge
 
 Weak safety relations: restricted to the set of reachable states.
 *)
 
-section{*Weak Safety*}
+section\<open>Weak Safety\<close>
 
 theory Constrains imports UNITY begin
 
   (*Initial states and program => (final state, reversed trace to it)...
     Arguments MUST be curried in an inductive definition*)

   (*Polymorphic in both states and the meaning of \<le> *)
 definition Increasing :: "['a => 'b::{order}] => 'a program set" where
     "Increasing f == \<Inter>z. Stable {s. z \<le> f s}"
 
 
-subsection{*traces and reachable*}
+subsection\<open>traces and reachable\<close>
 
 lemma reachable_equiv_traces:
      "reachable F = {s. \<exists>evs. (s,evs) \<in> traces (Init F) (Acts F)}"
 apply safe
 apply (erule_tac [2] traces.induct)

 apply (erule reachable.induct)
 apply (blast intro: reachable.intros)+
 done
 
 
-subsection{*Co*}
+subsection\<open>Co\<close>
 
 (*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
 lemmas constrains_reachable_Int =  
     subset_refl [THEN stable_reachable [unfolded stable_def], THEN constrains_Int]
 

 apply (simp add: Constrains_eq_constrains constrains_def)
 apply best
 done
 
 
-subsection{*Stable*}
+subsection\<open>Stable\<close>
 
 (*Useful because there's no Stable_weaken.  [Tanja Vos]*)
 lemma Stable_eq: "[| F \<in> Stable A; A = B |] ==> F \<in> Stable B"
 by blast
 

 lemma Stable_reachable: "F \<in> Stable (reachable F)"
 by (simp add: Stable_eq_stable)
 
 
 
-subsection{*Increasing*}
+subsection\<open>Increasing\<close>
 
 lemma IncreasingD: 
      "F \<in> Increasing f ==> F \<in> Stable {s. x \<le> f s}"
 by (unfold Increasing_def, blast)
 

 done
 
 lemmas Increasing_constant = increasing_constant [THEN increasing_imp_Increasing, iff]
 
 
-subsection{*The Elimination Theorem*}
+subsection\<open>The Elimination Theorem\<close>
 
 (*The "free" m has become universally quantified! Should the premise be !!m
 instead of \<forall>m ?  Would make it harder to use in forward proof.*)
 
 lemma Elimination: 

 lemma Elimination_sing: 
     "(\<forall>m. F \<in> {m} Co (B m)) ==> F \<in> M Co (\<Union>m \<in> M. B m)"
 by (unfold Constrains_def constrains_def, blast)
 
 
-subsection{*Specialized laws for handling Always*}
+subsection\<open>Specialized laws for handling Always\<close>
 
 (** Natural deduction rules for "Always A" **)
 
 lemma AlwaysI: "[| Init F \<subseteq> A;  F \<in> Stable A |] ==> F \<in> Always A"
 by (simp add: Always_def)

 
 lemma Always_weaken: "[| F \<in> Always A; A \<subseteq> B |] ==> F \<in> Always B"
 by (auto simp add: Always_eq_includes_reachable)
 
 
-subsection{*"Co" rules involving Always*}
+subsection\<open>"Co" rules involving Always\<close>
 
 lemma Always_Constrains_pre:
      "F \<in> Always INV ==> (F \<in> (INV \<inter> A) Co A') = (F \<in> A Co A')"
 by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def 
               Int_assoc [symmetric])

 (*Delete the nearest invariance assumption (which will be the second one
   used by Always_Int_I) *)
 lemmas Always_thin = thin_rl [of "F \<in> Always A"]
 
 
-subsection{*Totalize*}
+subsection\<open>Totalize\<close>
 
 lemma reachable_imp_reachable_tot:
       "s \<in> reachable F ==> s \<in> reachable (totalize F)"
 apply (erule reachable.induct)
  apply (rule reachable.Init)