theory Foo
imports Main
begin

  locale nondegenerate =
  fixes dummy :: 'a
  assumes is_nondegenerate: "\<exists>x :: 'a. x \<noteq> undefined"

(*
  The above produces in the output window:

  locale nondegenerate
  fixes dummy :: "'a"
  assumes "nondegenerate TYPE('a)"
 *)

  context
  begin

    interpretation nondegenerate \<open>undefined :: bool\<close>
(*
  proof (prove)
  goal (1 subgoal):
   1. nondegenerate TYPE(bool)
 *)
    proof
      obtain f :: "bool \<Rightarrow> bool" where f: "inj f"
        using inj_on_id2 by blast
      show "\<exists>x :: bool. x \<noteq> undefined"
        by blast
    qed

    lemma bool_is_nondegenerate:
    shows "nondegenerate (undefined :: bool)"

(*
  Type unification failed: Clash of types "bool" and "_ itself"

  Type error in application: incompatible operand type

  Operator:  nondegenerate :: ??'a itself \<Rightarrow> bool
  Operand:   undefined :: bool
*)

    lemma bool_is_nondegenerate:
    shows "nondegenerate (undefined :: bool itself)"
      using nondegenerate_axioms
      apply blast

(*
  theorem bool_is_nondegenerate:
   nondegenerate undefined 
  Failed to apply initial proof method\<^here>:
  using this:
    nondegenerate TYPE(bool)
  goal (1 subgoal):
   1. nondegenerate undefined


  In this case, Ctrl-hover in the output window over the
  "undefined" in the goal shows "constant: HOL.undefined".
 *)

    oops

    lemma bool_is_nondegenerate:
    shows "nondegenerate TYPE(bool)"
      ..

(*
  theorem bool_is_nondegenerate:
   nondegenerate TYPE(bool)
 *)

  end

  context
  begin

    interpretation nondegenerate \<open>undefined :: bool\<close>
      using bool_is_nondegenerate by blast

    (* Succeeds. *)

  end

end