262 

   262 lemma equivp_rspl:

   263 end

   263   "equivp r \<Longrightarrow> r a b \<Longrightarrow> r a c = r b c"

   264   unfolding equivp_reflp_symp_transp symp_def transp_def 

   265   by blast

   266 

   267 lemma equivp_rspr:

   268   "equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b"

   269   unfolding equivp_reflp_symp_transp symp_def transp_def 

   270   by blast

   271 

   272 ML {*

   273 fun prove_alpha_bn_rsp alphas inducts inj_dis equivps ctxt (alpha_bn, n) =

   274 let

   275   val alpha = nth alphas n;

   276   val ty = domain_type (fastype_of alpha);

   277   val names = Datatype_Prop.make_tnames [ty, ty];

   278   val [l, r] = map (fn x => (Free (x, ty))) names;

   279   val g1 =

   280     Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r),

   281       HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty,

   282         HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0))))

   283   val g2 =

   284     Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r),

   285       HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty,

   286         HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))))

   287   fun tac {context, ...} = (

   288     etac (nth inducts n) THEN_ALL_NEW

   289     (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW

   290     InductTacs.case_tac context "a" THEN_ALL_NEW split_conjs THEN_ALL_NEW

   291     asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW

   292     REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW

   293     TRY o eresolve_tac (map (fn x => @{thm equivp_rspl} OF [x]) equivps) THEN_ALL_NEW

   294     TRY o eresolve_tac (map (fn x => @{thm equivp_rspr} OF [x]) equivps) THEN_ALL_NEW

   295     TRY o rtac refl

   296   ) 1;

   297   val t1 = Goal.prove ctxt names [] g1 tac;

   298   val t2 = Goal.prove ctxt names [] g2 tac;

   299 in

   300   [t1, t2]

   301 end

   302 *}

   303 

   304 

   305 end