<div dir="ltr">ETA_AX used to be a primitive in the HOL logic, but <div>someone (Bruno Barras? John Harrison?) realized that</div><div>it could be proved from the other axioms. Since </div><div>removing unnecessary axioms is thought to be </div><div>a good thing, it was made into a proved theorem.</div><div><br></div><div>Konrad.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jun 3, 2015 at 11:00 AM, Robert White <span dir="ltr"><<a href="mailto:ai.robert.wangshuai@gmail.com" target="_blank">ai.robert.wangshuai@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Dear Joe,<div><br></div><div>Is there any reason why you want to change some axioms in the files as "proofs"?</div><div>For example: </div><div><div><br></div><div>let ETA_AX =</div><div>  let axiom =</div><div>      let ty0 = mk_vartype "A" in</div><div>      let ty1 = mk_vartype "B" in</div><div>      let ty2 = mk_fun_ty ty0 ty1 in</div><div>      let ty3 = mk_type ("bool",[]) in</div><div>      let ty4 = mk_fun_ty ty2 ty3 in</div><div>      let tm0 = mk_var ("a",ty4) in</div><div>      let tm1 = mk_var ("b",ty2) in</div><div>      let tm2 = mk_var ("c",ty3) in</div><div>      let tm3 = mk_abs (tm2,tm2) in</div><div>      let tm4 = mk_eq (tm3,tm3) in</div><div>      let tm5 = mk_abs (tm1,tm4) in</div><div>      let tm6 = mk_eq (tm0,tm5) in</div><div>      let tm7 = mk_abs (tm0,tm6) in</div><div>      let tm8 = mk_var ("d",ty2) in</div><div>      let tm9 = mk_var ("e",ty0) in</div><div>      let tm10 = mk_comb (tm8,tm9) in</div><div>      let tm11 = mk_abs (tm9,tm10) in</div><div>      let tm12 = mk_eq (tm11,tm8) in</div><div>      let tm13 = mk_abs (tm8,tm12) in</div><div>      let tm14 = mk_comb (tm7,tm13) in</div><div>      new_axiom tm14</div><div>  in</div><div>  prove</div><div>    (`!(t:A->B). (\x. t x) = t`,</div><div>     PURE_REWRITE_TAC [FORALL_DEF; T_DEF] THEN</div><div>     ACCEPT_TAC axiom);;</div><div><br></div><div><br></div><div>instead of just :</div><div><br></div><div><div>let ETA_AX = new_axiom</div><div>  `!t:A->B. (\x. t x) = t`;;</div></div><div><br></div><div>Thanks!</div><span class="HOEnZb"><font color="#888888"><div><br></div>-- <br><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><br></div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div></div></div></div></div></div></div></div></div>
</font></span></div></div>
<br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>