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