For HOL Light I've got a tool called Tactician that would be ideal for that:
http://www.proof-technologies.com/tactician/
but it doesn't work for HOL4. One day I hope to port it, but that's
unlikely to be done in the near future.
Mark.
on 27/11/15 8:20 AM, Ada <ada.k...@qq.com> wrote:
> Hey guys,
>
> I am learning to use HOL. Here is some code.
>
> load "abs_tools";
>
> open abs_tools;
> val _ = type_abbrev ("num_field", ``:complex -> bool``);
> (* ------------------------------------------------------------------ *)
> (* Definition of number field. *)
> (* ------------------------------------------------------------------ *)
>
> val s = ``s : num_field``;
>
> val nf_carrier = ``s SUBSET univ(:complex) /\ s <> {}:complex -> bool``;
> val nf_constant = ``0c IN s /\ 1c IN s``;
> val nf_operation = ``!a:complex b:complex. a IN s /\ b IN s
> ==> (a+b IN s) /\ (a-b IN s) /\
> (a*b IN s)
> /\ (if a <> 0 then b/a IN s
> else a = 0c)``;
>
> val is_num_field_def = Define `
> num_field ^s =
> ^nf_carrier
> /\ ^nf_constant
> /\ ^nf_operation `;
> (* We work on an abstract number field s *)
>
> val _ = set_assums [ ``num_field ^s`` ];
>
> (* prove the coditions of number field *)
>
> val nf_proj_tac =
>
> POP_ASSUM MP_TAC THEN RW_TAC arith_ss [is_num_field_def] THEN STRIP_TAC;
> val carrier =
>
> asm_store_thm("carrier",nf_carrier,nf_proj_tac);
> val constant =
>
> asm_store_thm("constant",nf_constant,nf_proj_tac);
> val operation =
> asm_store_thm("operation",nf_operation,nf_proj_tac);
>
> Now, I want to write the prove in another way. For example, how to
> transform
>
> "val carrier =
>
> asm_store_thm("carrier",nf_carrier,nf_proj_tac); "
>
> into the form of
>
> "g(...)
> e(...)
> e(...)
> "
> Thanks! --Wish.
>
>
> ----------------------------------------
>
>
----------------------------------------------------------------------------
> --
>
>
>
> ----------------------------------------
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
