tuned;
authorwenzelm
Sat May 27 17:42:02 2006 +0200 (2006-05-27)
changeset 19736d8d0f8f51d69
parent 19735 ff13585fbdab
child 19737 3b8920131be2
tuned;
TFL/post.ML
src/HOL/Complex/ex/NSPrimes.thy
src/HOL/Complex/ex/Sqrt_Script.thy
src/HOL/Induct/Com.thy
src/HOL/Induct/Comb.thy
src/HOL/Induct/LFilter.thy
src/HOL/Induct/LList.thy
src/HOL/Induct/Mutil.thy
src/HOL/Induct/Ordinals.thy
src/HOL/Induct/PropLog.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Induct/SList.thy
src/HOL/Induct/Sexp.thy
src/HOL/Induct/Tree.thy
src/HOL/Lattice/Bounds.thy
src/HOL/Lattice/CompleteLattice.thy
src/HOL/Lattice/Lattice.thy
src/HOL/Lattice/Orders.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/NatPair.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Product_ord.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Library/Word.thy
src/HOL/Library/Zorn.thy
src/HOL/Real/HahnBanach/Bounds.thy
src/HOL/Real/HahnBanach/FunctionOrder.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/HOL/W0/W0.thy
src/HOL/ex/Adder.thy
src/HOL/ex/Fundefs.thy
src/HOL/ex/Higher_Order_Logic.thy
src/HOL/ex/InductiveInvariant.thy
src/HOL/ex/Lagrange.thy
src/HOL/ex/MonoidGroup.thy
src/HOL/ex/PER.thy
src/HOL/ex/Primrec.thy
src/HOL/ex/Records.thy
src/HOL/ex/Reflected_Presburger.thy
src/HOL/ex/Sorting.thy
src/HOL/ex/Tarski.thy
src/HOL/ex/ThreeDivides.thy
     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 -
     2.8 -constdefs
     2.9 +definition
    2.10    hdvd  :: "[hypnat, hypnat] => bool"       (infixl "hdvd" 50)
    2.11 -   "(M::hypnat) hdvd N == ( *p2* (op dvd)) M N"
    2.12 -
    2.13 -declare hdvd_def [transfer_unfold]
    2.14 +  [transfer_unfold]: "(M::hypnat) hdvd N = ( *p2* (op dvd)) M N"
    2.15  
    2.16 -constdefs
    2.17    starprime :: "hypnat set"
    2.18 -  "starprime == ( *s* {p. prime p})"
    2.19 +  [transfer_unfold]: "starprime = ( *s* {p. prime p})"
    2.20  
    2.21 -declare starprime_def [transfer_unfold]
    2.22 -
    2.23 -constdefs
    2.24    choicefun :: "'a set => 'a"
    2.25 -  "choicefun E == (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
    2.26 +  "choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
    2.27  
    2.28  consts injf_max :: "nat => ('a::{order} set) => 'a"
    2.29  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  
    4.12 -syntax  eval'   :: "[exp*state,nat*state] =>
    4.13 -                    ((exp*state) * (nat*state)) set => bool"
    4.14 -                                           ("_/ -|[_]-> _" [50,0,50] 50)
    4.15 +abbreviation
    4.16 +  exec_rel  ("_/ -[_]-> _" [50,0,50] 50)
    4.17 +  "csig -[eval]-> s == (csig,s) \<in> exec eval"
    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 -
   26.19 -syntax (xsymbols)
   26.20 -  Infty :: inat    ("\<infinity>")
   26.21 +  "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<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,10 +22,10 @@
    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 -declare vectorspace.intro [intro?] subspace.intro [intro?]
    34.8 +const_syntax (symbols)
    34.9 +  subspace  (infix "\<unlhd>" 50)
   34.10  
   34.11 -syntax (symbols)
   34.12 -  subspace :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"    (infix "\<unlhd>" 50)
   34.13 +declare vectorspace.intro [intro?] subspace.intro [intro?]
   34.14  
   34.15  lemma subspace_subset [elim]: "U \<unlhd> V \<Longrightarrow> U \<subseteq> V"
   34.16    by (rule subspace.subset)
   34.17 @@ -130,9 +130,9 @@
   34.18    scalar multiples of @{text x}.
   34.19  *}
   34.20  
   34.21 -constdefs
   34.22 +definition
   34.23    lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set"
   34.24 -  "lin x \<equiv> {a \<cdot> x | a. True}"
   34.25 +  "lin x = {a \<cdot> x | a. True}"
   34.26  
   34.27  lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x"
   34.28    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