Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Rules for Lib #704

Merged
merged 21 commits into from
Jan 15, 2024
Merged

Rules for Lib #704

merged 21 commits into from
Jan 15, 2024

Conversation

michaelmcinerney
Copy link
Contributor

No description provided.

@michaelmcinerney michaelmcinerney self-assigned this Jan 10, 2024
@michaelmcinerney
Copy link
Contributor Author

The errors should hopefully be fixed now: they all seemed to be caused by the reordering of the assumptions in no_fail_bind. The changes are all in the last commit, which I will squash into the appropriate commit, once approved

lsf37
lsf37 approved these changes Jan 12, 2024
View reviewed changes
Copy link
Member

@lsf37 lsf37 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good from my side!

lib/Corres_UL.thy Show resolved Hide resolved
lib/Corres_UL.thy Show resolved Hide resolved
lib/ExtraCorres.thy Outdated Show resolved Hide resolved
lib/ExtraCorres.thy Outdated Show resolved Hide resolved
@michaelmcinerney
lib+refine: strengthen corres_assert_assume_l and move to Lib
e4ec9f3 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add corres_if_strong
ca3624e 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
corlewis
corlewis reviewed Jan 15, 2024
View reviewed changes
lib/ExtraCorres.thy Outdated
done


\<comment> \<open>Some @{term corres_underlying }rules for @{term whileLoop}\<close>
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very minor

Suggested change
\<comment> \<open>Some @{term corres_underlying }rules for @{term whileLoop}\<close>
\<comment> \<open>Some @{term corres_underlying} rules for @{term whileLoop}\<close>

@michaelmcinerney
lib: add some rules involving ex_abs_underlying, including corres_fro…
45ece43 
…m_valid

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: strengthen no_ofail_gets_the
48f8ea7 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add monadic_rewrite_guard_arg_cong
d13c538 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: generalise monadic_rewrite_is_valid
0078984 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add monadic_rewrite_corres_r_generic_ex_abs
25968fd 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add ifM_to_top_of_bind
962d097 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add ifM_corres' and orM_corres'
f2b047f 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: reorder assumptions of no_fail_bind
4edbe22 
In order to aid wp-style reasoning

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: modify no_ofail_obind and no_ofail_pre_imp
04e7eea 
In order to aid wp-style reasoning

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add ovalid_post_taut
943ab13 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add no_ofail_if
82abdf8 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add defn of list_insert_before, and some lemmas
c486058 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add Heap_List.thy, for reasoning about linked lists on heaps
fd6656c 
From the rt branch

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: heap_ls lemmas relating an update to the list to an update to th…
0f5987a 
…e heap

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add heap_path_sym_heap_non_nil_lookup_prev
b2962e9 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add fun_upd_swap
d04daa5 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: several miscellaneous lemmas for heap_ls
d588c6c 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: add "no loops" lemmas for heap_ls
1991f59 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney
lib: some sym_heap lemmas regarding heap updates
58d5752 
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
@michaelmcinerney michaelmcinerney merged commit afcbba9 into master Jan 15, 2024
13 of 14 checks passed
@michaelmcinerney michaelmcinerney deleted the michaelm-rules_for_Lib branch January 15, 2024 07:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lsf37 lsf37 lsf37 approved these changes

@corlewis corlewis corlewis left review comments

@Xaphiosis Xaphiosis Awaiting requested review from Xaphiosis

Assignees

@michaelmcinerney michaelmcinerney

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@michaelmcinerney @lsf37 @corlewis