--- a/src/HOL/UNITY/Alloc.ML Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML Fri Sep 10 18:40:06 1999 +0200
@@ -214,25 +214,33 @@
Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
by (res_inst_tac
- [("X", "(INT i : lessThan Nclients. (sub i o allocRel) localTo Network \
-\ Int Increasing (sub i o allocRel))")]
- component_guaranteesD 1);;
+ [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")]
+ component_guaranteesD 1);
by (rtac Alloc_component_System 3);
+by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
by (rtac project_guarantees 1);
by (rtac Alloc_Safety 1);
+by Auto_tac;
+by (rtac project_Increasing_I 1);
+
by (dtac (alloc_export (project_extend_Join RSN (2, subst_elem RS project_Always_D))) 2
THEN
full_simp_tac
(simpset() addsimps [inv_sysOfAlloc_eq,
alloc_export Collect_eq_extend_set RS sym]) 2);
by Auto_tac;
-by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 3);
by (dtac bspec 1);
by (Blast_tac 1);
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
+FIRST STEP WAS
+by (res_inst_tac
+ [("X", "(INT i : lessThan Nclients. (sub i o allocRel) localTo Network \
+\ Int Increasing (sub i o allocRel))")]
+ component_guaranteesD 1);
+
[| i < Nclients;
extend sysOfAlloc Alloc Join G
--- a/src/HOL/UNITY/Alloc.thy Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Alloc.thy Fri Sep 10 18:40:06 1999 +0200
@@ -4,6 +4,10 @@
Copyright 1998 University of Cambridge
Specification of Chandy and Charpentier's Allocator
+
+CONSIDER CHANGING "sum" to work on type "int", not "nat"
+ --then can use subtraction in spec (1),
+ --but need invariants that values are non-negative
*)
Alloc = Follows + Extend + PPROD +
--- a/src/HOL/UNITY/Client.ML Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Client.ML Fri Sep 10 18:40:06 1999 +0200
@@ -90,7 +90,7 @@
\ size (rel s) = k & ask s ! k <= giv s ! k}";
by (res_inst_tac [("act", "rel_act")] transient_mem 1);
by (auto_tac (claset(),
- simpset() addsimps [Domain_def, Acts_Join, Cli_prg_def]));
+ simpset() addsimps [Domain_def, Cli_prg_def]));
qed "transient_lemma";
--- a/src/HOL/UNITY/Common.thy Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Common.thy Fri Sep 10 18:40:06 1999 +0200
@@ -10,7 +10,7 @@
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
*)
-Common = SubstAx + Union +
+Common = Union +
consts
ftime,gtime :: nat=>nat
--- a/src/HOL/UNITY/Comp.ML Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML Fri Sep 10 18:40:06 1999 +0200
@@ -21,7 +21,7 @@
Goalw [component_def]
"(F <= G) = (Init G <= Init F & Acts F <= Acts G)";
by (force_tac (claset() addSIs [exI, program_equalityI],
- simpset() addsimps [Acts_Join]) 1);
+ simpset()) 1);
qed "component_eq_subset";
Goalw [component_def] "SKIP <= F";
@@ -67,7 +67,7 @@
qed "component_eq";
Goal "((F Join G) <= H) = (F <= H & G <= H)";
-by (simp_tac (simpset() addsimps [component_eq_subset, Acts_Join]) 1);
+by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
by (Blast_tac 1);
qed "Join_component_iff";
--- a/src/HOL/UNITY/Extend.ML Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML Fri Sep 10 18:40:06 1999 +0200
@@ -10,6 +10,14 @@
(** These we prove OUTSIDE the locale. **)
+
+(****************UNITY.ML****************)
+Goalw [stable_def, constrains_def] "stable UNIV = UNIV";
+by Auto_tac;
+qed "stable_UNIV";
+Addsimps [stable_UNIV];
+
+
(*Possibly easier than reasoning about "inv h"*)
val [surj_h,prem] =
Goalw [good_map_def]
@@ -76,7 +84,8 @@
by Auto_tac;
qed "Collect_eq_extend_set";
-Goalw [extend_set_def, project_set_def] "project_set h (extend_set h F) = F";
+Goalw [extend_set_def, project_set_def]
+ "project_set h (extend_set h F) = F";
by Auto_tac;
qed "extend_set_inverse";
Addsimps [extend_set_inverse];
@@ -153,16 +162,18 @@
by Auto_tac;
qed "extend_act_D";
-Goalw [extend_act_def, project_act_def]
- "project_act h (extend_act h act) = act";
-by Auto_tac;
-by (Blast_tac 1);
+(*Premise is still undesirably strong, since Domain act can include
+ non-reachable states, but it seems necessary for this result.*)
+Goalw [extend_act_def,project_set_def, project_act_def]
+ "Domain act <= project_set h C ==> project_act C h (extend_act h act) = act";
+by (Force_tac 1);
qed "extend_act_inverse";
Addsimps [extend_act_inverse];
Goal "inj (extend_act h)";
by (rtac inj_on_inverseI 1);
by (rtac extend_act_inverse 1);
+by (force_tac (claset(), simpset() addsimps [project_set_def]) 1);
qed "inj_extend_act";
Goalw [extend_set_def, extend_act_def]
@@ -188,18 +199,21 @@
qed "extend_act_Id";
Goalw [project_act_def]
- "(z, z') : act ==> (f z, f z') : project_act h act";
+ "[| (z, z') : act; f z = f z' | z: C |] \
+\ ==> (f z, f z') : project_act C h act";
by (auto_tac (claset() addSIs [exI] addIs [h_f_g_eq RS ssubst],
simpset()));
qed "project_act_I";
Goalw [project_set_def, project_act_def]
- "project_act h Id = Id";
+ "project_act C h Id = Id";
by (Force_tac 1);
qed "project_act_Id";
+(*premise can be weakened*)
Goalw [project_set_def, project_act_def]
- "Domain (project_act h act) = project_set h (Domain act)";
+ "Domain act <= C \
+\ ==> Domain (project_act C h act) = project_set h (Domain act)";
by Auto_tac;
by (res_inst_tac [("y1", "ya")] (surj_h RS surjD RS exE) 1);
by Auto_tac;
@@ -221,7 +235,7 @@
by Auto_tac;
qed "Init_extend";
-Goalw [project_def] "Init (project h F) = project_set h (Init F)";
+Goalw [project_def] "Init (project C h F) = project_set h (Init F)";
by Auto_tac;
qed "Init_project";
@@ -230,7 +244,7 @@
simpset() addsimps [extend_def, image_iff]));
qed "Acts_extend";
-Goal "Acts (project h F) = (project_act h `` Acts F)";
+Goal "Acts (project C h F) = (project_act C h `` Acts F)";
by (auto_tac (claset() addSIs [project_act_Id RS sym],
simpset() addsimps [project_def, image_iff]));
qed "Acts_project";
@@ -242,16 +256,23 @@
by Auto_tac;
qed "extend_SKIP";
-Goalw [SKIP_def] "project h SKIP = SKIP";
+Goalw [SKIP_def] "project C h SKIP = SKIP";
by (rtac program_equalityI 1);
by (auto_tac (claset() addIs [h_f_g_eq RS sym],
simpset() addsimps [project_set_def]));
qed "project_SKIP";
-Goal "project h (extend h F) = F";
+Goalw [project_set_def] "UNIV <= project_set h UNIV";
+by Auto_tac;
+qed "project_set_UNIV";
+
+(*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
+Goal "UNIV <= project_set h C \
+\ ==> project C h (extend h F) = F";
by (simp_tac (simpset() addsimps [extend_def, project_def]) 1);
by (rtac program_equalityI 1);
-by (simp_tac (simpset() addsimps [image_compose RS sym, o_def]) 2);
+by (asm_simp_tac (simpset() addsimps [image_image_eq_UN,
+ subset_UNIV RS subset_trans RS extend_act_inverse]) 2);
by (Simp_tac 1);
qed "extend_inverse";
Addsimps [extend_inverse];
@@ -259,33 +280,35 @@
Goal "inj (extend h)";
by (rtac inj_on_inverseI 1);
by (rtac extend_inverse 1);
+by (force_tac (claset(), simpset() addsimps [project_set_def]) 1);
qed "inj_extend";
Goal "extend h (F Join G) = extend h F Join extend h G";
by (rtac program_equalityI 1);
-by (simp_tac (simpset() addsimps [image_Un, Acts_Join]) 2);
+by (simp_tac (simpset() addsimps [image_Un]) 2);
by (simp_tac (simpset() addsimps [extend_set_Int_distrib]) 1);
qed "extend_Join";
Addsimps [extend_Join];
Goal "extend h (JOIN I F) = (JN i:I. extend h (F i))";
by (rtac program_equalityI 1);
-by (simp_tac (simpset() addsimps [image_UN, Acts_JN]) 2);
+by (simp_tac (simpset() addsimps [image_UN]) 2);
by (simp_tac (simpset() addsimps [extend_set_INT_distrib]) 1);
qed "extend_JN";
Addsimps [extend_JN];
-Goal "project h ((extend h F) Join G) = F Join (project h G)";
+Goal "UNIV <= project_set h C \
+\ ==> project C h ((extend h F) Join G) = F Join (project C h G)";
by (rtac program_equalityI 1);
-by (simp_tac (simpset() addsimps [Acts_Join, image_Un,
- image_compose RS sym, o_def]) 2);
+by (asm_simp_tac (simpset() addsimps [image_Un, image_image_eq_UN,
+ subset_UNIV RS subset_trans RS extend_act_inverse]) 2);
by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
qed "project_extend_Join";
-Goal "(extend h F) Join G = extend h H ==> H = F Join (project h G)";
-by (dres_inst_tac [("f", "project h")] arg_cong 1);
-by (full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
-by (etac sym 1);
+Goal "UNIV <= project_set h C \
+\ ==> (extend h F) Join G = extend h H ==> H = F Join (project C h G)";
+by (dres_inst_tac [("f", "project C h")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
qed "extend_Join_eq_extend_D";
@@ -307,19 +330,28 @@
(** Safety and project **)
Goalw [constrains_def]
- "(project h F : A co B) = (F : (extend_set h A) co (extend_set h B))";
-by Auto_tac;
-by (force_tac (claset(), simpset() addsimps [project_act_def]) 2);
+ "(project C h F : A co B) = \
+\ (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
by (auto_tac (claset() addSIs [project_act_I], simpset()));
+by (rewtac project_act_def);
+by (force_tac (claset() addSDs [Id_in_Acts RSN (2,bspec)], simpset()) 1);
+(*the <== direction*)
+by (force_tac (claset() addSDs [subsetD], simpset()) 1);
qed "project_constrains";
-Goal "(project h F : stable A) = (F : stable (extend_set h A))";
-by (simp_tac (simpset() addsimps [stable_def, project_constrains]) 1);
+(*The condition is required to prove the left-to-right direction;
+ could weaken it to F : (C Int extend_set h A) co C*)
+Goalw [stable_def]
+ "F : stable C \
+\ ==> (project C h F : stable A) = (F : stable (C Int extend_set h A))";
+by (simp_tac (simpset() addsimps [project_constrains]) 1);
+by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
qed "project_stable";
-Goal "(project h F : increasing func) = (F : increasing (func o f))";
-by (simp_tac (simpset() addsimps [increasing_def, project_stable,
- Collect_eq_extend_set RS sym]) 1);
+Goal "(project UNIV h F : increasing func) = \
+\ (F : increasing (func o f))";
+by (asm_simp_tac (simpset() addsimps [increasing_def, project_stable,
+ Collect_eq_extend_set RS sym]) 1);
qed "project_increasing";
@@ -329,21 +361,32 @@
(*Opposite direction fails because Diff in the extended state may remove
fewer actions, i.e. those that affect other state variables.*)
-Goal "Diff (project h G) acts <= project h (Diff G (extend_act h `` acts))";
-by (force_tac (claset(),
- simpset() addsimps [component_eq_subset, Diff_def]) 1);
+Goal "(UN act:acts. Domain act) <= project_set h C \
+\ ==> Diff (project C h G) acts <= \
+\ project C h (Diff G (extend_act h `` acts))";
+by (asm_full_simp_tac (simpset() addsimps [component_eq_subset, Diff_def,
+ UN_subset_iff]) 1);
+by (force_tac (claset() addSIs [image_diff_subset RS subsetD],
+ simpset() addsimps [image_image_eq_UN]) 1);
qed "Diff_project_component_project_Diff";
-Goal "Diff G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) \
-\ ==> Diff (project h G) acts : A co B";
-by (rtac (Diff_project_component_project_Diff RS component_constrains) 1);
-by (etac (project_constrains RS iffD2) 1);
+Goal
+ "[| (UN act:acts. Domain act) <= project_set h C; \
+\ Diff G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) |]\
+\ ==> Diff (project C h G) acts : A co B";
+by (etac (Diff_project_component_project_Diff RS component_constrains) 1);
+by (rtac (project_constrains RS iffD2) 1);
+by (ftac constrains_imp_subset 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "Diff_project_co";
Goalw [stable_def]
- "Diff G (extend_act h `` acts) : stable (extend_set h A) \
-\ ==> Diff (project h G) acts : stable A";
+ "[| (UN act:acts. Domain act) <= project_set h C; \
+\ Diff G (extend_act h `` acts) : stable (extend_set h A) |] \
+\ ==> Diff (project C h G) acts : stable A";
by (etac Diff_project_co 1);
+by (assume_tac 1);
qed "Diff_project_stable";
(** extend versions **)
@@ -351,8 +394,7 @@
Goal "(Diff (extend h G) (extend_act h `` acts)) = extend h (Diff G acts)";
by (auto_tac (claset() addSIs [program_equalityI],
simpset() addsimps [Diff_def,
- inj_extend_act RS image_set_diff RS sym,
- image_compose RS sym, o_def]));
+ inj_extend_act RS image_set_diff RS sym]));
qed "Diff_extend_eq";
Goal "(Diff (extend h G) (extend_act h `` acts) \
@@ -367,11 +409,12 @@
qed "Diff_extend_stable";
(*Converse appears to fail*)
-Goal "(H : (func o f) localTo extend h G) ==> (project h H : func localTo G)";
+Goal "[| UNIV <= project_set h C; (H : (func o f) localTo extend h G) |] \
+\ ==> (project C h H : func localTo G)";
by (asm_full_simp_tac
(simpset() addsimps [localTo_def,
project_extend_Join RS sym,
- Diff_project_stable,
+ subset_UNIV RS subset_trans RS Diff_project_stable,
Collect_eq_extend_set RS sym]) 1);
qed "project_localTo_I";
@@ -419,7 +462,8 @@
(** Reachability and project **)
-Goal "z : reachable F ==> f z : reachable (project h F)";
+Goal "[| reachable F <= C; z : reachable F |] \
+\ ==> f z : reachable (project C h F)";
by (etac reachable.induct 1);
by (force_tac (claset() addIs [reachable.Acts, project_act_I],
simpset()) 2);
@@ -427,38 +471,104 @@
simpset()) 1);
qed "reachable_imp_reachable_project";
-(*Converse fails (?) *)
Goalw [Constrains_def]
- "project h F : A Co B ==> F : (extend_set h A) Co (extend_set h B)";
+ "[| reachable F <= C; project C h F : A Co B |] \
+\ ==> F : (extend_set h A) Co (extend_set h B)";
by (full_simp_tac (simpset() addsimps [project_constrains]) 1);
+by (Clarify_tac 1);
by (etac constrains_weaken_L 1);
by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset()));
qed "project_Constrains_D";
-Goalw [Stable_def] "project h F : Stable A ==> F : Stable (extend_set h A)";
+Goalw [Stable_def]
+ "[| reachable F <= C; project C h F : Stable A |] \
+\ ==> F : Stable (extend_set h A)";
by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
qed "project_Stable_D";
-Goalw [Always_def] "project h F : Always A ==> F : Always (extend_set h A)";
+Goalw [Always_def]
+ "[| reachable F <= C; project C h F : Always A |] \
+\ ==> F : Always (extend_set h A)";
by (force_tac (claset() addIs [reachable.Init, project_set_I],
simpset() addsimps [project_Stable_D]) 1);
qed "project_Always_D";
Goalw [Increasing_def]
- "project h F : Increasing func ==> F : Increasing (func o f)";
+ "[| reachable F <= C; project C h F : Increasing func |] \
+\ ==> F : Increasing (func o f)";
by Auto_tac;
by (stac Collect_eq_extend_set 1);
by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1);
qed "project_Increasing_D";
-(*NOT useful in its own right, but a guarantees rule likes premises
- in this form*)
-Goal "F Join project h G : A Co B \
-\ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
-by (asm_simp_tac
- (simpset() addsimps [project_extend_Join, project_Constrains_D]) 1);
-qed "extend_Join_Constrains";
+
+(** Converse results for weak safety: benefits of the argument C *)
+
+Goal "[| C <= reachable F; x : reachable (project C h F) |] \
+\ ==> EX y. h(x,y) : reachable F";
+by (etac reachable.induct 1);
+by (ALLGOALS
+ (asm_full_simp_tac
+ (simpset() addsimps [project_set_def, project_act_def])));
+by (force_tac (claset() addIs [reachable.Acts],
+ simpset() addsimps [project_act_def]) 2);
+by (force_tac (claset() addIs [reachable.Init],
+ simpset() addsimps [project_set_def]) 1);
+qed "reachable_project_imp_reachable";
+
+Goalw [Constrains_def]
+ "[| C <= reachable F; F : (extend_set h A) Co (extend_set h B) |] \
+\ ==> project C h F : A Co B";
+by (full_simp_tac (simpset() addsimps [project_constrains,
+ extend_set_Int_distrib]) 1);
+by (rtac conjI 1);
+by (force_tac (claset() addSDs [constrains_imp_subset,
+ reachable_project_imp_reachable],
+ simpset()) 2);
+by (etac constrains_weaken 1);
+by Auto_tac;
+qed "project_Constrains_I";
+
+Goalw [Stable_def]
+ "[| C <= reachable F; F : Stable (extend_set h A) |] \
+\ ==> project C h F : Stable A";
+by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
+qed "project_Stable_I";
+Goalw [Increasing_def]
+ "[| C <= reachable F; F : Increasing (func o f) |] \
+\ ==> project C h F : Increasing func";
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
+ project_Stable_I]) 1);
+qed "project_Increasing_I";
+
+Goal "(project (reachable F) h F : A Co B) = \
+\ (F : (extend_set h A) Co (extend_set h B))";
+by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1);
+qed "project_Constrains";
+
+Goalw [Stable_def]
+ "(project (reachable F) h F : Stable A) = \
+\ (F : Stable (extend_set h A))";
+by (rtac project_Constrains 1);
+qed "project_Stable";
+
+Goal "(project (reachable F) h F : Increasing func) = \
+\ (F : Increasing (func o f))";
+by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
+ Collect_eq_extend_set RS sym]) 1);
+qed "project_Increasing";
+
+(**
+ (*NOT useful in its own right, but a guarantees rule likes premises
+ in this form*)
+ Goal "F Join project C h G : A Co B \
+ \ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
+ by (asm_simp_tac
+ (simpset() addsimps [project_extend_Join, project_Constrains_D]) 1);
+ qed "extend_Join_Constrains";
+**)
(*** Progress: transient, ensures ***)
@@ -557,53 +667,14 @@
qed "extend_LeadsTo";
-(*** progress for (project h F) ***)
-
-Goal "F : transient (extend_set h A) ==> project h F : transient A";
-by (auto_tac (claset(),
- simpset() addsimps [transient_def, Domain_project_act]));
-by (rtac bexI 1);
-by (assume_tac 2);
-by (full_simp_tac (simpset() addsimps [extend_set_def, project_set_def,
- project_act_def]) 1);
-by (Blast_tac 1);
-qed "transient_extend_set_imp_project_transient";
-
-(*Converse of the above...it requires a strong assumption about actions
- being enabled for all possible values of the new variables.*)
-Goal "[| project h F : transient A; \
-\ ALL act: Acts F. extend_set h (project_set h (Domain act)) <= \
-\ Domain act |] \
-\ ==> F : transient (extend_set h A)";
-by (auto_tac (claset(),
- simpset() addsimps [transient_def, Domain_project_act]));
-by (rtac bexI 1);
-by (assume_tac 2);
-by Auto_tac;
-by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
-by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1);
-by (thin_tac "ALL act:?AA. ?P (act)" 1);
-by (force_tac (claset() addDs [project_act_I], simpset()) 1);
-qed "project_transient_imp_transient_extend_set";
-
-
-Goal "F : (extend_set h A) ensures (extend_set h B) \
-\ ==> project h F : A ensures B";
-by (asm_full_simp_tac
- (simpset() addsimps [ensures_def, project_constrains,
- transient_extend_set_imp_project_transient,
- extend_set_Un_distrib RS sym,
- extend_set_Diff_distrib RS sym]) 1);
-qed "ensures_extend_set_imp_project_ensures";
-
-
(** Strong precondition and postcondition; doesn't seem very useful. **)
Goal "F : X guarantees Y ==> \
\ extend h F : (extend h `` X) guarantees (extend h `` Y)";
by (rtac guaranteesI 1);
by Auto_tac;
-by (blast_tac (claset() addDs [extend_Join_eq_extend_D, guaranteesD]) 1);
+by (blast_tac (claset() addDs [project_set_UNIV RS extend_Join_eq_extend_D,
+ guaranteesD]) 1);
qed "guarantees_imp_extend_guarantees";
Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
@@ -624,11 +695,12 @@
qed "extend_guarantees_eq";
(*Weak precondition and postcondition; this is the good one!
- Not clear that it has a converse [or that we want one!] *)
+ Not clear that it has a converse [or that we want one!]
+ Can generalize project (C G) to the function variable "proj"*)
val [xguary,project,extend] =
Goal "[| F : X guarantees Y; \
-\ !!G. extend h F Join G : X' ==> F Join project h G : X; \
-\ !!G. F Join project h G : Y ==> extend h F Join G : Y' |] \
+\ !!G. extend h F Join G : X' ==> F Join project (C G) h G : X; \
+\ !!G. F Join project (C G) h G : Y ==> extend h F Join G : Y' |] \
\ ==> extend h F : X' guarantees Y'";
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
by (etac project 1);
@@ -642,16 +714,16 @@
Goal "F : UNIV guarantees increasing func \
\ ==> extend h F : UNIV guarantees increasing (func o f)";
by (etac project_guarantees 1);
-by (asm_simp_tac
- (simpset() addsimps [project_extend_Join, project_increasing RS sym]) 2);
+by (asm_simp_tac (simpset() addsimps [project_increasing RS sym]) 2);
+by (stac (project_set_UNIV RS project_extend_Join) 2);
by Auto_tac;
qed "extend_guar_increasing";
Goal "F : UNIV guarantees Increasing func \
\ ==> extend h F : UNIV guarantees Increasing (func o f)";
by (etac project_guarantees 1);
-by (asm_simp_tac
- (simpset() addsimps [project_extend_Join, project_Increasing_D]) 2);
+by (rtac (subset_UNIV RS project_Increasing_D) 2);
+by (stac (project_set_UNIV RS project_extend_Join) 2);
by Auto_tac;
qed "extend_guar_Increasing";
@@ -661,10 +733,13 @@
by (etac project_guarantees 1);
(*the "increasing" guarantee*)
by (asm_simp_tac
- (simpset() addsimps [project_extend_Join, project_increasing RS sym]) 2);
+ (simpset() addsimps [project_increasing RS sym]) 2);
+by (stac (project_set_UNIV RS project_extend_Join) 2);
+by (assume_tac 2);
(*the "localTo" requirement*)
+by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
by (asm_simp_tac
- (simpset() addsimps [project_localTo_I, project_extend_Join RS sym]) 1);
+ (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
qed "extend_localTo_guar_increasing";
Goal "F : (func localTo G) guarantees Increasing func \
@@ -672,11 +747,13 @@
\ guarantees Increasing (func o f)";
by (etac project_guarantees 1);
(*the "Increasing" guarantee*)
-by (asm_simp_tac
- (simpset() addsimps [project_extend_Join, project_Increasing_D]) 2);
+by (rtac (subset_UNIV RS project_Increasing_D) 2);
+by (stac (project_set_UNIV RS project_extend_Join) 2);
+by (assume_tac 2);
(*the "localTo" requirement*)
+by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
by (asm_simp_tac
- (simpset() addsimps [project_localTo_I, project_extend_Join RS sym]) 1);
+ (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
qed "extend_localTo_guar_Increasing";
Close_locale "Extend";
--- a/src/HOL/UNITY/Extend.thy Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy Fri Sep 10 18:40:06 1999 +0200
@@ -25,16 +25,18 @@
extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
"extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
- project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
- "project_act h act == {(x,x'). EX y y'. (h(x,y), h(x',y')) : act}"
+ project_act :: "['c set, 'a*'b => 'c, ('c*'c) set] => ('a*'a) set"
+ "project_act C h act ==
+ {(x,x'). EX y y'. (h(x,y), h(x',y')) : act &
+ (x = x' | h(x,y) : C)}"
extend :: "['a*'b => 'c, 'a program] => 'c program"
"extend h F == mk_program (extend_set h (Init F),
extend_act h `` Acts F)"
- project :: "['a*'b => 'c, 'c program] => 'a program"
- "project h F == mk_program (project_set h (Init F),
- project_act h `` Acts F)"
+ project :: "['c set, 'a*'b => 'c, 'c program] => 'a program"
+ "project C h F == mk_program (project_set h (Init F),
+ project_act C h `` Acts F)"
locale Extend =
fixes
--- a/src/HOL/UNITY/Guar.ML Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Guar.ML Fri Sep 10 18:40:06 1999 +0200
@@ -192,7 +192,7 @@
qed "guarantees_Join_Un";
Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)";
-by (simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1);
+by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
by (Blast_tac 1);
qed "JN_component_iff";
--- a/src/HOL/UNITY/Lift_prog.ML Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Fri Sep 10 18:40:06 1999 +0200
@@ -100,12 +100,12 @@
Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)";
by (rtac program_equalityI 1);
-by (auto_tac (claset(), simpset() addsimps [Acts_Join]));
+by Auto_tac;
qed "lift_prog_Join";
Goal "lift_prog i (JOIN J F) = (JN j:J. lift_prog i (F j))";
by (rtac program_equalityI 1);
-by (auto_tac (claset(), simpset() addsimps [Acts_JN]));
+by Auto_tac;
qed "lift_prog_JN";
Goal "drop_prog i SKIP = SKIP";
@@ -161,7 +161,7 @@
Goal "drop_prog i (lift_prog i F) = F";
by (simp_tac (simpset() addsimps [lift_prog_def, drop_prog_def]) 1);
by (rtac program_equalityI 1);
-by (simp_tac (simpset() addsimps [image_compose RS sym, o_def]) 2);
+by (simp_tac (simpset() addsimps [image_image_eq_UN]) 2);
by (Simp_tac 1);
qed "lift_prog_inverse";
Addsimps [lift_prog_inverse];
@@ -224,7 +224,7 @@
by (auto_tac (claset() addSIs [exI], simpset()));
qed "lift_act_correct";
-Goal "drop_act i = project_act (lift_map i)";
+Goal "drop_act i = project_act UNIV (lift_map i)";
by (rtac ext 1);
by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]);
by Auto_tac;
@@ -241,7 +241,7 @@
lift_act_correct]) 1);
qed "lift_prog_correct";
-Goal "drop_prog i F = project (lift_map i) F";
+Goal "drop_prog i F = project UNIV (lift_map i) F";
by (rtac program_equalityI 1);
by (simp_tac (simpset() addsimps [drop_set_correct]) 1);
by (simp_tac (simpset()
@@ -408,8 +408,7 @@
Goal "drop_prog i ((lift_prog i F) Join G) = F Join (drop_prog i G)";
by (rtac program_equalityI 1);
-by (simp_tac (simpset() addsimps [Acts_Join, image_Un,
- image_compose RS sym, o_def]) 2);
+by (simp_tac (simpset() addsimps [image_Un, image_image_eq_UN]) 2);
by (simp_tac (simpset() addsimps [drop_set_Int_lift_set]) 1);
qed "drop_prog_lift_prog_Join";
@@ -426,7 +425,7 @@
by (force_tac (claset() addIs [reachable.Init, drop_set_I], simpset()) 1);
(*By case analysis on whether the action is of lift_prog i F or G*)
by (force_tac (claset() addIs [reachable.Acts, drop_act_I],
- simpset() addsimps [Acts_Join, image_iff]) 1);
+ simpset() addsimps [image_iff]) 1);
qed "reachable_lift_prog_Join_D";
(*Opposite inclusion fails, even for the initial state: lift_set i includes
--- a/src/HOL/UNITY/PPROD.ML Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML Fri Sep 10 18:40:06 1999 +0200
@@ -19,7 +19,7 @@
Goal "Acts (PLam I F) = insert Id (UN i:I. lift_act i `` Acts (F i))";
by (auto_tac (claset(),
- simpset() addsimps [PLam_def, Acts_JN]));
+ simpset() addsimps [PLam_def]));
qed "Acts_PLam";
Goal "PLam {} F = SKIP";
@@ -140,19 +140,19 @@
by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
(*Init of F, action of PLam F case*)
by (rtac reachable.Acts 1);
-by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1);
+by (Force_tac 1);
by (assume_tac 1);
by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1);
(*induction over the 2nd "reachable" assumption*)
by (eres_inst_tac [("xa","f")] reachable.induct 1);
(*Init of PLam F, action of F case*)
by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1);
-by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1);
+by (Force_tac 1);
by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1);
(*last case: an action of PLam I F*)
by (rtac reachable.Acts 1);
-by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1);
+by (Force_tac 1);
by (assume_tac 1);
by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1);
qed_spec_mp "reachable_lift_Join_PLam";
@@ -185,7 +185,7 @@
simpset() addsimps [Constrains_def, Collect_conj_eq RS sym,
reachable_PLam_eq]));
by (auto_tac (claset(),
- simpset() addsimps [constrains_def, PLam_def, Acts_JN]));
+ simpset() addsimps [constrains_def, PLam_def]));
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
qed "Constrains_imp_PLam_Constrains";
--- a/src/HOL/UNITY/TimerArray.ML Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/TimerArray.ML Fri Sep 10 18:40:06 1999 +0200
@@ -9,10 +9,7 @@
Addsimps [Timer_def RS def_prg_Init];
program_defs_ref := [Timer_def];
-Goal "Timer : stable {0}";
-by (constrains_tac 1);
-qed "Timer_stable_zero";
-Addsimps [Timer_stable_zero];
+Addsimps [decr_def];
(*Demonstrates induction, but not used in the following proof*)
Goal "Timer : UNIV leadsTo {0}";
@@ -20,22 +17,22 @@
by (Simp_tac 1);
by (exhaust_tac "m" 1);
by (blast_tac (claset() addSIs [subset_imp_leadsTo]) 1);
-by (ensures_tac "range (%n. (Suc n, n))" 1);
-by (Blast_tac 1);
+by (ensures_tac "decr" 1);
qed "Timer_leadsTo_zero";
Goal "finite I ==> (plam i: I. Timer) : UNIV leadsTo {s. ALL i:I. s i = 0}";
by (eres_inst_tac [("A'1", "%i. lift_set i {0}")]
(finite_stable_completion RS leadsTo_weaken) 1);
by Auto_tac;
+by (constrains_tac 2);
by (res_inst_tac [("f", "sub i")] (allI RS lessThan_induct) 1);
by (exhaust_tac "m" 1);
by (auto_tac (claset() addIs [subset_imp_leadsTo],
simpset() addsimps [insert_absorb, lessThan_Suc RS sym]));
by (rename_tac "n" 1);
-br PLam_leadsTo_Basis 1;
+by (rtac PLam_leadsTo_Basis 1);
by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
by (constrains_tac 1);
-by (res_inst_tac [("act", "range (%n. (Suc n, n))")] transient_mem 1);
+by (res_inst_tac [("act", "decr")] transient_mem 1);
by (auto_tac (claset(), simpset() addsimps [Timer_def]));
qed "TimerArray_leadsTo_zero";
--- a/src/HOL/UNITY/TimerArray.thy Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/TimerArray.thy Fri Sep 10 18:40:06 1999 +0200
@@ -9,7 +9,10 @@
TimerArray = PPROD +
constdefs
+ decr :: "(nat*nat) set"
+ "decr == UN n. {(Suc n, n)}"
+
Timer :: nat program
- "Timer == mk_program (UNIV, {range(%n. (Suc n, n))})"
+ "Timer == mk_program (UNIV, {decr})"
end
--- a/src/HOL/UNITY/Union.ML Fri Sep 10 18:37:04 1999 +0200
+++ b/src/HOL/UNITY/Union.ML Fri Sep 10 18:40:06 1999 +0200
@@ -58,7 +58,7 @@
by (auto_tac (claset(), simpset() addsimps [Join_def]));
qed "Acts_Join";
-Addsimps [Init_Join];
+Addsimps [Init_Join, Acts_Join];
(** JN **)
@@ -82,7 +82,7 @@
by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
qed "Acts_JN";
-Addsimps [Init_JN];
+Addsimps [Init_JN, Acts_JN];
val prems = Goalw [JOIN_def]
"[| I=J; !!i. i:J ==> F i = G i |] ==> \
@@ -139,23 +139,19 @@
(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
Goal "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)";
-by (auto_tac (claset() addSIs [program_equalityI],
- simpset() addsimps [Acts_JN, Acts_Join]));
+by (auto_tac (claset() addSIs [program_equalityI], simpset()));
qed "JN_absorb";
Goal "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))";
-by (auto_tac (claset() addSIs [program_equalityI],
- simpset() addsimps [Acts_JN, Acts_Join]));
+by (auto_tac (claset() addSIs [program_equalityI], simpset()));
qed "JN_Un";
Goal "(JN i:I. c) = (if I={} then SKIP else c)";
-by (auto_tac (claset() addSIs [program_equalityI],
- simpset() addsimps [Acts_JN]));
+by (auto_tac (claset() addSIs [program_equalityI], simpset()));
qed "JN_constant";
Goal "(JN i:I. F i Join G i) = (JN i:I. F i) Join (JN i:I. G i)";
-by (auto_tac (claset() addSIs [program_equalityI],
- simpset() addsimps [Acts_JN, Acts_Join]));
+by (auto_tac (claset() addSIs [program_equalityI], simpset()));
qed "JN_Join_distrib";
Goal "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)";
@@ -268,7 +264,7 @@
by (full_simp_tac (simpset() addsimps [Always_def, invariant_def,
Stable_eq_stable, Join_stable]) 1);
by (force_tac(claset() addIs [stable_reachable, stable_Int],
- simpset() addsimps [Acts_Join]) 1);
+ simpset()) 1);
qed "stable_Join_Always";
Goal "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B";
@@ -300,7 +296,7 @@
\ ==> G : (INT z. stable {s. v s = z})";
by (asm_full_simp_tac
(simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
- Acts_Join, stable_def, constrains_def]) 1);
+ stable_def, constrains_def]) 1);
by (Blast_tac 1);
qed "localTo_imp_stable";
@@ -308,7 +304,7 @@
\ act : Acts G; Disjoint F G |] ==> v s' = v s";
by (asm_full_simp_tac
(simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
- Acts_Join, stable_def, constrains_def]) 1);
+ stable_def, constrains_def]) 1);
by (Blast_tac 1);
qed "localTo_imp_equals";
@@ -326,7 +322,7 @@
\ F Join G : w localTo F; \
\ Disjoint F G |] \
\ ==> F Join G : {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
-by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
+by (auto_tac (claset(), simpset() addsimps [constrains_def]));
by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
by Auto_tac;
qed "constrains_localTo_constrains2";