--- a/src/HOL/Library/Infinite_Set.thy Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Library/Infinite_Set.thy Tue Aug 23 15:46:53 2011 -0700
@@ -546,7 +546,7 @@
apply (induct n arbitrary: S)
apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
apply simp
-apply (metis Collect_mem_eq DiffE infinite_remove)
+apply (metis DiffE infinite_remove)
done
declare enumerate_0 [simp del] enumerate_Suc [simp del]
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Tue Aug 23 15:46:53 2011 -0700
@@ -20,12 +20,18 @@
val rat_1 = Rat.one;
val rat_2 = Rat.two;
val rat_10 = Rat.rat_of_int 10;
+(*
val rat_1_2 = rat_1 // rat_2;
+*)
val max = Integer.max;
+(*
val min = Integer.min;
+*)
val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
+(*
val numerator_rat = Rat.quotient_of_rat #> fst #> Rat.rat_of_int;
+*)
fun int_of_rat a =
case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int";
fun lcm_rat x y = Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
@@ -99,7 +105,7 @@
type matrix = (int*int)*(Rat.rat FuncUtil.Intpairfunc.table);
-fun iszero (k,r) = r =/ rat_0;
+fun iszero (_,r) = r =/ rat_0;
(* Vectors. Conventionally indexed 1..n. *)
@@ -108,11 +114,13 @@
fun dim (v:vector) = fst v;
+(*
fun vector_const c n =
if c =/ rat_0 then vector_0 n
else (n,fold_rev (fn k => FuncUtil.Intfunc.update (k,c)) (1 upto n) FuncUtil.Intfunc.empty) :vector;
val vector_1 = vector_const rat_1;
+*)
fun vector_cmul c (v:vector) =
let val n = dim v
@@ -120,6 +128,7 @@
else (n,FuncUtil.Intfunc.map (fn _ => fn x => c */ x) (snd v))
end;
+(*
fun vector_neg (v:vector) = (fst v,FuncUtil.Intfunc.map (K Rat.neg) (snd v)) :vector;
fun vector_add (v1:vector) (v2:vector) =
@@ -135,9 +144,10 @@
let val m = dim v1
val n = dim v2
in if m <> n then error "vector_dot: incompatible dimensions"
- else FuncUtil.Intfunc.fold (fn (i,x) => fn a => x +/ a)
+ else FuncUtil.Intfunc.fold (fn (_,x) => fn a => x +/ a)
(FuncUtil.Intfunc.combine (curry op */) (fn x => x =/ rat_0) (snd v1) (snd v2)) rat_0
end;
+*)
fun vector_of_list l =
let val n = length l
@@ -146,10 +156,13 @@
(* Matrices; again rows and columns indexed from 1. *)
+(*
fun matrix_0 (m,n) = ((m,n),FuncUtil.Intpairfunc.empty):matrix;
+*)
fun dimensions (m:matrix) = fst m;
+(*
fun matrix_const c (mn as (m,n)) =
if m <> n then error "matrix_const: needs to be square"
else if c =/ rat_0 then matrix_0 mn
@@ -175,15 +188,17 @@
end;;
fun matrix_sub m1 m2 = matrix_add m1 (matrix_neg m2);
+*)
fun row k (m:matrix) =
- let val (i,j) = dimensions m
+ let val (_,j) = dimensions m
in (j,
FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => if i = k then FuncUtil.Intfunc.update (j,c) a else a) (snd m) FuncUtil.Intfunc.empty ) : vector
end;
+(*
fun column k (m:matrix) =
- let val (i,j) = dimensions m
+ let val (i,_) = dimensions m
in (i,
FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => if j = k then FuncUtil.Intfunc.update (i,c) a else a) (snd m) FuncUtil.Intfunc.empty)
: vector
@@ -207,6 +222,7 @@
in ((m,n),itern 1 l (fn v => fn i => itern 1 v (fn c => fn j => FuncUtil.Intpairfunc.update ((i,j), c))) FuncUtil.Intpairfunc.empty)
end
end;
+*)
(* Monomials. *)
@@ -220,6 +236,7 @@
val monomial_mul =
FuncUtil.Ctermfunc.combine Integer.add (K false);
+(*
fun monomial_pow m k =
if k = 0 then monomial_1
else FuncUtil.Ctermfunc.map (fn _ => fn x => k * x) m;
@@ -230,7 +247,7 @@
fun monomial_div m1 m2 =
let val m = FuncUtil.Ctermfunc.combine Integer.add
(fn x => x = 0) m1 (FuncUtil.Ctermfunc.map (fn _ => fn x => ~ x) m2)
- in if FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k >= 0 andalso a) m true then m
+ in if FuncUtil.Ctermfunc.fold (fn (_, k) => fn a => k >= 0 andalso a) m true then m
else error "monomial_div: non-divisible"
end;
@@ -240,9 +257,10 @@
fun monomial_lcm m1 m2 =
fold_rev (fn x => FuncUtil.Ctermfunc.update (x, max (monomial_degree x m1) (monomial_degree x m2)))
(union (is_equal o FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1) (FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty);
+*)
fun monomial_multidegree m =
- FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k + a) m 0;;
+ FuncUtil.Ctermfunc.fold (fn (_, k) => fn a => k + a) m 0;;
fun monomial_variables m = FuncUtil.Ctermfunc.dom m;;
@@ -254,7 +272,7 @@
val poly_0 = FuncUtil.Monomialfunc.empty;
fun poly_isconst p =
- FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => FuncUtil.Ctermfunc.is_empty m andalso a) p true;
+ FuncUtil.Monomialfunc.fold (fn (m, _) => fn a => FuncUtil.Ctermfunc.is_empty m andalso a) p true;
fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x,rat_1);
@@ -281,6 +299,7 @@
fun poly_mul p1 p2 =
FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => poly_add (poly_cmmul (c,m) p2) a) p1 poly_0;
+(*
fun poly_div p1 p2 =
if not(poly_isconst p2)
then error "poly_div: non-constant" else
@@ -288,6 +307,7 @@
in if c =/ rat_0 then error "poly_div: division by zero"
else poly_cmul (Rat.inv c) p1
end;
+*)
fun poly_square p = poly_mul p p;
@@ -297,22 +317,25 @@
else let val q = poly_square(poly_pow p (k div 2)) in
if k mod 2 = 1 then poly_mul p q else q end;
+(*
fun poly_exp p1 p2 =
if not(poly_isconst p2)
then error "poly_exp: not a constant"
else poly_pow p1 (int_of_rat (eval FuncUtil.Ctermfunc.empty p2));
fun degree x p =
- FuncUtil.Monomialfunc.fold (fn (m,c) => fn a => max (monomial_degree x m) a) p 0;
+ FuncUtil.Monomialfunc.fold (fn (m,_) => fn a => max (monomial_degree x m) a) p 0;
+*)
fun multidegree p =
- FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => max (monomial_multidegree m) a) p 0;
+ FuncUtil.Monomialfunc.fold (fn (m, _) => fn a => max (monomial_multidegree m) a) p 0;
fun poly_variables p =
- sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => union (is_equal o FuncUtil.cterm_ord) (monomial_variables m)) p []);;
+ sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, _) => union (is_equal o FuncUtil.cterm_ord) (monomial_variables m)) p []);;
(* Order monomials for human presentation. *)
+(*
val humanorder_varpow = prod_ord FuncUtil.cterm_ord (rev_order o int_ord);
local
@@ -328,9 +351,11 @@
ord (sort humanorder_varpow (FuncUtil.Ctermfunc.dest m1),
sort humanorder_varpow (FuncUtil.Ctermfunc.dest m2))
end;
+*)
(* Conversions to strings. *)
+(*
fun string_of_vector min_size max_size (v:vector) =
let val n_raw = dim v
in if n_raw = 0 then "[]" else
@@ -394,6 +419,7 @@
val s2 = String.substring (s, 3, String.size s - 3)
in "<<" ^(if s1 = " + " then s2 else "-"^s2)^">>"
end;
+*)
(* Conversion from HOL term. *)
@@ -407,7 +433,9 @@
val pow_tm = @{cterm "op ^ :: real => _"}
val zero_tm = @{cterm "0:: real"}
val is_numeral = can (HOLogic.dest_number o term_of)
+(*
fun is_comb t = case t of _$_ => true | _ => false
+*)
fun poly_of_term tm =
if tm aconvc zero_tm then poly_0
else if RealArith.is_ratconst tm
@@ -466,6 +494,7 @@
(* String for block diagonal matrix numbered k. *)
+(*
fun sdpa_of_blockdiagonal k m =
let
val pfx = string_of_int k ^" "
@@ -476,9 +505,11 @@
pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
" " ^ decimalize 20 c ^ "\n" ^ a) entss ""
end;
+*)
(* String for a matrix numbered k, in SDPA sparse format. *)
+(*
fun sdpa_of_matrix k (m:matrix) =
let
val pfx = string_of_int k ^ " 1 "
@@ -488,6 +519,7 @@
pfx ^ string_of_int i ^ " " ^ string_of_int j ^
" " ^ decimalize 20 c ^ "\n" ^ a) mss ""
end;;
+*)
(* ------------------------------------------------------------------------- *)
(* String in SDPA sparse format for standard SDP problem: *)
@@ -496,6 +528,7 @@
(* Minimize obj_1 * v_1 + ... obj_m * v_m *)
(* ------------------------------------------------------------------------- *)
+(*
fun sdpa_of_problem obj mats =
let
val m = length mats - 1
@@ -507,6 +540,7 @@
sdpa_of_vector obj ^
fold_rev2 (fn k => fn m => fn a => sdpa_of_matrix (k - 1) m ^ a) (1 upto length mats) mats ""
end;
+*)
fun index_char str chr pos =
if pos >= String.size str then ~1
@@ -523,14 +557,18 @@
end
end;
+(*
fun isspace x = (x = " ");
+*)
fun isnum x = member (op =) ["0","1","2","3","4","5","6","7","8","9"] x;
(* More parser basics. *)
+(*
val word = Scan.this_string
fun token s =
Scan.repeat ($$ " ") |-- word s --| Scan.repeat ($$ " ")
+*)
val numeral = Scan.one isnum
val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
val decimalfrac = Scan.repeat1 numeral
@@ -558,7 +596,7 @@
(* Parse back csdp output. *)
- fun ignore inp = ((),[])
+ fun ignore _ = ((),[])
fun csdpoutput inp =
((decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) >>
(fn (h,to) => map_filter I ((SOME h)::to))) --| ignore >> vector_of_list) inp
@@ -566,8 +604,10 @@
(* Run prover on a problem in linear form. *)
+(*
fun run_problem prover obj mats =
parse_csdpoutput (prover (sdpa_of_problem obj mats))
+*)
(* Try some apparently sensible scaling first. Note that this is purely to *)
(* get a cleaner translation to floating-point, and doesn't affect any of *)
@@ -575,6 +615,7 @@
(* are extreme numbers in the original problem. *)
(* Version for (int*int) keys *)
+(*
local
fun max_rat x y = if x </ y then y else x
fun common_denominator fld amat acc =
@@ -600,6 +641,7 @@
in solver obj'' mats''
end
end;
+*)
(* Try some apparently sensible scaling first. Note that this is purely to *)
(* get a cleaner translation to floating-point, and doesn't affect any of *)
@@ -610,9 +652,9 @@
local
fun max_rat x y = if x </ y then y else x
fun common_denominator fld amat acc =
- fld (fn (m,c) => fn a => lcm_rat (denominator_rat c) a) amat acc
+ fld (fn (_,c) => fn a => lcm_rat (denominator_rat c) a) amat acc
fun maximal_element fld amat acc =
- fld (fn (m,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc
+ fld (fn (_,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc
fun float_of_rat x = let val (a,b) = Rat.quotient_of_rat x
in Real.fromInt a / Real.fromInt b end;
fun int_of_float x = (trunc x handle Overflow => 0 | Domain => 0)
@@ -661,6 +703,7 @@
(* assignments for the others in terms of them. We give one pseudo-variable *)
(* "one" that's used for a constant term. *)
+(*
local
fun extract_first p l = case l of (* FIXME : use find_first instead *)
[] => error "extract_first"
@@ -686,10 +729,11 @@
fun tri_eliminate_equations one vars eqs =
let
val assig = eliminate vars Inttriplefunc.empty eqs
- val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
+ val vs = Inttriplefunc.fold (fn (_, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
in (distinct (dest_ord triple_int_ord) vs, assig)
end
end;
+*)
(* Eliminate all variables, in an essentially arbitrary order. *)
@@ -723,13 +767,14 @@
in fn eqs =>
let
val assig = eliminate Inttriplefunc.empty eqs
- val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
+ val vs = Inttriplefunc.fold (fn (_, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
in (distinct (dest_ord triple_int_ord) vs,assig)
end
end;
(* Solve equations by assigning arbitrary numbers. *)
+(*
fun tri_solve_equations one eqs =
let
val (vars,assigs) = tri_eliminate_all_equations one eqs
@@ -741,6 +786,7 @@
in if forall (fn e => tri_equation_eval ass e =/ rat_0) eqs
then Inttriplefunc.delete_safe one ass else raise Sanity
end;
+*)
(* Multiply equation-parametrized poly by regular poly and add accumulator. *)
@@ -754,6 +800,7 @@
(* Usual operations on equation-parametrized poly. *)
+(*
fun tri_epoly_cmul c l =
if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (K (tri_equation_cmul c)) l;;
@@ -762,9 +809,11 @@
val tri_epoly_add = Inttriplefunc.combine tri_equation_add Inttriplefunc.is_empty;
fun tri_epoly_sub p q = tri_epoly_add p (tri_epoly_neg q);;
+*)
(* Stuff for "equations" ((int*int)->num functions). *)
+(*
fun pi_equation_cmul c eq =
if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (fn _ => fn d => c */ d) eq;
@@ -774,11 +823,13 @@
let fun value v = Inttriplefunc.apply assig v
in Inttriplefunc.fold (fn (v, c) => fn a => a +/ value v */ c) eq rat_0
end;
+*)
(* Eliminate among linear equations: return unconstrained variables and *)
(* assignments for the others in terms of them. We give one pseudo-variable *)
(* "one" that's used for a constant term. *)
+(*
local
fun extract_first p l = case l of
[] => error "extract_first"
@@ -804,13 +855,15 @@
fun pi_eliminate_equations one vars eqs =
let
val assig = eliminate vars Inttriplefunc.empty eqs
- val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
+ val vs = Inttriplefunc.fold (fn (_, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
in (distinct (dest_ord triple_int_ord) vs, assig)
end
end;
+*)
(* Eliminate all variables, in an essentially arbitrary order. *)
+(*
fun pi_eliminate_all_equations one =
let
fun choose_variable eq =
@@ -841,13 +894,15 @@
in fn eqs =>
let
val assig = eliminate Inttriplefunc.empty eqs
- val vs = Inttriplefunc.fold (fn (x, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
+ val vs = Inttriplefunc.fold (fn (_, f) => fn a => remove (dest_ord triple_int_ord) one (Inttriplefunc.dom f) @ a) assig []
in (distinct (dest_ord triple_int_ord) vs,assig)
end
end;
+*)
(* Solve equations by assigning arbitrary numbers. *)
+(*
fun pi_solve_equations one eqs =
let
val (vars,assigs) = pi_eliminate_all_equations one eqs
@@ -859,9 +914,11 @@
in if forall (fn e => pi_equation_eval ass e =/ rat_0) eqs
then Inttriplefunc.delete_safe one ass else raise Sanity
end;
+*)
(* Multiply equation-parametrized poly by regular poly and add accumulator. *)
+(*
fun pi_epoly_pmul p q acc =
FuncUtil.Monomialfunc.fold (fn (m1, c) => fn a =>
FuncUtil.Monomialfunc.fold (fn (m2,e) => fn b =>
@@ -869,9 +926,11 @@
val es = FuncUtil.Monomialfunc.tryapplyd b m Inttriplefunc.empty
in FuncUtil.Monomialfunc.update (m,pi_equation_add (pi_equation_cmul c e) es) b
end) q a) p acc ;
+*)
(* Usual operations on equation-parametrized poly. *)
+(*
fun pi_epoly_cmul c l =
if c =/ rat_0 then Inttriplefunc.empty else Inttriplefunc.map (K (pi_equation_cmul c)) l;;
@@ -882,6 +941,7 @@
fun pi_epoly_sub p q = pi_epoly_add p (pi_epoly_neg q);;
fun allpairs f l1 l2 = fold_rev (fn x => (curry (op @)) (map (f x) l2)) l1 [];
+*)
(* Hence produce the "relevant" monomials: those whose squares lie in the *)
(* Newton polytope of the monomials in the input. (This is enough according *)
@@ -930,17 +990,20 @@
end
end;
+(*
fun gcd_rat a b = Rat.rat_of_int (Integer.gcd (int_of_rat a) (int_of_rat b));
+*)
(* Adjust a diagonalization to collect rationals at the start. *)
(* FIXME : Potentially polymorphic keys, but here only: integers!! *)
+(*
local
fun upd0 x y a = if y =/ rat_0 then a else FuncUtil.Intfunc.update(x,y) a;
fun mapa f (d,v) =
(d, FuncUtil.Intfunc.fold (fn (i,c) => fn a => upd0 i (f c) a) v FuncUtil.Intfunc.empty)
fun adj (c,l) =
let val a =
- FuncUtil.Intfunc.fold (fn (i,c) => fn a => lcm_rat a (denominator_rat c))
+ FuncUtil.Intfunc.fold (fn (_,c) => fn a => lcm_rat a (denominator_rat c))
(snd l) rat_1 //
FuncUtil.Intfunc.fold (fn (i,c) => fn a => gcd_rat a (numerator_rat c))
(snd l) rat_0
@@ -954,6 +1017,7 @@
in ((rat_1 // a),map (fn (c,l) => (a */ c,l)) d')
end
end;
+*)
(* Enumeration of monomials with given multidegree bound. *)
@@ -1031,7 +1095,9 @@
else Inttriplefunc.map (fn _ => fn x => c */ x) bm;
val bmatrix_neg = bmatrix_cmul (Rat.rat_of_int ~1);
+(*
fun bmatrix_sub m1 m2 = bmatrix_add m1 (bmatrix_neg m2);;
+*)
(* Smash a block matrix into components. *)
@@ -1039,14 +1105,14 @@
map (fn (bs,b0) =>
let val m = Inttriplefunc.fold
(fn ((b,i,j),c) => fn a => if b = b0 then FuncUtil.Intpairfunc.update ((i,j),c) a else a) bm FuncUtil.Intpairfunc.empty
- val d = FuncUtil.Intpairfunc.fold (fn ((i,j),c) => fn a => max a (max i j)) m 0
+ val _ = FuncUtil.Intpairfunc.fold (fn ((i,j),_) => fn a => max a (max i j)) m 0
in (((bs,bs),m):matrix) end)
(blocksizes ~~ (1 upto length blocksizes));;
(* FIXME : Get rid of this !!!*)
local
- fun tryfind_with msg f [] = raise Failure msg
- | tryfind_with msg f (x::xs) = (f x handle Failure s => tryfind_with s f xs);
+ fun tryfind_with msg _ [] = raise Failure msg
+ | tryfind_with _ f (x::xs) = (f x handle Failure s => tryfind_with s f xs);
in
fun tryfind f = tryfind_with "tryfind" f
end
@@ -1060,7 +1126,7 @@
(pol :: eqs @ map fst leqs) []
val monoid = if linf then
(poly_const rat_1,RealArith.Rational_lt rat_1)::
- (filter (fn (p,c) => multidegree p <= d) leqs)
+ (filter (fn (p,_) => multidegree p <= d) leqs)
else enumerate_products d leqs
val nblocks = length monoid
fun mk_idmultiplier k p =
@@ -1072,7 +1138,7 @@
fold_rev (fn (m,n) => FuncUtil.Monomialfunc.update(m,Inttriplefunc.onefunc((~k,~n,n),rat_1))) nons FuncUtil.Monomialfunc.empty)
end
- fun mk_sqmultiplier k (p,c) =
+ fun mk_sqmultiplier k (p,_) =
let
val e = (d - multidegree p) div 2
val mons = enumerate_monomials e vars
@@ -1091,13 +1157,13 @@
end
val (sqmonlist,sqs) = split_list (map2 mk_sqmultiplier (1 upto length monoid) monoid)
- val (idmonlist,ids) = split_list(map2 mk_idmultiplier (1 upto length eqs) eqs)
+ val (_(*idmonlist*),ids) = split_list(map2 mk_idmultiplier (1 upto length eqs) eqs)
val blocksizes = map length sqmonlist
val bigsum =
fold_rev2 (fn p => fn q => fn a => tri_epoly_pmul p q a) eqs ids
- (fold_rev2 (fn (p,c) => fn s => fn a => tri_epoly_pmul p s a) monoid sqs
+ (fold_rev2 (fn (p,_) => fn s => fn a => tri_epoly_pmul p s a) monoid sqs
(epoly_of_poly(poly_neg pol)))
- val eqns = FuncUtil.Monomialfunc.fold (fn (m,e) => fn a => e::a) bigsum []
+ val eqns = FuncUtil.Monomialfunc.fold (fn (_,e) => fn a => e::a) bigsum []
val (pvs,assig) = tri_eliminate_all_equations (0,0,0) eqns
val qvars = (0,0,0)::pvs
val allassig = fold_rev (fn v => Inttriplefunc.update(v,(Inttriplefunc.onefunc(v,rat_1)))) pvs assig
@@ -1119,7 +1185,7 @@
FuncUtil.Intfunc.empty)
val raw_vec = if null pvs then vector_0 0
else tri_scale_then (run_blockproblem prover nblocks blocksizes) obj mats
- fun int_element (d,v) i = FuncUtil.Intfunc.tryapplyd v i rat_0
+ fun int_element (_,v) i = FuncUtil.Intfunc.tryapplyd v i rat_0
fun find_rounding d =
let
@@ -1154,10 +1220,10 @@
end
val sqs = map2 mk_sos sqmonlist ratdias
val cfs = map poly_of_epoly ids
- val msq = filter (fn (a,b) => not (null b)) (map2 pair monoid sqs)
+ val msq = filter (fn (_,b) => not (null b)) (map2 pair monoid sqs)
fun eval_sq sqs = fold_rev (fn (c,q) => poly_add (poly_cmul c (poly_mul q q))) sqs poly_0
val sanity =
- fold_rev (fn ((p,c),s) => poly_add (poly_mul p (eval_sq s))) msq
+ fold_rev (fn ((p,_),s) => poly_add (poly_mul p (eval_sq s))) msq
(fold_rev2 (fn p => fn q => poly_add (poly_mul p q)) cfs eqs
(poly_neg pol))
@@ -1189,11 +1255,11 @@
(* FIXME: Replace tryfind by get_first !! *)
fun real_nonlinear_prover proof_method ctxt =
let
- val {add,mul,neg,pow,sub,main} = Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
+ val {add = _, mul = _, neg = _, pow = _,
+ sub = _, main = real_poly_conv} =
+ Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
(the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
- val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
- real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
fun mainf cert_choice translator (eqs,les,lts) =
let
val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs
@@ -1244,9 +1310,9 @@
(poly_neg(poly_pow pol i))))
(0 upto k)
end
- val (d,i,(cert_ideal,cert_cone)) = deepen tryall 0
+ val (_,i,(cert_ideal,cert_cone)) = deepen tryall 0
val proofs_ideal =
- map2 (fn q => fn (p,ax) => RealArith.Eqmul(q,ax)) cert_ideal eq
+ map2 (fn q => fn (_,ax) => RealArith.Eqmul(q,ax)) cert_ideal eq
val proofs_cone = map cterm_of_sos cert_cone
val proof_ne = if null ltp then RealArith.Rational_lt Rat.one else
let val p = foldr1 RealArith.Product (map snd ltp)
@@ -1283,10 +1349,10 @@
fun substitutable_monomial fvs tm = case term_of tm of
Free(_,@{typ real}) => if not (member (op aconvc) fvs tm) then (Rat.one,tm)
else raise Failure "substitutable_monomial"
- | @{term "op * :: real => _"}$c$(t as Free _ ) =>
+ | @{term "op * :: real => _"}$_$(Free _) =>
if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso not (member (op aconvc) fvs (Thm.dest_arg tm))
then (RealArith.dest_ratconst (Thm.dest_arg1 tm),Thm.dest_arg tm) else raise Failure "substitutable_monomial"
- | @{term "op + :: real => _"}$s$t =>
+ | @{term "op + :: real => _"}$_$_ =>
(substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
handle Failure _ => substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
| _ => raise Failure "substitutable_monomial"
@@ -1295,7 +1361,7 @@
let val w = Thm.dest_arg1 (cprop_of th)
in if v aconvc w then th
else case term_of w of
- @{term "op + :: real => _"}$s$t =>
+ @{term "op + :: real => _"}$_$_ =>
if Thm.dest_arg1 w aconvc v then shuffle2 th
else isolate_variable v (shuffle1 th)
| _ => error "isolate variable : This should not happen?"
@@ -1304,13 +1370,12 @@
fun real_nonlinear_subst_prover prover ctxt =
let
- val {add,mul,neg,pow,sub,main} = Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
+ val {add = _, mul = real_poly_mul_conv, neg = _,
+ pow = _, sub = _, main = real_poly_conv} =
+ Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
(the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
- val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
- real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
-
fun make_substitution th =
let
val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th))
@@ -1390,11 +1455,11 @@
val _ = print_cert certificates
in rtac ths 1 end)
-fun default_SOME f NONE v = SOME v
- | default_SOME f (SOME v) _ = SOME v;
+fun default_SOME _ NONE v = SOME v
+ | default_SOME _ (SOME v) _ = SOME v;
fun lift_SOME f NONE a = f a
- | lift_SOME f (SOME a) _ = SOME a;
+ | lift_SOME _ (SOME a) _ = SOME a;
local
--- a/src/HOL/Library/positivstellensatz.ML Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Tue Aug 23 15:46:53 2011 -0700
@@ -204,10 +204,12 @@
@{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and
"(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+};
+(*
val nnfD_simps =
@{lemma "((~(P & Q)) = (~P | ~Q))" and "((~(P | Q)) = (~P & ~Q) )" and
"((P --> Q) = (~P | Q) )" and "((P = Q) = ((P & Q) | (~P & ~ Q)))" and
"((~(P = Q)) = ((P & ~ Q) | (~P & Q)) )" and "((~ ~(P)) = P)" by blast+};
+*)
val choice_iff = @{lemma "(ALL x. EX y. P x y) = (EX f. ALL x. P x (f x))" by metis};
val prenex_simps =
@@ -293,16 +295,18 @@
| _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
fun is_ratconst t = can dest_ratconst t
+(*
fun find_term p t = if p t then t else
case t of
a$b => (find_term p a handle TERM _ => find_term p b)
| Abs (_,_,t') => find_term p t'
| _ => raise TERM ("find_term",[t]);
+*)
fun find_cterm p t = if p t then t else
case term_of t of
- a$b => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
- | Abs (_,_,t') => find_cterm p (Thm.dest_abs NONE t |> snd)
+ _$_ => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
+ | Abs (_,_,_) => find_cterm p (Thm.dest_abs NONE t |> snd)
| _ => raise CTERM ("find_cterm",[t]);
(* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
@@ -477,7 +481,7 @@
val strip_exists =
let fun h (acc, t) =
case (term_of t) of
- Const(@{const_name Ex},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+ Const(@{const_name Ex},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
@@ -512,7 +516,7 @@
val strip_forall =
let fun h (acc, t) =
case (term_of t) of
- Const(@{const_name All},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+ Const(@{const_name All},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
@@ -725,7 +729,7 @@
fun gen_prover_real_arith ctxt prover =
let
fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
- val {add,mul,neg,pow,sub,main} =
+ val {add, mul, neg, pow = _, sub = _, main} =
Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
(the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Aug 23 15:46:53 2011 -0700
@@ -533,7 +533,7 @@
case False hence "t = {}" using `finite t` by auto
show ?thesis
proof (cases "s = {}")
- have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" by (auto intro: ext)
+ have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" by auto
case True thus ?thesis using `t = {}` by (auto simp: *)
next
case False thus ?thesis using `t = {}` by simp
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Aug 23 15:46:53 2011 -0700
@@ -831,7 +831,7 @@
have IU: " (UNIV :: (real^'m) set) \<subseteq> span ?I" by blast
from linear_eq[OF lf lg IU] fg x
have "f x = g x" unfolding Ball_def mem_Collect_eq by metis}
- then show ?thesis by (auto intro: ext)
+ then show ?thesis by auto
qed
lemma bilinear_eq_stdbasis_cart:
@@ -841,7 +841,7 @@
shows "f = g"
proof-
from fg have th: "\<forall>x \<in> {cart_basis i| i. i\<in> (UNIV :: 'm set)}. \<forall>y\<in> {cart_basis j |j. j \<in> (UNIV :: 'n set)}. f x y = g x y" by blast
- from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by (blast intro: ext)
+ from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by blast
qed
lemma left_invertible_transpose:
@@ -1102,11 +1102,6 @@
lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
by (simp add: Collect_all_eq closed_INT closed_Collect_le)
-lemma Lim_component_cart:
- fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
- shows "(f ---> l) net \<Longrightarrow> ((\<lambda>a. f a $i) ---> l$i) net"
- by (intro tendsto_intros)
-
lemma bounded_component_cart: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x $ i) ` s)"
unfolding bounded_def
apply clarify
@@ -2006,4 +2001,8 @@
apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
+text {* Legacy theorem names *}
+
+lemmas Lim_component_cart = tendsto_vec_nth
+
end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Aug 23 15:46:53 2011 -0700
@@ -96,11 +96,7 @@
unfolding subspace_def by auto
lemma span_eq[simp]: "(span s = s) <-> subspace s"
-proof-
- { fix f assume "Ball f subspace"
- hence "subspace (Inter f)" using subspace_Inter[of f] unfolding Ball_def by auto }
- thus ?thesis using hull_eq[of subspace s] span_def by auto
-qed
+ unfolding span_def by (rule hull_eq, rule subspace_Inter)
lemma basis_inj_on: "d \<subseteq> {..<DIM('n)} \<Longrightarrow> inj_on (basis :: nat => 'n::euclidean_space) d"
by(auto simp add: inj_on_def euclidean_eq[where 'a='n])
@@ -291,8 +287,6 @@
shows "scaleR 2 x = x + x"
unfolding one_add_one_is_two [symmetric] scaleR_left_distrib by simp
-declare euclidean_simps[simp]
-
lemma vector_choose_size: "0 <= c ==> \<exists>(x::'a::euclidean_space). norm x = c"
apply (rule exI[where x="c *\<^sub>R basis 0 ::'a"]) using DIM_positive[where 'a='a] by auto
@@ -973,7 +967,7 @@
lemma convex_box: fixes a::"'a::euclidean_space"
assumes "\<And>i. i<DIM('a) \<Longrightarrow> convex {x. P i x}"
shows "convex {x. \<forall>i<DIM('a). P i (x$$i)}"
- using assms unfolding convex_def by(auto simp add:euclidean_simps)
+ using assms unfolding convex_def by auto
lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\<forall>i<DIM('a). 0 \<le> x$$i)}"
by (rule convex_box) (simp add: atLeast_def[symmetric] convex_real_interval)
@@ -1641,7 +1635,7 @@
hence "V <= affine hull T" using B_def assms translation_inverse_subset[of a V "span B"] by auto
moreover have "T<=V" using T_def B_def a_def assms by auto
ultimately have "affine hull T = affine hull V"
- by (metis Int_absorb1 Int_absorb2 Int_commute Int_lower2 assms hull_hull hull_mono)
+ by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono)
moreover have "S<=T" using T_def B_def translation_inverse_subset[of a "S-{a}" B] by auto
moreover have "~(affine_dependent T)" using T_def affine_dependent_translation_eq[of "insert 0 B"] affine_dependent_imp_dependent2 B_def by auto
ultimately show ?thesis using `T<=V` by auto
@@ -1675,7 +1669,7 @@
lemma affine_hull_nonempty: "(S ~= {}) <-> affine hull S ~= {}"
proof-
-fix S have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto
+have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto
moreover have "affine hull S = {} ==> S = {}" unfolding hull_def by auto
ultimately show "(S ~= {}) <-> affine hull S ~= {}" by blast
qed
@@ -2076,7 +2070,7 @@
apply (simp add: rel_interior, safe)
apply (force simp add: open_contains_ball)
apply (rule_tac x="ball x e" in exI)
- apply (simp add: centre_in_ball)
+ apply simp
done
lemma rel_interior_ball:
@@ -2087,7 +2081,7 @@
apply (simp add: rel_interior, safe)
apply (force simp add: open_contains_cball)
apply (rule_tac x="ball x e" in exI)
- apply (simp add: open_ball centre_in_ball subset_trans [OF ball_subset_cball])
+ apply (simp add: subset_trans [OF ball_subset_cball])
apply auto
done
@@ -3370,7 +3364,7 @@
hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis 0" in ballE) defer
apply(erule_tac x="basis 0" in ballE)
unfolding Ball_def mem_cball dist_norm using DIM_positive[where 'a='a]
- by(auto simp add:norm_basis[unfolded One_nat_def])
+ by auto
case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI)
apply(rule) apply(rule divide_pos_pos) prefer 3 apply(rule,rule,erule conjE)
unfolding norm_zero scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel proof-
@@ -3508,7 +3502,7 @@
hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: field_simps)
hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) }
ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
- using as(3-) DIM_positive[where 'a='a] by(auto simp add:euclidean_simps) qed
+ using as(3-) DIM_positive[where 'a='a] by auto qed
lemma is_interval_connected:
fixes s :: "('a::euclidean_space) set"
@@ -3570,7 +3564,7 @@
shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
apply(subst neg_equal_iff_equal[THEN sym])
using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] using assms using continuous_on_neg
- by (auto simp add:euclidean_simps)
+ by auto
lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
@@ -3624,18 +3618,18 @@
by auto
next let ?y = "\<lambda>j. if x$$j = 0 then 0 else (x$$j - x$$i) / (1 - x$$i)"
case False hence *:"x = x$$i *\<^sub>R (\<chi>\<chi> j. if x$$j = 0 then 0 else 1) + (1 - x$$i) *\<^sub>R (\<chi>\<chi> j. ?y j)"
- apply(subst euclidean_eq) by(auto simp add: field_simps euclidean_simps)
+ apply(subst euclidean_eq) by(auto simp add: field_simps)
{ fix j assume j:"j<DIM('a)"
have "x$$j \<noteq> 0 \<Longrightarrow> 0 \<le> (x $$ j - x $$ i) / (1 - x $$ i)" "(x $$ j - x $$ i) / (1 - x $$ i) \<le> 1"
apply(rule_tac divide_nonneg_pos) using i(1)[of j] using False i01
using Suc(2)[unfolded mem_interval, rule_format, of j] using j
- by(auto simp add:field_simps euclidean_simps)
+ by(auto simp add:field_simps)
hence "0 \<le> ?y j \<and> ?y j \<le> 1" by auto }
moreover have "i\<in>{j. j<DIM('a) \<and> x$$j \<noteq> 0} - {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0}"
using i01 using i'(3) by auto
hence "{j. j<DIM('a) \<and> x$$j \<noteq> 0} \<noteq> {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0}" using i'(3) by blast
hence **:"{j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0} \<subset> {j. j<DIM('a) \<and> x$$j \<noteq> 0}" apply - apply rule
- by( auto simp add:euclidean_simps)
+ by auto
have "card {j. j<DIM('a) \<and> ((\<chi>\<chi> j. ?y j)::'a) $$ j \<noteq> 0} \<le> n"
using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto
ultimately show ?thesis apply(subst *) apply(rule convex_convex_hull[unfolded convex_def, rule_format])
@@ -3671,14 +3665,14 @@
fix y assume as:"y\<in>{x - ?d .. x + ?d}"
{ fix i assume i:"i<DIM('a)" have "x $$ i \<le> d + y $$ i" "y $$ i \<le> d + x $$ i"
using as[unfolded mem_interval, THEN spec[where x=i]] i
- by(auto simp add:euclidean_simps)
+ by auto
hence "1 \<ge> inverse d * (x $$ i - y $$ i)" "1 \<ge> inverse d * (y $$ i - x $$ i)"
apply(rule_tac[!] mult_left_le_imp_le[OF _ assms]) unfolding mult_assoc[THEN sym]
using assms by(auto simp add: field_simps)
hence "inverse d * (x $$ i * 2) \<le> 2 + inverse d * (y $$ i * 2)"
"inverse d * (y $$ i * 2) \<le> 2 + inverse d * (x $$ i * 2)" by(auto simp add:field_simps) }
hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..\<chi>\<chi> i.1}" unfolding mem_interval using assms
- by(auto simp add: euclidean_simps field_simps)
+ by(auto simp add: field_simps)
thus "\<exists>z\<in>{0..\<chi>\<chi> i.1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
using assms by auto
next
@@ -3688,7 +3682,7 @@
apply rule apply(rule mult_nonneg_nonneg) prefer 3 apply(rule mult_right_le_one_le)
using assms by auto
thus "y \<in> {x - ?d..x + ?d}" unfolding as(2) mem_interval apply- apply rule using as(1)[unfolded mem_interval]
- apply(erule_tac x=i in allE) using assms by(auto simp add: euclidean_simps) qed
+ apply(erule_tac x=i in allE) using assms by auto qed
obtain s where "finite s" "{0::'a..\<chi>\<chi> i.1} = convex hull s" using unit_cube_convex_hull by auto
thus ?thesis apply(rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"]) unfolding * and convex_hull_affinity by auto qed
@@ -3774,7 +3768,7 @@
have "0 < d" unfolding d_def using `e>0` dimge1 by(rule_tac divide_pos_pos, auto)
let ?d = "(\<chi>\<chi> i. d)::'a"
obtain c where c:"finite c" "{x - ?d..x + ?d} = convex hull c" using cube_convex_hull[OF `d>0`, of x] by auto
- have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by(auto simp add:euclidean_simps)
+ have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by auto
hence "c\<noteq>{}" using c by auto
def k \<equiv> "Max (f ` c)"
have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)])
@@ -3783,7 +3777,7 @@
have e:"e = setsum (\<lambda>i. d) {..<DIM('a)}" unfolding setsum_constant d_def using dimge1
unfolding real_eq_of_nat by auto
show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
- using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:euclidean_simps) qed
+ using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed
hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
unfolding k_def apply(rule, rule Max_ge) using c(1) by auto
have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 by auto
@@ -3792,9 +3786,9 @@
hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof
fix y assume y:"y\<in>cball x d"
{ fix i assume "i<DIM('a)" hence "x $$ i - d \<le> y $$ i" "y $$ i \<le> x $$ i + d"
- using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by(auto simp add:euclidean_simps) }
+ using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by auto }
thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm
- by(auto simp add:euclidean_simps) qed
+ by auto qed
hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
apply force
@@ -3929,10 +3923,10 @@
proof(rule,rule) fix i assume i:"i<DIM('a)"
have "((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $$ i =
((norm (a - b) - norm (a - x)) * (a $$ i) + norm (a - x) * (b $$ i)) / norm (a - b)"
- using Fal by(auto simp add: field_simps euclidean_simps)
+ using Fal by(auto simp add: field_simps)
also have "\<dots> = x$$i" apply(rule divide_eq_imp[OF Fal])
unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq] apply-
- apply(subst (asm) euclidean_eq) using i apply(erule_tac x=i in allE) by(auto simp add:field_simps euclidean_simps)
+ apply(subst (asm) euclidean_eq) using i apply(erule_tac x=i in allE) by(auto simp add:field_simps)
finally show "x $$ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $$ i"
by auto
qed(insert Fal2, auto) qed qed
@@ -3943,7 +3937,7 @@
proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by auto
show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
unfolding euclidean_eq[where 'a='a]
- by(auto simp add:field_simps euclidean_simps) qed
+ by(auto simp add:field_simps) qed
lemma between_mem_convex_hull:
"between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
@@ -3962,7 +3956,7 @@
have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
unfolding dist_norm unfolding norm_scaleR[THEN sym] apply(rule arg_cong[where f=norm]) using `e>0`
- by(auto simp add: euclidean_simps euclidean_eq[where 'a='a] field_simps)
+ by(auto simp add: euclidean_eq[where 'a='a] field_simps)
also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute)
@@ -4042,7 +4036,7 @@
apply(rule_tac x="\<lambda>y. inner y x" in exI) apply(rule,rule) unfolding mem_Collect_eq apply(erule exE)
using as(1) apply(erule_tac x=i in allE) unfolding sumbas apply safe unfolding not_less basis_zero
unfolding substdbasis_expansion_unique[OF assms] euclidean_component_def[THEN sym]
- using as(2,3) by(auto simp add:dot_basis not_less basis_zero)
+ using as(2,3) by(auto simp add:dot_basis not_less)
qed qed
lemma std_simplex:
@@ -4058,11 +4052,11 @@
fix x::"'a" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x<DIM('a). 0 \<le> xa $$ x) \<and> setsum (op $$ xa) {..<DIM('a)} \<le> 1"
show "(\<forall>xa<DIM('a). 0 < x $$ xa) \<and> setsum (op $$ x) {..<DIM('a)} < 1" apply(safe) proof-
fix i assume i:"i<DIM('a)" thus "0 < x $$ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
- unfolding dist_norm by(auto simp add: inner_simps euclidean_component_def dot_basis elim!:allE[where x=i])
+ unfolding dist_norm by (auto elim!:allE[where x=i])
next have **:"dist x (x + (e / 2) *\<^sub>R basis 0) < e" using `e>0`
unfolding dist_norm by(auto intro!: mult_strict_left_mono)
have "\<And>i. i<DIM('a) \<Longrightarrow> (x + (e / 2) *\<^sub>R basis 0) $$ i = x$$i + (if i = 0 then e/2 else 0)"
- unfolding euclidean_component_def by(auto simp add:inner_simps dot_basis)
+ by auto
hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)} = setsum (\<lambda>i. x$$i + (if 0 = i then e/2 else 0)) {..<DIM('a)}"
apply(rule_tac setsum_cong) by auto
have "setsum (op $$ x) {..<DIM('a)} < setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)}" unfolding * setsum_addf
@@ -4143,7 +4137,7 @@
setsum (\<lambda>i. x$$i + (if a = i then e/2 else 0)) d" by(rule_tac setsum_cong, auto)
have h1: "(ALL i<DIM('a). i ~: d --> (x + (e / 2) *\<^sub>R basis a) $$ i = 0)"
using as[THEN spec[where x="x + (e / 2) *\<^sub>R basis a"]] `a:d` using x0
- by(auto simp add: norm_basis elim:allE[where x=a])
+ by(auto elim:allE[where x=a])
have "setsum (op $$ x) d < setsum (op $$ (x + (e / 2) *\<^sub>R basis a)) d" unfolding * setsum_addf
using `0<e` `a:d` using `finite d` by(auto simp add: setsum_delta')
also have "\<dots> \<le> 1" using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R basis a"] by auto
@@ -4776,7 +4770,7 @@
} from this obtain mS where mS_def: "!S : I. (mS(S) > (1 :: real) &
(!e. (e>1 & e<=mS(S)) --> (1-e)*\<^sub>R x+ e *\<^sub>R z : S))" by metis
obtain e where e_def: "e=Min (mS ` I)" by auto
- have "e : (mS ` I)" using e_def assms `I ~= {}` by (simp add: Min_in)
+ have "e : (mS ` I)" using e_def assms `I ~= {}` by simp
hence "e>(1 :: real)" using mS_def by auto
moreover have "!S : I. e<=mS(S)" using e_def assms by auto
ultimately have "EX e>1. (1 - e) *\<^sub>R x + e *\<^sub>R z : Inter I" using mS_def by auto
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Aug 23 15:46:53 2011 -0700
@@ -598,7 +598,7 @@
case True thus ?thesis
apply(rule_tac x="(min (b$$i - a$$i) e) / 2" in exI)
using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2)
- unfolding mem_interval euclidean_simps basis_component
+ unfolding mem_interval euclidean_simps
using i by (auto simp add: field_simps)
next note * = assms(2)[unfolded mem_interval,THEN spec[where x=i]]
case False moreover have "a $$ i < x $$ i" using False * by auto
@@ -614,7 +614,7 @@
ultimately show ?thesis
apply(rule_tac x="- (min (x$$i - a$$i) e) / 2" in exI)
using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2)
- unfolding mem_interval euclidean_simps basis_component
+ unfolding mem_interval euclidean_simps
using i by (auto simp add: field_simps)
qed
qed
@@ -655,7 +655,7 @@
proof -
have fA: "finite {..<DIM('a)}" by simp
have "?rhs = (\<Sum>i<DIM('a). x$$i *\<^sub>R f (basis i))$$j"
- by (simp add: euclidean_simps)
+ by simp
then show ?thesis
unfolding linear_setsum_mul[OF lf fA, symmetric]
unfolding euclidean_representation[symmetric] ..
@@ -1550,7 +1550,7 @@
apply(rule has_derivative_sequence[OF assms(1) _ assms(3), of "\<lambda>n x. f n x + (f 0 a - f n a)"])
apply(rule,rule)
apply(rule has_derivative_add_const, rule assms(2)[rule_format], assumption)
- apply(rule `a\<in>s`) by(auto intro!: tendsto_const)
+ apply(rule `a\<in>s`) by auto
qed auto
lemma has_antiderivative_limit:
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Aug 23 15:46:53 2011 -0700
@@ -515,7 +515,7 @@
shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}"
proof(induct k)
case 0
- have th: "{f. \<forall>i. f i = i} = {id}" by (auto intro: ext)
+ have th: "{f. \<forall>i. f i = i} = {id}" by auto
show ?case by (auto simp add: th)
next
case (Suc k)
@@ -525,14 +525,14 @@
apply (auto simp add: image_iff)
apply (rule_tac x="x (Suc k)" in bexI)
apply (rule_tac x = "\<lambda>i. if i = Suc k then i else x i" in exI)
- apply (auto intro: ext)
+ apply auto
done
with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f]
show ?case by metis
qed
-lemma eq_id_iff[simp]: "(\<forall>x. f x = x) = (f = id)" by (auto intro: ext)
+lemma eq_id_iff[simp]: "(\<forall>x. f x = x) = (f = id)" by auto
lemma det_linear_rows_setsum_lemma:
assumes fS: "finite S" and fT: "finite T"
@@ -575,7 +575,7 @@
blast intro: finite_cartesian_product fS finite,
blast intro: finite_cartesian_product fS finite)
using `z \<notin> T`
- apply (auto intro: ext)
+ apply auto
apply (rule cong[OF refl[of det]])
by vector
qed
@@ -739,7 +739,7 @@
unfolding setsum_diff1'[OF fU iU] setsum_cmul
apply -
apply (rule vector_mul_lcancel_imp[OF ci])
- apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps)
+ apply (auto simp add: field_simps)
unfolding stupid ..
have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
unfolding thr0
@@ -775,7 +775,7 @@
have kUk: "k \<notin> ?Uk" by simp
have th00: "\<And>k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s"
by (vector field_simps)
- have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by (auto intro: ext)
+ have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by auto
have "(\<chi> i. row i A) = A" by (vector row_def)
then have thd1: "det (\<chi> i. row i A) = det A" by simp
have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A"
@@ -931,7 +931,7 @@
unfolding dot_norm_neg dist_norm[symmetric]
unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
note fc = this
- show ?thesis unfolding linear_def vector_eq[where 'a="real^'n"] smult_conv_scaleR by (simp add: inner_simps fc field_simps)
+ show ?thesis unfolding linear_def vector_eq[where 'a="real^'n"] smult_conv_scaleR by (simp add: inner_add fc field_simps)
qed
lemma isometry_linear:
@@ -973,7 +973,7 @@
"x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'"
"norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1"
"norm(x0' - y0') = norm(x0 - y0)"
- hence *:"x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> x0 " by(simp add: norm_eq norm_eq_1 inner_simps)
+ hence *:"x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> x0 " by(simp add: norm_eq norm_eq_1 inner_add inner_diff)
have "norm(x' - y') = norm(x - y)"
apply (subst H(1))
apply (subst H(2))
@@ -981,7 +981,7 @@
apply (subst H(4))
using H(5-9)
apply (simp add: norm_eq norm_eq_1)
- apply (simp add: inner_simps smult_conv_scaleR) unfolding *
+ apply (simp add: inner_diff smult_conv_scaleR) unfolding *
by (simp add: field_simps) }
note th0 = this
let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)"
@@ -1015,7 +1015,7 @@
"norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) =
norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)"
using z
- by (auto simp add: vector_smult_assoc field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
+ by (auto simp add: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
by (simp add: dist_norm)}
ultimately have "dist (?g x) (?g y) = dist x y" by blast}
@@ -1049,7 +1049,7 @@
by (simp add: eval_nat_numeral setprod_numseg mult_commute)
lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
- by (simp add: det_def sign_id UNIV_1)
+ by (simp add: det_def sign_id)
lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
proof-
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 23 15:46:53 2011 -0700
@@ -129,19 +129,19 @@
lemma euclidean_component_zero [simp]: "0 $$ i = 0"
unfolding euclidean_component_def by (rule inner_zero_right)
-lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
+lemma euclidean_component_add [simp]: "(x + y) $$ i = x $$ i + y $$ i"
unfolding euclidean_component_def by (rule inner_add_right)
-lemma euclidean_component_diff: "(x - y) $$ i = x $$ i - y $$ i"
+lemma euclidean_component_diff [simp]: "(x - y) $$ i = x $$ i - y $$ i"
unfolding euclidean_component_def by (rule inner_diff_right)
-lemma euclidean_component_minus: "(- x) $$ i = - (x $$ i)"
+lemma euclidean_component_minus [simp]: "(- x) $$ i = - (x $$ i)"
unfolding euclidean_component_def by (rule inner_minus_right)
-lemma euclidean_component_scaleR: "(scaleR a x) $$ i = a * (x $$ i)"
+lemma euclidean_component_scaleR [simp]: "(scaleR a x) $$ i = a * (x $$ i)"
unfolding euclidean_component_def by (rule inner_scaleR_right)
-lemma euclidean_component_setsum: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
+lemma euclidean_component_setsum [simp]: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
unfolding euclidean_component_def by (rule inner_setsum_right)
lemma euclidean_eqI:
@@ -183,7 +183,6 @@
fixes x :: "'a::euclidean_space"
shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
apply (rule euclidean_eqI)
- apply (simp add: euclidean_component_setsum euclidean_component_scaleR)
apply (simp add: if_distrib setsum_delta cong: if_cong)
done
@@ -194,8 +193,7 @@
lemma euclidean_lambda_beta [simp]:
"((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
- by (auto simp: euclidean_component_setsum euclidean_component_scaleR
- Chi_def if_distrib setsum_cases intro!: setsum_cong)
+ by (auto simp: Chi_def if_distrib setsum_cases intro!: setsum_cong)
lemma euclidean_lambda_beta':
"j < DIM('a) \<Longrightarrow> ((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = f j"
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Tue Aug 23 15:46:53 2011 -0700
@@ -180,7 +180,7 @@
"(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
"(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
"(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
- unfolding interval_bij_cart vec_lambda_beta vector_component_simps o_def split_conv
+ unfolding interval_bij_cart vector_component_simps o_def split_conv
unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this
from z(1) guess zf unfolding image_iff .. note zf=this
from z(2) guess zg unfolding image_iff .. note zg=this
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Aug 23 15:46:53 2011 -0700
@@ -485,7 +485,7 @@
show "k\<subseteq>{a..b}" apply(rule,unfold mem_interval,rule,rule)
proof fix i x assume i:"i<DIM('a)" assume "x \<in> k" moreover have "\<pi>' i < l \<or> \<pi>' i = l \<or> \<pi>' i > l" by auto
ultimately show "a$$i \<le> x$$i" "x$$i \<le> b$$i" using abcd[of i] using l using i
- by(auto elim:disjE elim!:allE[where x=i] simp add:eucl_le[where 'a='a])
+ by(auto elim!:allE[where x=i] simp add:eucl_le[where 'a='a]) (* FIXME: SLOW *)
qed have "\<And>l. ?p1 l \<noteq> {}" "\<And>l. ?p2 l \<noteq> {}" unfolding interval_eq_empty not_ex apply(rule_tac[!] allI)
proof- case goal1 thus ?case using abcd[of x] by auto
next case goal2 thus ?case using abcd[of x] by auto
@@ -967,7 +967,7 @@
subsection {* The set we're concerned with must be closed. *}
lemma division_of_closed: "s division_of i \<Longrightarrow> closed (i::('n::ordered_euclidean_space) set)"
- unfolding division_of_def by(fastsimp intro!: closed_Union closed_interval)
+ unfolding division_of_def by fastsimp
subsection {* General bisection principle for intervals; might be useful elsewhere. *}
@@ -2544,7 +2544,7 @@
apply(subst interval_doublesplit[OF k]) apply(rule content_pos_le) apply(rule indicator_pos_le)
proof- have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) * ?i x) \<le> (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}))"
apply(rule setsum_mono) unfolding split_paired_all split_conv
- apply(rule mult_right_le_one_le) apply(drule p'(4)) by(auto simp add:interval_doublesplit[OF k] intro!:content_pos_le)
+ apply(rule mult_right_le_one_le) apply(drule p'(4)) by(auto simp add:interval_doublesplit[OF k])
also have "... < e" apply(subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]])
proof- case goal1 have "content ({u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<le> content {u..v}"
unfolding interval_doublesplit[OF k] apply(rule content_subset) unfolding interval_doublesplit[THEN sym,OF k] by auto
@@ -4627,7 +4627,7 @@
case goal1 show ?case using int .
next case goal2 thus ?case apply-apply(cases "x\<in>s") using assms(3) by auto
next case goal3 thus ?case apply-apply(cases "x\<in>s")
- using assms(4) by (auto intro: tendsto_const)
+ using assms(4) by auto
next case goal4 note * = integral_nonneg
have "\<And>k. norm (integral {a..b} (\<lambda>x. if x \<in> s then f k x else 0)) \<le> norm (integral s (f k))"
unfolding real_norm_def apply(subst abs_of_nonneg) apply(rule *[OF int])
@@ -4678,7 +4678,7 @@
next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto
next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto
next case goal4 thus ?case apply-apply(rule tendsto_diff)
- using seq_offset[OF assms(3)[rule_format],of x 1] by (auto intro: tendsto_const)
+ using seq_offset[OF assms(3)[rule_format],of x 1] by auto
next case goal5 thus ?case using assms(4) unfolding bounded_iff
apply safe apply(rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI)
apply safe apply(erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE) unfolding sub
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Aug 23 15:46:53 2011 -0700
@@ -215,8 +215,8 @@
next
assume ?rhs
then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0" by simp
- hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0" by (simp add: inner_simps inner_commute)
- then have "(x - y) \<bullet> (x - y) = 0" by (simp add: field_simps inner_simps inner_commute)
+ hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0" by (simp add: inner_diff inner_commute)
+ then have "(x - y) \<bullet> (x - y) = 0" by (simp add: field_simps inner_diff inner_commute)
then show "x = y" by (simp)
qed
@@ -378,15 +378,15 @@
by (auto intro: setsum_0')
lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> y = setsum (\<lambda>x. f x \<bullet> y) S "
- apply(induct rule: finite_induct) by(auto simp add: inner_simps)
+ apply(induct rule: finite_induct) by(auto simp add: inner_add)
lemma dot_rsum: "finite S \<Longrightarrow> y \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
- apply(induct rule: finite_induct) by(auto simp add: inner_simps)
+ apply(induct rule: finite_induct) by(auto simp add: inner_add)
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
proof
assume "\<forall>x. x \<bullet> y = x \<bullet> z"
- hence "\<forall>x. x \<bullet> (y - z) = 0" by (simp add: inner_simps)
+ hence "\<forall>x. x \<bullet> (y - z) = 0" by (simp add: inner_diff)
hence "(y - z) \<bullet> (y - z) = 0" ..
thus "y = z" by simp
qed simp
@@ -394,7 +394,7 @@
lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y"
proof
assume "\<forall>z. x \<bullet> z = y \<bullet> z"
- hence "\<forall>z. (x - y) \<bullet> z = 0" by (simp add: inner_simps)
+ hence "\<forall>z. (x - y) \<bullet> z = 0" by (simp add: inner_diff)
hence "(x - y) \<bullet> (x - y) = 0" ..
thus "x = y" by simp
qed simp
@@ -1624,10 +1624,6 @@
lemma in_span_basis: "(x::'a::euclidean_space) \<in> span (basis ` {..<DIM('a)})"
unfolding span_basis' ..
-lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
- unfolding euclidean_component_def
- apply(rule order_trans[OF real_inner_class.Cauchy_Schwarz_ineq2]) by auto
-
lemma norm_bound_component_le: "norm (x::'a::euclidean_space) \<le> e \<Longrightarrow> \<bar>x$$i\<bar> <= e"
by (metis component_le_norm order_trans)
@@ -1663,10 +1659,9 @@
have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+
have Ppe:"setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp \<le> e"
using component_le_norm[of "setsum (\<lambda>x. f x) ?Pp" i] fPs[OF PpP]
- unfolding euclidean_component_setsum by(auto intro: abs_le_D1)
+ by(auto intro: abs_le_D1)
have Pne: "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn \<le> e"
using component_le_norm[of "setsum (\<lambda>x. - f x) ?Pn" i] fPs[OF PnP]
- unfolding euclidean_component_setsum euclidean_component_minus
by(auto simp add: setsum_negf intro: abs_le_D1)
have "setsum (\<lambda>x. \<bar>f x $$ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $$ i\<bar>) ?Pn"
apply (subst thp)
@@ -2150,7 +2145,7 @@
apply (subst Cy)
using C(1) fth
apply (simp only: setsum_clauses)
- apply (auto simp add: inner_simps inner_commute[of y a] dot_lsum[OF fth])
+ apply (auto simp add: inner_add inner_commute[of y a] dot_lsum[OF fth])
apply (rule setsum_0')
apply clarsimp
apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
@@ -2167,7 +2162,7 @@
using C(1) fth
apply (simp only: setsum_clauses)
apply (subst inner_commute[of x])
- apply (auto simp add: inner_simps inner_commute[of x a] dot_rsum[OF fth])
+ apply (auto simp add: inner_add inner_commute[of x a] dot_rsum[OF fth])
apply (rule setsum_0')
apply clarsimp
apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
@@ -2228,7 +2223,7 @@
with a have a0:"?a \<noteq> 0" by auto
have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
proof(rule span_induct')
- show "subspace {x. ?a \<bullet> x = 0}" by (auto simp add: subspace_def inner_simps)
+ show "subspace {x. ?a \<bullet> x = 0}" by (auto simp add: subspace_def inner_add)
next
{fix x assume x: "x \<in> B"
from x have B': "B = insert x (B - {x})" by blast
@@ -2237,7 +2232,7 @@
apply (subst B') using fB fth
unfolding setsum_clauses(2)[OF fth]
apply simp unfolding inner_simps
- apply (clarsimp simp add: inner_simps dot_lsum)
+ apply (clarsimp simp add: inner_add dot_lsum)
apply (rule setsum_0', rule ballI)
unfolding inner_commute
by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
@@ -2538,7 +2533,7 @@
from equalityD2[OF span_basis'[where 'a='a]]
have IU: " (UNIV :: 'a set) \<subseteq> span ?I" by blast
have "f x = g x" apply(rule linear_eq[OF lf lg IU,rule_format]) using fg x by auto }
- then show ?thesis by (auto intro: ext)
+ then show ?thesis by auto
qed
text {* Similar results for bilinear functions. *}
@@ -2563,7 +2558,7 @@
apply (auto simp add: subspace_def)
using bf bg unfolding bilinear_def linear_def
by(auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf])
- then show ?thesis using SB TC by (auto intro: ext)
+ then show ?thesis using SB TC by auto
qed
lemma bilinear_eq_stdbasis: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> _"
@@ -2574,7 +2569,7 @@
proof-
from fg have th: "\<forall>x \<in> (basis ` {..<DIM('a)}). \<forall>y\<in> (basis ` {..<DIM('b)}). f x y = g x y" by blast
from bilinear_eq[OF bf bg equalityD2[OF span_basis'] equalityD2[OF span_basis'] th]
- show ?thesis by (blast intro: ext)
+ show ?thesis by blast
qed
text {* Detailed theorems about left and right invertibility in general case. *}
@@ -2829,7 +2824,7 @@
unfolding infnorm_def
unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
unfolding infnorm_set_image ball_simps
- apply(subst (1) euclidean_eq) unfolding euclidean_component_zero
+ apply(subst (1) euclidean_eq)
by auto
then show ?thesis using infnorm_pos_le[of x] by simp
qed
@@ -2840,7 +2835,7 @@
lemma infnorm_neg: "infnorm (- x) = infnorm x"
unfolding infnorm_def
apply (rule cong[of "Sup" "Sup"])
- apply blast by(auto simp add: euclidean_simps)
+ apply blast by auto
lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
proof-
@@ -2855,7 +2850,7 @@
from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
"infnorm y \<le> infnorm (x - y) + infnorm x"
- by (simp_all add: field_simps infnorm_neg diff_minus[symmetric])
+ by (simp_all add: field_simps infnorm_neg)
from th[OF ths] show ?thesis .
qed
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 23 15:46:53 2011 -0700
@@ -14,7 +14,7 @@
lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
- apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff ..
+ by(auto simp add:power2_eq_square)
lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
@@ -5601,26 +5601,17 @@
lemma subspace_substandard:
"subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
- unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)
+ unfolding subspace_def by auto
lemma closed_substandard:
"closed {x::'a::euclidean_space. \<forall>i<DIM('a). P i --> x$$i = 0}" (is "closed ?A")
proof-
let ?D = "{i. P i} \<inter> {..<DIM('a)}"
- let ?Bs = "{{x::'a. inner (basis i) x = 0}| i. i \<in> ?D}"
- { fix x
- { assume "x\<in>?A"
- hence x:"\<forall>i\<in>?D. x $$ i = 0" by auto
- hence "x\<in> \<Inter> ?Bs" by(auto simp add: x euclidean_component_def) }
- moreover
- { assume x:"x\<in>\<Inter>?Bs"
- { fix i assume i:"i \<in> ?D"
- then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::'a. inner (basis i) x = 0}" by auto
- hence "x $$ i = 0" unfolding B using x unfolding euclidean_component_def by auto }
- hence "x\<in>?A" by auto }
- ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" .. }
- hence "?A = \<Inter> ?Bs" by auto
- thus ?thesis by(auto simp add: closed_Inter closed_hyperplane)
+ have "closed (\<Inter>i\<in>?D. {x::'a. x$$i = 0})"
+ by (simp add: closed_INT closed_Collect_eq)
+ also have "(\<Inter>i\<in>?D. {x::'a. x$$i = 0}) = ?A"
+ by auto
+ finally show "closed ?A" .
qed
lemma dim_substandard: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
@@ -5645,7 +5636,7 @@
have y:"x = y + (x$$k) *\<^sub>R basis k" unfolding y_def by auto
{ fix i assume i':"i \<notin> F"
hence "y $$ i = 0" unfolding y_def
- using *[THEN spec[where x=i]] by(auto simp add: euclidean_simps) }
+ using *[THEN spec[where x=i]] by auto }
hence "y \<in> span (basis ` F)" using insert(3) by auto
hence "y \<in> span (basis ` (insert k F))"
using span_mono[of "?bas ` F" "?bas ` (insert k F)"]
@@ -5763,25 +5754,25 @@
case False
{ fix y assume "a \<le> y" "y \<le> b" "m > 0"
hence "m *\<^sub>R a + c \<le> m *\<^sub>R y + c" "m *\<^sub>R y + c \<le> m *\<^sub>R b + c"
- unfolding eucl_le[where 'a='a] by(auto simp add: euclidean_simps)
+ unfolding eucl_le[where 'a='a] by auto
} moreover
{ fix y assume "a \<le> y" "y \<le> b" "m < 0"
hence "m *\<^sub>R b + c \<le> m *\<^sub>R y + c" "m *\<^sub>R y + c \<le> m *\<^sub>R a + c"
- unfolding eucl_le[where 'a='a] by(auto simp add: mult_left_mono_neg euclidean_simps)
+ unfolding eucl_le[where 'a='a] by(auto simp add: mult_left_mono_neg)
} moreover
{ fix y assume "m > 0" "m *\<^sub>R a + c \<le> y" "y \<le> m *\<^sub>R b + c"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
apply(auto simp add: pth_3[symmetric]
intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
- by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff euclidean_simps)
+ by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
} moreover
{ fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
apply(auto simp add: pth_3[symmetric]
intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
- by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff euclidean_simps)
+ by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
}
ultimately show ?thesis using False by auto
qed
--- a/src/HOL/Multivariate_Analysis/normarith.ML Tue Aug 23 23:18:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Tue Aug 23 15:46:53 2011 -0700
@@ -26,7 +26,7 @@
fun find_normedterms t acc = case term_of t of
@{term "op + :: real => _"}$_$_ =>
find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
- | @{term "op * :: real => _"}$_$n =>
+ | @{term "op * :: real => _"}$_$_ =>
if not (is_ratconst (Thm.dest_arg1 t)) then acc else
augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero)
(Thm.dest_arg t) acc
@@ -39,12 +39,16 @@
fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
+(*
val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
+*)
fun int_lincomb_cmul c t =
if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x */ c) t
fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
+(*
fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
+*)
fun vector_lincomb t = case term_of t of
Const(@{const_name plus}, _) $ _ $ _ =>
@@ -82,9 +86,11 @@
| @{term "op * :: real => _"}$_$_ =>
if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive t
| _ => Thm.reflexive t
+(*
fun flip v eq =
if FuncUtil.Ctermfunc.defined eq v
then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
+*)
fun allsubsets s = case s of
[] => [[]]
|(a::t) => let val res = allsubsets t in
@@ -178,8 +184,8 @@
fun headvector t = case t of
Const(@{const_name plus}, _)$
- (Const(@{const_name scaleR}, _)$l$v)$r => v
- | Const(@{const_name scaleR}, _)$l$v => v
+ (Const(@{const_name scaleR}, _)$_$v)$_ => v
+ | Const(@{const_name scaleR}, _)$_$v => v
| _ => error "headvector: non-canonical term"
fun vector_cmul_conv ct =