# HG changeset patch
# User wenzelm
# Date 1331678015 -3600
# Node ID e0cd5c4df8e6a79d8a53441d5f4f81124c056fff
# Parent  6d2a2f0e904ec2a71f7ab198d81a6b65b4c01965
tuned context specifications and proofs;

diff -r 6d2a2f0e904e -r e0cd5c4df8e6 src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Tue Mar 13 22:49:02 2012 +0100
+++ b/src/HOL/UNITY/Comp.thy	Tue Mar 13 23:33:35 2012 +0100
@@ -17,31 +17,29 @@
 instantiation program :: (type) ord
 begin
 
-definition
-  component_def: "F \<le> H <-> (\<exists>G. F\<squnion>G = H)"
+definition component_def: "F \<le> H <-> (\<exists>G. F\<squnion>G = H)"
 
-definition
-  strict_component_def: "F < (H::'a program) <-> (F \<le> H & F \<noteq> H)"
+definition strict_component_def: "F < (H::'a program) <-> (F \<le> H & F \<noteq> H)"
 
 instance ..
 
 end
 
-definition component_of :: "'a program =>'a program=> bool" (infixl "component'_of" 50) where
-  "F component_of H == \<exists>G. F ok G & F\<squnion>G = H"
+definition component_of :: "'a program =>'a program=> bool" (infixl "component'_of" 50)
+  where "F component_of H == \<exists>G. F ok G & F\<squnion>G = H"
 
-definition strict_component_of :: "'a program\<Rightarrow>'a program=> bool" (infixl "strict'_component'_of" 50)  where
-  "F strict_component_of H == F component_of H & F\<noteq>H"
+definition strict_component_of :: "'a program\<Rightarrow>'a program=> bool" (infixl "strict'_component'_of" 50)
+  where "F strict_component_of H == F component_of H & F\<noteq>H"
 
-definition preserves :: "('a=>'b) => 'a program set" where
-    "preserves v == \<Inter>z. stable {s. v s = z}"
+definition preserves :: "('a=>'b) => 'a program set"
+  where "preserves v == \<Inter>z. stable {s. v s = z}"
 
 definition localize :: "('a=>'b) => 'a program => 'a program" where
   "localize v F == mk_program(Init F, Acts F,
                               AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G))"
 
-definition funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c" where
-  "funPair f g == %x. (f x, g x)"
+definition funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
+  where "funPair f g == %x. (f x, g x)"
 
 
 subsection{*The component relation*}
diff -r 6d2a2f0e904e -r e0cd5c4df8e6 src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Tue Mar 13 22:49:02 2012 +0100
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Tue Mar 13 23:33:35 2012 +0100
@@ -240,34 +240,37 @@
 
 subsection{*Theorems for Merge*}
 
-lemma (in Merge) Merge_Allowed:
+context Merge
+begin
+
+lemma Merge_Allowed:
      "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"
 apply (cut_tac Merge_spec)
 apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def
                       safety_prop_Acts_iff)
 done
 
-lemma (in Merge) M_ok_iff [iff]:
+lemma M_ok_iff [iff]:
      "M ok G = (G \<in> preserves merge.Out & G \<in> preserves merge.iOut &
                      M \<in> Allowed G)"
 by (auto simp add: Merge_Allowed ok_iff_Allowed)
 
 
-lemma (in Merge) Merge_Always_Out_eq_iOut:
+lemma Merge_Always_Out_eq_iOut:
      "[| G \<in> preserves merge.Out; G \<in> preserves merge.iOut; M \<in> Allowed G |]
       ==> M Join G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
 apply (cut_tac Merge_spec)
 apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
 done
 
-lemma (in Merge) Merge_Bounded:
+lemma Merge_Bounded:
      "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
       ==> M Join G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
 apply (cut_tac Merge_spec)
 apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
 done
 
-lemma (in Merge) Merge_Bag_Follows_lemma:
+lemma Merge_Bag_Follows_lemma:
      "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
   ==> M Join G \<in> Always
           {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (merge.Out s)
@@ -287,7 +290,7 @@
 apply blast
 done
 
-lemma (in Merge) Merge_Bag_Follows:
+lemma Merge_Bag_Follows:
      "M \<in> (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
           guarantees
              (bag_of o merge.Out) Fols
@@ -301,10 +304,15 @@
   apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
 done
 
+end
+
 
 subsection{*Theorems for Distributor*}
 
-lemma (in Distrib) Distr_Increasing_Out:
+context Distrib
+begin
+
+lemma Distr_Increasing_Out:
      "D \<in> Increasing distr.In Int Increasing distr.iIn Int
           Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
           guarantees
@@ -315,7 +323,7 @@
 apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD)
 done
 
-lemma (in Distrib) Distr_Bag_Follows_lemma:
+lemma Distr_Bag_Follows_lemma:
      "[| G \<in> preserves distr.Out;
          D Join G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
   ==> D Join G \<in> Always
@@ -335,14 +343,14 @@
 apply blast
 done
 
-lemma (in Distrib) D_ok_iff [iff]:
+lemma D_ok_iff [iff]:
      "D ok G = (G \<in> preserves distr.Out & D \<in> Allowed G)"
 apply (cut_tac Distrib_spec)
 apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def
                       safety_prop_Acts_iff ok_iff_Allowed)
 done
 
-lemma (in Distrib) Distr_Bag_Follows:
+lemma Distr_Bag_Follows:
  "D \<in> Increasing distr.In Int Increasing distr.iIn Int
       Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
       guarantees
@@ -360,6 +368,8 @@
   apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
 done
 
+end
+
 
 subsection{*Theorems for Allocator*}
 
diff -r 6d2a2f0e904e -r e0cd5c4df8e6 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Tue Mar 13 22:49:02 2012 +0100
+++ b/src/HOL/UNITY/ELT.thy	Tue Mar 13 23:33:35 2012 +0100
@@ -471,22 +471,25 @@
 
 (**** EXTEND/PROJECT PROPERTIES ****)
 
-lemma (in Extend) givenBy_o_eq_extend_set:
+context Extend
+begin
+
+lemma givenBy_o_eq_extend_set:
      "givenBy (v o f) = extend_set h ` (givenBy v)"
 apply (simp add: givenBy_eq_Collect)
 apply (rule equalityI, best)
 apply blast 
 done
 
-lemma (in Extend) givenBy_eq_extend_set: "givenBy f = range (extend_set h)"
+lemma givenBy_eq_extend_set: "givenBy f = range (extend_set h)"
 by (simp add: givenBy_eq_Collect, best)
 
-lemma (in Extend) extend_set_givenBy_I:
+lemma extend_set_givenBy_I:
      "D : givenBy v ==> extend_set h D : givenBy (v o f)"
 apply (simp (no_asm_use) add: givenBy_eq_all, blast)
 done
 
-lemma (in Extend) leadsETo_imp_extend_leadsETo:
+lemma leadsETo_imp_extend_leadsETo:
      "F : A leadsTo[CC] B  
       ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]  
                        (extend_set h B)"
@@ -500,7 +503,7 @@
 
 (*This version's stronger in the "ensures" precondition
   BUT there's no ensures_weaken_L*)
-lemma (in Extend) Join_project_ensures_strong:
+lemma Join_project_ensures_strong:
      "[| project h C G ~: transient (project_set h C Int (A-B)) |  
            project_set h C Int (A - B) = {};   
          extend h F\<squnion>G : stable C;   
@@ -512,7 +515,7 @@
 done
 
 (*NOT WORKING.  MODIFY AS IN Project.thy
-lemma (in Extend) pld_lemma:
+lemma pld_lemma:
      "[| extend h F\<squnion>G : stable C;   
          F\<squnion>project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;   
          G : preserves (v o f) |]  
@@ -535,7 +538,7 @@
 apply (simp (no_asm_simp) add: stable_ensures_Int [THEN ensures_weaken_R] Int_lower2 project_stable_project_set extend_stable_project_set)
 done
 
-lemma (in Extend) project_leadsETo_D_lemma:
+lemma project_leadsETo_D_lemma:
      "[| extend h F\<squnion>G : stable C;   
          F\<squnion>project h C G :  
              (project_set h C Int A)  
@@ -547,7 +550,7 @@
 apply (auto simp add: split_extended_all)
 done
 
-lemma (in Extend) project_leadsETo_D:
+lemma project_leadsETo_D:
      "[| F\<squnion>project h UNIV G : A leadsTo[givenBy v] B;   
          G : preserves (v o f) |]   
       ==> extend h F\<squnion>G : (extend_set h A)  
@@ -557,7 +560,7 @@
 apply (rule givenBy_o_eq_extend_set [THEN equalityD2])
 done
 
-lemma (in Extend) project_LeadsETo_D:
+lemma project_LeadsETo_D:
      "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G  
              : A LeadsTo[givenBy v] B;   
          G : preserves (v o f) |]  
@@ -570,7 +573,7 @@
 apply (simp add: project_set_reachable_extend_eq [symmetric])
 done
 
-lemma (in Extend) extending_leadsETo: 
+lemma extending_leadsETo: 
      "(ALL G. extend h F ok G --> G : preserves (v o f))  
       ==> extending (%G. UNIV) h F  
                 (extend_set h A leadsTo[givenBy (v o f)] extend_set h B)  
@@ -579,7 +582,7 @@
 apply (auto simp add: project_leadsETo_D)
 done
 
-lemma (in Extend) extending_LeadsETo: 
+lemma extending_LeadsETo: 
      "(ALL G. extend h F ok G --> G : preserves (v o f))  
       ==> extending (%G. reachable (extend h F\<squnion>G)) h F  
                 (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B)  
@@ -593,7 +596,7 @@
 (*** leadsETo in the precondition ***)
 
 (*Lemma for the Trans case*)
-lemma (in Extend) pli_lemma:
+lemma pli_lemma:
      "[| extend h F\<squnion>G : stable C;     
          F\<squnion>project h C G     
            : project_set h C Int project_set h A leadsTo project_set h B |]  
@@ -604,7 +607,7 @@
 apply (auto simp add: project_stable_project_set extend_stable_project_set)
 done
 
-lemma (in Extend) project_leadsETo_I_lemma:
+lemma project_leadsETo_I_lemma:
      "[| extend h F\<squnion>G : stable C;   
          extend h F\<squnion>G :  
            (C Int A) leadsTo[(%D. C Int D)`givenBy f]  B |]   
@@ -620,13 +623,13 @@
 apply (blast intro: ensures_extend_set_imp_project_ensures)
 done
 
-lemma (in Extend) project_leadsETo_I:
+lemma project_leadsETo_I:
      "extend h F\<squnion>G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)
       ==> F\<squnion>project h UNIV G : A leadsTo B"
 apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken], auto)
 done
 
-lemma (in Extend) project_LeadsETo_I:
+lemma project_LeadsETo_I:
      "extend h F\<squnion>G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B) 
       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G   
            : A LeadsTo B"
@@ -635,7 +638,7 @@
 apply (auto simp add: project_set_reachable_extend_eq [symmetric])
 done
 
-lemma (in Extend) projecting_leadsTo: 
+lemma projecting_leadsTo: 
      "projecting (%G. UNIV) h F  
                  (extend_set h A leadsTo[givenBy f] extend_set h B)  
                  (A leadsTo B)"
@@ -643,7 +646,7 @@
 apply (force dest: project_leadsETo_I)
 done
 
-lemma (in Extend) projecting_LeadsTo: 
+lemma projecting_LeadsTo: 
      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
                  (extend_set h A LeadsTo[givenBy f] extend_set h B)  
                  (A LeadsTo B)"
@@ -652,3 +655,5 @@
 done
 
 end
+
+end
diff -r 6d2a2f0e904e -r e0cd5c4df8e6 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Tue Mar 13 22:49:02 2012 +0100
+++ b/src/HOL/UNITY/Extend.thy	Tue Mar 13 23:33:35 2012 +0100
@@ -132,23 +132,26 @@
 
 subsection{*Trivial properties of f, g, h*}
 
-lemma (in Extend) f_h_eq [simp]: "f(h(x,y)) = x" 
+context Extend
+begin
+
+lemma f_h_eq [simp]: "f(h(x,y)) = x" 
 by (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
 
-lemma (in Extend) h_inject1 [dest]: "h(x,y) = h(x',y') ==> x=x'"
+lemma h_inject1 [dest]: "h(x,y) = h(x',y') ==> x=x'"
 apply (drule_tac f = f in arg_cong)
 apply (simp add: f_def good_h [unfolded good_map_def, THEN conjunct2])
 done
 
-lemma (in Extend) h_f_g_equiv: "h(f z, g z) == z"
+lemma h_f_g_equiv: "h(f z, g z) == z"
 by (simp add: f_def g_def 
             good_h [unfolded good_map_def, THEN conjunct1, THEN surj_f_inv_f])
 
-lemma (in Extend) h_f_g_eq: "h(f z, g z) = z"
+lemma h_f_g_eq: "h(f z, g z) = z"
 by (simp add: h_f_g_equiv)
 
 
-lemma (in Extend) split_extended_all:
+lemma split_extended_all:
      "(!!z. PROP P z) == (!!u y. PROP P (h (u, y)))"
 proof 
    assume allP: "\<And>z. PROP P z"
@@ -161,6 +164,7 @@
    show "PROP P z" by (rule Phfgz [unfolded h_f_g_equiv])
 qed 
 
+end
 
 
 subsection{*@{term extend_set}: basic properties*}
@@ -172,40 +176,41 @@
 lemma extend_set_mono: "A \<subseteq> B ==> extend_set h A \<subseteq> extend_set h B"
 by (unfold extend_set_def, blast)
 
-lemma (in Extend) mem_extend_set_iff [iff]: "z \<in> extend_set h A = (f z \<in> A)"
+context Extend
+begin
+
+lemma mem_extend_set_iff [iff]: "z \<in> extend_set h A = (f z \<in> A)"
 apply (unfold extend_set_def)
 apply (force intro: h_f_g_eq [symmetric])
 done
 
-lemma (in Extend) extend_set_strict_mono [iff]:
+lemma extend_set_strict_mono [iff]:
      "(extend_set h A \<subseteq> extend_set h B) = (A \<subseteq> B)"
 by (unfold extend_set_def, force)
 
-lemma extend_set_empty [simp]: "extend_set h {} = {}"
+lemma (in -) extend_set_empty [simp]: "extend_set h {} = {}"
 by (unfold extend_set_def, auto)
 
-lemma (in Extend) extend_set_eq_Collect: "extend_set h {s. P s} = {s. P(f s)}"
+lemma extend_set_eq_Collect: "extend_set h {s. P s} = {s. P(f s)}"
 by auto
 
-lemma (in Extend) extend_set_sing: "extend_set h {x} = {s. f s = x}"
+lemma extend_set_sing: "extend_set h {x} = {s. f s = x}"
 by auto
 
-lemma (in Extend) extend_set_inverse [simp]:
-     "project_set h (extend_set h C) = C"
+lemma extend_set_inverse [simp]: "project_set h (extend_set h C) = C"
 by (unfold extend_set_def, auto)
 
-lemma (in Extend) extend_set_project_set:
-     "C \<subseteq> extend_set h (project_set h C)"
+lemma extend_set_project_set: "C \<subseteq> extend_set h (project_set h C)"
 apply (unfold extend_set_def)
 apply (auto simp add: split_extended_all, blast)
 done
 
-lemma (in Extend) inj_extend_set: "inj (extend_set h)"
+lemma inj_extend_set: "inj (extend_set h)"
 apply (rule inj_on_inverseI)
 apply (rule extend_set_inverse)
 done
 
-lemma (in Extend) extend_set_UNIV_eq [simp]: "extend_set h UNIV = UNIV"
+lemma extend_set_UNIV_eq [simp]: "extend_set h UNIV = UNIV"
 apply (unfold extend_set_def)
 apply (auto simp add: split_extended_all)
 done
@@ -213,11 +218,11 @@
 subsection{*@{term project_set}: basic properties*}
 
 (*project_set is simply image!*)
-lemma (in Extend) project_set_eq: "project_set h C = f ` C"
+lemma project_set_eq: "project_set h C = f ` C"
 by (auto intro: f_h_eq [symmetric] simp add: split_extended_all)
 
 (*Converse appears to fail*)
-lemma (in Extend) project_set_I: "!!z. z \<in> C ==> f z \<in> project_set h C"
+lemma project_set_I: "!!z. z \<in> C ==> f z \<in> project_set h C"
 by (auto simp add: split_extended_all)
 
 
@@ -227,42 +232,34 @@
    cannot generalize to 
       project_set h (A \<inter> B) = project_set h A \<inter> project_set h B
 *)
-lemma (in Extend) project_set_extend_set_Int:
-     "project_set h ((extend_set h A) \<inter> B) = A \<inter> (project_set h B)"
-by auto
+lemma project_set_extend_set_Int: "project_set h ((extend_set h A) \<inter> B) = A \<inter> (project_set h B)"
+  by auto
 
 (*Unused, but interesting?*)
-lemma (in Extend) project_set_extend_set_Un:
-     "project_set h ((extend_set h A) \<union> B) = A \<union> (project_set h B)"
-by auto
-
-lemma project_set_Int_subset:
-     "project_set h (A \<inter> B) \<subseteq> (project_set h A) \<inter> (project_set h B)"
-by auto
+lemma project_set_extend_set_Un: "project_set h ((extend_set h A) \<union> B) = A \<union> (project_set h B)"
+  by auto
 
-lemma (in Extend) extend_set_Un_distrib:
-     "extend_set h (A \<union> B) = extend_set h A \<union> extend_set h B"
-by auto
+lemma (in -) project_set_Int_subset:
+    "project_set h (A \<inter> B) \<subseteq> (project_set h A) \<inter> (project_set h B)"
+  by auto
 
-lemma (in Extend) extend_set_Int_distrib:
-     "extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B"
-by auto
+lemma extend_set_Un_distrib: "extend_set h (A \<union> B) = extend_set h A \<union> extend_set h B"
+  by auto
 
-lemma (in Extend) extend_set_INT_distrib:
-     "extend_set h (INTER A B) = (\<Inter>x \<in> A. extend_set h (B x))"
-by auto
+lemma extend_set_Int_distrib: "extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B"
+  by auto
 
-lemma (in Extend) extend_set_Diff_distrib:
-     "extend_set h (A - B) = extend_set h A - extend_set h B"
-by auto
+lemma extend_set_INT_distrib: "extend_set h (INTER A B) = (\<Inter>x \<in> A. extend_set h (B x))"
+  by auto
 
-lemma (in Extend) extend_set_Union:
-     "extend_set h (Union A) = (\<Union>X \<in> A. extend_set h X)"
-by blast
+lemma extend_set_Diff_distrib: "extend_set h (A - B) = extend_set h A - extend_set h B"
+  by auto
 
-lemma (in Extend) extend_set_subset_Compl_eq:
-     "(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)"
-by (unfold extend_set_def, auto)
+lemma extend_set_Union: "extend_set h (Union A) = (\<Union>X \<in> A. extend_set h X)"
+  by blast
+
+lemma extend_set_subset_Compl_eq: "(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)"
+  by (auto simp: extend_set_def)
 
 
 subsection{*@{term extend_act}*}
@@ -270,96 +267,81 @@
 (*Can't strengthen it to
   ((h(s,y), h(s',y')) \<in> extend_act h act) = ((s, s') \<in> act & y=y')
   because h doesn't have to be injective in the 2nd argument*)
-lemma (in Extend) mem_extend_act_iff [iff]: 
-     "((h(s,y), h(s',y)) \<in> extend_act h act) = ((s, s') \<in> act)"
-by (unfold extend_act_def, auto)
+lemma mem_extend_act_iff [iff]: "((h(s,y), h(s',y)) \<in> extend_act h act) = ((s, s') \<in> act)"
+  by (auto simp: extend_act_def)
 
 (*Converse fails: (z,z') would include actions that changed the g-part*)
-lemma (in Extend) extend_act_D: 
-     "(z, z') \<in> extend_act h act ==> (f z, f z') \<in> act"
-by (unfold extend_act_def, auto)
+lemma extend_act_D: "(z, z') \<in> extend_act h act ==> (f z, f z') \<in> act"
+  by (auto simp: extend_act_def)
 
-lemma (in Extend) extend_act_inverse [simp]: 
-     "project_act h (extend_act h act) = act"
-by (unfold extend_act_def project_act_def, blast)
+lemma extend_act_inverse [simp]: "project_act h (extend_act h act) = act"
+  unfolding extend_act_def project_act_def by blast
 
-lemma (in Extend) project_act_extend_act_restrict [simp]: 
+lemma project_act_extend_act_restrict [simp]:
      "project_act h (Restrict C (extend_act h act)) =  
       Restrict (project_set h C) act"
-by (unfold extend_act_def project_act_def, blast)
+  unfolding extend_act_def project_act_def by blast
 
-lemma (in Extend) subset_extend_act_D: 
-     "act' \<subseteq> extend_act h act ==> project_act h act' \<subseteq> act"
-by (unfold extend_act_def project_act_def, force)
+lemma subset_extend_act_D: "act' \<subseteq> extend_act h act ==> project_act h act' \<subseteq> act"
+  unfolding extend_act_def project_act_def by force
 
-lemma (in Extend) inj_extend_act: "inj (extend_act h)"
+lemma inj_extend_act: "inj (extend_act h)"
 apply (rule inj_on_inverseI)
 apply (rule extend_act_inverse)
 done
 
-lemma (in Extend) extend_act_Image [simp]: 
+lemma extend_act_Image [simp]:
      "extend_act h act `` (extend_set h A) = extend_set h (act `` A)"
-by (unfold extend_set_def extend_act_def, force)
+  unfolding extend_set_def extend_act_def by force
 
-lemma (in Extend) extend_act_strict_mono [iff]:
+lemma extend_act_strict_mono [iff]:
      "(extend_act h act' \<subseteq> extend_act h act) = (act'<=act)"
-by (unfold extend_act_def, auto)
+  by (auto simp: extend_act_def)
 
-declare (in Extend) inj_extend_act [THEN inj_eq, iff]
-(*This theorem is  (extend_act h act' = extend_act h act) = (act'=act) *)
-
-lemma Domain_extend_act: 
-    "Domain (extend_act h act) = extend_set h (Domain act)"
-by (unfold extend_set_def extend_act_def, force)
+lemma [iff]: "(extend_act h act = extend_act h act') = (act = act')"
+  by (rule inj_extend_act [THEN inj_eq])
 
-lemma (in Extend) extend_act_Id [simp]: 
-    "extend_act h Id = Id"
-apply (unfold extend_act_def)
-apply (force intro: h_f_g_eq [symmetric])
-done
+lemma (in -) Domain_extend_act:
+    "Domain (extend_act h act) = extend_set h (Domain act)"
+  unfolding extend_set_def extend_act_def by force
+
+lemma extend_act_Id [simp]: "extend_act h Id = Id"
+  unfolding extend_act_def by (force intro: h_f_g_eq [symmetric])
 
-lemma (in Extend) project_act_I: 
-     "!!z z'. (z, z') \<in> act ==> (f z, f z') \<in> project_act h act"
-apply (unfold project_act_def)
-apply (force simp add: split_extended_all)
-done
+lemma project_act_I:  "!!z z'. (z, z') \<in> act ==> (f z, f z') \<in> project_act h act"
+  unfolding project_act_def by (force simp add: split_extended_all)
 
-lemma (in Extend) project_act_Id [simp]: "project_act h Id = Id"
-by (unfold project_act_def, force)
+lemma project_act_Id [simp]: "project_act h Id = Id"
+  unfolding project_act_def by force
 
-lemma (in Extend) Domain_project_act: 
-  "Domain (project_act h act) = project_set h (Domain act)"
-apply (unfold project_act_def)
-apply (force simp add: split_extended_all)
-done
-
+lemma Domain_project_act: "Domain (project_act h act) = project_set h (Domain act)"
+  unfolding project_act_def by (force simp add: split_extended_all)
 
 
 subsection{*extend*}
 
 text{*Basic properties*}
 
-lemma Init_extend [simp]:
+lemma (in -) Init_extend [simp]:
      "Init (extend h F) = extend_set h (Init F)"
-by (unfold extend_def, auto)
+  by (auto simp: extend_def)
 
-lemma Init_project [simp]:
+lemma (in -) Init_project [simp]:
      "Init (project h C F) = project_set h (Init F)"
-by (unfold project_def, auto)
+  by (auto simp: project_def)
 
-lemma (in Extend) Acts_extend [simp]:
-     "Acts (extend h F) = (extend_act h ` Acts F)"
-by (simp add: extend_def insert_Id_image_Acts)
+lemma Acts_extend [simp]: "Acts (extend h F) = (extend_act h ` Acts F)"
+  by (simp add: extend_def insert_Id_image_Acts)
 
-lemma (in Extend) AllowedActs_extend [simp]:
+lemma AllowedActs_extend [simp]:
      "AllowedActs (extend h F) = project_act h -` AllowedActs F"
-by (simp add: extend_def insert_absorb)
+  by (simp add: extend_def insert_absorb)
 
-lemma Acts_project [simp]:
+lemma (in -) Acts_project [simp]:
      "Acts(project h C F) = insert Id (project_act h ` Restrict C ` Acts F)"
-by (auto simp add: project_def image_iff)
+  by (auto simp add: project_def image_iff)
 
-lemma (in Extend) AllowedActs_project [simp]:
+lemma AllowedActs_project [simp]:
      "AllowedActs(project h C F) =  
         {act. Restrict (project_set h C) act  
                \<in> project_act h ` Restrict C ` AllowedActs F}"
@@ -368,35 +350,31 @@
 apply (auto intro!: bexI [of _ Id] simp add: project_act_def)
 done
 
-lemma (in Extend) Allowed_extend:
-     "Allowed (extend h F) = project h UNIV -` Allowed F"
-by (auto simp add: Allowed_def)
+lemma Allowed_extend: "Allowed (extend h F) = project h UNIV -` Allowed F"
+  by (auto simp add: Allowed_def)
 
-lemma (in Extend) extend_SKIP [simp]: "extend h SKIP = SKIP"
+lemma extend_SKIP [simp]: "extend h SKIP = SKIP"
 apply (unfold SKIP_def)
 apply (rule program_equalityI, auto)
 done
 
-lemma project_set_UNIV [simp]: "project_set h UNIV = UNIV"
-by auto
+lemma (in -) project_set_UNIV [simp]: "project_set h UNIV = UNIV"
+  by auto
 
-lemma project_set_Union:
-     "project_set h (Union A) = (\<Union>X \<in> A. project_set h X)"
-by blast
+lemma (in -) project_set_Union: "project_set h (Union A) = (\<Union>X \<in> A. project_set h X)"
+  by blast
 
 
 (*Converse FAILS: the extended state contributing to project_set h C
   may not coincide with the one contributing to project_act h act*)
-lemma (in Extend) project_act_Restrict_subset:
-     "project_act h (Restrict C act) \<subseteq>  
-      Restrict (project_set h C) (project_act h act)"
-by (auto simp add: project_act_def)
+lemma (in -) project_act_Restrict_subset:
+     "project_act h (Restrict C act) \<subseteq> Restrict (project_set h C) (project_act h act)"
+  by (auto simp add: project_act_def)
 
-lemma (in Extend) project_act_Restrict_Id_eq:
-     "project_act h (Restrict C Id) = Restrict (project_set h C) Id"
-by (auto simp add: project_act_def)
+lemma project_act_Restrict_Id_eq: "project_act h (Restrict C Id) = Restrict (project_set h C) Id"
+  by (auto simp add: project_act_def)
 
-lemma (in Extend) project_extend_eq:
+lemma project_extend_eq:
      "project h C (extend h F) =  
       mk_program (Init F, Restrict (project_set h C) ` Acts F,  
                   {act. Restrict (project_set h C) act 
@@ -408,7 +386,7 @@
 apply (simp add: project_def)
 done
 
-lemma (in Extend) extend_inverse [simp]:
+lemma extend_inverse [simp]:
      "project h UNIV (extend h F) = F"
 apply (simp (no_asm_simp) add: project_extend_eq image_eq_UN
           subset_UNIV [THEN subset_trans, THEN Restrict_triv])
@@ -421,20 +399,18 @@
 apply (rule_tac x = "extend_act h act" in bexI, auto)
 done
 
-lemma (in Extend) inj_extend: "inj (extend h)"
+lemma inj_extend: "inj (extend h)"
 apply (rule inj_on_inverseI)
 apply (rule extend_inverse)
 done
 
-lemma (in Extend) extend_Join [simp]:
-     "extend h (F\<squnion>G) = extend h F\<squnion>extend h G"
+lemma extend_Join [simp]: "extend h (F\<squnion>G) = extend h F\<squnion>extend h G"
 apply (rule program_equalityI)
 apply (simp (no_asm) add: extend_set_Int_distrib)
 apply (simp add: image_Un, auto)
 done
 
-lemma (in Extend) extend_JN [simp]:
-     "extend h (JOIN I F) = (\<Squnion>i \<in> I. extend h (F i))"
+lemma extend_JN [simp]: "extend h (JOIN I F) = (\<Squnion>i \<in> I. extend h (F i))"
 apply (rule program_equalityI)
   apply (simp (no_asm) add: extend_set_INT_distrib)
  apply (simp add: image_UN, auto)
@@ -442,55 +418,50 @@
 
 (** These monotonicity results look natural but are UNUSED **)
 
-lemma (in Extend) extend_mono: "F \<le> G ==> extend h F \<le> extend h G"
-by (force simp add: component_eq_subset)
+lemma extend_mono: "F \<le> G ==> extend h F \<le> extend h G"
+  by (force simp add: component_eq_subset)
 
-lemma (in Extend) project_mono: "F \<le> G ==> project h C F \<le> project h C G"
-by (simp add: component_eq_subset, blast)
+lemma project_mono: "F \<le> G ==> project h C F \<le> project h C G"
+  by (simp add: component_eq_subset, blast)
 
-lemma (in Extend) all_total_extend: "all_total F ==> all_total (extend h F)"
-by (simp add: all_total_def Domain_extend_act)
+lemma all_total_extend: "all_total F ==> all_total (extend h F)"
+  by (simp add: all_total_def Domain_extend_act)
 
 subsection{*Safety: co, stable*}
 
-lemma (in Extend) extend_constrains:
+lemma extend_constrains:
      "(extend h F \<in> (extend_set h A) co (extend_set h B)) =  
       (F \<in> A co B)"
-by (simp add: constrains_def)
+  by (simp add: constrains_def)
 
-lemma (in Extend) extend_stable:
+lemma extend_stable:
      "(extend h F \<in> stable (extend_set h A)) = (F \<in> stable A)"
-by (simp add: stable_def extend_constrains)
+  by (simp add: stable_def extend_constrains)
 
-lemma (in Extend) extend_invariant:
+lemma extend_invariant:
      "(extend h F \<in> invariant (extend_set h A)) = (F \<in> invariant A)"
-by (simp add: invariant_def extend_stable)
+  by (simp add: invariant_def extend_stable)
 
 (*Projects the state predicates in the property satisfied by  extend h F.
   Converse fails: A and B may differ in their extra variables*)
-lemma (in Extend) extend_constrains_project_set:
+lemma extend_constrains_project_set:
      "extend h F \<in> A co B ==> F \<in> (project_set h A) co (project_set h B)"
-by (auto simp add: constrains_def, force)
+  by (auto simp add: constrains_def, force)
 
-lemma (in Extend) extend_stable_project_set:
+lemma extend_stable_project_set:
      "extend h F \<in> stable A ==> F \<in> stable (project_set h A)"
-by (simp add: stable_def extend_constrains_project_set)
+  by (simp add: stable_def extend_constrains_project_set)
 
 
 subsection{*Weak safety primitives: Co, Stable*}
 
-lemma (in Extend) reachable_extend_f:
-     "p \<in> reachable (extend h F) ==> f p \<in> reachable F"
-apply (erule reachable.induct)
-apply (auto intro: reachable.intros simp add: extend_act_def image_iff)
-done
+lemma reachable_extend_f: "p \<in> reachable (extend h F) ==> f p \<in> reachable F"
+  by (induct set: reachable) (auto intro: reachable.intros simp add: extend_act_def image_iff)
 
-lemma (in Extend) h_reachable_extend:
-     "h(s,y) \<in> reachable (extend h F) ==> s \<in> reachable F"
-by (force dest!: reachable_extend_f)
+lemma h_reachable_extend: "h(s,y) \<in> reachable (extend h F) ==> s \<in> reachable F"
+  by (force dest!: reachable_extend_f)
 
-lemma (in Extend) reachable_extend_eq: 
-     "reachable (extend h F) = extend_set h (reachable F)"
+lemma reachable_extend_eq: "reachable (extend h F) = extend_set h (reachable F)"
 apply (unfold extend_set_def)
 apply (rule equalityI)
 apply (force intro: h_f_g_eq [symmetric] dest!: reachable_extend_f, clarify)
@@ -498,42 +469,40 @@
 apply (force intro: reachable.intros)+
 done
 
-lemma (in Extend) extend_Constrains:
+lemma extend_Constrains:
      "(extend h F \<in> (extend_set h A) Co (extend_set h B)) =   
       (F \<in> A Co B)"
-by (simp add: Constrains_def reachable_extend_eq extend_constrains 
+  by (simp add: Constrains_def reachable_extend_eq extend_constrains 
               extend_set_Int_distrib [symmetric])
 
-lemma (in Extend) extend_Stable:
-     "(extend h F \<in> Stable (extend_set h A)) = (F \<in> Stable A)"
-by (simp add: Stable_def extend_Constrains)
+lemma extend_Stable: "(extend h F \<in> Stable (extend_set h A)) = (F \<in> Stable A)"
+  by (simp add: Stable_def extend_Constrains)
 
-lemma (in Extend) extend_Always:
-     "(extend h F \<in> Always (extend_set h A)) = (F \<in> Always A)"
-by (simp (no_asm_simp) add: Always_def extend_Stable)
+lemma extend_Always: "(extend h F \<in> Always (extend_set h A)) = (F \<in> Always A)"
+  by (simp add: Always_def extend_Stable)
 
 
 (** Safety and "project" **)
 
 (** projection: monotonicity for safety **)
 
-lemma project_act_mono:
+lemma (in -) project_act_mono:
      "D \<subseteq> C ==>  
       project_act h (Restrict D act) \<subseteq> project_act h (Restrict C act)"
-by (auto simp add: project_act_def)
+  by (auto simp add: project_act_def)
 
-lemma (in Extend) project_constrains_mono:
+lemma project_constrains_mono:
      "[| D \<subseteq> C; project h C F \<in> A co B |] ==> project h D F \<in> A co B"
 apply (auto simp add: constrains_def)
 apply (drule project_act_mono, blast)
 done
 
-lemma (in Extend) project_stable_mono:
+lemma project_stable_mono:
      "[| D \<subseteq> C;  project h C F \<in> stable A |] ==> project h D F \<in> stable A"
-by (simp add: stable_def project_constrains_mono)
+  by (simp add: stable_def project_constrains_mono)
 
 (*Key lemma used in several proofs about project and co*)
-lemma (in Extend) project_constrains: 
+lemma project_constrains: 
      "(project h C F \<in> A co B)  =   
       (F \<in> (C \<inter> extend_set h A) co (extend_set h B) & A \<subseteq> B)"
 apply (unfold constrains_def)
@@ -544,45 +513,41 @@
 apply (force dest!: subsetD)
 done
 
-lemma (in Extend) project_stable: 
-     "(project h UNIV F \<in> stable A) = (F \<in> stable (extend_set h A))"
-apply (unfold stable_def)
-apply (simp (no_asm) add: project_constrains)
-done
+lemma project_stable: "(project h UNIV F \<in> stable A) = (F \<in> stable (extend_set h A))"
+  by (simp add: stable_def project_constrains)
 
-lemma (in Extend) project_stable_I:
-     "F \<in> stable (extend_set h A) ==> project h C F \<in> stable A"
+lemma project_stable_I: "F \<in> stable (extend_set h A) ==> project h C F \<in> stable A"
 apply (drule project_stable [THEN iffD2])
 apply (blast intro: project_stable_mono)
 done
 
-lemma (in Extend) Int_extend_set_lemma:
+lemma Int_extend_set_lemma:
      "A \<inter> extend_set h ((project_set h A) \<inter> B) = A \<inter> extend_set h B"
-by (auto simp add: split_extended_all)
+  by (auto simp add: split_extended_all)
 
 (*Strange (look at occurrences of C) but used in leadsETo proofs*)
 lemma project_constrains_project_set:
      "G \<in> C co B ==> project h C G \<in> project_set h C co project_set h B"
-by (simp add: constrains_def project_def project_act_def, blast)
+  by (simp add: constrains_def project_def project_act_def, blast)
 
 lemma project_stable_project_set:
      "G \<in> stable C ==> project h C G \<in> stable (project_set h C)"
-by (simp add: stable_def project_constrains_project_set)
+  by (simp add: stable_def project_constrains_project_set)
 
 
 subsection{*Progress: transient, ensures*}
 
-lemma (in Extend) extend_transient:
+lemma extend_transient:
      "(extend h F \<in> transient (extend_set h A)) = (F \<in> transient A)"
-by (auto simp add: transient_def extend_set_subset_Compl_eq Domain_extend_act)
+  by (auto simp add: transient_def extend_set_subset_Compl_eq Domain_extend_act)
 
-lemma (in Extend) extend_ensures:
+lemma extend_ensures:
      "(extend h F \<in> (extend_set h A) ensures (extend_set h B)) =  
       (F \<in> A ensures B)"
-by (simp add: ensures_def extend_constrains extend_transient 
+  by (simp add: ensures_def extend_constrains extend_transient 
         extend_set_Un_distrib [symmetric] extend_set_Diff_distrib [symmetric])
 
-lemma (in Extend) leadsTo_imp_extend_leadsTo:
+lemma leadsTo_imp_extend_leadsTo:
      "F \<in> A leadsTo B  
       ==> extend h F \<in> (extend_set h A) leadsTo (extend_set h B)"
 apply (erule leadsTo_induct)
@@ -593,42 +558,41 @@
 
 subsection{*Proving the converse takes some doing!*}
 
-lemma (in Extend) slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
-by (simp (no_asm) add: slice_def)
+lemma slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
+  by (simp add: slice_def)
 
-lemma (in Extend) slice_Union: "slice (Union S) y = (\<Union>x \<in> S. slice x y)"
-by auto
+lemma slice_Union: "slice (Union S) y = (\<Union>x \<in> S. slice x y)"
+  by auto
 
-lemma (in Extend) slice_extend_set: "slice (extend_set h A) y = A"
-by auto
+lemma slice_extend_set: "slice (extend_set h A) y = A"
+  by auto
 
-lemma (in Extend) project_set_is_UN_slice:
-     "project_set h A = (\<Union>y. slice A y)"
-by auto
+lemma project_set_is_UN_slice: "project_set h A = (\<Union>y. slice A y)"
+  by auto
 
-lemma (in Extend) extend_transient_slice:
+lemma extend_transient_slice:
      "extend h F \<in> transient A ==> F \<in> transient (slice A y)"
-by (unfold transient_def, auto)
+  by (auto simp: transient_def)
 
 (*Converse?*)
-lemma (in Extend) extend_constrains_slice:
+lemma extend_constrains_slice:
      "extend h F \<in> A co B ==> F \<in> (slice A y) co (slice B y)"
-by (auto simp add: constrains_def)
+  by (auto simp add: constrains_def)
 
-lemma (in Extend) extend_ensures_slice:
+lemma extend_ensures_slice:
      "extend h F \<in> A ensures B ==> F \<in> (slice A y) ensures (project_set h B)"
 apply (auto simp add: ensures_def extend_constrains extend_transient)
 apply (erule_tac [2] extend_transient_slice [THEN transient_strengthen])
 apply (erule extend_constrains_slice [THEN constrains_weaken], auto)
 done
 
-lemma (in Extend) leadsTo_slice_project_set:
+lemma leadsTo_slice_project_set:
      "\<forall>y. F \<in> (slice B y) leadsTo CU ==> F \<in> (project_set h B) leadsTo CU"
-apply (simp (no_asm) add: project_set_is_UN_slice)
+apply (simp add: project_set_is_UN_slice)
 apply (blast intro: leadsTo_UN)
 done
 
-lemma (in Extend) extend_leadsTo_slice [rule_format]:
+lemma extend_leadsTo_slice [rule_format]:
      "extend h F \<in> AU leadsTo BU  
       ==> \<forall>y. F \<in> (slice AU y) leadsTo (project_set h BU)"
 apply (erule leadsTo_induct)
@@ -637,7 +601,7 @@
 apply (simp add: leadsTo_UN slice_Union)
 done
 
-lemma (in Extend) extend_leadsTo:
+lemma extend_leadsTo:
      "(extend h F \<in> (extend_set h A) leadsTo (extend_set h B)) =  
       (F \<in> A leadsTo B)"
 apply safe
@@ -646,44 +610,43 @@
 apply (simp add: slice_extend_set)
 done
 
-lemma (in Extend) extend_LeadsTo:
+lemma extend_LeadsTo:
      "(extend h F \<in> (extend_set h A) LeadsTo (extend_set h B)) =   
       (F \<in> A LeadsTo B)"
-by (simp add: LeadsTo_def reachable_extend_eq extend_leadsTo
+  by (simp add: LeadsTo_def reachable_extend_eq extend_leadsTo
               extend_set_Int_distrib [symmetric])
 
 
 subsection{*preserves*}
 
-lemma (in Extend) project_preserves_I:
+lemma project_preserves_I:
      "G \<in> preserves (v o f) ==> project h C G \<in> preserves v"
-by (auto simp add: preserves_def project_stable_I extend_set_eq_Collect)
+  by (auto simp add: preserves_def project_stable_I extend_set_eq_Collect)
 
 (*to preserve f is to preserve the whole original state*)
-lemma (in Extend) project_preserves_id_I:
+lemma project_preserves_id_I:
      "G \<in> preserves f ==> project h C G \<in> preserves id"
-by (simp add: project_preserves_I)
+  by (simp add: project_preserves_I)
 
-lemma (in Extend) extend_preserves:
+lemma extend_preserves:
      "(extend h G \<in> preserves (v o f)) = (G \<in> preserves v)"
-by (auto simp add: preserves_def extend_stable [symmetric] 
+  by (auto simp add: preserves_def extend_stable [symmetric] 
                    extend_set_eq_Collect)
 
-lemma (in Extend) inj_extend_preserves: "inj h ==> (extend h G \<in> preserves g)"
-by (auto simp add: preserves_def extend_def extend_act_def stable_def 
+lemma inj_extend_preserves: "inj h ==> (extend h G \<in> preserves g)"
+  by (auto simp add: preserves_def extend_def extend_act_def stable_def 
                    constrains_def g_def)
 
 
 subsection{*Guarantees*}
 
-lemma (in Extend) project_extend_Join:
-     "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
+lemma project_extend_Join: "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
 apply (rule program_equalityI)
   apply (simp add: project_set_extend_set_Int)
  apply (auto simp add: image_eq_UN)
 done
 
-lemma (in Extend) extend_Join_eq_extend_D:
+lemma extend_Join_eq_extend_D:
      "(extend h F)\<squnion>G = extend h H ==> H = F\<squnion>(project h UNIV G)"
 apply (drule_tac f = "project h UNIV" in arg_cong)
 apply (simp add: project_extend_Join)
@@ -693,26 +656,25 @@
     the old and new state sets are in bijection **)
 
 
-lemma (in Extend) ok_extend_imp_ok_project:
-     "extend h F ok G ==> F ok project h UNIV G"
+lemma ok_extend_imp_ok_project: "extend h F ok G ==> F ok project h UNIV G"
 apply (auto simp add: ok_def)
 apply (drule subsetD)
 apply (auto intro!: rev_image_eqI)
 done
 
-lemma (in Extend) ok_extend_iff: "(extend h F ok extend h G) = (F ok G)"
+lemma ok_extend_iff: "(extend h F ok extend h G) = (F ok G)"
 apply (simp add: ok_def, safe)
-apply (force+)
+apply force+
 done
 
-lemma (in Extend) OK_extend_iff: "OK I (%i. extend h (F i)) = (OK I F)"
+lemma OK_extend_iff: "OK I (%i. extend h (F i)) = (OK I F)"
 apply (unfold OK_def, safe)
 apply (drule_tac x = i in bspec)
 apply (drule_tac [2] x = j in bspec)
-apply (force+)
+apply force+
 done
 
-lemma (in Extend) guarantees_imp_extend_guarantees:
+lemma guarantees_imp_extend_guarantees:
      "F \<in> X guarantees Y ==>  
       extend h F \<in> (extend h ` X) guarantees (extend h ` Y)"
 apply (rule guaranteesI, clarify)
@@ -720,7 +682,7 @@
                    guaranteesD)
 done
 
-lemma (in Extend) extend_guarantees_imp_guarantees:
+lemma extend_guarantees_imp_guarantees:
      "extend h F \<in> (extend h ` X) guarantees (extend h ` Y)  
       ==> F \<in> X guarantees Y"
 apply (auto simp add: guar_def)
@@ -730,10 +692,12 @@
                  inj_extend [THEN inj_image_mem_iff])
 done
 
-lemma (in Extend) extend_guarantees_eq:
+lemma extend_guarantees_eq:
      "(extend h F \<in> (extend h ` X) guarantees (extend h ` Y)) =  
       (F \<in> X guarantees Y)"
-by (blast intro: guarantees_imp_extend_guarantees 
+  by (blast intro: guarantees_imp_extend_guarantees 
                  extend_guarantees_imp_guarantees)
 
 end
+
+end
diff -r 6d2a2f0e904e -r e0cd5c4df8e6 src/HOL/UNITY/Project.thy
--- a/src/HOL/UNITY/Project.thy	Tue Mar 13 22:49:02 2012 +0100
+++ b/src/HOL/UNITY/Project.thy	Tue Mar 13 23:33:35 2012 +0100
@@ -26,7 +26,10 @@
     "subset_closed U == \<forall>A \<in> U. Pow A \<subseteq> U"  
 
 
-lemma (in Extend) project_extend_constrains_I:
+context Extend
+begin
+
+lemma project_extend_constrains_I:
      "F \<in> A co B ==> project h C (extend h F) \<in> A co B"
 apply (auto simp add: extend_act_def project_act_def constrains_def)
 done
@@ -35,7 +38,7 @@
 subsection{*Safety*}
 
 (*used below to prove Join_project_ensures*)
-lemma (in Extend) project_unless:
+lemma project_unless:
      "[| G \<in> stable C;  project h C G \<in> A unless B |]  
       ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
 apply (simp add: unless_def project_constrains)
@@ -44,7 +47,7 @@
 
 (*Generalizes project_constrains to the program F\<squnion>project h C G
   useful with guarantees reasoning*)
-lemma (in Extend) Join_project_constrains:
+lemma Join_project_constrains:
      "(F\<squnion>project h C G \<in> A co B)  =   
         (extend h F\<squnion>G \<in> (C \<inter> extend_set h A) co (extend_set h B) &   
          F \<in> A co B)"
@@ -55,7 +58,7 @@
 
 (*The condition is required to prove the left-to-right direction
   could weaken it to G \<in> (C \<inter> extend_set h A) co C*)
-lemma (in Extend) Join_project_stable: 
+lemma Join_project_stable: 
      "extend h F\<squnion>G \<in> stable C  
       ==> (F\<squnion>project h C G \<in> stable A)  =   
           (extend h F\<squnion>G \<in> stable (C \<inter> extend_set h A) &   
@@ -66,14 +69,14 @@
 done
 
 (*For using project_guarantees in particular cases*)
-lemma (in Extend) project_constrains_I:
+lemma project_constrains_I:
      "extend h F\<squnion>G \<in> extend_set h A co extend_set h B  
       ==> F\<squnion>project h C G \<in> A co B"
 apply (simp add: project_constrains extend_constrains)
 apply (blast intro: constrains_weaken dest: constrains_imp_subset)
 done
 
-lemma (in Extend) project_increasing_I: 
+lemma project_increasing_I: 
      "extend h F\<squnion>G \<in> increasing (func o f)  
       ==> F\<squnion>project h C G \<in> increasing func"
 apply (unfold increasing_def stable_def)
@@ -81,7 +84,7 @@
             add: project_constrains_I extend_set_eq_Collect)
 done
 
-lemma (in Extend) Join_project_increasing:
+lemma Join_project_increasing:
      "(F\<squnion>project h UNIV G \<in> increasing func)  =   
       (extend h F\<squnion>G \<in> increasing (func o f))"
 apply (rule iffI)
@@ -92,11 +95,13 @@
 done
 
 (*The UNIV argument is essential*)
-lemma (in Extend) project_constrains_D:
+lemma project_constrains_D:
      "F\<squnion>project h UNIV G \<in> A co B  
       ==> extend h F\<squnion>G \<in> extend_set h A co extend_set h B"
 by (simp add: project_constrains extend_constrains)
 
+end
+
 
 subsection{*"projecting" and union/intersection (no converses)*}
 
@@ -159,41 +164,44 @@
 lemma projecting_UNIV: "projecting C h F X' UNIV"
 by (simp add: projecting_def)
 
-lemma (in Extend) projecting_constrains: 
+context Extend
+begin
+
+lemma projecting_constrains: 
      "projecting C h F (extend_set h A co extend_set h B) (A co B)"
 apply (unfold projecting_def)
 apply (blast intro: project_constrains_I)
 done
 
-lemma (in Extend) projecting_stable: 
+lemma projecting_stable: 
      "projecting C h F (stable (extend_set h A)) (stable A)"
 apply (unfold stable_def)
 apply (rule projecting_constrains)
 done
 
-lemma (in Extend) projecting_increasing: 
+lemma projecting_increasing: 
      "projecting C h F (increasing (func o f)) (increasing func)"
 apply (unfold projecting_def)
 apply (blast intro: project_increasing_I)
 done
 
-lemma (in Extend) extending_UNIV: "extending C h F UNIV Y"
+lemma extending_UNIV: "extending C h F UNIV Y"
 apply (simp (no_asm) add: extending_def)
 done
 
-lemma (in Extend) extending_constrains: 
+lemma extending_constrains: 
      "extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)"
 apply (unfold extending_def)
 apply (blast intro: project_constrains_D)
 done
 
-lemma (in Extend) extending_stable: 
+lemma extending_stable: 
      "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)"
 apply (unfold stable_def)
 apply (rule extending_constrains)
 done
 
-lemma (in Extend) extending_increasing: 
+lemma extending_increasing: 
      "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)"
 by (force simp only: extending_def Join_project_increasing)
 
@@ -201,7 +209,7 @@
 subsection{*Reachability and project*}
 
 (*In practice, C = reachable(...): the inclusion is equality*)
-lemma (in Extend) reachable_imp_reachable_project:
+lemma reachable_imp_reachable_project:
      "[| reachable (extend h F\<squnion>G) \<subseteq> C;   
          z \<in> reachable (extend h F\<squnion>G) |]  
       ==> f z \<in> reachable (F\<squnion>project h C G)"
@@ -214,7 +222,7 @@
        in project_act_I [THEN [3] reachable.Acts], auto) 
 done
 
-lemma (in Extend) project_Constrains_D: 
+lemma project_Constrains_D: 
      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B   
       ==> extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)"
 apply (unfold Constrains_def)
@@ -224,21 +232,21 @@
 apply (auto intro: reachable_imp_reachable_project)
 done
 
-lemma (in Extend) project_Stable_D: 
+lemma project_Stable_D: 
      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A   
       ==> extend h F\<squnion>G \<in> Stable (extend_set h A)"
 apply (unfold Stable_def)
 apply (simp (no_asm_simp) add: project_Constrains_D)
 done
 
-lemma (in Extend) project_Always_D: 
+lemma project_Always_D: 
      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A   
       ==> extend h F\<squnion>G \<in> Always (extend_set h A)"
 apply (unfold Always_def)
 apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
 done
 
-lemma (in Extend) project_Increasing_D: 
+lemma project_Increasing_D: 
      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func   
       ==> extend h F\<squnion>G \<in> Increasing (func o f)"
 apply (unfold Increasing_def, auto)
@@ -250,7 +258,7 @@
 subsection{*Converse results for weak safety: benefits of the argument C *}
 
 (*In practice, C = reachable(...): the inclusion is equality*)
-lemma (in Extend) reachable_project_imp_reachable:
+lemma reachable_project_imp_reachable:
      "[| C \<subseteq> reachable(extend h F\<squnion>G);    
          x \<in> reachable (F\<squnion>project h C G) |]  
       ==> \<exists>y. h(x,y) \<in> reachable (extend h F\<squnion>G)"
@@ -260,21 +268,21 @@
 apply (force del: Id_in_Acts intro: reachable.Acts extend_act_D)+
 done
 
-lemma (in Extend) project_set_reachable_extend_eq:
+lemma project_set_reachable_extend_eq:
      "project_set h (reachable (extend h F\<squnion>G)) =  
       reachable (F\<squnion>project h (reachable (extend h F\<squnion>G)) G)"
 by (auto dest: subset_refl [THEN reachable_imp_reachable_project] 
                subset_refl [THEN reachable_project_imp_reachable])
 
 (*UNUSED*)
-lemma (in Extend) reachable_extend_Join_subset:
+lemma reachable_extend_Join_subset:
      "reachable (extend h F\<squnion>G) \<subseteq> C   
       ==> reachable (extend h F\<squnion>G) \<subseteq>  
           extend_set h (reachable (F\<squnion>project h C G))"
 apply (auto dest: reachable_imp_reachable_project)
 done
 
-lemma (in Extend) project_Constrains_I: 
+lemma project_Constrains_I: 
      "extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)   
       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B"
 apply (unfold Constrains_def)
@@ -288,14 +296,14 @@
 apply (blast intro: constrains_weaken_L)
 done
 
-lemma (in Extend) project_Stable_I: 
+lemma project_Stable_I: 
      "extend h F\<squnion>G \<in> Stable (extend_set h A)   
       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A"
 apply (unfold Stable_def)
 apply (simp (no_asm_simp) add: project_Constrains_I)
 done
 
-lemma (in Extend) project_Always_I: 
+lemma project_Always_I: 
      "extend h F\<squnion>G \<in> Always (extend_set h A)   
       ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A"
 apply (unfold Always_def)
@@ -303,27 +311,27 @@
 apply (unfold extend_set_def, blast)
 done
 
-lemma (in Extend) project_Increasing_I: 
+lemma project_Increasing_I: 
     "extend h F\<squnion>G \<in> Increasing (func o f)   
      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func"
 apply (unfold Increasing_def, auto)
 apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
 done
 
-lemma (in Extend) project_Constrains:
+lemma project_Constrains:
      "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B)  =   
       (extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B))"
 apply (blast intro: project_Constrains_I project_Constrains_D)
 done
 
-lemma (in Extend) project_Stable: 
+lemma project_Stable: 
      "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A)  =   
       (extend h F\<squnion>G \<in> Stable (extend_set h A))"
 apply (unfold Stable_def)
 apply (rule project_Constrains)
 done
 
-lemma (in Extend) project_Increasing: 
+lemma project_Increasing: 
    "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func)  =  
     (extend h F\<squnion>G \<in> Increasing (func o f))"
 apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
@@ -332,7 +340,7 @@
 subsection{*A lot of redundant theorems: all are proved to facilitate reasoning
     about guarantees.*}
 
-lemma (in Extend) projecting_Constrains: 
+lemma projecting_Constrains: 
      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
                  (extend_set h A Co extend_set h B) (A Co B)"
 
@@ -340,49 +348,49 @@
 apply (blast intro: project_Constrains_I)
 done
 
-lemma (in Extend) projecting_Stable: 
+lemma projecting_Stable: 
      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
                  (Stable (extend_set h A)) (Stable A)"
 apply (unfold Stable_def)
 apply (rule projecting_Constrains)
 done
 
-lemma (in Extend) projecting_Always: 
+lemma projecting_Always: 
      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
                  (Always (extend_set h A)) (Always A)"
 apply (unfold projecting_def)
 apply (blast intro: project_Always_I)
 done
 
-lemma (in Extend) projecting_Increasing: 
+lemma projecting_Increasing: 
      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
                  (Increasing (func o f)) (Increasing func)"
 apply (unfold projecting_def)
 apply (blast intro: project_Increasing_I)
 done
 
-lemma (in Extend) extending_Constrains: 
+lemma extending_Constrains: 
      "extending (%G. reachable (extend h F\<squnion>G)) h F  
                   (extend_set h A Co extend_set h B) (A Co B)"
 apply (unfold extending_def)
 apply (blast intro: project_Constrains_D)
 done
 
-lemma (in Extend) extending_Stable: 
+lemma extending_Stable: 
      "extending (%G. reachable (extend h F\<squnion>G)) h F  
                   (Stable (extend_set h A)) (Stable A)"
 apply (unfold extending_def)
 apply (blast intro: project_Stable_D)
 done
 
-lemma (in Extend) extending_Always: 
+lemma extending_Always: 
      "extending (%G. reachable (extend h F\<squnion>G)) h F  
                   (Always (extend_set h A)) (Always A)"
 apply (unfold extending_def)
 apply (blast intro: project_Always_D)
 done
 
-lemma (in Extend) extending_Increasing: 
+lemma extending_Increasing: 
      "extending (%G. reachable (extend h F\<squnion>G)) h F  
                   (Increasing (func o f)) (Increasing func)"
 apply (unfold extending_def)
@@ -394,7 +402,7 @@
 
 subsubsection{*transient*}
 
-lemma (in Extend) transient_extend_set_imp_project_transient: 
+lemma transient_extend_set_imp_project_transient: 
      "[| G \<in> transient (C \<inter> extend_set h A);  G \<in> stable C |]   
       ==> project h C G \<in> transient (project_set h C \<inter> A)"
 apply (auto simp add: transient_def Domain_project_act)
@@ -408,7 +416,7 @@
 done
 
 (*converse might hold too?*)
-lemma (in Extend) project_extend_transient_D: 
+lemma project_extend_transient_D: 
      "project h C (extend h F) \<in> transient (project_set h C \<inter> D)  
       ==> F \<in> transient (project_set h C \<inter> D)"
 apply (simp add: transient_def Domain_project_act, safe)
@@ -419,12 +427,12 @@
 subsubsection{*ensures -- a primitive combining progress with safety*}
 
 (*Used to prove project_leadsETo_I*)
-lemma (in Extend) ensures_extend_set_imp_project_ensures:
+lemma ensures_extend_set_imp_project_ensures:
      "[| extend h F \<in> stable C;  G \<in> stable C;   
          extend h F\<squnion>G \<in> A ensures B;  A-B = C \<inter> extend_set h D |]   
       ==> F\<squnion>project h C G   
             \<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)"
-apply (simp add: ensures_def project_constrains Join_transient extend_transient,
+apply (simp add: ensures_def project_constrains extend_transient,
        clarify)
 apply (intro conjI) 
 (*first subgoal*)
@@ -451,7 +459,7 @@
 done
 
 text{*Transferring a transient property upwards*}
-lemma (in Extend) project_transient_extend_set:
+lemma project_transient_extend_set:
      "project h C G \<in> transient (project_set h C \<inter> A - B)
       ==> G \<in> transient (C \<inter> extend_set h A - extend_set h B)"
 apply (simp add: transient_def project_set_def extend_set_def project_act_def)
@@ -460,7 +468,7 @@
   apply (blast intro!: rev_bexI )+
 done
 
-lemma (in Extend) project_unless2:
+lemma project_unless2:
      "[| G \<in> stable C;  project h C G \<in> (project_set h C \<inter> A) unless B |]  
       ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)"
 by (auto dest: stable_constrains_Int intro: constrains_weaken
@@ -468,7 +476,7 @@
                    Int_extend_set_lemma)
 
 
-lemma (in Extend) extend_unless:
+lemma extend_unless:
    "[|extend h F \<in> stable C; F \<in> A unless B|]
     ==> extend h F \<in> C \<inter> extend_set h A unless extend_set h B"
 apply (simp add: unless_def stable_def)
@@ -479,7 +487,7 @@
 done
 
 (*Used to prove project_leadsETo_D*)
-lemma (in Extend) Join_project_ensures:
+lemma Join_project_ensures:
      "[| extend h F\<squnion>G \<in> stable C;   
          F\<squnion>project h C G \<in> A ensures B |]  
       ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
@@ -493,18 +501,18 @@
 
 (*The strange induction formula allows induction over the leadsTo
   assumption's non-atomic precondition*)
-lemma (in Extend) PLD_lemma:
+lemma PLD_lemma:
      "[| extend h F\<squnion>G \<in> stable C;   
          F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
       ==> extend h F\<squnion>G \<in>  
           C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)"
 apply (erule leadsTo_induct)
-  apply (blast intro: leadsTo_Basis Join_project_ensures)
+  apply (blast intro: Join_project_ensures)
  apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans)
 apply (simp del: UN_simps add: Int_UN_distrib leadsTo_UN extend_set_Union)
 done
 
-lemma (in Extend) project_leadsTo_D_lemma:
+lemma project_leadsTo_D_lemma:
      "[| extend h F\<squnion>G \<in> stable C;   
          F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
       ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
@@ -512,7 +520,7 @@
 apply (auto simp add: split_extended_all)
 done
 
-lemma (in Extend) Join_project_LeadsTo:
+lemma Join_project_LeadsTo:
      "[| C = (reachable (extend h F\<squnion>G));  
          F\<squnion>project h C G \<in> A LeadsTo B |]  
       ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
@@ -522,7 +530,7 @@
 
 subsection{*Towards the theorem @{text project_Ensures_D}*}
 
-lemma (in Extend) project_ensures_D_lemma:
+lemma project_ensures_D_lemma:
      "[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B));   
          F\<squnion>project h C G \<in> (project_set h C \<inter> A) ensures B;   
          extend h F\<squnion>G \<in> stable C |]  
@@ -540,14 +548,14 @@
              simp add: split_extended_all)
 done
 
-lemma (in Extend) project_ensures_D:
+lemma project_ensures_D:
      "[| F\<squnion>project h UNIV G \<in> A ensures B;   
          G \<in> stable (extend_set h A - extend_set h B) |]  
       ==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)"
 apply (rule project_ensures_D_lemma [of _ UNIV, elim_format], auto)
 done
 
-lemma (in Extend) project_Ensures_D: 
+lemma project_Ensures_D: 
      "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Ensures B;   
          G \<in> stable (reachable (extend h F\<squnion>G) \<inter> extend_set h A -  
                      extend_set h B) |]  
@@ -560,13 +568,13 @@
 
 subsection{*Guarantees*}
 
-lemma (in Extend) project_act_Restrict_subset_project_act:
+lemma project_act_Restrict_subset_project_act:
      "project_act h (Restrict C act) \<subseteq> project_act h act"
 apply (auto simp add: project_act_def)
 done
                                            
                                                            
-lemma (in Extend) subset_closed_ok_extend_imp_ok_project:
+lemma subset_closed_ok_extend_imp_ok_project:
      "[| extend h F ok G; subset_closed (AllowedActs F) |]  
       ==> F ok project h C G"
 apply (auto simp add: ok_def)
@@ -584,7 +592,7 @@
 
 (*The raw version; 3rd premise could be weakened by adding the
   precondition extend h F\<squnion>G \<in> X' *)
-lemma (in Extend) project_guarantees_raw:
+lemma project_guarantees_raw:
  assumes xguary:  "F \<in> X guarantees Y"
      and closed:  "subset_closed (AllowedActs F)"
      and project: "!!G. extend h F\<squnion>G \<in> X' 
@@ -597,7 +605,7 @@
 apply (erule project)
 done
 
-lemma (in Extend) project_guarantees:
+lemma project_guarantees:
      "[| F \<in> X guarantees Y;  subset_closed (AllowedActs F);  
          projecting C h F X' X;  extending C h F Y' Y |]  
       ==> extend h F \<in> X' guarantees Y'"
@@ -614,7 +622,7 @@
 
 subsubsection{*Some could be deleted: the required versions are easy to prove*}
 
-lemma (in Extend) extend_guar_increasing:
+lemma extend_guar_increasing:
      "[| F \<in> UNIV guarantees increasing func;   
          subset_closed (AllowedActs F) |]  
       ==> extend h F \<in> X' guarantees increasing (func o f)"
@@ -623,7 +631,7 @@
 apply (rule_tac [2] projecting_UNIV, auto)
 done
 
-lemma (in Extend) extend_guar_Increasing:
+lemma extend_guar_Increasing:
      "[| F \<in> UNIV guarantees Increasing func;   
          subset_closed (AllowedActs F) |]  
       ==> extend h F \<in> X' guarantees Increasing (func o f)"
@@ -632,7 +640,7 @@
 apply (rule_tac [2] projecting_UNIV, auto)
 done
 
-lemma (in Extend) extend_guar_Always:
+lemma extend_guar_Always:
      "[| F \<in> Always A guarantees Always B;   
          subset_closed (AllowedActs F) |]  
       ==> extend h F                    
@@ -645,26 +653,26 @@
 
 subsubsection{*Guarantees with a leadsTo postcondition*}
 
-lemma (in Extend) project_leadsTo_D:
+lemma project_leadsTo_D:
      "F\<squnion>project h UNIV G \<in> A leadsTo B
       ==> extend h F\<squnion>G \<in> (extend_set h A) leadsTo (extend_set h B)"
 apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto)
 done
 
-lemma (in Extend) project_LeadsTo_D:
+lemma project_LeadsTo_D:
      "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A LeadsTo B   
        ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
 apply (rule refl [THEN Join_project_LeadsTo], auto)
 done
 
-lemma (in Extend) extending_leadsTo: 
+lemma extending_leadsTo: 
      "extending (%G. UNIV) h F  
                 (extend_set h A leadsTo extend_set h B) (A leadsTo B)"
 apply (unfold extending_def)
 apply (blast intro: project_leadsTo_D)
 done
 
-lemma (in Extend) extending_LeadsTo: 
+lemma extending_LeadsTo: 
      "extending (%G. reachable (extend h F\<squnion>G)) h F  
                 (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
 apply (unfold extending_def)
@@ -672,3 +680,5 @@
 done
 
 end
+
+end
diff -r 6d2a2f0e904e -r e0cd5c4df8e6 src/HOL/UNITY/Simple/Lift.thy
--- a/src/HOL/UNITY/Simple/Lift.thy	Tue Mar 13 22:49:02 2012 +0100
+++ b/src/HOL/UNITY/Simple/Lift.thy	Tue Mar 13 23:33:35 2012 +0100
@@ -303,26 +303,29 @@
 
 lemmas linorder_leI = linorder_not_less [THEN iffD1]
 
-lemmas (in Floor) le_MinD = Min_le_n [THEN order_antisym]
-              and Max_leD = n_le_Max [THEN [2] order_antisym]
+context Floor
+begin
 
-declare (in Floor) le_MinD [dest!]
-               and linorder_leI [THEN le_MinD, dest!]
-               and Max_leD [dest!]
-               and linorder_leI [THEN Max_leD, dest!]
+lemmas le_MinD = Min_le_n [THEN order_antisym]
+  and Max_leD = n_le_Max [THEN [2] order_antisym]
+
+declare le_MinD [dest!]
+  and linorder_leI [THEN le_MinD, dest!]
+  and Max_leD [dest!]
+  and linorder_leI [THEN Max_leD, dest!]
 
 
 (*lem_lift_2_0 
   NOT an ensures_tac property, but a mere inclusion
   don't know why script lift_2.uni says ENSURES*)
-lemma (in Floor) E_thm05c: 
+lemma E_thm05c: 
     "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
              LeadsTo ((closed \<inter> goingup \<inter> Req n)  \<union> 
                       (closed \<inter> goingdown \<inter> Req n))"
 by (auto intro!: subset_imp_LeadsTo simp add: linorder_neq_iff)
 
 (*lift_2*)
-lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
+lemma lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
              LeadsTo (moving \<inter> Req n)"
 apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])
 apply (unfold Lift_def) 
@@ -337,7 +340,7 @@
 
 
 (*lem_lift_4_1 *)
-lemma (in Floor) E_thm12a:
+lemma E_thm12a:
      "0 < N ==>  
       Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
               {s. floor s \<notin> req s} \<inter> {s. up s})    
@@ -352,7 +355,7 @@
 
 
 (*lem_lift_4_3 *)
-lemma (in Floor) E_thm12b: "0 < N ==>  
+lemma E_thm12b: "0 < N ==>  
       Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
               {s. floor s \<notin> req s} - {s. up s})    
              LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
@@ -364,7 +367,7 @@
 done
 
 (*lift_4*)
-lemma (in Floor) lift_4:
+lemma lift_4:
      "0<N ==> Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
                             {s. floor s \<notin> req s}) LeadsTo      
                            (moving \<inter> Req n \<inter> {s. metric n s < N})"
@@ -376,7 +379,7 @@
 (** towards lift_5 **)
 
 (*lem_lift_5_3*)
-lemma (in Floor) E_thm16a: "0<N    
+lemma E_thm16a: "0<N    
   ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingup) LeadsTo  
              (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (cut_tac bounded)
@@ -386,7 +389,7 @@
 
 
 (*lem_lift_5_1 has ~goingup instead of goingdown*)
-lemma (in Floor) E_thm16b: "0<N ==>    
+lemma E_thm16b: "0<N ==>    
       Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingdown) LeadsTo  
                    (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (cut_tac bounded)
@@ -397,13 +400,13 @@
 
 (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
   i.e. the trivial disjunction, leading to an asymmetrical proof.*)
-lemma (in Floor) E_thm16c:
+lemma E_thm16c:
      "0<N ==> Req n \<inter> {s. metric n s = N} \<subseteq> goingup \<union> goingdown"
 by (force simp add: metric_def)
 
 
 (*lift_5*)
-lemma (in Floor) lift_5:
+lemma lift_5:
      "0<N ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N}) LeadsTo    
                      (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
@@ -415,20 +418,20 @@
 (** towards lift_3 **)
 
 (*lemma used to prove lem_lift_3_1*)
-lemma (in Floor) metric_eq_0D [dest]:
+lemma metric_eq_0D [dest]:
      "[| metric n s = 0;  Min \<le> floor s;  floor s \<le> Max |] ==> floor s = n"
 by (force simp add: metric_def)
 
 
 (*lem_lift_3_1*)
-lemma (in Floor) E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo    
+lemma E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo    
                        (stopped \<inter> atFloor n)"
 apply (cut_tac bounded)
 apply (unfold Lift_def, ensures_tac "request_act", auto)
 done
 
 (*lem_lift_3_5*)
-lemma (in Floor) E_thm13: 
+lemma E_thm13: 
   "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
   LeadsTo (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})"
 apply (unfold Lift_def, ensures_tac "request_act")
@@ -436,7 +439,7 @@
 done
 
 (*lem_lift_3_6*)
-lemma (in Floor) E_thm14: "0 < N ==>  
+lemma E_thm14: "0 < N ==>  
       Lift \<in>  
         (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
         LeadsTo (opened \<inter> Req n \<inter> {s. metric n s = N})"
@@ -445,7 +448,7 @@
 done
 
 (*lem_lift_3_7*)
-lemma (in Floor) E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N})   
+lemma E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N})   
              LeadsTo (closed \<inter> Req n \<inter> {s. metric n s = N})"
 apply (unfold Lift_def, ensures_tac "close_act")
 apply (auto simp add: metric_def)
@@ -454,7 +457,7 @@
 
 (** the final steps **)
 
-lemma (in Floor) lift_3_Req: "0 < N ==>  
+lemma lift_3_Req: "0 < N ==>  
       Lift \<in>  
         (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})    
         LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
@@ -463,15 +466,14 @@
 
 
 (*Now we observe that our integer metric is really a natural number*)
-lemma (in Floor) Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}"
+lemma Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}"
 apply (rule bounded [THEN Always_weaken])
 apply (auto simp add: metric_def)
 done
 
-lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]
+lemmas R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]
 
-lemma (in Floor) lift_3:
-     "Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)"
+lemma lift_3: "Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)"
 apply (rule Always_nonneg [THEN integ_0_le_induct])
 apply (case_tac "0 < z")
 (*If z \<le> 0 then actually z = 0*)
@@ -482,7 +484,7 @@
 done
 
 
-lemma (in Floor) lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)"
+lemma lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)"
 apply (rule LeadsTo_Trans)
  prefer 2
  apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])
@@ -496,5 +498,6 @@
 apply (case_tac "open x", auto)
 done
 
+end
 
 end
diff -r 6d2a2f0e904e -r e0cd5c4df8e6 src/HOL/UNITY/Simple/Token.thy
--- a/src/HOL/UNITY/Simple/Token.thy	Tue Mar 13 22:49:02 2012 +0100
+++ b/src/HOL/UNITY/Simple/Token.thy	Tue Mar 13 23:33:35 2012 +0100
@@ -59,7 +59,10 @@
 apply (cases "proc s i", auto)
 done
 
-lemma (in Token) token_stable: "F \<in> stable (-(E i) \<union> (HasTok i))"
+context Token
+begin
+
+lemma token_stable: "F \<in> stable (-(E i) \<union> (HasTok i))"
 apply (unfold stable_def)
 apply (rule constrains_weaken)
 apply (rule constrains_Un [OF constrains_Un [OF TR2 TR4] TR5])
@@ -70,12 +73,12 @@
 
 subsection{*Progress under Weak Fairness*}
 
-lemma (in Token) wf_nodeOrder: "wf(nodeOrder j)"
+lemma wf_nodeOrder: "wf(nodeOrder j)"
 apply (unfold nodeOrder_def)
 apply (rule wf_measure [THEN wf_subset], blast)
 done
 
-lemma (in Token) nodeOrder_eq: 
+lemma nodeOrder_eq: 
      "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
 apply (unfold nodeOrder_def next_def)
 apply (auto simp add: mod_Suc mod_geq)
@@ -84,7 +87,7 @@
 
 text{*From "A Logic for Concurrent Programming", but not used in Chapter 4.
   Note the use of @{text cases}.  Reasoning about leadsTo takes practice!*}
-lemma (in Token) TR7_nodeOrder:
+lemma TR7_nodeOrder:
      "[| i<N; j<N |] ==>    
       F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
 apply (cases "i=j")
@@ -95,19 +98,19 @@
 
 
 text{*Chapter 4 variant, the one actually used below.*}
-lemma (in Token) TR7_aux: "[| i<N; j<N; i\<noteq>j |]     
+lemma TR7_aux: "[| i<N; j<N; i\<noteq>j |]     
       ==> F \<in> (HasTok i) leadsTo {s. (token s, i) \<in> nodeOrder j}"
 apply (rule TR7 [THEN leadsTo_weaken_R])
 apply (auto simp add: HasTok_def nodeOrder_eq)
 done
 
-lemma (in Token) token_lemma:
+lemma token_lemma:
      "({s. token s < N} \<inter> token -` {m}) = (if m<N then token -` {m} else {})"
 by auto
 
 
 text{*Misra's TR9: the token reaches an arbitrary node*}
-lemma  (in Token) leadsTo_j: "j<N ==> F \<in> {s. token s < N} leadsTo (HasTok j)"
+lemma leadsTo_j: "j<N ==> F \<in> {s. token s < N} leadsTo (HasTok j)"
 apply (rule leadsTo_weaken_R)
 apply (rule_tac I = "-{j}" and f = token and B = "{}" 
        in wf_nodeOrder [THEN bounded_induct])
@@ -119,12 +122,13 @@
 done
 
 text{*Misra's TR8: a hungry process eventually eats*}
-lemma (in Token) token_progress:
+lemma token_progress:
      "j<N ==> F \<in> ({s. token s < N} \<inter> H j) leadsTo (E j)"
 apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])
 apply (rule_tac [2] TR6)
 apply (rule psp [OF leadsTo_j TR3, THEN leadsTo_weaken], blast+)
 done
 
+end
 
 end