在伊莎贝尔定义常数之间的函数

我是一个刚刚开始习惯伊莎贝尔的数学家，而一些应该令人难以置信的简单事情竟然令人沮丧。我如何定义两个常量之间的函数？假设函数f：{1,2,3} \ to {1,2,4}映射1到1,2到4和3到2？在伊莎贝尔定义常数之间的函数

我想我设法定义设置为常数T1和T2无事，但（我猜，因为他们不是数据类型），我不能尝试像

definition f ::"t1 => t2" where 
"f 1 = 1" | 
"f 2 = 4" | 
"f 3 = 2"

我相信一定会有这是这个难题背后的根本误解，所以我很欣赏任何指导。

来源

2016-06-21 José Siqueira

您的问题有很多方面。

首先，拿东西快速工作，使用fun关键字来代替definition，就像这样：

fun test :: "nat ⇒ nat" where 
    "test (Suc 0) = 1" | 
    "test (Suc (Suc 0)) = 4" | 
    "test (Suc (Suc (Suc 0))) = 2" | 
    "test _ = undefined"

您可以直接在使用definition关键字定义的头部任何参数不是模式匹配，而你可以用fun。还要注意，我已经用模式匹配中的nat数据类型（0和Suc）的构造函数替换了重载的数字文字（1,2,3等）。

另一种方法是坚持definition，但使用case声明推函数的参数的情况下，分析的定义体内，就像这样：

definition test2 :: "nat ⇒ nat" where 
    "test2 x ≡ 
    case x of 
     (Suc 0) ⇒ 1 
    | (Suc (Suc 0)) ⇒ 4 
    | (Suc (Suc (Suc 0))) ⇒ 2 
    | _ ⇒ undefined"

注意，像test2定义不如果要在证明中扩展test2的出现位置，则需要手动将定理test2_def添加到简化器的simpset中。

您还可以定义与您的两个三元素集合typedef相对应的新类型（不能直接使用集合作为类型），但我个人坚持使用nat。

编辑：使用typedef，做这样的事情：

typedef t1 = "{x::nat. x = 1 ∨ x = 2 ∨ x = 3}" 
    by auto 

definition test :: "t1 ⇒ t1" where 
    "test x ≡ 
    case (Rep_t1 x) of 
    | Suc 0 ⇒ Abs_t1 1 
    | Suc (Suc 0) ⇒ Abs_t1 4 
    | Suc (Suc (Suc 0)) ⇒ Abs_t1 2"

虽然，我真的不用不完typedef自己，所以这可能不是使用这个的最佳方式和其他人可能建议另一种方式。 typedef所做的就是从现有的类型中挖掘出一种新的类型，通过识别新类型的非空集合的居民。证明义务在这里以auto结尾，仅仅是为了证明新类型的定义集合确实是非空的，在这种情况下，我将三元素集划分为一个新类型，称为t1，所以证明是相当微不足道的。创建了两个新常量，Abs_t1和Rep_t1，它们允许您在自然和新类型之间来回移动。如果你在typedef命令后面输入print_theorems，你会看到几条关于Isabelle为你自动生成的关于t1的新定理。

来源

2016-06-21 12:24:39

谢谢你。简而言之，你可以通过将函数定义为自然之间的部分函数来绕过这个问题，对吗？你能告诉我你如何去使用typedef吗？我真正担心的是，在尝试在Isabelle中开发更复杂的理论之后，我想要检查它是如何处理某些特定情况的，以便验证所有事情是否符合预期（例如，使用Topology.thy定义的理论拓扑空间和它们之间的连续映射的例子，并测试一些东西）。 –

@JoséSiqueira回答你的第一个问题：是的，你可以在自然中使用“部分”函数（实际上，HOL是全部函数的逻辑，看起来像部分函数实际上不是）。至于如何使用'typedef'：在你的情况下，它可能看起来像我上面的编辑。 –

在伊莎贝尔定义常数之间的函数

回答

相关问题