--- a/src/HOL/UNITY/Comp/Client.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Comp/Client.thy Thu Jun 02 13:47:08 2005 +0200
@@ -83,7 +83,7 @@
"Client \<in> UNIV guarantees Increasing ask Int Increasing rel"
apply (auto intro!: increasing_imp_Increasing simp add: guar_def preserves_subset_increasing [THEN subsetD])
apply (auto simp add: Client_def increasing_def)
-apply (constrains, auto)+
+apply (safety, auto)+
done
declare nth_append [simp] append_one_prefix [simp]
@@ -101,7 +101,7 @@
apply (rule invariantI [THEN stable_Join_Always2], force)
prefer 2
apply (fast elim!: preserves_subset_stable [THEN subsetD] intro!: stable_Int)
-apply (simp add: Client_def, constrains)
+apply (simp add: Client_def, safety)
apply (cut_tac m = "tok s" in NbT_pos [THEN mod_less_divisor], auto)
done
@@ -118,7 +118,7 @@
text{*** Towards proving the liveness property ***}
lemma stable_rel_le_giv: "Client \<in> stable {s. rel s \<le> giv s}"
-by (simp add: Client_def, constrains, auto)
+by (simp add: Client_def, safety, auto)
lemma Join_Stable_rel_le_giv:
"[| Client Join G \<in> Increasing giv; G \<in> preserves rel |]
@@ -197,14 +197,14 @@
text{*This shows that the Client won't alter other variables in any state
that it is combined with*}
lemma client_preserves_dummy: "Client \<in> preserves dummy"
-by (simp add: Client_def preserves_def, clarify, constrains, auto)
+by (simp add: Client_def preserves_def, clarify, safety, auto)
text{** Obsolete lemmas from first version of the Client **}
lemma stable_size_rel_le_giv:
"Client \<in> stable {s. size (rel s) \<le> size (giv s)}"
-by (simp add: Client_def, constrains, auto)
+by (simp add: Client_def, safety, auto)
text{*clients return the right number of tokens*}
lemma ok_guar_rel_prefix_giv:
--- a/src/HOL/UNITY/Comp/Counter.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Comp/Counter.thy Thu Jun 02 13:47:08 2005 +0200
@@ -84,10 +84,10 @@
(* Correctness proofs for Components *)
(* p2 and p3 proofs *)
lemma p2: "Component i \<in> stable {s. s C = s (c i) + k}"
-by (simp add: Component_def, constrains)
+by (simp add: Component_def, safety)
lemma p3: "Component i \<in> stable {s. \<forall>v. v\<noteq>c i & v\<noteq>C --> s v = k v}"
-by (simp add: Component_def, constrains)
+by (simp add: Component_def, safety)
lemma p2_p3_lemma1:
--- a/src/HOL/UNITY/Comp/Counterc.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.thy Thu Jun 02 13:47:08 2005 +0200
@@ -87,7 +87,7 @@
lemma p2: "Component i \<in> stable {s. C s = (c s) i + k}"
-by (simp add: Component_def, constrains)
+by (simp add: Component_def, safety)
lemma p3:
"[| OK I Component; i\<in>I |]
--- a/src/HOL/UNITY/Comp/Handshake.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Comp/Handshake.thy Thu Jun 02 13:47:08 2005 +0200
@@ -49,14 +49,14 @@
apply force
apply (rule constrains_imp_Constrains [THEN StableI])
apply auto
- apply (unfold F_def, constrains)
-apply (unfold G_def, constrains)
+ apply (unfold F_def, safety)
+apply (unfold G_def, safety)
done
lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo
({s. NF s = k} Int {s. BB s})"
apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
- apply (unfold F_def, constrains)
+ apply (unfold F_def, safety)
apply (unfold G_def, ensures_tac "cmdG")
done
@@ -64,7 +64,7 @@
{s. k < NF s}"
apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
apply (unfold F_def, ensures_tac "cmdF")
-apply (unfold G_def, constrains)
+apply (unfold G_def, safety)
done
lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}"
--- a/src/HOL/UNITY/Comp/Priority.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy Thu Jun 02 13:47:08 2005 +0200
@@ -84,11 +84,11 @@
text{* neighbors is stable *}
lemma Component_neighbors_stable: "Component i \<in> stable {s. neighbors k s = n}"
-by (simp add: Component_def, constrains, auto)
+by (simp add: Component_def, safety, auto)
text{* property 4 *}
lemma Component_waits_priority: "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}"
-by (simp add: Component_def, constrains)
+by (simp add: Component_def, safety)
text{* property 5: charpentier and Chandy mistakenly express it as
'transient Highest i'. Consider the case where i has neighbors *}
@@ -107,11 +107,11 @@
text{* property 6: Component doesn't introduce cycle *}
lemma Component_well_behaves: "Component i \<in> Highest i co Highest i Un Lowest i"
-by (simp add: Component_def, constrains, fast)
+by (simp add: Component_def, safety, fast)
text{* property 7: local axiom *}
lemma locality: "Component i \<in> stable {s. \<forall>j k. j\<noteq>i & k\<noteq>i--> ((j,k):s) = b j k}"
-by (simp add: Component_def, constrains)
+by (simp add: Component_def, safety)
subsection{*System properties*}
@@ -120,12 +120,12 @@
lemma Safety: "system \<in> stable Safety"
apply (unfold Safety_def)
apply (rule stable_INT)
-apply (simp add: system_def, constrains, fast)
+apply (simp add: system_def, safety, fast)
done
text{* property 13: universal *}
lemma p13: "system \<in> {s. s = q} co {s. s=q} Un {s. \<exists>i. derive i q s}"
-by (simp add: system_def Component_def mk_total_program_def totalize_JN, constrains, blast)
+by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, blast)
text{* property 14: the 'above set' of a Component that hasn't got
priority doesn't increase *}
@@ -133,7 +133,7 @@
"system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}"
apply (insert reach_lemma [of concl: j])
apply (simp add: system_def Component_def mk_total_program_def totalize_JN,
- constrains)
+ safety)
apply (simp add: trancl_converse, blast)
done
@@ -150,7 +150,7 @@
"\<forall>i. system \<in> Highest i co Highest i Un Lowest i"
apply clarify
apply (simp add: system_def Component_def mk_total_program_def totalize_JN,
- constrains, auto)
+ safety, auto)
done
--- a/src/HOL/UNITY/Comp/Progress.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Comp/Progress.thy Thu Jun 02 13:47:08 2005 +0200
@@ -93,8 +93,8 @@
apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
apply simp
apply (rule_tac T = "atLeast 0" in leadsTo_Join)
- apply (simp add: awp_iff FF_def, constrains)
- apply (simp add: awp_iff GG_def wens_set_FF, constrains)
+ apply (simp add: awp_iff FF_def, safety)
+ apply (simp add: awp_iff GG_def wens_set_FF, safety)
apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp)
done
--- a/src/HOL/UNITY/Comp/TimerArray.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Comp/TimerArray.thy Thu Jun 02 13:47:08 2005 +0200
@@ -35,7 +35,7 @@
lemma Timer_preserves_snd [iff]: "Timer : preserves snd"
apply (rule preservesI)
-apply (unfold Timer_def, constrains)
+apply (unfold Timer_def, safety)
done
@@ -49,7 +49,7 @@
apply auto
(*Safety property, already reduced to the single Timer case*)
prefer 2
- apply (simp add: Timer_def, constrains)
+ apply (simp add: Timer_def, safety)
(*Progress property for the array of Timers*)
apply (rule_tac f = "sub i o fst" in lessThan_induct)
apply (case_tac "m")
@@ -61,7 +61,7 @@
apply (rename_tac "n")
apply (rule PLam_leadsTo_Basis)
apply (auto simp add: lessThan_Suc [symmetric])
-apply (unfold Timer_def mk_total_program_def, constrains)
+apply (unfold Timer_def mk_total_program_def, safety)
apply (rule_tac act = decr in totalize_transientI, auto)
done
--- a/src/HOL/UNITY/Simple/Lift.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Simple/Lift.thy Thu Jun 02 13:47:08 2005 +0200
@@ -6,26 +6,29 @@
The Lift-Control Example
*)
-theory Lift = UNITY_Main:
+theory Lift
+imports "../UNITY_Main"
+
+begin
record state =
- floor :: "int" (*current position of the lift*)
- "open" :: "bool" (*whether the door is opened at floor*)
- stop :: "bool" (*whether the lift is stopped at floor*)
- req :: "int set" (*for each floor, whether the lift is requested*)
- up :: "bool" (*current direction of movement*)
- move :: "bool" (*whether moving takes precedence over opening*)
+ floor :: "int" --{*current position of the lift*}
+ "open" :: "bool" --{*whether the door is opened at floor*}
+ stop :: "bool" --{*whether the lift is stopped at floor*}
+ req :: "int set" --{*for each floor, whether the lift is requested*}
+ up :: "bool" --{*current direction of movement*}
+ move :: "bool" --{*whether moving takes precedence over opening*}
consts
- Min :: "int" (*least and greatest floors*)
- Max :: "int" (*least and greatest floors*)
+ Min :: "int" --{*least and greatest floors*}
+ Max :: "int" --{*least and greatest floors*}
axioms
Min_le_Max [iff]: "Min \<le> Max"
constdefs
- (** Abbreviations: the "always" part **)
+ --{*Abbreviations: the "always" part*}
above :: "state set"
"above == {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}"
@@ -45,7 +48,7 @@
ready :: "state set"
"ready == {s. stop s & ~ open s & move s}"
- (** Further abbreviations **)
+ --{*Further abbreviations*}
moving :: "state set"
"moving == {s. ~ stop s & ~ open s}"
@@ -56,7 +59,7 @@
opened :: "state set"
"opened == {s. stop s & open s & move s}"
- closed :: "state set" (*but this is the same as ready!!*)
+ closed :: "state set" --{*but this is the same as ready!!*}
"closed == {s. stop s & ~ open s & move s}"
atFloor :: "int => state set"
@@ -67,7 +70,7 @@
- (** The program **)
+ --{*The program*}
request_act :: "(state*state) set"
"request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
@@ -108,18 +111,20 @@
{(s,s'). s' = s (|floor := floor s - 1|)
& ~ stop s & ~ up s & floor s \<notin> req s}"
- (*This action is omitted from prior treatments, which therefore are
- unrealistic: nobody asks the lift to do anything! But adding this
- action invalidates many of the existing progress arguments: various
- "ensures" properties fail.*)
button_press :: "(state*state) set"
+ --{*This action is omitted from prior treatments, which therefore are
+ unrealistic: nobody asks the lift to do anything! But adding this
+ action invalidates many of the existing progress arguments: various
+ "ensures" properties fail. Maybe it should be constrained to only
+ allow button presses in the current direction of travel, like in a
+ real lift.*}
"button_press ==
{(s,s'). \<exists>n. s' = s (|req := insert n (req s)|)
& Min \<le> n & n \<le> Max}"
Lift :: "state program"
- (*for the moment, we OMIT button_press*)
+ --{*for the moment, we OMIT @{text button_press}*}
"Lift == mk_total_program
({s. floor s = Min & ~ up s & move s & stop s &
~ open s & req s = {}},
@@ -128,7 +133,7 @@
UNIV)"
- (** Invariants **)
+ --{*Invariants*}
bounded :: "state set"
"bounded == {s. Min \<le> floor s & floor s \<le> Max}"
@@ -197,37 +202,37 @@
lemma open_stop: "Lift \<in> Always open_stop"
apply (rule AlwaysI, force)
-apply (unfold Lift_def, constrains)
+apply (unfold Lift_def, safety)
done
lemma stop_floor: "Lift \<in> Always stop_floor"
apply (rule AlwaysI, force)
-apply (unfold Lift_def, constrains)
+apply (unfold Lift_def, safety)
done
(*This one needs open_stop, which was proved above*)
lemma open_move: "Lift \<in> Always open_move"
apply (cut_tac open_stop)
apply (rule AlwaysI, force)
-apply (unfold Lift_def, constrains)
+apply (unfold Lift_def, safety)
done
lemma moving_up: "Lift \<in> Always moving_up"
apply (rule AlwaysI, force)
-apply (unfold Lift_def, constrains)
+apply (unfold Lift_def, safety)
apply (auto dest: order_le_imp_less_or_eq simp add: add1_zle_eq)
done
lemma moving_down: "Lift \<in> Always moving_down"
apply (rule AlwaysI, force)
-apply (unfold Lift_def, constrains)
+apply (unfold Lift_def, safety)
apply (blast dest: order_le_imp_less_or_eq)
done
lemma bounded: "Lift \<in> Always bounded"
apply (cut_tac moving_up moving_down)
apply (rule AlwaysI, force)
-apply (unfold Lift_def, constrains, auto)
+apply (unfold Lift_def, safety, auto)
apply (drule not_mem_distinct, assumption, arith)+
done
@@ -242,7 +247,7 @@
declare Req_def [THEN def_set_simp, simp]
-(** The HUG'93 paper mistakenly omits the Req n from these! **)
+text{*The HUG'93 paper mistakenly omits the Req n from these!*}
(** Lift_1 **)
lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)"
--- a/src/HOL/UNITY/Simple/Mutex.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Simple/Mutex.thy Thu Jun 02 13:47:08 2005 +0200
@@ -94,13 +94,13 @@
lemma IU: "Mutex \<in> Always IU"
apply (rule AlwaysI, force)
-apply (unfold Mutex_def, constrains)
+apply (unfold Mutex_def, safety)
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*)
@@ -113,7 +113,7 @@
(*The bad invariant FAILS in V1*)
lemma "Mutex \<in> Always bad_IU"
apply (rule AlwaysI, force)
-apply (unfold Mutex_def, constrains, auto)
+apply (unfold Mutex_def, safety, auto)
(*Resulting state: n=1, p=false, m=4, u=false.
Execution of V1 (the command of process v guarded by n=1) sets p:=true,
violating the invariant!*)
@@ -127,7 +127,7 @@
(*** Progress for U ***)
lemma U_F0: "Mutex \<in> {s. m s=2} Unless {s. m s=3}"
-by (unfold Unless_def Mutex_def, constrains)
+by (unfold Unless_def Mutex_def, safety)
lemma U_F1: "Mutex \<in> {s. m s=1} LeadsTo {s. p s = v s & m s = 2}"
by (unfold Mutex_def, ensures_tac U1)
@@ -165,7 +165,7 @@
lemma V_F0: "Mutex \<in> {s. n s=2} Unless {s. n s=3}"
-by (unfold Unless_def Mutex_def, constrains)
+by (unfold Unless_def Mutex_def, safety)
lemma V_F1: "Mutex \<in> {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}"
by (unfold Mutex_def, ensures_tac "V1")
--- a/src/HOL/UNITY/Simple/Reach.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy Thu Jun 02 13:47:08 2005 +0200
@@ -62,7 +62,7 @@
lemma reach_invariant: "Rprg \<in> Always reach_invariant"
apply (rule AlwaysI, force)
-apply (unfold Rprg_def, constrains)
+apply (unfold Rprg_def, safety)
apply (blast intro: rtrancl_trans)
done
--- a/src/HOL/UNITY/UNITY.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/UNITY.thy Thu Jun 02 13:47:08 2005 +0200
@@ -21,7 +21,7 @@
Acts :: "'a program => ('a * 'a)set set"
"Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
- constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60)
+ "constrains" :: "['a set, 'a set] => 'a program set" (infixl "co" 60)
"A co B == {F. \<forall>act \<in> Acts F. act``A \<subseteq> B}"
unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60)
@@ -58,7 +58,7 @@
text{*Perhaps equalities.ML shouldn't add this in the first place!*}
declare image_Collect [simp del]
-(*** The abstract type of programs ***)
+subsubsection{*The abstract type of programs*}
lemmas program_typedef =
Rep_Program Rep_Program_inverse Abs_Program_inverse
@@ -83,7 +83,7 @@
lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
by (simp add: insert_absorb Id_in_AllowedActs)
-(** Inspectors for type "program" **)
+subsubsection{*Inspectors for type "program"*}
lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
by (simp add: program_typedef)
@@ -95,7 +95,7 @@
"AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
by (simp add: program_typedef)
-(** Equality for UNITY programs **)
+subsubsection{*Equality for UNITY programs*}
lemma surjective_mk_program [simp]:
"mk_program (Init F, Acts F, AllowedActs F) = F"
@@ -124,7 +124,7 @@
by (blast intro: program_equalityI program_equalityE)
-(*** co ***)
+subsubsection{*co*}
lemma constrainsI:
"(!!act s s'. [| act: Acts F; (s,s') \<in> act; s \<in> A |] ==> s': A')
@@ -161,7 +161,7 @@
"[| F \<in> A co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B co B'"
by (unfold constrains_def, blast)
-(** Union **)
+subsubsection{*Union*}
lemma constrains_Un:
"[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')"
@@ -184,7 +184,7 @@
lemma constrains_INT_distrib: "A co (\<Inter>i \<in> I. B i) = (\<Inter>i \<in> I. A co B i)"
by (unfold constrains_def, blast)
-(** Intersection **)
+subsubsection{*Intersection*}
lemma constrains_Int:
"[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
@@ -209,7 +209,7 @@
by (unfold constrains_def, clarify, blast)
-(*** unless ***)
+subsubsection{*unless*}
lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
by (unfold unless_def, assumption)
@@ -218,7 +218,7 @@
by (unfold unless_def, assumption)
-(*** stable ***)
+subsubsection{*stable*}
lemma stableI: "F \<in> A co A ==> F \<in> stable A"
by (unfold stable_def, assumption)
@@ -229,7 +229,7 @@
lemma stable_UNIV [simp]: "stable UNIV = UNIV"
by (unfold stable_def constrains_def, auto)
-(** Union **)
+subsubsection{*Union*}
lemma stable_Un:
"[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
@@ -248,7 +248,7 @@
"(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Union>X)"
by (unfold stable_def constrains_def, blast)
-(** Intersection **)
+subsubsection{*Intersection*}
lemma stable_Int:
"[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<inter> A')"
@@ -278,7 +278,7 @@
lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI, standard]
-(*** invariant ***)
+subsubsection{*invariant*}
lemma invariantI: "[| Init F \<subseteq> A; F \<in> stable A |] ==> F \<in> invariant A"
by (simp add: invariant_def)
@@ -289,7 +289,7 @@
by (auto simp add: invariant_def stable_Int)
-(*** increasing ***)
+subsubsection{*increasing*}
lemma increasingD:
"F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
@@ -327,7 +327,7 @@
-(*** Theoretical Results from Section 6 ***)
+subsubsection{*Theoretical Results from Section 6*}
lemma constrains_strongest_rhs:
"F \<in> A co (strongest_rhs F A )"
@@ -338,7 +338,7 @@
by (unfold constrains_def strongest_rhs_def, blast)
-(** Ad-hoc set-theory rules **)
+subsubsection{*Ad-hoc set-theory rules*}
lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
by blast
@@ -346,7 +346,7 @@
lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
by blast
-(** Needed for WF reasoning in WFair.ML **)
+text{*Needed for WF reasoning in WFair.ML*}
lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
by blast
@@ -377,7 +377,7 @@
by (blast intro: sym [THEN image_eqI])
-text{*Basic properties*}
+subsubsection{*Basic properties*}
lemma totalize_act_Id [simp]: "totalize_act Id = Id"
by (simp add: totalize_act_def)
@@ -455,7 +455,7 @@
lemma def_set_simp: "A == B ==> (x \<in> A) = (x \<in> B)"
by (simp add: mk_total_program_def)
-(** Inspectors for type "program" **)
+subsubsection{*Inspectors for type "program"*}
lemma Init_total_eq [simp]:
"Init (mk_total_program (init,acts,allowed)) = init"
--- a/src/HOL/UNITY/UNITY_Main.thy Thu Jun 02 13:17:06 2005 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Thu Jun 02 13:47:08 2005 +0200
@@ -9,7 +9,7 @@
theory UNITY_Main = Detects + PPROD + Follows + ProgressSets
files "UNITY_tactics.ML":
-method_setup constrains = {*
+method_setup safety = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}