Hi Gerwin, > Thanks for that pointer. FOL-Fitting looks reasonably well behaved with its > 2-way nesting. This file has 4-way nesting and something seems to have > changed in the order of the subgoals that the induction leaves, which makes > the unstructured apply scripts a pain to update. > > Is the goal order sensitive to the order I give the induct rules in, the > induction statement, or the primrec equations, or all of these?
I don’t entirely understand what some of the suggested “dependencies” are, but if you are using the induction schemes generated by “primrec” I can’t guarantee that the order will be the same as it used to be. It might be that the order of the primrec equations have an impact. But: > Maybe datatype_compat is the one I should go with for now. Need to check if > that has an influence on the induction order. “datatype_compat” should give exactly the same induction principle as before, modulo naming of its schematic variables, even in the presence of 4-way nesting. >> As for “size”, I’d be curious to know what the exact issue is. It did >> change, and there are some incompatibilities (typically off-by-ones), but if >> you can tell me a bit more what you’re doing, I might be able to help here. >> In the worst case, it’s always possible (and not very difficult) to define >> “size” manually, if you need a specific semantics. > > I don’t think I really need the specific semantics, but I’m having a hard > time understanding what the actual problem is. In particular, it is this > lemma td_set_size_lte’ and the few corollaries following it > > https://github.com/seL4/l4v/blob/2015/tools/c-parser/umm_heap/CTypes.thy#L578 > > lemma td_set_size_lte’ doesn’t seem to be provable any more if you dig into > it a bit and the corollaries don’t seem to follow any more either. > Replicating the old size definition would probably do it, but it would be > nice not to have to. > > (You should be able to just clone the 2015 branch of this repo and load up > the file in JEdit with base logic HOL if you want to see what’s going on). > > I have the feeling that a real overhaul of this file should use mapping > functions to reduce the nesting, but that’s more than I have time for at the > moment. OK, I’m also a bit time-limited at the moment but will look into this once I get a chance. Let me know if you discover anything important until then. I suspect the above issue is just an instance of the “off-by-one” issue I mentioned. With the old package, the “size” overloaded instance did not always coincide with the more general “size_t” function, which I found unsatisfactory both on aesthetic grounds and to avoid duplicating proofs. A simple example is thm option.size which used to be size_sum ?fa ?fb (Inl ?a) = ?fa ?a + Suc 0 size (Inl ?a) = 0 whereas now “size (Inl _) = Suc 0” for consistency with “size_sum” (by taking ?fa = ?fb = %_. 0). Sorry about the trouble. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
