type_synonym VS在伊莎貝爾定義

Question

我在伊莎貝爾以下兩個表達式consts：

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

type_synonym drives="(Person × Car) set" 

他們是如何在語義方面有什麼不同？

我認爲type_synonym只是它前面指定的類型的簡短名稱。對？

但是const是爲了什麼？ （伊莎貝爾教程文件--page 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)}" 

然而，標準的定義可以更直接地通過定義進行。

希望這有助於 勒