Hi again,

I've been getting great help here, so here's another problem I've ran into.

I have been working towards proving a behavior that executes an HTTP request, so proving the serialization and deserialization of the data has been a main component of that. What I'm running into now is that a theorem that I've proven for `nat`

is not being used to simplify a record that contains a `nat`

value. Here's what I mean:

```
type_synonym http_data = string
record order =
amount :: nat
fun deserialize :: "http_data ⇒ order" where
"deserialize d = ⦇ amount = (nat_of_string d) ⦈"
fun serialize :: "order ⇒ http_data" where
"serialize ord = string_of_nat (amount ord)"
(* This theorem has been successfully proven *)
theorem ser_deser: "nat_of_string (string_of_nat n) = n"
```

I would then expect to be able to prove this as follows:

```
lemma "deserialize (serialize order) = order"
apply(cases order)
apply(simp add: ser_deser)
```

This leaves me with the following goal:

```
1. ⋀amount.
order = ⦇amount = amount⦈ ⟹
nat_of_string (map char_of (digit_list amount)) = amount
```

The `map char_of ...`

is part of the definition of `string_of_nat`

, but I was hoping that the simplifier would see `nat_of_string (string_of_nat amount)`

and simplify that to `amount`

, especially since I specified `ser_deser`

as a simplification rule.

Is there something obvious to do here to discharge the goal, or are there some gotchas with using records?

Last updated: Jul 15 2022 at 23:21 UTC