# HG changeset patch
# User krauss
# Date 1267529210 -3600
# Node ID bdf8ad377877b4e9806c0236be5157bd925f5069
# Parent  888993948a1ddc704245b5eead15a3eeccb753a6
killed more recdefs

diff -r 888993948a1d -r bdf8ad377877 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Bali/Decl.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -763,51 +763,57 @@
 
 section "general recursion operators for the interface and class hiearchies"
 
-consts
-  iface_rec  :: "prog \<times> qtname \<Rightarrow>   \<spacespace>  (qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
-  class_rec  :: "prog \<times> qtname \<Rightarrow> 'a \<Rightarrow> (qtname \<Rightarrow> class \<Rightarrow> 'a     \<Rightarrow> 'a) \<Rightarrow> 'a"
-
-recdef iface_rec "same_fst ws_prog (\<lambda>G. (subint1 G)^-1)" 
-"iface_rec (G,I) = 
-  (\<lambda>f. case iface G I of 
+function
+  iface_rec  :: "prog \<Rightarrow> qtname \<Rightarrow>   \<spacespace>(qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
+where
+[simp del]: "iface_rec G I f = 
+  (case iface G I of 
          None \<Rightarrow> undefined 
        | Some i \<Rightarrow> if ws_prog G 
                       then f I i 
-                               ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))
+                               ((\<lambda>J. iface_rec G J f)`set (isuperIfs i))
                       else undefined)"
-(hints recdef_wf: wf_subint1 intro: subint1I)
-declare iface_rec.simps [simp del]
+by auto
+termination
+by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subint1 G)^-1)) (%(x,y,z). (x,y))")
+ (auto simp: wf_subint1 subint1I wf_same_fst)
 
 lemma iface_rec: 
 "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow> 
- iface_rec (G,I) f = f I i ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))"
+ iface_rec G I f = f I i ((\<lambda>J. iface_rec G J f)`set (isuperIfs i))"
 apply (subst iface_rec.simps)
 apply simp
 done
 
-recdef class_rec "same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)"
-"class_rec(G,C) = 
-  (\<lambda>t f. case class G C of 
+
+function
+  class_rec  :: "prog \<Rightarrow> qtname \<Rightarrow> 'a \<Rightarrow> (qtname \<Rightarrow> class \<Rightarrow> 'a     \<Rightarrow> 'a) \<Rightarrow> 'a"
+where
+[simp del]: "class_rec G C t f = 
+  (case class G C of 
            None \<Rightarrow> undefined 
          | Some c \<Rightarrow> if ws_prog G 
                         then f C c 
                                  (if C = Object then t 
-                                                else class_rec (G,super c) t f)
+                                                else class_rec G (super c) t f)
                         else undefined)"
-(hints recdef_wf: wf_subcls1 intro: subcls1I)
-declare class_rec.simps [simp del]
+
+by auto
+termination
+by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)) (%(x,y,z,w). (x,y))")
+ (auto simp: wf_subcls1 subcls1I wf_same_fst)
 
 lemma class_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
- class_rec (G,C) t f = 
-   f C c (if C = Object then t else class_rec (G,super c) t f)"
-apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
+ class_rec G C t f = 
+   f C c (if C = Object then t else class_rec G (super c) t f)"
+apply (subst class_rec.simps)
 apply simp
 done
 
 definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
   --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
 "imethds G I 
-  \<equiv> iface_rec (G,I)  
+  \<equiv> iface_rec G I  
               (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
                         (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
         
diff -r 888993948a1d -r bdf8ad377877 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -1381,7 +1381,7 @@
 
 definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
 "imethds G I 
-  \<equiv> iface_rec (G,I)  
+  \<equiv> iface_rec G I  
               (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
                         (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
 text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
@@ -1396,7 +1396,7 @@
 definition methd :: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
 
 "methd G C 
- \<equiv> class_rec (G,C) empty
+ \<equiv> class_rec G C empty
              (\<lambda>C c subcls_mthds. 
                filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
                           subcls_mthds 
@@ -1429,7 +1429,7 @@
         then (case methd G statC sig of
                 None \<Rightarrow> None
               | Some statM 
-                  \<Rightarrow> (class_rec (G,dynC) empty
+                  \<Rightarrow> (class_rec G dynC empty
                        (\<lambda>C c subcls_mthds. 
                           subcls_mthds
                           ++
@@ -1481,7 +1481,7 @@
 
 definition fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
 "fields G C 
-  \<equiv> class_rec (G,C) [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
+  \<equiv> class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
 text {* @{term "fields G C"} 
      list of fields of a class, including all the fields of the superclasses
      (private, inherited and hidden ones) not only the accessible ones
@@ -1805,7 +1805,7 @@
                 (\<lambda>_ dynM. G,sig \<turnstile> dynM overrides statM \<or> dynM = statM)
                 (methd G C)"
         let "?class_rec C" =
-              "(class_rec (G, C) empty
+              "(class_rec G C empty
                            (\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C)))"
         from statM Subcls ws subclseq_dynC_statC
         have dynmethd_dynC_def:
@@ -2270,7 +2270,7 @@
 section "calculation of the superclasses of a class"
 
 definition superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
- "superclasses G C \<equiv> class_rec (G,C) {} 
+ "superclasses G C \<equiv> class_rec G C {} 
                        (\<lambda> C c superclss. (if C=Object 
                                             then {} 
                                             else insert (super c) superclss))"
diff -r 888993948a1d -r bdf8ad377877 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Bali/WellForm.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -730,13 +730,15 @@
  \<Longrightarrow> \<not>is_static im \<and> accmodi im = Public"
 proof -
   assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
+
+  note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]
   have "wf_prog G \<longrightarrow> 
          (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
                   \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
-  proof (rule iface_rec.induct,intro allI impI)
+  proof (induct G I rule: iface_rec_induct', intro allI impI)
     fix G I i im
-    assume hyp: "\<forall> J i. J \<in> set (isuperIfs i) \<and> ws_prog G \<and> iface G I = Some i
-                 \<longrightarrow> ?P G J"
+    assume hyp: "\<And> i J. iface G I = Some i \<Longrightarrow> ws_prog G \<Longrightarrow> J \<in> set (isuperIfs i)
+                 \<Longrightarrow> ?P G J"
     assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 
            im: "im \<in> imethds G I sig" 
     show "\<not>is_static im \<and> accmodi im = Public" 
@@ -1345,14 +1347,16 @@
   qed
 qed
 
+lemmas class_rec_induct' = class_rec.induct[of "%x y z w. P x y", standard]
+
 lemma declclass_widen[rule_format]: 
  "wf_prog G 
  \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 
  \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
-proof (rule class_rec.induct,intro allI impI)
+proof (induct G C rule: class_rec_induct', intro allI impI)
   fix G C c m
-  assume Hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c 
-               \<longrightarrow> ?P G (super c)"
+  assume Hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object
+               \<Longrightarrow> ?P G (super c)"
   assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
          m:  "methd G C sig = Some m"
   show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 
@@ -1976,27 +1980,6 @@
   qed
 qed
 
-(* Tactical version *)
-(*
-lemma declclassD[rule_format]:
- "wf_prog G \<longrightarrow>  
- (\<forall> c d m. class G C = Some c \<longrightarrow> methd G C sig = Some m \<longrightarrow> 
-  class G (declclass m) = Some d
- \<longrightarrow> table_of (methods d) sig  = Some (mthd m))"
-apply (rule class_rec.induct)
-apply (rule impI)
-apply (rule allI)+
-apply (rule impI)
-apply (case_tac "C=Object")
-apply   (force simp add: methd_rec)
-
-apply   (subst methd_rec)
-apply     (blast dest: wf_ws_prog)+
-apply   (case_tac "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig")
-apply     (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
-done
-*)
-
 lemma dynmethd_Object:
   assumes statM: "methd G Object sig = Some statM" and
         private: "accmodi statM = Private" and 
@@ -2355,9 +2338,9 @@
   have "wf_prog G  \<longrightarrow> 
            (\<forall> c m. class G C = Some c \<longrightarrow>  methd G C sig = Some m 
                    \<longrightarrow>  methd G (declclass m) sig = Some m)"      (is "?P G C") 
-  proof (rule class_rec.induct,intro allI impI)
+  proof (induct G C rule: class_rec_induct', intro allI impI)
     fix G C c m
-    assume hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c \<longrightarrow>
+    assume hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object \<Longrightarrow>
                      ?P G (super c)"
     assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
             m: "methd G C sig = Some m"
diff -r 888993948a1d -r bdf8ad377877 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Lambda/ParRed.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -85,14 +85,14 @@
 
 subsection {* Complete developments *}
 
-consts
+fun
   "cd" :: "dB => dB"
-recdef "cd" "measure size"
+where
   "cd (Var n) = Var n"
-  "cd (Var n \<degree> t) = Var n \<degree> cd t"
-  "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
-  "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
-  "cd (Abs s) = Abs (cd s)"
+| "cd (Var n \<degree> t) = Var n \<degree> cd t"
+| "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
+| "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
+| "cd (Abs s) = Abs (cd s)"
 
 lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s"
   apply (induct s arbitrary: t rule: cd.induct)
diff -r 888993948a1d -r bdf8ad377877 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Library/Word.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -311,11 +311,11 @@
 lemma norm_unsigned_idem [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w"
   by (rule bit_list_induct [of _ w],simp_all)
 
-consts
+fun
   nat_to_bv_helper :: "nat => bit list => bit list"
-recdef nat_to_bv_helper "measure (\<lambda>n. n)"
-  "nat_to_bv_helper n = (%bs. (if n = 0 then bs
-                               else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
+where
+  "nat_to_bv_helper n bs = (if n = 0 then bs
+                               else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs))"
 
 definition
   nat_to_bv :: "nat => bit list" where
diff -r 888993948a1d -r bdf8ad377877 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -34,33 +34,34 @@
 | "succs Throw pc              = [pc]"
 
 text "Effect of instruction on the state type:"
-consts 
-eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
 
-recdef eff' "{}"
-"eff' (Load idx,  G, (ST, LT))          = (ok_val (LT ! idx) # ST, LT)"
-"eff' (Store idx, G, (ts#ST, LT))       = (ST, LT[idx:= OK ts])"
-"eff' (LitPush v, G, (ST, LT))           = (the (typeof (\<lambda>v. None) v) # ST, LT)"
-"eff' (Getfield F C, G, (oT#ST, LT))    = (snd (the (field (G,C) F)) # ST, LT)"
-"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)"
-"eff' (New C, G, (ST,LT))               = (Class C # ST, LT)"
-"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)"
-"eff' (Pop, G, (ts#ST,LT))              = (ST,LT)"
-"eff' (Dup, G, (ts#ST,LT))              = (ts#ts#ST,LT)"
-"eff' (Dup_x1, G, (ts1#ts2#ST,LT))      = (ts1#ts2#ts1#ST,LT)"
-"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT))  = (ts1#ts2#ts3#ts1#ST,LT)"
-"eff' (Swap, G, (ts1#ts2#ST,LT))        = (ts2#ts1#ST,LT)"
+fun eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
+where
+"eff' (Load idx,  G, (ST, LT))          = (ok_val (LT ! idx) # ST, LT)" |
+"eff' (Store idx, G, (ts#ST, LT))       = (ST, LT[idx:= OK ts])" |
+"eff' (LitPush v, G, (ST, LT))           = (the (typeof (\<lambda>v. None) v) # ST, LT)" |
+"eff' (Getfield F C, G, (oT#ST, LT))    = (snd (the (field (G,C) F)) # ST, LT)" |
+"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)" |
+"eff' (New C, G, (ST,LT))               = (Class C # ST, LT)" |
+"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)" |
+"eff' (Pop, G, (ts#ST,LT))              = (ST,LT)" |
+"eff' (Dup, G, (ts#ST,LT))              = (ts#ts#ST,LT)" |
+"eff' (Dup_x1, G, (ts1#ts2#ST,LT))      = (ts1#ts2#ts1#ST,LT)" |
+"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT))  = (ts1#ts2#ts3#ts1#ST,LT)" |
+"eff' (Swap, G, (ts1#ts2#ST,LT))        = (ts2#ts1#ST,LT)" |
 "eff' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) 
-                                         = (PrimT Integer#ST,LT)"
-"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT))   = (ST,LT)"
-"eff' (Goto b, G, s)                    = s"
+                                         = (PrimT Integer#ST,LT)" |
+"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT))   = (ST,LT)" |
+"eff' (Goto b, G, s)                    = s" |
   -- "Return has no successor instruction in the same method"
-"eff' (Return, G, s)                    = s" 
+"eff' (Return, G, s)                    = s" |
   -- "Throw always terminates abruptly"
-"eff' (Throw, G, s)                     = s"
+"eff' (Throw, G, s)                     = s" |
 "eff' (Invoke C mn fpTs, G, (ST,LT))    = (let ST' = drop (length fpTs) ST 
   in  (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" 
 
+
+
 primrec match_any :: "jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list" where
   "match_any G pc [] = []"
 | "match_any G pc (e#es) = (let (start_pc, end_pc, handler_pc, catch_type) = e;
@@ -77,16 +78,16 @@
   "match G X pc et = (if \<exists>e \<in> set et. match_exception_entry G (Xcpt X) pc e then [Xcpt X] else [])"
   by (induct et) auto
 
-consts
+fun
   xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table \<Rightarrow> cname list" 
-recdef xcpt_names "{}"
+where
   "xcpt_names (Getfield F C, G, pc, et) = match G NullPointer pc et" 
-  "xcpt_names (Putfield F C, G, pc, et) = match G NullPointer pc et" 
-  "xcpt_names (New C, G, pc, et)        = match G OutOfMemory pc et"
-  "xcpt_names (Checkcast C, G, pc, et)  = match G ClassCast pc et"
-  "xcpt_names (Throw, G, pc, et)        = match_any G pc et"
-  "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et" 
-  "xcpt_names (i, G, pc, et)            = []" 
+| "xcpt_names (Putfield F C, G, pc, et) = match G NullPointer pc et" 
+| "xcpt_names (New C, G, pc, et)        = match G OutOfMemory pc et"
+| "xcpt_names (Checkcast C, G, pc, et)  = match G ClassCast pc et"
+| "xcpt_names (Throw, G, pc, et)        = match_any G pc et"
+| "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et" 
+| "xcpt_names (i, G, pc, et)            = []" 
 
 
 definition xcpt_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> state_type option \<Rightarrow> exception_table \<Rightarrow> succ_type" where
@@ -118,53 +119,53 @@
 
 
 text "Conditions under which eff is applicable:"
-consts
+
+fun
 app' :: "instr \<times> jvm_prog \<times> p_count \<times> nat \<times> ty \<times> state_type \<Rightarrow> bool"
-
-recdef app' "{}"
+where
 "app' (Load idx, G, pc, maxs, rT, s) = 
-  (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> length (fst s) < maxs)"
+  (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> length (fst s) < maxs)" |
 "app' (Store idx, G, pc, maxs, rT, (ts#ST, LT)) = 
-  (idx < length LT)"
+  (idx < length LT)" |
 "app' (LitPush v, G, pc, maxs, rT, s) = 
-  (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)"
+  (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)" |
 "app' (Getfield F C, G, pc, maxs, rT, (oT#ST, LT)) = 
   (is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and> 
-  G \<turnstile> oT \<preceq> (Class C))"
+  G \<turnstile> oT \<preceq> (Class C))" |
 "app' (Putfield F C, G, pc, maxs, rT, (vT#oT#ST, LT)) = 
   (is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
-  G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" 
+  G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" |
 "app' (New C, G, pc, maxs, rT, s) = 
-  (is_class G C \<and> length (fst s) < maxs)"
+  (is_class G C \<and> length (fst s) < maxs)" |
 "app' (Checkcast C, G, pc, maxs, rT, (RefT rt#ST,LT)) = 
-  (is_class G C)"
+  (is_class G C)" |
 "app' (Pop, G, pc, maxs, rT, (ts#ST,LT)) = 
-  True"
+  True" |
 "app' (Dup, G, pc, maxs, rT, (ts#ST,LT)) = 
-  (1+length ST < maxs)"
+  (1+length ST < maxs)" |
 "app' (Dup_x1, G, pc, maxs, rT, (ts1#ts2#ST,LT)) = 
-  (2+length ST < maxs)"
+  (2+length ST < maxs)" |
 "app' (Dup_x2, G, pc, maxs, rT, (ts1#ts2#ts3#ST,LT)) = 
-  (3+length ST < maxs)"
+  (3+length ST < maxs)" |
 "app' (Swap, G, pc, maxs, rT, (ts1#ts2#ST,LT)) = 
-  True"
+  True" |
 "app' (IAdd, G, pc, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT)) =
-  True"
+  True" |
 "app' (Ifcmpeq b, G, pc, maxs, rT, (ts#ts'#ST,LT)) = 
-  (0 \<le> int pc + b \<and> (isPrimT ts \<and> ts' = ts \<or> isRefT ts \<and> isRefT ts'))"
+  (0 \<le> int pc + b \<and> (isPrimT ts \<and> ts' = ts \<or> isRefT ts \<and> isRefT ts'))" |
 "app' (Goto b, G, pc, maxs, rT, s) = 
-  (0 \<le> int pc + b)"
+  (0 \<le> int pc + b)" |
 "app' (Return, G, pc, maxs, rT, (T#ST,LT)) = 
-  (G \<turnstile> T \<preceq> rT)"
+  (G \<turnstile> T \<preceq> rT)" |
 "app' (Throw, G, pc, maxs, rT, (T#ST,LT)) = 
-  isRefT T"
+  isRefT T" |
 "app' (Invoke C mn fpTs, G, pc, maxs, rT, s) = 
   (length fpTs < length (fst s) \<and> 
   (let apTs = rev (take (length fpTs) (fst s));
        X    = hd (drop (length fpTs) (fst s)) 
    in  
        G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and>
-       list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))"
+       list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))" |
   
 "app' (i,G, pc,maxs,rT,s) = False"
 
@@ -208,7 +209,7 @@
 qed auto
 
 lemma 2: "\<not>(2 < length a) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
-proof -;
+proof -
   assume "\<not>(2 < length a)"
   hence "length a < (Suc (Suc (Suc 0)))" by simp
   hence * : "length a = 0 \<or> length a = Suc 0 \<or> length a = Suc (Suc 0)" 
@@ -268,7 +269,7 @@
   "(app (Checkcast C) G maxs rT pc et (Some s)) =  
   (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C \<and>
   (\<forall>x \<in> set (match G ClassCast pc et). is_class G x))"
-  by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)
+  by (cases s, cases "fst s", simp) (cases "hd (fst s)", auto)
 
 lemma appPop[simp]: 
 "(app Pop G maxs rT pc et (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))"
@@ -359,7 +360,7 @@
     assume app: "?app (a,b)"
     hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> 
            length fpTs < length a" (is "?a \<and> ?l") 
-      by (auto simp add: app_def)
+      by auto
     hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") 
       by auto
     hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" 
@@ -374,7 +375,7 @@
     hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs" 
       by blast
     with app
-    show ?thesis by (unfold app_def, clarsimp) blast
+    show ?thesis by clarsimp blast
   qed
   with Pair 
   have "?app s \<Longrightarrow> ?P s" by (simp only:)
diff -r 888993948a1d -r bdf8ad377877 src/HOL/MicroJava/JVM/JVMExec.thy
--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -8,21 +8,19 @@
 theory JVMExec imports JVMExecInstr JVMExceptions begin
 
 
-consts
+fun
   exec :: "jvm_prog \<times> jvm_state => jvm_state option"
-
-
--- "exec is not recursive. recdef is just used for pattern matching"
-recdef exec "{}"
+-- "exec is not recursive. fun is just used for pattern matching"
+where
   "exec (G, xp, hp, []) = None"
 
-  "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
+| "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
   (let 
      i = fst(snd(snd(snd(snd(the(method (G,C) sig)))))) ! pc;
      (xcpt', hp', frs') = exec_instr i G hp stk loc C sig pc frs
    in Some (find_handler G xcpt' hp' frs'))"
 
-  "exec (G, Some xp, hp, frs) = None" 
+| "exec (G, Some xp, hp, frs) = None" 
 
 
 definition exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
diff -r 888993948a1d -r bdf8ad377877 src/HOL/Old_Number_Theory/EulerFermat.thy
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -25,20 +25,18 @@
   | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
       \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
 
-consts
-  BnorRset :: "int * int => int set"
-
-recdef BnorRset
-  "measure ((\<lambda>(a, m). nat a) :: int * int => nat)"
-  "BnorRset (a, m) =
+fun
+  BnorRset :: "int \<Rightarrow> int => int set"
+where
+  "BnorRset a m =
    (if 0 < a then
-    let na = BnorRset (a - 1, m)
+    let na = BnorRset (a - 1) m
     in (if zgcd a m = 1 then insert a na else na)
     else {})"
 
 definition
   norRRset :: "int => int set" where
-  "norRRset m = BnorRset (m - 1, m)"
+  "norRRset m = BnorRset (m - 1) m"
 
 definition
   noXRRset :: "int => int => int set" where
@@ -74,28 +72,27 @@
 
 lemma BnorRset_induct:
   assumes "!!a m. P {} a m"
-    and "!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m
-      ==> P (BnorRset(a,m)) a m"
-  shows "P (BnorRset(u,v)) u v"
+    and "!!a m :: int. 0 < a ==> P (BnorRset (a - 1) m) (a - 1) m
+      ==> P (BnorRset a m) a m"
+  shows "P (BnorRset u v) u v"
   apply (rule BnorRset.induct)
-  apply safe
-   apply (case_tac [2] "0 < a")
-    apply (rule_tac [2] prems)
+   apply (case_tac "0 < a")
+    apply (rule_tac assms)
      apply simp_all
-   apply (simp_all add: BnorRset.simps prems)
+   apply (simp_all add: BnorRset.simps assms)
   done
 
-lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) \<longrightarrow> b \<le> a"
+lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset a m \<longrightarrow> b \<le> a"
   apply (induct a m rule: BnorRset_induct)
    apply simp
   apply (subst BnorRset.simps)
    apply (unfold Let_def, auto)
   done
 
-lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
+lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset a m"
   by (auto dest: Bnor_mem_zle)
 
-lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b"
+lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset a m --> 0 < b"
   apply (induct a m rule: BnorRset_induct)
    prefer 2
    apply (subst BnorRset.simps)
@@ -103,7 +100,7 @@
   done
 
 lemma Bnor_mem_if [rule_format]:
-    "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
+    "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset a m"
   apply (induct a m rule: BnorRset.induct, auto)
    apply (subst BnorRset.simps)
    defer
@@ -111,7 +108,7 @@
    apply (unfold Let_def, auto)
   done
 
-lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \<in> RsetR m"
+lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset a m \<in> RsetR m"
   apply (induct a m rule: BnorRset_induct, simp)
   apply (subst BnorRset.simps)
   apply (unfold Let_def, auto)
@@ -124,7 +121,7 @@
         apply (rule_tac [5] Bnor_mem_zg, auto)
   done
 
-lemma Bnor_fin: "finite (BnorRset (a, m))"
+lemma Bnor_fin: "finite (BnorRset a m)"
   apply (induct a m rule: BnorRset_induct)
    prefer 2
    apply (subst BnorRset.simps)
@@ -258,8 +255,8 @@
 by (unfold inj_on_def, auto)
 
 lemma Bnor_prod_power [rule_format]:
-  "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset (a, m)) =
-      \<Prod>(BnorRset(a, m)) * x^card (BnorRset (a, m))"
+  "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset a m) =
+      \<Prod>(BnorRset a m) * x^card (BnorRset a m)"
   apply (induct a m rule: BnorRset_induct)
    prefer 2
    apply (simplesubst BnorRset.simps)  --{*multiple redexes*}
@@ -284,7 +281,7 @@
   done
 
 lemma Bnor_prod_zgcd [rule_format]:
-    "a < m --> zgcd (\<Prod>(BnorRset(a, m))) m = 1"
+    "a < m --> zgcd (\<Prod>(BnorRset a m)) m = 1"
   apply (induct a m rule: BnorRset_induct)
    prefer 2
    apply (subst BnorRset.simps)
@@ -299,13 +296,13 @@
   apply (case_tac "x = 0")
    apply (case_tac [2] "m = 1")
     apply (rule_tac [3] iffD1)
-     apply (rule_tac [3] k = "\<Prod>(BnorRset(m - 1, m))"
+     apply (rule_tac [3] k = "\<Prod>(BnorRset (m - 1) m)"
        in zcong_cancel2)
       prefer 5
       apply (subst Bnor_prod_power [symmetric])
         apply (rule_tac [7] Bnor_prod_zgcd, simp_all)
   apply (rule bijzcong_zcong_prod)
-  apply (fold norRRset_def noXRRset_def)
+  apply (fold norRRset_def, fold noXRRset_def)
   apply (subst RRset2norRR_eq_norR [symmetric])
     apply (rule_tac [3] inj_func_bijR, auto)
      apply (unfold zcongm_def)
@@ -319,12 +316,12 @@
   done
 
 lemma Bnor_prime:
-  "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset (a, p)) = nat a"
+  "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset a p) = nat a"
   apply (induct a p rule: BnorRset.induct)
   apply (subst BnorRset.simps)
   apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime)
-  apply (subgoal_tac "finite (BnorRset (a - 1,m))")
-   apply (subgoal_tac "a ~: BnorRset (a - 1,m)")
+  apply (subgoal_tac "finite (BnorRset (a - 1) m)")
+   apply (subgoal_tac "a ~: BnorRset (a - 1) m")
     apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1)
    apply (frule Bnor_mem_zle, arith)
   apply (frule Bnor_fin)
diff -r 888993948a1d -r bdf8ad377877 src/HOL/Old_Number_Theory/IntFact.thy
--- a/src/HOL/Old_Number_Theory/IntFact.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Old_Number_Theory/IntFact.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -14,14 +14,14 @@
   \bigskip
 *}
 
-consts
+fun
   zfact :: "int => int"
-  d22set :: "int => int set"
-
-recdef zfact  "measure ((\<lambda>n. nat n) :: int => nat)"
+where
   "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
 
-recdef d22set  "measure ((\<lambda>a. nat a) :: int => nat)"
+fun
+  d22set :: "int => int set"
+where
   "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
 
 
@@ -38,12 +38,10 @@
     and "!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1) ==> P (d22set a) a"
   shows "P (d22set u) u"
   apply (rule d22set.induct)
-  apply safe
-   prefer 2
-   apply (case_tac "1 < a")
-    apply (rule_tac prems)
-     apply (simp_all (no_asm_simp))
-   apply (simp_all (no_asm_simp) add: d22set.simps prems)
+  apply (case_tac "1 < a")
+   apply (rule_tac assms)
+    apply (simp_all (no_asm_simp))
+  apply (simp_all (no_asm_simp) add: d22set.simps assms)
   done
 
 lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> 1 < b"
@@ -66,7 +64,8 @@
 lemma d22set_mem: "1 < b \<Longrightarrow> b \<le> a \<Longrightarrow> b \<in> d22set a"
   apply (induct a rule: d22set.induct)
   apply auto
-   apply (simp_all add: d22set.simps)
+  apply (subst d22set.simps)
+  apply (case_tac "b < a", auto)
   done
 
 lemma d22set_fin: "finite (d22set a)"
@@ -81,8 +80,6 @@
 
 lemma d22set_prod_zfact: "\<Prod>(d22set a) = zfact a"
   apply (induct a rule: d22set.induct)
-  apply safe
-   apply (simp add: d22set.simps zfact.simps)
   apply (subst d22set.simps)
   apply (subst zfact.simps)
   apply (case_tac "1 < a")
diff -r 888993948a1d -r bdf8ad377877 src/HOL/Old_Number_Theory/IntPrimes.thy
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -19,17 +19,14 @@
 
 subsection {* Definitions *}
 
-consts
-  xzgcda :: "int * int * int * int * int * int * int * int => int * int * int"
-
-recdef xzgcda
-  "measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r)
-    :: int * int * int * int *int * int * int * int => nat)"
-  "xzgcda (m, n, r', r, s', s, t', t) =
+fun
+  xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
+where
+  "xzgcda m n r' r s' s t' t =
         (if r \<le> 0 then (r', s', t')
-         else xzgcda (m, n, r, r' mod r, 
-                      s, s' - (r' div r) * s, 
-                      t, t' - (r' div r) * t))"
+         else xzgcda m n r (r' mod r) 
+                      s (s' - (r' div r) * s) 
+                      t (t' - (r' div r) * t))"
 
 definition
   zprime :: "int \<Rightarrow> bool" where
@@ -37,7 +34,7 @@
 
 definition
   xzgcd :: "int => int => int * int * int" where
-  "xzgcd m n = xzgcda (m, n, m, n, 1, 0, 0, 1)"
+  "xzgcd m n = xzgcda m n m n 1 0 0 1"
 
 definition
   zcong :: "int => int => int => bool"  ("(1[_ = _] '(mod _'))") where
@@ -307,9 +304,8 @@
 
 lemma xzgcd_correct_aux1:
   "zgcd r' r = k --> 0 < r -->
-    (\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))"
-  apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
-    z = s and aa = t' and ab = t in xzgcda.induct)
+    (\<exists>sn tn. xzgcda m n r' r s' s t' t = (k, sn, tn))"
+  apply (induct m n r' r s' s t' t rule: xzgcda.induct)
   apply (subst zgcd_eq)
   apply (subst xzgcda.simps, auto)
   apply (case_tac "r' mod r = 0")
@@ -321,17 +317,16 @@
   done
 
 lemma xzgcd_correct_aux2:
-  "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r -->
+  "(\<exists>sn tn. xzgcda m n r' r s' s t' t = (k, sn, tn)) --> 0 < r -->
     zgcd r' r = k"
-  apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
-    z = s and aa = t' and ab = t in xzgcda.induct)
+  apply (induct m n r' r s' s t' t rule: xzgcda.induct)
   apply (subst zgcd_eq)
   apply (subst xzgcda.simps)
   apply (auto simp add: linorder_not_le)
   apply (case_tac "r' mod r = 0")
    prefer 2
    apply (frule_tac a = "r'" in pos_mod_sign, auto)
-  apply (metis Pair_eq simps zle_refl)
+  apply (metis Pair_eq xzgcda.simps zle_refl)
   done
 
 lemma xzgcd_correct:
@@ -362,10 +357,9 @@
   by (rule iffD2 [OF order_less_le conjI])
 
 lemma xzgcda_linear [rule_format]:
-  "0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) -->
+  "0 < r --> xzgcda m n r' r s' s t' t = (rn, sn, tn) -->
     r' = s' * m + t' * n -->  r = s * m + t * n --> rn = sn * m + tn * n"
-  apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
-    z = s and aa = t' and ab = t in xzgcda.induct)
+  apply (induct m n r' r s' s t' t rule: xzgcda.induct)
   apply (subst xzgcda.simps)
   apply (simp (no_asm))
   apply (rule impI)+
diff -r 888993948a1d -r bdf8ad377877 src/HOL/Old_Number_Theory/WilsonRuss.thy
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -17,14 +17,12 @@
   inv :: "int => int => int" where
   "inv p a = (a^(nat (p - 2))) mod p"
 
-consts
-  wset :: "int * int => int set"
-
-recdef wset
-  "measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
-  "wset (a, p) =
+fun
+  wset :: "int \<Rightarrow> int => int set"
+where
+  "wset a p =
     (if 1 < a then
-      let ws = wset (a - 1, p)
+      let ws = wset (a - 1) p
       in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})"
 
 
@@ -163,35 +161,33 @@
 lemma wset_induct:
   assumes "!!a p. P {} a p"
     and "!!a p. 1 < (a::int) \<Longrightarrow>
-      P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
-  shows "P (wset (u, v)) u v"
-  apply (rule wset.induct, safe)
-   prefer 2
-   apply (case_tac "1 < a")
-    apply (rule prems)
-     apply simp_all
-   apply (simp_all add: wset.simps prems)
+      P (wset (a - 1) p) (a - 1) p ==> P (wset a p) a p"
+  shows "P (wset u v) u v"
+  apply (rule wset.induct)
+  apply (case_tac "1 < a")
+   apply (rule assms)
+    apply (simp_all add: wset.simps assms)
   done
 
 lemma wset_mem_imp_or [rule_format]:
-  "1 < a \<Longrightarrow> b \<notin> wset (a - 1, p)
-    ==> b \<in> wset (a, p) --> b = a \<or> b = inv p a"
+  "1 < a \<Longrightarrow> b \<notin> wset (a - 1) p
+    ==> b \<in> wset a p --> b = a \<or> b = inv p a"
   apply (subst wset.simps)
   apply (unfold Let_def, simp)
   done
 
-lemma wset_mem_mem [simp]: "1 < a ==> a \<in> wset (a, p)"
+lemma wset_mem_mem [simp]: "1 < a ==> a \<in> wset a p"
   apply (subst wset.simps)
   apply (unfold Let_def, simp)
   done
 
-lemma wset_subset: "1 < a \<Longrightarrow> b \<in> wset (a - 1, p) ==> b \<in> wset (a, p)"
+lemma wset_subset: "1 < a \<Longrightarrow> b \<in> wset (a - 1) p ==> b \<in> wset a p"
   apply (subst wset.simps)
   apply (unfold Let_def, auto)
   done
 
 lemma wset_g_1 [rule_format]:
-    "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> 1 < b"
+    "zprime p --> a < p - 1 --> b \<in> wset a p --> 1 < b"
   apply (induct a p rule: wset_induct, auto)
   apply (case_tac "b = a")
    apply (case_tac [2] "b = inv p a")
@@ -203,7 +199,7 @@
   done
 
 lemma wset_less [rule_format]:
-    "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> b < p - 1"
+    "zprime p --> a < p - 1 --> b \<in> wset a p --> b < p - 1"
   apply (induct a p rule: wset_induct, auto)
   apply (case_tac "b = a")
    apply (case_tac [2] "b = inv p a")
@@ -216,7 +212,7 @@
 
 lemma wset_mem [rule_format]:
   "zprime p -->
-    a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset (a, p)"
+    a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset a p"
   apply (induct a p rule: wset.induct, auto)
   apply (rule_tac wset_subset)
   apply (simp (no_asm_simp))
@@ -224,8 +220,8 @@
   done
 
 lemma wset_mem_inv_mem [rule_format]:
-  "zprime p --> 5 \<le> p --> a < p - 1 --> b \<in> wset (a, p)
-    --> inv p b \<in> wset (a, p)"
+  "zprime p --> 5 \<le> p --> a < p - 1 --> b \<in> wset a p
+    --> inv p b \<in> wset a p"
   apply (induct a p rule: wset_induct, auto)
    apply (case_tac "b = a")
     apply (subst wset.simps)
@@ -240,13 +236,13 @@
 
 lemma wset_inv_mem_mem:
   "zprime p \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - 1 \<Longrightarrow> 1 < b \<Longrightarrow> b < p - 1
-    \<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
+    \<Longrightarrow> inv p b \<in> wset a p \<Longrightarrow> b \<in> wset a p"
   apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
    apply (rule_tac [2] wset_mem_inv_mem)
       apply (rule inv_inv, simp_all)
   done
 
-lemma wset_fin: "finite (wset (a, p))"
+lemma wset_fin: "finite (wset a p)"
   apply (induct a p rule: wset_induct)
    prefer 2
    apply (subst wset.simps)
@@ -255,27 +251,27 @@
 
 lemma wset_zcong_prod_1 [rule_format]:
   "zprime p -->
-    5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset(a, p). x) = 1] (mod p)"
+    5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset a p. x) = 1] (mod p)"
   apply (induct a p rule: wset_induct)
    prefer 2
    apply (subst wset.simps)
-   apply (unfold Let_def, auto)
+   apply (auto, unfold Let_def, auto)
   apply (subst setprod_insert)
     apply (tactic {* stac (thm "setprod_insert") 3 *})
       apply (subgoal_tac [5]
-        "zcong (a * inv p a * (\<Prod>x\<in> wset(a - 1, p). x)) (1 * 1) p")
+        "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
        prefer 5
        apply (simp add: zmult_assoc)
       apply (rule_tac [5] zcong_zmult)
        apply (rule_tac [5] inv_is_inv)
          apply (tactic "clarify_tac @{claset} 4")
-         apply (subgoal_tac [4] "a \<in> wset (a - 1, p)")
+         apply (subgoal_tac [4] "a \<in> wset (a - 1) p")
           apply (rule_tac [5] wset_inv_mem_mem)
                apply (simp_all add: wset_fin)
   apply (rule inv_distinct, auto)
   done
 
-lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2, p)"
+lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2) p"
   apply safe
    apply (erule wset_mem)
      apply (rule_tac [2] d22set_g_1)
diff -r 888993948a1d -r bdf8ad377877 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/ZF/Games.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ZF/Games.thy
+(*  Title:      HOL/ZF/MainZF.thy/Games.thy
     Author:     Steven Obua
 
 An application of HOLZF: Partizan Games.  See "Partizan Games in
@@ -347,13 +347,12 @@
     right_option_def[symmetric] left_option_def[symmetric])
   done
 
-consts
+function
   neg_game :: "game \<Rightarrow> game"
-
-recdef neg_game "option_of"
-  "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))"
-
-declare neg_game.simps[simp del]
+where
+  [simp del]: "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))"
+by auto
+termination by (relation "option_of") auto
 
 lemma "neg_game (neg_game g) = g"
   apply (induct g rule: neg_game.induct)
@@ -365,17 +364,16 @@
   apply (auto simp add: zet_ext_eq zimage_iff)
   done
 
-consts
+function
   ge_game :: "(game * game) \<Rightarrow> bool" 
-
-recdef ge_game "(gprod_2_1 option_of)"
-  "ge_game (G, H) = (\<forall> x. if zin x (right_options G) then (
+where
+  [simp del]: "ge_game (G, H) = (\<forall> x. if zin x (right_options G) then (
                           if zin x (left_options H) then \<not> (ge_game (H, x) \<or> (ge_game (x, G))) 
                                                     else \<not> (ge_game (H, x)))
                           else (if zin x (left_options H) then \<not> (ge_game (x, G)) else True))"
-(hints simp: gprod_2_1_def)
-
-declare ge_game.simps [simp del]
+by auto
+termination by (relation "(gprod_2_1 option_of)") 
+ (simp, auto simp: gprod_2_1_def)
 
 lemma ge_game_eq: "ge_game (G, H) = (\<forall> x. (zin x (right_options G) \<longrightarrow> \<not> ge_game (H, x)) \<and> (zin x (left_options H) \<longrightarrow> \<not> ge_game (x, G)))"
   apply (subst ge_game.simps[where G=G and H=H])
@@ -506,19 +504,18 @@
 definition zero_game :: game
  where  "zero_game \<equiv> Game zempty zempty"
 
-consts 
-  plus_game :: "game * game \<Rightarrow> game"
+function 
+  plus_game :: "game \<Rightarrow> game \<Rightarrow> game"
+where
+  [simp del]: "plus_game G H = Game (zunion (zimage (\<lambda> g. plus_game g H) (left_options G))
+                                   (zimage (\<lambda> h. plus_game G h) (left_options H)))
+                           (zunion (zimage (\<lambda> g. plus_game g H) (right_options G))
+                                   (zimage (\<lambda> h. plus_game G h) (right_options H)))"
+by auto
+termination by (relation "gprod_2_2 option_of")
+  (simp, auto simp: gprod_2_2_def)
 
-recdef plus_game "gprod_2_2 option_of"
-  "plus_game (G, H) = Game (zunion (zimage (\<lambda> g. plus_game (g, H)) (left_options G))
-                                   (zimage (\<lambda> h. plus_game (G, h)) (left_options H)))
-                           (zunion (zimage (\<lambda> g. plus_game (g, H)) (right_options G))
-                                   (zimage (\<lambda> h. plus_game (G, h)) (right_options H)))"
-(hints simp add: gprod_2_2_def)
-
-declare plus_game.simps[simp del]
-
-lemma plus_game_comm: "plus_game (G, H) = plus_game (H, G)"
+lemma plus_game_comm: "plus_game G H = plus_game H G"
 proof (induct G H rule: plus_game.induct)
   case (1 G H)
   show ?case
@@ -541,11 +538,11 @@
 lemma right_zero_game[simp]: "right_options (zero_game) = zempty"
   by (simp add: zero_game_def)
 
-lemma plus_game_zero_right[simp]: "plus_game (G, zero_game) = G"
+lemma plus_game_zero_right[simp]: "plus_game G zero_game = G"
 proof -
   { 
     fix G H
-    have "H = zero_game \<longrightarrow> plus_game (G, H) = G "
+    have "H = zero_game \<longrightarrow> plus_game G H = G "
     proof (induct G H rule: plus_game.induct, rule impI)
       case (goal1 G H)
       note induct_hyp = prems[simplified goal1, simplified] and prems
@@ -553,7 +550,7 @@
         apply (simp only: plus_game.simps[where G=G and H=H])
         apply (simp add: game_ext_eq prems)
         apply (auto simp add: 
-          zimage_cong[where f = "\<lambda> g. plus_game (g, zero_game)" and g = "id"] 
+          zimage_cong[where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
           induct_hyp)
         done
     qed
@@ -561,7 +558,7 @@
   then show ?thesis by auto
 qed
 
-lemma plus_game_zero_left: "plus_game (zero_game, G) = G"
+lemma plus_game_zero_left: "plus_game zero_game G = G"
   by (simp add: plus_game_comm)
 
 lemma left_imp_options[simp]: "zin opt (left_options g) \<Longrightarrow> zin opt (options g)"
@@ -571,11 +568,11 @@
   by (simp add: options_def zunion)
 
 lemma left_options_plus: 
-  "left_options (plus_game (u, v)) =  zunion (zimage (\<lambda>g. plus_game (g, v)) (left_options u)) (zimage (\<lambda>h. plus_game (u, h)) (left_options v))" 
+  "left_options (plus_game u v) =  zunion (zimage (\<lambda>g. plus_game g v) (left_options u)) (zimage (\<lambda>h. plus_game u h) (left_options v))" 
   by (subst plus_game.simps, simp)
 
 lemma right_options_plus:
-  "right_options (plus_game (u, v)) =  zunion (zimage (\<lambda>g. plus_game (g, v)) (right_options u)) (zimage (\<lambda>h. plus_game (u, h)) (right_options v))"
+  "right_options (plus_game u v) =  zunion (zimage (\<lambda>g. plus_game g v) (right_options u)) (zimage (\<lambda>h. plus_game u h) (right_options v))"
   by (subst plus_game.simps, simp)
 
 lemma left_options_neg: "left_options (neg_game u) = zimage neg_game (right_options u)"  
@@ -584,32 +581,32 @@
 lemma right_options_neg: "right_options (neg_game u) = zimage neg_game (left_options u)"
   by (subst neg_game.simps, simp)
   
-lemma plus_game_assoc: "plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))"
+lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)"
 proof -
   { 
     fix a
-    have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))"
+    have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game F G) H = plus_game F (plus_game G H)"
     proof (induct a rule: induct_game, (rule impI | rule allI)+)
       case (goal1 x F G H)
-      let ?L = "plus_game (plus_game (F, G), H)"
-      let ?R = "plus_game (F, plus_game (G, H))"
+      let ?L = "plus_game (plus_game F G) H"
+      let ?R = "plus_game F (plus_game G H)"
       note options_plus = left_options_plus right_options_plus
       {
         fix opt
         note hyp = goal1(1)[simplified goal1(2), rule_format] 
-        have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game (opt, G), H) = plus_game (opt, plus_game (G, H))"
+        have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
           by (blast intro: hyp lprod_3_3)
-        have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game (F, opt), H) = plus_game (F, plus_game (opt, H))"
+        have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
           by (blast intro: hyp lprod_3_4)
-        have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game (F, G), opt) = plus_game (F, plus_game (G, opt))" 
+        have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game F G) opt = plus_game F (plus_game G opt)" 
           by (blast intro: hyp lprod_3_5)
         note F and G and H
       }
       note induct_hyp = this
       have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
         by (auto simp add: 
-          plus_game.simps[where G="plus_game (F,G)" and H=H]
-          plus_game.simps[where G="F" and H="plus_game (G,H)"] 
+          plus_game.simps[where G="plus_game F G" and H=H]
+          plus_game.simps[where G="F" and H="plus_game G H"] 
           zet_ext_eq zunion zimage_iff options_plus
           induct_hyp left_imp_options right_imp_options)
       then show ?case
@@ -619,7 +616,7 @@
   then show ?thesis by auto
 qed
 
-lemma neg_plus_game: "neg_game (plus_game (G, H)) = plus_game(neg_game G, neg_game H)"
+lemma neg_plus_game: "neg_game (plus_game G H) = plus_game (neg_game G) (neg_game H)"
 proof (induct G H rule: plus_game.induct)
   case (1 G H)
   note opt_ops = 
@@ -627,26 +624,26 @@
     left_options_neg right_options_neg  
   show ?case
     by (auto simp add: opt_ops
-      neg_game.simps[of "plus_game (G,H)"]
+      neg_game.simps[of "plus_game G H"]
       plus_game.simps[of "neg_game G" "neg_game H"]
       Game_ext zet_ext_eq zunion zimage_iff prems)
 qed
 
-lemma eq_game_plus_inverse: "eq_game (plus_game (x, neg_game x)) zero_game"
+lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
 proof (induct x rule: wf_induct[OF wf_option_of])
   case (goal1 x)
   { fix y
     assume "zin y (options x)"
-    then have "eq_game (plus_game (y, neg_game y)) zero_game"
+    then have "eq_game (plus_game y (neg_game y)) zero_game"
       by (auto simp add: prems)
   }
   note ihyp = this
   {
     fix y
     assume y: "zin y (right_options x)"
-    have "\<not> (ge_game (zero_game, plus_game (y, neg_game x)))"
+    have "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
       apply (subst ge_game.simps, simp)
-      apply (rule exI[where x="plus_game (y, neg_game y)"])
+      apply (rule exI[where x="plus_game y (neg_game y)"])
       apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
       apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: prems)
       done
@@ -655,9 +652,9 @@
   {
     fix y
     assume y: "zin y (left_options x)"
-    have "\<not> (ge_game (zero_game, plus_game (x, neg_game y)))"
+    have "\<not> (ge_game (zero_game, plus_game x (neg_game y)))"
       apply (subst ge_game.simps, simp)
-      apply (rule exI[where x="plus_game (y, neg_game y)"])
+      apply (rule exI[where x="plus_game y (neg_game y)"])
       apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
       apply (auto simp add: left_options_plus zunion zimage_iff intro: prems)
       done
@@ -666,9 +663,9 @@
   {
     fix y
     assume y: "zin y (left_options x)"
-    have "\<not> (ge_game (plus_game (y, neg_game x), zero_game))"
+    have "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
       apply (subst ge_game.simps, simp)
-      apply (rule exI[where x="plus_game (y, neg_game y)"])
+      apply (rule exI[where x="plus_game y (neg_game y)"])
       apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
       apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: prems)
       done
@@ -677,9 +674,9 @@
   {
     fix y
     assume y: "zin y (right_options x)"
-    have "\<not> (ge_game (plus_game (x, neg_game y), zero_game))"
+    have "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
       apply (subst ge_game.simps, simp)
-      apply (rule exI[where x="plus_game (y, neg_game y)"])
+      apply (rule exI[where x="plus_game y (neg_game y)"])
       apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
       apply (auto simp add: right_options_plus zunion zimage_iff intro: prems)
       done
@@ -687,28 +684,28 @@
   note case4 = this
   show ?case
     apply (simp add: eq_game_def)
-    apply (simp add: ge_game.simps[of "plus_game (x, neg_game x)" "zero_game"])
-    apply (simp add: ge_game.simps[of "zero_game" "plus_game (x, neg_game x)"])
+    apply (simp add: ge_game.simps[of "plus_game x (neg_game x)" "zero_game"])
+    apply (simp add: ge_game.simps[of "zero_game" "plus_game x (neg_game x)"])
     apply (simp add: right_options_plus left_options_plus right_options_neg left_options_neg zunion zimage_iff)
     apply (auto simp add: case1 case2 case3 case4)
     done
 qed
 
-lemma ge_plus_game_left: "ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))"
+lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
 proof -
   { fix a
-    have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))"
+    have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
     proof (induct a rule: induct_game, (rule impI | rule allI)+)
       case (goal1 a x y z)
       note induct_hyp = goal1(1)[rule_format, simplified goal1(2)]
       { 
-        assume hyp: "ge_game(plus_game (x, y), plus_game (x, z))"
+        assume hyp: "ge_game(plus_game x y, plus_game x z)"
         have "ge_game (y, z)"
         proof -
           { fix yr
             assume yr: "zin yr (right_options y)"
-            from hyp have "\<not> (ge_game (plus_game (x, z), plus_game (x, yr)))"
-              by (auto simp add: ge_game_eq[of "plus_game (x,y)" "plus_game(x,z)"]
+            from hyp have "\<not> (ge_game (plus_game x z, plus_game x yr))"
+              by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
                 right_options_plus zunion zimage_iff intro: yr)
             then have "\<not> (ge_game (z, yr))"
               apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
@@ -718,8 +715,8 @@
           note yr = this
           { fix zl
             assume zl: "zin zl (left_options z)"
-            from hyp have "\<not> (ge_game (plus_game (x, zl), plus_game (x, y)))"
-              by (auto simp add: ge_game_eq[of "plus_game (x,y)" "plus_game(x,z)"]
+            from hyp have "\<not> (ge_game (plus_game x zl, plus_game x y))"
+              by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
                 left_options_plus zunion zimage_iff intro: zl)
             then have "\<not> (ge_game (zl, y))"
               apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
@@ -739,11 +736,11 @@
         {
           fix x'
           assume x': "zin x' (right_options x)"
-          assume hyp: "ge_game (plus_game (x, z), plus_game (x', y))"
-          then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
-            by (auto simp add: ge_game_eq[of "plus_game (x,z)" "plus_game (x', y)"] 
+          assume hyp: "ge_game (plus_game x z, plus_game x' y)"
+          then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
+            by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"] 
               right_options_plus zunion zimage_iff intro: x')
-          have t: "ge_game (plus_game (x', y), plus_game (x', z))"
+          have t: "ge_game (plus_game x' y, plus_game x' z)"
             apply (subst induct_hyp[symmetric])
             apply (auto intro: lprod_3_3 x' yz)
             done
@@ -753,11 +750,11 @@
         {
           fix x'
           assume x': "zin x' (left_options x)"
-          assume hyp: "ge_game (plus_game (x', z), plus_game (x, y))"
-          then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
-            by (auto simp add: ge_game_eq[of "plus_game (x',z)" "plus_game (x, y)"] 
+          assume hyp: "ge_game (plus_game x' z, plus_game x y)"
+          then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
+            by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"] 
               left_options_plus zunion zimage_iff intro: x')
-          have t: "ge_game (plus_game (x', y), plus_game (x', z))"
+          have t: "ge_game (plus_game x' y, plus_game x' z)"
             apply (subst induct_hyp[symmetric])
             apply (auto intro: lprod_3_3 x' yz)
             done
@@ -767,7 +764,7 @@
         {
           fix y'
           assume y': "zin y' (right_options y)"
-          assume hyp: "ge_game (plus_game(x, z), plus_game (x, y'))"
+          assume hyp: "ge_game (plus_game x z, plus_game x y')"
           then have "ge_game(z, y')"
             apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
             apply (auto simp add: hyp lprod_3_6 y')
@@ -780,7 +777,7 @@
         {
           fix z'
           assume z': "zin z' (left_options z)"
-          assume hyp: "ge_game (plus_game(x, z'), plus_game (x, y))"
+          assume hyp: "ge_game (plus_game x z', plus_game x y)"
           then have "ge_game(z', y)"
             apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
             apply (auto simp add: hyp lprod_3_7 z')
@@ -790,7 +787,7 @@
           with z' have "False" by (auto simp add: ge_game_leftright_refl)
         }
         note case4 = this   
-        have "ge_game(plus_game (x, y), plus_game (x, z))"
+        have "ge_game(plus_game x y, plus_game x z)"
           apply (subst ge_game_eq)
           apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
           apply (auto intro: case1 case2 case3 case4)
@@ -804,7 +801,7 @@
   then show ?thesis by blast
 qed
 
-lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game (y, x), plus_game (z, x))"
+lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game y x, plus_game z x)"
   by (simp add: ge_plus_game_left plus_game_comm)
 
 lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
@@ -865,7 +862,7 @@
   Pg_minus_def: "- G = contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
 
 definition
-  Pg_plus_def: "G + H = contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game (g,h)})})"
+  Pg_plus_def: "G + H = contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
 
 definition
   Pg_diff_def: "G - H = G + (- (H::Pg))"
@@ -891,14 +888,14 @@
   apply (simp add: eq_game_rel_def)
   done
 
-lemma char_Pg_plus[simp]: "Abs_Pg (eq_game_rel `` {g}) + Abs_Pg (eq_game_rel `` {h}) = Abs_Pg (eq_game_rel `` {plus_game (g, h)})"
+lemma char_Pg_plus[simp]: "Abs_Pg (eq_game_rel `` {g}) + Abs_Pg (eq_game_rel `` {h}) = Abs_Pg (eq_game_rel `` {plus_game g h})"
 proof -
-  have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game (g, h)})}) respects2 eq_game_rel" 
+  have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game g h})}) respects2 eq_game_rel" 
     apply (simp add: congruent2_def)
     apply (auto simp add: eq_game_rel_def eq_game_def)
-    apply (rule_tac y="plus_game (y1, z2)" in ge_game_trans)
+    apply (rule_tac y="plus_game y1 z2" in ge_game_trans)
     apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
-    apply (rule_tac y="plus_game (z1, y2)" in ge_game_trans)
+    apply (rule_tac y="plus_game z1 y2" in ge_game_trans)
     apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
     done
   then show ?thesis
diff -r 888993948a1d -r bdf8ad377877 src/HOL/ZF/Zet.thy
--- a/src/HOL/ZF/Zet.thy	Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/ZF/Zet.thy	Tue Mar 02 12:26:50 2010 +0100
@@ -196,7 +196,7 @@
 lemma zimage_id[simp]: "zimage id A = A"
   by (simp add: zet_ext_eq zimage_iff)
 
-lemma zimage_cong[recdef_cong]: "\<lbrakk> M = N; !! x. zin x N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> zimage f M = zimage g N"
+lemma zimage_cong[recdef_cong, fundef_cong]: "\<lbrakk> M = N; !! x. zin x N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> zimage f M = zimage g N"
   by (auto simp add: zet_ext_eq zimage_iff)
 
 end