Unfold/simp has no effect in a primrec type class instantiation proof

Question

Up until several days ago, I always defined a type, and then proved theorems directly about the type. Now I'm trying to use type classes.

Problem

The problem is that I can't instantiate cNAT for my type myD below, and it appears it's because simp has no effect on the abstract function cNAT, which I've made concrete with my primrec function cNAT_myD. I can only guess what's happening because of the automation that happens after instance proof.

Questions

Q1: Below, at the statement instantiation myD :: (type) cNAT, can you tell me how to finish the proof, and why I can prove the following theorem, but not the type class proof, which requires injective?

theorem dNAT_1_to_1: "(dNAT n = dNAT m) ==> n = m"

assumes injective: "(cNAT n = cNAT m) ==> n = m"

Q2: This is not as important, but at the bottom is this statement:

instantiation myD :: (type) cNAT2

It involves another way I was trying to instantiate cNAT. Can you tell me why I get Failed to refine any pending goal at shows? I put some comments in the source to explain some of what I did to set it up. I used this slightly modified formula for the requirement injective:

assumes injective: "!!n m. (cNAT2 n = cNAT2 m) --> n = m"

Specifics

My contrived datatype is this, which may be useful to me someday: (Update: Well, for another example maybe. A good mental exercise is for me to try and figure out how I can actually get something inside a 'a myD list, other than []. With BNF, something like datatype_new 'a myD = myS "'a myD fset" gives me the warning that there's an unused type variable on the right-hand side)

datatype 'a myD = myL "'a myD list"

The type class is this, which requires an injective function from nat to 'a:

class cNAT =
  fixes cNAT :: "nat => 'a"
  assumes injective: "(cNAT n = cNAT m) ==> n = m"

dNAT: this non-type class version of cNAT works

fun get_myL :: "'a myD => 'a myD list" where
  "get_myL (myL L) = L"

primrec dNAT :: "nat => 'a myD" where
  "dNAT 0       = myL []"
 |"dNAT (Suc n) = myL (myL [] # get_myL(dNAT n))"

fun myD2nat :: "'a myD => nat" where
  "myD2nat (myL [])       = 0"
 |"myD2nat (myL (x # xs)) = Suc(myD2nat (myL xs))"

theorem left_inverse_1 [simp]:
  "myD2nat(dNAT n) = n"
apply(induct n, auto)
by(metis get_myL.cases get_myL.simps)

theorem dNAT_1_to_1:
  "(dNAT n = dNAT m) ==> n = m"
apply(induct n)
apply(simp) (*
  The simp method expanded dNAT.*)
apply(metis left_inverse_1 myD2nat.simps(1))
by (metis left_inverse_1)

cNAT: type class version that I can't instantiate

instantiation myD :: (type) cNAT
begin
primrec cNAT_myD :: "nat => 'a myD" where
  "cNAT_myD 0       = myL []"
 |"cNAT_myD (Suc n) = myL (myL [] # get_myL(cNAT_myD n))"

instance
proof 
  fix n m :: nat
show "cNAT n = cNAT m ==> n = m"
  apply(induct n)
  apply(simp) (*
The simp method won't expand cNAT to cNAT_myD's definition.*)
  by(metis injective)+ (*
Metis proved it without unfolding cNAT_myD. It's useless. Goals always remain,
and the type variables in the output panel are all weird.*)
oops
end

cNAT2: Failed to refine any pending goal at show

(*I define a variation of `injective` in which the `assumes` definition, the
  goal, and the `show` statement are exactly the same, and that strange `fails
  to refine any pending goal shows up.*)
class cNAT2 =
  fixes cNAT2 :: "nat => 'a"
  assumes injective: "!!n m. (cNAT2 n = cNAT2 m) --> n = m"

instantiation myD :: (type) cNAT2
begin
primrec cNAT2_myD :: "nat => 'a myD" where
  "cNAT2_myD 0       = myL []"
 |"cNAT2_myD (Suc n) = myL (myL [] # get_myL(cNAT2_myD n))"
instance
proof (*
  goal: !!n m. cNAT2 n = cNAT2 m --> n = m.*)
show 
  "!!n m. cNAT2 n = cNAT2 m --> n = m"

  (*Failed to refine any pending goal 
    Local statement fails to refine any pending goal
    Failed attempt to solve goal by exported rule:
      cNAT2 (n::nat) = cNAT2 (m::nat) --> n = m *)

Answer 1

Your function cNAT is polymorphic in its result type, but the type variable does not appear among the parameters. This often causes type inference to compute a type which is more general than you want. In your case for cNAT, Isabelle infers for the two occurrences of cNAT in the show statement the type nat => 'b for some 'b of sort cNAT, but their type in the goal is nat => 'a myD. You can see this in jEdit by Ctrl-hovering over the cNAT occurrences to inspect the types. In ProofGeneral, you can enable printing of types with using [[show_consts]].

Therefore, you have to explicitly constrain types in the show statement as follows:

fix n m
assume "(cNAT n :: 'a myD) = cNAT m"
then show "n = m"

Note that it is usually not a good idea to use Isabelle's meta-connectives !! and ==> inside a show statement, you better rephrase them using fix/assume/show.