avoid rebinding of existing facts;
authorwenzelm
Mon Mar 17 22:34:26 2008 +0100 (2008-03-17)
changeset 26312e9a65675e5e8
parent 26311 81a0fc28b0de
child 26313 8590bf5ef343
avoid rebinding of existing facts;
src/HOL/Hyperreal/SEQ.thy
src/HOL/Library/Executable_Set.thy
src/HOL/MetisExamples/BT.thy
src/HOL/MetisExamples/BigO.thy
src/HOL/MetisExamples/set.thy
     1.1 --- a/src/HOL/Hyperreal/SEQ.thy	Mon Mar 17 22:34:25 2008 +0100
     1.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Mon Mar 17 22:34:26 2008 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4  
     1.5  subsection {* Bounded Sequences *}
     1.6  
     1.7 -lemma BseqI: assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
     1.8 +lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
     1.9  unfolding Bseq_def
    1.10  proof (intro exI conjI allI)
    1.11    show "0 < max K 1" by simp
    1.12 @@ -66,14 +66,11 @@
    1.13    thus "norm (X n) \<le> max K 1" by simp
    1.14  qed
    1.15  
    1.16 -lemma BseqD: "Bseq X \<Longrightarrow> \<exists>K>0. \<forall>n. norm (X n) \<le> K"
    1.17 -unfolding Bseq_def by simp
    1.18 -
    1.19  lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    1.20  unfolding Bseq_def by auto
    1.21  
    1.22 -lemma BseqI2: assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X"
    1.23 -proof (rule BseqI)
    1.24 +lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X"
    1.25 +proof (rule BseqI')
    1.26    let ?A = "norm ` X ` {..N}"
    1.27    have 1: "finite ?A" by simp
    1.28    have 2: "?A \<noteq> {}" by auto
    1.29 @@ -96,7 +93,7 @@
    1.30  
    1.31  lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
    1.32  apply (erule BseqE)
    1.33 -apply (rule_tac N="k" and K="K" in BseqI2)
    1.34 +apply (rule_tac N="k" and K="K" in BseqI2')
    1.35  apply clarify
    1.36  apply (drule_tac x="n - k" in spec, simp)
    1.37  done
    1.38 @@ -413,7 +410,7 @@
    1.39    obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r"
    1.40      using LIMSEQ_D [OF X r1] by fast
    1.41    show ?thesis
    1.42 -  proof (rule BseqI2 [rule_format])
    1.43 +  proof (rule BseqI2' [rule_format])
    1.44      fix n assume n: "N \<le> n"
    1.45      hence 1: "norm (X n - a) < r" by (rule N)
    1.46      hence 2: "X n \<noteq> 0" using r2 by auto
     2.1 --- a/src/HOL/Library/Executable_Set.thy	Mon Mar 17 22:34:25 2008 +0100
     2.2 +++ b/src/HOL/Library/Executable_Set.thy	Mon Mar 17 22:34:26 2008 +0100
     2.3 @@ -99,7 +99,7 @@
     2.4  by pat_completeness auto
     2.5  termination by lexicographic_order
     2.6  
     2.7 -lemmas unionl_def = unionl.simps(2)
     2.8 +lemmas unionl_eq = unionl.simps(2)
     2.9  
    2.10  function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    2.11  where
    2.12 @@ -109,7 +109,7 @@
    2.13  by pat_completeness auto
    2.14  termination by lexicographic_order
    2.15  
    2.16 -lemmas intersect_def = intersect.simps(3)
    2.17 +lemmas intersect_eq = intersect.simps(3)
    2.18  
    2.19  function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    2.20  where
    2.21 @@ -119,7 +119,7 @@
    2.22  by pat_completeness auto
    2.23  termination by lexicographic_order
    2.24  
    2.25 -lemmas subtract_def = subtract.simps(3)
    2.26 +lemmas subtract_eq = subtract.simps(3)
    2.27  
    2.28  function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
    2.29  where
    2.30 @@ -128,7 +128,7 @@
    2.31  by pat_completeness auto
    2.32  termination by lexicographic_order
    2.33  
    2.34 -lemmas map_distinct_def = map_distinct.simps(2)
    2.35 +lemmas map_distinct_eq = map_distinct.simps(2)
    2.36  
    2.37  function unions :: "'a list list \<Rightarrow> 'a list"
    2.38  where
    2.39 @@ -137,7 +137,7 @@
    2.40  by pat_completeness auto
    2.41  termination by lexicographic_order
    2.42  
    2.43 -lemmas unions_def = unions.simps(2)
    2.44 +lemmas unions_eq = unions.simps(2)
    2.45  
    2.46  consts intersects :: "'a list list \<Rightarrow> 'a list"
    2.47  primrec
    2.48 @@ -169,12 +169,12 @@
    2.49  
    2.50  lemma iso_union:
    2.51    "set (unionl xs ys) = set xs \<union> set ys"
    2.52 -  unfolding unionl_def
    2.53 +  unfolding unionl_eq
    2.54    by (induct xs arbitrary: ys) (simp_all add: iso_insert)
    2.55  
    2.56  lemma iso_intersect:
    2.57    "set (intersect xs ys) = set xs \<inter> set ys"
    2.58 -  unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
    2.59 +  unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
    2.60  
    2.61  definition
    2.62    subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    2.63 @@ -185,16 +185,16 @@
    2.64    assumes distnct: "distinct ys"
    2.65    shows "set (subtract' ys xs) = set ys - set xs"
    2.66      and "distinct (subtract' ys xs)"
    2.67 -  unfolding subtract'_def flip_def subtract_def
    2.68 +  unfolding subtract'_def flip_def subtract_eq
    2.69    using distnct by (induct xs arbitrary: ys) auto
    2.70  
    2.71  lemma iso_map_distinct:
    2.72    "set (map_distinct f xs) = image f (set xs)"
    2.73 -  unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
    2.74 +  unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
    2.75  
    2.76  lemma iso_unions:
    2.77    "set (unions xss) = \<Union> set (map set xss)"
    2.78 -  unfolding unions_def
    2.79 +  unfolding unions_eq
    2.80  proof (induct xss)
    2.81    case Nil show ?case by simp
    2.82  next
     3.1 --- a/src/HOL/MetisExamples/BT.thy	Mon Mar 17 22:34:25 2008 +0100
     3.2 +++ b/src/HOL/MetisExamples/BT.thy	Mon Mar 17 22:34:26 2008 +0100
     3.3 @@ -232,7 +232,7 @@
     3.4    done
     3.5  
     3.6  ML {*ResAtp.problem_name := "BT__bt_map_appnd"*}
     3.7 -lemma bt_map_appnd:
     3.8 +lemma (*bt_map_appnd:*)
     3.9       "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
    3.10    apply (induct t1)
    3.11    apply (metis appnd.simps(1) bt_map_appnd)
     4.1 --- a/src/HOL/MetisExamples/BigO.thy	Mon Mar 17 22:34:25 2008 +0100
     4.2 +++ b/src/HOL/MetisExamples/BigO.thy	Mon Mar 17 22:34:26 2008 +0100
     4.3 @@ -33,7 +33,7 @@
     4.4  
     4.5  declare [[reconstruction_modulus = 1]]
     4.6  
     4.7 -lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
     4.8 +lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
     4.9      ALL x. (abs (h x)) <= (c * (abs (f x))))
    4.10        = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
    4.11    apply auto
    4.12 @@ -374,7 +374,7 @@
    4.13    apply (metis OrderedGroup.abs_le_D1 Orderings.linorder_class.not_less  order_less_le  Orderings.xt1(12)  Ring_and_Field.abs_mult)
    4.14    done
    4.15  
    4.16 -lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
    4.17 +lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
    4.18      f : O(g)" 
    4.19    apply (auto simp add: bigo_def)
    4.20  (*Version 2: single-step proof*)
     5.1 --- a/src/HOL/MetisExamples/set.thy	Mon Mar 17 22:34:25 2008 +0100
     5.2 +++ b/src/HOL/MetisExamples/set.thy	Mon Mar 17 22:34:26 2008 +0100
     5.3 @@ -215,7 +215,7 @@
     5.4      "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
     5.5  by metis
     5.6  
     5.7 -lemma fixedpoint:
     5.8 +lemma (*fixedpoint:*)
     5.9      "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
    5.10  proof (neg_clausify)
    5.11  fix x xa