--- a/src/HOL/UNITY/Lift.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML Thu Oct 15 11:35:07 1998 +0200
@@ -55,7 +55,8 @@
zless_not_refl2, zless_not_refl3];
-Addsimps [Lprg_def RS def_prg_simps];
+Addsimps [Lprg_def RS def_prg_Init];
+program_defs_ref := [Lprg_def];
Addsimps (map simp_of_act
[request_act_def, open_act_def, close_act_def,
@@ -69,7 +70,7 @@
val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
-(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
+(* [| Lprg : LeadsTo B C; Lprg : LeadsTo A B |] ==> Lprg : LeadsTo (A Un B) C *)
(*Simplification for records*)
@@ -87,41 +88,41 @@
val nat_exhaust_pred_le =
read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
-Goal "Invariant Lprg open_stop";
+Goal "Lprg : Invariant open_stop";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
qed "open_stop";
-Goal "Invariant Lprg stop_floor";
+Goal "Lprg : Invariant stop_floor";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
qed "stop_floor";
(*This one needs open_stop, which was proved above*)
-Goal "Invariant Lprg open_move";
+Goal "Lprg : Invariant open_move";
by (rtac InvariantI 1);
by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2);
by (Force_tac 1);
by (constrains_tac 1);
qed "open_move";
-Goal "Invariant Lprg moving_up";
+Goal "Lprg : Invariant moving_up";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
qed "moving_up";
-Goal "Invariant Lprg moving_down";
+Goal "Lprg : Invariant moving_down";
by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac 1);
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
qed "moving_down";
-Goal "Invariant Lprg bounded";
+Goal "Lprg : Invariant bounded";
by (rtac InvariantI 1);
by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2);
by (Force_tac 1);
@@ -150,23 +151,23 @@
(** Lift_1 **)
-Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
+Goal "Lprg : LeadsTo (stopped Int atFloor n) (opened Int atFloor n)";
by (cut_facts_tac [stop_floor] 1);
by (ensures_tac "open_act" 1);
qed "E_thm01"; (*lem_lift_1_5*)
-Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \
+Goal "Lprg : LeadsTo (Req n Int stopped - atFloor n) \
\ (Req n Int opened - atFloor n)";
by (cut_facts_tac [stop_floor] 1);
by (ensures_tac "open_act" 1);
qed "E_thm02"; (*lem_lift_1_1*)
-Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
+Goal "Lprg : LeadsTo (Req n Int opened - atFloor n) \
\ (Req n Int closed - (atFloor n - queueing))";
by (ensures_tac "close_act" 1);
qed "E_thm03"; (*lem_lift_1_2*)
-Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
+Goal "Lprg : LeadsTo (Req n Int closed Int (atFloor n - queueing)) \
\ (opened Int atFloor n)";
by (ensures_tac "open_act" 1);
qed "E_thm04"; (*lem_lift_1_7*)
@@ -190,7 +191,7 @@
(*lem_lift_2_0
NOT an ensures property, but a mere inclusion;
don't know why script lift_2.uni says ENSURES*)
-Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
+Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing)) \
\ ((closed Int goingup Int Req n) Un \
\ (closed Int goingdown Int Req n))";
by (rtac subset_imp_LeadsTo 1);
@@ -198,7 +199,7 @@
qed "E_thm05c";
(*lift_2*)
-Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing)) \
+Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing)) \
\ (moving Int Req n)";
by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (ensures_tac "req_down" 2);
@@ -212,7 +213,7 @@
(*lem_lift_4_1 *)
Goal "#0 < N ==> \
-\ LeadsTo Lprg \
+\ Lprg : LeadsTo \
\ (moving Int Req n Int {s. metric n s = N} Int \
\ {s. floor s ~: req s} Int {s. up s}) \
\ (moving Int Req n Int {s. metric n s < N})";
@@ -232,7 +233,7 @@
(*lem_lift_4_3 *)
Goal "#0 < N ==> \
-\ LeadsTo Lprg \
+\ Lprg : LeadsTo \
\ (moving Int Req n Int {s. metric n s = N} Int \
\ {s. floor s ~: req s} - {s. up s}) \
\ (moving Int Req n Int {s. metric n s < N})";
@@ -250,7 +251,7 @@
qed "E_thm12b";
(*lift_4*)
-Goal "#0<N ==> LeadsTo Lprg (moving Int Req n Int {s. metric n s = N} Int \
+Goal "#0<N ==> Lprg : LeadsTo (moving Int Req n Int {s. metric n s = N} Int \
\ {s. floor s ~: req s}) \
\ (moving Int Req n Int {s. metric n s < N})";
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
@@ -264,7 +265,7 @@
(*lem_lift_5_3*)
Goal "#0<N \
-\ ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingup) \
+\ ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingup) \
\ (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "req_up" 1);
@@ -280,7 +281,7 @@
(*lem_lift_5_1 has ~goingup instead of goingdown*)
Goal "#0<N ==> \
-\ LeadsTo Lprg (closed Int Req n Int {s. metric n s = N} Int goingdown) \
+\ Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingdown) \
\ (moving Int Req n Int {s. metric n s < N})";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "req_down" 1);
@@ -309,7 +310,7 @@
(*lift_5*)
-Goal "#0<N ==> LeadsTo Lprg (closed Int Req n Int {s. metric n s = N}) \
+Goal "#0<N ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N}) \
\ (moving Int Req n Int {s. metric n s < N})";
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
by (etac E_thm16b 3);
@@ -341,7 +342,7 @@
(*lem_lift_3_1*)
-Goal "LeadsTo Lprg (moving Int Req n Int {s. metric n s = #0}) \
+Goal "Lprg : LeadsTo (moving Int Req n Int {s. metric n s = #0}) \
\ (stopped Int atFloor n)";
by (cut_facts_tac [bounded] 1);
by (ensures_tac "request_act" 1);
@@ -349,7 +350,7 @@
qed "E_thm11";
(*lem_lift_3_5*)
-Goal "LeadsTo Lprg \
+Goal "Lprg : LeadsTo \
\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
by (ensures_tac "request_act" 1);
@@ -358,7 +359,7 @@
(*lem_lift_3_6*)
Goal "#0 < N ==> \
-\ LeadsTo Lprg \
+\ Lprg : LeadsTo \
\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
\ (opened Int Req n Int {s. metric n s = N})";
by (ensures_tac "open_act" 1);
@@ -367,7 +368,7 @@
qed "E_thm14";
(*lem_lift_3_7*)
-Goal "LeadsTo Lprg \
+Goal "Lprg : LeadsTo \
\ (opened Int Req n Int {s. metric n s = N}) \
\ (closed Int Req n Int {s. metric n s = N})";
by (ensures_tac "close_act" 1);
@@ -378,7 +379,7 @@
(** the final steps **)
Goal "#0 < N ==> \
-\ LeadsTo Lprg \
+\ Lprg : LeadsTo \
\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
\ (moving Int Req n Int {s. metric n s < N})";
by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
@@ -399,7 +400,7 @@
val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken;
-Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)";
+Goal "Lprg : LeadsTo (moving Int Req n) (stopped Int atFloor n)";
by (rtac (reach_nonneg RS integ_0_le_induct) 1);
by (case_tac "#0 < z" 1);
(*If z <= #0 then actually z = #0*)
@@ -413,7 +414,7 @@
qed "lift_3";
-Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)";
+Goal "Lprg : LeadsTo (Req n) (opened Int atFloor n)";
by (rtac LeadsTo_Trans 1);
by (rtac (E_thm04 RS LeadsTo_Un) 2);
by (rtac LeadsTo_Un_post 2);