Qiyuan Xu (Nov 26 2021 at 02:11): Qiyuan Xu (Nov 26 2021 at 02:11):In src/Pure/asssumption.ML, the ML type Assumption.export is defined as bool -> cterm list -> (thm -> thm) * (term -> term). The documentation implementation describes that type as however bool -> cterm list -> thm -> thm (page 121 for version Isabelle2021), which loses the explanation about the second argument, the export map of type term -> term. I guess it is used for exporting some term shape, but what term it is, the term of proposition of the theorem or the term variables (fixed variables)? However, both the standard exports, the assume_export and presume_export set that term export as just fn x => x, seeming that the term export just useless, which makes me confused more. While that term export, I found, does be used somewhere in the Isabelle system, can I naively set it also as fn x => x?
Qiyuan Xu (Nov 26 2021 at 02:18):When I set that as the naive fn x => x, everything works well, but it may just seem to work well...
Mathias Fleury (Nov 26 2021 at 06:43):I have only used Assumption.import and co (the difference is that they work on a proper proof context), but my guess is that this comes from variables you declare locally (the one that become ?x in the goal) that can conflict with global constants.
Manuel Eberl (Nov 26 2021 at 09:29):It's a good idea to ask such questions on the mailing list, since the best person to answer them is probably Makarius, and he boycotts Zulip.
Qiyuan Xu (Nov 26 2021 at 14:17):Mathias Fleury said:
I have only used Assumption.import and co (the difference is that they work on a proper proof context), but my guess is that this comes from variables you declare locally (the one that become
?xin the goal) that can conflict with global constants.
sorry, do you mean the import function in Assumption structure? I don't find that function in file src/Pure/assumption.ML
Mathias Fleury (Nov 26 2021 at 14:18):Sorry I meant Assumption.add_assumes
Last updated: Dec 21 2024 at 16:20 UTC