2

这是数学中的一个小定理：

假设 u 不是 A 的元素，v 不是 B 的元素，f 是从 A 到 B 的单射函数。令 A' = A union {u} 和 B' = B union {v}，并定义g: A' -> B' by g(x) = f(x) 如果 x 在 A 中，并且 g(u) = v。那么 g 也是单射的。

如果我正在编写类似 OCaml 的代码，我会将 A 和 B 表示为类型，并将 f 表示为 A->B 函数，例如

module type Q = 
  sig
   type 'a
   type 'b
   val f: 'a -> 'b
  end

然后定义一个函子

module Extend (M : Q) : Q = 
  struct
    type a = OrdinaryA of M.a | ExoticA
    type b = OrdinaryB of M.b | ExoticB
    let f x = match x with
        OrdinaryA t -> OrdinaryB ( M.f t)
      | Exotic A -> ExoticB
  end;;

我的定理是 ifQ.f是单射的，那么 也是(Extend Q).f，我希望我的语法或多或少是正确的。

我想在 Isabelle/Isar 做同样的事情。通常，这意味着写类似

definition injective :: "('a  ⇒ 'b)  ⇒ bool"
  where "injective f  ⟷ ( ∀ P Q.  (f(P) = f(Q)) ⟷ (P = Q))" 

proposition: "injective f ⟹ injective (Q(f))"

并且Q是……某事。我不知道如何在 Isabelle 中创建一个类似于QOCaml 中的仿函数的单个操作，它创建两个新的数据类型和它们之间的函数。单射性的证明似乎相当简单——只是一个四例拆分。但是我想要帮助定义我调用的新函数Q f，给定函数f。

4

1 回答 1

1

这是一个解决方案。我试图为函数做一个“定义” Q，但做不到；相反，创建一个常数Q（与 强烈类比map）让我陈述并证明定理：

theory Extensions
  imports Main
begin
text ‹We show that if we have f: 'a → 'b that's injective, and we extend 
both the domain and codomain types by a new element, and extend f in the 
obvious way, then the resulting function is still injective.›
  definition injective :: "('a  ⇒ 'b)  ⇒ bool"
    where "injective f  ⟷ ( ∀ P Q.  (f(P) = f(Q)) ⟷ (P = Q))" 

datatype 'a extension = Ordinary 'a | Exotic

fun Q ::  "('a  ⇒ 'b) ⇒ (('a extension)  ⇒ ('b extension))"  where 
   "Q f (Ordinary u) = Ordinary (f u)" |
   "Q f (Exotic) = Exotic"

lemma "⟦injective f⟧ ⟹ injective (Q f)"
  by (smt Q.elims extension.distinct(1) extension.inject injective_def)

end
于 2019-03-06T20:27:47.577 回答