src/HOL/UNITY/Lift.ML
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5320 79b326bceafb
     1.1 --- a/src/HOL/UNITY/Lift.ML	Thu Aug 13 17:44:50 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Lift.ML	Thu Aug 13 18:06:40 1998 +0200
     1.3 @@ -44,34 +44,36 @@
     1.4  qed "less_imp_le_pred";
     1.5  
     1.6  
     1.7 -Goalw [Lprg_def] "invariant Lprg open_stop";
     1.8 -by (rtac invariantI 1);
     1.9 +Goalw [Lprg_def] "Invariant Lprg open_stop";
    1.10 +by (rtac InvariantI 1);
    1.11  by (Force_tac 1);
    1.12  by (constrains_tac (cmd_defs@always_defs) 1);
    1.13  qed "open_stop";
    1.14  
    1.15 -Goalw [Lprg_def] "invariant Lprg stop_floor";
    1.16 -by (rtac invariantI 1);
    1.17 +Goalw [Lprg_def] "Invariant Lprg stop_floor";
    1.18 +by (rtac InvariantI 1);
    1.19  by (Force_tac 1);
    1.20  by (constrains_tac (cmd_defs@always_defs) 1);
    1.21  qed "stop_floor";
    1.22  
    1.23 -(*Should not have to prove open_stop concurrently!!*)
    1.24 -Goalw [Lprg_def] "invariant Lprg (open_stop Int open_move)";
    1.25 -by (rtac invariantI 1);
    1.26 +(*This one needs open_stop, which was proved above*)
    1.27 +Goal "Invariant Lprg open_move";
    1.28 +by (rtac InvariantI 1);
    1.29 +br (open_stop RS Invariant_ConstrainsI RS StableI) 2;
    1.30 +bw Lprg_def;
    1.31  by (Force_tac 1);
    1.32  by (constrains_tac (cmd_defs@always_defs) 1);
    1.33  qed "open_move";
    1.34  
    1.35 -Goalw [Lprg_def] "invariant Lprg moving_up";
    1.36 -by (rtac invariantI 1);
    1.37 +Goalw [Lprg_def] "Invariant Lprg moving_up";
    1.38 +by (rtac InvariantI 1);
    1.39  by (Force_tac 1);
    1.40  by (constrains_tac (cmd_defs@always_defs) 1);
    1.41  by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1);
    1.42  qed "moving_up";
    1.43  
    1.44 -Goalw [Lprg_def] "invariant Lprg moving_down";
    1.45 -by (rtac invariantI 1);
    1.46 +Goalw [Lprg_def] "Invariant Lprg moving_down";
    1.47 +by (rtac InvariantI 1);
    1.48  by (Force_tac 1);
    1.49  by (constrains_tac (cmd_defs@always_defs) 1);
    1.50  by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3);
    1.51 @@ -82,8 +84,8 @@
    1.52  
    1.53  xxxxxxxxxxxxxxxx;
    1.54  
    1.55 -Goalw [Lprg_def] "invariant Lprg bounded";
    1.56 -by (rtac invariantI 1);
    1.57 +Goalw [Lprg_def] "Invariant Lprg bounded";
    1.58 +by (rtac InvariantI 1);
    1.59  by (Force_tac 1);
    1.60  by (constrains_tac (cmd_defs@always_defs) 1);
    1.61  by (ALLGOALS
    1.62 @@ -94,8 +96,8 @@
    1.63  by (blast_tac (claset() addIs [diff_le_self, le_trans]) 3);
    1.64  qed "bounded";
    1.65  
    1.66 -Goalw [Lprg_def] "invariant Lprg invariantV";
    1.67 -by (rtac invariantI 1);
    1.68 +Goalw [Lprg_def] "Invariant Lprg invariantV";
    1.69 +by (rtac InvariantI 1);
    1.70  by (constrains_tac cmd_defs 2);
    1.71  by Auto_tac;
    1.72  qed "invariantV";
    1.73 @@ -122,7 +124,7 @@
    1.74  
    1.75  Goal "LeadsTo Lprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
    1.76  by (cut_facts_tac [invariantUV] 1);
    1.77 -bw Lprg_def;
    1.78 +by (rewtac Lprg_def);
    1.79  by (ensures_tac cmd_defs "cmd2U" 1);
    1.80  qed "U_F2";
    1.81