diff --git a/lib/Etanercept.thy b/lib/Etanercept.thy
new file mode 100644
index 000000000..8e18e5ece
--- /dev/null
+++ b/lib/Etanercept.thy
@@ -0,0 +1,711 @@
+(*
+ * Copyright 2015, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ *)
+
+theory Etanercept imports
+  "~~/src/HOL/Word/Word"
+  NICTACompat
+  SignedWords
+  WordBitwiseSigned
+keywords
+  "etanercept" :: diag
+begin
+
+text {*
+  This theory implements a tool for refuting word propositions. It works by constructing a C program
+  that exhaustively explores the state space of your proposition.
+
+  It is currently a work in progress and has the following known issues:
+   - Temporary files are just left for Isabelle to clean up when it exits. Should we be attempting
+     to remove these ourselves?
+   - The exploration strategy is completely naive, which simplifies the code, but sometimes leads to
+     a failure to find trivial counter-examples.
+   - There's no support for HOL binders like \<forall> and \<exists>. These could be supported relatively easily
+     with GNU statement expressions, but I'm unsure if it's worth it.
+   - We currently only support 8-, 16-, 32-, and 64-bit words. It would be straightforward to
+     support other non-standard widths if required.
+   - Much of the pattern matching in this theory was generated by a script and is quite verbose. It
+     could probably be simplified.
+
+  The tool is named after etanercept, an ill-advised treatment for primary progressive aphasia, a
+  condition who's symptoms include an inability to find the right words for things. Amusingly the
+  word "etanercept" is also quite hard to remember.
+*}
+
+ML {*
+  signature ETANERCEPT =
+  sig
+  end;
+
+  structure Etanercept : ETANERCEPT =
+  struct
+
+  (* Toggle this to enable debugging output. *)
+  val debug = false
+
+  (* XXX: Clagged from metis *)
+  fun dropWhile p =
+    let
+      fun f [] = []
+        | f (l as x :: xs) = if p x then f xs else l
+    in
+      f
+    end
+
+  (* Exponentiation. *)
+  fun exp base n = Real.floor (Math.pow (Real.fromInt base, Real.fromInt n))
+
+  (* Strip whitespace from the end of a string. *)
+  fun rstrip s =
+    s
+    |> String.explode
+    |> List.rev
+    |> dropWhile Char.isSpace
+    |> List.rev
+    |> String.implode
+
+  (* Generate a string that's safe to put in a C string. In particular, we escape backslashes and
+   * remove trailing underscores. The latter is not for string safety, but because focusing leads to
+   * a variable named, e.g. "x__", that originated from a meta-bound "x". Stripping these
+   * underscores makes the counter-example output clearer to the user.
+   *)
+  fun safe_name s =
+    s
+    |> String.explode
+    |> map (fn c => if c = #"\\" then "\\\\" else String.implode [c])
+    |> List.rev
+    |> dropWhile (fn c => c = "_")
+    |> List.rev
+    |> String.concat
+
+  (* Find a C compiler. Prefer Clang. *)
+  val cc =
+    let
+      val (clang, r1) = Isabelle_System.bash_output "which clang";
+      val (gcc, r2) = Isabelle_System.bash_output "which gcc"
+    in
+      if r1 = 0 then SOME (rstrip clang ^ " -Wno-tautological-compare") else
+      if r2 = 0 then SOME (rstrip gcc) else
+      NONE
+    end
+
+  (* Compile a C program. *)
+  fun compile file =
+    case cc of
+        SOME compiler =>
+          let
+            val serial = serial_string ();
+            val tmp = File.shell_path (File.tmp_path (Path.explode ("etanercept" ^ serial ^ ".exe")));
+            val (_, ret) = Isabelle_System.bash_output (compiler ^ " -O3 -o " ^ tmp ^ " " ^ file)
+          in
+            if ret = 0
+              then tmp
+              else error "failed to compile generated program (BUG)"
+          end
+      | NONE => error "no available C compiler"
+
+  (* Find index of x in xs *)
+  fun indexOf xs x =
+    let
+      fun indexOf' i xs x = 
+        case xs of
+            [] => NONE
+          | (y::ys) => if x = y then SOME i else indexOf' (i + 1) ys x
+    in
+      indexOf' 0 xs x
+    end
+
+  (* FIXME: ugh *)
+  fun type_supported [typ] =
+    (case typ of
+        @{typ 8} => true
+      | @{typ "8 signed"} => true
+      | @{typ 16} => true
+      | @{typ "16 signed"} => true
+      | @{typ 32} => true
+      | @{typ "32 signed"} => true
+      | @{typ 64} => true
+      | @{typ "64 signed"} => true
+      | _ => false)
+    | type_supported _ = false
+
+  (* Find a previously seen variable's index or register a newly discovered variable. *)
+  fun var_index vs v =
+    case indexOf vs v of
+        NONE => (vs @ [v], length vs)
+      | SOME n => (vs, n)
+
+  (* The C symbol for the nth variable. *)
+  fun to_var n = "v" ^ Int.toString n
+
+  fun min_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "INT8_MIN"
+    | min_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "INT16_MIN"
+    | min_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "INT32_MIN"
+    | min_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "INT64_MIN"
+    | min_of (Var (_, Type (@{type_name "Word.word"}, _))) = "0"
+    | min_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "INT8_MIN"
+    | min_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "INT16_MIN"
+    | min_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "INT32_MIN"
+    | min_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "INT64_MIN"
+    | min_of (Var (_, Type (@{type_name nat}, _))) = "0"
+    | min_of (Var (_, Type (@{type_name int}, _))) = "INTMAX_MIN"
+    | min_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "INT8_MIN"
+    | min_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "INT16_MIN"
+    | min_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "INT32_MIN"
+    | min_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "INT64_MIN"
+    | min_of (Free (_, Type (@{type_name "Word.word"}, _))) = "0"
+    | min_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "INT8_MIN"
+    | min_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "INT16_MIN"
+    | min_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "INT32_MIN"
+    | min_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "INT64_MIN"
+    | min_of (Free (_, Type (@{type_name nat}, _))) = "0"
+    | min_of (Free (_, Type (@{type_name int}, _))) = "INTMAX_MIN"
+    | min_of _ = error "unsupported type (BUG)"
+
+  fun max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "UINT8_MAX"
+    | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "INT8_MAX"
+    | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "UINT16_MAX"
+    | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "INT16_MAX"
+    | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "UINT32_MAX"
+    | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "INT32_MAX"
+    | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "UINT64_MAX"
+    | max_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "INT64_MAX"
+    | max_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "INT8_MAX"
+    | max_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "INT16_MAX"
+    | max_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "INT32_MAX"
+    | max_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "INT64_MAX"
+    | max_of (Var (_, Type (@{type_name nat}, _))) = "UINTMAX_MAX"
+    | max_of (Var (_, Type (@{type_name int}, _))) = "INTMAX_MAX"
+    | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "UINT8_MAX"
+    | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "INT8_MAX"
+    | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "UINT16_MAX"
+    | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "INT16_MAX"
+    | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "UINT32_MAX"
+    | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "INT32_MAX"
+    | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "UINT64_MAX"
+    | max_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "INT64_MAX"
+    | max_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "INT8_MAX"
+    | max_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "INT16_MAX"
+    | max_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "INT32_MAX"
+    | max_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "INT64_MAX"
+    | max_of (Free (_, Type (@{type_name nat}, _))) = "UINTMAX_MAX"
+    | max_of (Free (_, Type (@{type_name int}, _))) = "INTMAX_MAX"
+    | max_of _ = error "unsupported type (BUG)"
+
+  fun type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "uint8_t"
+    | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "int8_t"
+    | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "uint16_t"
+    | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "int16_t"
+    | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "uint32_t"
+    | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "int32_t"
+    | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "uint64_t"
+    | type_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "int64_t"
+    | type_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "int8_t"
+    | type_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "int16_t"
+    | type_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "int32_t"
+    | type_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "int64_t"
+    | type_of (Var (_, Type (@{type_name nat}, _))) = "uintmax_t"
+    | type_of (Var (_, Type (@{type_name int}, _))) = "intmax_t"
+    | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "uint8_t"
+    | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "int8_t"
+    | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "uint16_t"
+    | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "int16_t"
+    | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "uint32_t"
+    | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "int32_t"
+    | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "uint64_t"
+    | type_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "int64_t"
+    | type_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "int8_t"
+    | type_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "int16_t"
+    | type_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "int32_t"
+    | type_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "int64_t"
+    | type_of (Free (_, Type (@{type_name nat}, _))) = "uintmax_t"
+    | type_of (Free (_, Type (@{type_name int}, _))) = "intmax_t"
+    | type_of _ = error "unsupported type (BUG)"
+
+  fun name_of (Var ((name, _), _)) = safe_name name
+    | name_of (Free (name, _)) = safe_name name
+    | name_of _ = error "unexpected variable (BUG)"
+
+  fun format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "PRIu8"
+    | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "PRId8"
+    | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "PRIu16"
+    | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "PRId16"
+    | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "PRIu32"
+    | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "PRId32"
+    | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "PRIu64"
+    | format_of (Var (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "PRId64"
+    | format_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "PRId8"
+    | format_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "PRId16"
+    | format_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "PRId32"
+    | format_of (Var (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "PRId64"
+    | format_of (Var (_, Type (@{type_name nat}, _))) = "PRIuMAX"
+    | format_of (Var (_, Type (@{type_name int}, _))) = "PRIdMAX"
+    | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 8}]))) = "PRIu8"
+    | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "8 signed"}]))) = "PRId8"
+    | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 16}]))) = "PRIu16"
+    | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "16 signed"}]))) = "PRId16"
+    | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 32}]))) = "PRIu32"
+    | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "32 signed"}]))) = "PRId32"
+    | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ 64}]))) = "PRIu64"
+    | format_of (Free (_, Type (@{type_name "Word.word"}, [@{typ "64 signed"}]))) = "PRId64"
+    | format_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 8}]))) = "PRId8"
+    | format_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 16}]))) = "PRId16"
+    | format_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 32}]))) = "PRId32"
+    | format_of (Free (_, Type (@{type_name "SignedWords.signed"}, [@{typ 64}]))) = "PRId64"
+    | format_of (Free (_, Type (@{type_name nat}, _))) = "PRIuMAX"
+    | format_of (Free (_, Type (@{type_name int}, _))) = "PRIdMAX"
+    | format_of _ = error "unsupported type (BUG)"
+
+  fun cast_to _ @{typ "8 signed word \<Rightarrow> 8 signed word"} = "int8_t"
+    | cast_to _ @{typ "8 signed word \<Rightarrow> 8 word"} = "uint8_t"
+    | cast_to _ @{typ "8 signed word \<Rightarrow> 16 signed word"} = "int16_t"
+    | cast_to _ @{typ "8 signed word \<Rightarrow> 16 word"} = "uint16_t"
+    | cast_to _ @{typ "8 signed word \<Rightarrow> 32 signed word"} = "int32_t"
+    | cast_to _ @{typ "8 signed word \<Rightarrow> 32 word"} = "uint32_t"
+    | cast_to _ @{typ "8 signed word \<Rightarrow> 64 signed word"} = "int64_t"
+    | cast_to _ @{typ "8 signed word \<Rightarrow> 64 word"} = "uint64_t"
+    | cast_to _ @{typ "8 word \<Rightarrow> 8 signed word"} = "int8_t"
+    | cast_to _ @{typ "8 word \<Rightarrow> 8 word"} = "uint8_t"
+    | cast_to _ @{typ "8 word \<Rightarrow> 16 signed word"} = "int16_t"
+    | cast_to _ @{typ "8 word \<Rightarrow> 16 word"} = "uint16_t"
+    | cast_to _ @{typ "8 word \<Rightarrow> 32 signed word"} = "int32_t"
+    | cast_to _ @{typ "8 word \<Rightarrow> 32 word"} = "uint32_t"
+    | cast_to _ @{typ "8 word \<Rightarrow> 64 signed word"} = "int64_t"
+    | cast_to _ @{typ "8 word \<Rightarrow> 64 word"} = "uint64_t"
+    | cast_to _ @{typ "16 signed word \<Rightarrow> 8 signed word"} = "int8_t"
+    | cast_to _ @{typ "16 signed word \<Rightarrow> 8 word"} = "uint8_t"
+    | cast_to _ @{typ "16 signed word \<Rightarrow> 16 signed word"} = "int16_t"
+    | cast_to _ @{typ "16 signed word \<Rightarrow> 16 word"} = "uint16_t"
+    | cast_to _ @{typ "16 signed word \<Rightarrow> 32 signed word"} = "int32_t"
+    | cast_to _ @{typ "16 signed word \<Rightarrow> 32 word"} = "uint32_t"
+    | cast_to _ @{typ "16 signed word \<Rightarrow> 64 signed word"} = "int64_t"
+    | cast_to _ @{typ "16 signed word \<Rightarrow> 64 word"} = "uint64_t"
+    | cast_to _ @{typ "16 word \<Rightarrow> 8 signed word"} = "int8_t"
+    | cast_to _ @{typ "16 word \<Rightarrow> 8 word"} = "uint8_t"
+    | cast_to _ @{typ "16 word \<Rightarrow> 16 signed word"} = "int16_t"
+    | cast_to _ @{typ "16 word \<Rightarrow> 16 word"} = "uint16_t"
+    | cast_to _ @{typ "16 word \<Rightarrow> 32 signed word"} = "int32_t"
+    | cast_to _ @{typ "16 word \<Rightarrow> 32 word"} = "uint32_t"
+    | cast_to _ @{typ "16 word \<Rightarrow> 64 signed word"} = "int64_t"
+    | cast_to _ @{typ "16 word \<Rightarrow> 64 word"} = "uint64_t"
+    | cast_to _ @{typ "32 signed word \<Rightarrow> 8 signed word"} = "int8_t"
+    | cast_to _ @{typ "32 signed word \<Rightarrow> 8 word"} = "uint8_t"
+    | cast_to _ @{typ "32 signed word \<Rightarrow> 16 signed word"} = "int16_t"
+    | cast_to _ @{typ "32 signed word \<Rightarrow> 16 word"} = "uint16_t"
+    | cast_to _ @{typ "32 signed word \<Rightarrow> 32 signed word"} = "int32_t"
+    | cast_to _ @{typ "32 signed word \<Rightarrow> 32 word"} = "uint32_t"
+    | cast_to _ @{typ "32 signed word \<Rightarrow> 64 signed word"} = "int64_t"
+    | cast_to _ @{typ "32 signed word \<Rightarrow> 64 word"} = "uint64_t"
+    | cast_to _ @{typ "32 word \<Rightarrow> 8 signed word"} = "int8_t"
+    | cast_to _ @{typ "32 word \<Rightarrow> 8 word"} = "uint8_t"
+    | cast_to _ @{typ "32 word \<Rightarrow> 16 signed word"} = "int16_t"
+    | cast_to _ @{typ "32 word \<Rightarrow> 16 word"} = "uint16_t"
+    | cast_to _ @{typ "32 word \<Rightarrow> 32 signed word"} = "int32_t"
+    | cast_to _ @{typ "32 word \<Rightarrow> 32 word"} = "uint32_t"
+    | cast_to _ @{typ "32 word \<Rightarrow> 64 signed word"} = "int64_t"
+    | cast_to _ @{typ "32 word \<Rightarrow> 64 word"} = "uint64_t"
+    | cast_to _ @{typ "64 signed word \<Rightarrow> 8 signed word"} = "int8_t"
+    | cast_to _ @{typ "64 signed word \<Rightarrow> 8 word"} = "uint8_t"
+    | cast_to _ @{typ "64 signed word \<Rightarrow> 16 signed word"} = "int16_t"
+    | cast_to _ @{typ "64 signed word \<Rightarrow> 16 word"} = "uint16_t"
+    | cast_to _ @{typ "64 signed word \<Rightarrow> 32 signed word"} = "int32_t"
+    | cast_to _ @{typ "64 signed word \<Rightarrow> 32 word"} = "uint32_t"
+    | cast_to _ @{typ "64 signed word \<Rightarrow> 64 signed word"} = "int64_t"
+    | cast_to _ @{typ "64 signed word \<Rightarrow> 64 word"} = "uint64_t"
+    | cast_to _ @{typ "64 word \<Rightarrow> 8 signed word"} = "int8_t"
+    | cast_to _ @{typ "64 word \<Rightarrow> 8 word"} = "uint8_t"
+    | cast_to _ @{typ "64 word \<Rightarrow> 16 signed word"} = "int16_t"
+    | cast_to _ @{typ "64 word \<Rightarrow> 16 word"} = "uint16_t"
+    | cast_to _ @{typ "64 word \<Rightarrow> 32 signed word"} = "int32_t"
+    | cast_to _ @{typ "64 word \<Rightarrow> 32 word"} = "uint32_t"
+    | cast_to _ @{typ "64 word \<Rightarrow> 64 signed word"} = "int64_t"
+    | cast_to _ @{typ "64 word \<Rightarrow> 64 word"} = "uint64_t"
+    | cast_to st t = error ("unsupported ucast/scast result type: " ^
+        Pretty.string_of (Syntax.pretty_typ (Proof.context_of st) t))
+
+  (* A printf format string for printing the variables. *)
+  fun format_string vs =
+    case vs of
+        [] => ""
+      | (y::ys) => "\" " ^ name_of y ^ " = %\" " ^ format_of y ^ " \"\\n\" " ^ format_string ys
+
+  (* The variables as a list of arguments to be passed to a C function. *)
+  fun as_args vs =
+    let
+      fun as_args' n vs =
+        case vs of
+            [] => ""
+          | (_::ys) => ", " ^ to_var n ^ as_args' (n + 1) ys
+    in
+      as_args' 0 vs
+    end
+
+  (* Initialisation for the variables. *)
+  fun loop_header vs =
+    let
+      fun loop_header' i vs =
+        case vs of
+            [] => ""
+          | (y::ys) => type_of y ^ " " ^ to_var i ^ ";\n" ^
+                       "for (" ^ to_var i ^ " = " ^ min_of y ^ "; ; " ^ to_var i ^ "++) {\n" ^
+                       loop_header' (i + 1) ys
+    in
+      loop_header' 0 vs
+    end
+
+  (* Per-variable loop termination. *)
+  fun loop_footer vs =
+    let
+      fun loop_footer' i vs =
+        case vs of
+            [] => ""
+          | (y::ys) => loop_footer' (i + 1) ys ^
+                       "if (" ^ to_var i ^ " == " ^ max_of y ^ ") { break; }\n" ^
+                       "}\n"
+    in
+      loop_footer' 0 vs
+    end
+
+  (* Translate an Isabelle term into the equivalent C expression, collecting discovered variables
+   * along the way.
+   *)
+  fun translate state vs t =
+    let
+      val tr = translate state
+      fun bin_op op1 op2 =
+        let val (vs', s1) = tr vs op1;
+            val (vs'', s2) = tr vs' op2
+          in (vs'', s1, s2)
+        end
+    in
+      case t of
+          @{term "Trueprop"} $ t' => tr vs t'
+        | @{term "True"} => (vs, "true")
+        | @{term "False"} => (vs, "false")
+        | Const (@{const_name HOL.eq}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " == " ^ s2 ^ ")")
+            end
+        | Const (@{const_name HOL.Not}, _) $ a =>
+            let val (vs', s) = tr vs a
+              in (vs', "(!" ^ s ^ ")")
+            end
+        | Const (@{const_name less}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " < " ^ s2 ^ ")")
+            end
+        | Const (@{const_name less_eq}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " <= " ^ s2 ^ ")")
+            end
+        | Const (@{const_name plus}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " + " ^ s2 ^ ")")
+            end
+        | Const (@{const_name minus}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " - " ^ s2 ^ ")")
+            end
+        | Const (@{const_name times}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " * " ^ s2 ^ ")")
+            end
+        | Const (@{const_name uminus}, _) $ a =>
+            let val (vs', s) = tr vs a
+              in (vs', "(-" ^ s ^ ")")
+            end
+        | Const (@{const_name div}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s2 ^ " == 0 ? 0 : (" ^ s1 ^ " / " ^ s2 ^ "))")
+            end
+        | Const (@{const_name mod}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s2 ^ " == 0 ? " ^ s1 ^ " : (" ^ s1 ^ " % " ^ s2 ^ "))")
+            end
+        | Const (@{const_name HOL.implies}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "((!" ^ s1 ^ ") || (" ^ s2 ^ "))")
+            end
+        | Const (@{const_name Bits.shiftl}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " << " ^ s2 ^ ")")
+            end
+        | Const (@{const_name Bits.shiftr}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " >> " ^ s2 ^ ")")
+            end
+        | Const (@{const_name Bits.bitAND}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " & " ^ s2 ^ ")")
+            end
+        | Const (@{const_name Bits.bitOR}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " | " ^ s2 ^ ")")
+            end
+        | Const (@{const_name Bits.bitXOR}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " ^ " ^ s2 ^ ")")
+            end
+        | Const (@{const_name Bits.bitNOT}, _) $ a =>
+            let val (vs', s) = tr vs a
+              in (vs', "(~" ^ s ^ ")")
+            end
+        | Const (@{const_name Bits.test_bit}, _) $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " ^ & (1ULL << " ^ s2 ^ "))")
+            end
+        | Const (@{const_name Bits.lsb}, _) $ a =>
+            let val (vs', s) = tr vs a
+              in (vs', "(" ^ s ^ " & 1)")
+            end
+        | Const (@{const_name Word.ucast}, typ) $ a =>
+            let val (vs', s) = tr vs a
+              in (vs', "((" ^ cast_to state typ ^ ")" ^ s ^ ")")
+            end
+        | Const (@{const_name Word.scast}, typ) $ a =>
+            let val (vs', s) = tr vs a
+              in (vs', "((" ^ cast_to state typ ^ ")" ^ s ^ ")")
+            end
+        | Free (name, Type (@{type_name "Word.word"}, typs)) =>
+            if type_supported typs
+              then let val (vs', n) = var_index vs t
+                     in (vs', to_var n)
+                   end
+              else error ("unsupported word width of variable " ^ name)
+        | Var ((name, _), Type (@{type_name "Word.word"}, typs)) =>
+            if type_supported typs
+              then let val (vs', n) = var_index vs t
+                     in (vs', to_var n)
+                   end
+              else error ("unsupported word width of variable " ^ name)
+        | Free (_, Type (@{type_name nat}, _)) =>
+            let val (vs', n) = var_index vs t
+              in (vs', to_var n)
+            end
+        | Var (_, Type (@{type_name nat}, _)) =>
+            let val (vs', n) = var_index vs t
+              in (vs', to_var n)
+            end
+        | Free (_, Type (@{type_name int}, _)) =>
+            let val (vs', n) = var_index vs t
+              in (vs', to_var n)
+            end
+        | Var (_, Type (@{type_name int}, _)) =>
+            let val (vs', n) = var_index vs t
+              in (vs', to_var n)
+            end
+        | @{const HOL.conj} $ a $ b =>
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " && " ^ s2 ^ ")")
+            end
+        | @{const HOL.disj} $ a $ b => 
+            let val (vs', s1, s2) = bin_op a b
+              in (vs', "(" ^ s1 ^ " || " ^ s2 ^ ")")
+            end
+        | Const (@{const_name Groups.zero}, _) => (vs, "(0)")
+        | Const (@{const_name Groups.one}, _) => (vs, "(1)")
+        | Const (@{const_name Suc}, _) $ a =>
+            let val (vs', s) = tr vs a
+              in (vs', "(1 + " ^ s ^ ")")
+            end
+        | Const (@{const_name numeral}, _) $ a =>
+            (* XXX: Clagged from c-parser *)
+            let fun calc acc base t = case t of
+                    Const (@{const_name "Num.num.Bit0"}, _) $ t' => calc acc (base * 2) t'
+                  | Const (@{const_name "Num.num.Bit1"}, _) $ t' => calc (acc + base) (base * 2) t'
+                  | Const (@{const_name "Num.num.One"}, _) => acc + base
+                  | _ => error "unexpected numeric literal case (BUG)";
+                val v = calc 0 1 a;
+                val suffix = if v > exp 2 32 - 1 then "ull" else ""
+              in (vs, "(" ^ string_of_int (calc 0 1 a) ^ suffix ^ ")")
+            end
+        | _ => error ("unsupported subterm " ^ Pretty.string_of (Syntax.pretty_term (Proof.context_of state) t))
+    end
+
+  (* Construct a C program to match the current goal state. *)
+  fun make_program st =
+    let
+      val state = Toplevel.proof_of st;
+      val {goal = g, ...} = Proof.raw_goal state;
+      val (_, g') = Subgoal.focus (Proof.context_of state) 1 g
+      val (gi, _) = Logic.goal_params (Thm.prop_of g') 1
+      val (vars, expr) = translate state [] gi
+    in
+      "#include <inttypes.h>\n" ^
+      "#include <limits.h>\n" ^
+      "#include <stdbool.h>\n" ^ 
+      "#include <stdint.h>\n" ^
+      "#include <stdio.h>\n" ^
+      "int main(void) {\n" ^
+      loop_header vars ^
+      "if (!" ^ expr ^ ") {\n" ^
+      "printf(\"Found counter-example:\\n\"" ^ format_string vars ^ as_args vars ^ ");\n" ^
+      "return 0;\n" ^
+      "}\n" ^
+      loop_footer vars ^
+      "return -1;\n" ^
+      "}"
+    end
+
+  (* Try to refute the current goal by using a C program to find a counter example. *)
+  fun refute st =
+    case cc of
+        SOME _ =>
+          let
+            val program = make_program st;
+            val serial = serial_string ();
+            val tmp = File.tmp_path (Path.explode ("etanercept" ^ serial ^ ".c"));
+            val _ = File.write tmp program;
+            val aout = compile (File.shell_path tmp);
+            val (msg, ret) = Isabelle_System.bash_output aout
+          in
+            if debug
+               then writeln ("Program:\n" ^ program ^ "\nWritten to: " ^ File.shell_path tmp ^ "\nCompiled to: " ^ aout)
+               else ();
+            (if ret = 0
+              then msg
+              else "Etanercept found no counter example")
+            |> writeln
+          end
+      | NONE => writeln "no available C compiler"
+
+  (* Install the command itself. *)
+  val _ = Outer_Syntax.command @{command_keyword etanercept}
+            "Construct a C program to find counter-examples to word propositions"
+              (Scan.succeed [] >> (fn _ => Toplevel.keep_proof refute))
+
+  end
+*}
+
+lemma "True \<and> False"
+  etanercept
+  oops
+
+lemma "(x::32 word) = 0"
+  etanercept
+  oops
+
+etanercept
+
+lemma "\<And>x. (x::32 word) \<noteq> y\<^sub>1 \<and> y \<ge> x"
+  etanercept
+  oops
+
+lemma "(x::8 word) = y"
+  etanercept
+  oops
+
+lemma "(x::64 word) < y"
+  etanercept
+  oops
+
+lemma "\<And>(x::32 word) y. x = y"
+  etanercept
+  oops
+
+text {* Previously, this example would give us a tautological comparison warning from Clang. *}
+lemma "y = y \<and> (x::32 word) << y = x"
+  etanercept
+  oops
+
+text {* Example that partially demonstrates Etanercept's utility. *}
+lemma "(x::8 word) > y \<or> x < y + y + y + y"
+  (* quickcheck cannot handle this *)
+    (* quickcheck *)
+  (* quickcheck[random] takes a little while *)
+    quickcheck[random]
+  (* Etanercept immediately finds the trivial counterexample *)
+    etanercept
+  oops
+
+text {* Example that demonstrates one of Etanercept's weaknesses. *}
+lemma "(x::32 word) div y = x"
+  (* The naive exploration strategy means we wait for Etanercept to try every value of y before
+   * moving x beyond 0.
+   *)
+    etanercept
+  oops
+
+text {*
+  This is an interesting example that, due to Etanercept's exploration strategy, *should* be out of
+  its reach with a reasonable time out. Instead, the C compiler folds the entire loop into immediate
+  discovery of a counter-example.
+*}
+lemma "(x::64 word) \<ge> y \<and> x \<ge> y + y"
+  etanercept
+  oops
+
+text {* Various cases that test our handling of numeric literals. *}
+lemma "(x::32 word) && 45 = 0"
+  etanercept
+  oops
+lemma "(x::32 word) < 45"
+  etanercept
+  oops
+lemma "(x::32 word) < 0"
+  etanercept
+  oops
+lemma "(x::32 word) < 1"
+  etanercept
+  oops
+lemma "(x::32 word) < 0x45"
+  etanercept
+  oops
+
+text {* Test something non-trivial that we shouldn't be able to refute. *}
+lemma "(x::32 word) && 1 = 1 \<and> x && (~~ 1) = 0 \<longrightarrow> x = 1"
+  etanercept
+  apply word_bitwise
+  done
+lemma "(x::32 signed word) && 1 = 1 \<and> x && (~~ 1) = 0 \<longrightarrow> x = 1"
+  etanercept
+  apply word_bitwise_signed
+  done
+
+text {* Test that division by zero is correctly modelled with Isabelle's semantics. *}
+lemma "(x::64 word) div 0 = 0"
+  etanercept
+  by (simp add: word_arith_nat_defs(6))
+
+text {* Test we can handle large literals. *}
+lemma "(x::64 word) > 0xcafebeefcafebeef"
+  etanercept
+  oops
+
+text {* Test some casting operations. *}
+lemma "(ucast::32 signed word \<Rightarrow> 32 word) (x::32 signed word) = (y::32 word)"
+  etanercept
+  oops
+lemma "ucast (x::32 word) = (y:: 8 word)"
+  etanercept
+  oops
+lemma "ucast (x::32 word) = (y::32 word)"
+  etanercept
+  oops
+lemma "scast (x::32 signed word) = (y::8 word)"
+  etanercept
+  oops
+
+text {* Try some things we shouldn't be able to refute. *}
+lemma "(x::64 word) >> 0 = x"
+  etanercept
+  by simp
+lemma "(x::64 word) >> 1 = x div 2"
+  etanercept
+  apply simp
+  apply (rule shiftr_div_2n_w[where n=1, simplified])
+  apply (simp add:word_size)
+  done
+lemma "(x::64 word) << 1 = x * 2"
+  etanercept
+  apply (subst shiftl_t2n)
+  apply simp
+  done
+
+end