avoid warnings
authorhuffman
Mon Aug 22 17:22:49 2011 -0700 (2011-08-22)
changeset 444546f28f96a09bf
parent 44453 082edd97ffe1
child 44455 8382f4c2470c
avoid warnings
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/positivstellensatz.ML
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/normarith.ML
     1.1 --- a/src/HOL/Library/Infinite_Set.thy	Mon Aug 22 16:49:45 2011 -0700
     1.2 +++ b/src/HOL/Library/Infinite_Set.thy	Mon Aug 22 17:22:49 2011 -0700
     1.3 @@ -546,7 +546,7 @@
     1.4  apply (induct n arbitrary: S)
     1.5   apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
     1.6  apply simp
     1.7 -apply (metis Collect_mem_eq DiffE infinite_remove)
     1.8 +apply (metis DiffE infinite_remove)
     1.9  done
    1.10  
    1.11  declare enumerate_0 [simp del] enumerate_Suc [simp del]
     2.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Aug 22 16:49:45 2011 -0700
     2.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Aug 22 17:22:49 2011 -0700
     2.3 @@ -204,10 +204,12 @@
     2.4      @{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and
     2.5        "(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+};
     2.6  
     2.7 +(*
     2.8  val nnfD_simps =
     2.9    @{lemma "((~(P & Q)) = (~P | ~Q))" and "((~(P | Q)) = (~P & ~Q) )" and
    2.10      "((P --> Q) = (~P | Q) )" and "((P = Q) = ((P & Q) | (~P & ~ Q)))" and
    2.11      "((~(P = Q)) = ((P & ~ Q) | (~P & Q)) )" and "((~ ~(P)) = P)" by blast+};
    2.12 +*)
    2.13  
    2.14  val choice_iff = @{lemma "(ALL x. EX y. P x y) = (EX f. ALL x. P x (f x))" by metis};
    2.15  val prenex_simps =
    2.16 @@ -293,16 +295,18 @@
    2.17   | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
    2.18   fun is_ratconst t = can dest_ratconst t
    2.19  
    2.20 +(*
    2.21  fun find_term p t = if p t then t else 
    2.22   case t of
    2.23    a$b => (find_term p a handle TERM _ => find_term p b)
    2.24   | Abs (_,_,t') => find_term p t'
    2.25   | _ => raise TERM ("find_term",[t]);
    2.26 +*)
    2.27  
    2.28  fun find_cterm p t = if p t then t else 
    2.29   case term_of t of
    2.30 -  a$b => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
    2.31 - | Abs (_,_,t') => find_cterm p (Thm.dest_abs NONE t |> snd)
    2.32 +  _$_ => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
    2.33 + | Abs (_,_,_) => find_cterm p (Thm.dest_abs NONE t |> snd)
    2.34   | _ => raise CTERM ("find_cterm",[t]);
    2.35  
    2.36      (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
    2.37 @@ -477,7 +481,7 @@
    2.38   val strip_exists =
    2.39    let fun h (acc, t) =
    2.40     case (term_of t) of
    2.41 -    Const(@{const_name Ex},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    2.42 +    Const(@{const_name Ex},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    2.43    | _ => (acc,t)
    2.44    in fn t => h ([],t)
    2.45    end
    2.46 @@ -512,7 +516,7 @@
    2.47   val strip_forall =
    2.48    let fun h (acc, t) =
    2.49     case (term_of t) of
    2.50 -    Const(@{const_name All},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    2.51 +    Const(@{const_name All},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
    2.52    | _ => (acc,t)
    2.53    in fn t => h ([],t)
    2.54    end
    2.55 @@ -725,7 +729,7 @@
    2.56  fun gen_prover_real_arith ctxt prover = 
    2.57   let
    2.58    fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
    2.59 -  val {add,mul,neg,pow,sub,main} = 
    2.60 +  val {add, mul, neg, pow = _, sub = _, main} = 
    2.61       Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    2.62        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
    2.63       simple_cterm_ord
     3.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Aug 22 16:49:45 2011 -0700
     3.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Aug 22 17:22:49 2011 -0700
     3.3 @@ -215,8 +215,8 @@
     3.4  next
     3.5    assume ?rhs
     3.6    then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0" by simp
     3.7 -  hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0" by (simp add: inner_simps inner_commute)
     3.8 -  then have "(x - y) \<bullet> (x - y) = 0" by (simp add: field_simps inner_simps inner_commute)
     3.9 +  hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0" by (simp add: inner_diff inner_commute)
    3.10 +  then have "(x - y) \<bullet> (x - y) = 0" by (simp add: field_simps inner_diff inner_commute)
    3.11    then show "x = y" by (simp)
    3.12  qed
    3.13  
    3.14 @@ -378,15 +378,15 @@
    3.15    by (auto intro: setsum_0')
    3.16  
    3.17  lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> y = setsum (\<lambda>x. f x \<bullet> y) S "
    3.18 -  apply(induct rule: finite_induct) by(auto simp add: inner_simps)
    3.19 +  apply(induct rule: finite_induct) by(auto simp add: inner_add)
    3.20  
    3.21  lemma dot_rsum: "finite S \<Longrightarrow> y \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
    3.22 -  apply(induct rule: finite_induct) by(auto simp add: inner_simps)
    3.23 +  apply(induct rule: finite_induct) by(auto simp add: inner_add)
    3.24  
    3.25  lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
    3.26  proof
    3.27    assume "\<forall>x. x \<bullet> y = x \<bullet> z"
    3.28 -  hence "\<forall>x. x \<bullet> (y - z) = 0" by (simp add: inner_simps)
    3.29 +  hence "\<forall>x. x \<bullet> (y - z) = 0" by (simp add: inner_diff)
    3.30    hence "(y - z) \<bullet> (y - z) = 0" ..
    3.31    thus "y = z" by simp
    3.32  qed simp
    3.33 @@ -394,7 +394,7 @@
    3.34  lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y"
    3.35  proof
    3.36    assume "\<forall>z. x \<bullet> z = y \<bullet> z"
    3.37 -  hence "\<forall>z. (x - y) \<bullet> z = 0" by (simp add: inner_simps)
    3.38 +  hence "\<forall>z. (x - y) \<bullet> z = 0" by (simp add: inner_diff)
    3.39    hence "(x - y) \<bullet> (x - y) = 0" ..
    3.40    thus "x = y" by simp
    3.41  qed simp
    3.42 @@ -2146,7 +2146,7 @@
    3.43          apply (subst Cy)
    3.44          using C(1) fth
    3.45          apply (simp only: setsum_clauses)
    3.46 -        apply (auto simp add: inner_simps inner_commute[of y a] dot_lsum[OF fth])
    3.47 +        apply (auto simp add: inner_add inner_commute[of y a] dot_lsum[OF fth])
    3.48          apply (rule setsum_0')
    3.49          apply clarsimp
    3.50          apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
    3.51 @@ -2163,7 +2163,7 @@
    3.52          using C(1) fth
    3.53          apply (simp only: setsum_clauses)
    3.54          apply (subst inner_commute[of x])
    3.55 -        apply (auto simp add: inner_simps inner_commute[of x a] dot_rsum[OF fth])
    3.56 +        apply (auto simp add: inner_add inner_commute[of x a] dot_rsum[OF fth])
    3.57          apply (rule setsum_0')
    3.58          apply clarsimp
    3.59          apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
    3.60 @@ -2224,7 +2224,7 @@
    3.61    with a have a0:"?a  \<noteq> 0" by auto
    3.62    have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
    3.63    proof(rule span_induct')
    3.64 -    show "subspace {x. ?a \<bullet> x = 0}" by (auto simp add: subspace_def inner_simps)
    3.65 +    show "subspace {x. ?a \<bullet> x = 0}" by (auto simp add: subspace_def inner_add)
    3.66  next
    3.67      {fix x assume x: "x \<in> B"
    3.68        from x have B': "B = insert x (B - {x})" by blast
    3.69 @@ -2233,7 +2233,7 @@
    3.70          apply (subst B') using fB fth
    3.71          unfolding setsum_clauses(2)[OF fth]
    3.72          apply simp unfolding inner_simps
    3.73 -        apply (clarsimp simp add: inner_simps dot_lsum)
    3.74 +        apply (clarsimp simp add: inner_add dot_lsum)
    3.75          apply (rule setsum_0', rule ballI)
    3.76          unfolding inner_commute
    3.77          by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
    3.78 @@ -2534,7 +2534,7 @@
    3.79      from equalityD2[OF span_basis'[where 'a='a]]
    3.80      have IU: " (UNIV :: 'a set) \<subseteq> span ?I" by blast
    3.81      have "f x = g x" apply(rule linear_eq[OF lf lg IU,rule_format]) using fg x by auto }
    3.82 -  then show ?thesis by (auto intro: ext)
    3.83 +  then show ?thesis by auto
    3.84  qed
    3.85  
    3.86  text {* Similar results for bilinear functions. *}
    3.87 @@ -2559,7 +2559,7 @@
    3.88      apply (auto simp add: subspace_def)
    3.89      using bf bg unfolding bilinear_def linear_def
    3.90      by(auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro:  bilinear_ladd[OF bf])
    3.91 -  then show ?thesis using SB TC by (auto intro: ext)
    3.92 +  then show ?thesis using SB TC by auto
    3.93  qed
    3.94  
    3.95  lemma bilinear_eq_stdbasis: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> _"
    3.96 @@ -2570,7 +2570,7 @@
    3.97  proof-
    3.98    from fg have th: "\<forall>x \<in> (basis ` {..<DIM('a)}). \<forall>y\<in> (basis ` {..<DIM('b)}). f x y = g x y" by blast
    3.99    from bilinear_eq[OF bf bg equalityD2[OF span_basis'] equalityD2[OF span_basis'] th]
   3.100 -  show ?thesis by (blast intro: ext)
   3.101 +  show ?thesis by blast
   3.102  qed
   3.103  
   3.104  text {* Detailed theorems about left and right invertibility in general case. *}
   3.105 @@ -2836,7 +2836,7 @@
   3.106  lemma infnorm_neg: "infnorm (- x) = infnorm x"
   3.107    unfolding infnorm_def
   3.108    apply (rule cong[of "Sup" "Sup"])
   3.109 -  apply blast by(auto simp add: euclidean_simps)
   3.110 +  apply blast by(auto simp add: euclidean_component_minus)
   3.111  
   3.112  lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
   3.113  proof-
   3.114 @@ -2851,7 +2851,7 @@
   3.115    from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
   3.116    have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
   3.117      "infnorm y \<le> infnorm (x - y) + infnorm x"
   3.118 -    by (simp_all add: field_simps infnorm_neg diff_minus[symmetric])
   3.119 +    by (simp_all add: field_simps infnorm_neg)
   3.120    from th[OF ths]  show ?thesis .
   3.121  qed
   3.122  
     4.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Mon Aug 22 16:49:45 2011 -0700
     4.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Mon Aug 22 17:22:49 2011 -0700
     4.3 @@ -26,7 +26,7 @@
     4.4   fun find_normedterms t acc = case term_of t of
     4.5      @{term "op + :: real => _"}$_$_ =>
     4.6              find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
     4.7 -      | @{term "op * :: real => _"}$_$n =>
     4.8 +      | @{term "op * :: real => _"}$_$_ =>
     4.9              if not (is_ratconst (Thm.dest_arg1 t)) then acc else
    4.10              augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero)
    4.11                        (Thm.dest_arg t) acc
    4.12 @@ -39,12 +39,16 @@
    4.13   fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
    4.14   fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
    4.15  
    4.16 +(*
    4.17   val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
    4.18 +*)
    4.19   fun int_lincomb_cmul c t =
    4.20      if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x */ c) t
    4.21   fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
    4.22 +(*
    4.23   fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
    4.24   fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
    4.25 +*)
    4.26  
    4.27  fun vector_lincomb t = case term_of t of
    4.28     Const(@{const_name plus}, _) $ _ $ _ =>
    4.29 @@ -82,9 +86,11 @@
    4.30  | @{term "op * :: real => _"}$_$_ =>
    4.31      if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive t
    4.32  | _ => Thm.reflexive t
    4.33 +(*
    4.34  fun flip v eq =
    4.35    if FuncUtil.Ctermfunc.defined eq v
    4.36    then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
    4.37 +*)
    4.38  fun allsubsets s = case s of
    4.39    [] => [[]]
    4.40  |(a::t) => let val res = allsubsets t in
    4.41 @@ -178,8 +184,8 @@
    4.42  
    4.43  fun headvector t = case t of
    4.44    Const(@{const_name plus}, _)$
    4.45 -   (Const(@{const_name scaleR}, _)$l$v)$r => v
    4.46 - | Const(@{const_name scaleR}, _)$l$v => v
    4.47 +   (Const(@{const_name scaleR}, _)$_$v)$_ => v
    4.48 + | Const(@{const_name scaleR}, _)$_$v => v
    4.49   | _ => error "headvector: non-canonical term"
    4.50  
    4.51  fun vector_cmul_conv ct =