# HG changeset patch # User haftmann # Date 1184081456 -7200 # Node ID 49b08f25db296fe20be67914434635c1d6c7bb0b # Parent db10cf19f1f8f2b8ea3e7747dc7534078125d696 now a monolithic module diff -r db10cf19f1f8 -r 49b08f25db29 src/HOL/Tools/Qelim/generated_cooper.ML --- a/src/HOL/Tools/Qelim/generated_cooper.ML Tue Jul 10 17:30:54 2007 +0200 +++ b/src/HOL/Tools/Qelim/generated_cooper.ML Tue Jul 10 17:30:56 2007 +0200 @@ -7,26 +7,11 @@ structure GeneratedCooper = struct -structure Product_Type = -struct - -fun fst (y, b) = y; - -fun snd (a, y) = y; - -end; (*struct Product_Type*) - -structure Integer = -struct +type 'a eq = {eq : 'a -> 'a -> bool}; +fun eq (A_:'a eq) = #eq A_; datatype bit = B0 | B1; -fun suc n = (IntInf.+ (n, (1 : IntInf.int))); - -val zero_nat : IntInf.int = (0 : IntInf.int); - -fun nat k = (if IntInf.< (k, (0 : IntInf.int)) then zero_nat else k); - fun adjust b = (fn a as (q, r) => (if IntInf.<= ((0 : IntInf.int), IntInf.- (r, b)) @@ -58,90 +43,102 @@ else (if IntInf.< ((0 : IntInf.int), b) then negDivAlg aa b else negateSnd (posDivAlg (IntInf.~ aa) (IntInf.~ b))))); +fun snd (a, y) = y; + +fun mod_nat m k = (snd (divAlg (m, k))); + +val zero_nat : IntInf.int = (0 : IntInf.int); + +fun gcd (m, n) = + (if ((n : IntInf.int) = zero_nat) then m else gcd (n, mod_nat m n)); + +fun fst (y, b) = y; + +fun div_nat m k = (fst (divAlg (m, k))); + +val lcm : IntInf.int * IntInf.int -> IntInf.int = + (fn a as (m, n) => div_nat (IntInf.* (m, n)) (gcd (m, n))); + +fun suc n = (IntInf.+ (n, (1 : IntInf.int))); + fun abs_int i = (if IntInf.< (i, (0 : IntInf.int)) then IntInf.~ i else i); -fun div_int a b = Product_Type.fst (divAlg (a, b)); - -fun mod_int a b = Product_Type.snd (divAlg (a, b)); - -fun dvd_int m n = (((mod_int n m) : IntInf.int) = (0 : IntInf.int)); - -fun eq_bit B0 B0 = true - | eq_bit B1 B1 = true - | eq_bit B0 B1 = false - | eq_bit B1 B0 = false; +fun nat k = (if IntInf.< (k, (0 : IntInf.int)) then zero_nat else k); fun int_aux i n = (if ((n : IntInf.int) = (0 : IntInf.int)) then i else int_aux (IntInf.+ (i, (1 : IntInf.int))) (IntInf.- (n, (1 : IntInf.int)))); -end; (*struct Integer*) - -structure Nat = -struct - -fun div_nat m k = (Product_Type.fst (Integer.divAlg (m, k))); - -fun mod_nat m k = (Product_Type.snd (Integer.divAlg (m, k))); - -end; (*struct Nat*) - -structure GCD = -struct - -fun gcd (m, n) = - (if ((n : IntInf.int) = Integer.zero_nat) then m - else gcd (n, Nat.mod_nat m n)); - -val lcm : IntInf.int * IntInf.int -> IntInf.int = - (fn a as (m, n) => Nat.div_nat (IntInf.* (m, n)) (gcd (m, n))); - val ilcm : IntInf.int -> IntInf.int -> IntInf.int = (fn i => fn j => - Integer.int_aux (0 : IntInf.int) - (lcm (Integer.nat (Integer.abs_int i), Integer.nat (Integer.abs_int j)))); - -end; (*struct GCD*) - -structure HOL = -struct + int_aux (0 : IntInf.int) (lcm (nat (abs_int i), nat (abs_int j)))); -type 'a eq = {eq : 'a -> 'a -> bool}; -fun eq (A_:'a eq) = #eq A_; - -end; (*struct HOL*) - -structure List = -struct +type 'a zero = {zero : 'a}; +fun zero (A_:'a zero) = #zero A_; fun map f (x :: xs) = f x :: map f xs | map f [] = []; +type 'a times = {times : 'a -> 'a -> 'a}; +fun times (A_:'a times) = #times A_; + fun foldr f (x :: xs) a = f x (foldr f xs a) | foldr f [] y = y; +type 'a diva = {div : 'a -> 'a -> 'a, mod : 'a -> 'a -> 'a}; +fun diva (A_:'a diva) = #div A_; +fun moda (A_:'a diva) = #mod A_; + +type 'a dvd_mod = + {Divides__dvd_mod_div : 'a diva, Divides__dvd_mod_times : 'a times, + Divides__dvd_mod_zero : 'a zero}; +fun dvd_mod_div (A_:'a dvd_mod) = #Divides__dvd_mod_div A_; +fun dvd_mod_times (A_:'a dvd_mod) = #Divides__dvd_mod_times A_; +fun dvd_mod_zero (A_:'a dvd_mod) = #Divides__dvd_mod_zero A_; + +fun dvd (A1_, A2_) x y = + eq A2_ (moda (dvd_mod_div A1_) y x) (zero (dvd_mod_zero A1_)); + fun append (x :: xs) ys = x :: append xs ys | append [] y = y; -fun memberl A_ x (y :: ys) = HOL.eq A_ x y orelse memberl A_ x ys +fun memberl A_ x (y :: ys) = eq A_ x y orelse memberl A_ x ys | memberl A_ x [] = false; fun remdups A_ (x :: xs) = (if memberl A_ x xs then remdups A_ xs else x :: remdups A_ xs) | remdups A_ [] = []; +fun mod_int a b = snd (divAlg (a, b)); + +fun div_int a b = fst (divAlg (a, b)); + +val div_inta = {div = div_int, mod = mod_int} : IntInf.int diva; + fun allpairs f (x :: xs) ys = append (map (f x) ys) (allpairs f xs ys) | allpairs f [] ys = []; -fun size_list (a :: lista) = - (IntInf.+ ((size_list lista), (Integer.suc Integer.zero_nat))) - | size_list [] = Integer.zero_nat; +val eq_int = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq; + +val zero_int : IntInf.int = (0 : IntInf.int); + +val zero_inta = {zero = zero_int} : IntInf.int zero; + +fun size_list (a :: lista) = (IntInf.+ ((size_list lista), (suc zero_nat))) + | size_list [] = zero_nat; -end; (*struct List*) +fun eq_bit B0 B0 = true + | eq_bit B1 B1 = true + | eq_bit B0 B1 = false + | eq_bit B1 B0 = false; -structure Reflected_Presburger = -struct +val times_int = {times = (fn a => fn b => IntInf.* (a, b))} : IntInf.int times; + +val dvd_mod_int = + {Divides__dvd_mod_div = div_inta, Divides__dvd_mod_times = times_int, + Divides__dvd_mod_zero = zero_inta} + : IntInf.int dvd_mod; datatype num = C of IntInf.int | Bound of IntInf.int | Cx of IntInf.int * num | Neg of num | Add of num * num | Sub of num * num | Mul of IntInf.int * num; @@ -169,7 +166,7 @@ | disjuncts (Lt u) = [Lt u] | disjuncts T = [T] | disjuncts F = [] - | disjuncts (Or (p, q)) = List.append (disjuncts p) (disjuncts q); + | disjuncts (Or (p, q)) = append (disjuncts p) (disjuncts q); fun eq_num (C int) (C int') = ((int : IntInf.int) = int') | eq_num (Bound nat) (Bound nat') = ((nat : IntInf.int) = nat') @@ -608,7 +605,7 @@ | A fm => Or (f p, q) | Closed nat => Or (f p, q) | NClosed nat => Or (f p, q)))); -fun evaldjf f ps = List.foldr (djf f) ps F; +fun evaldjf f ps = foldr (djf f) ps F; fun dj f p = evaldjf f (disjuncts p); @@ -645,7 +642,7 @@ (IntInf.+ (i, i'), aa) end | zsplit0 (Bound n) = - (if ((n : IntInf.int) = Integer.zero_nat) + (if ((n : IntInf.int) = zero_nat) then ((1 : IntInf.int), C (0 : IntInf.int)) else ((0 : IntInf.int), Bound n)) | zsplit0 (C c) = ((0 : IntInf.int), C c); @@ -681,22 +678,20 @@ else let val (c, r) = zsplit0 a; in - (if ((c : IntInf.int) = (0 : IntInf.int)) - then NDvd (Integer.abs_int i, r) + (if ((c : IntInf.int) = (0 : IntInf.int)) then NDvd (abs_int i, r) else (if IntInf.< ((0 : IntInf.int), c) - then NDvd (Integer.abs_int i, Cx (c, r)) - else NDvd (Integer.abs_int i, Cx (IntInf.~ c, Neg r)))) + then NDvd (abs_int i, Cx (c, r)) + else NDvd (abs_int i, Cx (IntInf.~ c, Neg r)))) end) | zlfm (Dvd (i, a)) = (if ((i : IntInf.int) = (0 : IntInf.int)) then zlfm (Eq a) else let val (c, r) = zsplit0 a; in - (if ((c : IntInf.int) = (0 : IntInf.int)) - then Dvd (Integer.abs_int i, r) + (if ((c : IntInf.int) = (0 : IntInf.int)) then Dvd (abs_int i, r) else (if IntInf.< ((0 : IntInf.int), c) - then Dvd (Integer.abs_int i, Cx (c, r)) - else Dvd (Integer.abs_int i, Cx (IntInf.~ c, Neg r)))) + then Dvd (abs_int i, Cx (c, r)) + else Dvd (abs_int i, Cx (IntInf.~ c, Neg r)))) end) | zlfm (NEq a) = let @@ -817,8 +812,8 @@ | zeta (Lt (Cx (y, e))) = y | zeta (NEq (Cx (y, e))) = y | zeta (Eq (Cx (y, e))) = y - | zeta (Or (p, q)) = GCD.ilcm (zeta p) (zeta q) - | zeta (And (p, q)) = GCD.ilcm (zeta p) (zeta q); + | zeta (Or (p, q)) = ilcm (zeta p) (zeta q) + | zeta (And (p, q)) = ilcm (zeta p) (zeta q); fun a_beta (NClosed aq) = (fn k => NClosed aq) | a_beta (Closed ap) = (fn k => Closed ap) @@ -879,24 +874,24 @@ | a_beta T = (fn k => T) | a_beta (NDvd (i, Cx (c, e))) = (fn k => - NDvd (IntInf.* (Integer.div_int k c, i), - Cx ((1 : IntInf.int), Mul (Integer.div_int k c, e)))) + NDvd (IntInf.* (div_int k c, i), + Cx ((1 : IntInf.int), Mul (div_int k c, e)))) | a_beta (Dvd (i, Cx (c, e))) = (fn k => - Dvd (IntInf.* (Integer.div_int k c, i), - Cx ((1 : IntInf.int), Mul (Integer.div_int k c, e)))) + Dvd (IntInf.* (div_int k c, i), + Cx ((1 : IntInf.int), Mul (div_int k c, e)))) | a_beta (Ge (Cx (c, e))) = - (fn k => Ge (Cx ((1 : IntInf.int), Mul (Integer.div_int k c, e)))) + (fn k => Ge (Cx ((1 : IntInf.int), Mul (div_int k c, e)))) | a_beta (Gt (Cx (c, e))) = - (fn k => Gt (Cx ((1 : IntInf.int), Mul (Integer.div_int k c, e)))) + (fn k => Gt (Cx ((1 : IntInf.int), Mul (div_int k c, e)))) | a_beta (Le (Cx (c, e))) = - (fn k => Le (Cx ((1 : IntInf.int), Mul (Integer.div_int k c, e)))) + (fn k => Le (Cx ((1 : IntInf.int), Mul (div_int k c, e)))) | a_beta (Lt (Cx (c, e))) = - (fn k => Lt (Cx ((1 : IntInf.int), Mul (Integer.div_int k c, e)))) + (fn k => Lt (Cx ((1 : IntInf.int), Mul (div_int k c, e)))) | a_beta (NEq (Cx (c, e))) = - (fn k => NEq (Cx ((1 : IntInf.int), Mul (Integer.div_int k c, e)))) + (fn k => NEq (Cx ((1 : IntInf.int), Mul (div_int k c, e)))) | a_beta (Eq (Cx (c, e))) = - (fn k => Eq (Cx ((1 : IntInf.int), Mul (Integer.div_int k c, e)))) + (fn k => Eq (Cx ((1 : IntInf.int), Mul (div_int k c, e)))) | a_beta (Or (p, q)) = (fn k => Or (a_beta p k, a_beta q k)) | a_beta (And (p, q)) = (fn k => And (a_beta p k, a_beta q k)); @@ -929,8 +924,8 @@ | delta T = (1 : IntInf.int) | delta (NDvd (y, Cx (c, e))) = y | delta (Dvd (y, Cx (c, e))) = y - | delta (Or (p, q)) = GCD.ilcm (delta p) (delta q) - | delta (And (p, q)) = GCD.ilcm (delta p) (delta q); + | delta (Or (p, q)) = ilcm (delta p) (delta q) + | delta (And (p, q)) = ilcm (delta p) (delta q); fun beta (NClosed aq) = [] | beta (Closed ap) = [] @@ -985,8 +980,8 @@ | beta (Lt (Cx (c, e))) = [] | beta (NEq (Cx (c, e))) = [Neg e] | beta (Eq (Cx (c, e))) = [Sub (C (~1 : IntInf.int), e)] - | beta (Or (p, q)) = List.append (beta p) (beta q) - | beta (And (p, q)) = List.append (beta p) (beta q); + | beta (Or (p, q)) = append (beta p) (beta q) + | beta (And (p, q)) = append (beta p) (beta q); fun alpha (NClosed aq) = [] | alpha (Closed ap) = [] @@ -1041,8 +1036,8 @@ | alpha (Lt (Cx (c, e))) = [e] | alpha (NEq (Cx (c, e))) = [e] | alpha (Eq (Cx (c, e))) = [Add (C (~1 : IntInf.int), e)] - | alpha (Or (p, q)) = List.append (alpha p) (alpha q) - | alpha (And (p, q)) = List.append (alpha p) (alpha q); + | alpha (Or (p, q)) = append (alpha p) (alpha q) + | alpha (And (p, q)) = append (alpha p) (alpha q); fun numadd (Mul (ar, asa), Mul (aza, azb)) = Add (Mul (ar, asa), Mul (aza, azb)) | numadd (Mul (ar, asa), Sub (ayy, ayz)) = Add (Mul (ar, asa), Sub (ayy, ayz)) @@ -1768,7 +1763,7 @@ Add (Mul ((1 : IntInf.int), Bound n), C (0 : IntInf.int)) | simpnum (C j) = C j; -val eq_numa = {eq = eq_num} : num HOL.eq; +val eq_numa = {eq = eq_num} : num eq; fun mirror (NClosed aq) = NClosed aq | mirror (Closed ap) = Closed ap @@ -1845,10 +1840,10 @@ val q = And (Dvd (l, Cx ((1 : IntInf.int), C (0 : IntInf.int))), a_beta p' l); val d = delta q; - val b = List.remdups eq_numa (List.map simpnum (beta q)); - val a = List.remdups eq_numa (List.map simpnum (alpha q)); + val b = remdups eq_numa (map simpnum (beta q)); + val a = remdups eq_numa (map simpnum (alpha q)); in - (if IntInf.<= ((List.size_list b), (List.size_list a)) then (q, (b, d)) + (if IntInf.<= ((size_list b), (size_list a)) then (q, (b, d)) else (mirror q, (a, d))) end; @@ -1918,7 +1913,7 @@ | numsubst0 t (Neg a) = Neg (numsubst0 t a) | numsubst0 t (Cx (i, a)) = Add (Mul (i, t), numsubst0 t a) | numsubst0 t (Bound n) = - (if ((n : IntInf.int) = Integer.zero_nat) then t else Bound n) + (if ((n : IntInf.int) = zero_nat) then t else Bound n) | numsubst0 t (C c) = C c; fun subst0 t (NClosed p) = NClosed p @@ -1989,12 +1984,13 @@ | simpfm T = T | simpfm (NDvd (i, a)) = (if ((i : IntInf.int) = (0 : IntInf.int)) then simpfm (NEq a) - else (if (((Integer.abs_int i) : IntInf.int) = (1 : IntInf.int)) then F + else (if (((abs_int i) : IntInf.int) = (1 : IntInf.int)) then F else let val a' = simpnum a; in (case a' - of C v => (if not (Integer.dvd_int i v) then T else F) + of C v => + (if not (dvd (dvd_mod_int, eq_int) i v) then T else F) | Bound nat => NDvd (i, a') | Cx (int, num) => NDvd (i, a') | Neg num => NDvd (i, a') | Add (num1, num2) => NDvd (i, a') @@ -2003,11 +1999,13 @@ end)) | simpfm (Dvd (i, a)) = (if ((i : IntInf.int) = (0 : IntInf.int)) then simpfm (Eq a) - else (if (((Integer.abs_int i) : IntInf.int) = (1 : IntInf.int)) then T + else (if (((abs_int i) : IntInf.int) = (1 : IntInf.int)) then T else let val a' = simpnum a; in - (case a' of C v => (if Integer.dvd_int i v then T else F) + (case a' + of C v => + (if dvd (dvd_mod_int, eq_int) i v then T else F) | Bound nat => Dvd (i, a') | Cx (int, num) => Dvd (i, a') | Neg num => Dvd (i, a') | Add (num1, num2) => Dvd (i, a') @@ -2082,7 +2080,7 @@ | decrnum (Sub (a, b)) = Sub (decrnum a, decrnum b) | decrnum (Add (a, b)) = Add (decrnum a, decrnum b) | decrnum (Neg a) = Neg (decrnum a) - | decrnum (Bound n) = Bound (Integer.nat (IntInf.- (n, (1 : IntInf.int)))); + | decrnum (Bound n) = Bound (nat (IntInf.- (n, (1 : IntInf.int)))); fun decr (NClosed ar) = NClosed ar | decr (Closed aq) = Closed aq @@ -2116,7 +2114,7 @@ else let val qd = evaldjf (fn aa as (ba, j) => simpfm (subst0 (Add (ba, C j)) q)) - (List.allpairs (fn aa => fn ba => (aa, ba)) b js); + (allpairs (fn aa => fn ba => (aa, ba)) b js); in decr (disj md qd) end) @@ -2239,6 +2237,4 @@ val pa : fm -> fm = (fn p => qelim (prep p) cooper); -end; (*struct Reflected_Presburger*) - -end; (*struct ROOT*) +end; (*struct GeneratedCooper*)