Isabelle/Isar中的函数式构造

Question

下面是数学中的一个小定理：

设u不是A的元素，v也不是B的元素，f是从A到B的内射函数.设A‘=A并{u}，B’=B并{v}，定义g: A‘-> B’，如果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

然后定义一个functor

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;;

我的定理是，如果Q.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中创建一个操作，类似于OCaml中的函数式Q，它创建了两个新的数据类型，并在它们之间创建了一个函数。内射性的证明似乎相当简单-仅仅是四种情况的拆分。但是我需要帮助定义一个新的函数，我已经调用了Q f，给出了函数f。

Answer 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