--- a/src/HOL/UNITY/Alloc.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Alloc.ML Fri Jul 21 18:01:36 2000 +0200
@@ -49,7 +49,7 @@
val record_auto_tac =
auto_tac (claset() addIs [ext] addSWrapper record_split_wrapper,
simpset() addsimps [sysOfAlloc_def, sysOfClient_def,
- client_map_def, non_extra_def, funPair_def,
+ client_map_def, non_dummy_def, funPair_def,
o_apply, Let_def]);
@@ -64,7 +64,7 @@
\ (| allocGiv = allocGiv s, \
\ allocAsk = allocAsk s, \
\ allocRel = allocRel s, \
-\ allocState_u.extra = (client s, extra s) |)";
+\ allocState_d.dummy = (client s, dummy s) |)";
by (rtac (inj_sysOfAlloc RS inv_f_eq) 1);
by record_auto_tac;
qed "inv_sysOfAlloc_eq";
@@ -95,7 +95,7 @@
\ (| allocGiv = allocGiv s, \
\ allocAsk = allocAsk s, \
\ allocRel = allocRel s, \
-\ allocState_u.extra = systemState.extra s|) )";
+\ allocState_d.dummy = systemState.dummy s|) )";
by (rtac (inj_sysOfClient RS inv_f_eq) 1);
by record_auto_tac;
qed "inv_sysOfClient_eq";
@@ -122,7 +122,7 @@
Goal "!!s. inv client_map s = \
\ (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, \
-\ clientState_u.extra = y|)) s";
+\ clientState_d.dummy = y|)) s";
by (rtac (inj_client_map RS inv_f_eq) 1);
by record_auto_tac;
qed "inv_client_map_eq";
@@ -142,19 +142,19 @@
(** o-simprules for client_map **)
-Goalw [client_map_def] "fst o client_map = non_extra";
+Goalw [client_map_def] "fst o client_map = non_dummy";
by (rtac fst_o_funPair 1);
qed "fst_o_client_map";
Addsimps (make_o_equivs fst_o_client_map);
-Goalw [client_map_def] "snd o client_map = clientState_u.extra";
+Goalw [client_map_def] "snd o client_map = clientState_d.dummy";
by (rtac snd_o_funPair 1);
qed "snd_o_client_map";
Addsimps (make_o_equivs snd_o_client_map);
(** o-simprules for sysOfAlloc [MUST BE AUTOMATED] **)
-Goal "client o sysOfAlloc = fst o allocState_u.extra ";
+Goal "client o sysOfAlloc = fst o allocState_d.dummy ";
by record_auto_tac;
qed "client_o_sysOfAlloc";
Addsimps (make_o_equivs client_o_sysOfAlloc);
@@ -220,13 +220,13 @@
val [Client_Increasing_ask, Client_Increasing_rel,
Client_Bounded, Client_Progress, Client_preserves_giv,
- Client_preserves_extra] =
+ Client_preserves_dummy] =
Client_Spec
|> simplify (simpset() addsimps [guarantees_Int_right])
|> list_of_Int;
AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded,
- Client_preserves_giv, Client_preserves_extra];
+ Client_preserves_giv, Client_preserves_dummy];
(*Network : <unfolded specification> *)
@@ -319,7 +319,7 @@
bij_imp_bij_inv, surj_rename RS surj_range,
inv_inv_eq]) 1,
asm_simp_tac
- (simpset() addsimps [o_def, non_extra_def, guarantees_Int_right]) 1];
+ (simpset() addsimps [o_def, non_dummy_def, guarantees_Int_right]) 1];
(*Lifting Client_Increasing to systemState*)
@@ -379,7 +379,7 @@
by (auto_tac (claset() addSIs [Network_Giv RS component_guaranteesD,
rename_Alloc_Increasing RS component_guaranteesD],
simpset()));
-by (ALLGOALS (simp_tac (simpset() addsimps [o_def, non_extra_def])));
+by (ALLGOALS (simp_tac (simpset() addsimps [o_def, non_dummy_def])));
by (auto_tac
(claset() addSIs [rename_Alloc_Increasing RS component_guaranteesD],
simpset()));
@@ -406,14 +406,16 @@
(*** Proof of the safety property (1) ***)
-(*safety (1), step 1 is System_Increasing_rel*)
+(*safety (1), step 1 is System_Follows_rel*)
(*safety (1), step 2*)
-Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
-by (etac (System_Follows_rel RS Follows_Increasing1) 1);
-qed "System_Increasing_allocRel";
+(* i < Nclients ==> System : Increasing (sub i o allocRel) *)
+bind_thm ("System_Increasing_allocRel",
+ System_Follows_rel RS Follows_Increasing1);
-(*Lifting Alloc_safety up to the level of systemState*)
+(*Lifting Alloc_safety up to the level of systemState.
+ Simplififying with o_def gets rid of the translations but it unfortunately
+ gets rid of the other "o"s too.*)
val rename_Alloc_Safety =
Alloc_Safety RS rename_guarantees_sysOfAlloc_I
|> simplify (simpset() addsimps [o_def]);
@@ -427,7 +429,7 @@
by (simp_tac (simpset() addsimps [o_apply]) 1);
by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1);
by (auto_tac (claset(),
- simpset() addsimps [o_simp System_Increasing_allocRel]));
+ simpset() addsimps [o_simp System_Increasing_allocRel]));
qed "System_sum_bounded";
@@ -464,19 +466,14 @@
(*** Proof of the progress property (2) ***)
-(*Now there are proofs identical to System_Increasing_rel and
- System_Increasing_allocRel: tactics needed!*)
-
-(*progress (2), step 1 is System_Increasing_ask and System_Increasing_rel*)
+(*progress (2), step 1 is System_Follows_ask and System_Follows_rel*)
(*progress (2), step 2; see also System_Increasing_allocRel*)
-Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)";
-by (etac (System_Follows_ask RS Follows_Increasing1) 1);
-qed "System_Increasing_allocAsk";
+(* i < Nclients ==> System : Increasing (sub i o allocAsk) *)
+bind_thm ("System_Increasing_allocAsk",
+ System_Follows_ask RS Follows_Increasing1);
-(*progress (2), step 3*)
-(*All this trouble just to lift "Client_Bounded" to systemState
- (though it is similar to that for Client_Increasing*)
+(*progress (2), step 3: lifting "Client_Bounded" to systemState*)
Goal "i : I \
\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \
\ UNIV \
@@ -498,10 +495,9 @@
qed "Collect_all_imp_eq";
(*progress (2), step 4*)
-Goal "System : Always {s. ALL i. i<Nclients --> \
-\ (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}";
-by (auto_tac (claset(),
- simpset() addsimps [Collect_all_imp_eq]));
+Goal "System : Always {s. ALL i<Nclients. \
+\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}";
+by (auto_tac (claset(), simpset() addsimps [Collect_all_imp_eq]));
by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask]
RS Always_weaken) 1);
by (auto_tac (claset() addDs [set_mono], simpset()));
@@ -510,9 +506,9 @@
(*progress (2), step 5 is System_Increasing_allocGiv*)
(*progress (2), step 6*)
-Goal "i < Nclients ==> System : Increasing (giv o sub i o client)";
-by (etac (System_Follows_allocGiv RS Follows_Increasing1) 1);
-qed "System_Increasing_giv";
+(* i < Nclients ==> System : Increasing (giv o sub i o client) *)
+bind_thm ("System_Increasing_giv",
+ System_Follows_allocGiv RS Follows_Increasing1);
Goal "i: I \
@@ -523,8 +519,7 @@
\ h pfixGe (ask o sub i o client) s} \
\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
by rename_client_map_tac;
-by (asm_simp_tac
- (simpset() addsimps [rewrite_rule [o_def] Client_Progress]) 1);
+by (asm_simp_tac (simpset() addsimps [o_simp Client_Progress]) 1);
qed "rename_Client_Progress";
@@ -538,8 +533,7 @@
(*Couldn't have just used Auto_tac since the "INT h" must be kept*)
by (rtac ([rename_Client_Progress,
Client_component_System] MRS component_guaranteesD) 1);
-by (asm_full_simp_tac (simpset() addsimps [System_Increasing_giv]) 2);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [System_Increasing_giv]));
qed "System_Client_Progress";
(*Concludes
@@ -609,13 +603,10 @@
(*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);
+by (cut_facts_tac [System_Alloc_Progress] 1);
+by (blast_tac (claset() addIs [LeadsTo_Trans,
+ System_Follows_allocGiv RS Follows_LeadsTo_pfixLe,
+ System_Follows_ask RS Follows_LeadsTo]) 1);
qed "System_Progress";
--- a/src/HOL/UNITY/Alloc.thy Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Alloc.thy Fri Jul 21 18:01:36 2000 +0200
@@ -15,19 +15,19 @@
ask :: nat list (*client's OUTPUT history: tokens REQUESTED*)
rel :: nat list (*client's OUTPUT history: tokens RELEASED*)
-record 'a clientState_u =
+record 'a clientState_d =
clientState +
- extra :: 'a (*dummy field for new variables*)
+ dummy :: 'a (*dummy field for new variables*)
constdefs
(*DUPLICATED FROM Client.thy, but with "tok" removed*)
(*Maybe want a special theory section to declare such maps*)
- non_extra :: 'a clientState_u => clientState
- "non_extra s == (|giv = giv s, ask = ask s, rel = rel s|)"
+ non_dummy :: 'a clientState_d => clientState
+ "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)"
(*Renaming map to put a Client into the standard form*)
- client_map :: "'a clientState_u => clientState*'a"
- "client_map == funPair non_extra extra"
+ client_map :: "'a clientState_d => clientState*'a"
+ "client_map == funPair non_dummy dummy"
record allocState =
@@ -35,14 +35,14 @@
allocAsk :: nat => nat list (*INPUT: allocator's copy of "ask" for i*)
allocRel :: nat => nat list (*INPUT: allocator's copy of "rel" for i*)
-record 'a allocState_u =
+record 'a allocState_d =
allocState +
- extra :: 'a (*dummy field for new variables*)
+ dummy :: 'a (*dummy field for new variables*)
record 'a systemState =
allocState +
client :: nat => clientState (*states of all clients*)
- extra :: 'a (*dummy field for new variables*)
+ dummy :: 'a (*dummy field for new variables*)
constdefs
@@ -68,19 +68,19 @@
(** Client specification (required) ***)
(*spec (3)*)
- client_increasing :: 'a clientState_u program set
+ client_increasing :: 'a clientState_d program set
"client_increasing ==
UNIV guarantees[funPair rel ask]
Increasing ask Int Increasing rel"
(*spec (4)*)
- client_bounded :: 'a clientState_u program set
+ client_bounded :: 'a clientState_d program set
"client_bounded ==
UNIV guarantees[ask]
Always {s. ALL elt : set (ask s). elt <= NbT}"
(*spec (5)*)
- client_progress :: 'a clientState_u program set
+ client_progress :: 'a clientState_d program set
"client_progress ==
Increasing giv
guarantees[funPair rel ask]
@@ -88,24 +88,24 @@
LeadsTo {s. tokens h <= (tokens o rel) s})"
(*spec: preserves part*)
- client_preserves :: 'a clientState_u program set
- "client_preserves == preserves (funPair giv clientState_u.extra)"
+ client_preserves :: 'a clientState_d program set
+ "client_preserves == preserves (funPair giv clientState_d.dummy)"
- client_spec :: 'a clientState_u program set
+ client_spec :: 'a clientState_d program set
"client_spec == client_increasing Int client_bounded Int client_progress
Int client_preserves"
(** Allocator specification (required) ***)
(*spec (6)*)
- alloc_increasing :: 'a allocState_u program set
+ alloc_increasing :: 'a allocState_d program set
"alloc_increasing ==
UNIV
guarantees[allocGiv]
(INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
(*spec (7)*)
- alloc_safety :: 'a allocState_u program set
+ alloc_safety :: 'a allocState_d program set
"alloc_safety ==
(INT i : lessThan Nclients. Increasing (sub i o allocRel))
guarantees[allocGiv]
@@ -113,13 +113,13 @@
<= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
(*spec (8)*)
- alloc_progress :: 'a allocState_u program set
+ alloc_progress :: 'a allocState_d program set
"alloc_progress ==
(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
Increasing (sub i o allocRel))
Int
- Always {s. ALL i. i<Nclients -->
- (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}
+ Always {s. ALL i<Nclients.
+ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}
Int
(INT i : lessThan Nclients.
INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
@@ -139,11 +139,11 @@
looked at.*)
(*spec: preserves part*)
- alloc_preserves :: 'a allocState_u program set
+ alloc_preserves :: 'a allocState_d program set
"alloc_preserves == preserves (funPair allocRel
- (funPair allocAsk allocState_u.extra))"
+ (funPair allocAsk allocState_d.dummy))"
- alloc_spec :: 'a allocState_u program set
+ alloc_spec :: 'a allocState_d program set
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
alloc_preserves"
@@ -182,25 +182,25 @@
(** State mappings **)
- sysOfAlloc :: "((nat => clientState) * 'a) allocState_u => 'a systemState"
- "sysOfAlloc == %s. let (cl,xtr) = allocState_u.extra s
+ sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
+ "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
in (| allocGiv = allocGiv s,
allocAsk = allocAsk s,
allocRel = allocRel s,
client = cl,
- extra = xtr|)"
+ dummy = xtr|)"
- sysOfClient :: "(nat => clientState) * 'a allocState_u => 'a systemState"
+ sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState"
"sysOfClient == %(cl,al). (| allocGiv = allocGiv al,
allocAsk = allocAsk al,
allocRel = allocRel al,
client = cl,
- systemState.extra = allocState_u.extra al|)"
+ systemState.dummy = allocState_d.dummy al|)"
consts
- Alloc :: 'a allocState_u program
- Client :: 'a clientState_u program
+ Alloc :: 'a allocState_d program
+ Client :: 'a clientState_d program
Network :: 'a systemState program
System :: 'a systemState program
@@ -219,8 +219,8 @@
(**
locale System =
fixes
- Alloc :: 'a allocState_u program
- Client :: 'a clientState_u program
+ Alloc :: 'a allocState_d program
+ Client :: 'a clientState_d program
Network :: 'a systemState program
System :: 'a systemState program
--- a/src/HOL/UNITY/AllocImpl.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/AllocImpl.ML Fri Jul 21 18:01:36 2000 +0200
@@ -4,9 +4,6 @@
Copyright 2000 University of Cambridge
Implementation of a multiple-client allocator from a single-client allocator
-
-add_path "../Induct";
-time_use_thy "AllocImpl";
*)
AddIs [impOfSubs subset_preserves_o];
--- a/src/HOL/UNITY/AllocImpl.thy Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/AllocImpl.thy Fri Jul 21 18:01:36 2000 +0200
@@ -4,9 +4,6 @@
Copyright 1998 University of Cambridge
Implementation of a multiple-client allocator from a single-client allocator
-
-add_path "../Induct";
-with_path "../Induct" time_use_thy "AllocImpl";
*)
AllocImpl = AllocBase + Follows + PPROD +
@@ -20,38 +17,38 @@
Out :: 'b list (*merge's OUTPUT history: merged items*)
iOut :: nat list (*merge's OUTPUT history: origins of merged items*)
-record ('a,'b) merge_u =
+record ('a,'b) merge_d =
'b merge +
- extra :: 'a (*dummy field for new variables*)
+ dummy :: 'a (*dummy field for new variables*)
constdefs
- non_extra :: ('a,'b) merge_u => 'b merge
- "non_extra s == (|In = In s, Out = Out s, iOut = iOut s|)"
+ non_dummy :: ('a,'b) merge_d => 'b merge
+ "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
record 'b distr =
In :: 'b list (*items to distribute*)
iIn :: nat list (*destinations of items to distribute*)
Out :: nat => 'b list (*distributed items*)
-record ('a,'b) distr_u =
+record ('a,'b) distr_d =
'b distr +
- extra :: 'a (*dummy field for new variables*)
+ dummy :: 'a (*dummy field for new variables*)
record allocState =
giv :: nat list (*OUTPUT history: source of tokens*)
ask :: nat list (*INPUT: tokens requested from allocator*)
rel :: nat list (*INPUT: tokens released to allocator*)
-record 'a allocState_u =
+record 'a allocState_d =
allocState +
- extra :: 'a (*dummy field for new variables*)
+ dummy :: 'a (*dummy field for new variables*)
record 'a systemState =
allocState +
mergeRel :: nat merge
mergeAsk :: nat merge
distr :: nat distr
- extra :: 'a (*dummy field for new variables*)
+ dummy :: 'a (*dummy field for new variables*)
constdefs
@@ -59,25 +56,25 @@
(** Merge specification (the number of inputs is Nclients) ***)
(*spec (10)*)
- merge_increasing :: ('a,'b) merge_u program set
+ merge_increasing :: ('a,'b) merge_d program set
"merge_increasing ==
UNIV guarantees[funPair merge.Out merge.iOut]
(Increasing merge.Out) Int (Increasing merge.iOut)"
(*spec (11)*)
- merge_eqOut :: ('a,'b) merge_u program set
+ merge_eqOut :: ('a,'b) merge_d program set
"merge_eqOut ==
UNIV guarantees[funPair merge.Out merge.iOut]
Always {s. length (merge.Out s) = length (merge.iOut s)}"
(*spec (12)*)
- merge_bounded :: ('a,'b) merge_u program set
+ merge_bounded :: ('a,'b) merge_d program set
"merge_bounded ==
UNIV guarantees[merge.iOut]
Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
(*spec (13)*)
- merge_follows :: ('a,'b) merge_u program set
+ merge_follows :: ('a,'b) merge_d program set
"merge_follows ==
(INT i : lessThan Nclients. Increasing (sub i o merge.In))
guarantees[funPair merge.Out merge.iOut]
@@ -87,17 +84,17 @@
Fols (sub i o merge.In))"
(*spec: preserves part*)
- merge_preserves :: ('a,'b) merge_u program set
- "merge_preserves == preserves (funPair merge.In merge_u.extra)"
+ merge_preserves :: ('a,'b) merge_d program set
+ "merge_preserves == preserves (funPair merge.In merge_d.dummy)"
- merge_spec :: ('a,'b) merge_u program set
+ merge_spec :: ('a,'b) merge_d program set
"merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
merge_follows Int merge_preserves"
(** Distributor specification (the number of outputs is Nclients) ***)
(*spec (14)*)
- distr_follows :: ('a,'b) distr_u program set
+ distr_follows :: ('a,'b) distr_d program set
"distr_follows ==
Increasing distr.In Int Increasing distr.iIn Int
Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
@@ -111,17 +108,17 @@
(** Single-client allocator specification (required) ***)
(*spec (18)*)
- alloc_increasing :: 'a allocState_u program set
+ alloc_increasing :: 'a allocState_d program set
"alloc_increasing == UNIV guarantees[giv] Increasing giv"
(*spec (19)*)
- alloc_safety :: 'a allocState_u program set
+ alloc_safety :: 'a allocState_d program set
"alloc_safety ==
Increasing rel
guarantees[giv] Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
(*spec (20)*)
- alloc_progress :: 'a allocState_u program set
+ alloc_progress :: 'a allocState_d program set
"alloc_progress ==
Increasing ask Int Increasing rel Int
Always {s. ALL elt : set (ask s). elt <= NbT}
@@ -133,11 +130,11 @@
(INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
(*spec: preserves part*)
- alloc_preserves :: 'a allocState_u program set
+ alloc_preserves :: 'a allocState_d program set
"alloc_preserves == preserves (funPair rel
- (funPair ask allocState_u.extra))"
+ (funPair ask allocState_d.dummy))"
- alloc_spec :: 'a allocState_u program set
+ alloc_spec :: 'a allocState_d program set
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
alloc_preserves"
@@ -177,26 +174,27 @@
(** State mappings **)
- sysOfAlloc :: "((nat => merge) * 'a) allocState_u => 'a systemState"
- "sysOfAlloc == %s. let (cl,xtr) = allocState_u.extra s
+ sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
+ "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
in (| giv = giv s,
ask = ask s,
rel = rel s,
client = cl,
- extra = xtr|)"
+ dummy = xtr|)"
- sysOfClient :: "(nat => merge) * 'a allocState_u => 'a systemState"
+ sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
"sysOfClient == %(cl,al). (| giv = giv al,
ask = ask al,
rel = rel al,
client = cl,
- systemState.extra = allocState_u.extra al|)"
+ systemState.dummy = allocState_d.dummy al|)"
****)
consts
- Alloc :: 'a allocState_u program
- Merge :: ('a,'b) merge_u program
+ Alloc :: 'a allocState_d program
+ Merge :: ('a,'b) merge_d program
+
(*
Network :: 'a systemState program
System :: 'a systemState program
@@ -205,17 +203,9 @@
rules
Alloc "Alloc : alloc_spec"
Merge "Merge : merge_spec"
+
(** Network "Network : network_spec"**)
-(**
-defs
- System_def
- "System == rename sysOfAlloc Alloc Join Network Join
- (rename sysOfMerge
- (plam x: lessThan Nclients. rename merge_map Merge))"
-**)
-
-
end
--- a/src/HOL/UNITY/Client.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Client.ML Fri Jul 21 18:01:36 2000 +0200
@@ -15,11 +15,9 @@
(*Safety property 1: ask, rel are increasing*)
Goal "Client: UNIV guarantees[funPair rel ask] \
\ Increasing ask Int Increasing rel";
-by (safe_tac (claset() addSIs [guaranteesI,increasing_imp_Increasing]));
by (auto_tac
- (claset(),
- simpset() addsimps [impOfSubs preserves_subset_increasing,
- Join_increasing]));
+ (claset() addSIs [increasing_imp_Increasing],
+ simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
by (auto_tac (claset(), simpset() addsimps [increasing_def]));
by (ALLGOALS constrains_tac);
by Auto_tac;
@@ -70,9 +68,7 @@
Goal "[| Client Join G : Increasing giv; G : preserves rel |] \
\ ==> Client Join G : Always {s. rel s <= giv s}";
-by (rtac AlwaysI 1);
-by (rtac Join_Stable_rel_le_giv 2);
-by Auto_tac;
+by (force_tac (claset() addIs [AlwaysI, Join_Stable_rel_le_giv], simpset()) 1);
qed "Join_Always_rel_le_giv";
Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
@@ -146,12 +142,12 @@
(*This shows that the Client won't alter other variables in any state
that it is combined with*)
-Goal "Client : preserves extra";
+Goal "Client : preserves dummy";
by (rewtac preserves_def);
by Auto_tac;
by (constrains_tac 1);
by Auto_tac;
-qed "client_preserves_extra";
+qed "client_preserves_dummy";
(** Obsolete lemmas from first version of the Client **)
--- a/src/HOL/UNITY/Client.thy Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Client.thy Fri Jul 21 18:01:36 2000 +0200
@@ -17,9 +17,9 @@
rel :: tokbag list (*output history: tokens released*)
tok :: tokbag (*current token request*)
-record 'a state_u =
+record 'a state_d =
state +
- extra :: 'a (*new variables*)
+ dummy :: 'a (*new variables*)
(*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
@@ -28,7 +28,7 @@
(** Release some tokens **)
- rel_act :: "('a state_u * 'a state_u) set"
+ rel_act :: "('a state_d * 'a state_d) set"
"rel_act == {(s,s').
EX nrel. nrel = size (rel s) &
s' = s (| rel := rel s @ [giv s!nrel] |) &
@@ -40,24 +40,24 @@
(** Including s'=s suppresses fairness, allowing the non-trivial part
of the action to be ignored **)
- tok_act :: "('a state_u * 'a state_u) set"
+ tok_act :: "('a state_d * 'a state_d) set"
"tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
- ask_act :: "('a state_u * 'a state_u) set"
+ ask_act :: "('a state_d * 'a state_d) set"
"ask_act == {(s,s'). s'=s |
(s' = s (|ask := ask s @ [tok s]|))}"
- Client :: 'a state_u program
+ Client :: 'a state_d program
"Client == mk_program ({s. tok s : atMost NbT &
giv s = [] & ask s = [] & rel s = []},
{rel_act, tok_act, ask_act})"
(*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|)"
+ non_dummy :: 'a state_d => state
+ "non_dummy 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"
+ client_map :: "'a state_d => state*'a"
+ "client_map == funPair non_dummy dummy"
end
--- a/src/HOL/UNITY/Comp.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Comp.ML Fri Jul 21 18:01:36 2000 +0200
@@ -100,9 +100,9 @@
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);
+Goalw [preserves_def]
+ "(F Join G : preserves v) = (F : preserves v & G : preserves v)";
+by Auto_tac;
qed "Join_preserves";
Goal "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)";
@@ -173,7 +173,7 @@
Goal "[| F : stable {s. P (v s) (w s)}; \
\ G : preserves v; G : preserves w |] \
\ ==> F Join G : stable {s. P (v s) (w s)}";
-by (asm_simp_tac (simpset() addsimps [Join_stable]) 1);
+by (Asm_simp_tac 1);
by (subgoal_tac "G: preserves (funPair v w)" 1);
by (Asm_simp_tac 2);
by (dres_inst_tac [("P1", "split ?Q")]
@@ -186,7 +186,7 @@
\ ==> F Join G : Stable {s. v s <= w s}";
by (auto_tac (claset(),
simpset() addsimps [stable_def, Stable_def, Increasing_def,
- Constrains_def, Join_constrains, all_conj_distrib]));
+ Constrains_def, all_conj_distrib]));
by (blast_tac (claset() addIs [constrains_weaken]) 1);
(*The G case remains*)
by (auto_tac (claset(),
--- a/src/HOL/UNITY/ELT.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/ELT.ML Fri Jul 21 18:01:36 2000 +0200
@@ -316,8 +316,7 @@
by (auto_tac (claset(),
simpset() addsimps [Diff_eq_empty_iff RS iffD2,
Int_Diff, ensures_def,
- givenBy_eq_Collect, Join_stable,
- Join_constrains, Join_transient]));
+ givenBy_eq_Collect, Join_transient]));
by (blast_tac (claset() addIs [transient_strengthen]) 3);
by (ALLGOALS (dres_inst_tac [("P1","P")] (impOfSubs preserves_subset_stable)));
by (rewtac stable_def);
@@ -335,8 +334,7 @@
by (case_tac "A <= B" 1);
by (etac subset_imp_ensures 1);
by (auto_tac (claset() addIs [constrains_weaken],
- simpset() addsimps [stable_def, ensures_def,
- Join_constrains, Join_transient]));
+ simpset() addsimps [stable_def, ensures_def, Join_transient]));
by (REPEAT (thin_tac "?F : ?A co ?B" 1));
by (etac transientE 1);
by (rewtac constrains_def);
@@ -551,11 +549,11 @@
by (rtac Join_project_ensures_strong 1);
by (auto_tac (claset() addDs [preserves_o_project_transient_empty]
addIs [project_stable_project_set],
- simpset() addsimps [Int_left_absorb, Join_stable]));
+ simpset() addsimps [Int_left_absorb]));
by (asm_simp_tac
(simpset() addsimps [stable_ensures_Int RS ensures_weaken_R,
Int_lower2, project_stable_project_set,
- Join_stable, extend_stable_project_set]) 1);
+ extend_stable_project_set]) 1);
val lemma = result();
Goal "[| extend h F Join G : stable C; \
@@ -623,7 +621,7 @@
\ project_set h C Int project_set h B";
by (rtac (psp_stable2 RS leadsTo_weaken_L) 1);
by (auto_tac (claset(),
- simpset() addsimps [project_stable_project_set, Join_stable,
+ simpset() addsimps [project_stable_project_set,
extend_stable_project_set]));
val lemma = result();
@@ -637,7 +635,7 @@
by (blast_tac (claset() addIs [leadsTo_UN]) 3);
by (blast_tac (claset() addIs [leadsTo_Trans, lemma]) 2);
by (asm_full_simp_tac
- (simpset() addsimps [givenBy_eq_extend_set, Join_stable]) 1);
+ (simpset() addsimps [givenBy_eq_extend_set]) 1);
by (rtac leadsTo_Basis 1);
by (blast_tac (claset() addIs [leadsTo_Basis,
ensures_extend_set_imp_project_ensures]) 1);
--- a/src/HOL/UNITY/Extend.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Extend.ML Fri Jul 21 18:01:36 2000 +0200
@@ -384,8 +384,7 @@
Goal "project h C (extend h F) = \
\ mk_program (Init F, Restrict (project_set h C) `` Acts F)";
by (rtac program_equalityI 1);
-by (asm_simp_tac (simpset() addsimps [image_eq_UN,
- project_act_extend_act_restrict]) 2);
+by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 2);
by (Simp_tac 1);
qed "project_extend_eq";
--- a/src/HOL/UNITY/Handshake.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Handshake.ML Fri Jul 21 18:01:36 2000 +0200
@@ -19,7 +19,7 @@
by (rtac AlwaysI 1);
by (Force_tac 1);
by (rtac (constrains_imp_Constrains RS StableI) 1);
-by (auto_tac (claset(), simpset() addsimps [Join_constrains]));
+by Auto_tac;
by (constrains_tac 2);
by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset()));
by (constrains_tac 1);
--- a/src/HOL/UNITY/Lift_prog.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Fri Jul 21 18:01:36 2000 +0200
@@ -46,6 +46,7 @@
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";
+Addsimps [drop_map_lift_map_eq];
Goalw [lift_map_def] "inj (lift_map i)";
by (rtac injI 1);
@@ -57,10 +58,11 @@
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";
+Addsimps [lift_map_drop_map_eq];
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);
+by (Full_simp_tac 1);
qed "drop_map_inject";
AddSDs [drop_map_inject];
@@ -74,19 +76,15 @@
qed "bij_lift_map";
AddIffs [bij_lift_map];
-AddIffs [bij_lift_map RS mem_rename_act_iff];
-
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);
+by Auto_tac;
qed "inv_lift_map_eq";
Addsimps [inv_lift_map_eq];
Goal "inv (drop_map i) = lift_map i";
by (rtac inv_equality 1);
-by (rtac drop_map_lift_map_eq 2);
-by (rtac lift_map_drop_map_eq 1);
+by Auto_tac;
qed "inv_drop_map_eq";
Addsimps [inv_drop_map_eq];
@@ -96,18 +94,13 @@
qed "bij_drop_map";
AddIffs [bij_drop_map];
-(*** sub ***)
-
+(*sub's main property!*)
Goal "sub i f = f i";
by (simp_tac (simpset() addsimps [sub_def]) 1);
qed "sub_apply";
Addsimps [sub_apply];
-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, bij_image_Collect_eq]) 1);
-qed "lift_set_eq_Collect";
+(*** lift_set ***)
Goalw [lift_set_def] "lift_set i {} = {}";
by Auto_tac;
@@ -117,7 +110,6 @@
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];
(*Do we really need both this one and its predecessor?*)
Goal "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)";
@@ -232,6 +224,11 @@
qed "lift_guarantees_eq_lift_inv";
+(*** We devote an ENORMOUS effort to proving lift_transient_eq_disj,
+ which is used only in TimerArray and perhaps isn't even essential
+ there!
+***)
+
(*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*)
@@ -264,12 +261,21 @@
Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set];
+Goalw [extend_act_def]
+ "((s,s') : extend_act (%(x,u::unit). lift_map i x) act) = \
+\ ((drop_map i s, drop_map i s') : act)";
+by Auto_tac;
+by (rtac bexI 1);
+by Auto_tac;
+qed "mem_lift_act_iff";
+AddIffs [mem_lift_act_iff];
+
Goal "[| F : preserves snd; i~=j |] \
\ ==> lift j F : stable (lift_set i (A <*> UNIV))";
by (auto_tac (claset(),
simpset() addsimps [lift_def, lift_set_def,
- stable_def, constrains_def,
- mem_rename_act_iff, mem_rename_set_iff]));
+ stable_def, constrains_def, rename_def,
+ extend_def, 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);
@@ -326,8 +332,8 @@
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]));
+ simpset() addsimps [lift_set_def, lift_def, transient_def,
+ rename_def, extend_def, Domain_extend_act]));
by (dtac subsetD 1);
by (Blast_tac 1);
by Auto_tac;
@@ -338,12 +344,11 @@
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
+ (bij_lift_map RS good_map_bij RS export (mem_extend_act_iff RS iffD2)) 1);
+by (Force_tac 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);
+by Auto_tac;
qed "lift_transient_eq_disj";
(*USELESS??*)
--- a/src/HOL/UNITY/PPROD.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/PPROD.ML Fri Jul 21 18:01:36 2000 +0200
@@ -15,12 +15,7 @@
by (simp_tac (simpset() addsimps [PLam_def, lift_def, lift_set_def]) 1);
qed "Init_PLam";
-(*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];
+Addsimps [Init_PLam];
Goal "PLam {} F = SKIP";
by (simp_tac (simpset() addsimps [PLam_def]) 1);
@@ -46,14 +41,13 @@
qed "component_PLam";
-(** Safety & Progress **)
+(** Safety & Progress: but are they used anywhere? **)
Goal "[| i : I; ALL j. F j : preserves snd |] ==> \
\ (PLam I F : (lift_set i (A <*> UNIV)) co \
\ (lift_set i (B <*> UNIV))) = \
\ (F i : (A <*> UNIV) co (B <*> UNIV))";
-by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains,
- Join_constrains]) 1);
+by (asm_simp_tac (simpset() addsimps [PLam_def, JN_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);
@@ -70,18 +64,17 @@
by (asm_simp_tac (simpset() addsimps [JN_transient, PLam_def]) 1);
qed "PLam_transient";
-Addsimps [PLam_constrains, PLam_stable, PLam_transient];
-
(*This holds because the F j cannot change (lift_set i)*)
Goal "[| i : I; F i : (A <*> UNIV) ensures (B <*> UNIV); \
\ ALL j. F j : preserves snd |] ==> \
\ PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)";
by (auto_tac (claset(),
- 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]));
+ simpset() addsimps [ensures_def, PLam_constrains, PLam_transient,
+ 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; \
@@ -102,7 +95,7 @@
\ ALL j. F j : preserves snd |] \
\ ==> PLam I F : invariant (lift_set i (A <*> UNIV))";
by (auto_tac (claset(),
- simpset() addsimps [invariant_def]));
+ simpset() addsimps [PLam_stable, invariant_def]));
qed "invariant_imp_PLam_invariant";
--- a/src/HOL/UNITY/Project.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Project.ML Fri Jul 21 18:01:36 2000 +0200
@@ -32,7 +32,7 @@
Goal "(F Join project h C G : A co B) = \
\ (extend h F Join G : (C Int extend_set h A) co (extend_set h B) & \
\ F : A co B)";
-by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
+by (simp_tac (simpset() addsimps [project_constrains]) 1);
by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken]
addDs [constrains_imp_subset]) 1);
qed "Join_project_constrains";
@@ -44,7 +44,7 @@
\ ==> (F Join project h C G : stable A) = \
\ (extend h F Join G : stable (C Int extend_set h A) & \
\ F : stable A)";
-by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
+by (simp_tac (HOL_ss addsimps [Join_project_constrains]) 1);
by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
qed "Join_project_stable";
@@ -52,8 +52,7 @@
Goal "extend h F Join G : extend_set h A co extend_set h B \
\ ==> F Join project h C G : A co B";
by (asm_full_simp_tac
- (simpset() addsimps [project_constrains, Join_constrains,
- extend_constrains]) 1);
+ (simpset() addsimps [project_constrains, extend_constrains]) 1);
by (blast_tac (claset() addIs [constrains_weaken]
addDs [constrains_imp_subset]) 1);
qed "project_constrains_I";
@@ -61,18 +60,18 @@
Goalw [increasing_def, stable_def]
"extend h F Join G : increasing (func o f) \
\ ==> F Join project h C G : increasing func";
-by (asm_full_simp_tac (simpset() addsimps [project_constrains_I,
- extend_set_eq_Collect]) 1);
+by (asm_full_simp_tac (simpset_of SubstAx.thy
+ addsimps [project_constrains_I, extend_set_eq_Collect]) 1);
qed "project_increasing_I";
Goal "(F Join project h UNIV G : increasing func) = \
\ (extend h F Join G : increasing (func o f))";
by (rtac iffI 1);
by (etac project_increasing_I 2);
-by (asm_full_simp_tac
- (simpset() addsimps [increasing_def, Join_project_stable]) 1);
+by (asm_full_simp_tac (simpset_of SubstAx.thy
+ addsimps [increasing_def, Join_project_stable]) 1);
by (auto_tac (claset(),
- simpset() addsimps [Join_stable, extend_set_eq_Collect,
+ simpset() addsimps [extend_set_eq_Collect,
extend_stable RS iffD1]));
qed "Join_project_increasing";
@@ -80,8 +79,7 @@
Goal "F Join project h UNIV G : A co B \
\ ==> extend h F Join G : extend_set h A co extend_set h B";
by (asm_full_simp_tac
- (simpset() addsimps [project_constrains, Join_constrains,
- extend_constrains]) 1);
+ (simpset() addsimps [project_constrains, extend_constrains]) 1);
qed "project_constrains_D";
@@ -192,7 +190,7 @@
Goalw [extending_def]
"extending v (%G. UNIV) h F (increasing (func o f)) (increasing func)";
-by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
+by (simp_tac (HOL_ss addsimps [Join_project_increasing]) 1);
qed "extending_increasing";
@@ -216,7 +214,7 @@
Goalw [Constrains_def]
"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 (full_simp_tac (simpset_of SubstAx.thy addsimps [Join_project_constrains]) 1);
by (Clarify_tac 1);
by (etac constrains_weaken 1);
by (auto_tac (claset() addIs [reachable_imp_reachable_project], simpset()));
@@ -277,14 +275,14 @@
Goalw [Constrains_def]
"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,
+by (full_simp_tac (simpset_of SubstAx.thy addsimps [Join_project_constrains,
extend_set_Int_distrib]) 1);
by (rtac conjI 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);
+ simpset()) 2);
by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
qed "project_Constrains_I";
@@ -421,7 +419,7 @@
\ ==> F Join project h C G \
\ : (project_set h C Int project_set h A) ensures (project_set h B)";
by (asm_full_simp_tac
- (simpset() addsimps [ensures_def, Join_constrains, project_constrains,
+ (simpset() addsimps [ensures_def, project_constrains,
Join_transient, extend_transient]) 1);
by (Clarify_tac 1);
by (REPEAT_FIRST (rtac conjI));
@@ -463,8 +461,7 @@
addIs [transient_strengthen, project_set_I,
project_unless RS unlessD, unlessI,
project_extend_constrains_I],
- simpset() addsimps [ensures_def, Join_constrains,
- Join_stable, Join_transient]));
+ simpset() addsimps [ensures_def, Join_transient]));
qed_spec_mp "Join_project_ensures";
(** Lemma useful for both STRONG and WEAK progress, but the transient
@@ -498,7 +495,7 @@
\ F Join project h C G : A LeadsTo B |] \
\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
by (asm_full_simp_tac
- (simpset() addsimps [LeadsTo_def, project_leadsTo_D_lemma,
+ (simpset_of SubstAx.thy addsimps [LeadsTo_def, project_leadsTo_D_lemma,
project_set_reachable_extend_eq]) 1);
qed "Join_project_LeadsTo";
@@ -506,7 +503,6 @@
(*** Towards project_Ensures_D ***)
-
Goalw [project_set_def, extend_set_def, project_act_def]
"act ^^ (C Int extend_set h A) <= B \
\ ==> project_act h (Restrict C act) ^^ (project_set h C Int A) \
@@ -560,8 +556,7 @@
(*unless*)
by (auto_tac (claset() addSIs [rewrite_rule [unless_def] project_unless2]
addIs [project_extend_constrains_I],
- simpset() addsimps [ensures_def, Join_constrains,
- Join_stable]));
+ simpset() addsimps [ensures_def]));
(*transient*)
by (auto_tac (claset(), simpset() addsimps [Join_transient]));
by (blast_tac (claset() addIs [stable_project_transient]) 2);
--- a/src/HOL/UNITY/Rename.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Rename.ML Fri Jul 21 18:01:36 2000 +0200
@@ -40,34 +40,8 @@
by (Simp_tac 1);
qed "Init_rename";
-Goalw [rename_def, rename_act_def]
- "bij h ==> Acts (rename h F) = (rename_act h `` Acts F)";
-by (asm_simp_tac (simpset() addsimps [export Acts_extend]) 1);
-qed "Acts_rename";
-
-Addsimps [Init_rename, Acts_rename];
-
-(*Useful if we don't assume bij h*)
-Goalw [rename_def, rename_act_def, extend_def]
- "Acts (rename h F) = insert Id (rename_act h `` Acts F)";
-by (asm_simp_tac (simpset() addsimps [export Acts_extend]) 1);
-qed "raw_Acts_rename";
+Addsimps [Init_rename];
-Goalw [rename_act_def, extend_act_def]
- "(s,s') : act ==> (h s, h s') : rename_act h act";
-by Auto_tac;
-qed "rename_actI";
-
-Goalw [rename_act_def]
- "bij h ==> ((s,s') : rename_act h act) = ((inv h s, inv h s') : act)";
-by (rtac trans 1);
-by (etac (bij_export mem_extend_act_iff) 2);
-by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 1);
-qed "mem_rename_act_iff";
-
-Goalw [rename_act_def] "Domain (rename_act h act) = h``(Domain act)";
-by (asm_simp_tac (simpset() addsimps [export Domain_extend_act]) 1);
-qed "Domain_rename_act";
(*** inverse properties ***)
@@ -139,14 +113,16 @@
by (dres_inst_tac [("x", "mk_program ({x}, {})")] spec 1);
by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1);
by (auto_tac (claset(),
- simpset() addsimps [program_equality_iff, raw_Acts_rename]));
+ simpset() addsimps [program_equality_iff,
+ rename_def, extend_def]));
qed "inj_rename_imp_inj";
Goalw [surj_def] "surj (rename h) ==> surj h";
by Auto_tac;
by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1);
by (auto_tac (claset(),
- simpset() addsimps [program_equality_iff, raw_Acts_rename]));
+ simpset() addsimps [program_equality_iff,
+ rename_def, extend_def]));
qed "surj_rename_imp_surj";
Goalw [bij_def] "bij (rename h) ==> bij h";
@@ -337,41 +313,3 @@
Goal "bij h ==> rename h `` (A LeadsTo B) = (h `` A) LeadsTo (h``B)";
by (rename_image_tac [rename_LeadsTo]);
qed "rename_image_LeadsTo";
-
-
-
-
-(** junk
-
-
-Goalw [extend_act_def, project_act_def, surj_def]
- "surj h ==> extend_act (%(x,u). h x) (project_act (%(x,u). h x) act) = act";
-by Auto_tac;
-by (forw_inst_tac [("x", "a")] spec 1);
-by (dres_inst_tac [("x", "b")] spec 1);
-by Auto_tac;
-qed "project_act_inverse";
-
-Goal "bij h ==> rename h (rename (inv h) F) = F";
-by (rtac program_equalityI 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac
- (simpset() addsimps [rename_def, inverse_def, export Acts_extend,
- image_eq_UN, export extend_act_Id,
- bij_is_surj RS project_act_inverse]) 1);
-qed "rename_rename_inv";
-Addsimps [rename_rename_inv];
-
-
-
-Goalw [bij_def]
- "bij h \
-\ ==> extend_set (%(x,u::'c). inv h x) = inv (extend_set (%(x,u::'c). h x))";
-by (rtac ext 1);
-by (auto_tac (claset() addSIs [image_eqI],
- simpset() addsimps [extend_set_def, project_set_def,
- surj_f_inv_f]));
-qed "extend_set_inv";
-
-
-***)
--- a/src/HOL/UNITY/Rename.thy Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Rename.thy Fri Jul 21 18:01:36 2000 +0200
@@ -9,13 +9,6 @@
Rename = Extend +
constdefs
- rename_act :: "['a => 'b, ('a*'a) set] => ('b*'b) set"
- "rename_act h == extend_act (%(x,u::unit). h x)"
-
-(**OR
- "rename_act h == %act. UN (s,s'): act. {(h s, h s')}"
- "rename_act h == %act. (prod_fun h h) `` act"
-**)
rename :: "['a => 'b, 'a program] => 'b program"
"rename h == extend (%(x,u::unit). h x)"
--- a/src/HOL/UNITY/TimerArray.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/TimerArray.ML Fri Jul 21 18:01:36 2000 +0200
@@ -26,6 +26,7 @@
qed "Timer_preserves_snd";
AddIffs [Timer_preserves_snd];
+Addsimps [PLam_stable];
Goal "finite I \
\ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";
--- a/src/HOL/UNITY/Union.ML Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Union.ML Fri Jul 21 18:01:36 2000 +0200
@@ -188,6 +188,8 @@
by (simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1);
qed "Join_unless";
+Addsimps [Join_constrains, Join_unless];
+
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
reachable (F Join G) could be much bigger than reachable F, reachable G
*)
@@ -195,7 +197,7 @@
Goal "[| F : A co A'; G : B co B' |] \
\ ==> F Join G : (A Int B) co (A' Un B')";
-by (simp_tac (simpset() addsimps [Join_constrains]) 1);
+by (Simp_tac 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "Join_constrains_weaken";
@@ -219,7 +221,7 @@
Goal "(F Join G : stable A) = \
\ (F : stable A & G : stable A)";
-by (simp_tac (simpset() addsimps [stable_def, Join_constrains]) 1);
+by (simp_tac (simpset() addsimps [stable_def]) 1);
qed "Join_stable";
Goal "(F Join G : increasing f) = \
@@ -228,9 +230,11 @@
by (Blast_tac 1);
qed "Join_increasing";
+Addsimps [Join_stable, Join_increasing];
+
Goal "[| F : invariant A; G : invariant A |] \
\ ==> F Join G : invariant A";
-by (full_simp_tac (simpset() addsimps [invariant_def, Join_stable]) 1);
+by (full_simp_tac (simpset() addsimps [invariant_def]) 1);
by (Blast_tac 1);
qed "invariant_JoinI";
@@ -254,6 +258,8 @@
Join_def]));
qed "Join_transient";
+Addsimps [Join_transient];
+
Goal "F : transient A ==> F Join G : transient A";
by (asm_simp_tac (simpset() addsimps [Join_transient]) 1);
qed "Join_transient_I1";
@@ -274,8 +280,7 @@
"F Join G : A ensures B = \
\ (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) & \
\ (F : transient (A-B) | G : transient (A-B)))";
-by (auto_tac (claset(),
- simpset() addsimps [Join_constrains, Join_transient]));
+by (auto_tac (claset(), simpset() addsimps [Join_transient]));
qed "Join_ensures";
Goalw [stable_def, constrains_def, Join_def]
@@ -289,7 +294,7 @@
G : stable A *)
Goal "[| F : stable A; G : invariant A |] ==> F Join G : Always A";
by (full_simp_tac (simpset() addsimps [Always_def, invariant_def,
- Stable_eq_stable, Join_stable]) 1);
+ Stable_eq_stable]) 1);
by (force_tac(claset() addIs [stable_Int], simpset()) 1);
qed "stable_Join_Always1";