New treatment of "guarantees" with polymorphic components and bijections.
Works EXCEPT FOR Alloc.
--- a/src/HOL/UNITY/Alloc.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Alloc.ML Fri Feb 18 15:20:44 2000 +0100
@@ -425,8 +425,8 @@
Client_component_System] MRS component_guaranteesD) 1);
by (rtac Client_i_Bounded 1);
by (auto_tac(claset(),
- simpset() addsimps [o_apply, lift_export Collect_eq_extend_set RS sym,
- client_export Collect_eq_extend_set RS sym]));
+ simpset() addsimps [o_apply, lift_export extend_set_eq_Collect,
+ client_export extend_set_eq_Collect]));
qed "System_Bounded_ask";
(*progress (2), step 4*)
@@ -479,7 +479,7 @@
by (full_simp_tac (simpset() addsimps [fold_o_sub, lift_prog_correct]) 1);
by (rtac INT_I 1);
by (simp_tac (simpset() addsimps [o_apply]) 1);
-by (REPEAT (stac (lift_export Collect_eq_extend_set) 1));
+by (REPEAT (stac (lift_export extend_set_eq_Collect RS sym) 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);
@@ -541,18 +541,17 @@
by (Simp_tac 1);
by (rtac INT_I 1);
by (simp_tac (simpset() addsimps [o_apply]) 1);
-by (REPEAT (stac (client_export Collect_eq_extend_set) 1));
+by (REPEAT (stac (client_export extend_set_eq_Collect RS sym) 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);
+ extend_set_eq_Collect]) 1);
by (Clarify_tac 1);
by (dtac G_stable_sysOfClient 1);
by (auto_tac (claset(),
- simpset() addsimps [o_apply,
- client_export Collect_eq_extend_set RS sym]));
+ simpset() addsimps [o_apply, client_export extend_set_eq_Collect]));
qed "sysOfClient_i_Progress";
--- a/src/HOL/UNITY/Client.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Client.ML Fri Feb 18 15:20:44 2000 +0100
@@ -46,10 +46,12 @@
by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
addSIs [stable_Int]) 3);
by (constrains_tac 2);
+by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2);
by Auto_tac;
qed "ask_bounded_lemma";
-(*export version, with no mention of tok*)
+(*export version, with no mention of tok in the postcondition, but
+ unfortunately tok must be declared local.*)
Goal "Client: UNIV guarantees[funPair ask tok] \
\ Always {s. ALL elt : set (ask s). elt <= NbT}";
by (rtac guaranteesI 1);
@@ -90,7 +92,6 @@
qed "transient_lemma";
-
Goal "[| Client Join G : Increasing giv; G : preserves (funPair rel ask) |] \
\ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s} \
\ LeadsTo {s. k < rel s & rel s <= giv s & \
@@ -139,6 +140,7 @@
addDs [common_prefix_linear]) 1);
qed "client_progress_lemma";
+(*Progress property: all tokens that are given will be released*)
Goal "Client : \
\ Increasing giv guarantees[funPair rel ask] \
\ (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
@@ -147,6 +149,28 @@
by (blast_tac (claset() addIs [client_progress_lemma]) 1);
qed "client_progress";
+Goal "Client : preserves extra";
+by (rewtac preserves_def);
+by Auto_tac;
+by (constrains_tac 1);
+by Auto_tac;
+qed "client_preserves_extra";
+
+Goal "bij client_map";
+by (auto_tac (claset() addSWrapper record_split_wrapper,
+ simpset() addsimps [client_map_def, non_extra_def, bij_def,
+ inj_on_def, surj_def]));
+by (res_inst_tac
+ [("x", "(|giv=?a, ask=?b, rel=?c, tok=?d, extra=?e|)")] exI 1);
+by (Force_tac 1);
+qed "bij_client_map";
+
+Goal "rename client_map Client : preserves snd";
+by (asm_simp_tac (simpset() addsimps [bij_client_map RS rename_preserves]) 1);
+by (asm_simp_tac (simpset() addsimps [client_map_def]) 1);
+by (rtac client_preserves_extra 1);
+qed "client_preserves_extra";
+
(** Obsolete lemmas from first version of the Client **)
--- a/src/HOL/UNITY/Client.thy Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Client.thy Fri Feb 18 15:20:44 2000 +0100
@@ -6,7 +6,7 @@
Distributed Resource Management System: the Client
*)
-Client = Extend +
+Client = Rename +
consts
NbT :: nat (*Maximum number of tokens*)
@@ -20,6 +20,10 @@
rel :: tokbag list (*output history: tokens released*)
tok :: tokbag (*current token request*)
+record 'a state_u =
+ state +
+ extra :: 'a (*new variables*)
+
(*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
@@ -27,7 +31,7 @@
(** Release some tokens **)
- rel_act :: "(state*state) set"
+ rel_act :: "('a state_u * 'a state_u) set"
"rel_act == {(s,s').
EX nrel. nrel = size (rel s) &
s' = s (| rel := rel s @ [giv s!nrel] |) &
@@ -39,26 +43,27 @@
(** Including s'=s suppresses fairness, allowing the non-trivial part
of the action to be ignored **)
- tok_act :: "(state*state) set"
- "tok_act == {(s,s'). s'=s | (EX t: atMost NbT. s' = s (|tok := t|))}"
-
- (*
- "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
- *)
-
+ tok_act :: "('a state_u * 'a state_u) set"
+ "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
- ask_act :: "(state*state) set"
+ ask_act :: "('a state_u * 'a state_u) set"
"ask_act == {(s,s'). s'=s |
(s' = s (|ask := ask s @ [tok s]|))}"
- Client :: state program
+ Client :: 'a state_u program
"Client == mk_program ({s. tok s : atMost NbT &
giv s = [] & ask s = [] & rel s = []},
{rel_act, tok_act, ask_act})"
- giv_meets_ask :: state set
- "giv_meets_ask ==
- {s. size (giv s) <= size (ask s) &
- (ALL n: lessThan (size (giv s)). ask s!n <= giv s!n)}"
+ (*Maybe want a special theory section to declare such maps*)
+ non_extra :: 'a state_u => state
+ "non_extra s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
+
+ (*Renaming map to put a Client into the standard form*)
+ client_map :: "'a state_u => state*'a"
+ "client_map == funPair non_extra extra"
+
+rules
+ NbT_pos "0 < NbT"
end
--- a/src/HOL/UNITY/Comp.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Comp.ML Fri Feb 18 15:20:44 2000 +0100
@@ -90,6 +90,16 @@
(*** preserves ***)
+val prems =
+Goalw [preserves_def] "(!!z. F : stable {s. v s = z}) ==> F : preserves v";
+by (blast_tac (claset() addIs prems) 1);
+qed "preservesI";
+
+Goalw [preserves_def, stable_def, constrains_def]
+ "[| F : preserves v; act : Acts F; (s,s') : act |] ==> v s = v s'";
+by (Force_tac 1);
+qed "preserves_imp_eq";
+
Goal "(F Join G : preserves v) = (F : preserves v & G : preserves v)";
by (simp_tac (simpset() addsimps [Join_stable, preserves_def]) 1);
by (Blast_tac 1);
@@ -102,10 +112,14 @@
AddIffs [Join_preserves, JN_preserves];
+Goalw [funPair_def] "(funPair f g) x = (f x, g x)";
+by (Simp_tac 1);
+qed "funPair_apply";
+Addsimps [funPair_apply];
+
Goal "preserves (funPair v w) = preserves v Int preserves w";
by (auto_tac (claset(),
- simpset() addsimps [funPair_def, preserves_def,
- stable_def, constrains_def]));
+ simpset() addsimps [preserves_def, stable_def, constrains_def]));
by (Blast_tac 1);
qed "preserves_funPair";
@@ -117,6 +131,17 @@
by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
qed "funPair_o_distrib";
+
+Goal "fst o (funPair f g) = f";
+by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
+qed "fst_o_funPair";
+
+Goal "snd o (funPair f g) = g";
+by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
+qed "snd_o_funPair";
+Addsimps [fst_o_funPair, snd_o_funPair];
+
+
Goal "preserves v <= preserves (w o v)";
by (force_tac (claset(),
simpset() addsimps [preserves_def,
@@ -125,8 +150,7 @@
Goal "preserves v <= stable {s. P (v s)}";
by (auto_tac (claset(),
- simpset() addsimps [preserves_def,
- stable_def, constrains_def]));
+ simpset() addsimps [preserves_def, stable_def, constrains_def]));
by (rename_tac "s' s" 1);
by (subgoal_tac "v s = v s'" 1);
by (ALLGOALS Force_tac);
@@ -154,7 +178,7 @@
by (Asm_simp_tac 2);
by (dres_inst_tac [("P1", "split ?Q")]
(impOfSubs preserves_subset_stable) 1);
-by (auto_tac (claset(), simpset() addsimps [funPair_def]));
+by Auto_tac;
qed "stable_localTo_stable2";
Goal "[| F : stable {s. v s <= w s}; G : preserves v; \
--- a/src/HOL/UNITY/Extend.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Extend.ML Fri Feb 18 15:20:44 2000 +0100
@@ -10,6 +10,10 @@
(** These we prove OUTSIDE the locale. **)
+Goal "f Id = Id ==> insert Id (f``Acts F) = f `` Acts F";
+by (blast_tac (claset() addIs [sym RS image_eqI]) 1);
+qed "insert_Id_image_Acts";
+
(*Possibly easier than reasoning about "inv h"*)
val [surj_h,prem] =
Goalw [good_map_def]
@@ -115,22 +119,25 @@
qed "extend_set_strict_mono";
AddIffs [extend_set_strict_mono];
-Goal "{s. P (f s)} = extend_set h {s. P s}";
+Goalw [extend_set_def] "extend_set h {} = {}";
by Auto_tac;
-qed "Collect_eq_extend_set";
+qed "extend_set_empty";
+Addsimps [extend_set_empty];
+
+Goal "extend_set h {s. P s} = {s. P (f s)}";
+by Auto_tac;
+qed "extend_set_eq_Collect";
Goal "extend_set h {x} = {s. f s = x}";
by Auto_tac;
qed "extend_set_sing";
-Goalw [extend_set_def]
- "project_set h (extend_set h C) = C";
+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]
- "C <= extend_set h (project_set h C)";
+Goalw [extend_set_def] "C <= extend_set h (project_set h C)";
by (auto_tac (claset(),
simpset() addsimps [split_extended_all]));
by (Blast_tac 1);
@@ -277,8 +284,7 @@
simpset() addsimps [split_extended_all]) 1);
qed "project_act_I";
-Goalw [project_act_def]
- "UNIV <= project_set h C ==> project_act h (Restrict C Id) = Id";
+Goalw [project_act_def] "project_act h Id = Id";
by (Force_tac 1);
qed "project_act_Id";
@@ -288,18 +294,7 @@
simpset() addsimps [split_extended_all]) 1);
qed "Domain_project_act";
-Addsimps [extend_act_Id, project_act_Id];
-
-Goal "(extend_act h act = Id) = (act = Id)";
-by Auto_tac;
-by (rewtac extend_act_def);
-by (ALLGOALS (blast_tac (claset() addEs [equalityE])));
-qed "extend_act_Id_iff";
-
-Goal "Id : extend_act h `` Acts F";
-by (auto_tac (claset() addSIs [extend_act_Id RS sym],
- simpset() addsimps [image_iff]));
-qed "Id_mem_extend_act";
+Addsimps [extend_act_Id];
(**** extend ****)
@@ -315,11 +310,10 @@
qed "Init_project";
Goal "Acts (extend h F) = (extend_act h `` Acts F)";
-by (auto_tac (claset() addSIs [extend_act_Id RS sym],
- simpset() addsimps [extend_def, image_iff]));
+by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1);
qed "Acts_extend";
-Goal "Acts (project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
+Goal "Acts(project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
by (auto_tac (claset(),
simpset() addsimps [project_def, image_iff]));
qed "Acts_project";
@@ -341,7 +335,6 @@
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);
@@ -378,7 +371,6 @@
qed "extend_JN";
Addsimps [extend_JN];
-
(** These monotonicity results look natural but are UNUSED **)
Goal "F <= G ==> extend h F <= extend h G";
@@ -460,7 +452,45 @@
qed "extend_Always";
-(** Further lemmas **)
+(** Safety and "project" **)
+
+(** projection: monotonicity for safety **)
+
+Goal "D <= C ==> \
+\ project_act h (Restrict D act) <= project_act h (Restrict C act)";
+by (auto_tac (claset(), simpset() addsimps [project_act_def]));
+qed "project_act_mono";
+
+Goal "[| D <= C; project h C F : A co B |] ==> project h D F : A co B";
+by (auto_tac (claset(), simpset() addsimps [constrains_def]));
+by (dtac project_act_mono 1);
+by (Blast_tac 1);
+qed "project_constrains_mono";
+
+Goal "[| D <= C; project h C F : stable A |] ==> project h D F : stable A";
+by (asm_full_simp_tac
+ (simpset() addsimps [stable_def, project_constrains_mono]) 1);
+qed "project_stable_mono";
+
+Goalw [constrains_def]
+ "(project h C 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() addsimps [ball_Un]));
+by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
+(*the <== direction*)
+by (rewtac project_act_def);
+by (force_tac (claset() addSDs [subsetD], simpset()) 1);
+qed "project_constrains";
+
+Goalw [stable_def]
+ "(project h UNIV F : stable A) = (F : stable (extend_set h A))";
+by (simp_tac (simpset() addsimps [project_constrains]) 1);
+qed "project_stable";
+
+Goal "F : stable (extend_set h A) ==> project h C F : stable A";
+by (dtac (project_stable RS iffD2) 1);
+by (blast_tac (claset() addIs [project_stable_mono]) 1);
+qed "project_stable_I";
Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
@@ -562,16 +592,84 @@
by (etac leadsTo_imp_extend_leadsTo 2);
by (dtac extend_leadsTo_slice 1);
by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1);
-qed "extend_leadsto";
+qed "extend_leadsTo";
Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) = \
\ (F : A LeadsTo B)";
by (simp_tac
(simpset() addsimps [LeadsTo_def, reachable_extend_eq,
- extend_leadsto, extend_set_Int_distrib RS sym]) 1);
+ extend_leadsTo, extend_set_Int_distrib RS sym]) 1);
qed "extend_LeadsTo";
+(*** preserves ***)
+
+Goal "G : preserves (v o f) ==> project h C G : preserves v";
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, project_stable_I,
+ extend_set_eq_Collect]));
+qed "project_preserves_I";
+
+(*to preserve f is to preserve the whole original state*)
+Goal "G : preserves f ==> project h C G : preserves id";
+by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
+qed "project_preserves_id_I";
+
+Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, extend_stable RS sym,
+ extend_set_eq_Collect]));
+qed "extend_preserves";
+
+Goal "inj h ==> (extend h G : preserves g)";
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, extend_def, extend_act_def,
+ stable_def, constrains_def, g_def]));
+qed "inj_extend_preserves";
+
+
+(*** Guarantees ***)
+
+Goal "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)";
+by (rtac program_equalityI 1);
+by (asm_simp_tac
+ (simpset() addsimps [image_eq_UN, UN_Un, project_act_extend_act]) 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 UNIV G)";
+by (dres_inst_tac [("f", "project h UNIV")] arg_cong 1);
+by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
+qed "extend_Join_eq_extend_D";
+
+(** Strong precondition and postcondition; only useful when
+ the old and new state sets are in bijection **)
+
+Goal "F : X guarantees[v] Y ==> \
+\ extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
+by (rtac guaranteesI 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [project_preserves_I]
+ addDs [extend_Join_eq_extend_D, guaranteesD]) 1);
+qed "guarantees_imp_extend_guarantees";
+
+Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
+\ ==> F : X guarantees[v] Y";
+by (auto_tac (claset(), simpset() addsimps [guar_def]));
+by (dres_inst_tac [("x", "extend h G")] spec 1);
+by (asm_full_simp_tac
+ (simpset() delsimps [extend_Join]
+ addsimps [extend_Join RS sym, extend_preserves,
+ inj_extend RS inj_image_mem_iff]) 1);
+qed "extend_guarantees_imp_guarantees";
+
+Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
+\ (F : X guarantees[v] Y)";
+by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
+ extend_guarantees_imp_guarantees]) 1);
+qed "extend_guarantees_eq";
+
+
Close_locale "Extend";
(*Close_locale should do this!
--- a/src/HOL/UNITY/Guar.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Guar.ML Fri Feb 18 15:20:44 2000 +0100
@@ -120,7 +120,7 @@
qed "guarantees_UN_left";
Goalw [guar_def]
- "(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)";
+ "(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)";
by (Blast_tac 1);
qed "guarantees_Un_left";
@@ -130,10 +130,15 @@
qed "guarantees_INT_right";
Goalw [guar_def]
- "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)";
+ "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)";
by (Blast_tac 1);
qed "guarantees_Int_right";
+Goal "[| F : Z guarantees[v] X; F : Z guarantees[v] Y |] \
+\ ==> F : Z guarantees[v] (X Int Y)";
+by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
+qed "guarantees_Int_right_I";
+
Goal "(F : X guarantees[v] (INTER I Y)) = \
\ (ALL i:I. F : X guarantees[v] (Y i))";
by (simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
--- a/src/HOL/UNITY/Lift_prog.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML Fri Feb 18 15:20:44 2000 +0100
@@ -3,67 +3,87 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Arrays of processes. Many results are instances of those in Extend & Project.
+Arrays of processes.
*)
+Addsimps [insert_map_def, delete_map_def];
-(*** Basic properties ***)
+Goal "delete_map i (insert_map i x f) = f";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "insert_map_inverse";
-(** lift_set and drop_set **)
+Goal "(insert_map i x (delete_map i g)) = g(i:=x)";
+by (rtac ext 1);
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
+by (exhaust_tac "d" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "insert_map_delete_map_eq";
+
+(*** Injectiveness proof ***)
-Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)";
-by Auto_tac;
-qed "lift_set_iff";
-AddIffs [lift_set_iff];
+Goal "(insert_map i x f) = (insert_map i y g) ==> x=y";
+by (dres_inst_tac [("x","i")] fun_cong 1);
+by (Full_simp_tac 1);
+qed "insert_map_inject1";
+
+Goal "(insert_map i x f) = (insert_map i y g) ==> f=g";
+by (dres_inst_tac [("f", "delete_map i")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [insert_map_inverse]) 1);
+qed "insert_map_inject2";
-Goalw [lift_set_def] "lift_set i A Int lift_set i B = lift_set i (A Int B)";
+Goal "(insert_map i x f) = (insert_map i y g) ==> x=y & f=g";
+by (blast_tac (claset() addDs [insert_map_inject1, insert_map_inject2]) 1);
+bind_thm ("insert_map_inject", result() RS conjE);
+AddSEs [insert_map_inject];
+
+(*The general case: we don't assume i=i'*)
+Goalw [lift_map_def]
+ "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu'))) \
+\ = (uu = uu' & insert_map i s f = insert_map i' s' f')";
by Auto_tac;
-qed "Int_lift_set";
-
-Goalw [lift_set_def] "lift_set i A Un lift_set i B = lift_set i (A Un B)";
-by Auto_tac;
-qed "Un_lift_set";
-
-Goalw [lift_set_def] "lift_set i A - lift_set i B = lift_set i (A-B)";
-by Auto_tac;
-qed "Diff_lift_set";
-
-Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set];
-
-(** lift_act and drop_act **)
+qed "lift_map_eq_iff";
+AddIffs [lift_map_eq_iff];
-(*For compatibility with the original definition and perhaps simpler proofs*)
-Goalw [lift_act_def]
- "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
-by Auto_tac;
-by (rtac exI 1);
+Goalw [lift_map_def, drop_map_def] "!!s. drop_map i (lift_map i s) = s";
+by (force_tac (claset() addIs [insert_map_inverse], simpset()) 1);
+qed "drop_map_lift_map_eq";
+
+Goalw [lift_map_def] "inj (lift_map i)";
+by (rtac injI 1);
by Auto_tac;
-qed "lift_act_eq";
-AddIffs [lift_act_eq];
+qed "inj_lift_map";
-(** lift_prog and drop_prog **)
+(*** Surjectiveness proof ***)
-Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
-by Auto_tac;
-qed "Init_lift_prog";
-Addsimps [Init_lift_prog];
+Goalw [lift_map_def, drop_map_def] "!!s. lift_map i (drop_map i s) = s";
+by (force_tac (claset(), simpset() addsimps [insert_map_delete_map_eq]) 1);
+qed "lift_map_drop_map_eq";
-Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
-by (auto_tac (claset() addIs [rev_image_eqI], simpset()));
-qed "Acts_lift_prog";
-Addsimps [Acts_lift_prog];
+Goal "(drop_map i s) = (drop_map i s') ==> s=s'";
+by (dres_inst_tac [("f", "lift_map i")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [lift_map_drop_map_eq]) 1);
+qed "drop_map_inject";
+AddSDs [drop_map_inject];
+
+Goal "surj (lift_map i)";
+by (rtac surjI 1);
+by (rtac lift_map_drop_map_eq 1);
+qed "surj_lift_map";
-Goalw [drop_prog_def] "Init (drop_prog i C F) = drop_set i (Init F)";
-by Auto_tac;
-qed "Init_drop_prog";
-Addsimps [Init_drop_prog];
+Goal "bij (lift_map i)";
+by (simp_tac (simpset() addsimps [bij_def, inj_lift_map, surj_lift_map]) 1);
+qed "bij_lift_map";
+AddIffs [bij_lift_map];
+
+AddIffs [bij_lift_map RS mem_rename_act_iff];
-Goal "Acts (drop_prog i C F) = insert Id (drop_act i `` Restrict C `` Acts F)";
-by (auto_tac (claset() addIs [image_eqI],
- simpset() addsimps [drop_prog_def]));
-qed "Acts_drop_prog";
-Addsimps [Acts_drop_prog];
-
+Goal "inv (lift_map i) = drop_map i";
+by (rtac inv_equality 1);
+by (rtac lift_map_drop_map_eq 2);
+by (rtac drop_map_lift_map_eq 1);
+qed "inv_lift_map_eq";
+Addsimps [inv_lift_map_eq];
(*** sub ***)
@@ -72,374 +92,293 @@
qed "sub_apply";
Addsimps [sub_apply];
-Goal "lift_set i {s. P s} = {s. P (sub i s)}";
-by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
-qed "lift_set_sub";
-
-Goal "{s. P (s i)} = lift_set i {s. P s}";
-by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
-qed "Collect_eq_lift_set";
-
-Goal "sub i -`` A = lift_set i A";
-by (Force_tac 1);
-qed "sub_vimage";
-Addsimps [sub_vimage];
+Goal "lift_set i {s. P s} = {s. P (drop_map i s)}";
+by (rtac set_ext 1);
+by (asm_simp_tac (simpset() delsimps [image_Collect]
+ addsimps [lift_set_def, rename_set_eq_Collect]) 1);
+qed "lift_set_eq_Collect";
-(*For tidying the result of "export"*)
-Goal "v o (%z. z i) = v o sub i";
-by (simp_tac (simpset() addsimps [sub_def]) 1);
-qed "fold_o_sub";
-
-
+Goalw [lift_set_def] "lift_set i {} = {}";
+by Auto_tac;
+qed "lift_set_empty";
+Addsimps [lift_set_empty];
-(*** lift_prog and the lattice operations ***)
-
-Goal "lift_prog i SKIP = SKIP";
-by (auto_tac (claset() addSIs [program_equalityI],
- simpset() addsimps [SKIP_def, lift_prog_def]));
-qed "lift_prog_SKIP";
+Goalw [lift_set_def] "(lift_map i x : lift_set i A) = (x : A)";
+by (rtac (inj_lift_map RS inj_image_mem_iff) 1);
+qed "lift_set_iff";
+AddIffs [lift_set_iff];
-Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)";
-by (rtac program_equalityI 1);
-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;
-qed "lift_prog_JN";
-
-
-(*** Equivalence with "extend" version ***)
+Goal "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)";
+by (asm_simp_tac (simpset() addsimps [lift_set_def,
+ mem_rename_set_iff, drop_map_def]) 1);
+qed "lift_set_iff";
+AddIffs [lift_set_iff];
-Goalw [lift_map_def] "good_map (lift_map i)";
-by (rtac good_mapI 1);
-by (res_inst_tac [("f", "%f. (f i, f)")] surjI 1);
-by Auto_tac;
-by (dres_inst_tac [("f", "%f. f i")] arg_cong 1);
-by Auto_tac;
-qed "good_map_lift_map";
+Goalw [lift_set_def] "A<=B ==> lift_set i A <= lift_set i B";
+by (etac image_mono 1);
+qed "lift_set_mono";
-fun lift_export0 th =
- good_map_lift_map RS export th
- |> simplify (simpset() addsimps [fold_o_sub]);
+Goalw [lift_set_def] "lift_set i (A Un B) = lift_set i A Un lift_set i B";
+by (asm_simp_tac (simpset() addsimps [image_Un]) 1);
+qed "lift_set_Un_distrib";
-Goal "fst (inv (lift_map i) g) = g i";
-by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1);
-by (auto_tac (claset(), simpset() addsimps [lift_map_def]));
-qed "fst_inv_lift_map";
-Addsimps [fst_inv_lift_map];
+Goalw [lift_set_def] "lift_set i (A-B) = lift_set i A - lift_set i B";
+by (rtac (inj_lift_map RS image_set_diff) 1);
+qed "lift_set_Diff_distrib";
-Goal "lift_set i A = extend_set (lift_map i) A";
-by (auto_tac (claset(),
- simpset() addsimps [lift_export0 mem_extend_set_iff]));
-qed "lift_set_correct";
-
-Goalw [drop_set_def, project_set_def, lift_map_def]
- "drop_set i A = project_set (lift_map i) A";
-by Auto_tac;
-by (rtac image_eqI 2);
-by (rtac exI 1);
-by (stac (refl RS fun_upd_idem) 1);
-by Auto_tac;
-qed "drop_set_correct";
-
-Goal "lift_act i = extend_act (lift_map i)";
-by (rtac ext 1);
-by Auto_tac;
-by (forward_tac [lift_export0 extend_act_D] 2);
-by (auto_tac (claset(), simpset() addsimps [extend_act_def]));
-by (auto_tac (claset(), simpset() addsimps [extend_act_def, lift_map_def]));
-by (rtac bexI 1);
-by (auto_tac (claset() addSIs [exI], simpset()));
-qed "lift_act_correct";
+(*** the lattice operations ***)
-Goal "drop_act i = project_act (lift_map i)";
-by (rtac ext 1);
-by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]);
-by Auto_tac;
-by (REPEAT_FIRST (ares_tac [exI, conjI]));
-by Auto_tac;
-by (REPEAT_FIRST (assume_tac ORELSE' stac (refl RS fun_upd_idem)));
-qed "drop_act_correct";
-
-Goal "lift_prog i = extend (lift_map i)";
-by (rtac (program_equalityI RS ext) 1);
-by (simp_tac (simpset() addsimps [lift_set_correct]) 1);
-by (simp_tac (simpset()
- addsimps [lift_export0 Acts_extend,
- lift_act_correct]) 1);
-qed "lift_prog_correct";
-
-Goal "drop_prog i C = project (lift_map i) C";
-by (rtac (program_equalityI RS ext) 1);
-by (simp_tac (simpset() addsimps [drop_set_correct]) 1);
-by (simp_tac (simpset()
- addsimps [Acts_project, drop_act_correct]) 1);
-qed "drop_prog_correct";
-
+Goalw [lift_def] "lift i SKIP = SKIP";
+by (Asm_simp_tac 1);
+qed "lift_SKIP";
+Addsimps [lift_SKIP];
-(** Injectivity of lift_set, lift_act, lift_prog **)
-
-Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F";
-by Auto_tac;
-qed "lift_set_inverse";
-Addsimps [lift_set_inverse];
-
-Goal "inj (lift_set i)";
-by (rtac inj_on_inverseI 1);
-by (rtac lift_set_inverse 1);
-qed "inj_lift_set";
-
-(*Because A and B could differ outside i, cannot generalize result to
- drop_set i (A Int B) = drop_set i A Int drop_set i B
-*)
-Goalw [lift_set_def, drop_set_def]
- "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)";
-by Auto_tac;
-qed "drop_set_Int_lift_set";
-
-Goalw [lift_set_def, drop_set_def]
- "drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A";
-by Auto_tac;
-qed "drop_set_Int_lift_set2";
+Goalw [lift_def] "lift i (F Join G) = lift i F Join lift i G";
+by (Asm_simp_tac 1);
+qed "lift_Join";
+Addsimps [lift_Join];
-Goalw [drop_set_def]
- "i : I ==> drop_set i (INT j:I. lift_set j A) = A";
-by Auto_tac;
-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);
-qed "lift_set_UNIV_eq";
-Addsimps [lift_set_UNIV_eq];
-
-Goal "inj (lift_prog i)";
-by (simp_tac
- (simpset() addsimps [lift_prog_correct, lift_export0 inj_extend]) 1);
-qed "inj_lift_prog";
-
-
-(*** More Lemmas ***)
-
-Goal "lift_act i act ^^ lift_set i A = lift_set i (act^^A)";
-by (asm_simp_tac (simpset() addsimps [lift_set_correct, lift_act_correct,
- lift_export0 extend_act_Image]) 1);
-qed "lift_act_Image";
-Addsimps [lift_act_Image];
-
-
+Goalw [lift_def] "lift j (JOIN I F) = (JN i:I. lift j (F i))";
+by (Asm_simp_tac 1);
+qed "lift_JN";
+Addsimps [lift_JN];
(*** Safety: co, stable, invariant ***)
-(** Safety and lift_prog **)
-
-Goal "(lift_prog i F : (lift_set i A) co (lift_set i B)) = \
-\ (F : A co B)";
-by (auto_tac (claset(),
- simpset() addsimps [constrains_def]));
-by (Force_tac 1);
-qed "lift_prog_constrains";
-
-Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)";
-by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains]) 1);
-qed "lift_prog_stable";
-
-Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)";
-by (auto_tac (claset(),
- simpset() addsimps [invariant_def, lift_prog_stable]));
-qed "lift_prog_invariant";
-
-Goal "[| lift_prog i F : A co B |] \
-\ ==> F : (drop_set i A) co (drop_set i B)";
-by (asm_full_simp_tac
- (simpset() addsimps [drop_set_correct, lift_prog_correct,
- lift_export0 extend_constrains_project_set]) 1);
-qed "lift_prog_constrains_drop_set";
+Goalw [lift_def, lift_set_def]
+ "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)";
+by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1);
+qed "lift_constrains";
-(*This one looks strange! Proof probably is by case analysis on i=j.
- If i~=j then lift_prog j (F j) does nothing to lift_set i, and the
- premise ensures A<=B.*)
-Goal "F i : A co B \
-\ ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)";
-by (auto_tac (claset(),
- simpset() addsimps [constrains_def]));
-by (REPEAT (Blast_tac 1));
-qed "constrains_imp_lift_prog_constrains";
-
+Goalw [lift_def, lift_set_def]
+ "(lift i F : stable (lift_set i A)) = (F : stable A)";
+by (asm_simp_tac (simpset() addsimps [rename_stable]) 1);
+qed "lift_stable";
-(** Safety and drop_prog **)
-
-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);
-qed "drop_prog_constrains";
-
-Goal "(drop_prog i UNIV F : stable A) = (F : stable (lift_set i A))";
-by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1);
-qed "drop_prog_stable";
-
+Goalw [lift_def, lift_set_def]
+ "(lift i F : invariant (lift_set i A)) = (F : invariant A)";
+by (asm_simp_tac (simpset() addsimps [rename_invariant]) 1);
+qed "lift_invariant";
-(*** Weak safety primitives: Co, Stable ***)
-
-(** Reachability **)
-
-Goal "reachable (lift_prog i F) = lift_set i (reachable F)";
-by (simp_tac
- (simpset() addsimps [lift_prog_correct, lift_set_correct,
- lift_export0 reachable_extend_eq]) 1);
-qed "reachable_lift_prog";
-
-Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B)) = \
-\ (F : A Co B)";
-by (simp_tac
- (simpset() addsimps [lift_prog_correct, lift_set_correct,
- lift_export0 extend_Constrains]) 1);
-qed "lift_prog_Constrains";
-
-Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
-by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1);
-qed "lift_prog_Stable";
+Goalw [lift_def, lift_set_def]
+ "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)";
+by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1);
+qed "lift_Constrains";
-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,
- lift_set_correct, lift_export0 project_Constrains_D]) 1);
-qed "drop_prog_Constrains_D";
-
-Goalw [Stable_def]
- "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";
+Goalw [lift_def, lift_set_def]
+ "(lift i F : Stable (lift_set i A)) = (F : Stable A)";
+by (asm_simp_tac (simpset() addsimps [rename_Stable]) 1);
+qed "lift_Stable";
-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,
- lift_set_correct, lift_export0 project_Always_D]) 1);
-qed "drop_prog_Always_D";
-
-Goalw [Increasing_def]
- "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";
-
+Goalw [lift_def, lift_set_def]
+ "(lift i F : Always (lift_set i A)) = (F : Always A)";
+by (asm_simp_tac (simpset() addsimps [rename_Always]) 1);
+qed "lift_Always";
(*** Progress: transient, ensures ***)
-Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)";
-by (simp_tac (simpset() addsimps [lift_set_correct, lift_prog_correct,
- lift_export0 extend_transient]) 1);
-qed "lift_prog_transient";
+Goalw [lift_def, lift_set_def]
+ "(lift i F : transient (lift_set i A)) = (F : transient A)";
+by (asm_simp_tac (simpset() addsimps [rename_transient]) 1);
+qed "lift_transient";
+
+Goalw [lift_def, lift_set_def]
+ "(lift i F : (lift_set i A) ensures (lift_set i B)) = \
+\ (F : A ensures B)";
+by (asm_simp_tac (simpset() addsimps [rename_ensures]) 1);
+qed "lift_ensures";
+
+Goalw [lift_def, lift_set_def]
+ "(lift i F : (lift_set i A) leadsTo (lift_set i B)) = \
+\ (F : A leadsTo B)";
+by (asm_simp_tac (simpset() addsimps [rename_leadsTo]) 1);
+qed "lift_leadsTo";
-Goal "(lift_prog i F : transient (lift_set j A)) = \
-\ (i=j & F : transient A | A={})";
-by (case_tac "i=j" 1);
-by (auto_tac (claset(), simpset() addsimps [lift_prog_transient]));
-by (auto_tac (claset(), simpset() addsimps [lift_prog_def, transient_def]));
-by (Force_tac 1);
-qed "lift_prog_transient_eq_disj";
+Goalw [lift_def, lift_set_def]
+ "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) = \
+\ (F : A LeadsTo B)";
+by (asm_simp_tac (simpset() addsimps [rename_LeadsTo]) 1);
+qed "lift_LeadsTo";
+
+
+(** guarantees **)
+
+Goalw [lift_def]
+ "(lift i F : (lift i `` X) guarantees[v o drop_map i] (lift i `` Y)) = \
+\ (F : X guarantees[v] Y)";
+by (stac (bij_lift_map RS rename_rename_guarantees_eq RS sym) 1);
+by (asm_simp_tac (simpset() addsimps [o_def]) 1);
+qed "lift_lift_guarantees_eq";
+
+Goal "(lift i F : X guarantees[v] Y) = \
+\ (F : (rename (drop_map i) `` X) guarantees[v o lift_map i] \
+\ (rename (drop_map i) `` Y))";
+by (asm_simp_tac
+ (simpset() addsimps [bij_lift_map RS rename_guarantees_eq_rename_inv,
+ lift_def]) 1);
+qed "lift_guarantees_eq_lift_inv";
-(*** guarantees properties ***)
+(*To preserve snd means that the second component is there just to allow
+ guarantees properties to be stated. Converse fails, for lift i F can
+ change function components other than i*)
+Goal "F : preserves snd ==> lift i F : preserves snd";
+by (dres_inst_tac [("w1", "snd")] (impOfSubs subset_preserves_o) 1);
+by (asm_simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1);
+by (full_simp_tac (simpset() addsimps [lift_map_def, o_def, split_def]) 1);
+qed "lift_preserves_snd_I";
+
+Goal "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)";
+by (dres_inst_tac [("f", "insert_map i (g i)")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [insert_map_delete_map_eq]) 1);
+by (etac exI 1);
+bind_thm ("delete_map_eqE", result() RS exE);
+AddSEs [delete_map_eqE];
-Goal "lift_prog i F : preserves (v o sub j) = \
-\ (if i=j then F : preserves v else True)";
-by (simp_tac (simpset() addsimps [lift_prog_correct,
- lift_export0 extend_preserves]) 1);
+Goal "[| delete_map j g = delete_map j g'; i~=j |] ==> g i = g' i";
+by (Force_tac 1);
+qed "delete_map_neq_apply";
+
+(*A set of the form (A Times UNIV) ignores the second (dummy) state component*)
+
+Goal "(f o fst) -`` A = (f-``A) Times UNIV";
+by Auto_tac;
+qed "vimage_o_fst_eq";
+
+Goal "(sub i -``A) Times UNIV = lift_set i (A Times UNIV)";
+by Auto_tac;
+qed "vimage_sub_eq_lift_set";
+
+Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set];
+
+Goal "[| F : preserves snd; i~=j |] \
+\ ==> lift j F : stable (lift_set i (A Times UNIV))";
by (auto_tac (claset(),
- simpset() addsimps [preserves_def, extend_def, extend_act_def,
- stable_def, constrains_def, lift_map_def]));
-qed "lift_prog_preserves_sub";
-
-Addsimps [lift_prog_preserves_sub];
+ simpset() addsimps [lift_def, lift_set_def,
+ stable_def, constrains_def,
+ mem_rename_act_iff, mem_rename_set_iff]));
+by (auto_tac (claset() addSDs [preserves_imp_eq],
+ simpset() addsimps [lift_map_def, drop_map_def]));
+by (dres_inst_tac [("x", "i")] fun_cong 1);
+by Auto_tac;
+qed "preserves_snd_lift_stable";
-Goal "G : preserves (v o sub i) ==> drop_prog i C G : preserves v";
-by (asm_simp_tac
- (simpset() addsimps [drop_prog_correct, fold_o_sub,
- lift_export0 project_preserves_I]) 1);
-qed "drop_prog_preserves_I";
+(*If i~=j then lift j F does nothing to lift_set i, and the
+ premise ensures A<=B.*)
+Goal "[| F i : (A Times UNIV) co (B Times UNIV); \
+\ F j : preserves snd |] \
+\ ==> lift j (F j) : (lift_set i (A Times UNIV)) co (lift_set i (B Times UNIV))";
+by (case_tac "i=j" 1);
+by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def,
+ rename_constrains]) 1);
+by (etac (preserves_snd_lift_stable RS stableD RS constrains_weaken_R) 1);
+by (assume_tac 1);
+by (etac (constrains_imp_subset RS lift_set_mono) 1);
+qed "constrains_imp_lift_constrains";
+
+(** Lemmas for the transient theorem **)
+
+Goal "(insert_map i t f)(i := s) = insert_map i s f";
+by (rtac ext 1);
+by Auto_tac;
+qed "insert_map_upd_same";
-(*The raw version*)
-val [xguary,drop_prog,lift_prog] =
-Goal "[| F : X guarantees[v] Y; \
-\ !!G. lift_prog i F Join G : X' ==> F Join drop_prog i (C G) G : X; \
-\ !!G. [| F Join drop_prog i (C G) G : Y; lift_prog i F Join G : X'; \
-\ G : preserves (v o sub i) |] \
-\ ==> lift_prog i F Join G : Y' |] \
-\ ==> lift_prog i F : X' guarantees[v o sub i] Y'";
-by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
-by (etac drop_prog_preserves_I 1);
-by (etac drop_prog 1);
+Goal "(insert_map j t f)(i := s) = \
+\ (if i=j then insert_map i s f \
+\ else if i<j then insert_map j t (f(i:=s)) \
+\ else insert_map j t (f(i-1:=s)))";
+by (rtac ext 1);
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split']));
+by (ALLGOALS arith_tac);
+qed "insert_map_upd";
+
+Goal "[| insert_map i s f = insert_map j t g; i~=j |] \
+\ ==> EX g'. insert_map i s' f = insert_map j t g'";
+by (stac (insert_map_upd_same RS sym) 1);
+by (etac ssubst 1);
+by (asm_simp_tac (HOL_ss addsimps [insert_map_upd]) 1);
+by (Blast_tac 1);
+qed "insert_map_eq_diff";
+
+Goalw [lift_map_def]
+ "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i~=j |] \
+\ ==> EX g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))";
+by Auto_tac;
+by (blast_tac (claset() addDs [insert_map_eq_diff]) 1);
+qed "lift_map_eq_diff";
+
+Goal "F : preserves snd \
+\ ==> (lift i F : transient (lift_set j (A Times UNIV))) = \
+\ (i=j & F : transient (A Times UNIV) | A={})";
+by (case_tac "i=j" 1);
+by (auto_tac (claset(), simpset() addsimps [lift_transient]));
+by (auto_tac (claset(),
+ simpset() addsimps [lift_def, transient_def,
+ Domain_rename_act]));
+by (dtac subsetD 1);
+by (Blast_tac 1);
by Auto_tac;
-qed "drop_prog_guarantees_raw";
+ren "s f uu s' f' uu'" 1;
+by (subgoal_tac "f'=f & uu'=uu" 1);
+by (force_tac (claset() addSDs [preserves_imp_eq], simpset()) 2);
+by Auto_tac;
+by (dtac sym 1);
+by (dtac subsetD 1);
+by (rtac ImageI 1);
+by (etac rename_actI 1);
+by (force_tac (claset(), simpset() addsimps [lift_set_def]) 1);
+by (etac (lift_map_eq_diff RS exE) 1);
+by (assume_tac 1);
+by (dtac ComplD 1);
+by (etac notE 1 THEN etac ssubst 1 THEN Fast_tac 1);
+qed "lift_transient_eq_disj";
-Goal "[| F : X guarantees[v] Y; \
-\ projecting C (lift_map i) F X' X; \
-\ extending w C (lift_map i) F Y' Y; \
-\ preserves w <= preserves (v o sub i) |] \
-\ ==> lift_prog i F : X' guarantees[w] Y'";
-by (asm_simp_tac
- (simpset() addsimps [lift_prog_correct, fold_o_sub,
- lift_export0 project_guarantees]) 1);
-qed "drop_prog_guarantees";
+(*USELESS??*)
+Goal "lift_map i `` (A Times UNIV) = \
+\ (UN s:A. UN f. {insert_map i s f}) Times UNIV";
+by (auto_tac (claset() addSIs [bexI, image_eqI],
+ simpset() addsimps [lift_map_def]));
+by (rtac (split RS sym) 1);
+qed "lift_map_image_Times";
+
+Goal "(lift i F : preserves v) = (F : preserves (v o lift_map i))";
+by (simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1);
+qed "lift_preserves_eq";
+
+Goal "F : preserves snd \
+\ ==> lift i F : preserves (v o sub j o fst) = \
+\ (if i=j then F : preserves (v o fst) else True)";
+by (dtac (impOfSubs subset_preserves_o) 1);
+by (full_simp_tac (simpset() addsimps [lift_preserves_eq, o_def,
+ drop_map_lift_map_eq]) 1);
+by (asm_simp_tac (simpset() delcongs [if_weak_cong]
+ addsimps [lift_map_def,
+ eq_commute, split_def, o_def]) 1);
+by Auto_tac;
+qed "lift_preserves_sub";
-(** Are these two useful?? **)
-(*The other direction fails: having FF : Stable {s. z <= f (s i)} does not
- ensure that F has the form lift_prog i F for some F.*)
-Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}";
-by Auto_tac;
-by (stac Collect_eq_lift_set 1);
-by (asm_simp_tac (simpset() addsimps [lift_prog_Stable]) 1);
-qed "image_lift_prog_Stable";
-
-Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)";
-by (simp_tac (simpset() addsimps [Increasing_def,
- inj_lift_prog RS image_INT]) 1);
-by (blast_tac (claset() addIs [impOfSubs image_lift_prog_Stable]) 1);
-qed "image_lift_prog_Increasing";
-
-
-(*** guarantees corollaries ***)
+(*** guarantees corollaries [NOT USED]
Goal "F : UNIV guarantees[v] increasing func \
-\ ==> lift_prog i F : UNIV guarantees[v o sub i] increasing (func o sub i)";
+\ ==> lift i F : UNIV guarantees[v o sub i] increasing (func o sub i)";
by (dtac (lift_export0 extend_guar_increasing) 1);
-by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
-qed "lift_prog_guar_increasing";
+by (asm_full_simp_tac (simpset() addsimps [lift_correct, o_def]) 1);
+qed "lift_guar_increasing";
Goal "F : UNIV guarantees[v] Increasing func \
-\ ==> lift_prog i F : UNIV guarantees[v o sub i] Increasing (func o sub i)";
+\ ==> lift i F : UNIV guarantees[v o sub i] Increasing (func o sub i)";
by (dtac (lift_export0 extend_guar_Increasing) 1);
-by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
-qed "lift_prog_guar_Increasing";
+by (asm_full_simp_tac (simpset() addsimps [lift_correct, o_def]) 1);
+qed "lift_guar_Increasing";
Goal "F : Always A guarantees[v] Always B \
-\ ==> lift_prog i F : \
+\ ==> lift i F : \
\ Always(lift_set i A) guarantees[v o sub i] Always (lift_set i B)";
by (asm_simp_tac
- (simpset() addsimps [lift_set_correct, lift_prog_correct,
+ (simpset() addsimps [lift_set_correct, lift_correct,
lift_export0 extend_guar_Always]) 1);
-qed "lift_prog_guar_Always";
-
-(*version for outside use*)
-fun lift_export th =
- good_map_lift_map RS export th
- |> simplify
- (simpset() addsimps [fold_o_sub,
- drop_set_correct RS sym,
- lift_set_correct RS sym,
- drop_prog_correct RS sym,
- lift_prog_correct RS sym]);;
-
+qed "lift_guar_Always";
+***)
--- a/src/HOL/UNITY/Lift_prog.thy Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Fri Feb 18 15:20:44 2000 +0100
@@ -6,35 +6,29 @@
lift_prog, etc: replication of components
*)
-Lift_prog = Project +
+Lift_prog = Rename +
constdefs
- lift_map :: "['a, 'b * ('a => 'b)] => ('a => 'b)"
- "lift_map i == %(s,f). f(i := s)"
-
- lift_set :: "['a, 'b set] => ('a => 'b) set"
- "lift_set i A == {f. f i : A}"
+ insert_map :: "[nat, 'b, nat=>'b] => (nat=>'b)"
+ "insert_map i z f k == if k<i then f k
+ else if k=i then z
+ else f(k-1)"
- drop_set :: "['a, ('a=>'b) set] => 'b set"
- "drop_set i A == (%f. f i) `` A"
-
- lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
- "lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}"
+ delete_map :: "[nat, nat=>'b] => (nat=>'b)"
+ "delete_map i g k == if k<i then g k else g (Suc k)"
- drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
- "drop_act i act == {(f i, f' i) | f f'. (f,f'): act}"
+ lift_map :: "[nat, 'b * ((nat=>'b) * 'c)] => (nat=>'b) * 'c"
+ "lift_map i == %(s,(f,uu)). (insert_map i s f, uu)"
+
+ drop_map :: "[nat, (nat=>'b) * 'c] => 'b * ((nat=>'b) * 'c)"
+ "drop_map i == %(g, uu). (g i, (delete_map i g, uu))"
- lift_prog :: "['a, 'b program] => ('a => 'b) program"
- "lift_prog i F ==
- mk_program (lift_set i (Init F),
- lift_act i `` Acts F)"
+ lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set"
+ "lift_set i A == lift_map i `` A"
- (*Argument C allows weak safety laws to be projected*)
- drop_prog :: "['a, ('a=>'b) set, ('a=>'b) program] => 'b program"
- "drop_prog i C F ==
- mk_program (drop_set i (Init F),
- drop_act i `` Restrict C `` (Acts F))"
+ lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program"
+ "lift i == rename (lift_map i)"
(*simplifies the expression of specifications*)
constdefs
--- a/src/HOL/UNITY/PPROD.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/PPROD.ML Fri Feb 18 15:20:44 2000 +0100
@@ -6,24 +6,20 @@
Abstraction over replicated components (PLam)
General products of programs (Pi operation)
-Probably some dead wood here!
+Some dead wood here!
*)
-
-val image_eqI' = read_instantiate_sg (sign_of thy)
- [("x", "?ff(i := ?u)")] image_eqI;
-
(*** Basic properties ***)
-Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
-by Auto_tac;
+Goal "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
+by (simp_tac (simpset() addsimps [PLam_def, lift_def, lift_set_def]) 1);
qed "Init_PLam";
-Goal "Acts (PLam I F) = insert Id (UN i:I. lift_act i `` Acts (F i))";
-by (auto_tac (claset(),
- simpset() addsimps [PLam_def]));
+(*The "insert Id" is needed if I={}, since otherwise the RHS would be {} too*)
+Goal "Acts (PLam I F) = \
+\ insert Id (UN i:I. rename_act (lift_map i) `` Acts (F i))";
+by (simp_tac (simpset() addsimps [PLam_def, lift_def]) 1);
qed "Acts_PLam";
-
Addsimps [Init_PLam, Acts_PLam];
Goal "PLam {} F = SKIP";
@@ -31,21 +27,20 @@
qed "PLam_empty";
Goal "(plam i: I. SKIP) = SKIP";
-by (simp_tac (simpset() addsimps [PLam_def,lift_prog_SKIP,JN_constant]) 1);
+by (simp_tac (simpset() addsimps [PLam_def,lift_SKIP,JN_constant]) 1);
qed "PLam_SKIP";
Addsimps [PLam_SKIP, PLam_empty];
-Goalw [PLam_def]
- "PLam (insert i I) F = (lift_prog i (F i)) Join (PLam I F)";
+Goalw [PLam_def] "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)";
by Auto_tac;
qed "PLam_insert";
-Goal "((PLam I F) <= H) = (ALL i: I. lift_prog i (F i) <= H)";
+Goal "((PLam I F) <= H) = (ALL i: I. lift i (F i) <= H)";
by (simp_tac (simpset() addsimps [PLam_def, JN_component_iff]) 1);
qed "PLam_component_iff";
-Goalw [PLam_def] "i : I ==> lift_prog i (F i) <= (PLam I F)";
+Goalw [PLam_def] "i : I ==> lift i (F i) <= (PLam I F)";
(*blast_tac doesn't use HO unification*)
by (fast_tac (claset() addIs [component_JN]) 1);
qed "component_PLam";
@@ -53,240 +48,223 @@
(** Safety & Progress **)
-Goal "i : I ==> \
-\ (PLam I F : (lift_set i A) co (lift_set i B)) = \
-\ (F i : A co B)";
-by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains]) 1);
-by (blast_tac (claset() addIs [lift_prog_constrains RS iffD1,
- constrains_imp_lift_prog_constrains]) 1);
+Goal "[| i : I; ALL j. F j : preserves snd |] ==> \
+\ (PLam I F : (lift_set i (A Times UNIV)) co \
+\ (lift_set i (B Times UNIV))) = \
+\ (F i : (A Times UNIV) co (B Times UNIV))";
+by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains,
+ Join_constrains]) 1);
+by (stac (insert_Diff RS sym) 1 THEN assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [lift_constrains]) 1);
+by (blast_tac (claset() addIs [constrains_imp_lift_constrains]) 1);
qed "PLam_constrains";
-Goal "i : I ==> (PLam I F : stable (lift_set i A)) = (F i : stable A)";
+Goal "[| i : I; ALL j. F j : preserves snd |] \
+\ ==> (PLam I F : stable (lift_set i (A Times UNIV))) = \
+\ (F i : stable (A Times UNIV))";
by (asm_simp_tac (simpset() addsimps [stable_def, PLam_constrains]) 1);
qed "PLam_stable";
Goal "i : I ==> \
-\ PLam I F : transient A = (EX i:I. lift_prog i (F i) : transient A)";
+\ PLam I F : transient A = (EX i:I. lift i (F i) : transient A)";
by (asm_simp_tac (simpset() addsimps [JN_transient, PLam_def]) 1);
qed "PLam_transient";
Addsimps [PLam_constrains, PLam_stable, PLam_transient];
-Goal "[| i : I; F i : A ensures B |] ==> \
-\ PLam I F : (lift_set i A) ensures lift_set i B";
+(*This holds because the F j cannot change (lift_set i)*)
+Goal "[| i : I; F i : (A Times UNIV) ensures (B Times UNIV); \
+\ ALL j. F j : preserves snd |] ==> \
+\ PLam I F : lift_set i (A Times UNIV) ensures lift_set i (B Times UNIV)";
by (auto_tac (claset(),
- simpset() addsimps [ensures_def, lift_prog_transient_eq_disj]));
+ simpset() addsimps [ensures_def, lift_transient_eq_disj,
+ lift_set_Un_distrib RS sym,
+ lift_set_Diff_distrib RS sym,
+ Times_Un_distrib1 RS sym,
+ Times_Diff_distrib1 RS sym]));
qed "PLam_ensures";
-Goal "[| i : I; F i : (A-B) co (A Un B); F i : transient (A-B) |] ==> \
-\ PLam I F : (lift_set i A) leadsTo lift_set i B";
+Goal "[| i : I; \
+\ F i : ((A Times UNIV) - (B Times UNIV)) co \
+\ ((A Times UNIV) Un (B Times UNIV)); \
+\ F i : transient ((A Times UNIV) - (B Times UNIV)); \
+\ ALL j. F j : preserves snd |] ==> \
+\ PLam I F : lift_set i (A Times UNIV) leadsTo lift_set i (B Times UNIV)";
by (rtac (PLam_ensures RS leadsTo_Basis) 1);
by (rtac ensuresI 2);
by (ALLGOALS assume_tac);
qed "PLam_leadsTo_Basis";
-Goal "[| PLam I F : AA co BB; i: I |] \
-\ ==> F i : (drop_set i AA) co (drop_set i BB)";
-by (rtac lift_prog_constrains_drop_set 1);
-(*rotate this assumption to be last*)
-by (dres_inst_tac [("psi", "PLam I F : ?C")] asm_rl 1);
-by (asm_full_simp_tac (simpset() addsimps [PLam_def, JN_constrains]) 1);
-qed "PLam_constrains_drop_set";
-
(** invariant **)
-Goal "[| F i : invariant A; i : I |] \
-\ ==> PLam I F : invariant (lift_set i A)";
+Goal "[| F i : invariant (A Times UNIV); i : I; \
+\ ALL j. F j : preserves snd |] \
+\ ==> PLam I F : invariant (lift_set i (A Times UNIV))";
by (auto_tac (claset(),
simpset() addsimps [invariant_def]));
qed "invariant_imp_PLam_invariant";
-(*The f0 premise ensures that the product is well-defined.*)
-Goal "[| PLam I F : invariant (lift_set i A); i : I; \
-\ f0: Init (PLam I F) |] ==> F i : invariant A";
-by (auto_tac (claset(),
- simpset() addsimps [invariant_def]));
-by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1);
-by Auto_tac;
-qed "PLam_invariant_imp_invariant";
+
+Goal "ALL j. F j : preserves snd \
+\ ==> (PLam I F : preserves (v o sub j o fst)) = \
+\ (if j: I then F j : preserves (v o fst) else True)";
+by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_sub]) 1);
+by (Blast_tac 1);
+qed "PLam_preserves";
+Addsimps [PLam_preserves];
+
-Goal "[| i : I; f0: Init (PLam I F) |] \
-\ ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)";
-by (blast_tac (claset() addIs [invariant_imp_PLam_invariant,
- PLam_invariant_imp_invariant]) 1);
-qed "PLam_invariant";
+(**UNUSED
+ (*The f0 premise ensures that the product is well-defined.*)
+ Goal "[| PLam I F : invariant (lift_set i A); i : I; \
+ \ f0: Init (PLam I F) |] ==> F i : invariant A";
+ by (auto_tac (claset(),
+ simpset() addsimps [invariant_def]));
+ by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1);
+ by Auto_tac;
+ qed "PLam_invariant_imp_invariant";
-(*The f0 premise isn't needed if F is a constant program because then
- we get an initial state by replicating that of F*)
-Goal "i : I \
-\ ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)";
-by (auto_tac (claset(),
- simpset() addsimps [invariant_def]));
-qed "const_PLam_invariant";
+ Goal "[| i : I; f0: Init (PLam I F) |] \
+ \ ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)";
+ by (blast_tac (claset() addIs [invariant_imp_PLam_invariant,
+ PLam_invariant_imp_invariant]) 1);
+ qed "PLam_invariant";
+
+ (*The f0 premise isn't needed if F is a constant program because then
+ we get an initial state by replicating that of F*)
+ Goal "i : I \
+ \ ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)";
+ by (auto_tac (claset(),
+ simpset() addsimps [invariant_def]));
+ qed "const_PLam_invariant";
+**)
-(** Reachability **)
+(**UNUSED
+ (** Reachability **)
-Goal "[| f : reachable (PLam I F); i : I |] ==> f i : reachable (F i)";
-by (etac reachable.induct 1);
-by (auto_tac (claset() addIs reachable.intrs, simpset()));
-qed "reachable_PLam";
+ Goal "[| f : reachable (PLam I F); i : I |] ==> f i : reachable (F i)";
+ by (etac reachable.induct 1);
+ by (auto_tac (claset() addIs reachable.intrs, simpset()));
+ qed "reachable_PLam";
-(*Result to justify a re-organization of this file*)
-Goal "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))";
-by Auto_tac;
-result();
+ (*Result to justify a re-organization of this file*)
+ Goal "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))";
+ by Auto_tac;
+ result();
-Goal "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))";
-by (force_tac (claset() addSDs [reachable_PLam], simpset()) 1);
-qed "reachable_PLam_subset1";
+ Goal "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))";
+ by (force_tac (claset() addSDs [reachable_PLam], simpset()) 1);
+ qed "reachable_PLam_subset1";
-(*simplify using reachable_lift_prog??*)
-Goal "[| i ~: I; A : reachable (F i) |] \
-\ ==> ALL f. f : reachable (PLam I F) \
-\ --> f(i:=A) : reachable (lift_prog i (F i) Join PLam I F)";
-by (etac reachable.induct 1);
-by (ALLGOALS Clarify_tac);
-by (etac reachable.induct 1);
-(*Init, Init case*)
-by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
-(*Init of F, action of PLam F case*)
-by (res_inst_tac [("act","act")] reachable.Acts 1);
-by (Force_tac 1);
-by (assume_tac 1);
-by (force_tac (claset() addIs [ext], simpset()) 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 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 (res_inst_tac [("act","acta")] reachable.Acts 1);
-by (Force_tac 1);
-by (assume_tac 1);
-by (force_tac (claset() addIs [ext], simpset()) 1);
-qed_spec_mp "reachable_lift_Join_PLam";
-
-
-(*The index set must be finite: otherwise infinitely many copies of F can
- perform actions, and PLam can never catch up in finite time.*)
-Goal "finite I \
-\ ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)";
-by (etac finite_induct 1);
-by (Simp_tac 1);
-by (force_tac (claset() addDs [reachable_lift_Join_PLam],
- simpset() addsimps [PLam_insert]) 1);
-qed "reachable_PLam_subset2";
-
-Goal "finite I ==> \
-\ reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))";
-by (REPEAT_FIRST (ares_tac [equalityI,
- reachable_PLam_subset1,
- reachable_PLam_subset2]));
-qed "reachable_PLam_eq";
+ (*simplify using reachable_lift??*)
+ Goal "[| i ~: I; A : reachable (F i) |] \
+ \ ==> ALL f. f : reachable (PLam I F) \
+ \ --> f(i:=A) : reachable (lift i (F i) Join PLam I F)";
+ by (etac reachable.induct 1);
+ by (ALLGOALS Clarify_tac);
+ by (etac reachable.induct 1);
+ (*Init, Init case*)
+ by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
+ (*Init of F, action of PLam F case*)
+ by (res_inst_tac [("act","act")] reachable.Acts 1);
+ by (Force_tac 1);
+ by (assume_tac 1);
+ by (force_tac (claset() addIs [ext], simpset()) 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 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 (res_inst_tac [("act","acta")] reachable.Acts 1);
+ by (Force_tac 1);
+ by (assume_tac 1);
+ by (force_tac (claset() addIs [ext], simpset()) 1);
+ qed_spec_mp "reachable_lift_Join_PLam";
-(** Co **)
-
-Goal "[| F i : A Co B; i: I; finite I |] \
-\ ==> PLam I F : (lift_set i A) Co (lift_set i B)";
-by (auto_tac
- (claset(),
- simpset() addsimps [Constrains_def, Collect_conj_eq RS sym,
- reachable_PLam_eq]));
-by (auto_tac (claset(),
- simpset() addsimps [constrains_def, PLam_def]));
-by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
-qed "Constrains_imp_PLam_Constrains";
+ (*The index set must be finite: otherwise infinitely many copies of F can
+ perform actions, and PLam can never catch up in finite time.*)
+ Goal "finite I \
+ \ ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)";
+ by (etac finite_induct 1);
+ by (Simp_tac 1);
+ by (force_tac (claset() addDs [reachable_lift_Join_PLam],
+ simpset() addsimps [PLam_insert]) 1);
+ qed "reachable_PLam_subset2";
-Goal "[| ALL j:I. f0 j : A j; i: I |] \
-\ ==> drop_set i (INT j:I. lift_set j (A j)) = A i";
-by (force_tac (claset() addSIs [image_eqI'],
- simpset() addsimps [drop_set_def]) 1);
-qed "drop_set_INT_lift_set";
-
-(*Again, we need the f0 premise so that PLam I F has an initial state;
- otherwise its Co-property is vacuous.*)
-Goal "[| PLam I F : (lift_set i A) Co (lift_set i B); \
-\ i: I; finite I; f0: Init (PLam I F) |] \
-\ ==> F i : A Co B";
-by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
-by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1);
-by (blast_tac (claset() addIs [reachable.Init]) 2);
-by (dtac PLam_constrains_drop_set 1);
-by (assume_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [drop_set_Int_lift_set2,
- drop_set_INT_lift_set, reachable_PLam_eq]) 1);
-qed "PLam_Constrains_imp_Constrains";
+ Goal "finite I ==> \
+ \ reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))";
+ by (REPEAT_FIRST (ares_tac [equalityI,
+ reachable_PLam_subset1,
+ reachable_PLam_subset2]));
+ qed "reachable_PLam_eq";
-Goal "[| i: I; finite I; f0: Init (PLam I F) |] \
-\ ==> (PLam I F : (lift_set i A) Co (lift_set i B)) = \
-\ (F i : A Co B)";
-by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains,
- PLam_Constrains_imp_Constrains]) 1);
-qed "PLam_Constrains";
+ (** Co **)
-Goal "[| i: I; finite I; f0: Init (PLam I F) |] \
-\ ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)";
-by (asm_simp_tac (simpset() delsimps [Init_PLam]
- addsimps [Stable_def, PLam_Constrains]) 1);
-qed "PLam_Stable";
+ Goal "[| F i : A Co B; i: I; finite I |] \
+ \ ==> PLam I F : (lift_set i A) Co (lift_set i B)";
+ by (auto_tac
+ (claset(),
+ simpset() addsimps [Constrains_def, Collect_conj_eq RS sym,
+ reachable_PLam_eq]));
+ by (auto_tac (claset(),
+ simpset() addsimps [constrains_def, PLam_def]));
+ by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+ qed "Constrains_imp_PLam_Constrains";
+
-(** const_PLam (no dependence on i) doesn't require the f0 premise **)
-
-Goal "[| (plam x:I. F) : (lift_set i A) Co (lift_set i B); \
-\ i: I; finite I |] \
-\ ==> F : A Co B";
-by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
-by (dtac PLam_constrains_drop_set 1);
-by (assume_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [drop_set_INT,
- drop_set_Int_lift_set2, Collect_conj_eq RS sym,
- reachable_PLam_eq]) 1);
-qed "const_PLam_Constrains_imp_Constrains";
+ Goal "[| i: I; finite I; f0: Init (PLam I F) |] \
+ \ ==> (PLam I F : (lift_set i A) Co (lift_set i B)) = \
+ \ (F i : A Co B)";
+ by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains,
+ PLam_Constrains_imp_Constrains]) 1);
+ qed "PLam_Constrains";
-Goal "[| i: I; finite I |] \
-\ ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) = \
-\ (F : A Co B)";
-by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains,
- const_PLam_Constrains_imp_Constrains]) 1);
-qed "const_PLam_Constrains";
-
-Goal "[| i: I; finite I |] \
-\ ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)";
-by (asm_simp_tac (simpset() addsimps [Stable_def, const_PLam_Constrains]) 1);
-qed "const_PLam_Stable";
-
-Goalw [Increasing_def]
- "[| i: I; finite I |] \
-\ ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)";
-by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1);
-by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2);
-by (asm_full_simp_tac
- (simpset() addsimps [finite_lessThan, const_PLam_Stable]) 1);
-qed "const_PLam_Increasing";
+ Goal "[| i: I; finite I; f0: Init (PLam I F) |] \
+ \ ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)";
+ by (asm_simp_tac (simpset() delsimps [Init_PLam]
+ addsimps [Stable_def, PLam_Constrains]) 1);
+ qed "PLam_Stable";
-(*** guarantees properties ***)
+ (** const_PLam (no dependence on i) doesn't require the f0 premise **)
+
+ Goal "[| i: I; finite I |] \
+ \ ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) = \
+ \ (F : A Co B)";
+ by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains,
+ const_PLam_Constrains_imp_Constrains]) 1);
+ qed "const_PLam_Constrains";
+
+ Goal "[| i: I; finite I |] \
+ \ ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)";
+ by (asm_simp_tac (simpset() addsimps [Stable_def, const_PLam_Constrains]) 1);
+ qed "const_PLam_Stable";
-Goalw [PLam_def]
- "[| lift_prog i (F i): X guarantees[v] Y; i : I; \
-\ ALL j:I. i~=j --> lift_prog j (F j) : preserves v |] \
-\ ==> (PLam I F) : X guarantees[v] Y";
-by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
-qed "guarantees_PLam_I";
+ Goalw [Increasing_def]
+ "[| i: I; finite I |] \
+ \ ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)";
+ by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1);
+ by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2);
+ by (asm_full_simp_tac
+ (simpset() addsimps [finite_lessThan, const_PLam_Stable]) 1);
+ qed "const_PLam_Increasing";
+
-Goal "(PLam I F : preserves (v o sub j)) = \
-\ (if j: I then F j : preserves v else True)";
-by (asm_simp_tac (simpset() addsimps [PLam_def, lift_prog_preserves_sub]) 1);
-by (Blast_tac 1);
-qed "PLam_preserves";
+ (*** guarantees properties ***)
-AddIffs [PLam_preserves];
+ Goalw [PLam_def]
+ "[| lift i (F i): X guarantees[v] Y; i : I; \
+ \ ALL j:I. i~=j --> lift j (F j) : preserves v |] \
+ \ ==> (PLam I F) : X guarantees[v] Y";
+ by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
+ qed "guarantees_PLam_I";
+**)
+
--- a/src/HOL/UNITY/PPROD.thy Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/PPROD.thy Fri Feb 18 15:20:44 2000 +0100
@@ -11,11 +11,12 @@
constdefs
- PLam :: ['a set, 'a => 'b program] => ('a => 'b) program
- "PLam I F == JN i:I. lift_prog i (F i)"
+ PLam :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
+ => ((nat=>'b) * 'c) program"
+ "PLam I F == JN i:I. lift i (F i)"
syntax
- "@PLam" :: [pttrn, 'a set, 'b set] => ('a => 'b) set ("(3plam _:_./ _)" 10)
+ "@PLam" :: [pttrn, nat set, 'b set] => (nat => 'b) set ("(3plam _:_./ _)" 10)
translations
"plam x:A. B" == "PLam A (%x. B)"
--- a/src/HOL/UNITY/Project.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Project.ML Fri Feb 18 15:20:44 2000 +0100
@@ -10,66 +10,14 @@
Open_locale "Extend";
-(** projection: monotonicity for safety **)
-
-Goal "D <= C ==> \
-\ project_act h (Restrict D act) <= project_act h (Restrict C act)";
-by (auto_tac (claset(), simpset() addsimps [project_act_def]));
-qed "project_act_mono";
-
-Goal "[| D <= C; project h C F : A co B |] ==> project h D F : A co B";
-by (auto_tac (claset(), simpset() addsimps [constrains_def]));
-by (dtac project_act_mono 1);
-by (Blast_tac 1);
-qed "project_constrains_mono";
-
-Goal "[| D <= C; project h C F : stable A |] ==> project h D F : stable A";
-by (asm_full_simp_tac
- (simpset() addsimps [stable_def, project_constrains_mono]) 1);
-qed "project_stable_mono";
-
Goal "F : A co B ==> project h C (extend h F) : A co B";
by (auto_tac (claset(),
simpset() addsimps [extend_act_def, project_act_def, constrains_def]));
qed "project_extend_constrains_I";
-Goal "UNIV <= project_set h C \
-\ ==> project h C ((extend h F) Join G) = F Join (project h C G)";
-by (rtac program_equalityI 1);
-by (asm_simp_tac (simpset() addsimps [image_eq_UN, UN_Un,
- subset_UNIV RS subset_trans RS Restrict_triv]) 2);
-by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
-qed "project_extend_Join";
-
-Goal "UNIV <= project_set h C \
-\ ==> (extend h F) Join G = extend h H ==> H = F Join (project h C G)";
-by (dres_inst_tac [("f", "project h C")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
-qed "extend_Join_eq_extend_D";
-
(** Safety **)
-Goalw [constrains_def]
- "(project h C 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() addsimps [ball_Un]));
-by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
-(*the <== direction*)
-by (rewtac project_act_def);
-by (force_tac (claset() addSDs [subsetD], simpset()) 1);
-qed "project_constrains";
-
-Goalw [stable_def]
- "(project h UNIV F : stable A) = (F : stable (extend_set h A))";
-by (simp_tac (simpset() addsimps [project_constrains]) 1);
-qed "project_stable";
-
-Goal "F : stable (extend_set h A) ==> project h C F : stable A";
-by (dtac (project_stable RS iffD2) 1);
-by (blast_tac (claset() addIs [project_stable_mono]) 1);
-qed "project_stable_I";
-
(*used below to prove Join_project_ensures*)
Goal "[| G : stable C; project h C G : A unless B |] \
\ ==> G : (C Int extend_set h A) unless (extend_set h B)";
@@ -113,7 +61,7 @@
"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);
+ extend_set_eq_Collect]) 1);
qed "project_increasing_I";
Goal "(F Join project h UNIV G : increasing func) = \
@@ -123,7 +71,7 @@
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,
+ simpset() addsimps [Join_stable, extend_set_eq_Collect,
extend_stable RS iffD1]));
qed "Join_project_increasing";
@@ -136,32 +84,6 @@
qed "project_constrains_D";
-(*** preserves ***)
-
-Goal "G : preserves (v o f) ==> project h C G : preserves v";
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, project_stable_I,
- Collect_eq_extend_set RS sym]));
-qed "project_preserves_I";
-
-(*to preserve f is to preserve the whole original state*)
-Goal "G : preserves f ==> project h C G : preserves id";
-by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
-qed "project_preserves_id_I";
-
-Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, extend_stable RS sym,
- Collect_eq_extend_set RS sym]));
-qed "extend_preserves";
-
-Goal "inj h ==> (extend h G : preserves g)";
-by (auto_tac (claset(),
- simpset() addsimps [preserves_def, extend_def, extend_act_def,
- stable_def, constrains_def, g_def]));
-qed "inj_extend_preserves";
-
-
(*** "projecting" and union/intersection (no converses) ***)
Goalw [projecting_def]
@@ -315,7 +237,7 @@
"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);
+by (stac (extend_set_eq_Collect RS sym) 1);
by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1);
qed "project_Increasing_D";
@@ -381,7 +303,7 @@
"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,
+by (asm_simp_tac (simpset() addsimps [extend_set_eq_Collect,
project_Stable_I]) 1);
qed "project_Increasing_I";
@@ -400,7 +322,7 @@
"(F Join project h (reachable (extend h F Join G)) G : Increasing func) = \
\ (extend h F Join G : Increasing (func o f))";
by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
- Collect_eq_extend_set RS sym]) 1);
+ extend_set_eq_Collect]) 1);
qed "project_Increasing";
(** A lot of redundant theorems: all are proved to facilitate reasoning
@@ -662,38 +584,9 @@
qed "project_Ensures_D";
-(*** GUARANTEES and EXTEND ***)
-
-(** Strong precondition and postcondition; doesn't seem very useful. **)
-
-Goal "F : X guarantees[v] Y ==> \
-\ extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
-by (rtac guaranteesI 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [project_preserves_I]
- addDs [project_set_UNIV RS equalityD2 RS
- extend_Join_eq_extend_D,
- guaranteesD]) 1);
-qed "guarantees_imp_extend_guarantees";
+(*** Guarantees ***)
-Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
-\ ==> F : X guarantees[v] Y";
-by (auto_tac (claset(), simpset() addsimps [guar_def]));
-by (dres_inst_tac [("x", "extend h G")] spec 1);
-by (asm_full_simp_tac
- (simpset() delsimps [extend_Join]
- addsimps [extend_Join RS sym, extend_preserves,
- inj_extend RS inj_image_mem_iff]) 1);
-qed "extend_guarantees_imp_guarantees";
-
-Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
-\ (F : X guarantees[v] Y)";
-by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
- extend_guarantees_imp_guarantees]) 1);
-qed "extend_guarantees_eq";
-
-
-(*Weak precondition and postcondition; this is the good one!
+(*Weak precondition and postcondition
Not clear that it has a converse [or that we want one!]*)
(*The raw version*)
--- a/src/HOL/UNITY/ROOT.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/ROOT.ML Fri Feb 18 15:20:44 2000 +0100
@@ -28,7 +28,9 @@
time_use_thy "Extend";
time_use_thy "PPROD";
time_use_thy "TimerArray";
+(**
time_use_thy "Alloc";
+**)
add_path "../Auth"; (*to find Public.thy*)
use_thy"NSP_Bad";
--- a/src/HOL/UNITY/TimerArray.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/TimerArray.ML Fri Feb 18 15:20:44 2000 +0100
@@ -9,26 +9,40 @@
Addsimps [Timer_def RS def_prg_Init];
program_defs_ref := [Timer_def];
-Addsimps [decr_def];
+Addsimps [count_def, decr_def];
(*Demonstrates induction, but not used in the following proof*)
-Goal "Timer : UNIV leadsTo {0}";
-by (res_inst_tac [("f", "id")] (allI RS lessThan_induct) 1);
+Goal "Timer : UNIV leadsTo {s. count s = 0}";
+by (res_inst_tac [("f", "count")] lessThan_induct 1);
by (Simp_tac 1);
by (exhaust_tac "m" 1);
-by (blast_tac (claset() addSIs [subset_imp_leadsTo]) 1);
+by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 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}")]
+Goal "Timer : preserves snd";
+by (rtac preservesI 1);
+by (constrains_tac 1);
+qed "Timer_preserves_snd";
+AddIffs [Timer_preserves_snd];
+
+
+Goal "finite I \
+\ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";
+by (eres_inst_tac [("A'1", "%i. lift_set i ({0} Times UNIV)")]
(finite_stable_completion RS leadsTo_weaken) 1);
by Auto_tac;
+(*Safety property, already reduced to the single Timer case*)
by (constrains_tac 2);
-by (res_inst_tac [("f", "sub i")] (allI RS lessThan_induct) 1);
+(*Progress property for the array of Timers*)
+by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
by (exhaust_tac "m" 1);
+(*Annoying need to massage the conditions to have the form (... Times UNIV)*)
by (auto_tac (claset() addIs [subset_imp_leadsTo],
- simpset() addsimps [insert_absorb, lessThan_Suc RS sym]));
+ simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
+ lift_set_Un_distrib RS sym,
+ Times_Un_distrib1 RS sym,
+ Times_Diff_distrib1 RS sym]));
by (rename_tac "n" 1);
by (rtac PLam_leadsTo_Basis 1);
by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
--- a/src/HOL/UNITY/TimerArray.thy Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/TimerArray.thy Fri Feb 18 15:20:44 2000 +0100
@@ -8,11 +8,16 @@
TimerArray = PPROD +
+types 'a state = "nat * 'a" (*second component allows new variables*)
+
constdefs
- decr :: "(nat*nat) set"
- "decr == UN n. {(Suc n, n)}"
+ count :: "'a state => nat"
+ "count s == fst s"
- Timer :: nat program
+ decr :: "('a state * 'a state) set"
+ "decr == UN n uu. {((Suc n, uu), (n,uu))}"
+
+ Timer :: 'a state program
"Timer == mk_program (UNIV, {decr})"
end
--- a/src/HOL/UNITY/Union.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/Union.ML Fri Feb 18 15:20:44 2000 +0100
@@ -168,7 +168,9 @@
(*** Safety: co, stable, FP ***)
-(*Fails if I={} because it collapses to SKIP : A co B*)
+(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B. So an
+ alternative precondition is A<=B, but most proofs using this rule require
+ I to be nonempty for other reasons anyway.*)
Goalw [constrains_def, JOIN_def]
"i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)";
by (Simp_tac 1);
@@ -196,6 +198,7 @@
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "Join_constrains_weaken";
+(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*)
Goal "[| ALL i:I. F i : A i co A' i; i: I |] \
\ ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)";
by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1);
@@ -258,10 +261,10 @@
by (asm_simp_tac (simpset() addsimps [Join_transient]) 1);
qed "Join_transient_I2";
+(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
Goal "i : I ==> \
\ (JN i:I. F i) : A ensures B = \
-\ ((ALL i:I. F i : (A-B) co (A Un B)) & \
-\ (EX i:I. F i : A ensures B))";
+\ ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))";
by (auto_tac (claset(),
simpset() addsimps [ensures_def, JN_constrains, JN_transient]));
qed "JN_ensures";
--- a/src/HOL/UNITY/WFair.ML Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/WFair.ML Fri Feb 18 15:20:44 2000 +0100
@@ -401,11 +401,12 @@
(*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
-Goal "[| ALL m. F : (A Int f-``{m}) leadsTo \
-\ ((A Int f-``(lessThan m)) Un B) |] \
+val prems =
+Goal "[| !!m. F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
\ ==> F : A leadsTo B";
by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
by (Asm_simp_tac 1);
+by (blast_tac (claset() addIs prems) 1);
qed "lessThan_induct";
Goal "[| ALL m:(greaterThan l). \