Re: [Hol-info] How to transform the proof form

[Mark Adams]

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  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

[Hol-info] How to transform the proof form

[Ada]

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