removed some dubious code lemmas
authorhaftmann
Tue Jun 10 15:30:56 2008 +0200 (2008-06-10)
changeset 27106ff27dc6e7d05
parent 27105 5f139027c365
child 27107 4a7415c67063
removed some dubious code lemmas
src/HOL/Fun.thy
src/HOL/Int.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Primes.thy
src/HOL/Library/Word.thy
src/HOL/List.thy
src/HOL/Real/PReal.thy
src/HOL/Real/RealDef.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Fun.thy	Tue Jun 10 15:30:54 2008 +0200
     1.2 +++ b/src/HOL/Fun.thy	Tue Jun 10 15:30:56 2008 +0200
     1.3 @@ -117,7 +117,7 @@
     1.4  
     1.5  definition
     1.6    bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
     1.7 -  "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
     1.8 +  [code func del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
     1.9  
    1.10  constdefs
    1.11    surj :: "('a => 'b) => bool"                   (*surjective*)
     2.1 --- a/src/HOL/Int.thy	Tue Jun 10 15:30:54 2008 +0200
     2.2 +++ b/src/HOL/Int.thy	Tue Jun 10 15:30:56 2008 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4  definition
     2.5    intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
     2.6  where
     2.7 -  "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
     2.8 +  [code func del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
     2.9  
    2.10  typedef (Integ)
    2.11    int = "UNIV//intrel"
    2.12 @@ -1167,7 +1167,7 @@
    2.13  definition
    2.14    Ints  :: "'a set"
    2.15  where
    2.16 -  "Ints = range of_int"
    2.17 +  [code func del]: "Ints = range of_int"
    2.18  
    2.19  end
    2.20  
    2.21 @@ -1688,12 +1688,12 @@
    2.22  lemma int_val_lemma:
    2.23       "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
    2.24        f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
    2.25 -apply (induct_tac "n", simp)
    2.26 +apply (induct n, simp)
    2.27  apply (intro strip)
    2.28  apply (erule impE, simp)
    2.29  apply (erule_tac x = n in allE, simp)
    2.30  apply (case_tac "k = f (n+1) ")
    2.31 - apply force
    2.32 +apply force
    2.33  apply (erule impE)
    2.34   apply (simp add: abs_if split add: split_if_asm)
    2.35  apply (blast intro: le_SucI)
     3.1 --- a/src/HOL/Library/GCD.thy	Tue Jun 10 15:30:54 2008 +0200
     3.2 +++ b/src/HOL/Library/GCD.thy	Tue Jun 10 15:30:56 2008 +0200
     3.3 @@ -18,7 +18,7 @@
     3.4  
     3.5  definition
     3.6    is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
     3.7 -  "is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
     3.8 +  [code func del]: "is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
     3.9      (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
    3.10  
    3.11  text {* Uniqueness *}
     4.1 --- a/src/HOL/Library/Multiset.thy	Tue Jun 10 15:30:54 2008 +0200
     4.2 +++ b/src/HOL/Library/Multiset.thy	Tue Jun 10 15:30:56 2008 +0200
     4.3 @@ -500,7 +500,7 @@
     4.4  
     4.5  definition
     4.6    mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
     4.7 -  "mult1 r =
     4.8 +  [code func del]:"mult1 r =
     4.9      {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
    4.10        (\<forall>b. b :# K --> (b, a) \<in> r)}"
    4.11  
    4.12 @@ -716,10 +716,10 @@
    4.13  begin
    4.14  
    4.15  definition
    4.16 -  less_multiset_def: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
    4.17 +  less_multiset_def [code func del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
    4.18  
    4.19  definition
    4.20 -  le_multiset_def: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
    4.21 +  le_multiset_def [code func del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
    4.22  
    4.23  lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
    4.24  unfolding trans_def by (blast intro: order_less_trans)
    4.25 @@ -988,11 +988,11 @@
    4.26  
    4.27  definition
    4.28    mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
    4.29 -  "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
    4.30 +  [code func del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
    4.31  
    4.32  definition
    4.33    mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
    4.34 -  "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
    4.35 +  [code func del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
    4.36  
    4.37  notation mset_le  (infix "\<subseteq>#" 50)
    4.38  notation mset_less  (infix "\<subset>#" 50)
     5.1 --- a/src/HOL/Library/Primes.thy	Tue Jun 10 15:30:54 2008 +0200
     5.2 +++ b/src/HOL/Library/Primes.thy	Tue Jun 10 15:30:56 2008 +0200
     5.3 @@ -1,6 +1,6 @@
     5.4  (*  Title:      HOL/Library/Primes.thy
     5.5      ID:         $Id$
     5.6 -    Author:     Amine Chaieb Christophe Tabacznyj and Lawrence C Paulson
     5.7 +    Author:     Amine Chaieb, Christophe Tabacznyj and Lawrence C Paulson
     5.8      Copyright   1996  University of Cambridge
     5.9  *)
    5.10  
    5.11 @@ -16,7 +16,7 @@
    5.12  
    5.13  definition
    5.14    prime :: "nat \<Rightarrow> bool" where
    5.15 -  "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    5.16 +  [code func del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    5.17  
    5.18  
    5.19  lemma two_is_prime: "prime 2"
     6.1 --- a/src/HOL/Library/Word.thy	Tue Jun 10 15:30:54 2008 +0200
     6.2 +++ b/src/HOL/Library/Word.thy	Tue Jun 10 15:30:56 2008 +0200
     6.3 @@ -2042,7 +2042,7 @@
     6.4  
     6.5  definition
     6.6    length_nat :: "nat => nat" where
     6.7 -  "length_nat x = (LEAST n. x < 2 ^ n)"
     6.8 +  [code func del]: "length_nat x = (LEAST n. x < 2 ^ n)"
     6.9  
    6.10  lemma length_nat: "length (nat_to_bv n) = length_nat n"
    6.11    apply (simp add: length_nat_def)
     7.1 --- a/src/HOL/List.thy	Tue Jun 10 15:30:54 2008 +0200
     7.2 +++ b/src/HOL/List.thy	Tue Jun 10 15:30:56 2008 +0200
     7.3 @@ -2831,7 +2831,7 @@
     7.4  
     7.5  definition
     7.6   sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
     7.7 -"sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
     7.8 + [code func del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
     7.9  
    7.10  lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
    7.11    set(sorted_list_of_set A) = A &
    7.12 @@ -2993,6 +2993,7 @@
    7.13  constdefs
    7.14    set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
    7.15    "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
    7.16 +declare set_Cons_def [code func del]
    7.17  
    7.18  lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
    7.19  by (auto simp add: set_Cons_def)
    7.20 @@ -3030,6 +3031,8 @@
    7.21      "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
    7.22          --{*Compares lists by their length and then lexicographically*}
    7.23  
    7.24 +declare lex_def [code func del]
    7.25 +
    7.26  
    7.27  lemma wf_lexn: "wf r ==> wf (lexn r n)"
    7.28  apply (induct n, simp, simp)
    7.29 @@ -3104,6 +3107,7 @@
    7.30    lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set" 
    7.31    "lexord  r == {(x,y). \<exists> a v. y = x @ a # v \<or> 
    7.32              (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
    7.33 +declare lexord_def [code func del]
    7.34  
    7.35  lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
    7.36  by (unfold lexord_def, induct_tac y, auto) 
     8.1 --- a/src/HOL/Real/PReal.thy	Tue Jun 10 15:30:54 2008 +0200
     8.2 +++ b/src/HOL/Real/PReal.thy	Tue Jun 10 15:30:56 2008 +0200
     8.3 @@ -19,7 +19,7 @@
     8.4  
     8.5  definition
     8.6    cut :: "rat set => bool" where
     8.7 -  "cut A = ({} \<subset> A &
     8.8 +  [code func del]: "cut A = ({} \<subset> A &
     8.9              A < {r. 0 < r} &
    8.10              (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
    8.11  
    8.12 @@ -56,7 +56,7 @@
    8.13  
    8.14  definition
    8.15    diff_set :: "[rat set,rat set] => rat set" where
    8.16 -  "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
    8.17 +  [code func del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
    8.18  
    8.19  definition
    8.20    mult_set :: "[rat set,rat set] => rat set" where
    8.21 @@ -64,17 +64,17 @@
    8.22  
    8.23  definition
    8.24    inverse_set :: "rat set => rat set" where
    8.25 -  "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
    8.26 +  [code func del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
    8.27  
    8.28  instantiation preal :: "{ord, plus, minus, times, inverse, one}"
    8.29  begin
    8.30  
    8.31  definition
    8.32 -  preal_less_def:
    8.33 +  preal_less_def [code func del]:
    8.34      "R < S == Rep_preal R < Rep_preal S"
    8.35  
    8.36  definition
    8.37 -  preal_le_def:
    8.38 +  preal_le_def [code func del]:
    8.39      "R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
    8.40  
    8.41  definition
     9.1 --- a/src/HOL/Real/RealDef.thy	Tue Jun 10 15:30:54 2008 +0200
     9.2 +++ b/src/HOL/Real/RealDef.thy	Tue Jun 10 15:30:56 2008 +0200
     9.3 @@ -15,7 +15,7 @@
     9.4  
     9.5  definition
     9.6    realrel   ::  "((preal * preal) * (preal * preal)) set" where
     9.7 -  "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
     9.8 +  [code func del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
     9.9  
    9.10  typedef (Real)  real = "UNIV//realrel"
    9.11    by (auto simp add: quotient_def)
    10.1 --- a/src/HOL/Set.thy	Tue Jun 10 15:30:54 2008 +0200
    10.2 +++ b/src/HOL/Set.thy	Tue Jun 10 15:30:56 2008 +0200
    10.3 @@ -2156,7 +2156,7 @@
    10.4  definition
    10.5    contents :: "'a set \<Rightarrow> 'a"
    10.6  where
    10.7 -  "contents X = (THE x. X = {x})"
    10.8 +  [code func del]: "contents X = (THE x. X = {x})"
    10.9  
   10.10  lemma contents_eq [simp]: "contents {x} = x"
   10.11    by (simp add: contents_def)
   10.12 @@ -2202,13 +2202,6 @@
   10.13    apply (auto elim: monoD intro!: order_antisym)
   10.14    done
   10.15  
   10.16 -lemma Least_equality:
   10.17 -  "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   10.18 -apply (simp add: Least_def)
   10.19 -apply (rule the_equality)
   10.20 -apply (auto intro!: order_antisym)
   10.21 -done
   10.22 -
   10.23  
   10.24  subsection {* Basic ML bindings *}
   10.25