106  

   106 lemma plus_sym_pre:

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

   108   sorry

   109 

   110 lemma equiv_intrel: "EQUIV intrel"

   111   sorry

   112 

   113 lemma intrel_refl: "intrel a a"

   114   sorry

   115 

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

   117   sorry

   118 

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

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

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

   122 

   123 ML {*

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

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

   126 *}

   127 ML {*

   128 fun r_mk_comb_tac_myint ctxt =

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

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

   131 *}

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

   133   Toplevel.program (fn () =>

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

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

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

   137   )

   138 *}

   139 ML {*

   140   val t_t2 =

   141   Toplevel.program (fn () =>

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

   143   )

   144 *}

   145 ML {*

   146  val lpi = Drule.instantiate'

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

   148 *}

   149 prove lambda_prs_mn_b : {* concl_of lpi *}

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

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

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

   153 done

   154 

   155 ML {*

   156   fun simp_lam_prs lthy thm =

   157     simp_lam_prs lthy (eqsubst_thm lthy

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

   159     thm)

   160     handle _ => thm

   161 *}

   162 ML {* t_t2 *}

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

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

   165 

   166 ML {*

   167   fun simp_allex_prs lthy thm =

   168     let

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

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

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

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

   173     in

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

   175     end

   176     handle _ => thm

   177 *}

   178 

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

   180 

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

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

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

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

   185 ML {* ObjectLogic.rulify t_r *}