# HG changeset patch # User paulson # Date 1117712828 -7200 # Node ID 80617b8d33c53f7d467a7af6dfed1fd6a0ef61f0 # Parent 052d9aba392d61c1b3e29e8d76a8defba68b4fb9 renamed "constrains" to "safety" to avoid keyword clash diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/Comp/Client.thy --- 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 \ 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 \ stable {s. rel s \ 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 \ Increasing giv; G \ 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 \ 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 \ stable {s. size (rel s) \ 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: diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/Comp/Counter.thy --- 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 \ stable {s. s C = s (c i) + k}" -by (simp add: Component_def, constrains) +by (simp add: Component_def, safety) lemma p3: "Component i \ stable {s. \v. v\c i & v\C --> s v = k v}" -by (simp add: Component_def, constrains) +by (simp add: Component_def, safety) lemma p2_p3_lemma1: diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/Comp/Counterc.thy --- 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 \ 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\I |] diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/Comp/Handshake.thy --- 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}" diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/Comp/Priority.thy --- 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 \ 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 \ 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 \ stable {s. \j k. j\i & k\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 \ 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 \ {s. s = q} co {s. s=q} Un {s. \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 \ -Highest i Int {s. j\above i s} co {s. j\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 @@ "\i. system \ 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 diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/Comp/Progress.thy --- 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\GG \ (atLeast 0 \ 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 diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/Comp/TimerArray.thy --- 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 diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/Simple/Lift.thy --- 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 \ Max" constdefs - (** Abbreviations: the "always" part **) + --{*Abbreviations: the "always" part*} above :: "state set" "above == {s. \i. floor s < i & i \ Max & i \ 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 \ 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'). \n. s' = s (|req := insert n (req s)|) & Min \ n & n \ 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 \ floor s & floor s \ Max}" @@ -197,37 +202,37 @@ lemma open_stop: "Lift \ Always open_stop" apply (rule AlwaysI, force) -apply (unfold Lift_def, constrains) +apply (unfold Lift_def, safety) done lemma stop_floor: "Lift \ 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 \ 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 \ 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 \ 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 \ 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 \ (stopped \ atFloor n) LeadsTo (opened \ atFloor n)" diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/Simple/Mutex.thy --- 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 \ Always IU" apply (rule AlwaysI, force) -apply (unfold Mutex_def, constrains) +apply (unfold Mutex_def, safety) done lemma IV: "Mutex \ 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 \ 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 \ {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 \ {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 \ {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 \ {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}" by (unfold Mutex_def, ensures_tac "V1") diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/Simple/Reach.thy --- 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 \ Always reach_invariant" apply (rule AlwaysI, force) -apply (unfold Rprg_def, constrains) +apply (unfold Rprg_def, safety) apply (blast intro: rtrancl_trans) done diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/UNITY.thy --- 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. \act \ Acts F. act``A \ 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') \ act; s \ A |] ==> s': A') @@ -161,7 +161,7 @@ "[| F \ A co A'; B \ A; A'<=B' |] ==> F \ B co B'" by (unfold constrains_def, blast) -(** Union **) +subsubsection{*Union*} lemma constrains_Un: "[| F \ A co A'; F \ B co B' |] ==> F \ (A \ B) co (A' \ B')" @@ -184,7 +184,7 @@ lemma constrains_INT_distrib: "A co (\i \ I. B i) = (\i \ I. A co B i)" by (unfold constrains_def, blast) -(** Intersection **) +subsubsection{*Intersection*} lemma constrains_Int: "[| F \ A co A'; F \ B co B' |] ==> F \ (A \ B) co (A' \ B')" @@ -209,7 +209,7 @@ by (unfold constrains_def, clarify, blast) -(*** unless ***) +subsubsection{*unless*} lemma unlessI: "F \ (A-B) co (A \ B) ==> F \ A unless B" by (unfold unless_def, assumption) @@ -218,7 +218,7 @@ by (unfold unless_def, assumption) -(*** stable ***) +subsubsection{*stable*} lemma stableI: "F \ A co A ==> F \ 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 \ stable A; F \ stable A' |] ==> F \ stable (A \ A')" @@ -248,7 +248,7 @@ "(!!A. A \ X ==> F \ stable A) ==> F \ stable (\X)" by (unfold stable_def constrains_def, blast) -(** Intersection **) +subsubsection{*Intersection*} lemma stable_Int: "[| F \ stable A; F \ stable A' |] ==> F \ stable (A \ A')" @@ -278,7 +278,7 @@ lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI, standard] -(*** invariant ***) +subsubsection{*invariant*} lemma invariantI: "[| Init F \ A; F \ stable A |] ==> F \ 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 \ increasing f ==> F \ stable {s. z \ f s}" @@ -327,7 +327,7 @@ -(*** Theoretical Results from Section 6 ***) +subsubsection{*Theoretical Results from Section 6*} lemma constrains_strongest_rhs: "F \ 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 \ B - (A - B) = B" by blast @@ -346,7 +346,7 @@ lemma Int_Union_Union: "Union(B) \ A = Union((%C. C \ 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 \ A) = (x \ 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" diff -r 052d9aba392d -r 80617b8d33c5 src/HOL/UNITY/UNITY_Main.thy --- 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)) *}