--- a/src/HOL/Hyperreal/SEQ.thy Mon Mar 17 22:34:25 2008 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy Mon Mar 17 22:34:26 2008 +0100
@@ -56,7 +56,7 @@
subsection {* Bounded Sequences *}
-lemma BseqI: assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
+lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
unfolding Bseq_def
proof (intro exI conjI allI)
show "0 < max K 1" by simp
@@ -66,14 +66,11 @@
thus "norm (X n) \<le> max K 1" by simp
qed
-lemma BseqD: "Bseq X \<Longrightarrow> \<exists>K>0. \<forall>n. norm (X n) \<le> K"
-unfolding Bseq_def by simp
-
lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
unfolding Bseq_def by auto
-lemma BseqI2: assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X"
-proof (rule BseqI)
+lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X"
+proof (rule BseqI')
let ?A = "norm ` X ` {..N}"
have 1: "finite ?A" by simp
have 2: "?A \<noteq> {}" by auto
@@ -96,7 +93,7 @@
lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
apply (erule BseqE)
-apply (rule_tac N="k" and K="K" in BseqI2)
+apply (rule_tac N="k" and K="K" in BseqI2')
apply clarify
apply (drule_tac x="n - k" in spec, simp)
done
@@ -413,7 +410,7 @@
obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r"
using LIMSEQ_D [OF X r1] by fast
show ?thesis
- proof (rule BseqI2 [rule_format])
+ proof (rule BseqI2' [rule_format])
fix n assume n: "N \<le> n"
hence 1: "norm (X n - a) < r" by (rule N)
hence 2: "X n \<noteq> 0" using r2 by auto
--- a/src/HOL/Library/Executable_Set.thy Mon Mar 17 22:34:25 2008 +0100
+++ b/src/HOL/Library/Executable_Set.thy Mon Mar 17 22:34:26 2008 +0100
@@ -99,7 +99,7 @@
by pat_completeness auto
termination by lexicographic_order
-lemmas unionl_def = unionl.simps(2)
+lemmas unionl_eq = unionl.simps(2)
function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
@@ -109,7 +109,7 @@
by pat_completeness auto
termination by lexicographic_order
-lemmas intersect_def = intersect.simps(3)
+lemmas intersect_eq = intersect.simps(3)
function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
@@ -119,7 +119,7 @@
by pat_completeness auto
termination by lexicographic_order
-lemmas subtract_def = subtract.simps(3)
+lemmas subtract_eq = subtract.simps(3)
function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
where
@@ -128,7 +128,7 @@
by pat_completeness auto
termination by lexicographic_order
-lemmas map_distinct_def = map_distinct.simps(2)
+lemmas map_distinct_eq = map_distinct.simps(2)
function unions :: "'a list list \<Rightarrow> 'a list"
where
@@ -137,7 +137,7 @@
by pat_completeness auto
termination by lexicographic_order
-lemmas unions_def = unions.simps(2)
+lemmas unions_eq = unions.simps(2)
consts intersects :: "'a list list \<Rightarrow> 'a list"
primrec
@@ -169,12 +169,12 @@
lemma iso_union:
"set (unionl xs ys) = set xs \<union> set ys"
- unfolding unionl_def
+ unfolding unionl_eq
by (induct xs arbitrary: ys) (simp_all add: iso_insert)
lemma iso_intersect:
"set (intersect xs ys) = set xs \<inter> set ys"
- unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
+ unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
definition
subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -185,16 +185,16 @@
assumes distnct: "distinct ys"
shows "set (subtract' ys xs) = set ys - set xs"
and "distinct (subtract' ys xs)"
- unfolding subtract'_def flip_def subtract_def
+ unfolding subtract'_def flip_def subtract_eq
using distnct by (induct xs arbitrary: ys) auto
lemma iso_map_distinct:
"set (map_distinct f xs) = image f (set xs)"
- unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
+ unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
lemma iso_unions:
"set (unions xss) = \<Union> set (map set xss)"
- unfolding unions_def
+ unfolding unions_eq
proof (induct xss)
case Nil show ?case by simp
next
--- a/src/HOL/MetisExamples/BT.thy Mon Mar 17 22:34:25 2008 +0100
+++ b/src/HOL/MetisExamples/BT.thy Mon Mar 17 22:34:26 2008 +0100
@@ -232,7 +232,7 @@
done
ML {*ResAtp.problem_name := "BT__bt_map_appnd"*}
-lemma bt_map_appnd:
+lemma (*bt_map_appnd:*)
"bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
apply (induct t1)
apply (metis appnd.simps(1) bt_map_appnd)
--- a/src/HOL/MetisExamples/BigO.thy Mon Mar 17 22:34:25 2008 +0100
+++ b/src/HOL/MetisExamples/BigO.thy Mon Mar 17 22:34:26 2008 +0100
@@ -33,7 +33,7 @@
declare [[reconstruction_modulus = 1]]
-lemma bigo_pos_const: "(EX (c::'a::ordered_idom).
+lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
= (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
apply auto
@@ -374,7 +374,7 @@
apply (metis OrderedGroup.abs_le_D1 Orderings.linorder_class.not_less order_less_le Orderings.xt1(12) Ring_and_Field.abs_mult)
done
-lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
+lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==>
f : O(g)"
apply (auto simp add: bigo_def)
(*Version 2: single-step proof*)
--- a/src/HOL/MetisExamples/set.thy Mon Mar 17 22:34:25 2008 +0100
+++ b/src/HOL/MetisExamples/set.thy Mon Mar 17 22:34:26 2008 +0100
@@ -215,7 +215,7 @@
"\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
by metis
-lemma fixedpoint:
+lemma (*fixedpoint:*)
"\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
proof (neg_clausify)
fix x xa