simplified thanks to the arithmetic prover
authorpaulson
Tue Jan 19 11:16:07 1999 +0100 (1999-01-19)
changeset 613926abad27b03c
parent 6138 b7e6e607bb4d
child 6140 af32e2c3f77a
simplified thanks to the arithmetic prover
src/HOL/UNITY/Lift.ML
     1.1 --- a/src/HOL/UNITY/Lift.ML	Tue Jan 19 11:15:40 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Lift.ML	Tue Jan 19 11:16:07 1999 +0100
     1.3 @@ -6,11 +6,6 @@
     1.4  The Lift-Control Example
     1.5  *)
     1.6  
     1.7 -Goal "~ z < w ==> (z < w + #1) = (z = w)";
     1.8 -by (asm_simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1);
     1.9 -qed "not_zless_zless1_eq";
    1.10 -
    1.11 -
    1.12  (*split_all_tac causes a big blow-up*)
    1.13  claset_ref() := claset() delSWrapper record_split_name;
    1.14  
    1.15 @@ -43,12 +38,7 @@
    1.16  val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4];
    1.17  
    1.18  
    1.19 -val zless_zadd1_contra = zless_zadd1_imp_zless COMP rev_contrapos;
    1.20 -val zless_zadd1_contra' = zless_not_sym RS zless_zadd1_contra;
    1.21 -
    1.22 -
    1.23 -val metric_simps =
    1.24 -    [metric_def, vimage_def];
    1.25 +val metric_simps = [metric_def, vimage_def];
    1.26  
    1.27  
    1.28  Addsimps [Lprg_def RS def_prg_Init];
    1.29 @@ -78,12 +68,6 @@
    1.30  AddIffs [Min_le_Max];
    1.31  
    1.32  
    1.33 -val nat_exhaust_le_pred = 
    1.34 -    read_instantiate_sg (sign_of thy) [("P", "?m <= ?y-1")] nat.exhaust;
    1.35 -
    1.36 -val nat_exhaust_pred_le = 
    1.37 -    read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
    1.38 -
    1.39  Goal "Lprg : Invariant open_stop";
    1.40  by (rtac InvariantI 1);
    1.41  by (Force_tac 1);
    1.42 @@ -125,11 +109,7 @@
    1.43  by (constrains_tac 1);
    1.44  by (ALLGOALS Clarify_tac);
    1.45  by (REPEAT_FIRST distinct_tac);
    1.46 -by (ALLGOALS 
    1.47 -    (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd]@zcompare_rls)));
    1.48 -by (ALLGOALS 
    1.49 -    (blast_tac (claset() addDs [zle_imp_zless_or_eq] 
    1.50 -                         addIs [zless_trans])));
    1.51 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd])));
    1.52  qed "bounded";
    1.53  
    1.54  
    1.55 @@ -153,18 +133,18 @@
    1.56  qed "E_thm01";  (*lem_lift_1_5*)
    1.57  
    1.58  Goal "Lprg : LeadsTo (Req n Int stopped - atFloor n) \
    1.59 -\                  (Req n Int opened - atFloor n)";
    1.60 +\                    (Req n Int opened - atFloor n)";
    1.61  by (cut_facts_tac [stop_floor] 1);
    1.62  by (ensures_tac "open_act" 1);
    1.63  qed "E_thm02";  (*lem_lift_1_1*)
    1.64  
    1.65  Goal "Lprg : LeadsTo (Req n Int opened - atFloor n) \
    1.66 -\                  (Req n Int closed - (atFloor n - queueing))";
    1.67 +\                    (Req n Int closed - (atFloor n - queueing))";
    1.68  by (ensures_tac "close_act" 1);
    1.69  qed "E_thm03";  (*lem_lift_1_2*)
    1.70  
    1.71  Goal "Lprg : LeadsTo (Req n Int closed Int (atFloor n - queueing)) \
    1.72 -\                  (opened Int atFloor n)";
    1.73 +\                    (opened Int atFloor n)";
    1.74  by (ensures_tac "open_act" 1);
    1.75  qed "E_thm04";  (*lem_lift_1_7*)
    1.76  
    1.77 @@ -188,15 +168,15 @@
    1.78    NOT an ensures property, but a mere inclusion;
    1.79    don't know why script lift_2.uni says ENSURES*)
    1.80  Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing))   \
    1.81 -\                  ((closed Int goingup Int Req n)  Un \
    1.82 -\                   (closed Int goingdown Int Req n))";
    1.83 +\                    ((closed Int goingup Int Req n)  Un \
    1.84 +\                     (closed Int goingdown Int Req n))";
    1.85  by (rtac subset_imp_LeadsTo 1);
    1.86  by (auto_tac (claset() addSEs [int_neqE], simpset()));
    1.87  qed "E_thm05c";
    1.88  
    1.89  (*lift_2*)
    1.90  Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing))   \
    1.91 -\                  (moving Int Req n)";
    1.92 +\                    (moving Int Req n)";
    1.93  by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
    1.94  by (ensures_tac "req_down" 2);
    1.95  by (ensures_tac "req_up" 1);
    1.96 @@ -210,9 +190,9 @@
    1.97  (*lem_lift_4_1 *)
    1.98  Goal "#0 < N ==> \
    1.99  \     Lprg : LeadsTo \
   1.100 -\       (moving Int Req n Int {s. metric n s = N} Int \
   1.101 -\         {s. floor s ~: req s} Int {s. up s})   \
   1.102 -\       (moving Int Req n Int {s. metric n s < N})";
   1.103 +\              (moving Int Req n Int {s. metric n s = N} Int \
   1.104 +\               {s. floor s ~: req s} Int {s. up s})   \
   1.105 +\              (moving Int Req n Int {s. metric n s < N})";
   1.106  by (cut_facts_tac [moving_up] 1);
   1.107  by (ensures_tac "move_up" 1);
   1.108  by Safe_tac;
   1.109 @@ -230,9 +210,9 @@
   1.110  (*lem_lift_4_3 *)
   1.111  Goal "#0 < N ==> \
   1.112  \     Lprg : LeadsTo \
   1.113 -\       (moving Int Req n Int {s. metric n s = N} Int \
   1.114 -\        {s. floor s ~: req s} - {s. up s})   \
   1.115 -\       (moving Int Req n Int {s. metric n s < N})";
   1.116 +\              (moving Int Req n Int {s. metric n s = N} Int \
   1.117 +\               {s. floor s ~: req s} - {s. up s})   \
   1.118 +\              (moving Int Req n Int {s. metric n s < N})";
   1.119  by (cut_facts_tac [moving_down] 1);
   1.120  by (ensures_tac "move_down" 1);
   1.121  by Safe_tac;
   1.122 @@ -241,9 +221,7 @@
   1.123  by (REPEAT_FIRST (eresolve_tac mov_metrics));
   1.124  by (REPEAT_FIRST distinct_tac);
   1.125  (** LEVEL 6 **)
   1.126 -by (ALLGOALS (asm_simp_tac (simpset() addsimps 
   1.127 -			    [zle_def] @ metric_simps @ zcompare_rls)));
   1.128 -by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
   1.129 +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
   1.130  qed "E_thm12b";
   1.131  
   1.132  (*lift_4*)
   1.133 @@ -267,8 +245,7 @@
   1.134  by (ensures_tac "req_up" 1);
   1.135  by Auto_tac;
   1.136  by (REPEAT_FIRST (eresolve_tac mov_metrics));
   1.137 -by (ALLGOALS
   1.138 -    (asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls)));
   1.139 +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
   1.140  (** LEVEL 5 **)
   1.141  by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1);
   1.142  by (Blast_tac 1);
   1.143 @@ -282,9 +259,7 @@
   1.144  by (ensures_tac "req_down" 1);
   1.145  by Auto_tac;
   1.146  by (REPEAT_FIRST (eresolve_tac mov_metrics));
   1.147 -by (ALLGOALS
   1.148 -    (asm_simp_tac (simpset() addsimps [zle_def] @ 
   1.149 -		                      metric_simps @ zcompare_rls)));
   1.150 +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
   1.151  (** LEVEL 5 **)
   1.152  by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
   1.153  by (Blast_tac 1);
   1.154 @@ -297,7 +272,7 @@
   1.155  Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
   1.156  by (asm_simp_tac (simpset() addsimps metric_simps) 1);
   1.157  by (force_tac (claset() delrules [impCE] addEs [impCE], 
   1.158 -	      simpset() addsimps conj_comms) 1);
   1.159 +	       simpset() addsimps conj_comms) 1);
   1.160  qed "E_thm16c";
   1.161  
   1.162