# HG changeset patch # User paulson # Date 1117711026 -7200 # Node ID 052d9aba392d61c1b3e29e8d76a8defba68b4fb9 # Parent a5c77d298ad7358d444f68d3ad002260ef8fa847 renamed "constrains" to "safety" to avoid keyword clash diff -r a5c77d298ad7 -r 052d9aba392d src/ZF/UNITY/AllocImpl.thy --- 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 \ (\x \ 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 \ 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 \ stable({s\state. s`NbR \ length(s`rel)} \ {s\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. \ 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 \ program; alloc_prog ok G; k\nat |] ==> alloc_prog \ G \ Stable({s\state . k \ 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 \ program; alloc_prog ok G; k\nat |] ==> alloc_prog \ G \ Stable({s\state . k \ 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) diff -r a5c77d298ad7 -r 052d9aba392d src/ZF/UNITY/ClientImpl.thy --- 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:(\x \ 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 \ stable({s \ state. \ prefix(nat)})" -by (constrains, auto) +by (safety, auto) lemma client_prog_Join_Stable_rel_le_giv: "[| client_prog \ G \ Incr(lift(giv)); G \ preserves(lift(rel)) |] diff -r a5c77d298ad7 -r 052d9aba392d src/ZF/UNITY/Constrains.thy --- 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)) *} diff -r a5c77d298ad7 -r 052d9aba392d src/ZF/UNITY/Mutex.thy --- 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 \ Always(IU)" apply (rule AlwaysI, force) -apply (unfold Mutex_def, constrains, auto) +apply (unfold Mutex_def, safety, auto) 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*) @@ -214,7 +207,7 @@ lemma "Mutex \ 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 \ {s \ state. s`m=#2} Unless {s \ state. s`m=#3}" -by (unfold Unless_def Mutex_def, constrains) +by (unfold Unless_def Mutex_def, safety) lemma U_F1: "Mutex \ {s \ state. s`m=#1} LeadsTo {s \ state. s`p = s`v & s`m = #2}" @@ -281,7 +274,7 @@ (*** Progress for V ***) lemma V_F0: "Mutex \ {s \ state. s`n=#2} Unless {s \ state. s`n=#3}" -by (unfold Unless_def Mutex_def, constrains) +by (unfold Unless_def Mutex_def, safety) lemma V_F1: "Mutex \ {s \ state. s`n=#1} LeadsTo {s \ state. s`p = not(s`u) & s`n = #2}" by (unfold Mutex_def, ensures_tac "V1") diff -r a5c77d298ad7 -r 052d9aba392d src/ZF/UNITY/UNITY.thy --- 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 \ program" by (force simp add: SKIP_def program_def mk_program_def) @@ -100,7 +101,7 @@ lemma programify_in_program [iff,TC]: "programify(F) \ 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) \ Pow(state*state)" by (simp add: RawAllowedActs_type AllowedActs_def) -(* Needed in Behaviors *) +text{*Needed in Behaviors*} lemma ActsD: "[| act \ Acts(F); \ act |] ==> s \ state & s' \ 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) \ program" @@ -246,7 +247,7 @@ cons(id(state), allowed \ 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 \ 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 == { \ A*B. P(s, s')} |] ==> ( \ act) <-> ( \ 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 \ A) <-> (x \ 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 \ A co A'; A'\B' |] ==> F \ 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 \ A co A'; B\A |] ==> F \ B co A'" apply (unfold constrains_def st_set_def, blast) @@ -439,8 +440,8 @@ "[| F \ A co A' |] ==> A \ 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 \ A co B; F \ B co C |] ==> F \ A co C" by (unfold constrains_def st_set_def, auto, blast) @@ -583,13 +584,13 @@ Should the premise be !!m instead of \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": "[| \m \ M. F \ {s \ A. x(s) = m} co B(m); F \ program |] ==> F \ {s \ A. x(s) \ M} co (\m \ 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: "[| \m \ M. F \ {s \ state. x(s) = m} co B(m); F \ program |] ==> F:{s \ state. x(s) \ M} co (\m \ M. B(m))"