More monad improvements #765
Merged
Commits on Jul 9, 2024
-
lib/monads: more improvements to monads consistency
This makes the lemma names in the monad rule sets even more consistent, and changes the variables used in the lemmas to avoid R and G being used in pre or post-conditions. These variable names are instead reserved for the rely and guarantee conditions in the trace monads RG rule set. Signed-off-by: Corey Lewis <[email protected]>
-
lib+proof+sys-init: update for more changed monad lemmas
The following commands are updates for changed lemma names: sed -i 's/hoare_valid_validE/valid_validE/g' **/*.thy sed -i 's/hoare_vcg_E_conj/hoare_vcg_conj_liftE_E/g' **/*.thy sed -i "s/hoare_vcg_conj_liftE_R/hoare_vcg_conj_liftE_R'/g" **/*.thy sed -i 's/hoare_vcg_R_conj/hoare_vcg_conj_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_E_elim/hoare_vcg_conj_elimE/g' **/*.thy sed -i 's/hoare_vcg_const_imp_lift_R/hoare_vcg_const_imp_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_const_Ball_lift_R/hoare_vcg_const_Ball_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_conj_lift_R/hoare_vcg_conj_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_const_imp_lift_E/hoare_vcg_const_imp_liftE_E/g' **/*.thy sed -i 's/hoare_weak_lift_imp_R/hoare_weak_lift_impE_R/g' **/*.thy sed -i 's/hoare_post_imp_dc2_actual/hoare_post_impE_R_dc_actual/g' **/*.thy sed -i 's/hoare_post_imp_dc2E_actual/hoare_post_impE_E_dc_actual/g' **/*.thy sed -i 's/hoare_post_imp_dc2E/hoare_post_impE_E_dc/g' **/*.thy perl -0777 -pi -e 's/hoare_pre\(1\)/hoare_weaken_pre/g' **/*.thy perl -0777 -pi -e 's/hoare_drop_imps\(2\)/hoare_drop_impE_R/g' **/*.thy sed -i 's/hoare_vcg_imp_lift_R/hoare_vcg_imp_liftE_R/g' **/*.thy The following commmands update changed variable names: perl -0777 -pi -e "s/hoare_post_imp\h*(\s*)\[(\s*)where\h*Q\h*=\h*/hoare_post_imp\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_post_imp/rule_tac Q'=\"\1\"\2in hoare_post_imp/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_strengthen_post/rule_tac Q'=\"\1\"\2in hoare_strengthen_post/g" **/*.thy perl -0777 -pi -e "s/hoare_strengthen_post\h*(\s*)\[(\s*)where\h*Q\h*=\h*/hoare_strengthen_post\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_strengthen_post\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_strengthen_post\1\[\2where Q=/g" **/*.thy perl -0777 -pi -e "s/hoare_drop_impE_R\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_drop_impE_R\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_drop_imp\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_drop_imp\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_drop_imps\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_drop_imps\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*G\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_grab_asm/rule_tac P'=\"\1\"\2in hoare_grab_asm/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*R\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_vcg_if_split/rule_tac P''=\"\1\"\2in hoare_vcg_if_split/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*R\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_post_add/rule_tac Q'=\"\1\"\2in hoare_post_add/g" **/*.thy perl -0777 -pi -e "s/hoare_strengthen_postE\h*(\s*)\[where\h*E\h*=\h*/hoare_strengthen_postE\1\[\2where E'=/g" **/*.thy perl -0777 -pi -e "s/hoare_disjI2\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_disjI2\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_weaken_pre/rule_tac P'=\"\1\"\2in hoare_weaken_pre/g" **/*.thy perl -0777 -pi -e "s/hoare_weaken_pre\h*(\s*)\[(\s*)where\h*Q\h*=\h*/hoare_weaken_pre\1\[\2where P'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_pre_imp/rule_tac P'=\"\1\"\2in hoare_pre_imp/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)and(\s*)E\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_strengthen_postE/rule_tac Q'=\"\1\"\2and\3E'=\"\4\"\5in hoare_strengthen_postE/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*E\h*=\h*\"([^\"]+)\"(\s*)and(\s*)Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_strengthen_postE/rule_tac E'=\"\1\"\2and\3Q'=\"\4\"\5in hoare_strengthen_postE/g" **/*.thy perl -0777 -pi -e "s/hoare_vcg_conj_liftE_R\h*(\s*)\[(\s*)where\h*S\h*=\h*/hoare_vcg_conj_liftE_R\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_post_add\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_post_add\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)for(.*)(\s*)in\h*hoare_strengthen_post/rule_tac Q'=\"\1\"\2for\3\4in hoare_strengthen_post/g" **/*.thy perl -0777 -pi -e "s/unless_wp\h*(\s*)\[(\s*)where\h*Q\h*=\h*/unless_wp\1\[\2where P'=/g" **/*.thy perl -0777 -pi -e "s/hoare_chain\h*(\s*)\[(\s*)where\h*P\h*=\h*/hoare_chain\1\[\2where P'=/g" **/*.thy Signed-off-by: Corey Lewis <[email protected]>
-
lib+proof+sys-init: more updates for monad changes
This fixes the proofs not handled by the automated changes in the previous commits. Signed-off-by: Corey Lewis <[email protected]>
-
lib/monads: remove FIXMEs and hoare_gets
These FIXMEs were recently added and apart from removing hoare_gets I no longer think that they are worth doing, as the lemmas they refer to are used in more proofs than I first thought. Signed-off-by: Corey Lewis <[email protected]>
-
proof: update for removed hoare_gets
Signed-off-by: Corey Lewis <[email protected]>
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.