src/HOL/UNITY/Lift_prog.ML

new theory UNITY/Lift_prog

(*  Title:      HOL/UNITY/Lift_prog.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge
*)


(*** Basic properties ***)

(** lift_set and drop_set **)

Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)";
by Auto_tac;
qed "lift_set_iff";
AddIffs [lift_set_iff];

Goalw [lift_set_def] "lift_set i (A Int B) = lift_set i A Int lift_set i B";
by Auto_tac;
qed "lift_set_Int";

(*Converse fails*)
Goalw [drop_set_def] "f : A ==> f i : drop_set i A";
by Auto_tac;
qed "drop_set_I";

(** lift_act and drop_act **)

Goalw [lift_act_def] "lift_act i Id = Id";
by Auto_tac;
by (etac rev_mp 1);
by (dtac sym 1);
by (asm_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
qed "lift_act_Id";
Addsimps [lift_act_Id];

Goalw [drop_act_def] "(s, s') : act ==> (s i, s' i) : drop_act i act";
by (auto_tac (claset() addSIs [image_eqI], simpset()));
qed "drop_act_I";

Goalw [drop_act_def] "drop_act i Id = Id";
by Auto_tac;
by (res_inst_tac [("x", "((%u. x), (%u. x))")] image_eqI 1);
by Auto_tac;
qed "drop_act_Id";
Addsimps [drop_act_Id];

(** lift_prog and drop_prog **)

Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
by Auto_tac;
qed "Init_lift_prog";
Addsimps [Init_lift_prog];

Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
qed "Acts_lift_prog";
Addsimps [Acts_lift_prog];

Goalw [drop_prog_def] "Init (drop_prog i F) = drop_set i (Init F)";
by Auto_tac;
qed "Init_drop_prog";
Addsimps [Init_drop_prog];

Goalw [drop_prog_def] "Acts (drop_prog i F) = drop_act i `` Acts F";
by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
qed "Acts_drop_prog";
Addsimps [Acts_drop_prog];

Goal "F component G ==> lift_prog i F component lift_prog i G";
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
by Auto_tac;
qed "lift_prog_mono";

Goal "F component G ==> drop_prog i F component drop_prog i G";
by (full_simp_tac (simpset() addsimps [component_eq_subset, drop_set_def]) 1);
by Auto_tac;
qed "drop_prog_mono";

Goal "lift_prog i SKIP = SKIP";
by (auto_tac (claset() addSIs [program_equalityI],
	      simpset() addsimps [SKIP_def, lift_prog_def]));
qed "lift_prog_SKIP";

Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)";
by (rtac program_equalityI 1);
by (auto_tac (claset(), simpset() addsimps [Acts_Join]));
qed "lift_prog_Join";

Goal "lift_prog i (JOIN I F) = (JN j:I. lift_prog i (F j))";
by (rtac program_equalityI 1);
by (auto_tac (claset(), simpset() addsimps [Acts_JN]));
qed "lift_prog_JN";

Goal "drop_prog i SKIP = SKIP";
by (auto_tac (claset() addSIs [program_equalityI],
	      simpset() addsimps [SKIP_def, drop_set_def, drop_prog_def]));
qed "drop_prog_SKIP";


(** Injectivity of lift_set, lift_act, lift_prog **)

Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F";
by Auto_tac;
qed "lift_set_inverse";
Addsimps [lift_set_inverse];

Goal "inj (lift_set i)";
by (rtac inj_on_inverseI 1);
by (rtac lift_set_inverse 1);
qed "inj_lift_set";

(*Because A and B could differ outside i, cannot generalize result to 
   drop_set i (A Int B) = drop_set i A Int drop_set i B
*)
Goalw [lift_set_def, drop_set_def]
     "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)";
by Auto_tac;
qed "drop_set_lift_set_Int";

Goalw [lift_set_def, drop_set_def]
     "drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A";
by Auto_tac;
qed "drop_set_lift_set_Int2";

Goalw [drop_set_def]
     "i : I ==> drop_set i (INT j:I. lift_set j A) = A";
by Auto_tac;
qed "drop_set_INT";

Goalw [lift_act_def, drop_act_def] "drop_act i (lift_act i act) = act";
by Auto_tac;
by (res_inst_tac [("x", "f(i:=a)")] exI 1);
by (Asm_simp_tac 1);
by (res_inst_tac [("x", "f(i:=b)")] exI 1);
by (Asm_simp_tac 1);
by (rtac ext 1);
by (Asm_simp_tac 1);
qed "lift_act_inverse";
Addsimps [lift_act_inverse];

Goal "inj (lift_act i)";
by (rtac inj_on_inverseI 1);
by (rtac lift_act_inverse 1);
qed "inj_lift_act";

Goal "drop_prog i (lift_prog i F) = F";
by (simp_tac (simpset() addsimps [lift_prog_def, drop_prog_def]) 1);
by (rtac program_equalityI 1);
by (simp_tac (simpset() addsimps [image_compose RS sym, o_def]) 2);
by (Simp_tac 1);
qed "lift_prog_inverse";
Addsimps [lift_prog_inverse];

Goal "inj (lift_prog i)";
by (rtac inj_on_inverseI 1);
by (rtac lift_prog_inverse 1);
qed "inj_lift_prog";


(*For compatibility with the original definition and perhaps simpler proofs*)
Goalw [lift_act_def]
    "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
by Auto_tac;
by (rtac exI 1);
by Auto_tac;
qed "lift_act_eq";
AddIffs [lift_act_eq];


(*** Safety: co, stable, invariant ***)

(** Safety and lift_prog **)

Goal "(lift_prog i F : (lift_set i A) co (lift_set i B))  =  \
\     (F : A co B)";
by (auto_tac (claset(), 
	      simpset() addsimps [constrains_def]));
by (Blast_tac 2);
by (Force_tac 1);
qed "lift_prog_constrains_eq";

Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)";
by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains_eq]) 1);
qed "lift_prog_stable_eq";

Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)";
by (auto_tac (claset(),
	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
qed "lift_prog_invariant_eq";

(*This one looks strange!  Proof probably is by case analysis on i=j.
  If i~=j then lift_prog j (F j) does nothing to lift_set i, and the 
  premise ensures A<=B.*)
Goal "F i : A co B  \
\     ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)";
by (auto_tac (claset(), 
	      simpset() addsimps [constrains_def]));
by (REPEAT (Blast_tac 1));
qed "constrains_imp_lift_prog_constrains";


(** Safety and drop_prog **)

Goalw [constrains_def]
     "(drop_prog i F : A co B)  =  (F : (lift_set i A) co (lift_set i B))";
by Auto_tac;
by (force_tac (claset(), 
	       simpset() addsimps [drop_act_def]) 2);
by (blast_tac (claset() addIs [drop_act_I]) 1);
qed "drop_prog_constrains_eq";

Goal "(drop_prog i F : stable A)  =  (F : stable (lift_set i A))";
by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains_eq]) 1);
qed "drop_prog_stable_eq";


(** Diff, needed for localTo **)

Goal "Diff G (lift_act i `` Acts F) : (lift_set i A) co (lift_set i B)  \
\     ==> Diff (drop_prog i G) (Acts F) : A co B";
by (auto_tac (claset(), 
	      simpset() addsimps [constrains_def, Diff_def]));
by (dtac bspec 1);
by (Force_tac 1);
by (auto_tac (claset(), simpset() addsimps [drop_act_def]));
by (auto_tac (claset(), simpset() addsimps [lift_set_def]));
qed "Diff_drop_prog_co";

Goalw [stable_def]
     "Diff G (lift_act i `` Acts F) : stable (lift_set i A)  \
\     ==> Diff (drop_prog i G) (Acts F) : stable A";
by (etac Diff_drop_prog_co 1);
qed "Diff_drop_prog_stable";

Goal "Diff G (Acts F) : A co B  \
\     ==> Diff (lift_prog i G) (lift_act i `` Acts F) \
\         : (lift_set i A) co (lift_set i B)";
by (auto_tac (claset(), 
	      simpset() addsimps [constrains_def, Diff_def]));
by (auto_tac (claset(), simpset() addsimps [drop_act_def]));
qed "Diff_lift_prog_co";

Goalw [stable_def]
     "Diff G (Acts F) : stable A  \
\     ==> Diff (lift_prog i G) (lift_act i `` Acts F) : stable (lift_set i A)";
by (etac Diff_lift_prog_co 1);
qed "Diff_lift_prog_stable";


(*** Weak versions: Co, Stable ***)

(** Reachability **)

Goal "s : reachable F ==> f(i:=s) : reachable (lift_prog i F)";
by (etac reachable.induct 1);
by (force_tac (claset() addIs [reachable.Acts, ext], 
	       simpset()) 2);
by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
qed "reachable_lift_progI";

Goal "f : reachable (lift_prog i F) ==> f i : reachable F";
by (etac reachable.induct 1);
by Auto_tac;
by (ALLGOALS (blast_tac (claset() addIs reachable.intrs)));
qed "reachable_lift_progD";

Goal "reachable (lift_prog i F) = lift_set i (reachable F)";
by Auto_tac;
by (etac reachable_lift_progD 1);
ren "f" 1;
by (dres_inst_tac [("f","f"),("i","i")] reachable_lift_progI 1);
by Auto_tac;
qed "reachable_lift_prog";

Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B))  =  \
\     (F : A Co B)";
by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog,
				  lift_set_Int RS sym,
				  lift_prog_constrains_eq]) 1);
qed "lift_prog_Constrains_eq";

Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains_eq]) 1);
qed "lift_prog_Stable_eq";

(** Reachability and drop_prog **)

Goal "f : reachable F ==> f i : reachable (drop_prog i F)";
by (etac reachable.induct 1);
by (force_tac (claset() addIs [reachable.Acts, drop_act_I],
	       simpset()) 2);
by (force_tac (claset() addIs [reachable.Init, drop_set_I],
	       simpset()) 1);
qed "reachable_imp_reachable_drop_prog";

(*Converse fails because it would require
  [| s i : reachable (drop_prog i F); s i : A |] ==> s : reachable F
*)
Goalw [Constrains_def]
     "drop_prog i F : A Co B ==> F : (lift_set i A) Co (lift_set i B)";
by (full_simp_tac (simpset() addsimps [drop_prog_constrains_eq]) 1);
by (etac constrains_weaken_L 1);
by Auto_tac;
by (etac reachable_imp_reachable_drop_prog 1);
qed "drop_prog_Constrains_D";

Goalw [Stable_def]
     "drop_prog i F : Stable A ==> F : Stable (lift_set i A)";
by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
qed "drop_prog_Stable_D";


(*** Programs of the form lift_prog i F Join G
     in other words programs containing a replicated component ***)

Goal "drop_prog i ((lift_prog i F) Join G) = F Join (drop_prog i G)";
by (rtac program_equalityI 1);
by (simp_tac (simpset() addsimps [Acts_Join, image_Un,
				  image_compose RS sym, o_def]) 2);
by (simp_tac (simpset() addsimps [drop_set_lift_set_Int]) 1);
qed "drop_prog_lift_prog_Join";

Goal "(lift_prog i F) Join G = lift_prog i H \
\     ==> H = F Join (drop_prog i G)";
by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1);
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
by (etac sym 1);
qed "lift_prog_Join_eq_lift_prog_D";

Goal "f : reachable (lift_prog i F Join G)  \
\     ==> f i : reachable (F Join drop_prog i G)";
by (etac reachable.induct 1);
by (force_tac (claset() addIs [reachable.Init, drop_set_I], simpset()) 1);
(*By case analysis on whether the action is of lift_prog i F  or  G*)
by (force_tac (claset() addIs [reachable.Acts, drop_act_I], 
	       simpset() addsimps [Acts_Join, image_iff]) 1);
qed "reachable_lift_prog_Join_D";

(*Opposite inclusion fails, even for the initial state: lift_set i includes
  ALL functions determined only by their value at i.*)
Goal "reachable (lift_prog i F Join G) <= \
\     lift_set i (reachable (F Join drop_prog i G))";
by Auto_tac;
by (etac reachable_lift_prog_Join_D 1);
qed "reachable_lift_prog_Join_subset";

Goal "F Join drop_prog i G : Stable A    \
\     ==> lift_prog i F Join G : Stable (lift_set i A)";
by (full_simp_tac (simpset() addsimps [Stable_def, Constrains_def]) 1);
by (subgoal_tac 
    "lift_prog i F Join G : lift_set i (reachable (F Join drop_prog i G)) Int \
\                           lift_set i A \
\    co lift_set i A" 1);
by (asm_full_simp_tac 
    (simpset() addsimps [lift_set_Int RS sym,
			 lift_prog_constrains_eq,
			 drop_prog_constrains_eq RS sym,
			 drop_prog_lift_prog_Join]) 2);
by (blast_tac (claset() addIs [constrains_weaken, 
			       reachable_lift_prog_Join_D]) 1);
qed "lift_prog_Join_Stable_eq";


(*** guarantees properties ***)

(** It seems that neither of these can be proved from the other. **)

(*Strong precondition and postcondition; doesn't seem very useful*)
Goal "F : X guar Y \
\     ==> lift_prog i F : (lift_prog i `` X) guar (lift_prog i `` Y)";
by (rtac guaranteesI 1);
by Auto_tac;
by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
qed "lift_prog_guarantees";

(*Weak precondition and postcondition; doesn't seem very useful*)
Goal "[| F : X guar Y;  drop_prog i `` XX <= X;  \
\        ALL G. F Join drop_prog i G : Y --> lift_prog i F Join G : YY |] \
\     ==> lift_prog i F : XX guar YY";
by (rtac guaranteesI 1);
by (dtac guaranteesD 1);
by (etac subsetD 1);
by (rtac image_eqI 1);
by (auto_tac (claset(), simpset() addsimps [drop_prog_lift_prog_Join]));
qed "drop_prog_guarantees";


(*** sub ***)

Addsimps [sub_def];

Goal "lift_set i {s. P s} = {s. P (sub i s)}";
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
qed "lift_set_sub";

Goal "{s. P (s i)} = lift_set i {s. P s}";
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
qed "Collect_eq_lift_set";


(** Are these two useful?? **)

(*The other direction fails: having FF : Stable {s. z <= f (s i)} does not
  ensure that F has the form lift_prog i F for some F.*)
Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}";
by Auto_tac;
by (stac Collect_eq_lift_set 1); 
by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
qed "image_lift_prog_Stable";

Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)";
by (simp_tac (simpset() addsimps [Increasing_def,
				  inj_lift_prog RS image_INT]) 1);
by (blast_tac (claset() addIs [impOfSubs image_lift_prog_Stable]) 1);
qed "image_lift_prog_Increasing";


(*** guarantees corollaries ***)

Goalw [increasing_def]
     "F : UNIV guar increasing f \
\     ==> lift_prog i F : UNIV guar increasing (f o sub i)";
by (etac drop_prog_guarantees 1);
by Auto_tac;
by (stac Collect_eq_lift_set 1); 
by (asm_full_simp_tac
    (simpset() addsimps [lift_prog_stable_eq, drop_prog_stable_eq, 
			 stable_Join]) 1);
qed "lift_prog_guar_increasing";

Goalw [Increasing_def]
     "F : UNIV guar Increasing f \
\     ==> lift_prog i F : UNIV guar Increasing (f o sub i)";
by (etac drop_prog_guarantees 1);
by Auto_tac;
by (stac Collect_eq_lift_set 1); 
by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable_eq]) 1);
qed "lift_prog_guar_Increasing";

Goalw [localTo_def, increasing_def]
     "F : (f localTo F) guar increasing f  \
\     ==> lift_prog i F : (f o sub i) localTo (lift_prog i F)  \
\                         guar increasing (f o sub i)";
by (etac drop_prog_guarantees 1);
by Auto_tac;
by (stac Collect_eq_lift_set 2); 
(*the "increasing" guarantee*)
by (asm_full_simp_tac
    (simpset() addsimps [lift_prog_stable_eq, drop_prog_stable_eq, 
			 stable_Join]) 2);
(*the "localTo" requirement*)
by (asm_simp_tac
    (simpset() addsimps [Diff_drop_prog_stable, 
			 Collect_eq_lift_set RS sym]) 1); 
qed "lift_prog_guar_increasing2";

Goalw [localTo_def, Increasing_def]
     "F : (f localTo F) guar Increasing f  \
\     ==> lift_prog i F : (f o sub i) localTo (lift_prog i F)  \
\                         guar Increasing (f o sub i)";
by (etac drop_prog_guarantees 1);
by Auto_tac;
by (stac Collect_eq_lift_set 2); 
(*the "Increasing" guarantee*)
by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable_eq]) 2);
(*the "localTo" requirement*)
by (asm_simp_tac
    (simpset() addsimps [Diff_drop_prog_stable, 
			 Collect_eq_lift_set RS sym]) 1); 
qed "lift_prog_guar_Increasing2";

(*Converse fails.  Useful?*)
Goal "lift_prog i `` (f localTo F) <= (f o sub i) localTo (lift_prog i F)";
by (simp_tac (simpset() addsimps [localTo_def]) 1);
by Auto_tac;
by (stac Collect_eq_lift_set 1); 
by (asm_simp_tac (simpset() addsimps [Diff_lift_prog_stable]) 1); 
qed "localTo_lift_prog_I";