51 ML {*

    52 fun neq_to_rel r neq =

    53 let

    54   val neq = HOLogic.dest_Trueprop (prop_of neq)

    55   val eq = HOLogic.dest_not neq

    56   val (lhs, rhs) = HOLogic.dest_eq eq

    57   val rel = r $ lhs $ rhs

    58   val nrel = HOLogic.mk_not rel

    59 in

    60   HOLogic.mk_Trueprop nrel

    61 end

    62 *}

    63 

    64 ML {*

    65 fun neq_to_rel_tac cases distinct =

    66   rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct)

    67 *}

    68 

    69 ML {*

    70 fun distinct_rel ctxt cases (dists, rel) =

    71 let

    72   val ((_, thms), ctxt') = Variable.import false dists ctxt

    73   val terms = map (neq_to_rel rel) thms

    74   val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms

    75 in

    76   Variable.export ctxt' ctxt nrels

    77 end

    78 *}