lemma plus_sym_pre:

  shows "intrel (my_plus a b) (my_plus b a)"

  sorry

lemma equiv_intrel: "EQUIV intrel"

  sorry

lemma intrel_refl: "intrel a a"

  sorry

lemma ho_plus_rsp : "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus"

  sorry

ML {* val t_a = atomize_thm @{thm plus_sym_pre} *}

ML {* val t_r = regularize t_a @{typ "nat \<times> nat"} @{term "intrel"} @{thm equiv_intrel} @{context} *}

ML {* val consts = [@{const_name "my_plus"}] *}

ML {*

  val rt = build_repabs_term @{context} t_r consts @{typ "nat \<times> nat"} @{typ "my_int"}

  val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);

*}

ML {*

fun r_mk_comb_tac_myint ctxt =

  r_mk_comb_tac ctxt @{thm QUOTIENT_my_int} @{thm intrel_refl} @{thm QUOT_TYPE_I_my_int.R_trans2}

   (@{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs})

*}

ML {* val (g, thm, othm) =

  Toplevel.program (fn () =>

  repabs_eq @{context} t_r consts @{typ "nat \<times> nat"} @{typ "my_int"}

   @{thm QUOTIENT_my_int} @{thm intrel_refl} @{thm QUOT_TYPE_I_my_int.R_trans2}

   (@{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs})

  )

*}

ML {*

  val t_t2 =

  Toplevel.program (fn () =>

    repabs_eq2 @{context} (g, thm, othm)

  )

*}

ML {*

 val lpi = Drule.instantiate'

   [SOME @{ctyp "nat \<times> nat"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS};

*}

prove lambda_prs_mn_b : {* concl_of lpi *}

apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})

apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})

apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})

done

ML {*

  fun simp_lam_prs lthy thm =

    simp_lam_prs lthy (eqsubst_thm lthy

      @{thms HOL.sym[OF lambda_prs_mn_b,simplified]}

    thm)

    handle _ => thm

*}

ML {* t_t2 *}

ML {* val t_l = simp_lam_prs @{context} t_t2 *}

ML {* findabs @{typ "nat \<times> nat"} (prop_of (atomize_thm @{thm plus_sym_pre})) *}

ML {*

  fun simp_allex_prs lthy thm =

    let

      val rwf = @{thm FORALL_PRS[OF QUOTIENT_my_int]};

      val rwfs = @{thm "HOL.sym"} OF [rwf];

      val rwe = @{thm EXISTS_PRS[OF QUOTIENT_my_int]};

      val rwes = @{thm "HOL.sym"} OF [rwe]

    in

      (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm))

    end

    handle _ => thm

*}

ML {* val t_a = simp_allex_prs @{context} t_l *}

ML {* val t_defs = @{thms PLUS_def} *}

ML {* val t_defs_sym = add_lower_defs @{context} t_defs *}

ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *}

ML {* val t_r = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_my_int.REPS_same} t_d *}

ML {* ObjectLogic.rulify t_r *}