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