-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathHoare_Logic.thy
1390 lines (1107 loc) · 52.9 KB
/
Hoare_Logic.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
theory Hoare_Logic
imports ProcessEpoch
Fun_Algebra
Word_Lib.More_Divides Word_Lib.Word_EqI
Word_Lib.Word_64 Word_Lib.Bitwise Word_Lib.Word_Lemmas
begin
declare [[show_sorts=false]]
lemma map_insort_sorted: "mono f \<Longrightarrow> sorted xs \<Longrightarrow> map f (insort a xs) = insort (f a) (map f xs)"
apply (induct xs; clarsimp)
apply (safe)
using monoD apply blast
using monoD apply blast
apply (simp add: monoD order_antisym)
by (smt (verit) insort_is_Cons insort_key.simps(2)
linorder_le_cases list.set_cases list.set_intros(1) list.simps(9) monotoneD order_antisym)
lemma Id_on_relcomp_eq: "Id_on P O Id_on Q = Id_on (P \<inter> Q)"
by (safe; clarsimp simp: Id_on_def, rule relcompI, blast, blast)
(* instantiation option :: (type) stronger_sep_algebra begin
fun sep_disj_option :: "'b option \<Rightarrow> 'b option \<Rightarrow> bool" where
"sep_disj_option (Some x) (Some y) = False" |
"sep_disj_option x y = True"
fun plus_option where
"plus_option (Some x) (Some y) = Some x" |
"plus_option (None) y = y" |
"plus_option x (None) = x"
*)
lemma [simp]: "x + None = x"
by (case_tac x; clarsimp simp: plus_option_def)
(* definition "zero_option = None"
instance
apply (standard, case_tac x; (clarsimp simp: zero_option_def)?)
apply (case_tac x; case_tac y; clarsimp)
apply (case_tac x; case_tac y; clarsimp)
apply (case_tac x; case_tac y; clarsimp)
apply (case_tac x; case_tac y; case_tac z; clarsimp)
done
end
*)
(* instantiation "fun" :: (type, stronger_sep_algebra) stronger_sep_algebra begin
definition sep_disj_fun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
"sep_disj_fun f g \<equiv> (\<forall>x. f x ## g x)"
definition plus_fun where
"plus_fun f g = (\<lambda>x. f x + g x)"
lemma [simp]: "x + None = x"
by (case_tac x; clarsimp)
definition "zero_fun = (\<lambda>x. 0)"
instance
apply (standard; (rule ext)?, (clarsimp simp: plus_fun_def sep_disj_fun_def zero_fun_def)? )
apply (metis sep_disj_commute)
apply (metis sep_add_commute)
apply (metis sep_add_assoc)
apply (blast)
done
end
*)
(* instantiation prod :: (stronger_sep_algebra, stronger_sep_algebra) stronger_sep_algebra begin
fun sep_disj_prod :: "'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" where
"sep_disj_prod (a,b) (x,y) \<longleftrightarrow> (a ## x \<and> b ## y)"
fun plus_prod where
"plus_prod (a,b) (x,y) = (a + x, b + y)"
definition "zero_prod = (0,0)"
instance
apply (standard, case_tac x; (clarsimp simp: zero_prod_def split: prod.splits)?)
apply (metis sep_disj_commute)
apply (metis sep_add_commute)
apply (metis sep_add_assoc)
by blast
end
*)
sorry
text \<open>
lemma "valid_lens a \<Longrightarrow> valid_lens b \<Longrightarrow> valid_lens c \<Longrightarrow>
(\<lambda>s. set b s v) o (\<lambda>s. set c s v') = (\<lambda>s. set c s v') o (\<lambda>s. set b s v) \<Longrightarrow>
(\<lambda>s. set a s v'') o ((\<lambda>s. set b s v) o (\<lambda>s. set c s v')) =
((\<lambda>s. set b (s :: bool \<times> bool \<times> bool) v) o (\<lambda>s. set c s v')) o (\<lambda>s. set a s v'') \<Longrightarrow>
(\<lambda>s. set a s v'') o (\<lambda>s. set b s v) = (\<lambda>s. set b s v) o (\<lambda>s. set a s v'')"
apply (frule lens_commute_cases, assumption, assumption)
apply (elim disjE)
apply simp
apply (clarsimp)
apply (intro ext; clarsimp?)
sledgehammer
oops
apply (frule lens_commute_cases, assumption, assumption)
apply (elim disjE; clarsimp)
apply (smt (verit, ccfv_SIG) fun.map_comp)
apply (rule lens_commuteI, assumption, assumption)
apply (clarsimp)
oops
apply (clarsimp simp: valid_lens_def)
apply (drule_tac x=x in fun_cong) back
apply (clarsimp)
\<close>
instantiation p_set :: (type) sep_algebra begin
definition "sep_disj_p_set x y \<equiv> disj_cylindric_set (set_of x) (set_of y) "
definition "plus_p_set x y \<equiv> Abs_p_set (Pair ({h. \<exists>f\<in>(set_of x). \<exists>g\<in>(set_of y). h = f o g}) (point_of x o point_of y))"
lemma set_of_plus_domain_iff: "set_of ( x + y) = {h. \<exists>f\<in>(set_of x). \<exists>g\<in>(set_of y). h = f o g}"
apply (subst set_of_def)
apply (subst plus_p_set_def)
apply (subst Abs_p_set_inverse; clarsimp)
apply (intro conjI)
apply (rule_tac x="point_of x" in bexI; clarsimp?)
apply (rule_tac x="point_of y" in bexI; clarsimp?)
by (rule_tac x=id in bexI;clarsimp)
lemma point_of_plus_domain_iff: "point_of ( x + y) = point_of x o point_of y"
apply (subst point_of_def)
apply (subst plus_p_set_def)
apply (subst Abs_p_set_inverse; clarsimp)
apply (intro conjI)
apply (rule_tac x="point_of x" in bexI; clarsimp?)
apply (rule_tac x="point_of y" in bexI; clarsimp?)
by (rule_tac x=id in bexI;clarsimp)
lemmas plus_p_simps = point_of_plus_domain_iff set_of_plus_domain_iff
definition "zero_p_set \<equiv> id_p"
instance
apply (standard)
apply (clarsimp simp: sep_disj_p_set_def zero_p_set_def disj_cylindric_set_def)
apply (clarsimp simp: sep_disj_p_set_def zero_p_set_def disj_cylindric_set_def)
apply (rule p_set_eqI; clarsimp simp: point_of_plus_domain_iff set_of_plus_domain_iff zero_p_set_def)
apply (rule p_set_eqI; clarsimp simp: plus_p_simps zero_p_set_def)
apply (clarsimp simp: sep_disj_p_set_def zero_p_set_def disj_cylindric_set_def)
apply (intro set_eqI iffI; clarsimp)
apply blast
apply metis
apply (clarsimp simp: sep_disj_p_set_def zero_p_set_def disj_cylindric_set_def)
using point_in_set apply blast
apply (clarsimp simp: sep_disj_p_set_def zero_p_set_def disj_cylindric_set_def)
apply (intro p_set_eqI set_eqI iffI; clarsimp simp: plus_p_simps)
apply (metis comp_assoc)
apply (metis comp_assoc)
apply (meson comp_assoc)
apply (clarsimp simp: plus_p_simps sep_disj_p_set_def zero_p_set_def disj_cylindric_set_def)
apply (metis comp_id id_in_set)
apply (clarsimp simp: plus_p_simps sep_disj_p_set_def zero_p_set_def disj_cylindric_set_def)
by (metis (no_types, lifting) comp_assoc fun.map_id0 id_apply id_in_set)
end
definition "maps_to l v \<equiv> \<lambda>D. valid_lens l \<and>
set_of D = ({f. (\<exists>v. (\<lambda>s. set l s v) = f)} \<union> {id}) \<and> point_of D = (\<lambda>s. set l s (Some v))"
notation maps_to (infixl "\<mapsto>\<^sub>l" 50)
definition "lift P s = (\<exists>S. P S \<and> point_of S s = s)"
notation lift ("\<lless>_\<then>")
instantiation BeaconState_ext :: (stronger_sep_algebra) stronger_sep_algebra begin
definition sep_disj_BeaconState_ext :: "'a BeaconState_scheme \<Rightarrow> 'a BeaconState_scheme \<Rightarrow> bool"
where "sep_disj_BeaconState_ext x y == x = y"
text \<open> definition sep_disj_BeaconState_ext :: "'a BeaconState_scheme \<Rightarrow> 'a BeaconState_scheme \<Rightarrow> bool"
where "sep_disj_BeaconState_ext x y ==
genesis_time_f x ## genesis_time_f y \<and>
genesis_validators_root_f x ## genesis_validators_root_f y \<and>
slot_f x ## slot_f y \<and> fork_f x ## fork_f y \<and>
latest_block_header_f x ## latest_block_header_f y \<and>
block_roots_f x ## block_roots_f y \<and>
state_roots_f x ## state_roots_f y \<and>
historical_roots_f x ## historical_roots_f y \<and>
eth1_data_f x ## eth1_data_f y \<and>
eth1_data_votes_f x ## eth1_data_votes_f y \<and>
eth1_deposit_index_f x ## eth1_deposit_index_f y \<and>
validators_f x ## validators_f y \<and>
balances_f x ## balances_f y \<and>
randao_mixes_f x ## randao_mixes_f y \<and>
slashings_f x ## slashings_f y \<and>
previous_epoch_participation_f x ## previous_epoch_participation_f y \<and>
current_epoch_participation_f x ## current_epoch_participation_f y \<and>
justification_bits_f x ## justification_bits_f y \<and>
previous_justified_checkpoint_f x ## previous_justified_checkpoint_f y \<and>
current_justified_checkpoint_f x ## current_justified_checkpoint_f y \<and>
finalized_checkpoint_f x ## finalized_checkpoint_f y \<and>
inactivity_scores_f x ## inactivity_scores_f y \<and>
current_sync_committee_f x ## current_sync_committee_f y \<and>
next_sync_committee_f x ## next_sync_committee_f y \<and>
latest_execution_payload_header x ## latest_execution_payload_header y \<and>
next_withdrawal_index_f x ## next_withdrawal_index_f y \<and>
next_withdrawal_validator_index_f x ## next_withdrawal_validator_index_f y \<and>
historical_summaries_f x ## historical_summaries_f y \<and> BeaconState.more x ## BeaconState.more y" \<close>
definition plus_BeaconState_ext :: "'a BeaconState_scheme \<Rightarrow> 'a BeaconState_scheme \<Rightarrow> 'a BeaconState_scheme"
where "plus_BeaconState_ext x y == x"
text \<open>definition plus_BeaconState_ext :: "'a BeaconState_scheme \<Rightarrow> 'a BeaconState_scheme \<Rightarrow> 'a BeaconState_scheme"
where "plus_BeaconState_ext x y ==
\<lparr> genesis_time_f = genesis_time_f x + genesis_time_f y,
genesis_validators_root_f = genesis_validators_root_f x + genesis_validators_root_f y,
slot_f = slot_f x + slot_f y, fork_f = fork_f x + fork_f y ,
latest_block_header_f = latest_block_header_f x + latest_block_header_f y ,
block_roots_f = block_roots_f x + block_roots_f y,
state_roots_f = state_roots_f x + state_roots_f y ,
historical_roots_f = historical_roots_f x + historical_roots_f y,
eth1_data_f = eth1_data_f x + eth1_data_f y,
eth1_data_votes_f = eth1_data_votes_f x + eth1_data_votes_f y,
eth1_deposit_index_f = eth1_deposit_index_f x + eth1_deposit_index_f y,
validators_f = validators_f x + validators_f y,
balances_f = balances_f x + balances_f y,
randao_mixes_f = randao_mixes_f x + randao_mixes_f y,
slashings_f = slashings_f x + slashings_f y,
previous_epoch_participation_f = previous_epoch_participation_f x + previous_epoch_participation_f y,
current_epoch_participation_f = current_epoch_participation_f x + current_epoch_participation_f y,
justification_bits_f = justification_bits_f x + justification_bits_f y,
previous_justified_checkpoint_f = previous_justified_checkpoint_f x + previous_justified_checkpoint_f y,
current_justified_checkpoint_f = current_justified_checkpoint_f x + current_justified_checkpoint_f y,
finalized_checkpoint_f = finalized_checkpoint_f x + finalized_checkpoint_f y,
inactivity_scores_f = inactivity_scores_f x + inactivity_scores_f y,
current_sync_committee_f = current_sync_committee_f x + current_sync_committee_f y,
next_sync_committee_f = next_sync_committee_f x + next_sync_committee_f y,
latest_execution_payload_header = latest_execution_payload_header x + latest_execution_payload_header y,
next_withdrawal_index_f = next_withdrawal_index_f x + next_withdrawal_index_f y,
next_withdrawal_validator_index_f = next_withdrawal_validator_index_f x + next_withdrawal_validator_index_f y,
historical_summaries_f = historical_summaries_f x + historical_summaries_f y,
\<dots> = BeaconState.more x + BeaconState.more y \<rparr>"\<close>
definition "zero_BeaconState_ext \<equiv> \<lparr> genesis_time_f = None,
genesis_validators_root_f = None,
slot_f = None, fork_f = None ,
latest_block_header_f = None ,
block_roots_f = None,
state_roots_f = None ,
historical_roots_f = None,
eth1_data_f = None,
eth1_data_votes_f = None,
eth1_deposit_index_f = None,
validators_f = None,
balances_f = None,
randao_mixes_f = None,
slashings_f = None,
previous_epoch_participation_f = None,
current_epoch_participation_f = None,
justification_bits_f = None,
previous_justified_checkpoint_f = None,
current_justified_checkpoint_f = None,
finalized_checkpoint_f = None,
inactivity_scores_f = None,
current_sync_committee_f = None,
next_sync_committee_f = None,
latest_execution_payload_header = None,
next_withdrawal_index_f = None,
next_withdrawal_validator_index_f = None,
historical_summaries_f = None, \<dots> = 0\<rparr>"
instance
apply (standard; (clarsimp simp: plus_BeaconState_ext_def sep_disj_BeaconState_ext_def zero_BeaconState_ext_def)?)
sorry
apply (clarsimp simp: sep_disj_commute)
apply (simp add: sep_disj_commute)
apply (metis sep_add_commute)
apply (intro conjI; metis sep_add_assoc)
apply (safe; clarsimp)
done
end
instantiation BeaconState_ext :: (cancellative_sep_algebra) cancellative_sep_algebra begin
instance
apply (standard; (clarsimp simp: plus_BeaconState_ext_def sep_disj_BeaconState_ext_def zero_BeaconState_ext_def)?)
using Extended_Separation_Algebra.cancellative_sep_algebra_class.sep_add_cancelD apply blast+
done
end
locale hoare_logic = verified_con + strong_spec begin
definition "hoare_triple P f Q \<equiv> run f \<le> assert (Collect P); spec (UNIV \<triangleright> (Collect Q)) "
notation hoare_triple ("\<lblot>_\<rblot> _ \<lblot>_\<rblot>")
lemma hoare_strengthen_post: "hoare_triple P f Q' \<Longrightarrow> Q' \<le> Q \<Longrightarrow> hoare_triple P f Q"
apply (clarsimp simp: hoare_triple_def le_fun_def)
apply (rule order_trans)
apply (assumption)
apply (rule seq_mono)
using assert_iso apply blast
apply (rule spec_strengthen)
by (simp add: Collect_mono_iff range_restrict_p_mono)
lemma hoare_weaken_pre: "hoare_triple P' f Q \<Longrightarrow> P \<le> P' \<Longrightarrow> hoare_triple P f Q"
apply (clarsimp simp: hoare_triple_def)
apply (rule order_trans)
apply (assumption)
apply (rule seq_mono)
using assert_iso apply blast
by (clarsimp)
lemma setState_spec: "(run (setState s)) \<le> spec (UNIV \<triangleright> {s}) "
apply (clarsimp simp: spec_def)
apply (rule conj_refine)
apply (clarsimp simp: run_def setState_def)
using pspec_ref_pgm apply presburger
apply (clarsimp simp: run_def setState_def)
by (meson order_trans spec_ref_pgm spec_term)
lemma set_state_valid: "hoare_triple \<top> (setState s) (eq s)"
apply (clarsimp simp: hoare_triple_def assert_top)
by (metis assert_top seq_nil_left setState_spec top_set_def)
lemma getState_spec: "(run (getState)) \<le> spec (UNIV) "
apply (clarsimp simp: spec_def)
apply (rule conj_refine)
apply (clarsimp simp: run_def getState_def)
apply (simp add: Nondet_test_nil chaos_ref_nil pspec_univ)
apply (clarsimp simp: run_def getState_def)
by (simp add: Nondet_test_nil term_nil)
lemma getState_valid: "hoare_triple \<top> (getState) \<top>"
apply (clarsimp simp: hoare_triple_def assert_top)
apply (simp add: getState_spec spec_test_restricts test_top)
by (metis UNIV_eq_I assert_top getState_spec mem_Collect_eq
seq_nil_left seq_nil_right test_top top1I)
definition "bind_rel P Q = (Id_on P) O Q "
lemma pgm_post_assert: "\<pi> (UNIV \<triangleright> S) = \<pi> (UNIV \<triangleright> S) ; assert S"
by (metis pgm_test_post seq_assoc test_seq_assert)
lemma rewrite: "UNIV \<triangleright> (Q `` (P \<inter> {s})) = (UNIV \<triangleright> {s}) O (P \<triangleleft> Q) "
apply (safe; clarsimp simp: Image_iff restrict_range_def restrict_domain_def)
by blast
lemma stutter_range_restriction: "a \<in> P \<Longrightarrow> (a,a) \<in> range_restriction P"
apply (clarsimp)
done
lemma restrict_domain_compose_Id: "(P \<triangleleft> Q) = ((Id_on P) O Q)"
apply (rule set_eqI)
apply (safe)
apply (clarsimp simp: restrict_range_def restrict_domain_def, rule relcompI)
apply (erule Id_onI, assumption)
by (clarsimp simp: restrict_range_def restrict_domain_def)
lemma test_smaller_assert: "p \<subseteq> q \<Longrightarrow> test p ; assert q = test p"
apply (clarsimp simp: assert_def)
apply (subst par.seq_nondet_distrib)
by (metis assert_bot le_iff_inf seq_assoc sup_bot.right_neutral test.hom_bot test_seq_assert test_seq_compl test_seq_magic test_seq_test)
lemma hoare_chain: "(\<lbrace>P\<rbrace>;\<lparr>Q\<rparr>; \<lbrace>P'\<rbrace>;\<lparr>Q'\<rparr>) \<le> \<lbrace>P - (converse Q `` (-P'))\<rbrace>;\<lparr>(Q) O Q'\<rparr>"
apply (subst assert_restricts_spec) back
apply (subst assert_galois_test)
apply (subst domain_restrict_relcomp[symmetric])
apply (rule order_trans[rotated], rule spec_seq_introduce[where p="P'"])
apply (rule_tac y="(\<tau> (P - Q\<inverse> `` (- P')) ; \<lbrace>P\<rbrace> ; \<lparr>Q\<rparr>) ; (\<lbrace>P'\<rbrace> ; \<lparr>Q'\<rparr>)" in order_trans)
apply (clarsimp simp: seq_assoc)
apply (subst seq_assoc, rule seq_mono[rotated], rule order_refl)
apply ( subst test_smaller_assert)
apply (blast)
apply (subst test_seq_refine)
apply (subst test_restricts_spec)
apply (rule seq_mono, rule order_refl)
apply (rule spec_strengthen)
apply (clarsimp simp: restrict_domain_def restrict_range_def Image_iff)
apply (blast)
done
lemma set_state_hoare_inner: "\<pi> (UNIV \<triangleright> {s}) \<le> \<lbrace>UNIV\<rbrace> ; spec (UNIV \<triangleright> {s})"
by (simp add: assert_top spec_ref_pgm)
lemma univ_sub_neg: "UNIV - P = - P"
apply (safe; clarsimp)
done
lemma setState_seq': "run (g ()) \<le> spec P \<Longrightarrow> (run (do {x <- setState s ; g x})) \<le> spec (UNIV \<triangleright> {s} O P) "
apply (clarsimp simp: run_def bindCont_def setState_def)
apply (rule order_trans[rotated], rule spec_to_sequential)
apply (rule seq_mono)
apply (rule spec_ref_pgm)
apply (assumption)
done
lemma spec_ref_pspec: "spec P \<le> pspec P "
apply (clarsimp simp: spec_def)
by (simp add: conj_conjoin_non_aborting term_nonaborting)
lemma specI: "x \<le> term \<Longrightarrow> x \<le> pspec P \<Longrightarrow> x \<le> spec P"
apply (clarsimp simp: spec_def)
apply (rule conj_refine, assumption+)
done
lemma pspec_strengthen: "p \<subseteq> q \<Longrightarrow> pspec p \<le> pspec q" by (erule pspec_strengthen)
lemma spec_strengthen: "p \<subseteq> q \<Longrightarrow> spec p \<le> spec q" by (erule spec_strengthen)
lemma restrict_dom_singleton: "restrict_domain {x} {x. P x} = {(a,b). a = x \<and> P (a, b) }"
apply (clarsimp simp: restrict_domain_def)
apply (safe)
done
lemma assert_commute: "assert a ; assert b = assert b ; assert a"
by (simp add: Int_commute assert_seq_assert)
lemma test_spec: "test {t} \<le> \<lbrace>UNIV\<rbrace> ; \<lparr>Id_on {t}\<rparr>"
apply (clarsimp simp: assert_top)
apply (rule spec_refine)
using dual_order.trans nil_ref_test term_nil apply blast
apply (clarsimp)
using test_inf_eq_seq test_seq_commute test_seq_refine by fastforce
named_theorems wp
lemma getState_seq: "(\<And>x. run (g x) \<le> spec (P x)) \<Longrightarrow> (run (do { x <- getState ; g (x)})) \<le> spec ({(s, s'). (s, s') \<in> P s}) "
apply (clarsimp simp: run_def bindCont_def getState_def)
apply (rule specI)
apply (subst Sup_le_iff, clarsimp)
apply (atomize)
apply (erule_tac x="a" in allE)
apply (erule_tac x="b" in allE)
using nil_ref_test order_trans seq_mono spec_def spec_term apply fastforce
apply (subst Sup_le_iff, clarsimp)
apply (atomize)
apply (erule_tac x="a" in allE)
apply (erule_tac x="b" in allE)
apply (drule order_trans, rule spec_ref_pspec)
apply (rule order_trans, rule seq_mono, rule order_refl, assumption)
apply (subst test_seq_refine)
apply (subst test_restricts_pspec)
apply (subst test_restricts_pspec) back
apply (rule seq_mono, rule order_refl)
apply (rule pspec_strengthen)
apply (subst restrict_dom_singleton)
apply (clarsimp simp: restrict_domain_def)
done
lemma test_refines_id_spec: "\<tau> S \<le> spec (Id_on S) "
apply (rule spec_refine; clarsimp?)
using dual_order.trans nil_ref_test term_nil apply blast
using test_inf_eq_seq test_seq_commute test_seq_refine by auto
lemma test_inf_singletons: "(\<tau> {x} \<sqinter> \<tau> {xa}) = (if x = xa then test {x} else \<bottom>)"
by (metis Int_empty_right Int_insert_right_if0 insert_inter_insert singletonD test.hom_bot test.hom_inf)
lemma test_prefix_spec: "\<tau> {x} ; spec P \<le> spec {(a, b). a = x \<and> (a, b) \<in> P}"
apply (subst test_seq_refine)
apply (subst test_restricts_spec)
apply (subst test_restricts_spec)
apply (rule seq_mono; clarsimp?)
apply (rule spec_strengthen)
apply (clarsimp simp: restrict_range_def restrict_domain_def restrict_dom_singleton Sup_le_iff)
done
lemma spec_singletonI[intro!]: "x \<in> S \<Longrightarrow> \<lparr>{x}\<rparr> \<le> \<lparr>S\<rparr>"
by (simp add: spec_strengthen)
lemma hoare_anti_mono: "hoare_triple P' f Q' \<Longrightarrow> P \<le> P' \<Longrightarrow> Q' \<le> Q \<Longrightarrow> hoare_triple P f Q"
apply (clarsimp simp: hoare_triple_def)
apply (rule order_trans)
apply (assumption)
apply (rule seq_mono)
using assert_iso apply blast
apply (rule spec_strengthen)
by (safe; clarsimp simp: restrict_range_def le_fun_def)
lemma restrict_range_UNIV[simp]: "UNIV \<triangleright> S = UNIV \<times> S "
by (safe; clarsimp simp: restrict_range_def)
lemma restrict_domain_UNIV[simp]: "UNIV \<triangleleft> R = R "
by (safe; clarsimp simp: restrict_domain_def)
lemma return_triple'[wp]: "(\<lblot>P\<rblot> (C v) \<lblot>Q\<rblot>) \<Longrightarrow> \<lblot>P\<rblot> (bindCont (return v) C) \<lblot>Q\<rblot>"
apply (clarsimp simp: bindCont_return')
done
lemma if_seq:
"run (bindCont P c) \<le> assert S ; spec R \<Longrightarrow> run (bindCont Q c) \<le> assert S' ; spec R' \<Longrightarrow>
run (do {x <- (if B then P else Q); c x}) \<le> assert (if B then S else S') ; spec (if B then R else R')"
apply (clarsimp split: if_splits)
done
lemma if_seq_valid:
"hoare_triple S (bindCont P c) R \<Longrightarrow> hoare_triple S' (bindCont Q c) R' \<Longrightarrow>
hoare_triple (if B then S else S') (do {x <- (if B then P else Q); c x}) (if B then R else R')"
apply (clarsimp split: if_splits)
done
lemmas if_seq_valid' = if_seq_valid[where c=return, simplified bindCont_return]
lemma run_fail_assert: "run (bindCont fail c) \<le> assert {} ; \<lparr>{}\<rparr>"
apply (clarsimp simp: run_def fail_def bindCont_def spec_def pspec_def assert_def)
using assert_bot local.assert_def by force
lemma Collect_bot[simp]:"Collect \<bottom> = {}"
apply (clarsimp)
done
lemma run_fail_assert_valid: "hoare_triple \<bottom> (bindCont fail c) R"
apply (clarsimp simp: run_def fail_def bindCont_def spec_def pspec_def assert_def hoare_triple_def)
using assert_bot local.assert_def by force
declare in_dom_iff[simp]
lemma "x \<in> S \<triangleleft> R \<longleftrightarrow> fst x \<in> S \<and> x \<in> R"
by (clarsimp simp: restrict_domain_def, safe; clarsimp)
definition "wf_lens l \<longleftrightarrow> (\<forall>s v. get l (set l s v) = v)"
text \<open>definition "maps_to l v s \<equiv> wf_lens l \<and> get l (fst s) = Some v \<and> valid l (Some v)" \<close>
lemma restrict_UNIV_times: "P \<triangleleft> (UNIV \<times> R) = (P \<times> R)"
by (safe; clarsimp)
lemma spec_ref_pgm':"R \<subseteq> R' \<Longrightarrow> pgm R \<le> spec R'"
by (meson dual_order.trans pgm.hom_mono spec_ref_pgm)
lemma test_botI: "S = {} \<Longrightarrow> test S = \<bottom>"
by (clarsimp)
abbreviation "write l v \<equiv> (\<lambda>s. lens.set l s v)"
lemma valid_write_write:
"valid_lens l \<Longrightarrow> write l v o (write l v') = write l v"
apply (clarsimp simp: valid_lens_def)
apply (clarsimp simp: set_set_def)
apply (intro ext; clarsimp)
done
thm maps_to_def
definition "lens_pset l v = Abs_p_set (Pair ({f. (\<exists>v. (\<lambda>s. set l s v) = f)} \<union> {id}) (\<lambda>s. set l s (Some v)))"
declare [[show_types=false]]
lemma set_of_lens_pset: "set_of (lens_pset l v) = {f. (\<exists>v. (\<lambda>s. set l s v) = f)} \<union> {id} "
apply (clarsimp simp: lens_pset_def set_of_def)
apply (subst Abs_p_set_inverse)
apply (clarsimp)
apply (blast)
apply (clarsimp)
done
lemma point_of_lens_pset: "point_of (lens_pset l v) = (\<lambda>s. set l s (Some v)) "
apply (clarsimp simp: lens_pset_def point_of_def)
apply (subst Abs_p_set_inverse)
apply (clarsimp)
apply (blast)
apply (clarsimp)
done
lemmas lens_pset_simps = set_of_lens_pset point_of_lens_pset
lemma maps_to_lens_pset[simp]: "valid_lens l \<Longrightarrow> maps_to l v' (lens_pset l v')"
by (clarsimp simp: maps_to_def lens_pset_simps)
lemma maps_to_lens_pset'[simp]: "maps_to l v s \<Longrightarrow> maps_to l v' (lens_pset l v')"
by (clarsimp simp: maps_to_def lens_pset_simps)
lemma maps_point_simp: "maps_to l v s \<Longrightarrow> point_of s = (\<lambda>s. set l s (Some v))"
by (clarsimp simp: maps_to_def)
lemma write_beacon_sep: " hoare_triple ( lift (maps_to l v \<and>* R)) (write_beacon l v') ( lift (maps_to l v' \<and>* R))"
apply (clarsimp simp: hoare_triple_def run_def write_beacon_def bindCont_def getState_def Sup_le_iff)
apply (intro conjI impI)
apply (clarsimp simp: assert_galois_test)
apply (clarsimp simp: seq_assoc[symmetric] test_seq_test)
apply (clarsimp simp: fail_def)
apply (subgoal_tac "\<tau> (Collect (lift (maps_to l v \<and>* R))) \<sqinter> \<tau> {(a, b)} = \<bottom>"; clarsimp?)
defer
apply (clarsimp)
apply (clarsimp simp: assert_galois_test seq_assoc[symmetric] test_seq_test setState_def pgm_test_pre domain_restrict_twice )
apply (clarsimp simp: restrict_UNIV_times)
apply (rule spec_ref_pgm')
apply (clarsimp)
apply (clarsimp simp: sep_conj_def)
using [[show_types=false]]
apply (clarsimp simp: lift_def)
apply (rule_tac x= "lens_pset l v' + ya" in exI)
apply (intro conjI)
apply (rule_tac x="lens_pset l v'" in exI)
apply (rule_tac x=ya in exI)
apply (intro conjI)(*
apply (clarsimp simp: plus_domain_pair_def sep_disj_domain_pair_def sep_disj_BeaconState_ext_def)
apply (rule_tac x="Pair _ (write l (Some v') o state_of ya)" in exI)
apply (intro conjI)
apply (rule_tac x="Pair {f. (\<exists>v. (\<lambda>s. set l s v) = f)} (\<lambda>s. set l s (Some v'))" in exI)
apply (rule_tac x=ya in exI)
apply (intro conjI)*)
apply (clarsimp simp: disj_cylindric_set_def sep_disj_p_set_def set_of_lens_pset)
apply (intro conjI; clarsimp?)
apply (clarsimp simp: maps_to_def)
apply blast
apply (clarsimp simp: maps_to_def)
apply (clarsimp)
apply blast
find_theorems name:plus name:simps
apply (clarsimp simp: plus_p_simps lens_pset_simps)
apply (clarsimp simp: disj_cylindric_set_def sep_disj_p_set_def)
apply (clarsimp simp: maps_point_simp)
apply (smt (verit) comp_eq_elim maps_to_def point_in_set set_set_def valid_lens_def)
(* apply (frule_tac x="(\<lambda>s. lens.set l s (Some v')) o (\<lambda>s. lens.set l s (Some v))" in bspec)
apply (drule mp)
apply (rule_tac x="(Some v')" in exI)
apply (clarsimp simp: valid_write_write)
apply (clarsimp)
apply (clarsimp simp: comp_assoc)
apply (subst comp_apply[where f="state_of _" and g="write l (Some _)", symmetric])
apply (subst comp_apply[where f="write l (Some _)", symmetric]) back back back
apply (subgoal_tac "(state_of ya \<circ> (\<lambda>s. lens.set l s (Some v'))) = (write l (Some v') o (write l (Some v)) o state_of ya)")
apply (simp only:)
apply (subst comp_apply)+
apply (clarsimp)
apply (clarsimp simp: comp_assoc)
apply (simp add: set_set_def valid_lens_def)
apply (subst valid_write_write, assumption)
apply metis
apply (clarsimp simp: )
*)
apply (subst inf.test_sync_to_inf)
apply (rule test_botI)
apply (clarsimp)
apply (clarsimp simp: lift_def sep_conj_def maps_to_def)
apply (clarsimp simp: plus_p_simps)
by (metis get_set_def option.distinct(1) valid_lens_def)
abbreviation (input) "member S \<equiv> (\<lambda>x. x \<in> S)"
lemma run_read_beacon_split[simp]: "run (bindCont (read_beacon l) c) = ((run (read l)) ; (\<Squnion>x. \<tau> {s. get l s = Some x} ; run (c x)))"
apply (clarsimp simp: run_def bindCont_def read_beacon_def getState_def return_def Nondet_seq_distrib split: if_splits )
apply (rule antisym; (clarsimp simp: Sup_le_iff Nondet_seq_distrib)?)
apply (safe; (clarsimp split: if_splits)?)
apply (rule Sup_upper)
apply (clarsimp simp: image_iff)
apply (rule_tac x=a in exI)
apply (rule_tac x=b in exI)
apply (safe; clarsimp?)
apply (clarsimp simp: fail_def seq_assoc)
apply (clarsimp simp: return_def)
apply (rule Sup_upper2)
apply (clarsimp simp: image_iff)
apply (rule_tac x=a in exI)
apply (rule_tac x=b in exI)
apply (safe; clarsimp?)
apply (rule refl)
apply (clarsimp simp: return_def par.seq_Nondet_distrib)
apply (rule Sup_upper2, clarsimp simp: image_iff)
apply (rule_tac x=y in exI, rule refl)
using seq_mono_left test.hom_mono test_seq_refine apply force
apply (safe)
apply (clarsimp simp: fail_def)
apply (rule Sup_upper2)
apply (clarsimp simp: image_iff)
apply (rule_tac x=a in exI)
apply (rule_tac x=b in exI)
apply (clarsimp, rule refl, clarsimp simp: fail_def seq_assoc)
apply (clarsimp simp: return_def)
apply (clarsimp simp: par.seq_Nondet_distrib Sup_le_iff)
apply (case_tac "y = aa"; clarsimp?)
apply (rule Sup_upper2, clarsimp simp: image_iff)
apply (rule_tac x=a in exI)
apply (rule_tac x=b in exI)
apply (clarsimp simp: return_def)
apply (rule refl)
apply (meson dual_order.refl seq_mono_right test_seq_refine)
apply (subst seq_assoc[symmetric], subst test_seq_test)
apply (clarsimp)
done
lemma run_write_beacon_split[simp]: "run (bindCont (write_beacon l v') c) = ((run (write_beacon l v')) ; run (c ()))"
apply (clarsimp simp: run_def bindCont_def write_beacon_def getState_def)
apply (rule antisym; (clarsimp simp: Sup_le_iff Nondet_seq_distrib)?)
apply (safe)
apply (rule Sup_upper)
apply (clarsimp simp: image_iff)
apply (rule_tac x=a in exI)
apply (rule_tac x=b in exI)
apply (safe; clarsimp simp: fail_def)
apply (simp add: seq_assoc)
apply (rule Sup_upper)
apply (clarsimp simp: image_iff)
apply (rule_tac x=a in exI)
apply (rule_tac x=b in exI)
apply (safe; clarsimp simp: fail_def)
apply (simp add: seq_assoc)
apply (clarsimp simp: setState_def)
apply (rule Sup_upper)
apply (clarsimp simp: image_iff)
apply (rule_tac x=a in exI)
apply (rule_tac x=b in exI)
apply (safe; clarsimp simp: fail_def)
apply (simp add: seq_assoc)
apply (rule Sup_upper)
apply (clarsimp simp: image_iff)
apply (rule_tac x=a in exI)
apply (rule_tac x=b in exI)
apply (safe; clarsimp simp: fail_def)
apply (simp add: seq_assoc)
apply (clarsimp simp: setState_def)
done
lemma hoare_chain': "Q \<subseteq> P' \<Longrightarrow>
(assert P ; spec (UNIV \<times> Q)) ; (assert P' ; spec (UNIV \<times> Q')) \<le> assert P ; spec (UNIV \<times> Q')"
apply (subst assert_restricts_spec) back back
apply (simp only: restrict_UNIV_times)
apply (clarsimp simp: seq_assoc[symmetric])
apply (rule order_trans)
apply (rule hoare_chain)
apply (subst assert_restricts_spec)
apply (rule seq_mono)
apply (clarsimp simp: assert_iso[symmetric])
apply (blast)
apply (rule spec_strengthen)
apply (clarsimp)
done
declare [[show_types=false]]
lemma lift_mono: "lift P s \<Longrightarrow> P \<le> Q \<Longrightarrow> lift Q s"
apply (clarsimp simp: lift_def)
by blast
lemma write_beacon_wp[wp]: "hoare_triple (lift P) (c ()) Q \<Longrightarrow> hoare_triple (lift (maps_to l v \<and>* (maps_to l v' \<longrightarrow>* P))) (do {x <- write_beacon l v' ; c x}) ( Q)"
apply (clarsimp simp: hoare_triple_def)
apply (rule order_trans)
apply (rule seq_mono)
apply (rule write_beacon_sep[simplified hoare_triple_def, where R="(maps_to l v' \<longrightarrow>* P)"])
apply (assumption)
apply (clarsimp simp: )
apply (rule hoare_chain', clarsimp)
apply (erule lift_mono, clarsimp)
apply (sep_mp)
apply (sep_solve)
done
lemma read_sep: " hoare_triple ( lift (maps_to l v \<and>* R)) (read l) ( lift (maps_to l v \<and>* R))"
apply (clarsimp simp: hoare_triple_def run_def read_beacon_def bindCont_def getState_def Sup_le_iff, safe)
apply (clarsimp simp: fail_def assert_galois_test)
defer
apply (clarsimp simp: return_def)
apply (metis assert_galois_test nil_ref_test restrict_range_UNIV seq_mono
seq_mono_left seq_nil_left spec_test_restricts spec_univ term_nil test_seq_commute)
apply (subgoal_tac "\<tau> (Collect (lift (maps_to l v \<and>* R))) ; \<tau> {(a, b)} \<le> \<bottom>")
apply (metis bot.extremum inf.absorb_iff2 inf_bot_left seq_assoc seq_magic_left)
apply (subst test_seq_test)
apply (subgoal_tac "(Collect (lift (maps_to l v \<and>* R)) \<inter> {(a, b)}) = {}"; clarsimp)
apply (clarsimp simp: sep_conj_def lift_def maps_to_def)
apply (clarsimp simp: plus_p_simps)
by (metis get_set_def option.distinct(1) valid_lens_def)
lemma times_restrict_range[simp]: "(UNIV \<times> P) \<triangleright> Q = (UNIV \<times> (P \<inter> Q))"
by (safe; (clarsimp simp: restrict_range_def)?)
lemma maps_to_get_wf:"lift (maps_to l v \<and>* R) (a, b) \<Longrightarrow> get l (a, b) = (Some v)"
apply (clarsimp simp: sep_conj_def maps_to_def)
sorry
lemma read_beacon_wp[wp]: "(\<And>a. hoare_triple (lift (P a)) (c a) (Q )) \<Longrightarrow> hoare_triple ( lift (maps_to l v \<and>* (maps_to l v \<longrightarrow>* (P v )))) (do {v <- read_beacon l ; c v}) (Q )"
apply (clarsimp simp: hoare_triple_def bindCont_def run_def read_beacon_def getState_def )
apply (clarsimp simp: Sup_le_iff)
apply (safe)
apply (clarsimp simp: fail_def assert_galois_test)
defer
apply (clarsimp simp: fail_def assert_galois_test return_def)
apply (case_tac "y = v"; clarsimp?)
apply (subst seq_assoc[symmetric])
apply (subst test_seq_test)
apply (rule order_trans, rule seq_mono_left)
apply (rule test.hom_mono[where p="Collect (lift (P v))"])
apply (clarsimp)
apply (erule lift_mono, clarsimp)
apply (sep_solve)
apply (blast)
apply (subst seq_assoc[symmetric])
apply (subst test_seq_test)
apply (rule order_trans, rule seq_mono_left)
apply (rule test.hom_mono[where p="{}"])
apply (clarsimp)
defer
apply (clarsimp)
apply (subst seq_assoc[symmetric])
apply (subst test_seq_test)
apply (rule order_trans, rule seq_mono_left)
apply (rule test.hom_mono[where p="{}"])
apply (clarsimp)
defer
apply (clarsimp)
apply (drule maps_to_get_wf, clarsimp)
apply (drule maps_to_get_wf, clarsimp)
done
definition "swap l l' \<equiv> do {x <- read_beacon l;
y <- read l';
_ <- write_beacon l' x;
write_beacon l y}"
definition "add_fields l l' \<equiv> do {x <- read_beacon l;
y <- read_beacon l';
return (x + y)}"
definition "set_max a b c \<equiv> do { x <- read_beacon a;
y <- read_beacon b;
(if (x \<le> y) then write_beacon c y else write_beacon c x)}"
lemma return_wp: "hoare_triple P (return c) P"
apply (clarsimp simp: hoare_triple_def)
apply (clarsimp simp: run_def return_def)
by (metis assert_galois_test restrict_range_UNIV seq_mono_left seq_nil_left seq_nil_right spec_test_restricts spec_univ term_nil)
lemma swap_sep: "hoare_triple (lift (maps_to l v \<and>* maps_to l' v' \<and>* R)) (swap l l') ( lift (maps_to l v' \<and>* maps_to l' v \<and>* R) )"
apply (clarsimp simp: swap_def)
apply (rule hoare_weaken_pre)
apply (rule read_beacon_wp)
thm read_beacon_wp
thm wp
apply (rule read_beacon_wp[where v="v'"])
apply (rule write_beacon_wp)
apply (rule wp )+
apply (rule write_beacon_wp[where c=return, simplified bindCont_return, OF return_wp])
apply (clarsimp)
apply (erule lift_mono, clarsimp)
apply (sep_solve)
done
lemma swap_wp: "hoare_triple ( lift P) (c ()) Q \<Longrightarrow> hoare_triple (lift (maps_to l v \<and>* maps_to l' v' \<and>* (maps_to l v' \<and>* maps_to l' v \<longrightarrow>* P))) (do {x <- swap l l'; c x}) (Q)"
apply (clarsimp simp: swap_def)
apply (rule hoare_anti_mono)
apply (clarsimp simp: bindCont_assoc[symmetric])
apply (rule wp )+
apply (assumption)
apply (clarsimp)
apply (erule lift_mono, clarsimp)
apply (sep_cancel)+
apply (sep_solve)
apply (clarsimp)
done
lemma return_triple: "hoare_triple P (bindCont C return) Q \<Longrightarrow> hoare_triple P C Q "
apply (clarsimp simp: bindCont_return)
done
method wp = ((simp only: bindCont_assoc[symmetric] bindCont_return')?,
(rule wp return_wp wp[THEN return_triple]) | assumption )+
lemma add_fields_wp: "(\<And>a. hoare_triple (lift (P a)) (c a) (Q)) \<Longrightarrow>
hoare_triple (lift (maps_to l v \<and>* maps_to l' v' \<and>* (maps_to l v \<and>* maps_to l' v' \<longrightarrow>* P (v + v'))))
(do {x <- add_fields l l'; c x}) (Q )"
apply (clarsimp simp: add_fields_def)
apply (rule hoare_weaken_pre)
apply (wp)
apply (clarsimp)
apply (erule lift_mono, clarsimp)
by ( sep_cancel+, sep_solve)
thm swap_wp[where c=return, simplified bindCont_return]
thm add_fields_wp[where c=return, simplified bindCont_return]
find_theorems "if _ then _ else _" bindCont
lemma if_wp[wp]:
"(B \<Longrightarrow> hoare_triple ( S) ( bindCont P c) R) \<Longrightarrow> (\<not>B \<Longrightarrow> hoare_triple ( S') (bindCont Q c) R) \<Longrightarrow>
hoare_triple ( (if B then S else S')) (do {x <- (if B then P else Q); c x}) R"
apply (clarsimp split: if_splits)
done
lemma inf_spec: " \<Inter> (Set.range P) \<le> P (a, b)"
apply (clarsimp)
done
lemma getState_wp[wp]: "(\<And>a. hoare_triple (P a) (c a) Q) \<Longrightarrow>
hoare_triple (\<lambda>x. P x x) (bindCont getState c) Q"
apply (clarsimp simp: getState_def hoare_triple_def bindCont_def run_def Sup_le_iff assert_galois_test test_restricts_Nondet)
apply (atomize)
apply (erule_tac x=a in allE)
apply (erule_tac x=b in allE)
apply (erule order_trans[rotated])
using seq_mono_left test.hom_mono by force
lemma run_setState_distrib: "run (bindCont (setState s) c) = run (setState s); run (c ())"
by (clarsimp simp: run_def bindCont_def setState_def)
lemma run_setState_le: "run (setState s) \<le> assert UNIV ; spec (UNIV \<times> {s})"
apply (clarsimp simp: setState_def run_def)
by (simp add: assert_top spec_ref_pgm)
lemma setState_wp[wp]: " hoare_triple (P) (c ()) Q \<Longrightarrow>
hoare_triple (\<lambda>_. P s) (bindCont (setState s) c) Q"
apply (clarsimp simp: hoare_triple_def Sup_le_iff run_setState_distrib)
apply (safe)
apply (rule order_trans)
apply (rule seq_mono)