src/HOL/UNITY/Lift.ML
author paulson
Tue, 01 Sep 1998 10:10:11 +0200
changeset 5410 5ed7547a7f74
parent 5357 6efb2b87610c
child 5424 771a68a468cc
permissions -rw-r--r--
Moved lemmas to Arith.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Lift
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
     2
    ID:         $Id$
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
     5
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
     6
The Lift-Control Example
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
     7
*)
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
     8
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
     9
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    10
(*To move  0 < metric n s  out of the assumptions for case splitting*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    11
val rev_mp' = read_instantiate_sg (sign_of thy) 
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    12
                 [("P", "0 < metric ?n ?s")] rev_mp;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    13
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    14
val Suc_lessD_contra = Suc_lessD COMP rev_contrapos;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    15
val Suc_lessD_contra' = less_not_sym RS Suc_lessD_contra;
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
    16
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    17
val always_defs = [above_def, below_def, queueing_def, 
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    18
		   goingup_def, goingdown_def, ready_def];
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    19
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    20
val cmd_defs = [Lprg_def, 
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    21
		request_act_def, open_act_def, close_act_def,
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    22
		req_up_def, req_down_def, move_up_def, move_down_def,
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    23
		button_press_def];
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    24
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    25
Goalw [Lprg_def] "id : Acts Lprg";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    26
by (Simp_tac 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    27
qed "id_in_Acts";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    28
AddIffs [id_in_Acts];
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    29
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    30
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    31
val LeadsTo_Un_post' = id_in_Acts RS LeadsTo_Un_post
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    32
and LeadsTo_Trans_Un' = rotate_prems 1 (id_in_Acts RS LeadsTo_Trans_Un);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    33
(* [| LeadsTo Lprg B C; LeadsTo Lprg A B |] ==> LeadsTo Lprg (A Un B) C *)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    34
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    35
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    36
val metric_simps =
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    37
    [metric_def, vimage_def, 
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    38
     not_less_less_Suc_eq, less_not_sym RS not_less_less_Suc_eq,
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    39
     Suc_lessD_contra, Suc_lessD_contra',
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    40
     less_not_refl2, less_not_refl3];
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    41
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    42
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    43
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    44
(*split_all_tac causes a big blow-up*)
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    45
claset_ref() := claset() delSWrapper "split_all_tac";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    46
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    47
(*Simplification for records*)
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    48
Addsimps (thms"state.update_defs");
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    49
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    50
Addsimps [Suc_le_eq];
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    51
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    52
Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    53
	  moving_up_def, moving_down_def];
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    54
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    55
AddIffs [Min_le_Max];
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    56
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    57
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    58
val nat_exhaust_le_pred = 
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    59
    read_instantiate_sg (sign_of thy) [("P", "?m <= ?y-1")] nat.exhaust;
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    60
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    61
val nat_exhaust_pred_le = 
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    62
    read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    63
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    64
Goal "m < n ==> m <= n-1";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    65
by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    66
qed "less_imp_le_pred";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    67
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    68
Goalw [Lprg_def] "Invariant Lprg open_stop";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    69
by (rtac InvariantI 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    70
by (Force_tac 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    71
by (constrains_tac (cmd_defs@always_defs) 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    72
qed "open_stop";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    73
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    74
Goalw [Lprg_def] "Invariant Lprg stop_floor";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    75
by (rtac InvariantI 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    76
by (Force_tac 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    77
by (constrains_tac (cmd_defs@always_defs) 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    78
qed "stop_floor";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    79
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    80
(*This one needs open_stop, which was proved above*)
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    81
Goal "Invariant Lprg open_move";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    82
by (rtac InvariantI 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    83
br (open_stop RS Invariant_ConstrainsI RS StableI) 2;
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    84
bw Lprg_def;
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    85
by (Force_tac 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    86
by (constrains_tac (cmd_defs@always_defs) 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    87
qed "open_move";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    88
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    89
Goalw [Lprg_def] "Invariant Lprg moving_up";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    90
by (rtac InvariantI 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    91
by (Force_tac 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    92
by (constrains_tac (cmd_defs@always_defs) 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    93
by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    94
qed "moving_up";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    95
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    96
Goalw [Lprg_def] "Invariant Lprg moving_down";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    97
by (rtac InvariantI 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    98
by (Force_tac 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    99
by (constrains_tac (cmd_defs@always_defs) 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   100
by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   101
by (auto_tac (claset(),
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   102
	      simpset() addsimps [gr_implies_gr0 RS le_pred_eq]));
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   103
qed "moving_down";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   104
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   105
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   106
Goal "Invariant Lprg bounded";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
   107
by (rtac InvariantI 1);
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   108
br (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2;
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   109
bw Lprg_def;
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   110
by (Force_tac 1);
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   111
by (constrains_tac (cmd_defs@always_defs) 1);
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   112
by (TRYALL (resolve_tac [nat_exhaust_le_pred, nat_exhaust_pred_le]));
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   113
by (auto_tac (claset(), simpset() addsimps [less_Suc_eq]));
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   114
by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]));
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   115
qed "bounded";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   116
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   117
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   118
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   119
(*** Progress ***)
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   120
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   121
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   122
val abbrev_defs = [moving_def, stopped_def, 
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   123
		   opened_def, closed_def, atFloor_def, Req_def];
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   124
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   125
val defs = cmd_defs@always_defs@abbrev_defs;
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   126
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   127
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   128
(** The HUG'93 paper mistakenly omits the Req n from these! **)
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   129
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   130
(** Lift_1 **)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   131
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   132
(*lem_lift_1_5*)
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   133
Goal "LeadsTo Lprg (stopped Int atFloor n) (opened Int atFloor n)";
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   134
by (cut_facts_tac [stop_floor] 1);
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   135
by (ensures_tac defs "open_act" 1);
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   136
qed "E_thm01";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   137
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   138
(*lem_lift_1_1*)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   139
Goal "LeadsTo Lprg (Req n Int stopped - atFloor n) \
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   140
\                  (Req n Int opened - atFloor n)";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   141
by (cut_facts_tac [stop_floor] 1);
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   142
by (ensures_tac defs "open_act" 1);
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   143
qed "E_thm02";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   144
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   145
(*lem_lift_1_2*)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   146
Goal "LeadsTo Lprg (Req n Int opened - atFloor n) \
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   147
\                  (Req n Int closed - (atFloor n - queueing))";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   148
by (ensures_tac defs "close_act" 1);
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   149
qed "E_thm03";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   150
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   151
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   152
(*lem_lift_1_7*)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   153
Goal "LeadsTo Lprg (Req n Int closed Int (atFloor n - queueing)) \
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   154
\                  (opened Int atFloor n)";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   155
by (ensures_tac defs "open_act" 1);
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   156
qed "E_thm04";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   157
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   158
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   159
(** Lift 2.  Statements of thm05a and thm05b were wrong! **)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   160
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   161
Open_locale "floor"; 
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   162
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   163
val Min_le_n = thm "Min_le_n";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   164
val n_le_Max = thm "n_le_Max";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   165
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   166
AddIffs [Min_le_n, n_le_Max];
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   167
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   168
val le_MinD = Min_le_n RS le_anti_sym;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   169
val Max_leD = n_le_Max RSN (2,le_anti_sym);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   170
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   171
AddSDs [le_MinD, leI RS le_MinD,
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   172
	Max_leD, leI RS Max_leD];
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   173
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   174
(*lem_lift_2_0 
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   175
  NOT an ensures property, but a mere inclusion;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   176
  don't know why script lift_2.uni says ENSURES*)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   177
Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing))   \
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   178
\                  ((closed Int goingup Int Req n)  Un \
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   179
\                   (closed Int goingdown Int Req n))";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   180
br subset_imp_LeadsTo 1;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   181
by (auto_tac (claset() addSEs [nat_neqE], simpset() addsimps defs));
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   182
qed "E_thm05c";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   183
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   184
(*lift_2*)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   185
Goal "LeadsTo Lprg (Req n Int closed - (atFloor n - queueing))   \
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   186
\                  (moving Int Req n)";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   187
br ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1;
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   188
by (ensures_tac defs "req_down" 2);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   189
by (ensures_tac defs "req_up" 1);
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   190
qed "lift_2";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   191
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   192
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   193
(** Towards lift_4 ***)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   194
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   195
Goal "[| x ~: A;  y : A |] ==> x ~= y";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   196
by (Blast_tac 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   197
qed "not_mem_distinct";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   198
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   199
fun distinct_tac i =
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   200
    dtac le_neq_implies_less i THEN
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   201
    eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   202
    assume_tac i;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   203
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   204
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   205
(*lem_lift_4_1 *)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   206
Goal "0 < N ==> \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   207
\     LeadsTo Lprg \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   208
\       (moving Int Req n Int (metric n -`` {N}) Int \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   209
\        {s. floor s ~: req s} Int {s. up s})   \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   210
\       (moving Int Req n Int (metric n -`` lessThan N))";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   211
by (cut_facts_tac [moving_up] 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   212
by (ensures_tac defs "move_up" 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   213
(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   214
be (leI RS le_anti_sym RS sym) 1;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   215
by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   216
by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   217
by (REPEAT_FIRST (etac rev_mp'));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   218
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   219
by (distinct_tac 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   220
by (auto_tac
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   221
    (claset() addEs [diff_Suc_less_diff RS less_not_refl3 RSN (2, rev_notE)]
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   222
	      addIs [diff_Suc_less_diff], 
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   223
     simpset()));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   224
qed "E_thm12a";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   225
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   226
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   227
(*This rule helps eliminate occurrences of  (floor s - 1) *)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   228
val less_floor_imp = read_instantiate_sg (sign_of thy) 
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   229
                 [("n", "floor ?s")] less_eq_Suc_add RS exE;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   230
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   231
(*lem_lift_4_3 *)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   232
Goal "0 < N ==> \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   233
\     LeadsTo Lprg \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   234
\       (moving Int Req n Int (metric n -`` {N}) Int \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   235
\        {s. floor s ~: req s} - {s. up s})   \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   236
\       (moving Int Req n Int (metric n -`` lessThan N))";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   237
by (cut_facts_tac [moving_down] 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   238
by (ensures_tac defs "move_down" 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   239
by (ALLGOALS distinct_tac);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   240
by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   241
(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   242
be (leI RS le_anti_sym RS sym) 1;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   243
by (eres_inst_tac [("P", "?x < metric n s")] notE 2);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   244
by (eres_inst_tac [("P", "?x = metric n ?y")] rev_notE 3);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   245
by (REPEAT_FIRST (etac rev_mp'));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   246
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   247
by (auto_tac
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   248
    (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)]
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   249
              addIs [diff_le_Suc_diff, diff_less_Suc_diff],
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   250
	      simpset() addsimps [trans_le_add1]));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   251
qed "E_thm12b";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   252
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   253
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   254
(*lift_4*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   255
Goal "0<N ==> LeadsTo Lprg (moving Int Req n Int (metric n -`` {N}) Int \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   256
\                           {s. floor s ~: req s})     \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   257
\                          (moving Int Req n Int (metric n -`` lessThan N))";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   258
br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   259
by (etac E_thm12b 4);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   260
by (etac E_thm12a 3);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   261
by (rtac id_in_Acts 2);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   262
by (Blast_tac 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   263
qed "lift_4";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   264
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   265
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   266
(** towards lift_5 **)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   267
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   268
(*lem_lift_5_3*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   269
Goal "0<N   \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   270
\     ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingup) \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   271
\                      (moving Int Req n Int (metric n -`` lessThan N))";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   272
by (cut_facts_tac [bounded] 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   273
by (ensures_tac defs "req_up" 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   274
by (REPEAT_FIRST (etac rev_mp'));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   275
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   276
by (auto_tac (claset() addIs [diff_Suc_less_diff], 
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   277
	      simpset() addsimps [arith1, arith2]));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   278
qed "E_thm16a";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   279
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   280
    (*arith1 comes from
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   281
     1. !!s i.
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   282
	   [| n : req s; stop s; ~ open s; move s; floor s < i; i <= Max;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   283
	      i : req s; ALL i. i < floor s --> Min <= i --> i ~: req s;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   284
	      ~ n < Suc (floor s); ~ n < floor s; ~ up s; floor s < n;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   285
	      Suc (floor s) < n; 0 < floor s - Min |]
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   286
	   ==> n - Suc (floor s) < floor s - Min + (n - Min)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   287
    *)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   288
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   289
    (*arith2 comes from
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   290
     2. !!s i.
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   291
	   [| Min <= floor s; ...
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   292
	      n : req s; stop s; ~ open s; move s; floor s < i; i <= Max;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   293
	      i : req s; ALL i. i < floor s --> Min <= i --> i ~: req s;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   294
	      ~ n < floor s; ~ up s; floor s < n; ~ n < Suc (floor s);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   295
	      Suc (floor s) < n; Min < n |]
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   296
	   ==> n - Suc (floor s) < floor s - Min + (n - Min)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   297
    *)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   298
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   299
(*lem_lift_5_1 has ~goingup instead of goingdown*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   300
Goal "0<N ==>   \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   301
\     LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}) Int goingdown) \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   302
\                  (moving Int Req n Int (metric n -`` lessThan N))";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   303
by (cut_facts_tac [bounded] 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   304
by (ensures_tac defs "req_down" 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   305
by (ALLGOALS (etac less_floor_imp THEN' Clarify_tac THEN' Asm_full_simp_tac));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   306
by (REPEAT_FIRST (etac rev_mp'));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   307
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   308
by (auto_tac (claset() addIs [diff_Suc_less_diff, diff_less_Suc_diff], 
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   309
	      simpset() addsimps [trans_le_add1, arith3, arith4]));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   310
qed "E_thm16b";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   311
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   312
    (*arith3 comes from
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   313
     1. !!s i x.
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   314
	   [| floor s = Suc (i + x); Min <= Suc (i + x); stop s; i + x < Max;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   315
	      ~ open s; n : req s; move s; Min <= i; i : req s;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   316
	      ALL ia. ia <= Max --> Suc (i + x) < ia --> ia ~: req s;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   317
	      ~ Suc (i + x) < n; ~ i + x < n; n ~= i + x; up s; n < i + x;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   318
	      Suc (i + x) < Max |]
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   319
	   ==> i + x - n < Max - Suc (i + x) + (Max - n)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   320
    *)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   321
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   322
    (*arith4 comes from
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   323
     2. !!s i x.
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   324
	   [| floor s = Suc (i + x); Min <= Suc (i + x); stop s; i + x < Max;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   325
	      ~ open s; n : req s; move s; Min <= i; i : req s;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   326
	      ALL ia. ia <= Max --> Suc (i + x) < ia --> ia ~: req s;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   327
	      ~ Suc (i + x) < n; ~ i + x < n; n ~= i + x; up s; n < i + x;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   328
	      n < Max |]
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   329
	   ==> i + x - n < Max - Suc (i + x) + (Max - n)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   330
    *)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   331
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   332
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   333
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   334
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   335
  i.e. the trivial disjunction, leading to an asymmetrical proof.*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   336
Goal "0<N ==> Req n Int (metric n -``{N}) <= goingup Un goingdown";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   337
by (asm_simp_tac (simpset() addsimps (defs@metric_simps)) 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   338
by (Blast_tac 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   339
qed "E_thm16c";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   340
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   341
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   342
(*lift_5*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   343
Goal "0<N ==> LeadsTo Lprg (closed Int Req n Int (metric n -`` {N}))   \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   344
\                          (moving Int Req n Int (metric n -`` lessThan N))";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   345
br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   346
by (etac E_thm16b 4);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   347
by (etac E_thm16a 3);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   348
by (rtac id_in_Acts 2);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   349
bd E_thm16c 1;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   350
by (Blast_tac 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   351
qed "lift_5";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   352
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   353
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   354
(** towards lift_3 **)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   355
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   356
(*lemma used to prove lem_lift_3_1*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   357
Goal "[| metric n s = 0;  Min <= floor s;  floor s <= Max |] ==> floor s = n";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   358
be rev_mp 1;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   359
by (asm_simp_tac (simpset() addsimps metric_simps) 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   360
auto();
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   361
qed "metric_eq_0D";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   362
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   363
AddDs [metric_eq_0D];
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   364
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   365
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   366
(*lem_lift_3_1*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   367
Goal "LeadsTo Lprg (moving Int Req n Int (metric n -`` {0}))   \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   368
\                  (stopped Int atFloor n)";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   369
by (cut_facts_tac [bounded] 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   370
by (ensures_tac defs "request_act" 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   371
qed "E_thm11";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   372
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   373
(*lem_lift_3_5*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   374
Goal "LeadsTo Lprg \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   375
\       (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})   \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   376
\       (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   377
by (ensures_tac defs "request_act" 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   378
by (asm_simp_tac (simpset() addsimps metric_simps) 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   379
qed "E_thm13";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   380
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   381
(*lem_lift_3_6*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   382
Goal "0 < N ==> \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   383
\     LeadsTo Lprg \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   384
\       (stopped Int Req n Int (metric n -`` {N}) Int {s. floor s : req s}) \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   385
\       (opened Int Req n Int (metric n -`` {N}))";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   386
by (ensures_tac defs "open_act" 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   387
by (REPEAT_FIRST (etac rev_mp'));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   388
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps)));
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   389
qed "E_thm14";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   390
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   391
(*lem_lift_3_7*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   392
Goal "LeadsTo Lprg \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   393
\       (opened Int Req n Int (metric n -`` {N}))  \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   394
\       (closed Int Req n Int (metric n -`` {N}))";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   395
by (ensures_tac defs "close_act" 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   396
by (asm_simp_tac (simpset() addsimps metric_simps) 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   397
qed "E_thm15";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   398
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   399
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   400
(** the final steps **)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   401
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   402
Goal "0 < N ==> \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   403
\     LeadsTo Lprg \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   404
\       (moving Int Req n Int (metric n -`` {N}) Int {s. floor s : req s})   \
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   405
\       (moving Int Req n Int (metric n -`` lessThan N))";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   406
(*Blast_tac: PROOF FAILED*)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   407
by (best_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   408
	               addIs [LeadsTo_Trans]) 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   409
qed "lift_3_Req";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   410
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   411
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   412
Goal "LeadsTo Lprg (moving Int Req n) (stopped Int atFloor n)";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   413
br (allI RS LessThan_induct) 1;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   414
by (exhaust_tac "m" 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   415
auto();
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   416
br E_thm11 1;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   417
br ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   418
br ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   419
br lift_3_Req 4;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   420
br lift_4 3;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   421
auto();
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   422
qed "lift_3";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   423
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   424
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   425
Goal "LeadsTo Lprg (Req n) (opened Int atFloor n)";
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   426
br LeadsTo_Trans 1;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   427
br (E_thm04 RS LeadsTo_Un) 2;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   428
br LeadsTo_Un_post' 2;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   429
br (E_thm01 RS LeadsTo_Trans_Un') 2;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   430
br (lift_3 RS LeadsTo_Trans_Un') 2;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   431
br (lift_2 RS LeadsTo_Trans_Un') 2;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   432
br (E_thm03 RS LeadsTo_Trans_Un') 2;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   433
br E_thm02 2;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   434
br (open_move RS Invariant_LeadsToI) 1;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   435
br (open_stop RS Invariant_LeadsToI) 1;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   436
br subset_imp_LeadsTo 1;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   437
by (rtac id_in_Acts 2);
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   438
bws defs;
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   439
by (Clarify_tac 1);
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   440
	(*stops simplification from looping*)
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   441
by (Full_simp_tac 1);
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   442
by (REPEAT (Safe_step_tac 1 ORELSE Blast_tac 1));
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   443
qed "lift_1";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   444
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   445
Close_locale;
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   446
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   447