1.1 --- a/TFL/post.ML Sat May 27 17:42:00 2006 +0200
1.2 +++ b/TFL/post.ML Sat May 27 17:42:02 2006 +0200
1.3 @@ -156,7 +156,7 @@
1.4
1.5 (*lcp: curry the predicate of the induction rule*)
1.6 fun curry_rule rl =
1.7 - SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl)), rl);
1.8 + SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl;
1.9
1.10 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
1.11 val meta_outer =
2.1 --- a/src/HOL/Complex/ex/NSPrimes.thy Sat May 27 17:42:00 2006 +0200
2.2 +++ b/src/HOL/Complex/ex/NSPrimes.thy Sat May 27 17:42:02 2006 +0200
2.3 @@ -13,22 +13,15 @@
2.4 text{*These can be used to derive an alternative proof of the infinitude of
2.5 primes by considering a property of nonstandard sets.*}
2.6
2.7 +definition
2.8 + hdvd :: "[hypnat, hypnat] => bool" (infixl "hdvd" 50)
2.9 + [transfer_unfold]: "(M::hypnat) hdvd N = ( *p2* (op dvd)) M N"
2.10
2.11 -constdefs
2.12 - hdvd :: "[hypnat, hypnat] => bool" (infixl "hdvd" 50)
2.13 - "(M::hypnat) hdvd N == ( *p2* (op dvd)) M N"
2.14 + starprime :: "hypnat set"
2.15 + [transfer_unfold]: "starprime = ( *s* {p. prime p})"
2.16
2.17 -declare hdvd_def [transfer_unfold]
2.18 -
2.19 -constdefs
2.20 - starprime :: "hypnat set"
2.21 - "starprime == ( *s* {p. prime p})"
2.22 -
2.23 -declare starprime_def [transfer_unfold]
2.24 -
2.25 -constdefs
2.26 choicefun :: "'a set => 'a"
2.27 - "choicefun E == (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
2.28 + "choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
2.29
2.30 consts injf_max :: "nat => ('a::{order} set) => 'a"
2.31 primrec
3.1 --- a/src/HOL/Complex/ex/Sqrt_Script.thy Sat May 27 17:42:00 2006 +0200
3.2 +++ b/src/HOL/Complex/ex/Sqrt_Script.thy Sat May 27 17:42:02 2006 +0200
3.3 @@ -52,9 +52,9 @@
3.4
3.5 subsection {* The set of rational numbers *}
3.6
3.7 -constdefs
3.8 +definition
3.9 rationals :: "real set" ("\<rat>")
3.10 - "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
3.11 + "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
3.12
3.13
3.14 subsection {* Main theorem *}
4.1 --- a/src/HOL/Induct/Com.thy Sat May 27 17:42:00 2006 +0200
4.2 +++ b/src/HOL/Induct/Com.thy Sat May 27 17:42:02 2006 +0200
4.3 @@ -34,17 +34,14 @@
4.4
4.5 text{* Execution of commands *}
4.6 consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
4.7 -syntax "@exec" :: "((exp*state) * (nat*state)) set =>
4.8 - [com*state,state] => bool" ("_/ -[_]-> _" [50,0,50] 50)
4.9
4.10 -translations "csig -[eval]-> s" == "(csig,s) \<in> exec eval"
4.11 +abbreviation
4.12 + exec_rel ("_/ -[_]-> _" [50,0,50] 50)
4.13 + "csig -[eval]-> s == (csig,s) \<in> exec eval"
4.14
4.15 -syntax eval' :: "[exp*state,nat*state] =>
4.16 - ((exp*state) * (nat*state)) set => bool"
4.17 - ("_/ -|[_]-> _" [50,0,50] 50)
4.18 -
4.19 -translations
4.20 - "esig -|[eval]-> ns" => "(esig,ns) \<in> eval"
4.21 +abbreviation (input)
4.22 + generic_rel ("_/ -|[_]-> _" [50,0,50] 50)
4.23 + "esig -|[eval]-> ns == (esig,ns) \<in> eval"
4.24
4.25 text{*Command execution. Natural numbers represent Booleans: 0=True, 1=False*}
4.26 inductive "exec eval"
4.27 @@ -105,12 +102,12 @@
4.28 subsection {* Expressions *}
4.29
4.30 text{* Evaluation of arithmetic expressions *}
4.31 -consts eval :: "((exp*state) * (nat*state)) set"
4.32 - "-|->" :: "[exp*state,nat*state] => bool" (infixl 50)
4.33 +consts
4.34 + eval :: "((exp*state) * (nat*state)) set"
4.35
4.36 -translations
4.37 - "esig -|-> (n,s)" <= "(esig,n,s) \<in> eval"
4.38 - "esig -|-> ns" == "(esig,ns ) \<in> eval"
4.39 +abbreviation
4.40 + eval_rel :: "[exp*state,nat*state] => bool" (infixl "-|->" 50)
4.41 + "esig -|-> ns == (esig, ns) \<in> eval"
4.42
4.43 inductive eval
4.44 intros
5.1 --- a/src/HOL/Induct/Comb.thy Sat May 27 17:42:00 2006 +0200
5.2 +++ b/src/HOL/Induct/Comb.thy Sat May 27 17:42:02 2006 +0200
5.3 @@ -23,7 +23,11 @@
5.4
5.5 datatype comb = K
5.6 | S
5.7 - | "##" comb comb (infixl 90)
5.8 + | Ap comb comb (infixl "##" 90)
5.9 +
5.10 +const_syntax (xsymbols)
5.11 + Ap (infixl "\<bullet>" 90)
5.12 +
5.13
5.14 text {*
5.15 Inductive definition of contractions, @{text "-1->"} and
5.16 @@ -32,15 +36,12 @@
5.17
5.18 consts
5.19 contract :: "(comb*comb) set"
5.20 - "-1->" :: "[comb,comb] => bool" (infixl 50)
5.21 - "--->" :: "[comb,comb] => bool" (infixl 50)
5.22
5.23 -translations
5.24 - "x -1-> y" == "(x,y) \<in> contract"
5.25 - "x ---> y" == "(x,y) \<in> contract^*"
5.26 -
5.27 -syntax (xsymbols)
5.28 - "op ##" :: "[comb,comb] => comb" (infixl "\<bullet>" 90)
5.29 +abbreviation
5.30 + contract_rel1 :: "[comb,comb] => bool" (infixl "-1->" 50)
5.31 + "x -1-> y == (x,y) \<in> contract"
5.32 + contract_rel :: "[comb,comb] => bool" (infixl "--->" 50)
5.33 + "x ---> y == (x,y) \<in> contract^*"
5.34
5.35 inductive contract
5.36 intros
5.37 @@ -56,12 +57,12 @@
5.38
5.39 consts
5.40 parcontract :: "(comb*comb) set"
5.41 - "=1=>" :: "[comb,comb] => bool" (infixl 50)
5.42 - "===>" :: "[comb,comb] => bool" (infixl 50)
5.43
5.44 -translations
5.45 - "x =1=> y" == "(x,y) \<in> parcontract"
5.46 - "x ===> y" == "(x,y) \<in> parcontract^*"
5.47 +abbreviation
5.48 + parcontract_rel1 :: "[comb,comb] => bool" (infixl "=1=>" 50)
5.49 + "x =1=> y == (x,y) \<in> parcontract"
5.50 + parcontract_rel :: "[comb,comb] => bool" (infixl "===>" 50)
5.51 + "x ===> y == (x,y) \<in> parcontract^*"
5.52
5.53 inductive parcontract
5.54 intros
5.55 @@ -74,15 +75,15 @@
5.56 Misc definitions.
5.57 *}
5.58
5.59 -constdefs
5.60 +definition
5.61 I :: comb
5.62 - "I == S##K##K"
5.63 + "I = S##K##K"
5.64
5.65 diamond :: "('a * 'a)set => bool"
5.66 --{*confluence; Lambda/Commutation treats this more abstractly*}
5.67 - "diamond(r) == \<forall>x y. (x,y) \<in> r -->
5.68 + "diamond(r) = (\<forall>x y. (x,y) \<in> r -->
5.69 (\<forall>y'. (x,y') \<in> r -->
5.70 - (\<exists>z. (y,z) \<in> r & (y',z) \<in> r))"
5.71 + (\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))"
5.72
5.73
5.74 subsection {*Reflexive/Transitive closure preserves Church-Rosser property*}
6.1 --- a/src/HOL/Induct/LFilter.thy Sat May 27 17:42:00 2006 +0200
6.2 +++ b/src/HOL/Induct/LFilter.thy Sat May 27 17:42:02 2006 +0200
6.3 @@ -19,12 +19,12 @@
6.4
6.5 declare findRel.intros [intro]
6.6
6.7 -constdefs
6.8 +definition
6.9 find :: "['a => bool, 'a llist] => 'a llist"
6.10 - "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))"
6.11 + "find p l = (SOME l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p)))"
6.12
6.13 lfilter :: "['a => bool, 'a llist] => 'a llist"
6.14 - "lfilter p l == llist_corec l (%l. case find p l of
6.15 + "lfilter p l = llist_corec l (%l. case find p l of
6.16 LNil => None
6.17 | LCons y z => Some(y,z))"
6.18
7.1 --- a/src/HOL/Induct/LList.thy Sat May 27 17:42:00 2006 +0200
7.2 +++ b/src/HOL/Induct/LList.thy Sat May 27 17:42:02 2006 +0200
7.3 @@ -46,48 +46,48 @@
7.4 'a llist = "llist(range Leaf) :: 'a item set"
7.5 by (blast intro: llist.NIL_I)
7.6
7.7 -constdefs
7.8 +definition
7.9 list_Fun :: "['a item set, 'a item set] => 'a item set"
7.10 --{*Now used exclusively for abbreviating the coinduction rule*}
7.11 - "list_Fun A X == {z. z = NIL | (\<exists>M a. z = CONS a M & a \<in> A & M \<in> X)}"
7.12 + "list_Fun A X = {z. z = NIL | (\<exists>M a. z = CONS a M & a \<in> A & M \<in> X)}"
7.13
7.14 LListD_Fun ::
7.15 "[('a item * 'a item)set, ('a item * 'a item)set] =>
7.16 ('a item * 'a item)set"
7.17 - "LListD_Fun r X ==
7.18 + "LListD_Fun r X =
7.19 {z. z = (NIL, NIL) |
7.20 (\<exists>M N a b. z = (CONS a M, CONS b N) & (a, b) \<in> r & (M, N) \<in> X)}"
7.21
7.22 LNil :: "'a llist"
7.23 --{*abstract constructor*}
7.24 - "LNil == Abs_LList NIL"
7.25 + "LNil = Abs_LList NIL"
7.26
7.27 LCons :: "['a, 'a llist] => 'a llist"
7.28 --{*abstract constructor*}
7.29 - "LCons x xs == Abs_LList(CONS (Leaf x) (Rep_LList xs))"
7.30 + "LCons x xs = Abs_LList(CONS (Leaf x) (Rep_LList xs))"
7.31
7.32 llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
7.33 - "llist_case c d l ==
7.34 + "llist_case c d l =
7.35 List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)"
7.36
7.37 LList_corec_fun :: "[nat, 'a=> ('b item * 'a) option, 'a] => 'b item"
7.38 - "LList_corec_fun k f ==
7.39 + "LList_corec_fun k f ==
7.40 nat_rec (%x. {})
7.41 (%j r x. case f x of None => NIL
7.42 | Some(z,w) => CONS z (r w))
7.43 k"
7.44
7.45 LList_corec :: "['a, 'a => ('b item * 'a) option] => 'b item"
7.46 - "LList_corec a f == \<Union>k. LList_corec_fun k f a"
7.47 + "LList_corec a f = (\<Union>k. LList_corec_fun k f a)"
7.48
7.49 llist_corec :: "['a, 'a => ('b * 'a) option] => 'b llist"
7.50 - "llist_corec a f ==
7.51 + "llist_corec a f =
7.52 Abs_LList(LList_corec a
7.53 (%z. case f z of None => None
7.54 | Some(v,w) => Some(Leaf(v), w)))"
7.55
7.56 llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
7.57 - "llistD_Fun(r) ==
7.58 + "llistD_Fun(r) =
7.59 prod_fun Abs_LList Abs_LList `
7.60 LListD_Fun (diag(range Leaf))
7.61 (prod_fun Rep_LList Rep_LList ` r)"
7.62 @@ -101,27 +101,27 @@
7.63
7.64 subsubsection{* Sample function definitions. Item-based ones start with @{text L} *}
7.65
7.66 -constdefs
7.67 +definition
7.68 Lmap :: "('a item => 'b item) => ('a item => 'b item)"
7.69 - "Lmap f M == LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
7.70 + "Lmap f M = LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
7.71
7.72 lmap :: "('a=>'b) => ('a llist => 'b llist)"
7.73 - "lmap f l == llist_corec l (%z. case z of LNil => None
7.74 + "lmap f l = llist_corec l (%z. case z of LNil => None
7.75 | LCons y z => Some(f(y), z))"
7.76
7.77 iterates :: "['a => 'a, 'a] => 'a llist"
7.78 - "iterates f a == llist_corec a (%x. Some((x, f(x))))"
7.79 + "iterates f a = llist_corec a (%x. Some((x, f(x))))"
7.80
7.81 Lconst :: "'a item => 'a item"
7.82 "Lconst(M) == lfp(%N. CONS M N)"
7.83
7.84 Lappend :: "['a item, 'a item] => 'a item"
7.85 - "Lappend M N == LList_corec (M,N)
7.86 + "Lappend M N = LList_corec (M,N)
7.87 (split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2)))))
7.88 (%M1 M2 N. Some((M1, (M2,N))))))"
7.89
7.90 lappend :: "['a llist, 'a llist] => 'a llist"
7.91 - "lappend l n == llist_corec (l,n)
7.92 + "lappend l n = llist_corec (l,n)
7.93 (split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2)))))
7.94 (%l1 l2 n. Some((l1, (l2,n))))))"
7.95
7.96 @@ -198,6 +198,7 @@
7.97 declare LList_corec_fun_def [THEN def_nat_rec_0, simp]
7.98 LList_corec_fun_def [THEN def_nat_rec_Suc, simp]
7.99
7.100 +
7.101 subsubsection{* The directions of the equality are proved separately *}
7.102
7.103 lemma LList_corec_subset1:
7.104 @@ -226,7 +227,7 @@
7.105
7.106 text{*definitional version of same*}
7.107 lemma def_LList_corec:
7.108 - "[| !!x. h(x) == LList_corec x f |]
7.109 + "[| !!x. h(x) = LList_corec x f |]
7.110 ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))"
7.111 by (simp add: LList_corec)
7.112
7.113 @@ -652,7 +653,7 @@
7.114
7.115 text{*definitional version of same*}
7.116 lemma def_llist_corec:
7.117 - "[| !!x. h(x) == llist_corec x f |] ==>
7.118 + "[| !!x. h(x) = llist_corec x f |] ==>
7.119 h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))"
7.120 by (simp add: llist_corec)
7.121
8.1 --- a/src/HOL/Induct/Mutil.thy Sat May 27 17:42:00 2006 +0200
8.2 +++ b/src/HOL/Induct/Mutil.thy Sat May 27 17:42:02 2006 +0200
8.3 @@ -30,16 +30,15 @@
8.4
8.5 text {* \medskip Sets of squares of the given colour*}
8.6
8.7 -constdefs
8.8 +definition
8.9 coloured :: "nat => (nat \<times> nat) set"
8.10 - "coloured b == {(i, j). (i + j) mod 2 = b}"
8.11 + "coloured b = {(i, j). (i + j) mod 2 = b}"
8.12
8.13 -syntax whites :: "(nat \<times> nat) set"
8.14 - blacks :: "(nat \<times> nat) set"
8.15 -
8.16 -translations
8.17 - "whites" == "coloured 0"
8.18 - "blacks" == "coloured (Suc 0)"
8.19 +abbreviation
8.20 + whites :: "(nat \<times> nat) set"
8.21 + "whites == coloured 0"
8.22 + blacks :: "(nat \<times> nat) set"
8.23 + "blacks == coloured (Suc 0)"
8.24
8.25
8.26 text {* \medskip The union of two disjoint tilings is a tiling *}
9.1 --- a/src/HOL/Induct/Ordinals.thy Sat May 27 17:42:00 2006 +0200
9.2 +++ b/src/HOL/Induct/Ordinals.thy Sat May 27 17:42:02 2006 +0200
9.3 @@ -31,11 +31,11 @@
9.4 "iter f 0 = id"
9.5 "iter f (Suc n) = f \<circ> (iter f n)"
9.6
9.7 -constdefs
9.8 +definition
9.9 OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)"
9.10 - "OpLim F a == Limit (\<lambda>n. F n a)"
9.11 + "OpLim F a = Limit (\<lambda>n. F n a)"
9.12 OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)" ("\<Squnion>")
9.13 - "\<Squnion>f == OpLim (iter f)"
9.14 + "\<Squnion>f = OpLim (iter f)"
9.15
9.16 consts
9.17 cantor :: "ordinal => ordinal => ordinal"
9.18 @@ -51,9 +51,9 @@
9.19 "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
9.20 "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
9.21
9.22 -constdefs
9.23 +definition
9.24 deriv :: "(ordinal => ordinal) => (ordinal => ordinal)"
9.25 - "deriv f == \<nabla>(\<Squnion>f)"
9.26 + "deriv f = \<nabla>(\<Squnion>f)"
9.27
9.28 consts
9.29 veblen :: "ordinal => ordinal => ordinal"
9.30 @@ -62,9 +62,9 @@
9.31 "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
9.32 "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
9.33
9.34 -constdefs
9.35 - "veb a == veblen a Zero"
9.36 - "\<epsilon>\<^isub>0 == veb Zero"
9.37 - "\<Gamma>\<^isub>0 == Limit (\<lambda>n. iter veb n Zero)"
9.38 +definition
9.39 + "veb a = veblen a Zero"
9.40 + "\<epsilon>\<^isub>0 = veb Zero"
9.41 + "\<Gamma>\<^isub>0 = Limit (\<lambda>n. iter veb n Zero)"
9.42
9.43 end
10.1 --- a/src/HOL/Induct/PropLog.thy Sat May 27 17:42:00 2006 +0200
10.2 +++ b/src/HOL/Induct/PropLog.thy Sat May 27 17:42:02 2006 +0200
10.3 @@ -28,10 +28,10 @@
10.4
10.5 consts
10.6 thms :: "'a pl set => 'a pl set"
10.7 - "|-" :: "['a pl set, 'a pl] => bool" (infixl 50)
10.8
10.9 -translations
10.10 - "H |- p" == "p \<in> thms(H)"
10.11 +abbreviation
10.12 + thm_rel :: "['a pl set, 'a pl] => bool" (infixl "|-" 50)
10.13 + "H |- p == p \<in> thms H"
10.14
10.15 inductive "thms(H)"
10.16 intros
10.17 @@ -72,9 +72,9 @@
10.18 is @{text p}.
10.19 *}
10.20
10.21 -constdefs
10.22 +definition
10.23 sat :: "['a pl set, 'a pl] => bool" (infixl "|=" 50)
10.24 - "H |= p == (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
10.25 + "H |= p = (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
10.26
10.27
10.28 subsection {* Proof theory of propositional logic *}
11.1 --- a/src/HOL/Induct/QuoDataType.thy Sat May 27 17:42:00 2006 +0200
11.2 +++ b/src/HOL/Induct/QuoDataType.thy Sat May 27 17:42:02 2006 +0200
11.3 @@ -22,14 +22,14 @@
11.4 provided the keys are the same.*}
11.5 consts msgrel :: "(freemsg * freemsg) set"
11.6
11.7 -syntax
11.8 - "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "~~" 50)
11.9 -syntax (xsymbols)
11.10 - "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50)
11.11 -syntax (HTML output)
11.12 - "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50)
11.13 -translations
11.14 - "X \<sim> Y" == "(X,Y) \<in> msgrel"
11.15 +abbreviation
11.16 + msg_rel :: "[freemsg, freemsg] => bool" (infixl "~~" 50)
11.17 + "X ~~ Y == (X,Y) \<in> msgrel"
11.18 +
11.19 +const_syntax (xsymbols)
11.20 + msg_rel (infixl "\<sim>" 50)
11.21 +const_syntax (HTML output)
11.22 + msg_rel (infixl "\<sim>" 50)
11.23
11.24 text{*The first two rules are the desired equations. The next four rules
11.25 make the equations applicable to subterms. The last two rules are symmetry
11.26 @@ -142,20 +142,20 @@
11.27
11.28
11.29 text{*The abstract message constructors*}
11.30 -constdefs
11.31 +definition
11.32 Nonce :: "nat \<Rightarrow> msg"
11.33 - "Nonce N == Abs_Msg(msgrel``{NONCE N})"
11.34 + "Nonce N = Abs_Msg(msgrel``{NONCE N})"
11.35
11.36 MPair :: "[msg,msg] \<Rightarrow> msg"
11.37 - "MPair X Y ==
11.38 + "MPair X Y =
11.39 Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"
11.40
11.41 Crypt :: "[nat,msg] \<Rightarrow> msg"
11.42 - "Crypt K X ==
11.43 + "Crypt K X =
11.44 Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"
11.45
11.46 Decrypt :: "[nat,msg] \<Rightarrow> msg"
11.47 - "Decrypt K X ==
11.48 + "Decrypt K X =
11.49 Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
11.50
11.51
11.52 @@ -227,9 +227,9 @@
11.53
11.54 subsection{*The Abstract Function to Return the Set of Nonces*}
11.55
11.56 -constdefs
11.57 +definition
11.58 nonces :: "msg \<Rightarrow> nat set"
11.59 - "nonces X == \<Union>U \<in> Rep_Msg X. freenonces U"
11.60 + "nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"
11.61
11.62 lemma nonces_congruent: "freenonces respects msgrel"
11.63 by (simp add: congruent_def msgrel_imp_eq_freenonces)
11.64 @@ -262,9 +262,9 @@
11.65
11.66 subsection{*The Abstract Function to Return the Left Part*}
11.67
11.68 -constdefs
11.69 +definition
11.70 left :: "msg \<Rightarrow> msg"
11.71 - "left X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
11.72 + "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
11.73
11.74 lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
11.75 by (simp add: congruent_def msgrel_imp_eqv_freeleft)
11.76 @@ -296,9 +296,9 @@
11.77
11.78 subsection{*The Abstract Function to Return the Right Part*}
11.79
11.80 -constdefs
11.81 +definition
11.82 right :: "msg \<Rightarrow> msg"
11.83 - "right X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
11.84 + "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
11.85
11.86 lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
11.87 by (simp add: congruent_def msgrel_imp_eqv_freeright)
11.88 @@ -431,9 +431,9 @@
11.89 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
11.90 need this function in order to prove discrimination theorems.*}
11.91
11.92 -constdefs
11.93 +definition
11.94 discrim :: "msg \<Rightarrow> int"
11.95 - "discrim X == contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
11.96 + "discrim X = contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
11.97
11.98 lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
11.99 by (simp add: congruent_def msgrel_imp_eq_freediscrim)
12.1 --- a/src/HOL/Induct/QuoNestedDataType.thy Sat May 27 17:42:00 2006 +0200
12.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy Sat May 27 17:42:02 2006 +0200
12.3 @@ -20,14 +20,14 @@
12.4 text{*The equivalence relation, which makes PLUS associative.*}
12.5 consts exprel :: "(freeExp * freeExp) set"
12.6
12.7 -syntax
12.8 - "_exprel" :: "[freeExp, freeExp] => bool" (infixl "~~" 50)
12.9 -syntax (xsymbols)
12.10 - "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50)
12.11 -syntax (HTML output)
12.12 - "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50)
12.13 -translations
12.14 - "X \<sim> Y" == "(X,Y) \<in> exprel"
12.15 +abbreviation
12.16 + exp_rel :: "[freeExp, freeExp] => bool" (infixl "~~" 50)
12.17 + "X ~~ Y == (X,Y) \<in> exprel"
12.18 +
12.19 +const_syntax (xsymbols)
12.20 + exp_rel (infixl "\<sim>" 50)
12.21 +const_syntax (HTML output)
12.22 + exp_rel (infixl "\<sim>" 50)
12.23
12.24 text{*The first rule is the desired equation. The next three rules
12.25 make the equations applicable to subterms. The last two rules are symmetry
12.26 @@ -159,16 +159,16 @@
12.27
12.28 text{*The abstract message constructors*}
12.29
12.30 -constdefs
12.31 +definition
12.32 Var :: "nat \<Rightarrow> exp"
12.33 - "Var N == Abs_Exp(exprel``{VAR N})"
12.34 + "Var N = Abs_Exp(exprel``{VAR N})"
12.35
12.36 Plus :: "[exp,exp] \<Rightarrow> exp"
12.37 - "Plus X Y ==
12.38 + "Plus X Y =
12.39 Abs_Exp (\<Union>U \<in> Rep_Exp X. \<Union>V \<in> Rep_Exp Y. exprel``{PLUS U V})"
12.40
12.41 FnCall :: "[nat, exp list] \<Rightarrow> exp"
12.42 - "FnCall F Xs ==
12.43 + "FnCall F Xs =
12.44 Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})"
12.45
12.46
12.47 @@ -206,8 +206,9 @@
12.48 subsection{*Every list of abstract expressions can be expressed in terms of a
12.49 list of concrete expressions*}
12.50
12.51 -constdefs Abs_ExpList :: "freeExp list => exp list"
12.52 - "Abs_ExpList Xs == map (%U. Abs_Exp(exprel``{U})) Xs"
12.53 +definition
12.54 + Abs_ExpList :: "freeExp list => exp list"
12.55 + "Abs_ExpList Xs = map (%U. Abs_Exp(exprel``{U})) Xs"
12.56
12.57 lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] == []"
12.58 by (simp add: Abs_ExpList_def)
12.59 @@ -283,9 +284,9 @@
12.60
12.61 subsection{*The Abstract Function to Return the Set of Variables*}
12.62
12.63 -constdefs
12.64 +definition
12.65 vars :: "exp \<Rightarrow> nat set"
12.66 - "vars X == \<Union>U \<in> Rep_Exp X. freevars U"
12.67 + "vars X = (\<Union>U \<in> Rep_Exp X. freevars U)"
12.68
12.69 lemma vars_respects: "freevars respects exprel"
12.70 by (simp add: congruent_def exprel_imp_eq_freevars)
12.71 @@ -349,9 +350,9 @@
12.72
12.73 subsection{*Injectivity of @{term FnCall}*}
12.74
12.75 -constdefs
12.76 +definition
12.77 fun :: "exp \<Rightarrow> nat"
12.78 - "fun X == contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
12.79 + "fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
12.80
12.81 lemma fun_respects: "(%U. {freefun U}) respects exprel"
12.82 by (simp add: congruent_def exprel_imp_eq_freefun)
12.83 @@ -361,9 +362,9 @@
12.84 apply (simp add: FnCall fun_def UN_equiv_class [OF equiv_exprel fun_respects])
12.85 done
12.86
12.87 -constdefs
12.88 +definition
12.89 args :: "exp \<Rightarrow> exp list"
12.90 - "args X == contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
12.91 + "args X = contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
12.92
12.93 text{*This result can probably be generalized to arbitrary equivalence
12.94 relations, but with little benefit here.*}
12.95 @@ -396,9 +397,9 @@
12.96 text{*However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this
12.97 function in order to prove discrimination theorems.*}
12.98
12.99 -constdefs
12.100 +definition
12.101 discrim :: "exp \<Rightarrow> int"
12.102 - "discrim X == contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
12.103 + "discrim X = contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
12.104
12.105 lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
12.106 by (simp add: congruent_def exprel_imp_eq_freediscrim)
13.1 --- a/src/HOL/Induct/SList.thy Sat May 27 17:42:00 2006 +0200
13.2 +++ b/src/HOL/Induct/SList.thy Sat May 27 17:42:02 2006 +0200
13.3 @@ -36,12 +36,12 @@
13.4
13.5
13.6 (* Defining the Concrete Constructors *)
13.7 -constdefs
13.8 +definition
13.9 NIL :: "'a item"
13.10 - "NIL == In0(Numb(0))"
13.11 + "NIL = In0(Numb(0))"
13.12
13.13 CONS :: "['a item, 'a item] => 'a item"
13.14 - "CONS M N == In1(Scons M N)"
13.15 + "CONS M N = In1(Scons M N)"
13.16
13.17 consts
13.18 list :: "'a item set => 'a item set"
13.19 @@ -55,12 +55,12 @@
13.20 'a list = "list(range Leaf) :: 'a item set"
13.21 by (blast intro: list.NIL_I)
13.22
13.23 -constdefs
13.24 +definition
13.25 List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
13.26 - "List_case c d == Case(%x. c)(Split(d))"
13.27 + "List_case c d = Case(%x. c)(Split(d))"
13.28
13.29 List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
13.30 - "List_rec M c d == wfrec (trancl pred_sexp)
13.31 + "List_rec M c d = wfrec (trancl pred_sexp)
13.32 (%g. List_case c (%x y. d x y (g y))) M"
13.33
13.34
13.35 @@ -72,20 +72,20 @@
13.36
13.37 (*Declaring the abstract list constructors*)
13.38
13.39 -constdefs
13.40 +definition
13.41 Nil :: "'a list"
13.42 - "Nil == Abs_List(NIL)"
13.43 + "Nil = Abs_List(NIL)"
13.44
13.45 "Cons" :: "['a, 'a list] => 'a list" (infixr "#" 65)
13.46 - "x#xs == Abs_List(CONS (Leaf x)(Rep_List xs))"
13.47 + "x#xs = Abs_List(CONS (Leaf x)(Rep_List xs))"
13.48
13.49 (* list Recursion -- the trancl is Essential; see list.ML *)
13.50 list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
13.51 - "list_rec l c d ==
13.52 + "list_rec l c d =
13.53 List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
13.54
13.55 list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
13.56 - "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
13.57 + "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
13.58
13.59 (* list Enumeration *)
13.60 consts
13.61 @@ -110,83 +110,82 @@
13.62
13.63 (* Generalized Map Functionals *)
13.64
13.65 -constdefs
13.66 +definition
13.67 Rep_map :: "('b => 'a item) => ('b list => 'a item)"
13.68 - "Rep_map f xs == list_rec xs NIL(%x l r. CONS(f x) r)"
13.69 + "Rep_map f xs = list_rec xs NIL(%x l r. CONS(f x) r)"
13.70
13.71 Abs_map :: "('a item => 'b) => 'a item => 'b list"
13.72 - "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
13.73 + "Abs_map g M = List_rec M Nil (%N L r. g(N)#r)"
13.74
13.75
13.76 (**** Function definitions ****)
13.77
13.78 -constdefs
13.79 +definition
13.80
13.81 null :: "'a list => bool"
13.82 - "null xs == list_rec xs True (%x xs r. False)"
13.83 + "null xs = list_rec xs True (%x xs r. False)"
13.84
13.85 hd :: "'a list => 'a"
13.86 - "hd xs == list_rec xs (@x. True) (%x xs r. x)"
13.87 + "hd xs = list_rec xs (@x. True) (%x xs r. x)"
13.88
13.89 tl :: "'a list => 'a list"
13.90 - "tl xs == list_rec xs (@xs. True) (%x xs r. xs)"
13.91 + "tl xs = list_rec xs (@xs. True) (%x xs r. xs)"
13.92
13.93 (* a total version of tl: *)
13.94 ttl :: "'a list => 'a list"
13.95 - "ttl xs == list_rec xs [] (%x xs r. xs)"
13.96 + "ttl xs = list_rec xs [] (%x xs r. xs)"
13.97
13.98 member :: "['a, 'a list] => bool" (infixl "mem" 55)
13.99 - "x mem xs == list_rec xs False (%y ys r. if y=x then True else r)"
13.100 + "x mem xs = list_rec xs False (%y ys r. if y=x then True else r)"
13.101
13.102 list_all :: "('a => bool) => ('a list => bool)"
13.103 - "list_all P xs == list_rec xs True(%x l r. P(x) & r)"
13.104 + "list_all P xs = list_rec xs True(%x l r. P(x) & r)"
13.105
13.106 map :: "('a=>'b) => ('a list => 'b list)"
13.107 - "map f xs == list_rec xs [] (%x l r. f(x)#r)"
13.108 + "map f xs = list_rec xs [] (%x l r. f(x)#r)"
13.109
13.110
13.111 -constdefs
13.112 append :: "['a list, 'a list] => 'a list" (infixr "@" 65)
13.113 - "xs@ys == list_rec xs ys (%x l r. x#r)"
13.114 + "xs@ys = list_rec xs ys (%x l r. x#r)"
13.115
13.116 filter :: "['a => bool, 'a list] => 'a list"
13.117 - "filter P xs == list_rec xs [] (%x xs r. if P(x)then x#r else r)"
13.118 + "filter P xs = list_rec xs [] (%x xs r. if P(x)then x#r else r)"
13.119
13.120 foldl :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
13.121 - "foldl f a xs == list_rec xs (%a. a)(%x xs r.%a. r(f a x))(a)"
13.122 + "foldl f a xs = list_rec xs (%a. a)(%x xs r.%a. r(f a x))(a)"
13.123
13.124 foldr :: "[['a,'b] => 'b, 'b, 'a list] => 'b"
13.125 - "foldr f a xs == list_rec xs a (%x xs r. (f x r))"
13.126 + "foldr f a xs = list_rec xs a (%x xs r. (f x r))"
13.127
13.128 length :: "'a list => nat"
13.129 - "length xs== list_rec xs 0 (%x xs r. Suc r)"
13.130 + "length xs = list_rec xs 0 (%x xs r. Suc r)"
13.131
13.132 drop :: "['a list,nat] => 'a list"
13.133 - "drop t n == (nat_rec(%x. x)(%m r xs. r(ttl xs)))(n)(t)"
13.134 + "drop t n = (nat_rec(%x. x)(%m r xs. r(ttl xs)))(n)(t)"
13.135
13.136 copy :: "['a, nat] => 'a list" (* make list of n copies of x *)
13.137 - "copy t == nat_rec [] (%m xs. t # xs)"
13.138 + "copy t = nat_rec [] (%m xs. t # xs)"
13.139
13.140 flat :: "'a list list => 'a list"
13.141 - "flat == foldr (op @) []"
13.142 + "flat = foldr (op @) []"
13.143
13.144 nth :: "[nat, 'a list] => 'a"
13.145 - "nth == nat_rec hd (%m r xs. r(tl xs))"
13.146 + "nth = nat_rec hd (%m r xs. r(tl xs))"
13.147
13.148 rev :: "'a list => 'a list"
13.149 - "rev xs == list_rec xs [] (%x xs xsa. xsa @ [x])"
13.150 + "rev xs = list_rec xs [] (%x xs xsa. xsa @ [x])"
13.151
13.152 (* miscellaneous definitions *)
13.153 zipWith :: "['a * 'b => 'c, 'a list * 'b list] => 'c list"
13.154 - "zipWith f S == (list_rec (fst S) (%T.[])
13.155 + "zipWith f S = (list_rec (fst S) (%T.[])
13.156 (%x xs r. %T. if null T then []
13.157 else f(x,hd T) # r(tl T)))(snd(S))"
13.158
13.159 zip :: "'a list * 'b list => ('a*'b) list"
13.160 - "zip == zipWith (%s. s)"
13.161 + "zip = zipWith (%s. s)"
13.162
13.163 unzip :: "('a*'b) list => ('a list * 'b list)"
13.164 - "unzip == foldr(% (a,b)(c,d).(a#c,b#d))([],[])"
13.165 + "unzip = foldr(% (a,b)(c,d).(a#c,b#d))([],[])"
13.166
13.167
13.168 consts take :: "['a list,nat] => 'a list"
13.169 @@ -425,9 +424,9 @@
13.170 "[| M: sexp; N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N"
13.171 by (simp add: Abs_map_def)
13.172
13.173 -(*Eases the use of primitive recursion. NOTE USE OF == *)
13.174 +(*Eases the use of primitive recursion.*)
13.175 lemma def_list_rec_NilCons:
13.176 - "[| !!xs. f(xs) == list_rec xs c h |]
13.177 + "[| !!xs. f(xs) = list_rec xs c h |]
13.178 ==> f [] = c & f(x#xs) = h x xs (f xs)"
13.179 by simp
13.180
13.181 @@ -475,11 +474,11 @@
13.182 (** nth **)
13.183
13.184 lemma def_nat_rec_0_eta:
13.185 - "[| !!n. f == nat_rec c h |] ==> f(0) = c"
13.186 + "[| !!n. f = nat_rec c h |] ==> f(0) = c"
13.187 by simp
13.188
13.189 lemma def_nat_rec_Suc_eta:
13.190 - "[| !!n. f == nat_rec c h |] ==> f(Suc(n)) = h n (f n)"
13.191 + "[| !!n. f = nat_rec c h |] ==> f(Suc(n)) = h n (f n)"
13.192 by simp
13.193
13.194 declare def_nat_rec_0_eta [OF nth_def, simp]
14.1 --- a/src/HOL/Induct/Sexp.thy Sat May 27 17:42:00 2006 +0200
14.2 +++ b/src/HOL/Induct/Sexp.thy Sat May 27 17:42:02 2006 +0200
14.3 @@ -17,20 +17,20 @@
14.4 NumbI: "Numb(i) \<in> sexp"
14.5 SconsI: "[| M \<in> sexp; N \<in> sexp |] ==> Scons M N \<in> sexp"
14.6
14.7 -constdefs
14.8 +definition
14.9
14.10 sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b,
14.11 'a item] => 'b"
14.12 - "sexp_case c d e M == THE z. (EX x. M=Leaf(x) & z=c(x))
14.13 + "sexp_case c d e M = (THE z. (EX x. M=Leaf(x) & z=c(x))
14.14 | (EX k. M=Numb(k) & z=d(k))
14.15 - | (EX N1 N2. M = Scons N1 N2 & z=e N1 N2)"
14.16 + | (EX N1 N2. M = Scons N1 N2 & z=e N1 N2))"
14.17
14.18 pred_sexp :: "('a item * 'a item)set"
14.19 - "pred_sexp == \<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)}"
14.20 + "pred_sexp = (\<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)})"
14.21
14.22 sexp_rec :: "['a item, 'a=>'b, nat=>'b,
14.23 ['a item, 'a item, 'b, 'b]=>'b] => 'b"
14.24 - "sexp_rec M c d e == wfrec pred_sexp
14.25 + "sexp_rec M c d e = wfrec pred_sexp
14.26 (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
14.27
14.28
15.1 --- a/src/HOL/Induct/Tree.thy Sat May 27 17:42:00 2006 +0200
15.2 +++ b/src/HOL/Induct/Tree.thy Sat May 27 17:42:02 2006 +0200
15.3 @@ -71,12 +71,12 @@
15.4 ordinals. Start with a predecessor relation and form its transitive
15.5 closure. *}
15.6
15.7 -constdefs
15.8 +definition
15.9 brouwer_pred :: "(brouwer * brouwer) set"
15.10 - "brouwer_pred == \<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)}"
15.11 + "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
15.12
15.13 brouwer_order :: "(brouwer * brouwer) set"
15.14 - "brouwer_order == brouwer_pred^+"
15.15 + "brouwer_order = brouwer_pred^+"
15.16
15.17 lemma wf_brouwer_pred: "wf brouwer_pred"
15.18 by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
16.1 --- a/src/HOL/Lattice/Bounds.thy Sat May 27 17:42:00 2006 +0200
16.2 +++ b/src/HOL/Lattice/Bounds.thy Sat May 27 17:42:02 2006 +0200
16.3 @@ -15,18 +15,18 @@
16.4 number of elements.
16.5 *}
16.6
16.7 -constdefs
16.8 +definition
16.9 is_inf :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
16.10 - "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)"
16.11 + "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))"
16.12
16.13 is_sup :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
16.14 - "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)"
16.15 + "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))"
16.16
16.17 is_Inf :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
16.18 - "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)"
16.19 + "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))"
16.20
16.21 is_Sup :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
16.22 - "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)"
16.23 + "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))"
16.24
16.25 text {*
16.26 These definitions entail the following basic properties of boundary
17.1 --- a/src/HOL/Lattice/CompleteLattice.thy Sat May 27 17:42:00 2006 +0200
17.2 +++ b/src/HOL/Lattice/CompleteLattice.thy Sat May 27 17:42:02 2006 +0200
17.3 @@ -31,15 +31,15 @@
17.4 such infimum and supremum elements.
17.5 *}
17.6
17.7 -consts
17.8 +definition
17.9 Meet :: "'a::complete_lattice set \<Rightarrow> 'a"
17.10 + "Meet A = (THE inf. is_Inf A inf)"
17.11 Join :: "'a::complete_lattice set \<Rightarrow> 'a"
17.12 -syntax (xsymbols)
17.13 - Meet :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90)
17.14 - Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90)
17.15 -defs
17.16 - Meet_def: "\<Sqinter>A \<equiv> THE inf. is_Inf A inf"
17.17 - Join_def: "\<Squnion>A \<equiv> THE sup. is_Sup A sup"
17.18 + "Join A = (THE sup. is_Sup A sup)"
17.19 +
17.20 +const_syntax (xsymbols)
17.21 + Meet ("\<Sqinter>_" [90] 90)
17.22 + Join ("\<Squnion>_" [90] 90)
17.23
17.24 text {*
17.25 Due to unique existence of bounds, the complete lattice operations
17.26 @@ -142,11 +142,11 @@
17.27 greatest elements.
17.28 *}
17.29
17.30 -constdefs
17.31 +definition
17.32 bottom :: "'a::complete_lattice" ("\<bottom>")
17.33 - "\<bottom> \<equiv> \<Sqinter>UNIV"
17.34 + "\<bottom> = \<Sqinter>UNIV"
17.35 top :: "'a::complete_lattice" ("\<top>")
17.36 - "\<top> \<equiv> \<Squnion>UNIV"
17.37 + "\<top> = \<Squnion>UNIV"
17.38
17.39 lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
17.40 proof (unfold bottom_def)
18.1 --- a/src/HOL/Lattice/Lattice.thy Sat May 27 17:42:00 2006 +0200
18.2 +++ b/src/HOL/Lattice/Lattice.thy Sat May 27 17:42:02 2006 +0200
18.3 @@ -24,15 +24,15 @@
18.4 infimum and supremum elements.
18.5 *}
18.6
18.7 -consts
18.8 +definition
18.9 meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "&&" 70)
18.10 + "x && y = (THE inf. is_inf x y inf)"
18.11 join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "||" 65)
18.12 -syntax (xsymbols)
18.13 - meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
18.14 - join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
18.15 -defs
18.16 - meet_def: "x && y \<equiv> THE inf. is_inf x y inf"
18.17 - join_def: "x || y \<equiv> THE sup. is_sup x y sup"
18.18 + "x || y = (THE sup. is_sup x y sup)"
18.19 +
18.20 +const_syntax (xsymbols)
18.21 + meet (infixl "\<sqinter>" 70)
18.22 + join (infixl "\<squnion>" 65)
18.23
18.24 text {*
18.25 Due to unique existence of bounds, the lattice operations may be
18.26 @@ -336,11 +336,11 @@
18.27 are a (degenerate) example of lattice structures.
18.28 *}
18.29
18.30 -constdefs
18.31 +definition
18.32 minimum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
18.33 - "minimum x y \<equiv> (if x \<sqsubseteq> y then x else y)"
18.34 + "minimum x y = (if x \<sqsubseteq> y then x else y)"
18.35 maximum :: "'a::linear_order \<Rightarrow> 'a \<Rightarrow> 'a"
18.36 - "maximum x y \<equiv> (if x \<sqsubseteq> y then y else x)"
18.37 + "maximum x y = (if x \<sqsubseteq> y then y else x)"
18.38
18.39 lemma is_inf_minimum: "is_inf x y (minimum x y)"
18.40 proof
19.1 --- a/src/HOL/Lattice/Orders.thy Sat May 27 17:42:00 2006 +0200
19.2 +++ b/src/HOL/Lattice/Orders.thy Sat May 27 17:42:02 2006 +0200
19.3 @@ -21,8 +21,8 @@
19.4 axclass leq < type
19.5 consts
19.6 leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool" (infixl "[=" 50)
19.7 -syntax (xsymbols)
19.8 - leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
19.9 +const_syntax (xsymbols)
19.10 + leq (infixl "\<sqsubseteq>" 50)
19.11
19.12 axclass quasi_order < leq
19.13 leq_refl [intro?]: "x \<sqsubseteq> x"
20.1 --- a/src/HOL/Library/BigO.thy Sat May 27 17:42:00 2006 +0200
20.2 +++ b/src/HOL/Library/BigO.thy Sat May 27 17:42:02 2006 +0200
20.3 @@ -38,10 +38,9 @@
20.4
20.5 subsection {* Definitions *}
20.6
20.7 -constdefs
20.8 -
20.9 +definition
20.10 bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set" ("(1O'(_'))")
20.11 - "O(f::('a => 'b)) ==
20.12 + "O(f::('a => 'b)) =
20.13 {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
20.14
20.15 lemma bigo_pos_const: "(EX (c::'a::ordered_idom).
20.16 @@ -735,10 +734,10 @@
20.17
20.18 subsection {* Less than or equal to *}
20.19
20.20 -constdefs
20.21 +definition
20.22 lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
20.23 (infixl "<o" 70)
20.24 - "f <o g == (%x. max (f x - g x) 0)"
20.25 + "f <o g = (%x. max (f x - g x) 0)"
20.26
20.27 lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
20.28 g =o O(h)"
21.1 --- a/src/HOL/Library/Char_ord.thy Sat May 27 17:42:00 2006 +0200
21.2 +++ b/src/HOL/Library/Char_ord.thy Sat May 27 17:42:02 2006 +0200
21.3 @@ -13,8 +13,6 @@
21.4
21.5 consts
21.6 nibble_to_int:: "nibble \<Rightarrow> int"
21.7 - int_to_nibble:: "int \<Rightarrow> nibble"
21.8 -
21.9 primrec
21.10 "nibble_to_int Nibble0 = 0"
21.11 "nibble_to_int Nibble1 = 1"
21.12 @@ -33,25 +31,25 @@
21.13 "nibble_to_int NibbleE = 14"
21.14 "nibble_to_int NibbleF = 15"
21.15
21.16 -defs
21.17 - int_to_nibble_def:
21.18 - "int_to_nibble x \<equiv> (let y = x mod 16 in
21.19 - if y = 0 then Nibble0 else
21.20 - if y = 1 then Nibble1 else
21.21 - if y = 2 then Nibble2 else
21.22 - if y = 3 then Nibble3 else
21.23 - if y = 4 then Nibble4 else
21.24 - if y = 5 then Nibble5 else
21.25 - if y = 6 then Nibble6 else
21.26 - if y = 7 then Nibble7 else
21.27 - if y = 8 then Nibble8 else
21.28 - if y = 9 then Nibble9 else
21.29 - if y = 10 then NibbleA else
21.30 - if y = 11 then NibbleB else
21.31 - if y = 12 then NibbleC else
21.32 - if y = 13 then NibbleD else
21.33 - if y = 14 then NibbleE else
21.34 - NibbleF)"
21.35 +definition
21.36 + int_to_nibble :: "int \<Rightarrow> nibble"
21.37 + "int_to_nibble x \<equiv> (let y = x mod 16 in
21.38 + if y = 0 then Nibble0 else
21.39 + if y = 1 then Nibble1 else
21.40 + if y = 2 then Nibble2 else
21.41 + if y = 3 then Nibble3 else
21.42 + if y = 4 then Nibble4 else
21.43 + if y = 5 then Nibble5 else
21.44 + if y = 6 then Nibble6 else
21.45 + if y = 7 then Nibble7 else
21.46 + if y = 8 then Nibble8 else
21.47 + if y = 9 then Nibble9 else
21.48 + if y = 10 then NibbleA else
21.49 + if y = 11 then NibbleB else
21.50 + if y = 12 then NibbleC else
21.51 + if y = 13 then NibbleD else
21.52 + if y = 14 then NibbleE else
21.53 + NibbleF)"
21.54
21.55 lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x"
21.56 by (cases x) (auto simp: int_to_nibble_def Let_def)
21.57 @@ -93,15 +91,9 @@
21.58 lemmas char_ord_defs = char_less_def char_le_def
21.59
21.60 instance char :: order
21.61 - apply intro_classes
21.62 - apply (unfold char_ord_defs)
21.63 - apply (auto simp: char_to_int_pair_eq order_less_le)
21.64 - done
21.65 + by default (auto simp: char_ord_defs char_to_int_pair_eq order_less_le)
21.66
21.67 -instance char::linorder
21.68 - apply intro_classes
21.69 - apply (unfold char_le_def)
21.70 - apply auto
21.71 - done
21.72 +instance char :: linorder
21.73 + by default (auto simp: char_le_def)
21.74
21.75 end
22.1 --- a/src/HOL/Library/Commutative_Ring.thy Sat May 27 17:42:00 2006 +0200
22.2 +++ b/src/HOL/Library/Commutative_Ring.thy Sat May 27 17:42:02 2006 +0200
22.3 @@ -47,16 +47,16 @@
22.4
22.5 text {* Create polynomial normalized polynomials given normalized inputs. *}
22.6
22.7 -constdefs
22.8 +definition
22.9 mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
22.10 - "mkPinj x P \<equiv> (case P of
22.11 + "mkPinj x P = (case P of
22.12 Pc c \<Rightarrow> Pc c |
22.13 Pinj y P \<Rightarrow> Pinj (x + y) P |
22.14 PX p1 y p2 \<Rightarrow> Pinj x P)"
22.15
22.16 -constdefs
22.17 +definition
22.18 mkPX :: "'a::{comm_ring,recpower} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
22.19 - "mkPX P i Q == (case P of
22.20 + "mkPX P i Q = (case P of
22.21 Pc c \<Rightarrow> (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) |
22.22 Pinj j R \<Rightarrow> PX P i Q |
22.23 PX P2 i2 Q2 \<Rightarrow> (if (Q2 = (Pc 0)) then (PX P2 (i+i2) Q) else (PX P i Q)) )"
22.24 @@ -127,9 +127,9 @@
22.25 "neg (PX P x Q) = PX (neg P) x (neg Q)"
22.26
22.27 text {* Substraction *}
22.28 -constdefs
22.29 +definition
22.30 sub :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
22.31 - "sub p q \<equiv> add (p, neg q)"
22.32 + "sub p q = add (p, neg q)"
22.33
22.34 text {* Square for Fast Exponentation *}
22.35 primrec
22.36 @@ -316,11 +316,6 @@
22.37 qed
22.38
22.39
22.40 -text {* Code generation *}
22.41 -(*
22.42 -Does not work, since no generic ring operations implementation is there
22.43 -generate_code ("ring.ML") test = "norm"*)
22.44 -
22.45 use "comm_ring.ML"
22.46 setup CommRing.setup
22.47
23.1 --- a/src/HOL/Library/Continuity.thy Sat May 27 17:42:00 2006 +0200
23.2 +++ b/src/HOL/Library/Continuity.thy Sat May 27 17:42:02 2006 +0200
23.3 @@ -11,9 +11,9 @@
23.4
23.5 subsection "Chains"
23.6
23.7 -constdefs
23.8 +definition
23.9 up_chain :: "(nat => 'a set) => bool"
23.10 - "up_chain F == \<forall>i. F i \<subseteq> F (Suc i)"
23.11 + "up_chain F = (\<forall>i. F i \<subseteq> F (Suc i))"
23.12
23.13 lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
23.14 by (simp add: up_chain_def)
23.15 @@ -21,10 +21,10 @@
23.16 lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)"
23.17 by (simp add: up_chain_def)
23.18
23.19 -lemma up_chain_less_mono [rule_format]:
23.20 - "up_chain F ==> x < y --> F x \<subseteq> F y"
23.21 - apply (induct_tac y)
23.22 - apply (blast dest: up_chainD elim: less_SucE)+
23.23 +lemma up_chain_less_mono:
23.24 + "up_chain F ==> x < y ==> F x \<subseteq> F y"
23.25 + apply (induct y)
23.26 + apply (blast dest: up_chainD elim: less_SucE)+
23.27 done
23.28
23.29 lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y"
23.30 @@ -33,9 +33,9 @@
23.31 done
23.32
23.33
23.34 -constdefs
23.35 +definition
23.36 down_chain :: "(nat => 'a set) => bool"
23.37 - "down_chain F == \<forall>i. F (Suc i) \<subseteq> F i"
23.38 + "down_chain F = (\<forall>i. F (Suc i) \<subseteq> F i)"
23.39
23.40 lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
23.41 by (simp add: down_chain_def)
23.42 @@ -43,10 +43,10 @@
23.43 lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i"
23.44 by (simp add: down_chain_def)
23.45
23.46 -lemma down_chain_less_mono [rule_format]:
23.47 - "down_chain F ==> x < y --> F y \<subseteq> F x"
23.48 - apply (induct_tac y)
23.49 - apply (blast dest: down_chainD elim: less_SucE)+
23.50 +lemma down_chain_less_mono:
23.51 + "down_chain F ==> x < y ==> F y \<subseteq> F x"
23.52 + apply (induct y)
23.53 + apply (blast dest: down_chainD elim: less_SucE)+
23.54 done
23.55
23.56 lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x"
23.57 @@ -57,9 +57,9 @@
23.58
23.59 subsection "Continuity"
23.60
23.61 -constdefs
23.62 +definition
23.63 up_cont :: "('a set => 'a set) => bool"
23.64 - "up_cont f == \<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F)"
23.65 + "up_cont f = (\<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F))"
23.66
23.67 lemma up_contI:
23.68 "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
23.69 @@ -84,10 +84,10 @@
23.70 done
23.71
23.72
23.73 -constdefs
23.74 +definition
23.75 down_cont :: "('a set => 'a set) => bool"
23.76 - "down_cont f ==
23.77 - \<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F)"
23.78 + "down_cont f =
23.79 + (\<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F))"
23.80
23.81 lemma down_contI:
23.82 "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>
23.83 @@ -114,9 +114,9 @@
23.84
23.85 subsection "Iteration"
23.86
23.87 -constdefs
23.88 +definition
23.89 up_iterate :: "('a set => 'a set) => nat => 'a set"
23.90 - "up_iterate f n == (f^n) {}"
23.91 + "up_iterate f n = (f^n) {}"
23.92
23.93 lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
23.94 by (simp add: up_iterate_def)
23.95 @@ -166,9 +166,9 @@
23.96 done
23.97
23.98
23.99 -constdefs
23.100 +definition
23.101 down_iterate :: "('a set => 'a set) => nat => 'a set"
23.102 - "down_iterate f n == (f^n) UNIV"
23.103 + "down_iterate f n = (f^n) UNIV"
23.104
23.105 lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
23.106 by (simp add: down_iterate_def)
24.1 --- a/src/HOL/Library/FuncSet.thy Sat May 27 17:42:00 2006 +0200
24.2 +++ b/src/HOL/Library/FuncSet.thy Sat May 27 17:42:02 2006 +0200
24.3 @@ -9,15 +9,15 @@
24.4 imports Main
24.5 begin
24.6
24.7 -constdefs
24.8 +definition
24.9 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
24.10 - "Pi A B == {f. \<forall>x. x \<in> A --> f x \<in> B x}"
24.11 + "Pi A B = {f. \<forall>x. x \<in> A --> f x \<in> B x}"
24.12
24.13 extensional :: "'a set => ('a => 'b) set"
24.14 - "extensional A == {f. \<forall>x. x~:A --> f x = arbitrary}"
24.15 + "extensional A = {f. \<forall>x. x~:A --> f x = arbitrary}"
24.16
24.17 "restrict" :: "['a => 'b, 'a set] => ('a => 'b)"
24.18 - "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
24.19 + "restrict f A = (%x. if x \<in> A then f x else arbitrary)"
24.20
24.21 abbreviation
24.22 funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "->" 60)
24.23 @@ -27,24 +27,24 @@
24.24 funcset (infixr "\<rightarrow>" 60)
24.25
24.26 syntax
24.27 - "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
24.28 - "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3%_:_./ _)" [0,0,3] 3)
24.29 + "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10)
24.30 + "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3%_:_./ _)" [0,0,3] 3)
24.31
24.32 syntax (xsymbols)
24.33 - "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
24.34 - "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
24.35 + "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
24.36 + "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
24.37
24.38 syntax (HTML output)
24.39 - "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
24.40 - "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
24.41 + "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
24.42 + "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
24.43
24.44 translations
24.45 "PI x:A. B" == "Pi A (%x. B)"
24.46 "%x:A. f" == "restrict (%x. f) A"
24.47
24.48 -constdefs
24.49 +definition
24.50 "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
24.51 - "compose A g f == \<lambda>x\<in>A. g (f x)"
24.52 + "compose A g f = (\<lambda>x\<in>A. g (f x))"
24.53
24.54
24.55 subsection{*Basic Properties of @{term Pi}*}
24.56 @@ -62,7 +62,7 @@
24.57 by (simp add: Pi_def)
24.58
24.59 lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B"
24.60 -by (auto simp add: Pi_def)
24.61 + by (auto simp add: Pi_def)
24.62
24.63 lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
24.64 apply (simp add: Pi_def, auto)
24.65 @@ -133,7 +133,7 @@
24.66 by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
24.67
24.68 lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
24.69 - by (auto simp add: restrict_def)
24.70 + by (auto simp add: restrict_def)
24.71
24.72
24.73 subsection{*Bijections Between Sets*}
24.74 @@ -141,21 +141,21 @@
24.75 text{*The basic definition could be moved to @{text "Fun.thy"}, but most of
24.76 the theorems belong here, or need at least @{term Hilbert_Choice}.*}
24.77
24.78 -constdefs
24.79 - bij_betw :: "['a => 'b, 'a set, 'b set] => bool" (*bijective*)
24.80 - "bij_betw f A B == inj_on f A & f ` A = B"
24.81 +definition
24.82 + bij_betw :: "['a => 'b, 'a set, 'b set] => bool" -- {* bijective *}
24.83 + "bij_betw f A B = (inj_on f A & f ` A = B)"
24.84
24.85 lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
24.86 -by (simp add: bij_betw_def)
24.87 + by (simp add: bij_betw_def)
24.88
24.89 lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
24.90 -by (auto simp add: bij_betw_def inj_on_Inv Pi_def)
24.91 + by (auto simp add: bij_betw_def inj_on_Inv Pi_def)
24.92
24.93 lemma bij_betw_Inv: "bij_betw f A B \<Longrightarrow> bij_betw (Inv A f) B A"
24.94 -apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
24.95 -apply (simp add: image_compose [symmetric] o_def)
24.96 -apply (simp add: image_def Inv_f_f)
24.97 -done
24.98 + apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
24.99 + apply (simp add: image_compose [symmetric] o_def)
24.100 + apply (simp add: image_def Inv_f_f)
24.101 + done
24.102
24.103 lemma inj_on_compose:
24.104 "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
24.105 @@ -163,9 +163,9 @@
24.106
24.107 lemma bij_betw_compose:
24.108 "[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C"
24.109 -apply (simp add: bij_betw_def compose_eq inj_on_compose)
24.110 -apply (auto simp add: compose_def image_def)
24.111 -done
24.112 + apply (simp add: bij_betw_def compose_eq inj_on_compose)
24.113 + apply (auto simp add: compose_def image_def)
24.114 + done
24.115
24.116 lemma bij_betw_restrict_eq [simp]:
24.117 "bij_betw (restrict f A) A B = bij_betw f A B"
24.118 @@ -210,13 +210,13 @@
24.119 subsection{*Cardinality*}
24.120
24.121 lemma card_inj: "[|f \<in> A\<rightarrow>B; inj_on f A; finite B|] ==> card(A) \<le> card(B)"
24.122 -apply (rule card_inj_on_le)
24.123 -apply (auto simp add: Pi_def)
24.124 -done
24.125 + apply (rule card_inj_on_le)
24.126 + apply (auto simp add: Pi_def)
24.127 + done
24.128
24.129 lemma card_bij:
24.130 "[|f \<in> A\<rightarrow>B; inj_on f A;
24.131 g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
24.132 -by (blast intro: card_inj order_antisym)
24.133 + by (blast intro: card_inj order_antisym)
24.134
24.135 end
25.1 --- a/src/HOL/Library/NatPair.thy Sat May 27 17:42:00 2006 +0200
25.2 +++ b/src/HOL/Library/NatPair.thy Sat May 27 17:42:02 2006 +0200
25.3 @@ -11,25 +11,24 @@
25.4 begin
25.5
25.6 text{*
25.7 - An injective function from @{text "\<nat>\<twosuperior>"} to @{text
25.8 - \<nat>}. Definition and proofs are from \cite[page
25.9 - 85]{Oberschelp:1993}.
25.10 + An injective function from @{text "\<nat>\<twosuperior>"} to @{text \<nat>}. Definition
25.11 + and proofs are from \cite[page 85]{Oberschelp:1993}.
25.12 *}
25.13
25.14 -constdefs
25.15 +definition
25.16 nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
25.17 - "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n"
25.18 + "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
25.19
25.20 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
25.21 proof (cases "2 dvd a")
25.22 case True
25.23 - thus ?thesis by (rule dvd_mult2)
25.24 + then show ?thesis by (rule dvd_mult2)
25.25 next
25.26 case False
25.27 - hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
25.28 - hence "Suc a mod 2 = 0" by (simp add: mod_Suc)
25.29 - hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
25.30 - thus ?thesis by (rule dvd_mult)
25.31 + then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
25.32 + then have "Suc a mod 2 = 0" by (simp add: mod_Suc)
25.33 + then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
25.34 + then show ?thesis by (rule dvd_mult)
25.35 qed
25.36
25.37 lemma
25.38 @@ -37,7 +36,7 @@
25.39 shows nat2_to_nat_help: "u+v \<le> x+y"
25.40 proof (rule classical)
25.41 assume "\<not> ?thesis"
25.42 - hence contrapos: "x+y < u+v"
25.43 + then have contrapos: "x+y < u+v"
25.44 by simp
25.45 have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
25.46 by (unfold nat2_to_nat_def) (simp add: Let_def)
25.47 @@ -48,7 +47,7 @@
25.48 proof -
25.49 have "2 dvd (x+y)*Suc(x+y)"
25.50 by (rule dvd2_a_x_suc_a)
25.51 - hence "(x+y)*Suc(x+y) mod 2 = 0"
25.52 + then have "(x+y)*Suc(x+y) mod 2 = 0"
25.53 by (simp only: dvd_eq_mod_eq_0)
25.54 also
25.55 have "2 * Suc(x+y) mod 2 = 0"
25.56 @@ -56,7 +55,7 @@
25.57 ultimately have
25.58 "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
25.59 by simp
25.60 - thus ?thesis
25.61 + then show ?thesis
25.62 by simp
25.63 qed
25.64 also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
25.65 @@ -75,7 +74,7 @@
25.66 proof -
25.67 {
25.68 fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
25.69 - hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
25.70 + then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
25.71 also from prems [symmetric] have "x+y \<le> u+v"
25.72 by (rule nat2_to_nat_help)
25.73 finally have eq: "u+v = x+y" .
25.74 @@ -86,9 +85,9 @@
25.75 with ux have "(u,v) = (x,y)"
25.76 by simp
25.77 }
25.78 - hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
25.79 + then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
25.80 by fast
25.81 - thus ?thesis
25.82 + then show ?thesis
25.83 by (unfold inj_on_def) simp
25.84 qed
25.85
26.1 --- a/src/HOL/Library/Nat_Infinity.thy Sat May 27 17:42:00 2006 +0200
26.2 +++ b/src/HOL/Library/Nat_Infinity.thy Sat May 27 17:42:02 2006 +0200
26.3 @@ -19,20 +19,20 @@
26.4
26.5 datatype inat = Fin nat | Infty
26.6
26.7 +const_syntax (xsymbols)
26.8 + Infty ("\<infinity>")
26.9 +
26.10 +const_syntax (HTML output)
26.11 + Infty ("\<infinity>")
26.12 +
26.13 instance inat :: "{ord, zero}" ..
26.14
26.15 -consts
26.16 +definition
26.17 iSuc :: "inat => inat"
26.18 + "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>)"
26.19
26.20 -syntax (xsymbols)
26.21 - Infty :: inat ("\<infinity>")
26.22 -
26.23 -syntax (HTML output)
26.24 - Infty :: inat ("\<infinity>")
26.25 -
26.26 -defs
26.27 +defs (overloaded)
26.28 Zero_inat_def: "0 == Fin 0"
26.29 - iSuc_def: "iSuc i == case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>"
26.30 iless_def: "m < n ==
26.31 case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
26.32 | \<infinity> => False"
26.33 @@ -114,7 +114,6 @@
26.34 by (simp add: inat_defs split:inat_splits, arith?)
26.35
26.36
26.37 -(* ----------------------------------------------------------------------- *)
26.38
26.39 lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
26.40 by (simp add: inat_defs split:inat_splits, arith?)
27.1 --- a/src/HOL/Library/Product_ord.thy Sat May 27 17:42:00 2006 +0200
27.2 +++ b/src/HOL/Library/Product_ord.thy Sat May 27 17:42:02 2006 +0200
27.3 @@ -9,20 +9,19 @@
27.4 imports Main
27.5 begin
27.6
27.7 -instance "*" :: (ord,ord) ord ..
27.8 +instance "*" :: (ord, ord) ord ..
27.9
27.10 defs (overloaded)
27.11 - prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
27.12 + prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
27.13 prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)"
27.14
27.15
27.16 lemmas prod_ord_defs = prod_less_def prod_le_def
27.17
27.18 -instance "*" :: (order,order) order
27.19 - apply (intro_classes, unfold prod_ord_defs)
27.20 - by (auto intro: order_less_trans)
27.21 +instance * :: (order, order) order
27.22 + by default (auto simp: prod_ord_defs intro: order_less_trans)
27.23
27.24 -instance "*":: (linorder,linorder)linorder
27.25 - by (intro_classes, unfold prod_le_def, auto)
27.26 +instance * :: (linorder, linorder) linorder
27.27 + by default (auto simp: prod_le_def)
27.28
27.29 -end
27.30 \ No newline at end of file
27.31 +end
28.1 --- a/src/HOL/Library/SetsAndFunctions.thy Sat May 27 17:42:00 2006 +0200
28.2 +++ b/src/HOL/Library/SetsAndFunctions.thy Sat May 27 17:42:02 2006 +0200
28.3 @@ -1,5 +1,5 @@
28.4 (* Title: HOL/Library/SetsAndFunctions.thy
28.5 - ID: $Id$
28.6 + ID: $Id$
28.7 Author: Jeremy Avigad and Kevin Donnelly
28.8 *)
28.9
28.10 @@ -9,13 +9,13 @@
28.11 imports Main
28.12 begin
28.13
28.14 -text {*
28.15 +text {*
28.16 This library lifts operations like addition and muliplication to sets and
28.17 functions of appropriate types. It was designed to support asymptotic
28.18 calculations. See the comments at the top of theory @{text BigO}.
28.19 *}
28.20
28.21 -subsection {* Basic definitions *}
28.22 +subsection {* Basic definitions *}
28.23
28.24 instance set :: (plus) plus ..
28.25 instance fun :: (type, plus) plus ..
28.26 @@ -28,14 +28,14 @@
28.27 instance fun :: (type, times) times ..
28.28
28.29 defs (overloaded)
28.30 - func_times: "f * g == (%x. f x * g x)"
28.31 + func_times: "f * g == (%x. f x * g x)"
28.32 set_times:"A * B == {c. EX a:A. EX b:B. c = a * b}"
28.33
28.34 instance fun :: (type, minus) minus ..
28.35
28.36 defs (overloaded)
28.37 func_minus: "- f == (%x. - f x)"
28.38 - func_diff: "f - g == %x. f x - g x"
28.39 + func_diff: "f - g == %x. f x - g x"
28.40
28.41 instance fun :: (type, zero) zero ..
28.42 instance set :: (zero) zero ..
28.43 @@ -51,12 +51,12 @@
28.44 func_one: "1::(('a::type) => ('b::one)) == %x. 1"
28.45 set_one: "1::('a::one)set == {1}"
28.46
28.47 -constdefs
28.48 +definition
28.49 elt_set_plus :: "'a::plus => 'a set => 'a set" (infixl "+o" 70)
28.50 - "a +o B == {c. EX b:B. c = a + b}"
28.51 + "a +o B = {c. EX b:B. c = a + b}"
28.52
28.53 elt_set_times :: "'a::times => 'a set => 'a set" (infixl "*o" 80)
28.54 - "a *o B == {c. EX b:B. c = a * b}"
28.55 + "a *o B = {c. EX b:B. c = a * b}"
28.56
28.57 abbreviation (input)
28.58 elt_set_eq :: "'a => 'a set => bool" (infix "=o" 50)
28.59 @@ -69,291 +69,292 @@
28.60 by default (auto simp add: func_zero func_plus add_ac)
28.61
28.62 instance fun :: (type,ab_group_add)ab_group_add
28.63 - apply intro_classes
28.64 - apply (simp add: func_minus func_plus func_zero)
28.65 + apply default
28.66 + apply (simp add: func_minus func_plus func_zero)
28.67 apply (simp add: func_minus func_plus func_diff diff_minus)
28.68 -done
28.69 + done
28.70
28.71 instance fun :: (type,semigroup_mult)semigroup_mult
28.72 - apply intro_classes
28.73 + apply default
28.74 apply (auto simp add: func_times mult_assoc)
28.75 -done
28.76 + done
28.77
28.78 instance fun :: (type,comm_monoid_mult)comm_monoid_mult
28.79 - apply intro_classes
28.80 - apply (auto simp add: func_one func_times mult_ac)
28.81 -done
28.82 + apply default
28.83 + apply (auto simp add: func_one func_times mult_ac)
28.84 + done
28.85
28.86 instance fun :: (type,comm_ring_1)comm_ring_1
28.87 - apply intro_classes
28.88 - apply (auto simp add: func_plus func_times func_minus func_diff ext
28.89 - func_one func_zero ring_eq_simps)
28.90 + apply default
28.91 + apply (auto simp add: func_plus func_times func_minus func_diff ext
28.92 + func_one func_zero ring_eq_simps)
28.93 apply (drule fun_cong)
28.94 apply simp
28.95 -done
28.96 + done
28.97
28.98 instance set :: (semigroup_add)semigroup_add
28.99 - apply intro_classes
28.100 + apply default
28.101 apply (unfold set_plus)
28.102 apply (force simp add: add_assoc)
28.103 -done
28.104 + done
28.105
28.106 instance set :: (semigroup_mult)semigroup_mult
28.107 - apply intro_classes
28.108 + apply default
28.109 apply (unfold set_times)
28.110 apply (force simp add: mult_assoc)
28.111 -done
28.112 + done
28.113
28.114 instance set :: (comm_monoid_add)comm_monoid_add
28.115 - apply intro_classes
28.116 - apply (unfold set_plus)
28.117 - apply (force simp add: add_ac)
28.118 + apply default
28.119 + apply (unfold set_plus)
28.120 + apply (force simp add: add_ac)
28.121 apply (unfold set_zero)
28.122 apply force
28.123 -done
28.124 + done
28.125
28.126 instance set :: (comm_monoid_mult)comm_monoid_mult
28.127 - apply intro_classes
28.128 - apply (unfold set_times)
28.129 - apply (force simp add: mult_ac)
28.130 + apply default
28.131 + apply (unfold set_times)
28.132 + apply (force simp add: mult_ac)
28.133 apply (unfold set_one)
28.134 apply force
28.135 -done
28.136 + done
28.137 +
28.138
28.139 subsection {* Basic properties *}
28.140
28.141 -lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
28.142 -by (auto simp add: set_plus)
28.143 +lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
28.144 + by (auto simp add: set_plus)
28.145
28.146 lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
28.147 -by (auto simp add: elt_set_plus_def)
28.148 + by (auto simp add: elt_set_plus_def)
28.149
28.150 -lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) +
28.151 - (b +o D) = (a + b) +o (C + D)"
28.152 +lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) +
28.153 + (b +o D) = (a + b) +o (C + D)"
28.154 apply (auto simp add: elt_set_plus_def set_plus add_ac)
28.155 - apply (rule_tac x = "ba + bb" in exI)
28.156 + apply (rule_tac x = "ba + bb" in exI)
28.157 apply (auto simp add: add_ac)
28.158 apply (rule_tac x = "aa + a" in exI)
28.159 apply (auto simp add: add_ac)
28.160 -done
28.161 + done
28.162
28.163 -lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
28.164 - (a + b) +o C"
28.165 -by (auto simp add: elt_set_plus_def add_assoc)
28.166 +lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
28.167 + (a + b) +o C"
28.168 + by (auto simp add: elt_set_plus_def add_assoc)
28.169
28.170 -lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C =
28.171 - a +o (B + C)"
28.172 +lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C =
28.173 + a +o (B + C)"
28.174 apply (auto simp add: elt_set_plus_def set_plus)
28.175 - apply (blast intro: add_ac)
28.176 + apply (blast intro: add_ac)
28.177 apply (rule_tac x = "a + aa" in exI)
28.178 apply (rule conjI)
28.179 - apply (rule_tac x = "aa" in bexI)
28.180 - apply auto
28.181 + apply (rule_tac x = "aa" in bexI)
28.182 + apply auto
28.183 apply (rule_tac x = "ba" in bexI)
28.184 - apply (auto simp add: add_ac)
28.185 -done
28.186 + apply (auto simp add: add_ac)
28.187 + done
28.188
28.189 -theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) =
28.190 - a +o (C + D)"
28.191 +theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) =
28.192 + a +o (C + D)"
28.193 apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus add_ac)
28.194 - apply (rule_tac x = "aa + ba" in exI)
28.195 - apply (auto simp add: add_ac)
28.196 -done
28.197 + apply (rule_tac x = "aa + ba" in exI)
28.198 + apply (auto simp add: add_ac)
28.199 + done
28.200
28.201 theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
28.202 set_plus_rearrange3 set_plus_rearrange4
28.203
28.204 lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
28.205 -by (auto simp add: elt_set_plus_def)
28.206 + by (auto simp add: elt_set_plus_def)
28.207
28.208 -lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
28.209 +lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
28.210 C + E <= D + F"
28.211 -by (auto simp add: set_plus)
28.212 + by (auto simp add: set_plus)
28.213
28.214 lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C + D"
28.215 -by (auto simp add: elt_set_plus_def set_plus)
28.216 + by (auto simp add: elt_set_plus_def set_plus)
28.217
28.218 -lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
28.219 - a +o D <= D + C"
28.220 -by (auto simp add: elt_set_plus_def set_plus add_ac)
28.221 +lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
28.222 + a +o D <= D + C"
28.223 + by (auto simp add: elt_set_plus_def set_plus add_ac)
28.224
28.225 lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C + D"
28.226 apply (subgoal_tac "a +o B <= a +o D")
28.227 - apply (erule order_trans)
28.228 - apply (erule set_plus_mono3)
28.229 + apply (erule order_trans)
28.230 + apply (erule set_plus_mono3)
28.231 apply (erule set_plus_mono)
28.232 -done
28.233 + done
28.234
28.235 -lemma set_plus_mono_b: "C <= D ==> x : a +o C
28.236 +lemma set_plus_mono_b: "C <= D ==> x : a +o C
28.237 ==> x : a +o D"
28.238 apply (frule set_plus_mono)
28.239 apply auto
28.240 -done
28.241 + done
28.242
28.243 -lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==>
28.244 +lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==>
28.245 x : D + F"
28.246 apply (frule set_plus_mono2)
28.247 - prefer 2
28.248 - apply force
28.249 + prefer 2
28.250 + apply force
28.251 apply assumption
28.252 -done
28.253 + done
28.254
28.255 lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C + D"
28.256 apply (frule set_plus_mono3)
28.257 apply auto
28.258 -done
28.259 + done
28.260
28.261 -lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
28.262 - x : a +o D ==> x : D + C"
28.263 +lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
28.264 + x : a +o D ==> x : D + C"
28.265 apply (frule set_plus_mono4)
28.266 apply auto
28.267 -done
28.268 + done
28.269
28.270 lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
28.271 -by (auto simp add: elt_set_plus_def)
28.272 + by (auto simp add: elt_set_plus_def)
28.273
28.274 lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A + B"
28.275 apply (auto intro!: subsetI simp add: set_plus)
28.276 apply (rule_tac x = 0 in bexI)
28.277 - apply (rule_tac x = x in bexI)
28.278 - apply (auto simp add: add_ac)
28.279 -done
28.280 + apply (rule_tac x = x in bexI)
28.281 + apply (auto simp add: add_ac)
28.282 + done
28.283
28.284 lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
28.285 -by (auto simp add: elt_set_plus_def add_ac diff_minus)
28.286 + by (auto simp add: elt_set_plus_def add_ac diff_minus)
28.287
28.288 lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
28.289 apply (auto simp add: elt_set_plus_def add_ac diff_minus)
28.290 apply (subgoal_tac "a = (a + - b) + b")
28.291 - apply (rule bexI, assumption, assumption)
28.292 + apply (rule bexI, assumption, assumption)
28.293 apply (auto simp add: add_ac)
28.294 -done
28.295 + done
28.296
28.297 lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
28.298 -by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
28.299 + by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
28.300 assumption)
28.301
28.302 -lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
28.303 -by (auto simp add: set_times)
28.304 +lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
28.305 + by (auto simp add: set_times)
28.306
28.307 lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
28.308 -by (auto simp add: elt_set_times_def)
28.309 + by (auto simp add: elt_set_times_def)
28.310
28.311 -lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) *
28.312 - (b *o D) = (a * b) *o (C * D)"
28.313 +lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) *
28.314 + (b *o D) = (a * b) *o (C * D)"
28.315 apply (auto simp add: elt_set_times_def set_times)
28.316 - apply (rule_tac x = "ba * bb" in exI)
28.317 - apply (auto simp add: mult_ac)
28.318 + apply (rule_tac x = "ba * bb" in exI)
28.319 + apply (auto simp add: mult_ac)
28.320 apply (rule_tac x = "aa * a" in exI)
28.321 apply (auto simp add: mult_ac)
28.322 -done
28.323 + done
28.324
28.325 -lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
28.326 - (a * b) *o C"
28.327 -by (auto simp add: elt_set_times_def mult_assoc)
28.328 +lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
28.329 + (a * b) *o C"
28.330 + by (auto simp add: elt_set_times_def mult_assoc)
28.331
28.332 -lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C =
28.333 - a *o (B * C)"
28.334 +lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C =
28.335 + a *o (B * C)"
28.336 apply (auto simp add: elt_set_times_def set_times)
28.337 - apply (blast intro: mult_ac)
28.338 + apply (blast intro: mult_ac)
28.339 apply (rule_tac x = "a * aa" in exI)
28.340 apply (rule conjI)
28.341 - apply (rule_tac x = "aa" in bexI)
28.342 - apply auto
28.343 + apply (rule_tac x = "aa" in bexI)
28.344 + apply auto
28.345 apply (rule_tac x = "ba" in bexI)
28.346 - apply (auto simp add: mult_ac)
28.347 -done
28.348 + apply (auto simp add: mult_ac)
28.349 + done
28.350
28.351 -theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) =
28.352 - a *o (C * D)"
28.353 - apply (auto intro!: subsetI simp add: elt_set_times_def set_times
28.354 +theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) =
28.355 + a *o (C * D)"
28.356 + apply (auto intro!: subsetI simp add: elt_set_times_def set_times
28.357 mult_ac)
28.358 - apply (rule_tac x = "aa * ba" in exI)
28.359 - apply (auto simp add: mult_ac)
28.360 -done
28.361 + apply (rule_tac x = "aa * ba" in exI)
28.362 + apply (auto simp add: mult_ac)
28.363 + done
28.364
28.365 theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
28.366 set_times_rearrange3 set_times_rearrange4
28.367
28.368 lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
28.369 -by (auto simp add: elt_set_times_def)
28.370 + by (auto simp add: elt_set_times_def)
28.371
28.372 -lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
28.373 +lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
28.374 C * E <= D * F"
28.375 -by (auto simp add: set_times)
28.376 + by (auto simp add: set_times)
28.377
28.378 lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C * D"
28.379 -by (auto simp add: elt_set_times_def set_times)
28.380 + by (auto simp add: elt_set_times_def set_times)
28.381
28.382 -lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
28.383 - a *o D <= D * C"
28.384 -by (auto simp add: elt_set_times_def set_times mult_ac)
28.385 +lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
28.386 + a *o D <= D * C"
28.387 + by (auto simp add: elt_set_times_def set_times mult_ac)
28.388
28.389 lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C * D"
28.390 apply (subgoal_tac "a *o B <= a *o D")
28.391 - apply (erule order_trans)
28.392 - apply (erule set_times_mono3)
28.393 + apply (erule order_trans)
28.394 + apply (erule set_times_mono3)
28.395 apply (erule set_times_mono)
28.396 -done
28.397 + done
28.398
28.399 -lemma set_times_mono_b: "C <= D ==> x : a *o C
28.400 +lemma set_times_mono_b: "C <= D ==> x : a *o C
28.401 ==> x : a *o D"
28.402 apply (frule set_times_mono)
28.403 apply auto
28.404 -done
28.405 + done
28.406
28.407 -lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==>
28.408 +lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==>
28.409 x : D * F"
28.410 apply (frule set_times_mono2)
28.411 - prefer 2
28.412 - apply force
28.413 + prefer 2
28.414 + apply force
28.415 apply assumption
28.416 -done
28.417 + done
28.418
28.419 lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C * D"
28.420 apply (frule set_times_mono3)
28.421 apply auto
28.422 -done
28.423 + done
28.424
28.425 -lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
28.426 - x : a *o D ==> x : D * C"
28.427 +lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
28.428 + x : a *o D ==> x : D * C"
28.429 apply (frule set_times_mono4)
28.430 apply auto
28.431 -done
28.432 + done
28.433
28.434 lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
28.435 -by (auto simp add: elt_set_times_def)
28.436 + by (auto simp add: elt_set_times_def)
28.437
28.438 -lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
28.439 - (a * b) +o (a *o C)"
28.440 -by (auto simp add: elt_set_plus_def elt_set_times_def ring_distrib)
28.441 +lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
28.442 + (a * b) +o (a *o C)"
28.443 + by (auto simp add: elt_set_plus_def elt_set_times_def ring_distrib)
28.444
28.445 -lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
28.446 - (a *o B) + (a *o C)"
28.447 +lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
28.448 + (a *o B) + (a *o C)"
28.449 apply (auto simp add: set_plus elt_set_times_def ring_distrib)
28.450 - apply blast
28.451 + apply blast
28.452 apply (rule_tac x = "b + bb" in exI)
28.453 apply (auto simp add: ring_distrib)
28.454 -done
28.455 + done
28.456
28.457 -lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
28.458 +lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
28.459 a *o D + C * D"
28.460 - apply (auto intro!: subsetI simp add:
28.461 - elt_set_plus_def elt_set_times_def set_times
28.462 + apply (auto intro!: subsetI simp add:
28.463 + elt_set_plus_def elt_set_times_def set_times
28.464 set_plus ring_distrib)
28.465 apply auto
28.466 -done
28.467 + done
28.468
28.469 theorems set_times_plus_distribs =
28.470 set_times_plus_distrib
28.471 set_times_plus_distrib2
28.472
28.473 -lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
28.474 - - a : C"
28.475 -by (auto simp add: elt_set_times_def)
28.476 +lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
28.477 + - a : C"
28.478 + by (auto simp add: elt_set_times_def)
28.479
28.480 lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
28.481 - a : (- 1) *o C"
28.482 -by (auto simp add: elt_set_times_def)
28.483 -
28.484 + by (auto simp add: elt_set_times_def)
28.485 +
28.486 end
29.1 --- a/src/HOL/Library/While_Combinator.thy Sat May 27 17:42:00 2006 +0200
29.2 +++ b/src/HOL/Library/While_Combinator.thy Sat May 27 17:42:02 2006 +0200
29.3 @@ -35,7 +35,7 @@
29.4 apply blast
29.5 done
29.6
29.7 -constdefs
29.8 +definition
29.9 while :: "('a => bool) => ('a => 'a) => 'a => 'a"
29.10 "while b c s == while_aux (b, c, s)"
29.11
29.12 @@ -88,7 +88,8 @@
29.13 and terminate: "!!s. P s ==> \<not> b s ==> Q s"
29.14 and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
29.15 shows "P s \<Longrightarrow> Q (while b c s)"
29.16 - apply (induct s rule: wf [THEN wf_induct])
29.17 + using wf
29.18 + apply (induct s)
29.19 apply simp
29.20 apply (subst while_unfold)
29.21 apply (simp add: invariant terminate)
29.22 @@ -101,13 +102,13 @@
29.23 wf r;
29.24 !!s. [| P s; b s |] ==> (c s, s) \<in> r |] ==>
29.25 Q (while b c s)"
29.26 -apply (rule while_rule_lemma)
29.27 -prefer 4 apply assumption
29.28 -apply blast
29.29 -apply blast
29.30 -apply(erule wf_subset)
29.31 -apply blast
29.32 -done
29.33 + apply (rule while_rule_lemma)
29.34 + prefer 4 apply assumption
29.35 + apply blast
29.36 + apply blast
29.37 + apply (erule wf_subset)
29.38 + apply blast
29.39 + done
29.40
29.41 text {*
29.42 \medskip An application: computation of the @{term lfp} on finite
29.43 @@ -142,12 +143,11 @@
29.44 looping because the antisymmetry simproc turns the subset relationship
29.45 back into equality. *}
29.46
29.47 -lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))"
29.48 - by blast
29.49 -
29.50 theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
29.51 P {0, 4, 2}"
29.52 proof -
29.53 + have seteq: "!!A B. (A = B) = ((!a : A. a:B) & (!b:B. b:A))"
29.54 + by blast
29.55 have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
29.56 apply blast
29.57 done
30.1 --- a/src/HOL/Library/Word.thy Sat May 27 17:42:00 2006 +0200
30.2 +++ b/src/HOL/Library/Word.thy Sat May 27 17:42:02 2006 +0200
30.3 @@ -56,17 +56,17 @@
30.4 bitor :: "bit => bit => bit" (infixr "bitor" 30)
30.5 bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
30.6
30.7 -syntax (xsymbols)
30.8 - bitnot :: "bit => bit" ("\<not>\<^sub>b _" [40] 40)
30.9 - bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
30.10 - bitor :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
30.11 - bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
30.12 +const_syntax (xsymbols)
30.13 + bitnot ("\<not>\<^sub>b _" [40] 40)
30.14 + bitand (infixr "\<and>\<^sub>b" 35)
30.15 + bitor (infixr "\<or>\<^sub>b" 30)
30.16 + bitxor (infixr "\<oplus>\<^sub>b" 30)
30.17
30.18 -syntax (HTML output)
30.19 - bitnot :: "bit => bit" ("\<not>\<^sub>b _" [40] 40)
30.20 - bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
30.21 - bitor :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
30.22 - bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
30.23 +const_syntax (HTML output)
30.24 + bitnot ("\<not>\<^sub>b _" [40] 40)
30.25 + bitand (infixr "\<and>\<^sub>b" 35)
30.26 + bitor (infixr "\<or>\<^sub>b" 30)
30.27 + bitxor (infixr "\<oplus>\<^sub>b" 30)
30.28
30.29 primrec
30.30 bitnot_zero: "(bitnot \<zero>) = \<one>"
30.31 @@ -141,13 +141,13 @@
30.32 by (cases b,auto intro!: zero one)
30.33 qed
30.34
30.35 -constdefs
30.36 +definition
30.37 bv_msb :: "bit list => bit"
30.38 - "bv_msb w == if w = [] then \<zero> else hd w"
30.39 + "bv_msb w = (if w = [] then \<zero> else hd w)"
30.40 bv_extend :: "[nat,bit,bit list]=>bit list"
30.41 - "bv_extend i b w == (replicate (i - length w) b) @ w"
30.42 + "bv_extend i b w = (replicate (i - length w) b) @ w"
30.43 bv_not :: "bit list => bit list"
30.44 - "bv_not w == map bitnot w"
30.45 + "bv_not w = map bitnot w"
30.46
30.47 lemma bv_length_extend [simp]: "length w \<le> i ==> length (bv_extend i b w) = i"
30.48 by (simp add: bv_extend_def)
30.49 @@ -176,9 +176,9 @@
30.50 lemma length_bv_not [simp]: "length (bv_not w) = length w"
30.51 by (induct w,simp_all)
30.52
30.53 -constdefs
30.54 +definition
30.55 bv_to_nat :: "bit list => nat"
30.56 - "bv_to_nat == foldl (%bn b. 2 * bn + bitval b) 0"
30.57 + "bv_to_nat = foldl (%bn b. 2 * bn + bitval b) 0"
30.58
30.59 lemma bv_to_nat_Nil [simp]: "bv_to_nat [] = 0"
30.60 by (simp add: bv_to_nat_def)
30.61 @@ -326,9 +326,9 @@
30.62 ..
30.63 qed
30.64
30.65 -constdefs
30.66 +definition
30.67 norm_unsigned :: "bit list => bit list"
30.68 - "norm_unsigned == rem_initial \<zero>"
30.69 + "norm_unsigned = rem_initial \<zero>"
30.70
30.71 lemma norm_unsigned_Nil [simp]: "norm_unsigned [] = []"
30.72 by (simp add: norm_unsigned_def)
30.73 @@ -349,9 +349,9 @@
30.74 "nat_to_bv_helper n = (%bs. (if n = 0 then bs
30.75 else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
30.76
30.77 -constdefs
30.78 +definition
30.79 nat_to_bv :: "nat => bit list"
30.80 - "nat_to_bv n == nat_to_bv_helper n []"
30.81 + "nat_to_bv n = nat_to_bv_helper n []"
30.82
30.83 lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []"
30.84 by (simp add: nat_to_bv_def)
30.85 @@ -400,7 +400,7 @@
30.86 assume "k \<le> j" and "j < i"
30.87 with a
30.88 show "P j"
30.89 - by auto
30.90 + by auto
30.91 qed
30.92 show "\<forall> j. k \<le> j \<and> j < i + 1 --> P j"
30.93 proof auto
30.94 @@ -409,18 +409,18 @@
30.95 assume ji: "j \<le> i"
30.96 show "P j"
30.97 proof (cases "j = i")
30.98 - assume "j = i"
30.99 - with pi
30.100 - show "P j"
30.101 - by simp
30.102 + assume "j = i"
30.103 + with pi
30.104 + show "P j"
30.105 + by simp
30.106 next
30.107 - assume "j ~= i"
30.108 - with ji
30.109 - have "j < i"
30.110 - by simp
30.111 - with kj and a
30.112 - show "P j"
30.113 - by blast
30.114 + assume "j ~= i"
30.115 + with ji
30.116 + have "j < i"
30.117 + by simp
30.118 + with kj and a
30.119 + show "P j"
30.120 + by blast
30.121 qed
30.122 qed
30.123 qed
30.124 @@ -446,39 +446,39 @@
30.125 fix l
30.126 show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
30.127 proof (cases "n < 0")
30.128 - assume "n < 0"
30.129 - thus ?thesis
30.130 - by (simp add: nat_to_bv_helper.simps)
30.131 + assume "n < 0"
30.132 + thus ?thesis
30.133 + by (simp add: nat_to_bv_helper.simps)
30.134 next
30.135 - assume "~n < 0"
30.136 - show ?thesis
30.137 - proof (rule n_div_2_cases [of n])
30.138 - assume [simp]: "n = 0"
30.139 - show ?thesis
30.140 - apply (simp only: nat_to_bv_helper.simps [of n])
30.141 - apply simp
30.142 - done
30.143 - next
30.144 - assume n2n: "n div 2 < n"
30.145 - assume [simp]: "0 < n"
30.146 - hence n20: "0 \<le> n div 2"
30.147 - by arith
30.148 - from ind [of "n div 2"] and n2n n20
30.149 - have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
30.150 - by blast
30.151 - show ?thesis
30.152 - apply (simp only: nat_to_bv_helper.simps [of n])
30.153 - apply (cases "n=0")
30.154 - apply simp
30.155 - apply (simp only: if_False)
30.156 - apply simp
30.157 - apply (subst spec [OF ind',of "\<zero>#l"])
30.158 - apply (subst spec [OF ind',of "\<one>#l"])
30.159 - apply (subst spec [OF ind',of "[\<one>]"])
30.160 - apply (subst spec [OF ind',of "[\<zero>]"])
30.161 - apply simp
30.162 - done
30.163 - qed
30.164 + assume "~n < 0"
30.165 + show ?thesis
30.166 + proof (rule n_div_2_cases [of n])
30.167 + assume [simp]: "n = 0"
30.168 + show ?thesis
30.169 + apply (simp only: nat_to_bv_helper.simps [of n])
30.170 + apply simp
30.171 + done
30.172 + next
30.173 + assume n2n: "n div 2 < n"
30.174 + assume [simp]: "0 < n"
30.175 + hence n20: "0 \<le> n div 2"
30.176 + by arith
30.177 + from ind [of "n div 2"] and n2n n20
30.178 + have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
30.179 + by blast
30.180 + show ?thesis
30.181 + apply (simp only: nat_to_bv_helper.simps [of n])
30.182 + apply (cases "n=0")
30.183 + apply simp
30.184 + apply (simp only: if_False)
30.185 + apply simp
30.186 + apply (subst spec [OF ind',of "\<zero>#l"])
30.187 + apply (subst spec [OF ind',of "\<one>#l"])
30.188 + apply (subst spec [OF ind',of "[\<one>]"])
30.189 + apply (subst spec [OF ind',of "[\<zero>]"])
30.190 + apply simp
30.191 + done
30.192 + qed
30.193 qed
30.194 qed
30.195 qed
30.196 @@ -511,14 +511,14 @@
30.197 fix l2
30.198 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"
30.199 proof -
30.200 - have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
30.201 - by (induct "length xs",simp_all)
30.202 - hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
30.203 - bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
30.204 - by simp
30.205 - also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
30.206 - by (simp add: ring_distrib)
30.207 - finally show ?thesis .
30.208 + have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
30.209 + by (induct "length xs",simp_all)
30.210 + hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
30.211 + bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
30.212 + by simp
30.213 + also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
30.214 + by (simp add: ring_distrib)
30.215 + finally show ?thesis .
30.216 qed
30.217 qed
30.218 qed
30.219 @@ -553,15 +553,15 @@
30.220 apply (simp add: ind' split del: split_if)
30.221 apply (cases "n mod 2 = 0")
30.222 proof simp_all
30.223 - assume "n mod 2 = 0"
30.224 - with mod_div_equality [of n 2]
30.225 - show "n div 2 * 2 = n"
30.226 - by simp
30.227 + assume "n mod 2 = 0"
30.228 + with mod_div_equality [of n 2]
30.229 + show "n div 2 * 2 = n"
30.230 + by simp
30.231 next
30.232 - assume "n mod 2 = Suc 0"
30.233 - with mod_div_equality [of n 2]
30.234 - show "Suc (n div 2 * 2) = n"
30.235 - by simp
30.236 + assume "n mod 2 = Suc 0"
30.237 + with mod_div_equality [of n 2]
30.238 + show "Suc (n div 2 * 2) = n"
30.239 + by simp
30.240 qed
30.241 qed
30.242 qed
30.243 @@ -715,41 +715,41 @@
30.244 assume ind: "\<forall>ys. length ys < length xs --> ?P ys"
30.245 show "?P xs"
30.246 proof (cases xs)
30.247 - assume [simp]: "xs = []"
30.248 - show ?thesis
30.249 - by (simp add: nat_to_bv_non0)
30.250 + assume [simp]: "xs = []"
30.251 + show ?thesis
30.252 + by (simp add: nat_to_bv_non0)
30.253 next
30.254 - fix y ys
30.255 - assume [simp]: "xs = y # ys"
30.256 - show ?thesis
30.257 - apply simp
30.258 - apply (subst bv_to_nat_dist_append)
30.259 - apply simp
30.260 - proof -
30.261 - have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
30.262 - nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
30.263 - by (simp add: add_ac mult_ac)
30.264 - also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
30.265 - by simp
30.266 - also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
30.267 - proof -
30.268 - from ind
30.269 - have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
30.270 - by auto
30.271 - hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
30.272 - by simp
30.273 - show ?thesis
30.274 - apply (subst nat_helper1)
30.275 - apply simp_all
30.276 - done
30.277 - qed
30.278 - also have "... = (\<one>#rev ys) @ [y]"
30.279 - by simp
30.280 - also have "... = \<one> # rev ys @ [y]"
30.281 - by simp
30.282 - finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]"
30.283 - .
30.284 - qed
30.285 + fix y ys
30.286 + assume [simp]: "xs = y # ys"
30.287 + show ?thesis
30.288 + apply simp
30.289 + apply (subst bv_to_nat_dist_append)
30.290 + apply simp
30.291 + proof -
30.292 + have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
30.293 + nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
30.294 + by (simp add: add_ac mult_ac)
30.295 + also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
30.296 + by simp
30.297 + also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
30.298 + proof -
30.299 + from ind
30.300 + have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
30.301 + by auto
30.302 + hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
30.303 + by simp
30.304 + show ?thesis
30.305 + apply (subst nat_helper1)
30.306 + apply simp_all
30.307 + done
30.308 + qed
30.309 + also have "... = (\<one>#rev ys) @ [y]"
30.310 + by simp
30.311 + also have "... = \<one> # rev ys @ [y]"
30.312 + by simp
30.313 + finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]"
30.314 + .
30.315 + qed
30.316 qed
30.317 qed
30.318 qed
30.319 @@ -856,9 +856,9 @@
30.320
30.321 subsection {* Unsigned Arithmetic Operations *}
30.322
30.323 -constdefs
30.324 +definition
30.325 bv_add :: "[bit list, bit list ] => bit list"
30.326 - "bv_add w1 w2 == nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"
30.327 + "bv_add w1 w2 = nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"
30.328
30.329 lemma bv_add_type1 [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2"
30.330 by (simp add: bv_add_def)
30.331 @@ -893,13 +893,13 @@
30.332 proof
30.333 assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
30.334 hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
30.335 - by (rule add_right_mono)
30.336 + by (rule add_right_mono)
30.337 hence "(2::nat) ^ length w1 \<le> 2 ^ length w2"
30.338 - by simp
30.339 + by simp
30.340 hence "length w1 \<le> length w2"
30.341 - by simp
30.342 + by simp
30.343 thus False
30.344 - by simp
30.345 + by simp
30.346 qed
30.347 thus ?thesis
30.348 by (simp add: diff_mult_distrib2 split: split_max)
30.349 @@ -908,9 +908,9 @@
30.350 by arith
30.351 qed
30.352
30.353 -constdefs
30.354 +definition
30.355 bv_mult :: "[bit list, bit list ] => bit list"
30.356 - "bv_mult w1 w2 == nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"
30.357 + "bv_mult w1 w2 = nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"
30.358
30.359 lemma bv_mult_type1 [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2"
30.360 by (simp add: bv_mult_def)
30.361 @@ -968,11 +968,11 @@
30.362
30.363 lemmas [simp del] = norm_signed_Cons
30.364
30.365 -constdefs
30.366 +definition
30.367 int_to_bv :: "int => bit list"
30.368 - "int_to_bv n == if 0 \<le> n
30.369 + "int_to_bv n = (if 0 \<le> n
30.370 then norm_signed (\<zero>#nat_to_bv (nat n))
30.371 - else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))"
30.372 + else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1)))))"
30.373
30.374 lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv (nat n))"
30.375 by (simp add: int_to_bv_def)
30.376 @@ -1003,9 +1003,11 @@
30.377 qed
30.378 qed
30.379
30.380 -constdefs
30.381 +definition
30.382 bv_to_int :: "bit list => int"
30.383 - "bv_to_int w == case bv_msb w of \<zero> => int (bv_to_nat w) | \<one> => - int (bv_to_nat (bv_not w) + 1)"
30.384 + "bv_to_int w =
30.385 + (case bv_msb w of \<zero> => int (bv_to_nat w)
30.386 + | \<one> => - int (bv_to_nat (bv_not w) + 1))"
30.387
30.388 lemma bv_to_int_Nil [simp]: "bv_to_int [] = 0"
30.389 by (simp add: bv_to_int_def)
30.390 @@ -1232,23 +1234,23 @@
30.391 assume "norm_unsigned w' = []"
30.392 with weq and w0
30.393 show False
30.394 - by (simp add: norm_empty_bv_to_nat_zero)
30.395 + by (simp add: norm_empty_bv_to_nat_zero)
30.396 next
30.397 assume w'0: "norm_unsigned w' \<noteq> []"
30.398 have "0 < bv_to_nat w'"
30.399 proof (rule ccontr)
30.400 - assume "~ (0 < bv_to_nat w')"
30.401 - hence "bv_to_nat w' = 0"
30.402 - by arith
30.403 - hence "norm_unsigned w' = []"
30.404 - by (simp add: bv_to_nat_zero_imp_empty)
30.405 - with w'0
30.406 - show False
30.407 - by simp
30.408 + assume "~ (0 < bv_to_nat w')"
30.409 + hence "bv_to_nat w' = 0"
30.410 + by arith
30.411 + hence "norm_unsigned w' = []"
30.412 + by (simp add: bv_to_nat_zero_imp_empty)
30.413 + with w'0
30.414 + show False
30.415 + by simp
30.416 qed
30.417 with bv_to_nat_lower_limit [of w']
30.418 show "2 ^ (length (norm_unsigned w') - Suc 0) \<le> int (bv_to_nat w')"
30.419 - by (simp add: int_nat_two_exp)
30.420 + by (simp add: int_nat_two_exp)
30.421 qed
30.422 next
30.423 fix w'
30.424 @@ -1327,47 +1329,47 @@
30.425 proof (rule bit_list_cases [of "norm_signed w"])
30.426 assume "norm_signed w = []"
30.427 hence "bv_to_int (norm_signed w) = 0"
30.428 - by simp
30.429 + by simp
30.430 with w0
30.431 show ?thesis
30.432 - by simp
30.433 + by simp
30.434 next
30.435 fix w'
30.436 assume nw: "norm_signed w = \<zero> # w'"
30.437 from msbw
30.438 have "bv_msb (norm_signed w) = \<one>"
30.439 - by simp
30.440 + by simp
30.441 with nw
30.442 show ?thesis
30.443 - by simp
30.444 + by simp
30.445 next
30.446 fix w'
30.447 assume weq: "norm_signed w = \<one> # w'"
30.448 show ?thesis
30.449 proof (rule bit_list_cases [of w'])
30.450 - assume w'eq: "w' = []"
30.451 - from w0
30.452 - have "bv_to_int (norm_signed w) < -1"
30.453 - by simp
30.454 - with w'eq and weq
30.455 - show ?thesis
30.456 - by simp
30.457 + assume w'eq: "w' = []"
30.458 + from w0
30.459 + have "bv_to_int (norm_signed w) < -1"
30.460 + by simp
30.461 + with w'eq and weq
30.462 + show ?thesis
30.463 + by simp
30.464 next
30.465 - fix w''
30.466 - assume w'eq: "w' = \<zero> # w''"
30.467 - show ?thesis
30.468 - apply (simp add: weq w'eq)
30.469 - apply (subgoal_tac "- int (bv_to_nat (bv_not w'')) + -1 < 0 + 0")
30.470 - apply (simp add: int_nat_two_exp)
30.471 - apply (rule add_le_less_mono)
30.472 - apply simp_all
30.473 - done
30.474 + fix w''
30.475 + assume w'eq: "w' = \<zero> # w''"
30.476 + show ?thesis
30.477 + apply (simp add: weq w'eq)
30.478 + apply (subgoal_tac "- int (bv_to_nat (bv_not w'')) + -1 < 0 + 0")
30.479 + apply (simp add: int_nat_two_exp)
30.480 + apply (rule add_le_less_mono)
30.481 + apply simp_all
30.482 + done
30.483 next
30.484 - fix w''
30.485 - assume w'eq: "w' = \<one> # w''"
30.486 - with weq and msb_tl
30.487 - show ?thesis
30.488 - by simp
30.489 + fix w''
30.490 + assume w'eq: "w' = \<one> # w''"
30.491 + with weq and msb_tl
30.492 + show ?thesis
30.493 + by simp
30.494 qed
30.495 qed
30.496 qed
30.497 @@ -1396,7 +1398,7 @@
30.498 proof (rule bv_to_int_lower_limit_gt0)
30.499 from w0
30.500 show "0 < bv_to_int (int_to_bv i)"
30.501 - by simp
30.502 + by simp
30.503 qed
30.504 thus ?thesis
30.505 by simp
30.506 @@ -1586,9 +1588,9 @@
30.507
30.508 subsubsection {* Conversion from unsigned to signed *}
30.509
30.510 -constdefs
30.511 +definition
30.512 utos :: "bit list => bit list"
30.513 - "utos w == norm_signed (\<zero> # w)"
30.514 + "utos w = norm_signed (\<zero> # w)"
30.515
30.516 lemma utos_type [simp]: "utos (norm_unsigned w) = utos w"
30.517 by (simp add: utos_def norm_signed_Cons)
30.518 @@ -1610,9 +1612,9 @@
30.519
30.520 subsubsection {* Unary minus *}
30.521
30.522 -constdefs
30.523 +definition
30.524 bv_uminus :: "bit list => bit list"
30.525 - "bv_uminus w == int_to_bv (- bv_to_int w)"
30.526 + "bv_uminus w = int_to_bv (- bv_to_int w)"
30.527
30.528 lemma bv_uminus_type [simp]: "bv_uminus (norm_signed w) = bv_uminus w"
30.529 by (simp add: bv_uminus_def)
30.530 @@ -1636,16 +1638,16 @@
30.531 proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all)
30.532 from prems
30.533 show "bv_to_int w < 0"
30.534 - by simp
30.535 + by simp
30.536 next
30.537 have "-(2^(length w - 1)) \<le> bv_to_int w"
30.538 - by (rule bv_to_int_lower_range)
30.539 + by (rule bv_to_int_lower_range)
30.540 hence "- bv_to_int w \<le> 2^(length w - 1)"
30.541 - by simp
30.542 + by simp
30.543 also from lw have "... < 2 ^ length w"
30.544 - by simp
30.545 + by simp
30.546 finally show "- bv_to_int w < 2 ^ length w"
30.547 - by simp
30.548 + by simp
30.549 qed
30.550 next
30.551 assume p: "- bv_to_int w = 1"
30.552 @@ -1674,10 +1676,10 @@
30.553 apply simp
30.554 proof -
30.555 have "bv_to_int w < 2 ^ (length w - 1)"
30.556 - by (rule bv_to_int_upper_range)
30.557 + by (rule bv_to_int_upper_range)
30.558 also have "... \<le> 2 ^ length w" by simp
30.559 finally show "bv_to_int w \<le> 2 ^ length w"
30.560 - by simp
30.561 + by simp
30.562 qed
30.563 qed
30.564 qed
30.565 @@ -1709,9 +1711,9 @@
30.566 qed
30.567 qed
30.568
30.569 -constdefs
30.570 +definition
30.571 bv_sadd :: "[bit list, bit list ] => bit list"
30.572 - "bv_sadd w1 w2 == int_to_bv (bv_to_int w1 + bv_to_int w2)"
30.573 + "bv_sadd w1 w2 = int_to_bv (bv_to_int w1 + bv_to_int w2)"
30.574
30.575 lemma bv_sadd_type1 [simp]: "bv_sadd (norm_signed w1) w2 = bv_sadd w1 w2"
30.576 by (simp add: bv_sadd_def)
30.577 @@ -1756,10 +1758,10 @@
30.578 assume [simp]: "w1 = []"
30.579 show "w2 \<noteq> []"
30.580 proof (rule ccontr,simp)
30.581 - assume [simp]: "w2 = []"
30.582 - from p
30.583 - show False
30.584 - by simp
30.585 + assume [simp]: "w2 = []"
30.586 + from p
30.587 + show False
30.588 + by simp
30.589 qed
30.590 qed
30.591 qed
30.592 @@ -1784,18 +1786,18 @@
30.593 proof simp
30.594 from bv_to_int_upper_range [of w2]
30.595 have "bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
30.596 - by simp
30.597 + by simp
30.598 with bv_to_int_upper_range [of w1]
30.599 have "bv_to_int w1 + bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
30.600 - by (rule zadd_zless_mono)
30.601 + by (rule zadd_zless_mono)
30.602 also have "... \<le> 2 ^ max (length w1) (length w2)"
30.603 - apply (rule adder_helper)
30.604 - apply (rule helper)
30.605 - using p
30.606 - apply simp
30.607 - done
30.608 + apply (rule adder_helper)
30.609 + apply (rule helper)
30.610 + using p
30.611 + apply simp
30.612 + done
30.613 finally show "?Q < 2 ^ max (length w1) (length w2)"
30.614 - .
30.615 + .
30.616 qed
30.617 next
30.618 assume p: "?Q < -1"
30.619 @@ -1805,26 +1807,26 @@
30.620 apply (rule p)
30.621 proof -
30.622 have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
30.623 - apply (rule adder_helper)
30.624 - apply (rule helper)
30.625 - using p
30.626 - apply simp
30.627 - done
30.628 + apply (rule adder_helper)
30.629 + apply (rule helper)
30.630 + using p
30.631 + apply simp
30.632 + done
30.633 hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
30.634 - by simp
30.635 + by simp
30.636 also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> ?Q"
30.637 - apply (rule add_mono)
30.638 - apply (rule bv_to_int_lower_range [of w1])
30.639 - apply (rule bv_to_int_lower_range [of w2])
30.640 - done
30.641 + apply (rule add_mono)
30.642 + apply (rule bv_to_int_lower_range [of w1])
30.643 + apply (rule bv_to_int_lower_range [of w2])
30.644 + done
30.645 finally show "- (2^max (length w1) (length w2)) \<le> ?Q" .
30.646 qed
30.647 qed
30.648 qed
30.649
30.650 -constdefs
30.651 +definition
30.652 bv_sub :: "[bit list, bit list] => bit list"
30.653 - "bv_sub w1 w2 == bv_sadd w1 (bv_uminus w2)"
30.654 + "bv_sub w1 w2 = bv_sadd w1 (bv_uminus w2)"
30.655
30.656 lemma bv_sub_type1 [simp]: "bv_sub (norm_signed w1) w2 = bv_sub w1 w2"
30.657 by (simp add: bv_sub_def)
30.658 @@ -1878,18 +1880,18 @@
30.659 proof simp
30.660 from bv_to_int_lower_range [of w2]
30.661 have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
30.662 - by simp
30.663 + by simp
30.664 have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
30.665 - apply (rule zadd_zless_mono)
30.666 - apply (rule bv_to_int_upper_range [of w1])
30.667 - apply (rule v2)
30.668 - done
30.669 + apply (rule zadd_zless_mono)
30.670 + apply (rule bv_to_int_upper_range [of w1])
30.671 + apply (rule v2)
30.672 + done
30.673 also have "... \<le> 2 ^ max (length w1) (length w2)"
30.674 - apply (rule adder_helper)
30.675 - apply (rule lmw)
30.676 - done
30.677 + apply (rule adder_helper)
30.678 + apply (rule lmw)
30.679 + done
30.680 finally show "?Q < 2 ^ max (length w1) (length w2)"
30.681 - by simp
30.682 + by simp
30.683 qed
30.684 next
30.685 assume p: "?Q < -1"
30.686 @@ -1899,26 +1901,26 @@
30.687 apply (rule p)
30.688 proof simp
30.689 have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
30.690 - apply (rule adder_helper)
30.691 - apply (rule lmw)
30.692 - done
30.693 + apply (rule adder_helper)
30.694 + apply (rule lmw)
30.695 + done
30.696 hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
30.697 - by simp
30.698 + by simp
30.699 also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> bv_to_int w1 + -bv_to_int w2"
30.700 - apply (rule add_mono)
30.701 - apply (rule bv_to_int_lower_range [of w1])
30.702 - using bv_to_int_upper_range [of w2]
30.703 - apply simp
30.704 - done
30.705 + apply (rule add_mono)
30.706 + apply (rule bv_to_int_lower_range [of w1])
30.707 + using bv_to_int_upper_range [of w2]
30.708 + apply simp
30.709 + done
30.710 finally show "- (2^max (length w1) (length w2)) \<le> ?Q"
30.711 - by simp
30.712 + by simp
30.713 qed
30.714 qed
30.715 qed
30.716
30.717 -constdefs
30.718 +definition
30.719 bv_smult :: "[bit list, bit list] => bit list"
30.720 - "bv_smult w1 w2 == int_to_bv (bv_to_int w1 * bv_to_int w2)"
30.721 + "bv_smult w1 w2 = int_to_bv (bv_to_int w1 * bv_to_int w2)"
30.722
30.723 lemma bv_smult_type1 [simp]: "bv_smult (norm_signed w1) w2 = bv_smult w1 w2"
30.724 by (simp add: bv_smult_def)
30.725 @@ -1963,58 +1965,58 @@
30.726 assume bi1: "0 < bv_to_int w1"
30.727 assume bi2: "0 < bv_to_int w2"
30.728 show ?thesis
30.729 - apply (simp add: bv_smult_def)
30.730 - apply (rule length_int_to_bv_upper_limit_gt0)
30.731 - apply (rule p)
30.732 + apply (simp add: bv_smult_def)
30.733 + apply (rule length_int_to_bv_upper_limit_gt0)
30.734 + apply (rule p)
30.735 proof simp
30.736 - have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
30.737 - apply (rule mult_strict_mono)
30.738 - apply (rule bv_to_int_upper_range)
30.739 - apply (rule bv_to_int_upper_range)
30.740 - apply (rule zero_less_power)
30.741 - apply simp
30.742 - using bi2
30.743 - apply simp
30.744 - done
30.745 - also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
30.746 - apply simp
30.747 - apply (subst zpower_zadd_distrib [symmetric])
30.748 - apply simp
30.749 - apply arith
30.750 - done
30.751 - finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
30.752 - .
30.753 + have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
30.754 + apply (rule mult_strict_mono)
30.755 + apply (rule bv_to_int_upper_range)
30.756 + apply (rule bv_to_int_upper_range)
30.757 + apply (rule zero_less_power)
30.758 + apply simp
30.759 + using bi2
30.760 + apply simp
30.761 + done
30.762 + also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
30.763 + apply simp
30.764 + apply (subst zpower_zadd_distrib [symmetric])
30.765 + apply simp
30.766 + apply arith
30.767 + done
30.768 + finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
30.769 + .
30.770 qed
30.771 next
30.772 assume bi1: "bv_to_int w1 < 0"
30.773 assume bi2: "bv_to_int w2 < 0"
30.774 show ?thesis
30.775 - apply (simp add: bv_smult_def)
30.776 - apply (rule length_int_to_bv_upper_limit_gt0)
30.777 - apply (rule p)
30.778 + apply (simp add: bv_smult_def)
30.779 + apply (rule length_int_to_bv_upper_limit_gt0)
30.780 + apply (rule p)
30.781 proof simp
30.782 - have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
30.783 - apply (rule mult_mono)
30.784 - using bv_to_int_lower_range [of w1]
30.785 - apply simp
30.786 - using bv_to_int_lower_range [of w2]
30.787 - apply simp
30.788 - apply (rule zero_le_power,simp)
30.789 - using bi2
30.790 - apply simp
30.791 - done
30.792 - hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
30.793 - by simp
30.794 - also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
30.795 - apply simp
30.796 - apply (subst zpower_zadd_distrib [symmetric])
30.797 - apply simp
30.798 - apply (cut_tac lmw)
30.799 - apply arith
30.800 - apply (cut_tac p)
30.801 - apply arith
30.802 - done
30.803 - finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
30.804 + have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
30.805 + apply (rule mult_mono)
30.806 + using bv_to_int_lower_range [of w1]
30.807 + apply simp
30.808 + using bv_to_int_lower_range [of w2]
30.809 + apply simp
30.810 + apply (rule zero_le_power,simp)
30.811 + using bi2
30.812 + apply simp
30.813 + done
30.814 + hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
30.815 + by simp
30.816 + also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
30.817 + apply simp
30.818 + apply (subst zpower_zadd_distrib [symmetric])
30.819 + apply simp
30.820 + apply (cut_tac lmw)
30.821 + apply arith
30.822 + apply (cut_tac p)
30.823 + apply arith
30.824 + done
30.825 + finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
30.826 qed
30.827 qed
30.828 next
30.829 @@ -2025,60 +2027,60 @@
30.830 apply (rule p)
30.831 proof simp
30.832 have "(2::int) ^ (length w1 - 1) * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
30.833 - apply simp
30.834 - apply (subst zpower_zadd_distrib [symmetric])
30.835 - apply simp
30.836 - apply (cut_tac lmw)
30.837 - apply arith
30.838 - apply (cut_tac p)
30.839 - apply arith
30.840 - done
30.841 + apply simp
30.842 + apply (subst zpower_zadd_distrib [symmetric])
30.843 + apply simp
30.844 + apply (cut_tac lmw)
30.845 + apply arith
30.846 + apply (cut_tac p)
30.847 + apply arith
30.848 + done
30.849 hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
30.850 - by simp
30.851 + by simp
30.852 also have "... \<le> ?Q"
30.853 proof -
30.854 - from p
30.855 - have q: "bv_to_int w1 * bv_to_int w2 < 0"
30.856 - by simp
30.857 - thus ?thesis
30.858 - proof (simp add: mult_less_0_iff,safe)
30.859 - assume bi1: "0 < bv_to_int w1"
30.860 - assume bi2: "bv_to_int w2 < 0"
30.861 - have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
30.862 - apply (rule mult_mono)
30.863 - using bv_to_int_lower_range [of w2]
30.864 - apply simp
30.865 - using bv_to_int_upper_range [of w1]
30.866 - apply simp
30.867 - apply (rule zero_le_power,simp)
30.868 - using bi1
30.869 - apply simp
30.870 - done
30.871 - hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
30.872 - by (simp add: zmult_ac)
30.873 - thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
30.874 - by simp
30.875 - next
30.876 - assume bi1: "bv_to_int w1 < 0"
30.877 - assume bi2: "0 < bv_to_int w2"
30.878 - have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
30.879 - apply (rule mult_mono)
30.880 - using bv_to_int_lower_range [of w1]
30.881 - apply simp
30.882 - using bv_to_int_upper_range [of w2]
30.883 - apply simp
30.884 - apply (rule zero_le_power,simp)
30.885 - using bi2
30.886 - apply simp
30.887 - done
30.888 - hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
30.889 - by (simp add: zmult_ac)
30.890 - thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
30.891 - by simp
30.892 - qed
30.893 + from p
30.894 + have q: "bv_to_int w1 * bv_to_int w2 < 0"
30.895 + by simp
30.896 + thus ?thesis
30.897 + proof (simp add: mult_less_0_iff,safe)
30.898 + assume bi1: "0 < bv_to_int w1"
30.899 + assume bi2: "bv_to_int w2 < 0"
30.900 + have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
30.901 + apply (rule mult_mono)
30.902 + using bv_to_int_lower_range [of w2]
30.903 + apply simp
30.904 + using bv_to_int_upper_range [of w1]
30.905 + apply simp
30.906 + apply (rule zero_le_power,simp)
30.907 + using bi1
30.908 + apply simp
30.909 + done
30.910 + hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
30.911 + by (simp add: zmult_ac)
30.912 + thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
30.913 + by simp
30.914 + next
30.915 + assume bi1: "bv_to_int w1 < 0"
30.916 + assume bi2: "0 < bv_to_int w2"
30.917 + have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
30.918 + apply (rule mult_mono)
30.919 + using bv_to_int_lower_range [of w1]
30.920 + apply simp
30.921 + using bv_to_int_upper_range [of w2]
30.922 + apply simp
30.923 + apply (rule zero_le_power,simp)
30.924 + using bi2
30.925 + apply simp
30.926 + done
30.927 + hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
30.928 + by (simp add: zmult_ac)
30.929 + thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
30.930 + by simp
30.931 + qed
30.932 qed
30.933 finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q"
30.934 - .
30.935 + .
30.936 qed
30.937 qed
30.938 qed
30.939 @@ -2110,35 +2112,35 @@
30.940 proof (simp add: zero_less_mult_iff,safe)
30.941 assume biw2: "0 < bv_to_int w2"
30.942 show ?thesis
30.943 - apply (simp add: bv_smult_def)
30.944 - apply (rule length_int_to_bv_upper_limit_gt0)
30.945 - apply (rule p)
30.946 + apply (simp add: bv_smult_def)
30.947 + apply (rule length_int_to_bv_upper_limit_gt0)
30.948 + apply (rule p)
30.949 proof simp
30.950 - have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
30.951 - apply (rule mult_strict_mono)
30.952 - apply (simp add: bv_to_int_utos int_nat_two_exp)
30.953 - apply (rule bv_to_nat_upper_range)
30.954 - apply (rule bv_to_int_upper_range)
30.955 - apply (rule zero_less_power,simp)
30.956 - using biw2
30.957 - apply simp
30.958 - done
30.959 - also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
30.960 - apply simp
30.961 - apply (subst zpower_zadd_distrib [symmetric])
30.962 - apply simp
30.963 - apply (cut_tac lmw)
30.964 - apply arith
30.965 - using p
30.966 - apply auto
30.967 - done
30.968 - finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
30.969 - .
30.970 + have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
30.971 + apply (rule mult_strict_mono)
30.972 + apply (simp add: bv_to_int_utos int_nat_two_exp)
30.973 + apply (rule bv_to_nat_upper_range)
30.974 + apply (rule bv_to_int_upper_range)
30.975 + apply (rule zero_less_power,simp)
30.976 + using biw2
30.977 + apply simp
30.978 + done
30.979 + also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
30.980 + apply simp
30.981 + apply (subst zpower_zadd_distrib [symmetric])
30.982 + apply simp
30.983 + apply (cut_tac lmw)
30.984 + apply arith
30.985 + using p
30.986 + apply auto
30.987 + done
30.988 + finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
30.989 + .
30.990 qed
30.991 next
30.992 assume "bv_to_int (utos w1) < 0"
30.993 thus ?thesis
30.994 - by (simp add: bv_to_int_utos)
30.995 + by (simp add: bv_to_int_utos)
30.996 qed
30.997 next
30.998 assume p: "?Q = -1"
30.999 @@ -2156,48 +2158,48 @@
30.1000 apply (rule p)
30.1001 proof simp
30.1002 have "(2::int) ^ length w1 * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
30.1003 - apply simp
30.1004 - apply (subst zpower_zadd_distrib [symmetric])
30.1005 - apply simp
30.1006 - apply (cut_tac lmw)
30.1007 - apply arith
30.1008 - apply (cut_tac p)
30.1009 - apply arith
30.1010 - done
30.1011 + apply simp
30.1012 + apply (subst zpower_zadd_distrib [symmetric])
30.1013 + apply simp
30.1014 + apply (cut_tac lmw)
30.1015 + apply arith
30.1016 + apply (cut_tac p)
30.1017 + apply arith
30.1018 + done
30.1019 hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^ length w1 * 2 ^ (length w2 - 1))"
30.1020 - by simp
30.1021 + by simp
30.1022 also have "... \<le> ?Q"
30.1023 proof -
30.1024 - from p
30.1025 - have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
30.1026 - by simp
30.1027 - thus ?thesis
30.1028 - proof (simp add: mult_less_0_iff,safe)
30.1029 - assume bi1: "0 < bv_to_int (utos w1)"
30.1030 - assume bi2: "bv_to_int w2 < 0"
30.1031 - have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
30.1032 - apply (rule mult_mono)
30.1033 - using bv_to_int_lower_range [of w2]
30.1034 - apply simp
30.1035 - apply (simp add: bv_to_int_utos)
30.1036 - using bv_to_nat_upper_range [of w1]
30.1037 - apply (simp add: int_nat_two_exp)
30.1038 - apply (rule zero_le_power,simp)
30.1039 - using bi1
30.1040 - apply simp
30.1041 - done
30.1042 - hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))"
30.1043 - by (simp add: zmult_ac)
30.1044 - thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
30.1045 - by simp
30.1046 - next
30.1047 - assume bi1: "bv_to_int (utos w1) < 0"
30.1048 - thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
30.1049 - by (simp add: bv_to_int_utos)
30.1050 - qed
30.1051 + from p
30.1052 + have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
30.1053 + by simp
30.1054 + thus ?thesis
30.1055 + proof (simp add: mult_less_0_iff,safe)
30.1056 + assume bi1: "0 < bv_to_int (utos w1)"
30.1057 + assume bi2: "bv_to_int w2 < 0"
30.1058 + have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
30.1059 + apply (rule mult_mono)
30.1060 + using bv_to_int_lower_range [of w2]
30.1061 + apply simp
30.1062 + apply (simp add: bv_to_int_utos)
30.1063 + using bv_to_nat_upper_range [of w1]
30.1064 + apply (simp add: int_nat_two_exp)
30.1065 + apply (rule zero_le_power,simp)
30.1066 + using bi1
30.1067 + apply simp
30.1068 + done
30.1069 + hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))"
30.1070 + by (simp add: zmult_ac)
30.1071 + thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
30.1072 + by simp
30.1073 + next
30.1074 + assume bi1: "bv_to_int (utos w1) < 0"
30.1075 + thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
30.1076 + by (simp add: bv_to_int_utos)
30.1077 + qed
30.1078 qed
30.1079 finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q"
30.1080 - .
30.1081 + .
30.1082 qed
30.1083 qed
30.1084 qed
30.1085 @@ -2207,13 +2209,13 @@
30.1086
30.1087 subsection {* Structural operations *}
30.1088
30.1089 -constdefs
30.1090 +definition
30.1091 bv_select :: "[bit list,nat] => bit"
30.1092 - "bv_select w i == w ! (length w - 1 - i)"
30.1093 + "bv_select w i = w ! (length w - 1 - i)"
30.1094 bv_chop :: "[bit list,nat] => bit list * bit list"
30.1095 - "bv_chop w i == let len = length w in (take (len - i) w,drop (len - i) w)"
30.1096 + "bv_chop w i = (let len = length w in (take (len - i) w,drop (len - i) w))"
30.1097 bv_slice :: "[bit list,nat*nat] => bit list"
30.1098 - "bv_slice w == \<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e)"
30.1099 + "bv_slice w = (\<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e))"
30.1100
30.1101 lemma bv_select_rev:
30.1102 assumes notnull: "n < length w"
30.1103 @@ -2230,36 +2232,36 @@
30.1104 assume "xs = []"
30.1105 with notx
30.1106 show ?thesis
30.1107 - by simp
30.1108 + by simp
30.1109 next
30.1110 fix y ys
30.1111 assume [simp]: "xs = y # ys"
30.1112 show ?thesis
30.1113 proof (auto simp add: nth_append)
30.1114 - assume noty: "n < length ys"
30.1115 - from spec [OF ind,of ys]
30.1116 - have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
30.1117 - by simp
30.1118 - hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
30.1119 - ..
30.1120 - hence "ys ! (length ys - Suc n) = rev ys ! n"
30.1121 - ..
30.1122 - thus "(y # ys) ! (length ys - n) = rev ys ! n"
30.1123 - by (simp add: nth_Cons' noty linorder_not_less [symmetric])
30.1124 + assume noty: "n < length ys"
30.1125 + from spec [OF ind,of ys]
30.1126 + have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
30.1127 + by simp
30.1128 + hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
30.1129 + ..
30.1130 + hence "ys ! (length ys - Suc n) = rev ys ! n"
30.1131 + ..
30.1132 + thus "(y # ys) ! (length ys - n) = rev ys ! n"
30.1133 + by (simp add: nth_Cons' noty linorder_not_less [symmetric])
30.1134 next
30.1135 - assume "~ n < length ys"
30.1136 - hence x: "length ys \<le> n"
30.1137 - by simp
30.1138 - from notx
30.1139 - have "n < Suc (length ys)"
30.1140 - by simp
30.1141 - hence "n \<le> length ys"
30.1142 - by simp
30.1143 - with x
30.1144 - have "length ys = n"
30.1145 - by simp
30.1146 - thus "y = [y] ! (n - length ys)"
30.1147 - by simp
30.1148 + assume "~ n < length ys"
30.1149 + hence x: "length ys \<le> n"
30.1150 + by simp
30.1151 + from notx
30.1152 + have "n < Suc (length ys)"
30.1153 + by simp
30.1154 + hence "n \<le> length ys"
30.1155 + by simp
30.1156 + with x
30.1157 + have "length ys = n"
30.1158 + by simp
30.1159 + thus "y = [y] ! (n - length ys)"
30.1160 + by simp
30.1161 qed
30.1162 qed
30.1163 qed
30.1164 @@ -2284,9 +2286,9 @@
30.1165 lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
30.1166 by (auto simp add: bv_slice_def,arith)
30.1167
30.1168 -constdefs
30.1169 +definition
30.1170 length_nat :: "nat => nat"
30.1171 - "length_nat x == LEAST n. x < 2 ^ n"
30.1172 + "length_nat x = (LEAST n. x < 2 ^ n)"
30.1173
30.1174 lemma length_nat: "length (nat_to_bv n) = length_nat n"
30.1175 apply (simp add: length_nat_def)
30.1176 @@ -2316,9 +2318,12 @@
30.1177 apply (simp_all add: n0)
30.1178 done
30.1179
30.1180 -constdefs
30.1181 +definition
30.1182 length_int :: "int => nat"
30.1183 - "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)))"
30.1184 + "length_int x =
30.1185 + (if 0 < x then Suc (length_nat (nat x))
30.1186 + else if x = 0 then 0
30.1187 + else Suc (length_nat (nat (-x - 1))))"
30.1188
30.1189 lemma length_int: "length (int_to_bv i) = length_int i"
30.1190 proof (cases "0 < i")
30.1191 @@ -2410,12 +2415,11 @@
30.1192 shows "bv_slice w (j,i) = bv_slice (bv_slice w (l,k)) (j-k,i-k)"
30.1193 proof -
30.1194 def w1 == "fst (bv_chop w (Suc l))"
30.1195 - def w2 == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
30.1196 - def w3 == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
30.1197 - def w4 == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
30.1198 - def w5 == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
30.1199 -
30.1200 - note w_defs = w1_def w2_def w3_def w4_def w5_def
30.1201 + and w2 == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
30.1202 + and w3 == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
30.1203 + and w4 == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
30.1204 + and w5 == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
30.1205 + note w_defs = this
30.1206
30.1207 have w_def: "w = w1 @ w2 @ w3 @ w4 @ w5"
30.1208 by (simp add: w_defs append_bv_chop_id)
30.1209 @@ -2443,12 +2447,14 @@
30.1210 apply (simp add: bv_extend_def)
30.1211 apply (subst bv_to_nat_dist_append)
30.1212 apply simp
30.1213 - apply (induct "n - length w",simp_all)
30.1214 + apply (induct "n - length w")
30.1215 + apply simp_all
30.1216 done
30.1217
30.1218 lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b"
30.1219 apply (simp add: bv_extend_def)
30.1220 - apply (induct "n - length w",simp_all)
30.1221 + apply (induct "n - length w")
30.1222 + apply simp_all
30.1223 done
30.1224
30.1225 lemma bv_to_int_extend [simp]:
30.1226 @@ -2632,18 +2638,21 @@
30.1227 declare bv_to_nat1 [simp del]
30.1228 declare bv_to_nat_helper [simp del]
30.1229
30.1230 -constdefs
30.1231 +definition
30.1232 bv_mapzip :: "[bit => bit => bit,bit list, bit list] => bit list"
30.1233 - "bv_mapzip f w1 w2 == let g = bv_extend (max (length w1) (length w2)) \<zero>
30.1234 - in map (split f) (zip (g w1) (g w2))"
30.1235 + "bv_mapzip f w1 w2 =
30.1236 + (let g = bv_extend (max (length w1) (length w2)) \<zero>
30.1237 + in map (split f) (zip (g w1) (g w2)))"
30.1238
30.1239 -lemma bv_length_bv_mapzip [simp]: "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
30.1240 +lemma bv_length_bv_mapzip [simp]:
30.1241 + "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
30.1242 by (simp add: bv_mapzip_def Let_def split: split_max)
30.1243
30.1244 lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"
30.1245 by (simp add: bv_mapzip_def Let_def)
30.1246
30.1247 -lemma bv_mapzip_Cons [simp]: "length w1 = length w2 ==> bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
30.1248 +lemma bv_mapzip_Cons [simp]: "length w1 = length w2 ==>
30.1249 + bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
30.1250 by (simp add: bv_mapzip_def Let_def)
30.1251
30.1252 end
31.1 --- a/src/HOL/Library/Zorn.thy Sat May 27 17:42:00 2006 +0200
31.2 +++ b/src/HOL/Library/Zorn.thy Sat May 27 17:42:02 2006 +0200
31.3 @@ -15,24 +15,23 @@
31.4 \cite{Abrial-Laffitte}.
31.5 *}
31.6
31.7 -constdefs
31.8 +definition
31.9 chain :: "'a set set => 'a set set set"
31.10 - "chain S == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
31.11 + "chain S = {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
31.12
31.13 super :: "['a set set,'a set set] => 'a set set set"
31.14 - "super S c == {d. d \<in> chain S & c \<subset> d}"
31.15 + "super S c = {d. d \<in> chain S & c \<subset> d}"
31.16
31.17 maxchain :: "'a set set => 'a set set set"
31.18 - "maxchain S == {c. c \<in> chain S & super S c = {}}"
31.19 + "maxchain S = {c. c \<in> chain S & super S c = {}}"
31.20
31.21 succ :: "['a set set,'a set set] => 'a set set"
31.22 - "succ S c ==
31.23 - if c \<notin> chain S | c \<in> maxchain S
31.24 - then c else SOME c'. c' \<in> super S c"
31.25 + "succ S c =
31.26 + (if c \<notin> chain S | c \<in> maxchain S
31.27 + then c else SOME c'. c' \<in> super S c)"
31.28
31.29 consts
31.30 TFin :: "'a set set => 'a set set set"
31.31 -
31.32 inductive "TFin S"
31.33 intros
31.34 succI: "x \<in> TFin S ==> succ S x \<in> TFin S"
31.35 @@ -64,7 +63,7 @@
31.36 !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
31.37 !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
31.38 ==> P(n)"
31.39 - apply (erule TFin.induct)
31.40 + apply (induct set: TFin)
31.41 apply blast+
31.42 done
31.43
32.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy Sat May 27 17:42:00 2006 +0200
32.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy Sat May 27 17:42:02 2006 +0200
32.3 @@ -14,12 +14,12 @@
32.4
32.5 lemmas [elim?] = lub.least lub.upper
32.6
32.7 -constdefs
32.8 +definition
32.9 the_lub :: "'a::order set \<Rightarrow> 'a"
32.10 - "the_lub A \<equiv> The (lub A)"
32.11 + "the_lub A = The (lub A)"
32.12
32.13 -syntax (xsymbols)
32.14 - the_lub :: "'a::order set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90)
32.15 +const_syntax (xsymbols)
32.16 + the_lub ("\<Squnion>_" [90] 90)
32.17
32.18 lemma the_lub_equality [elim?]:
32.19 includes lub
33.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Sat May 27 17:42:00 2006 +0200
33.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Sat May 27 17:42:02 2006 +0200
33.3 @@ -22,9 +22,9 @@
33.4
33.5 types 'a graph = "('a \<times> real) set"
33.6
33.7 -constdefs
33.8 +definition
33.9 graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph"
33.10 - "graph F f \<equiv> {(x, f x) | x. x \<in> F}"
33.11 + "graph F f = {(x, f x) | x. x \<in> F}"
33.12
33.13 lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
33.14 by (unfold graph_def) blast
33.15 @@ -65,12 +65,12 @@
33.16 funct}.
33.17 *}
33.18
33.19 -constdefs
33.20 +definition
33.21 "domain" :: "'a graph \<Rightarrow> 'a set"
33.22 - "domain g \<equiv> {x. \<exists>y. (x, y) \<in> g}"
33.23 + "domain g = {x. \<exists>y. (x, y) \<in> g}"
33.24
33.25 funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)"
33.26 - "funct g \<equiv> \<lambda>x. (SOME y. (x, y) \<in> g)"
33.27 + "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
33.28
33.29 text {*
33.30 The following lemma states that @{text g} is the graph of a function
33.31 @@ -101,12 +101,12 @@
33.32 @{text p}, is defined as follows.
33.33 *}
33.34
33.35 -constdefs
33.36 +definition
33.37 norm_pres_extensions ::
33.38 "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
33.39 \<Rightarrow> 'a graph set"
33.40 "norm_pres_extensions E p F f
33.41 - \<equiv> {g. \<exists>H h. g = graph H h
33.42 + = {g. \<exists>H h. g = graph H h
33.43 \<and> linearform H h
33.44 \<and> H \<unlhd> E
33.45 \<and> F \<unlhd> H
34.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy Sat May 27 17:42:00 2006 +0200
34.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy Sat May 27 17:42:02 2006 +0200
34.3 @@ -22,11 +22,11 @@
34.4 and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
34.5 and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
34.6
34.7 +const_syntax (symbols)
34.8 + subspace (infix "\<unlhd>" 50)
34.9 +
34.10 declare vectorspace.intro [intro?] subspace.intro [intro?]
34.11
34.12 -syntax (symbols)
34.13 - subspace :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infix "\<unlhd>" 50)
34.14 -
34.15 lemma subspace_subset [elim]: "U \<unlhd> V \<Longrightarrow> U \<subseteq> V"
34.16 by (rule subspace.subset)
34.17
34.18 @@ -130,9 +130,9 @@
34.19 scalar multiples of @{text x}.
34.20 *}
34.21
34.22 -constdefs
34.23 +definition
34.24 lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set"
34.25 - "lin x \<equiv> {a \<cdot> x | a. True}"
34.26 + "lin x = {a \<cdot> x | a. True}"
34.27
34.28 lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x"
34.29 by (unfold lin_def) blast
35.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy Sat May 27 17:42:00 2006 +0200
35.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Sat May 27 17:42:02 2006 +0200
35.3 @@ -18,10 +18,10 @@
35.4 consts
35.5 prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70)
35.6
35.7 -syntax (xsymbols)
35.8 - prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
35.9 -syntax (HTML output)
35.10 - prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
35.11 +const_syntax (xsymbols)
35.12 + prod (infixr "\<cdot>" 70)
35.13 +const_syntax (HTML output)
35.14 + prod (infixr "\<cdot>" 70)
35.15
35.16
35.17 subsection {* Vector space laws *}
36.1 --- a/src/HOL/W0/W0.thy Sat May 27 17:42:00 2006 +0200
36.2 +++ b/src/HOL/W0/W0.thy Sat May 27 17:42:02 2006 +0200
36.3 @@ -11,9 +11,9 @@
36.4
36.5 datatype 'a maybe = Ok 'a | Fail
36.6
36.7 -constdefs
36.8 +definition
36.9 bind :: "'a maybe \<Rightarrow> ('a \<Rightarrow> 'b maybe) \<Rightarrow> 'b maybe" (infixl "\<bind>" 60)
36.10 - "m \<bind> f \<equiv> case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail"
36.11 + "m \<bind> f = (case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail)"
36.12
36.13 syntax
36.14 "_bind" :: "patterns \<Rightarrow> 'a maybe \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ := _;//_)" 0)
36.15 @@ -84,16 +84,16 @@
36.16 "free_tv [] = {}"
36.17 "free_tv (x # xs) = free_tv x \<union> free_tv xs"
36.18
36.19 -constdefs
36.20 +definition
36.21 dom :: "subst \<Rightarrow> nat set"
36.22 - "dom s \<equiv> {n. s n \<noteq> TVar n}"
36.23 + "dom s = {n. s n \<noteq> TVar n}"
36.24 -- {* domain of a substitution *}
36.25
36.26 cod :: "subst \<Rightarrow> nat set"
36.27 - "cod s \<equiv> \<Union>m \<in> dom s. free_tv (s m)"
36.28 + "cod s = (\<Union>m \<in> dom s. free_tv (s m))"
36.29 -- {* codomain of a substitutions: the introduced variables *}
36.30
36.31 -defs
36.32 +defs (overloaded)
36.33 free_tv_subst: "free_tv s \<equiv> dom s \<union> cod s"
36.34
36.35 text {*
36.36 @@ -102,16 +102,16 @@
36.37 than any type variable occuring in the type structure.
36.38 *}
36.39
36.40 -constdefs
36.41 +definition
36.42 new_tv :: "nat \<Rightarrow> 'a::type_struct \<Rightarrow> bool"
36.43 - "new_tv n ts \<equiv> \<forall>m. m \<in> free_tv ts \<longrightarrow> m < n"
36.44 + "new_tv n ts = (\<forall>m. m \<in> free_tv ts \<longrightarrow> m < n)"
36.45
36.46
36.47 subsubsection {* Identity substitution *}
36.48
36.49 -constdefs
36.50 +definition
36.51 id_subst :: subst
36.52 - "id_subst \<equiv> \<lambda>n. TVar n"
36.53 + "id_subst = (\<lambda>n. TVar n)"
36.54
36.55 lemma app_subst_id_te [simp]:
36.56 "$id_subst = (\<lambda>t::typ. t)"
36.57 @@ -218,35 +218,36 @@
36.58 by (induct x) simp_all
36.59
36.60 lemma subst_te_new_tv [simp]:
36.61 - "new_tv n (t::typ) \<longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
36.62 + "new_tv n (t::typ) \<Longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t"
36.63 -- {* substitution affects only variables occurring freely *}
36.64 by (induct t) simp_all
36.65
36.66 lemma subst_tel_new_tv [simp]:
36.67 - "new_tv n (ts::typ list) \<longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
36.68 + "new_tv n (ts::typ list) \<Longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
36.69 by (induct ts) simp_all
36.70
36.71 lemma new_tv_le: "n \<le> m \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv m t"
36.72 -- {* all greater variables are also new *}
36.73 proof (induct t)
36.74 case (TVar n)
36.75 - thus ?case by (auto intro: less_le_trans)
36.76 + then show ?case by (auto intro: less_le_trans)
36.77 next
36.78 case TFun
36.79 - thus ?case by simp
36.80 + then show ?case by simp
36.81 qed
36.82
36.83 lemma [simp]: "new_tv n t \<Longrightarrow> new_tv (Suc n) (t::typ)"
36.84 by (rule lessI [THEN less_imp_le [THEN new_tv_le]])
36.85
36.86 lemma new_tv_list_le:
36.87 - "n \<le> m \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
36.88 + assumes "n \<le> m"
36.89 + shows "new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
36.90 proof (induct ts)
36.91 case Nil
36.92 - thus ?case by simp
36.93 + then show ?case by simp
36.94 next
36.95 case Cons
36.96 - thus ?case by (auto intro: new_tv_le)
36.97 + with `n \<le> m` show ?case by (auto intro: new_tv_le)
36.98 qed
36.99
36.100 lemma [simp]: "new_tv n ts \<Longrightarrow> new_tv (Suc n) (ts::typ list)"
36.101 @@ -397,31 +398,27 @@
36.102 text {* Type assigment is closed wrt.\ substitution. *}
36.103
36.104 lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
36.105 -proof -
36.106 - assume "a |- e :: t"
36.107 - thus ?thesis (is "?P a e t")
36.108 - proof induct
36.109 - case (Var a n)
36.110 - hence "n < length (map ($ s) a)" by simp
36.111 - hence "map ($ s) a |- Var n :: map ($ s) a ! n"
36.112 - by (rule has_type.Var)
36.113 - also have "map ($ s) a ! n = $ s (a ! n)"
36.114 - by (rule nth_map)
36.115 - also have "map ($ s) a = $ s a"
36.116 - by (simp only: app_subst_list)
36.117 - finally show "?P a (Var n) (a ! n)" .
36.118 - next
36.119 - case (Abs a e t1 t2)
36.120 - hence "$ s t1 # map ($ s) a |- e :: $ s t2"
36.121 - by (simp add: app_subst_list)
36.122 - hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
36.123 - by (rule has_type.Abs)
36.124 - thus "?P a (Abs e) (t1 -> t2)"
36.125 - by (simp add: app_subst_list)
36.126 - next
36.127 - case App
36.128 - thus ?case by (simp add: has_type.App)
36.129 - qed
36.130 +proof (induct set: has_type)
36.131 + case (Var a n)
36.132 + then have "n < length (map ($ s) a)" by simp
36.133 + then have "map ($ s) a |- Var n :: map ($ s) a ! n"
36.134 + by (rule has_type.Var)
36.135 + also have "map ($ s) a ! n = $ s (a ! n)"
36.136 + by (rule nth_map)
36.137 + also have "map ($ s) a = $ s a"
36.138 + by (simp only: app_subst_list)
36.139 + finally show ?case .
36.140 +next
36.141 + case (Abs a e t1 t2)
36.142 + then have "$ s t1 # map ($ s) a |- e :: $ s t2"
36.143 + by (simp add: app_subst_list)
36.144 + then have "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
36.145 + by (rule has_type.Abs)
36.146 + then show ?case
36.147 + by (simp add: app_subst_list)
36.148 +next
36.149 + case App
36.150 + then show ?case by (simp add: has_type.App)
36.151 qed
36.152
36.153
36.154 @@ -442,52 +439,48 @@
36.155 u := mgu ($ s2 t1) (t2 -> TVar m2);
36.156 Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
36.157
36.158 -theorem W_correct: "!!a s t m n. Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
36.159 - (is "PROP ?P e")
36.160 -proof (induct e)
36.161 - fix a s t m n
36.162 - {
36.163 - fix i
36.164 - assume "Ok (s, t, m) = \<W> (Var i) a n"
36.165 - thus "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
36.166 - next
36.167 - fix e assume hyp: "PROP ?P e"
36.168 - assume "Ok (s, t, m) = \<W> (Abs e) a n"
36.169 - then obtain t' where "t = s n -> t'"
36.170 - and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
36.171 - by (auto split: bind_splits)
36.172 - with hyp show "$s a |- Abs e :: t"
36.173 - by (force intro: has_type.Abs)
36.174 - next
36.175 - fix e1 e2 assume hyp1: "PROP ?P e1" and hyp2: "PROP ?P e2"
36.176 - assume "Ok (s, t, m) = \<W> (App e1 e2) a n"
36.177 - then obtain s1 t1 n1 s2 t2 n2 u where
36.178 +theorem W_correct: "Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t"
36.179 +proof (induct e fixing: a s t m n)
36.180 + case (Var i)
36.181 + from `Ok (s, t, m) = \<W> (Var i) a n`
36.182 + show "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
36.183 +next
36.184 + case (Abs e)
36.185 + from `Ok (s, t, m) = \<W> (Abs e) a n`
36.186 + obtain t' where "t = s n -> t'"
36.187 + and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)"
36.188 + by (auto split: bind_splits)
36.189 + with Abs.hyps show "$s a |- Abs e :: t"
36.190 + by (force intro: has_type.Abs)
36.191 +next
36.192 + case (App e1 e2)
36.193 + from `Ok (s, t, m) = \<W> (App e1 e2) a n`
36.194 + obtain s1 t1 n1 s2 t2 n2 u where
36.195 s: "s = $u o $s2 o s1"
36.196 - and t: "t = u n2"
36.197 - and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
36.198 - and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
36.199 - and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
36.200 - by (auto split: bind_splits simp: that)
36.201 - show "$s a |- App e1 e2 :: t"
36.202 - proof (rule has_type.App)
36.203 - from s have s': "$u ($s2 ($s1 a)) = $s a"
36.204 - by (simp add: subst_comp_tel o_def)
36.205 - show "$s a |- e1 :: $u t2 -> t"
36.206 - proof -
36.207 - from W1_ok have "$s1 a |- e1 :: t1" by (rule hyp1)
36.208 - hence "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
36.209 - by (intro has_type_subst_closed)
36.210 - with s' t mgu_ok show ?thesis by simp
36.211 - qed
36.212 - show "$s a |- e2 :: $u t2"
36.213 - proof -
36.214 - from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule hyp2)
36.215 - hence "$u ($s2 ($s1 a)) |- e2 :: $u t2"
36.216 - by (rule has_type_subst_closed)
36.217 - with s' show ?thesis by simp
36.218 - qed
36.219 + and t: "t = u n2"
36.220 + and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
36.221 + and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n"
36.222 + and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1"
36.223 + by (auto split: bind_splits simp: that)
36.224 + show "$s a |- App e1 e2 :: t"
36.225 + proof (rule has_type.App)
36.226 + from s have s': "$u ($s2 ($s1 a)) = $s a"
36.227 + by (simp add: subst_comp_tel o_def)
36.228 + show "$s a |- e1 :: $u t2 -> t"
36.229 + proof -
36.230 + from W1_ok have "$s1 a |- e1 :: t1" by (rule App.hyps)
36.231 + then have "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
36.232 + by (intro has_type_subst_closed)
36.233 + with s' t mgu_ok show ?thesis by simp
36.234 qed
36.235 - }
36.236 + show "$s a |- e2 :: $u t2"
36.237 + proof -
36.238 + from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule App.hyps)
36.239 + then have "$u ($s2 ($s1 a)) |- e2 :: $u t2"
36.240 + by (rule has_type_subst_closed)
36.241 + with s' show ?thesis by simp
36.242 + qed
36.243 + qed
36.244 qed
36.245
36.246
37.1 --- a/src/HOL/ex/Adder.thy Sat May 27 17:42:00 2006 +0200
37.2 +++ b/src/HOL/ex/Adder.thy Sat May 27 17:42:02 2006 +0200
37.3 @@ -13,9 +13,9 @@
37.4 lemma bv_to_nat_helper': "bv \<noteq> [] ==> bv_to_nat bv = bitval (hd bv) * 2 ^ (length bv - 1) + bv_to_nat (tl bv)"
37.5 by (cases bv,simp_all add: bv_to_nat_helper)
37.6
37.7 -constdefs
37.8 +definition
37.9 half_adder :: "[bit,bit] => bit list"
37.10 - "half_adder a b == [a bitand b,a bitxor b]"
37.11 + "half_adder a b = [a bitand b,a bitxor b]"
37.12
37.13 lemma half_adder_correct: "bv_to_nat (half_adder a b) = bitval a + bitval b"
37.14 apply (simp add: half_adder_def)
37.15 @@ -26,10 +26,10 @@
37.16 lemma [simp]: "length (half_adder a b) = 2"
37.17 by (simp add: half_adder_def)
37.18
37.19 -constdefs
37.20 +definition
37.21 full_adder :: "[bit,bit,bit] => bit list"
37.22 - "full_adder a b c ==
37.23 - let x = a bitxor b in [a bitand b bitor c bitand x,x bitxor c]"
37.24 + "full_adder a b c =
37.25 + (let x = a bitxor b in [a bitand b bitor c bitand x,x bitxor c])"
37.26
37.27 lemma full_adder_correct:
37.28 "bv_to_nat (full_adder a b c) = bitval a + bitval b + bitval c"
38.1 --- a/src/HOL/ex/Fundefs.thy Sat May 27 17:42:00 2006 +0200
38.2 +++ b/src/HOL/ex/Fundefs.thy Sat May 27 17:42:02 2006 +0200
38.3 @@ -13,23 +13,23 @@
38.4 section {* Very basic *}
38.5
38.6 consts fib :: "nat \<Rightarrow> nat"
38.7 -function
38.8 +function
38.9 "fib 0 = 1"
38.10 "fib (Suc 0) = 1"
38.11 "fib (Suc (Suc n)) = fib n + fib (Suc n)"
38.12 -by pat_completeness (* shows that the patterns are complete *)
38.13 - auto (* shows that the patterns are compatible *)
38.14 +by pat_completeness -- {* shows that the patterns are complete *}
38.15 + auto -- {* shows that the patterns are compatible *}
38.16
38.17 -(* we get partial simp and induction rules: *)
38.18 +text {* we get partial simp and induction rules: *}
38.19 thm fib.psimps
38.20 thm fib.pinduct
38.21
38.22 -(* There is also a cases rule to distinguish cases along the definition *)
38.23 +text {* There is also a cases rule to distinguish cases along the definition *}
38.24 thm fib.cases
38.25
38.26 -(* Now termination: *)
38.27 +text {* Now termination: *}
38.28 termination fib
38.29 - by (auto_term "less_than")
38.30 + by (auto_term "less_than")
38.31
38.32 thm fib.simps
38.33 thm fib.induct
38.34 @@ -37,15 +37,15 @@
38.35
38.36 section {* Currying *}
38.37
38.38 -consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
38.39 +consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
38.40 function
38.41 "add 0 y = y"
38.42 "add (Suc x) y = Suc (add x y)"
38.43 by pat_completeness auto
38.44 -termination
38.45 +termination
38.46 by (auto_term "measure fst")
38.47
38.48 -thm add.induct (* Note the curried induction predicate *)
38.49 +thm add.induct -- {* Note the curried induction predicate *}
38.50
38.51
38.52 section {* Nested recursion *}
38.53 @@ -57,14 +57,14 @@
38.54 "nz (Suc x) = nz (nz x)"
38.55 by pat_completeness auto
38.56
38.57 -lemma nz_is_zero: (* A lemma we need to prove termination *)
38.58 +lemma nz_is_zero: -- {* A lemma we need to prove termination *}
38.59 assumes trm: "x \<in> nz_dom"
38.60 shows "nz x = 0"
38.61 using trm
38.62 by induct auto
38.63
38.64 termination nz
38.65 - apply (auto_term "less_than") (* Oops, it left us something to prove *)
38.66 + apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
38.67 by (auto simp:nz_is_zero)
38.68
38.69 thm nz.simps
38.70 @@ -73,13 +73,12 @@
38.71
38.72 section {* More general patterns *}
38.73
38.74 -(* Currently, patterns must always be compatible with each other, since
38.75 +text {* Currently, patterns must always be compatible with each other, since
38.76 no automatich splitting takes place. But the following definition of
38.77 -gcd is ok, although patterns overlap: *)
38.78 -
38.79 +gcd is ok, although patterns overlap: *}
38.80
38.81 consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
38.82 -function
38.83 +function
38.84 "gcd2 x 0 = x"
38.85 "gcd2 0 y = y"
38.86 "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
38.87 @@ -91,17 +90,17 @@
38.88 thm gcd2.induct
38.89
38.90
38.91 -(* General patterns allow even strange definitions: *)
38.92 +text {* General patterns allow even strange definitions: *}
38.93 consts ev :: "nat \<Rightarrow> bool"
38.94 -function
38.95 +function
38.96 "ev (2 * n) = True"
38.97 "ev (2 * n + 1) = False"
38.98 -proof - (* completeness is more difficult here. . . *)
38.99 +proof - -- {* completeness is more difficult here \dots *}
38.100 assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
38.101 and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
38.102 have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto
38.103 show "P"
38.104 - proof cases
38.105 + proof cases
38.106 assume "x mod 2 = 0"
38.107 with divmod have "x = 2 * (x div 2)" by simp
38.108 with c1 show "P" .
38.109 @@ -111,15 +110,11 @@
38.110 with divmod have "x = 2 * (x div 2) + 1" by simp
38.111 with c2 show "P" .
38.112 qed
38.113 -qed presburger+ (* solve compatibility with presburger *)
38.114 +qed presburger+ -- {* solve compatibility with presburger *}
38.115 termination by (auto_term "{}")
38.116
38.117 thm ev.simps
38.118 thm ev.induct
38.119 thm ev.cases
38.120
38.121 -
38.122 -
38.123 -
38.124 -
38.125 -end
38.126 \ No newline at end of file
38.127 +end
39.1 --- a/src/HOL/ex/Higher_Order_Logic.thy Sat May 27 17:42:00 2006 +0200
39.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy Sat May 27 17:42:02 2006 +0200
39.3 @@ -79,7 +79,7 @@
39.4
39.5 subsubsection {* Derived connectives *}
39.6
39.7 -constdefs
39.8 +definition
39.9 false :: o ("\<bottom>")
39.10 "\<bottom> \<equiv> \<forall>A. A"
39.11 true :: o ("\<top>")
40.1 --- a/src/HOL/ex/InductiveInvariant.thy Sat May 27 17:42:00 2006 +0200
40.2 +++ b/src/HOL/ex/InductiveInvariant.thy Sat May 27 17:42:02 2006 +0200
40.3 @@ -14,14 +14,16 @@
40.4
40.5 text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
40.6
40.7 -constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
40.8 - "indinv r S F == \<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x)"
40.9 +definition
40.10 + indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
40.11 + "indinv r S F = (\<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x))"
40.12
40.13
40.14 text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."
40.15
40.16 -constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
40.17 - "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)"
40.18 +definition
40.19 + indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
40.20 + "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))"
40.21
40.22
40.23 text "The key theorem, corresponding to theorem 1 of the paper. All other results
40.24 @@ -29,15 +31,16 @@
40.25 derived from this theorem."
40.26
40.27 theorem indinv_wfrec:
40.28 - assumes WF: "wf r" and
40.29 - INV: "indinv r S F"
40.30 + assumes wf: "wf r" and
40.31 + inv: "indinv r S F"
40.32 shows "S x (wfrec r F x)"
40.33 -proof (induct_tac x rule: wf_induct [OF WF])
40.34 + using wf
40.35 +proof (induct x)
40.36 fix x
40.37 - assume IHYP: "\<forall>y. (y,x) \<in> r --> S y (wfrec r F y)"
40.38 - then have "\<forall>y. (y,x) \<in> r --> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
40.39 - with INV have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
40.40 - thus "S x (wfrec r F x)" using WF by (simp add: wfrec)
40.41 + assume IHYP: "!!y. (y,x) \<in> r \<Longrightarrow> S y (wfrec r F y)"
40.42 + then have "!!y. (y,x) \<in> r \<Longrightarrow> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
40.43 + with inv have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
40.44 + thus "S x (wfrec r F x)" using wf by (simp add: wfrec)
40.45 qed
40.46
40.47 theorem indinv_on_wfrec:
41.1 --- a/src/HOL/ex/Lagrange.thy Sat May 27 17:42:00 2006 +0200
41.2 +++ b/src/HOL/ex/Lagrange.thy Sat May 27 17:42:02 2006 +0200
41.3 @@ -16,8 +16,9 @@
41.4 The enterprising reader might consider proving all of Lagrange's
41.5 theorem. *}
41.6
41.7 -constdefs sq :: "'a::times => 'a"
41.8 - "sq x == x*x"
41.9 +definition
41.10 + sq :: "'a::times => 'a"
41.11 + "sq x == x*x"
41.12
41.13 text {* The following lemma essentially shows that every natural
41.14 number is the sum of four squares, provided all prime numbers are.
41.15 @@ -26,7 +27,6 @@
41.16
41.17 ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]"
41.18
41.19 --- {* once a slow step, but now (2001) just three seconds! *}
41.20 lemma Lagrange_lemma:
41.21 "!!x1::'a::comm_ring.
41.22 (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
42.1 --- a/src/HOL/ex/MonoidGroup.thy Sat May 27 17:42:00 2006 +0200
42.2 +++ b/src/HOL/ex/MonoidGroup.thy Sat May 27 17:42:02 2006 +0200
42.3 @@ -14,17 +14,17 @@
42.4 record 'a group_sig = "'a monoid_sig" +
42.5 inv :: "'a => 'a"
42.6
42.7 -constdefs
42.8 +definition
42.9 monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"
42.10 - "monoid M == \<forall>x y z.
42.11 + "monoid M = (\<forall>x y z.
42.12 times M (times M x y) z = times M x (times M y z) \<and>
42.13 - times M (one M) x = x \<and> times M x (one M) = x"
42.14 + times M (one M) x = x \<and> times M x (one M) = x)"
42.15
42.16 group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool"
42.17 - "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"
42.18 + "group G = (monoid G \<and> (\<forall>x. times G (inv G x) x = one G))"
42.19
42.20 reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
42.21 (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
42.22 - "reverse M == M (| times := \<lambda>x y. times M y x |)"
42.23 + "reverse M = M (| times := \<lambda>x y. times M y x |)"
42.24
42.25 end
43.1 --- a/src/HOL/ex/PER.thy Sat May 27 17:42:00 2006 +0200
43.2 +++ b/src/HOL/ex/PER.thy Sat May 27 17:42:02 2006 +0200
43.3 @@ -44,9 +44,9 @@
43.4 \emph{any} other one.
43.5 *}
43.6
43.7 -constdefs
43.8 - domain :: "'a::partial_equiv set"
43.9 - "domain == {x. x \<sim> x}"
43.10 +definition
43.11 + "domain" :: "'a::partial_equiv set"
43.12 + "domain = {x. x \<sim> x}"
43.13
43.14 lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
43.15 by (unfold domain_def) blast
43.16 @@ -164,9 +164,9 @@
43.17 representation of elements of a quotient type.
43.18 *}
43.19
43.20 -constdefs
43.21 +definition
43.22 eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>")
43.23 - "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
43.24 + "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
43.25
43.26 theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
43.27 proof (cases A)
43.28 @@ -231,9 +231,9 @@
43.29
43.30 subsection {* Picking representing elements *}
43.31
43.32 -constdefs
43.33 +definition
43.34 pick :: "'a::partial_equiv quot => 'a"
43.35 - "pick A == SOME a. A = \<lfloor>a\<rfloor>"
43.36 + "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
43.37
43.38 theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a"
43.39 proof (unfold pick_def)
44.1 --- a/src/HOL/ex/Primrec.thy Sat May 27 17:42:00 2006 +0200
44.2 +++ b/src/HOL/ex/Primrec.thy Sat May 27 17:42:02 2006 +0200
44.3 @@ -42,24 +42,24 @@
44.4
44.5 text {* The set of primitive recursive functions of type @{typ "nat list => nat"}. *}
44.6
44.7 -constdefs
44.8 +definition
44.9 SC :: "nat list => nat"
44.10 - "SC l == Suc (zeroHd l)"
44.11 + "SC l = Suc (zeroHd l)"
44.12
44.13 CONSTANT :: "nat => nat list => nat"
44.14 - "CONSTANT k l == k"
44.15 + "CONSTANT k l = k"
44.16
44.17 PROJ :: "nat => nat list => nat"
44.18 - "PROJ i l == zeroHd (drop i l)"
44.19 + "PROJ i l = zeroHd (drop i l)"
44.20
44.21 COMP :: "(nat list => nat) => (nat list => nat) list => nat list => nat"
44.22 - "COMP g fs l == g (map (\<lambda>f. f l) fs)"
44.23 + "COMP g fs l = g (map (\<lambda>f. f l) fs)"
44.24
44.25 PREC :: "(nat list => nat) => (nat list => nat) => nat list => nat"
44.26 - "PREC f g l ==
44.27 - case l of
44.28 + "PREC f g l =
44.29 + (case l of
44.30 [] => 0
44.31 - | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x"
44.32 + | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x)"
44.33 -- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *}
44.34
44.35 consts PRIMREC :: "(nat list => nat) set"
45.1 --- a/src/HOL/ex/Records.thy Sat May 27 17:42:00 2006 +0200
45.2 +++ b/src/HOL/ex/Records.thy Sat May 27 17:42:02 2006 +0200
45.3 @@ -50,11 +50,11 @@
45.4
45.5 subsubsection {* Record selection and record update *}
45.6
45.7 -constdefs
45.8 +definition
45.9 getX :: "'a point_scheme => nat"
45.10 - "getX r == xpos r"
45.11 + "getX r = xpos r"
45.12 setX :: "'a point_scheme => nat => 'a point_scheme"
45.13 - "setX r n == r (| xpos := n |)"
45.14 + "setX r n = r (| xpos := n |)"
45.15
45.16
45.17 subsubsection {* Some lemmas about records *}
45.18 @@ -144,16 +144,16 @@
45.19 \medskip Concrete records are type instances of record schemes.
45.20 *}
45.21
45.22 -constdefs
45.23 +definition
45.24 foo5 :: nat
45.25 - "foo5 == getX (| xpos = 1, ypos = 0 |)"
45.26 + "foo5 = getX (| xpos = 1, ypos = 0 |)"
45.27
45.28
45.29 text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *}
45.30
45.31 -constdefs
45.32 +definition
45.33 incX :: "'a point_scheme => 'a point_scheme"
45.34 - "incX r == (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
45.35 + "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
45.36
45.37 lemma "incX r = setX r (Suc (getX r))"
45.38 by (simp add: getX_def setX_def incX_def)
45.39 @@ -161,9 +161,9 @@
45.40
45.41 text {* An alternative definition. *}
45.42
45.43 -constdefs
45.44 +definition
45.45 incX' :: "'a point_scheme => 'a point_scheme"
45.46 - "incX' r == r (| xpos := xpos r + 1 |)"
45.47 + "incX' r = r (| xpos := xpos r + 1 |)"
45.48
45.49
45.50 subsection {* Coloured points: record extension *}
45.51 @@ -193,9 +193,9 @@
45.52 Functions on @{text point} schemes work for @{text cpoints} as well.
45.53 *}
45.54
45.55 -constdefs
45.56 +definition
45.57 foo10 :: nat
45.58 - "foo10 == getX (| xpos = 2, ypos = 0, colour = Blue |)"
45.59 + "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
45.60
45.61
45.62 subsubsection {* Non-coercive structural subtyping *}
45.63 @@ -205,9 +205,9 @@
45.64 Great!
45.65 *}
45.66
45.67 -constdefs
45.68 +definition
45.69 foo11 :: cpoint
45.70 - "foo11 == setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
45.71 + "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
45.72
45.73
45.74 subsection {* Other features *}
46.1 --- a/src/HOL/ex/Reflected_Presburger.thy Sat May 27 17:42:00 2006 +0200
46.2 +++ b/src/HOL/ex/Reflected_Presburger.thy Sat May 27 17:42:02 2006 +0200
46.3 @@ -529,8 +529,9 @@
46.4 "islintn (n0, Add (Mult (Cst i) (Var n)) r) = (i \<noteq> 0 \<and> n0 \<le> n \<and> islintn (n+1,r))"
46.5 "islintn (n0, t) = False"
46.6
46.7 -constdefs islint :: "intterm \<Rightarrow> bool"
46.8 - "islint t \<equiv> islintn(0,t)"
46.9 +definition
46.10 + islint :: "intterm \<Rightarrow> bool"
46.11 + "islint t = islintn(0,t)"
46.12
46.13 (* And the equivalence to the first definition *)
46.14 lemma islinintterm_eq_islint: "islinintterm t = islint t"
46.15 @@ -728,8 +729,9 @@
46.16 by (induct l t rule: lin_mul.induct) simp_all
46.17
46.18 (* lin_neg neagtes a linear term *)
46.19 -constdefs lin_neg :: "intterm \<Rightarrow> intterm"
46.20 -"lin_neg i == lin_mul ((-1::int),i)"
46.21 +definition
46.22 + lin_neg :: "intterm \<Rightarrow> intterm"
46.23 + "lin_neg i = lin_mul ((-1::int),i)"
46.24
46.25 (* lin_neg has the semantics of Neg *)
46.26 lemma lin_neg_corr:
46.27 @@ -1622,11 +1624,13 @@
46.28 by simp
46.29
46.30 (* Definitions and lemmas about gcd and lcm *)
46.31 -constdefs lcm :: "nat \<times> nat \<Rightarrow> nat"
46.32 - "lcm \<equiv> (\<lambda>(m,n). m*n div gcd(m,n))"
46.33 -
46.34 -constdefs ilcm :: "int \<Rightarrow> int \<Rightarrow> int"
46.35 - "ilcm \<equiv> \<lambda>i.\<lambda>j. int (lcm(nat(abs i),nat(abs j)))"
46.36 +definition
46.37 + lcm :: "nat \<times> nat \<Rightarrow> nat"
46.38 + "lcm = (\<lambda>(m,n). m*n div gcd(m,n))"
46.39 +
46.40 +definition
46.41 + ilcm :: "int \<Rightarrow> int \<Rightarrow> int"
46.42 + "ilcm = (\<lambda>i.\<lambda>j. int (lcm(nat(abs i),nat(abs j))))"
46.43
46.44 (* ilcm_dvd12 are needed later *)
46.45 lemma lcm_dvd1:
46.46 @@ -1874,8 +1878,9 @@
46.47
46.48
46.49 (* unitycoeff expects a quantifier free formula an transforms it to an equivalent formula where the bound variable occurs only with coeffitient 1 or -1 *)
46.50 -constdefs unitycoeff :: "QF \<Rightarrow> QF"
46.51 - "unitycoeff p ==
46.52 +definition
46.53 + unitycoeff :: "QF \<Rightarrow> QF"
46.54 + "unitycoeff p =
46.55 (let l = formlcm p;
46.56 p' = adjustcoeff (l,p)
46.57 in (if l=1 then p' else
46.58 @@ -5085,8 +5090,9 @@
46.59
46.60
46.61 (* An implementation of sets trough lists *)
46.62 -constdefs list_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
46.63 - "list_insert x xs \<equiv> (if x mem xs then xs else x#xs)"
46.64 +definition
46.65 + list_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
46.66 + "list_insert x xs = (if x mem xs then xs else x#xs)"
46.67
46.68 lemma list_insert_set: "set (list_insert x xs) = set (x#xs)"
46.69 by(induct xs) (auto simp add: list_insert_def)
46.70 @@ -5362,8 +5368,8 @@
46.71 (* An implementation of cooper's method for both plus/minus/infinity *)
46.72
46.73 (* unify the formula *)
46.74 -constdefs unify:: "QF \<Rightarrow> (QF \<times> intterm list)"
46.75 - "unify p \<equiv>
46.76 +definition unify:: "QF \<Rightarrow> (QF \<times> intterm list)"
46.77 + "unify p =
46.78 (let q = unitycoeff p;
46.79 B = list_set(bset q);
46.80 A = list_set (aset q)
46.81 @@ -5477,8 +5483,9 @@
46.82 using qB_def by simp
46.83 qed
46.84 (* An implementation of cooper's method *)
46.85 -constdefs cooper:: "QF \<Rightarrow> QF option"
46.86 -"cooper p \<equiv> lift_un (\<lambda>q. decrvars(explode_minf (unify q))) (linform (nnf p))"
46.87 +definition
46.88 + cooper:: "QF \<Rightarrow> QF option"
46.89 + "cooper p = lift_un (\<lambda>q. decrvars(explode_minf (unify q))) (linform (nnf p))"
46.90
46.91 (* cooper eliminates quantifiers *)
46.92 lemma cooper_qfree: "(\<And> q q'. \<lbrakk>isqfree q ; cooper q = Some q'\<rbrakk> \<Longrightarrow> isqfree q')"
46.93 @@ -5530,8 +5537,9 @@
46.94 qed
46.95
46.96 (* A decision procedure for Presburger Arithmetics *)
46.97 -constdefs pa:: "QF \<Rightarrow> QF option"
46.98 -"pa p \<equiv> lift_un psimpl (qelim(cooper, p))"
46.99 +definition
46.100 + pa:: "QF \<Rightarrow> QF option"
46.101 + "pa p \<equiv> lift_un psimpl (qelim(cooper, p))"
46.102
46.103 lemma psimpl_qfree: "isqfree p \<Longrightarrow> isqfree (psimpl p)"
46.104 apply(induct p rule: isqfree.induct)
47.1 --- a/src/HOL/ex/Sorting.thy Sat May 27 17:42:00 2006 +0200
47.2 +++ b/src/HOL/ex/Sorting.thy Sat May 27 17:42:02 2006 +0200
47.3 @@ -24,12 +24,12 @@
47.4 "sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)"
47.5
47.6
47.7 -constdefs
47.8 +definition
47.9 total :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
47.10 - "total r == (\<forall>x y. r x y | r y x)"
47.11 + "total r = (\<forall>x y. r x y | r y x)"
47.12
47.13 transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
47.14 - "transf f == (\<forall>x y z. f x y & f y z --> f x z)"
47.15 + "transf f = (\<forall>x y z. f x y & f y z --> f x z)"
47.16
47.17
47.18
47.19 @@ -44,8 +44,8 @@
47.20 done
47.21
47.22 lemma sorted_append [simp]:
47.23 - "sorted le (xs@ys) =
47.24 - (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
47.25 -by (induct xs, auto)
47.26 + "sorted le (xs@ys) =
47.27 + (sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
47.28 + by (induct xs) auto
47.29
47.30 end
48.1 --- a/src/HOL/ex/Tarski.thy Sat May 27 17:42:00 2006 +0200
48.2 +++ b/src/HOL/ex/Tarski.thy Sat May 27 17:42:02 2006 +0200
48.3 @@ -20,79 +20,77 @@
48.4 pset :: "'a set"
48.5 order :: "('a * 'a) set"
48.6
48.7 -constdefs
48.8 +definition
48.9 monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
48.10 - "monotone f A r == \<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r"
48.11 + "monotone f A r = (\<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r)"
48.12
48.13 least :: "['a => bool, 'a potype] => 'a"
48.14 - "least P po == @ x. x: pset po & P x &
48.15 - (\<forall>y \<in> pset po. P y --> (x,y): order po)"
48.16 + "least P po = (SOME x. x: pset po & P x &
48.17 + (\<forall>y \<in> pset po. P y --> (x,y): order po))"
48.18
48.19 greatest :: "['a => bool, 'a potype] => 'a"
48.20 - "greatest P po == @ x. x: pset po & P x &
48.21 - (\<forall>y \<in> pset po. P y --> (y,x): order po)"
48.22 + "greatest P po = (SOME x. x: pset po & P x &
48.23 + (\<forall>y \<in> pset po. P y --> (y,x): order po))"
48.24
48.25 lub :: "['a set, 'a potype] => 'a"
48.26 - "lub S po == least (%x. \<forall>y\<in>S. (y,x): order po) po"
48.27 + "lub S po = least (%x. \<forall>y\<in>S. (y,x): order po) po"
48.28
48.29 glb :: "['a set, 'a potype] => 'a"
48.30 - "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
48.31 + "glb S po = greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
48.32
48.33 isLub :: "['a set, 'a potype, 'a] => bool"
48.34 - "isLub S po == %L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
48.35 - (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po))"
48.36 + "isLub S po = (%L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
48.37 + (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po)))"
48.38
48.39 isGlb :: "['a set, 'a potype, 'a] => bool"
48.40 - "isGlb S po == %G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
48.41 - (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po))"
48.42 + "isGlb S po = (%G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
48.43 + (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po)))"
48.44
48.45 "fix" :: "[('a => 'a), 'a set] => 'a set"
48.46 - "fix f A == {x. x: A & f x = x}"
48.47 + "fix f A = {x. x: A & f x = x}"
48.48
48.49 interval :: "[('a*'a) set,'a, 'a ] => 'a set"
48.50 - "interval r a b == {x. (a,x): r & (x,b): r}"
48.51 + "interval r a b = {x. (a,x): r & (x,b): r}"
48.52
48.53
48.54 -constdefs
48.55 +definition
48.56 Bot :: "'a potype => 'a"
48.57 - "Bot po == least (%x. True) po"
48.58 + "Bot po = least (%x. True) po"
48.59
48.60 Top :: "'a potype => 'a"
48.61 - "Top po == greatest (%x. True) po"
48.62 + "Top po = greatest (%x. True) po"
48.63
48.64 PartialOrder :: "('a potype) set"
48.65 - "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) &
48.66 + "PartialOrder = {P. refl (pset P) (order P) & antisym (order P) &
48.67 trans (order P)}"
48.68
48.69 CompleteLattice :: "('a potype) set"
48.70 - "CompleteLattice == {cl. cl: PartialOrder &
48.71 + "CompleteLattice = {cl. cl: PartialOrder &
48.72 (\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) &
48.73 (\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}"
48.74
48.75 CLF :: "('a potype * ('a => 'a)) set"
48.76 - "CLF == SIGMA cl: CompleteLattice.
48.77 - {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)}"
48.78 + "CLF = (SIGMA cl: CompleteLattice.
48.79 + {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
48.80
48.81 induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
48.82 - "induced A r == {(a,b). a : A & b: A & (a,b): r}"
48.83 + "induced A r = {(a,b). a : A & b: A & (a,b): r}"
48.84
48.85
48.86 -constdefs
48.87 +definition
48.88 sublattice :: "('a potype * 'a set)set"
48.89 - "sublattice ==
48.90 - SIGMA cl: CompleteLattice.
48.91 + "sublattice =
48.92 + (SIGMA cl: CompleteLattice.
48.93 {S. S \<subseteq> pset cl &
48.94 - (| pset = S, order = induced S (order cl) |): CompleteLattice }"
48.95 + (| pset = S, order = induced S (order cl) |): CompleteLattice})"
48.96
48.97 -syntax
48.98 - "@SL" :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
48.99 +abbreviation
48.100 + sublat :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
48.101 + "S <<= cl == S : sublattice `` {cl}"
48.102
48.103 -translations
48.104 - "S <<= cl" == "S : sublattice `` {cl}"
48.105 -
48.106 -constdefs
48.107 +definition
48.108 dual :: "'a potype => 'a potype"
48.109 - "dual po == (| pset = pset po, order = converse (order po) |)"
48.110 + "dual po = (| pset = pset po, order = converse (order po) |)"
48.111
48.112 locale (open) PO =
48.113 fixes cl :: "'a potype"
49.1 --- a/src/HOL/ex/ThreeDivides.thy Sat May 27 17:42:00 2006 +0200
49.2 +++ b/src/HOL/ex/ThreeDivides.thy Sat May 27 17:42:02 2006 +0200
49.3 @@ -155,9 +155,9 @@
49.4 text {* The function @{text "sumdig"} returns the sum of all digits in
49.5 some number n. *}
49.6
49.7 -constdefs
49.8 +definition
49.9 sumdig :: "nat \<Rightarrow> nat"
49.10 - "sumdig n \<equiv> \<Sum>x < nlen n. n div 10^x mod 10"
49.11 + "sumdig n = (\<Sum>x < nlen n. n div 10^x mod 10)"
49.12
49.13 text {* Some properties of these functions follow. *}
49.14