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

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

Alex Weisberger has marked this topic as resolved.

Last updated: Sep 11 2024 at 16:22 UTC