Email Gateway (Aug 18 2022 at 10:06): Email Gateway (Aug 18 2022 at 10:06):From: SrinivasaRao Subramanya <SrinivasaRao.Subramanya@rsise.anu.edu.au>
Hello
Just wondering if there is a problem with the lemma "mod_add1_eq"(see
below) in the theory Divides.
(* Snippet from the divides theory which I am not able to verify*)
lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
apply (case_tac "c = 0", simp)
apply (blast intro: quorem_div_mod quorem_div_mod
quorem_add1_eq [THEN quorem_mod])
done
(* end of snippet *)
Iam finding it a bit difficult to get this verified. Iam a new-comer
both to Isabelle and to theorem verification, so if I have missed out on
something really primitive, apologies for taking your time.
Is there an easier way to verify "(a+b) mod (c::nat) = (a mod c + b mod
c) mod c", though?
Regards
Srinivas
Email Gateway (Aug 18 2022 at 10:06):From: Lawrence Paulson <lp15@cam.ac.uk>
I assume that by "verify" you mean you are trying to replay the proof
script. In fact this script does not replay in a normal Isabelle
session. Some of the theorem names used in this proof are re-used by
theory IntDiv. You can disambiguate using name spaces like this:
lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
apply (case_tac "c = 0", simp)
apply (blast intro: quorem_div_mod Divides.quorem_div_mod
quorem_add1_eq [THEN Divides.quorem_mod])
done
The proof scripts used in the main Isabelle/HOL theory are
progressively building up the verification environment, so it's quite
normal for them to behave differently in the full Isabelle/HOL.
Larry Paulson
Last updated: May 03 2024 at 08:18 UTC