HOL
HOL copied to clipboard
HOL-Theorem-Prover
Update Definition syntaxes to allow declaration of types of new constants
One possibility
Definition foo_def:
(** constname1 : type1 *)
(** constname2 : type2 *)
...
End
multiDefine will support lists of definitions, so the proposed syntax could be more liberal.
On Wed, Oct 26, 2022 at 4:39 AM Michael Norrish @.***> wrote:
One possibility
Definition foo_def: (** constname1 : type1 ) (* constname2 : type2 *) ... End
— Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/1065, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOAD3755WCNHPSFGM7O5DWFD33RANCNFSM6AAAAAAROZTGNE . You are receiving this because you are subscribed to this thread.Message ID: @.***>
It also supports prim. rec defns. in the list:
TotalDefn.multiDefine
(f2 0 = 3) /\ (f2 (SUC n) = 1 + f2 n) /\ (f3 0 = f2 0) /\ (f3 (SUC n) = f2 n + f2 n) /\ (f4 x = f2 x + f3 (f2 x));
On Wed, Oct 26, 2022 at 1:59 PM Konrad Slind @.***> wrote:
multiDefine will support lists of definitions, so the proposed syntax could be more liberal.
On Wed, Oct 26, 2022 at 4:39 AM Michael Norrish @.***> wrote:
One possibility
Definition foo_def: (** constname1 : type1 ) (* constname2 : type2 *) ... End
— Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/1065, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOAD3755WCNHPSFGM7O5DWFD33RANCNFSM6AAAAAAROZTGNE . You are receiving this because you are subscribed to this thread.Message ID: @.***>
And it supports wfrec defns when the auto-prover manages to solve the termination problem:
TotalDefn.multiDefine
(f5 n = if n = 0n then 1 else n * f5 (n-1)) /\ (f6 [] = [] /\ f6 [[x]] = [x] /\ f6 (h::t) = h ++ f6 t);
On Wed, Oct 26, 2022 at 2:05 PM Konrad Slind @.***> wrote:
It also supports prim. rec defns. in the list:
TotalDefn.multiDefine
(f2 0 = 3) /\ (f2 (SUC n) = 1 + f2 n) /\ (f3 0 = f2 0) /\ (f3 (SUC n) = f2 n + f2 n) /\ (f4 x = f2 x + f3 (f2 x));On Wed, Oct 26, 2022 at 1:59 PM Konrad Slind @.***> wrote:
multiDefine will support lists of definitions, so the proposed syntax could be more liberal.
On Wed, Oct 26, 2022 at 4:39 AM Michael Norrish @.***> wrote:
One possibility
Definition foo_def: (** constname1 : type1 ) (* constname2 : type2 *) ... End
— Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/1065, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOAD3755WCNHPSFGM7O5DWFD33RANCNFSM6AAAAAAROZTGNE . You are receiving this because you are subscribed to this thread.Message ID: @.***>
And there is elaborate clique-finding etc so the order of the declarations doesn't matter. See
https://github.com/HOL-Theorem-Prover/HOL/blob/2eff78b608efb12cbea315f4813b4f4af70793a0/src/tfl/src/Defn.sml#L1825
for where that stuff is implemented. It might be too elaborate ... I thought it was a good idea at the time.
Konrad.
On Wed, Oct 26, 2022 at 2:08 PM Konrad Slind @.***> wrote:
And it supports wfrec defns when the auto-prover manages to solve the termination problem:
TotalDefn.multiDefine
(f5 n = if n = 0n then 1 else n * f5 (n-1)) /\ (f6 [] = [] /\ f6 [[x]] = [x] /\ f6 (h::t) = h ++ f6 t);On Wed, Oct 26, 2022 at 2:05 PM Konrad Slind @.***> wrote:
It also supports prim. rec defns. in the list:
TotalDefn.multiDefine
(f2 0 = 3) /\ (f2 (SUC n) = 1 + f2 n) /\ (f3 0 = f2 0) /\ (f3 (SUC n) = f2 n + f2 n) /\ (f4 x = f2 x + f3 (f2 x));On Wed, Oct 26, 2022 at 1:59 PM Konrad Slind @.***> wrote:
multiDefine will support lists of definitions, so the proposed syntax could be more liberal.
On Wed, Oct 26, 2022 at 4:39 AM Michael Norrish < @.***> wrote:
One possibility
Definition foo_def: (** constname1 : type1 ) (* constname2 : type2 *) ... End
— Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/1065, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOAD3755WCNHPSFGM7O5DWFD33RANCNFSM6AAAAAAROZTGNE . You are receiving this because you are subscribed to this thread.Message ID: @.***>