[isabelle] Question about finite sets

Dear all,

I was trying to define a (recursive) function over sets. One of the
premises in my setting is that sets are finite. The function should
behave as follows:

function remove :: "'b set => 'b set => 'b set"
  remove_Nil: "remove A {} = A"
  | remove_Cons: "remove A (insert x B) = (if _ then remove whatever B
else remove whatever' B)"

The function is decreasing in the size of the second argument (which
has a finite cardinal), but I do not know if there is some chance to
define "remove" by means of "fun", "function" or some other recursive
mechanism. What kind of induction rule is then obtained for that
recursive definition (something similar to finite.induct)?

Thanks in advance for any help,


Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.