type_synonym对伊莎贝尔定义的比较

Question

“伊莎贝尔”中有以下两种表述：

consts drives ::"(Person × Car) set"

type_synonym drives="(Person × Car) set"

它们在语义上有何不同？

我认为type_synonym只是前面指定的类型的简单名称。对吗？

但是const是干什么用的呢？(伊莎贝尔教程文件--第119页)说：“这是伊莎贝尔在不定义常量的情况下声明常量的方法。”但是，在什么意义上，上面的表达式可以是一个常数呢？！！)

谢谢

Answer 1

实际上，type_synonym只是指定类型的同义词，它没有引入任何新类型。

consts只是声明您将定义给定类型的新常量，而不实际指定它是如何定义的。(请注意，由于在Isabelle/HOL中，每一种类型都是居住的，因此不需要证明这样的常数甚至可以存在)。之后，您可以定义其他函数、定义等，这些函数和定义可能已经使用了新定义的常量(在示例中使用drives，在下面的示例中使用drives_c )。在某个时候，您可以通过、defs、实际提供常量的定义。

type_synonym drives_t = "(int * nat) set"

consts drives_c :: "(int * nat) set"

(* test_drives already used drives_c *)
definition test_drives :: "int => bool" where 
   "test_drives x == (x, 5) : drives_c"

(* here, you actually define drives_c *)
defs drives_c_def: "drives_c == {(3,2), (7,5)}"

但是，标准定义可以通过定义更直接地执行。

definition drives_c :: drives_t where
  "drives_c == {(3,2), (7,5)}"

希望这能帮上忙，勒内