Functor-like construction in Isabelle/Isar

Question

Here's a small theorem in mathematics:

Suppose u is not an element of A, and v is not an element of B, and f is an injective function from A to B. Let A' = A union {u} and B' = B union {v}, and define g: A' -> B' by g(x) = f(x) if x is in A, and g(u) = v. Then g is injective as well.

If I were writing OCaml-like code, I'd represent A and B as types, and f as an A->B function, something like

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

and then define a 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;;

and my theorem would be that if Q.f is injective, then so is (Extend Q).f, where I'm hoping I've gotten the syntax more or less correct.

I'd like to do the same thing in Isabelle/Isar. Normally, that'd mean writing something like

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

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

and Q is ... something. I don't know how to make, in Isabelle a single operation analogous to the functor Q in OCaml that creates two new datatypes and a function between them. The proof of injectivity seems as if it'd be fairly straightforward --- merely a four-case split. But I'd like help defining the new function that I've called Q f, given the function f.

John John · Accepted Answer · 2019-03-06T20:27:47

Here's a solution. I tried to make a "definition" for the function Q, but could not do so; instead, creating a constant Q (built in strong analogy to map) let me state and prove the theorem:

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

Functor-like construction in Isabelle/Isar

1 Answers