[opentheory-users] axioms or proofs?

[Konrad Slind]

ETA_AX used to be a primitive in the HOL logic, but
someone (Bruno Barras? John Harrison?) realized that
it could be proved from the other axioms. Since
removing unnecessary axioms is thought to be
a good thing, it was made into a proved theorem.

Konrad.


On Wed, Jun 3, 2015 at 11:00 AM, Robert White <ai.robert.wangshuai at gmail.com
> wrote:

> 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/>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150603/ff713dc3/attachment.html>