-
Notifications
You must be signed in to change notification settings - Fork 0
/
Move_C.thy
1361 lines (1161 loc) · 50.9 KB
/
Move_C.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: GPL-2.0-only
*)
(* Arch generic lemmas that should be moved into theory files before CRefine *)
theory Move_C
imports CBaseRefine.Include_C
begin
lemma dumb_bool_for_all: "(\<forall>x. x) = False"
by auto
lemma (in semigroup) foldl_first:
"f x (foldl f y zs) = foldl f (f x y) zs"
by (induction zs arbitrary: x y) (auto simp: assoc)
lemma (in monoid) foldl_first':
"f x (foldl f z zs) = foldl f x zs"
using foldl_first by simp
(* FIXME: move to Lib *)
lemma hd_in_zip_set:
"slots \<noteq> [] \<Longrightarrow> (hd slots, 0) \<in> set (zip slots [0.e.of_nat (length slots - Suc 0)::machine_word])"
by (cases slots; simp add: upto_enum_word upto_0_to_n2 del: upt_Suc)
(* FIXME: move to Lib *)
lemma last_in_zip_set:
"\<lbrakk> slots \<noteq> []; length js = length slots \<rbrakk> \<Longrightarrow> (last slots, last js) \<in> set (zip slots js)"
apply (simp add: in_set_zip last_conv_nth)
apply (rule_tac x="length slots - 1" in exI)
apply clarsimp
apply (subst last_conv_nth)
apply (cases js; simp)
apply simp
done
(* FIXME: move to Lib *)
lemma list_length_less:
"(args = [] \<or> length args \<le> Suc 0) = (length args < 2)"
by (case_tac args, simp_all)
(* FIXME: move to Lib *)
lemma at_least_2_args:
"\<not> length args < 2 \<Longrightarrow> \<exists>a b c. args = a#b#c"
apply (case_tac args)
apply simp
apply (case_tac list)
apply simp
apply (case_tac lista)
apply simp
apply simp
done
(* FIXME: move to Lib *)
lemma rel_option_alt_def:
"rel_option f a b = (
(a = None \<and> b = None)
\<or> (\<exists>x y. a = Some x \<and> b = Some y \<and> f x y))"
apply (case_tac a, case_tac b, simp, simp, case_tac b, auto)
done
lemmas and_neq_0_is_nth = arg_cong [where f=Not, OF and_eq_0_is_nth, simplified]
lemma nat_le_induct [consumes 1, case_names base step]:
assumes le: "i \<le> (k::nat)" and
base: "P(k)" and
step: "\<And>i. \<lbrakk>i \<le> k; P i; 0 < i\<rbrakk> \<Longrightarrow> P(i - 1)"
shows "P i"
proof -
obtain j where jk: "j \<le> k" and j_eq: "i = k - j"
using le
apply (drule_tac x="k - i" in meta_spec)
apply simp
done
have "j \<le> k \<Longrightarrow> P (k - j)"
apply (induct j)
apply (simp add: base)
apply simp
apply (drule step[rotated], simp+)
done
thus "P i" using jk j_eq
by simp
qed
lemma assumes A: "is_inv f g" shows the_inv_map_eq: "the_inv_map f = g"
by (simp add: is_inv_unique[OF A A[THEN is_inv_inj, THEN is_inv_the_inv_map]])
lemma ran_map_comp_subset: "ran (map_comp f g) <= (ran f)"
by (fastforce simp: map_comp_def ran_def split: option.splits)
lemma eq_option_to_0_rev:
"Some 0 ~: A \<Longrightarrow> \<forall>x. \<forall>y\<in>A.
((=) \<circ> option_to_0) y x \<longrightarrow> (if x = 0 then None else Some x) = y"
by (clarsimp simp: option_to_0_def split: option.splits)
lemma inj_image_inv:
assumes inj_f: "inj f"
shows "f ` A = B \<Longrightarrow> inv f ` B = A"
by (drule sym) (simp add: image_inv_f_f[OF inj_f])
lemma Collect_mono2: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)" by auto
lemma injection_handler_liftM:
"injection_handler f
= liftM (\<lambda>v. case v of Inl ex \<Rightarrow> Inl (f ex) | Inr rv \<Rightarrow> Inr rv)"
apply (intro ext, simp add: injection_handler_def liftM_def
handleE'_def)
apply (rule bind_apply_cong, rule refl)
apply (simp add: throwError_def split: sum.split)
done
(* FIXME MOVE to where option_to_0 is defined *)
lemma option_to_0_simps [simp]:
"option_to_0 None = 0"
"option_to_0 (Some x) = x"
by (auto simp: option_to_0_def split: option.split)
lemma of_bool_from_bool: "of_bool = from_bool"
by (rule ext, simp add: from_bool_def split: bool.split)
lemma hoare_vcg_imp_lift_R:
"\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, -; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, -"
by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)
(* FIXME: move to Lib *)
lemma length_Suc_0_conv:
"length x = Suc 0 = (\<exists>y. x = [y])"
by (induct x; clarsimp)
lemma imp_ignore: "B \<Longrightarrow> A \<longrightarrow> B" by blast
lemma cteSizeBits_eq:
"cteSizeBits = cte_level_bits"
by (simp add: cte_level_bits_def cteSizeBits_def)
lemma cteSizeBits_le_cte_level_bits[simp]:
"cteSizeBits \<le> cte_level_bits"
by (simp add: cte_level_bits_def cteSizeBits_def)
lemma msb_le_mono:
fixes v w :: "'a::len word"
shows "v \<le> w \<Longrightarrow> msb v \<Longrightarrow> msb w"
by (simp add: msb_big)
lemma neg_msb_le_mono:
fixes v w :: "'a::len word"
shows "v \<le> w \<Longrightarrow> \<not> msb w \<Longrightarrow> \<not> msb v"
by (simp add: msb_big)
lemmas msb_less_mono = msb_le_mono[OF less_imp_le]
lemmas neg_msb_less_mono = neg_msb_le_mono[OF less_imp_le]
lemma word_sless_iff_less:
"\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <s w \<longleftrightarrow> v < w"
by (simp add: word_sless_alt sint_eq_uint word_less_alt)
lemmas word_sless_imp_less = word_sless_iff_less[THEN iffD1, rotated 2]
lemmas word_less_imp_sless = word_sless_iff_less[THEN iffD2, rotated 2]
lemma word_sle_iff_le:
"\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <=s w \<longleftrightarrow> v \<le> w"
by (simp add: word_sle_def sint_eq_uint word_le_def)
lemmas word_sle_imp_le = word_sle_iff_le[THEN iffD1, rotated 2]
lemmas word_le_imp_sle = word_sle_iff_le[THEN iffD2, rotated 2]
lemma to_bool_if:
"(if w \<noteq> 0 then 1 else 0) = (if to_bool w then 1 else 0)"
by (auto simp: to_bool_def)
(* FIXME: move to Word_Lib *)
lemma word_upcast_shiftr:
assumes "LENGTH('a::len) \<le> LENGTH('b::len)"
shows "UCAST('a \<rightarrow> 'b) (w >> n) = UCAST('a \<rightarrow> 'b) w >> n"
apply (intro word_eqI impI iffI; clarsimp simp: word_size nth_shiftr nth_ucast)
apply (drule test_bit_size)
using assms by (simp add: word_size)
lemma word_upcast_neg_msb:
"LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> \<not> msb (UCAST('a \<rightarrow> 'b) w)"
apply (simp only: ucast_def msb_word_of_int, clarsimp)
apply (drule bin_nth_uint_imp)
by simp
(* FIXME: move to Word_Lib *)
lemma word_upcast_0_sle:
"LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> 0 <=s UCAST('a \<rightarrow> 'b) w"
by (simp add: word_sle_iff_le[OF word_msb_0 word_upcast_neg_msb])
(* FIXME: move to Word_Lib *)
lemma scast_ucast_up_eq_ucast:
assumes "LENGTH('a::len) < LENGTH('b::len)"
shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c::len) w"
using assms
apply (subst scast_eq_ucast; simp)
apply (simp only: ucast_def msb_word_of_int, clarsimp)
apply (drule bin_nth_uint_imp)
apply simp
by (metis Word.of_nat_unat nat_less_le unat_ucast_up_simp)
lemma not_max_word_iff_less:
"w \<noteq> max_word \<longleftrightarrow> w < max_word"
by (simp add: order_less_le)
lemma ucast_increment:
assumes "w \<noteq> max_word"
shows "UCAST('a::len \<rightarrow> 'b::len) w + 1 = UCAST('a \<rightarrow> 'b) (w + 1)"
apply (cases "LENGTH('b) \<le> LENGTH('a)")
apply (simp add: ucast_down_add is_down)
apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('a)")
apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('b)")
apply (subst word_uint_eq_iff)
apply (simp add: uint_arith_simps uint_up_ucast is_up)
apply (erule less_trans, rule power_strict_increasing, simp, simp)
apply (subst less_diff_eq[symmetric])
using assms
apply (simp add: not_max_word_iff_less word_less_alt)
apply (erule less_le_trans)
apply simp
done
lemma max_word_gt_0:
"0 < max_word"
by (simp add: le_neq_trans[OF max_word_max] max_word_not_0)
lemma and_not_max_word:
"m \<noteq> max_word \<Longrightarrow> w && m \<noteq> max_word"
by (simp add: not_max_word_iff_less word_and_less')
lemma mask_not_max_word:
"m < LENGTH('a::len) \<Longrightarrow> mask m \<noteq> (max_word :: 'a word)"
by (simp add: mask_eq_exp_minus_1)
lemmas and_mask_not_max_word =
and_not_max_word[OF mask_not_max_word]
lemma shiftr_not_max_word:
"0 < n \<Longrightarrow> w >> n \<noteq> max_word"
apply (simp add: not_max_word_iff_less)
apply (cases "n < size w")
apply (cases "w = 0")
apply (simp add: max_word_gt_0)
apply (subst shiftr_div_2n_w, assumption)
apply (rule less_le_trans[OF div_less_dividend_word max_word_max])
apply simp
apply (metis word_size_gt_0 less_numeral_extra(3) mask_def nth_mask power_0 shiftl_t2n)
apply (simp add: not_less word_size)
apply (subgoal_tac "w >> n = 0"; simp add: max_word_gt_0 shiftr_eq_0)
done
lemma word_sandwich1:
fixes a b c :: "'a::len word"
assumes "a < b"
assumes "b <= c"
shows "0 < b - a \<and> b - a <= c"
using assms diff_add_cancel order_less_irrefl add_0 word_le_imp_diff_le
word_le_less_eq word_neq_0_conv
by metis
lemma word_sandwich2:
fixes a b :: "'a::len word"
assumes "0 < a"
assumes "a <= b"
shows "b - a < b"
using assms less_le_trans word_diff_less
by blast
lemma unat_and_mask_less_2p:
fixes w :: "'a::len word"
shows "m < LENGTH('a) \<Longrightarrow> unat (w && mask m) < 2 ^ m"
by (simp add: unat_less_helper and_mask_less')
lemma unat_shiftr_less_2p:
fixes w :: "'a::len word"
shows "n + m = LENGTH('a) \<Longrightarrow> unat (w >> n) < 2 ^ m"
by (cases "n = 0"; simp add: unat_less_helper shiftr_less_t2n3)
lemma nat_div_less_mono:
fixes m n :: nat
shows "m div d < n div d \<Longrightarrow> m < n"
by (meson div_le_mono not_less)
lemma word_shiftr_less_mono:
fixes w :: "'a::len word"
shows "w >> n < v >> n \<Longrightarrow> w < v"
by (auto simp: word_less_nat_alt shiftr_div_2n' elim: nat_div_less_mono)
lemma word_shiftr_less_mask:
fixes w :: "'a::len word"
shows "(w >> n < v >> n) \<longleftrightarrow> (w && ~~mask n < v && ~~mask n)"
by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)
lemma word_shiftr_le_mask:
fixes w :: "'a::len word"
shows "(w >> n \<le> v >> n) \<longleftrightarrow> (w && ~~mask n \<le> v && ~~mask n)"
by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)
lemma word_shiftr_eq_mask:
fixes w :: "'a::len word"
shows "(w >> n = v >> n) \<longleftrightarrow> (w && ~~mask n = v && ~~mask n)"
by (metis (mono_tags) mask_shift shiftr_eq_neg_mask_eq)
lemmas word_shiftr_cmp_mask =
word_shiftr_less_mask word_shiftr_le_mask word_shiftr_eq_mask
lemma if_if_if_same_output:
"(if c1 then if c2 then t else f else if c3 then t else f) = (if c1 \<and> c2 \<or> \<not>c1 \<and> c3 then t else f)"
by (simp split: if_splits)
lemma word_le_split_mask:
"(w \<le> v) \<longleftrightarrow> (w >> n < v >> n \<or> w >> n = v >> n \<and> w && mask n \<le> v && mask n)"
apply (simp add: word_shiftr_eq_mask word_shiftr_less_mask)
apply (rule subst[where P="\<lambda>c. c \<le> d = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]])
apply (rule subst[where P="\<lambda>c. d \<le> c = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]])
apply (rule iffI)
apply safe
apply (fold_subgoals (prefix))[2]
apply (subst atomize_conj)
apply (rule context_conjI)
apply (metis AND_NOT_mask_plus_AND_mask_eq neg_mask_mono_le word_le_less_eq)
apply (metis add.commute word_and_le1 word_bw_comms(1) word_plus_and_or_coroll2 word_plus_mcs_4)
apply (metis Groups.add_ac(2) neg_mask_mono_le word_le_less_eq word_not_le word_plus_and_or_coroll2)
apply (metis add.commute word_and_le1 word_bw_comms(1) word_plus_and_or_coroll2 word_plus_mcs_3)
done
lemma unat_ucast_prio_mask_simp[simp]:
"unat (ucast (p::priority) && mask m :: machine_word) = unat (p && mask m)"
by (simp add: ucast_and_mask)
lemma unat_ucast_prio_shiftr_simp[simp]:
"unat (ucast (p::priority) >> n :: machine_word) = unat (p >> n)"
by simp
lemma from_bool_to_bool_and_1 [simp]:
assumes r_size: "1 < size r"
shows "from_bool (to_bool (r && 1)) = r && 1"
proof -
from r_size have "r && 1 < 2"
by (simp add: and_mask_less_size [where n=1, unfolded mask_def, simplified])
thus ?thesis
by (fastforce simp add: from_bool_def to_bool_def dest: word_less_cases)
qed
lemma wb_gt_2:
"2 < word_bits" by (simp add: word_bits_conv)
(* NOTE: unused. *)
lemma inj_on_option_map:
"inj_on (map_option f o m) (dom m) \<Longrightarrow> inj_on m (dom m)"
by (simp add: inj_on_imageI2)
lemma of_bool_inject[simp]: "of_bool a = of_bool b \<longleftrightarrow> a=b"
by (cases a) (cases b, simp_all)+
lemma shiftr_and_eq_shiftl:
fixes w x y :: "'a::len word"
assumes r: "(w >> n) && x = y"
shows "w && (x << n) = (y << n)"
using assms
proof -
{ fix i
assume i: "i < LENGTH('a)"
hence "test_bit (w && (x << n)) i \<longleftrightarrow> test_bit (y << n) i"
using word_eqD[where x="i-n", OF r]
by (cases "n \<le> i") (auto simp: nth_shiftl nth_shiftr)
}
thus ?thesis using word_eq_iff by blast
qed
(* FIXME: move to Word_Lib *)
lemma sign_extend_0[simp]:
"sign_extend a 0 = 0"
by (simp add: sign_extend_def)
lemma mask_shiftr_times_simp:
"\<lbrakk>x > n;is_aligned p n\<rbrakk> \<Longrightarrow> (p && mask x >> n) * (2^n) = (p && mask x)"
apply (subst mult.commute)
apply (simp add: shiftl_t2n[symmetric])
by (simp add: is_aligned_andI1 is_aligned_shiftr_shiftl)
lemma name_seq_bound_helper:
"(\<not> CP n \<and> (\<forall>n' < n. CP n'))
\<Longrightarrow> (if \<exists>n. \<not> CP n
then simpl_sequence c' (map f [0 ..< (LEAST n. \<not> CP n)])
else c) = (simpl_sequence c' (map f [0 ..< n]))"
apply (simp add: exI[where x=n])
apply (subst Least_equality[where x=n], simp_all)
apply (rule ccontr, simp add: linorder_not_le)
done
(* FIXME: what's being proven here? it's a pure word lemma - should it go in Word_Lib? *)
lemma reset_name_seq_bound_helper:
fixes sz
fixes v :: "('a :: len) word"
defines "CP \<equiv> (\<lambda>n. ~ (v && ~~ mask sz) + of_nat n * (-1 << sz) =
((-1 :: 'a word) << sz))"
and "n \<equiv> Suc (unat (shiftR v sz))"
assumes vsz: "v + 1 < 2 ^ (len_of TYPE('a) - 1)" "2 ^ sz \<noteq> (0 :: 'a word)"
and vless: "v < v'"
shows "(\<not> CP n \<and> (\<forall>n' < n. CP n'))"
apply (clarsimp simp: shiftl_t2n field_simps less_Suc_eq_le CP_def n_def)
apply (simp add: shiftr_shiftl1[where b=sz and c=sz, simplified, symmetric]
shiftl_t2n)
apply (clarsimp simp: word_sle_msb_le shiftl_t2n[symmetric])
apply (case_tac n', simp_all)
apply (cut_tac vsz(1) order_less_le_trans[OF vless max_word_max])
apply (clarsimp simp: shiftr_shiftl1 dest!: word_add_no_overflow)
apply (drule_tac f="\<lambda>x. x - 2 ^ sz" in arg_cong, simp)
apply (metis less_irrefl order_le_less_trans order_less_trans
word_and_le2[where a=v and y="~~ mask sz"]
word_two_power_neg_ineq[OF vsz(2)])
apply (clarsimp simp add: field_simps)
apply (drule_tac f="\<lambda>x. shiftr x sz" in arg_cong)
apply simp
apply (simp add: shiftr_div_2n')
apply (simp only: linorder_not_less[symmetric], erule notE)
apply (rule order_le_less_trans[OF div_le_mono])
apply (rule_tac b="v * 2 ^ sz" for v in word_unat_less_le,
simp, rule order_refl)
apply simp
done
schematic_goal sz8_helper:
"((-1) << 8 :: addr) = ?v"
by (simp add: shiftl_t2n)
lemmas reset_name_seq_bound_helper2
= reset_name_seq_bound_helper[where sz=8 and v="v :: addr" for v,
simplified sz8_helper word_bits_def[symmetric],
THEN name_seq_bound_helper]
(* FIXME move to lib/Eisbach_Methods *)
(* FIXME consider printing error on solve goal apply *)
context
begin
private definition "bool_protect (b::bool) \<equiv> b"
lemma bool_protectD:
"bool_protect P \<Longrightarrow> P"
unfolding bool_protect_def by simp
lemma bool_protectI:
"P \<Longrightarrow> bool_protect P"
unfolding bool_protect_def by simp
(*
When you want to apply a rule/tactic to transform a potentially complex goal into another
one manually, but want to indicate that any fresh emerging goals are solved by a more
brutal method.
E.g. apply (solves_emerging \<open>frule x=... in my_rule\<close>\<open>fastforce simp: ... intro!: ... \<close> *)
method solves_emerging methods m1 m2 = (rule bool_protectD, (m1 ; (rule bool_protectI | (m2; fail))))
end
lemma shiftr_le_mask:
fixes w :: "'a::len word"
shows "w >> n \<le> mask (LENGTH('a) - n)"
by (metis and_mask_eq_iff_shiftr_0 le_mask_iff shiftr_mask_eq word_size)
lemma word_minus_1_shiftr:
notes word_unat.Rep_inject[simp del]
fixes w :: "'a::len word"
assumes low_bits_zero: "w && mask n = 0"
assumes neq_zero: "w \<noteq> 0"
shows "(w - 1) >> n = (w >> n) - 1"
using neq_zero low_bits_zero
apply (subgoal_tac "n < LENGTH('a)")
prefer 2
apply (metis not_less ucast_id ucast_mask_drop)
apply (rule_tac t="w - 1" and s="(w && ~~ mask n) - 1" in subst,
fastforce simp: low_bits_zero mask_eq_x_eq_0)
apply (clarsimp simp: mask_eq_0_eq_x neg_mask_is_div lt1_neq0[symmetric])
apply (subst shiftr_div_2n_w, fastforce simp: word_size)+
apply (rule word_uint.Rep_eqD)
apply (simp only: uint_word_ariths uint_div uint_power_lower)
apply (subst mod_pos_pos_trivial, fastforce, fastforce)+
apply (subst mod_pos_pos_trivial)
apply (simp add: word_less_def)
apply (subst uint_1[symmetric])
apply (fastforce intro: uint_sub_lt2p)
apply (subst int_div_sub_1, fastforce)
apply (clarsimp simp: and_mask_dvd low_bits_zero)
apply (subst mod_pos_pos_trivial)
apply (metis le_step_down_int mult_zero_left shiftr_div_2n shiftr_div_2n_w uint_0_iff
uint_nonnegative word_not_simps(1) wsst_TYs(3))
apply (metis shiftr_div_2n uint_1 uint_sub_lt2p)
apply fastforce
done
(* FIXME: move to Word *)
lemma ucast_shiftr:
"UCAST('a::len \<rightarrow> 'b::len) w >> n = UCAST('a \<rightarrow> 'b) ((w && mask LENGTH('b)) >> n)"
apply (rule word_eqI[rule_format]; rule iffI; clarsimp simp: nth_ucast nth_shiftr word_size)
done
(* FIXME: move to Word *)
lemma mask_eq_ucast_shiftr:
assumes mask: "w && mask LENGTH('b) = w"
shows "UCAST('a::len \<rightarrow> 'b::len) w >> n = UCAST('a \<rightarrow> 'b) (w >> n)"
by (rule ucast_shiftr[where 'a='a and 'b='b, of w n, simplified mask])
(* FIXME: move to Word *)
lemma mask_eq_ucast_shiftl:
assumes "w && mask (LENGTH('a) - n) = w"
shows "UCAST('a::len \<rightarrow> 'b::len) w << n = UCAST('a \<rightarrow> 'b) (w << n)"
apply (rule subst[where P="\<lambda>c. ucast c << n = ucast (c << n)", OF assms])
apply (rule word_eqI[rule_format]; rule iffI;
clarsimp simp: nth_ucast nth_shiftl word_size;
drule test_bit_size; simp add: word_size)
done
(* FIXME: replace by mask_mono *)
lemma mask_le_mono:
"m \<le> n \<Longrightarrow> mask m \<le> (mask n::'a::len word)"
by (rule mask_mono)
(* FIXME: move to Word *)
lemma word_and_mask_eq_le_mono:
"w && mask m = w \<Longrightarrow> m \<le> n \<Longrightarrow> w && mask n = w"
apply (simp add: and_mask_eq_iff_le_mask)
by (erule order.trans, erule mask_le_mono)
lemma word_not_exists_nth:
"(w::'a::len word) = 0 \<Longrightarrow> \<forall>i<LENGTH('a). \<not> w !! i"
by (clarsimp simp: nth_0)
lemma word_highbits_bounded_highbits_eq:
"\<lbrakk>x \<le> (y :: 'a::len word); y < (x >> n) + 1 << n\<rbrakk> \<Longrightarrow> x >> n = y >> n"
apply (cases "n < LENGTH('a)")
prefer 2
apply (simp add: shiftr_eq_0)
apply (drule_tac n=n in le_shiftr)
apply (subst (asm) word_shiftl_add_distrib)
apply (drule_tac word_less_sub_1)
apply (simp only: add_diff_eq[symmetric] mask_def[symmetric] and_not_mask[symmetric])
apply (drule_tac u=y and n=n in le_shiftr)
apply (subgoal_tac "(x && ~~ mask n) + mask n >> n \<le> x >> n")
apply fastforce
apply (subst aligned_shift')
apply (fastforce simp: mask_lt_2pn)
apply (fastforce simp: is_aligned_neg_mask)
apply fastforce
apply (fastforce simp: mask_shift)
done
lemma word_eq_cast_unsigned:
"(x = y) = (UCAST ('a signed \<rightarrow> ('a :: len)) x = ucast y)"
by (simp add: word_eq_iff nth_ucast)
lemma ran_tcb_cte_cases:
"ran tcb_cte_cases =
{(Structures_H.tcbCTable, tcbCTable_update),
(Structures_H.tcbVTable, tcbVTable_update),
(Structures_H.tcbReply, tcbReply_update),
(Structures_H.tcbCaller, tcbCaller_update),
(tcbIPCBufferFrame, tcbIPCBufferFrame_update)}"
by (auto simp add: tcb_cte_cases_def cteSizeBits_def split: if_split_asm)
lemma user_data_at_ko:
"typ_at' UserDataT p s \<Longrightarrow> ko_at' UserData p s"
apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def projectKOs)
apply (case_tac ko, auto)
done
lemma map_to_ko_atI:
"\<lbrakk>(projectKO_opt \<circ>\<^sub>m ksPSpace s) x = Some v;
pspace_aligned' s; pspace_distinct' s\<rbrakk>
\<Longrightarrow> ko_at' v x s"
apply (clarsimp simp: map_comp_Some_iff)
apply (erule (2) aligned_distinct_obj_atI')
apply (simp add: project_inject)
done
lemma map_to_ko_atI':
"\<lbrakk>(projectKO_opt \<circ>\<^sub>m (ksPSpace s)) x = Some v; invs' s\<rbrakk> \<Longrightarrow> ko_at' v x s"
apply (clarsimp simp: map_comp_Some_iff)
apply (erule aligned_distinct_obj_atI')
apply clarsimp
apply clarsimp
apply (simp add: project_inject)
done
(* FIXME: move up to SR_lemmas_C *)
lemma map_to_ko_atI2:
"\<lbrakk>(projectKO_opt \<circ>\<^sub>m (ksPSpace s)) x = Some v; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> ko_at' v x s"
apply (clarsimp simp: map_comp_Some_iff)
apply (erule (2) aligned_distinct_obj_atI')
apply (simp add: project_inject)
done
lemma map_to_ko_at_updI':
"\<And>x x' y y' y''.
\<lbrakk> (projectKO_opt \<circ>\<^sub>m (ksPSpace s)) x = Some y;
valid_pspace' s; ko_at' y' x' s;
objBitsKO (injectKO y') = objBitsKO y''; x \<noteq> x' \<rbrakk> \<Longrightarrow>
ko_at' y x (s\<lparr>ksPSpace := ksPSpace s(x' \<mapsto> y'')\<rparr>)"
by (fastforce simp: obj_at'_def projectKOs objBitsKO_def ps_clear_upd
dest: map_to_ko_atI2)
lemma ps_clear_upd_None:
"ksPSpace s y = None \<Longrightarrow>
ps_clear x n (ksPSpace_update (\<lambda>a. (ksPSpace s)(y := None)) s') = ps_clear x n s"
by (rule iffI | clarsimp elim!: ps_clear_domE | fastforce)+
(* FIXME move the thread_submonad stuff to SubMonad_R and use it for asUser *)
definition
"thread_fetch \<equiv> \<lambda>ext t s. case (ksPSpace s t) of
Some (KOTCB tcb) \<Rightarrow> ext tcb
| None \<Rightarrow> undefined"
definition
"thread_fetch_option \<equiv> \<lambda>ext t s. case (ksPSpace s t) of
Some (KOTCB tcb) \<Rightarrow> ext tcb
| None \<Rightarrow> None"
definition
"thread_replace \<equiv> \<lambda>upd t nv s.
let obj = case (ksPSpace s t) of
Some (KOTCB tcb) \<Rightarrow> Some (KOTCB (upd (\<lambda>_. nv) tcb))
| obj \<Rightarrow> obj
in s \<lparr> ksPSpace := (ksPSpace s) (t := obj) \<rparr>"
lemma thread_submonad_args:
"\<lbrakk> \<And>f v. ext (upd f v) = f (ext v);
\<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v;
\<And>f v. upd (\<lambda>_. ext v) v = v \<rbrakk> \<Longrightarrow>
submonad_args (thread_fetch ext t) (thread_replace upd t) (tcb_at' t)"
apply unfold_locales
apply (clarsimp simp: thread_fetch_def thread_replace_def
Let_def obj_at'_def projectKOs
split: kernel_object.split option.split)
apply (clarsimp simp: thread_replace_def Let_def
split: kernel_object.split option.split)
apply (clarsimp simp: thread_fetch_def thread_replace_def Let_def
fun_upd_idem
split: kernel_object.splits option.splits)
apply (clarsimp simp: obj_at'_def thread_replace_def Let_def projectKOs
split: kernel_object.splits option.splits)
apply (rename_tac tcb)
apply (case_tac tcb, simp add: objBitsKO_def ps_clear_def)
done
lemma tcbFault_submonad_args:
"submonad_args (thread_fetch tcbFault t) (thread_replace tcbFault_update t)
(tcb_at' t)"
apply (rule thread_submonad_args)
apply (case_tac v, simp)+
done
lemma threadGet_stateAssert_gets:
"threadGet ext t = do stateAssert (tcb_at' t) []; gets (thread_fetch ext t) od"
apply (rule is_stateAssert_gets [OF _ _ empty_fail_threadGet no_fail_threadGet])
apply (clarsimp intro!: obj_at_ko_at'[where P="\<lambda>tcb :: tcb. True", simplified]
| wp threadGet_wp)+
apply (clarsimp simp: obj_at'_def thread_fetch_def projectKOs)
done
lemma threadGet_tcbFault_submonad_fn:
"threadGet tcbFault t =
submonad_fn (thread_fetch tcbFault t) (thread_replace tcbFault_update t)
(tcb_at' t) get"
apply (rule ext)
apply (clarsimp simp: submonad_fn_def bind_assoc split_def)
apply (subst threadGet_stateAssert_gets, simp)
apply (rule bind_apply_cong [OF refl])
apply (clarsimp simp: in_monad bind_def gets_def get_def return_def
submonad_args.args(3) [OF tcbFault_submonad_args]
select_f_def modify_def put_def)
done
lemmas asUser_return = submonad.return [OF submonad_asUser]
lemmas asUser_bind_distrib =
submonad_bind [OF submonad_asUser submonad_asUser submonad_asUser]
lemma asUser_obj_at_notQ:
"\<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace>
asUser t (setRegister r v)
\<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace>"
apply (simp add: asUser_def)
apply (rule hoare_seq_ext)+
apply (simp add: split_def)
apply (rule threadSet_obj_at'_really_strongest)
apply (wp threadGet_wp |rule gets_inv|wpc|clarsimp)+
apply (clarsimp simp: obj_at'_def)
done
lemma empty_fail_asUser[iff]:
"empty_fail m \<Longrightarrow> empty_fail (asUser t m)"
apply (simp add: asUser_def split_def)
apply (intro empty_fail_bind, simp_all)
apply (simp add: select_f_def empty_fail_def)
done
lemma asUser_mapM_x:
"(\<And>x. empty_fail (f x)) \<Longrightarrow>
asUser t (mapM_x f xs) = do stateAssert (tcb_at' t) []; mapM_x (\<lambda>x. asUser t (f x)) xs od"
apply (simp add: mapM_x_mapM asUser_bind_distrib)
apply (subst submonad_mapM [OF submonad_asUser submonad_asUser])
apply simp
apply (simp add: asUser_return bind_assoc o_def)
apply (rule ext)
apply (rule bind_apply_cong [OF refl])+
apply (clarsimp simp: in_monad dest!: fst_stateAssertD)
apply (drule use_valid, rule mapM_wp', rule asUser_typ_ats, assumption)
apply (simp add: stateAssert_def get_def NonDetMonad.bind_def)
done
lemma asUser_threadGet_tcbFault_comm:
"empty_fail im \<Longrightarrow>
do y \<leftarrow> asUser t im;
x \<leftarrow> threadGet tcbFault t';
n x y
od =
do x \<leftarrow> threadGet tcbFault t';
asUser t im >>= n x
od"
apply (rule submonad_comm2 [OF tcbFault_submonad_args
threadGet_tcbFault_submonad_fn
submonad_asUser, symmetric])
apply (clarsimp simp: thread_replace_def asUser_replace_def Let_def
split: option.split)
apply (clarsimp simp: fun_upd_idem fun_upd_twist
split: kernel_object.split)
apply (rename_tac tcb)
apply (case_tac tcb, simp)
apply (clarsimp simp: asUser_replace_def Let_def obj_at'_real_def
ko_wp_at'_def ps_clear_upd_None ps_clear_upd
objBitsKO_def projectKOs
split: option.split kernel_object.split)
apply (clarsimp simp: thread_replace_def Let_def obj_at'_real_def
ko_wp_at'_def ps_clear_upd_None
ps_clear_upd objBitsKO_def projectKOs
split: option.split kernel_object.split)
apply (simp add: get_def empty_fail_def)
apply assumption
done
lemma asUser_getRegister_threadGet_comm:
"do
ra \<leftarrow> asUser a (getRegister r);
rb \<leftarrow> threadGet fb b;
c ra rb
od = do
rb \<leftarrow> threadGet fb b;
ra \<leftarrow> asUser a (getRegister r);
c ra rb
od"
by (rule bind_inv_inv_comm, auto; wp)
lemma threadGet_tcbFault_doMachineOp_comm:
"\<lbrakk> empty_fail m' \<rbrakk> \<Longrightarrow>
do x \<leftarrow> threadGet tcbFault t; y \<leftarrow> doMachineOp m'; n x y od =
do y \<leftarrow> doMachineOp m'; x \<leftarrow> threadGet tcbFault t; n x y od"
apply (rule submonad_comm2 [OF tcbFault_submonad_args
threadGet_tcbFault_submonad_fn
submonad_doMachineOp])
apply (simp add: thread_replace_def Let_def)
apply simp
apply (rule refl)
apply (simp add: get_def empty_fail_def)
apply assumption
done
lemma getObject_tcb_det:
"(r::tcb,s') \<in> fst (getObject p s) \<Longrightarrow> fst (getObject p s) = {(r,s)} \<and> s' = s"
apply (clarsimp simp add: getObject_def bind_def get_def gets_def
return_def loadObject_default_def split_def)
apply (clarsimp split: kernel_object.split_asm if_split_asm option.split_asm
simp: in_monad typeError_def alignError_def magnitudeCheck_def
objBits_def objBitsKO_def projectKOs
lookupAround2_def Let_def o_def)
apply (simp_all add: bind_def return_def assert_opt_def split_def projectKOs
alignCheck_def is_aligned_mask[symmetric]
unless_def when_def magnitudeCheck_def)
done
lemma threadGet_again:
"\<And>rv s s' n. (rv, s') \<in> fst (threadGet ext t s) \<Longrightarrow>
(threadGet ext t >>= n) s' = n rv s'"
apply (clarsimp simp add: threadGet_def liftM_def in_monad)
apply (frule use_valid [OF _ getObject_obj_at'])
apply (simp add: objBits_simps')+
apply (frule getObject_tcb_det)
apply (clarsimp simp: bind_def split_def)
apply (insert no_fail_getObject_tcb)
apply (clarsimp simp: no_fail_def obj_at'_def is_tcb)
done
lemma setMRs_Nil:
"setMRs thread buffer [] = stateAssert (tcb_at' thread) [] >>= (\<lambda>_. return 0)"
unfolding setMRs_def
by (simp add: zipWithM_x_def sequence_x_def zipWith_def
asUser_return)
lemma device_data_at_ko:
"typ_at' UserDataDeviceT p s \<Longrightarrow> ko_at' UserDataDevice p s"
apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def
projectKO_user_data_device projectKO_eq projectKO_eq2)
apply (case_tac ko, auto)
done
lemma empty_fail_rethrowFailure:
"empty_fail f \<Longrightarrow> empty_fail (rethrowFailure fn f)"
apply (simp add: rethrowFailure_def handleE'_def)
apply (erule empty_fail_bind)
apply (simp split: sum.split)
done
lemma empty_fail_resolveAddressBits:
"empty_fail (resolveAddressBits cap cptr bits)"
proof -
note empty_fail_assertE[iff]
show ?thesis
apply (rule empty_fail_use_cutMon)
apply (induct rule: resolveAddressBits.induct)
apply (subst resolveAddressBits.simps)
apply (unfold Let_def cnode_cap_case_if fun_app_def
K_bind_def haskell_assertE_def split_def)
apply (intro empty_fail_cutMon_intros)
apply (clarsimp simp: empty_fail_drop_cutMon empty_fail_whenEs
locateSlot_conv returnOk_liftE[symmetric]
isCap_simps)+
done
qed
lemma mapM_only_length:
"do ys \<leftarrow> mapM f xs;
g (length ys)
od =
do _ \<leftarrow> mapM_x f xs;
g (length xs)
od"
by (subst bind_return_subst [OF mapM_length])
(rule mapM_discarded)
lemma tcb_aligned':
"tcb_at' t s \<Longrightarrow> is_aligned t tcbBlockSizeBits"
apply (drule obj_at_aligned')
apply (simp add: objBits_simps)
apply (simp add: objBits_simps)
done
lemma cte_at_0' [dest!]:
"\<lbrakk> cte_at' 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> False"
apply (clarsimp simp: cte_wp_at_obj_cases')
by (auto simp: tcb_cte_cases_def is_aligned_def objBits_simps' dest!:tcb_aligned' split: if_split_asm)
lemma getMessageInfo_le3:
"\<lbrace>\<top>\<rbrace> getMessageInfo sender \<lbrace>\<lambda>rv s. unat (msgExtraCaps rv) \<le> 3\<rbrace>"
including no_pre
apply (simp add: getMessageInfo_def)
apply wp
apply (rule_tac Q="\<lambda>_. \<top>" in hoare_strengthen_post)
apply wp
apply (simp add: messageInfoFromWord_def Let_def msgExtraCapBits_def)
apply (cut_tac y="r >> Types_H.msgLengthBits" in word_and_le1 [where a=3])
apply (simp add: word_le_nat_alt)
done
lemma getMessageInfo_msgLength:
"\<lbrace>\<top>\<rbrace> getMessageInfo sender \<lbrace>\<lambda>rv. K (unat (msgLength rv) \<le> msgMaxLength)\<rbrace>"
including no_pre
apply (simp add: getMessageInfo_def)
apply wp
apply (rule_tac Q="\<lambda>_. \<top>" in hoare_strengthen_post)
apply wp
apply (simp add: messageInfoFromWord_def Let_def not_less msgMaxLength_def msgLengthBits_def
split: if_split)
apply (cut_tac y="r" in word_and_le1 [where a="0x7F"])
apply (simp add: word_le_nat_alt)
done
lemma cancelAllIPC_sch_act_wf:
"\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
cancelAllIPC ep
\<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: cancelAllIPC_def)
apply (rule hoare_TrueI|wp getEndpoint_wp|wpc|simp)+
apply fastforce?
done
lemma cancelAllSignals_sch_act_wf:
"\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
cancelAllSignals ep
\<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: cancelAllSignals_def)
apply (rule hoare_TrueI|wp getNotification_wp|wpc|simp)+
apply fastforce?
done
lemma cteDeleteOne_sch_act_wf:
"\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
cteDeleteOne slot
\<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: cteDeleteOne_def unless_when split_def)
apply (simp add: finaliseCapTrue_standin_def Let_def)
apply (rule hoare_pre)
apply (wp isFinalCapability_inv cancelAllSignals_sch_act_wf
cancelAllIPC_sch_act_wf getCTE_wp' static_imp_wp
| wpc
| simp add: Let_def split: if_split)+
done
lemma vp_invs_strg': "invs' s \<longrightarrow> valid_pspace' s" by auto
lemma setCTE_tcbFault:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
setCTE slot cte
\<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>"
apply (simp add: setCTE_def)
apply (rule setObject_cte_obj_at_tcb', simp_all)
done
lemmas threadSet_obj_at' = threadSet_obj_at'_strongish
lemmas setEndpoint_tcb = KHeap_R.setEndpoint_obj_at'_tcb
lemma setNotification_tcb:
"\<lbrace>obj_at' (\<lambda>tcb::tcb. P tcb) t\<rbrace>
setNotification ntfn e
\<lbrace>\<lambda>_. obj_at' P t\<rbrace>"
apply (simp add: setNotification_def)
apply (rule obj_at_setObject2)
apply (clarsimp simp: updateObject_default_def in_monad)
done
lemma state_refs_of'_upd:
"\<lbrakk> valid_pspace' s; ko_wp_at' (\<lambda>ko. objBitsKO ko = objBitsKO ko') ptr s \<rbrakk> \<Longrightarrow>
state_refs_of' (s\<lparr>ksPSpace := ksPSpace s(ptr \<mapsto> ko')\<rparr>) =
(state_refs_of' s)(ptr := refs_of' ko')"
apply (rule ext)
apply (clarsimp simp: ps_clear_upd valid_pspace'_def pspace_aligned'_def
obj_at'_def ko_wp_at'_def state_refs_of'_def
split: option.split if_split)
done
lemma ex_st_tcb_at'_simp[simp]:
"(\<exists>ts. st_tcb_at' ((=) ts) dest s) = tcb_at' dest s"
by (auto simp add: pred_tcb_at'_def obj_at'_def)
lemma threadGet_wp:
"\<lbrace>\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> P (f tcb) s\<rbrace> threadGet f thread \<lbrace>P\<rbrace>"
apply (rule hoare_post_imp [OF _ tg_sp'])
apply clarsimp
apply (frule obj_at_ko_at')
apply (clarsimp elim: obj_atE')
done
lemma threadGet_wp'':
"\<lbrace>\<lambda>s. \<forall>v. obj_at' (\<lambda>tcb. f tcb = v) thread s \<longrightarrow> P v s\<rbrace> threadGet f thread \<lbrace>P\<rbrace>"
apply (rule hoare_pre)
apply (rule threadGet_wp)
apply (clarsimp simp: obj_at'_def)
done
lemma dom_less_0x10_helper:
"d \<le> maxDomain \<Longrightarrow> (ucast d :: machine_word) < 0x10"
unfolding maxDomain_def numDomains_def
by (clarsimp simp add: word_less_nat_alt unat_ucast_upcast is_up word_le_nat_alt)
lemma filter_empty_unfiltered_contr:
"\<lbrakk> [x\<leftarrow>xs . x \<noteq> y] = [] ; x' \<in> set xs ; x' \<noteq> y \<rbrakk> \<Longrightarrow> False"
by (induct xs, auto split: if_split_asm)
lemma filter_noteq_op:
"[x \<leftarrow> xs . x \<noteq> y] = filter ((\<noteq>) y) xs"
by (induct xs) auto
lemma all_filter_propI:
"\<forall>x\<in>set lst. P x \<Longrightarrow> \<forall>x\<in>set (filter Q lst). P x"
by (induct lst, auto)
lemma returnOK_catch[simp]:
"(returnOk rv <catch> m) = return rv"
unfolding catch_def returnOk_def
by clarsimp
lemma ignoreFailure_liftM:
"ignoreFailure = liftM (\<lambda>v. ())"
apply (rule ext)+
apply (simp add: ignoreFailure_def liftM_def
catch_def)
apply (rule bind_apply_cong[OF refl])
apply (simp split: sum.split)
done
lemma dom_eq:
"dom um = dom um' \<longleftrightarrow> (\<forall>a. um a = None \<longleftrightarrow> um' a = None)"
apply (simp add: dom_def del: not_None_eq)
apply (rule iffI)
apply (rule allI)
apply (simp add: set_eq_iff)