## Stream: Beginner Questions

### Topic: Where to put assumptions in Isar proof

#### Alex Weisberger (Nov 21 2021 at 00:46):

Hello,

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
``````

(`of_char` and `char_of` come from the `Show.Show_Instances` theory)

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 `char` and `string` implementation implement 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?

#### Alex Weisberger (Nov 21 2021 at 04:34):

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.

#### Mathias Fleury (Nov 21 2021 at 06:58):

you are missing an `using assms` before the `proof (induction n)`

#### Wenda Li (Nov 21 2021 at 11:19):

Assuming the constants`of_char` and `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
``````

#### Alex Weisberger (Nov 21 2021 at 13:09):

`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.

Thanks everyone!

Last updated: Jul 15 2022 at 23:21 UTC