--- a/TFL/post.ML Sat May 27 17:42:00 2006 +0200
+++ b/TFL/post.ML Sat May 27 17:42:02 2006 +0200
@@ -156,7 +156,7 @@
(*lcp: curry the predicate of the induction rule*)
fun curry_rule rl =
- SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl)), rl);
+ SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
val meta_outer =
--- a/src/HOL/Complex/ex/NSPrimes.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy Sat May 27 17:42:02 2006 +0200
@@ -13,22 +13,15 @@
text{*These can be used to derive an alternative proof of the infinitude of
primes by considering a property of nonstandard sets.*}
-
-constdefs
+definition
hdvd :: "[hypnat, hypnat] => bool" (infixl "hdvd" 50)
- "(M::hypnat) hdvd N == ( *p2* (op dvd)) M N"
-
-declare hdvd_def [transfer_unfold]
+ [transfer_unfold]: "(M::hypnat) hdvd N = ( *p2* (op dvd)) M N"
-constdefs
starprime :: "hypnat set"
- "starprime == ( *s* {p. prime p})"
+ [transfer_unfold]: "starprime = ( *s* {p. prime p})"
-declare starprime_def [transfer_unfold]
-
-constdefs
choicefun :: "'a set => 'a"
- "choicefun E == (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
+ "choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
consts injf_max :: "nat => ('a::{order} set) => 'a"
primrec
--- a/src/HOL/Complex/ex/Sqrt_Script.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Complex/ex/Sqrt_Script.thy Sat May 27 17:42:02 2006 +0200
@@ -52,9 +52,9 @@
subsection {* The set of rational numbers *}
-constdefs
+definition
rationals :: "real set" ("\<rat>")
- "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
+ "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
subsection {* Main theorem *}
--- a/src/HOL/Induct/Com.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Com.thy Sat May 27 17:42:02 2006 +0200
@@ -34,17 +34,14 @@
text{* Execution of commands *}
consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
-syntax "@exec" :: "((exp*state) * (nat*state)) set =>
- [com*state,state] => bool" ("_/ -[_]-> _" [50,0,50] 50)
-
-translations "csig -[eval]-> s" == "(csig,s) \<in> exec eval"
-syntax eval' :: "[exp*state,nat*state] =>
- ((exp*state) * (nat*state)) set => bool"
- ("_/ -|[_]-> _" [50,0,50] 50)
+abbreviation
+ exec_rel ("_/ -[_]-> _" [50,0,50] 50)
+ "csig -[eval]-> s == (csig,s) \<in> exec eval"
-translations
- "esig -|[eval]-> ns" => "(esig,ns) \<in> eval"
+abbreviation (input)
+ generic_rel ("_/ -|[_]-> _" [50,0,50] 50)
+ "esig -|[eval]-> ns == (esig,ns) \<in> eval"
text{*Command execution. Natural numbers represent Booleans: 0=True, 1=False*}
inductive "exec eval"
@@ -105,12 +102,12 @@
subsection {* Expressions *}
text{* Evaluation of arithmetic expressions *}
-consts eval :: "((exp*state) * (nat*state)) set"
- "-|->" :: "[exp*state,nat*state] => bool" (infixl 50)
+consts
+ eval :: "((exp*state) * (nat*state)) set"
-translations
- "esig -|-> (n,s)" <= "(esig,n,s) \<in> eval"
- "esig -|-> ns" == "(esig,ns ) \<in> eval"
+abbreviation
+ eval_rel :: "[exp*state,nat*state] => bool" (infixl "-|->" 50)
+ "esig -|-> ns == (esig, ns) \<in> eval"
inductive eval
intros
--- a/src/HOL/Induct/Comb.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Comb.thy Sat May 27 17:42:02 2006 +0200
@@ -23,7 +23,11 @@
datatype comb = K
| S
- | "##" comb comb (infixl 90)
+ | Ap comb comb (infixl "##" 90)
+
+const_syntax (xsymbols)
+ Ap (infixl "\<bullet>" 90)
+
text {*
Inductive definition of contractions, @{text "-1->"} and
@@ -32,15 +36,12 @@
consts
contract :: "(comb*comb) set"
- "-1->" :: "[comb,comb] => bool" (infixl 50)
- "--->" :: "[comb,comb] => bool" (infixl 50)
-translations
- "x -1-> y" == "(x,y) \<in> contract"
- "x ---> y" == "(x,y) \<in> contract^*"
-
-syntax (xsymbols)
- "op ##" :: "[comb,comb] => comb" (infixl "\<bullet>" 90)
+abbreviation
+ contract_rel1 :: "[comb,comb] => bool" (infixl "-1->" 50)
+ "x -1-> y == (x,y) \<in> contract"
+ contract_rel :: "[comb,comb] => bool" (infixl "--->" 50)
+ "x ---> y == (x,y) \<in> contract^*"
inductive contract
intros
@@ -56,12 +57,12 @@
consts
parcontract :: "(comb*comb) set"
- "=1=>" :: "[comb,comb] => bool" (infixl 50)
- "===>" :: "[comb,comb] => bool" (infixl 50)
-translations
- "x =1=> y" == "(x,y) \<in> parcontract"
- "x ===> y" == "(x,y) \<in> parcontract^*"
+abbreviation
+ parcontract_rel1 :: "[comb,comb] => bool" (infixl "=1=>" 50)
+ "x =1=> y == (x,y) \<in> parcontract"
+ parcontract_rel :: "[comb,comb] => bool" (infixl "===>" 50)
+ "x ===> y == (x,y) \<in> parcontract^*"
inductive parcontract
intros
@@ -74,15 +75,15 @@
Misc definitions.
*}
-constdefs
+definition
I :: comb
- "I == S##K##K"
+ "I = S##K##K"
diamond :: "('a * 'a)set => bool"
--{*confluence; Lambda/Commutation treats this more abstractly*}
- "diamond(r) == \<forall>x y. (x,y) \<in> r -->
+ "diamond(r) = (\<forall>x y. (x,y) \<in> r -->
(\<forall>y'. (x,y') \<in> r -->
- (\<exists>z. (y,z) \<in> r & (y',z) \<in> r))"
+ (\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))"
subsection {*Reflexive/Transitive closure preserves Church-Rosser property*}
--- a/src/HOL/Induct/LFilter.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/LFilter.thy Sat May 27 17:42:02 2006 +0200
@@ -19,12 +19,12 @@
declare findRel.intros [intro]
-constdefs
+definition
find :: "['a => bool, 'a llist] => 'a llist"
- "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))"
+ "find p l = (SOME l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p)))"
lfilter :: "['a => bool, 'a llist] => 'a llist"
- "lfilter p l == llist_corec l (%l. case find p l of
+ "lfilter p l = llist_corec l (%l. case find p l of
LNil => None
| LCons y z => Some(y,z))"
--- a/src/HOL/Induct/LList.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/LList.thy Sat May 27 17:42:02 2006 +0200
@@ -46,48 +46,48 @@
'a llist = "llist(range Leaf) :: 'a item set"
by (blast intro: llist.NIL_I)
-constdefs
+definition
list_Fun :: "['a item set, 'a item set] => 'a item set"
--{*Now used exclusively for abbreviating the coinduction rule*}
- "list_Fun A X == {z. z = NIL | (\<exists>M a. z = CONS a M & a \<in> A & M \<in> X)}"
+ "list_Fun A X = {z. z = NIL | (\<exists>M a. z = CONS a M & a \<in> A & M \<in> X)}"
LListD_Fun ::
"[('a item * 'a item)set, ('a item * 'a item)set] =>
('a item * 'a item)set"
- "LListD_Fun r X ==
+ "LListD_Fun r X =
{z. z = (NIL, NIL) |
(\<exists>M N a b. z = (CONS a M, CONS b N) & (a, b) \<in> r & (M, N) \<in> X)}"
LNil :: "'a llist"
--{*abstract constructor*}
- "LNil == Abs_LList NIL"
+ "LNil = Abs_LList NIL"
LCons :: "['a, 'a llist] => 'a llist"
--{*abstract constructor*}
- "LCons x xs == Abs_LList(CONS (Leaf x) (Rep_LList xs))"
+ "LCons x xs = Abs_LList(CONS (Leaf x) (Rep_LList xs))"
llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
- "llist_case c d l ==
+ "llist_case c d l =
List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)"
LList_corec_fun :: "[nat, 'a=> ('b item * 'a) option, 'a] => 'b item"
- "LList_corec_fun k f ==
+ "LList_corec_fun k f ==
nat_rec (%x. {})
(%j r x. case f x of None => NIL
| Some(z,w) => CONS z (r w))
k"
LList_corec :: "['a, 'a => ('b item * 'a) option] => 'b item"
- "LList_corec a f == \<Union>k. LList_corec_fun k f a"
+ "LList_corec a f = (\<Union>k. LList_corec_fun k f a)"
llist_corec :: "['a, 'a => ('b * 'a) option] => 'b llist"
- "llist_corec a f ==
+ "llist_corec a f =
Abs_LList(LList_corec a
(%z. case f z of None => None
| Some(v,w) => Some(Leaf(v), w)))"
llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
- "llistD_Fun(r) ==
+ "llistD_Fun(r) =
prod_fun Abs_LList Abs_LList `
LListD_Fun (diag(range Leaf))
(prod_fun Rep_LList Rep_LList ` r)"
@@ -101,27 +101,27 @@
subsubsection{* Sample function definitions. Item-based ones start with @{text L} *}
-constdefs
+definition
Lmap :: "('a item => 'b item) => ('a item => 'b item)"
- "Lmap f M == LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
+ "Lmap f M = LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
lmap :: "('a=>'b) => ('a llist => 'b llist)"
- "lmap f l == llist_corec l (%z. case z of LNil => None
+ "lmap f l = llist_corec l (%z. case z of LNil => None
| LCons y z => Some(f(y), z))"
iterates :: "['a => 'a, 'a] => 'a llist"
- "iterates f a == llist_corec a (%x. Some((x, f(x))))"
+ "iterates f a = llist_corec a (%x. Some((x, f(x))))"
Lconst :: "'a item => 'a item"
"Lconst(M) == lfp(%N. CONS M N)"
Lappend :: "['a item, 'a item] => 'a item"
- "Lappend M N == LList_corec (M,N)
+ "Lappend M N = LList_corec (M,N)
(split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2)))))
(%M1 M2 N. Some((M1, (M2,N))))))"
lappend :: "['a llist, 'a llist] => 'a llist"
- "lappend l n == llist_corec (l,n)
+ "lappend l n = llist_corec (l,n)
(split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2)))))
(%l1 l2 n. Some((l1, (l2,n))))))"
@@ -198,6 +198,7 @@
declare LList_corec_fun_def [THEN def_nat_rec_0, simp]
LList_corec_fun_def [THEN def_nat_rec_Suc, simp]
+
subsubsection{* The directions of the equality are proved separately *}
lemma LList_corec_subset1:
@@ -226,7 +227,7 @@
text{*definitional version of same*}
lemma def_LList_corec:
- "[| !!x. h(x) == LList_corec x f |]
+ "[| !!x. h(x) = LList_corec x f |]
==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))"
by (simp add: LList_corec)
@@ -652,7 +653,7 @@
text{*definitional version of same*}
lemma def_llist_corec:
- "[| !!x. h(x) == llist_corec x f |] ==>
+ "[| !!x. h(x) = llist_corec x f |] ==>
h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))"
by (simp add: llist_corec)
--- a/src/HOL/Induct/Mutil.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Mutil.thy Sat May 27 17:42:02 2006 +0200
@@ -30,16 +30,15 @@
text {* \medskip Sets of squares of the given colour*}
-constdefs
+definition
coloured :: "nat => (nat \<times> nat) set"
- "coloured b == {(i, j). (i + j) mod 2 = b}"
+ "coloured b = {(i, j). (i + j) mod 2 = b}"
-syntax whites :: "(nat \<times> nat) set"
- blacks :: "(nat \<times> nat) set"
-
-translations
- "whites" == "coloured 0"
- "blacks" == "coloured (Suc 0)"
+abbreviation
+ whites :: "(nat \<times> nat) set"
+ "whites == coloured 0"
+ blacks :: "(nat \<times> nat) set"
+ "blacks == coloured (Suc 0)"
text {* \medskip The union of two disjoint tilings is a tiling *}
--- a/src/HOL/Induct/Ordinals.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Ordinals.thy Sat May 27 17:42:02 2006 +0200
@@ -31,11 +31,11 @@
"iter f 0 = id"
"iter f (Suc n) = f \<circ> (iter f n)"
-constdefs
+definition
OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)"
- "OpLim F a == Limit (\<lambda>n. F n a)"
+ "OpLim F a = Limit (\<lambda>n. F n a)"
OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<Squnion>")
- "\<Squnion>f == OpLim (iter f)"
+ "\<Squnion>f = OpLim (iter f)"
consts
cantor :: "ordinal => ordinal => ordinal"
@@ -51,9 +51,9 @@
"\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
"\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
-constdefs
+definition
deriv :: "(ordinal => ordinal) => (ordinal => ordinal)"
- "deriv f == \<nabla>(\<Squnion>f)"
+ "deriv f = \<nabla>(\<Squnion>f)"
consts
veblen :: "ordinal => ordinal => ordinal"
@@ -62,9 +62,9 @@
"veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
"veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
-constdefs
- "veb a == veblen a Zero"
- "\<epsilon>\<^isub>0 == veb Zero"
- "\<Gamma>\<^isub>0 == Limit (\<lambda>n. iter veb n Zero)"
+definition
+ "veb a = veblen a Zero"
+ "\<epsilon>\<^isub>0 = veb Zero"
+ "\<Gamma>\<^isub>0 = Limit (\<lambda>n. iter veb n Zero)"
end
--- a/src/HOL/Induct/PropLog.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/PropLog.thy Sat May 27 17:42:02 2006 +0200
@@ -28,10 +28,10 @@
consts
thms :: "'a pl set => 'a pl set"
- "|-" :: "['a pl set, 'a pl] => bool" (infixl 50)
-translations
- "H |- p" == "p \<in> thms(H)"
+abbreviation
+ thm_rel :: "['a pl set, 'a pl] => bool" (infixl "|-" 50)
+ "H |- p == p \<in> thms H"
inductive "thms(H)"
intros
@@ -72,9 +72,9 @@
is @{text p}.
*}
-constdefs
+definition
sat :: "['a pl set, 'a pl] => bool" (infixl "|=" 50)
- "H |= p == (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
+ "H |= p = (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
subsection {* Proof theory of propositional logic *}
--- a/src/HOL/Induct/QuoDataType.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Sat May 27 17:42:02 2006 +0200
@@ -22,14 +22,14 @@
provided the keys are the same.*}
consts msgrel :: "(freemsg * freemsg) set"
-syntax
- "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "~~" 50)
-syntax (xsymbols)
- "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50)
-syntax (HTML output)
- "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50)
-translations
- "X \<sim> Y" == "(X,Y) \<in> msgrel"
+abbreviation
+ msg_rel :: "[freemsg, freemsg] => bool" (infixl "~~" 50)
+ "X ~~ Y == (X,Y) \<in> msgrel"
+
+const_syntax (xsymbols)
+ msg_rel (infixl "\<sim>" 50)
+const_syntax (HTML output)
+ msg_rel (infixl "\<sim>" 50)
text{*The first two rules are the desired equations. The next four rules
make the equations applicable to subterms. The last two rules are symmetry
@@ -142,20 +142,20 @@
text{*The abstract message constructors*}
-constdefs
+definition
Nonce :: "nat \<Rightarrow> msg"
- "Nonce N == Abs_Msg(msgrel``{NONCE N})"
+ "Nonce N = Abs_Msg(msgrel``{NONCE N})"
MPair :: "[msg,msg] \<Rightarrow> msg"
- "MPair X Y ==
+ "MPair X Y =
Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"
Crypt :: "[nat,msg] \<Rightarrow> msg"
- "Crypt K X ==
+ "Crypt K X =
Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"
Decrypt :: "[nat,msg] \<Rightarrow> msg"
- "Decrypt K X ==
+ "Decrypt K X =
Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
@@ -227,9 +227,9 @@
subsection{*The Abstract Function to Return the Set of Nonces*}
-constdefs
+definition
nonces :: "msg \<Rightarrow> nat set"
- "nonces X == \<Union>U \<in> Rep_Msg X. freenonces U"
+ "nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"
lemma nonces_congruent: "freenonces respects msgrel"
by (simp add: congruent_def msgrel_imp_eq_freenonces)
@@ -262,9 +262,9 @@
subsection{*The Abstract Function to Return the Left Part*}
-constdefs
+definition
left :: "msg \<Rightarrow> msg"
- "left X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
+ "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
by (simp add: congruent_def msgrel_imp_eqv_freeleft)
@@ -296,9 +296,9 @@
subsection{*The Abstract Function to Return the Right Part*}
-constdefs
+definition
right :: "msg \<Rightarrow> msg"
- "right X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
+ "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
by (simp add: congruent_def msgrel_imp_eqv_freeright)
@@ -431,9 +431,9 @@
text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
need this function in order to prove discrimination theorems.*}
-constdefs
+definition
discrim :: "msg \<Rightarrow> int"
- "discrim X == contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
+ "discrim X = contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
by (simp add: congruent_def msgrel_imp_eq_freediscrim)
--- a/src/HOL/Induct/QuoNestedDataType.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy Sat May 27 17:42:02 2006 +0200
@@ -20,14 +20,14 @@
text{*The equivalence relation, which makes PLUS associative.*}
consts exprel :: "(freeExp * freeExp) set"
-syntax
- "_exprel" :: "[freeExp, freeExp] => bool" (infixl "~~" 50)
-syntax (xsymbols)
- "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50)
-syntax (HTML output)
- "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50)
-translations
- "X \<sim> Y" == "(X,Y) \<in> exprel"
+abbreviation
+ exp_rel :: "[freeExp, freeExp] => bool" (infixl "~~" 50)
+ "X ~~ Y == (X,Y) \<in> exprel"
+
+const_syntax (xsymbols)
+ exp_rel (infixl "\<sim>" 50)
+const_syntax (HTML output)
+ exp_rel (infixl "\<sim>" 50)
text{*The first rule is the desired equation. The next three rules
make the equations applicable to subterms. The last two rules are symmetry
@@ -159,16 +159,16 @@
text{*The abstract message constructors*}
-constdefs
+definition
Var :: "nat \<Rightarrow> exp"
- "Var N == Abs_Exp(exprel``{VAR N})"
+ "Var N = Abs_Exp(exprel``{VAR N})"
Plus :: "[exp,exp] \<Rightarrow> exp"
- "Plus X Y ==
+ "Plus X Y =
Abs_Exp (\<Union>U \<in> Rep_Exp X. \<Union>V \<in> Rep_Exp Y. exprel``{PLUS U V})"
FnCall :: "[nat, exp list] \<Rightarrow> exp"
- "FnCall F Xs ==
+ "FnCall F Xs =
Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})"
@@ -206,8 +206,9 @@
subsection{*Every list of abstract expressions can be expressed in terms of a
list of concrete expressions*}
-constdefs Abs_ExpList :: "freeExp list => exp list"
- "Abs_ExpList Xs == map (%U. Abs_Exp(exprel``{U})) Xs"
+definition
+ Abs_ExpList :: "freeExp list => exp list"
+ "Abs_ExpList Xs = map (%U. Abs_Exp(exprel``{U})) Xs"
lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] == []"
by (simp add: Abs_ExpList_def)
@@ -283,9 +284,9 @@
subsection{*The Abstract Function to Return the Set of Variables*}
-constdefs
+definition
vars :: "exp \<Rightarrow> nat set"
- "vars X == \<Union>U \<in> Rep_Exp X. freevars U"
+ "vars X = (\<Union>U \<in> Rep_Exp X. freevars U)"
lemma vars_respects: "freevars respects exprel"
by (simp add: congruent_def exprel_imp_eq_freevars)
@@ -349,9 +350,9 @@
subsection{*Injectivity of @{term FnCall}*}
-constdefs
+definition
fun :: "exp \<Rightarrow> nat"
- "fun X == contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
+ "fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
lemma fun_respects: "(%U. {freefun U}) respects exprel"
by (simp add: congruent_def exprel_imp_eq_freefun)
@@ -361,9 +362,9 @@
apply (simp add: FnCall fun_def UN_equiv_class [OF equiv_exprel fun_respects])
done
-constdefs
+definition
args :: "exp \<Rightarrow> exp list"
- "args X == contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
+ "args X = contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
text{*This result can probably be generalized to arbitrary equivalence
relations, but with little benefit here.*}
@@ -396,9 +397,9 @@
text{*However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this
function in order to prove discrimination theorems.*}
-constdefs
+definition
discrim :: "exp \<Rightarrow> int"
- "discrim X == contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
+ "discrim X = contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
by (simp add: congruent_def exprel_imp_eq_freediscrim)
--- a/src/HOL/Induct/SList.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/SList.thy Sat May 27 17:42:02 2006 +0200
@@ -36,12 +36,12 @@
(* Defining the Concrete Constructors *)
-constdefs
+definition
NIL :: "'a item"
- "NIL == In0(Numb(0))"
+ "NIL = In0(Numb(0))"
CONS :: "['a item, 'a item] => 'a item"
- "CONS M N == In1(Scons M N)"
+ "CONS M N = In1(Scons M N)"
consts
list :: "'a item set => 'a item set"
@@ -55,12 +55,12 @@
'a list = "list(range Leaf) :: 'a item set"
by (blast intro: list.NIL_I)
-constdefs
+definition
List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
- "List_case c d == Case(%x. c)(Split(d))"
+ "List_case c d = Case(%x. c)(Split(d))"
List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
- "List_rec M c d == wfrec (trancl pred_sexp)
+ "List_rec M c d = wfrec (trancl pred_sexp)
(%g. List_case c (%x y. d x y (g y))) M"
@@ -72,20 +72,20 @@
(*Declaring the abstract list constructors*)
-constdefs
+definition
Nil :: "'a list"
- "Nil == Abs_List(NIL)"
+ "Nil = Abs_List(NIL)"
"Cons" :: "['a, 'a list] => 'a list" (infixr "#" 65)
- "x#xs == Abs_List(CONS (Leaf x)(Rep_List xs))"
+ "x#xs = Abs_List(CONS (Leaf x)(Rep_List xs))"
(* list Recursion -- the trancl is Essential; see list.ML *)
list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
- "list_rec l c d ==
+ "list_rec l c d =
List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
- "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
+ "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
(* list Enumeration *)
consts
@@ -110,83 +110,82 @@
(* Generalized Map Functionals *)
-constdefs
+definition
Rep_map :: "('b => 'a item) => ('b list => 'a item)"
- "Rep_map f xs == list_rec xs NIL(%x l r. CONS(f x) r)"
+ "Rep_map f xs = list_rec xs NIL(%x l r. CONS(f x) r)"
Abs_map :: "('a item => 'b) => 'a item => 'b list"
- "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
+ "Abs_map g M = List_rec M Nil (%N L r. g(N)#r)"
(**** Function definitions ****)
-constdefs
+definition
null :: "'a list => bool"
- "null xs == list_rec xs True (%x xs r. False)"
+ "null xs = list_rec xs True (%x xs r. False)"
hd :: "'a list => 'a"
- "hd xs == list_rec xs (@x. True) (%x xs r. x)"
+ "hd xs = list_rec xs (@x. True) (%x xs r. x)"
tl :: "'a list => 'a list"
- "tl xs == list_rec xs (@xs. True) (%x xs r. xs)"
+ "tl xs = list_rec xs (@xs. True) (%x xs r. xs)"
(* a total version of tl: *)
ttl :: "'a list => 'a list"
- "ttl xs == list_rec xs [] (%x xs r. xs)"
+ "ttl xs = list_rec xs [] (%x xs r. xs)"
member :: "['a, 'a list] => bool" (infixl "mem" 55)
- "x mem xs == list_rec xs False (%y ys r. if y=x then True else r)"
+ "x mem xs = list_rec xs False (%y ys r. if y=x then True else r)"
list_all :: "('a => bool) => ('a list => bool)"
- "list_all P xs == list_rec xs True(%x l r. P(x) & r)"
+ "list_all P xs = list_rec xs True(%x l r. P(x) & r)"
map :: "('a=>'b) => ('a list => 'b list)"
- "map f xs == list_rec xs [] (%x l r. f(x)#r)"
+ "map f xs = list_rec xs [] (%x l r. f(x)#r)"
-constdefs
append :: "['a list, 'a list] => 'a list" (infixr "@" 65)
- "xs@ys == list_rec xs ys (%x l r. x#r)"
+ "xs@ys = list_rec xs ys (%x l r. x#r)"
filter :: "['a => bool, 'a list] => 'a list"
- "filter P xs == list_rec xs [] (%x xs r. if P(x)then x#r else r)"
+ "filter P xs = list_rec xs [] (%x xs r. if P(x)then x#r else r)"
foldl :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
- "foldl f a xs == list_rec xs (%a. a)(%x xs r.%a. r(f a x))(a)"
+ "foldl f a xs = list_rec xs (%a. a)(%x xs r.%a. r(f a x))(a)"
foldr :: "[['a,'b] => 'b, 'b, 'a list] => 'b"
- "foldr f a xs == list_rec xs a (%x xs r. (f x r))"
+ "foldr f a xs = list_rec xs a (%x xs r. (f x r))"
length :: "'a list => nat"
- "length xs== list_rec xs 0 (%x xs r. Suc r)"
+ "length xs = list_rec xs 0 (%x xs r. Suc r)"
drop :: "['a list,nat] => 'a list"
- "drop t n == (nat_rec(%x. x)(%m r xs. r(ttl xs)))(n)(t)"
+ "drop t n = (nat_rec(%x. x)(%m r xs. r(ttl xs)))(n)(t)"
copy :: "['a, nat] => 'a list" (* make list of n copies of x *)
- "copy t == nat_rec [] (%m xs. t # xs)"
+ "copy t = nat_rec [] (%m xs. t # xs)"
flat :: "'a list list => 'a list"
- "flat == foldr (op @) []"
+ "flat = foldr (op @) []"
nth :: "[nat, 'a list] => 'a"
- "nth == nat_rec hd (%m r xs. r(tl xs))"
+ "nth = nat_rec hd (%m r xs. r(tl xs))"
rev :: "'a list => 'a list"
- "rev xs == list_rec xs [] (%x xs xsa. xsa @ [x])"
+ "rev xs = list_rec xs [] (%x xs xsa. xsa @ [x])"
(* miscellaneous definitions *)
zipWith :: "['a * 'b => 'c, 'a list * 'b list] => 'c list"
- "zipWith f S == (list_rec (fst S) (%T.[])
+ "zipWith f S = (list_rec (fst S) (%T.[])
(%x xs r. %T. if null T then []
else f(x,hd T) # r(tl T)))(snd(S))"
zip :: "'a list * 'b list => ('a*'b) list"
- "zip == zipWith (%s. s)"
+ "zip = zipWith (%s. s)"
unzip :: "('a*'b) list => ('a list * 'b list)"
- "unzip == foldr(% (a,b)(c,d).(a#c,b#d))([],[])"
+ "unzip = foldr(% (a,b)(c,d).(a#c,b#d))([],[])"
consts take :: "['a list,nat] => 'a list"
@@ -425,9 +424,9 @@
"[| M: sexp; N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N"
by (simp add: Abs_map_def)
-(*Eases the use of primitive recursion. NOTE USE OF == *)
+(*Eases the use of primitive recursion.*)
lemma def_list_rec_NilCons:
- "[| !!xs. f(xs) == list_rec xs c h |]
+ "[| !!xs. f(xs) = list_rec xs c h |]
==> f [] = c & f(x#xs) = h x xs (f xs)"
by simp
@@ -475,11 +474,11 @@
(** nth **)
lemma def_nat_rec_0_eta:
- "[| !!n. f == nat_rec c h |] ==> f(0) = c"
+ "[| !!n. f = nat_rec c h |] ==> f(0) = c"
by simp
lemma def_nat_rec_Suc_eta:
- "[| !!n. f == nat_rec c h |] ==> f(Suc(n)) = h n (f n)"
+ "[| !!n. f = nat_rec c h |] ==> f(Suc(n)) = h n (f n)"
by simp
declare def_nat_rec_0_eta [OF nth_def, simp]
--- a/src/HOL/Induct/Sexp.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Sexp.thy Sat May 27 17:42:02 2006 +0200
@@ -17,20 +17,20 @@
NumbI: "Numb(i) \<in> sexp"
SconsI: "[| M \<in> sexp; N \<in> sexp |] ==> Scons M N \<in> sexp"
-constdefs
+definition
sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b,
'a item] => 'b"
- "sexp_case c d e M == THE z. (EX x. M=Leaf(x) & z=c(x))
+ "sexp_case c d e M = (THE z. (EX x. M=Leaf(x) & z=c(x))
| (EX k. M=Numb(k) & z=d(k))
- | (EX N1 N2. M = Scons N1 N2 & z=e N1 N2)"
+ | (EX N1 N2. M = Scons N1 N2 & z=e N1 N2))"
pred_sexp :: "('a item * 'a item)set"
- "pred_sexp == \<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)}"
+ "pred_sexp = (\<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)})"
sexp_rec :: "['a item, 'a=>'b, nat=>'b,
['a item, 'a item, 'b, 'b]=>'b] => 'b"
- "sexp_rec M c d e == wfrec pred_sexp
+ "sexp_rec M c d e = wfrec pred_sexp
(%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
--- a/src/HOL/Induct/Tree.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Tree.thy Sat May 27 17:42:02 2006 +0200
@@ -71,12 +71,12 @@
ordinals. Start with a predecessor relation and form its transitive
closure. *}
-constdefs
+definition
brouwer_pred :: "(brouwer * brouwer) set"
- "brouwer_pred == \<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)}"
+ "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
brouwer_order :: "(brouwer * brouwer) set"
- "brouwer_order == brouwer_pred^+"
+ "brouwer_order = brouwer_pred^+"
lemma wf_brouwer_pred: "wf brouwer_pred"
by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
--- a/src/HOL/Lattice/Bounds.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Lattice/Bounds.thy Sat May 27 17:42:02 2006 +0200
@@ -15,18 +15,18 @@
number of elements.
*}
-constdefs
+definition
is_inf :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
- "is_inf x y inf \<equiv> inf \<sqsubseteq> x \<and> inf \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> inf)"
+ "is_inf x y inf = (inf \<sqsubseteq> x \<and> inf \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> inf))"
is_sup :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
- "is_sup x y sup \<equiv> x \<sqsubseteq> sup \<and> y \<sqsubseteq> sup \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> sup \<sqsubseteq> z)"
+ "is_sup x y sup = (x \<sqsubseteq> sup \<and> y \<sqsubseteq> sup \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> sup \<sqsubseteq> z))"
is_Inf :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
- "is_Inf A inf \<equiv> (\<forall>x \<in> A. inf \<sqsubseteq> x) \<and> (\<forall>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<longrightarrow> z \<sqsubseteq> inf)"
+ "is_Inf A inf = ((\<forall>x \<in> A. inf \<sqsubseteq> x) \<and> (\<forall>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<longrightarrow> z \<sqsubseteq> inf))"
is_Sup :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
- "is_Sup A sup \<equiv> (\<forall>x \<in> A. x \<sqsubseteq> sup) \<and> (\<forall>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<longrightarrow> sup \<sqsubseteq> z)"
+ "is_Sup A sup = ((\<forall>x \<in> A. x \<sqsubseteq> sup) \<and> (\<forall>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<longrightarrow> sup \<sqsubseteq> z))"
text {*
These definitions entail the following basic properties of boundary
--- a/src/HOL/Lattice/CompleteLattice.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy Sat May 27 17:42:02 2006 +0200
@@ -31,15 +31,15 @@
such infimum and supremum elements.
*}
-consts
+definition
Meet :: "'a::complete_lattice set \<Rightarrow> 'a"
+ "Meet A = (THE inf. is_Inf A inf)"
Join :: "'a::complete_lattice set \<Rightarrow> 'a"
-syntax (xsymbols)
- Meet :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90)
- Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90)
-defs
- Meet_def: "\<Sqinter>A \<equiv> THE inf. is_Inf A inf"
- Join_def: "\<Squnion>A \<equiv> THE sup. is_Sup A sup"
+ "Join A = (THE sup. is_Sup A sup)"
+
+const_syntax (xsymbols)
+ Meet ("\<Sqinter>_" [90] 90)
+ Join ("\<Squnion>_" [90] 90)
text {*
Due to unique existence of bounds, the complete lattice operations
@@ -142,11 +142,11 @@
greatest elements.
*}
-constdefs
+definition
bottom :: "'a::complete_lattice" ("\<bottom>")
- "\<bottom> \<equiv> \<Sqinter>UNIV"
+ "\<bottom> = \<Sqinter>UNIV"
top :: "'a::complete_lattice" ("\<top>")
- "\<top> \<equiv> \<Squnion>UNIV"
+ "\<top> = \<Squnion>UNIV"
lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
proof (unfold bottom_def)
--- a/src/HOL/Lattice/Lattice.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Lattice/Lattice.thy Sat May 27 17:42:02 2006 +0200
@@ -24,15 +24,15 @@
infimum and supremum elements.
*}
-consts
+definition
meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "&&" 70)
+ "x && y = (THE inf. is_inf x y inf)"
join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "||" 65)
-syntax (xsymbols)
- meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
- join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
-defs
- meet_def: "x && y \<equiv> THE inf. is_inf x y inf"
- join_def: "x || y \<equiv> THE sup. is_sup x y sup"
+ "x || y = (THE sup. is_sup x y sup)"
+
+const_syntax (xsymbols)
+ meet (infixl "\<sqinter>" 70)
+ join (infixl "\<squnion>" 65)
text {*
Due to unique existence of bounds, the lattice operations may be
@@ -336,11 +336,11 @@
are a (degenerate) example of lattice structures.
*}
-constdefs
+definition
minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
- "minimum x y \<equiv> (if x \<sqsubseteq> y then x else y)"
+ "minimum x y = (if x \<sqsubseteq> y then x else y)"
maximum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
- "maximum x y \<equiv> (if x \<sqsubseteq> y then y else x)"
+ "maximum x y = (if x \<sqsubseteq> y then y else x)"
lemma is_inf_minimum: "is_inf x y (minimum x y)"
proof
--- a/src/HOL/Lattice/Orders.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Lattice/Orders.thy Sat May 27 17:42:02 2006 +0200
@@ -21,8 +21,8 @@
axclass leq < type
consts
leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool" (infixl "[=" 50)
-syntax (xsymbols)
- leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
+const_syntax (xsymbols)
+ leq (infixl "\<sqsubseteq>" 50)
axclass quasi_order < leq
leq_refl [intro?]: "x \<sqsubseteq> x"
--- a/src/HOL/Library/BigO.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/BigO.thy Sat May 27 17:42:02 2006 +0200
@@ -38,10 +38,9 @@
subsection {* Definitions *}
-constdefs
-
+definition
bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set" ("(1O'(_'))")
- "O(f::('a => 'b)) ==
+ "O(f::('a => 'b)) =
{h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
lemma bigo_pos_const: "(EX (c::'a::ordered_idom).
@@ -735,10 +734,10 @@
subsection {* Less than or equal to *}
-constdefs
+definition
lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
(infixl "<o" 70)
- "f <o g == (%x. max (f x - g x) 0)"
+ "f <o g = (%x. max (f x - g x) 0)"
lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
g =o O(h)"
--- a/src/HOL/Library/Char_ord.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Char_ord.thy Sat May 27 17:42:02 2006 +0200
@@ -13,8 +13,6 @@
consts
nibble_to_int:: "nibble \<Rightarrow> int"
- int_to_nibble:: "int \<Rightarrow> nibble"
-
primrec
"nibble_to_int Nibble0 = 0"
"nibble_to_int Nibble1 = 1"
@@ -33,25 +31,25 @@
"nibble_to_int NibbleE = 14"
"nibble_to_int NibbleF = 15"
-defs
- int_to_nibble_def:
- "int_to_nibble x \<equiv> (let y = x mod 16 in
- if y = 0 then Nibble0 else
- if y = 1 then Nibble1 else
- if y = 2 then Nibble2 else
- if y = 3 then Nibble3 else
- if y = 4 then Nibble4 else
- if y = 5 then Nibble5 else
- if y = 6 then Nibble6 else
- if y = 7 then Nibble7 else
- if y = 8 then Nibble8 else
- if y = 9 then Nibble9 else
- if y = 10 then NibbleA else
- if y = 11 then NibbleB else
- if y = 12 then NibbleC else
- if y = 13 then NibbleD else
- if y = 14 then NibbleE else
- NibbleF)"
+definition
+ int_to_nibble :: "int \<Rightarrow> nibble"
+ "int_to_nibble x \<equiv> (let y = x mod 16 in
+ if y = 0 then Nibble0 else
+ if y = 1 then Nibble1 else
+ if y = 2 then Nibble2 else
+ if y = 3 then Nibble3 else
+ if y = 4 then Nibble4 else
+ if y = 5 then Nibble5 else
+ if y = 6 then Nibble6 else
+ if y = 7 then Nibble7 else
+ if y = 8 then Nibble8 else
+ if y = 9 then Nibble9 else
+ if y = 10 then NibbleA else
+ if y = 11 then NibbleB else
+ if y = 12 then NibbleC else
+ if y = 13 then NibbleD else
+ if y = 14 then NibbleE else
+ NibbleF)"
lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x"
by (cases x) (auto simp: int_to_nibble_def Let_def)
@@ -93,15 +91,9 @@
lemmas char_ord_defs = char_less_def char_le_def
instance char :: order
- apply intro_classes
- apply (unfold char_ord_defs)
- apply (auto simp: char_to_int_pair_eq order_less_le)
- done
+ by default (auto simp: char_ord_defs char_to_int_pair_eq order_less_le)
-instance char::linorder
- apply intro_classes
- apply (unfold char_le_def)
- apply auto
- done
+instance char :: linorder
+ by default (auto simp: char_le_def)
end
--- a/src/HOL/Library/Commutative_Ring.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Commutative_Ring.thy Sat May 27 17:42:02 2006 +0200
@@ -47,16 +47,16 @@
text {* Create polynomial normalized polynomials given normalized inputs. *}
-constdefs
+definition
mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
- "mkPinj x P \<equiv> (case P of
+ "mkPinj x P = (case P of
Pc c \<Rightarrow> Pc c |
Pinj y P \<Rightarrow> Pinj (x + y) P |
PX p1 y p2 \<Rightarrow> Pinj x P)"
-constdefs
+definition
mkPX :: "'a::{comm_ring,recpower} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
- "mkPX P i Q == (case P of
+ "mkPX P i Q = (case P of
Pc c \<Rightarrow> (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) |
Pinj j R \<Rightarrow> PX P i Q |
PX P2 i2 Q2 \<Rightarrow> (if (Q2 = (Pc 0)) then (PX P2 (i+i2) Q) else (PX P i Q)) )"
@@ -127,9 +127,9 @@
"neg (PX P x Q) = PX (neg P) x (neg Q)"
text {* Substraction *}
-constdefs
+definition
sub :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
- "sub p q \<equiv> add (p, neg q)"
+ "sub p q = add (p, neg q)"
text {* Square for Fast Exponentation *}
primrec
@@ -316,11 +316,6 @@
qed
-text {* Code generation *}
-(*
-Does not work, since no generic ring operations implementation is there
-generate_code ("ring.ML") test = "norm"*)
-
use "comm_ring.ML"
setup CommRing.setup
--- a/src/HOL/Library/Continuity.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Continuity.thy Sat May 27 17:42:02 2006 +0200
@@ -11,9 +11,9 @@
subsection "Chains"
-constdefs
+definition
up_chain :: "(nat => 'a set) => bool"
- "up_chain F == \<forall>i. F i \<subseteq> F (Suc i)"
+ "up_chain F = (\<forall>i. F i \<subseteq> F (Suc i))"
lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
by (simp add: up_chain_def)
@@ -21,10 +21,10 @@
lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)"
by (simp add: up_chain_def)
-lemma up_chain_less_mono [rule_format]:
- "up_chain F ==> x < y --> F x \<subseteq> F y"
- apply (induct_tac y)
- apply (blast dest: up_chainD elim: less_SucE)+
+lemma up_chain_less_mono:
+ "up_chain F ==> x < y ==> F x \<subseteq> F y"
+ apply (induct y)
+ apply (blast dest: up_chainD elim: less_SucE)+
done
lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y"
@@ -33,9 +33,9 @@
done
-constdefs
+definition
down_chain :: "(nat => 'a set) => bool"
- "down_chain F == \<forall>i. F (Suc i) \<subseteq> F i"
+ "down_chain F = (\<forall>i. F (Suc i) \<subseteq> F i)"
lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
by (simp add: down_chain_def)
@@ -43,10 +43,10 @@
lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i"
by (simp add: down_chain_def)
-lemma down_chain_less_mono [rule_format]:
- "down_chain F ==> x < y --> F y \<subseteq> F x"
- apply (induct_tac y)
- apply (blast dest: down_chainD elim: less_SucE)+
+lemma down_chain_less_mono:
+ "down_chain F ==> x < y ==> F y \<subseteq> F x"
+ apply (induct y)
+ apply (blast dest: down_chainD elim: less_SucE)+
done
lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x"
@@ -57,9 +57,9 @@
subsection "Continuity"
-constdefs
+definition
up_cont :: "('a set => 'a set) => bool"
- "up_cont f == \<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F)"
+ "up_cont f = (\<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F))"
lemma up_contI:
"(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
@@ -84,10 +84,10 @@
done
-constdefs
+definition
down_cont :: "('a set => 'a set) => bool"
- "down_cont f ==
- \<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F)"
+ "down_cont f =
+ (\<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F))"
lemma down_contI:
"(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>
@@ -114,9 +114,9 @@
subsection "Iteration"
-constdefs
+definition
up_iterate :: "('a set => 'a set) => nat => 'a set"
- "up_iterate f n == (f^n) {}"
+ "up_iterate f n = (f^n) {}"
lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
by (simp add: up_iterate_def)
@@ -166,9 +166,9 @@
done
-constdefs
+definition
down_iterate :: "('a set => 'a set) => nat => 'a set"
- "down_iterate f n == (f^n) UNIV"
+ "down_iterate f n = (f^n) UNIV"
lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
by (simp add: down_iterate_def)
--- a/src/HOL/Library/FuncSet.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/FuncSet.thy Sat May 27 17:42:02 2006 +0200
@@ -9,15 +9,15 @@
imports Main
begin
-constdefs
+definition
Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
- "Pi A B == {f. \<forall>x. x \<in> A --> f x \<in> B x}"
+ "Pi A B = {f. \<forall>x. x \<in> A --> f x \<in> B x}"
extensional :: "'a set => ('a => 'b) set"
- "extensional A == {f. \<forall>x. x~:A --> f x = arbitrary}"
+ "extensional A = {f. \<forall>x. x~:A --> f x = arbitrary}"
"restrict" :: "['a => 'b, 'a set] => ('a => 'b)"
- "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
+ "restrict f A = (%x. if x \<in> A then f x else arbitrary)"
abbreviation
funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "->" 60)
@@ -27,24 +27,24 @@
funcset (infixr "\<rightarrow>" 60)
syntax
- "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
- "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3%_:_./ _)" [0,0,3] 3)
+ "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
+ "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3%_:_./ _)" [0,0,3] 3)
syntax (xsymbols)
- "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
- "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
+ "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
+ "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
syntax (HTML output)
- "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
- "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
+ "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
+ "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
translations
"PI x:A. B" == "Pi A (%x. B)"
"%x:A. f" == "restrict (%x. f) A"
-constdefs
+definition
"compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
- "compose A g f == \<lambda>x\<in>A. g (f x)"
+ "compose A g f = (\<lambda>x\<in>A. g (f x))"
subsection{*Basic Properties of @{term Pi}*}
@@ -62,7 +62,7 @@
by (simp add: Pi_def)
lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B"
-by (auto simp add: Pi_def)
+ by (auto simp add: Pi_def)
lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
apply (simp add: Pi_def, auto)
@@ -133,7 +133,7 @@
by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
- by (auto simp add: restrict_def)
+ by (auto simp add: restrict_def)
subsection{*Bijections Between Sets*}
@@ -141,21 +141,21 @@
text{*The basic definition could be moved to @{text "Fun.thy"}, but most of
the theorems belong here, or need at least @{term Hilbert_Choice}.*}
-constdefs
- bij_betw :: "['a => 'b, 'a set, 'b set] => bool" (*bijective*)
- "bij_betw f A B == inj_on f A & f ` A = B"
+definition
+ bij_betw :: "['a => 'b, 'a set, 'b set] => bool" -- {* bijective *}
+ "bij_betw f A B = (inj_on f A & f ` A = B)"
lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
-by (simp add: bij_betw_def)
+ by (simp add: bij_betw_def)
lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
-by (auto simp add: bij_betw_def inj_on_Inv Pi_def)
+ by (auto simp add: bij_betw_def inj_on_Inv Pi_def)
lemma bij_betw_Inv: "bij_betw f A B \<Longrightarrow> bij_betw (Inv A f) B A"
-apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
-apply (simp add: image_compose [symmetric] o_def)
-apply (simp add: image_def Inv_f_f)
-done
+ apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
+ apply (simp add: image_compose [symmetric] o_def)
+ apply (simp add: image_def Inv_f_f)
+ done
lemma inj_on_compose:
"[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
@@ -163,9 +163,9 @@
lemma bij_betw_compose:
"[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C"
-apply (simp add: bij_betw_def compose_eq inj_on_compose)
-apply (auto simp add: compose_def image_def)
-done
+ apply (simp add: bij_betw_def compose_eq inj_on_compose)
+ apply (auto simp add: compose_def image_def)
+ done
lemma bij_betw_restrict_eq [simp]:
"bij_betw (restrict f A) A B = bij_betw f A B"
@@ -210,13 +210,13 @@
subsection{*Cardinality*}
lemma card_inj: "[|f \<in> A\<rightarrow>B; inj_on f A; finite B|] ==> card(A) \<le> card(B)"
-apply (rule card_inj_on_le)
-apply (auto simp add: Pi_def)
-done
+ apply (rule card_inj_on_le)
+ apply (auto simp add: Pi_def)
+ done
lemma card_bij:
"[|f \<in> A\<rightarrow>B; inj_on f A;
g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
-by (blast intro: card_inj order_antisym)
+ by (blast intro: card_inj order_antisym)
end
--- a/src/HOL/Library/NatPair.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/NatPair.thy Sat May 27 17:42:02 2006 +0200
@@ -11,25 +11,24 @@
begin
text{*
- An injective function from @{text "\<nat>\<twosuperior>"} to @{text
- \<nat>}. Definition and proofs are from \cite[page
- 85]{Oberschelp:1993}.
+ An injective function from @{text "\<nat>\<twosuperior>"} to @{text \<nat>}. Definition
+ and proofs are from \cite[page 85]{Oberschelp:1993}.
*}
-constdefs
+definition
nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
- "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n"
+ "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
proof (cases "2 dvd a")
case True
- thus ?thesis by (rule dvd_mult2)
+ then show ?thesis by (rule dvd_mult2)
next
case False
- hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
- hence "Suc a mod 2 = 0" by (simp add: mod_Suc)
- hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
- thus ?thesis by (rule dvd_mult)
+ then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
+ then have "Suc a mod 2 = 0" by (simp add: mod_Suc)
+ then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
+ then show ?thesis by (rule dvd_mult)
qed
lemma
@@ -37,7 +36,7 @@
shows nat2_to_nat_help: "u+v \<le> x+y"
proof (rule classical)
assume "\<not> ?thesis"
- hence contrapos: "x+y < u+v"
+ then have contrapos: "x+y < u+v"
by simp
have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
by (unfold nat2_to_nat_def) (simp add: Let_def)
@@ -48,7 +47,7 @@
proof -
have "2 dvd (x+y)*Suc(x+y)"
by (rule dvd2_a_x_suc_a)
- hence "(x+y)*Suc(x+y) mod 2 = 0"
+ then have "(x+y)*Suc(x+y) mod 2 = 0"
by (simp only: dvd_eq_mod_eq_0)
also
have "2 * Suc(x+y) mod 2 = 0"
@@ -56,7 +55,7 @@
ultimately have
"((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
by simp
- thus ?thesis
+ then show ?thesis
by simp
qed
also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
@@ -75,7 +74,7 @@
proof -
{
fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
- hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
+ then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
also from prems [symmetric] have "x+y \<le> u+v"
by (rule nat2_to_nat_help)
finally have eq: "u+v = x+y" .
@@ -86,9 +85,9 @@
with ux have "(u,v) = (x,y)"
by simp
}
- hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
+ then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
by fast
- thus ?thesis
+ then show ?thesis
by (unfold inj_on_def) simp
qed
--- a/src/HOL/Library/Nat_Infinity.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Sat May 27 17:42:02 2006 +0200
@@ -19,20 +19,20 @@
datatype inat = Fin nat | Infty
+const_syntax (xsymbols)
+ Infty ("\<infinity>")
+
+const_syntax (HTML output)
+ Infty ("\<infinity>")
+
instance inat :: "{ord, zero}" ..
-consts
+definition
iSuc :: "inat => inat"
-
-syntax (xsymbols)
- Infty :: inat ("\<infinity>")
+ "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>)"
-syntax (HTML output)
- Infty :: inat ("\<infinity>")
-
-defs
+defs (overloaded)
Zero_inat_def: "0 == Fin 0"
- iSuc_def: "iSuc i == case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>"
iless_def: "m < n ==
case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
| \<infinity> => False"
@@ -114,7 +114,6 @@
by (simp add: inat_defs split:inat_splits, arith?)
-(* ----------------------------------------------------------------------- *)
lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
by (simp add: inat_defs split:inat_splits, arith?)
--- a/src/HOL/Library/Product_ord.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Product_ord.thy Sat May 27 17:42:02 2006 +0200
@@ -9,20 +9,19 @@
imports Main
begin
-instance "*" :: (ord,ord) ord ..
+instance "*" :: (ord, ord) ord ..
defs (overloaded)
- prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
+ prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)"
lemmas prod_ord_defs = prod_less_def prod_le_def
-instance "*" :: (order,order) order
- apply (intro_classes, unfold prod_ord_defs)
- by (auto intro: order_less_trans)
+instance * :: (order, order) order
+ by default (auto simp: prod_ord_defs intro: order_less_trans)
-instance "*":: (linorder,linorder)linorder
- by (intro_classes, unfold prod_le_def, auto)
+instance * :: (linorder, linorder) linorder
+ by default (auto simp: prod_le_def)
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/SetsAndFunctions.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/SetsAndFunctions.thy Sat May 27 17:42:02 2006 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Library/SetsAndFunctions.thy
- ID: $Id$
+ ID: $Id$
Author: Jeremy Avigad and Kevin Donnelly
*)
@@ -9,13 +9,13 @@
imports Main
begin
-text {*
+text {*
This library lifts operations like addition and muliplication to sets and
functions of appropriate types. It was designed to support asymptotic
calculations. See the comments at the top of theory @{text BigO}.
*}
-subsection {* Basic definitions *}
+subsection {* Basic definitions *}
instance set :: (plus) plus ..
instance fun :: (type, plus) plus ..
@@ -28,14 +28,14 @@
instance fun :: (type, times) times ..
defs (overloaded)
- func_times: "f * g == (%x. f x * g x)"
+ func_times: "f * g == (%x. f x * g x)"
set_times:"A * B == {c. EX a:A. EX b:B. c = a * b}"
instance fun :: (type, minus) minus ..
defs (overloaded)
func_minus: "- f == (%x. - f x)"
- func_diff: "f - g == %x. f x - g x"
+ func_diff: "f - g == %x. f x - g x"
instance fun :: (type, zero) zero ..
instance set :: (zero) zero ..
@@ -51,12 +51,12 @@
func_one: "1::(('a::type) => ('b::one)) == %x. 1"
set_one: "1::('a::one)set == {1}"
-constdefs
+definition
elt_set_plus :: "'a::plus => 'a set => 'a set" (infixl "+o" 70)
- "a +o B == {c. EX b:B. c = a + b}"
+ "a +o B = {c. EX b:B. c = a + b}"
elt_set_times :: "'a::times => 'a set => 'a set" (infixl "*o" 80)
- "a *o B == {c. EX b:B. c = a * b}"
+ "a *o B = {c. EX b:B. c = a * b}"
abbreviation (input)
elt_set_eq :: "'a => 'a set => bool" (infix "=o" 50)
@@ -69,291 +69,292 @@
by default (auto simp add: func_zero func_plus add_ac)
instance fun :: (type,ab_group_add)ab_group_add
- apply intro_classes
- apply (simp add: func_minus func_plus func_zero)
+ apply default
+ apply (simp add: func_minus func_plus func_zero)
apply (simp add: func_minus func_plus func_diff diff_minus)
-done
+ done
instance fun :: (type,semigroup_mult)semigroup_mult
- apply intro_classes
+ apply default
apply (auto simp add: func_times mult_assoc)
-done
+ done
instance fun :: (type,comm_monoid_mult)comm_monoid_mult
- apply intro_classes
- apply (auto simp add: func_one func_times mult_ac)
-done
+ apply default
+ apply (auto simp add: func_one func_times mult_ac)
+ done
instance fun :: (type,comm_ring_1)comm_ring_1
- apply intro_classes
- apply (auto simp add: func_plus func_times func_minus func_diff ext
- func_one func_zero ring_eq_simps)
+ apply default
+ apply (auto simp add: func_plus func_times func_minus func_diff ext
+ func_one func_zero ring_eq_simps)
apply (drule fun_cong)
apply simp
-done
+ done
instance set :: (semigroup_add)semigroup_add
- apply intro_classes
+ apply default
apply (unfold set_plus)
apply (force simp add: add_assoc)
-done
+ done
instance set :: (semigroup_mult)semigroup_mult
- apply intro_classes
+ apply default
apply (unfold set_times)
apply (force simp add: mult_assoc)
-done
+ done
instance set :: (comm_monoid_add)comm_monoid_add
- apply intro_classes
- apply (unfold set_plus)
- apply (force simp add: add_ac)
+ apply default
+ apply (unfold set_plus)
+ apply (force simp add: add_ac)
apply (unfold set_zero)
apply force
-done
+ done
instance set :: (comm_monoid_mult)comm_monoid_mult
- apply intro_classes
- apply (unfold set_times)
- apply (force simp add: mult_ac)
+ apply default
+ apply (unfold set_times)
+ apply (force simp add: mult_ac)
apply (unfold set_one)
apply force
-done
+ done
+
subsection {* Basic properties *}
-lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
-by (auto simp add: set_plus)
+lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
+ by (auto simp add: set_plus)
lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
-by (auto simp add: elt_set_plus_def)
+ by (auto simp add: elt_set_plus_def)
-lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) +
- (b +o D) = (a + b) +o (C + D)"
+lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) +
+ (b +o D) = (a + b) +o (C + D)"
apply (auto simp add: elt_set_plus_def set_plus add_ac)
- apply (rule_tac x = "ba + bb" in exI)
+ apply (rule_tac x = "ba + bb" in exI)
apply (auto simp add: add_ac)
apply (rule_tac x = "aa + a" in exI)
apply (auto simp add: add_ac)
-done
+ done
-lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
- (a + b) +o C"
-by (auto simp add: elt_set_plus_def add_assoc)
+lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
+ (a + b) +o C"
+ by (auto simp add: elt_set_plus_def add_assoc)
-lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C =
- a +o (B + C)"
+lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C =
+ a +o (B + C)"
apply (auto simp add: elt_set_plus_def set_plus)
- apply (blast intro: add_ac)
+ apply (blast intro: add_ac)
apply (rule_tac x = "a + aa" in exI)
apply (rule conjI)
- apply (rule_tac x = "aa" in bexI)
- apply auto
+ apply (rule_tac x = "aa" in bexI)
+ apply auto
apply (rule_tac x = "ba" in bexI)
- apply (auto simp add: add_ac)
-done
+ apply (auto simp add: add_ac)
+ done
-theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) =
- a +o (C + D)"
+theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) =
+ a +o (C + D)"
apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus add_ac)
- apply (rule_tac x = "aa + ba" in exI)
- apply (auto simp add: add_ac)
-done
+ apply (rule_tac x = "aa + ba" in exI)
+ apply (auto simp add: add_ac)
+ done
theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
set_plus_rearrange3 set_plus_rearrange4
lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
-by (auto simp add: elt_set_plus_def)
+ by (auto simp add: elt_set_plus_def)
-lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
+lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
C + E <= D + F"
-by (auto simp add: set_plus)
+ by (auto simp add: set_plus)
lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C + D"
-by (auto simp add: elt_set_plus_def set_plus)
+ by (auto simp add: elt_set_plus_def set_plus)
-lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
- a +o D <= D + C"
-by (auto simp add: elt_set_plus_def set_plus add_ac)
+lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
+ a +o D <= D + C"
+ by (auto simp add: elt_set_plus_def set_plus add_ac)
lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C + D"
apply (subgoal_tac "a +o B <= a +o D")
- apply (erule order_trans)
- apply (erule set_plus_mono3)
+ apply (erule order_trans)
+ apply (erule set_plus_mono3)
apply (erule set_plus_mono)
-done
+ done
-lemma set_plus_mono_b: "C <= D ==> x : a +o C
+lemma set_plus_mono_b: "C <= D ==> x : a +o C
==> x : a +o D"
apply (frule set_plus_mono)
apply auto
-done
+ done
-lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==>
+lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==>
x : D + F"
apply (frule set_plus_mono2)
- prefer 2
- apply force
+ prefer 2
+ apply force
apply assumption
-done
+ done
lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C + D"
apply (frule set_plus_mono3)
apply auto
-done
+ done
-lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
- x : a +o D ==> x : D + C"
+lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
+ x : a +o D ==> x : D + C"
apply (frule set_plus_mono4)
apply auto
-done
+ done
lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
-by (auto simp add: elt_set_plus_def)
+ by (auto simp add: elt_set_plus_def)
lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A + B"
apply (auto intro!: subsetI simp add: set_plus)
apply (rule_tac x = 0 in bexI)
- apply (rule_tac x = x in bexI)
- apply (auto simp add: add_ac)
-done
+ apply (rule_tac x = x in bexI)
+ apply (auto simp add: add_ac)
+ done
lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
-by (auto simp add: elt_set_plus_def add_ac diff_minus)
+ by (auto simp add: elt_set_plus_def add_ac diff_minus)
lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
apply (auto simp add: elt_set_plus_def add_ac diff_minus)
apply (subgoal_tac "a = (a + - b) + b")
- apply (rule bexI, assumption, assumption)
+ apply (rule bexI, assumption, assumption)
apply (auto simp add: add_ac)
-done
+ done
lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
-by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
+ by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
assumption)
-lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
-by (auto simp add: set_times)
+lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
+ by (auto simp add: set_times)
lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
-by (auto simp add: elt_set_times_def)
+ by (auto simp add: elt_set_times_def)
-lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) *
- (b *o D) = (a * b) *o (C * D)"
+lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) *
+ (b *o D) = (a * b) *o (C * D)"
apply (auto simp add: elt_set_times_def set_times)
- apply (rule_tac x = "ba * bb" in exI)
- apply (auto simp add: mult_ac)
+ apply (rule_tac x = "ba * bb" in exI)
+ apply (auto simp add: mult_ac)
apply (rule_tac x = "aa * a" in exI)
apply (auto simp add: mult_ac)
-done
+ done
-lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
- (a * b) *o C"
-by (auto simp add: elt_set_times_def mult_assoc)
+lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
+ (a * b) *o C"
+ by (auto simp add: elt_set_times_def mult_assoc)
-lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C =
- a *o (B * C)"
+lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C =
+ a *o (B * C)"
apply (auto simp add: elt_set_times_def set_times)
- apply (blast intro: mult_ac)
+ apply (blast intro: mult_ac)
apply (rule_tac x = "a * aa" in exI)
apply (rule conjI)
- apply (rule_tac x = "aa" in bexI)
- apply auto
+ apply (rule_tac x = "aa" in bexI)
+ apply auto
apply (rule_tac x = "ba" in bexI)
- apply (auto simp add: mult_ac)
-done
+ apply (auto simp add: mult_ac)
+ done
-theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) =
- a *o (C * D)"
- apply (auto intro!: subsetI simp add: elt_set_times_def set_times
+theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) =
+ a *o (C * D)"
+ apply (auto intro!: subsetI simp add: elt_set_times_def set_times
mult_ac)
- apply (rule_tac x = "aa * ba" in exI)
- apply (auto simp add: mult_ac)
-done
+ apply (rule_tac x = "aa * ba" in exI)
+ apply (auto simp add: mult_ac)
+ done
theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
set_times_rearrange3 set_times_rearrange4
lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
-by (auto simp add: elt_set_times_def)
+ by (auto simp add: elt_set_times_def)
-lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
+lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
C * E <= D * F"
-by (auto simp add: set_times)
+ by (auto simp add: set_times)
lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C * D"
-by (auto simp add: elt_set_times_def set_times)
+ by (auto simp add: elt_set_times_def set_times)
-lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
- a *o D <= D * C"
-by (auto simp add: elt_set_times_def set_times mult_ac)
+lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
+ a *o D <= D * C"
+ by (auto simp add: elt_set_times_def set_times mult_ac)
lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C * D"
apply (subgoal_tac "a *o B <= a *o D")
- apply (erule order_trans)
- apply (erule set_times_mono3)
+ apply (erule order_trans)
+ apply (erule set_times_mono3)
apply (erule set_times_mono)
-done
+ done
-lemma set_times_mono_b: "C <= D ==> x : a *o C
+lemma set_times_mono_b: "C <= D ==> x : a *o C
==> x : a *o D"
apply (frule set_times_mono)
apply auto
-done
+ done
-lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==>
+lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==>
x : D * F"
apply (frule set_times_mono2)
- prefer 2
- apply force
+ prefer 2
+ apply force
apply assumption
-done
+ done
lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C * D"
apply (frule set_times_mono3)
apply auto
-done
+ done
-lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
- x : a *o D ==> x : D * C"
+lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
+ x : a *o D ==> x : D * C"
apply (frule set_times_mono4)
apply auto
-done
+ done
lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
-by (auto simp add: elt_set_times_def)
+ by (auto simp add: elt_set_times_def)
-lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
- (a * b) +o (a *o C)"
-by (auto simp add: elt_set_plus_def elt_set_times_def ring_distrib)
+lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
+ (a * b) +o (a *o C)"
+ by (auto simp add: elt_set_plus_def elt_set_times_def ring_distrib)
-lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
- (a *o B) + (a *o C)"
+lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
+ (a *o B) + (a *o C)"
apply (auto simp add: set_plus elt_set_times_def ring_distrib)
- apply blast
+ apply blast
apply (rule_tac x = "b + bb" in exI)
apply (auto simp add: ring_distrib)
-done
+ done
-lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
+lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
a *o D + C * D"
- apply (auto intro!: subsetI simp add:
- elt_set_plus_def elt_set_times_def set_times
+ apply (auto intro!: subsetI simp add:
+ elt_set_plus_def elt_set_times_def set_times
set_plus ring_distrib)
apply auto
-done
+ done
theorems set_times_plus_distribs =
set_times_plus_distrib
set_times_plus_distrib2
-lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
- - a : C"
-by (auto simp add: elt_set_times_def)
+lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
+ - a : C"
+ by (auto simp add: elt_set_times_def)
lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
- a : (- 1) *o C"
-by (auto simp add: elt_set_times_def)
-
+ by (auto simp add: elt_set_times_def)
+
end
--- a/src/HOL/Library/While_Combinator.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/While_Combinator.thy Sat May 27 17:42:02 2006 +0200
@@ -35,7 +35,7 @@
apply blast
done
-constdefs
+definition
while :: "('a => bool) => ('a => 'a) => 'a => 'a"
"while b c s == while_aux (b, c, s)"
@@ -88,7 +88,8 @@
and terminate: "!!s. P s ==> \<not> b s ==> Q s"
and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
shows "P s \<Longrightarrow> Q (while b c s)"
- apply (induct s rule: wf [THEN wf_induct])
+ using wf
+ apply (induct s)
apply simp
apply (subst while_unfold)
apply (simp add: invariant terminate)
@@ -101,13 +102,13 @@
wf r;
!!s. [| P s; b s |] ==> (c s, s) \<in> r |] ==>
Q (while b c s)"
-apply (rule while_rule_lemma)
-prefer 4 apply assumption
-apply blast
-apply blast
-apply(erule wf_subset)
-apply blast
-done
+ apply (rule while_rule_lemma)
+ prefer 4 apply assumption
+ apply blast
+ apply blast
+ apply (erule wf_subset)
+ apply blast
+ done
text {*
\medskip An application: computation of the @{term lfp} on finite
@@ -142,12 +143,11 @@
looping because the antisymmetry simproc turns the subset relationship
back into equality. *}
-lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))"
- by blast
-
theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
P {0, 4, 2}"
proof -
+ have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))"
+ by blast
have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
apply blast
done
--- a/src/HOL/Library/Word.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Word.thy Sat May 27 17:42:02 2006 +0200
@@ -56,17 +56,17 @@
bitor :: "bit => bit => bit" (infixr "bitor" 30)
bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
-syntax (xsymbols)
- bitnot :: "bit => bit" ("\<not>\<^sub>b _" [40] 40)
- bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
- bitor :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
- bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
+const_syntax (xsymbols)
+ bitnot ("\<not>\<^sub>b _" [40] 40)
+ bitand (infixr "\<and>\<^sub>b" 35)
+ bitor (infixr "\<or>\<^sub>b" 30)
+ bitxor (infixr "\<oplus>\<^sub>b" 30)
-syntax (HTML output)
- bitnot :: "bit => bit" ("\<not>\<^sub>b _" [40] 40)
- bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
- bitor :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
- bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
+const_syntax (HTML output)
+ bitnot ("\<not>\<^sub>b _" [40] 40)
+ bitand (infixr "\<and>\<^sub>b" 35)
+ bitor (infixr "\<or>\<^sub>b" 30)
+ bitxor (infixr "\<oplus>\<^sub>b" 30)
primrec
bitnot_zero: "(bitnot \<zero>) = \<one>"
@@ -141,13 +141,13 @@
by (cases b,auto intro!: zero one)
qed
-constdefs
+definition
bv_msb :: "bit list => bit"
- "bv_msb w == if w = [] then \<zero> else hd w"
+ "bv_msb w = (if w = [] then \<zero> else hd w)"
bv_extend :: "[nat,bit,bit list]=>bit list"
- "bv_extend i b w == (replicate (i - length w) b) @ w"
+ "bv_extend i b w = (replicate (i - length w) b) @ w"
bv_not :: "bit list => bit list"
- "bv_not w == map bitnot w"
+ "bv_not w = map bitnot w"
lemma bv_length_extend [simp]: "length w \<le> i ==> length (bv_extend i b w) = i"
by (simp add: bv_extend_def)
@@ -176,9 +176,9 @@
lemma length_bv_not [simp]: "length (bv_not w) = length w"
by (induct w,simp_all)
-constdefs
+definition
bv_to_nat :: "bit list => nat"
- "bv_to_nat == foldl (%bn b. 2 * bn + bitval b) 0"
+ "bv_to_nat = foldl (%bn b. 2 * bn + bitval b) 0"
lemma bv_to_nat_Nil [simp]: "bv_to_nat [] = 0"
by (simp add: bv_to_nat_def)
@@ -326,9 +326,9 @@
..
qed
-constdefs
+definition
norm_unsigned :: "bit list => bit list"
- "norm_unsigned == rem_initial \<zero>"
+ "norm_unsigned = rem_initial \<zero>"
lemma norm_unsigned_Nil [simp]: "norm_unsigned [] = []"
by (simp add: norm_unsigned_def)
@@ -349,9 +349,9 @@
"nat_to_bv_helper n = (%bs. (if n = 0 then bs
else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
-constdefs
+definition
nat_to_bv :: "nat => bit list"
- "nat_to_bv n == nat_to_bv_helper n []"
+ "nat_to_bv n = nat_to_bv_helper n []"
lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []"
by (simp add: nat_to_bv_def)
@@ -400,7 +400,7 @@
assume "k \<le> j" and "j < i"
with a
show "P j"
- by auto
+ by auto
qed
show "\<forall> j. k \<le> j \<and> j < i + 1 --> P j"
proof auto
@@ -409,18 +409,18 @@
assume ji: "j \<le> i"
show "P j"
proof (cases "j = i")
- assume "j = i"
- with pi
- show "P j"
- by simp
+ assume "j = i"
+ with pi
+ show "P j"
+ by simp
next
- assume "j ~= i"
- with ji
- have "j < i"
- by simp
- with kj and a
- show "P j"
- by blast
+ assume "j ~= i"
+ with ji
+ have "j < i"
+ by simp
+ with kj and a
+ show "P j"
+ by blast
qed
qed
qed
@@ -446,39 +446,39 @@
fix l
show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
proof (cases "n < 0")
- assume "n < 0"
- thus ?thesis
- by (simp add: nat_to_bv_helper.simps)
+ assume "n < 0"
+ thus ?thesis
+ by (simp add: nat_to_bv_helper.simps)
next
- assume "~n < 0"
- show ?thesis
- proof (rule n_div_2_cases [of n])
- assume [simp]: "n = 0"
- show ?thesis
- apply (simp only: nat_to_bv_helper.simps [of n])
- apply simp
- done
- next
- assume n2n: "n div 2 < n"
- assume [simp]: "0 < n"
- hence n20: "0 \<le> n div 2"
- by arith
- from ind [of "n div 2"] and n2n n20
- have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
- by blast
- show ?thesis
- apply (simp only: nat_to_bv_helper.simps [of n])
- apply (cases "n=0")
- apply simp
- apply (simp only: if_False)
- apply simp
- apply (subst spec [OF ind',of "\<zero>#l"])
- apply (subst spec [OF ind',of "\<one>#l"])
- apply (subst spec [OF ind',of "[\<one>]"])
- apply (subst spec [OF ind',of "[\<zero>]"])
- apply simp
- done
- qed
+ assume "~n < 0"
+ show ?thesis
+ proof (rule n_div_2_cases [of n])
+ assume [simp]: "n = 0"
+ show ?thesis
+ apply (simp only: nat_to_bv_helper.simps [of n])
+ apply simp
+ done
+ next
+ assume n2n: "n div 2 < n"
+ assume [simp]: "0 < n"
+ hence n20: "0 \<le> n div 2"
+ by arith
+ from ind [of "n div 2"] and n2n n20
+ have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
+ by blast
+ show ?thesis
+ apply (simp only: nat_to_bv_helper.simps [of n])
+ apply (cases "n=0")
+ apply simp
+ apply (simp only: if_False)
+ apply simp
+ apply (subst spec [OF ind',of "\<zero>#l"])
+ apply (subst spec [OF ind',of "\<one>#l"])
+ apply (subst spec [OF ind',of "[\<one>]"])
+ apply (subst spec [OF ind',of "[\<zero>]"])
+ apply simp
+ done
+ qed
qed
qed
qed
@@ -511,14 +511,14 @@
fix l2
show "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
proof -
- have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
- by (induct "length xs",simp_all)
- hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
- bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
- by simp
- also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
- by (simp add: ring_distrib)
- finally show ?thesis .
+ have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
+ by (induct "length xs",simp_all)
+ hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
+ bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
+ by simp
+ also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
+ by (simp add: ring_distrib)
+ finally show ?thesis .
qed
qed
qed
@@ -553,15 +553,15 @@
apply (simp add: ind' split del: split_if)
apply (cases "n mod 2 = 0")
proof simp_all
- assume "n mod 2 = 0"
- with mod_div_equality [of n 2]
- show "n div 2 * 2 = n"
- by simp
+ assume "n mod 2 = 0"
+ with mod_div_equality [of n 2]
+ show "n div 2 * 2 = n"
+ by simp
next
- assume "n mod 2 = Suc 0"
- with mod_div_equality [of n 2]
- show "Suc (n div 2 * 2) = n"
- by simp
+ assume "n mod 2 = Suc 0"
+ with mod_div_equality [of n 2]
+ show "Suc (n div 2 * 2) = n"
+ by simp
qed
qed
qed
@@ -715,41 +715,41 @@
assume ind: "\<forall>ys. length ys < length xs --> ?P ys"
show "?P xs"
proof (cases xs)
- assume [simp]: "xs = []"
- show ?thesis
- by (simp add: nat_to_bv_non0)
+ assume [simp]: "xs = []"
+ show ?thesis
+ by (simp add: nat_to_bv_non0)
next
- fix y ys
- assume [simp]: "xs = y # ys"
- show ?thesis
- apply simp
- apply (subst bv_to_nat_dist_append)
- apply simp
- proof -
- have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
- nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
- by (simp add: add_ac mult_ac)
- also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
- by simp
- also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
- proof -
- from ind
- have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
- by auto
- hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
- by simp
- show ?thesis
- apply (subst nat_helper1)
- apply simp_all
- done
- qed
- also have "... = (\<one>#rev ys) @ [y]"
- by simp
- also have "... = \<one> # rev ys @ [y]"
- by simp
- finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]"
- .
- qed
+ fix y ys
+ assume [simp]: "xs = y # ys"
+ show ?thesis
+ apply simp
+ apply (subst bv_to_nat_dist_append)
+ apply simp
+ proof -
+ have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
+ nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
+ by (simp add: add_ac mult_ac)
+ also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
+ by simp
+ also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
+ proof -
+ from ind
+ have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
+ by auto
+ hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
+ by simp
+ show ?thesis
+ apply (subst nat_helper1)
+ apply simp_all
+ done
+ qed
+ also have "... = (\<one>#rev ys) @ [y]"
+ by simp
+ also have "... = \<one> # rev ys @ [y]"
+ by simp
+ finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]"
+ .
+ qed
qed
qed
qed
@@ -856,9 +856,9 @@
subsection {* Unsigned Arithmetic Operations *}
-constdefs
+definition
bv_add :: "[bit list, bit list ] => bit list"
- "bv_add w1 w2 == nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"
+ "bv_add w1 w2 = nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"
lemma bv_add_type1 [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2"
by (simp add: bv_add_def)
@@ -893,13 +893,13 @@
proof
assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
- by (rule add_right_mono)
+ by (rule add_right_mono)
hence "(2::nat) ^ length w1 \<le> 2 ^ length w2"
- by simp
+ by simp
hence "length w1 \<le> length w2"
- by simp
+ by simp
thus False
- by simp
+ by simp
qed
thus ?thesis
by (simp add: diff_mult_distrib2 split: split_max)
@@ -908,9 +908,9 @@
by arith
qed
-constdefs
+definition
bv_mult :: "[bit list, bit list ] => bit list"
- "bv_mult w1 w2 == nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"
+ "bv_mult w1 w2 = nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"
lemma bv_mult_type1 [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2"
by (simp add: bv_mult_def)
@@ -968,11 +968,11 @@
lemmas [simp del] = norm_signed_Cons
-constdefs
+definition
int_to_bv :: "int => bit list"
- "int_to_bv n == if 0 \<le> n
+ "int_to_bv n = (if 0 \<le> n
then norm_signed (\<zero>#nat_to_bv (nat n))
- else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))"
+ else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1)))))"
lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv (nat n))"
by (simp add: int_to_bv_def)
@@ -1003,9 +1003,11 @@
qed
qed
-constdefs
+definition
bv_to_int :: "bit list => int"
- "bv_to_int w == case bv_msb w of \<zero> => int (bv_to_nat w) | \<one> => - int (bv_to_nat (bv_not w) + 1)"
+ "bv_to_int w =
+ (case bv_msb w of \<zero> => int (bv_to_nat w)
+ | \<one> => - int (bv_to_nat (bv_not w) + 1))"
lemma bv_to_int_Nil [simp]: "bv_to_int [] = 0"
by (simp add: bv_to_int_def)
@@ -1232,23 +1234,23 @@
assume "norm_unsigned w' = []"
with weq and w0
show False
- by (simp add: norm_empty_bv_to_nat_zero)
+ by (simp add: norm_empty_bv_to_nat_zero)
next
assume w'0: "norm_unsigned w' \<noteq> []"
have "0 < bv_to_nat w'"
proof (rule ccontr)
- assume "~ (0 < bv_to_nat w')"
- hence "bv_to_nat w' = 0"
- by arith
- hence "norm_unsigned w' = []"
- by (simp add: bv_to_nat_zero_imp_empty)
- with w'0
- show False
- by simp
+ assume "~ (0 < bv_to_nat w')"
+ hence "bv_to_nat w' = 0"
+ by arith
+ hence "norm_unsigned w' = []"
+ by (simp add: bv_to_nat_zero_imp_empty)
+ with w'0
+ show False
+ by simp
qed
with bv_to_nat_lower_limit [of w']
show "2 ^ (length (norm_unsigned w') - Suc 0) \<le> int (bv_to_nat w')"
- by (simp add: int_nat_two_exp)
+ by (simp add: int_nat_two_exp)
qed
next
fix w'
@@ -1327,47 +1329,47 @@
proof (rule bit_list_cases [of "norm_signed w"])
assume "norm_signed w = []"
hence "bv_to_int (norm_signed w) = 0"
- by simp
+ by simp
with w0
show ?thesis
- by simp
+ by simp
next
fix w'
assume nw: "norm_signed w = \<zero> # w'"
from msbw
have "bv_msb (norm_signed w) = \<one>"
- by simp
+ by simp
with nw
show ?thesis
- by simp
+ by simp
next
fix w'
assume weq: "norm_signed w = \<one> # w'"
show ?thesis
proof (rule bit_list_cases [of w'])
- assume w'eq: "w' = []"
- from w0
- have "bv_to_int (norm_signed w) < -1"
- by simp
- with w'eq and weq
- show ?thesis
- by simp
+ assume w'eq: "w' = []"
+ from w0
+ have "bv_to_int (norm_signed w) < -1"
+ by simp
+ with w'eq and weq
+ show ?thesis
+ by simp
next
- fix w''
- assume w'eq: "w' = \<zero> # w''"
- show ?thesis
- apply (simp add: weq w'eq)
- apply (subgoal_tac "- int (bv_to_nat (bv_not w'')) + -1 < 0 + 0")
- apply (simp add: int_nat_two_exp)
- apply (rule add_le_less_mono)
- apply simp_all
- done
+ fix w''
+ assume w'eq: "w' = \<zero> # w''"
+ show ?thesis
+ apply (simp add: weq w'eq)
+ apply (subgoal_tac "- int (bv_to_nat (bv_not w'')) + -1 < 0 + 0")
+ apply (simp add: int_nat_two_exp)
+ apply (rule add_le_less_mono)
+ apply simp_all
+ done
next
- fix w''
- assume w'eq: "w' = \<one> # w''"
- with weq and msb_tl
- show ?thesis
- by simp
+ fix w''
+ assume w'eq: "w' = \<one> # w''"
+ with weq and msb_tl
+ show ?thesis
+ by simp
qed
qed
qed
@@ -1396,7 +1398,7 @@
proof (rule bv_to_int_lower_limit_gt0)
from w0
show "0 < bv_to_int (int_to_bv i)"
- by simp
+ by simp
qed
thus ?thesis
by simp
@@ -1586,9 +1588,9 @@
subsubsection {* Conversion from unsigned to signed *}
-constdefs
+definition
utos :: "bit list => bit list"
- "utos w == norm_signed (\<zero> # w)"
+ "utos w = norm_signed (\<zero> # w)"
lemma utos_type [simp]: "utos (norm_unsigned w) = utos w"
by (simp add: utos_def norm_signed_Cons)
@@ -1610,9 +1612,9 @@
subsubsection {* Unary minus *}
-constdefs
+definition
bv_uminus :: "bit list => bit list"
- "bv_uminus w == int_to_bv (- bv_to_int w)"
+ "bv_uminus w = int_to_bv (- bv_to_int w)"
lemma bv_uminus_type [simp]: "bv_uminus (norm_signed w) = bv_uminus w"
by (simp add: bv_uminus_def)
@@ -1636,16 +1638,16 @@
proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all)
from prems
show "bv_to_int w < 0"
- by simp
+ by simp
next
have "-(2^(length w - 1)) \<le> bv_to_int w"
- by (rule bv_to_int_lower_range)
+ by (rule bv_to_int_lower_range)
hence "- bv_to_int w \<le> 2^(length w - 1)"
- by simp
+ by simp
also from lw have "... < 2 ^ length w"
- by simp
+ by simp
finally show "- bv_to_int w < 2 ^ length w"
- by simp
+ by simp
qed
next
assume p: "- bv_to_int w = 1"
@@ -1674,10 +1676,10 @@
apply simp
proof -
have "bv_to_int w < 2 ^ (length w - 1)"
- by (rule bv_to_int_upper_range)
+ by (rule bv_to_int_upper_range)
also have "... \<le> 2 ^ length w" by simp
finally show "bv_to_int w \<le> 2 ^ length w"
- by simp
+ by simp
qed
qed
qed
@@ -1709,9 +1711,9 @@
qed
qed
-constdefs
+definition
bv_sadd :: "[bit list, bit list ] => bit list"
- "bv_sadd w1 w2 == int_to_bv (bv_to_int w1 + bv_to_int w2)"
+ "bv_sadd w1 w2 = int_to_bv (bv_to_int w1 + bv_to_int w2)"
lemma bv_sadd_type1 [simp]: "bv_sadd (norm_signed w1) w2 = bv_sadd w1 w2"
by (simp add: bv_sadd_def)
@@ -1756,10 +1758,10 @@
assume [simp]: "w1 = []"
show "w2 \<noteq> []"
proof (rule ccontr,simp)
- assume [simp]: "w2 = []"
- from p
- show False
- by simp
+ assume [simp]: "w2 = []"
+ from p
+ show False
+ by simp
qed
qed
qed
@@ -1784,18 +1786,18 @@
proof simp
from bv_to_int_upper_range [of w2]
have "bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
- by simp
+ by simp
with bv_to_int_upper_range [of w1]
have "bv_to_int w1 + bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
- by (rule zadd_zless_mono)
+ by (rule zadd_zless_mono)
also have "... \<le> 2 ^ max (length w1) (length w2)"
- apply (rule adder_helper)
- apply (rule helper)
- using p
- apply simp
- done
+ apply (rule adder_helper)
+ apply (rule helper)
+ using p
+ apply simp
+ done
finally show "?Q < 2 ^ max (length w1) (length w2)"
- .
+ .
qed
next
assume p: "?Q < -1"
@@ -1805,26 +1807,26 @@
apply (rule p)
proof -
have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
- apply (rule adder_helper)
- apply (rule helper)
- using p
- apply simp
- done
+ apply (rule adder_helper)
+ apply (rule helper)
+ using p
+ apply simp
+ done
hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
- by simp
+ by simp
also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> ?Q"
- apply (rule add_mono)
- apply (rule bv_to_int_lower_range [of w1])
- apply (rule bv_to_int_lower_range [of w2])
- done
+ apply (rule add_mono)
+ apply (rule bv_to_int_lower_range [of w1])
+ apply (rule bv_to_int_lower_range [of w2])
+ done
finally show "- (2^max (length w1) (length w2)) \<le> ?Q" .
qed
qed
qed
-constdefs
+definition
bv_sub :: "[bit list, bit list] => bit list"
- "bv_sub w1 w2 == bv_sadd w1 (bv_uminus w2)"
+ "bv_sub w1 w2 = bv_sadd w1 (bv_uminus w2)"
lemma bv_sub_type1 [simp]: "bv_sub (norm_signed w1) w2 = bv_sub w1 w2"
by (simp add: bv_sub_def)
@@ -1878,18 +1880,18 @@
proof simp
from bv_to_int_lower_range [of w2]
have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
- by simp
+ by simp
have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
- apply (rule zadd_zless_mono)
- apply (rule bv_to_int_upper_range [of w1])
- apply (rule v2)
- done
+ apply (rule zadd_zless_mono)
+ apply (rule bv_to_int_upper_range [of w1])
+ apply (rule v2)
+ done
also have "... \<le> 2 ^ max (length w1) (length w2)"
- apply (rule adder_helper)
- apply (rule lmw)
- done
+ apply (rule adder_helper)
+ apply (rule lmw)
+ done
finally show "?Q < 2 ^ max (length w1) (length w2)"
- by simp
+ by simp
qed
next
assume p: "?Q < -1"
@@ -1899,26 +1901,26 @@
apply (rule p)
proof simp
have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
- apply (rule adder_helper)
- apply (rule lmw)
- done
+ apply (rule adder_helper)
+ apply (rule lmw)
+ done
hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
- by simp
+ by simp
also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> bv_to_int w1 + -bv_to_int w2"
- apply (rule add_mono)
- apply (rule bv_to_int_lower_range [of w1])
- using bv_to_int_upper_range [of w2]
- apply simp
- done
+ apply (rule add_mono)
+ apply (rule bv_to_int_lower_range [of w1])
+ using bv_to_int_upper_range [of w2]
+ apply simp
+ done
finally show "- (2^max (length w1) (length w2)) \<le> ?Q"
- by simp
+ by simp
qed
qed
qed
-constdefs
+definition
bv_smult :: "[bit list, bit list] => bit list"
- "bv_smult w1 w2 == int_to_bv (bv_to_int w1 * bv_to_int w2)"
+ "bv_smult w1 w2 = int_to_bv (bv_to_int w1 * bv_to_int w2)"
lemma bv_smult_type1 [simp]: "bv_smult (norm_signed w1) w2 = bv_smult w1 w2"
by (simp add: bv_smult_def)
@@ -1963,58 +1965,58 @@
assume bi1: "0 < bv_to_int w1"
assume bi2: "0 < bv_to_int w2"
show ?thesis
- apply (simp add: bv_smult_def)
- apply (rule length_int_to_bv_upper_limit_gt0)
- apply (rule p)
+ apply (simp add: bv_smult_def)
+ apply (rule length_int_to_bv_upper_limit_gt0)
+ apply (rule p)
proof simp
- have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
- apply (rule mult_strict_mono)
- apply (rule bv_to_int_upper_range)
- apply (rule bv_to_int_upper_range)
- apply (rule zero_less_power)
- apply simp
- using bi2
- apply simp
- done
- also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
- apply simp
- apply (subst zpower_zadd_distrib [symmetric])
- apply simp
- apply arith
- done
- finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
- .
+ have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
+ apply (rule mult_strict_mono)
+ apply (rule bv_to_int_upper_range)
+ apply (rule bv_to_int_upper_range)
+ apply (rule zero_less_power)
+ apply simp
+ using bi2
+ apply simp
+ done
+ also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
+ apply simp
+ apply (subst zpower_zadd_distrib [symmetric])
+ apply simp
+ apply arith
+ done
+ finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
+ .
qed
next
assume bi1: "bv_to_int w1 < 0"
assume bi2: "bv_to_int w2 < 0"
show ?thesis
- apply (simp add: bv_smult_def)
- apply (rule length_int_to_bv_upper_limit_gt0)
- apply (rule p)
+ apply (simp add: bv_smult_def)
+ apply (rule length_int_to_bv_upper_limit_gt0)
+ apply (rule p)
proof simp
- have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
- apply (rule mult_mono)
- using bv_to_int_lower_range [of w1]
- apply simp
- using bv_to_int_lower_range [of w2]
- apply simp
- apply (rule zero_le_power,simp)
- using bi2
- apply simp
- done
- hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
- by simp
- also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
- apply simp
- apply (subst zpower_zadd_distrib [symmetric])
- apply simp
- apply (cut_tac lmw)
- apply arith
- apply (cut_tac p)
- apply arith
- done
- finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
+ have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
+ apply (rule mult_mono)
+ using bv_to_int_lower_range [of w1]
+ apply simp
+ using bv_to_int_lower_range [of w2]
+ apply simp
+ apply (rule zero_le_power,simp)
+ using bi2
+ apply simp
+ done
+ hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
+ by simp
+ also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
+ apply simp
+ apply (subst zpower_zadd_distrib [symmetric])
+ apply simp
+ apply (cut_tac lmw)
+ apply arith
+ apply (cut_tac p)
+ apply arith
+ done
+ finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
qed
qed
next
@@ -2025,60 +2027,60 @@
apply (rule p)
proof simp
have "(2::int) ^ (length w1 - 1) * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
- apply simp
- apply (subst zpower_zadd_distrib [symmetric])
- apply simp
- apply (cut_tac lmw)
- apply arith
- apply (cut_tac p)
- apply arith
- done
+ apply simp
+ apply (subst zpower_zadd_distrib [symmetric])
+ apply simp
+ apply (cut_tac lmw)
+ apply arith
+ apply (cut_tac p)
+ apply arith
+ done
hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
- by simp
+ by simp
also have "... \<le> ?Q"
proof -
- from p
- have q: "bv_to_int w1 * bv_to_int w2 < 0"
- by simp
- thus ?thesis
- proof (simp add: mult_less_0_iff,safe)
- assume bi1: "0 < bv_to_int w1"
- assume bi2: "bv_to_int w2 < 0"
- have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
- apply (rule mult_mono)
- using bv_to_int_lower_range [of w2]
- apply simp
- using bv_to_int_upper_range [of w1]
- apply simp
- apply (rule zero_le_power,simp)
- using bi1
- apply simp
- done
- hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
- by (simp add: zmult_ac)
- thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
- by simp
- next
- assume bi1: "bv_to_int w1 < 0"
- assume bi2: "0 < bv_to_int w2"
- have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
- apply (rule mult_mono)
- using bv_to_int_lower_range [of w1]
- apply simp
- using bv_to_int_upper_range [of w2]
- apply simp
- apply (rule zero_le_power,simp)
- using bi2
- apply simp
- done
- hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
- by (simp add: zmult_ac)
- thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
- by simp
- qed
+ from p
+ have q: "bv_to_int w1 * bv_to_int w2 < 0"
+ by simp
+ thus ?thesis
+ proof (simp add: mult_less_0_iff,safe)
+ assume bi1: "0 < bv_to_int w1"
+ assume bi2: "bv_to_int w2 < 0"
+ have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
+ apply (rule mult_mono)
+ using bv_to_int_lower_range [of w2]
+ apply simp
+ using bv_to_int_upper_range [of w1]
+ apply simp
+ apply (rule zero_le_power,simp)
+ using bi1
+ apply simp
+ done
+ hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
+ by (simp add: zmult_ac)
+ thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
+ by simp
+ next
+ assume bi1: "bv_to_int w1 < 0"
+ assume bi2: "0 < bv_to_int w2"
+ have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
+ apply (rule mult_mono)
+ using bv_to_int_lower_range [of w1]
+ apply simp
+ using bv_to_int_upper_range [of w2]
+ apply simp
+ apply (rule zero_le_power,simp)
+ using bi2
+ apply simp
+ done
+ hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
+ by (simp add: zmult_ac)
+ thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
+ by simp
+ qed
qed
finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q"
- .
+ .
qed
qed
qed
@@ -2110,35 +2112,35 @@
proof (simp add: zero_less_mult_iff,safe)
assume biw2: "0 < bv_to_int w2"
show ?thesis
- apply (simp add: bv_smult_def)
- apply (rule length_int_to_bv_upper_limit_gt0)
- apply (rule p)
+ apply (simp add: bv_smult_def)
+ apply (rule length_int_to_bv_upper_limit_gt0)
+ apply (rule p)
proof simp
- have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
- apply (rule mult_strict_mono)
- apply (simp add: bv_to_int_utos int_nat_two_exp)
- apply (rule bv_to_nat_upper_range)
- apply (rule bv_to_int_upper_range)
- apply (rule zero_less_power,simp)
- using biw2
- apply simp
- done
- also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
- apply simp
- apply (subst zpower_zadd_distrib [symmetric])
- apply simp
- apply (cut_tac lmw)
- apply arith
- using p
- apply auto
- done
- finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
- .
+ have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
+ apply (rule mult_strict_mono)
+ apply (simp add: bv_to_int_utos int_nat_two_exp)
+ apply (rule bv_to_nat_upper_range)
+ apply (rule bv_to_int_upper_range)
+ apply (rule zero_less_power,simp)
+ using biw2
+ apply simp
+ done
+ also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
+ apply simp
+ apply (subst zpower_zadd_distrib [symmetric])
+ apply simp
+ apply (cut_tac lmw)
+ apply arith
+ using p
+ apply auto
+ done
+ finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
+ .
qed
next
assume "bv_to_int (utos w1) < 0"
thus ?thesis
- by (simp add: bv_to_int_utos)
+ by (simp add: bv_to_int_utos)
qed
next
assume p: "?Q = -1"
@@ -2156,48 +2158,48 @@
apply (rule p)
proof simp
have "(2::int) ^ length w1 * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
- apply simp
- apply (subst zpower_zadd_distrib [symmetric])
- apply simp
- apply (cut_tac lmw)
- apply arith
- apply (cut_tac p)
- apply arith
- done
+ apply simp
+ apply (subst zpower_zadd_distrib [symmetric])
+ apply simp
+ apply (cut_tac lmw)
+ apply arith
+ apply (cut_tac p)
+ apply arith
+ done
hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^ length w1 * 2 ^ (length w2 - 1))"
- by simp
+ by simp
also have "... \<le> ?Q"
proof -
- from p
- have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
- by simp
- thus ?thesis
- proof (simp add: mult_less_0_iff,safe)
- assume bi1: "0 < bv_to_int (utos w1)"
- assume bi2: "bv_to_int w2 < 0"
- have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
- apply (rule mult_mono)
- using bv_to_int_lower_range [of w2]
- apply simp
- apply (simp add: bv_to_int_utos)
- using bv_to_nat_upper_range [of w1]
- apply (simp add: int_nat_two_exp)
- apply (rule zero_le_power,simp)
- using bi1
- apply simp
- done
- hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))"
- by (simp add: zmult_ac)
- thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
- by simp
- next
- assume bi1: "bv_to_int (utos w1) < 0"
- thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
- by (simp add: bv_to_int_utos)
- qed
+ from p
+ have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
+ by simp
+ thus ?thesis
+ proof (simp add: mult_less_0_iff,safe)
+ assume bi1: "0 < bv_to_int (utos w1)"
+ assume bi2: "bv_to_int w2 < 0"
+ have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
+ apply (rule mult_mono)
+ using bv_to_int_lower_range [of w2]
+ apply simp
+ apply (simp add: bv_to_int_utos)
+ using bv_to_nat_upper_range [of w1]
+ apply (simp add: int_nat_two_exp)
+ apply (rule zero_le_power,simp)
+ using bi1
+ apply simp
+ done
+ hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))"
+ by (simp add: zmult_ac)
+ thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
+ by simp
+ next
+ assume bi1: "bv_to_int (utos w1) < 0"
+ thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
+ by (simp add: bv_to_int_utos)
+ qed
qed
finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q"
- .
+ .
qed
qed
qed
@@ -2207,13 +2209,13 @@
subsection {* Structural operations *}
-constdefs
+definition
bv_select :: "[bit list,nat] => bit"
- "bv_select w i == w ! (length w - 1 - i)"
+ "bv_select w i = w ! (length w - 1 - i)"
bv_chop :: "[bit list,nat] => bit list * bit list"
- "bv_chop w i == let len = length w in (take (len - i) w,drop (len - i) w)"
+ "bv_chop w i = (let len = length w in (take (len - i) w,drop (len - i) w))"
bv_slice :: "[bit list,nat*nat] => bit list"
- "bv_slice w == \<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e)"
+ "bv_slice w = (\<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e))"
lemma bv_select_rev:
assumes notnull: "n < length w"
@@ -2230,36 +2232,36 @@
assume "xs = []"
with notx
show ?thesis
- by simp
+ by simp
next
fix y ys
assume [simp]: "xs = y # ys"
show ?thesis
proof (auto simp add: nth_append)
- assume noty: "n < length ys"
- from spec [OF ind,of ys]
- have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
- by simp
- hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
- ..
- hence "ys ! (length ys - Suc n) = rev ys ! n"
- ..
- thus "(y # ys) ! (length ys - n) = rev ys ! n"
- by (simp add: nth_Cons' noty linorder_not_less [symmetric])
+ assume noty: "n < length ys"
+ from spec [OF ind,of ys]
+ have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
+ by simp
+ hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
+ ..
+ hence "ys ! (length ys - Suc n) = rev ys ! n"
+ ..
+ thus "(y # ys) ! (length ys - n) = rev ys ! n"
+ by (simp add: nth_Cons' noty linorder_not_less [symmetric])
next
- assume "~ n < length ys"
- hence x: "length ys \<le> n"
- by simp
- from notx
- have "n < Suc (length ys)"
- by simp
- hence "n \<le> length ys"
- by simp
- with x
- have "length ys = n"
- by simp
- thus "y = [y] ! (n - length ys)"
- by simp
+ assume "~ n < length ys"
+ hence x: "length ys \<le> n"
+ by simp
+ from notx
+ have "n < Suc (length ys)"
+ by simp
+ hence "n \<le> length ys"
+ by simp
+ with x
+ have "length ys = n"
+ by simp
+ thus "y = [y] ! (n - length ys)"
+ by simp
qed
qed
qed
@@ -2284,9 +2286,9 @@
lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
by (auto simp add: bv_slice_def,arith)
-constdefs
+definition
length_nat :: "nat => nat"
- "length_nat x == LEAST n. x < 2 ^ n"
+ "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)
@@ -2316,9 +2318,12 @@
apply (simp_all add: n0)
done
-constdefs
+definition
length_int :: "int => nat"
- "length_int x == if 0 < x then Suc (length_nat (nat x)) else if x = 0 then 0 else Suc (length_nat (nat (-x - 1)))"
+ "length_int x =
+ (if 0 < x then Suc (length_nat (nat x))
+ else if x = 0 then 0
+ else Suc (length_nat (nat (-x - 1))))"
lemma length_int: "length (int_to_bv i) = length_int i"
proof (cases "0 < i")
@@ -2410,12 +2415,11 @@
shows "bv_slice w (j,i) = bv_slice (bv_slice w (l,k)) (j-k,i-k)"
proof -
def w1 == "fst (bv_chop w (Suc l))"
- def w2 == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
- def w3 == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
- def w4 == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
- def w5 == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
-
- note w_defs = w1_def w2_def w3_def w4_def w5_def
+ and w2 == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
+ and w3 == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
+ and w4 == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
+ and w5 == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
+ note w_defs = this
have w_def: "w = w1 @ w2 @ w3 @ w4 @ w5"
by (simp add: w_defs append_bv_chop_id)
@@ -2443,12 +2447,14 @@
apply (simp add: bv_extend_def)
apply (subst bv_to_nat_dist_append)
apply simp
- apply (induct "n - length w",simp_all)
+ apply (induct "n - length w")
+ apply simp_all
done
lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b"
apply (simp add: bv_extend_def)
- apply (induct "n - length w",simp_all)
+ apply (induct "n - length w")
+ apply simp_all
done
lemma bv_to_int_extend [simp]:
@@ -2632,18 +2638,21 @@
declare bv_to_nat1 [simp del]
declare bv_to_nat_helper [simp del]
-constdefs
+definition
bv_mapzip :: "[bit => bit => bit,bit list, bit list] => bit list"
- "bv_mapzip f w1 w2 == let g = bv_extend (max (length w1) (length w2)) \<zero>
- in map (split f) (zip (g w1) (g w2))"
+ "bv_mapzip f w1 w2 =
+ (let g = bv_extend (max (length w1) (length w2)) \<zero>
+ in map (split f) (zip (g w1) (g w2)))"
-lemma bv_length_bv_mapzip [simp]: "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
+lemma bv_length_bv_mapzip [simp]:
+ "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
by (simp add: bv_mapzip_def Let_def split: split_max)
lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"
by (simp add: bv_mapzip_def Let_def)
-lemma bv_mapzip_Cons [simp]: "length w1 = length w2 ==> bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
+lemma bv_mapzip_Cons [simp]: "length w1 = length w2 ==>
+ bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
by (simp add: bv_mapzip_def Let_def)
end
--- a/src/HOL/Library/Zorn.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Library/Zorn.thy Sat May 27 17:42:02 2006 +0200
@@ -15,24 +15,23 @@
\cite{Abrial-Laffitte}.
*}
-constdefs
+definition
chain :: "'a set set => 'a set set set"
- "chain S == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
+ "chain S = {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
super :: "['a set set,'a set set] => 'a set set set"
- "super S c == {d. d \<in> chain S & c \<subset> d}"
+ "super S c = {d. d \<in> chain S & c \<subset> d}"
maxchain :: "'a set set => 'a set set set"
- "maxchain S == {c. c \<in> chain S & super S c = {}}"
+ "maxchain S = {c. c \<in> chain S & super S c = {}}"
succ :: "['a set set,'a set set] => 'a set set"
- "succ S c ==
- if c \<notin> chain S | c \<in> maxchain S
- then c else SOME c'. c' \<in> super S c"
+ "succ S c =
+ (if c \<notin> chain S | c \<in> maxchain S
+ then c else SOME c'. c' \<in> super S c)"
consts
TFin :: "'a set set => 'a set set set"
-
inductive "TFin S"
intros
succI: "x \<in> TFin S ==> succ S x \<in> TFin S"
@@ -64,7 +63,7 @@
!!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
!!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
==> P(n)"
- apply (erule TFin.induct)
+ apply (induct set: TFin)
apply blast+
done
--- a/src/HOL/Real/HahnBanach/Bounds.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Sat May 27 17:42:02 2006 +0200
@@ -14,12 +14,12 @@
lemmas [elim?] = lub.least lub.upper
-constdefs
+definition
the_lub :: "'a::order set \<Rightarrow> 'a"
- "the_lub A \<equiv> The (lub A)"
+ "the_lub A = The (lub A)"
-syntax (xsymbols)
- the_lub :: "'a::order set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90)
+const_syntax (xsymbols)
+ the_lub ("\<Squnion>_" [90] 90)
lemma the_lub_equality [elim?]:
includes lub
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Sat May 27 17:42:02 2006 +0200
@@ -22,9 +22,9 @@
types 'a graph = "('a \<times> real) set"
-constdefs
+definition
graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph"
- "graph F f \<equiv> {(x, f x) | x. x \<in> F}"
+ "graph F f = {(x, f x) | x. x \<in> F}"
lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
by (unfold graph_def) blast
@@ -65,12 +65,12 @@
funct}.
*}
-constdefs
+definition
"domain" :: "'a graph \<Rightarrow> 'a set"
- "domain g \<equiv> {x. \<exists>y. (x, y) \<in> g}"
+ "domain g = {x. \<exists>y. (x, y) \<in> g}"
funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)"
- "funct g \<equiv> \<lambda>x. (SOME y. (x, y) \<in> g)"
+ "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
text {*
The following lemma states that @{text g} is the graph of a function
@@ -101,12 +101,12 @@
@{text p}, is defined as follows.
*}
-constdefs
+definition
norm_pres_extensions ::
"'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
\<Rightarrow> 'a graph set"
"norm_pres_extensions E p F f
- \<equiv> {g. \<exists>H h. g = graph H h
+ = {g. \<exists>H h. g = graph H h
\<and> linearform H h
\<and> H \<unlhd> E
\<and> F \<unlhd> H
--- a/src/HOL/Real/HahnBanach/Subspace.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Sat May 27 17:42:02 2006 +0200
@@ -22,10 +22,10 @@
and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
-declare vectorspace.intro [intro?] subspace.intro [intro?]
+const_syntax (symbols)
+ subspace (infix "\<unlhd>" 50)
-syntax (symbols)
- subspace :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infix "\<unlhd>" 50)
+declare vectorspace.intro [intro?] subspace.intro [intro?]
lemma subspace_subset [elim]: "U \<unlhd> V \<Longrightarrow> U \<subseteq> V"
by (rule subspace.subset)
@@ -130,9 +130,9 @@
scalar multiples of @{text x}.
*}
-constdefs
+definition
lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set"
- "lin x \<equiv> {a \<cdot> x | a. True}"
+ "lin x = {a \<cdot> x | a. True}"
lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x"
by (unfold lin_def) blast
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Sat May 27 17:42:02 2006 +0200
@@ -18,10 +18,10 @@
consts
prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70)
-syntax (xsymbols)
- prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
-syntax (HTML output)
- prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
+const_syntax (xsymbols)
+ prod (infixr "\<cdot>" 70)
+const_syntax (HTML output)
+ prod (infixr "\<cdot>" 70)
subsection {* Vector space laws *}
--- a/src/HOL/W0/W0.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/W0/W0.thy Sat May 27 17:42:02 2006 +0200
@@ -11,9 +11,9 @@
datatype 'a maybe = Ok 'a | Fail
-constdefs
+definition
bind :: "'a maybe \<Rightarrow> ('a \<Rightarrow> 'b maybe) \<Rightarrow> 'b maybe" (infixl "\<bind>" 60)
- "m \<bind> f \<equiv> case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail"
+ "m \<bind> f = (case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail)"
syntax
"_bind" :: "patterns \<Rightarrow> 'a maybe \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ := _;//_)" 0)
@@ -84,16 +84,16 @@
"free_tv [] = {}"
"free_tv (x # xs) = free_tv x \<union> free_tv xs"
-constdefs
+definition
dom :: "subst \<Rightarrow> nat set"
- "dom s \<equiv> {n. s n \<noteq> TVar n}"
+ "dom s = {n. s n \<noteq> TVar n}"
-- {* domain of a substitution *}
cod :: "subst \<Rightarrow> nat set"
- "cod s \<equiv> \<Union>m \<in> dom s. free_tv (s m)"
+ "cod s = (\<Union>m \<in> dom s. free_tv (s m))"
-- {* codomain of a substitutions: the introduced variables *}
-defs
+defs (overloaded)
free_tv_subst: "free_tv s \<equiv> dom s \<union> cod s"
text {*
@@ -102,16 +102,16 @@
than any type variable occuring in the type structure.
*}
-constdefs
+definition
new_tv :: "nat \<Rightarrow> 'a::type_struct \<Rightarrow> bool"
- "new_tv n ts \<equiv> \<forall>m. m \<in> free_tv ts \<longrightarrow> m < n"
+ "new_tv n ts = (\<forall>m. m \<in> free_tv ts \<longrightarrow> m < n)"
subsubsection {* Identity substitution *}
-constdefs
+definition
id_subst :: subst
- "id_subst \<equiv> \<lambda>n. TVar n"
+ "id_subst = (\<lambda>n. TVar n)"
lemma app_subst_id_te [simp]:
"$id_subst = (\<lambda>t::typ. t)"
@@ -218,35 +218,36 @@
by (induct x) simp_all
lemma subst_te_new_tv [simp]:
- "new_tv n (t::typ) \<longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
+ "new_tv n (t::typ) \<Longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
-- {* substitution affects only variables occurring freely *}
by (induct t) simp_all
lemma subst_tel_new_tv [simp]:
- "new_tv n (ts::typ list) \<longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
+ "new_tv n (ts::typ list) \<Longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
by (induct ts) simp_all
lemma new_tv_le: "n \<le> m \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv m t"
-- {* all greater variables are also new *}
proof (induct t)
case (TVar n)
- thus ?case by (auto intro: less_le_trans)
+ then show ?case by (auto intro: less_le_trans)
next
case TFun
- thus ?case by simp
+ then show ?case by simp
qed
lemma [simp]: "new_tv n t \<Longrightarrow> new_tv (Suc n) (t::typ)"
by (rule lessI [THEN less_imp_le [THEN new_tv_le]])
lemma new_tv_list_le:
- "n \<le> m \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
+ assumes "n \<le> m"
+ shows "new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
proof (induct ts)
case Nil
- thus ?case by simp
+ then show ?case by simp
next
case Cons
- thus ?case by (auto intro: new_tv_le)
+ with `n \<le> m` show ?case by (auto intro: new_tv_le)
qed
lemma [simp]: "new_tv n ts \<Longrightarrow> new_tv (Suc n) (ts::typ list)"
@@ -397,31 +398,27 @@
text {* Type assigment is closed wrt.\ substitution. *}
lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
-proof -
- assume "a |- e :: t"
- thus ?thesis (is "?P a e t")
- proof induct
- case (Var a n)
- hence "n < length (map ($ s) a)" by simp
- hence "map ($ s) a |- Var n :: map ($ s) a ! n"
- by (rule has_type.Var)
- also have "map ($ s) a ! n = $ s (a ! n)"
- by (rule nth_map)
- also have "map ($ s) a = $ s a"
- by (simp only: app_subst_list)
- finally show "?P a (Var n) (a ! n)" .
- next
- case (Abs a e t1 t2)
- hence "$ s t1 # map ($ s) a |- e :: $ s t2"
- by (simp add: app_subst_list)
- hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
- by (rule has_type.Abs)
- thus "?P a (Abs e) (t1 -> t2)"
- by (simp add: app_subst_list)
- next
- case App
- thus ?case by (simp add: has_type.App)
- qed
+proof (induct set: has_type)
+ case (Var a n)
+ then have "n < length (map ($ s) a)" by simp
+ then have "map ($ s) a |- Var n :: map ($ s) a ! n"
+ by (rule has_type.Var)
+ also have "map ($ s) a ! n = $ s (a ! n)"
+ by (rule nth_map)
+ also have "map ($ s) a = $ s a"
+ by (simp only: app_subst_list)
+ finally show ?case .
+next
+ case (Abs a e t1 t2)
+ then have "$ s t1 # map ($ s) a |- e :: $ s t2"
+ by (simp add: app_subst_list)
+ then have "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
+ by (rule has_type.Abs)
+ then show ?case
+ by (simp add: app_subst_list)
+next
+ case App
+ then show ?case by (simp add: has_type.App)
qed
@@ -442,52 +439,48 @@
u := mgu ($ s2 t1) (t2 -> TVar m2);
Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
-theorem W_correct: "!!a s t m n. Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
- (is "PROP ?P e")
-proof (induct e)
- fix a s t m n
- {
- fix i
- assume "Ok (s, t, m) = \<W> (Var i) a n"
- thus "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
- next
- fix e assume hyp: "PROP ?P e"
- assume "Ok (s, t, m) = \<W> (Abs e) a n"
- then obtain t' where "t = s n -> t'"
- and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
- by (auto split: bind_splits)
- with hyp show "$s a |- Abs e :: t"
- by (force intro: has_type.Abs)
- next
- fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
- assume "Ok (s, t, m) = \<W> (App e1 e2) a n"
- then obtain s1 t1 n1 s2 t2 n2 u where
+theorem W_correct: "Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
+proof (induct e fixing: a s t m n)
+ case (Var i)
+ from `Ok (s, t, m) = \<W> (Var i) a n`
+ show "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
+next
+ case (Abs e)
+ from `Ok (s, t, m) = \<W> (Abs e) a n`
+ obtain t' where "t = s n -> t'"
+ and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
+ by (auto split: bind_splits)
+ with Abs.hyps show "$s a |- Abs e :: t"
+ by (force intro: has_type.Abs)
+next
+ case (App e1 e2)
+ from `Ok (s, t, m) = \<W> (App e1 e2) a n`
+ obtain s1 t1 n1 s2 t2 n2 u where
s: "s = $u o $s2 o s1"
- and t: "t = u n2"
- and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
- and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
- and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
- by (auto split: bind_splits simp: that)
- show "$s a |- App e1 e2 :: t"
- proof (rule has_type.App)
- from s have s': "$u ($s2 ($s1 a)) = $s a"
- by (simp add: subst_comp_tel o_def)
- show "$s a |- e1 :: $u t2 -> t"
- proof -
- from W1_ok have "$s1 a |- e1 :: t1" by (rule hyp1)
- hence "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
- by (intro has_type_subst_closed)
- with s' t mgu_ok show ?thesis by simp
- qed
- show "$s a |- e2 :: $u t2"
- proof -
- from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule hyp2)
- hence "$u ($s2 ($s1 a)) |- e2 :: $u t2"
- by (rule has_type_subst_closed)
- with s' show ?thesis by simp
- qed
+ and t: "t = u n2"
+ and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
+ and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
+ and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
+ by (auto split: bind_splits simp: that)
+ show "$s a |- App e1 e2 :: t"
+ proof (rule has_type.App)
+ from s have s': "$u ($s2 ($s1 a)) = $s a"
+ by (simp add: subst_comp_tel o_def)
+ show "$s a |- e1 :: $u t2 -> t"
+ proof -
+ from W1_ok have "$s1 a |- e1 :: t1" by (rule App.hyps)
+ then have "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
+ by (intro has_type_subst_closed)
+ with s' t mgu_ok show ?thesis by simp
qed
- }
+ show "$s a |- e2 :: $u t2"
+ proof -
+ from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule App.hyps)
+ then have "$u ($s2 ($s1 a)) |- e2 :: $u t2"
+ by (rule has_type_subst_closed)
+ with s' show ?thesis by simp
+ qed
+ qed
qed
--- a/src/HOL/ex/Adder.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Adder.thy Sat May 27 17:42:02 2006 +0200
@@ -13,9 +13,9 @@
lemma bv_to_nat_helper': "bv \<noteq> [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)"
by (cases bv,simp_all add: bv_to_nat_helper)
-constdefs
+definition
half_adder :: "[bit,bit] => bit list"
- "half_adder a b == [a bitand b,a bitxor b]"
+ "half_adder a b = [a bitand b,a bitxor b]"
lemma half_adder_correct: "bv_to_nat (half_adder a b) = bitval a + bitval b"
apply (simp add: half_adder_def)
@@ -26,10 +26,10 @@
lemma [simp]: "length (half_adder a b) = 2"
by (simp add: half_adder_def)
-constdefs
+definition
full_adder :: "[bit,bit,bit] => bit list"
- "full_adder a b c ==
- let x = a bitxor b in [a bitand b bitor c bitand x,x bitxor c]"
+ "full_adder a b c =
+ (let x = a bitxor b in [a bitand b bitor c bitand x,x bitxor c])"
lemma full_adder_correct:
"bv_to_nat (full_adder a b c) = bitval a + bitval b + bitval c"
--- a/src/HOL/ex/Fundefs.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Fundefs.thy Sat May 27 17:42:02 2006 +0200
@@ -13,23 +13,23 @@
section {* Very basic *}
consts fib :: "nat \<Rightarrow> nat"
-function
+function
"fib 0 = 1"
"fib (Suc 0) = 1"
"fib (Suc (Suc n)) = fib n + fib (Suc n)"
-by pat_completeness (* shows that the patterns are complete *)
- auto (* shows that the patterns are compatible *)
+by pat_completeness -- {* shows that the patterns are complete *}
+ auto -- {* shows that the patterns are compatible *}
-(* we get partial simp and induction rules: *)
+text {* we get partial simp and induction rules: *}
thm fib.psimps
thm fib.pinduct
-(* There is also a cases rule to distinguish cases along the definition *)
+text {* There is also a cases rule to distinguish cases along the definition *}
thm fib.cases
-(* Now termination: *)
+text {* Now termination: *}
termination fib
- by (auto_term "less_than")
+ by (auto_term "less_than")
thm fib.simps
thm fib.induct
@@ -37,15 +37,15 @@
section {* Currying *}
-consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
function
"add 0 y = y"
"add (Suc x) y = Suc (add x y)"
by pat_completeness auto
-termination
+termination
by (auto_term "measure fst")
-thm add.induct (* Note the curried induction predicate *)
+thm add.induct -- {* Note the curried induction predicate *}
section {* Nested recursion *}
@@ -57,14 +57,14 @@
"nz (Suc x) = nz (nz x)"
by pat_completeness auto
-lemma nz_is_zero: (* A lemma we need to prove termination *)
+lemma nz_is_zero: -- {* A lemma we need to prove termination *}
assumes trm: "x \<in> nz_dom"
shows "nz x = 0"
using trm
by induct auto
termination nz
- apply (auto_term "less_than") (* Oops, it left us something to prove *)
+ apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
by (auto simp:nz_is_zero)
thm nz.simps
@@ -73,13 +73,12 @@
section {* More general patterns *}
-(* Currently, patterns must always be compatible with each other, since
+text {* Currently, patterns must always be compatible with each other, since
no automatich splitting takes place. But the following definition of
-gcd is ok, although patterns overlap: *)
-
+gcd is ok, although patterns overlap: *}
consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-function
+function
"gcd2 x 0 = x"
"gcd2 0 y = y"
"gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
@@ -91,17 +90,17 @@
thm gcd2.induct
-(* General patterns allow even strange definitions: *)
+text {* General patterns allow even strange definitions: *}
consts ev :: "nat \<Rightarrow> bool"
-function
+function
"ev (2 * n) = True"
"ev (2 * n + 1) = False"
-proof - (* completeness is more difficult here. . . *)
+proof - -- {* completeness is more difficult here \dots *}
assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto
show "P"
- proof cases
+ proof cases
assume "x mod 2 = 0"
with divmod have "x = 2 * (x div 2)" by simp
with c1 show "P" .
@@ -111,15 +110,11 @@
with divmod have "x = 2 * (x div 2) + 1" by simp
with c2 show "P" .
qed
-qed presburger+ (* solve compatibility with presburger *)
+qed presburger+ -- {* solve compatibility with presburger *}
termination by (auto_term "{}")
thm ev.simps
thm ev.induct
thm ev.cases
-
-
-
-
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/Higher_Order_Logic.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy Sat May 27 17:42:02 2006 +0200
@@ -79,7 +79,7 @@
subsubsection {* Derived connectives *}
-constdefs
+definition
false :: o ("\<bottom>")
"\<bottom> \<equiv> \<forall>A. A"
true :: o ("\<top>")
--- a/src/HOL/ex/InductiveInvariant.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/InductiveInvariant.thy Sat May 27 17:42:02 2006 +0200
@@ -14,14 +14,16 @@
text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
-constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
- "indinv r S F == \<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x)"
+definition
+ indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
+ "indinv r S F = (\<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x))"
text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."
-constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
- "indinv_on r D S F == \<forall>f. \<forall>x\<in>D. (\<forall>y\<in>D. (y,x) \<in> r --> S y (f y)) --> S x (F f x)"
+definition
+ indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
+ "indinv_on r D S F = (\<forall>f. \<forall>x\<in>D. (\<forall>y\<in>D. (y,x) \<in> r --> S y (f y)) --> S x (F f x))"
text "The key theorem, corresponding to theorem 1 of the paper. All other results
@@ -29,15 +31,16 @@
derived from this theorem."
theorem indinv_wfrec:
- assumes WF: "wf r" and
- INV: "indinv r S F"
+ assumes wf: "wf r" and
+ inv: "indinv r S F"
shows "S x (wfrec r F x)"
-proof (induct_tac x rule: wf_induct [OF WF])
+ using wf
+proof (induct x)
fix x
- assume IHYP: "\<forall>y. (y,x) \<in> r --> S y (wfrec r F y)"
- then have "\<forall>y. (y,x) \<in> r --> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
- with INV have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
- thus "S x (wfrec r F x)" using WF by (simp add: wfrec)
+ assume IHYP: "!!y. (y,x) \<in> r \<Longrightarrow> S y (wfrec r F y)"
+ then have "!!y. (y,x) \<in> r \<Longrightarrow> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
+ with inv have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
+ thus "S x (wfrec r F x)" using wf by (simp add: wfrec)
qed
theorem indinv_on_wfrec:
--- a/src/HOL/ex/Lagrange.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Lagrange.thy Sat May 27 17:42:02 2006 +0200
@@ -16,8 +16,9 @@
The enterprising reader might consider proving all of Lagrange's
theorem. *}
-constdefs sq :: "'a::times => 'a"
- "sq x == x*x"
+definition
+ sq :: "'a::times => 'a"
+ "sq x == x*x"
text {* The following lemma essentially shows that every natural
number is the sum of four squares, provided all prime numbers are.
@@ -26,7 +27,6 @@
ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]"
--- {* once a slow step, but now (2001) just three seconds! *}
lemma Lagrange_lemma:
"!!x1::'a::comm_ring.
(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
--- a/src/HOL/ex/MonoidGroup.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/MonoidGroup.thy Sat May 27 17:42:02 2006 +0200
@@ -14,17 +14,17 @@
record 'a group_sig = "'a monoid_sig" +
inv :: "'a => 'a"
-constdefs
+definition
monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"
- "monoid M == \<forall>x y z.
+ "monoid M = (\<forall>x y z.
times M (times M x y) z = times M x (times M y z) \<and>
- times M (one M) x = x \<and> times M x (one M) = x"
+ times M (one M) x = x \<and> times M x (one M) = x)"
group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool"
- "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"
+ "group G = (monoid G \<and> (\<forall>x. times G (inv G x) x = one G))"
reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
- "reverse M == M (| times := \<lambda>x y. times M y x |)"
+ "reverse M = M (| times := \<lambda>x y. times M y x |)"
end
--- a/src/HOL/ex/PER.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/PER.thy Sat May 27 17:42:02 2006 +0200
@@ -44,9 +44,9 @@
\emph{any} other one.
*}
-constdefs
- domain :: "'a::partial_equiv set"
- "domain == {x. x \<sim> x}"
+definition
+ "domain" :: "'a::partial_equiv set"
+ "domain = {x. x \<sim> x}"
lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
by (unfold domain_def) blast
@@ -164,9 +164,9 @@
representation of elements of a quotient type.
*}
-constdefs
+definition
eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>")
- "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
+ "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
proof (cases A)
@@ -231,9 +231,9 @@
subsection {* Picking representing elements *}
-constdefs
+definition
pick :: "'a::partial_equiv quot => 'a"
- "pick A == SOME a. A = \<lfloor>a\<rfloor>"
+ "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a"
proof (unfold pick_def)
--- a/src/HOL/ex/Primrec.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Primrec.thy Sat May 27 17:42:02 2006 +0200
@@ -42,24 +42,24 @@
text {* The set of primitive recursive functions of type @{typ "nat list => nat"}. *}
-constdefs
+definition
SC :: "nat list => nat"
- "SC l == Suc (zeroHd l)"
+ "SC l = Suc (zeroHd l)"
CONSTANT :: "nat => nat list => nat"
- "CONSTANT k l == k"
+ "CONSTANT k l = k"
PROJ :: "nat => nat list => nat"
- "PROJ i l == zeroHd (drop i l)"
+ "PROJ i l = zeroHd (drop i l)"
COMP :: "(nat list => nat) => (nat list => nat) list => nat list => nat"
- "COMP g fs l == g (map (\<lambda>f. f l) fs)"
+ "COMP g fs l = g (map (\<lambda>f. f l) fs)"
PREC :: "(nat list => nat) => (nat list => nat) => nat list => nat"
- "PREC f g l ==
- case l of
+ "PREC f g l =
+ (case l of
[] => 0
- | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x"
+ | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x)"
-- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *}
consts PRIMREC :: "(nat list => nat) set"
--- a/src/HOL/ex/Records.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Records.thy Sat May 27 17:42:02 2006 +0200
@@ -50,11 +50,11 @@
subsubsection {* Record selection and record update *}
-constdefs
+definition
getX :: "'a point_scheme => nat"
- "getX r == xpos r"
+ "getX r = xpos r"
setX :: "'a point_scheme => nat => 'a point_scheme"
- "setX r n == r (| xpos := n |)"
+ "setX r n = r (| xpos := n |)"
subsubsection {* Some lemmas about records *}
@@ -144,16 +144,16 @@
\medskip Concrete records are type instances of record schemes.
*}
-constdefs
+definition
foo5 :: nat
- "foo5 == getX (| xpos = 1, ypos = 0 |)"
+ "foo5 = getX (| xpos = 1, ypos = 0 |)"
text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *}
-constdefs
+definition
incX :: "'a point_scheme => 'a point_scheme"
- "incX r == (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
+ "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
lemma "incX r = setX r (Suc (getX r))"
by (simp add: getX_def setX_def incX_def)
@@ -161,9 +161,9 @@
text {* An alternative definition. *}
-constdefs
+definition
incX' :: "'a point_scheme => 'a point_scheme"
- "incX' r == r (| xpos := xpos r + 1 |)"
+ "incX' r = r (| xpos := xpos r + 1 |)"
subsection {* Coloured points: record extension *}
@@ -193,9 +193,9 @@
Functions on @{text point} schemes work for @{text cpoints} as well.
*}
-constdefs
+definition
foo10 :: nat
- "foo10 == getX (| xpos = 2, ypos = 0, colour = Blue |)"
+ "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
subsubsection {* Non-coercive structural subtyping *}
@@ -205,9 +205,9 @@
Great!
*}
-constdefs
+definition
foo11 :: cpoint
- "foo11 == setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
+ "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
subsection {* Other features *}
--- a/src/HOL/ex/Reflected_Presburger.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Sat May 27 17:42:02 2006 +0200
@@ -529,8 +529,9 @@
"islintn (n0, Add (Mult (Cst i) (Var n)) r) = (i \<noteq> 0 \<and> n0 \<le> n \<and> islintn (n+1,r))"
"islintn (n0, t) = False"
-constdefs islint :: "intterm \<Rightarrow> bool"
- "islint t \<equiv> islintn(0,t)"
+definition
+ islint :: "intterm \<Rightarrow> bool"
+ "islint t = islintn(0,t)"
(* And the equivalence to the first definition *)
lemma islinintterm_eq_islint: "islinintterm t = islint t"
@@ -728,8 +729,9 @@
by (induct l t rule: lin_mul.induct) simp_all
(* lin_neg neagtes a linear term *)
-constdefs lin_neg :: "intterm \<Rightarrow> intterm"
-"lin_neg i == lin_mul ((-1::int),i)"
+definition
+ lin_neg :: "intterm \<Rightarrow> intterm"
+ "lin_neg i = lin_mul ((-1::int),i)"
(* lin_neg has the semantics of Neg *)
lemma lin_neg_corr:
@@ -1622,11 +1624,13 @@
by simp
(* Definitions and lemmas about gcd and lcm *)
-constdefs lcm :: "nat \<times> nat \<Rightarrow> nat"
- "lcm \<equiv> (\<lambda>(m,n). m*n div gcd(m,n))"
-
-constdefs ilcm :: "int \<Rightarrow> int \<Rightarrow> int"
- "ilcm \<equiv> \<lambda>i.\<lambda>j. int (lcm(nat(abs i),nat(abs j)))"
+definition
+ lcm :: "nat \<times> nat \<Rightarrow> nat"
+ "lcm = (\<lambda>(m,n). m*n div gcd(m,n))"
+
+definition
+ ilcm :: "int \<Rightarrow> int \<Rightarrow> int"
+ "ilcm = (\<lambda>i.\<lambda>j. int (lcm(nat(abs i),nat(abs j))))"
(* ilcm_dvd12 are needed later *)
lemma lcm_dvd1:
@@ -1874,8 +1878,9 @@
(* unitycoeff expects a quantifier free formula an transforms it to an equivalent formula where the bound variable occurs only with coeffitient 1 or -1 *)
-constdefs unitycoeff :: "QF \<Rightarrow> QF"
- "unitycoeff p ==
+definition
+ unitycoeff :: "QF \<Rightarrow> QF"
+ "unitycoeff p =
(let l = formlcm p;
p' = adjustcoeff (l,p)
in (if l=1 then p' else
@@ -5085,8 +5090,9 @@
(* An implementation of sets trough lists *)
-constdefs list_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
- "list_insert x xs \<equiv> (if x mem xs then xs else x#xs)"
+definition
+ list_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ "list_insert x xs = (if x mem xs then xs else x#xs)"
lemma list_insert_set: "set (list_insert x xs) = set (x#xs)"
by(induct xs) (auto simp add: list_insert_def)
@@ -5362,8 +5368,8 @@
(* An implementation of cooper's method for both plus/minus/infinity *)
(* unify the formula *)
-constdefs unify:: "QF \<Rightarrow> (QF \<times> intterm list)"
- "unify p \<equiv>
+definition unify:: "QF \<Rightarrow> (QF \<times> intterm list)"
+ "unify p =
(let q = unitycoeff p;
B = list_set(bset q);
A = list_set (aset q)
@@ -5477,8 +5483,9 @@
using qB_def by simp
qed
(* An implementation of cooper's method *)
-constdefs cooper:: "QF \<Rightarrow> QF option"
-"cooper p \<equiv> lift_un (\<lambda>q. decrvars(explode_minf (unify q))) (linform (nnf p))"
+definition
+ cooper:: "QF \<Rightarrow> QF option"
+ "cooper p = lift_un (\<lambda>q. decrvars(explode_minf (unify q))) (linform (nnf p))"
(* cooper eliminates quantifiers *)
lemma cooper_qfree: "(\<And> q q'. \<lbrakk>isqfree q ; cooper q = Some q'\<rbrakk> \<Longrightarrow> isqfree q')"
@@ -5530,8 +5537,9 @@
qed
(* A decision procedure for Presburger Arithmetics *)
-constdefs pa:: "QF \<Rightarrow> QF option"
-"pa p \<equiv> lift_un psimpl (qelim(cooper, p))"
+definition
+ pa:: "QF \<Rightarrow> QF option"
+ "pa p \<equiv> lift_un psimpl (qelim(cooper, p))"
lemma psimpl_qfree: "isqfree p \<Longrightarrow> isqfree (psimpl p)"
apply(induct p rule: isqfree.induct)
--- a/src/HOL/ex/Sorting.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Sorting.thy Sat May 27 17:42:02 2006 +0200
@@ -24,12 +24,12 @@
"sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)"
-constdefs
+definition
total :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
- "total r == (\<forall>x y. r x y | r y x)"
+ "total r = (\<forall>x y. r x y | r y x)"
transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
- "transf f == (\<forall>x y z. f x y & f y z --> f x z)"
+ "transf f = (\<forall>x y z. f x y & f y z --> f x z)"
@@ -44,8 +44,8 @@
done
lemma sorted_append [simp]:
- "sorted le (xs@ys) =
- (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
-by (induct xs, auto)
+ "sorted le (xs@ys) =
+ (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
+ by (induct xs) auto
end
--- a/src/HOL/ex/Tarski.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/Tarski.thy Sat May 27 17:42:02 2006 +0200
@@ -20,79 +20,77 @@
pset :: "'a set"
order :: "('a * 'a) set"
-constdefs
+definition
monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
- "monotone f A r == \<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r"
+ "monotone f A r = (\<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r)"
least :: "['a => bool, 'a potype] => 'a"
- "least P po == @ x. x: pset po & P x &
- (\<forall>y \<in> pset po. P y --> (x,y): order po)"
+ "least P po = (SOME x. x: pset po & P x &
+ (\<forall>y \<in> pset po. P y --> (x,y): order po))"
greatest :: "['a => bool, 'a potype] => 'a"
- "greatest P po == @ x. x: pset po & P x &
- (\<forall>y \<in> pset po. P y --> (y,x): order po)"
+ "greatest P po = (SOME x. x: pset po & P x &
+ (\<forall>y \<in> pset po. P y --> (y,x): order po))"
lub :: "['a set, 'a potype] => 'a"
- "lub S po == least (%x. \<forall>y\<in>S. (y,x): order po) po"
+ "lub S po = least (%x. \<forall>y\<in>S. (y,x): order po) po"
glb :: "['a set, 'a potype] => 'a"
- "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
+ "glb S po = greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
isLub :: "['a set, 'a potype, 'a] => bool"
- "isLub S po == %L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
- (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po))"
+ "isLub S po = (%L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
+ (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po)))"
isGlb :: "['a set, 'a potype, 'a] => bool"
- "isGlb S po == %G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
- (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po))"
+ "isGlb S po = (%G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
+ (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po)))"
"fix" :: "[('a => 'a), 'a set] => 'a set"
- "fix f A == {x. x: A & f x = x}"
+ "fix f A = {x. x: A & f x = x}"
interval :: "[('a*'a) set,'a, 'a ] => 'a set"
- "interval r a b == {x. (a,x): r & (x,b): r}"
+ "interval r a b = {x. (a,x): r & (x,b): r}"
-constdefs
+definition
Bot :: "'a potype => 'a"
- "Bot po == least (%x. True) po"
+ "Bot po = least (%x. True) po"
Top :: "'a potype => 'a"
- "Top po == greatest (%x. True) po"
+ "Top po = greatest (%x. True) po"
PartialOrder :: "('a potype) set"
- "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) &
+ "PartialOrder = {P. refl (pset P) (order P) & antisym (order P) &
trans (order P)}"
CompleteLattice :: "('a potype) set"
- "CompleteLattice == {cl. cl: PartialOrder &
+ "CompleteLattice = {cl. cl: PartialOrder &
(\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) &
(\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}"
CLF :: "('a potype * ('a => 'a)) set"
- "CLF == SIGMA cl: CompleteLattice.
- {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)}"
+ "CLF = (SIGMA cl: CompleteLattice.
+ {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
- "induced A r == {(a,b). a : A & b: A & (a,b): r}"
+ "induced A r = {(a,b). a : A & b: A & (a,b): r}"
-constdefs
+definition
sublattice :: "('a potype * 'a set)set"
- "sublattice ==
- SIGMA cl: CompleteLattice.
+ "sublattice =
+ (SIGMA cl: CompleteLattice.
{S. S \<subseteq> pset cl &
- (| pset = S, order = induced S (order cl) |): CompleteLattice }"
+ (| pset = S, order = induced S (order cl) |): CompleteLattice})"
-syntax
- "@SL" :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
+abbreviation
+ sublat :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
+ "S <<= cl == S : sublattice `` {cl}"
-translations
- "S <<= cl" == "S : sublattice `` {cl}"
-
-constdefs
+definition
dual :: "'a potype => 'a potype"
- "dual po == (| pset = pset po, order = converse (order po) |)"
+ "dual po = (| pset = pset po, order = converse (order po) |)"
locale (open) PO =
fixes cl :: "'a potype"
--- a/src/HOL/ex/ThreeDivides.thy Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/ex/ThreeDivides.thy Sat May 27 17:42:02 2006 +0200
@@ -155,9 +155,9 @@
text {* The function @{text "sumdig"} returns the sum of all digits in
some number n. *}
-constdefs
+definition
sumdig :: "nat \<Rightarrow> nat"
- "sumdig n \<equiv> \<Sum>x < nlen n. n div 10^x mod 10"
+ "sumdig n = (\<Sum>x < nlen n. n div 10^x mod 10)"
text {* Some properties of these functions follow. *}