# HG changeset patch
# User haftmann
# Date 1179767502 -7200
# Node ID b4ee6ec4f9c6626603102dc3ee5eba746ff094af
# Parent  d88d2087436dd5942048eaa0dc89f1fe3bbb0b5f
tuned

diff -r d88d2087436d -r b4ee6ec4f9c6 src/HOL/Library/Pure_term.thy
--- a/src/HOL/Library/Pure_term.thy	Mon May 21 19:11:41 2007 +0200
+++ b/src/HOL/Library/Pure_term.thy	Mon May 21 19:11:42 2007 +0200
@@ -72,26 +72,8 @@
      \<and> list_all2 (op =) tys1 tys2"
   by (auto simp add: list_all2_eq [symmetric])
 
-definition
-  Bound :: "int \<Rightarrow> term"
-where
-  "Bound k = Bnd (nat k)"
-
-lemma Bnd_Bound [code inline, code func]:
-  "Bnd n = Bound (int n)"
-  unfolding Bound_def by auto
+code_datatype Const App Fix
 
-definition
-  Absp :: "vname \<Rightarrow> typ \<Rightarrow> term \<Rightarrow> term"
-where
-  "Absp v ty t = (v, ty) \<mapsto> t"
-
-lemma Abs_Absp [code inline, code func]:
-  "(op \<mapsto>) (v, ty) = Absp v ty"
-  by rule (auto simp add: Absp_def)
-
-code_datatype Const App Fix Absp Bound
-lemmas [code func] = Bnd_Bound Abs_Absp
 lemmas [code func del] = term.recs term.cases term.size
 lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
 
@@ -102,9 +84,7 @@
   (SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)")
 
 code_const Const and App and Fix
-  and Absp and Bound
-  (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)"
-    and "Term.Abs/ (_, _, _)" and "!((_); Term.Bound/ (raise Fail \"Bound\"))")
+  (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)")
  
 code_reserved SML Term
 
diff -r d88d2087436d -r b4ee6ec4f9c6 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Mon May 21 19:11:41 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon May 21 19:11:42 2007 +0200
@@ -155,10 +155,6 @@
 
 datatype lineq = Lineq of IntInf.int * lineq_type * IntInf.int list * injust;
 
-fun el 0 (h::_) = h
-  | el n (_::t) = el (n - 1) t
-  | el _ _  = sys_error "el";
-
 (* ------------------------------------------------------------------------- *)
 (* Finding a (counter) example from the trace of a failed elimination        *)
 (* ------------------------------------------------------------------------- *)
@@ -181,8 +177,8 @@
   let
     val rs = map Rat.rat_of_int cs;
     val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero;
-  in (Rat.mult (Rat.add (Rat.rat_of_int a) (Rat.neg rsum)) (Rat.inv (el v rs)), le) end;
-(* If el v rs < 0, le should be negated.
+  in (Rat.mult (Rat.add (Rat.rat_of_int a) (Rat.neg rsum)) (Rat.inv (nth rs v)), le) end;
+(* If nth rs v < 0, le should be negated.
    Instead this swap is taken into account in ratrelmin2.
 *)
 
@@ -228,18 +224,20 @@
 
 fun findex1 discr (v, lineqs) ex =
   let
-    val nz = filter (fn (Lineq (_, _, cs, _)) => el v cs <> 0) lineqs;
+    val nz = filter (fn (Lineq (_, _, cs, _)) => nth cs v <> 0) lineqs;
     val ineqs = maps elim_eqns nz;
-    val (ge, le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
+    val (ge, le) = List.partition (fn (_,_,cs) => nth cs v > 0) ineqs
     val lb = ratrelmax (map (eval ex v) ge)
     val ub = ratrelmin (map (eval ex v) le)
   in nth_map v (K (choose2 (nth discr v) (lb, ub))) ex end;
 
 fun elim1 v x =
-  map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (el v bs) x)), le,
+  map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (nth bs v) x)), le,
                         nth_map v (K Rat.zero) bs));
 
-fun single_var v (_,_,cs) = (filter_out (curry (op =) EQUAL o Rat.cmp_zero) cs = [el v cs]);
+fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.cmp_zero) cs
+ of [x] => x =/ nth cs v
+  | _ => false;
 
 (* The base case:
    all variables occur only with positive or only with negative coefficients *)
@@ -249,14 +247,14 @@
      | (_,_,cs) :: _ =>
        let val v = find_index (not o curry (op =) EQUAL o Rat.cmp_zero) cs
            val d = nth discr v;
-           val pos = not (Rat.cmp_zero (el v cs) = LESS);
+           val pos = not (Rat.cmp_zero (nth cs v) = LESS);
            val sv = filter (single_var v) nz;
            val minmax =
              if pos then if d then Rat.roundup o fst o ratrelmax
                          else ratexact true o ratrelmax
                     else if d then Rat.rounddown o fst o ratrelmin
                          else ratexact false o ratrelmin
-           val bnds = map (fn (a,le,bs) => (Rat.mult a (Rat.inv (el v bs)), le)) sv
+           val bnds = map (fn (a,le,bs) => (Rat.mult a (Rat.inv (nth bs v)), le)) sv
            val x = minmax((Rat.zero,if pos then true else false)::bnds)
            val ineqs' = elim1 v x nz
            val ex' = nth_map v (K x) ex
@@ -307,7 +305,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
-  let val c1 = el v l1 and c2 = el v l2
+  let val c1 = nth l1 v and c2 = nth l2 v
       val m = lcm(abs c1, abs c2)
       val m1 = m div (abs c1) and m2 = m div (abs c2)
       val (n1,n2) =
@@ -384,22 +382,22 @@
          val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) =
                extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
          val v = find_index_eq c ceq
-         val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => el v l = 0)
+         val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0)
                                      (othereqs @ noneqs)
          val others = map (elim_var v eq) roth @ ioth
      in elim(others,(v,nontriv)::hist) end
   else
   let val lists = map (fn (Lineq(_,_,l,_)) => l) noneqs
-      val numlist = 0 upto (length(hd lists) - 1)
-      val coeffs = map (fn i => map (el i) lists) numlist
+      val numlist = 0 upto (length (hd lists) - 1)
+      val coeffs = map (fn i => map (fn xs => nth xs i) lists) numlist
       val blows = map calc_blowup coeffs
       val iblows = blows ~~ numlist
-      val nziblows = List.filter (fn (i,_) => i<>0) iblows
+      val nziblows = filter_out (fn (i, _) => i = 0) iblows
   in if null nziblows then Failure((~1,nontriv)::hist)
      else
      let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows)
-         val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => el v l = 0) ineqs
-         val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => el v l > 0) yes
+         val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ineqs
+         val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => nth l v > 0) yes
      in elim(no @ allpairs (elim_var v) pos neg, (v,nontriv)::hist) end
   end
   end
diff -r d88d2087436d -r b4ee6ec4f9c6 src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Mon May 21 19:11:41 2007 +0200
+++ b/src/Pure/General/rat.ML	Mon May 21 19:11:42 2007 +0200
@@ -29,7 +29,7 @@
   val rounddown: rat -> rat
 end;
 
-structure Rat: RAT =
+structure Rat :> RAT =
 struct
 
 datatype rat = Rat of bool * Intt.int * Intt.int;
@@ -71,19 +71,15 @@
   | eq (Rat (true, _, _), Rat (false, _, _)) = false
   | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 = p2 andalso q1 = q2
 
-fun le (Rat (false, _, _)) (Rat (true, _, _)) = true
-  | le (Rat (true, _, _)) (Rat (false, _, _)) = false
-  | le (Rat (a, p1, q1)) (Rat (_, p2, q2)) =
-      let val (r1, r2, _) = common (p1, q1, p2, q2)
-      in if a then r1 <= r2 else r2 <= r1 end;
-
 fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS
   | cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER
   | cmp (Rat (a, p1, q1), Rat (_, p2, q2)) =
       let val (r1, r2, _) = common (p1, q1, p2, q2)
       in if a then Intt.cmp (r1, r2) else Intt.cmp (r2, r1) end;
 
-fun lt a b = cmp (a,b) = LESS;
+fun le a b = let val order = cmp (a, b) in order = LESS orelse order = EQUAL end;
+fun lt a b = cmp (a, b) = LESS;
+
 fun cmp_zero (Rat (false, _, _)) = LESS
   | cmp_zero (Rat (_, 0, _)) = EQUAL
   | cmp_zero (Rat (_, _, _)) = GREATER;
@@ -126,16 +122,16 @@
 
 end;
 
-infix 5 +/;
-infix 6 -/;
-infix 4 */;
-infix 3 //;
-infix 9 =/ </ <=/ >/ >=/ <>/;
+infix 6 +/; (*FIXME infix 5?*)
+infix 5 -/;
+infix 7 */;
+infix 8 //; (*FIXME infix 7?*)
+infix 4 =/ </ <=/ >/ >=/ <>/;
 
 fun a +/ b = Rat.add a b;
-fun a -/ b = a +/ (Rat.neg b);
-fun a  */ b = Rat.mult a b;
-fun a // b = a */ (Rat.inv b); 
+fun a -/ b = a +/ Rat.neg b;
+fun a */ b = Rat.mult a b;
+fun a // b = a */ Rat.inv b; 
 fun a =/ b = Rat.eq (a,b);
 fun a </ b = Rat.lt a b;
 fun a <=/ b = Rat.le a b;
diff -r d88d2087436d -r b4ee6ec4f9c6 src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Mon May 21 19:11:41 2007 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Mon May 21 19:11:42 2007 +0200
@@ -37,7 +37,7 @@
 
 (** purification **)
 
-val purify_name =
+fun purify_name upper_else_lower =
   let
     fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
     val is_junk = not o is_valid andf Symbol.not_eof;
@@ -47,32 +47,20 @@
         (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
         --| junk))
       -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
-  in explode #> scan_valids #> space_implode "_" end;
-
-fun purify_op "op -->" = "implies"
-  | purify_op "{}" = "empty"
-  | purify_op s =
-      let
-        fun rep_op "+" = SOME "plus"
-          | rep_op "*" = SOME "times"
-          | rep_op "&" = SOME "and"
-          | rep_op "|" = SOME "or"
-          | rep_op "=" = SOME "eq"
-          | rep_op s = NONE;
-        val scan_valids = Symbol.scanner "Malformed input"
-           (Scan.repeat (Scan.some rep_op || Scan.one Symbol.not_eof));
-      in (explode #> scan_valids #> implode) s end;
-
-val purify_lower =
-  explode
-  #> (fn cs => (if forall Symbol.is_ascii_upper cs
-        then map else nth_map 0) Symbol.to_ascii_lower cs)
-  #> implode;
-
-val purify_upper = explode #> nth_map 0 Symbol.to_ascii_upper #> implode;
+    fun upper_lower cs = if upper_else_lower then nth_map 0 Symbol.to_ascii_upper cs
+      else (if forall Symbol.is_ascii_upper cs
+        then map else nth_map 0) Symbol.to_ascii_lower cs;
+  in
+    explode
+    #> scan_valids
+    #> space_implode "_"
+    #> explode
+    #> upper_lower
+    #> implode
+  end;
 
 fun purify_var "" = "x"
-  | purify_var v = (purify_name #> purify_lower) v;
+  | purify_var v = purify_name false v;
 
 fun purify_tvar "" = "'a"
   | purify_tvar v =
@@ -81,7 +69,7 @@
 fun check_modulename mn =
   let
     val mns = NameSpace.explode mn;
-    val mns' = map purify_upper mns;
+    val mns' = map (purify_name true) mns;
   in
     if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
       ^ "perhaps try " ^ quote (NameSpace.implode mns'))
@@ -187,28 +175,38 @@
 
 (* naming policies *)
 
-val purify_idf = purify_op #> purify_name;
-val purify_prefix = map (purify_idf #> purify_upper);
-val purify_base = purify_idf #> purify_lower;
-
-val dotify =
+val purify_prefix =
   explode
   (*should disappear as soon as hierarchical theory name spaces are available*)
   #> Symbol.scanner "Malformed name"
       (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.not_eof))
-  #> implode;
+  #> implode
+  #> NameSpace.explode
+  #> map (purify_name true);
 
-fun policy thy get_basename get_thyname name =
+fun purify_base "op =" = "eq"
+  | purify_base "op &" = "and"
+  | purify_base "op |" = "or"
+  | purify_base "op -->" = "implies"
+  | purify_base "{}" = "empty"
+  | purify_base "op :" = "member"
+  | purify_base "op Int" = "intersect"
+  | purify_base "op Un" = "union"
+  | purify_base "*" = "product"
+  | purify_base "+" = "sum"
+  | purify_base s = purify_name false s;
+
+fun default_policy thy get_basename get_thyname name =
   let
-    val prefix = (purify_prefix o NameSpace.explode o dotify o get_thyname thy) name;
+    val prefix = (purify_prefix o get_thyname thy) name;
     val base = (purify_base o get_basename) name;
   in NameSpace.implode (prefix @ [base]) end;
 
-fun class_policy thy = policy thy NameSpace.base thyname_of_class;
-fun classrel_policy thy = policy thy (fn (class1, class2) => 
+fun class_policy thy = default_policy thy NameSpace.base thyname_of_class;
+fun classrel_policy thy = default_policy thy (fn (class1, class2) => 
   NameSpace.base class1 ^ "_" ^ NameSpace.base class2) thyname_of_classrel;
-fun tyco_policy thy = policy thy NameSpace.base thyname_of_tyco;
-fun instance_policy thy = policy thy (fn (class, tyco) => 
+fun tyco_policy thy = default_policy thy NameSpace.base thyname_of_tyco;
+fun instance_policy thy = default_policy thy (fn (class, tyco) => 
   NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
 
 fun force_thyname thy (const as (c, opt_tyco)) =
@@ -222,9 +220,9 @@
 
 fun const_policy thy (const as (c, opt_tyco)) =
   case force_thyname thy const
-   of NONE => policy thy NameSpace.base thyname_of_const c
+   of NONE => default_policy thy NameSpace.base thyname_of_const c
     | SOME thyname => let
-        val prefix = (purify_prefix o NameSpace.explode o dotify) thyname;
+        val prefix = purify_prefix thyname;
         val tycos = the_list opt_tyco;
         val base = map (purify_base o NameSpace.base) (c :: tycos);
       in NameSpace.implode (prefix @ [space_implode "_" base]) end;