28 

    29 

    30 fun

    31   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"

    32 where

    33   "intrel (x, y) (u, v) = (x + v = u + y)"

    34 

    35 quotient_type int = "nat \<times> nat" / intrel

    36   apply(unfold equivp_def)

    37   apply(auto simp add: mem_def expand_fun_eq)

    38   done

    39 

    40 

    41 ML {*

    42 open Quotient_Term;

    43 *}

    44 

    45 ML {*

    46 absrep_fun absF @{context} (@{typ "'a list"}, 

    47                          @{typ "'a fset"})

    48 |> Syntax.check_term @{context}

    49 |> Syntax.string_of_term @{context}

    50 |> writeln

    51 *}

    52 

    53 term "map id"

    54 term "abs_fset o (map id)"

    55 

    56 ML {*

    57 absrep_fun absF @{context} (@{typ "(nat * nat) list"}, 

    58                          @{typ "int fset"})

    59 |> Syntax.check_term @{context}

    60 |> Syntax.string_of_term @{context}

    61 |> writeln

    62 *}

    63 

    64 term "map abs_int"

    65 term "abs_fset o map abs_int"

    66 

    67 

    68 ML {*

    69 absrep_fun absF @{context} (@{typ "('a list) list"}, 

    70                          @{typ "('a fset) fset"})

    71 |> Syntax.check_term @{context}

    72 |> Syntax.string_of_term @{context}

    73 |> writeln

    74 *}

    75 

    76 ML {*

    77 absrep_fun absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, 

    78                          @{typ "('a fset) fset \<Rightarrow> 'a"})

    79 |> Syntax.check_term @{context}

    80 |> Syntax.string_of_term @{context}

    81 |> writeln

    82 *}