CODEWITHSUNDEEP
isabelle
José Siqueira
José Siqueira

Reputation: 191

Defining functions between constants in Isabelle

I'm a mathematician just starting to get used to Isabelle, and something that should be incredibly simple turned out to be frustrating. How do I define a function between two constants? Say, the function f: {1,2,3} \to {1,2,4} mapping 1 to 1, 2 to 4 and 3 to 2?

I suppose I managed to define the sets as constants t1 and t2 without incident, but (I guess since they're not datatypes) I can't try something like

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

I believe there must be a fundamental misconception behind this difficulty, so I appreciate any guidance.

Upvotes: 5

Views: 415

Answers (1)

Dominic Mulligan
Dominic Mulligan

Reputation: 466

There's a number of aspects to your question.

First, to get something working quickly, use the fun keyword instead of definition, like so:

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

You cannot pattern match on any arguments directly in the head of the definition using the definition keyword, whereas you can with fun. Note also that I have replaced the overloaded numeric literals (1, 2, 3, etc.) with the constructors for the nat datatype (0 and Suc) in the pattern match.

An alternative would be to stick with definition, but push the case analysis of the function's argument inside the body of the definition using a case statement, like so:

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

Note that definitions like test2 are not unfolded by the simplifier by default, and you will need to manually add the theorem test2_def to the simplifier's simpset if you want to expand occurrences of test2 in a proof.

You can also define new types (you cannot use sets as types, directly, as you are trying to do) corresponding to your two three-element sets with typedef, but personally I would stick with nat.

EDIT: to use typedef, do something like:

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"

Though, I don't really ever use typedef myself, and so this may not be the best way of using this and others may possibly suggest some other way. What typedef does is carve out a new type from an existing one, by identifying a non-empty set of inhabitants for the new type. The proof obligation, here closed by auto, is merely to demonstrate that the defining set for the new type is indeed non-empty, and in this case I am carving out a three-element set of naturals into a new type, called t1, so the proof is fairly trivial. Two new constants are created, Abs_t1 and Rep_t1 which allow you to move back-and-forth between the naturals and the new type. If you put a print_theorems after the typedef command you will see several new theorems about t1 that Isabelle has automatically generated for you.

Upvotes: 5

Related Questions