Re: [isabelle] "code_pred" introduces axioms?



Hi Andreas,

Thank you for the (as usual) very thorough explanation.

> The introduction rules for barP are recursive and go through the higher-order predicate IdP (just like the definition of bar higher-order-recurses throuch Id). If one wants to do this definitionally (e.g., with the inductive package), then one also has to prove the monotonicity rule for IdP. I am not sure whether one should spent that much effort, as [inductify] itself is very flaky anyway.

I believe Lars Hupel is trying to attack similar problems, also in the context of the code generator.

> With respect to the names of the axioms, I don't care what they are called. I have never wanted to use them, because they are really internal constructions of the code generator. Only the generated .equation theorem is of interest. But if you want to implement stable names, how about <predicate name>.intros?

I did something a bit simpler -- ".intros" doesn't quite work with "Specification.axiom", which does one axiom at a time. It's not that I care so much about the names, but for a tool like MaSh it's a bit worrying when the fact names change each time you reload the theory.

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.