numeral syntax: clarify parse trees vs. actual terms;
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
--- a/src/ZF/Bin.thy Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/Bin.thy Thu Feb 11 22:06:37 2010 +0100
@@ -26,11 +26,6 @@
| Min
| Bit ("w: bin", "b: bool") (infixl "BIT" 90)
-use "Tools/numeral_syntax.ML"
-
-syntax
- "_Int" :: "xnum => i" ("_")
-
consts
integ_of :: "i=>i"
NCons :: "[i,i]=>i"
@@ -106,6 +101,10 @@
"bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
NCons(bin_mult(v,w),0))"
+syntax
+ "_Int" :: "xnum => i" ("_")
+
+use "Tools/numeral_syntax.ML"
setup NumeralSyntax.setup
--- a/src/ZF/Induct/Multiset.thy Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/Induct/Multiset.thy Thu Feb 11 22:06:37 2010 +0100
@@ -74,9 +74,9 @@
"a :# M == a \<in> mset_of(M)"
syntax
- "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
+ "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
syntax (xsymbols)
- "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
+ "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
translations
"{#x \<in> M. P#}" == "CONST MCollect(M, %x. P)"
--- a/src/ZF/List_ZF.thy Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/List_ZF.thy Thu Feb 11 22:06:37 2010 +0100
@@ -16,7 +16,7 @@
syntax
"[]" :: i ("[]")
- "@List" :: "is => i" ("[(_)]")
+ "_List" :: "is => i" ("[(_)]")
translations
"[x, xs]" == "CONST Cons(x, [xs])"
--- a/src/ZF/OrdQuant.thy Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/OrdQuant.thy Thu Feb 11 22:06:37 2010 +0100
@@ -23,9 +23,9 @@
"OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
syntax
- "@oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10)
- "@oex" :: "[idt, i, o] => o" ("(3EX _<_./ _)" 10)
- "@OUNION" :: "[idt, i, i] => i" ("(3UN _<_./ _)" 10)
+ "_oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10)
+ "_oex" :: "[idt, i, o] => o" ("(3EX _<_./ _)" 10)
+ "_OUNION" :: "[idt, i, i] => i" ("(3UN _<_./ _)" 10)
translations
"ALL x<a. P" == "CONST oall(a, %x. P)"
@@ -33,13 +33,13 @@
"UN x<a. B" == "CONST OUnion(a, %x. B)"
syntax (xsymbols)
- "@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
- "@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
- "@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
+ "_oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
+ "_oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
+ "_OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
syntax (HTML output)
- "@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
- "@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
- "@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
+ "_oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
+ "_oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
+ "_OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
subsubsection {*simplification of the new quantifiers*}
@@ -203,15 +203,15 @@
"rex(M, P) == EX x. M(x) & P(x)"
syntax
- "@rall" :: "[pttrn, i=>o, o] => o" ("(3ALL _[_]./ _)" 10)
- "@rex" :: "[pttrn, i=>o, o] => o" ("(3EX _[_]./ _)" 10)
+ "_rall" :: "[pttrn, i=>o, o] => o" ("(3ALL _[_]./ _)" 10)
+ "_rex" :: "[pttrn, i=>o, o] => o" ("(3EX _[_]./ _)" 10)
syntax (xsymbols)
- "@rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
- "@rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
+ "_rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
+ "_rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
syntax (HTML output)
- "@rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
- "@rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
+ "_rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
+ "_rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
translations
"ALL x[M]. P" == "CONST rall(M, %x. P)"
--- a/src/ZF/Tools/numeral_syntax.ML Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML Thu Feb 11 22:06:37 2010 +0100
@@ -7,92 +7,83 @@
signature NUMERAL_SYNTAX =
sig
- val dest_bin : term -> int
- val mk_bin : int -> term
- val int_tr : term list -> term
- val int_tr' : bool -> typ -> term list -> term
- val setup : theory -> theory
+ val make_binary: int -> int list
+ val dest_binary: int list -> int
+ val int_tr: term list -> term
+ val int_tr': bool -> typ -> term list -> term
+ val setup: theory -> theory
end;
structure NumeralSyntax: NUMERAL_SYNTAX =
struct
-(* Bits *)
+(* bits *)
-fun mk_bit 0 = @{term "0"}
- | mk_bit 1 = @{term "succ(0)"}
+fun mk_bit 0 = Syntax.const @{const_syntax "0"}
+ | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
| mk_bit _ = sys_error "mk_bit";
-fun dest_bit (Const (@{const_name "0"}, _)) = 0
- | dest_bit (Const (@{const_name succ}, _) $ Const (@{const_name "0"}, _)) = 1
+fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
+ | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
| dest_bit _ = raise Match;
-(* Bit strings *) (*we try to handle superfluous leading digits nicely*)
+(* bit strings *)
+
+fun make_binary 0 = []
+ | make_binary ~1 = [~1]
+ | make_binary n = (n mod 2) :: make_binary (n div 2);
+fun dest_binary [] = 0
+ | dest_binary (b :: bs) = b + 2 * dest_binary bs;
+
+
+(*try to handle superfluous leading digits nicely*)
fun prefix_len _ [] = 0
| prefix_len pred (x :: xs) =
if pred x then 1 + prefix_len pred xs else 0;
fun mk_bin i =
- let fun bin_of_int 0 = []
- | bin_of_int ~1 = [~1]
- | bin_of_int n = (n mod 2) :: bin_of_int (n div 2);
-
- fun term_of [] = @{const Pls}
- | term_of [~1] = @{const Min}
- | term_of (b :: bs) = @{const Bit} $ term_of bs $ mk_bit b;
- in
- term_of (bin_of_int i)
- end;
+ let
+ fun term_of [] = Syntax.const @{const_syntax Pls}
+ | term_of [~1] = Syntax.const @{const_syntax Min}
+ | term_of (b :: bs) = Syntax.const @{const_syntax Bit} $ term_of bs $ mk_bit b;
+ in term_of (make_binary i) end;
-(*we consider all "spellings", since they could vary depending on the caller*)
-fun bin_of (Const ("Pls", _)) = []
- | bin_of (Const ("bin.Pls", _)) = []
- | bin_of (Const ("Bin.bin.Pls", _)) = []
- | bin_of (Const ("Min", _)) = [~1]
- | bin_of (Const ("bin.Min", _)) = [~1]
- | bin_of (Const ("Bin.bin.Min", _)) = [~1]
- | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
- | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
- | bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+fun bin_of (Const (@{const_syntax Pls}, _)) = []
+ | bin_of (Const (@{const_syntax Min}, _)) = [~1]
+ | bin_of (Const (@{const_syntax Bit}, _) $ bs $ b) = dest_bit b :: bin_of bs
| bin_of _ = raise Match;
-(*Convert a list of bits to an integer*)
-fun integ_of [] = 0
- | integ_of (b :: bs) = b + 2 * integ_of bs;
-
-val dest_bin = integ_of o bin_of;
-
-(*leading 0s and (for negative numbers) -1s cause complications, though they
+(*Leading 0s and (for negative numbers) -1s cause complications, though they
should never arise in normal use. The formalization used in HOL prevents
them altogether.*)
fun show_int t =
let
val rev_digs = bin_of t;
val (sign, zs) =
- (case rev rev_digs of
- ~1 :: bs => ("-", prefix_len (equal 1) bs)
- | bs => ("", prefix_len (equal 0) bs));
- val num = string_of_int (abs (integ_of rev_digs));
+ (case rev rev_digs of
+ ~1 :: bs => ("-", prefix_len (equal 1) bs)
+ | bs => ("", prefix_len (equal 0) bs));
+ val num = string_of_int (abs (dest_binary rev_digs));
in
"#" ^ sign ^ implode (replicate zs "0") ^ num
end;
-
(* translation of integer constant tokens to and from binary *)
fun int_tr (*"_Int"*) [t as Free (str, _)] =
- Syntax.const "integ_of" $ mk_bin (#value (Syntax.read_xnum str))
+ Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str))
| int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
-fun int_tr' _ _ (*"integ_of"*) [t] = Syntax.const "_Int" $ Syntax.free (show_int t)
- | int_tr' (_:bool) (_:typ) _ = raise Match;
+fun int_tr' _ _ (*"integ_of"*) [t] =
+ Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)
+ | int_tr' (_: bool) (_: typ) _ = raise Match;
val setup =
- (Sign.add_trfuns ([], [("_Int", int_tr)], [], []) #>
- Sign.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
+ (Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [], []) #>
+ Sign.add_trfunsT [(@{const_syntax integ_of}, int_tr')]);
end;
--- a/src/ZF/UNITY/Union.thy Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/UNITY/Union.thy Thu Feb 11 22:06:37 2010 +0100
@@ -41,8 +41,8 @@
SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
syntax
- "@JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10)
- "@JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10)
+ "_JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10)
+ "_JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10)
translations
"JN x:A. B" == "CONST JOIN(A, (%x. B))"
@@ -54,8 +54,8 @@
Join (infixl "\<squnion>" 65)
syntax (xsymbols)
- "@JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10)
- "@JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10)
+ "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10)
+ "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10)
subsection{*SKIP*}
--- a/src/ZF/ZF.thy Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/ZF.thy Thu Feb 11 22:06:37 2010 +0100
@@ -105,26 +105,26 @@
syntax
"" :: "i => is" ("_")
- "@Enum" :: "[i, is] => is" ("_,/ _")
+ "_Enum" :: "[i, is] => is" ("_,/ _")
- "@Finset" :: "is => i" ("{(_)}")
- "@Tuple" :: "[i, is] => i" ("<(_,/ _)>")
- "@Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})")
- "@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
- "@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51])
- "@INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10)
- "@UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10)
- "@PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10)
- "@SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10)
- "@lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10)
- "@Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10)
- "@Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10)
+ "_Finset" :: "is => i" ("{(_)}")
+ "_Tuple" :: "[i, is] => i" ("<(_,/ _)>")
+ "_Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})")
+ "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
+ "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51])
+ "_INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10)
+ "_UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10)
+ "_PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10)
+ "_SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10)
+ "_lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10)
+ "_Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10)
+ "_Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10)
(** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
- "@pattern" :: "patterns => pttrn" ("<_>")
+ "_pattern" :: "patterns => pttrn" ("<_>")
"" :: "pttrn => patterns" ("_")
- "@patterns" :: "[pttrn, patterns] => patterns" ("_,/_")
+ "_patterns" :: "[pttrn, patterns] => patterns" ("_,/_")
translations
"{x, xs}" == "CONST cons(x, {xs})"
@@ -158,18 +158,18 @@
Inter ("\<Inter>_" [90] 90)
syntax (xsymbols)
- "@Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})")
- "@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
- "@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51])
- "@UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10)
- "@INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10)
- "@PROD" :: "[pttrn, i, i] => i" ("(3\<Pi>_\<in>_./ _)" 10)
- "@SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<in>_./ _)" 10)
- "@lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10)
- "@Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10)
- "@Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10)
- "@Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
- "@pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
+ "_Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})")
+ "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
+ "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51])
+ "_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10)
+ "_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10)
+ "_PROD" :: "[pttrn, i, i] => i" ("(3\<Pi>_\<in>_./ _)" 10)
+ "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<in>_./ _)" 10)
+ "_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10)
+ "_Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10)
+ "_Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10)
+ "_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
+ "_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
notation (HTML output)
cart_prod (infixr "\<times>" 80) and
@@ -182,18 +182,18 @@
Inter ("\<Inter>_" [90] 90)
syntax (HTML output)
- "@Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})")
- "@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
- "@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51])
- "@UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10)
- "@INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10)
- "@PROD" :: "[pttrn, i, i] => i" ("(3\<Pi>_\<in>_./ _)" 10)
- "@SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<in>_./ _)" 10)
- "@lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10)
- "@Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10)
- "@Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10)
- "@Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
- "@pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
+ "_Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})")
+ "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
+ "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51])
+ "_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10)
+ "_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10)
+ "_PROD" :: "[pttrn, i, i] => i" ("(3\<Pi>_\<in>_./ _)" 10)
+ "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma>_\<in>_./ _)" 10)
+ "_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10)
+ "_Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10)
+ "_Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10)
+ "_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
+ "_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
finalconsts
--- a/src/ZF/int_arith.ML Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/int_arith.ML Thu Feb 11 22:06:37 2010 +0100
@@ -7,15 +7,40 @@
structure Int_Numeral_Simprocs =
struct
+(* abstract syntax operations *)
+
+fun mk_bit 0 = @{term "0"}
+ | mk_bit 1 = @{term "succ(0)"}
+ | mk_bit _ = sys_error "mk_bit";
+
+fun dest_bit @{term "0"} = 0
+ | dest_bit @{term "succ(0)"} = 1
+ | dest_bit _ = raise Match;
+
+fun mk_bin i =
+ let
+ fun term_of [] = @{term Pls}
+ | term_of [~1] = @{term Min}
+ | term_of (b :: bs) = @{term Bit} $ term_of bs $ mk_bit b;
+ in term_of (NumeralSyntax.make_binary i) end;
+
+fun dest_bin tm =
+ let
+ fun bin_of @{term Pls} = []
+ | bin_of @{term Min} = [~1]
+ | bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs
+ | bin_of _ = sys_error "dest_bin";
+ in NumeralSyntax.dest_binary (bin_of tm) end;
+
+
(*Utilities*)
-fun mk_numeral n = @{const integ_of} $ NumeralSyntax.mk_bin n;
+fun mk_numeral i = @{const integ_of} $ mk_bin i;
(*Decodes a binary INTEGER*)
fun dest_numeral (Const(@{const_name integ_of}, _) $ w) =
- (NumeralSyntax.dest_bin w
- handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
- | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
+ (dest_bin w handle SYS_ERROR _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
+ | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
fun find_first_numeral past (t::terms) =
((dest_numeral t, rev past @ terms)