Wolfgang Jeltsch (Mar 02 2023 at 13:52): Wolfgang Jeltsch (Mar 02 2023 at 13:52):This question should be asked under Beginner Questions or perhaps General. This place here is for discussions about extending Isabelle using meta-programming in ML.
Notification Bot (Mar 02 2023 at 14:32):This topic was moved here from #Isabelle/ML > isabelle by Kevin Kappelmann.
Notification Bot (Mar 02 2023 at 14:36):This topic was moved here from #Beginner Questions > a lemma prove by Kevin Kappelmann.
Kevin Kappelmann (Mar 02 2023 at 14:39):I think you need to cut down your question, give more context, and be more precise to receive helpful answers. I reckon most people are not willing to dive into random proof requests.
Mathias Fleury (Mar 02 2023 at 16:07):I managed to prove concat_lemma. But: it is exactly how you would do on paper and I don't do homeworks
Hongjian Jiang (Mar 03 2023 at 04:31):I succeed to prove by induction on x and arbitrary on y, that works.
Last updated: Dec 21 2024 at 16:20 UTC