--- 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
--- 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
--- 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;
--- 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;