src/HOL/UNITY/Comp/Priority.thy

 (*  Title:      HOL/UNITY/Priority
     ID:         $Id$
     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     Copyright   2001  University of Cambridge
-
-
 *)
 
 header{*The priority system*}
 
 theory Priority = PriorityAux:

 by (simp add: system_def Component_def mk_total_program_def totalize_JN, constrains, blast)
 
 (* property 14: the 'above set' of a Component that hasn't got 
       priority doesn't increase *)
 lemma above_not_increase: 
-     "\<forall>j. system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}"
-apply clarify
-apply (cut_tac i = j in reach_lemma)
+     "system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}"
+apply (insert reach_lemma [of concl: j])
 apply (simp add: system_def Component_def mk_total_program_def totalize_JN, 
        constrains)
-apply (auto simp add: trancl_converse)
+apply (simp add: trancl_converse, blast) 
 done
 
 lemma above_not_increase':
      "system \<in> -Highest i Int {s. above i s = x} co {s. above i s <= x}"
-apply (cut_tac i = i in above_not_increase)
+apply (insert above_not_increase [of i])
 apply (simp add: trancl_converse constrains_def, blast)
 done
 
 
 

 apply (drule above_lemma_b, auto)
 done
 
 (* property 17: original one is an invariant *)
 lemma Acyclic_Maximal_stable: "system \<in> stable (Acyclic Int Maximal)"
-apply (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable)
-done
+by (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable)
 
 
 (* propert 5: existential property *)
 
 lemma Highest_leadsTo_Lowest: "system \<in> Highest i leadsTo Lowest i"

      "system \<in> (\<Union>j. {s. above i s = x} Int {s. j \<in> above i s} Int Highest j)  
                leadsTo {s. above i s < x}"
 apply (rule leadsTo_UN)
 apply (rule single_leadsTo_I, clarify)
 apply (rule_tac x2 = "above i x" in above_decreases_lemma)
-apply (simp_all (no_asm_use) del: Highest_def add: Highest_iff_above0)
+apply (simp_all (no_asm_use) add: Highest_iff_above0)
 apply blast+
 done
 
 (** Just a massage of conditions to have the desired form ***)
 lemma Maximal_eq_Maximal': "Maximal = Maximal'"

 lemmas finite_psubset_induct = wf_finite_psubset [THEN leadsTo_wf_induct]
 
 
 lemma Progress: "system \<in> Acyclic leadsTo Highest i"
 apply (rule_tac f = "%s. above i s" in finite_psubset_induct)
-apply (simp del: Highest_def above_def
+apply (simp del: above_def
             add: Highest_iff_above0 vimage_def finite_psubset_def, clarify)
 apply (case_tac "m={}")
 apply (rule Int_lower2 [THEN [2] leadsTo_weaken_L])
 apply (force simp add: leadsTo_refl)
 apply (rule_tac A' = "Acyclic Int {x. above i x < m}" in leadsTo_weaken_R)