1 theory FiniteType

     2 imports "../Nominal2"

     3 begin

     4 

     5 typedef ('a::pt, 'b::fs) ffun = "{f::'a => 'b. finite (supp f)}"

     6 apply(rule_tac x="\<lambda>_. undefined::'b::fs" in exI)

     7 apply(auto)

     8 apply(rule_tac S="supp (undefined::'b::fs)" in supports_finite)

     9 apply(simp add: supports_def)

    10 apply(perm_simp)

    11 apply(simp add: fresh_def[symmetric])

    12 apply(simp add: swap_fresh_fresh)

    13 apply(simp add: finite_supp)

    14 done

    15 

    16 

    17 

    18 

    19 end