Induction on a well-founded order in Isabelle

I have to prove a property of this form:

lemma 
  assumes "set E ⊆ set E'" "⊢ E' ok"
  shows "set (cv T E b) ⊆ set (cv T E' b)"

I want to prove it using something like:

proof(induction "(size T, length E)" 
        arbitrary: E T rule: less_induct)

meaning that the induction hypothesis should give me the property for all pairs T, E such that in the lexicographic order:

(size T, length E)

is smaller.

So far I only got the error message:

exception THM 0 raised (line 760 of "drule.ML"):
  infer_instantiate_types: type ?'a of variable ?a
  cannot be unified with type nat × nat of term x__
  (⋀x. (⋀y. y < x ⟹ ?P y) ⟹ ?P x) ⟹ ?P ?a

Solution

The problem is that the typeclass instance for the ordering on pairs is not imported by default. You can import "HOL-Library.Product_Lexorder" to get the normal lexicographical ordering on pairs.

Alternatively you can use the rule wf_induct and provide your own well-founded relation.