--- a/src/HOL/UNITY/Channel.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Channel.ML Fri Jul 31 18:46:55 1998 +0200
@@ -8,11 +8,8 @@
From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
*)
-open Channel;
-
AddIffs [skip];
-
(*None represents "infinity" while Some represents proper integers*)
Goalw [minSet_def] "minSet A = Some x --> x : A";
by (Simp_tac 1);
--- a/src/HOL/UNITY/Deadlock.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Deadlock.ML Fri Jul 31 18:46:55 1998 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/UNITY/Traces
+(* Title: HOL/UNITY/Deadlock
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
--- a/src/HOL/UNITY/FP.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/FP.ML Fri Jul 31 18:46:55 1998 +0200
@@ -8,12 +8,6 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-Goal "Union(B) Int A = (UN C:B. C Int A)";
-by (Blast_tac 1);
-qed "Int_Union2";
-
-open FP;
-
Goalw [FP_Orig_def, stable_def] "stable Acts (FP_Orig Acts Int B)";
by (stac Int_Union2 1);
by (rtac ball_constrains_UN 1);
--- a/src/HOL/UNITY/LessThan.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/LessThan.ML Fri Jul 31 18:46:55 1998 +0200
@@ -7,9 +7,6 @@
*)
-open LessThan;
-
-
(*** lessThan ***)
Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
@@ -144,3 +141,55 @@
qed "atMost_Int_atLeast";
+
+
+(*** Finally, a few set-theoretic laws...
+ CAN BOOLEAN SIMPLIFICATION BE AUTOMATED? ***)
+
+context Set.thy;
+
+(** Rewrites rules to eliminate A. Conditions can be satisfied by letting B
+ be any set including A Int C and contained in A Un C, such as B=A or B=C.
+**)
+
+Goal "[| A Int C <= B; B <= A Un C |] \
+\ ==> (A Int B) Un (Compl A Int C) = B Un C";
+by (Blast_tac 1);
+
+Goal "[| A Int C <= B; B <= A Un C |] \
+\ ==> (A Un B) Int (Compl A Un C) = B Int C";
+by (Blast_tac 1);
+
+(*The base B=A*)
+Goal "A Un (Compl A Int C) = A Un C";
+by (Blast_tac 1);
+
+Goal "A Int (Compl A Un C) = A Int C";
+by (Blast_tac 1);
+
+(*The base B=C*)
+Goal "(A Int C) Un (Compl A Int C) = C";
+by (Blast_tac 1);
+
+Goal "(A Un C) Int (Compl A Un C) = C";
+by (Blast_tac 1);
+
+
+(** More ad-hoc rules **)
+
+Goal "A Un B - (A - B) = B";
+by (Blast_tac 1);
+qed "Un_Diff_Diff";
+
+Goal "A Int (B - C) Un C = A Int B Un C";
+by (Blast_tac 1);
+qed "Int_Diff_Un";
+
+Goal "Union(B) Int A = (UN C:B. C Int A)";
+by (Blast_tac 1);
+qed "Int_Union2";
+
+Goal "Union(B) Int A = Union((%C. C Int A)``B)";
+by (Blast_tac 1);
+qed "Int_Union_Union";
+
--- a/src/HOL/UNITY/LessThan.thy Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/LessThan.thy Fri Jul 31 18:46:55 1998 +0200
@@ -6,7 +6,7 @@
lessThan, greaterThan, atLeast, atMost
*)
-LessThan = List +
+LessThan = Main +
constdefs
--- a/src/HOL/UNITY/Mutex.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML Fri Jul 31 18:46:55 1998 +0200
@@ -6,10 +6,12 @@
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
*)
-open Mutex;
+(*split_all_tac causes a big blow-up*)
+claset_ref() := claset() delSWrapper "split_all_tac";
-val cmd_defs = [mutex_def, cmd0_def, cmd1u_def, cmd1v_def,
- cmd2_def, cmd3_def, cmd4_def];
+val cmd_defs = [mutex_def,
+ cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def,
+ cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def];
Goalw [mutex_def] "id : mutex";
by (Simp_tac 1);
@@ -17,7 +19,16 @@
AddIffs [id_in_mutex];
-(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
+(*Simplification for records*)
+val select_defs = thms"state.select_defs"
+and update_defs = thms"state.update_defs"
+and dest_defs = thms"state.dest_defs";
+
+Addsimps update_defs;
+
+
+(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS
+ [They have free occurrences of mutex_def and cmd_defs] **)
(*proves "constrains" properties when the program is specified*)
val constrains_tac =
@@ -32,82 +43,67 @@
(*proves "ensures" properties when the program is specified*)
fun ensures_tac sact =
SELECT_GOAL
- (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
+ (EVERY [etac reachable_LeadsTo_Basis 1
+ ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
+ REPEAT (ares_tac [leadsTo_imp_LeadsTo, leadsTo_Basis,
+ ensuresI] 1),
res_inst_tac [("act", sact)] transient_mem 2,
- Simp_tac 2,
+ simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
+ simp_tac (simpset() addsimps [mutex_def]) 2,
constrains_tac 1,
rewrite_goals_tac cmd_defs,
+ ALLGOALS Clarify_tac,
Auto_tac]);
-(*The booleans p, u, v are always either 0 or 1*)
-Goalw [stable_def, boolVars_def]
- "stable mutex boolVars";
+Goalw [stable_def, invariantU_def] "stable mutex invariantU";
by (constrains_tac 1);
-by (auto_tac (claset() addSEs [less_SucE], simpset()));
-qed "stable_boolVars";
+qed "stable_invariantU";
-Goal "reachable (MInit,mutex) <= boolVars";
-by (rtac strongest_invariant 1);
-by (rtac stable_boolVars 2);
-by (rewrite_goals_tac [MInit_def, boolVars_def]);
-by Auto_tac;
-qed "reachable_subset_boolVars";
-
-val reachable_subset_boolVars' =
- rewrite_rule [boolVars_def] reachable_subset_boolVars;
+Goalw [stable_def, invariantV_def] "stable mutex invariantV";
+by (constrains_tac 1);
+qed "stable_invariantV";
-Goalw [stable_def, invariant_def]
- "stable mutex (invariant 0 UU MM)";
-by (constrains_tac 1);
-qed "stable_invar_0um";
+Goalw [MInit_def, invariantU_def] "MInit <= invariantU";
+by Auto_tac;
+qed "MInit_invariantU";
-Goalw [stable_def, invariant_def]
- "stable mutex (invariant 1 VV NN)";
-by (constrains_tac 1);
-qed "stable_invar_1vn";
-
-Goalw [MInit_def, invariant_def] "MInit <= invariant 0 UU MM";
+Goalw [MInit_def, invariantV_def] "MInit <= invariantV";
by Auto_tac;
-qed "MInit_invar_0um";
-
-Goalw [MInit_def, invariant_def] "MInit <= invariant 1 VV NN";
-by Auto_tac;
-qed "MInit_invar_1vn";
+qed "MInit_invariantV";
(*The intersection is an invariant of the system*)
-Goal "reachable (MInit,mutex) <= invariant 0 UU MM Int invariant 1 VV NN";
+Goal "reachable (MInit,mutex) <= invariantU Int invariantV";
by (simp_tac (simpset() addsimps
[strongest_invariant, Int_greatest, stable_Int,
- stable_invar_0um, stable_invar_1vn,
- MInit_invar_0um,MInit_invar_1vn]) 1);
+ stable_invariantU, stable_invariantV,
+ MInit_invariantU,MInit_invariantV]) 1);
qed "reachable_subset_invariant";
val reachable_subset_invariant' =
- rewrite_rule [invariant_def] reachable_subset_invariant;
+ rewrite_rule [invariantU_def, invariantV_def] reachable_subset_invariant;
(*The safety property (mutual exclusion) follows from the claimed invar_s*)
-Goalw [invariant_def]
- "{s. s MM = 3 & s NN = 3} <= \
-\ Compl (invariant 0 UU MM Int invariant 1 VV NN)";
+Goalw [invariantU_def, invariantV_def]
+ "{s. MM s = 3 & NN s = 3} <= Compl (invariantU Int invariantV)";
by Auto_tac;
val lemma = result();
-Goal "{s. s MM = 3 & s NN = 3} <= Compl (reachable (MInit,mutex))";
-by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono] MRS subset_trans) 1);
+Goal "{s. MM s = 3 & NN s = 3} <= Compl (reachable (MInit,mutex))";
+by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono]
+ MRS subset_trans) 1);
qed "mutual_exclusion";
-(*The bad invariant FAILS in cmd1v*)
-Goalw [stable_def, bad_invariant_def]
- "stable mutex (bad_invariant 0 UU MM)";
+(*The bad invariant FAILS in cmd1V*)
+Goalw [stable_def, bad_invariantU_def] "stable mutex bad_invariantU";
by (constrains_tac 1);
-by (trans_tac 1);
+by (REPEAT (trans_tac 1));
by (safe_tac (claset() addSEs [le_SucE]));
by (Asm_full_simp_tac 1);
(*Resulting state: n=1, p=false, m=4, u=false.
- Execution of cmd1v (the command of process v guarded by n=1) sets p:=true,
+ Execution of cmd1V (the command of process v guarded by n=1) sets p:=true,
violating the invariant!*)
(*Check that subgoals remain: proof failed.*)
getgoal 1;
@@ -115,42 +111,40 @@
(*** Progress for U ***)
-Goalw [unless_def] "unless mutex {s. s MM=2} {s. s MM=3}";
+Goalw [unless_def] "unless mutex {s. MM s=2} {s. MM s=3}";
by (constrains_tac 1);
qed "U_F0";
-Goal "LeadsTo(MInit,mutex) {s. s MM=1} {s. s PP = s VV & s MM = 2}";
-by (rtac leadsTo_imp_LeadsTo 1); (*makes the proof much faster*)
-by (ensures_tac "cmd1u" 1);
+Goal "LeadsTo(MInit,mutex) {s. MM s=1} {s. PP s = VV s & MM s = 2}";
+by (ensures_tac "cmd1U" 1);
qed "U_F1";
-Goal "LeadsTo(MInit,mutex) {s. s PP = 0 & s MM = 2} {s. s MM = 3}";
+Goal "LeadsTo(MInit,mutex) {s. ~ PP s & MM s = 2} {s. MM s = 3}";
by (cut_facts_tac [reachable_subset_invariant'] 1);
-by (ensures_tac "cmd2 0 MM" 1);
+by (ensures_tac "cmd2U" 1);
qed "U_F2";
-Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. s MM = 3} {s. s PP = 1}";
+Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. MM s = 3} {s. PP s}";
by (rtac leadsTo_imp_LeadsTo 1);
-by (res_inst_tac [("B", "{s. s MM = 4}")] leadsTo_Trans 1);
-by (ensures_tac "cmd4 1 MM" 2);
-by (ensures_tac "cmd3 UU MM" 1);
+by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
+by (ensures_tac "cmd4U" 2);
+by (ensures_tac "cmd3U" 1);
qed "U_F3";
-Goal "LeadsTo(MInit,mutex) {s. s MM = 2} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {s. MM s = 2} {s. PP s}";
by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
-by (cut_facts_tac [reachable_subset_boolVars'] 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
val lemma2 = result();
-Goal "LeadsTo(MInit,mutex) {s. s MM = 1} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {s. MM s = 1} {s. PP s}";
by (rtac ([U_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
by (Blast_tac 1);
val lemma1 = result();
-Goal "LeadsTo(MInit,mutex) {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {s. 1 <= MM s & MM s <= 3} {s. PP s}";
by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL]
addcongs [rev_conj_cong]) 1);
by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
@@ -159,7 +153,7 @@
(*Misra's F4*)
-Goal "LeadsTo(MInit,mutex) {s. s UU = 1} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {s. UU s} {s. PP s}";
by (rtac LeadsTo_weaken_L 1);
by (rtac lemma123 1);
by (cut_facts_tac [reachable_subset_invariant'] 1);
@@ -170,42 +164,40 @@
(*** Progress for V ***)
-Goalw [unless_def] "unless mutex {s. s NN=2} {s. s NN=3}";
+Goalw [unless_def] "unless mutex {s. NN s=2} {s. NN s=3}";
by (constrains_tac 1);
qed "V_F0";
-Goal "LeadsTo(MInit,mutex) {s. s NN=1} {s. s PP = 1 - s UU & s NN = 2}";
-by (rtac leadsTo_imp_LeadsTo 1); (*makes the proof much faster*)
-by (ensures_tac "cmd1v" 1);
+Goal "LeadsTo(MInit,mutex) {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}";
+by (ensures_tac "cmd1V" 1);
qed "V_F1";
-Goal "LeadsTo(MInit,mutex) {s. s PP = 1 & s NN = 2} {s. s NN = 3}";
+Goal "LeadsTo(MInit,mutex) {s. PP s & NN s = 2} {s. NN s = 3}";
by (cut_facts_tac [reachable_subset_invariant'] 1);
-by (ensures_tac "cmd2 1 NN" 1);
+by (ensures_tac "cmd2V" 1);
qed "V_F2";
-Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. s NN = 3} {s. s PP = 0}";
+Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. NN s = 3} {s. ~ PP s}";
by (rtac leadsTo_imp_LeadsTo 1);
-by (res_inst_tac [("B", "{s. s NN = 4}")] leadsTo_Trans 1);
-by (ensures_tac "cmd4 0 NN" 2);
-by (ensures_tac "cmd3 VV NN" 1);
+by (res_inst_tac [("B", "{s. NN s = 4}")] leadsTo_Trans 1);
+by (ensures_tac "cmd4V" 2);
+by (ensures_tac "cmd3V" 1);
qed "V_F3";
-Goal "LeadsTo(MInit,mutex) {s. s NN = 2} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. NN s = 2} {s. ~ PP s}";
by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
-by (cut_facts_tac [reachable_subset_boolVars'] 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
val lemma2 = result();
-Goal "LeadsTo(MInit,mutex) {s. s NN = 1} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. NN s = 1} {s. ~ PP s}";
by (rtac ([V_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
by (Blast_tac 1);
val lemma1 = result();
-Goal "LeadsTo(MInit,mutex) {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. 1 <= NN s & NN s <= 3} {s. ~ PP s}";
by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL]
addcongs [rev_conj_cong]) 1);
by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
@@ -214,7 +206,7 @@
(*Misra's F4*)
-Goal "LeadsTo(MInit,mutex) {s. s VV = 1} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. VV s} {s. ~ PP s}";
by (rtac LeadsTo_weaken_L 1);
by (rtac lemma123 1);
by (cut_facts_tac [reachable_subset_invariant'] 1);
@@ -225,7 +217,7 @@
(** Absence of starvation **)
(*Misra's F6*)
-Goal "LeadsTo(MInit,mutex) {s. s MM = 1} {s. s MM = 3}";
+Goal "LeadsTo(MInit,mutex) {s. MM s = 1} {s. MM s = 3}";
by (rtac LeadsTo_Un_duplicate 1);
by (rtac LeadsTo_cancel2 1);
by (rtac U_F2 2);
@@ -234,13 +226,12 @@
by (rtac LeadsTo_Un_duplicate 1);
by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1);
by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
-by (cut_facts_tac [reachable_subset_boolVars'] 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
qed "m1_leadsto_3";
(*The same for V*)
-Goal "LeadsTo(MInit,mutex) {s. s NN = 1} {s. s NN = 3}";
+Goal "LeadsTo(MInit,mutex) {s. NN s = 1} {s. NN s = 3}";
by (rtac LeadsTo_Un_duplicate 1);
by (rtac LeadsTo_cancel2 1);
by (rtac V_F2 2);
@@ -249,6 +240,5 @@
by (rtac LeadsTo_Un_duplicate 1);
by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1);
by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
-by (cut_facts_tac [reachable_subset_boolVars'] 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
qed "n1_leadsto_3";
--- a/src/HOL/UNITY/Mutex.thy Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Mutex.thy Fri Jul 31 18:46:55 1998 +0200
@@ -6,7 +6,7 @@
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
*)
-Mutex = Update + UNITY + Traces + SubstAx +
+Mutex = UNITY + Traces + SubstAx +
(*WE NEED A GENERAL TREATMENT OF NUMBERS!!*)
syntax
@@ -18,57 +18,66 @@
"4" == "Suc 3"
-(*program variables*)
-datatype pvar = PP | MM | NN | UU | VV
-
-(*No booleans; instead True=1 and False=0*)
-types state = pvar => nat
+record state =
+ PP :: bool
+ MM :: nat
+ NN :: nat
+ UU :: bool
+ VV :: bool
constdefs
- cmd0 :: "[pvar,pvar] => (state*state) set"
- "cmd0 u m == {(s,s'). s' = s(u:=1,m:=1) & s m = 0}"
+ cmd0U :: "(state*state) set"
+ "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=1|) & MM s = 0}"
+
+ cmd1U :: "(state*state) set"
+ "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=2|) & MM s = 1}"
- cmd1u :: "(state*state) set"
- "cmd1u == {(s,s'). s' = s(PP:= s VV,MM:=2) & s MM = 1}"
+ cmd2U :: "(state*state) set"
+ "cmd2U == {(s,s'). s' = s (|MM:=3|) & ~ PP s & MM s = 2}"
- cmd1v :: "(state*state) set"
- "cmd1v == {(s,s'). s' = s(PP:= 1 - s UU,NN:=2) & s NN = 1}"
+ cmd3U :: "(state*state) set"
+ "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=4|) & MM s = 3}"
+
+ cmd4U :: "(state*state) set"
+ "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=0|) & MM s = 4}"
- (*Put pv=0 for u's program and pv=1 for v's program*)
- cmd2 :: "[nat,pvar] => (state*state) set"
- "cmd2 pv m == {(s,s'). s' = s(m:=3) & s PP = pv & s m = 2}"
+ cmd0V :: "(state*state) set"
+ "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=1|) & NN s = 0}"
+
+ cmd1V :: "(state*state) set"
+ "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=2|) & NN s = 1}"
- cmd3 :: "[pvar,pvar] => (state*state) set"
- "cmd3 u m == {(s,s'). s' = s(u:=0,m:=4) & s m = 3}"
+ cmd2V :: "(state*state) set"
+ "cmd2V == {(s,s'). s' = s (|NN:=3|) & PP s & NN s = 2}"
- (*Put pv=1 for u's program and pv=0 for v's program*)
- cmd4 :: "[nat,pvar] => (state*state) set"
- "cmd4 pv m == {(s,s'). s' = s(PP:=pv,m:=0) & s m = 4}"
+ cmd3V :: "(state*state) set"
+ "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=4|) & NN s = 3}"
+
+ cmd4V :: "(state*state) set"
+ "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=0|) & NN s = 4}"
mutex :: "(state*state) set set"
"mutex == {id,
- cmd0 UU MM, cmd0 VV NN,
- cmd1u, cmd1v,
- cmd2 0 MM, cmd2 1 NN,
- cmd3 UU MM, cmd3 VV NN,
- cmd4 1 MM, cmd4 0 NN}"
+ cmd0U, cmd1U, cmd2U, cmd3U, cmd4U,
+ cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}"
+
+ (** The correct invariants **)
+
+ invariantU :: "state set"
+ "invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) &
+ (MM s = 3 --> ~ PP s)}"
+
+ invariantV :: "state set"
+ "invariantV == {s. (VV s = (1 <= NN s & NN s <= 3)) &
+ (NN s = 3 --> PP s)}"
+
+ (** The faulty invariant (for U alone) **)
+
+ bad_invariantU :: "state set"
+ "bad_invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) &
+ (3 <= MM s & MM s <= 4 --> ~ PP s)}"
MInit :: "state set"
- "MInit == {s. s PP < 2 & s UU = 0 & s VV = 0 & s MM = 0 & s NN = 0}"
-
- boolVars :: "state set"
- "boolVars == {s. s PP<2 & s UU < 2 & s VV < 2}"
-
- (*Put pv=0 for u's program and pv=1 for v's program*)
- invariant :: "[nat,pvar,pvar] => state set"
- "invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
- (s m = 3 --> s PP = pv)}"
-
- bad_invariant :: "[nat,pvar,pvar] => state set"
- "bad_invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
- (3 <= s m & s m <= 4 --> s PP = pv)}"
-
-
-
+ "MInit == {s. ~ UU s & ~ VV s & MM s = 0 & NN s = 0}"
end
--- a/src/HOL/UNITY/Network.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Network.ML Fri Jul 31 18:46:55 1998 +0200
@@ -8,8 +8,6 @@
From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
*)
-open Network;
-
val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] =
Goalw [stable_def]
"[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \
--- a/src/HOL/UNITY/Reach.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML Fri Jul 31 18:46:55 1998 +0200
@@ -7,8 +7,6 @@
[ this example took only four days!]
*)
-open Reach;
-
(*TO SIMPDATA.ML?? FOR CLASET?? *)
val major::prems = goal thy
"[| if P then Q else R; \
--- a/src/HOL/UNITY/Reach.thy Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Reach.thy Fri Jul 31 18:46:55 1998 +0200
@@ -6,7 +6,7 @@
Reachability in Directed Graphs. From Chandy and Misra, section 6.4.
*)
-Reach = Update + FP + Traces + SubstAx +
+Reach = FP + Traces + SubstAx +
types vertex
state = "vertex=>bool"
--- a/src/HOL/UNITY/SubstAx.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Fri Jul 31 18:46:55 1998 +0200
@@ -8,8 +8,6 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-open SubstAx;
-
(*constrains Acts B B' ==> constrains Acts (reachable(Init,Acts) Int B)
(reachable(Init,Acts) Int B') *)
bind_thm ("constrains_reachable",
@@ -24,9 +22,9 @@
qed "leadsTo_imp_LeadsTo";
Goal "[| constrains Acts (reachable(Init,Acts) Int (A - A')) \
-\ (A Un A'); \
-\ transient Acts (reachable(Init,Acts) Int (A-A')) |] \
-\ ==> LeadsTo(Init,Acts) A A'";
+\ (A Un A'); \
+\ transient Acts (reachable(Init,Acts) Int (A-A')) |] \
+\ ==> LeadsTo(Init,Acts) A A'";
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1);
by (assume_tac 2);
@@ -36,7 +34,7 @@
qed "LeadsTo_Basis";
Goal "[| LeadsTo(Init,Acts) A B; LeadsTo(Init,Acts) B C |] \
-\ ==> LeadsTo(Init,Acts) A C";
+\ ==> LeadsTo(Init,Acts) A C";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
qed "LeadsTo_Trans";
@@ -75,15 +73,14 @@
qed "LeadsTo_UN";
(*Binary union introduction rule*)
-Goal
- "[| LeadsTo(Init,Acts) A C; LeadsTo(Init,Acts) B C |] ==> LeadsTo(Init,Acts) (A Un B) C";
+Goal "[| LeadsTo(Init,Acts) A C; LeadsTo(Init,Acts) B C |] ==> LeadsTo(Init,Acts) (A Un B) C";
by (stac Un_eq_Union 1);
by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
qed "LeadsTo_Un";
Goal "[| reachable(Init,Acts) Int A <= B; id: Acts |] \
-\ ==> LeadsTo(Init,Acts) A B";
+\ ==> LeadsTo(Init,Acts) A B";
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
qed "Int_subset_imp_LeadsTo";
@@ -97,55 +94,51 @@
Addsimps [empty_LeadsTo];
Goal "[| reachable(Init,Acts) Int A = {}; id: Acts |] \
-\ ==> LeadsTo(Init,Acts) A B";
+\ ==> LeadsTo(Init,Acts) A B";
by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1);
qed "Int_empty_LeadsTo";
Goal "[| LeadsTo(Init,Acts) A A'; \
-\ reachable(Init,Acts) Int A' <= B' |] \
-\ ==> LeadsTo(Init,Acts) A B'";
+\ reachable(Init,Acts) Int A' <= B' |] \
+\ ==> LeadsTo(Init,Acts) A B'";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
qed_spec_mp "LeadsTo_weaken_R";
Goal "[| LeadsTo(Init,Acts) A A'; \
-\ reachable(Init,Acts) Int B <= A; id: Acts |] \
-\ ==> LeadsTo(Init,Acts) B A'";
+\ reachable(Init,Acts) Int B <= A; id: Acts |] \
+\ ==> LeadsTo(Init,Acts) B A'";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
qed_spec_mp "LeadsTo_weaken_L";
(*Distributes over binary unions*)
-Goal
- "id: Acts ==> \
+Goal "id: Acts ==> \
\ LeadsTo(Init,Acts) (A Un B) C = \
\ (LeadsTo(Init,Acts) A C & LeadsTo(Init,Acts) B C)";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Un_distrib";
-Goal
- "id: Acts ==> \
+Goal "id: Acts ==> \
\ LeadsTo(Init,Acts) (UN i:I. A i) B = \
\ (ALL i : I. LeadsTo(Init,Acts) (A i) B)";
by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
qed "LeadsTo_UN_distrib";
-Goal
- "id: Acts ==> \
+Goal "id: Acts ==> \
\ LeadsTo(Init,Acts) (Union S) B = \
\ (ALL A : S. LeadsTo(Init,Acts) A B)";
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Union_distrib";
-Goal
- "[| LeadsTo(Init,Acts) A A'; id: Acts; \
-\ reachable(Init,Acts) Int B <= A; \
-\ reachable(Init,Acts) Int A' <= B' |] \
-\ ==> LeadsTo(Init,Acts) B B'";
+Goal "[| LeadsTo(Init,Acts) A A'; id: Acts; \
+\ reachable(Init,Acts) Int B <= A; \
+\ reachable(Init,Acts) Int A' <= B' |] \
+\ ==> LeadsTo(Init,Acts) B B'";
(*PROOF FAILED: why?*)
by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
LeadsTo_weaken_L]) 1);
@@ -153,8 +146,7 @@
(*Set difference: maybe combine with leadsTo_weaken_L??*)
-Goal
- "[| LeadsTo(Init,Acts) (A-B) C; LeadsTo(Init,Acts) B C; id: Acts |] \
+Goal "[| LeadsTo(Init,Acts) (A-B) C; LeadsTo(Init,Acts) B C; id: Acts |] \
\ ==> LeadsTo(Init,Acts) A C";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
qed "LeadsTo_Diff";
@@ -181,8 +173,7 @@
qed "LeadsTo_UN_UN_noindex";
(*Version with no index set*)
-Goal
- "ALL i. LeadsTo(Init,Acts) (A i) (A' i) \
+Goal "ALL i. LeadsTo(Init,Acts) (A i) (A' i) \
\ ==> LeadsTo(Init,Acts) (UN i. A i) (UN i. A' i)";
by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
qed "all_LeadsTo_UN_UN";
@@ -198,31 +189,27 @@
(** The cancellation law **)
-Goal
- "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) B B'; \
+Goal "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) B B'; \
\ id: Acts |] \
\ ==> LeadsTo(Init,Acts) A (A' Un B')";
by (blast_tac (claset() addIs [LeadsTo_Un_Un,
subset_imp_LeadsTo, LeadsTo_Trans]) 1);
qed "LeadsTo_cancel2";
-Goal
- "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
+Goal "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
\ ==> LeadsTo(Init,Acts) A (A' Un B')";
by (rtac LeadsTo_cancel2 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
qed "LeadsTo_cancel_Diff2";
-Goal
- "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) B B'; id: Acts |] \
+Goal "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) B B'; id: Acts |] \
\ ==> LeadsTo(Init,Acts) A (B' Un A')";
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
qed "LeadsTo_cancel1";
-Goal
- "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
+Goal "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
\ ==> LeadsTo(Init,Acts) A (B' Un A')";
by (rtac LeadsTo_cancel1 1);
by (assume_tac 2);
@@ -263,8 +250,7 @@
by (ALLGOALS Blast_tac);
qed "R_PSP";
-Goal
- "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \
+Goal "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \
\ ==> LeadsTo(Init,Acts) (B Int A) ((B Int A') Un (B' - B))";
by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1);
qed "R_PSP2";
@@ -285,8 +271,7 @@
(*** Induction rules ***)
(** Meta or object quantifier ????? **)
-Goal
- "[| wf r; \
+Goal "[| wf r; \
\ ALL m. LeadsTo(Init,Acts) (A Int f-``{m}) \
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
\ id: Acts |] \
@@ -298,12 +283,11 @@
qed "LeadsTo_wf_induct";
-Goal
- "[| wf r; \
-\ ALL m:I. LeadsTo(Init,Acts) (A Int f-``{m}) \
-\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
-\ id: Acts |] \
-\ ==> LeadsTo(Init,Acts) A ((A - (f-``I)) Un B)";
+Goal "[| wf r; \
+\ ALL m:I. LeadsTo(Init,Acts) (A Int f-``{m}) \
+\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
+\ id: Acts |] \
+\ ==> LeadsTo(Init,Acts) A ((A - (f-``I)) Un B)";
by (etac LeadsTo_wf_induct 1);
by Safe_tac;
by (case_tac "m:I" 1);
@@ -312,18 +296,16 @@
qed "R_bounded_induct";
-Goal
- "[| ALL m. LeadsTo(Init,Acts) (A Int f-``{m}) \
+Goal "[| ALL m. LeadsTo(Init,Acts) (A Int f-``{m}) \
\ ((A Int f-``(lessThan m)) Un B); \
-\ id: Acts |] \
-\ ==> LeadsTo(Init,Acts) A B";
+\ id: Acts |] \
+\ ==> LeadsTo(Init,Acts) A B";
by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
by (assume_tac 2);
by (Asm_simp_tac 1);
qed "R_lessThan_induct";
-Goal
- "[| ALL m:(greaterThan l). LeadsTo(Init,Acts) (A Int f-``{m}) \
+Goal "[| ALL m:(greaterThan l). LeadsTo(Init,Acts) (A Int f-``{m}) \
\ ((A Int f-``(lessThan m)) Un B); \
\ id: Acts |] \
\ ==> LeadsTo(Init,Acts) A ((A Int (f-``(atMost l))) Un B)";
@@ -333,11 +315,10 @@
by (Asm_simp_tac 1);
qed "R_lessThan_bounded_induct";
-Goal
- "[| ALL m:(lessThan l). LeadsTo(Init,Acts) (A Int f-``{m}) \
-\ ((A Int f-``(greaterThan m)) Un B); \
-\ id: Acts |] \
-\ ==> LeadsTo(Init,Acts) A ((A Int (f-``(atLeast l))) Un B)";
+Goal "[| ALL m:(lessThan l). LeadsTo(Init,Acts) (A Int f-``{m}) \
+\ ((A Int f-``(greaterThan m)) Un B); \
+\ id: Acts |] \
+\ ==> LeadsTo(Init,Acts) A ((A Int (f-``(atLeast l))) Un B)";
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
(wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
by (assume_tac 2);
@@ -352,10 +333,9 @@
(*** Completion: Binary and General Finite versions ***)
-Goal
- "[| LeadsTo(Init,Acts) A A'; stable Acts A'; \
-\ LeadsTo(Init,Acts) B B'; stable Acts B'; id: Acts |] \
-\ ==> LeadsTo(Init,Acts) (A Int B) (A' Int B')";
+Goal "[| LeadsTo(Init,Acts) A A'; stable Acts A'; \
+\ LeadsTo(Init,Acts) B B'; stable Acts B'; id: Acts |] \
+\ ==> LeadsTo(Init,Acts) (A Int B) (A' Int B')";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken]
addSIs [stable_Int, stable_reachable]) 1);
@@ -363,9 +343,9 @@
Goal "[| finite I; id: Acts |] \
-\ ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i)) --> \
-\ (ALL i:I. stable Acts (A' i)) --> \
-\ LeadsTo(Init,Acts) (INT i:I. A i) (INT i:I. A' i)";
+\ ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i)) --> \
+\ (ALL i:I. stable Acts (A' i)) --> \
+\ LeadsTo(Init,Acts) (INT i:I. A i) (INT i:I. A' i)";
by (etac finite_induct 1);
by (Asm_simp_tac 1);
by (asm_simp_tac
@@ -374,12 +354,10 @@
qed_spec_mp "R_finite_stable_completion";
-Goal
- "[| LeadsTo(Init,Acts) A (A' Un C); constrains Acts A' (A' Un C); \
-\ LeadsTo(Init,Acts) B (B' Un C); constrains Acts B' (B' Un C); \
-\ id: Acts |] \
-\ ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B') Un C)";
-
+Goal "[| LeadsTo(Init,Acts) A (A' Un C); constrains Acts A' (A' Un C); \
+\ LeadsTo(Init,Acts) B (B' Un C); constrains Acts B' (B' Un C); \
+\ id: Acts |] \
+\ ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B') Un C)";
by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1);
by (dtac completion 1);
by (assume_tac 2);
@@ -390,11 +368,10 @@
qed "R_completion";
-Goal
- "[| finite I; id: Acts |] \
-\ ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i Un C)) --> \
-\ (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
-\ LeadsTo(Init,Acts) (INT i:I. A i) ((INT i:I. A' i) Un C)";
+Goal "[| finite I; id: Acts |] \
+\ ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i Un C)) --> \
+\ (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
+\ LeadsTo(Init,Acts) (INT i:I. A i) ((INT i:I. A' i) Un C)";
by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
by (Clarify_tac 1);
@@ -402,3 +379,29 @@
by (asm_full_simp_tac (simpset() addsimps [R_completion]) 1);
qed "R_finite_completion";
+
+
+(*** Specialized laws for handling invariants ***)
+
+Goalw [transient_def]
+ "[| reachable(Init,Acts) <= INV; transient Acts (INV Int A) |] \
+\ ==> transient Acts (reachable(Init,Acts) Int A)";
+by (Clarify_tac 1);
+by (rtac bexI 1);
+by (assume_tac 2);
+by (Blast_tac 1);
+qed "reachable_transient";
+
+(*Eliminates the set "reachable (Init,Acts)" from the subgoals. This boosts
+ efficiency because the term contains a full copy of the program.*)
+Goal "[| reachable (Init,Acts) <= INV; \
+\ constrains Acts (INV Int (A - A')) (A Un A'); \
+\ transient Acts (INV Int (A-A')) |] \
+\ ==> LeadsTo(Init,Acts) A A'";
+by (rtac LeadsTo_Basis 1);
+by (blast_tac (claset() addSIs [reachable_transient]) 2);
+by (rewtac constrains_def);
+by (Blast_tac 1);
+qed "reachable_LeadsTo_Basis";
+
+
--- a/src/HOL/UNITY/Token.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Token.ML Fri Jul 31 18:46:55 1998 +0200
@@ -8,11 +8,7 @@
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
*)
-
-open Token;
-
-
-val Token_defs = [WellTyped_def, Token_def, HasTok_def, H_def, E_def, T_def];
+val Token_defs = [HasTok_def, H_def, E_def, T_def];
AddIffs [N_positive, skip];
@@ -20,33 +16,14 @@
by Auto_tac;
qed "HasToK_partition";
-Goalw Token_defs "s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
+Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)";
by (Simp_tac 1);
-by (exhaust_tac "s (Suc i)" 1);
+by (exhaust_tac "proc s i" 1);
by Auto_tac;
qed "not_E_eq";
-(** We should be able to prove WellTyped as a separate Invariant. Then
- the Invariant rule should let us assume that the initial
- state is reachable, and therefore contained in any Invariant. Then
- we'd not have to mention WellTyped in the statement of this theorem.
-**)
-
-Goalw [stable_def]
- "stable Acts (WellTyped Int {s. s : E i --> s : HasTok i})";
-by (rtac (stable_WT RS stable_constrains_Int) 1);
-by (cut_facts_tac [TR2,TR4,TR5] 1);
-by (asm_full_simp_tac (simpset() addsimps [constrains_def]) 1);
-by (REPEAT_FIRST (rtac ballI ORELSE' (dtac bspec THEN' assume_tac)));
-by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
-by (case_tac "xa : HasTok i" 1);
-by (auto_tac (claset(), simpset() addsimps [H_def, E_def, T_def]));
-qed "token_stable";
-
(*This proof is in the "massaging" style and is much faster! *)
-Goalw [stable_def]
- "stable Acts (WellTyped Int (Compl(E i) Un (HasTok i)))";
-by (rtac (stable_WT RS stable_constrains_Int) 1);
+Goalw [stable_def] "stable Acts (Compl(E i) Un (HasTok i))";
by (rtac constrains_weaken 1);
by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
@@ -99,9 +76,8 @@
(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
Note the use of case_tac. Reasoning about leadsTo takes practice!*)
-Goal
- "[| i<N; j<N |] ==> \
-\ leadsTo Acts (HasTok i) ({s. (Token s, i) : nodeOrder j} Un HasTok j)";
+Goal "[| i<N; j<N |] ==> \
+\ leadsTo Acts (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)";
by (case_tac "i=j" 1);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
by (rtac (TR7 RS leadsTo_weaken_R) 1);
@@ -111,27 +87,25 @@
(*Chapter 4 variant, the one actually used below.*)
-Goal
- "[| i<N; j<N; i~=j |] ==> \
-\ leadsTo Acts (HasTok i) {s. (Token s, i) : nodeOrder j}";
+Goal "[| i<N; j<N; i~=j |] \
+\ ==> leadsTo Acts (HasTok i) {s. (token s, i) : nodeOrder j}";
by (rtac (TR7 RS leadsTo_weaken_R) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
qed "TR7_aux";
-Goal "({s. Token s < N} Int Token -`` {m}) = \
-\ (if m<N then Token -`` {m} else {})";
+Goal "({s. token s < N} Int token -`` {m}) = \
+\ (if m<N then token -`` {m} else {})";
by Auto_tac;
-val Token_lemma = result();
+val token_lemma = result();
(*Misra's TR9: the token reaches an arbitrary node*)
-Goal
- "j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
+Goal "j<N ==> leadsTo Acts {s. token s < N} (HasTok j)";
by (rtac leadsTo_weaken_R 1);
-by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")]
+by (res_inst_tac [("I", "Compl{j}"), ("f", "token"), ("B", "{}")]
(wf_nodeOrder RS bounded_induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Token_lemma, vimage_Diff,
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff,
HasTok_def])));
by (Blast_tac 2);
by (Clarify_tac 1);
@@ -141,10 +115,10 @@
qed "leadsTo_j";
(*Misra's TR8: a hungry process eventually eats*)
-Goal "j<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)";
+Goal "j<N ==> leadsTo Acts ({s. token s < N} Int H j) (E j)";
by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
by (rtac TR6 2);
by (rtac leadsTo_weaken_R 1);
by (rtac ([leadsTo_j, TR3] MRS PSP) 1);
by (ALLGOALS Blast_tac);
-qed "Token_progress";
+qed "token_progress";
--- a/src/HOL/UNITY/Token.thy Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Token.thy Fri Jul 31 18:46:55 1998 +0200
@@ -12,9 +12,11 @@
Token = WFair +
(*process states*)
-datatype pstate = Hungry | Eating | Thinking | Pnum nat
+datatype pstate = Hungry | Eating | Thinking
-types state = nat => pstate
+record state =
+ token :: nat
+ proc :: nat => pstate
consts
N :: nat (*number of nodes in the ring*)
@@ -27,33 +29,21 @@
next :: nat => nat
"next i == (Suc i) mod N"
- WellTyped :: state set
- "WellTyped == {s. ALL i j. s (Suc i) ~= Pnum j}"
-
- Token :: state => nat
- "Token s == case s 0 of
- Hungry => 0
- | Eating => 0
- | Thinking => 0
- | Pnum i => i"
-
HasTok :: nat => state set
- "HasTok i == Token -`` {i}"
+ "HasTok i == {s. token s = i}"
H :: nat => state set
- "H i == {s. s (Suc i) = Hungry}"
+ "H i == {s. proc s i = Hungry}"
E :: nat => state set
- "E i == {s. s (Suc i) = Eating}"
+ "E i == {s. proc s i = Eating}"
T :: nat => state set
- "T i == {s. s (Suc i) = Thinking}"
+ "T i == {s. proc s i = Thinking}"
rules
N_positive "0<N"
- stable_WT "stable Acts WellTyped"
-
skip "id: Acts"
TR2 "constrains Acts (T i) (T i Un H i)"
--- a/src/HOL/UNITY/Traces.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML Fri Jul 31 18:46:55 1998 +0200
@@ -9,9 +9,6 @@
*)
-open Traces;
-
-
(****
Now simulate the inductive definition (illegal due to paired arguments)
@@ -38,7 +35,7 @@
\ ==> (s,s'): act --> s' : reachable(Init,Acts)";
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
by (etac exE 1);
-be traces.induct 1;
+by (etac traces.induct 1);
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS (blast_tac (claset() addIs traces.intrs)));
qed_spec_mp "reachable_Acts";
@@ -54,7 +51,7 @@
\ ==> P za";
by (cut_facts_tac [major] 1);
by Auto_tac;
-be traces.induct 1;
+by (etac traces.induct 1);
by (ALLGOALS (blast_tac (claset() addIs prems)));
qed "reachable_induct";
@@ -71,7 +68,7 @@
Goalw [stable_def, constrains_def]
"[| Init<=A; stable Acts A |] ==> reachable(Init,Acts) <= A";
by (rtac subsetI 1);
-be reachable.induct 1;
+by (etac reachable.induct 1);
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
qed "strongest_invariant";
--- a/src/HOL/UNITY/UNITY.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/UNITY.ML Fri Jul 31 18:46:55 1998 +0200
@@ -12,49 +12,6 @@
HOL_quantifiers := false;
-(*CAN BOOLEAN SIMPLIFICATION BE AUTOMATED?*)
-
-(** Rewrites rules to eliminate A. Conditions can be satisfied by letting B
- be any set including A Int C and contained in A Un C, such as B=A or B=C.
-**)
-
-Goal "[| A Int C <= B; B <= A Un C |] \
-\ ==> (A Int B) Un (Compl A Int C) = B Un C";
-by (Blast_tac 1);
-
-Goal "[| A Int C <= B; B <= A Un C |] \
-\ ==> (A Un B) Int (Compl A Un C) = B Int C";
-by (Blast_tac 1);
-
-(*The base B=A*)
-Goal "A Un (Compl A Int C) = A Un C";
-by (Blast_tac 1);
-
-Goal "A Int (Compl A Un C) = A Int C";
-by (Blast_tac 1);
-
-(*The base B=C*)
-Goal "(A Int C) Un (Compl A Int C) = C";
-by (Blast_tac 1);
-
-Goal "(A Un C) Int (Compl A Un C) = C";
-by (Blast_tac 1);
-
-
-(** More ad-hoc rules **)
-
-Goal "A Un B - (A - B) = B";
-by (Blast_tac 1);
-qed "Un_Diff_Diff";
-
-Goal "A Int (B - C) Un C = A Int B Un C";
-by (Blast_tac 1);
-qed "Int_Diff_Un";
-
-
-open UNITY;
-
-
(*** constrains ***)
val prems = goalw thy [constrains_def]
--- a/src/HOL/UNITY/WFair.ML Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML Fri Jul 31 18:46:55 1998 +0200
@@ -8,12 +8,6 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-open WFair;
-
-Goal "Union(B) Int A = Union((%C. C Int A)``B)";
-by (Blast_tac 1);
-qed "Int_Union_Union";
-
(*** transient ***)
@@ -121,7 +115,7 @@
\ ==> P A C; \
\ !!B S. ALL A:S. leadsTo Acts A B & P A B ==> P (Union S) B \
\ |] ==> P za zb";
-br (major RS leadsto.induct) 1;
+by (rtac (major RS leadsto.induct) 1);
by (REPEAT (blast_tac (claset() addIs prems) 1));
qed "leadsTo_induct";