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
