added Numeral.thy, Tools/numeral_syntax.ML;
authorwenzelm
Tue Jul 06 21:08:30 1999 +0200 (1999-07-06)
changeset 69059bc05ec3497b
parent 6904 4125d6b6d8f9
child 6906 46652582f831
added Numeral.thy, Tools/numeral_syntax.ML;
src/HOL/IsaMakefile
src/HOL/Numeral.thy
src/HOL/Tools/numeral_syntax.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Jul 06 21:06:51 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jul 06 21:08:30 1999 +0200
     1.3 @@ -31,9 +31,9 @@
     1.4  Pure:
     1.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     1.6  
     1.7 -$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \
     1.8 -  $(SRC)/Provers/Arith/fast_lin_arith.ML	\
     1.9 -  $(SRC)/Provers/Arith/abel_cancel.ML $(SRC)/Provers/blast.ML \
    1.10 +$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
    1.11 +  $(SRC)/Provers/Arith/cancel_sums.ML		\
    1.12 +  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
    1.13    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    1.14    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
    1.15    $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
    1.16 @@ -49,18 +49,19 @@
    1.17    Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \
    1.18    Integ/Int.thy Integ/simproc.ML Lfp.ML Lfp.thy List.ML List.thy \
    1.19    Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \
    1.20 -  Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy Prod.ML \
    1.21 -  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
    1.22 +  Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy \
    1.23 +  Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
    1.24    Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
    1.25    Sum.ML Sum.thy Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
    1.26    Tools/datatype_package.ML Tools/datatype_prop.ML \
    1.27    Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
    1.28 -  Tools/inductive_package.ML Tools/primrec_package.ML \
    1.29 -  Tools/recdef_package.ML Tools/record_package.ML \
    1.30 -  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
    1.31 -  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy cladata.ML \
    1.32 -  equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML \
    1.33 -  subset.ML subset.thy thy_syntax.ML
    1.34 +  Tools/inductive_package.ML Tools/numeral_syntax.ML \
    1.35 +  Tools/primrec_package.ML Tools/recdef_package.ML \
    1.36 +  Tools/record_package.ML Tools/typedef_package.ML Trancl.ML \
    1.37 +  Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML WF.thy \
    1.38 +  WF_Rel.ML WF_Rel.thy cladata.ML equalities.ML equalities.thy \
    1.39 +  hologic.ML mono.ML mono.thy simpdata.ML subset.ML subset.thy \
    1.40 +  thy_syntax.ML
    1.41  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
    1.42  
    1.43  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Numeral.thy	Tue Jul 06 21:08:30 1999 +0200
     2.3 @@ -0,0 +1,28 @@
     2.4 +(*  Title:      HOL/Numeral.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Larry Paulson and Markus Wenzel
     2.7 +
     2.8 +Generic numerals represented as twos-complement bitstrings.
     2.9 +*)
    2.10 +
    2.11 +theory Numeral = Datatype
    2.12 +files "Tools/numeral_syntax.ML":;
    2.13 +
    2.14 +datatype
    2.15 +  bin = Pls
    2.16 +      | Min
    2.17 +      | Bit bin bool	(infixl "BIT" 90);
    2.18 +
    2.19 +axclass
    2.20 +  numeral < "term";
    2.21 +
    2.22 +consts
    2.23 +  number_of :: "bin => 'a::numeral";
    2.24 +
    2.25 +syntax
    2.26 +  "_Numeral" :: "xnum => 'a"	("_");
    2.27 +
    2.28 +setup NumeralSyntax.setup;
    2.29 +
    2.30 +
    2.31 +end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Jul 06 21:08:30 1999 +0200
     3.3 @@ -0,0 +1,103 @@
     3.4 +(*  Title:      HOL/Tools/numeral_syntax.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Markus Wenzel, TU Muenchen
     3.7 +
     3.8 +Concrete syntax for generic numerals.  Assumes consts and syntax of
     3.9 +theory HOL/Numeral.
    3.10 +*)
    3.11 +
    3.12 +signature NUMERAL_SYNTAX =
    3.13 +sig
    3.14 +  val dest_bin: term -> int
    3.15 +  val setup: (theory -> theory) list
    3.16 +end;
    3.17 +
    3.18 +structure NumeralSyntax: NUMERAL_SYNTAX =
    3.19 +struct
    3.20 +
    3.21 +
    3.22 +(* bits *)
    3.23 +
    3.24 +fun mk_bit 0 = Syntax.const "False"
    3.25 +  | mk_bit 1 = Syntax.const "True"
    3.26 +  | mk_bit _ = sys_error "mk_bit";
    3.27 +
    3.28 +fun dest_bit (Const ("False", _)) = 0
    3.29 +  | dest_bit (Const ("True", _)) = 1
    3.30 +  | dest_bit _ = raise Match;
    3.31 +
    3.32 +
    3.33 +(* bit strings *)   (*we try to handle superfluous leading digits nicely*)
    3.34 +
    3.35 +fun prefix_len _ [] = 0
    3.36 +  | prefix_len pred (x :: xs) =
    3.37 +      if pred x then 1 + prefix_len pred xs else 0;
    3.38 +
    3.39 +fun mk_bin str =
    3.40 +  let
    3.41 +    val (sign, digs) =
    3.42 +      (case Symbol.explode str of
    3.43 +        "#" :: "-" :: cs => (~1, cs)
    3.44 +      | "#" :: cs => (1, cs)
    3.45 +      | _ => raise ERROR);
    3.46 +
    3.47 +    fun bin_of 0  = []
    3.48 +      | bin_of ~1 = [~1]
    3.49 +      | bin_of n  = (n mod 2) :: bin_of (n div 2);
    3.50 +
    3.51 +    fun term_of []   = Syntax.const "Numeral.bin.Pls"
    3.52 +      | term_of [~1] = Syntax.const "Numeral.bin.Min"
    3.53 +      | term_of (b :: bs) = Syntax.const "Numeral.bin.Bit" $ term_of bs $ mk_bit b;
    3.54 +    in term_of (bin_of (sign * (#1 (Term.read_int digs)))) end;
    3.55 +
    3.56 +(*we consider all "spellings"; Min is likely to be declared elsewhere*)
    3.57 +fun bin_of (Const ("Pls", _)) = []
    3.58 +  | bin_of (Const ("bin.Pls", _)) = []
    3.59 +  | bin_of (Const ("Numeral.bin.Pls", _)) = []
    3.60 +  | bin_of (Const ("Min", _)) = [~1]
    3.61 +  | bin_of (Const ("bin.Min", _)) = [~1]
    3.62 +  | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
    3.63 +  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    3.64 +  | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    3.65 +  | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    3.66 +  | bin_of _ = raise Match;
    3.67 +
    3.68 +fun int_of [] = 0
    3.69 +  | int_of (b :: bs) = b + 2 * int_of bs;
    3.70 +
    3.71 +val dest_bin = int_of o bin_of;
    3.72 +
    3.73 +fun dest_bin_str tm =
    3.74 +  let
    3.75 +    val rev_digs = bin_of tm;
    3.76 +    val (sign, zs) =
    3.77 +      (case rev rev_digs of
    3.78 +        ~1 :: bs => ("-", prefix_len (equal 1) bs)
    3.79 +      | bs => ("", prefix_len (equal 0) bs));
    3.80 +    val num = string_of_int (abs (int_of rev_digs));
    3.81 +  in "#" ^ sign ^ implode (replicate zs "0") ^ num end;
    3.82 +
    3.83 +
    3.84 +(* translation of integer numeral tokens to and from bitstrings *)
    3.85 +
    3.86 +fun numeral_tr (*"_Numeral"*) [t as Free (str, _)] =
    3.87 +      (Syntax.const "Numeral.number_of" $
    3.88 +        (mk_bin str handle ERROR => raise TERM ("numeral_tr", [t])))
    3.89 +  | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    3.90 +
    3.91 +fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    3.92 +      let val t' = Syntax.const "_Numeral" $ (Syntax.const "_xnum" $ Syntax.free (dest_bin_str t)) in
    3.93 +        if can Term.dest_Type T then t'
    3.94 +        else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
    3.95 +      end
    3.96 +  | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    3.97 +
    3.98 +
    3.99 +(* theory setup *)
   3.100 +
   3.101 +val setup =
   3.102 + [Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
   3.103 +  Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
   3.104 +
   3.105 +
   3.106 +end;