--- 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*)
--- 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)
--- 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 *}
--- 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)
--- 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"
--- 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)
--- 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)
--- 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
--- 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)
--- 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 *}