src/HOL/UNITY/Lift.ML
author wenzelm
Tue, 17 Nov 1998 14:07:25 +0100
changeset 5906 1f58694fc3e2
parent 5783 95ac0bf10518
child 6024 cb87f103d114
permissions -rw-r--r--
Drule.rev_triv_goal;
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
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
     9
Goal "~ z < w ==> (z < w + #1) = (z = w)";
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    10
by (asm_simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    11
qed "not_zless_zless1_eq";
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    12
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    13
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    14
(*split_all_tac causes a big blow-up*)
5706
21706a735c8d record_split_name;
wenzelm
parents: 5701
diff changeset
    15
claset_ref() := claset() delSWrapper record_split_name;
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    16
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    17
Delsimps [split_paired_All];
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    18
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    19
Goal "[| x ~: A;  y : A |] ==> x ~= y";
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    20
by (Blast_tac 1);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    21
qed "not_mem_distinct";
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    22
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    23
fun distinct_tac i =
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    24
    dtac zle_neq_implies_zless i THEN
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    25
    eresolve_tac [not_mem_distinct, not_mem_distinct RS not_sym] i THEN
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    26
    assume_tac i;
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    27
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    28
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    29
(** Rules to move "metric n s" out of the assumptions, for case splitting **)
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    30
val mov_metric1 = read_instantiate_sg (sign_of thy) 
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5583
diff changeset
    31
                   [("P", "?x < metric ?n ?s")] rev_mp;
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    32
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    33
val mov_metric2 = read_instantiate_sg (sign_of thy) 
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5583
diff changeset
    34
                   [("P", "?x = metric ?n ?s")] rev_mp;
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    35
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    36
val mov_metric3 = read_instantiate_sg (sign_of thy) 
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5583
diff changeset
    37
                   [("P", "~ (?x < metric ?n ?s)")] rev_mp;
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    38
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    39
val mov_metric4 = read_instantiate_sg (sign_of thy) 
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5583
diff changeset
    40
                   [("P", "(?x <= metric ?n ?s)")] rev_mp;
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    41
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    42
(*The order in which they are applied seems to be critical...*)
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    43
val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4];
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    44
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    45
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    46
val zless_zadd1_contra = zless_zadd1_imp_zless COMP rev_contrapos;
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    47
val zless_zadd1_contra' = zless_not_sym RS zless_zadd1_contra;
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    48
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    49
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    50
val metric_simps =
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    51
    [metric_def, vimage_def, order_less_imp_not_less, order_less_imp_triv, 
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    52
     order_less_imp_not_eq, order_less_imp_not_eq2,
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    53
     not_zless_zless1_eq, zless_not_sym RS not_zless_zless1_eq,
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    54
     zless_zadd1_contra, zless_zadd1_contra',
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    55
     zless_not_refl2, zless_not_refl3];
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
    56
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
    57
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
    58
Addsimps [Lprg_def RS def_prg_Init];
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
    59
program_defs_ref := [Lprg_def];
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    60
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    61
Addsimps (map simp_of_act
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    62
	  [request_act_def, open_act_def, close_act_def,
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    63
	   req_up_def, req_down_def, move_up_def, move_down_def,
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    64
	   button_press_def]);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    65
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    66
val always_defs = [above_def, below_def, queueing_def, 
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    67
		   goingup_def, goingdown_def, ready_def];
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    68
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    69
Addsimps (map simp_of_set always_defs);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    70
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    71
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
    72
val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
    73
(* [| Lprg : LeadsTo B C; Lprg : LeadsTo A B |] ==> Lprg : LeadsTo (A Un B) C *)
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    74
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    75
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    76
(*Simplification for records*)
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    77
Addsimps (thms"state.update_defs");
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    78
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    79
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
    80
	  moving_up_def, moving_down_def];
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    81
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
    82
AddIffs [Min_le_Max];
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    83
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    84
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    85
val nat_exhaust_le_pred = 
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    86
    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
    87
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    88
val nat_exhaust_pred_le = 
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
    89
    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
    90
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
    91
Goal "Lprg : Invariant open_stop";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    92
by (rtac InvariantI 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    93
by (Force_tac 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
    94
by (constrains_tac 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    95
qed "open_stop";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    96
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
    97
Goal "Lprg : Invariant stop_floor";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
    98
by (rtac InvariantI 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
    99
by (Force_tac 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   100
by (constrains_tac 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   101
qed "stop_floor";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   102
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
   103
(*This one needs open_stop, which was proved above*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   104
Goal "Lprg : Invariant open_move";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
   105
by (rtac InvariantI 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   106
by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   107
by (Force_tac 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   108
by (constrains_tac 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   109
qed "open_move";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   110
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   111
Goal "Lprg : Invariant moving_up";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
   112
by (rtac InvariantI 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   113
by (Force_tac 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   114
by (constrains_tac 1);
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   115
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   116
qed "moving_up";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   117
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   118
Goal "Lprg : Invariant moving_down";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
   119
by (rtac InvariantI 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   120
by (Force_tac 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   121
by (constrains_tac 1);
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   122
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   123
qed "moving_down";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   124
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   125
Goal "Lprg : Invariant bounded";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
   126
by (rtac InvariantI 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   127
by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   128
by (Force_tac 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   129
by (constrains_tac 1);
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   130
by (ALLGOALS Clarify_tac);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   131
by (REPEAT_FIRST distinct_tac);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   132
by (ALLGOALS 
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   133
    (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd]@zcompare_rls)));
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   134
by (ALLGOALS 
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   135
    (blast_tac (claset() addDs [zle_imp_zless_or_eq] 
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   136
                         addIs [zless_trans])));
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   137
qed "bounded";
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   138
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   139
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   140
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   141
(*** Progress ***)
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   142
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   143
5320
79b326bceafb now trans_tac is part of the claset...
paulson
parents: 5313
diff changeset
   144
val abbrev_defs = [moving_def, stopped_def, 
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   145
		   opened_def, closed_def, atFloor_def, Req_def];
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   146
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   147
Addsimps (map simp_of_set abbrev_defs);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
diff changeset
   148
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   149
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   150
(** 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
   151
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   152
(** Lift_1 **)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   153
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   154
Goal "Lprg : LeadsTo (stopped Int atFloor n) (opened Int atFloor n)";
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   155
by (cut_facts_tac [stop_floor] 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   156
by (ensures_tac "open_act" 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   157
qed "E_thm01";  (*lem_lift_1_5*)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   158
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   159
Goal "Lprg : LeadsTo (Req n Int stopped - atFloor n) \
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   160
\                  (Req n Int opened - atFloor n)";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   161
by (cut_facts_tac [stop_floor] 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   162
by (ensures_tac "open_act" 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   163
qed "E_thm02";  (*lem_lift_1_1*)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   164
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   165
Goal "Lprg : LeadsTo (Req n Int opened - atFloor n) \
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   166
\                  (Req n Int closed - (atFloor n - queueing))";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   167
by (ensures_tac "close_act" 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   168
qed "E_thm03";  (*lem_lift_1_2*)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   169
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   170
Goal "Lprg : LeadsTo (Req n Int closed Int (atFloor n - queueing)) \
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   171
\                  (opened Int atFloor n)";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   172
by (ensures_tac "open_act" 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   173
qed "E_thm04";  (*lem_lift_1_7*)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   174
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   175
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   176
(** Lift 2.  Statements of thm05a and thm05b were wrong! **)
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   177
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   178
Open_locale "floor"; 
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   179
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   180
val Min_le_n = thm "Min_le_n";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   181
val n_le_Max = thm "n_le_Max";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   182
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   183
AddIffs [Min_le_n, n_le_Max];
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   184
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   185
val le_MinD = Min_le_n RS zle_anti_sym;
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   186
val Max_leD = n_le_Max RSN (2,zle_anti_sym);
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   187
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   188
AddSDs [le_MinD, zleI RS le_MinD,
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   189
	Max_leD, zleI RS Max_leD];
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   190
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   191
(*lem_lift_2_0 
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   192
  NOT an ensures property, but a mere inclusion;
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   193
  don't know why script lift_2.uni says ENSURES*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   194
Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing))   \
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   195
\                  ((closed Int goingup Int Req n)  Un \
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   196
\                   (closed Int goingdown Int Req n))";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   197
by (rtac subset_imp_LeadsTo 1);
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   198
by (auto_tac (claset() addSEs [int_neqE], simpset()));
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   199
qed "E_thm05c";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   200
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   201
(*lift_2*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   202
Goal "Lprg : LeadsTo (Req n Int closed - (atFloor n - queueing))   \
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   203
\                  (moving Int Req n)";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   204
by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   205
by (ensures_tac "req_down" 2);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   206
by (ensures_tac "req_up" 1);
5424
771a68a468cc modified proofs for new constrains_tac and ensures_tac
paulson
parents: 5410
diff changeset
   207
by Auto_tac;
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   208
qed "lift_2";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   209
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   210
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   211
(** Towards lift_4 ***)
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   212
 
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   213
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   214
(*lem_lift_4_1 *)
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   215
Goal "#0 < N ==> \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   216
\     Lprg : LeadsTo \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   217
\       (moving Int Req n Int {s. metric n s = N} Int \
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   218
\         {s. floor s ~: req s} Int {s. up s})   \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   219
\       (moving Int Req n Int {s. metric n s < N})";
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   220
by (cut_facts_tac [moving_up] 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   221
by (ensures_tac "move_up" 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   222
by Safe_tac;
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   223
(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   224
by (etac (zleI RS zle_anti_sym RS sym) 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   225
by (REPEAT_FIRST (eresolve_tac mov_metrics));
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   226
by (REPEAT_FIRST distinct_tac);
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   227
(** LEVEL 6 **)
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   228
by (ALLGOALS (asm_simp_tac (simpset() addsimps 
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   229
			    [zle_def] @ metric_simps @ zcompare_rls)));
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   230
qed "E_thm12a";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   231
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   232
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   233
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   234
(*lem_lift_4_3 *)
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   235
Goal "#0 < N ==> \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   236
\     Lprg : LeadsTo \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   237
\       (moving Int Req n Int {s. metric n s = N} Int \
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   238
\        {s. floor s ~: req s} - {s. up s})   \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   239
\       (moving Int Req n Int {s. metric n s < N})";
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   240
by (cut_facts_tac [moving_down] 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   241
by (ensures_tac "move_down" 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   242
by Safe_tac;
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   243
(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   244
by (etac (zleI RS zle_anti_sym RS sym) 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   245
by (REPEAT_FIRST (eresolve_tac mov_metrics));
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   246
by (REPEAT_FIRST distinct_tac);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   247
(** LEVEL 6 **)
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   248
by (ALLGOALS (asm_simp_tac (simpset() addsimps 
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   249
			    [zle_def] @ metric_simps @ zcompare_rls)));
5783
95ac0bf10518 no need for int_0
paulson
parents: 5758
diff changeset
   250
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
5357
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
(*lift_4*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   254
Goal "#0<N ==> Lprg : LeadsTo (moving Int Req n Int {s. metric n s = N} Int \
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   255
\                           {s. floor s ~: req s})     \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   256
\                          (moving Int Req n Int {s. metric n s < N})";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   257
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   258
by (etac E_thm12b 3);
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   259
by (etac E_thm12a 2);
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   260
by (Blast_tac 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   261
qed "lift_4";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   262
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   263
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   264
(** towards lift_5 **)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   265
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   266
(*lem_lift_5_3*)
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   267
Goal "#0<N   \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   268
\     ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingup) \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   269
\                      (moving Int Req n Int {s. metric n s < N})";
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   270
by (cut_facts_tac [bounded] 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   271
by (ensures_tac "req_up" 1);
5424
771a68a468cc modified proofs for new constrains_tac and ensures_tac
paulson
parents: 5410
diff changeset
   272
by Auto_tac;
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   273
by (REPEAT_FIRST (eresolve_tac mov_metrics));
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   274
by (ALLGOALS
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   275
    (asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls)));
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   276
(** LEVEL 5 **)
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   277
by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 1);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   278
by Auto_tac;
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   279
by (full_simp_tac (simpset() addsimps [zadd_int_left]) 1);
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   280
qed "E_thm16a";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   281
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   282
(*lem_lift_5_1 has ~goingup instead of goingdown*)
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   283
Goal "#0<N ==>   \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   284
\     Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N} Int goingdown) \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   285
\                  (moving Int Req n Int {s. metric n s < N})";
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   286
by (cut_facts_tac [bounded] 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   287
by (ensures_tac "req_down" 1);
5424
771a68a468cc modified proofs for new constrains_tac and ensures_tac
paulson
parents: 5410
diff changeset
   288
by Auto_tac;
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   289
by (REPEAT_FIRST (eresolve_tac mov_metrics));
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   290
by (ALLGOALS
5783
95ac0bf10518 no need for int_0
paulson
parents: 5758
diff changeset
   291
    (asm_simp_tac (simpset() addsimps [zle_def] @ 
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5583
diff changeset
   292
		                      metric_simps @ zcompare_rls)));
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   293
(** LEVEL 5 **)
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   294
by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   295
by (etac exE 1);  
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   296
by (etac ssubst 1);
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   297
by Auto_tac;
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   298
by (full_simp_tac (simpset() addsimps [zadd_int_left]) 1);
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   299
qed "E_thm16b";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   300
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   301
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   302
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   303
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   304
  i.e. the trivial disjunction, leading to an asymmetrical proof.*)
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   305
Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   306
by (asm_simp_tac (simpset() addsimps metric_simps) 1);
5758
27a2b36efd95 corrected auto_tac (applications of unsafe wrappers)
oheimb
parents: 5706
diff changeset
   307
by (force_tac (claset() delrules [impCE] addEs [impCE], 
27a2b36efd95 corrected auto_tac (applications of unsafe wrappers)
oheimb
parents: 5706
diff changeset
   308
	      simpset() addsimps conj_comms) 1);
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   309
qed "E_thm16c";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   310
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   311
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   312
(*lift_5*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   313
Goal "#0<N ==> Lprg : LeadsTo (closed Int Req n Int {s. metric n s = N})   \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   314
\                          (moving Int Req n Int {s. metric n s < N})";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   315
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   316
by (etac E_thm16b 3);
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   317
by (etac E_thm16a 2);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   318
by (dtac E_thm16c 1);
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   319
by (Blast_tac 1);
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   320
qed "lift_5";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   321
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   322
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   323
(** towards lift_3 **)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   324
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   325
(*lemma used to prove lem_lift_3_1*)
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   326
Goal "[| metric n s = #0;  Min <= floor s;  floor s <= Max |] ==> floor s = n";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   327
by (etac rev_mp 1);
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   328
(*force simplification of "metric..." while in conclusion part*)
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   329
by (asm_simp_tac (simpset() addsimps metric_simps) 1);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   330
by (auto_tac (claset() addIs [zleI, zle_anti_sym], 
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   331
	      simpset() addsimps zcompare_rls@[zadd_int, integ_of_Min]));
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   332
(*trans_tac (or decision procedures) could do the rest*)
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   333
by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 2);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   334
by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   335
by (ALLGOALS (clarify_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1])));
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   336
by (REPEAT_FIRST (eres_inst_tac [("P", "?x+?y = ?z")] rev_mp));
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   337
by (REPEAT_FIRST (etac ssubst));
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   338
by (auto_tac (claset(), simpset() addsimps [zadd_int]));
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   339
qed "metric_eq_0D";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   340
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   341
AddDs [metric_eq_0D];
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   342
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   343
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   344
(*lem_lift_3_1*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   345
Goal "Lprg : LeadsTo (moving Int Req n Int {s. metric n s = #0})   \
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   346
\                  (stopped Int atFloor n)";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   347
by (cut_facts_tac [bounded] 1);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   348
by (ensures_tac "request_act" 1);
5424
771a68a468cc modified proofs for new constrains_tac and ensures_tac
paulson
parents: 5410
diff changeset
   349
by Auto_tac;
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   350
qed "E_thm11";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   351
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   352
(*lem_lift_3_5*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   353
Goal "Lprg : LeadsTo \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   354
\       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   355
\       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   356
by (ensures_tac "request_act" 1);
5424
771a68a468cc modified proofs for new constrains_tac and ensures_tac
paulson
parents: 5410
diff changeset
   357
by (auto_tac (claset(), simpset() addsimps metric_simps));
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   358
qed "E_thm13";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   359
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   360
(*lem_lift_3_6*)
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   361
Goal "#0 < N ==> \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   362
\     Lprg : LeadsTo \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   363
\       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   364
\       (opened Int Req n Int {s. metric n s = N})";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   365
by (ensures_tac "open_act" 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   366
by (REPEAT_FIRST (eresolve_tac mov_metrics));
5424
771a68a468cc modified proofs for new constrains_tac and ensures_tac
paulson
parents: 5410
diff changeset
   367
by (auto_tac (claset(), simpset() addsimps metric_simps));
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   368
qed "E_thm14";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   369
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   370
(*lem_lift_3_7*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   371
Goal "Lprg : LeadsTo \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   372
\       (opened Int Req n Int {s. metric n s = N})  \
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   373
\       (closed Int Req n Int {s. metric n s = N})";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   374
by (ensures_tac "close_act" 1);
5424
771a68a468cc modified proofs for new constrains_tac and ensures_tac
paulson
parents: 5410
diff changeset
   375
by (auto_tac (claset(), simpset() addsimps metric_simps));
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   376
qed "E_thm15";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   377
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   378
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   379
(** the final steps **)
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   380
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   381
Goal "#0 < N ==> \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   382
\     Lprg : LeadsTo \
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   383
\       (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})   \
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   384
\       (moving Int Req n Int {s. metric n s < N})";
5479
5a5dfb0f0d7d fixed PROOF FAILED
paulson
parents: 5426
diff changeset
   385
by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
5a5dfb0f0d7d fixed PROOF FAILED
paulson
parents: 5426
diff changeset
   386
	                addIs [LeadsTo_Trans]) 1);
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   387
qed "lift_3_Req";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   388
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   389
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   390
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   391
(*Now we observe that our integer metric is really a natural number*)
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   392
Goal "reachable Lprg <= {s. #0 <= metric n s}";
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   393
by (rtac (bounded RS Invariant_includes_reachable RS subset_trans) 1);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   394
by (simp_tac (simpset() addsimps metric_simps @ zcompare_rls) 1);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   395
by (auto_tac (claset(),
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   396
	      simpset() addsimps [zless_iff_Suc_zadd, zle_iff_zadd]));
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   397
by (REPEAT_FIRST (etac ssubst));
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   398
by (auto_tac (claset(), simpset() addsimps [zadd_int]));
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   399
qed "reach_nonneg";
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   400
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   401
val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken;
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   402
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   403
Goal "Lprg : LeadsTo (moving Int Req n) (stopped Int atFloor n)";
5563
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   404
by (rtac (reach_nonneg RS integ_0_le_induct) 1);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   405
by (case_tac "#0 < z" 1);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   406
(*If z <= #0 then actually z = #0*)
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   407
by (fold_tac [zle_def]);
228b92552d1f Now uses integers instead of naturals
paulson
parents: 5490
diff changeset
   408
by (force_tac (claset() addIs [R_thm11, zle_anti_sym], simpset()) 2);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   409
by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   410
by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   411
by (rtac lift_3_Req 3);
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   412
by (rtac lift_4 2);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   413
by Auto_tac;
5357
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   414
qed "lift_3";
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   415
6efb2b87610c New theory Lift
paulson
parents: 5340
diff changeset
   416
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5596
diff changeset
   417
Goal "Lprg : LeadsTo (Req n) (opened Int atFloor n)";
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   418
by (rtac LeadsTo_Trans 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   419
by (rtac (E_thm04 RS LeadsTo_Un) 2);
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   420
by (rtac LeadsTo_Un_post 2);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   421
by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   422
by (rtac (lift_3 RS LeadsTo_Trans_Un') 2);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   423
by (rtac (lift_2 RS LeadsTo_Trans_Un') 2);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   424
by (rtac (E_thm03 RS LeadsTo_Trans_Un') 2);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   425
by (rtac E_thm02 2);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   426
by (rtac (open_move RS Invariant_LeadsToI) 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   427
by (rtac (open_stop RS Invariant_LeadsToI) 1);
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   428
by (rtac subset_imp_LeadsTo 1);
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   429
by (Clarify_tac 1);
5484
e9430ed7e8d6 Extra steps at end to make it run faster
paulson
parents: 5479
diff changeset
   430
(*The case split is not essential but makes Blast_tac much faster.
e9430ed7e8d6 Extra steps at end to make it run faster
paulson
parents: 5479
diff changeset
   431
  Must also be careful to prevent simplification from looping*)
e9430ed7e8d6 Extra steps at end to make it run faster
paulson
parents: 5479
diff changeset
   432
by (case_tac "open x" 1);
e9430ed7e8d6 Extra steps at end to make it run faster
paulson
parents: 5479
diff changeset
   433
by (ALLGOALS (rotate_tac ~1));
e9430ed7e8d6 Extra steps at end to make it run faster
paulson
parents: 5479
diff changeset
   434
by (ALLGOALS Asm_full_simp_tac);
5426
566f47250bd0 A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents: 5424
diff changeset
   435
by (Blast_tac 1);
5340
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   436
qed "lift_1";
d75c03cf77b5 Misc changes
paulson
parents: 5320
diff changeset
   437
5583
d2377657f8ef modified proof for new simproc
paulson
parents: 5563
diff changeset
   438
Close_locale();