# HG changeset patch
# User haftmann
# Date 1276350497 -7200
# Node ID 6c9f23863808483d70310b4374751b4637c61ba9
# Parent  e6b1a0693f3fc89cec345e278276254045639230# Parent  f51ff37811bfabd9b96dd95cef1ccd295dfb9113
merged

diff -r e6b1a0693f3f -r 6c9f23863808 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Sat Jun 12 11:12:54 2010 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy	Sat Jun 12 15:48:17 2010 +0200
@@ -244,30 +244,30 @@
 lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m"
 by (cases m) (simp add: mhead_def member_is_static_simp)
 
-constdefs  --{* some mnemotic selectors for various pairs *} 
-           
- "decliface":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> qtname"
- "decliface \<equiv> fst"          --{* get the interface component *}
+-- {* some mnemotic selectors for various pairs *} 
+
+definition decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
+  "decliface = fst"          --{* get the interface component *}
 
- "mbr"::   "(qtname \<times> memberdecl) \<Rightarrow> memberdecl"
- "mbr \<equiv> snd"            --{* get the memberdecl component *}
+definition mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
+  "mbr = snd"            --{* get the memberdecl component *}
 
- "mthd"::   "('b \<times> 'a) \<Rightarrow> 'a"
-                           --{* also used for mdecl, mhead *}
- "mthd \<equiv> snd"              --{* get the method component *}
+definition mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
+  "mthd = snd"              --{* get the method component *}
+    --{* also used for mdecl, mhead *}
 
- "fld"::   "('b \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"
-              --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
- "fld \<equiv> snd"               --{* get the field component *}
+definition fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
+  "fld = snd"               --{* get the field component *}
+    --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
 
+-- {* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
 
-constdefs --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
- fname:: "(vname \<times> 'a) \<Rightarrow> vname" --{* also used for fdecl *}
- "fname \<equiv> fst"
-  
-  declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
- "declclassf \<equiv> snd"
+definition fname:: "vname \<times> 'a \<Rightarrow> vname" where 
+  "fname = fst"
+    --{* also used for fdecl *}
 
+definition declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" where
+  "declclassf = snd"
 
 
 lemma decliface_simp[simp]: "decliface (I,m) = I"
@@ -318,12 +318,13 @@
 lemma declclassf_simp[simp]:"declclassf (n,c) = c"
 by (simp add: declclassf_def)
 
-constdefs  --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
-  "fldname"  :: "(vname \<times> qtname) \<Rightarrow> vname" 
-  "fldname \<equiv> fst"
+  --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
 
-  "fldclass" :: "(vname \<times> qtname) \<Rightarrow> qtname"
-  "fldclass \<equiv> snd"
+definition fldname :: "vname \<times> qtname \<Rightarrow> vname"  where
+  "fldname = fst"
+
+definition fldclass :: "vname \<times> qtname \<Rightarrow> qtname" where
+  "fldclass = snd"
 
 lemma fldname_simp[simp]: "fldname (n,c) = n"
 by (simp add: fldname_def)
@@ -337,8 +338,8 @@
 text {* Convert a qualified method declaration (qualified with its declaring 
 class) to a qualified member declaration:  @{text methdMembr}  *}
 
-definition methdMembr :: "(qtname \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)" where
- "methdMembr m \<equiv> (fst m,mdecl (snd m))"
+definition methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl" where
+ "methdMembr m = (fst m, mdecl (snd m))"
 
 lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
 by (simp add: methdMembr_def)
diff -r e6b1a0693f3f -r 6c9f23863808 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Sat Jun 12 11:12:54 2010 +0200
+++ b/src/HOL/Bali/WellType.thy	Sat Jun 12 15:48:17 2010 +0200
@@ -103,22 +103,23 @@
 "mheads G S (ClassT C) = cmheads G S C"
 "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
 
-constdefs
+definition
   --{* applicable methods, cf. 15.11.2.1 *}
-  appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
- "appl_methds G S rt \<equiv> \<lambda> sig. 
+  appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+ "appl_methds G S rt = (\<lambda> sig. 
       {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
-                           G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
+                           G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
 
+definition
   --{* more specific methods, cf. 15.11.2.2 *}
-  more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
- "more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
+  more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
+ "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
 (*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
 
+definition
   --{* maximally specific methods, cf. 15.11.2.2 *}
-   max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
-
- "max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
+   max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+ "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
                       (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
 
 
diff -r e6b1a0693f3f -r 6c9f23863808 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sat Jun 12 11:12:54 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sat Jun 12 15:48:17 2010 +0200
@@ -1946,7 +1946,7 @@
                             val p3 = string_of_mixfix csyn
                             val p4 = smart_string_of_cterm crhs
                         in
-                          add_dump ("constdefs\n  " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ "\n  " ^ p4) thy''
+                          add_dump ("definition\n  " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ " where\n  " ^ p4) thy''
                         end
                     else
                         add_dump ("consts\n  " ^ quotename constname ^ " :: \"" ^
@@ -2139,18 +2139,6 @@
         end
         handle e => (message "exception in new_type_definition"; print_exn e)
 
-fun add_dump_constdefs thy defname constname rhs ty =
-    let
-        val n = quotename constname
-        val t = Syntax.string_of_typ_global thy ty
-        val syn = string_of_mixfix (mk_syn thy constname)
-        (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
-        val eq = quote (constname ^ " == "^rhs)
-        val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
-    in
-        add_dump ("constdefs\n  " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n  " ^ d ^ eq) thy
-    end
-
 fun add_dump_syntax thy name =
     let
       val n = quotename name
diff -r e6b1a0693f3f -r 6c9f23863808 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Jun 12 11:12:54 2010 +0200
+++ b/src/HOL/List.thy	Sat Jun 12 15:48:17 2010 +0200
@@ -4188,8 +4188,8 @@
         
 primrec -- {*The lexicographic ordering for lists of the specified length*}
   lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
-    "lexn r 0 = {}"
-  | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
+    [code del]: "lexn r 0 = {}"
+  | [code del]: "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
       {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
 
 definition
diff -r e6b1a0693f3f -r 6c9f23863808 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Sat Jun 12 11:12:54 2010 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Sat Jun 12 15:48:17 2010 +0200
@@ -15,48 +15,53 @@
   to type \emph{checking}.
 *}
 
-constdefs
+definition
   -- "The program counter will always be inside the method:"
-  check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool"
-  "check_bounded ins et \<equiv> 
+  check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool" where
+  "check_bounded ins et \<longleftrightarrow>
   (\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
                      (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
 
+definition
   -- "The method type only contains declared classes:"
-  check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool"
-  "check_types G mxs mxr phi \<equiv> set phi \<subseteq> states G mxs mxr"
+  check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" where
+  "check_types G mxs mxr phi \<longleftrightarrow> set phi \<subseteq> states G mxs mxr"
 
+definition
   -- "An instruction is welltyped if it is applicable and its effect"
   -- "is compatible with the type at all successor instructions:"
   wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
-                exception_table,p_count] \<Rightarrow> bool"
-  "wt_instr i G rT phi mxs max_pc et pc \<equiv>
+                exception_table,p_count] \<Rightarrow> bool" where
+  "wt_instr i G rT phi mxs max_pc et pc \<longleftrightarrow>
   app i G mxs rT pc et (phi!pc) \<and>
   (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
 
+definition
   -- {* The type at @{text "pc=0"} conforms to the method calling convention: *}
-  wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
-  "wt_start G C pTs mxl phi == 
+  wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool" where
+  "wt_start G C pTs mxl phi \<longleftrightarrow>
   G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
 
+definition
   -- "A method is welltyped if the body is not empty, if execution does not"
   -- "leave the body, if the method type covers all instructions and mentions"
   -- "declared classes only, if the method calling convention is respected, and"
   -- "if all instructions are welltyped."
   wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
-                 exception_table,method_type] \<Rightarrow> bool"
-  "wt_method G C pTs rT mxs mxl ins et phi \<equiv>
-  let max_pc = length ins in
+                 exception_table,method_type] \<Rightarrow> bool" where
+  "wt_method G C pTs rT mxs mxl ins et phi \<longleftrightarrow>
+  (let max_pc = length ins in
   0 < max_pc \<and> 
   length phi = length ins \<and>
   check_bounded ins et \<and> 
   check_types G mxs (1+length pTs+mxl) (map OK phi) \<and>
   wt_start G C pTs mxl phi \<and>
-  (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G rT phi mxs max_pc et pc)"
+  (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G rT phi mxs max_pc et pc))"
 
+definition
   -- "A program is welltyped if it is wellformed and all methods are welltyped"
-  wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
-  "wt_jvm_prog G phi ==
+  wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool" where
+  "wt_jvm_prog G phi \<longleftrightarrow>
   wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
            wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
 
diff -r e6b1a0693f3f -r 6c9f23863808 src/HOL/MicroJava/JVM/JVMDefensive.thy
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Sat Jun 12 11:12:54 2010 +0200
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Sat Jun 12 15:48:17 2010 +0200
@@ -117,10 +117,10 @@
     | Normal s' \<Rightarrow> if check G s' then Normal (exec (G, s')) else TypeError"
 
 
-constdefs
+definition
   exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 
-                   ("_ |- _ -jvmd-> _" [61,61,61]60)
-  "G |- s -jvmd-> t \<equiv>
+                   ("_ |- _ -jvmd-> _" [61,61,61]60) where
+  "G |- s -jvmd-> t \<longleftrightarrow>
          (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
                   {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
 
diff -r e6b1a0693f3f -r 6c9f23863808 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sat Jun 12 11:12:54 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Sat Jun 12 15:48:17 2010 +0200
@@ -517,7 +517,7 @@
   end
 
 (* ------------------------------------------------------------------------- *)
-(* get_def: looks up the definition of a constant, as created by "constdefs" *)
+(* get_def: looks up the definition of a constant                            *)
 (* ------------------------------------------------------------------------- *)
 
   (* theory -> string * Term.typ -> (string * Term.term) option *)
@@ -711,7 +711,7 @@
 
   (* Note: currently we use "inverse" functions to the definitional         *)
   (*       mechanisms provided by Isabelle/HOL, e.g. for "axclass",         *)
-  (*       "typedef", "constdefs".  A more general approach could consider  *)
+  (*       "typedef", "definition".  A more general approach could consider *)
   (*       *every* axiom of the theory and collect it if it has a constant/ *)
   (*       type/typeclass in common with the term 't'.                      *)
 
diff -r e6b1a0693f3f -r 6c9f23863808 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sat Jun 12 11:12:54 2010 +0200
+++ b/src/HOL/Wellfounded.thy	Sat Jun 12 15:48:17 2010 +0200
@@ -683,10 +683,8 @@
 text{* Lexicographic combinations *}
 
 definition
- lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
-               (infixr "<*lex*>" 80)
-where
-    "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
+  lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
+  [code del]: "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
 
 lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
 apply (unfold wf_def lex_prod_def) 
diff -r e6b1a0693f3f -r 6c9f23863808 src/HOL/ex/Codegenerator_Candidates.thy
--- a/src/HOL/ex/Codegenerator_Candidates.thy	Sat Jun 12 11:12:54 2010 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy	Sat Jun 12 15:48:17 2010 +0200
@@ -26,8 +26,6 @@
   While_Combinator
 begin
 
-declare lexn.simps [code del]
-
 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
     empty: "sublist [] xs"
   | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
diff -r e6b1a0693f3f -r 6c9f23863808 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Sat Jun 12 11:12:54 2010 +0200
+++ b/src/ZF/ZF.thy	Sat Jun 12 15:48:17 2010 +0200
@@ -199,10 +199,7 @@
 finalconsts
   0 Pow Inf Union PrimReplace mem
 
-defs 
-(*don't try to use constdefs: the declaration order is tightly constrained*)
-
-  (* Bounded Quantifiers *)
+defs  (* Bounded Quantifiers *)
   Ball_def:      "Ball(A, P) == \<forall>x. x\<in>A --> P(x)"
   Bex_def:       "Bex(A, P) == \<exists>x. x\<in>A & P(x)"