--- 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*}
--- 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*}
--- 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
--- 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
--- 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
--- 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
--- 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