numeral syntax: clarify parse trees vs. actual terms;
authorwenzelm
Thu Feb 11 22:06:37 2010 +0100 (2010-02-11)
changeset 35112ff6f60e6ab85
parent 35111 18cd034922ba
child 35113 1a0c129bb2e0
numeral syntax: clarify parse trees vs. actual terms;
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
src/ZF/Bin.thy
src/ZF/Induct/Multiset.thy
src/ZF/List_ZF.thy
src/ZF/OrdQuant.thy
src/ZF/Tools/numeral_syntax.ML
src/ZF/UNITY/Union.thy
src/ZF/ZF.thy
src/ZF/int_arith.ML
     1.1 --- a/src/ZF/Bin.thy	Thu Feb 11 22:03:37 2010 +0100
     1.2 +++ b/src/ZF/Bin.thy	Thu Feb 11 22:06:37 2010 +0100
     1.3 @@ -26,11 +26,6 @@
     1.4          | Min
     1.5          | Bit ("w: bin", "b: bool")     (infixl "BIT" 90)
     1.6  
     1.7 -use "Tools/numeral_syntax.ML"
     1.8 -
     1.9 -syntax
    1.10 -  "_Int"    :: "xnum => i"        ("_")
    1.11 -
    1.12  consts
    1.13    integ_of  :: "i=>i"
    1.14    NCons     :: "[i,i]=>i"
    1.15 @@ -106,6 +101,10 @@
    1.16      "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
    1.17                                   NCons(bin_mult(v,w),0))"
    1.18  
    1.19 +syntax
    1.20 +  "_Int"    :: "xnum => i"        ("_")
    1.21 +
    1.22 +use "Tools/numeral_syntax.ML"
    1.23  setup NumeralSyntax.setup
    1.24  
    1.25  
     2.1 --- a/src/ZF/Induct/Multiset.thy	Thu Feb 11 22:03:37 2010 +0100
     2.2 +++ b/src/ZF/Induct/Multiset.thy	Thu Feb 11 22:06:37 2010 +0100
     2.3 @@ -74,9 +74,9 @@
     2.4    "a :# M == a \<in> mset_of(M)"
     2.5  
     2.6  syntax
     2.7 -  "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
     2.8 +  "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
     2.9  syntax (xsymbols)
    2.10 -  "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
    2.11 +  "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
    2.12  translations
    2.13    "{#x \<in> M. P#}" == "CONST MCollect(M, %x. P)"
    2.14  
     3.1 --- a/src/ZF/List_ZF.thy	Thu Feb 11 22:03:37 2010 +0100
     3.2 +++ b/src/ZF/List_ZF.thy	Thu Feb 11 22:06:37 2010 +0100
     3.3 @@ -16,7 +16,7 @@
     3.4  
     3.5  syntax
     3.6   "[]"        :: i                                       ("[]")
     3.7 - "@List"     :: "is => i"                                 ("[(_)]")
     3.8 + "_List"     :: "is => i"                                 ("[(_)]")
     3.9  
    3.10  translations
    3.11    "[x, xs]"     == "CONST Cons(x, [xs])"
     4.1 --- a/src/ZF/OrdQuant.thy	Thu Feb 11 22:03:37 2010 +0100
     4.2 +++ b/src/ZF/OrdQuant.thy	Thu Feb 11 22:06:37 2010 +0100
     4.3 @@ -23,9 +23,9 @@
     4.4      "OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
     4.5  
     4.6  syntax
     4.7 -  "@oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
     4.8 -  "@oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
     4.9 -  "@OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
    4.10 +  "_oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
    4.11 +  "_oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
    4.12 +  "_OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
    4.13  
    4.14  translations
    4.15    "ALL x<a. P"  == "CONST oall(a, %x. P)"
    4.16 @@ -33,13 +33,13 @@
    4.17    "UN x<a. B"   == "CONST OUnion(a, %x. B)"
    4.18  
    4.19  syntax (xsymbols)
    4.20 -  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    4.21 -  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    4.22 -  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    4.23 +  "_oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    4.24 +  "_oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    4.25 +  "_OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    4.26  syntax (HTML output)
    4.27 -  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    4.28 -  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    4.29 -  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    4.30 +  "_oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    4.31 +  "_oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
    4.32 +  "_OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
    4.33  
    4.34  
    4.35  subsubsection {*simplification of the new quantifiers*}
    4.36 @@ -203,15 +203,15 @@
    4.37      "rex(M, P) == EX x. M(x) & P(x)"
    4.38  
    4.39  syntax
    4.40 -  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3ALL _[_]./ _)" 10)
    4.41 -  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3EX _[_]./ _)" 10)
    4.42 +  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3ALL _[_]./ _)" 10)
    4.43 +  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3EX _[_]./ _)" 10)
    4.44  
    4.45  syntax (xsymbols)
    4.46 -  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
    4.47 -  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
    4.48 +  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
    4.49 +  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
    4.50  syntax (HTML output)
    4.51 -  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
    4.52 -  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
    4.53 +  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
    4.54 +  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
    4.55  
    4.56  translations
    4.57    "ALL x[M]. P"  == "CONST rall(M, %x. P)"
     5.1 --- a/src/ZF/Tools/numeral_syntax.ML	Thu Feb 11 22:03:37 2010 +0100
     5.2 +++ b/src/ZF/Tools/numeral_syntax.ML	Thu Feb 11 22:06:37 2010 +0100
     5.3 @@ -7,92 +7,83 @@
     5.4  
     5.5  signature NUMERAL_SYNTAX =
     5.6  sig
     5.7 -  val dest_bin : term -> int
     5.8 -  val mk_bin   : int -> term
     5.9 -  val int_tr   : term list -> term
    5.10 -  val int_tr'  : bool -> typ -> term list -> term
    5.11 -  val setup    : theory -> theory
    5.12 +  val make_binary: int -> int list
    5.13 +  val dest_binary: int list -> int
    5.14 +  val int_tr: term list -> term
    5.15 +  val int_tr': bool -> typ -> term list -> term
    5.16 +  val setup: theory -> theory
    5.17  end;
    5.18  
    5.19  structure NumeralSyntax: NUMERAL_SYNTAX =
    5.20  struct
    5.21  
    5.22 -(* Bits *)
    5.23 +(* bits *)
    5.24  
    5.25 -fun mk_bit 0 = @{term "0"}
    5.26 -  | mk_bit 1 = @{term "succ(0)"}
    5.27 +fun mk_bit 0 = Syntax.const @{const_syntax "0"}
    5.28 +  | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
    5.29    | mk_bit _ = sys_error "mk_bit";
    5.30  
    5.31 -fun dest_bit (Const (@{const_name "0"}, _)) = 0
    5.32 -  | dest_bit (Const (@{const_name succ}, _) $ Const (@{const_name "0"}, _)) = 1
    5.33 +fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
    5.34 +  | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
    5.35    | dest_bit _ = raise Match;
    5.36  
    5.37  
    5.38 -(* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
    5.39 +(* bit strings *)
    5.40 +
    5.41 +fun make_binary 0 = []
    5.42 +  | make_binary ~1 = [~1]
    5.43 +  | make_binary n = (n mod 2) :: make_binary (n div 2);
    5.44  
    5.45 +fun dest_binary [] = 0
    5.46 +  | dest_binary (b :: bs) = b + 2 * dest_binary bs;
    5.47 +
    5.48 +
    5.49 +(*try to handle superfluous leading digits nicely*)
    5.50  fun prefix_len _ [] = 0
    5.51    | prefix_len pred (x :: xs) =
    5.52        if pred x then 1 + prefix_len pred xs else 0;
    5.53  
    5.54  fun mk_bin i =
    5.55 -  let fun bin_of_int 0  = []
    5.56 -        | bin_of_int ~1 = [~1]
    5.57 -        | bin_of_int n  = (n mod 2) :: bin_of_int (n div 2);
    5.58 -
    5.59 -      fun term_of [] = @{const Pls}
    5.60 -            | term_of [~1] = @{const Min}
    5.61 -            | term_of (b :: bs) = @{const Bit} $ term_of bs $ mk_bit b;
    5.62 -  in
    5.63 -    term_of (bin_of_int i)
    5.64 -  end;
    5.65 +  let
    5.66 +    fun term_of [] = Syntax.const @{const_syntax Pls}
    5.67 +      | term_of [~1] = Syntax.const @{const_syntax Min}
    5.68 +      | term_of (b :: bs) = Syntax.const @{const_syntax Bit} $ term_of bs $ mk_bit b;
    5.69 +  in term_of (make_binary i) end;
    5.70  
    5.71 -(*we consider all "spellings", since they could vary depending on the caller*)
    5.72 -fun bin_of (Const ("Pls", _)) = []
    5.73 -  | bin_of (Const ("bin.Pls", _)) = []
    5.74 -  | bin_of (Const ("Bin.bin.Pls", _)) = []
    5.75 -  | bin_of (Const ("Min", _)) = [~1]
    5.76 -  | bin_of (Const ("bin.Min", _)) = [~1]
    5.77 -  | bin_of (Const ("Bin.bin.Min", _)) = [~1]
    5.78 -  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    5.79 -  | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    5.80 -  | bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    5.81 +fun bin_of (Const (@{const_syntax Pls}, _)) = []
    5.82 +  | bin_of (Const (@{const_syntax Min}, _)) = [~1]
    5.83 +  | bin_of (Const (@{const_syntax Bit}, _) $ bs $ b) = dest_bit b :: bin_of bs
    5.84    | bin_of _ = raise Match;
    5.85  
    5.86 -(*Convert a list of bits to an integer*)
    5.87 -fun integ_of [] = 0
    5.88 -  | integ_of (b :: bs) = b + 2 * integ_of bs;
    5.89 -
    5.90 -val dest_bin = integ_of o bin_of;
    5.91 -
    5.92 -(*leading 0s and (for negative numbers) -1s cause complications, though they 
    5.93 +(*Leading 0s and (for negative numbers) -1s cause complications, though they 
    5.94    should never arise in normal use. The formalization used in HOL prevents 
    5.95    them altogether.*)
    5.96  fun show_int t =
    5.97    let
    5.98      val rev_digs = bin_of t;
    5.99      val (sign, zs) =
   5.100 -        (case rev rev_digs of
   5.101 -             ~1 :: bs => ("-", prefix_len (equal 1) bs)
   5.102 -           | bs =>       ("",  prefix_len (equal 0) bs));
   5.103 -    val num = string_of_int (abs (integ_of rev_digs));
   5.104 +      (case rev rev_digs of
   5.105 +         ~1 :: bs => ("-", prefix_len (equal 1) bs)
   5.106 +      | bs => ("",  prefix_len (equal 0) bs));
   5.107 +    val num = string_of_int (abs (dest_binary rev_digs));
   5.108    in
   5.109      "#" ^ sign ^ implode (replicate zs "0") ^ num
   5.110    end;
   5.111  
   5.112  
   5.113 -
   5.114  (* translation of integer constant tokens to and from binary *)
   5.115  
   5.116  fun int_tr (*"_Int"*) [t as Free (str, _)] =
   5.117 -      Syntax.const "integ_of" $ mk_bin (#value (Syntax.read_xnum str))
   5.118 +      Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str))
   5.119    | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
   5.120  
   5.121 -fun int_tr' _ _ (*"integ_of"*) [t] = Syntax.const "_Int" $ Syntax.free (show_int t)
   5.122 -  | int_tr' (_:bool) (_:typ)     _ = raise Match;
   5.123 +fun int_tr' _ _ (*"integ_of"*) [t] =
   5.124 +      Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)
   5.125 +  | int_tr' (_: bool) (_: typ) _ = raise Match;
   5.126  
   5.127  
   5.128  val setup =
   5.129 - (Sign.add_trfuns ([], [("_Int", int_tr)], [], []) #>
   5.130 -  Sign.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
   5.131 + (Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [], []) #>
   5.132 +  Sign.add_trfunsT [(@{const_syntax integ_of}, int_tr')]);
   5.133  
   5.134  end;
     6.1 --- a/src/ZF/UNITY/Union.thy	Thu Feb 11 22:03:37 2010 +0100
     6.2 +++ b/src/ZF/UNITY/Union.thy	Thu Feb 11 22:06:37 2010 +0100
     6.3 @@ -41,8 +41,8 @@
     6.4        SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
     6.5    
     6.6  syntax
     6.7 -  "@JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
     6.8 -  "@JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
     6.9 +  "_JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
    6.10 +  "_JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
    6.11  
    6.12  translations
    6.13    "JN x:A. B"   == "CONST JOIN(A, (%x. B))"
    6.14 @@ -54,8 +54,8 @@
    6.15    Join  (infixl "\<squnion>" 65)
    6.16  
    6.17  syntax (xsymbols)
    6.18 -  "@JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
    6.19 -  "@JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
    6.20 +  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
    6.21 +  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
    6.22  
    6.23  
    6.24  subsection{*SKIP*}
     7.1 --- a/src/ZF/ZF.thy	Thu Feb 11 22:03:37 2010 +0100
     7.2 +++ b/src/ZF/ZF.thy	Thu Feb 11 22:06:37 2010 +0100
     7.3 @@ -105,26 +105,26 @@
     7.4  
     7.5  syntax
     7.6    ""          :: "i => is"                   ("_")
     7.7 -  "@Enum"     :: "[i, is] => is"             ("_,/ _")
     7.8 +  "_Enum"     :: "[i, is] => is"             ("_,/ _")
     7.9  
    7.10 -  "@Finset"   :: "is => i"                   ("{(_)}")
    7.11 -  "@Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
    7.12 -  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
    7.13 -  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
    7.14 -  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
    7.15 -  "@INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
    7.16 -  "@UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
    7.17 -  "@PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
    7.18 -  "@SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
    7.19 -  "@lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
    7.20 -  "@Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
    7.21 -  "@Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
    7.22 +  "_Finset"   :: "is => i"                   ("{(_)}")
    7.23 +  "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
    7.24 +  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
    7.25 +  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
    7.26 +  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
    7.27 +  "_INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
    7.28 +  "_UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
    7.29 +  "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
    7.30 +  "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
    7.31 +  "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
    7.32 +  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
    7.33 +  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
    7.34  
    7.35    (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
    7.36  
    7.37 -  "@pattern"  :: "patterns => pttrn"         ("<_>")
    7.38 +  "_pattern"  :: "patterns => pttrn"         ("<_>")
    7.39    ""          :: "pttrn => patterns"         ("_")
    7.40 -  "@patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
    7.41 +  "_patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
    7.42  
    7.43  translations
    7.44    "{x, xs}"     == "CONST cons(x, {xs})"
    7.45 @@ -158,18 +158,18 @@
    7.46    Inter           ("\<Inter>_" [90] 90)
    7.47  
    7.48  syntax (xsymbols)
    7.49 -  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
    7.50 -  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
    7.51 -  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
    7.52 -  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
    7.53 -  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
    7.54 -  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
    7.55 -  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
    7.56 -  "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
    7.57 -  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
    7.58 -  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
    7.59 -  "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
    7.60 -  "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
    7.61 +  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
    7.62 +  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
    7.63 +  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
    7.64 +  "_UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
    7.65 +  "_INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
    7.66 +  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
    7.67 +  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
    7.68 +  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
    7.69 +  "_Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
    7.70 +  "_Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
    7.71 +  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
    7.72 +  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
    7.73  
    7.74  notation (HTML output)
    7.75    cart_prod       (infixr "\<times>" 80) and
    7.76 @@ -182,18 +182,18 @@
    7.77    Inter           ("\<Inter>_" [90] 90)
    7.78  
    7.79  syntax (HTML output)
    7.80 -  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
    7.81 -  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
    7.82 -  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
    7.83 -  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
    7.84 -  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
    7.85 -  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
    7.86 -  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
    7.87 -  "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
    7.88 -  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
    7.89 -  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
    7.90 -  "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
    7.91 -  "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
    7.92 +  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
    7.93 +  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
    7.94 +  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
    7.95 +  "_UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
    7.96 +  "_INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
    7.97 +  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
    7.98 +  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
    7.99 +  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
   7.100 +  "_Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
   7.101 +  "_Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
   7.102 +  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
   7.103 +  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
   7.104  
   7.105  
   7.106  finalconsts
     8.1 --- a/src/ZF/int_arith.ML	Thu Feb 11 22:03:37 2010 +0100
     8.2 +++ b/src/ZF/int_arith.ML	Thu Feb 11 22:06:37 2010 +0100
     8.3 @@ -7,15 +7,40 @@
     8.4  structure Int_Numeral_Simprocs =
     8.5  struct
     8.6  
     8.7 +(* abstract syntax operations *)
     8.8 +
     8.9 +fun mk_bit 0 = @{term "0"}
    8.10 +  | mk_bit 1 = @{term "succ(0)"}
    8.11 +  | mk_bit _ = sys_error "mk_bit";
    8.12 +
    8.13 +fun dest_bit @{term "0"} = 0
    8.14 +  | dest_bit @{term "succ(0)"} = 1
    8.15 +  | dest_bit _ = raise Match;
    8.16 +
    8.17 +fun mk_bin i =
    8.18 +  let
    8.19 +    fun term_of [] = @{term Pls}
    8.20 +      | term_of [~1] = @{term Min}
    8.21 +      | term_of (b :: bs) = @{term Bit} $ term_of bs $ mk_bit b;
    8.22 +  in term_of (NumeralSyntax.make_binary i) end;
    8.23 +
    8.24 +fun dest_bin tm =
    8.25 +  let
    8.26 +    fun bin_of @{term Pls} = []
    8.27 +      | bin_of @{term Min} = [~1]
    8.28 +      | bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs
    8.29 +      | bin_of _ = sys_error "dest_bin";
    8.30 +  in NumeralSyntax.dest_binary (bin_of tm) end;
    8.31 +
    8.32 +
    8.33  (*Utilities*)
    8.34  
    8.35 -fun mk_numeral n = @{const integ_of} $ NumeralSyntax.mk_bin n;
    8.36 +fun mk_numeral i = @{const integ_of} $ mk_bin i;
    8.37  
    8.38  (*Decodes a binary INTEGER*)
    8.39  fun dest_numeral (Const(@{const_name integ_of}, _) $ w) =
    8.40 -     (NumeralSyntax.dest_bin w
    8.41 -      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    8.42 -  | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    8.43 +     (dest_bin w handle SYS_ERROR _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    8.44 +  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    8.45  
    8.46  fun find_first_numeral past (t::terms) =
    8.47          ((dest_numeral t, rev past @ terms)