--- a/src/HOL/UNITY/Alloc.ML Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Alloc.ML Tue Dec 21 15:03:02 1999 +0100
@@ -28,8 +28,8 @@
handle THM _ => (list_of_Int (th RS INT_D))
handle THM _ => [th];
+(*useful??*)
val lessThanBspec = lessThan_iff RS iffD2 RSN (2, bspec);
-
fun normalize th =
normalize (th RS spec
handle THM _ => th RS lessThanBspec
@@ -223,8 +223,7 @@
alloc_progress_def, alloc_preserves_def] Alloc;
val [Alloc_Increasing, Alloc_Safety,
- Alloc_Progress, Alloc_preserves] =
- map normalize (list_of_Int Alloc_Spec);
+ Alloc_Progress, Alloc_preserves] = list_of_Int Alloc_Spec;
fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset());
@@ -283,14 +282,21 @@
AddIffs [extend_sysOfClient_preserves_o_client];
-(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
+(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing
+ (the form changes slightly, though, removing the INT) *)
Goal "i < Nclients \
\ ==> extend sysOfAlloc Alloc : \
\ UNIV guarantees[allocGiv] Increasing (sub i o allocGiv)";
-by (dtac (Alloc_Increasing RS alloc_export extend_guar_Increasing) 1);
-by (auto_tac (claset(), simpset() addsimps [o_def]));
+(* Alternative is something like
+by (dtac (Alloc_Increasing RS (guarantees_INT_right_iff RS iffD1)
+ RS lessThanBspec RS alloc_export extend_guar_Increasing) 1);
+*)
+by (cut_facts_tac [Alloc_Increasing] 1);
+by (auto_tac (claset() addSDs [alloc_export extend_guar_Increasing],
+ simpset() addsimps [guarantees_INT_right_iff, o_def]));
qed "extend_Alloc_Increasing_allocGiv";
+
Goalw [System_def]
"i < Nclients ==> System : Increasing (sub i o allocGiv)";
by (rtac (extend_Alloc_Increasing_allocGiv RS
@@ -393,25 +399,31 @@
by (etac (System_Follows_rel RS Follows_Increasing1) 1);
qed "System_Increasing_allocRel";
+(*NEED AUTOMATIC PROPAGATION of Alloc_Safety. The text is identical.*)
+Goal "extend sysOfAlloc Alloc : \
+\ (INT i : lessThan Nclients. Increasing (sub i o allocRel)) \
+\ guarantees[allocGiv] \
+\ Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
+\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
+by (rtac (Alloc_Safety RS alloc_export project_guarantees) 1);
+(*2: Always postcondition*)
+by (rtac ((alloc_export extending_Always RS extending_weaken)) 2);
+(*1: Increasing precondition*)
+by (rtac (alloc_export projecting_Increasing RS projecting_weaken RS
+ projecting_INT) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
+ o_def]));
+qed "extend_Alloc_Safety";
+
(*safety (1), step 3*)
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. 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 (Alloc_Safety RS alloc_export project_guarantees) 1);
-(*1: Increasing precondition*)
-by (rtac (alloc_export projecting_Increasing RS projecting_weaken RS
- projecting_INT) 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [o_def]) 1);
-(*2: Always postcondition*)
-by (rtac ((alloc_export extending_Always RS extending_weaken)) 1);
-by (auto_tac (claset(),
- simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
- o_def]));
+by (rtac (extend_Alloc_Safety RS component_guaranteesD) 1);
+by (rtac Alloc_component_System 2);
+(*preserves*)
+by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
+by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 1);
qed "System_sum_bounded";
(** Follows reasoning **)
@@ -545,7 +557,8 @@
by (rtac (client_export extending_LeadsETo RS extending_weaken RS
extending_INT) 1);
by (auto_tac (claset(),
- simpset() addsimps [o_apply, client_export Collect_eq_extend_set RS sym]));
+ simpset() addsimps [o_apply,
+ client_export Collect_eq_extend_set RS sym]));
qed "System_Client_Progress";
val lemma =
@@ -586,6 +599,57 @@
by (rtac (impOfSubs LeadsETo_subset_LeadsTo) 2);
by (cut_facts_tac [System_Client_Progress] 2);
by (Force_tac 2);
-by (simp_tac (simpset() addsimps [Collect_conj_eq]) 1);
by (etac lemma3 1);
qed "System_Alloc_Progress";
+
+
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
+
+(*NEED AUTOMATIC PROPAGATION of Alloc_Progress. The text is identical.*)
+Goal "extend sysOfAlloc Alloc : \
+\ (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int \
+\ Increasing (sub i o allocRel)) \
+\ Int \
+\ Always {s. ALL i : lessThan Nclients. \
+\ ALL k : lessThan (length (allocAsk s i)). \
+\ allocAsk s i ! k <= NbT} \
+\ Int \
+\ (INT i : lessThan Nclients. \
+\ INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} \
+\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s}) \
+\ guarantees[allocGiv] \
+\ (INT i : lessThan Nclients. \
+\ INT h. {s. h <= (sub i o allocAsk) s} \
+ \ LeadsTo[givenBy allocGiv] \
+\ {s. h pfixLe (sub i o allocGiv) s})";
+by (rtac (Alloc_Progress RS alloc_export project_guarantees) 1);
+(*preserves*)
+by (simp_tac (simpset() addsimps [o_def]) 3);
+(*2: LeadsTo postcondition*)
+by (rtac (extending_INT RS extending_INT) 2);
+by (rtac ((alloc_export extending_LeadsETo RS extending_weaken)) 2);
+by (rtac subset_refl 3);
+by (simp_tac (simpset() addsimps [o_def]) 3);
+by (simp_tac (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
+ o_def]) 2);
+(*1: Increasing precondition*)
+by (rtac (alloc_export projecting_Increasing RS projecting_weaken RS
+ projecting_INT) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
+ o_def]));
+qed "extend_Alloc_Progress";
+
+
+(*progress (2), step 9*)
+Goal
+ "System : (INT i : lessThan Nclients. \
+\ INT h. {s. h <= (sub i o allocAsk) s} \
+\ LeadsTo {s. h pfixLe (sub i o allocGiv) s})";
+by (res_inst_tac
+ [("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 (Alloc_Safety RS alloc_export project_guarantees) 1);
+
--- a/src/HOL/UNITY/Alloc.thy Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Alloc.thy Tue Dec 21 15:03:02 1999 +0100
@@ -131,7 +131,8 @@
LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})
guarantees[allocGiv]
(INT i : lessThan Nclients.
- INT h. {s. h <= (sub i o allocAsk) s} LeadsTo
+ INT h. {s. h <= (sub i o allocAsk) s}
+ LeadsTo[givenBy allocGiv]
{s. h pfixLe (sub i o allocGiv) s})"
(*spec: preserves part*)
--- a/src/HOL/UNITY/Constrains.ML Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Constrains.ML Tue Dec 21 15:03:02 1999 +0100
@@ -24,11 +24,13 @@
by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
qed "stable_reachable";
+AddSIs [stable_reachable];
+Addsimps [stable_reachable];
(*The set of all reachable states is an invariant...*)
Goal "F : invariant (reachable F)";
by (simp_tac (simpset() addsimps [invariant_def]) 1);
-by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
+by (blast_tac (claset() addIs reachable.intrs) 1);
qed "invariant_reachable";
(*...in fact the strongest invariant!*)
@@ -194,7 +196,7 @@
qed "ball_Stable_INT";
Goal "F : Stable (reachable F)";
-by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1);
+by (simp_tac (simpset() addsimps [Stable_eq_stable]) 1);
qed "Stable_reachable";
@@ -291,7 +293,6 @@
Goal "Always A = (UN I: Pow A. invariant I)";
by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable,
- stable_reachable,
impOfSubs invariant_includes_reachable]) 1);
qed "Always_eq_UN_invariant";
--- a/src/HOL/UNITY/ELT.ML Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/ELT.ML Tue Dec 21 15:03:02 1999 +0100
@@ -26,7 +26,7 @@
qed "givenBy_eq_Collect";
val prems =
-Goal "(!!x y. [| x:A; v x = v y |] ==> y: A) ==> A: givenBy v";
+Goal "(!!x y. [| x:A; v x = v y |] ==> y: A) ==> A: givenBy v";
by (stac givenBy_eq_all 1);
by (blast_tac (claset() addIs prems) 1);
qed "givenByI";
@@ -63,6 +63,11 @@
givenBy_eq_Collect]) 1);
qed "preserves_givenBy_imp_stable";
+Goal "givenBy (w o v) <= givenBy v";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_o_subset";
+
(** Standard leadsTo rules **)
@@ -380,7 +385,7 @@
(*Postcondition can be strengthened to (reachable F Int B) *)
Goal "F : A ensures B ==> F : (reachable F Int A) ensures B";
by (rtac (stable_ensures_Int RS ensures_weaken_R) 1);
-by (auto_tac (claset(), simpset() addsimps [stable_reachable]));
+by Auto_tac;
qed "reachable_ensures";
Goal "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B";
@@ -388,8 +393,7 @@
by (stac Int_Union 3);
by (blast_tac (claset() addIs [leadsETo_UN]) 3);
by (blast_tac (claset() addDs [e_psp_stable2]
- addIs [leadsETo_Trans, stable_reachable,
- leadsETo_weaken_L]) 2);
+ addIs [leadsETo_Trans, leadsETo_weaken_L]) 2);
by (blast_tac (claset() addIs [reachable_ensures, leadsETo_Basis]) 1);
val lemma = result();
@@ -406,11 +410,15 @@
Open_locale "Extend";
-(*Here h and f are locale constants*)
-Goal "extend_set h `` (givenBy v) <= (givenBy (v o f))";
-by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by (Blast_tac 1);
-qed "extend_set_givenBy_subset";
+Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_o_eq_extend_set";
+
+Goal "givenBy f = range (extend_set h)";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_eq_extend_set";
Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
@@ -428,20 +436,19 @@
extend_set_Diff_distrib RS sym]) 1);
qed "leadsETo_imp_extend_leadsETo";
-(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
+(*MOVE to Extend.ML?*)
Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
-by (auto_tac (claset() addIs [project_set_I],
- simpset()));
+by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
qed "Int_extend_set_lemma";
-(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
+(*MOVE to extend.ML??*)
Goal "G : C co B ==> project h C G : project_set h C co project_set h B";
by (full_simp_tac (simpset() addsimps [constrains_def, project_def,
- project_act_def, project_set_def]) 1);
+ project_act_def]) 1);
by (Blast_tac 1);
qed "project_constrains_project_set";
-(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
+(*MOVE to extend.ML??*)
Goal "G : stable C ==> project h C G : stable (project_set h C)";
by (asm_full_simp_tac (simpset() addsimps [stable_def,
project_constrains_project_set]) 1);
@@ -518,18 +525,19 @@
\ ==> extend h F Join G : (C Int extend_set h A) \
\ leadsTo[(%D. C Int extend_set h D)``givenBy v] (extend_set h B)";
by (rtac (lemma RS leadsETo_weaken) 1);
-by (auto_tac (claset() addIs [project_set_I], simpset()));
-qed "project_leadsETo_lemma";
+by (auto_tac (claset(),
+ simpset() addsimps [split_extended_all]));
+qed "project_leadsETo_D_lemma";
Goal "[| F Join project h UNIV G : A leadsTo[givenBy v] B; \
\ G : preserves (v o f) |] \
\ ==> extend h F Join G : (extend_set h A) \
\ leadsTo[givenBy (v o f)] (extend_set h B)";
-by (rtac (make_elim project_leadsETo_lemma) 1);
+by (rtac (make_elim project_leadsETo_D_lemma) 1);
by (stac stable_UNIV 1);
by Auto_tac;
by (etac leadsETo_givenBy 1);
-by (rtac extend_set_givenBy_subset 1);
+by (rtac (givenBy_o_eq_extend_set RS equalityD2) 1);
qed "project_leadsETo_D";
Goal "[| F Join project h (reachable (extend h F Join G)) G \
@@ -538,7 +546,7 @@
\ ==> extend h F Join G : \
\ (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)";
by (rtac (make_elim (subset_refl RS stable_reachable RS
- project_leadsETo_lemma)) 1);
+ project_leadsETo_D_lemma)) 1);
by (auto_tac (claset(),
simpset() addsimps [LeadsETo_def]));
by (asm_full_simp_tac
@@ -563,6 +571,133 @@
qed "extending_LeadsETo";
+(*** leadsETo in the precondition ***)
+
+Goalw [transient_def]
+ "[| G : transient (C Int extend_set h A); G : stable C |] \
+\ ==> project h C G : transient (project_set h C Int A)";
+by (auto_tac (claset(), simpset() addsimps [Domain_project_act]));
+by (subgoal_tac "act ^^ (C Int extend_set h A) <= - extend_set h A" 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [stable_def, constrains_def]) 2);
+by (Blast_tac 2);
+(*back to main goal*)
+by (thin_tac "?AA <= -C Un ?BB" 1);
+by (ball_tac 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [extend_set_def, project_act_def]) 1);
+by (Blast_tac 1);
+qed "transient_extend_set_imp_project_transient";
+
+(*converse might hold too?*)
+Goalw [transient_def]
+ "project h C (extend h F) : transient (project_set h C Int D) \
+\ ==> F : transient (project_set h C Int D)";
+by (auto_tac (claset(), simpset() addsimps [Domain_project_act]));
+by (rtac bexI 1);
+by (assume_tac 2);
+by Auto_tac;
+by (rewtac extend_act_def);
+by (Blast_tac 1);
+qed "project_extend_transient_D";
+
+
+Goal "[| extend h F : stable C; G : stable C; \
+\ extend h F Join G : A ensures B; A-B = C Int extend_set h D |] \
+\ ==> F Join project h C G \
+\ : (project_set h C Int project_set h A) ensures (project_set h B)";
+by (asm_full_simp_tac
+ (simpset() addsimps [ensures_def, Join_constrains, project_constrains,
+ Join_transient, extend_transient]) 1);
+by (Clarify_tac 1);
+by (REPEAT_FIRST (rtac conjI));
+(*first subgoal*)
+by (blast_tac (claset() addIs [extend_stable_project_set RS stableD RS
+ constrains_Int RS constrains_weaken]
+ addSDs [extend_constrains_project_set]
+ addSEs [equalityE]) 1);
+(*2nd subgoal*)
+by (etac (stableD RS constrains_Int RS constrains_weaken) 1);
+by (assume_tac 1);
+by (Blast_tac 3);
+by (full_simp_tac (simpset() addsimps [extend_set_Int_distrib,
+ extend_set_Un_distrib]) 2);
+by (blast_tac (claset() addSIs [impOfSubs extend_set_project_set]) 2);
+by (full_simp_tac (simpset() addsimps [extend_set_def]) 1);
+by (blast_tac (claset() addSEs [equalityE]) 1);
+(*The transient part*)
+by Auto_tac;
+by (force_tac (claset() addSEs [equalityE]
+ addIs [transient_extend_set_imp_project_transient RS
+ transient_strengthen],
+ simpset()) 2);
+by (full_simp_tac (simpset() addsimps [Int_Diff]) 1);
+by (force_tac (claset() addSEs [equalityE]
+ addIs [transient_extend_set_imp_project_transient RS
+ project_extend_transient_D RS transient_strengthen],
+ simpset()) 1);
+qed "ensures_extend_set_imp_project_ensures";
+
+
+(*Lemma for the Trans case*)
+Goal "[| extend h F Join G : stable C; \
+\ F Join project h C G \
+\ : project_set h C Int project_set h A leadsTo project_set h B |] \
+\ ==> F Join project h C G \
+\ : project_set h C Int project_set h A leadsTo \
+\ project_set h C Int project_set h B";
+by (rtac (psp_stable2 RS leadsTo_weaken_L) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [project_stable_project_set, Join_stable,
+ extend_stable_project_set]));
+val lemma = result();
+
+Goal "[| extend h F Join G : stable C; \
+\ extend h F Join G : \
+\ (C Int A) leadsTo[(%D. C Int D)``givenBy f] B |] \
+\ ==> F Join project h C G \
+\ : (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)";
+by (etac leadsETo_induct 1);
+by (asm_simp_tac (HOL_ss addsimps [Int_UN_distrib, project_set_Union]) 3);
+by (blast_tac (claset() addIs [leadsTo_UN]) 3);
+by (blast_tac (claset() addIs [leadsTo_Trans, lemma]) 2);
+by (asm_full_simp_tac
+ (simpset() addsimps [givenBy_eq_extend_set, Join_stable]) 1);
+by (rtac leadsTo_Basis 1);
+by (blast_tac (claset() addIs [leadsTo_Basis,
+ ensures_extend_set_imp_project_ensures]) 1);
+
+qed "project_leadsETo_I_lemma";
+
+Goal "extend h F Join G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)\
+\ ==> F Join project h UNIV G : A leadsTo B";
+by (rtac (project_leadsETo_I_lemma RS leadsTo_weaken) 1);
+by Auto_tac;
+qed "project_leadsETo_I";
+
+Goal "extend h F Join G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B)\
+\ ==> F Join project h (reachable (extend h F Join G)) G \
+\ : A LeadsTo B";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def, LeadsETo_def]) 1);
+by (rtac (project_leadsETo_I_lemma RS leadsTo_weaken) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [project_set_reachable_extend_eq RS sym]));
+qed "project_LeadsETo_I";
+
+Goalw [projecting_def]
+ "projecting (%G. UNIV) h F \
+\ (extend_set h A leadsTo[givenBy f] extend_set h B) \
+\ (A leadsTo B)";
+by (force_tac (claset() addDs [project_leadsETo_I], simpset()) 1);
+qed "projecting_leadsTo";
+
+Goalw [projecting_def]
+ "projecting (%G. reachable (extend h F Join G)) h F \
+\ (extend_set h A LeadsTo[givenBy f] extend_set h B) \
+\ (A LeadsTo B)";
+by (force_tac (claset() addDs [project_LeadsETo_I], simpset()) 1);
+qed "projecting_LeadsTo";
+
Close_locale "Extend";
--- a/src/HOL/UNITY/Extend.ML Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Extend.ML Tue Dec 21 15:03:02 1999 +0100
@@ -94,6 +94,12 @@
(*** extend_set: basic properties ***)
+Goal "(x : project_set h C) = (EX y. h(x,y) : C)";
+by (simp_tac (simpset() addsimps [project_set_def]) 1);
+qed "project_set_iff";
+
+AddIffs [project_set_iff];
+
Goalw [extend_set_def] "A<=B ==> extend_set h A <= extend_set h B";
by (Blast_tac 1);
qed "extend_set_mono";
@@ -101,10 +107,10 @@
Goalw [extend_set_def] "z : extend_set h A = (f z : A)";
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1);
qed "mem_extend_set_iff";
-AddIffs [mem_extend_set_iff];
-Goalw [extend_set_def]
- "(extend_set h A <= extend_set h B) = (A <= B)";
+AddIffs [mem_extend_set_iff];
+
+Goalw [extend_set_def] "(extend_set h A <= extend_set h B) = (A <= B)";
by (Force_tac 1);
qed "extend_set_strict_mono";
AddIffs [extend_set_strict_mono];
@@ -117,13 +123,13 @@
by Auto_tac;
qed "extend_set_sing";
-Goalw [extend_set_def, project_set_def]
+Goalw [extend_set_def]
"project_set h (extend_set h C) = C";
by Auto_tac;
qed "extend_set_inverse";
Addsimps [extend_set_inverse];
-Goalw [extend_set_def, project_set_def]
+Goalw [extend_set_def]
"C <= extend_set h (project_set h C)";
by (auto_tac (claset(),
simpset() addsimps [split_extended_all]));
@@ -144,13 +150,13 @@
(*** project_set: basic properties ***)
(*project_set is simply image!*)
-Goalw [project_set_def] "project_set h C = f `` C";
+Goal "project_set h C = f `` C";
by (auto_tac (claset() addIs [f_h_eq RS sym],
simpset() addsimps [split_extended_all]));
qed "project_set_eq";
(*Converse appears to fail*)
-Goalw [project_set_def] "!!z. z : C ==> f z : project_set h C";
+Goal "!!z. z : C ==> f z : project_set h C";
by (auto_tac (claset(),
simpset() addsimps [split_extended_all]));
qed "project_set_I";
@@ -162,13 +168,11 @@
cannot generalize to
project_set h (A Int B) = project_set h A Int project_set h B
*)
-Goalw [project_set_def]
- "project_set h ((extend_set h A) Int B) = A Int (project_set h B)";
+Goal "project_set h ((extend_set h A) Int B) = A Int (project_set h B)";
by Auto_tac;
qed "project_set_extend_set_Int";
-Goalw [project_set_def]
- "project_set h (A Int B) <= (project_set h A) Int (project_set h B)";
+Goal "project_set h (A Int B) <= (project_set h A) Int (project_set h B)";
by Auto_tac;
qed "project_set_Int_subset";
@@ -211,25 +215,18 @@
by Auto_tac;
qed "extend_act_D";
-Goalw [extend_act_def, project_act_def, project_set_def]
+Goalw [extend_act_def, project_act_def]
"project_act h (extend_act h act) = act";
by (Blast_tac 1);
qed "project_act_extend_act";
-Goalw [extend_act_def, project_act_def, project_set_def]
+Goalw [extend_act_def, project_act_def]
"project_act h (Restrict C (extend_act h act)) = \
\ Restrict (project_set h C) act";
by (Blast_tac 1);
qed "project_act_extend_act_restrict";
Addsimps [project_act_extend_act_restrict];
-Goalw [extend_act_def, project_act_def, project_set_def]
- "(Restrict C (extend_act h act) = Restrict C (extend_act h act')) \
-\ = (Restrict (project_set h C) act = Restrict (project_set h C) act')";
-by Auto_tac;
-by (ALLGOALS (blast_tac (claset() addSEs [equalityE])));
-qed "Restrict_extend_act_eq_Restrict_project_act";
-
(*Premise is still undesirably strong, since Domain act can include
non-reachable states, but it seems necessary for this result.*)
Goal "Domain act <= project_set h C \
@@ -245,7 +242,7 @@
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);
+by (Force_tac 1);
qed "inj_extend_act";
Goalw [extend_set_def, extend_act_def]
@@ -277,12 +274,12 @@
simpset() addsimps [split_extended_all]) 1);
qed "project_act_I";
-Goalw [project_set_def, project_act_def]
+Goalw [project_act_def]
"UNIV <= project_set h C ==> project_act h (Restrict C Id) = Id";
by (Force_tac 1);
qed "project_act_Id";
-Goalw [project_set_def, project_act_def]
+Goalw [project_act_def]
"Domain (project_act h act) = project_set h (Domain act)";
by (force_tac (claset(),
simpset() addsimps [split_extended_all]) 1);
@@ -331,11 +328,16 @@
by Auto_tac;
qed "extend_SKIP";
-Goalw [project_set_def] "project_set h UNIV = UNIV";
+Goal "project_set h UNIV = UNIV";
by Auto_tac;
qed "project_set_UNIV";
Addsimps [project_set_UNIV];
+Goal "project_set h (Union A) = (UN X:A. project_set h X)";
+by (Blast_tac 1);
+qed "project_set_Union";
+
+
Goal "project h C (extend h F) = \
\ mk_program (Init F, Restrict (project_set h C) `` Acts F)";
by (rtac program_equalityI 1);
@@ -355,7 +357,7 @@
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);
+by (Force_tac 1);
qed "inj_extend";
Goal "extend h (F Join G) = extend h F Join extend h G";
@@ -381,8 +383,7 @@
qed "extend_mono";
Goal "F <= G ==> project h C F <= project h C G";
-by (full_simp_tac
- (simpset() addsimps [component_eq_subset, project_set_def]) 1);
+by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
by Auto_tac;
qed "project_mono";
@@ -404,8 +405,7 @@
(*Converse fails: A and B may differ in their extra variables*)
Goal "extend h F : A co B ==> F : (project_set h A) co (project_set h B)";
-by (auto_tac (claset(),
- simpset() addsimps [constrains_def, project_set_def]));
+by (auto_tac (claset(), simpset() addsimps [constrains_def]));
by (Force_tac 1);
qed "extend_constrains_project_set";
@@ -490,7 +490,7 @@
by Auto_tac;
qed "slice_extend_set";
-Goalw [slice_def, project_set_def] "project_set h A = (UN y. slice A y)";
+Goalw [slice_def] "project_set h A = (UN y. slice A y)";
by Auto_tac;
qed "project_set_is_UN_slice";
--- a/src/HOL/UNITY/Project.ML Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Project.ML Tue Dec 21 15:03:02 1999 +0100
@@ -101,14 +101,6 @@
by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
qed "Join_project_stable";
-Goal "(F Join project h UNIV G : increasing func) = \
-\ (extend h F Join G : increasing (func o f))";
-by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1);
-by (auto_tac (claset(),
- simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
- extend_stable RS iffD1]));
-qed "Join_project_increasing";
-
(*For using project_guarantees in particular cases*)
Goal "extend h F Join G : extend_set h A co extend_set h B \
\ ==> F Join project h C G : A co B";
@@ -119,6 +111,24 @@
addDs [constrains_imp_subset]) 1);
qed "project_constrains_I";
+Goalw [increasing_def, stable_def]
+ "extend h F Join G : increasing (func o f) \
+\ ==> F Join project h C G : increasing func";
+by (asm_full_simp_tac (simpset() addsimps [project_constrains_I,
+ Collect_eq_extend_set RS sym]) 1);
+qed "project_increasing_I";
+
+Goal "(F Join project h UNIV G : increasing func) = \
+\ (extend h F Join G : increasing (func o f))";
+by (rtac iffI 1);
+by (etac project_increasing_I 2);
+by (asm_full_simp_tac
+ (simpset() addsimps [increasing_def, Join_project_stable]) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
+ extend_stable RS iffD1]));
+qed "Join_project_increasing";
+
(*The UNIV argument is essential*)
Goal "F Join project h UNIV G : A co B \
\ ==> extend h F Join G : extend_set h A co extend_set h B";
@@ -127,7 +137,7 @@
extend_constrains]) 1);
qed "project_constrains_D";
-(** "projecting" and union/intersection **)
+(** "projecting" and union/intersection (no converses) **)
Goalw [projecting_def]
"[| projecting C h F XA' XA; projecting C h F XB' XB |] \
@@ -183,7 +193,9 @@
qed "extending_UN";
Goalw [extending_def]
- "[| extending v C h F Y' Y; Y'<=V'; V<=Y |] ==> extending v C h F V' V";
+ "[| extending v C h F Y' Y; Y'<=V'; V<=Y; \
+\ preserves w <= preserves v |] \
+\ ==> extending w C h F V' V";
by Auto_tac;
qed "extending_weaken";
@@ -202,8 +214,8 @@
qed "projecting_stable";
Goalw [projecting_def]
- "projecting (%G. UNIV) h F (increasing (func o f)) (increasing func)";
-by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
+ "projecting C h F (increasing (func o f)) (increasing func)";
+by (blast_tac (claset() addIs [project_increasing_I]) 1);
qed "projecting_increasing";
Goal "extending v C h F UNIV Y";
@@ -225,19 +237,6 @@
by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
qed "extending_increasing";
-(*UNUSED*)
-Goalw [project_set_def, project_act_def]
- "Restrict (project_set h C) (project_act h (Restrict C act)) = \
-\ project_act h (Restrict C act)";
-by (Blast_tac 1);
-qed "Restrict_project_act";
-
-(*UNUSED*)
-Goalw [project_set_def, project_act_def]
- "project_act h (Restrict C Id) = Restrict (project_set h C) Id";
-by (Blast_tac 1);
-qed "project_act_Restrict_Id";
-
(** Reachability and project **)
@@ -245,8 +244,8 @@
\ z : reachable (extend h F Join G) |] \
\ ==> f z : reachable (F Join project h C G)";
by (etac reachable.induct 1);
-by (force_tac (claset() addIs [reachable.Init, project_set_I],
- simpset()) 1);
+by (force_tac (claset() addSIs [reachable.Init],
+ simpset() addsimps [split_extended_all]) 1);
by Auto_tac;
by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)],
simpset()) 2);
@@ -279,8 +278,8 @@
"[| reachable (extend h F Join G) <= C; \
\ F Join project h C G : Always A |] \
\ ==> extend h F Join G : Always (extend_set h A)";
-by (force_tac (claset() addIs [reachable.Init, project_set_I],
- simpset() addsimps [project_Stable_D]) 1);
+by (force_tac (claset() addIs [reachable.Init],
+ simpset() addsimps [project_Stable_D, split_extended_all]) 1);
qed "project_Always_D";
Goalw [Increasing_def]
@@ -305,14 +304,14 @@
addIs [reachable.Acts, extend_act_D],
simpset() addsimps [project_act_def]) 2);
by (force_tac (claset() addIs [reachable.Init],
- simpset() addsimps [project_set_def]) 1);
+ simpset()) 1);
qed "reachable_project_imp_reachable";
Goal "project_set h (reachable (extend h F Join G)) = \
\ reachable (F Join project h (reachable (extend h F Join G)) G)";
by (auto_tac (claset() addDs [subset_refl RS reachable_imp_reachable_project,
subset_refl RS reachable_project_imp_reachable],
- simpset() addsimps [project_set_def]));
+ simpset()));
qed "project_set_reachable_extend_eq";
Goal "reachable (extend h F Join G) <= C \
@@ -353,7 +352,7 @@
\ extend h F Join G : Always (extend_set h A) |] \
\ ==> F Join project h C G : Always A";
by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
-by (rewrite_goals_tac [project_set_def, extend_set_def]);
+by (rewtac extend_set_def);
by (Blast_tac 1);
qed "project_Always_I";
@@ -454,8 +453,7 @@
simpset() addsimps [Domain_project_act, Int_absorb1]));
by (REPEAT (ball_tac 1));
by (auto_tac (claset(),
- simpset() addsimps [extend_set_def, project_set_def,
- project_act_def]));
+ simpset() addsimps [extend_set_def, project_act_def]));
by (ALLGOALS Blast_tac);
qed "transient_extend_set_imp_project_transient";
@@ -510,7 +508,7 @@
\ F Join project h C G : (project_set h C Int A) leadsTo B |] \
\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
by (rtac (lemma RS leadsTo_weaken) 1);
-by (auto_tac (claset() addIs [project_set_I], simpset()));
+by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
qed "project_leadsTo_lemma";
Goal "[| C = (reachable (extend h F Join G)); \
@@ -518,12 +516,11 @@
\ F Join project h C G : A LeadsTo B |] \
\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
by (asm_full_simp_tac
- (simpset() addsimps [LeadsTo_def, project_leadsTo_lemma, stable_reachable,
+ (simpset() addsimps [LeadsTo_def, project_leadsTo_lemma,
project_set_reachable_extend_eq]) 1);
qed "Join_project_LeadsTo";
-
(*** GUARANTEES and EXTEND ***)
(** preserves **)
@@ -647,7 +644,8 @@
qed "preserves_project_transient_empty";
-(** Guarantees with a leadsTo postcondition **)
+(** Guarantees with a leadsTo postcondition
+ THESE ARE ALL TOO WEAK because G can't affect F's variables at all**)
Goal "[| F Join project h UNIV G : A leadsTo B; \
\ G : preserves f |] \
--- a/src/HOL/UNITY/SubstAx.ML Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/SubstAx.ML Tue Dec 21 15:03:02 1999 +0100
@@ -12,8 +12,7 @@
(*Resembles the previous definition of LeadsTo*)
Goalw [LeadsTo_def]
"A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}";
-by (blast_tac (claset() addDs [psp_stable2]
- addIs [leadsTo_weaken, stable_reachable]) 1);
+by (blast_tac (claset() addDs [psp_stable2] addIs [leadsTo_weaken]) 1);
qed "LeadsTo_eq_leadsTo";
--- a/src/HOL/UNITY/UNITY.ML Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/UNITY.ML Tue Dec 21 15:03:02 1999 +0100
@@ -269,7 +269,7 @@
(** Intersection **)
Goalw [stable_def]
- "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')";
+ "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')";
by (blast_tac (claset() addIs [constrains_Int]) 1);
qed "stable_Int";
@@ -284,11 +284,11 @@
qed "stable_constrains_Un";
Goalw [stable_def, constrains_def]
- "[| F : stable C; F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')";
+ "[| F : stable C; F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')";
by (Blast_tac 1);
qed "stable_constrains_Int";
-(*[| F : stable C; F : co (C Int A) A |] ==> F : stable (C Int A)*)
+(*[| F : stable C; F : (C Int A) co A |] ==> F : stable (C Int A) *)
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
--- a/src/HOL/UNITY/Union.ML Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Union.ML Tue Dec 21 15:03:02 1999 +0100
@@ -274,8 +274,7 @@
Goal "[| F : stable A; G : invariant A |] ==> F Join G : Always A";
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()) 1);
+by (force_tac(claset() addIs [stable_Int], simpset()) 1);
qed "stable_Join_Always";
Goal "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B";