--- a/src/ZF/UNITY/AllocImpl.thy Thu Jun 02 09:17:38 2005 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy Thu Jun 02 13:17:06 2005 +0200
@@ -89,7 +89,7 @@
"alloc_prog \<in> (\<Inter>x \<in> var-{giv, available_tok, NbR}. preserves(lift(x)))"
apply (rule Inter_var_DiffI, force)
apply (rule ballI)
-apply (rule preservesI, constrains)
+apply (rule preservesI, safety)
done
(* As a special case of the rule above *)
@@ -129,7 +129,7 @@
(** Safety property: (28) **)
lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))"
-apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed, constrains+)
+apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed, safety+)
apply (auto dest: ActsD)
apply (drule_tac f = "lift (giv) " in preserves_imp_eq)
apply auto
@@ -139,7 +139,7 @@
"alloc_prog \<in> stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
{s\<in>state. s`available_tok #+ tokens(s`giv) =
NbT #+ tokens(take(s`NbR, s`rel))})"
-apply constrains
+apply safety
apply auto
apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse)
apply (simp (no_asm_simp) add: take_succ)
@@ -209,7 +209,7 @@
prefer 2 apply (simp add: alloc_prog_ok_iff)
apply (rule_tac P = "%x y. <x,y> \<in> prefix(tokbag)" and A = "list(nat)"
in stable_Join_Stable)
-apply constrains
+apply safety
prefer 2 apply (simp add: lift_def, clarify)
apply (drule_tac a = k in Increasing_imp_Stable, auto)
done
@@ -239,7 +239,7 @@
lemma alloc_prog_rel_Stable_NbR_lemma:
"[| G \<in> program; alloc_prog ok G; k\<in>nat |]
==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
-apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains, auto)
+apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety, auto)
apply (blast intro: le_trans leI)
apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing)
apply (drule_tac [2] g = succ in imp_increasing_comp)
@@ -363,7 +363,7 @@
lemma alloc_prog_giv_Stable_lemma:
"[| G \<in> program; alloc_prog ok G; k\<in>nat |]
==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
-apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains)
+apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety)
apply (auto intro: leI)
apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp)
apply (drule_tac f = "length comp lift (giv)" and A = nat and r = Le in preserves_imp_increasing)
--- a/src/ZF/UNITY/ClientImpl.thy Thu Jun 02 09:17:38 2005 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy Thu Jun 02 13:17:06 2005 +0200
@@ -115,7 +115,7 @@
"client_prog:(\<Inter>x \<in> var-{ask, rel, tok}. preserves(lift(x)))"
apply (rule Inter_var_DiffI, force)
apply (rule ballI)
-apply (rule preservesI, constrains, auto)
+apply (rule preservesI, safety, auto)
done
@@ -136,7 +136,7 @@
apply (unfold guar_def)
apply (auto intro!: increasing_imp_Increasing
simp add: client_prog_ok_iff increasing_def preserves_imp_prefix)
-apply (constrains, force, force)+
+apply (safety, force, force)+
done
declare nth_append [simp] append_one_prefix [simp]
@@ -158,7 +158,7 @@
apply (auto simp add: client_prog_ok_iff)
apply (rule invariantI [THEN stable_Join_Always2], force)
prefer 2
- apply (fast intro: stable_Int preserves_lift_imp_stable, constrains)
+ apply (fast intro: stable_Int preserves_lift_imp_stable, safety)
apply (auto dest: ActsD)
apply (cut_tac NbT_pos)
apply (rule NbT_pos2 [THEN mod_less_divisor])
@@ -178,7 +178,7 @@
lemma client_prog_stable_rel_le_giv:
"client_prog \<in> stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
-by (constrains, auto)
+by (safety, auto)
lemma client_prog_Join_Stable_rel_le_giv:
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]
--- a/src/ZF/UNITY/Constrains.thy Thu Jun 02 09:17:38 2005 +0200
+++ b/src/ZF/UNITY/Constrains.thy Thu Jun 02 13:17:06 2005 +0200
@@ -564,7 +564,7 @@
rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;
*}
-method_setup constrains = {*
+method_setup safety = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
--- a/src/ZF/UNITY/Mutex.thy Thu Jun 02 09:17:38 2005 +0200
+++ b/src/ZF/UNITY/Mutex.thy Thu Jun 02 13:17:06 2005 +0200
@@ -148,13 +148,6 @@
by (simp add: Mutex_def)
-method_setup constrains = {*
- Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
- "for proving safety properties"
-
-
declare Mutex_def [THEN def_prg_Init, simp]
ML
{*
@@ -191,12 +184,12 @@
lemma IU: "Mutex \<in> Always(IU)"
apply (rule AlwaysI, force)
-apply (unfold Mutex_def, constrains, auto)
+apply (unfold Mutex_def, safety, auto)
done
lemma IV: "Mutex \<in> Always(IV)"
apply (rule AlwaysI, force)
-apply (unfold Mutex_def, constrains)
+apply (unfold Mutex_def, safety)
done
(*The safety property: mutual exclusion*)
@@ -214,7 +207,7 @@
lemma "Mutex \<in> Always(bad_IU)"
apply (rule AlwaysI, force)
-apply (unfold Mutex_def, constrains, auto)
+apply (unfold Mutex_def, safety, auto)
apply (subgoal_tac "#1 $<= #3")
apply (drule_tac x = "#1" and y = "#3" in zle_trans, auto)
apply (simp (no_asm) add: not_zless_iff_zle [THEN iff_sym])
@@ -229,7 +222,7 @@
(*** Progress for U ***)
lemma U_F0: "Mutex \<in> {s \<in> state. s`m=#2} Unless {s \<in> state. s`m=#3}"
-by (unfold Unless_def Mutex_def, constrains)
+by (unfold Unless_def Mutex_def, safety)
lemma U_F1:
"Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}"
@@ -281,7 +274,7 @@
(*** Progress for V ***)
lemma V_F0: "Mutex \<in> {s \<in> state. s`n=#2} Unless {s \<in> state. s`n=#3}"
-by (unfold Unless_def Mutex_def, constrains)
+by (unfold Unless_def Mutex_def, safety)
lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} LeadsTo {s \<in> state. s`p = not(s`u) & s`n = #2}"
by (unfold Mutex_def, ensures_tac "V1")
--- a/src/ZF/UNITY/UNITY.thy Thu Jun 02 09:17:38 2005 +0200
+++ b/src/ZF/UNITY/UNITY.thy Thu Jun 02 13:17:06 2005 +0200
@@ -2,19 +2,20 @@
ID: $Id$
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
-
-The basic UNITY theory (revised version, based upon the "co" operator)
-From Misra, "A Logic for Concurrent Programming", 1994
-
-Theory ported from HOL.
*)
header {*The Basic UNITY Theory*}
theory UNITY = State:
+
+text{*The basic UNITY theory (revised version, based upon the "co" operator)
+From Misra, "A Logic for Concurrent Programming", 1994.
+
+This ZF theory was ported from its HOL equivalent.*}
+
consts
- constrains :: "[i, i] => i" (infixl "co" 60)
- op_unless :: "[i, i] => i" (infixl "unless" 60)
+ "constrains" :: "[i, i] => i" (infixl "co" 60)
+ op_unless :: "[i, i] => i" (infixl "unless" 60)
constdefs
program :: i
@@ -86,7 +87,7 @@
unless_def: "A unless B == (A - B) co (A Un B)"
-(** SKIP **)
+text{*SKIP*}
lemma SKIP_in_program [iff,TC]: "SKIP \<in> program"
by (force simp add: SKIP_def program_def mk_program_def)
@@ -100,7 +101,7 @@
lemma programify_in_program [iff,TC]: "programify(F) \<in> program"
by (force simp add: programify_def)
-(** Collapsing rules: to remove programify from expressions **)
+text{*Collapsing rules: to remove programify from expressions*}
lemma programify_idem [simp]: "programify(programify(F))=programify(F)"
by (force simp add: programify_def)
@@ -164,7 +165,7 @@
lemma AllowedActs_type: "AllowedActs(F) \<subseteq> Pow(state*state)"
by (simp add: RawAllowedActs_type AllowedActs_def)
-(* Needed in Behaviors *)
+text{*Needed in Behaviors*}
lemma ActsD: "[| act \<in> Acts(F); <s,s'> \<in> act |] ==> s \<in> state & s' \<in> state"
by (blast dest: Acts_type [THEN subsetD])
@@ -213,7 +214,7 @@
by (cut_tac F = F in AllowedActs_type, blast)
-subsubsection{*The Opoerator @{term mk_program}*}
+subsubsection{*The Operator @{term mk_program}*}
lemma mk_program_in_program [iff,TC]:
"mk_program(init, acts, allowed) \<in> program"
@@ -246,7 +247,7 @@
cons(id(state), allowed \<inter> Pow(state*state))"
by (simp add: AllowedActs_def)
-(**Init, Acts, and AlowedActs of SKIP **)
+text{*Init, Acts, and AlowedActs of SKIP *}
lemma RawInit_SKIP [simp]: "RawInit(SKIP) = state"
by (simp add: SKIP_def)
@@ -266,7 +267,7 @@
lemma AllowedActs_SKIP [simp]: "AllowedActs(SKIP) = Pow(state*state)"
by (force simp add: SKIP_def)
-(** Equality of UNITY programs **)
+text{*Equality of UNITY programs*}
lemma raw_surjective_mk_program:
"F \<in> program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F"
@@ -323,13 +324,13 @@
by auto
-(*An action is expanded only if a pair of states is being tested against it*)
+text{*An action is expanded only if a pair of states is being tested against it*}
lemma def_act_simp:
"[| act == {<s,s'> \<in> A*B. P(s, s')} |]
==> (<s,s'> \<in> act) <-> (<s,s'> \<in> A*B & P(s, s'))"
by auto
-(*A set is expanded only if an element is being tested against it*)
+text{*A set is expanded only if an element is being tested against it*}
lemma def_set_simp: "A == B ==> (x \<in> A) <-> (x \<in> B)"
by auto
@@ -367,13 +368,13 @@
apply (force simp add: constrains_def st_set_def)
done
-(*monotonic in 2nd argument*)
+text{*monotonic in 2nd argument*}
lemma constrains_weaken_R:
"[| F \<in> A co A'; A'\<subseteq>B' |] ==> F \<in> A co B'"
apply (unfold constrains_def, blast)
done
-(*anti-monotonic in 1st argument*)
+text{*anti-monotonic in 1st argument*}
lemma constrains_weaken_L:
"[| F \<in> A co A'; B\<subseteq>A |] ==> F \<in> B co A'"
apply (unfold constrains_def st_set_def, blast)
@@ -439,8 +440,8 @@
"[| F \<in> A co A' |] ==> A \<subseteq> A'"
by (unfold constrains_def st_set_def, force)
-(*The reasoning is by subsets since "co" refers to single actions
- only. So this rule isn't that useful.*)
+text{*The reasoning is by subsets since "co" refers to single actions
+ only. So this rule isn't that useful.*}
lemma constrains_trans: "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
by (unfold constrains_def st_set_def, auto, blast)
@@ -583,13 +584,13 @@
Should the premise be !!m instead of \<forall>m ? Would make it harder
to use in forward proof. **)
-(* The general case easier to prove that le special case! *)
+text{*The general case is easier to prove than the special case!*}
lemma "elimination":
"[| \<forall>m \<in> M. F \<in> {s \<in> A. x(s) = m} co B(m); F \<in> program |]
==> F \<in> {s \<in> A. x(s) \<in> M} co (\<Union>m \<in> M. B(m))"
by (auto simp add: constrains_def st_set_def, blast)
-(* As above, but for the special case of A=state *)
+text{*As above, but for the special case of A=state*}
lemma elimination2:
"[| \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} co B(m); F \<in> program |]
==> F:{s \<in> state. x(s) \<in> M} co (\<Union>m \<in> M. B(m))"