# HG changeset patch
# User haftmann
# Date 1213104656 -7200
# Node ID ff27dc6e7d05ebd6e31651763f0e31dac17b2fb6
# Parent  5f139027c3653201b320b4b0784fe4a8ab401e44
removed some dubious code lemmas

diff -r 5f139027c365 -r ff27dc6e7d05 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/Fun.thy	Tue Jun 10 15:30:56 2008 +0200
@@ -117,7 +117,7 @@
 
 definition
   bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
-  "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
+  [code func del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
 
 constdefs
   surj :: "('a => 'b) => bool"                   (*surjective*)
diff -r 5f139027c365 -r ff27dc6e7d05 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/Int.thy	Tue Jun 10 15:30:56 2008 +0200
@@ -24,7 +24,7 @@
 definition
   intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
 where
-  "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
+  [code func del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
 
 typedef (Integ)
   int = "UNIV//intrel"
@@ -1167,7 +1167,7 @@
 definition
   Ints  :: "'a set"
 where
-  "Ints = range of_int"
+  [code func del]: "Ints = range of_int"
 
 end
 
@@ -1688,12 +1688,12 @@
 lemma int_val_lemma:
      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
-apply (induct_tac "n", simp)
+apply (induct n, simp)
 apply (intro strip)
 apply (erule impE, simp)
 apply (erule_tac x = n in allE, simp)
 apply (case_tac "k = f (n+1) ")
- apply force
+apply force
 apply (erule impE)
  apply (simp add: abs_if split add: split_if_asm)
 apply (blast intro: le_SucI)
diff -r 5f139027c365 -r ff27dc6e7d05 src/HOL/Library/GCD.thy
--- a/src/HOL/Library/GCD.thy	Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/Library/GCD.thy	Tue Jun 10 15:30:56 2008 +0200
@@ -18,7 +18,7 @@
 
 definition
   is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
-  "is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
+  [code func del]: "is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
     (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
 
 text {* Uniqueness *}
diff -r 5f139027c365 -r ff27dc6e7d05 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue Jun 10 15:30:56 2008 +0200
@@ -500,7 +500,7 @@
 
 definition
   mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
-  "mult1 r =
+  [code func del]:"mult1 r =
     {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
       (\<forall>b. b :# K --> (b, a) \<in> r)}"
 
@@ -716,10 +716,10 @@
 begin
 
 definition
-  less_multiset_def: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
+  less_multiset_def [code func del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
 
 definition
-  le_multiset_def: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
+  le_multiset_def [code func del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
 
 lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
 unfolding trans_def by (blast intro: order_less_trans)
@@ -988,11 +988,11 @@
 
 definition
   mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
-  "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
+  [code func del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
 
 definition
   mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
-  "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
+  [code func del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
 
 notation mset_le  (infix "\<subseteq>#" 50)
 notation mset_less  (infix "\<subset>#" 50)
diff -r 5f139027c365 -r ff27dc6e7d05 src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/Library/Primes.thy	Tue Jun 10 15:30:56 2008 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Library/Primes.thy
     ID:         $Id$
-    Author:     Amine Chaieb Christophe Tabacznyj and Lawrence C Paulson
+    Author:     Amine Chaieb, Christophe Tabacznyj and Lawrence C Paulson
     Copyright   1996  University of Cambridge
 *)
 
@@ -16,7 +16,7 @@
 
 definition
   prime :: "nat \<Rightarrow> bool" where
-  "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+  [code func del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
 
 
 lemma two_is_prime: "prime 2"
diff -r 5f139027c365 -r ff27dc6e7d05 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/Library/Word.thy	Tue Jun 10 15:30:56 2008 +0200
@@ -2042,7 +2042,7 @@
 
 definition
   length_nat :: "nat => nat" where
-  "length_nat x = (LEAST n. x < 2 ^ n)"
+  [code func del]: "length_nat x = (LEAST n. x < 2 ^ n)"
 
 lemma length_nat: "length (nat_to_bv n) = length_nat n"
   apply (simp add: length_nat_def)
diff -r 5f139027c365 -r ff27dc6e7d05 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/List.thy	Tue Jun 10 15:30:56 2008 +0200
@@ -2831,7 +2831,7 @@
 
 definition
  sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
-"sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
+ [code func del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
 
 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
   set(sorted_list_of_set A) = A &
@@ -2993,6 +2993,7 @@
 constdefs
   set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
   "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
+declare set_Cons_def [code func del]
 
 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
 by (auto simp add: set_Cons_def)
@@ -3030,6 +3031,8 @@
     "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
         --{*Compares lists by their length and then lexicographically*}
 
+declare lex_def [code func del]
+
 
 lemma wf_lexn: "wf r ==> wf (lexn r n)"
 apply (induct n, simp, simp)
@@ -3104,6 +3107,7 @@
   lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set" 
   "lexord  r == {(x,y). \<exists> a v. y = x @ a # v \<or> 
             (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
+declare lexord_def [code func del]
 
 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
 by (unfold lexord_def, induct_tac y, auto) 
diff -r 5f139027c365 -r ff27dc6e7d05 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/Real/PReal.thy	Tue Jun 10 15:30:56 2008 +0200
@@ -19,7 +19,7 @@
 
 definition
   cut :: "rat set => bool" where
-  "cut A = ({} \<subset> A &
+  [code func del]: "cut A = ({} \<subset> A &
             A < {r. 0 < r} &
             (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
 
@@ -56,7 +56,7 @@
 
 definition
   diff_set :: "[rat set,rat set] => rat set" where
-  "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
+  [code func del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
 
 definition
   mult_set :: "[rat set,rat set] => rat set" where
@@ -64,17 +64,17 @@
 
 definition
   inverse_set :: "rat set => rat set" where
-  "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
+  [code func del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
 
 instantiation preal :: "{ord, plus, minus, times, inverse, one}"
 begin
 
 definition
-  preal_less_def:
+  preal_less_def [code func del]:
     "R < S == Rep_preal R < Rep_preal S"
 
 definition
-  preal_le_def:
+  preal_le_def [code func del]:
     "R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
 
 definition
diff -r 5f139027c365 -r ff27dc6e7d05 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/Real/RealDef.thy	Tue Jun 10 15:30:56 2008 +0200
@@ -15,7 +15,7 @@
 
 definition
   realrel   ::  "((preal * preal) * (preal * preal)) set" where
-  "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
+  [code func del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
 
 typedef (Real)  real = "UNIV//realrel"
   by (auto simp add: quotient_def)
diff -r 5f139027c365 -r ff27dc6e7d05 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/Set.thy	Tue Jun 10 15:30:56 2008 +0200
@@ -2156,7 +2156,7 @@
 definition
   contents :: "'a set \<Rightarrow> 'a"
 where
-  "contents X = (THE x. X = {x})"
+  [code func del]: "contents X = (THE x. X = {x})"
 
 lemma contents_eq [simp]: "contents {x} = x"
   by (simp add: contents_def)
@@ -2202,13 +2202,6 @@
   apply (auto elim: monoD intro!: order_antisym)
   done
 
-lemma Least_equality:
-  "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
-apply (simp add: Least_def)
-apply (rule the_equality)
-apply (auto intro!: order_antisym)
-done
-
 
 subsection {* Basic ML bindings *}