I am trying to prove the following lemma to aid in a later theorem:
lemma char_of_symmetric: "((of_char (char_of n))::nat) = n" (is "?P n") proof (induction n) case 0 show ?case by auto next fix n assume "?P n" thus "?P (Suc n)" by simp qed
char_of come from the
After this, the proof state has 1 subgoal remaining:
1. n mod 256 = n ⟹ Suc n mod 256 = Suc n
I believe this
mod 256 is coming from the fact that the Isabelle
string implementation implements UTF-8, which sets this limit on character code digits (I'm not a UTF-8 expert, but this seems plausible).
In my case, I am serializing single digits, so I know that
n here will always be
< 10. Where can I put this assumption to hopefully get this proof goal to be discharged?
I have tried
fix n assume "n < 10 /\ (?P n)", and I've tried
assume "n < 10" at the beginning of the proof, before all case analyses. I am always met with a syntax error, or the errors: "Illegal application of proof command in "state" mode."
Any tips here?
I made some progress by re-reading the "Structured Lemma Statements" section of Concrete Semantics:
lemma char_of_symmetric: assumes single_digit: "(n::nat) < 10" shows "((of_char (char_of n))::nat) = n" (is "?P n") proof (induction n) case 0 show ?case by auto next fix n assume "(?P n)" with single_digit show "?P (Suc n)" by simp qed
I think adding the assumption
single_digit at the top level makes sense, though it doesn't seem to actually apply the assumption unless I use
with single_digit_show (which is slightly surprising). Even still, I'm left with this final proof goal:
1. n < 10 ⟹ n mod 256 = n ⟹ Suc n mod 256 = Suc n
This looks to me like a true statement -
n mod 256 = n if
n < 10. I even proved that in a separate lemma to double check, though it required some casting which might be the source of the issue:
lemma "(n::nat) < 10 ⟹ n mod 256 = n" by auto (* This is correctly proven *)
So, I'm not sure how to discharge this final goal.
you are missing an
using assms before the
proof (induction n)
Assuming the constants
char_of come from
HOL.String, a relevant lemma can be found through
find_theorems of_char char_of:
String.unique_euclidean_semiring_with_bit_shifts_class.of_char_of: of_char (char_of ?a) = ?a mod 256
In particular, this lemma has been declared as a simplification rule, so that we don't need to invoke it explicitly. Your intended lemma should be provable without induction:
lemma assumes "n<256" shows "((of_char (char_of n))::nat) = n" using assms by auto
using assms worked - here is the final proof:
lemma char_of_symmetric: fixes n :: nat assumes "n < 10" shows "of_char (char_of n) = n" using assms proof (induction n) case 0 show ?case by auto next case (Suc n) then show ?case by auto qed
I also didn't know about
find_theorems, so that is very helpful. I just wanted to carry the proof out myself for learning purposes, but obviously I want to use existing theorems as much as possible.
Alex Weisberger has marked this topic as resolved.
Last updated: Dec 07 2023 at 20:16 UTC