author | wenzelm |
Wed, 30 Dec 2015 21:57:52 +0100 | |
changeset 62002 | f1599e98c4d0 |
parent 61999 | 89291b5d0ede |
child 62116 | bc178c0fe1a1 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/IOA/NTP/Impl.thy |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
2 |
Author: Tobias Nipkow & Konrad Slind |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
3 |
*) |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
|
62002 | 5 |
section \<open>The implementation\<close> |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
6 |
|
17244 | 7 |
theory Impl |
8 |
imports Sender Receiver Abschannel |
|
9 |
begin |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
10 |
|
41476 | 11 |
type_synonym 'm impl_state |
19739 | 12 |
= "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset" |
13 |
(* sender_state * receiver_state * srch_state * rsch_state *) |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
14 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
|
27361 | 16 |
definition |
17 |
impl_ioa :: "('m action, 'm impl_state)ioa" where |
|
61999 | 18 |
impl_def: "impl_ioa == (sender_ioa \<parallel> receiver_ioa \<parallel> srch_ioa \<parallel> rsch_ioa)" |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
19 |
|
27361 | 20 |
definition sen :: "'m impl_state => 'm sender_state" where "sen = fst" |
21 |
definition rec :: "'m impl_state => 'm receiver_state" where "rec = fst o snd" |
|
22 |
definition srch :: "'m impl_state => 'm packet multiset" where "srch = fst o snd o snd" |
|
23 |
definition rsch :: "'m impl_state => bool multiset" where "rsch = snd o snd o snd" |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
24 |
|
27361 | 25 |
definition |
26 |
hdr_sum :: "'m packet multiset => bool => nat" where |
|
27 |
"hdr_sum M b == countm M (%pkt. hdr(pkt) = b)" |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
28 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
29 |
(* Lemma 5.1 *) |
27361 | 30 |
definition |
17244 | 31 |
"inv1(s) == |
32 |
(!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) |
|
33 |
& (!b. count (ssent(sen s)) b |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
34 |
= hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)" |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
35 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
36 |
(* Lemma 5.2 *) |
27361 | 37 |
definition |
38 |
"inv2(s) == |
|
17244 | 39 |
(rbit(rec(s)) = sbit(sen(s)) & |
40 |
ssending(sen(s)) & |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
41 |
count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) & |
17244 | 42 |
count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s))) |
43 |
| |
|
44 |
(rbit(rec(s)) = (~sbit(sen(s))) & |
|
45 |
rsending(rec(s)) & |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
46 |
count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) & |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
47 |
count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))" |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
48 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
49 |
(* Lemma 5.3 *) |
27361 | 50 |
definition |
51 |
"inv3(s) == |
|
17244 | 52 |
rbit(rec(s)) = sbit(sen(s)) |
53 |
--> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s))) |
|
54 |
--> count (rrcvd(rec s)) (sbit(sen(s)),m) |
|
55 |
+ count (srch s) (sbit(sen(s)),m) |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
56 |
<= count (rsent(rec s)) (~sbit(sen s)))" |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
57 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
58 |
(* Lemma 5.4 *) |
27361 | 59 |
definition "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []" |
17244 | 60 |
|
19739 | 61 |
|
62002 | 62 |
subsection \<open>Invariants\<close> |
19739 | 63 |
|
35215
a03462cbf86f
get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents:
35174
diff
changeset
|
64 |
declare le_SucI [simp] |
19739 | 65 |
|
66 |
lemmas impl_ioas = |
|
67 |
impl_def sender_ioa_def receiver_ioa_def srch_ioa_thm [THEN eq_reflection] |
|
68 |
rsch_ioa_thm [THEN eq_reflection] |
|
69 |
||
70 |
lemmas "transitions" = |
|
71 |
sender_trans_def receiver_trans_def srch_trans_def rsch_trans_def |
|
72 |
||
73 |
||
74 |
lemmas [simp] = |
|
75 |
ioa_triple_proj starts_of_par trans_of_par4 in_sender_asig |
|
76 |
in_receiver_asig in_srch_asig in_rsch_asig |
|
77 |
||
78 |
declare let_weak_cong [cong] |
|
79 |
||
80 |
lemma [simp]: |
|
81 |
"fst(x) = sen(x)" |
|
82 |
"fst(snd(x)) = rec(x)" |
|
83 |
"fst(snd(snd(x))) = srch(x)" |
|
84 |
"snd(snd(snd(x))) = rsch(x)" |
|
85 |
by (simp_all add: sen_def rec_def srch_def rsch_def) |
|
86 |
||
87 |
lemma [simp]: |
|
88 |
"a:actions(sender_asig) |
|
89 |
| a:actions(receiver_asig) |
|
90 |
| a:actions(srch_asig) |
|
91 |
| a:actions(rsch_asig)" |
|
92 |
by (induct a) simp_all |
|
93 |
||
94 |
declare split_paired_All [simp del] |
|
95 |
||
96 |
||
97 |
(* Three Simp_sets in different sizes |
|
98 |
---------------------------------------------- |
|
99 |
||
100 |
1) simpset() does not unfold the transition relations |
|
101 |
2) ss unfolds transition relations |
|
102 |
3) renname_ss unfolds transitions and the abstract channel *) |
|
103 |
||
62002 | 104 |
ML \<open> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
105 |
val ss = simpset_of (@{context} addsimps @{thms "transitions"}); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
106 |
val rename_ss = simpset_of (put_simpset ss @{context} addsimps @{thms unfold_renaming}); |
19739 | 107 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
108 |
fun tac ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
109 |
asm_simp_tac (put_simpset ss ctxt |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
110 |
|> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if}) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
111 |
fun tac_ren ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
112 |
asm_simp_tac (put_simpset rename_ss ctxt |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
113 |
|> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if}) |
62002 | 114 |
\<close> |
19739 | 115 |
|
116 |
||
62002 | 117 |
subsubsection \<open>Invariant 1\<close> |
19739 | 118 |
|
26305 | 119 |
lemma raw_inv1: "invariant impl_ioa inv1" |
19739 | 120 |
|
121 |
apply (unfold impl_ioas) |
|
122 |
apply (rule invariantI) |
|
123 |
apply (simp add: inv1_def hdr_sum_def srcvd_def ssent_def rsent_def rrcvd_def) |
|
124 |
||
125 |
apply (simp (no_asm) del: trans_of_par4 add: imp_conjR inv1_def) |
|
126 |
||
62002 | 127 |
txt \<open>Split proof in two\<close> |
19739 | 128 |
apply (rule conjI) |
129 |
||
130 |
(* First half *) |
|
131 |
apply (simp add: Impl.inv1_def split del: split_if) |
|
132 |
apply (induct_tac a) |
|
133 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
134 |
apply (tactic "EVERY1[tac @{context}, tac @{context}, tac @{context}, tac @{context}]") |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
135 |
apply (tactic "tac @{context} 1") |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
136 |
apply (tactic "tac_ren @{context} 1") |
19739 | 137 |
|
62002 | 138 |
txt \<open>5 + 1\<close> |
19739 | 139 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
140 |
apply (tactic "tac @{context} 1") |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
141 |
apply (tactic "tac_ren @{context} 1") |
19739 | 142 |
|
62002 | 143 |
txt \<open>4 + 1\<close> |
144 |
apply (tactic \<open>EVERY1[tac @{context}, tac @{context}, tac @{context}, tac @{context}]\<close>) |
|
19739 | 145 |
|
146 |
||
62002 | 147 |
txt \<open>Now the other half\<close> |
19739 | 148 |
apply (simp add: Impl.inv1_def split del: split_if) |
149 |
apply (induct_tac a) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
150 |
apply (tactic "EVERY1 [tac @{context}, tac @{context}]") |
19739 | 151 |
|
62002 | 152 |
txt \<open>detour 1\<close> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
153 |
apply (tactic "tac @{context} 1") |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
154 |
apply (tactic "tac_ren @{context} 1") |
19739 | 155 |
apply (rule impI) |
156 |
apply (erule conjE)+ |
|
157 |
apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def |
|
158 |
split add: split_if) |
|
62002 | 159 |
txt \<open>detour 2\<close> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
160 |
apply (tactic "tac @{context} 1") |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
161 |
apply (tactic "tac_ren @{context} 1") |
19739 | 162 |
apply (rule impI) |
163 |
apply (erule conjE)+ |
|
164 |
apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def |
|
25161 | 165 |
Multiset.delm_nonempty_def split add: split_if) |
19739 | 166 |
apply (rule allI) |
167 |
apply (rule conjI) |
|
168 |
apply (rule impI) |
|
169 |
apply hypsubst |
|
170 |
apply (rule pred_suc [THEN iffD1]) |
|
171 |
apply (drule less_le_trans) |
|
172 |
apply (cut_tac eq_packet_imp_eq_hdr [unfolded Packet.hdr_def, THEN countm_props]) |
|
173 |
apply assumption |
|
174 |
apply assumption |
|
175 |
||
176 |
apply (rule countm_done_delm [THEN mp, symmetric]) |
|
177 |
apply (rule refl) |
|
178 |
apply (simp (no_asm_simp) add: Multiset.count_def) |
|
179 |
||
180 |
apply (rule impI) |
|
181 |
apply (simp add: neg_flip) |
|
182 |
apply hypsubst |
|
183 |
apply (rule countm_spurious_delm) |
|
184 |
apply (simp (no_asm)) |
|
185 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
186 |
apply (tactic "EVERY1 [tac @{context}, tac @{context}, tac @{context}, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
187 |
tac @{context}, tac @{context}, tac @{context}]") |
19739 | 188 |
|
189 |
done |
|
190 |
||
191 |
||
192 |
||
62002 | 193 |
subsubsection \<open>INVARIANT 2\<close> |
19739 | 194 |
|
26305 | 195 |
lemma raw_inv2: "invariant impl_ioa inv2" |
19739 | 196 |
|
197 |
apply (rule invariantI1) |
|
62002 | 198 |
txt \<open>Base case\<close> |
19739 | 199 |
apply (simp add: inv2_def receiver_projections sender_projections impl_ioas) |
200 |
||
201 |
apply (simp (no_asm_simp) add: impl_ioas split del: split_if) |
|
202 |
apply (induct_tac "a") |
|
203 |
||
62002 | 204 |
txt \<open>10 cases. First 4 are simple, since state doesn't change\<close> |
19739 | 205 |
|
62002 | 206 |
ML_prf \<open>val tac2 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv2_def}])\<close> |
19739 | 207 |
|
62002 | 208 |
txt \<open>10 - 7\<close> |
19739 | 209 |
apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]") |
62002 | 210 |
txt \<open>6\<close> |
211 |
apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}] |
|
212 |
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>) |
|
19739 | 213 |
|
62002 | 214 |
txt \<open>6 - 5\<close> |
19739 | 215 |
apply (tactic "EVERY1 [tac2,tac2]") |
216 |
||
62002 | 217 |
txt \<open>4\<close> |
218 |
apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}] |
|
219 |
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>) |
|
19739 | 220 |
apply (tactic "tac2 1") |
221 |
||
62002 | 222 |
txt \<open>3\<close> |
223 |
apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}] |
|
224 |
(@{thm raw_inv1} RS @{thm invariantE})] 1\<close>) |
|
19739 | 225 |
|
226 |
apply (tactic "tac2 1") |
|
62002 | 227 |
apply (tactic \<open>fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}] |
228 |
(@{thm Impl.hdr_sum_def})]\<close>) |
|
19739 | 229 |
apply arith |
230 |
||
62002 | 231 |
txt \<open>2\<close> |
19739 | 232 |
apply (tactic "tac2 1") |
62002 | 233 |
apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}] |
234 |
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>) |
|
19739 | 235 |
apply (intro strip) |
236 |
apply (erule conjE)+ |
|
237 |
apply simp |
|
238 |
||
62002 | 239 |
txt \<open>1\<close> |
19739 | 240 |
apply (tactic "tac2 1") |
62002 | 241 |
apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}] |
242 |
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1\<close>) |
|
19739 | 243 |
apply (intro strip) |
244 |
apply (erule conjE)+ |
|
62002 | 245 |
apply (tactic \<open>fold_goals_tac @{context} |
246 |
[rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})]\<close>) |
|
19739 | 247 |
apply simp |
248 |
||
249 |
done |
|
250 |
||
251 |
||
62002 | 252 |
subsubsection \<open>INVARIANT 3\<close> |
19739 | 253 |
|
26305 | 254 |
lemma raw_inv3: "invariant impl_ioa inv3" |
19739 | 255 |
|
256 |
apply (rule invariantI) |
|
62002 | 257 |
txt \<open>Base case\<close> |
19739 | 258 |
apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas) |
259 |
||
260 |
apply (simp (no_asm_simp) add: impl_ioas split del: split_if) |
|
261 |
apply (induct_tac "a") |
|
262 |
||
62002 | 263 |
ML_prf \<open>val tac3 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv3_def}])\<close> |
19739 | 264 |
|
62002 | 265 |
txt \<open>10 - 8\<close> |
19739 | 266 |
|
267 |
apply (tactic "EVERY1[tac3,tac3,tac3]") |
|
268 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
269 |
apply (tactic "tac_ren @{context} 1") |
19739 | 270 |
apply (intro strip, (erule conjE)+) |
271 |
apply hypsubst |
|
272 |
apply (erule exE) |
|
273 |
apply simp |
|
274 |
||
62002 | 275 |
txt \<open>7\<close> |
19739 | 276 |
apply (tactic "tac3 1") |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
277 |
apply (tactic "tac_ren @{context} 1") |
19739 | 278 |
apply force |
279 |
||
62002 | 280 |
txt \<open>6 - 3\<close> |
19739 | 281 |
|
282 |
apply (tactic "EVERY1[tac3,tac3,tac3,tac3]") |
|
283 |
||
62002 | 284 |
txt \<open>2\<close> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45620
diff
changeset
|
285 |
apply (tactic "asm_full_simp_tac (put_simpset ss @{context}) 1") |
19739 | 286 |
apply (simp (no_asm) add: inv3_def) |
287 |
apply (intro strip, (erule conjE)+) |
|
288 |
apply (rule imp_disjL [THEN iffD1]) |
|
289 |
apply (rule impI) |
|
62002 | 290 |
apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}] |
291 |
(@{thm raw_inv2} RS @{thm invariantE})] 1\<close>) |
|
19739 | 292 |
apply simp |
293 |
apply (erule conjE)+ |
|
294 |
apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and |
|
295 |
k = "count (rsent (rec s)) (sbit (sen s))" in le_trans) |
|
62002 | 296 |
apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm inv1_def}] |
297 |
(@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1\<close>) |
|
19739 | 298 |
apply (simp add: hdr_sum_def Multiset.count_def) |
299 |
apply (rule add_le_mono) |
|
300 |
apply (rule countm_props) |
|
301 |
apply (simp (no_asm)) |
|
302 |
apply (rule countm_props) |
|
303 |
apply (simp (no_asm)) |
|
304 |
apply assumption |
|
305 |
||
62002 | 306 |
txt \<open>1\<close> |
19739 | 307 |
apply (tactic "tac3 1") |
308 |
apply (intro strip, (erule conjE)+) |
|
309 |
apply (rule imp_disjL [THEN iffD1]) |
|
310 |
apply (rule impI) |
|
62002 | 311 |
apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}] |
312 |
(@{thm raw_inv2} RS @{thm invariantE})] 1\<close>) |
|
19739 | 313 |
apply simp |
314 |
done |
|
315 |
||
316 |
||
62002 | 317 |
subsubsection \<open>INVARIANT 4\<close> |
19739 | 318 |
|
26305 | 319 |
lemma raw_inv4: "invariant impl_ioa inv4" |
19739 | 320 |
|
321 |
apply (rule invariantI) |
|
62002 | 322 |
txt \<open>Base case\<close> |
19739 | 323 |
apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas) |
324 |
||
325 |
apply (simp (no_asm_simp) add: impl_ioas split del: split_if) |
|
326 |
apply (induct_tac "a") |
|
327 |
||
62002 | 328 |
ML_prf \<open>val tac4 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv4_def}])\<close> |
19739 | 329 |
|
62002 | 330 |
txt \<open>10 - 2\<close> |
19739 | 331 |
|
332 |
apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]") |
|
333 |
||
62002 | 334 |
txt \<open>2 b\<close> |
19739 | 335 |
|
336 |
apply (intro strip, (erule conjE)+) |
|
62002 | 337 |
apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}] |
338 |
(@{thm raw_inv2} RS @{thm invariantE})] 1\<close>) |
|
19739 | 339 |
apply simp |
340 |
||
62002 | 341 |
txt \<open>1\<close> |
19739 | 342 |
apply (tactic "tac4 1") |
343 |
apply (intro strip, (erule conjE)+) |
|
344 |
apply (rule ccontr) |
|
62002 | 345 |
apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}] |
346 |
(@{thm raw_inv2} RS @{thm invariantE})] 1\<close>) |
|
347 |
apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv3_def}] |
|
348 |
(@{thm raw_inv3} RS @{thm invariantE})] 1\<close>) |
|
19739 | 349 |
apply simp |
58270 | 350 |
apply (rename_tac m, erule_tac x = "m" in allE) |
19739 | 351 |
apply simp |
352 |
done |
|
353 |
||
354 |
||
62002 | 355 |
text \<open>rebind them\<close> |
19739 | 356 |
|
26305 | 357 |
lemmas inv1 = raw_inv1 [THEN invariantE, unfolded inv1_def] |
358 |
and inv2 = raw_inv2 [THEN invariantE, unfolded inv2_def] |
|
359 |
and inv3 = raw_inv3 [THEN invariantE, unfolded inv3_def] |
|
360 |
and inv4 = raw_inv4 [THEN invariantE, unfolded inv4_def] |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
361 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
362 |
end |