Когда я импортирую файлы теории, которые имеют определенные константы (для рекурсивных функций или определений), например f, как я могу скрыть такую константу в текущем файле теории? Другими словами, я хочу убедиться, что f является свободной переменной. Я не хочу менять импортированные файлы.Как скрыть определенные константы
Это точно цель команды hide_const. НАПРИМЕР,
hide_const f
будет полностью удалить определенную константу f из текущего контекста (и, таким образом, сделать его недоступным). Если вы используете
hide_const (open) f
вместо этого, только базовое имя скрыто (т.е. f), но квалифицированное имя (например, A.f если f была определена в теории A) до сих пор работает.
Существуют аналогичные команды для классов, типов и фактов: hide_class, hide_type и hide_fact. См. Также the Isabelle/Isar Reference Manual, стр. 105.