--- a/src/HOL/UNITY/Alloc.ML Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Alloc.ML Fri Jan 14 12:17:53 2000 +0100
@@ -380,8 +380,7 @@
qed "Always_tokens_allocRel_le_rel";
(*safety (1), step 4 (final result!) *)
-Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client)s) Nclients \
-\ <= NbT + sum (%i. (tokens o rel o sub i o client)s) Nclients}";
+Goalw [system_safety_def] "System : system_safety";
by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv,
Always_tokens_allocRel_le_rel] RS Always_weaken) 1);
by Auto_tac;
@@ -393,7 +392,6 @@
qed "System_safety";
-
(*** Proof of the progress property (2) ***)
(*Now there are proofs identical to System_Increasing_rel and
@@ -422,7 +420,7 @@
Goal "i < Nclients \
\ ==> System : Always \
\ {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
-br Always_weaken 1;
+by (rtac Always_weaken 1);
by (rtac ([guarantees_PLam_I RS client_export UNIV_guar_Always,
Client_component_System] MRS component_guaranteesD) 1);
by (rtac Client_i_Bounded 1);
@@ -463,11 +461,11 @@
\ (reachable (lift_prog i Client Join G) Int \
\ {s. h <= (giv o sub i) s & h pfixGe (ask o sub i) s} - \
\ {s. tokens h <= tokens ((rel o sub i) s)})";
-auto();
+by Auto_tac;
by (REPEAT (dres_inst_tac [("x", "rel (xa i)")] spec 2));
by (REPEAT (dres_inst_tac [("x", "ask (xa i)")] spec 1));
by (REPEAT_FIRST ball_tac);
-auto();
+by Auto_tac;
qed "G_stable_lift_prog";
Goal "lift_prog i Client \
@@ -477,12 +475,12 @@
\ h pfixGe (ask o sub i) s} \
\ Ensures {s. tokens h <= (tokens o rel o sub i) s})";
by (rtac (Client_Progress RS drop_prog_guarantees_raw) 1);
-br (lift_export (subset_refl RS project_Increasing_I)) 1;
+by (rtac (lift_export project_Increasing_I) 1);
by (full_simp_tac (simpset() addsimps [fold_o_sub, lift_prog_correct]) 1);
-br INT_I 1;
+by (rtac INT_I 1);
by (simp_tac (simpset() addsimps [o_apply]) 1);
by (REPEAT (stac (lift_export Collect_eq_extend_set) 1));
-br (lift_export project_Ensures_D) 1;
+by (rtac (lift_export project_Ensures_D) 1);
by (asm_full_simp_tac (simpset() addsimps [o_apply, lift_prog_correct,
drop_prog_correct]) 1);
by (asm_full_simp_tac
@@ -492,7 +490,7 @@
Collect_eq_lift_set RS sym,
lift_prog_correct RS sym]) 1);
by (Clarify_tac 1);
-bd G_stable_lift_prog 1;
+by (dtac G_stable_lift_prog 1);
by (auto_tac (claset(),
simpset() addsimps [o_apply]));
qed "Client_i_Progress";
@@ -505,7 +503,7 @@
\ h pfixGe (ask o sub i) s} \
\ Ensures {s. tokens h <= (tokens o rel o sub i) s})";
by (rtac guarantees_PLam_I 1);
-br Client_i_Progress 1;
+by (rtac Client_i_Progress 1);
by Auto_tac;
val lemma2 = result();
@@ -523,11 +521,11 @@
\ {s. h <= (giv o sub i o client) s & \
\ h pfixGe (ask o sub i o client) s} - \
\ {s. tokens h <= tokens ((rel o sub i o client) s)})";
-auto();
+by Auto_tac;
by (REPEAT (dres_inst_tac [("x", "rel (client xa i)")] spec 2));
by (REPEAT (dres_inst_tac [("x", "ask (client xa i)")] spec 1));
by (REPEAT_FIRST ball_tac);
-auto();
+by Auto_tac;
qed "G_stable_sysOfClient";
Goal "i < Nclients \
@@ -538,20 +536,20 @@
\ h pfixGe (ask o sub i o client) s} \
\ Ensures {s. tokens h <= (tokens o rel o sub i o client) s})";
by (rtac (lemma2 RS client_export project_guarantees_raw) 1);
-ba 1;
-br (client_export (subset_refl RS project_Increasing_I)) 1;
+by (assume_tac 1);
+by (rtac (client_export project_Increasing_I) 1);
by (Simp_tac 1);
-br INT_I 1;
+by (rtac INT_I 1);
by (simp_tac (simpset() addsimps [o_apply]) 1);
by (REPEAT (stac (client_export Collect_eq_extend_set) 1));
-br (client_export project_Ensures_D) 1;
+by (rtac (client_export project_Ensures_D) 1);
by (asm_full_simp_tac (simpset() addsimps [o_apply]) 1);
by (asm_full_simp_tac
(simpset() addsimps [all_conj_distrib,
Increasing_def, Stable_eq_stable, Join_stable,
Collect_eq_extend_set RS sym]) 1);
by (Clarify_tac 1);
-bd G_stable_sysOfClient 1;
+by (dtac G_stable_sysOfClient 1);
by (auto_tac (claset(),
simpset() addsimps [o_apply,
client_export Collect_eq_extend_set RS sym]));
@@ -570,7 +568,7 @@
Client_component_System] MRS component_guaranteesD) 1);
by (asm_full_simp_tac
(simpset() addsimps [System_Increasing_giv]) 2);
-auto();
+by Auto_tac;
qed "System_Client_Progress";
val lemma =
@@ -627,50 +625,24 @@
simpset() addsimps [System_Increasing_allocRel,
System_Increasing_allocAsk]));
by (rtac System_Bounded_allocAsk 1);
-by (etac System_Alloc_Progress 1);
+by (etac System_Alloc_Client_Progress 1);
qed "System_Alloc_Progress";
+(*progress (2), step 10 (final result!) *)
+Goalw [system_progress_def] "System : system_progress";
+by (Clarify_tac 1);
+by (rtac LeadsTo_Trans 1);
+by (etac (System_Follows_allocGiv RS Follows_LeadsTo_pfixLe) 2);
+by (rtac LeadsTo_Trans 1);
+by (cut_facts_tac [System_Alloc_Progress] 2);
+by (Blast_tac 2);
+by (etac (System_Follows_ask RS Follows_LeadsTo) 1);
+qed "System_Progress";
+
(*Ultimate goal*)
-Goal "System : system_spec";
-
-xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
-
-
-(*progress (2), step 10*)
-Goal
- "System : (INT i : lessThan Nclients. \
-\ INT h. {s. h <= (ask o sub i o client) s} \
-\ LeadsTo {s. h pfixLe (giv o sub i o client) s})";
-by (Clarify_tac 1);
-by (rtac LeadsTo_Trans 1);
-by (dtac (System_Follows_allocGiv RS Follows_LeadsTo) 2);
-by (blast_tac (claset() addIs [prefix_imp_pfixLe, LeadsTo_weaken_R]) 2);
-
-prefix_imp_pfixLe
-
-
-System_Follows_ask
+Goalw [system_spec_def] "System : system_spec";
+by (blast_tac (claset() addIs [System_safety, System_Progress]) 1);
+qed "System_correct";
-by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS
- Follows_LeadsTo) 2);
-
-by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
-by (rtac LeadsTo_Trans 1);
-by (cut_facts_tac [System_Client_Progress] 2);
-by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
-by (etac lemma3 1);
-
-by (rtac ([Alloc_Progress, Alloc_component_System]
- MRS component_guaranteesD) 1);
-(*preserves*)
-by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
-(*the guarantees precondition*)
-by (auto_tac (claset(),
- simpset() addsimps [System_Increasing_allocRel,
- System_Increasing_allocAsk]));
-by (rtac System_Bounded_allocAsk 1);
-by (etac System_Alloc_Progress 1);
-qed "System_Alloc_Progress";
-
--- a/src/HOL/UNITY/Comp.ML Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Comp.ML Fri Jan 14 12:17:53 2000 +0100
@@ -173,74 +173,3 @@
by (Blast_tac 1);
qed "Increasing_preserves_Stable";
-
-(*** givenBy ***)
-
-Goalw [givenBy_def] "givenBy id = UNIV";
-by Auto_tac;
-qed "givenBy_id";
-Addsimps [givenBy_id];
-
-Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
-by Safe_tac;
-by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
-by Auto_tac;
-qed "givenBy_eq_all";
-
-Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
-by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by Safe_tac;
-by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
-by (Blast_tac 1);
-by Auto_tac;
-qed "givenBy_eq_Collect";
-
-val prems =
-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";
-
-Goalw [givenBy_def] "[| A: givenBy v; x:A; v x = v y |] ==> y: A";
-by Auto_tac;
-qed "givenByD";
-
-Goal "{} : givenBy v";
-by (blast_tac (claset() addSIs [givenByI]) 1);
-qed "empty_mem_givenBy";
-
-AddIffs [empty_mem_givenBy];
-
-Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
-by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
-by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by (Blast_tac 1);
-qed "givenBy_imp_eq_Collect";
-
-Goalw [givenBy_def] "{s. P(v s)} : givenBy v";
-by (Best_tac 1);
-qed "Collect_mem_givenBy";
-
-Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
-by (blast_tac (claset() addIs [Collect_mem_givenBy,
- givenBy_imp_eq_Collect]) 1);
-qed "givenBy_eq_eq_Collect";
-
-(*preserving v preserves properties given by v*)
-Goal "[| F : preserves v; D : givenBy v |] ==> F : stable D";
-by (force_tac (claset(),
- simpset() addsimps [impOfSubs preserves_subset_stable,
- 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";
-
-Goal "[| A : givenBy v; B : givenBy v |] ==> A-B : givenBy v";
-by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by Safe_tac;
-by (res_inst_tac [("x", "%z. ?R z & ~ ?Q z")] exI 1);
-by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
-qed "givenBy_DiffI";
--- a/src/HOL/UNITY/Comp.thy Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Comp.thy Fri Jan 14 12:17:53 2000 +0100
@@ -26,8 +26,4 @@
funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
"funPair f g == %x. (f x, g x)"
- (*the set of all sets determined by f alone*)
- givenBy :: "['a => 'b] => 'a set set"
- "givenBy f == range (%B. f-`` B)"
-
end
--- a/src/HOL/UNITY/ELT.ML Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/ELT.ML Fri Jan 14 12:17:53 2000 +0100
@@ -6,6 +6,93 @@
leadsTo strengthened with a specification of the allowable sets transient parts
*)
+(*** givenBy ***)
+
+Goalw [givenBy_def] "givenBy id = UNIV";
+by Auto_tac;
+qed "givenBy_id";
+Addsimps [givenBy_id];
+
+Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
+by Safe_tac;
+by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
+by Auto_tac;
+qed "givenBy_eq_all";
+
+Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
+by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by Safe_tac;
+by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
+by (Blast_tac 1);
+by Auto_tac;
+qed "givenBy_eq_Collect";
+
+val prems =
+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";
+
+Goalw [givenBy_def] "[| A: givenBy v; x:A; v x = v y |] ==> y: A";
+by Auto_tac;
+qed "givenByD";
+
+Goal "{} : givenBy v";
+by (blast_tac (claset() addSIs [givenByI]) 1);
+qed "empty_mem_givenBy";
+
+AddIffs [empty_mem_givenBy];
+
+Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
+by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
+by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by (Blast_tac 1);
+qed "givenBy_imp_eq_Collect";
+
+Goalw [givenBy_def] "{s. P(v s)} : givenBy v";
+by (Best_tac 1);
+qed "Collect_mem_givenBy";
+
+Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
+by (blast_tac (claset() addIs [Collect_mem_givenBy,
+ givenBy_imp_eq_Collect]) 1);
+qed "givenBy_eq_eq_Collect";
+
+(*preserving v preserves properties given by v*)
+Goal "[| F : preserves v; D : givenBy v |] ==> F : stable D";
+by (force_tac (claset(),
+ simpset() addsimps [impOfSubs preserves_subset_stable,
+ 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";
+
+Goal "[| A : givenBy v; B : givenBy v |] ==> A-B : givenBy v";
+by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by Safe_tac;
+by (res_inst_tac [("x", "%z. ?R z & ~ ?Q z")] exI 1);
+by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
+qed "givenBy_DiffI";
+
+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);
+by (Blast_tac 1);
+qed "extend_set_givenBy_I";
+
+
(** Standard leadsTo rules **)
Goalw [leadsETo_def]
--- a/src/HOL/UNITY/ELT.thy Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/ELT.thy Fri Jan 14 12:17:53 2000 +0100
@@ -43,6 +43,10 @@
constdefs
+
+ (*the set of all sets determined by f alone*)
+ givenBy :: "['a => 'b] => 'a set set"
+ "givenBy f == range (%B. f-`` B)"
(*visible version of the LEADS-TO relation*)
leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
--- a/src/HOL/UNITY/Extend.ML Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Extend.ML Fri Jan 14 12:17:53 2000 +0100
@@ -569,24 +569,6 @@
qed "extend_LeadsTo";
-(*** givenBy: USEFUL??? ***)
-
-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);
-by (Blast_tac 1);
-qed "extend_set_givenBy_I";
-
-
Close_locale "Extend";
(*Close_locale should do this!
--- a/src/HOL/UNITY/Follows.ML Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Follows.ML Fri Jan 14 12:17:53 2000 +0100
@@ -22,7 +22,6 @@
by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
qed "mono_LeadsTo_o";
-(*NOT PROVABLE USING leadsETo because givenBy f <= givenBy (h o f) fails*)
Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)";
by (Clarify_tac 1);
by (asm_full_simp_tac
@@ -31,34 +30,17 @@
impOfSubs mono_LeadsTo_o RS INT_D]) 1);
qed "mono_Follows_o";
-(*NOT PROVABLE USING leadsETo since it needs the previous thm*)
Goal "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))";
by (dtac mono_Follows_o 1);
by (force_tac (claset(), simpset() addsimps [o_def]) 1);
qed "mono_Follows_apply";
-(*NOT PROVABLE USING leadsETo since givenBy g doesn't imply givenBy f*)
Goalw [Follows_def]
"[| F : f Fols g; F: g Fols h |] ==> F : f Fols h";
by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1);
qed "Follows_trans";
-(*
-try:
-by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [order_trans, LeadsETo_Trans]) 1);
-by (rtac LeadsETo_Trans 1);
-by (Blast_tac 2);
-by (dtac spec 1);
-by (etac LeadsETo_weaken 1);
-by Auto_tac;
-by (thin_tac "All ?P" 1);
-by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by Safe_tac;
-**)
-
(** Destructiom rules **)
@@ -82,6 +64,24 @@
by (Blast_tac 1);
qed "Follows_LeadsTo";
+Goal "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}";
+by (rtac single_LeadsTo_I 1);
+by (Clarify_tac 1);
+by (dtac Follows_LeadsTo 1);
+by (etac LeadsTo_weaken 1);
+by (blast_tac set_cs 1);
+by (blast_tac (claset() addIs [pfixLe_trans, prefix_imp_pfixLe]) 1);
+qed "Follows_LeadsTo_pfixLe";
+
+Goal "F : f Fols g ==> F : {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}";
+by (rtac single_LeadsTo_I 1);
+by (Clarify_tac 1);
+by (dtac Follows_LeadsTo 1);
+by (etac LeadsTo_weaken 1);
+by (blast_tac set_cs 1);
+by (blast_tac (claset() addIs [pfixGe_trans, prefix_imp_pfixGe]) 1);
+qed "Follows_LeadsTo_pfixGe";
+
(*Can replace "Un" by any sup. But existing max only works for linorders.*)
--- a/src/HOL/UNITY/Follows.thy Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Follows.thy Fri Jan 14 12:17:53 2000 +0100
@@ -3,13 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-The Follows relation of Charpentier and Sivilotte
-
-The safety conditions ensures that "givenBy f" is implementable in the
- progress part: g cannot do anything silly.
+The "Follows" relation of Charpentier and Sivilotte
*)
-Follows = Project +
+Follows = SubstAx +
constdefs
--- a/src/HOL/UNITY/GenPrefix.ML Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/GenPrefix.ML Fri Jan 14 12:17:53 2000 +0100
@@ -313,9 +313,17 @@
by (Force_tac 1);
qed "prefix_append_iff";
+Goal "r<=s ==> genPrefix r <= genPrefix s";
+by (Clarify_tac 1);
+by (etac genPrefix.induct 1);
+by (auto_tac (claset() addIs [genPrefix.append], simpset()));
+qed "genPrefix_mono";
+
(*** pfixLe, pfixGe: properties inherited from the translations ***)
+(** pfixLe **)
+
Goalw [refl_def, Le_def] "reflexive Le";
by Auto_tac;
qed "reflexive_Le";
@@ -330,6 +338,23 @@
AddIffs [reflexive_Le, antisym_Le, trans_Le];
+Goal "x pfixLe x";
+by (Simp_tac 1);
+qed "pfixLe_refl";
+AddIffs[pfixLe_refl];
+
+Goal "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z";
+by (blast_tac (claset() addIs [genPrefix_trans]) 1);
+qed "pfixLe_trans";
+
+Goal "[| x pfixLe y; y pfixLe x |] ==> x = y";
+by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
+qed "pfixLe_antisym";
+
+Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys";
+by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
+qed "prefix_imp_pfixLe";
+
Goalw [refl_def, Ge_def] "reflexive Ge";
by Auto_tac;
qed "reflexive_Ge";
@@ -344,15 +369,18 @@
AddIffs [reflexive_Ge, antisym_Ge, trans_Ge];
-Goal "r<=s ==> genPrefix r <= genPrefix s";
-by (Clarify_tac 1);
-by (etac genPrefix.induct 1);
-by (auto_tac (claset() addIs [genPrefix.append], simpset()));
-qed "genPrefix_mono";
+Goal "x pfixGe x";
+by (Simp_tac 1);
+qed "pfixGe_refl";
+AddIffs[pfixGe_refl];
-Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys";
-by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
-qed "prefix_imp_pfixLe";
+Goal "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z";
+by (blast_tac (claset() addIs [genPrefix_trans]) 1);
+qed "pfixGe_trans";
+
+Goal "[| x pfixGe y; y pfixGe x |] ==> x = y";
+by (blast_tac (claset() addIs [genPrefix_antisym]) 1);
+qed "pfixGe_antisym";
Goalw [prefix_def, Ge_def] "xs<=ys ==> xs pfixGe ys";
by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
--- a/src/HOL/UNITY/LessThan.ML Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/LessThan.ML Fri Jan 14 12:17:53 2000 +0100
@@ -50,17 +50,6 @@
by Auto_tac;
qed "Restrict_imageI";
-Goal "(Restrict A `` (Restrict A `` r - s)) = (Restrict A `` r - s)";
-by Auto_tac;
-by (rewrite_goals_tac [image_def, Restrict_def]);
-by (Blast_tac 1);
-qed "Restrict_image_Diff";
-
-(*Nothing to do with Restrict, but to specialized for Fun.ML?*)
-Goal "f``(g``A - B) = (UN x: (A - g-`` B). {f(g(x))})";
-by (Blast_tac 1);
-qed "image_Diff_image_eq";
-
Goal "Domain (Restrict A r) = A Int Domain r";
by (Blast_tac 1);
qed "Domain_Restrict";
--- a/src/HOL/UNITY/Lift_prog.ML Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML Fri Jan 14 12:17:53 2000 +0100
@@ -211,27 +211,11 @@
qed "drop_set_INT";
Goal "lift_set i UNIV = UNIV";
-by (simp_tac
- (simpset() addsimps [lift_set_correct, lift_export0 extend_set_UNIV_eq]) 1);
+by (simp_tac (simpset() addsimps [lift_set_correct,
+ lift_export0 extend_set_UNIV_eq]) 1);
qed "lift_set_UNIV_eq";
Addsimps [lift_set_UNIV_eq];
-(*
-Goal "Domain act <= drop_set i C ==> drop_act i (Restrict C (lift_act i act)) = act";
-by (asm_full_simp_tac
- (simpset() addsimps [drop_set_correct, drop_act_correct,
- lift_act_correct, lift_export0 extend_act_inverse]) 1);
-qed "lift_act_inverse";
-Addsimps [lift_act_inverse];
-*)
-
-Goal "UNIV <= drop_set i C ==> drop_prog i C (lift_prog i F) = F";
-by (asm_full_simp_tac
- (simpset() addsimps [drop_set_correct, drop_prog_correct,
- lift_prog_correct, lift_export0 extend_inverse]) 1);
-qed "lift_prog_inverse";
-Addsimps [lift_prog_inverse];
-
Goal "inj (lift_prog i)";
by (simp_tac
(simpset() addsimps [lift_prog_correct, lift_export0 inj_extend]) 1);
@@ -291,8 +275,8 @@
Goal "(drop_prog i C F : A co B) = \
\ (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
by (simp_tac
- (simpset() addsimps [drop_prog_correct,
- lift_set_correct, lift_export0 project_constrains]) 1);
+ (simpset() addsimps [drop_prog_correct, lift_set_correct,
+ lift_export0 project_constrains]) 1);
qed "drop_prog_constrains";
Goal "(drop_prog i UNIV F : stable A) = (F : stable (lift_set i A))";
@@ -321,8 +305,7 @@
by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1);
qed "lift_prog_Stable";
-Goal "[| reachable (lift_prog i F Join G) <= C; \
-\ F Join drop_prog i C G : A Co B |] \
+Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : A Co B \
\ ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
by (asm_full_simp_tac
(simpset() addsimps [lift_prog_correct, drop_prog_correct,
@@ -330,14 +313,12 @@
qed "drop_prog_Constrains_D";
Goalw [Stable_def]
- "[| reachable (lift_prog i F Join G) <= C; \
-\ F Join drop_prog i C G : Stable A |] \
+ "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Stable A \
\ ==> lift_prog i F Join G : Stable (lift_set i A)";
by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
qed "drop_prog_Stable_D";
-Goal "[| reachable (lift_prog i F Join G) <= C; \
-\ F Join drop_prog i C G : Always A |] \
+Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Always A \
\ ==> lift_prog i F Join G : Always (lift_set i A)";
by (asm_full_simp_tac
(simpset() addsimps [lift_prog_correct, drop_prog_correct,
@@ -345,24 +326,14 @@
qed "drop_prog_Always_D";
Goalw [Increasing_def]
- "[| reachable (lift_prog i F Join G) <= C; \
-\ F Join drop_prog i C G : Increasing func |] \
-\ ==> lift_prog i F Join G : Increasing (func o (sub i))";
+ "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Increasing func \
+\ ==> lift_prog i F Join G : Increasing (func o (sub i))";
by Auto_tac;
by (stac Collect_eq_lift_set 1);
by (asm_simp_tac (simpset() addsimps [drop_prog_Stable_D]) 1);
qed "project_Increasing_D";
-(*UNUSED*)
-Goal "UNIV <= drop_set i C \
-\ ==> drop_prog i C ((lift_prog i F) Join G) = F Join (drop_prog i C G)";
-by (asm_full_simp_tac
- (simpset() addsimps [lift_prog_correct, drop_prog_correct,
- drop_set_correct, lift_export0 project_extend_Join]) 1);
-qed "drop_prog_lift_prog_Join";
-
-
(*** Progress: transient, ensures ***)
Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)";
--- a/src/HOL/UNITY/Project.ML Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Project.ML Fri Jan 14 12:17:53 2000 +0100
@@ -6,16 +6,8 @@
Projections of state sets (also of actions and programs)
Inheritance of GUARANTEES properties under extension
-
-POSSIBLY CAN DELETE Restrict_image_Diff
*)
-(*EQUALITIES.ML*)
- Goal "(A <= -A) = (A = {})";
- by (Blast_tac 1);
- qed "subset_Compl_self_eq";
-
-
Open_locale "Extend";
(** projection: monotonicity for safety **)
@@ -297,37 +289,30 @@
by (etac extend_act_D 1);
qed "reachable_imp_reachable_project";
-(*The extra generality in the first premise allows guarantees with STRONG
- preconditions (localT) and WEAK postconditions.*)
-(*LOCALTO NO LONGER EXISTS: replace C by reachable...??*)
Goalw [Constrains_def]
- "[| reachable (extend h F Join G) <= C; \
-\ F Join project h C G : A Co B |] \
+ "F Join project h (reachable (extend h F Join G)) G : A Co B \
\ ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
by (Clarify_tac 1);
by (etac constrains_weaken 1);
-by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset()));
+by (auto_tac (claset() addIs [reachable_imp_reachable_project], simpset()));
qed "project_Constrains_D";
Goalw [Stable_def]
- "[| reachable (extend h F Join G) <= C; \
-\ F Join project h C G : Stable A |] \
+ "F Join project h (reachable (extend h F Join G)) G : Stable A \
\ ==> extend h F Join G : Stable (extend_set h A)";
by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
qed "project_Stable_D";
Goalw [Always_def]
- "[| reachable (extend h F Join G) <= C; \
-\ F Join project h C G : Always A |] \
+ "F Join project h (reachable (extend h F Join G)) G : Always A \
\ ==> extend h F Join G : Always (extend_set h A)";
by (force_tac (claset() addIs [reachable.Init],
simpset() addsimps [project_Stable_D, split_extended_all]) 1);
qed "project_Always_D";
Goalw [Increasing_def]
- "[| reachable (extend h F Join G) <= C; \
-\ F Join project h C G : Increasing func |] \
+ "F Join project h (reachable (extend h F Join G)) G : Increasing func \
\ ==> extend h F Join G : Increasing (func o f)";
by Auto_tac;
by (stac Collect_eq_extend_set 1);
@@ -364,45 +349,37 @@
simpset()));
qed "reachable_extend_Join_subset";
-(*Perhaps should replace C by reachable...*)
Goalw [Constrains_def]
- "[| C <= reachable (extend h F Join G); \
-\ extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
-\ ==> F Join project h C G : A Co B";
+ "extend h F Join G : (extend_set h A) Co (extend_set h B) \
+\ ==> F Join project h (reachable (extend h F Join G)) G : A Co B";
by (full_simp_tac (simpset() addsimps [Join_project_constrains,
extend_set_Int_distrib]) 1);
by (rtac conjI 1);
-by (etac constrains_weaken 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1);
-(*Some generalization of constrains_weaken_L would be better, but what is it?*)
-by (rewtac constrains_def);
-by Auto_tac;
-by (thin_tac "ALL act : Acts G. ?P act" 1);
-by (force_tac (claset() addSDs [reachable_project_imp_reachable],
- simpset()) 1);
+by (force_tac
+ (claset() addEs [constrains_weaken_L]
+ addSDs [extend_constrains_project_set,
+ subset_refl RS reachable_project_imp_reachable],
+ simpset() addsimps [Join_constrains]) 2);
+by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
qed "project_Constrains_I";
Goalw [Stable_def]
- "[| C <= reachable (extend h F Join G); \
-\ extend h F Join G : Stable (extend_set h A) |] \
-\ ==> F Join project h C G : Stable A";
+ "extend h F Join G : Stable (extend_set h A) \
+\ ==> F Join project h (reachable (extend h F Join G)) G : Stable A";
by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
qed "project_Stable_I";
Goalw [Always_def]
- "[| C <= reachable (extend h F Join G); \
-\ extend h F Join G : Always (extend_set h A) |] \
-\ ==> F Join project h C G : Always A";
+ "extend h F Join G : Always (extend_set h A) \
+\ ==> F Join project h (reachable (extend h F Join G)) G : Always A";
by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
by (rewtac extend_set_def);
by (Blast_tac 1);
qed "project_Always_I";
Goalw [Increasing_def]
- "[| C <= reachable (extend h F Join G); \
-\ extend h F Join G : Increasing (func o f) |] \
-\ ==> F Join project h C G : Increasing func";
+ "extend h F Join G : Increasing (func o f) \
+\ ==> F Join project h (reachable (extend h F Join G)) G : Increasing func";
by Auto_tac;
by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
project_Stable_I]) 1);
@@ -471,11 +448,10 @@
by (blast_tac (claset() addIs [project_Always_D]) 1);
qed "extending_Always";
-val [prem] =
Goalw [extending_def]
- "(!!G. reachable (extend h F Join G) <= C G) \
-\ ==> extending v C h F (Increasing (func o f)) (Increasing func)";
-by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1);
+ "extending v (%G. reachable (extend h F Join G)) h F \
+\ (Increasing (func o f)) (Increasing func)";
+by (blast_tac (claset() addIs [project_Increasing_D]) 1);
qed "extending_Increasing";
@@ -630,10 +606,10 @@
by (auto_tac (claset(),
simpset() addsimps [Int_Diff,
extend_set_Diff_distrib RS sym]));
-bd act_subset_imp_project_act_subset 1;
+by (dtac act_subset_imp_project_act_subset 1);
by (subgoal_tac
"project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) <= {}" 1);
-bws [Restrict_def, project_set_def, extend_set_def, project_act_def];
+by (rewrite_goals_tac [Restrict_def, project_set_def, extend_set_def, project_act_def]);
(*using Int_greatest actually slows the next step!*)
by (Blast_tac 2);
by (force_tac (claset(),
@@ -670,9 +646,9 @@
Goal "[| F Join project h UNIV G : A ensures B; \
\ G : stable (extend_set h A - extend_set h B) |] \
\ ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)";
-br (project_ensures_D_lemma RS revcut_rl) 1;
+by (rtac (project_ensures_D_lemma RS revcut_rl) 1);
by (stac stable_UNIV 3);
-auto();
+by Auto_tac;
qed "project_ensures_D";
Goalw [Ensures_def]
@@ -680,7 +656,7 @@
\ G : stable (reachable (extend h F Join G) Int extend_set h A - \
\ extend_set h B) |] \
\ ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)";
-br (project_ensures_D_lemma RS revcut_rl) 1;
+by (rtac (project_ensures_D_lemma RS revcut_rl) 1);
by (auto_tac (claset(),
simpset() addsimps [project_set_reachable_extend_eq RS sym]));
qed "project_Ensures_D";
--- a/src/HOL/UNITY/ROOT.ML Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/ROOT.ML Fri Jan 14 12:17:53 2000 +0100
@@ -28,7 +28,7 @@
time_use_thy "Extend";
time_use_thy "PPROD";
time_use_thy "TimerArray";
-time_use_thy "Follows";
+time_use_thy "Alloc";
add_path "../Auth"; (*to find Public.thy*)
use_thy"NSP_Bad";