author | berghofe |
Mon, 30 Sep 2002 16:14:02 +0200 | |
changeset 13601 | fd3e3d6b37b2 |
parent 11868 | 56db9f3a6b3e |
permissions | -rw-r--r-- |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Lift |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
The Lift-Control Example |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
8 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
Goal "[| x ~: A; y : A |] ==> x ~= y"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
by (Blast_tac 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
qed "not_mem_distinct"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
Addsimps [Lift_def RS def_prg_Init]; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
program_defs_ref := [Lift_def]; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
17 |
Addsimps (map simp_of_act |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
[request_act_def, open_act_def, close_act_def, |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
req_up_def, req_down_def, move_up_def, move_down_def, |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
button_press_def]); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
(*The ALWAYS properties*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
Addsimps (map simp_of_set [above_def, below_def, queueing_def, |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
24 |
goingup_def, goingdown_def, ready_def]); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def, |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
moving_up_def, moving_down_def]; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
AddIffs [Min_le_Max]; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
31 |
Goal "Lift : Always open_stop"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
by (always_tac 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
qed "open_stop"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
34 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
Goal "Lift : Always stop_floor"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
by (always_tac 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
37 |
qed "stop_floor"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
38 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
39 |
(*This one needs open_stop, which was proved above*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
40 |
Goal "Lift : Always open_move"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
41 |
by (cut_facts_tac [open_stop] 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
42 |
by (always_tac 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
43 |
qed "open_move"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
44 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
45 |
Goal "Lift : Always moving_up"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
46 |
by (always_tac 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
47 |
by (auto_tac (claset() addDs [zle_imp_zless_or_eq], |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
48 |
simpset() addsimps [add1_zle_eq])); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
49 |
qed "moving_up"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
50 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
51 |
Goal "Lift : Always moving_down"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
52 |
by (always_tac 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
53 |
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
54 |
qed "moving_down"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
55 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
56 |
Goal "Lift : Always bounded"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
57 |
by (cut_facts_tac [moving_up, moving_down] 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
58 |
by (always_tac 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
59 |
by Auto_tac; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
60 |
by (ALLGOALS (dtac not_mem_distinct THEN' assume_tac)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
61 |
by (ALLGOALS arith_tac); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
62 |
qed "bounded"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
63 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
64 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
65 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
66 |
(*** Progress ***) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
67 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
68 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
69 |
val abbrev_defs = [moving_def, stopped_def, |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
70 |
opened_def, closed_def, atFloor_def, Req_def]; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
71 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
72 |
Addsimps (map simp_of_set abbrev_defs); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
73 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
74 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
75 |
(** The HUG'93 paper mistakenly omits the Req n from these! **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
76 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
77 |
(** Lift_1 **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
78 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
79 |
Goal "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
80 |
by (cut_facts_tac [stop_floor] 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
81 |
by (ensures_tac "open_act" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
82 |
qed "E_thm01"; (*lem_lift_1_5*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
83 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
84 |
Goal "Lift : (Req n Int stopped - atFloor n) LeadsTo \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
85 |
\ (Req n Int opened - atFloor n)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
86 |
by (cut_facts_tac [stop_floor] 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
87 |
by (ensures_tac "open_act" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
88 |
qed "E_thm02"; (*lem_lift_1_1*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
89 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
90 |
Goal "Lift : (Req n Int opened - atFloor n) LeadsTo \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
91 |
\ (Req n Int closed - (atFloor n - queueing))"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
92 |
by (ensures_tac "close_act" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
93 |
qed "E_thm03"; (*lem_lift_1_2*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
94 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
95 |
Goal "Lift : (Req n Int closed Int (atFloor n - queueing)) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
96 |
\ LeadsTo (opened Int atFloor n)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
97 |
by (ensures_tac "open_act" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
98 |
qed "E_thm04"; (*lem_lift_1_7*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
99 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
100 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
101 |
(** Lift 2. Statements of thm05a and thm05b were wrong! **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
102 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
103 |
Open_locale "floor"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
104 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
105 |
val Min_le_n = thm "Min_le_n"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
106 |
val n_le_Max = thm "n_le_Max"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
107 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
108 |
AddIffs [Min_le_n, n_le_Max]; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
109 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
110 |
val le_MinD = Min_le_n RS order_antisym; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
111 |
val Max_leD = n_le_Max RSN (2,order_antisym); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
112 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
113 |
val linorder_leI = linorder_not_less RS iffD1; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
114 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
115 |
AddSDs [le_MinD, linorder_leI RS le_MinD, |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
116 |
Max_leD, linorder_leI RS Max_leD]; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
117 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
118 |
(*lem_lift_2_0 |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
119 |
NOT an ensures property, but a mere inclusion; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
120 |
don't know why script lift_2.uni says ENSURES*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
121 |
Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
122 |
\ LeadsTo ((closed Int goingup Int Req n) Un \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
123 |
\ (closed Int goingdown Int Req n))"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
124 |
by (auto_tac (claset() addSIs [subset_imp_LeadsTo] addSEs [int_neqE], |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
125 |
simpset())); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
126 |
qed "E_thm05c"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
127 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
128 |
(*lift_2*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
129 |
Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
130 |
\ LeadsTo (moving Int Req n)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
131 |
by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
132 |
by (ensures_tac "req_down" 2); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
133 |
by (ensures_tac "req_up" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
134 |
by Auto_tac; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
135 |
qed "lift_2"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
136 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
137 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
138 |
(** Towards lift_4 ***) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
139 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
140 |
val metric_ss = simpset() addsplits [split_if_asm] |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
141 |
addsimps [metric_def, vimage_def]; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
142 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
143 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
144 |
(*lem_lift_4_1 *) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
145 |
Goal "0 < N ==> \ |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
146 |
\ Lift : (moving Int Req n Int {s. metric n s = N} Int \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
147 |
\ {s. floor s ~: req s} Int {s. up s}) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
148 |
\ LeadsTo \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
149 |
\ (moving Int Req n Int {s. metric n s < N})"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
150 |
by (cut_facts_tac [moving_up] 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
151 |
by (ensures_tac "move_up" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
152 |
by Safe_tac; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
153 |
(*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
154 |
by (etac (linorder_leI RS order_antisym RS sym) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
155 |
by (auto_tac (claset(), metric_ss)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
156 |
qed "E_thm12a"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
157 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
158 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
159 |
(*lem_lift_4_3 *) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
160 |
Goal "0 < N ==> \ |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
161 |
\ Lift : (moving Int Req n Int {s. metric n s = N} Int \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
162 |
\ {s. floor s ~: req s} - {s. up s}) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
163 |
\ LeadsTo (moving Int Req n Int {s. metric n s < N})"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
164 |
by (cut_facts_tac [moving_down] 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
165 |
by (ensures_tac "move_down" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
166 |
by Safe_tac; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
167 |
(*this step consolidates two formulae to the goal metric n s' <= metric n s*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
168 |
by (etac (linorder_leI RS order_antisym RS sym) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
169 |
by (auto_tac (claset(), metric_ss)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
170 |
qed "E_thm12b"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
171 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
172 |
(*lift_4*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
173 |
Goal "0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int \ |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
174 |
\ {s. floor s ~: req s}) LeadsTo \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
175 |
\ (moving Int Req n Int {s. metric n s < N})"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
176 |
by (rtac ([subset_imp_LeadsTo, [E_thm12a, E_thm12b] MRS LeadsTo_Un] |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
177 |
MRS LeadsTo_Trans) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
178 |
by Auto_tac; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
179 |
qed "lift_4"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
180 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
181 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
182 |
(** towards lift_5 **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
183 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
184 |
(*lem_lift_5_3*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
185 |
Goal "0<N \ |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
186 |
\ ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
187 |
\ (moving Int Req n Int {s. metric n s < N})"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
188 |
by (cut_facts_tac [bounded] 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
189 |
by (ensures_tac "req_up" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
190 |
by (auto_tac (claset(), metric_ss)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
191 |
qed "E_thm16a"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
192 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
193 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
194 |
(*lem_lift_5_1 has ~goingup instead of goingdown*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
195 |
Goal "0<N ==> \ |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
196 |
\ Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
197 |
\ (moving Int Req n Int {s. metric n s < N})"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
198 |
by (cut_facts_tac [bounded] 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
199 |
by (ensures_tac "req_down" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
200 |
by (auto_tac (claset(), metric_ss)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
201 |
qed "E_thm16b"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
202 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
203 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
204 |
(*lem_lift_5_0 proves an intersection involving ~goingup and goingup, |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
205 |
i.e. the trivial disjunction, leading to an asymmetrical proof.*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
206 |
Goal "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown"; |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
207 |
by (Clarify_tac 1); |
13601 | 208 |
by (force_tac (claset(), metric_ss) 1); |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
209 |
qed "E_thm16c"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
210 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
211 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
212 |
(*lift_5*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
213 |
Goal "0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo \ |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
214 |
\ (moving Int Req n Int {s. metric n s < N})"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
215 |
by (rtac ([subset_imp_LeadsTo, [E_thm16a, E_thm16b] MRS LeadsTo_Un] |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
216 |
MRS LeadsTo_Trans) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
217 |
by (dtac E_thm16c 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
218 |
by Auto_tac; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
219 |
qed "lift_5"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
220 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
221 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
222 |
(** towards lift_3 **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
223 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
224 |
(*lemma used to prove lem_lift_3_1*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
225 |
Goal "[| metric n s = 0; Min <= floor s; floor s <= Max |] ==> floor s = n"; |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
226 |
by (auto_tac (claset(), metric_ss)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
227 |
qed "metric_eq_0D"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
228 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
229 |
AddDs [metric_eq_0D]; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
230 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
231 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
232 |
(*lem_lift_3_1*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
233 |
Goal "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo \ |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
234 |
\ (stopped Int atFloor n)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
235 |
by (cut_facts_tac [bounded] 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
236 |
by (ensures_tac "request_act" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
237 |
by Auto_tac; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
238 |
qed "E_thm11"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
239 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
240 |
(*lem_lift_3_5*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
241 |
Goal |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
242 |
"Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
243 |
\ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
244 |
by (ensures_tac "request_act" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
245 |
by (auto_tac (claset(), metric_ss)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
246 |
qed "E_thm13"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
247 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
248 |
(*lem_lift_3_6*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
249 |
Goal "0 < N ==> \ |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
250 |
\ Lift : \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
251 |
\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
252 |
\ LeadsTo (opened Int Req n Int {s. metric n s = N})"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
253 |
by (ensures_tac "open_act" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
254 |
by (auto_tac (claset(), metric_ss)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
255 |
qed "E_thm14"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
256 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
257 |
(*lem_lift_3_7*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
258 |
Goal "Lift : (opened Int Req n Int {s. metric n s = N}) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
259 |
\ LeadsTo (closed Int Req n Int {s. metric n s = N})"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
260 |
by (ensures_tac "close_act" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
261 |
by (auto_tac (claset(), metric_ss)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
262 |
qed "E_thm15"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
263 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
264 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
265 |
(** the final steps **) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
266 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
267 |
Goal "0 < N ==> \ |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
268 |
\ Lift : \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
269 |
\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
270 |
\ LeadsTo (moving Int Req n Int {s. metric n s < N})"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
271 |
by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5] |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
272 |
addIs [LeadsTo_Trans]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
273 |
qed "lift_3_Req"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
274 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
275 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
276 |
(*Now we observe that our integer metric is really a natural number*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
277 |
Goal "Lift : Always {s. 0 <= metric n s}"; |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
278 |
by (rtac (bounded RS Always_weaken) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
279 |
by (auto_tac (claset(), metric_ss)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
280 |
qed "Always_nonneg"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
281 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
282 |
val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
283 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
284 |
Goal "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
285 |
by (rtac (Always_nonneg RS integ_0_le_induct) 1); |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
286 |
by (case_tac "0 < z" 1); |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
287 |
(*If z <= 0 then actually z = 0*) |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
288 |
by (force_tac (claset() addIs [R_thm11, order_antisym], |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
289 |
simpset() addsimps [linorder_not_less]) 2); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
290 |
by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
291 |
by (rtac ([subset_imp_LeadsTo, [lift_4, lift_3_Req] MRS LeadsTo_Un] |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
292 |
MRS LeadsTo_Trans) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
293 |
by Auto_tac; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
294 |
qed "lift_3"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
295 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
296 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
297 |
val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
298 |
(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
299 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
300 |
Goal "Lift : (Req n) LeadsTo (opened Int atFloor n)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
301 |
by (rtac LeadsTo_Trans 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
302 |
by (rtac ([E_thm04, LeadsTo_Un_post] MRS LeadsTo_Un) 2); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
303 |
by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
304 |
by (rtac (lift_3 RS LeadsTo_Trans_Un') 2); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
305 |
by (rtac (lift_2 RS LeadsTo_Trans_Un') 2); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
306 |
by (rtac ([E_thm03,E_thm02] MRS LeadsTo_Trans_Un') 2); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
307 |
by (rtac (open_move RS Always_LeadsToI) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
308 |
by (rtac ([open_stop, subset_imp_LeadsTo] MRS Always_LeadsToI) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
309 |
by (Clarify_tac 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
310 |
(*The case split is not essential but makes Blast_tac much faster. |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
311 |
Calling rotate_tac prevents simplification from looping*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
312 |
by (case_tac "open x" 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
313 |
by (ALLGOALS (rotate_tac ~1)); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
314 |
by Auto_tac; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
315 |
qed "lift_1"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
316 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
317 |
Close_locale "floor"; |