# HG changeset patch # User wenzelm # Date 1314199825 -7200 # Node ID 85103fbc9004b1c06c2f2a77a6eaed5e204cc87c # Parent c471a2b48fa13517df2a48a4f6511491b87449b7# Parent f9334afb6945d91bc8a5f042a9d1c498c9268c82 merged diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Library/Infinite_Set.thy --- a/src/HOL/Library/Infinite_Set.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Library/Infinite_Set.thy Wed Aug 24 17:30:25 2011 +0200 @@ -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] diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Wed Aug 24 17:30:25 2011 +0200 @@ -33,7 +33,7 @@ lemma collect_rsp[quot_respect]: assumes "Quotient R Abs Rep" shows "((R ===> op =) ===> set_rel R) Collect Collect" - by (auto intro!: fun_relI simp add: fun_rel_def set_rel_def) + by (intro fun_relI) (simp add: fun_rel_def set_rel_def) lemma collect_prs[quot_preserve]: assumes "Quotient R Abs Rep" @@ -44,7 +44,7 @@ lemma union_rsp[quot_respect]: assumes "Quotient R Abs Rep" shows "(set_rel R ===> set_rel R ===> set_rel R) op \ op \" - by (intro fun_relI) (auto simp add: set_rel_def) + by (intro fun_relI) (simp add: set_rel_def) lemma union_prs[quot_preserve]: assumes "Quotient R Abs Rep" @@ -55,7 +55,7 @@ lemma diff_rsp[quot_respect]: assumes "Quotient R Abs Rep" shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -" - by (intro fun_relI) (auto simp add: set_rel_def) + by (intro fun_relI) (simp add: set_rel_def) lemma diff_prs[quot_preserve]: assumes "Quotient R Abs Rep" @@ -74,4 +74,13 @@ unfolding fun_eq_iff by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]]) +lemma mem_prs[quot_preserve]: + assumes "Quotient R Abs Rep" + shows "(Rep ---> op -` Abs ---> id) op \ = op \" + by (simp add: fun_eq_iff Quotient_abs_rep[OF assms]) + +lemma mem_rsp[quot_respect]: + shows "(R ===> set_rel R ===> op =) op \ op \" + by (intro fun_relI) (simp add: set_rel_def) + end diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Aug 24 17:30:25 2011 +0200 @@ -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 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 diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Wed Aug 24 17:30:25 2011 +0200 @@ -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 diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 24 17:30:25 2011 +0200 @@ -21,6 +21,8 @@ val metis_ftK = "metis_ft" val reconstructorK = "reconstructor" +val preplay_timeout = "4" + fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " fun reconstructor_tag reconstructor id = @@ -384,9 +386,11 @@ [("verbose", "true"), ("type_enc", type_enc), ("sound", sound), + ("preplay_timeout", preplay_timeout), ("max_relevant", max_relevant), ("slicing", slicing), - ("timeout", string_of_int timeout)] + ("timeout", string_of_int timeout), + ("preplay_timeout", preplay_timeout)] val default_max_relevant = Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing prover_name @@ -522,7 +526,8 @@ ("verbose", "true"), ("type_enc", type_enc), ("sound", sound), - ("timeout", string_of_int timeout)] + ("timeout", string_of_int timeout), + ("preplay_timeout", preplay_timeout)] val minimize = Sledgehammer_Minimize.minimize_facts prover_name params true 1 (Sledgehammer_Util.subgoal_count st) @@ -545,40 +550,53 @@ end -val e_override_params = +fun e_override_params timeout = [("provers", "e"), + ("max_relevant", "0"), ("type_enc", "poly_guards?"), ("sound", "true"), - ("slicing", "false")] + ("slicing", "false"), + ("timeout", timeout |> Time.toSeconds |> string_of_int)] -val vampire_override_params = +fun vampire_override_params timeout = [("provers", "vampire"), + ("max_relevant", "0"), ("type_enc", "poly_tags"), ("sound", "true"), - ("slicing", "false")] + ("slicing", "false"), + ("timeout", timeout |> Time.toSeconds |> string_of_int)] fun run_reconstructor trivial full m name reconstructor named_thms id ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = let - fun do_reconstructor thms ctxt = - (if !reconstructor = "sledgehammer_tac" then - (fn ctxt => fn thms => - Method.insert_tac thms THEN' - (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt - e_override_params - ORELSE' - Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt - vampire_override_params)) - else if !reconstructor = "smt" then - SMT_Solver.smt_tac - else if full orelse !reconstructor = "metis (full_types)" then - Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] - else if !reconstructor = "metis (no_types)" then - Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] - else - Metis_Tactics.metis_tac []) ctxt thms - fun apply_reconstructor thms = - Mirabelle.can_apply timeout (do_reconstructor thms) st + fun do_reconstructor named_thms ctxt = + let + val ref_of_str = + suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm + #> fst + val thms = named_thms |> maps snd + val facts = named_thms |> map (ref_of_str o fst o fst) + val relevance_override = {add = facts, del = [], only = true} + in + if !reconstructor = "sledgehammer_tac" then + Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt + (e_override_params timeout) relevance_override + ORELSE' + Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt + (vampire_override_params timeout) relevance_override + else if !reconstructor = "smt" then + SMT_Solver.smt_tac ctxt thms + else if full orelse !reconstructor = "metis (full_types)" then + Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] ctxt thms + else if !reconstructor = "metis (no_types)" then + Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] ctxt thms + else if !reconstructor = "metis" then + Metis_Tactics.metis_tac [] ctxt thms + else + K all_tac + end + fun apply_reconstructor named_thms = + Mirabelle.can_apply timeout (do_reconstructor named_thms) st fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" | with_time (true, t) = (change_data id (inc_reconstructor_success m); @@ -590,8 +608,8 @@ if name = "proof" then change_data id (inc_reconstructor_proofs m) else (); "succeeded (" ^ string_of_int t ^ ")") - fun timed_reconstructor thms = - (with_time (Mirabelle.cpu_time apply_reconstructor thms), true) + fun timed_reconstructor named_thms = + (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true) handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); ("timeout", false)) | ERROR msg => ("error: " ^ msg, false) @@ -601,7 +619,7 @@ val _ = if trivial then () else change_data id (inc_reconstructor_nontriv_calls m) in - maps snd named_thms + named_thms |> timed_reconstructor |>> log o prefix (reconstructor_tag reconstructor id) |> snd @@ -617,49 +635,52 @@ if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then () else let - val reconstructor = Unsynchronized.ref "" - val named_thms = - Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) val max_calls = AList.lookup (op =) args max_callsK |> the_default "10000000" |> Int.fromString |> the - val minimize = AList.defined (op =) args minimizeK - val metis_ft = AList.defined (op =) args metis_ftK - val trivial = - Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre - handle TimeLimit.TimeOut => false - fun apply_reconstructor m1 m2 = - if metis_ft - then - if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false - (run_reconstructor trivial false m1 name reconstructor - (these (!named_thms))) id st) - then - (Mirabelle.catch_result (reconstructor_tag reconstructor) false - (run_reconstructor trivial true m2 name reconstructor - (these (!named_thms))) id st; ()) - else () - else - (Mirabelle.catch_result (reconstructor_tag reconstructor) false - (run_reconstructor trivial false m1 name reconstructor - (these (!named_thms))) id st; ()) val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1; - in + in if !num_sledgehammer_calls > max_calls then () else - change_data id (set_mini minimize); - Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor - named_thms) id st; - if is_some (!named_thms) - then - (apply_reconstructor Unminimized UnminimizedFT; - if minimize andalso not (null (these (!named_thms))) + let + val reconstructor = Unsynchronized.ref "" + val named_thms = + Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) + val minimize = AList.defined (op =) args minimizeK + val metis_ft = AList.defined (op =) args metis_ftK + val trivial = + Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre + handle TimeLimit.TimeOut => false + fun apply_reconstructor m1 m2 = + if metis_ft + then + if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false + (run_reconstructor trivial false m1 name reconstructor + (these (!named_thms))) id st) + then + (Mirabelle.catch_result (reconstructor_tag reconstructor) false + (run_reconstructor trivial true m2 name reconstructor + (these (!named_thms))) id st; ()) + else () + else + (Mirabelle.catch_result (reconstructor_tag reconstructor) false + (run_reconstructor trivial false m1 name reconstructor + (these (!named_thms))) id st; ()) + in + change_data id (set_mini minimize); + Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor + named_thms) id st; + if is_some (!named_thms) then - (Mirabelle.catch minimize_tag - (run_minimize args reconstructor named_thms) id st; - apply_reconstructor Minimized MinimizedFT) - else ()) - else () + (apply_reconstructor Unminimized UnminimizedFT; + if minimize andalso not (null (these (!named_thms))) + then + (Mirabelle.catch minimize_tag + (run_minimize args reconstructor named_thms) id st; + apply_reconstructor Minimized MinimizedFT) + else ()) + else () + end end end diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Aug 24 17:30:25 2011 +0200 @@ -533,7 +533,7 @@ case False hence "t = {}" using `finite t` by auto show ?thesis proof (cases "s = {}") - have *:"{f. \x. f x = d} = {\x. d}" by (auto intro: ext) + have *:"{f. \x. f x = d} = {\x. d}" by auto case True thus ?thesis using `t = {}` by (auto simp: *) next case False thus ?thesis using `t = {}` by simp diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 24 17:30:25 2011 +0200 @@ -831,7 +831,7 @@ have IU: " (UNIV :: (real^'m) set) \ 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: "\x \ {cart_basis i| i. i\ (UNIV :: 'm set)}. \y\ {cart_basis j |j. j \ (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. \i. 0 \x$i}" by (simp add: Collect_all_eq closed_INT closed_Collect_le) -lemma Lim_component_cart: - fixes f :: "'a \ 'b::metric_space ^ 'n" - shows "(f ---> l) net \ ((\a. f a $i) ---> l$i) net" - by (intro tendsto_intros) - lemma bounded_component_cart: "bounded s \ bounded ((\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 diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Aug 24 17:30:25 2011 +0200 @@ -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 \ {.. 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 ==> \(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 "\i. i convex {x. P i x}" shows "convex {x. \ii 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 \ 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 \ 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 "\x\{a..b}. (f x)$$k = y" apply(subst neg_equal_iff_equal[THEN sym]) using ivt_increasing_component_on_1[of a b "\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 \ 'a::euclidean_space" shows "a \ b \ \x\{a .. b}. continuous (at x) f @@ -3624,18 +3618,18 @@ by auto next let ?y = "\j. if x$$j = 0 then 0 else (x$$j - x$$i) / (1 - x$$i)" case False hence *:"x = x$$i *\<^sub>R (\\ j. if x$$j = 0 then 0 else 1) + (1 - x$$i) *\<^sub>R (\\ 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 0 \ 0 \ (x $$ j - x $$ i) / (1 - x $$ i)" "(x $$ j - x $$ i) / (1 - x $$ i) \ 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 \ ?y j \ ?y j \ 1" by auto } moreover have "i\{j. j x$$j \ 0} - {j. j ((\\ j. ?y j)::'a) $$ j \ 0}" using i01 using i'(3) by auto hence "{j. j x$$j \ 0} \ {j. j ((\\ j. ?y j)::'a) $$ j \ 0}" using i'(3) by blast hence **:"{j. j ((\\ j. ?y j)::'a) $$ j \ 0} \ {j. j x$$j \ 0}" apply - apply rule - by( auto simp add:euclidean_simps) + by auto have "card {j. j ((\\ j. ?y j)::'a) $$ j \ 0} \ 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\{x - ?d .. x + ?d}" { fix i assume i:"i d + y $$ i" "y $$ i \ d + x $$ i" using as[unfolded mem_interval, THEN spec[where x=i]] i - by(auto simp add:euclidean_simps) + by auto hence "1 \ inverse d * (x $$ i - y $$ i)" "1 \ 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) \ 2 + inverse d * (y $$ i * 2)" "inverse d * (y $$ i * 2) \ 2 + inverse d * (x $$ i * 2)" by(auto simp add:field_simps) } hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \ {0..\\ i.1}" unfolding mem_interval using assms - by(auto simp add: euclidean_simps field_simps) + by(auto simp add: field_simps) thus "\z\{0..\\ 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 \ {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..\\ i.1} = convex hull s" using unit_cube_convex_hull by auto thus ?thesis apply(rule_tac that[of "(\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 = "(\\ 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\{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by(auto simp add:euclidean_simps) + have "x\{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by auto hence "c\{}" using c by auto def k \ "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 (\i. d) {.. 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:"\y\{x - ?d..x + ?d}. f y \ 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 \ 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 "\y\cball x d. abs (f y) \ k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof fix y assume y:"y\cball x d" { fix i assume "i y $$ i" "y $$ i \ 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 \ 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:"iR 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 "\ = 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 *:"\x y z. x = (1/2::real) *\<^sub>R z \ y = (1/2) *\<^sub>R z \ 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 \ x \ 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 "\ = 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 "\ < 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="\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 "0xa. dist x xa < e \ (\x xa $$ x) \ setsum (op $$ xa) {.. 1" show "(\xa setsum (op $$ x) {..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 "\i. i (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)) {..i. x$$i + (if 0 = i then e/2 else 0)) {..R basis 0)) {..i. x$$i + (if a = i then e/2 else 0)) d" by(rule_tac setsum_cong, auto) have h1: "(ALL i (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 \ 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 diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Aug 24 17:30:25 2011 +0200 @@ -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 {..iR 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 "\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\s`) by(auto intro!: tendsto_const) + apply(rule `a\s`) by auto qed auto lemma has_antiderivative_limit: diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Wed Aug 24 17:30:25 2011 +0200 @@ -515,7 +515,7 @@ shows "finite {f. (\i \ {1.. (k::nat)}. f i \ S) \ (\i. i \ {1 .. k} \ f i = i)}" proof(induct k) case 0 - have th: "{f. \i. f i = i} = {id}" by (auto intro: ext) + have th: "{f. \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 = "\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]: "(\x. f x = x) = (f = id)" by (auto intro: ext) +lemma eq_id_iff[simp]: "(\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 \ 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 \ span {row j A| j. j \ i}" unfolding thr0 @@ -775,7 +775,7 @@ have kUk: "k \ ?Uk" by simp have th00: "\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: "\f k . (\x. if x = k then f k else f x) = f" by (auto intro: ext) + have th001: "\f k . (\x. if x = k then f k else f x) = f" by auto have "(\ i. row i A) = A" by (vector row_def) then have thd1: "det (\ i. row i A) = det A" by simp have thd0: "det (\ i. if i = k then row k A + (\i \ ?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 \ y0 = x0' \ y0' + y0' \ x0' - y0 \ x0 " by(simp add: norm_eq norm_eq_1 inner_simps) + hence *:"x0 \ y0 = x0' \ y0' + y0' \ x0' - y0 \ 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 = "\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- diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 24 17:30:25 2011 +0200 @@ -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: "(\x\A. f x) $$ i = (\x\A. f x $$ i)" +lemma euclidean_component_setsum [simp]: "(\x\A. f x) $$ i = (\x\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 = (\iR 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]: "((\\ 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) \ ((\\ i. f i)::'a::euclidean_space) $$ j = f j" diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Multivariate_Analysis/Fashoda.thy --- a/src/HOL/Multivariate_Analysis/Fashoda.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Wed Aug 24 17:30:25 2011 +0200 @@ -180,7 +180,7 @@ "(interval_bij (a, b) (- 1, 1) \ f) 1 $ 1 = 1" "(interval_bij (a, b) (- 1, 1) \ g) 0 $ 2 = -1" "(interval_bij (a, b) (- 1, 1) \ 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 diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Aug 24 17:30:25 2011 +0200 @@ -485,7 +485,7 @@ show "k\{a..b}" apply(rule,unfold mem_interval,rule,rule) proof fix i x assume i:"i k" moreover have "\' i < l \ \' i = l \ \' i > l" by auto ultimately show "a$$i \ x$$i" "x$$i \ 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 "\l. ?p1 l \ {}" "\l. ?p2 l \ {}" 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 \ 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 "(\(x, ka)\p. content (ka \ {x. \x $$ k - c\ \ d}) * ?i x) \ (\(x, ka)\p. content (ka \ {x. \x $$ k - c\ \ 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} \ {x. \x $$ k - c\ \ d}) \ 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\s") using assms(3) by auto next case goal3 thus ?case apply-apply(cases "x\s") - using assms(4) by (auto intro: tendsto_const) + using assms(4) by auto next case goal4 note * = integral_nonneg have "\k. norm (integral {a..b} (\x. if x \ s then f k x else 0)) \ 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 (\x. f 0 x))" in exI) apply safe apply(erule_tac x="integral s (\x. f (Suc k) x)" in ballE) unfolding sub diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Aug 24 17:30:25 2011 +0200 @@ -215,8 +215,8 @@ next assume ?rhs then have "x \ x - x \ y = 0 \ x \ y - y \ y = 0" by simp - hence "x \ (x - y) = 0 \ y \ (x - y) = 0" by (simp add: inner_simps inner_commute) - then have "(x - y) \ (x - y) = 0" by (simp add: field_simps inner_simps inner_commute) + hence "x \ (x - y) = 0 \ y \ (x - y) = 0" by (simp add: inner_diff inner_commute) + then have "(x - y) \ (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 \ setsum f S \ y = setsum (\x. f x \ 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 \ y \ setsum f S = setsum (\x. y \ 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: "(\x. x \ y = x \ z) \ y = z" proof assume "\x. x \ y = x \ z" - hence "\x. x \ (y - z) = 0" by (simp add: inner_simps) + hence "\x. x \ (y - z) = 0" by (simp add: inner_diff) hence "(y - z) \ (y - z) = 0" .. thus "y = z" by simp qed simp @@ -394,7 +394,7 @@ lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = y" proof assume "\z. x \ z = y \ z" - hence "\z. (x - y) \ z = 0" by (simp add: inner_simps) + hence "\z. (x - y) \ z = 0" by (simp add: inner_diff) hence "(x - y) \ (x - y) = 0" .. thus "x = y" by simp qed simp @@ -1624,10 +1624,6 @@ lemma in_span_basis: "(x::'a::euclidean_space) \ span (basis ` {..x$$i\ \ 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) \ e \ \x$$i\ <= e" by (metis component_le_norm order_trans) @@ -1663,10 +1659,9 @@ have PpP: "?Pp \ P" and PnP: "?Pn \ P" by blast+ have Ppe:"setsum (\x. \f x $$ i\) ?Pp \ e" using component_le_norm[of "setsum (\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 (\x. \f x $$ i\) ?Pn \ e" using component_le_norm[of "setsum (\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 (\x. \f x $$ i\) P = setsum (\x. \f x $$ i\) ?Pp + setsum (\x. \f x $$ i\) ?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 \ 0" by auto have "\x\span B. ?a \ x = 0" proof(rule span_induct') - show "subspace {x. ?a \ x = 0}" by (auto simp add: subspace_def inner_simps) + show "subspace {x. ?a \ x = 0}" by (auto simp add: subspace_def inner_add) next {fix x assume x: "x \ 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) \ 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 \ 'b::euclidean_space \ _" @@ -2574,7 +2569,7 @@ proof- from fg have th: "\x \ (basis ` {..y\ (basis ` {.. infnorm (x - y) + infnorm y" "infnorm y \ 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 diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 24 17:30:25 2011 +0200 @@ -14,7 +14,7 @@ lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\i. dist(x$$i) (y$$i)) {.. dist x (y::'a::euclidean_space)" apply(subst(2) euclidean_dist_l2) apply(cases "ii 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. \i x$$i = 0}" (is "closed ?A") proof- let ?D = "{i. P i} \ {..?A" - hence x:"\i\?D. x $$ i = 0" by auto - hence "x\ \ ?Bs" by(auto simp add: x euclidean_component_def) } - moreover - { assume x:"x\\?Bs" - { fix i assume i:"i \ ?D" - then obtain B where BB:"B \ ?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\?A" by auto } - ultimately have "x\?A \ x\ \?Bs" .. } - hence "?A = \ ?Bs" by auto - thus ?thesis by(auto simp add: closed_Inter closed_hyperplane) + have "closed (\i\?D. {x::'a. x$$i = 0})" + by (simp add: closed_INT closed_Collect_eq) + also have "(\i\?D. {x::'a. x$$i = 0}) = ?A" + by auto + finally show "closed ?A" . qed lemma dim_substandard: assumes "d\{..R basis k" unfolding y_def by auto { fix i assume i':"i \ 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 \ span (basis ` F)" using insert(3) by auto hence "y \ 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 \ y" "y \ b" "m > 0" hence "m *\<^sub>R a + c \ m *\<^sub>R y + c" "m *\<^sub>R y + c \ 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 \ y" "y \ b" "m < 0" hence "m *\<^sub>R b + c \ m *\<^sub>R y + c" "m *\<^sub>R y + c \ 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 \ y" "y \ m *\<^sub>R b + c" hence "y \ (\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 \ y" "y \ m *\<^sub>R a + c" "m < 0" hence "y \ (\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 diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Wed Aug 24 17:30:25 2011 +0200 @@ -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) 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 = diff -r f9334afb6945 -r 85103fbc9004 src/HOL/TPTP/CASC_Setup.thy --- a/src/HOL/TPTP/CASC_Setup.thy Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/TPTP/CASC_Setup.thy Wed Aug 24 17:30:25 2011 +0200 @@ -119,14 +119,16 @@ SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) ORELSE SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" - (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [])) + (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] + Sledgehammer_Filter.no_relevance_override)) ORELSE SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt))) ORELSE SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt)) ORELSE SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt - THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [])) + THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] + Sledgehammer_Filter.no_relevance_override)) ORELSE SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac [] ctxt [])) diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 24 17:30:25 2011 +0200 @@ -270,7 +270,7 @@ (* SPASS *) (* The "-VarWeight=3" option helps the higher-order problems, probably by - counteracting the presence of "hAPP". *) + counteracting the presence of explicit application operators. *) val spass_config : atp_config = {exec = ("ISABELLE_ATP", "scripts/spass"), required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 24 17:30:25 2011 +0200 @@ -165,8 +165,8 @@ val untyped_helper_suffix = "_U" val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem" -val predicator_name = "hBOOL" -val app_op_name = "hAPP" +val predicator_name = "p" +val app_op_name = "a" val type_guard_name = "g" val type_tag_name = "t" val simple_type_prefix = "ty_" @@ -1059,16 +1059,13 @@ | formula => SOME formula end -fun make_conjecture ctxt format type_enc ps = - let - val thy = Proof_Context.theory_of ctxt - val last = length ps - 1 - in - map2 (fn j => fn ((name, loc), (kind, t)) => - t |> make_formula thy type_enc (format <> CNF) name loc kind - |> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot) - (0 upto last) ps - end +fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t + | s_not_trueprop t = s_not t + +fun make_conjecture thy format type_enc = + map (fn ((name, loc), (kind, t)) => + t |> kind = Conjecture ? s_not_trueprop + |> make_formula thy type_enc (format <> CNF) name loc kind) (** Finite and infinite type inference **) @@ -1151,7 +1148,7 @@ | homo _ _ = raise Fail "expected function type" in homo end -(** "hBOOL" and "hAPP" **) +(** predicators and application operators **) type sym_info = {pred_sym : bool, min_ary : int, max_ary : int, types : typ list} @@ -1194,6 +1191,8 @@ if String.isPrefix bound_var_prefix s orelse String.isPrefix all_bound_var_prefix s then add_universal_var T accum + else if String.isPrefix exist_bound_var_prefix s then + accum else let val ary = length args in ((bool_vars, fun_var_Ts), @@ -1238,8 +1237,8 @@ end in add true end fun add_fact_syms_to_table ctxt explicit_apply = - fact_lift (formula_fold NONE - (K (add_iterm_syms_to_table ctxt explicit_apply))) + formula_fold NONE (K (add_iterm_syms_to_table ctxt explicit_apply)) + |> fact_lift val tvar_a = TVar (("'a", 0), HOLogic.typeS) @@ -1379,6 +1378,9 @@ (** Helper facts **) +val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast} +val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast} + (* The Boolean indicates that a fairly sound type encoding is needed. *) val helper_table = [(("COMBI", false), @{thms Meson.COMBI_def}), @@ -1386,9 +1388,10 @@ (("COMBB", false), @{thms Meson.COMBB_def}), (("COMBC", false), @{thms Meson.COMBC_def}), (("COMBS", false), @{thms Meson.COMBS_def}), - (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]), + ((predicator_name, false), [not_ffalse, ftrue]), + (("fFalse", false), [not_ffalse]), (("fFalse", true), @{thms True_or_False}), - (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]), + (("fTrue", false), [ftrue]), (("fTrue", true), @{thms True_or_False}), (("fNot", false), @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] @@ -1546,7 +1549,7 @@ |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t) val facts = facts |> map (apsnd (pair Axiom)) val conjs = - map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)] + map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)] |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts) val ((conjs, facts), lambdas) = if preproc then @@ -1557,7 +1560,7 @@ |>> apfst (map (apsnd (apsnd freeze_term))) else ((conjs, facts), []) - val conjs = conjs |> make_conjecture ctxt format type_enc + val conjs = conjs |> make_conjecture thy format type_enc val (fact_names, facts) = facts |> map_filter (fn (name, (_, t)) => @@ -1754,9 +1757,7 @@ (case type_enc of Guards _ => not pred_sym | _ => true) andalso - is_tptp_user_symbol s andalso - forall (fn prefix => not (String.isPrefix prefix s)) - [bound_var_prefix, all_bound_var_prefix, exist_bound_var_prefix] + is_tptp_user_symbol s fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab (conjs, facts) = diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Wed Aug 24 17:30:25 2011 +0200 @@ -272,7 +272,7 @@ (* Converts an elim-rule into an equivalent theorem that does not have the predicate variable. Leaves other theorems unchanged. We simply instantiate - the conclusion variable to False. (Cf. "transform_elim_theorem" in + the conclusion variable to "False". (Cf. "transform_elim_theorem" in "Meson_Clausify".) *) fun transform_elim_prop t = case Logic.strip_imp_concl t of diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Aug 24 17:30:25 2011 +0200 @@ -38,6 +38,7 @@ val trace : bool Config.T val ignore_no_atp : bool Config.T val instantiate_inducts : bool Config.T + val no_relevance_override : relevance_override val const_names_in_fact : theory -> (string * typ -> term list -> bool * term list) -> term -> string list @@ -100,6 +101,8 @@ del : (Facts.ref * Attrib.src list) list, only : bool} +val no_relevance_override = {add = [], del = [], only = false} + val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator val abs_name = sledgehammer_prefix ^ "abs" val skolem_prefix = sledgehammer_prefix ^ "sko" diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 24 17:30:25 2011 +0200 @@ -22,6 +22,7 @@ open ATP_Systems open ATP_Translate open Sledgehammer_Util +open Sledgehammer_Filter open Sledgehammer_Provers open Sledgehammer_Minimize open Sledgehammer_Run @@ -46,7 +47,6 @@ (** Sledgehammer commands **) -val no_relevance_override = {add = [], del = [], only = false} fun add_relevance_override ns : relevance_override = {add = ns, del = [], only = false} fun del_relevance_override ns : relevance_override = diff -r f9334afb6945 -r 85103fbc9004 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Aug 24 17:30:25 2011 +0200 @@ -57,16 +57,16 @@ (if verbose then " (timeout: " ^ string_from_time timeout ^ ")" else "") ^ "...") val {goal, ...} = Proof.goal state + val facts = + facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) val params = {debug = debug, verbose = verbose, overlord = overlord, blocking = true, provers = provers, type_enc = type_enc, sound = true, - relevance_thresholds = (1.01, 1.01), max_relevant = NONE, + relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, slicing = false, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} - val facts = - facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, facts = facts, smt_filter = NONE} diff -r f9334afb6945 -r 85103fbc9004 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Wed Aug 24 17:25:45 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Wed Aug 24 17:30:25 2011 +0200 @@ -7,16 +7,22 @@ signature SLEDGEHAMMER_TACTICS = sig + type relevance_override = Sledgehammer_Filter.relevance_override + val sledgehammer_with_metis_tac : - Proof.context -> (string * string) list -> int -> tactic + Proof.context -> (string * string) list -> relevance_override -> int + -> tactic val sledgehammer_as_oracle_tac : - Proof.context -> (string * string) list -> int -> tactic + Proof.context -> (string * string) list -> relevance_override -> int + -> tactic end; structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = struct -fun run_atp override_params i n ctxt goal = +open Sledgehammer_Filter + +fun run_atp override_params relevance_override i n ctxt goal = let val chained_ths = [] (* a tactic has no chained ths *) val params as {provers, relevance_thresholds, max_relevant, slicing, ...} = @@ -30,7 +36,6 @@ Sledgehammer_Provers.is_built_in_const_for_prover ctxt name val relevance_fudge = Sledgehammer_Provers.relevance_fudge_for_prover ctxt name - val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i val facts = Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths @@ -62,16 +67,17 @@ |> Source.exhaust end -fun sledgehammer_with_metis_tac ctxt override_params i th = - case run_atp override_params i i ctxt th of +fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th = + case run_atp override_params relevance_override i i ctxt th of SOME facts => Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th | NONE => Seq.empty -fun sledgehammer_as_oracle_tac ctxt override_params i th = +fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th = let val thy = Proof_Context.theory_of ctxt - val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th + val xs = run_atp (override_params @ [("sound", "true")]) relevance_override + i i ctxt th in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end end;