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