New treatment of "guarantees" with polymorphic components and bijections.
authorpaulson
Fri Feb 18 15:20:44 2000 +0100 (2000-02-18)
changeset 82519be357df93d4
parent 8250 f4029c34adef
child 8252 af44242c5e7a
New treatment of "guarantees" with polymorphic components and bijections.
Works EXCEPT FOR Alloc.
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Client.thy
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Guar.ML
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/PPROD.ML
src/HOL/UNITY/PPROD.thy
src/HOL/UNITY/Project.ML
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/TimerArray.ML
src/HOL/UNITY/TimerArray.thy
src/HOL/UNITY/Union.ML
src/HOL/UNITY/WFair.ML
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Wed Feb 16 15:04:12 2000 +0100
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Fri Feb 18 15:20:44 2000 +0100
     1.3 @@ -425,8 +425,8 @@
     1.4  	   Client_component_System] MRS component_guaranteesD) 1);
     1.5  by (rtac Client_i_Bounded 1);
     1.6  by (auto_tac(claset(),
     1.7 -	 simpset() addsimps [o_apply, lift_export Collect_eq_extend_set RS sym,
     1.8 -			     client_export Collect_eq_extend_set RS sym]));
     1.9 +	 simpset() addsimps [o_apply, lift_export extend_set_eq_Collect,
    1.10 +			     client_export extend_set_eq_Collect]));
    1.11  qed "System_Bounded_ask";
    1.12  
    1.13  (*progress (2), step 4*)
    1.14 @@ -479,7 +479,7 @@
    1.15  by (full_simp_tac (simpset() addsimps [fold_o_sub, lift_prog_correct]) 1);
    1.16  by (rtac INT_I 1);
    1.17  by (simp_tac (simpset() addsimps [o_apply]) 1);
    1.18 -by (REPEAT (stac (lift_export Collect_eq_extend_set) 1));
    1.19 +by (REPEAT (stac (lift_export extend_set_eq_Collect RS sym) 1));
    1.20  by (rtac (lift_export project_Ensures_D) 1);
    1.21  by (asm_full_simp_tac (simpset() addsimps [o_apply, lift_prog_correct, 
    1.22  					   drop_prog_correct]) 1);
    1.23 @@ -541,18 +541,17 @@
    1.24  by (Simp_tac 1);
    1.25  by (rtac INT_I 1);
    1.26  by (simp_tac (simpset() addsimps [o_apply]) 1);
    1.27 -by (REPEAT (stac (client_export Collect_eq_extend_set) 1));
    1.28 +by (REPEAT (stac (client_export extend_set_eq_Collect RS sym) 1));
    1.29  by (rtac (client_export project_Ensures_D) 1);
    1.30  by (asm_full_simp_tac (simpset() addsimps [o_apply]) 1);
    1.31  by (asm_full_simp_tac
    1.32      (simpset() addsimps [all_conj_distrib,
    1.33  			 Increasing_def, Stable_eq_stable, Join_stable,
    1.34 -			 Collect_eq_extend_set RS sym]) 1);
    1.35 +			 extend_set_eq_Collect]) 1);
    1.36  by (Clarify_tac 1);
    1.37  by (dtac G_stable_sysOfClient 1);
    1.38  by (auto_tac (claset(), 
    1.39 -	      simpset() addsimps [o_apply,
    1.40 -				client_export Collect_eq_extend_set RS sym]));
    1.41 +     simpset() addsimps [o_apply, client_export extend_set_eq_Collect]));
    1.42  qed "sysOfClient_i_Progress";
    1.43  
    1.44  
     2.1 --- a/src/HOL/UNITY/Client.ML	Wed Feb 16 15:04:12 2000 +0100
     2.2 +++ b/src/HOL/UNITY/Client.ML	Fri Feb 18 15:20:44 2000 +0100
     2.3 @@ -46,10 +46,12 @@
     2.4  by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
     2.5  		       addSIs [stable_Int]) 3);
     2.6  by (constrains_tac 2);
     2.7 +by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2);
     2.8  by Auto_tac;
     2.9  qed "ask_bounded_lemma";
    2.10  
    2.11 -(*export version, with no mention of tok*)
    2.12 +(*export version, with no mention of tok in the postcondition, but
    2.13 +  unfortunately tok must be declared local.*)
    2.14  Goal "Client: UNIV guarantees[funPair ask tok] \
    2.15  \             Always {s. ALL elt : set (ask s). elt <= NbT}";
    2.16  by (rtac guaranteesI 1);
    2.17 @@ -90,7 +92,6 @@
    2.18  qed "transient_lemma";
    2.19  
    2.20  
    2.21 -
    2.22  Goal "[| Client Join G : Increasing giv;  G : preserves (funPair rel ask) |] \
    2.23  \ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}  \
    2.24  \                     LeadsTo {s. k < rel s & rel s <= giv s & \
    2.25 @@ -139,6 +140,7 @@
    2.26  			addDs [common_prefix_linear]) 1);
    2.27  qed "client_progress_lemma";
    2.28  
    2.29 +(*Progress property: all tokens that are given will be released*)
    2.30  Goal "Client : \
    2.31  \      Increasing giv  guarantees[funPair rel ask]  \
    2.32  \      (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
    2.33 @@ -147,6 +149,28 @@
    2.34  by (blast_tac (claset() addIs [client_progress_lemma]) 1);
    2.35  qed "client_progress";
    2.36  
    2.37 +Goal "Client : preserves extra";
    2.38 +by (rewtac preserves_def);
    2.39 +by Auto_tac;
    2.40 +by (constrains_tac 1);
    2.41 +by Auto_tac;
    2.42 +qed "client_preserves_extra";
    2.43 +
    2.44 +Goal "bij client_map";
    2.45 +by (auto_tac (claset() addSWrapper record_split_wrapper, 
    2.46 +	      simpset() addsimps [client_map_def, non_extra_def, bij_def, 
    2.47 +				  inj_on_def, surj_def]));
    2.48 +by (res_inst_tac 
    2.49 +    [("x", "(|giv=?a, ask=?b, rel=?c, tok=?d, extra=?e|)")] exI 1);
    2.50 +by (Force_tac 1);
    2.51 +qed "bij_client_map";
    2.52 +
    2.53 +Goal "rename client_map Client : preserves snd";
    2.54 +by (asm_simp_tac (simpset() addsimps [bij_client_map RS rename_preserves]) 1);
    2.55 +by (asm_simp_tac (simpset() addsimps [client_map_def]) 1);
    2.56 +by (rtac client_preserves_extra 1);
    2.57 +qed "client_preserves_extra";
    2.58 +
    2.59  
    2.60  (** Obsolete lemmas from first version of the Client **)
    2.61  
     3.1 --- a/src/HOL/UNITY/Client.thy	Wed Feb 16 15:04:12 2000 +0100
     3.2 +++ b/src/HOL/UNITY/Client.thy	Fri Feb 18 15:20:44 2000 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  Distributed Resource Management System: the Client
     3.5  *)
     3.6  
     3.7 -Client = Extend + 
     3.8 +Client = Rename + 
     3.9  
    3.10  consts
    3.11    NbT :: nat       (*Maximum number of tokens*)
    3.12 @@ -20,6 +20,10 @@
    3.13    rel :: tokbag list   (*output history: tokens released*)
    3.14    tok :: tokbag	       (*current token request*)
    3.15  
    3.16 +record 'a state_u =
    3.17 +  state +  
    3.18 +  extra :: 'a          (*new variables*)
    3.19 +
    3.20  
    3.21  (*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
    3.22  
    3.23 @@ -27,7 +31,7 @@
    3.24    
    3.25    (** Release some tokens **)
    3.26    
    3.27 -  rel_act :: "(state*state) set"
    3.28 +  rel_act :: "('a state_u * 'a state_u) set"
    3.29      "rel_act == {(s,s').
    3.30  		  EX nrel. nrel = size (rel s) &
    3.31  		           s' = s (| rel := rel s @ [giv s!nrel] |) &
    3.32 @@ -39,26 +43,27 @@
    3.33    (** Including s'=s suppresses fairness, allowing the non-trivial part
    3.34        of the action to be ignored **)
    3.35  
    3.36 -  tok_act :: "(state*state) set"
    3.37 -    "tok_act == {(s,s'). s'=s | (EX t: atMost NbT. s' = s (|tok := t|))}"
    3.38 -
    3.39 -  (*
    3.40 -      "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
    3.41 -  *)
    3.42 -
    3.43 +  tok_act :: "('a state_u * 'a state_u) set"
    3.44 +     "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
    3.45    
    3.46 -  ask_act :: "(state*state) set"
    3.47 +  ask_act :: "('a state_u * 'a state_u) set"
    3.48      "ask_act == {(s,s'). s'=s |
    3.49  		         (s' = s (|ask := ask s @ [tok s]|))}"
    3.50  
    3.51 -  Client :: state program
    3.52 +  Client :: 'a state_u program
    3.53      "Client == mk_program ({s. tok s : atMost NbT &
    3.54  		               giv s = [] & ask s = [] & rel s = []},
    3.55  			   {rel_act, tok_act, ask_act})"
    3.56  
    3.57 -  giv_meets_ask :: state set
    3.58 -    "giv_meets_ask ==
    3.59 -       {s. size (giv s) <= size (ask s) & 
    3.60 -           (ALL n: lessThan (size (giv s)). ask s!n <= giv s!n)}"
    3.61 +  (*Maybe want a special theory section to declare such maps*)
    3.62 +  non_extra :: 'a state_u => state
    3.63 +    "non_extra s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
    3.64 +
    3.65 +  (*Renaming map to put a Client into the standard form*)
    3.66 +  client_map :: "'a state_u => state*'a"
    3.67 +    "client_map == funPair non_extra extra"
    3.68 +
    3.69 +rules
    3.70 +  NbT_pos  "0 < NbT"
    3.71  
    3.72  end
     4.1 --- a/src/HOL/UNITY/Comp.ML	Wed Feb 16 15:04:12 2000 +0100
     4.2 +++ b/src/HOL/UNITY/Comp.ML	Fri Feb 18 15:20:44 2000 +0100
     4.3 @@ -90,6 +90,16 @@
     4.4  
     4.5  (*** preserves ***)
     4.6  
     4.7 +val prems = 
     4.8 +Goalw [preserves_def] "(!!z. F : stable {s. v s = z}) ==> F : preserves v";
     4.9 +by (blast_tac (claset() addIs prems) 1);
    4.10 +qed "preservesI";
    4.11 +
    4.12 +Goalw [preserves_def, stable_def, constrains_def]
    4.13 +     "[| F : preserves v;  act : Acts F;  (s,s') : act |] ==> v s = v s'";
    4.14 +by (Force_tac 1);
    4.15 +qed "preserves_imp_eq";
    4.16 +
    4.17  Goal "(F Join G : preserves v) = (F : preserves v & G : preserves v)";
    4.18  by (simp_tac (simpset() addsimps [Join_stable, preserves_def]) 1);
    4.19  by (Blast_tac 1);
    4.20 @@ -102,10 +112,14 @@
    4.21  
    4.22  AddIffs [Join_preserves, JN_preserves];
    4.23  
    4.24 +Goalw [funPair_def] "(funPair f g) x = (f x, g x)";
    4.25 +by (Simp_tac 1);
    4.26 +qed "funPair_apply";
    4.27 +Addsimps [funPair_apply];
    4.28 +
    4.29  Goal "preserves (funPair v w) = preserves v Int preserves w";
    4.30  by (auto_tac (claset(),
    4.31 -	      simpset() addsimps [funPair_def, preserves_def, 
    4.32 -				  stable_def, constrains_def]));
    4.33 +	      simpset() addsimps [preserves_def, stable_def, constrains_def]));
    4.34  by (Blast_tac 1);
    4.35  qed "preserves_funPair";
    4.36  
    4.37 @@ -117,6 +131,17 @@
    4.38  by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
    4.39  qed "funPair_o_distrib";
    4.40  
    4.41 +
    4.42 +Goal "fst o (funPair f g) = f";
    4.43 +by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
    4.44 +qed "fst_o_funPair";
    4.45 +
    4.46 +Goal "snd o (funPair f g) = g";
    4.47 +by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
    4.48 +qed "snd_o_funPair";
    4.49 +Addsimps [fst_o_funPair, snd_o_funPair];
    4.50 +
    4.51 +
    4.52  Goal "preserves v <= preserves (w o v)";
    4.53  by (force_tac (claset(),
    4.54  	       simpset() addsimps [preserves_def, 
    4.55 @@ -125,8 +150,7 @@
    4.56  
    4.57  Goal "preserves v <= stable {s. P (v s)}";
    4.58  by (auto_tac (claset(),
    4.59 -	      simpset() addsimps [preserves_def, 
    4.60 -				  stable_def, constrains_def]));
    4.61 +	      simpset() addsimps [preserves_def, stable_def, constrains_def]));
    4.62  by (rename_tac "s' s" 1);
    4.63  by (subgoal_tac "v s = v s'" 1);
    4.64  by (ALLGOALS Force_tac);
    4.65 @@ -154,7 +178,7 @@
    4.66  by (Asm_simp_tac 2);
    4.67  by (dres_inst_tac [("P1", "split ?Q")]  
    4.68      (impOfSubs preserves_subset_stable) 1);
    4.69 -by (auto_tac (claset(), simpset() addsimps [funPair_def]));
    4.70 +by Auto_tac;
    4.71  qed "stable_localTo_stable2";
    4.72  
    4.73  Goal "[| F : stable {s. v s <= w s};  G : preserves v;       \
     5.1 --- a/src/HOL/UNITY/Extend.ML	Wed Feb 16 15:04:12 2000 +0100
     5.2 +++ b/src/HOL/UNITY/Extend.ML	Fri Feb 18 15:20:44 2000 +0100
     5.3 @@ -10,6 +10,10 @@
     5.4  
     5.5  (** These we prove OUTSIDE the locale. **)
     5.6  
     5.7 +Goal "f Id = Id ==> insert Id (f``Acts F) = f `` Acts F";
     5.8 +by (blast_tac (claset() addIs [sym RS image_eqI]) 1);
     5.9 +qed "insert_Id_image_Acts";
    5.10 +
    5.11  (*Possibly easier than reasoning about "inv h"*)
    5.12  val [surj_h,prem] = 
    5.13  Goalw [good_map_def]
    5.14 @@ -115,22 +119,25 @@
    5.15  qed "extend_set_strict_mono";
    5.16  AddIffs [extend_set_strict_mono];
    5.17  
    5.18 -Goal "{s. P (f s)} = extend_set h {s. P s}";
    5.19 +Goalw [extend_set_def] "extend_set h {} = {}";
    5.20  by Auto_tac;
    5.21 -qed "Collect_eq_extend_set";
    5.22 +qed "extend_set_empty";
    5.23 +Addsimps [extend_set_empty];
    5.24 +
    5.25 +Goal "extend_set h {s. P s} = {s. P (f s)}";
    5.26 +by Auto_tac;
    5.27 +qed "extend_set_eq_Collect";
    5.28  
    5.29  Goal "extend_set h {x} = {s. f s = x}";
    5.30  by Auto_tac;
    5.31  qed "extend_set_sing";
    5.32  
    5.33 -Goalw [extend_set_def]
    5.34 -     "project_set h (extend_set h C) = C";
    5.35 +Goalw [extend_set_def] "project_set h (extend_set h C) = C";
    5.36  by Auto_tac;
    5.37  qed "extend_set_inverse";
    5.38  Addsimps [extend_set_inverse];
    5.39  
    5.40 -Goalw [extend_set_def]
    5.41 -     "C <= extend_set h (project_set h C)";
    5.42 +Goalw [extend_set_def] "C <= extend_set h (project_set h C)";
    5.43  by (auto_tac (claset(), 
    5.44  	      simpset() addsimps [split_extended_all]));
    5.45  by (Blast_tac 1);
    5.46 @@ -277,8 +284,7 @@
    5.47                simpset() addsimps [split_extended_all]) 1);
    5.48  qed "project_act_I";
    5.49  
    5.50 -Goalw [project_act_def]
    5.51 -    "UNIV <= project_set h C ==> project_act h (Restrict C Id) = Id";
    5.52 +Goalw [project_act_def] "project_act h Id = Id";
    5.53  by (Force_tac 1);
    5.54  qed "project_act_Id";
    5.55  
    5.56 @@ -288,18 +294,7 @@
    5.57                simpset() addsimps [split_extended_all]) 1);
    5.58  qed "Domain_project_act";
    5.59  
    5.60 -Addsimps [extend_act_Id, project_act_Id];
    5.61 -
    5.62 -Goal "(extend_act h act = Id) = (act = Id)";
    5.63 -by Auto_tac;
    5.64 -by (rewtac extend_act_def);
    5.65 -by (ALLGOALS (blast_tac (claset() addEs [equalityE])));
    5.66 -qed "extend_act_Id_iff";
    5.67 -
    5.68 -Goal "Id : extend_act h `` Acts F";
    5.69 -by (auto_tac (claset() addSIs [extend_act_Id RS sym], 
    5.70 -	      simpset() addsimps [image_iff]));
    5.71 -qed "Id_mem_extend_act";
    5.72 +Addsimps [extend_act_Id];
    5.73  
    5.74  
    5.75  (**** extend ****)
    5.76 @@ -315,11 +310,10 @@
    5.77  qed "Init_project";
    5.78  
    5.79  Goal "Acts (extend h F) = (extend_act h `` Acts F)";
    5.80 -by (auto_tac (claset() addSIs [extend_act_Id RS sym], 
    5.81 -	      simpset() addsimps [extend_def, image_iff]));
    5.82 +by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1);
    5.83  qed "Acts_extend";
    5.84  
    5.85 -Goal "Acts (project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
    5.86 +Goal "Acts(project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
    5.87  by (auto_tac (claset(), 
    5.88  	      simpset() addsimps [project_def, image_iff]));
    5.89  qed "Acts_project";
    5.90 @@ -341,7 +335,6 @@
    5.91  by (Blast_tac 1);
    5.92  qed "project_set_Union";
    5.93  
    5.94 -
    5.95  Goal "project h C (extend h F) = \
    5.96  \     mk_program (Init F, Restrict (project_set h C) `` Acts F)";
    5.97  by (rtac program_equalityI 1);
    5.98 @@ -378,7 +371,6 @@
    5.99  qed "extend_JN";
   5.100  Addsimps [extend_JN];
   5.101  
   5.102 -
   5.103  (** These monotonicity results look natural but are UNUSED **)
   5.104  
   5.105  Goal "F <= G ==> extend h F <= extend h G";
   5.106 @@ -460,7 +452,45 @@
   5.107  qed "extend_Always";
   5.108  
   5.109  
   5.110 -(** Further lemmas **)
   5.111 +(** Safety and "project" **)
   5.112 +
   5.113 +(** projection: monotonicity for safety **)
   5.114 +
   5.115 +Goal "D <= C ==> \
   5.116 +\     project_act h (Restrict D act) <= project_act h (Restrict C act)";
   5.117 +by (auto_tac (claset(), simpset() addsimps [project_act_def]));
   5.118 +qed "project_act_mono";
   5.119 +
   5.120 +Goal "[| D <= C; project h C F : A co B |] ==> project h D F : A co B";
   5.121 +by (auto_tac (claset(), simpset() addsimps [constrains_def]));
   5.122 +by (dtac project_act_mono 1);
   5.123 +by (Blast_tac 1);
   5.124 +qed "project_constrains_mono";
   5.125 +
   5.126 +Goal "[| D <= C;  project h C F : stable A |] ==> project h D F : stable A";
   5.127 +by (asm_full_simp_tac
   5.128 +    (simpset() addsimps [stable_def, project_constrains_mono]) 1);
   5.129 +qed "project_stable_mono";
   5.130 +
   5.131 +Goalw [constrains_def]
   5.132 +     "(project h C F : A co B)  =  \
   5.133 +\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
   5.134 +by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
   5.135 +by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
   5.136 +(*the <== direction*)
   5.137 +by (rewtac project_act_def);
   5.138 +by (force_tac (claset() addSDs [subsetD], simpset()) 1);
   5.139 +qed "project_constrains";
   5.140 +
   5.141 +Goalw [stable_def]
   5.142 +     "(project h UNIV F : stable A) = (F : stable (extend_set h A))";
   5.143 +by (simp_tac (simpset() addsimps [project_constrains]) 1);
   5.144 +qed "project_stable";
   5.145 +
   5.146 +Goal "F : stable (extend_set h A) ==> project h C F : stable A";
   5.147 +by (dtac (project_stable RS iffD2) 1);
   5.148 +by (blast_tac (claset() addIs [project_stable_mono]) 1);
   5.149 +qed "project_stable_I";
   5.150  
   5.151  Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
   5.152  by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
   5.153 @@ -562,16 +592,84 @@
   5.154  by (etac leadsTo_imp_extend_leadsTo 2);
   5.155  by (dtac extend_leadsTo_slice 1);
   5.156  by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1);
   5.157 -qed "extend_leadsto";
   5.158 +qed "extend_leadsTo";
   5.159  
   5.160  Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) =  \
   5.161  \     (F : A LeadsTo B)";
   5.162  by (simp_tac
   5.163      (simpset() addsimps [LeadsTo_def, reachable_extend_eq, 
   5.164 -			 extend_leadsto, extend_set_Int_distrib RS sym]) 1);
   5.165 +			 extend_leadsTo, extend_set_Int_distrib RS sym]) 1);
   5.166  qed "extend_LeadsTo";
   5.167  
   5.168  
   5.169 +(*** preserves ***)
   5.170 +
   5.171 +Goal "G : preserves (v o f) ==> project h C G : preserves v";
   5.172 +by (auto_tac (claset(),
   5.173 +	      simpset() addsimps [preserves_def, project_stable_I,
   5.174 +				  extend_set_eq_Collect]));
   5.175 +qed "project_preserves_I";
   5.176 +
   5.177 +(*to preserve f is to preserve the whole original state*)
   5.178 +Goal "G : preserves f ==> project h C G : preserves id";
   5.179 +by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
   5.180 +qed "project_preserves_id_I";
   5.181 +
   5.182 +Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
   5.183 +by (auto_tac (claset(),
   5.184 +	      simpset() addsimps [preserves_def, extend_stable RS sym,
   5.185 +				  extend_set_eq_Collect]));
   5.186 +qed "extend_preserves";
   5.187 +
   5.188 +Goal "inj h ==> (extend h G : preserves g)";
   5.189 +by (auto_tac (claset(),
   5.190 +	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
   5.191 +				  stable_def, constrains_def, g_def]));
   5.192 +qed "inj_extend_preserves";
   5.193 +
   5.194 +
   5.195 +(*** Guarantees ***)
   5.196 +
   5.197 +Goal "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)";
   5.198 +by (rtac program_equalityI 1);
   5.199 +by (asm_simp_tac
   5.200 +    (simpset() addsimps [image_eq_UN, UN_Un, project_act_extend_act]) 2);
   5.201 +by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
   5.202 +qed "project_extend_Join";
   5.203 +
   5.204 +Goal "(extend h F) Join G = extend h H ==> H = F Join (project h UNIV G)";
   5.205 +by (dres_inst_tac [("f", "project h UNIV")] arg_cong 1);
   5.206 +by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
   5.207 +qed "extend_Join_eq_extend_D";
   5.208 +
   5.209 +(** Strong precondition and postcondition; only useful when
   5.210 +    the old and new state sets are in bijection **)
   5.211 +
   5.212 +Goal "F : X guarantees[v] Y ==> \
   5.213 +\     extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
   5.214 +by (rtac guaranteesI 1);
   5.215 +by Auto_tac;
   5.216 +by (blast_tac (claset() addIs [project_preserves_I]
   5.217 +			addDs [extend_Join_eq_extend_D, guaranteesD]) 1);
   5.218 +qed "guarantees_imp_extend_guarantees";
   5.219 +
   5.220 +Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
   5.221 +\     ==> F : X guarantees[v] Y";
   5.222 +by (auto_tac (claset(), simpset() addsimps [guar_def]));
   5.223 +by (dres_inst_tac [("x", "extend h G")] spec 1);
   5.224 +by (asm_full_simp_tac 
   5.225 +    (simpset() delsimps [extend_Join] 
   5.226 +           addsimps [extend_Join RS sym, extend_preserves,
   5.227 +		     inj_extend RS inj_image_mem_iff]) 1);
   5.228 +qed "extend_guarantees_imp_guarantees";
   5.229 +
   5.230 +Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
   5.231 +\    (F : X guarantees[v] Y)";
   5.232 +by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
   5.233 +			       extend_guarantees_imp_guarantees]) 1);
   5.234 +qed "extend_guarantees_eq";
   5.235 +
   5.236 +
   5.237  Close_locale "Extend";
   5.238  
   5.239  (*Close_locale should do this!
     6.1 --- a/src/HOL/UNITY/Guar.ML	Wed Feb 16 15:04:12 2000 +0100
     6.2 +++ b/src/HOL/UNITY/Guar.ML	Fri Feb 18 15:20:44 2000 +0100
     6.3 @@ -120,7 +120,7 @@
     6.4  qed "guarantees_UN_left";
     6.5  
     6.6  Goalw [guar_def]
     6.7 -    "(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)";
     6.8 +     "(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)";
     6.9  by (Blast_tac 1);
    6.10  qed "guarantees_Un_left";
    6.11  
    6.12 @@ -130,10 +130,15 @@
    6.13  qed "guarantees_INT_right";
    6.14  
    6.15  Goalw [guar_def]
    6.16 -    "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)";
    6.17 +     "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)";
    6.18  by (Blast_tac 1);
    6.19  qed "guarantees_Int_right";
    6.20  
    6.21 +Goal "[| F : Z guarantees[v] X;  F : Z guarantees[v] Y |] \
    6.22 +\    ==> F : Z guarantees[v] (X Int Y)";
    6.23 +by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
    6.24 +qed "guarantees_Int_right_I";
    6.25 +
    6.26  Goal "(F : X guarantees[v] (INTER I Y)) = \
    6.27  \     (ALL i:I. F : X guarantees[v] (Y i))";
    6.28  by (simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
     7.1 --- a/src/HOL/UNITY/Lift_prog.ML	Wed Feb 16 15:04:12 2000 +0100
     7.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Fri Feb 18 15:20:44 2000 +0100
     7.3 @@ -3,67 +3,87 @@
     7.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.5      Copyright   1998  University of Cambridge
     7.6  
     7.7 -Arrays of processes.  Many results are instances of those in Extend & Project.
     7.8 +Arrays of processes. 
     7.9  *)
    7.10  
    7.11 +Addsimps [insert_map_def, delete_map_def];
    7.12  
    7.13 -(*** Basic properties ***)
    7.14 +Goal "delete_map i (insert_map i x f) = f";
    7.15 +by (rtac ext 1);
    7.16 +by (Simp_tac 1);
    7.17 +qed "insert_map_inverse";
    7.18  
    7.19 -(** lift_set and drop_set **)
    7.20 +Goal "(insert_map i x (delete_map i g)) = g(i:=x)";
    7.21 +by (rtac ext 1);
    7.22 +by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
    7.23 +by (exhaust_tac "d" 1);
    7.24 +by (ALLGOALS Asm_simp_tac);
    7.25 +qed "insert_map_delete_map_eq";
    7.26 +
    7.27 +(*** Injectiveness proof ***)
    7.28  
    7.29 -Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)";
    7.30 -by Auto_tac;
    7.31 -qed "lift_set_iff";
    7.32 -AddIffs [lift_set_iff];
    7.33 +Goal "(insert_map i x f) = (insert_map i y g) ==> x=y";
    7.34 +by (dres_inst_tac [("x","i")] fun_cong 1);
    7.35 +by (Full_simp_tac 1);
    7.36 +qed "insert_map_inject1";
    7.37 +
    7.38 +Goal "(insert_map i x f) = (insert_map i y g) ==> f=g";
    7.39 +by (dres_inst_tac [("f", "delete_map i")] arg_cong 1);
    7.40 +by (full_simp_tac (simpset() addsimps [insert_map_inverse]) 1);
    7.41 +qed "insert_map_inject2";
    7.42  
    7.43 -Goalw [lift_set_def] "lift_set i A Int lift_set i B = lift_set i (A Int B)";
    7.44 +Goal "(insert_map i x f) = (insert_map i y g) ==> x=y & f=g";
    7.45 +by (blast_tac (claset() addDs [insert_map_inject1, insert_map_inject2]) 1);
    7.46 +bind_thm ("insert_map_inject", result() RS conjE);
    7.47 +AddSEs [insert_map_inject];
    7.48 +
    7.49 +(*The general case: we don't assume i=i'*)
    7.50 +Goalw [lift_map_def]
    7.51 +     "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu'))) \
    7.52 +\     = (uu = uu' & insert_map i s f = insert_map i' s' f')"; 
    7.53  by Auto_tac;
    7.54 -qed "Int_lift_set";
    7.55 -
    7.56 -Goalw [lift_set_def] "lift_set i A Un lift_set i B = lift_set i (A Un B)";
    7.57 -by Auto_tac;
    7.58 -qed "Un_lift_set";
    7.59 -
    7.60 -Goalw [lift_set_def] "lift_set i A - lift_set i B = lift_set i (A-B)";
    7.61 -by Auto_tac;
    7.62 -qed "Diff_lift_set";
    7.63 -
    7.64 -Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set];
    7.65 -
    7.66 -(** lift_act and drop_act **)
    7.67 +qed "lift_map_eq_iff";
    7.68 +AddIffs [lift_map_eq_iff];
    7.69  
    7.70 -(*For compatibility with the original definition and perhaps simpler proofs*)
    7.71 -Goalw [lift_act_def]
    7.72 -    "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
    7.73 -by Auto_tac;
    7.74 -by (rtac exI 1);
    7.75 +Goalw [lift_map_def, drop_map_def] "!!s. drop_map i (lift_map i s) = s";
    7.76 +by (force_tac (claset() addIs [insert_map_inverse], simpset()) 1);
    7.77 +qed "drop_map_lift_map_eq";
    7.78 +
    7.79 +Goalw [lift_map_def] "inj (lift_map i)";
    7.80 +by (rtac injI 1);
    7.81  by Auto_tac;
    7.82 -qed "lift_act_eq";
    7.83 -AddIffs [lift_act_eq];
    7.84 +qed "inj_lift_map";
    7.85  
    7.86 -(** lift_prog and drop_prog **)
    7.87 +(*** Surjectiveness proof ***)
    7.88  
    7.89 -Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
    7.90 -by Auto_tac;
    7.91 -qed "Init_lift_prog";
    7.92 -Addsimps [Init_lift_prog];
    7.93 +Goalw [lift_map_def, drop_map_def] "!!s. lift_map i (drop_map i s) = s";
    7.94 +by (force_tac (claset(), simpset() addsimps [insert_map_delete_map_eq]) 1);
    7.95 +qed "lift_map_drop_map_eq";
    7.96  
    7.97 -Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
    7.98 -by (auto_tac (claset() addIs [rev_image_eqI], simpset()));
    7.99 -qed "Acts_lift_prog";
   7.100 -Addsimps [Acts_lift_prog];
   7.101 +Goal "(drop_map i s) = (drop_map i s') ==> s=s'";
   7.102 +by (dres_inst_tac [("f", "lift_map i")] arg_cong 1);
   7.103 +by (full_simp_tac (simpset() addsimps [lift_map_drop_map_eq]) 1);
   7.104 +qed "drop_map_inject";
   7.105 +AddSDs [drop_map_inject];
   7.106 +
   7.107 +Goal "surj (lift_map i)";
   7.108 +by (rtac surjI 1);
   7.109 +by (rtac lift_map_drop_map_eq 1);
   7.110 +qed "surj_lift_map";
   7.111  
   7.112 -Goalw [drop_prog_def] "Init (drop_prog i C F) = drop_set i (Init F)";
   7.113 -by Auto_tac;
   7.114 -qed "Init_drop_prog";
   7.115 -Addsimps [Init_drop_prog];
   7.116 +Goal "bij (lift_map i)";
   7.117 +by (simp_tac (simpset() addsimps [bij_def, inj_lift_map, surj_lift_map]) 1);
   7.118 +qed "bij_lift_map";
   7.119 +AddIffs [bij_lift_map];
   7.120 +
   7.121 +AddIffs [bij_lift_map RS mem_rename_act_iff];
   7.122  
   7.123 -Goal "Acts (drop_prog i C F) = insert Id (drop_act i `` Restrict C `` Acts F)";
   7.124 -by (auto_tac (claset() addIs [image_eqI], 
   7.125 -	      simpset() addsimps [drop_prog_def]));
   7.126 -qed "Acts_drop_prog";
   7.127 -Addsimps [Acts_drop_prog];
   7.128 -
   7.129 +Goal "inv (lift_map i) = drop_map i";
   7.130 +by (rtac inv_equality 1);
   7.131 +by (rtac lift_map_drop_map_eq 2);
   7.132 +by (rtac drop_map_lift_map_eq 1);
   7.133 +qed "inv_lift_map_eq";
   7.134 +Addsimps [inv_lift_map_eq];
   7.135  
   7.136  (*** sub ***)
   7.137  
   7.138 @@ -72,374 +92,293 @@
   7.139  qed "sub_apply";
   7.140  Addsimps [sub_apply];
   7.141  
   7.142 -Goal "lift_set i {s. P s} = {s. P (sub i s)}";
   7.143 -by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
   7.144 -qed "lift_set_sub";
   7.145 -
   7.146 -Goal "{s. P (s i)} = lift_set i {s. P s}";
   7.147 -by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
   7.148 -qed "Collect_eq_lift_set";
   7.149 -
   7.150 -Goal "sub i -`` A = lift_set i A";
   7.151 -by (Force_tac 1);
   7.152 -qed "sub_vimage";
   7.153 -Addsimps [sub_vimage];
   7.154 +Goal "lift_set i {s. P s} = {s. P (drop_map i s)}";
   7.155 +by (rtac set_ext 1);
   7.156 +by (asm_simp_tac (simpset() delsimps [image_Collect]
   7.157 +			    addsimps [lift_set_def, rename_set_eq_Collect]) 1);
   7.158 +qed "lift_set_eq_Collect";
   7.159  
   7.160 -(*For tidying the result of "export"*)
   7.161 -Goal "v o (%z. z i) = v o sub i";
   7.162 -by (simp_tac (simpset() addsimps [sub_def]) 1);
   7.163 -qed "fold_o_sub";
   7.164 -
   7.165 -
   7.166 +Goalw [lift_set_def] "lift_set i {} = {}";
   7.167 +by Auto_tac;
   7.168 +qed "lift_set_empty";
   7.169 +Addsimps [lift_set_empty];
   7.170  
   7.171 -(*** lift_prog and the lattice operations ***)
   7.172 -
   7.173 -Goal "lift_prog i SKIP = SKIP";
   7.174 -by (auto_tac (claset() addSIs [program_equalityI],
   7.175 -	      simpset() addsimps [SKIP_def, lift_prog_def]));
   7.176 -qed "lift_prog_SKIP";
   7.177 +Goalw [lift_set_def] "(lift_map i x : lift_set i A) = (x : A)";
   7.178 +by (rtac (inj_lift_map RS inj_image_mem_iff) 1);
   7.179 +qed "lift_set_iff";
   7.180 +AddIffs [lift_set_iff];
   7.181  
   7.182 -Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)";
   7.183 -by (rtac program_equalityI 1);
   7.184 -by Auto_tac;
   7.185 -qed "lift_prog_Join";
   7.186 -
   7.187 -Goal "lift_prog i (JOIN J F) = (JN j:J. lift_prog i (F j))";
   7.188 -by (rtac program_equalityI 1);
   7.189 -by Auto_tac;
   7.190 -qed "lift_prog_JN";
   7.191 -
   7.192 -
   7.193 -(*** Equivalence with "extend" version ***)
   7.194 +Goal "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)";
   7.195 +by (asm_simp_tac (simpset() addsimps [lift_set_def, 
   7.196 +				      mem_rename_set_iff, drop_map_def]) 1);
   7.197 +qed "lift_set_iff";
   7.198 +AddIffs [lift_set_iff];
   7.199  
   7.200 -Goalw [lift_map_def] "good_map (lift_map i)";
   7.201 -by (rtac good_mapI 1);
   7.202 -by (res_inst_tac [("f", "%f. (f i, f)")] surjI 1);
   7.203 -by Auto_tac;
   7.204 -by (dres_inst_tac [("f", "%f. f i")] arg_cong 1);
   7.205 -by Auto_tac;
   7.206 -qed "good_map_lift_map";
   7.207 +Goalw [lift_set_def] "A<=B ==> lift_set i A <= lift_set i B";
   7.208 +by (etac image_mono 1);
   7.209 +qed "lift_set_mono";
   7.210  
   7.211 -fun lift_export0 th = 
   7.212 -    good_map_lift_map RS export th 
   7.213 -       |> simplify (simpset() addsimps [fold_o_sub]);
   7.214 +Goalw [lift_set_def] "lift_set i (A Un B) = lift_set i A Un lift_set i B";
   7.215 +by (asm_simp_tac (simpset() addsimps [image_Un]) 1);
   7.216 +qed "lift_set_Un_distrib";
   7.217  
   7.218 -Goal "fst (inv (lift_map i) g) = g i";
   7.219 -by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1);
   7.220 -by (auto_tac (claset(), simpset() addsimps [lift_map_def]));
   7.221 -qed "fst_inv_lift_map";
   7.222 -Addsimps [fst_inv_lift_map];
   7.223 +Goalw [lift_set_def] "lift_set i (A-B) = lift_set i A - lift_set i B";
   7.224 +by (rtac (inj_lift_map RS image_set_diff) 1);
   7.225 +qed "lift_set_Diff_distrib";
   7.226  
   7.227  
   7.228 -Goal "lift_set i A = extend_set (lift_map i) A";
   7.229 -by (auto_tac (claset(), 
   7.230 -     simpset() addsimps [lift_export0 mem_extend_set_iff]));
   7.231 -qed "lift_set_correct";
   7.232 -
   7.233 -Goalw [drop_set_def, project_set_def, lift_map_def]
   7.234 -     "drop_set i A = project_set (lift_map i) A";
   7.235 -by Auto_tac;
   7.236 -by (rtac image_eqI 2);
   7.237 -by (rtac exI 1);
   7.238 -by (stac (refl RS fun_upd_idem) 1);
   7.239 -by Auto_tac;
   7.240 -qed "drop_set_correct";
   7.241 -
   7.242 -Goal "lift_act i = extend_act (lift_map i)";
   7.243 -by (rtac ext 1);
   7.244 -by Auto_tac;
   7.245 -by (forward_tac [lift_export0 extend_act_D] 2);
   7.246 -by (auto_tac (claset(), simpset() addsimps [extend_act_def]));
   7.247 -by (auto_tac (claset(), simpset() addsimps [extend_act_def, lift_map_def]));
   7.248 -by (rtac bexI 1);
   7.249 -by (auto_tac (claset() addSIs [exI], simpset()));
   7.250 -qed "lift_act_correct";
   7.251 +(*** the lattice operations ***)
   7.252  
   7.253 -Goal "drop_act i = project_act (lift_map i)";
   7.254 -by (rtac ext 1);
   7.255 -by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]);
   7.256 -by Auto_tac;
   7.257 -by (REPEAT_FIRST (ares_tac [exI, conjI]));
   7.258 -by Auto_tac;
   7.259 -by (REPEAT_FIRST (assume_tac ORELSE' stac (refl RS fun_upd_idem)));
   7.260 -qed "drop_act_correct";
   7.261 -
   7.262 -Goal "lift_prog i = extend (lift_map i)";
   7.263 -by (rtac (program_equalityI RS ext) 1);
   7.264 -by (simp_tac (simpset() addsimps [lift_set_correct]) 1);
   7.265 -by (simp_tac (simpset() 
   7.266 -	      addsimps [lift_export0 Acts_extend, 
   7.267 -			lift_act_correct]) 1);
   7.268 -qed "lift_prog_correct";
   7.269 -
   7.270 -Goal "drop_prog i C = project (lift_map i) C";
   7.271 -by (rtac (program_equalityI RS ext) 1);
   7.272 -by (simp_tac (simpset() addsimps [drop_set_correct]) 1);
   7.273 -by (simp_tac (simpset() 
   7.274 -	      addsimps [Acts_project, drop_act_correct]) 1);
   7.275 -qed "drop_prog_correct";
   7.276 -
   7.277 +Goalw [lift_def] "lift i SKIP = SKIP";
   7.278 +by (Asm_simp_tac 1);
   7.279 +qed "lift_SKIP";
   7.280 +Addsimps [lift_SKIP];
   7.281  
   7.282 -(** Injectivity of lift_set, lift_act, lift_prog **)
   7.283 -
   7.284 -Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F";
   7.285 -by Auto_tac;
   7.286 -qed "lift_set_inverse";
   7.287 -Addsimps [lift_set_inverse];
   7.288 -
   7.289 -Goal "inj (lift_set i)";
   7.290 -by (rtac inj_on_inverseI 1);
   7.291 -by (rtac lift_set_inverse 1);
   7.292 -qed "inj_lift_set";
   7.293 -
   7.294 -(*Because A and B could differ outside i, cannot generalize result to 
   7.295 -   drop_set i (A Int B) = drop_set i A Int drop_set i B
   7.296 -*)
   7.297 -Goalw [lift_set_def, drop_set_def]
   7.298 -     "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)";
   7.299 -by Auto_tac;
   7.300 -qed "drop_set_Int_lift_set";
   7.301 -
   7.302 -Goalw [lift_set_def, drop_set_def]
   7.303 -     "drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A";
   7.304 -by Auto_tac;
   7.305 -qed "drop_set_Int_lift_set2";
   7.306 +Goalw [lift_def] "lift i (F Join G) = lift i F Join lift i G";
   7.307 +by (Asm_simp_tac 1);
   7.308 +qed "lift_Join";
   7.309 +Addsimps [lift_Join];
   7.310  
   7.311 -Goalw [drop_set_def]
   7.312 -     "i : I ==> drop_set i (INT j:I. lift_set j A) = A";
   7.313 -by Auto_tac;
   7.314 -qed "drop_set_INT";
   7.315 -
   7.316 -Goal "lift_set i UNIV = UNIV";
   7.317 -by (simp_tac (simpset() addsimps [lift_set_correct, 
   7.318 -				  lift_export0 extend_set_UNIV_eq]) 1);
   7.319 -qed "lift_set_UNIV_eq";
   7.320 -Addsimps [lift_set_UNIV_eq];
   7.321 -
   7.322 -Goal "inj (lift_prog i)";
   7.323 -by (simp_tac
   7.324 -    (simpset() addsimps [lift_prog_correct, lift_export0 inj_extend]) 1);
   7.325 -qed "inj_lift_prog";
   7.326 -
   7.327 -
   7.328 -(*** More Lemmas ***)
   7.329 -
   7.330 -Goal "lift_act i act ^^ lift_set i A = lift_set i (act^^A)";
   7.331 -by (asm_simp_tac (simpset() addsimps [lift_set_correct, lift_act_correct,
   7.332 -				      lift_export0 extend_act_Image]) 1);
   7.333 -qed "lift_act_Image";
   7.334 -Addsimps [lift_act_Image];
   7.335 -
   7.336 -
   7.337 +Goalw [lift_def] "lift j (JOIN I F) = (JN i:I. lift j (F i))";
   7.338 +by (Asm_simp_tac 1);
   7.339 +qed "lift_JN";
   7.340 +Addsimps [lift_JN];
   7.341  
   7.342  (*** Safety: co, stable, invariant ***)
   7.343  
   7.344 -(** Safety and lift_prog **)
   7.345 -
   7.346 -Goal "(lift_prog i F : (lift_set i A) co (lift_set i B))  =  \
   7.347 -\     (F : A co B)";
   7.348 -by (auto_tac (claset(), 
   7.349 -	      simpset() addsimps [constrains_def]));
   7.350 -by (Force_tac 1);
   7.351 -qed "lift_prog_constrains";
   7.352 -
   7.353 -Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)";
   7.354 -by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains]) 1);
   7.355 -qed "lift_prog_stable";
   7.356 -
   7.357 -Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)";
   7.358 -by (auto_tac (claset(),
   7.359 -	      simpset() addsimps [invariant_def, lift_prog_stable]));
   7.360 -qed "lift_prog_invariant";
   7.361 -
   7.362 -Goal "[| lift_prog i F : A co B |] \
   7.363 -\     ==> F : (drop_set i A) co (drop_set i B)";
   7.364 -by (asm_full_simp_tac
   7.365 -    (simpset() addsimps [drop_set_correct, lift_prog_correct, 
   7.366 -			 lift_export0 extend_constrains_project_set]) 1);
   7.367 -qed "lift_prog_constrains_drop_set";
   7.368 +Goalw [lift_def, lift_set_def]
   7.369 +     "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)";
   7.370 +by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1);
   7.371 +qed "lift_constrains";
   7.372  
   7.373 -(*This one looks strange!  Proof probably is by case analysis on i=j.
   7.374 -  If i~=j then lift_prog j (F j) does nothing to lift_set i, and the 
   7.375 -  premise ensures A<=B.*)
   7.376 -Goal "F i : A co B  \
   7.377 -\     ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)";
   7.378 -by (auto_tac (claset(), 
   7.379 -	      simpset() addsimps [constrains_def]));
   7.380 -by (REPEAT (Blast_tac 1));
   7.381 -qed "constrains_imp_lift_prog_constrains";
   7.382 -
   7.383 +Goalw [lift_def, lift_set_def]
   7.384 +     "(lift i F : stable (lift_set i A)) = (F : stable A)";
   7.385 +by (asm_simp_tac (simpset() addsimps [rename_stable]) 1);
   7.386 +qed "lift_stable";
   7.387  
   7.388 -(** Safety and drop_prog **)
   7.389 -
   7.390 -Goal "(drop_prog i C F : A co B)  =  \
   7.391 -\     (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
   7.392 -by (simp_tac
   7.393 -    (simpset() addsimps [drop_prog_correct, lift_set_correct, 
   7.394 -			 lift_export0 project_constrains]) 1);
   7.395 -qed "drop_prog_constrains";
   7.396 -
   7.397 -Goal "(drop_prog i UNIV F : stable A)  =  (F : stable (lift_set i A))";
   7.398 -by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1);
   7.399 -qed "drop_prog_stable";
   7.400 -
   7.401 +Goalw [lift_def, lift_set_def]
   7.402 +     "(lift i F : invariant (lift_set i A)) = (F : invariant A)";
   7.403 +by (asm_simp_tac (simpset() addsimps [rename_invariant]) 1);
   7.404 +qed "lift_invariant";
   7.405  
   7.406 -(*** Weak safety primitives: Co, Stable ***)
   7.407 -
   7.408 -(** Reachability **)
   7.409 -
   7.410 -Goal "reachable (lift_prog i F) = lift_set i (reachable F)";
   7.411 -by (simp_tac
   7.412 -    (simpset() addsimps [lift_prog_correct, lift_set_correct, 
   7.413 -			 lift_export0 reachable_extend_eq]) 1);
   7.414 -qed "reachable_lift_prog";
   7.415 -
   7.416 -Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B))  =  \
   7.417 -\     (F : A Co B)";
   7.418 -by (simp_tac
   7.419 -    (simpset() addsimps [lift_prog_correct, lift_set_correct, 
   7.420 -			 lift_export0 extend_Constrains]) 1);
   7.421 -qed "lift_prog_Constrains";
   7.422 -
   7.423 -Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
   7.424 -by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1);
   7.425 -qed "lift_prog_Stable";
   7.426 +Goalw [lift_def, lift_set_def]
   7.427 +     "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)";
   7.428 +by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1);
   7.429 +qed "lift_Constrains";
   7.430  
   7.431 -Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : A Co B  \
   7.432 -\     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
   7.433 -by (asm_full_simp_tac
   7.434 -    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   7.435 -		     lift_set_correct, lift_export0 project_Constrains_D]) 1);
   7.436 -qed "drop_prog_Constrains_D";
   7.437 -
   7.438 -Goalw [Stable_def]
   7.439 -     "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Stable A  \
   7.440 -\     ==> lift_prog i F Join G : Stable (lift_set i A)";
   7.441 -by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
   7.442 -qed "drop_prog_Stable_D";
   7.443 +Goalw [lift_def, lift_set_def]
   7.444 +     "(lift i F : Stable (lift_set i A)) = (F : Stable A)";
   7.445 +by (asm_simp_tac (simpset() addsimps [rename_Stable]) 1);
   7.446 +qed "lift_Stable";
   7.447  
   7.448 -Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Always A  \
   7.449 -\     ==> lift_prog i F Join G : Always (lift_set i A)";
   7.450 -by (asm_full_simp_tac
   7.451 -    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
   7.452 -		     lift_set_correct, lift_export0 project_Always_D]) 1);
   7.453 -qed "drop_prog_Always_D";
   7.454 -
   7.455 -Goalw [Increasing_def]
   7.456 - "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Increasing func \
   7.457 -\ ==> lift_prog i F Join G : Increasing (func o (sub i))";
   7.458 -by Auto_tac;
   7.459 -by (stac Collect_eq_lift_set 1);
   7.460 -by (asm_simp_tac (simpset() addsimps [drop_prog_Stable_D]) 1); 
   7.461 -qed "project_Increasing_D";
   7.462 -
   7.463 +Goalw [lift_def, lift_set_def]
   7.464 +     "(lift i F : Always (lift_set i A)) = (F : Always A)";
   7.465 +by (asm_simp_tac (simpset() addsimps [rename_Always]) 1);
   7.466 +qed "lift_Always";
   7.467  
   7.468  (*** Progress: transient, ensures ***)
   7.469  
   7.470 -Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)";
   7.471 -by (simp_tac (simpset() addsimps [lift_set_correct, lift_prog_correct,
   7.472 -			  lift_export0 extend_transient]) 1);
   7.473 -qed "lift_prog_transient";
   7.474 +Goalw [lift_def, lift_set_def]
   7.475 +     "(lift i F : transient (lift_set i A)) = (F : transient A)";
   7.476 +by (asm_simp_tac (simpset() addsimps [rename_transient]) 1);
   7.477 +qed "lift_transient";
   7.478 +
   7.479 +Goalw [lift_def, lift_set_def]
   7.480 +     "(lift i F : (lift_set i A) ensures (lift_set i B)) = \
   7.481 +\     (F : A ensures B)";
   7.482 +by (asm_simp_tac (simpset() addsimps [rename_ensures]) 1);
   7.483 +qed "lift_ensures";
   7.484 +
   7.485 +Goalw [lift_def, lift_set_def]
   7.486 +     "(lift i F : (lift_set i A) leadsTo (lift_set i B)) = \
   7.487 +\     (F : A leadsTo B)";
   7.488 +by (asm_simp_tac (simpset() addsimps [rename_leadsTo]) 1);
   7.489 +qed "lift_leadsTo";
   7.490  
   7.491 -Goal "(lift_prog i F : transient (lift_set j A)) = \
   7.492 -\     (i=j & F : transient A | A={})";
   7.493 -by (case_tac "i=j" 1);
   7.494 -by (auto_tac (claset(), simpset() addsimps [lift_prog_transient]));
   7.495 -by (auto_tac (claset(), simpset() addsimps [lift_prog_def, transient_def]));
   7.496 -by (Force_tac 1);
   7.497 -qed "lift_prog_transient_eq_disj";
   7.498 +Goalw [lift_def, lift_set_def]
   7.499 +     "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) =  \
   7.500 +\     (F : A LeadsTo B)";
   7.501 +by (asm_simp_tac (simpset() addsimps [rename_LeadsTo]) 1);
   7.502 +qed "lift_LeadsTo";
   7.503 +
   7.504 +
   7.505 +(** guarantees **)
   7.506 +
   7.507 +Goalw [lift_def]
   7.508 +     "(lift i F : (lift i `` X) guarantees[v o drop_map i] (lift i `` Y)) = \
   7.509 +\     (F : X guarantees[v] Y)";
   7.510 +by (stac (bij_lift_map RS rename_rename_guarantees_eq RS sym) 1);
   7.511 +by (asm_simp_tac (simpset() addsimps [o_def]) 1);
   7.512 +qed "lift_lift_guarantees_eq";
   7.513 +
   7.514 +Goal "(lift i F : X guarantees[v] Y) = \
   7.515 +\     (F : (rename (drop_map i) `` X) guarantees[v o lift_map i] \
   7.516 +\          (rename (drop_map i) `` Y))";
   7.517 +by (asm_simp_tac 
   7.518 +    (simpset() addsimps [bij_lift_map RS rename_guarantees_eq_rename_inv,
   7.519 +			 lift_def]) 1);
   7.520 +qed "lift_guarantees_eq_lift_inv";
   7.521  
   7.522  
   7.523 -(*** guarantees properties ***)
   7.524 +(*To preserve snd means that the second component is there just to allow
   7.525 +  guarantees properties to be stated.  Converse fails, for lift i F can 
   7.526 +  change function components other than i*)
   7.527 +Goal "F : preserves snd ==> lift i F : preserves snd";
   7.528 +by (dres_inst_tac [("w1", "snd")] (impOfSubs subset_preserves_o) 1);
   7.529 +by (asm_simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1);
   7.530 +by (full_simp_tac (simpset() addsimps [lift_map_def, o_def, split_def]) 1);
   7.531 +qed "lift_preserves_snd_I";
   7.532 +
   7.533 +Goal "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)";
   7.534 +by (dres_inst_tac [("f", "insert_map i (g i)")] arg_cong 1);
   7.535 +by (full_simp_tac (simpset() addsimps [insert_map_delete_map_eq]) 1);
   7.536 +by (etac exI 1);
   7.537 +bind_thm ("delete_map_eqE", result() RS exE);
   7.538 +AddSEs [delete_map_eqE];
   7.539  
   7.540 -Goal "lift_prog i F : preserves (v o sub j) = \
   7.541 -\     (if i=j then F : preserves v else True)";
   7.542 -by (simp_tac (simpset() addsimps [lift_prog_correct,
   7.543 -				  lift_export0 extend_preserves]) 1);
   7.544 +Goal "[| delete_map j g = delete_map j g';  i~=j |] ==> g i = g' i";
   7.545 +by (Force_tac 1);
   7.546 +qed "delete_map_neq_apply";
   7.547 +
   7.548 +(*A set of the form (A Times UNIV) ignores the second (dummy) state component*)
   7.549 +
   7.550 +Goal "(f o fst) -`` A = (f-``A) Times UNIV";
   7.551 +by Auto_tac;
   7.552 +qed "vimage_o_fst_eq";
   7.553 +
   7.554 +Goal "(sub i -``A) Times UNIV = lift_set i (A Times UNIV)";
   7.555 +by Auto_tac;
   7.556 +qed "vimage_sub_eq_lift_set";
   7.557 +
   7.558 +Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set];
   7.559 +
   7.560 +Goal "[| F : preserves snd;  i~=j |] \
   7.561 +\     ==> lift j F : stable (lift_set i (A Times UNIV))";
   7.562  by (auto_tac (claset(),
   7.563 -	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
   7.564 -				  stable_def, constrains_def, lift_map_def]));
   7.565 -qed "lift_prog_preserves_sub";
   7.566 -
   7.567 -Addsimps [lift_prog_preserves_sub];
   7.568 +	      simpset() addsimps [lift_def, lift_set_def, 
   7.569 +				  stable_def, constrains_def, 
   7.570 +				  mem_rename_act_iff, mem_rename_set_iff]));
   7.571 +by (auto_tac (claset() addSDs [preserves_imp_eq],
   7.572 +	      simpset() addsimps [lift_map_def, drop_map_def]));
   7.573 +by (dres_inst_tac [("x", "i")] fun_cong 1);
   7.574 +by Auto_tac;
   7.575 +qed "preserves_snd_lift_stable";
   7.576  
   7.577 -Goal "G : preserves (v o sub i) ==> drop_prog i C G : preserves v";
   7.578 -by (asm_simp_tac
   7.579 -    (simpset() addsimps [drop_prog_correct, fold_o_sub,
   7.580 -			 lift_export0 project_preserves_I]) 1);
   7.581 -qed "drop_prog_preserves_I";
   7.582 +(*If i~=j then lift j F  does nothing to lift_set i, and the 
   7.583 +  premise ensures A<=B.*)
   7.584 +Goal "[| F i : (A Times UNIV) co (B Times UNIV);  \
   7.585 +\        F j : preserves snd |]  \
   7.586 +\  ==> lift j (F j) : (lift_set i (A Times UNIV)) co (lift_set i (B Times UNIV))";
   7.587 +by (case_tac "i=j" 1);
   7.588 +by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def, 
   7.589 +					   rename_constrains]) 1);
   7.590 +by (etac (preserves_snd_lift_stable RS stableD RS constrains_weaken_R) 1);
   7.591 +by (assume_tac 1);
   7.592 +by (etac (constrains_imp_subset RS lift_set_mono) 1);
   7.593 +qed "constrains_imp_lift_constrains";
   7.594 +
   7.595 +(** Lemmas for the transient theorem **)
   7.596 +
   7.597 +Goal "(insert_map i t f)(i := s) = insert_map i s f";
   7.598 +by (rtac ext 1);
   7.599 +by Auto_tac;
   7.600 +qed "insert_map_upd_same";
   7.601  
   7.602 -(*The raw version*)
   7.603 -val [xguary,drop_prog,lift_prog] =
   7.604 -Goal "[| F : X guarantees[v] Y;  \
   7.605 -\        !!G. lift_prog i F Join G : X' ==> F Join drop_prog i (C G) G : X;  \
   7.606 -\        !!G. [| F Join drop_prog i (C G) G : Y; lift_prog i F Join G : X'; \
   7.607 -\                G : preserves (v o sub i) |] \
   7.608 -\             ==> lift_prog i F Join G : Y' |] \
   7.609 -\     ==> lift_prog i F : X' guarantees[v o sub i] Y'";
   7.610 -by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
   7.611 -by (etac drop_prog_preserves_I 1);
   7.612 -by (etac drop_prog 1);
   7.613 +Goal "(insert_map j t f)(i := s) = \
   7.614 +\     (if i=j then insert_map i s f \
   7.615 +\      else if i<j then insert_map j t (f(i:=s)) \
   7.616 +\      else insert_map j t (f(i-1:=s)))";
   7.617 +by (rtac ext 1);
   7.618 +by (auto_tac (claset(), simpset() addsplits [nat_diff_split']));
   7.619 +by (ALLGOALS arith_tac);
   7.620 +qed "insert_map_upd";
   7.621 +
   7.622 +Goal "[| insert_map i s f = insert_map j t g;  i~=j |] \
   7.623 +\     ==> EX g'. insert_map i s' f = insert_map j t g'";
   7.624 +by (stac (insert_map_upd_same RS sym) 1);
   7.625 +by (etac ssubst 1);
   7.626 +by (asm_simp_tac (HOL_ss addsimps [insert_map_upd]) 1);
   7.627 +by (Blast_tac 1);
   7.628 +qed "insert_map_eq_diff";
   7.629 +
   7.630 +Goalw [lift_map_def]
   7.631 +     "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv));  i~=j |] \
   7.632 +\     ==> EX g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))";
   7.633 +by Auto_tac;
   7.634 +by (blast_tac (claset() addDs [insert_map_eq_diff]) 1);
   7.635 +qed "lift_map_eq_diff";
   7.636 +
   7.637 +Goal "F : preserves snd \
   7.638 +\     ==> (lift i F : transient (lift_set j (A Times UNIV))) = \
   7.639 +\         (i=j & F : transient (A Times UNIV) | A={})";
   7.640 +by (case_tac "i=j" 1);
   7.641 +by (auto_tac (claset(), simpset() addsimps [lift_transient]));
   7.642 +by (auto_tac (claset(),
   7.643 +	      simpset() addsimps [lift_def, transient_def,
   7.644 +				  Domain_rename_act]));
   7.645 +by (dtac subsetD 1);
   7.646 +by (Blast_tac 1);
   7.647  by Auto_tac;
   7.648 -qed "drop_prog_guarantees_raw";
   7.649 +ren "s f uu s' f' uu'" 1;
   7.650 +by (subgoal_tac "f'=f & uu'=uu" 1);
   7.651 +by (force_tac (claset() addSDs [preserves_imp_eq], simpset()) 2);
   7.652 +by Auto_tac;
   7.653 +by (dtac sym 1);
   7.654 +by (dtac subsetD 1);
   7.655 +by (rtac ImageI 1);
   7.656 +by (etac rename_actI 1);
   7.657 +by (force_tac (claset(), simpset() addsimps [lift_set_def]) 1);
   7.658 +by (etac (lift_map_eq_diff RS exE) 1);
   7.659 +by (assume_tac 1);
   7.660 +by (dtac ComplD 1);
   7.661 +by (etac notE 1 THEN etac ssubst 1 THEN Fast_tac 1);
   7.662 +qed "lift_transient_eq_disj";
   7.663  
   7.664 -Goal "[| F : X guarantees[v] Y;  \
   7.665 -\        projecting  C (lift_map i) F X' X;  \
   7.666 -\        extending w C (lift_map i) F Y' Y; \
   7.667 -\        preserves w <= preserves (v o sub i) |] \
   7.668 -\     ==> lift_prog i F : X' guarantees[w] Y'";
   7.669 -by (asm_simp_tac
   7.670 -    (simpset() addsimps [lift_prog_correct, fold_o_sub,
   7.671 -			 lift_export0 project_guarantees]) 1);
   7.672 -qed "drop_prog_guarantees";
   7.673 +(*USELESS??*)
   7.674 +Goal "lift_map i `` (A Times UNIV) = \
   7.675 +\     (UN s:A. UN f. {insert_map i s f}) Times UNIV";
   7.676 +by (auto_tac (claset() addSIs [bexI, image_eqI],
   7.677 +              simpset() addsimps [lift_map_def]));
   7.678 +by (rtac (split RS sym) 1);
   7.679 +qed "lift_map_image_Times";
   7.680 +
   7.681 +Goal "(lift i F : preserves v) = (F : preserves (v o lift_map i))";
   7.682 +by (simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1);
   7.683 +qed "lift_preserves_eq";
   7.684 +
   7.685 +Goal "F : preserves snd \
   7.686 +\     ==> lift i F : preserves (v o sub j o fst) = \
   7.687 +\         (if i=j then F : preserves (v o fst) else True)";
   7.688 +by (dtac (impOfSubs subset_preserves_o) 1);
   7.689 +by (full_simp_tac (simpset() addsimps [lift_preserves_eq, o_def,
   7.690 +				       drop_map_lift_map_eq]) 1);
   7.691 +by (asm_simp_tac (simpset() delcongs [if_weak_cong]
   7.692 +			    addsimps [lift_map_def, 
   7.693 +				      eq_commute, split_def, o_def]) 1);
   7.694 +by Auto_tac;
   7.695 +qed "lift_preserves_sub";
   7.696  
   7.697  
   7.698 -(** Are these two useful?? **)
   7.699  
   7.700 -(*The other direction fails: having FF : Stable {s. z <= f (s i)} does not
   7.701 -  ensure that F has the form lift_prog i F for some F.*)
   7.702 -Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}";
   7.703 -by Auto_tac;
   7.704 -by (stac Collect_eq_lift_set 1); 
   7.705 -by (asm_simp_tac (simpset() addsimps [lift_prog_Stable]) 1);
   7.706 -qed "image_lift_prog_Stable";
   7.707 -
   7.708 -Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)";
   7.709 -by (simp_tac (simpset() addsimps [Increasing_def,
   7.710 -				  inj_lift_prog RS image_INT]) 1);
   7.711 -by (blast_tac (claset() addIs [impOfSubs image_lift_prog_Stable]) 1);
   7.712 -qed "image_lift_prog_Increasing";
   7.713 -
   7.714 -
   7.715 -(*** guarantees corollaries ***)
   7.716 +(*** guarantees corollaries [NOT USED]
   7.717  
   7.718  Goal "F : UNIV guarantees[v] increasing func \
   7.719 -\   ==> lift_prog i F : UNIV guarantees[v o sub i] increasing (func o sub i)";
   7.720 +\   ==> lift i F : UNIV guarantees[v o sub i] increasing (func o sub i)";
   7.721  by (dtac (lift_export0 extend_guar_increasing) 1);
   7.722 -by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   7.723 -qed "lift_prog_guar_increasing";
   7.724 +by (asm_full_simp_tac (simpset() addsimps [lift_correct, o_def]) 1);
   7.725 +qed "lift_guar_increasing";
   7.726  
   7.727  Goal "F : UNIV guarantees[v] Increasing func \
   7.728 -\   ==> lift_prog i F : UNIV guarantees[v o sub i] Increasing (func o sub i)";
   7.729 +\   ==> lift i F : UNIV guarantees[v o sub i] Increasing (func o sub i)";
   7.730  by (dtac (lift_export0 extend_guar_Increasing) 1);
   7.731 -by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
   7.732 -qed "lift_prog_guar_Increasing";
   7.733 +by (asm_full_simp_tac (simpset() addsimps [lift_correct, o_def]) 1);
   7.734 +qed "lift_guar_Increasing";
   7.735  
   7.736  Goal "F : Always A guarantees[v] Always B \
   7.737 -\ ==> lift_prog i F : \
   7.738 +\ ==> lift i F : \
   7.739  \       Always(lift_set i A) guarantees[v o sub i] Always (lift_set i B)";
   7.740  by (asm_simp_tac
   7.741 -    (simpset() addsimps [lift_set_correct, lift_prog_correct, 
   7.742 +    (simpset() addsimps [lift_set_correct, lift_correct, 
   7.743  			 lift_export0 extend_guar_Always]) 1);
   7.744 -qed "lift_prog_guar_Always";
   7.745 -
   7.746 -(*version for outside use*)
   7.747 -fun lift_export th = 
   7.748 -    good_map_lift_map RS export th 
   7.749 -       |> simplify
   7.750 -             (simpset() addsimps [fold_o_sub, 
   7.751 -				  drop_set_correct RS sym, 
   7.752 -				  lift_set_correct RS sym, 
   7.753 -				  drop_prog_correct RS sym, 
   7.754 -				  lift_prog_correct RS sym]);;
   7.755 -
   7.756 +qed "lift_guar_Always";
   7.757 +***)
     8.1 --- a/src/HOL/UNITY/Lift_prog.thy	Wed Feb 16 15:04:12 2000 +0100
     8.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Fri Feb 18 15:20:44 2000 +0100
     8.3 @@ -6,35 +6,29 @@
     8.4  lift_prog, etc: replication of components
     8.5  *)
     8.6  
     8.7 -Lift_prog = Project +
     8.8 +Lift_prog = Rename +
     8.9  
    8.10  constdefs
    8.11  
    8.12 -  lift_map :: "['a, 'b * ('a => 'b)] => ('a => 'b)"
    8.13 -    "lift_map i == %(s,f). f(i := s)"
    8.14 -
    8.15 -  lift_set :: "['a, 'b set] => ('a => 'b) set"
    8.16 -    "lift_set i A == {f. f i : A}"
    8.17 +  insert_map :: "[nat, 'b, nat=>'b] => (nat=>'b)"
    8.18 +    "insert_map i z f k == if k<i then f k
    8.19 +                           else if k=i then z
    8.20 +                           else f(k-1)"
    8.21  
    8.22 -  drop_set :: "['a, ('a=>'b) set] => 'b set"
    8.23 -    "drop_set i A == (%f. f i) `` A"
    8.24 -
    8.25 -  lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
    8.26 -    "lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}"
    8.27 +  delete_map :: "[nat, nat=>'b] => (nat=>'b)"
    8.28 +    "delete_map i g k == if k<i then g k else g (Suc k)"
    8.29  
    8.30 -  drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
    8.31 -    "drop_act i act == {(f i, f' i) | f f'. (f,f'): act}"
    8.32 +  lift_map :: "[nat, 'b * ((nat=>'b) * 'c)] => (nat=>'b) * 'c"
    8.33 +    "lift_map i == %(s,(f,uu)). (insert_map i s f, uu)"
    8.34 +
    8.35 +  drop_map :: "[nat, (nat=>'b) * 'c] => 'b * ((nat=>'b) * 'c)"
    8.36 +    "drop_map i == %(g, uu). (g i, (delete_map i g, uu))"
    8.37  
    8.38 -  lift_prog :: "['a, 'b program] => ('a => 'b) program"
    8.39 -    "lift_prog i F ==
    8.40 -       mk_program (lift_set i (Init F),
    8.41 -		   lift_act i `` Acts F)"
    8.42 +  lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set"
    8.43 +    "lift_set i A == lift_map i `` A"
    8.44  
    8.45 -  (*Argument C allows weak safety laws to be projected*)
    8.46 -  drop_prog :: "['a, ('a=>'b) set, ('a=>'b) program] => 'b program"
    8.47 -    "drop_prog i C F ==
    8.48 -       mk_program (drop_set i (Init F),
    8.49 -		   drop_act i `` Restrict C `` (Acts F))"
    8.50 +  lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program"
    8.51 +    "lift i == rename (lift_map i)"
    8.52  
    8.53    (*simplifies the expression of specifications*)
    8.54    constdefs
     9.1 --- a/src/HOL/UNITY/PPROD.ML	Wed Feb 16 15:04:12 2000 +0100
     9.2 +++ b/src/HOL/UNITY/PPROD.ML	Fri Feb 18 15:20:44 2000 +0100
     9.3 @@ -6,24 +6,20 @@
     9.4  Abstraction over replicated components (PLam)
     9.5  General products of programs (Pi operation)
     9.6  
     9.7 -Probably some dead wood here!
     9.8 +Some dead wood here!
     9.9  *)
    9.10  
    9.11 -
    9.12 -val image_eqI' = read_instantiate_sg (sign_of thy)
    9.13 -                     [("x", "?ff(i := ?u)")] image_eqI;
    9.14 -
    9.15  (*** Basic properties ***)
    9.16  
    9.17 -Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
    9.18 -by Auto_tac;
    9.19 +Goal "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
    9.20 +by (simp_tac (simpset() addsimps [PLam_def, lift_def, lift_set_def]) 1);
    9.21  qed "Init_PLam";
    9.22  
    9.23 -Goal "Acts (PLam I F) = insert Id (UN i:I. lift_act i `` Acts (F i))";
    9.24 -by (auto_tac (claset(),
    9.25 -	      simpset() addsimps [PLam_def]));
    9.26 +(*The "insert Id" is needed if I={}, since otherwise the RHS would be {} too*)
    9.27 +Goal "Acts (PLam I F) = \
    9.28 +\     insert Id (UN i:I. rename_act (lift_map i) `` Acts (F i))";
    9.29 +by (simp_tac (simpset() addsimps [PLam_def, lift_def]) 1);
    9.30  qed "Acts_PLam";
    9.31 -
    9.32  Addsimps [Init_PLam, Acts_PLam];
    9.33  
    9.34  Goal "PLam {} F = SKIP";
    9.35 @@ -31,21 +27,20 @@
    9.36  qed "PLam_empty";
    9.37  
    9.38  Goal "(plam i: I. SKIP) = SKIP";
    9.39 -by (simp_tac (simpset() addsimps [PLam_def,lift_prog_SKIP,JN_constant]) 1);
    9.40 +by (simp_tac (simpset() addsimps [PLam_def,lift_SKIP,JN_constant]) 1);
    9.41  qed "PLam_SKIP";
    9.42  
    9.43  Addsimps [PLam_SKIP, PLam_empty];
    9.44  
    9.45 -Goalw [PLam_def]
    9.46 -    "PLam (insert i I) F = (lift_prog i (F i)) Join (PLam I F)";
    9.47 +Goalw [PLam_def] "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)";
    9.48  by Auto_tac;
    9.49  qed "PLam_insert";
    9.50  
    9.51 -Goal "((PLam I F) <= H) = (ALL i: I. lift_prog i (F i) <= H)";
    9.52 +Goal "((PLam I F) <= H) = (ALL i: I. lift i (F i) <= H)";
    9.53  by (simp_tac (simpset() addsimps [PLam_def, JN_component_iff]) 1);
    9.54  qed "PLam_component_iff";
    9.55  
    9.56 -Goalw [PLam_def] "i : I ==> lift_prog i (F i) <= (PLam I F)";
    9.57 +Goalw [PLam_def] "i : I ==> lift i (F i) <= (PLam I F)";
    9.58  (*blast_tac doesn't use HO unification*)
    9.59  by (fast_tac (claset() addIs [component_JN]) 1);
    9.60  qed "component_PLam";
    9.61 @@ -53,240 +48,223 @@
    9.62  
    9.63  (** Safety & Progress **)
    9.64  
    9.65 -Goal "i : I ==>  \
    9.66 -\     (PLam I F : (lift_set i A) co (lift_set i B))  =  \
    9.67 -\     (F i : A co B)";
    9.68 -by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains]) 1);
    9.69 -by (blast_tac (claset() addIs [lift_prog_constrains RS iffD1, 
    9.70 -			       constrains_imp_lift_prog_constrains]) 1);
    9.71 +Goal "[| i : I;  ALL j. F j : preserves snd |] ==>  \
    9.72 +\     (PLam I F : (lift_set i (A Times UNIV)) co \
    9.73 +\                 (lift_set i (B Times UNIV)))  =  \
    9.74 +\     (F i : (A Times UNIV) co (B Times UNIV))";
    9.75 +by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains,
    9.76 +				      Join_constrains]) 1);
    9.77 +by (stac (insert_Diff RS sym) 1 THEN assume_tac 1);
    9.78 +by (asm_simp_tac (simpset() addsimps [lift_constrains]) 1);
    9.79 +by (blast_tac (claset() addIs [constrains_imp_lift_constrains]) 1);
    9.80  qed "PLam_constrains";
    9.81  
    9.82 -Goal "i : I ==> (PLam I F : stable (lift_set i A)) = (F i : stable A)";
    9.83 +Goal "[| i : I;  ALL j. F j : preserves snd |]  \
    9.84 +\     ==> (PLam I F : stable (lift_set i (A Times UNIV))) = \
    9.85 +\         (F i : stable (A Times UNIV))";
    9.86  by (asm_simp_tac (simpset() addsimps [stable_def, PLam_constrains]) 1);
    9.87  qed "PLam_stable";
    9.88  
    9.89  Goal "i : I ==> \
    9.90 -\   PLam I F : transient A = (EX i:I. lift_prog i (F i) : transient A)";
    9.91 +\   PLam I F : transient A = (EX i:I. lift i (F i) : transient A)";
    9.92  by (asm_simp_tac (simpset() addsimps [JN_transient, PLam_def]) 1);
    9.93  qed "PLam_transient";
    9.94  
    9.95  Addsimps [PLam_constrains, PLam_stable, PLam_transient];
    9.96  
    9.97 -Goal "[| i : I;  F i : A ensures B |] ==>  \
    9.98 -\     PLam I F : (lift_set i A) ensures lift_set i B";
    9.99 +(*This holds because the F j cannot change (lift_set i)*)
   9.100 +Goal "[| i : I;  F i : (A Times UNIV) ensures (B Times UNIV);  \
   9.101 +\        ALL j. F j : preserves snd |] ==>  \
   9.102 +\     PLam I F : lift_set i (A Times UNIV) ensures lift_set i (B Times UNIV)";
   9.103  by (auto_tac (claset(), 
   9.104 -	      simpset() addsimps [ensures_def, lift_prog_transient_eq_disj]));
   9.105 +	      simpset() addsimps [ensures_def, lift_transient_eq_disj,
   9.106 +				  lift_set_Un_distrib RS sym,
   9.107 +				  lift_set_Diff_distrib RS sym,
   9.108 +				  Times_Un_distrib1 RS sym,
   9.109 +				  Times_Diff_distrib1 RS sym]));
   9.110  qed "PLam_ensures";
   9.111  
   9.112 -Goal "[| i : I;  F i : (A-B) co (A Un B);  F i : transient (A-B) |] ==>  \
   9.113 -\     PLam I F : (lift_set i A) leadsTo lift_set i B";
   9.114 +Goal "[| i : I;  \
   9.115 +\        F i : ((A Times UNIV) - (B Times UNIV)) co \
   9.116 +\              ((A Times UNIV) Un (B Times UNIV));  \
   9.117 +\        F i : transient ((A Times UNIV) - (B Times UNIV));  \
   9.118 +\        ALL j. F j : preserves snd |] ==>  \
   9.119 +\     PLam I F : lift_set i (A Times UNIV) leadsTo lift_set i (B Times UNIV)";
   9.120  by (rtac (PLam_ensures RS leadsTo_Basis) 1);
   9.121  by (rtac ensuresI 2);
   9.122  by (ALLGOALS assume_tac);
   9.123  qed "PLam_leadsTo_Basis";
   9.124  
   9.125 -Goal "[| PLam I F : AA co BB;  i: I |] \
   9.126 -\     ==> F i : (drop_set i AA) co (drop_set i BB)";
   9.127 -by (rtac lift_prog_constrains_drop_set 1);
   9.128 -(*rotate this assumption to be last*)
   9.129 -by (dres_inst_tac [("psi", "PLam I F : ?C")] asm_rl 1);
   9.130 -by (asm_full_simp_tac (simpset() addsimps [PLam_def, JN_constrains]) 1);
   9.131 -qed "PLam_constrains_drop_set";
   9.132 -
   9.133  
   9.134  (** invariant **)
   9.135  
   9.136 -Goal "[| F i : invariant A;  i : I |] \
   9.137 -\     ==> PLam I F : invariant (lift_set i A)";
   9.138 +Goal "[| F i : invariant (A Times UNIV);  i : I;  \
   9.139 +\        ALL j. F j : preserves snd |] \
   9.140 +\     ==> PLam I F : invariant (lift_set i (A Times UNIV))";
   9.141  by (auto_tac (claset(),
   9.142  	      simpset() addsimps [invariant_def]));
   9.143  qed "invariant_imp_PLam_invariant";
   9.144  
   9.145 -(*The f0 premise ensures that the product is well-defined.*)
   9.146 -Goal "[| PLam I F : invariant (lift_set i A);  i : I;  \
   9.147 -\        f0: Init (PLam I F) |] ==> F i : invariant A";
   9.148 -by (auto_tac (claset(),
   9.149 -	      simpset() addsimps [invariant_def]));
   9.150 -by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1);
   9.151 -by Auto_tac;
   9.152 -qed "PLam_invariant_imp_invariant";
   9.153 +
   9.154 +Goal "ALL j. F j : preserves snd \
   9.155 +\     ==> (PLam I F : preserves (v o sub j o fst)) = \
   9.156 +\         (if j: I then F j : preserves (v o fst) else True)";
   9.157 +by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_sub]) 1);
   9.158 +by (Blast_tac 1);
   9.159 +qed "PLam_preserves";
   9.160 +Addsimps [PLam_preserves];
   9.161 +
   9.162  
   9.163 -Goal "[| i : I;  f0: Init (PLam I F) |] \
   9.164 -\     ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)";
   9.165 -by (blast_tac (claset() addIs [invariant_imp_PLam_invariant, 
   9.166 -			       PLam_invariant_imp_invariant]) 1);
   9.167 -qed "PLam_invariant";
   9.168 +(**UNUSED
   9.169 +    (*The f0 premise ensures that the product is well-defined.*)
   9.170 +    Goal "[| PLam I F : invariant (lift_set i A);  i : I;  \
   9.171 +    \        f0: Init (PLam I F) |] ==> F i : invariant A";
   9.172 +    by (auto_tac (claset(),
   9.173 +		  simpset() addsimps [invariant_def]));
   9.174 +    by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1);
   9.175 +    by Auto_tac;
   9.176 +    qed "PLam_invariant_imp_invariant";
   9.177  
   9.178 -(*The f0 premise isn't needed if F is a constant program because then
   9.179 -  we get an initial state by replicating that of F*)
   9.180 -Goal "i : I \
   9.181 -\     ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)";
   9.182 -by (auto_tac (claset(),
   9.183 -	      simpset() addsimps [invariant_def]));
   9.184 -qed "const_PLam_invariant";
   9.185 +    Goal "[| i : I;  f0: Init (PLam I F) |] \
   9.186 +    \     ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)";
   9.187 +    by (blast_tac (claset() addIs [invariant_imp_PLam_invariant, 
   9.188 +				   PLam_invariant_imp_invariant]) 1);
   9.189 +    qed "PLam_invariant";
   9.190 +
   9.191 +    (*The f0 premise isn't needed if F is a constant program because then
   9.192 +      we get an initial state by replicating that of F*)
   9.193 +    Goal "i : I \
   9.194 +    \     ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)";
   9.195 +    by (auto_tac (claset(),
   9.196 +		  simpset() addsimps [invariant_def]));
   9.197 +    qed "const_PLam_invariant";
   9.198 +**)
   9.199  
   9.200  
   9.201 -(** Reachability **)
   9.202 +(**UNUSED
   9.203 +    (** Reachability **)
   9.204  
   9.205 -Goal "[| f : reachable (PLam I F);  i : I |] ==> f i : reachable (F i)";
   9.206 -by (etac reachable.induct 1);
   9.207 -by (auto_tac (claset() addIs reachable.intrs, simpset()));
   9.208 -qed "reachable_PLam";
   9.209 +    Goal "[| f : reachable (PLam I F);  i : I |] ==> f i : reachable (F i)";
   9.210 +    by (etac reachable.induct 1);
   9.211 +    by (auto_tac (claset() addIs reachable.intrs, simpset()));
   9.212 +    qed "reachable_PLam";
   9.213  
   9.214 -(*Result to justify a re-organization of this file*)
   9.215 -Goal "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))";
   9.216 -by Auto_tac;
   9.217 -result();
   9.218 +    (*Result to justify a re-organization of this file*)
   9.219 +    Goal "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))";
   9.220 +    by Auto_tac;
   9.221 +    result();
   9.222  
   9.223 -Goal "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))";
   9.224 -by (force_tac (claset() addSDs [reachable_PLam], simpset()) 1);
   9.225 -qed "reachable_PLam_subset1";
   9.226 +    Goal "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))";
   9.227 +    by (force_tac (claset() addSDs [reachable_PLam], simpset()) 1);
   9.228 +    qed "reachable_PLam_subset1";
   9.229  
   9.230 -(*simplify using reachable_lift_prog??*)
   9.231 -Goal "[| i ~: I;  A : reachable (F i) |]     \
   9.232 -\  ==> ALL f. f : reachable (PLam I F)      \
   9.233 -\             --> f(i:=A) : reachable (lift_prog i (F i) Join PLam I F)";
   9.234 -by (etac reachable.induct 1);
   9.235 -by (ALLGOALS Clarify_tac);
   9.236 -by (etac reachable.induct 1);
   9.237 -(*Init, Init case*)
   9.238 -by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
   9.239 -(*Init of F, action of PLam F case*)
   9.240 -by (res_inst_tac [("act","act")] reachable.Acts 1);
   9.241 -by (Force_tac 1);
   9.242 -by (assume_tac 1);
   9.243 -by (force_tac (claset() addIs [ext], simpset()) 1);
   9.244 -(*induction over the 2nd "reachable" assumption*)
   9.245 -by (eres_inst_tac [("xa","f")] reachable.induct 1);
   9.246 -(*Init of PLam F, action of F case*)
   9.247 -by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1);
   9.248 -by (Force_tac 1);
   9.249 -by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
   9.250 -by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1);
   9.251 -(*last case: an action of PLam I F*)
   9.252 -by (res_inst_tac [("act","acta")] reachable.Acts 1);
   9.253 -by (Force_tac 1);
   9.254 -by (assume_tac 1);
   9.255 -by (force_tac (claset() addIs [ext], simpset()) 1);
   9.256 -qed_spec_mp "reachable_lift_Join_PLam";
   9.257 -
   9.258 -
   9.259 -(*The index set must be finite: otherwise infinitely many copies of F can
   9.260 -  perform actions, and PLam can never catch up in finite time.*)
   9.261 -Goal "finite I \
   9.262 -\     ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)";
   9.263 -by (etac finite_induct 1);
   9.264 -by (Simp_tac 1);
   9.265 -by (force_tac (claset() addDs [reachable_lift_Join_PLam], 
   9.266 -	       simpset() addsimps [PLam_insert]) 1);
   9.267 -qed "reachable_PLam_subset2";
   9.268 -
   9.269 -Goal "finite I ==> \
   9.270 -\     reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))";
   9.271 -by (REPEAT_FIRST (ares_tac [equalityI,
   9.272 -			    reachable_PLam_subset1, 
   9.273 -			    reachable_PLam_subset2]));
   9.274 -qed "reachable_PLam_eq";
   9.275 +    (*simplify using reachable_lift??*)
   9.276 +    Goal "[| i ~: I;  A : reachable (F i) |]     \
   9.277 +    \  ==> ALL f. f : reachable (PLam I F)      \
   9.278 +    \             --> f(i:=A) : reachable (lift i (F i) Join PLam I F)";
   9.279 +    by (etac reachable.induct 1);
   9.280 +    by (ALLGOALS Clarify_tac);
   9.281 +    by (etac reachable.induct 1);
   9.282 +    (*Init, Init case*)
   9.283 +    by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
   9.284 +    (*Init of F, action of PLam F case*)
   9.285 +    by (res_inst_tac [("act","act")] reachable.Acts 1);
   9.286 +    by (Force_tac 1);
   9.287 +    by (assume_tac 1);
   9.288 +    by (force_tac (claset() addIs [ext], simpset()) 1);
   9.289 +    (*induction over the 2nd "reachable" assumption*)
   9.290 +    by (eres_inst_tac [("xa","f")] reachable.induct 1);
   9.291 +    (*Init of PLam F, action of F case*)
   9.292 +    by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1);
   9.293 +    by (Force_tac 1);
   9.294 +    by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
   9.295 +    by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1);
   9.296 +    (*last case: an action of PLam I F*)
   9.297 +    by (res_inst_tac [("act","acta")] reachable.Acts 1);
   9.298 +    by (Force_tac 1);
   9.299 +    by (assume_tac 1);
   9.300 +    by (force_tac (claset() addIs [ext], simpset()) 1);
   9.301 +    qed_spec_mp "reachable_lift_Join_PLam";
   9.302  
   9.303  
   9.304 -(** Co **)
   9.305 -
   9.306 -Goal "[| F i : A Co B;  i: I;  finite I |]  \
   9.307 -\     ==> PLam I F : (lift_set i A) Co (lift_set i B)";
   9.308 -by (auto_tac
   9.309 -    (claset(),
   9.310 -     simpset() addsimps [Constrains_def, Collect_conj_eq RS sym,
   9.311 -			 reachable_PLam_eq]));
   9.312 -by (auto_tac (claset(), 
   9.313 -              simpset() addsimps [constrains_def, PLam_def]));
   9.314 -by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
   9.315 -qed "Constrains_imp_PLam_Constrains";
   9.316 +    (*The index set must be finite: otherwise infinitely many copies of F can
   9.317 +      perform actions, and PLam can never catch up in finite time.*)
   9.318 +    Goal "finite I \
   9.319 +    \     ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)";
   9.320 +    by (etac finite_induct 1);
   9.321 +    by (Simp_tac 1);
   9.322 +    by (force_tac (claset() addDs [reachable_lift_Join_PLam], 
   9.323 +		   simpset() addsimps [PLam_insert]) 1);
   9.324 +    qed "reachable_PLam_subset2";
   9.325  
   9.326 -Goal "[| ALL j:I. f0 j : A j;   i: I |] \
   9.327 -\     ==> drop_set i (INT j:I. lift_set j (A j)) = A i";
   9.328 -by (force_tac (claset() addSIs [image_eqI'],
   9.329 -	       simpset() addsimps [drop_set_def]) 1);
   9.330 -qed "drop_set_INT_lift_set";
   9.331 -
   9.332 -(*Again, we need the f0 premise so that PLam I F has an initial state;
   9.333 -  otherwise its Co-property is vacuous.*)
   9.334 -Goal "[| PLam I F : (lift_set i A) Co (lift_set i B);  \
   9.335 -\        i: I;  finite I;  f0: Init (PLam I F) |]  \
   9.336 -\     ==> F i : A Co B";
   9.337 -by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
   9.338 -by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1);
   9.339 -by (blast_tac (claset() addIs [reachable.Init]) 2);
   9.340 -by (dtac PLam_constrains_drop_set 1);
   9.341 -by (assume_tac 1);
   9.342 -by (asm_full_simp_tac
   9.343 -    (simpset() addsimps [drop_set_Int_lift_set2,
   9.344 -			 drop_set_INT_lift_set, reachable_PLam_eq]) 1);
   9.345 -qed "PLam_Constrains_imp_Constrains";
   9.346 +    Goal "finite I ==> \
   9.347 +    \     reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))";
   9.348 +    by (REPEAT_FIRST (ares_tac [equalityI,
   9.349 +				reachable_PLam_subset1, 
   9.350 +				reachable_PLam_subset2]));
   9.351 +    qed "reachable_PLam_eq";
   9.352  
   9.353  
   9.354 -Goal "[| i: I;  finite I;  f0: Init (PLam I F) |]  \
   9.355 -\     ==> (PLam I F : (lift_set i A) Co (lift_set i B)) =  \
   9.356 -\         (F i : A Co B)";
   9.357 -by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, 
   9.358 -			       PLam_Constrains_imp_Constrains]) 1);
   9.359 -qed "PLam_Constrains";
   9.360 +    (** Co **)
   9.361  
   9.362 -Goal "[| i: I;  finite I;  f0: Init (PLam I F) |]  \
   9.363 -\     ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)";
   9.364 -by (asm_simp_tac (simpset() delsimps [Init_PLam]
   9.365 -			    addsimps [Stable_def, PLam_Constrains]) 1);
   9.366 -qed "PLam_Stable";
   9.367 +    Goal "[| F i : A Co B;  i: I;  finite I |]  \
   9.368 +    \     ==> PLam I F : (lift_set i A) Co (lift_set i B)";
   9.369 +    by (auto_tac
   9.370 +	(claset(),
   9.371 +	 simpset() addsimps [Constrains_def, Collect_conj_eq RS sym,
   9.372 +			     reachable_PLam_eq]));
   9.373 +    by (auto_tac (claset(), 
   9.374 +		  simpset() addsimps [constrains_def, PLam_def]));
   9.375 +    by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
   9.376 +    qed "Constrains_imp_PLam_Constrains";
   9.377 +
   9.378  
   9.379  
   9.380 -(** const_PLam (no dependence on i) doesn't require the f0 premise **)
   9.381 -
   9.382 -Goal "[| (plam x:I. F) : (lift_set i A) Co (lift_set i B);  \
   9.383 -\        i: I;  finite I |]  \
   9.384 -\     ==> F : A Co B";
   9.385 -by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
   9.386 -by (dtac PLam_constrains_drop_set 1);
   9.387 -by (assume_tac 1);
   9.388 -by (asm_full_simp_tac
   9.389 -    (simpset() addsimps [drop_set_INT,
   9.390 -			 drop_set_Int_lift_set2, Collect_conj_eq RS sym,
   9.391 -			 reachable_PLam_eq]) 1);
   9.392 -qed "const_PLam_Constrains_imp_Constrains";
   9.393 +    Goal "[| i: I;  finite I;  f0: Init (PLam I F) |]  \
   9.394 +    \     ==> (PLam I F : (lift_set i A) Co (lift_set i B)) =  \
   9.395 +    \         (F i : A Co B)";
   9.396 +    by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, 
   9.397 +				   PLam_Constrains_imp_Constrains]) 1);
   9.398 +    qed "PLam_Constrains";
   9.399  
   9.400 -Goal "[| i: I;  finite I |]  \
   9.401 -\     ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) =  \
   9.402 -\         (F : A Co B)";
   9.403 -by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, 
   9.404 -			       const_PLam_Constrains_imp_Constrains]) 1);
   9.405 -qed "const_PLam_Constrains";
   9.406 -
   9.407 -Goal "[| i: I;  finite I |]  \
   9.408 -\     ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)";
   9.409 -by (asm_simp_tac (simpset() addsimps [Stable_def, const_PLam_Constrains]) 1);
   9.410 -qed "const_PLam_Stable";
   9.411 -
   9.412 -Goalw [Increasing_def]
   9.413 -     "[| i: I;  finite I |]  \
   9.414 -\     ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)";
   9.415 -by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1);
   9.416 -by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2);
   9.417 -by (asm_full_simp_tac
   9.418 -    (simpset() addsimps [finite_lessThan, const_PLam_Stable]) 1);
   9.419 -qed "const_PLam_Increasing";
   9.420 +    Goal "[| i: I;  finite I;  f0: Init (PLam I F) |]  \
   9.421 +    \     ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)";
   9.422 +    by (asm_simp_tac (simpset() delsimps [Init_PLam]
   9.423 +				addsimps [Stable_def, PLam_Constrains]) 1);
   9.424 +    qed "PLam_Stable";
   9.425  
   9.426  
   9.427 -(*** guarantees properties ***)
   9.428 +    (** const_PLam (no dependence on i) doesn't require the f0 premise **)
   9.429 +
   9.430 +    Goal "[| i: I;  finite I |]  \
   9.431 +    \     ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) =  \
   9.432 +    \         (F : A Co B)";
   9.433 +    by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, 
   9.434 +				   const_PLam_Constrains_imp_Constrains]) 1);
   9.435 +    qed "const_PLam_Constrains";
   9.436 +
   9.437 +    Goal "[| i: I;  finite I |]  \
   9.438 +    \     ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)";
   9.439 +    by (asm_simp_tac (simpset() addsimps [Stable_def, const_PLam_Constrains]) 1);
   9.440 +    qed "const_PLam_Stable";
   9.441  
   9.442 -Goalw [PLam_def]
   9.443 -    "[| lift_prog i (F i): X guarantees[v] Y;  i : I;  \
   9.444 -\        ALL j:I. i~=j --> lift_prog j (F j) : preserves v |]  \
   9.445 -\    ==> (PLam I F) : X guarantees[v] Y";
   9.446 -by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
   9.447 -qed "guarantees_PLam_I";
   9.448 +    Goalw [Increasing_def]
   9.449 +	 "[| i: I;  finite I |]  \
   9.450 +    \     ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)";
   9.451 +    by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1);
   9.452 +    by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2);
   9.453 +    by (asm_full_simp_tac
   9.454 +	(simpset() addsimps [finite_lessThan, const_PLam_Stable]) 1);
   9.455 +    qed "const_PLam_Increasing";
   9.456 +
   9.457  
   9.458 -Goal "(PLam I F : preserves (v o sub j)) = \
   9.459 -\     (if j: I then F j : preserves v else True)";
   9.460 -by (asm_simp_tac (simpset() addsimps [PLam_def, lift_prog_preserves_sub]) 1);
   9.461 -by (Blast_tac 1);
   9.462 -qed "PLam_preserves";
   9.463 +    (*** guarantees properties ***)
   9.464  
   9.465 -AddIffs [PLam_preserves];
   9.466 +    Goalw [PLam_def]
   9.467 +	"[| lift i (F i): X guarantees[v] Y;  i : I;  \
   9.468 +    \        ALL j:I. i~=j --> lift j (F j) : preserves v |]  \
   9.469 +    \    ==> (PLam I F) : X guarantees[v] Y";
   9.470 +    by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
   9.471 +    qed "guarantees_PLam_I";
   9.472 +**)
   9.473 +
    10.1 --- a/src/HOL/UNITY/PPROD.thy	Wed Feb 16 15:04:12 2000 +0100
    10.2 +++ b/src/HOL/UNITY/PPROD.thy	Fri Feb 18 15:20:44 2000 +0100
    10.3 @@ -11,11 +11,12 @@
    10.4  
    10.5  constdefs
    10.6  
    10.7 -  PLam  :: ['a set, 'a => 'b program] => ('a => 'b) program
    10.8 -    "PLam I F == JN i:I. lift_prog i (F i)"
    10.9 +  PLam  :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
   10.10 +            => ((nat=>'b) * 'c) program"
   10.11 +    "PLam I F == JN i:I. lift i (F i)"
   10.12  
   10.13  syntax
   10.14 -  "@PLam" :: [pttrn, 'a set, 'b set] => ('a => 'b) set ("(3plam _:_./ _)" 10)
   10.15 +  "@PLam" :: [pttrn, nat set, 'b set] => (nat => 'b) set ("(3plam _:_./ _)" 10)
   10.16  
   10.17  translations
   10.18    "plam x:A. B"   == "PLam A (%x. B)"
    11.1 --- a/src/HOL/UNITY/Project.ML	Wed Feb 16 15:04:12 2000 +0100
    11.2 +++ b/src/HOL/UNITY/Project.ML	Fri Feb 18 15:20:44 2000 +0100
    11.3 @@ -10,66 +10,14 @@
    11.4  
    11.5  Open_locale "Extend";
    11.6  
    11.7 -(** projection: monotonicity for safety **)
    11.8 -
    11.9 -Goal "D <= C ==> \
   11.10 -\     project_act h (Restrict D act) <= project_act h (Restrict C act)";
   11.11 -by (auto_tac (claset(), simpset() addsimps [project_act_def]));
   11.12 -qed "project_act_mono";
   11.13 -
   11.14 -Goal "[| D <= C; project h C F : A co B |] ==> project h D F : A co B";
   11.15 -by (auto_tac (claset(), simpset() addsimps [constrains_def]));
   11.16 -by (dtac project_act_mono 1);
   11.17 -by (Blast_tac 1);
   11.18 -qed "project_constrains_mono";
   11.19 -
   11.20 -Goal "[| D <= C;  project h C F : stable A |] ==> project h D F : stable A";
   11.21 -by (asm_full_simp_tac
   11.22 -    (simpset() addsimps [stable_def, project_constrains_mono]) 1);
   11.23 -qed "project_stable_mono";
   11.24 -
   11.25  Goal "F : A co B ==> project h C (extend h F) : A co B";
   11.26  by (auto_tac (claset(), 
   11.27        simpset() addsimps [extend_act_def, project_act_def, constrains_def]));
   11.28  qed "project_extend_constrains_I";
   11.29  
   11.30 -Goal "UNIV <= project_set h C \
   11.31 -\     ==> project h C ((extend h F) Join G) = F Join (project h C G)";
   11.32 -by (rtac program_equalityI 1);
   11.33 -by (asm_simp_tac (simpset() addsimps [image_eq_UN, UN_Un,
   11.34 -			subset_UNIV RS subset_trans RS Restrict_triv]) 2);
   11.35 -by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
   11.36 -qed "project_extend_Join";
   11.37 -
   11.38 -Goal "UNIV <= project_set h C \
   11.39 -\     ==> (extend h F) Join G = extend h H ==> H = F Join (project h C G)";
   11.40 -by (dres_inst_tac [("f", "project h C")] arg_cong 1);
   11.41 -by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
   11.42 -qed "extend_Join_eq_extend_D";
   11.43 -
   11.44  
   11.45  (** Safety **)
   11.46  
   11.47 -Goalw [constrains_def]
   11.48 -     "(project h C F : A co B)  =  \
   11.49 -\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
   11.50 -by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
   11.51 -by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
   11.52 -(*the <== direction*)
   11.53 -by (rewtac project_act_def);
   11.54 -by (force_tac (claset() addSDs [subsetD], simpset()) 1);
   11.55 -qed "project_constrains";
   11.56 -
   11.57 -Goalw [stable_def]
   11.58 -     "(project h UNIV F : stable A) = (F : stable (extend_set h A))";
   11.59 -by (simp_tac (simpset() addsimps [project_constrains]) 1);
   11.60 -qed "project_stable";
   11.61 -
   11.62 -Goal "F : stable (extend_set h A) ==> project h C F : stable A";
   11.63 -by (dtac (project_stable RS iffD2) 1);
   11.64 -by (blast_tac (claset() addIs [project_stable_mono]) 1);
   11.65 -qed "project_stable_I";
   11.66 -
   11.67  (*used below to prove Join_project_ensures*)
   11.68  Goal "[| G : stable C;  project h C G : A unless B |] \
   11.69  \     ==> G : (C Int extend_set h A) unless (extend_set h B)";
   11.70 @@ -113,7 +61,7 @@
   11.71       "extend h F Join G : increasing (func o f) \
   11.72  \     ==> F Join project h C G : increasing func";
   11.73  by (asm_full_simp_tac (simpset() addsimps [project_constrains_I, 
   11.74 -					   Collect_eq_extend_set RS sym]) 1);
   11.75 +					   extend_set_eq_Collect]) 1);
   11.76  qed "project_increasing_I";
   11.77  
   11.78  Goal "(F Join project h UNIV G : increasing func)  =  \
   11.79 @@ -123,7 +71,7 @@
   11.80  by (asm_full_simp_tac 
   11.81      (simpset() addsimps [increasing_def, Join_project_stable]) 1);
   11.82  by (auto_tac (claset(),
   11.83 -	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
   11.84 +	      simpset() addsimps [Join_stable, extend_set_eq_Collect,
   11.85  				  extend_stable RS iffD1]));
   11.86  qed "Join_project_increasing";
   11.87  
   11.88 @@ -136,32 +84,6 @@
   11.89  qed "project_constrains_D";
   11.90  
   11.91  
   11.92 -(*** preserves ***)
   11.93 -
   11.94 -Goal "G : preserves (v o f) ==> project h C G : preserves v";
   11.95 -by (auto_tac (claset(),
   11.96 -	      simpset() addsimps [preserves_def, project_stable_I,
   11.97 -				  Collect_eq_extend_set RS sym]));
   11.98 -qed "project_preserves_I";
   11.99 -
  11.100 -(*to preserve f is to preserve the whole original state*)
  11.101 -Goal "G : preserves f ==> project h C G : preserves id";
  11.102 -by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
  11.103 -qed "project_preserves_id_I";
  11.104 -
  11.105 -Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
  11.106 -by (auto_tac (claset(),
  11.107 -	      simpset() addsimps [preserves_def, extend_stable RS sym,
  11.108 -				  Collect_eq_extend_set RS sym]));
  11.109 -qed "extend_preserves";
  11.110 -
  11.111 -Goal "inj h ==> (extend h G : preserves g)";
  11.112 -by (auto_tac (claset(),
  11.113 -	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
  11.114 -				  stable_def, constrains_def, g_def]));
  11.115 -qed "inj_extend_preserves";
  11.116 -
  11.117 -
  11.118  (*** "projecting" and union/intersection (no converses) ***)
  11.119  
  11.120  Goalw [projecting_def]
  11.121 @@ -315,7 +237,7 @@
  11.122       "F Join project h (reachable (extend h F Join G)) G : Increasing func  \
  11.123  \     ==> extend h F Join G : Increasing (func o f)";
  11.124  by Auto_tac;
  11.125 -by (stac Collect_eq_extend_set 1);
  11.126 +by (stac (extend_set_eq_Collect RS sym) 1);
  11.127  by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); 
  11.128  qed "project_Increasing_D";
  11.129  
  11.130 @@ -381,7 +303,7 @@
  11.131      "extend h F Join G : Increasing (func o f)  \
  11.132  \    ==> F Join project h (reachable (extend h F Join G)) G : Increasing func";
  11.133  by Auto_tac;
  11.134 -by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
  11.135 +by (asm_simp_tac (simpset() addsimps [extend_set_eq_Collect,
  11.136  				      project_Stable_I]) 1); 
  11.137  qed "project_Increasing_I";
  11.138  
  11.139 @@ -400,7 +322,7 @@
  11.140     "(F Join project h (reachable (extend h F Join G)) G : Increasing func)  = \
  11.141  \   (extend h F Join G : Increasing (func o f))";
  11.142  by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
  11.143 -				      Collect_eq_extend_set RS sym]) 1);
  11.144 +				      extend_set_eq_Collect]) 1);
  11.145  qed "project_Increasing";
  11.146  
  11.147  (** A lot of redundant theorems: all are proved to facilitate reasoning
  11.148 @@ -662,38 +584,9 @@
  11.149  qed "project_Ensures_D";
  11.150  
  11.151  
  11.152 -(*** GUARANTEES and EXTEND ***)
  11.153 -
  11.154 -(** Strong precondition and postcondition; doesn't seem very useful. **)
  11.155 -
  11.156 -Goal "F : X guarantees[v] Y ==> \
  11.157 -\     extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
  11.158 -by (rtac guaranteesI 1);
  11.159 -by Auto_tac;
  11.160 -by (blast_tac (claset() addIs [project_preserves_I]
  11.161 -			addDs [project_set_UNIV RS equalityD2 RS 
  11.162 -			       extend_Join_eq_extend_D, 
  11.163 -			       guaranteesD]) 1);
  11.164 -qed "guarantees_imp_extend_guarantees";
  11.165 +(*** Guarantees ***)
  11.166  
  11.167 -Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
  11.168 -\     ==> F : X guarantees[v] Y";
  11.169 -by (auto_tac (claset(), simpset() addsimps [guar_def]));
  11.170 -by (dres_inst_tac [("x", "extend h G")] spec 1);
  11.171 -by (asm_full_simp_tac 
  11.172 -    (simpset() delsimps [extend_Join] 
  11.173 -           addsimps [extend_Join RS sym, extend_preserves,
  11.174 -		     inj_extend RS inj_image_mem_iff]) 1);
  11.175 -qed "extend_guarantees_imp_guarantees";
  11.176 -
  11.177 -Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
  11.178 -\    (F : X guarantees[v] Y)";
  11.179 -by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
  11.180 -			       extend_guarantees_imp_guarantees]) 1);
  11.181 -qed "extend_guarantees_eq";
  11.182 -
  11.183 -
  11.184 -(*Weak precondition and postcondition; this is the good one!
  11.185 +(*Weak precondition and postcondition
  11.186    Not clear that it has a converse [or that we want one!]*)
  11.187  
  11.188  (*The raw version*)
    12.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Feb 16 15:04:12 2000 +0100
    12.2 +++ b/src/HOL/UNITY/ROOT.ML	Fri Feb 18 15:20:44 2000 +0100
    12.3 @@ -28,7 +28,9 @@
    12.4  time_use_thy "Extend";
    12.5  time_use_thy "PPROD";
    12.6  time_use_thy "TimerArray";
    12.7 +(**
    12.8  time_use_thy "Alloc";
    12.9 +**)
   12.10  
   12.11  add_path "../Auth";	(*to find Public.thy*)
   12.12  use_thy"NSP_Bad";
    13.1 --- a/src/HOL/UNITY/TimerArray.ML	Wed Feb 16 15:04:12 2000 +0100
    13.2 +++ b/src/HOL/UNITY/TimerArray.ML	Fri Feb 18 15:20:44 2000 +0100
    13.3 @@ -9,26 +9,40 @@
    13.4  Addsimps [Timer_def RS def_prg_Init];
    13.5  program_defs_ref := [Timer_def];
    13.6  
    13.7 -Addsimps [decr_def];
    13.8 +Addsimps [count_def, decr_def];
    13.9  
   13.10  (*Demonstrates induction, but not used in the following proof*)
   13.11 -Goal "Timer : UNIV leadsTo {0}";
   13.12 -by (res_inst_tac [("f", "id")] (allI RS lessThan_induct) 1);
   13.13 +Goal "Timer : UNIV leadsTo {s. count s = 0}";
   13.14 +by (res_inst_tac [("f", "count")] lessThan_induct 1);
   13.15  by (Simp_tac 1);
   13.16  by (exhaust_tac "m" 1);
   13.17 -by (blast_tac (claset() addSIs [subset_imp_leadsTo]) 1);
   13.18 +by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1);
   13.19  by (ensures_tac "decr" 1);
   13.20  qed "Timer_leadsTo_zero";
   13.21  
   13.22 -Goal "finite I ==> (plam i: I. Timer) : UNIV leadsTo {s. ALL i:I. s i = 0}";
   13.23 -by (eres_inst_tac [("A'1", "%i. lift_set i {0}")]
   13.24 +Goal "Timer : preserves snd";
   13.25 +by (rtac preservesI 1);
   13.26 +by (constrains_tac 1);
   13.27 +qed "Timer_preserves_snd";
   13.28 +AddIffs [Timer_preserves_snd];
   13.29 +
   13.30 +
   13.31 +Goal "finite I \
   13.32 +\     ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";
   13.33 +by (eres_inst_tac [("A'1", "%i. lift_set i ({0} Times UNIV)")]
   13.34      (finite_stable_completion RS leadsTo_weaken) 1);
   13.35  by Auto_tac;
   13.36 +(*Safety property, already reduced to the single Timer case*)
   13.37  by (constrains_tac 2);
   13.38 -by (res_inst_tac [("f", "sub i")] (allI RS lessThan_induct) 1);
   13.39 +(*Progress property for the array of Timers*)
   13.40 +by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
   13.41  by (exhaust_tac "m" 1);
   13.42 +(*Annoying need to massage the conditions to have the form (... Times UNIV)*)
   13.43  by (auto_tac (claset() addIs [subset_imp_leadsTo], 
   13.44 -	      simpset() addsimps [insert_absorb, lessThan_Suc RS sym]));
   13.45 +	      simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
   13.46 +				  lift_set_Un_distrib RS sym,
   13.47 +				  Times_Un_distrib1 RS sym,
   13.48 +				  Times_Diff_distrib1 RS sym]));
   13.49  by (rename_tac "n" 1);
   13.50  by (rtac PLam_leadsTo_Basis 1);
   13.51  by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
    14.1 --- a/src/HOL/UNITY/TimerArray.thy	Wed Feb 16 15:04:12 2000 +0100
    14.2 +++ b/src/HOL/UNITY/TimerArray.thy	Fri Feb 18 15:20:44 2000 +0100
    14.3 @@ -8,11 +8,16 @@
    14.4  
    14.5  TimerArray = PPROD +
    14.6  
    14.7 +types 'a state = "nat * 'a"   (*second component allows new variables*)
    14.8 +
    14.9  constdefs
   14.10 -  decr  :: "(nat*nat) set"
   14.11 -    "decr == UN n. {(Suc n, n)}"
   14.12 +  count  :: "'a state => nat"
   14.13 +    "count s == fst s"
   14.14    
   14.15 -  Timer :: nat program
   14.16 +  decr  :: "('a state * 'a state) set"
   14.17 +    "decr == UN n uu. {((Suc n, uu), (n,uu))}"
   14.18 +  
   14.19 +  Timer :: 'a state program
   14.20      "Timer == mk_program (UNIV, {decr})"
   14.21  
   14.22  end
    15.1 --- a/src/HOL/UNITY/Union.ML	Wed Feb 16 15:04:12 2000 +0100
    15.2 +++ b/src/HOL/UNITY/Union.ML	Fri Feb 18 15:20:44 2000 +0100
    15.3 @@ -168,7 +168,9 @@
    15.4  
    15.5  (*** Safety: co, stable, FP ***)
    15.6  
    15.7 -(*Fails if I={} because it collapses to SKIP : A co B*)
    15.8 +(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B.  So an
    15.9 +  alternative precondition is A<=B, but most proofs using this rule require
   15.10 +  I to be nonempty for other reasons anyway.*)
   15.11  Goalw [constrains_def, JOIN_def]
   15.12      "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)";
   15.13  by (Simp_tac 1);
   15.14 @@ -196,6 +198,7 @@
   15.15  by (blast_tac (claset() addIs [constrains_weaken]) 1);
   15.16  qed "Join_constrains_weaken";
   15.17  
   15.18 +(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*)
   15.19  Goal "[| ALL i:I. F i : A i co A' i;  i: I |] \
   15.20  \     ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)";
   15.21  by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1);
   15.22 @@ -258,10 +261,10 @@
   15.23  by (asm_simp_tac (simpset() addsimps [Join_transient]) 1);
   15.24  qed "Join_transient_I2";
   15.25  
   15.26 +(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
   15.27  Goal "i : I ==> \
   15.28  \     (JN i:I. F i) : A ensures B = \
   15.29 -\     ((ALL i:I. F i : (A-B) co (A Un B)) & \
   15.30 -\      (EX i:I. F i : A ensures B))";
   15.31 +\     ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))";
   15.32  by (auto_tac (claset(),
   15.33  	      simpset() addsimps [ensures_def, JN_constrains, JN_transient]));
   15.34  qed "JN_ensures";
    16.1 --- a/src/HOL/UNITY/WFair.ML	Wed Feb 16 15:04:12 2000 +0100
    16.2 +++ b/src/HOL/UNITY/WFair.ML	Fri Feb 18 15:20:44 2000 +0100
    16.3 @@ -401,11 +401,12 @@
    16.4  
    16.5  
    16.6  (*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
    16.7 -Goal "[| ALL m. F : (A Int f-``{m}) leadsTo                     \
    16.8 -\                   ((A Int f-``(lessThan m)) Un B) |] \
    16.9 +val prems = 
   16.10 +Goal "[| !!m. F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
   16.11  \     ==> F : A leadsTo B";
   16.12  by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
   16.13  by (Asm_simp_tac 1);
   16.14 +by (blast_tac (claset() addIs prems) 1);
   16.15  qed "lessThan_induct";
   16.16  
   16.17  Goal "[| ALL m:(greaterThan l).    \