# HG changeset patch
# User paulson
# Date 1043428439 -3600
# Node ID ab8f39f48a6fcb3446c2fb615c9cdc8597efee83
# Parent  e2fcd88be55d288e5fd551f50204265c426750cc
More conversion of UNITY to Isar new-style theories

diff -r e2fcd88be55d -r ab8f39f48a6f src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Fri Jan 24 14:06:49 2003 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Fri Jan 24 18:13:59 2003 +0100
@@ -6,7 +6,7 @@
 Common declarations for Chandy and Charpentier's Allocator
 *)
 
-AllocBase = Rename + Follows + 
+AllocBase = UNITY_Main + 
 
 consts
   NbT      :: nat       (*Number of tokens in system*)
diff -r e2fcd88be55d -r ab8f39f48a6f src/HOL/UNITY/Comp/Handshake.ML
--- a/src/HOL/UNITY/Comp/Handshake.ML	Fri Jan 24 14:06:49 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-(*  Title:      HOL/UNITY/Handshake
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Handshake Protocol
-
-From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
-*)
-
-Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
-program_defs_ref := [F_def, G_def];
-
-Addsimps (map simp_of_act [cmdF_def, cmdG_def]);
-Addsimps [simp_of_set invFG_def];
-
-
-Goal "(F Join G) : Always invFG";
-by (rtac AlwaysI 1);
-by (Force_tac 1);
-by (rtac (constrains_imp_Constrains RS StableI) 1);
-by Auto_tac;
-by (constrains_tac 2);
-by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset()));
-by (constrains_tac 1);
-qed "invFG";
-
-Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \
-\                  ({s. NF s = k} Int {s. BB s})";
-by (rtac (stable_Join_ensures1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
-by (ensures_tac "cmdG" 2);
-by (constrains_tac 1);
-qed "lemma2_1";
-
-Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}";
-by (rtac (stable_Join_ensures2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
-by (constrains_tac 2);
-by (ensures_tac "cmdF" 1);
-qed "lemma2_2";
-
-Goal "(F Join G) : UNIV LeadsTo {s. m < NF s}";
-by (rtac LeadsTo_weaken_R 1);
-by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] 
-    GreaterThan_bounded_induct 1);
-(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
-by (auto_tac (claset() addSIs [lemma2_1, lemma2_2] 
-	               addIs[LeadsTo_Trans, LeadsTo_Diff], 
-	      simpset() addsimps [vimage_def]));
-qed "progress";
diff -r e2fcd88be55d -r ab8f39f48a6f src/HOL/UNITY/Comp/Handshake.thy
--- a/src/HOL/UNITY/Comp/Handshake.thy	Fri Jan 24 14:06:49 2003 +0100
+++ b/src/HOL/UNITY/Comp/Handshake.thy	Fri Jan 24 18:13:59 2003 +0100
@@ -8,7 +8,7 @@
 From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
 *)
 
-Handshake = Union +
+theory Handshake = UNITY_Main:
 
 record state =
   BB :: bool
@@ -34,4 +34,46 @@
   invFG :: "state set"
     "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
 
+
+declare F_def [THEN def_prg_Init, simp] 
+        G_def [THEN def_prg_Init, simp]
+
+        cmdF_def [THEN def_act_simp, simp]
+        cmdG_def [THEN def_act_simp, simp]
+
+        invFG_def [THEN def_set_simp, simp]
+
+
+lemma invFG: "(F Join G) : Always invFG"
+apply (rule AlwaysI)
+apply force
+apply (rule constrains_imp_Constrains [THEN StableI])
+apply auto
+ apply (unfold F_def, constrains) 
+apply (unfold G_def, constrains) 
+done
+
+lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo  
+                              ({s. NF s = k} Int {s. BB s})"
+apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
+ apply (unfold F_def, constrains) 
+apply (unfold G_def, ensures_tac "cmdG") 
+done
+
+lemma lemma2_2: "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo 
+                              {s. k < NF s}"
+apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
+ apply (unfold F_def, ensures_tac "cmdF") 
+apply (unfold G_def, constrains) 
+done
+
+lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}"
+apply (rule LeadsTo_weaken_R)
+apply (rule_tac f = "NF" and l = "Suc m" and B = "{}" 
+       in GreaterThan_bounded_induct)
+(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
+apply (auto intro!: lemma2_1 lemma2_2
+            intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def)
+done
+
 end
diff -r e2fcd88be55d -r ab8f39f48a6f src/HOL/UNITY/Comp/TimerArray.ML
--- a/src/HOL/UNITY/Comp/TimerArray.ML	Fri Jan 24 14:06:49 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(*  Title:      HOL/UNITY/TimerArray.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-A trivial example of reasoning about an array of processes
-*)
-
-Addsimps [Timer_def RS def_prg_Init];
-program_defs_ref := [Timer_def];
-
-Addsimps [count_def, decr_def];
-
-(*Demonstrates induction, but not used in the following proof*)
-Goal "Timer : UNIV leadsTo {s. count s = 0}";
-by (res_inst_tac [("f", "count")] lessThan_induct 1);
-by (Simp_tac 1);
-by (case_tac "m" 1);
-by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1);
-by (ensures_tac "decr" 1);
-qed "Timer_leadsTo_zero";
-
-Goal "Timer : preserves snd";
-by (rtac preservesI 1);
-by (constrains_tac 1);
-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}";
-by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")]
-    (finite_stable_completion RS leadsTo_weaken) 1);
-by Auto_tac;
-(*Safety property, already reduced to the single Timer case*)
-by (constrains_tac 2);
-(*Progress property for the array of Timers*)
-by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
-by (case_tac "m" 1);
-(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
-by (auto_tac (claset() addIs [subset_imp_leadsTo], 
-	      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]));
-by (constrains_tac 1);
-by (res_inst_tac [("act", "decr")] transientI 1);
-by (auto_tac (claset(), simpset() addsimps [Timer_def]));
-qed "TimerArray_leadsTo_zero";
diff -r e2fcd88be55d -r ab8f39f48a6f src/HOL/UNITY/Comp/TimerArray.thy
--- a/src/HOL/UNITY/Comp/TimerArray.thy	Fri Jan 24 14:06:49 2003 +0100
+++ b/src/HOL/UNITY/Comp/TimerArray.thy	Fri Jan 24 18:13:59 2003 +0100
@@ -6,7 +6,7 @@
 A trivial example of reasoning about an array of processes
 *)
 
-TimerArray = PPROD +
+theory TimerArray = UNITY_Main:
 
 types 'a state = "nat * 'a"   (*second component allows new variables*)
 
@@ -17,7 +17,52 @@
   decr  :: "('a state * 'a state) set"
     "decr == UN n uu. {((Suc n, uu), (n,uu))}"
   
-  Timer :: 'a state program
+  Timer :: "'a state program"
     "Timer == mk_program (UNIV, {decr}, UNIV)"
 
+
+declare Timer_def [THEN def_prg_Init, simp]
+
+declare count_def [simp] decr_def [simp]
+
+(*Demonstrates induction, but not used in the following proof*)
+lemma Timer_leadsTo_zero: "Timer : UNIV leadsTo {s. count s = 0}"
+apply (rule_tac f = count in lessThan_induct, simp)
+apply (case_tac "m")
+ apply (force intro!: subset_imp_leadsTo)
+apply (unfold Timer_def, ensures_tac "decr")
+done
+
+lemma Timer_preserves_snd [iff]: "Timer : preserves snd"
+apply (rule preservesI)
+apply (unfold Timer_def, constrains)
+done
+
+
+declare PLam_stable [simp]
+
+lemma TimerArray_leadsTo_zero:
+     "finite I  
+      ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"
+apply (erule_tac A'1 = "%i. lift_set i ({0} <*> UNIV)" 
+       in finite_stable_completion [THEN leadsTo_weaken])
+apply auto
+(*Safety property, already reduced to the single Timer case*)
+ prefer 2
+ apply (simp add: Timer_def, constrains) 
+(*Progress property for the array of Timers*)
+apply (rule_tac f = "sub i o fst" in lessThan_induct)
+apply (case_tac "m")
+(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
+apply (auto intro: subset_imp_leadsTo 
+        simp add: insert_absorb 
+                  lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric] 
+               Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
+apply (rename_tac "n")
+apply (rule PLam_leadsTo_Basis)
+apply (auto simp add: lessThan_Suc [symmetric])
+apply (unfold Timer_def, constrains) 
+apply (rule_tac act = decr in transientI, auto)
+done
+
 end
diff -r e2fcd88be55d -r ab8f39f48a6f src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Fri Jan 24 14:06:49 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,487 +0,0 @@
-(*  Title:      HOL/UNITY/Lift_prog.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Arrays of processes. 
-*)
-
-Addsimps [insert_map_def, delete_map_def];
-
-Goal "delete_map i (insert_map i x f) = f";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "insert_map_inverse";
-
-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]));
-qed "insert_map_delete_map_eq";
-
-(*** Injectiveness proof ***)
-
-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";
-
-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 "lift_map_eq_iff";
-AddIffs [lift_map_eq_iff];
-
-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);
-by Auto_tac;
-qed "inj_lift_map";
-
-(*** Surjectiveness proof ***)
-
-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 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";
-
-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];
-
-Goal "inv (lift_map i) = drop_map i";
-by (rtac inv_equality 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 Auto_tac;  
-qed "inv_drop_map_eq";
-Addsimps [inv_drop_map_eq];
-
-Goal "bij (drop_map i)";
-by (simp_tac (simpset() delsimps [inv_lift_map_eq]
-                        addsimps [inv_lift_map_eq RS sym, bij_imp_bij_inv]) 1);
-qed "bij_drop_map";
-AddIffs [bij_drop_map];
-
-(*sub's main property!*)
-Goal "sub i f = f i";
-by (simp_tac (simpset() addsimps [sub_def]) 1);
-qed "sub_apply";
-Addsimps [sub_apply];
-
-(*** lift_set ***)
-
-Goalw [lift_set_def] "lift_set i {} = {}";
-by Auto_tac;
-qed "lift_set_empty";
-Addsimps [lift_set_empty];
-
-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";
-
-(*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)";
-by (asm_simp_tac (simpset() addsimps [lift_set_def, 
-				      mem_rename_set_iff, drop_map_def]) 1);
-qed "lift_set_iff2";
-AddIffs [lift_set_iff2];
-
-Goalw [lift_set_def] "A<=B ==> lift_set i A <= lift_set i B";
-by (etac image_mono 1);
-qed "lift_set_mono";
-
-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";
-
-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";
-
-
-(*** the lattice operations ***)
-
-Goal "bij (lift i)";
-by (simp_tac (simpset() addsimps [lift_def]) 1);
-qed "bij_lift";
-AddIffs [bij_lift];
-
-Goalw [lift_def] "lift i SKIP = SKIP";
-by (Asm_simp_tac 1);
-qed "lift_SKIP";
-Addsimps [lift_SKIP];
-
-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 [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 ***)
-
-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";
-
-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";
-
-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";
-
-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";
-
-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";
-
-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 ***)
-
-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";
-
-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 (lift i ` Y)) = \
-\     (F : X guarantees 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 Y) = \
-\     (F : (rename (drop_map i) ` X) guarantees (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";
-
-
-(*** 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*)
-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 "[| 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 <*> UNIV) ignores the second (dummy) state component*)
-
-Goal "(f o fst) -` A = (f-`A) <*> UNIV";
-by Auto_tac;
-qed "vimage_o_fst_eq";
-
-Goal "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)";
-by Auto_tac;
-qed "vimage_sub_eq_lift_set";
-
-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, 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);
-by Auto_tac;
-qed "preserves_snd_lift_stable";
-
-(*If i~=j then lift j F  does nothing to lift_set i, and the 
-  premise ensures A<=B.*)
-Goal "[| F i : (A <*> UNIV) co (B <*> UNIV);  \
-\        F j : preserves snd |]  \
-\  ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> 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";
-
-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 - Suc 0 := 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 <*> UNIV))) = \
-\         (i=j & F : transient (A <*> UNIV) | A={})";
-by (case_tac "i=j" 1);
-by (auto_tac (claset(), simpset() addsimps [lift_transient]));
-by (auto_tac (claset(),
-	      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;
-by (rename_tac "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 
-    (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 Auto_tac;  
-qed "lift_transient_eq_disj";
-
-(*USELESS??*)
-Goal "lift_map i ` (A <*> UNIV) = \
-\     (UN s:A. UN f. {insert_map i s f}) <*> UNIV";
-by (auto_tac (claset() addSIs [bexI, image_eqI],
-              simpset() addsimps [lift_map_def]));
-by (rtac (split_conv 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";
-
-(*A useful rewrite.  If o, sub have been rewritten out already then can also
-  use it as   rewrite_rule [sub_def, o_def] lift_preserves_sub*)
-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";
-
-
-(*** Lemmas to handle function composition (o) more consistently ***)
-
-(*Lets us prove one version of a theorem and store others*)
-Goal "f o g = h ==> f' o f o g = f' o h";
-by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1);
-qed "o_equiv_assoc";
-
-Goal "f o g = h ==> ALL x. f(g x) = h x";
-by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1);
-qed "o_equiv_apply";
-
-fun make_o_equivs th = 
-    [th, 
-     th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]), 
-     th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];
-
-Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);
-
-Goal "sub i o fst o lift_map i = fst";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def, sub_def]));
-qed "fst_o_lift_map";
-
-Goal "snd o lift_map i = snd o snd";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def]));
-qed "snd_o_lift_map";
-
-Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);
-
-
-(*** More lemmas about extend and project 
-     They could be moved to {Extend,Project}.ML, but DON'T need the locale ***)
-
-Goal "extend_act h' (extend_act h act) = \
-\     extend_act (%(x,(y,y')). h'(h(x,y),y')) act";
-by (auto_tac (claset() addSEs [rev_bexI], 
-              simpset() addsimps [extend_act_def]));
-by (ALLGOALS Blast_tac);
-qed "extend_act_extend_act";
-
-Goal "project_act h (project_act h' act) = \
-\     project_act (%(x,(y,y')). h'(h(x,y),y')) act";
-by (auto_tac (claset() addSEs [rev_bexI], 
-              simpset() addsimps [project_act_def]));    
-qed "project_act_project_act";
-
-Goal "project_act h (extend_act h' act) = \
-\       {(x,x'). EX s s' y y' z. (s,s') : act & \
-\                h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}";
-by (simp_tac (simpset() addsimps [extend_act_def, project_act_def]) 1); 
-by (Blast_tac 1); 
-qed "project_act_extend_act";
-
-
-(*** OK and "lift" ***)
-
-Goal "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts";
-by (res_inst_tac [("a","mk_program(UNIV,{act},UNIV)")] UN_I 1);
-by (auto_tac (claset(),
-              simpset() addsimps [preserves_def,stable_def,constrains_def]));  
-qed "act_in_UNION_preserves_fst";
-
-Goal "[| ALL i:I. F i : preserves snd;  \
-\        ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |] \
-\     ==> OK I (%i. lift i (F i))";
-by (auto_tac (claset(),
-    simpset() addsimps [OK_def, lift_def, rename_def, export Acts_extend]));
-by (simp_tac (
-    simpset() addsimps [export AllowedActs_extend,project_act_extend_act]) 1);
-by (rename_tac "act" 1);
-by (subgoal_tac
-    "{(x, x'). EX s f u s' f' u'.   \
-\                ((s, f, u), s', f', u') : act &   \
-\                lift_map j x  = lift_map i (s, f, u) &   \
-\                lift_map j x' = lift_map i (s', f', u')}   \
-\    <= {(x,x'). fst x = fst x'}" 1);
-by (blast_tac (claset() addIs [act_in_UNION_preserves_fst]) 1);
-by (Clarify_tac 1); 
-by (REPEAT (dres_inst_tac [("x","j")] fun_cong 1) );
-by (dres_inst_tac [("x","i")] bspec 1); 
-by (assume_tac 1); 
-by (ftac preserves_imp_eq 1);
-by Auto_tac;  
-qed "UNION_OK_lift_I";
-
-Goal "[| ALL i:I. F i : preserves snd;  \
-\        ALL i:I. preserves fst <= Allowed (F i) |] \
-\     ==> OK I (%i. lift i (F i))";
-by (asm_full_simp_tac 
-    (simpset() addsimps [safety_prop_AllowedActs_iff_Allowed, 
-                         UNION_OK_lift_I]) 1); 
-qed "OK_lift_I";
-
-Goal "Allowed (lift i F) = lift i ` (Allowed F)";
-by (simp_tac (simpset() addsimps [lift_def, Allowed_rename]) 1); 
-qed "Allowed_lift"; 
-Addsimps [Allowed_lift];
-
-Goal "lift i ` preserves v = preserves (v o drop_map i)";
-by (simp_tac (simpset() addsimps [rename_image_preserves, lift_def, 
-                                  inv_lift_map_eq]) 1); 
-qed "lift_image_preserves";
diff -r e2fcd88be55d -r ab8f39f48a6f src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Fri Jan 24 14:06:49 2003 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Fri Jan 24 18:13:59 2003 +0100
@@ -3,10 +3,10 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
 
-lift_prog, etc: replication of components
+lift_prog, etc: replication of components and arrays of processes. 
 *)
 
-Lift_prog = Rename +
+theory Lift_prog = Rename:
 
 constdefs
 
@@ -31,9 +31,458 @@
     "lift i == rename (lift_map i)"
 
   (*simplifies the expression of specifications*)
-  constdefs
-    sub :: ['a, 'a=>'b] => 'b
-      "sub == %i f. f i"
+  sub :: "['a, 'a=>'b] => 'b"
+    "sub == %i f. f i"
+
+
+declare insert_map_def [simp] delete_map_def [simp]
+
+lemma insert_map_inverse: "delete_map i (insert_map i x f) = f"
+apply (rule ext)
+apply (simp (no_asm))
+done
+
+lemma insert_map_delete_map_eq: "(insert_map i x (delete_map i g)) = g(i:=x)"
+apply (rule ext)
+apply (auto split add: nat_diff_split)
+done
+
+(*** Injectiveness proof ***)
+
+lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y"
+apply (drule_tac x = i in fun_cong)
+apply (simp (no_asm_use))
+done
+
+lemma insert_map_inject2: "(insert_map i x f) = (insert_map i y g) ==> f=g"
+apply (drule_tac f = "delete_map i" in arg_cong)
+apply (simp (no_asm_use) add: insert_map_inverse)
+done
+
+lemma insert_map_inject':
+     "(insert_map i x f) = (insert_map i y g) ==> x=y & f=g"
+by (blast dest: insert_map_inject1 insert_map_inject2)
+
+lemmas insert_map_inject = insert_map_inject' [THEN conjE, elim!]
+
+(*The general case: we don't assume i=i'*)
+lemma lift_map_eq_iff [iff]: 
+     "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu')))  
+      = (uu = uu' & insert_map i s f = insert_map i' s' f')"
+apply (unfold lift_map_def, auto)
+done
+
+(*The !!s allows the automatic splitting of the bound variable*)
+lemma drop_map_lift_map_eq [simp]: "!!s. drop_map i (lift_map i s) = s"
+apply (unfold lift_map_def drop_map_def)
+apply (force intro: insert_map_inverse)
+done
+
+lemma inj_lift_map: "inj (lift_map i)"
+apply (unfold lift_map_def)
+apply (rule inj_onI, auto)
+done
+
+(*** Surjectiveness proof ***)
+
+lemma lift_map_drop_map_eq [simp]: "!!s. lift_map i (drop_map i s) = s"
+apply (unfold lift_map_def drop_map_def)
+apply (force simp add: insert_map_delete_map_eq)
+done
+
+lemma drop_map_inject [dest!]: "(drop_map i s) = (drop_map i s') ==> s=s'"
+apply (drule_tac f = "lift_map i" in arg_cong)
+apply (simp (no_asm_use))
+done
+
+lemma surj_lift_map: "surj (lift_map i)"
+apply (rule surjI)
+apply (rule lift_map_drop_map_eq)
+done
+
+lemma bij_lift_map [iff]: "bij (lift_map i)"
+apply (simp (no_asm) add: bij_def inj_lift_map surj_lift_map)
+done
+
+lemma inv_lift_map_eq [simp]: "inv (lift_map i) = drop_map i"
+by (rule inv_equality, auto)
+
+lemma inv_drop_map_eq [simp]: "inv (drop_map i) = lift_map i"
+by (rule inv_equality, auto)
+
+lemma bij_drop_map [iff]: "bij (drop_map i)"
+by (simp del: inv_lift_map_eq add: inv_lift_map_eq [symmetric] bij_imp_bij_inv)
+
+(*sub's main property!*)
+lemma sub_apply [simp]: "sub i f = f i"
+apply (simp (no_asm) add: sub_def)
+done
+
+(*** lift_set ***)
+
+lemma lift_set_empty [simp]: "lift_set i {} = {}"
+by (unfold lift_set_def, auto)
+
+lemma lift_set_iff: "(lift_map i x : lift_set i A) = (x : A)"
+apply (unfold lift_set_def)
+apply (rule inj_lift_map [THEN inj_image_mem_iff])
+done
+
+(*Do we really need both this one and its predecessor?*)
+lemma lift_set_iff2 [iff]:
+     "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)"
+by (simp (no_asm_simp) add: lift_set_def mem_rename_set_iff drop_map_def)
+
+
+lemma lift_set_mono: "A<=B ==> lift_set i A <= lift_set i B"
+apply (unfold lift_set_def)
+apply (erule image_mono)
+done
+
+lemma lift_set_Un_distrib: "lift_set i (A Un B) = lift_set i A Un lift_set i B"
+apply (unfold lift_set_def)
+apply (simp (no_asm_simp) add: image_Un)
+done
+
+lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B"
+apply (unfold lift_set_def)
+apply (rule inj_lift_map [THEN image_set_diff])
+done
+
+
+(*** the lattice operations ***)
+
+lemma bij_lift [iff]: "bij (lift i)"
+apply (simp (no_asm) add: lift_def)
+done
+
+lemma lift_SKIP [simp]: "lift i SKIP = SKIP"
+apply (unfold lift_def)
+apply (simp (no_asm_simp))
+done
+
+lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
+apply (unfold lift_def)
+apply (simp (no_asm_simp))
+done
+
+lemma lift_JN [simp]: "lift j (JOIN I F) = (JN i:I. lift j (F i))"
+apply (unfold lift_def)
+apply (simp (no_asm_simp))
+done
+
+(*** Safety: co, stable, invariant ***)
+
+lemma lift_constrains: 
+     "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_constrains)
+done
+
+lemma lift_stable: 
+     "(lift i F : stable (lift_set i A)) = (F : stable A)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_stable)
+done
+
+lemma lift_invariant: 
+     "(lift i F : invariant (lift_set i A)) = (F : invariant A)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_invariant)
+done
+
+lemma lift_Constrains: 
+     "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_Constrains)
+done
+
+lemma lift_Stable: 
+     "(lift i F : Stable (lift_set i A)) = (F : Stable A)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_Stable)
+done
+
+lemma lift_Always: 
+     "(lift i F : Always (lift_set i A)) = (F : Always A)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_Always)
+done
+
+(*** Progress: transient, ensures ***)
+
+lemma lift_transient: 
+     "(lift i F : transient (lift_set i A)) = (F : transient A)"
+
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_transient)
+done
+
+lemma lift_ensures: 
+     "(lift i F : (lift_set i A) ensures (lift_set i B)) =  
+      (F : A ensures B)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_ensures)
+done
+
+lemma lift_leadsTo: 
+     "(lift i F : (lift_set i A) leadsTo (lift_set i B)) =  
+      (F : A leadsTo B)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_leadsTo)
+done
+
+lemma lift_LeadsTo: 
+     "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) =   
+      (F : A LeadsTo B)"
+apply (unfold lift_def lift_set_def)
+apply (simp (no_asm_simp) add: rename_LeadsTo)
+done
+
+
+(** guarantees **)
+
+lemma lift_lift_guarantees_eq: 
+     "(lift i F : (lift i ` X) guarantees (lift i ` Y)) =  
+      (F : X guarantees Y)"
+
+apply (unfold lift_def)
+apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric])
+apply (simp (no_asm_simp) add: o_def)
+done
+
+lemma lift_guarantees_eq_lift_inv: "(lift i F : X guarantees Y) =  
+      (F : (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
+by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def)
 
 
+(*** 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*)
+lemma lift_preserves_snd_I: "F : preserves snd ==> lift i F : preserves snd"
+apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
+apply (simp (no_asm_simp) add: lift_def rename_preserves)
+apply (simp (no_asm_use) add: lift_map_def o_def split_def)
+done
+
+lemma delete_map_eqE':
+     "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)"
+apply (drule_tac f = "insert_map i (g i) " in arg_cong)
+apply (simp (no_asm_use) add: insert_map_delete_map_eq)
+apply (erule exI)
+done
+
+lemmas delete_map_eqE = delete_map_eqE' [THEN exE, elim!]
+
+lemma delete_map_neq_apply:
+     "[| delete_map j g = delete_map j g';  i~=j |] ==> g i = g' i"
+by force
+
+(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
+
+lemma vimage_o_fst_eq [simp]: "(f o fst) -` A = (f-`A) <*> UNIV"
+by auto
+
+lemma vimage_sub_eq_lift_set [simp]:
+     "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)"
+by auto
+
+lemma mem_lift_act_iff [iff]: 
+     "((s,s') : extend_act (%(x,u::unit). lift_map i x) act) =  
+      ((drop_map i s, drop_map i s') : act)"
+apply (unfold extend_act_def, auto)
+apply (rule bexI, auto)
+done
+
+lemma preserves_snd_lift_stable:
+     "[| F : preserves snd;  i~=j |]  
+      ==> lift j F : stable (lift_set i (A <*> UNIV))"
+apply (auto simp add: lift_def lift_set_def stable_def constrains_def rename_def extend_def mem_rename_set_iff)
+apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
+apply (drule_tac x = i in fun_cong, auto)
+done
+
+(*If i~=j then lift j F  does nothing to lift_set i, and the 
+  premise ensures A<=B.*)
+lemma constrains_imp_lift_constrains:
+    "[| F i : (A <*> UNIV) co (B <*> UNIV);   
+        F j : preserves snd |]   
+     ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
+apply (case_tac "i=j")
+apply (simp add: lift_def lift_set_def rename_constrains)
+apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R], assumption)
+apply (erule constrains_imp_subset [THEN lift_set_mono])
+done
+
+(** Lemmas for the transient theorem **)
+
+lemma insert_map_upd_same: "(insert_map i t f)(i := s) = insert_map i s f"
+by (rule ext, auto)
+
+lemma insert_map_upd:
+     "(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 - Suc 0 := s)))"
+apply (rule ext)
+apply (simp split add: nat_diff_split) 
+done
+
+lemma insert_map_eq_diff:
+     "[| insert_map i s f = insert_map j t g;  i~=j |]  
+      ==> EX g'. insert_map i s' f = insert_map j t g'"
+apply (subst insert_map_upd_same [symmetric])
+apply (erule ssubst)
+apply (simp only: insert_map_upd if_False split: split_if, blast)
+done
+
+lemma lift_map_eq_diff: 
+     "[| 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))"
+apply (unfold lift_map_def, auto)
+apply (blast dest: insert_map_eq_diff)
+done
+
+
+ML
+{*
+bind_thm ("export_mem_extend_act_iff", export mem_extend_act_iff)
+*}
+
+
+lemma lift_transient_eq_disj:
+     "F : preserves snd  
+      ==> (lift i F : transient (lift_set j (A <*> UNIV))) =  
+          (i=j & F : transient (A <*> UNIV) | A={})"
+apply (case_tac "i=j")
+apply (auto simp add: lift_transient)
+apply (auto simp add: lift_set_def lift_def transient_def rename_def extend_def Domain_extend_act)
+apply (drule subsetD, blast)
+apply auto
+apply (rename_tac s f uu s' f' uu')
+apply (subgoal_tac "f'=f & uu'=uu")
+ prefer 2 apply (force dest!: preserves_imp_eq, auto)
+apply (drule sym)
+apply (drule subsetD)
+apply (rule ImageI)
+apply (erule bij_lift_map [THEN good_map_bij, 
+                           THEN export_mem_extend_act_iff [THEN iffD2]], force)
+apply (erule lift_map_eq_diff [THEN exE], auto)
+done
+
+(*USELESS??*)
+lemma lift_map_image_Times: "lift_map i ` (A <*> UNIV) =  
+      (UN s:A. UN f. {insert_map i s f}) <*> UNIV"
+apply (auto intro!: bexI image_eqI simp add: lift_map_def)
+apply (rule split_conv [symmetric])
+done
+
+lemma lift_preserves_eq:
+     "(lift i F : preserves v) = (F : preserves (v o lift_map i))"
+by (simp add: lift_def rename_preserves)
+
+(*A useful rewrite.  If o, sub have been rewritten out already then can also
+  use it as   rewrite_rule [sub_def, o_def] lift_preserves_sub*)
+lemma lift_preserves_sub:
+     "F : preserves snd  
+      ==> lift i F : preserves (v o sub j o fst) =  
+          (if i=j then F : preserves (v o fst) else True)"
+apply (drule subset_preserves_o [THEN subsetD])
+apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
+apply (simp cong del: if_weak_cong add: lift_map_def eq_commute split_def o_def, auto)
+done
+
+
+(*** Lemmas to handle function composition (o) more consistently ***)
+
+(*Lets us prove one version of a theorem and store others*)
+lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
+by (simp add: expand_fun_eq o_def)
+
+lemma o_equiv_apply: "f o g = h ==> ALL x. f(g x) = h x"
+by (simp add: expand_fun_eq o_def)
+
+lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
+apply (rule ext)
+apply (auto simp add: o_def lift_map_def sub_def)
+done
+
+lemma snd_o_lift_map: "snd o lift_map i = snd o snd"
+apply (rule ext)
+apply (auto simp add: o_def lift_map_def)
+done
+
+
+(*** More lemmas about extend and project 
+     They could be moved to {Extend,Project}.ML, but DON'T need the locale ***)
+
+lemma extend_act_extend_act: "extend_act h' (extend_act h act) =  
+      extend_act (%(x,(y,y')). h'(h(x,y),y')) act"
+apply (auto elim!: rev_bexI simp add: extend_act_def, blast) 
+done
+
+lemma project_act_project_act: "project_act h (project_act h' act) =  
+      project_act (%(x,(y,y')). h'(h(x,y),y')) act"
+by (auto elim!: rev_bexI simp add: project_act_def)
+
+lemma project_act_extend_act:
+     "project_act h (extend_act h' act) =  
+        {(x,x'). EX s s' y y' z. (s,s') : act &  
+                 h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}"
+by (simp add: extend_act_def project_act_def, blast)
+
+
+(*** OK and "lift" ***)
+
+lemma act_in_UNION_preserves_fst:
+     "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts"
+apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I)
+apply (auto simp add: preserves_def stable_def constrains_def)
+done
+
+
+ML
+{*
+bind_thm ("export_Acts_extend", export Acts_extend);
+bind_thm ("export_AllowedActs_extend", export AllowedActs_extend)
+*}
+
+lemma UNION_OK_lift_I:
+     "[| ALL i:I. F i : preserves snd;   
+         ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |]  
+      ==> OK I (%i. lift i (F i))"
+apply (auto simp add: OK_def lift_def rename_def export_Acts_extend)
+apply (simp (no_asm) add: export_AllowedActs_extend project_act_extend_act)
+apply (rename_tac "act")
+apply (subgoal_tac
+       "{(x, x'). \<exists>s f u s' f' u'. 
+                    ((s, f, u), s', f', u') : act & 
+                    lift_map j x = lift_map i (s, f, u) & 
+                    lift_map j x' = lift_map i (s', f', u') } 
+                <= { (x,x') . fst x = fst x'}")
+apply (blast intro: act_in_UNION_preserves_fst, clarify)
+apply (drule_tac x = j in fun_cong)+
+apply (drule_tac x = i in bspec, assumption)
+apply (frule preserves_imp_eq, auto)
+done
+
+lemma OK_lift_I:
+     "[| ALL i:I. F i : preserves snd;   
+         ALL i:I. preserves fst <= Allowed (F i) |]  
+      ==> OK I (%i. lift i (F i))"
+by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)
+
+
+lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)"
+by (simp add: lift_def Allowed_rename)
+
+lemma lift_image_preserves: "lift i ` preserves v = preserves (v o drop_map i)"
+apply (simp (no_asm) add: rename_image_preserves lift_def inv_lift_map_eq)
+done
+
 end
diff -r e2fcd88be55d -r ab8f39f48a6f src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Fri Jan 24 14:06:49 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,281 +0,0 @@
-(*  Title:      HOL/UNITY/PPROD.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1999  University of Cambridge
-
-Abstraction over replicated components (PLam)
-General products of programs (Pi operation)
-
-Some dead wood here!
-*)
-
-(*** Basic properties ***)
-
-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";
-
-Addsimps [Init_PLam];
-
-Goal "PLam {} F = SKIP";
-by (simp_tac (simpset() addsimps [PLam_def]) 1);
-qed "PLam_empty";
-
-Goal "(plam i: I. SKIP) = SKIP";
-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 i (F i)) Join (PLam I F)";
-by Auto_tac;
-qed "PLam_insert";
-
-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 i (F i) <= (PLam I F)";
-(*blast_tac doesn't use HO unification*)
-by (fast_tac (claset() addIs [component_JN]) 1);
-qed "component_PLam";
-
-
-(** 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]) 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;  ALL j. F j : preserves snd |]  \
-\     ==> (PLam I F : stable (lift_set i (A <*> UNIV))) = \
-\         (F i : stable (A <*> 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 i (F i) : transient A)";
-by (asm_simp_tac (simpset() addsimps [JN_transient, PLam_def]) 1);
-qed "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, 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;  \
-\        F i : ((A <*> UNIV) - (B <*> UNIV)) co \
-\              ((A <*> UNIV) Un (B <*> UNIV));  \
-\        F i : transient ((A <*> UNIV) - (B <*> UNIV));  \
-\        ALL j. F j : preserves snd |] ==>  \
-\     PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)";
-by (rtac (PLam_ensures RS leadsTo_Basis) 1);
-by (rtac ensuresI 2);
-by (ALLGOALS assume_tac);
-qed "PLam_leadsTo_Basis";
-
-
-(** invariant **)
-
-Goal "[| F i : invariant (A <*> UNIV);  i : I;  \
-\        ALL j. F j : preserves snd |] \
-\     ==> PLam I F : invariant (lift_set i (A <*> UNIV))";
-by (auto_tac (claset(),
-	      simpset() addsimps [PLam_stable, invariant_def]));
-qed "invariant_imp_PLam_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);
-qed "PLam_preserves_fst";
-Addsimps [PLam_preserves_fst];
-
-Goal "ALL j. F j : preserves snd ==> PLam I F : preserves snd";
-by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_snd_I]) 1);
-qed "PLam_preserves_snd";
-Addsimps [PLam_preserves_snd];
-AddIs [PLam_preserves_snd];
-
-
-(*** guarantees properties ***)
-
-(*This rule looks unsatisfactory because it refers to "lift".  One must use
-  lift_guarantees_eq_lift_inv to rewrite the first subgoal and
-  something like lift_preserves_sub to rewrite the third.  However there's
-  no obvious way to alternative for the third premise.*)
-Goalw [PLam_def]
-    "[| lift i (F i): X guarantees Y;  i : I;  \
-\       OK I (%i. lift i (F i)) |]  \
-\    ==> (PLam I F) : X guarantees Y"; 
-by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
-qed "guarantees_PLam_I";
-
-Goal "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))";
-by (simp_tac (simpset() addsimps [PLam_def]) 1); 
-qed "Allowed_PLam";
-Addsimps [Allowed_PLam];
-
-Goal "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))";
-by (simp_tac (simpset() addsimps [PLam_def, lift_def, rename_preserves]) 1); 
-qed "PLam_preserves";
-Addsimps [PLam_preserves];
-
-(**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";
-
-    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";
-**)
-
-
-(**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";
-
-    (*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";
-
-    (*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";
-
-
-    (*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";
-
-
-    (** 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";
-
-
-
-    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;  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";
-
-
-    (** 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 [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";
-**)
-
diff -r e2fcd88be55d -r ab8f39f48a6f src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Fri Jan 24 14:06:49 2003 +0100
+++ b/src/HOL/UNITY/PPROD.thy	Fri Jan 24 18:13:59 2003 +0100
@@ -5,9 +5,11 @@
 
 Abstraction over replicated components (PLam)
 General products of programs (Pi operation)
+
+Some dead wood here!
 *)
 
-PPROD = Lift_prog +
+theory PPROD = Lift_prog:
 
 constdefs
 
@@ -16,9 +18,258 @@
     "PLam I F == JN i:I. lift i (F i)"
 
 syntax
-  "@PLam" :: [pttrn, nat set, 'b set] => (nat => 'b) set ("(3plam _:_./ _)" 10)
+  "@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"
+              ("(3plam _:_./ _)" 10)
 
 translations
   "plam x:A. B"   == "PLam A (%x. B)"
 
+
+(*** Basic properties ***)
+
+lemma Init_PLam: "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))"
+apply (simp (no_asm) add: PLam_def lift_def lift_set_def)
+done
+
+declare Init_PLam [simp]
+
+lemma PLam_empty: "PLam {} F = SKIP"
+apply (simp (no_asm) add: PLam_def)
+done
+
+lemma PLam_SKIP: "(plam i: I. SKIP) = SKIP"
+apply (simp (no_asm) add: PLam_def lift_SKIP JN_constant)
+done
+
+declare PLam_SKIP [simp] PLam_empty [simp]
+
+lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
+by (unfold PLam_def, auto)
+
+lemma PLam_component_iff: "((PLam I F) <= H) = (ALL i: I. lift i (F i) <= H)"
+apply (simp (no_asm) add: PLam_def JN_component_iff)
+done
+
+lemma component_PLam: "i : I ==> lift i (F i) <= (PLam I F)"
+apply (unfold PLam_def)
+(*blast_tac doesn't use HO unification*)
+apply (fast intro: component_JN)
+done
+
+
+(** Safety & Progress: but are they used anywhere? **)
+
+lemma PLam_constrains: "[| 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))"
+apply (simp (no_asm_simp) add: PLam_def JN_constrains)
+apply (subst insert_Diff [symmetric], assumption)
+apply (simp (no_asm_simp) add: lift_constrains)
+apply (blast intro: constrains_imp_lift_constrains)
+done
+
+lemma PLam_stable: "[| i : I;  ALL j. F j : preserves snd |]   
+      ==> (PLam I F : stable (lift_set i (A <*> UNIV))) =  
+          (F i : stable (A <*> UNIV))"
+apply (simp (no_asm_simp) add: stable_def PLam_constrains)
+done
+
+lemma PLam_transient: "i : I ==>  
+    PLam I F : transient A = (EX i:I. lift i (F i) : transient A)"
+apply (simp (no_asm_simp) add: JN_transient PLam_def)
+done
+
+(*This holds because the F j cannot change (lift_set i)*)
+lemma PLam_ensures: "[| 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)"
+apply (auto simp add: ensures_def PLam_constrains PLam_transient lift_transient_eq_disj lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
+done
+
+lemma PLam_leadsTo_Basis: "[| i : I;   
+         F i : ((A <*> UNIV) - (B <*> UNIV)) co  
+               ((A <*> UNIV) Un (B <*> UNIV));   
+         F i : transient ((A <*> UNIV) - (B <*> UNIV));   
+         ALL j. F j : preserves snd |] ==>   
+      PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
+by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
+
+
+
+(** invariant **)
+
+lemma invariant_imp_PLam_invariant: "[| F i : invariant (A <*> UNIV);  i : I;   
+         ALL j. F j : preserves snd |]  
+      ==> PLam I F : invariant (lift_set i (A <*> UNIV))"
+by (auto simp add: PLam_stable invariant_def)
+
+
+lemma PLam_preserves_fst [simp]:
+     "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 (simp (no_asm_simp) add: PLam_def lift_preserves_sub)
+
+lemma PLam_preserves_snd [simp,intro]:
+     "ALL j. F j : preserves snd ==> PLam I F : preserves snd"
+by (simp (no_asm_simp) add: PLam_def lift_preserves_snd_I)
+
+
+
+(*** guarantees properties ***)
+
+(*This rule looks unsatisfactory because it refers to "lift".  One must use
+  lift_guarantees_eq_lift_inv to rewrite the first subgoal and
+  something like lift_preserves_sub to rewrite the third.  However there's
+  no obvious way to alternative for the third premise.*)
+lemma guarantees_PLam_I: 
+    "[| lift i (F i): X guarantees Y;  i : I;   
+        OK I (%i. lift i (F i)) |]   
+     ==> (PLam I F) : X guarantees Y"
+apply (unfold PLam_def)
+apply (simp (no_asm_simp) add: guarantees_JN_I)
+done
+
+lemma Allowed_PLam [simp]:
+     "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))"
+by (simp (no_asm) add: PLam_def)
+
+
+lemma PLam_preserves [simp]:
+     "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))"
+by (simp (no_asm) add: PLam_def lift_def rename_preserves)
+
+
+(**UNUSED
+    (*The f0 premise ensures that the product is well-defined.*)
+    lemma PLam_invariant_imp_invariant: "[| PLam I F : invariant (lift_set i A);  i : I;   
+             f0: Init (PLam I F) |] ==> F i : invariant A"
+    apply (auto simp add: invariant_def)
+    apply (drule_tac c = "f0 (i:=x) " in subsetD)
+    apply auto
+    done
+
+    lemma PLam_invariant: "[| i : I;  f0: Init (PLam I F) |]  
+          ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)"
+    apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
+    done
+
+    (*The f0 premise isn't needed if F is a constant program because then
+      we get an initial state by replicating that of F*)
+    lemma reachable_PLam: "i : I  
+          ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)"
+    apply (auto simp add: invariant_def)
+    done
+**)
+
+
+(**UNUSED
+    (** Reachability **)
+
+    Goal "[| f : reachable (PLam I F);  i : I |] ==> f i : reachable (F i)"
+    apply (erule reachable.induct)
+    apply (auto intro: reachable.intrs)
+    done
+
+    (*Result to justify a re-organization of this file*)
+    lemma ??unknown??: "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"
+    apply auto
+    result()
+
+    lemma reachable_PLam_subset1: "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"
+    apply (force dest!: reachable_PLam)
+    done
+
+    (*simplify using reachable_lift??*)
+    lemma reachable_lift_Join_PLam [rule_format (no_asm)]: "[| 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)"
+    apply (erule reachable.induct)
+    apply (ALLGOALS Clarify_tac)
+    apply (erule reachable.induct)
+    (*Init, Init case*)
+    apply (force intro: reachable.intrs)
+    (*Init of F, action of PLam F case*)
+    apply (rule_tac act = act in reachable.Acts)
+    apply force
+    apply assumption
+    apply (force intro: ext)
+    (*induction over the 2nd "reachable" assumption*)
+    apply (erule_tac xa = f in reachable.induct)
+    (*Init of PLam F, action of F case*)
+    apply (rule_tac act = "lift_act i act" in reachable.Acts)
+    apply force
+    apply (force intro: reachable.Init)
+    apply (force intro: ext simp add: lift_act_def)
+    (*last case: an action of PLam I F*)
+    apply (rule_tac act = acta in reachable.Acts)
+    apply force
+    apply assumption
+    apply (force intro: ext)
+    done
+
+
+    (*The index set must be finite: otherwise infinitely many copies of F can
+      perform actions, and PLam can never catch up in finite time.*)
+    lemma reachable_PLam_subset2: "finite I  
+          ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)"
+    apply (erule finite_induct)
+    apply (simp (no_asm))
+    apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
+    done
+
+    lemma reachable_PLam_eq: "finite I ==>  
+          reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))"
+    apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
+    done
+
+
+    (** Co **)
+
+    lemma Constrains_imp_PLam_Constrains: "[| F i : A Co B;  i: I;  finite I |]   
+          ==> PLam I F : (lift_set i A) Co (lift_set i B)"
+    apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
+    apply (auto simp add: constrains_def PLam_def)
+    apply (REPEAT (blast intro: reachable.intrs))
+    done
+
+
+
+    lemma PLam_Constrains: "[| 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)"
+    apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
+    done
+
+    lemma PLam_Stable: "[| i: I;  finite I;  f0: Init (PLam I F) |]   
+          ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)"
+    apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains)
+    done
+
+
+    (** const_PLam (no dependence on i) doesn't require the f0 premise **)
+
+    lemma const_PLam_Constrains: "[| i: I;  finite I |]   
+          ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) =   
+              (F : A Co B)"
+    apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
+    done
+
+    lemma const_PLam_Stable: "[| i: I;  finite I |]   
+          ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)"
+    apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains)
+    done
+
+    lemma const_PLam_Increasing: 
+	 "[| i: I;  finite I |]   
+          ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)"
+    apply (unfold Increasing_def)
+    apply (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}")
+    apply (asm_simp_tac (simpset () add: lift_set_sub) 2)
+    apply (simp add: finite_lessThan const_PLam_Stable)
+    done
+**)
+
+
 end
diff -r e2fcd88be55d -r ab8f39f48a6f src/HOL/UNITY/UNITY_Main.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/UNITY_Main.thy	Fri Jan 24 18:13:59 2003 +0100
@@ -0,0 +1,27 @@
+(*  Title:      HOL/UNITY/UNITY_Main.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2003  University of Cambridge
+
+Inclusive UNITY theory
+*)
+
+theory UNITY_Main = Detects + PPROD + Follows
+files "UNITY_tactics.ML":
+
+method_setup constrains = {*
+    Method.ctxt_args (fn ctxt =>
+        Method.METHOD (fn facts => 
+            gen_constrains_tac (Classical.get_local_claset ctxt,
+                               Simplifier.get_local_simpset ctxt) 1)) *}
+    "for proving safety properties"
+
+method_setup ensures_tac = {*
+    fn args => fn ctxt =>
+        Method.goal_args' (Scan.lift Args.name) 
+           (gen_ensures_tac (Classical.get_local_claset ctxt,
+                               Simplifier.get_local_simpset ctxt))
+           args ctxt *}
+    "for proving progress properties"
+
+end
diff -r e2fcd88be55d -r ab8f39f48a6f src/HOL/UNITY/UNITY_tactics.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/UNITY_tactics.ML	Fri Jan 24 18:13:59 2003 +0100
@@ -0,0 +1,145 @@
+(*  Title:      HOL/UNITY/UNITY_tactics.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2003  University of Cambridge
+
+Specialized UNITY tactics, and ML bindings of theorems
+*)
+
+
+(*Lift_prog*)
+val sub_def = thm "sub_def";
+val lift_map_def = thm "lift_map_def";
+val drop_map_def = thm "drop_map_def";
+val insert_map_inverse = thm "insert_map_inverse";
+val insert_map_delete_map_eq = thm "insert_map_delete_map_eq";
+val insert_map_inject1 = thm "insert_map_inject1";
+val insert_map_inject2 = thm "insert_map_inject2";
+val insert_map_inject = thm "insert_map_inject";
+val insert_map_inject = thm "insert_map_inject";
+val lift_map_eq_iff = thm "lift_map_eq_iff";
+val drop_map_lift_map_eq = thm "drop_map_lift_map_eq";
+val inj_lift_map = thm "inj_lift_map";
+val lift_map_drop_map_eq = thm "lift_map_drop_map_eq";
+val drop_map_inject = thm "drop_map_inject";
+val surj_lift_map = thm "surj_lift_map";
+val bij_lift_map = thm "bij_lift_map";
+val inv_lift_map_eq = thm "inv_lift_map_eq";
+val inv_drop_map_eq = thm "inv_drop_map_eq";
+val bij_drop_map = thm "bij_drop_map";
+val sub_apply = thm "sub_apply";
+val lift_set_empty = thm "lift_set_empty";
+val lift_set_iff = thm "lift_set_iff";
+val lift_set_iff2 = thm "lift_set_iff2";
+val lift_set_mono = thm "lift_set_mono";
+val lift_set_Un_distrib = thm "lift_set_Un_distrib";
+val lift_set_Diff_distrib = thm "lift_set_Diff_distrib";
+val bij_lift = thm "bij_lift";
+val lift_SKIP = thm "lift_SKIP";
+val lift_Join = thm "lift_Join";
+val lift_JN = thm "lift_JN";
+val lift_constrains = thm "lift_constrains";
+val lift_stable = thm "lift_stable";
+val lift_invariant = thm "lift_invariant";
+val lift_Constrains = thm "lift_Constrains";
+val lift_Stable = thm "lift_Stable";
+val lift_Always = thm "lift_Always";
+val lift_transient = thm "lift_transient";
+val lift_ensures = thm "lift_ensures";
+val lift_leadsTo = thm "lift_leadsTo";
+val lift_LeadsTo = thm "lift_LeadsTo";
+val lift_lift_guarantees_eq = thm "lift_lift_guarantees_eq";
+val lift_guarantees_eq_lift_inv = thm "lift_guarantees_eq_lift_inv";
+val lift_preserves_snd_I = thm "lift_preserves_snd_I";
+val delete_map_eqE = thm "delete_map_eqE";
+val delete_map_eqE = thm "delete_map_eqE";
+val delete_map_neq_apply = thm "delete_map_neq_apply";
+val vimage_o_fst_eq = thm "vimage_o_fst_eq";
+val vimage_sub_eq_lift_set = thm "vimage_sub_eq_lift_set";
+val mem_lift_act_iff = thm "mem_lift_act_iff";
+val preserves_snd_lift_stable = thm "preserves_snd_lift_stable";
+val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains";
+val insert_map_upd_same = thm "insert_map_upd_same";
+val insert_map_upd = thm "insert_map_upd";
+val insert_map_eq_diff = thm "insert_map_eq_diff";
+val lift_map_eq_diff = thm "lift_map_eq_diff";
+val lift_transient_eq_disj = thm "lift_transient_eq_disj";
+val lift_map_image_Times = thm "lift_map_image_Times";
+val lift_preserves_eq = thm "lift_preserves_eq";
+val lift_preserves_sub = thm "lift_preserves_sub";
+val o_equiv_assoc = thm "o_equiv_assoc";
+val o_equiv_apply = thm "o_equiv_apply";
+val fst_o_lift_map = thm "fst_o_lift_map";
+val snd_o_lift_map = thm "snd_o_lift_map";
+val extend_act_extend_act = thm "extend_act_extend_act";
+val project_act_project_act = thm "project_act_project_act";
+val project_act_extend_act = thm "project_act_extend_act";
+val act_in_UNION_preserves_fst = thm "act_in_UNION_preserves_fst";
+val UNION_OK_lift_I = thm "UNION_OK_lift_I";
+val OK_lift_I = thm "OK_lift_I";
+val Allowed_lift = thm "Allowed_lift";
+val lift_image_preserves = thm "lift_image_preserves";
+
+
+(*PPROD*)
+val Init_PLam = thm "Init_PLam";
+val PLam_empty = thm "PLam_empty";
+val PLam_SKIP = thm "PLam_SKIP";
+val PLam_insert = thm "PLam_insert";
+val PLam_component_iff = thm "PLam_component_iff";
+val component_PLam = thm "component_PLam";
+val PLam_constrains = thm "PLam_constrains";
+val PLam_stable = thm "PLam_stable";
+val PLam_transient = thm "PLam_transient";
+val PLam_ensures = thm "PLam_ensures";
+val PLam_leadsTo_Basis = thm "PLam_leadsTo_Basis";
+val invariant_imp_PLam_invariant = thm "invariant_imp_PLam_invariant";
+val PLam_preserves_fst = thm "PLam_preserves_fst";
+val PLam_preserves_snd = thm "PLam_preserves_snd";
+val guarantees_PLam_I = thm "guarantees_PLam_I";
+val Allowed_PLam = thm "Allowed_PLam";
+val PLam_preserves = thm "PLam_preserves";
+
+
+(*proves "co" properties when the program is specified*)
+fun gen_constrains_tac(cs,ss) i = 
+   SELECT_GOAL
+      (EVERY [REPEAT (Always_Int_tac 1),
+	      REPEAT (etac Always_ConstrainsI 1
+		      ORELSE
+		      resolve_tac [StableI, stableI,
+				   constrains_imp_Constrains] 1),
+	      rtac constrainsI 1,
+	      full_simp_tac ss 1,
+	      REPEAT (FIRSTGOAL (etac disjE)),
+	      ALLGOALS (clarify_tac cs),
+	      ALLGOALS (asm_lr_simp_tac ss)]) i;
+
+(*proves "ensures/leadsTo" properties when the program is specified*)
+fun gen_ensures_tac(cs,ss) sact = 
+    SELECT_GOAL
+      (EVERY [REPEAT (Always_Int_tac 1),
+	      etac Always_LeadsTo_Basis 1 
+	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
+		  REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
+				    EnsuresI, ensuresI] 1),
+	      (*now there are two subgoals: co & transient*)
+	      simp_tac ss 2,
+	      res_inst_tac [("act", sact)] transientI 2,
+                 (*simplify the command's domain*)
+	      simp_tac (ss addsimps [Domain_def]) 3,
+	      gen_constrains_tac (cs,ss) 1,
+	      ALLGOALS (clarify_tac cs),
+	      ALLGOALS (asm_lr_simp_tac ss)]);
+
+
+(*Composition equivalences, from Lift_prog*)
+
+fun make_o_equivs th =
+    [th,
+     th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]),
+     th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];
+
+Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);
+
+Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);