# HG changeset patch
# User paulson
# Date 927554184 -7200
# Node ID e869ff059252fa4ed1a1b80bd01f9968d7524923
# Parent  70b251dc7055f6ea03ba09a0b5146b2979a98d13
renamed Lprg to Lift; simplified proof of Always_nonneg

diff -r 70b251dc7055 -r e869ff059252 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Mon May 24 15:54:58 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML	Mon May 24 15:56:24 1999 +0200
@@ -38,8 +38,8 @@
 val metric_simps = [metric_def, vimage_def];
 
 
-Addsimps [Lprg_def RS def_prg_Init];
-program_defs_ref := [Lprg_def];
+Addsimps [Lift_def RS def_prg_Init];
+program_defs_ref := [Lift_def];
 
 Addsimps (map simp_of_act
 	  [request_act_def, open_act_def, close_act_def,
@@ -53,7 +53,7 @@
 
 
 val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
-(* [| Lprg: B LeadsTo C; Lprg: A LeadsTo B |] ==> Lprg: (A Un B) LeadsTo C *)
+(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *)
 
 
 (*Simplification for records*)
@@ -65,41 +65,41 @@
 AddIffs [Min_le_Max];
 
 
-Goal "Lprg : Always open_stop";
+Goal "Lift : Always open_stop";
 by (rtac AlwaysI 1);
 by (Force_tac 1);
 by (constrains_tac 1);
 qed "open_stop";
 
-Goal "Lprg : Always stop_floor";
+Goal "Lift : Always stop_floor";
 by (rtac AlwaysI 1);
 by (Force_tac 1);
 by (constrains_tac 1);
 qed "stop_floor";
 
 (*This one needs open_stop, which was proved above*)
-Goal "Lprg : Always open_move";
+Goal "Lift : Always open_move";
 by (rtac AlwaysI 1);
 by (rtac (open_stop RS Always_ConstrainsI RS StableI) 2);
 by (Force_tac 1);
 by (constrains_tac 1);
 qed "open_move";
 
-Goal "Lprg : Always moving_up";
+Goal "Lift : Always moving_up";
 by (rtac AlwaysI 1);
 by (Force_tac 1);
 by (constrains_tac 1);
 by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
 qed "moving_up";
 
-Goal "Lprg : Always moving_down";
+Goal "Lift : Always moving_down";
 by (rtac AlwaysI 1);
 by (Force_tac 1);
 by (constrains_tac 1);
 by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
 qed "moving_down";
 
-Goal "Lprg : Always bounded";
+Goal "Lift : Always bounded";
 by (rtac AlwaysI 1);
 by (rtac (Always_Int_rule [moving_up, moving_down] RS Always_StableI) 2);
 by (Force_tac 1);
@@ -124,23 +124,23 @@
 
 (** Lift_1 **)
 
-Goal "Lprg : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)";
+Goal "Lift : (stopped Int atFloor n) LeadsTo (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 "Lprg : (Req n Int stopped - atFloor n) LeadsTo \
+Goal "Lift : (Req n Int stopped - atFloor n) LeadsTo \
 \                    (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 "Lprg : (Req n Int opened - atFloor n) LeadsTo \
+Goal "Lift : (Req n Int opened - atFloor n) LeadsTo \
 \                    (Req n Int closed - (atFloor n - queueing))";
 by (ensures_tac "close_act" 1);
 qed "E_thm03";  (*lem_lift_1_2*)
 
-Goal "Lprg : (Req n Int closed Int (atFloor n - queueing))  \
+Goal "Lift : (Req n Int closed Int (atFloor n - queueing))  \
 \            LeadsTo (opened Int atFloor n)";
 by (ensures_tac "open_act" 1);
 qed "E_thm04";  (*lem_lift_1_7*)
@@ -166,7 +166,7 @@
 (*lem_lift_2_0 
   NOT an ensures property, but a mere inclusion;
   don't know why script lift_2.uni says ENSURES*)
-Goal "Lprg : (Req n Int closed - (atFloor n - queueing))   \
+Goal "Lift : (Req n Int closed - (atFloor n - queueing))   \
 \            LeadsTo ((closed Int goingup Int Req n)  Un \
 \                     (closed Int goingdown Int Req n))";
 by (rtac subset_imp_LeadsTo 1);
@@ -174,7 +174,7 @@
 qed "E_thm05c";
 
 (*lift_2*)
-Goal "Lprg : (Req n Int closed - (atFloor n - queueing))   \
+Goal "Lift : (Req n Int closed - (atFloor n - queueing))   \
 \            LeadsTo (moving Int Req n)";
 by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
 by (ensures_tac "req_down" 2);
@@ -188,7 +188,7 @@
 
 (*lem_lift_4_1 *)
 Goal "#0 < N ==> \
-\     Lprg : (moving Int Req n Int {s. metric n s = N} Int \
+\     Lift : (moving Int Req n Int {s. metric n s = N} Int \
 \             {s. floor s ~: req s} Int {s. up s})   \
 \            LeadsTo \
 \              (moving Int Req n Int {s. metric n s < N})";
@@ -208,7 +208,7 @@
 
 (*lem_lift_4_3 *)
 Goal "#0 < N ==> \
-\     Lprg : (moving Int Req n Int {s. metric n s = N} Int \
+\     Lift : (moving Int Req n Int {s. metric n s = N} Int \
 \             {s. floor s ~: req s} - {s. up s})   \
 \            LeadsTo (moving Int Req n Int {s. metric n s < N})";
 by (cut_facts_tac [moving_down] 1);
@@ -223,7 +223,7 @@
 qed "E_thm12b";
 
 (*lift_4*)
-Goal "#0<N ==> Lprg : (moving Int Req n Int {s. metric n s = N} Int \
+Goal "#0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int \
 \                           {s. floor s ~: req s}) LeadsTo     \
 \                          (moving Int Req n Int {s. metric n s < N})";
 by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
@@ -237,7 +237,7 @@
 
 (*lem_lift_5_3*)
 Goal "#0<N   \
-\     ==> Lprg : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \
+\     ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \
 \                      (moving Int Req n Int {s. metric n s < N})";
 by (cut_facts_tac [bounded] 1);
 by (ensures_tac "req_up" 1);
@@ -249,7 +249,7 @@
 
 (*lem_lift_5_1 has ~goingup instead of goingdown*)
 Goal "#0<N ==>   \
-\     Lprg : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \
+\     Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \
 \                  (moving Int Req n Int {s. metric n s < N})";
 by (cut_facts_tac [bounded] 1);
 by (ensures_tac "req_down" 1);
@@ -271,7 +271,7 @@
 
 
 (*lift_5*)
-Goal "#0<N ==> Lprg : (closed Int Req n Int {s. metric n s = N}) LeadsTo   \
+Goal "#0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo   \
 \                          (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);
@@ -294,7 +294,7 @@
 
 
 (*lem_lift_3_1*)
-Goal "Lprg : (moving Int Req n Int {s. metric n s = #0}) LeadsTo   \
+Goal "Lift : (moving Int Req n Int {s. metric n s = #0}) LeadsTo   \
 \                  (stopped Int atFloor n)";
 by (cut_facts_tac [bounded] 1);
 by (ensures_tac "request_act" 1);
@@ -303,7 +303,7 @@
 
 (*lem_lift_3_5*)
 Goal
-  "Lprg : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
+  "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
 \ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
 by (ensures_tac "request_act" 1);
 by (auto_tac (claset(), simpset() addsimps metric_simps));
@@ -311,7 +311,7 @@
 
 (*lem_lift_3_6*)
 Goal "#0 < N ==> \
-\     Lprg : \
+\     Lift : \
 \       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
 \       LeadsTo (opened Int Req n Int {s. metric n s = N})";
 by (ensures_tac "open_act" 1);
@@ -320,7 +320,7 @@
 qed "E_thm14";
 
 (*lem_lift_3_7*)
-Goal "Lprg : (opened Int Req n Int {s. metric n s = N})  \
+Goal "Lift : (opened Int Req n Int {s. metric n s = N})  \
 \            LeadsTo (closed Int Req n Int {s. metric n s = N})";
 by (ensures_tac "close_act" 1);
 by (auto_tac (claset(), simpset() addsimps metric_simps));
@@ -330,7 +330,7 @@
 (** the final steps **)
 
 Goal "#0 < N ==> \
-\     Lprg : \
+\     Lift : \
 \       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
 \       LeadsTo (moving Int Req n Int {s. metric n s < N})";
 by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
@@ -340,18 +340,14 @@
 
 
 (*Now we observe that our integer metric is really a natural number*)
-Goal "Lprg : Always {s. #0 <= metric n s}";
+Goal "Lift : Always {s. #0 <= metric n s}";
 by (rtac (bounded RS Always_weaken) 1);
-by (simp_tac (simpset() addsimps metric_simps @ zcompare_rls) 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [zless_iff_Suc_zadd, zle_iff_zadd]));
-by (REPEAT_FIRST (etac ssubst));
-by (auto_tac (claset(), simpset() addsimps [zadd_int]));
+by (auto_tac (claset(), simpset() addsimps metric_simps));
 qed "Always_nonneg";
 
 val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken;
 
-Goal "Lprg : (moving Int Req n) LeadsTo (stopped Int atFloor n)";
+Goal "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)";
 by (rtac (Always_nonneg RS integ_0_le_induct) 1);
 by (case_tac "#0 < z" 1);
 (*If z <= #0 then actually z = #0*)
@@ -365,7 +361,7 @@
 qed "lift_3";
 
 
-Goal "Lprg : (Req n) LeadsTo (opened Int atFloor n)";
+Goal "Lift : (Req n) LeadsTo (opened Int atFloor n)";
 by (rtac LeadsTo_Trans 1);
 by (rtac (E_thm04 RS LeadsTo_Un) 2);
 by (rtac LeadsTo_Un_post 2);
diff -r 70b251dc7055 -r e869ff059252 src/HOL/UNITY/Lift.thy
--- a/src/HOL/UNITY/Lift.thy	Mon May 24 15:54:58 1999 +0200
+++ b/src/HOL/UNITY/Lift.thy	Mon May 24 15:56:24 1999 +0200
@@ -114,9 +114,9 @@
 		        & Min <= n & n <= Max}"
 
 
-  Lprg :: state program
+  Lift :: state program
     (*for the moment, we OMIT button_press*)
-    "Lprg == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
+    "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
 		          ~ open s & req s = {}},
 			 {request_act, open_act, close_act,
 			  req_up, req_down, move_up, move_down})"