Isabelle tacti c определение - PullRequest
Новая
       21

Isabelle tacti c определение

1 голос
/ 03 августа 2020

Я пытался скопировать файл tacti c, который мог бы помочь в доказательстве моей теоремы, однако, похоже, возникли некоторые проблемы.

Исходный tacti c выглядит следующим образом: 

fun typechk_step_tac tyrls =
  FIRSTGOAL (test_assume_tac ORELSE' filt_resolve_tac tyrls 4);

(* Output:
Value or constructor (filt_resolve_tac) has not been declared
*)

Пытался найти этот tacti c в inte rnet, но объяснений этому не так много. Я видел, что какой-то файл теории в 2009 году использует этот метод, а для файла теории 2020 года используется аналогичный метод под названием filter_resolve_from_net_ta c, который, как мне кажется, их типы разные, поэтому я не уверен, как их использовать.

Помимо filter_resolve_ta c, файл tacti c использовал функцию с именем ref , например: 

val basictypeinfo = ref([]:thm list);
(* Output:
Value or constructor (ref) has not been declared
*)

Тем не менее, Isabelle 2020, похоже, что-то знает о ref, поскольку, когда я что-то изменил: 

val basictypeinfo = [];

fun addT typelist = (basictypeinfo := (typelist @(!basictypeinfo)));

(* It shows error:
Type error in function application.
   Function: ! : 'a ref -> 'a
   Argument: basictypeinfo : 'a list
   Reason: Can't unify 'a ref (*In Basis*) with 'a list (*In Basis*) (Different type constructors)
*)

Он ясно показывает, что ref похож на тип, и он определен в Isabelle, верно? Поэтому ссылка в ref ([]: список) должна быть похожа на функцию приведения, и я обнаружил, что есть вещь под названием Unsynchronized.ref , которая решает проблему типа, могу ли я узнать, являются ли они то же самое в этом контексте?

В более поздней части файлов есть также некоторые tacti c, и набор правил кажется не определенным, например: 

etac: Value or constructor (etac) has not been declared
(*
I saw Prof. Paulson had shown this tactic in his Isabelle lecture, 
but I couldn't find it in the Isabelle manual or the implementation manual, 
is the name of it changed?
*)

ZF_typechecks: I couldn't find any rule sets that has this name in the whole ZF directory.

Извините Чтобы задать столько вопросов, кажется, что файл tacti c больше не поддерживается новой Isabelle, есть ли еще люди, использующие Isar / ML для определения новых tacti c? Или большинство людей делают это с помощью объявления метода в Isabelle? И какую часть справочного руководства Изабель / Изар мне следует прочитать, чтобы овладеть этим навыком? Большое спасибо.

...