moved mk_bin from Numerals to HOLogic
authornipkow
Mon Dec 18 14:59:05 2000 +0100 (2000-12-18)
changeset 106939e4a0e84d0d6
parent 10692 6077fd933575
child 10694 9a5d5df29e5c
moved mk_bin from Numerals to HOLogic
first steps towards rational lin arith
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/nat_bin.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Real/RealBin.ML
src/HOL/Real/real_arith.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/arith_data.ML
src/HOL/hologic.ML
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Mon Dec 18 14:57:58 2000 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Mon Dec 18 14:59:05 2000 +0100
     1.3 @@ -79,8 +79,7 @@
     1.4  
     1.5  (*Utilities*)
     1.6  
     1.7 -fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ 
     1.8 -                   NumeralSyntax.mk_bin n;
     1.9 +fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ HOLogic.mk_bin n;
    1.10  
    1.11  (*Decodes a binary INTEGER*)
    1.12  fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
    1.13 @@ -416,8 +415,9 @@
    1.14  in
    1.15  
    1.16  val int_arith_setup =
    1.17 - [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
    1.18 + [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    1.19     {add_mono_thms = add_mono_thms @ add_mono_thms_int,
    1.20 +    mult_mono_thms = mult_mono_thms,
    1.21      inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
    1.22      lessD = lessD @ [add1_zle_eq RS iffD2],
    1.23      simpset = simpset addsimps add_rules
     2.1 --- a/src/HOL/Integ/nat_bin.ML	Mon Dec 18 14:57:58 2000 +0100
     2.2 +++ b/src/HOL/Integ/nat_bin.ML	Mon Dec 18 14:59:05 2000 +0100
     2.3 @@ -45,8 +45,8 @@
     2.4  
     2.5  
     2.6  val nat_bin_arith_setup =
     2.7 - [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
     2.8 -   {add_mono_thms = add_mono_thms,
     2.9 + [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    2.10 +   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    2.11      inj_thms = inj_thms,
    2.12      lessD = lessD,
    2.13      simpset = simpset addsimps [int_nat_number_of,
     3.1 --- a/src/HOL/Integ/nat_simprocs.ML	Mon Dec 18 14:57:58 2000 +0100
     3.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Mon Dec 18 14:59:05 2000 +0100
     3.3 @@ -88,8 +88,7 @@
     3.4  
     3.5  (*Utilities*)
     3.6  
     3.7 -fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $
     3.8 -                   NumeralSyntax.mk_bin n;
     3.9 +fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_bin n;
    3.10  
    3.11  (*Decodes a unary or binary numeral to a NATURAL NUMBER*)
    3.12  fun dest_numeral (Const ("0", _)) = 0
    3.13 @@ -466,8 +465,9 @@
    3.14  in
    3.15  
    3.16  val nat_simprocs_setup =
    3.17 - [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
    3.18 -   {add_mono_thms = add_mono_thms, inj_thms = inj_thms, lessD = lessD,
    3.19 + [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    3.20 +   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    3.21 +    inj_thms = inj_thms, lessD = lessD,
    3.22      simpset = simpset addsimps add_rules
    3.23                        addsimps basic_renamed_arith_simps
    3.24                        addsimprocs simprocs})];
     4.1 --- a/src/HOL/Real/RealBin.ML	Mon Dec 18 14:57:58 2000 +0100
     4.2 +++ b/src/HOL/Real/RealBin.ML	Mon Dec 18 14:59:05 2000 +0100
     4.3 @@ -262,8 +262,7 @@
     4.4  
     4.5  (*Utilities*)
     4.6  
     4.7 -fun mk_numeral n = HOLogic.number_of_const HOLogic.realT $ 
     4.8 -                   NumeralSyntax.mk_bin n;
     4.9 +fun mk_numeral n = HOLogic.number_of_const HOLogic.realT $ HOLogic.mk_bin n;
    4.10  
    4.11  (*Decodes a binary real constant*)
    4.12  fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
     5.1 --- a/src/HOL/Real/real_arith.ML	Mon Dec 18 14:57:58 2000 +0100
     5.2 +++ b/src/HOL/Real/real_arith.ML	Mon Dec 18 14:59:05 2000 +0100
     5.3 @@ -24,7 +24,7 @@
     5.4           real_mult_minus_1, real_mult_minus_1_right];
     5.5  
     5.6  val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
     5.7 -               Real_Numeral_Simprocs.cancel_numerals;
     5.8 +               Real_Numeral_Simprocs.cancel_numerals(* @ real_cancel_numeral_factors*);
     5.9  
    5.10  val mono_ss = simpset() addsimps
    5.11                  [real_add_le_mono,real_add_less_mono,
    5.12 @@ -47,17 +47,26 @@
    5.13    map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT))
    5.14        ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
    5.15  
    5.16 +fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
    5.17 +
    5.18 +val real_mult_mono_thms =
    5.19 + [(rotate_prems 1 real_mult_less_mono2,
    5.20 +   cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))),
    5.21 +  (real_mult_le_mono2,
    5.22 +   cvar(real_mult_le_mono2, hd(tl(prems_of real_mult_le_mono2))))]
    5.23 +
    5.24  in
    5.25  
    5.26  val fast_real_arith_simproc = mk_simproc
    5.27    "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
    5.28  
    5.29  val real_arith_setup =
    5.30 - [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
    5.31 + [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    5.32     {add_mono_thms = add_mono_thms @ add_mono_thms_real,
    5.33 +    mult_mono_thms = mult_mono_thms @ real_mult_mono_thms,
    5.34      inj_thms = inj_thms, (*FIXME: add real*)
    5.35      lessD = lessD,  (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*)
    5.36 -    simpset = simpset addsimps simps@add_rules
    5.37 +    simpset = simpset addsimps (True_implies_equals :: add_rules @ simps)
    5.38                        addsimprocs simprocs
    5.39                        addcongs [if_weak_cong]}),
    5.40    arith_discrete ("RealDef.real",false),
     6.1 --- a/src/HOL/Tools/numeral_syntax.ML	Mon Dec 18 14:57:58 2000 +0100
     6.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Mon Dec 18 14:59:05 2000 +0100
     6.3 @@ -10,7 +10,6 @@
     6.4  signature NUMERAL_SYNTAX =
     6.5  sig
     6.6    val dest_bin : term -> int
     6.7 -  val mk_bin   : int -> term
     6.8    val setup    : (theory -> theory) list
     6.9  end;
    6.10  
    6.11 @@ -20,10 +19,6 @@
    6.12  
    6.13  (* bits *)
    6.14  
    6.15 -fun mk_bit 0 = HOLogic.false_const
    6.16 -  | mk_bit 1 = HOLogic.true_const
    6.17 -  | mk_bit _ = sys_error "mk_bit";
    6.18 -
    6.19  fun dest_bit (Const ("False", _)) = 0
    6.20    | dest_bit (Const ("True", _)) = 1
    6.21    | dest_bit _ = raise Match;
    6.22 @@ -35,17 +30,6 @@
    6.23    | prefix_len pred (x :: xs) =
    6.24        if pred x then 1 + prefix_len pred xs else 0;
    6.25  
    6.26 -fun mk_bin n =
    6.27 -  let
    6.28 -    fun bin_of 0  = []
    6.29 -      | bin_of ~1 = [~1]
    6.30 -      | bin_of n  = (n mod 2) :: bin_of (n div 2);
    6.31 -
    6.32 -    fun term_of []   = HOLogic.pls_const
    6.33 -      | term_of [~1] = HOLogic.min_const
    6.34 -      | term_of (b :: bs) = HOLogic.bit_const $ term_of bs $ mk_bit b;
    6.35 -    in term_of (bin_of n) end;
    6.36 -
    6.37  (*we consider all "spellings"; Min is likely to be declared elsewhere*)
    6.38  fun bin_of (Const ("Pls", _)) = []
    6.39    | bin_of (Const ("bin.Pls", _)) = []
    6.40 @@ -74,7 +58,7 @@
    6.41  (* translation of integer numeral tokens to and from bitstrings *)
    6.42  
    6.43  fun numeral_tr (*"_Numeral"*) [t as Free (str, _)] =
    6.44 -      (Syntax.const "Numeral.number_of" $ mk_bin (Syntax.read_xnum str))
    6.45 +      (Syntax.const "Numeral.number_of" $ HOLogic.mk_bin (Syntax.read_xnum str))
    6.46    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    6.47  
    6.48  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
     7.1 --- a/src/HOL/arith_data.ML	Mon Dec 18 14:57:58 2000 +0100
     7.2 +++ b/src/HOL/arith_data.ML	Mon Dec 18 14:59:05 2000 +0100
     7.3 @@ -299,8 +299,14 @@
     7.4    | nT _ = false;
     7.5  
     7.6  fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
     7.7 -                           | Some n => (overwrite(p,(t,n+m:int)), i));
     7.8 +                           | Some n => (overwrite(p,(t,ratadd(n,m))), i));
     7.9 +
    7.10 +exception Zero;
    7.11  
    7.12 +fun rat_of_term(numt,dent) =
    7.13 +  let val num = HOLogic.dest_binum numt and den = HOLogic.dest_binum dent
    7.14 +  in if den = 0 then raise Zero else int_ratdiv(num,den) end;
    7.15 + 
    7.16  fun decomp2 inj_consts (rel,lhs,rhs) =
    7.17  
    7.18  let
    7.19 @@ -308,30 +314,44 @@
    7.20  fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
    7.21    | poly(all as Const("op -",T) $ s $ t, m, pi) =
    7.22        if nT T then add_atom(all,m,pi)
    7.23 -      else poly(s,m,poly(t,~1*m,pi))
    7.24 -  | poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi)
    7.25 +      else poly(s,m,poly(t,ratneg m,pi))
    7.26 +  | poly(Const("uminus",_) $ t, m, pi) = poly(t,ratneg m,pi)
    7.27    | poly(Const("0",_), _, pi) = pi
    7.28 -  | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,i+m))
    7.29 +  | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m)))
    7.30    | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi)=
    7.31 -      (poly(t,m*HOLogic.dest_binum c,pi)
    7.32 +      (poly(t,ratmul(m, rat_of_int(HOLogic.dest_binum c)),pi)
    7.33         handle TERM _ => add_atom(all,m,pi))
    7.34    | poly(all as Const("op *",_) $ t $ (Const("Numeral.number_of",_)$c), m, pi)=
    7.35 -      (poly(t,m*HOLogic.dest_binum c,pi)
    7.36 +      (poly(t,ratmul(m, rat_of_int(HOLogic.dest_binum c)),pi)
    7.37         handle TERM _ => add_atom(all,m,pi))
    7.38 +  | poly(Const("op *",_) $ (Const("HOL.divide",_) $ (Const("Numeral.number_of",_)$numt) $
    7.39 +                                               (Const("Numeral.number_of",_)$dent)) $ t, m, pi) =
    7.40 +      poly(t,ratmul(m,rat_of_term(numt,dent)),pi)
    7.41 +  | poly(Const("op *",_) $ t $ (Const("HOL.divide",_) $ (Const("Numeral.number_of",_)$numt) $
    7.42 +                                               (Const("Numeral.number_of",_)$dent)), m, pi) =
    7.43 +      poly(t,ratmul(m,rat_of_term(numt,dent)),pi)
    7.44 +  | poly(all as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m, pi) =
    7.45 +      let val den = HOLogic.dest_binum dent
    7.46 +      in if den = 0 then raise Zero else poly(t,ratmul(m, ratinv(rat_of_int den)),pi) end
    7.47    | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
    7.48 -     ((p,i + m*HOLogic.dest_binum t)
    7.49 +     ((p,ratadd(i,ratmul(m,rat_of_int(HOLogic.dest_binum t))))
    7.50        handle TERM _ => add_atom(all,m,(p,i)))
    7.51 +  | poly(Const("HOL.divide",_) $ (Const("Numeral.number_of",_)$numt) $
    7.52 +                                 (Const("Numeral.number_of",_)$dent), m, (p,i)) =
    7.53 +      (p,ratadd(i,ratmul(m,rat_of_term(numt,dent))))
    7.54    | poly(all as Const f $ x, m, pi) =
    7.55        if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi)
    7.56    | poly x  = add_atom x;
    7.57  
    7.58 -  val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
    7.59 +  val (p,i) = poly(lhs,rat_of_int 1,([],rat_of_int 0))
    7.60 +  and (q,j) = poly(rhs,rat_of_int 1,([],rat_of_int 0))
    7.61 +
    7.62    in case rel of
    7.63         "op <"  => Some(p,i,"<",q,j)
    7.64       | "op <=" => Some(p,i,"<=",q,j)
    7.65       | "op ="  => Some(p,i,"=",q,j)
    7.66       | _       => None
    7.67 -  end;
    7.68 +  end handle Zero => None;
    7.69  
    7.70  fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
    7.71    | negate None = None;
    7.72 @@ -355,6 +375,8 @@
    7.73    let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg
    7.74    in decomp2 (discrete,inj_consts) end
    7.75  
    7.76 +fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n)
    7.77 +
    7.78  end;
    7.79  
    7.80  
    7.81 @@ -384,8 +406,9 @@
    7.82  
    7.83  val init_lin_arith_data =
    7.84   Fast_Arith.setup @
    7.85 - [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset = _} =>
    7.86 + [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset = _} =>
    7.87     {add_mono_thms = add_mono_thms @ add_mono_thms_nat,
    7.88 +    mult_mono_thms = mult_mono_thms,
    7.89      inj_thms = inj_thms,
    7.90      lessD = lessD @ [Suc_leI],
    7.91      simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
     8.1 --- a/src/HOL/hologic.ML	Mon Dec 18 14:57:58 2000 +0100
     8.2 +++ b/src/HOL/hologic.ML	Mon Dec 18 14:59:05 2000 +0100
     8.3 @@ -71,6 +71,7 @@
     8.4    val number_of_const: typ -> term
     8.5    val int_of: int list -> int
     8.6    val dest_binum: term -> int
     8.7 +  val mk_bin   : int -> term
     8.8  end;
     8.9  
    8.10  
    8.11 @@ -290,4 +291,19 @@
    8.12  
    8.13  val dest_binum = int_of o bin_of;
    8.14  
    8.15 +fun mk_bit 0 = false_const
    8.16 +  | mk_bit 1 = true_const
    8.17 +  | mk_bit _ = sys_error "mk_bit";
    8.18 +
    8.19 +fun mk_bin n =
    8.20 +  let
    8.21 +    fun bin_of 0  = []
    8.22 +      | bin_of ~1 = [~1]
    8.23 +      | bin_of n  = (n mod 2) :: bin_of (n div 2);
    8.24 +
    8.25 +    fun term_of []   = pls_const
    8.26 +      | term_of [~1] = min_const
    8.27 +      | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
    8.28 +    in term_of (bin_of n) end;
    8.29 +
    8.30  end;