Как включить «Трассировка» в Isabelle/jEdit

Question

Я ВИМ вентилятор, но только Emacs имеет эту среду Isabelle/HOL. jEdit велик, но я не могу использовать

using [[simp_trace=true]] 

как в Emacs.

Как включить «Трассировка» в jEdit?

Answer 1

Вы действительно можете использовать simp_trace в середине доказательства в Isabelle/jEdit, например, так:

lemma "(2 :: nat) + 2 = 4" 
    using [[simp_trace]] 
    apply simp 
    done 

В качестве альтернативы, вы можете объявить его во всем мире, например, так:

declare [[simp_trace]] 

lemma "(2 :: nat) + 2 = 4" 
    apply simp 
    done 

Оба дают вы отслеживаете трассировку упрощения в окне «Выход», когда ваш курсор сразу после инструкции apply simp в jEdit.

Answer 2

Если вам нужна глубина трассировки глубже, чем 1 (по умолчанию), вы точно настроить его по

declare [[simp_trace_depth_limit=4]] 

Этот пример затем дает глубину трассировки 4.

Answer 3

Как уже отмечалось, вы можете использовать simp_trace. Тем не менее, вы также можете использовать simp_trace_new в сочетании с окном «Упростительная трассировка». Это обеспечивает улучшенный выход через simp_trace:

lemma "rev (rev xs) = xs" 
    using [[simp_trace_new]] 
    apply(induction xs) 
    apply(auto) 
    done 

Для просмотра трассировки, установите курсор на «применить (автоматический режим)» и нажмите на «См Simplifier следа». Откроется окно «Ускоритель трассировки» (вкладка). Нажмите «Показать трассировку», и должно появиться новое окно, показывающее след для каждой подцели.

Изабель/Изар reference содержит более подробную информацию:

simp_trace_new управления Simplifier трассировки в приложениях Изабелль/PIDE, в частности Изабель/jEdit.
Это обеспечивает иерархическое представление шагов перезаписи, выполняемых Упротификатором.
Пользователи могут настраивать поведение, указывая точки останова, verbosity и включение или отключение интерактивного режима.
В обычной многословии (по умолчанию) только правила, соответствующие точке останова, будут отображаться , указанным пользователем. В полной мере, все приложения правил будут регистрироваться. Интерактивный режим прерывает обычный поток Упротивления и отменяет решение о продолжении использования пользователем через какой-либо диалог графического интерфейса.

В качестве альтернативы можно указать "с помощью [[simp_trace_new режим = полный]]" link here Чтобы увидеть все шаги, предпринятые Simplifier.

ПРИМЕЧАНИЕ: в предыдущем примере, показывающий след «apply (induction xs)», не выводит результат.