mapM_x_commute requires "distinct" even if the operations in the mapM
don't require any guards. Add a separate version without distinct when
guard is \top.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Document/test surprising interactions of hide_const, locales and
requalify for the purposes of temporarily making arch-specific constants
visible in theory scope.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Previous attempts to update the code to allow ctrl+clicking on names
resulted in markup overlap errors for arch_requalify commands.
This was due to a misconception that YXML strings already containing
correct position information (e.g. obtained via Parse.const) would
be used directly by Proof_context.read_const/read_type_name. This is not
the case. Instead, position information is adjusted for the content
length, and since we add a prefix for L4V_ARCH, we got annotation that
did not match the document text.
After hours of digging to uncover the above issue, we get this:
* the "check_parsed_nm" in gen_requalify was not an extra check, but a
hook to do document annotation; updated comments
* use Proof_Context.check_const/check_type_name with user-supplied name
and parsed position of Parse.name, and manually report resulting markup
(do not use previously resolved name as it could point to a hidden
const/type)
* since the above works for arch_requalify_const, the normal
requalify_const becomes a simpler instance of it
* the whole Parse.const/Parse.typ was a red herring and ultimately did
not add anything to the code except for read_const/read_type_name
interaction; removed
The resulting code is simpler; large cautionary comments remain for
future generations.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This uses a complex workaround to unify the parse location of the
original name encoded in YXML with the name the user is actually aiming
for. While intuitively one could think to use the position of the name we
parsed, there appears to be no way to pass that location to
read_const/read_type_name, as those expect to be fed the result of
Parse.const and Parse.typ respectively.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
* add warnings when exporting a name that already exists in theory
context, suppressable by `(aliasing)` option
* add `arch` variants of requalify commands that implicitly add the
value of L4V_ARCH before whatever you give them, with optional
suffixes for abstract (A) and Haskell (H) spec global naming.
* write hopefully-understandable documentation with commented examples
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This was required after a recent update to the schematics of
corres_symb_exec_r_conj_ex_abs
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This adds ostate_assert and ohaskell_state_assert, which are
versions of state_assert/stateAssert for the reader monad.
Also adds several rules for basic reasoning about these
functions.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This helps to reduce dependence between the schematics used in
the assumptions, and allows for easier wp reasoning.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
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 <corey.lewis@proofcraft.systems>
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 <corey.lewis@proofcraft.systems>
This has been performed by the following commands:
perl -0777 -pi -e "s/^crunch(\s*\(in\s*\w*\))?\s*([(]\w*[)])\s*([\w'\"-]*)\s*(\[[\w,\s\!]*\])?\s*:(\s*)([\w'\".-]+)((?:\s*,\s*[\w'\".-]+)*)(?\!\h*[\w'\",.])/crunches\1\5\6\7\n for \2 \3\4/gm" **/*.thy
perl -0777 -pi -e "s/^crunch(\s*\(in\s*\w*\))?(\s*[(]\w*[)])?\s*([\w'\"-]*)\s*(\[[\w,\s\!]*\])?\s*:(\s*)([\w'\".-]+)((?:\s*,\s*[\w'\".-]+)*)\s*([^\n]*)/crunches\1\5\6\7\n for\2 \3\4: \8/gm" **/*.thy
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
The old Global_Theory.add_defs command lost some options and no longer
processes attributes. This commit reflects these changes up into the
"defs" command:
- remove "overloading" and "unchecked" options
- remove attribute spec -- use pure binding for thm name
- only one equation per "defs" command
- remove deprecation warning, because we are using this command
intentionally
- document these changes in the header
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- Exn.interruptible_capture has been renamed to Exn.result.
- simproc setup has changed slightly
- can no longer catch all exceptions
- Term_Subst renames
- Global_Theory.add_defs was downgraded to Global_Theory.add_def
Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This involved the following sed commands, with care taken to avoid
unnecessary rewrites in lib/Monads and lib/StateMonad.thy
sed -i 's/hoare_post_taut/hoare_TrueI/g' **/*.thy
sed -i 's/hoare_TrueI\s*\[where P=\\<top>\]/wp_post_taut/g'
proof/**/*.thy
sed -i 's/hoare_post_imp_R/hoare_strengthen_postE_R/g' **/*.thy
sed -i 's/hoare_seq_ext\b/bind_wp/g' **/*.thy
sed -i 's/bind_wp\s*\[rotated\]/bind_wp_fwd/g' **/*.thy
sed -i 's/hoare_vcg_precond_imp/hoare_weaken_pre/g' **/*.thy
sed -i 's/hoare_vcg_seqE/bindE_wp/g' **/*.thy
sed -i 's/bindE_wp\s*\[rotated\]/bindE_wp_fwd/g' **/*.thy
sed -i 's/validE_weaken/hoare_chainE/g' **/*.thy
sed -i 's/validE_weaken/hoare_chainE/g' **/*.ML
sed -i 's/seqE/bindE_wp_fwd/g' **/*.thy
sed -i 's/bindE_wp_fwd\s*\[rotated\]/bindE_wp/g' **/*.thy
sed -i 's/hoare_True_E_R/hoareE_R_TrueI/g' **/*.thy
sed -i -e 's/hoareE_R_TrueI\[where
P="\\<top>"\]/wp_post_tautE_R/g' **/*.thy
sed -i "s/hoare_post_impErr'/hoare_strengthen_postE/g" **/*.thy
sed -i 's/hoare_post_impErr/hoare_strengthen_postE/g' **/*.thy
sed -i 's/hoare_vcg_all_lift_R/hoare_vcg_all_liftE_R/g' **/*.thy
sed -i 's/hoare_seq_ext_skip/bind_wp_fwd_skip/g' **/*.thy
sed -i 's/True_E_E/wp_post_tautE_E/g' **/*.thy
sed -i 's/\bseq_ext/bind_wp_fwd/g' proof/**/*.thy
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This improves the structure and naming consistency of the various monad
rule sets, for both the nondet and trace monads.
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
DupSkip used to be a proof caching option since replaced by "defer
proofs". It is no longer available in our Isabelle branch. Remove last
mentions and related files.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
We want them as wp rules instead of wp_split rules so that they are used
with the correct priority and in combination with wp_comb rules when
necessary. This also adds new validE_R and validE_E variants, along with
rules for when bind appears inside a validE term.
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
This tries to remove ambiguity around the order in which `wp`, `wp_comb`
and `wp_split` rules are applied.
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Produce a _def theorem for the value type that provides direct symbolic
access to the right-hand side of the value_type definition. This avoids
having to unfold those terms in subsequent proofs.
The numeric value as as term is still available as <type-name>_val.
This restricts value_type to nat/int inputs, i.e. word is no longer
accepted on the rhs (so far unused). A manual cast to nat on the rhs
will still work.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
reindent corres_cross_add_guard and friend squash
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Gerwin Klein