[opentheory-users] axioms or proofs?

[Robert White]

Dear Joe,

Is there any reason why you want to change some axioms in the files as
"proofs"?
For example:

let ETA_AX =
  let axiom =
      let ty0 = mk_vartype "A" in
      let ty1 = mk_vartype "B" in
      let ty2 = mk_fun_ty ty0 ty1 in
      let ty3 = mk_type ("bool",[]) in
      let ty4 = mk_fun_ty ty2 ty3 in
      let tm0 = mk_var ("a",ty4) in
      let tm1 = mk_var ("b",ty2) in
      let tm2 = mk_var ("c",ty3) in
      let tm3 = mk_abs (tm2,tm2) in
      let tm4 = mk_eq (tm3,tm3) in
      let tm5 = mk_abs (tm1,tm4) in
      let tm6 = mk_eq (tm0,tm5) in
      let tm7 = mk_abs (tm0,tm6) in
      let tm8 = mk_var ("d",ty2) in
      let tm9 = mk_var ("e",ty0) in
      let tm10 = mk_comb (tm8,tm9) in
      let tm11 = mk_abs (tm9,tm10) in
      let tm12 = mk_eq (tm11,tm8) in
      let tm13 = mk_abs (tm8,tm12) in
      let tm14 = mk_comb (tm7,tm13) in
      new_axiom tm14
  in
  prove
    (`!(t:A->B). (\x. t x) = t`,
     PURE_REWRITE_TAC [FORALL_DEF; T_DEF] THEN
     ACCEPT_TAC axiom);;


instead of just :

let ETA_AX = new_axiom
  `!t:A->B. (\x. t x) = t`;;

Thanks!

-- 

Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150603/047e2811/attachment.html>