# HG changeset patch
# User huffman
# Date 1314058969 25200
# Node ID 6f28f96a09bf4988a72edec9f75c452cf246e0c7
# Parent  082edd97ffe13cf87b654c603387bc89b7504b1c
avoid warnings

diff -r 082edd97ffe1 -r 6f28f96a09bf src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Aug 22 16:49:45 2011 -0700
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Aug 22 17:22:49 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]
diff -r 082edd97ffe1 -r 6f28f96a09bf src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Mon Aug 22 16:49:45 2011 -0700
+++ b/src/HOL/Library/positivstellensatz.ML	Mon Aug 22 17:22:49 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
diff -r 082edd97ffe1 -r 6f28f96a09bf src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Aug 22 16:49:45 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Aug 22 17:22:49 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
@@ -2146,7 +2146,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])
@@ -2163,7 +2163,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])
@@ -2224,7 +2224,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
@@ -2233,7 +2233,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])}
@@ -2534,7 +2534,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. *}
@@ -2559,7 +2559,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> _"
@@ -2570,7 +2570,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. *}
@@ -2836,7 +2836,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 simp add: euclidean_component_minus)
 
 lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
 proof-
@@ -2851,7 +2851,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
 
diff -r 082edd97ffe1 -r 6f28f96a09bf src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Mon Aug 22 16:49:45 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Mon Aug 22 17:22:49 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 =