--- 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]
--- 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
--- 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
--- 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 =