Juvix can be used to generate Isabelle theories¶

For example, we can define the following Juvix module, assuming the file is named isabelle.juvix:

module isabelle;

type Nat : Type :=
  | zero
  | succ Nat;

add : Nat -> Nat -> Nat
  | zero n := n
  | (succ m) n := succ (add m n);

And then we can generate an Isabelle theory from it with the following command:

juvix isabelle isabelle.juvix

This will generate a file isabelle.thy in the current directory.

theory isabelle
imports Main
begin

datatype Nat
  = zero |
    succ Nat

(* --8<-- [start:isabelle-add-def] *)
fun add :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat" where
  "add zero n = n" |
  "add (succ m) n = (succ (add m n))"
(* --8<-- [end:isabelle-add-def] *)
end