killed more recdefs
authorkrauss
Tue Mar 02 12:26:50 2010 +0100 (2010-03-02)
changeset 35440bdf8ad377877
parent 35439 888993948a1d
child 35498 5c70de748522
child 35509 13e83ce8391b
killed more recdefs
src/HOL/Bali/Decl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/WellForm.thy
src/HOL/Lambda/ParRed.thy
src/HOL/Library/Word.thy
src/HOL/MicroJava/BV/Effect.thy
src/HOL/MicroJava/JVM/JVMExec.thy
src/HOL/Old_Number_Theory/EulerFermat.thy
src/HOL/Old_Number_Theory/IntFact.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/WilsonRuss.thy
src/HOL/ZF/Games.thy
src/HOL/ZF/Zet.thy
     1.1 --- a/src/HOL/Bali/Decl.thy	Mon Mar 01 18:49:55 2010 +0100
     1.2 +++ b/src/HOL/Bali/Decl.thy	Tue Mar 02 12:26:50 2010 +0100
     1.3 @@ -763,51 +763,57 @@
     1.4  
     1.5  section "general recursion operators for the interface and class hiearchies"
     1.6  
     1.7 -consts
     1.8 -  iface_rec  :: "prog \<times> qtname \<Rightarrow>   \<spacespace>  (qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
     1.9 -  class_rec  :: "prog \<times> qtname \<Rightarrow> 'a \<Rightarrow> (qtname \<Rightarrow> class \<Rightarrow> 'a     \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.10 -
    1.11 -recdef iface_rec "same_fst ws_prog (\<lambda>G. (subint1 G)^-1)" 
    1.12 -"iface_rec (G,I) = 
    1.13 -  (\<lambda>f. case iface G I of 
    1.14 +function
    1.15 +  iface_rec  :: "prog \<Rightarrow> qtname \<Rightarrow>   \<spacespace>(qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.16 +where
    1.17 +[simp del]: "iface_rec G I f = 
    1.18 +  (case iface G I of 
    1.19           None \<Rightarrow> undefined 
    1.20         | Some i \<Rightarrow> if ws_prog G 
    1.21                        then f I i 
    1.22 -                               ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))
    1.23 +                               ((\<lambda>J. iface_rec G J f)`set (isuperIfs i))
    1.24                        else undefined)"
    1.25 -(hints recdef_wf: wf_subint1 intro: subint1I)
    1.26 -declare iface_rec.simps [simp del]
    1.27 +by auto
    1.28 +termination
    1.29 +by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subint1 G)^-1)) (%(x,y,z). (x,y))")
    1.30 + (auto simp: wf_subint1 subint1I wf_same_fst)
    1.31  
    1.32  lemma iface_rec: 
    1.33  "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow> 
    1.34 - iface_rec (G,I) f = f I i ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))"
    1.35 + iface_rec G I f = f I i ((\<lambda>J. iface_rec G J f)`set (isuperIfs i))"
    1.36  apply (subst iface_rec.simps)
    1.37  apply simp
    1.38  done
    1.39  
    1.40 -recdef class_rec "same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)"
    1.41 -"class_rec(G,C) = 
    1.42 -  (\<lambda>t f. case class G C of 
    1.43 +
    1.44 +function
    1.45 +  class_rec  :: "prog \<Rightarrow> qtname \<Rightarrow> 'a \<Rightarrow> (qtname \<Rightarrow> class \<Rightarrow> 'a     \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.46 +where
    1.47 +[simp del]: "class_rec G C t f = 
    1.48 +  (case class G C of 
    1.49             None \<Rightarrow> undefined 
    1.50           | Some c \<Rightarrow> if ws_prog G 
    1.51                          then f C c 
    1.52                                   (if C = Object then t 
    1.53 -                                                else class_rec (G,super c) t f)
    1.54 +                                                else class_rec G (super c) t f)
    1.55                          else undefined)"
    1.56 -(hints recdef_wf: wf_subcls1 intro: subcls1I)
    1.57 -declare class_rec.simps [simp del]
    1.58 +
    1.59 +by auto
    1.60 +termination
    1.61 +by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)) (%(x,y,z,w). (x,y))")
    1.62 + (auto simp: wf_subcls1 subcls1I wf_same_fst)
    1.63  
    1.64  lemma class_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
    1.65 - class_rec (G,C) t f = 
    1.66 -   f C c (if C = Object then t else class_rec (G,super c) t f)"
    1.67 -apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
    1.68 + class_rec G C t f = 
    1.69 +   f C c (if C = Object then t else class_rec G (super c) t f)"
    1.70 +apply (subst class_rec.simps)
    1.71  apply simp
    1.72  done
    1.73  
    1.74  definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
    1.75    --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
    1.76  "imethds G I 
    1.77 -  \<equiv> iface_rec (G,I)  
    1.78 +  \<equiv> iface_rec G I  
    1.79                (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
    1.80                          (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
    1.81          
     2.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Mar 01 18:49:55 2010 +0100
     2.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Tue Mar 02 12:26:50 2010 +0100
     2.3 @@ -1381,7 +1381,7 @@
     2.4  
     2.5  definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
     2.6  "imethds G I 
     2.7 -  \<equiv> iface_rec (G,I)  
     2.8 +  \<equiv> iface_rec G I  
     2.9                (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
    2.10                          (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
    2.11  text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
    2.12 @@ -1396,7 +1396,7 @@
    2.13  definition methd :: "prog \<Rightarrow> qtname  \<Rightarrow> (sig,qtname \<times> methd) table" where
    2.14  
    2.15  "methd G C 
    2.16 - \<equiv> class_rec (G,C) empty
    2.17 + \<equiv> class_rec G C empty
    2.18               (\<lambda>C c subcls_mthds. 
    2.19                 filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
    2.20                            subcls_mthds 
    2.21 @@ -1429,7 +1429,7 @@
    2.22          then (case methd G statC sig of
    2.23                  None \<Rightarrow> None
    2.24                | Some statM 
    2.25 -                  \<Rightarrow> (class_rec (G,dynC) empty
    2.26 +                  \<Rightarrow> (class_rec G dynC empty
    2.27                         (\<lambda>C c subcls_mthds. 
    2.28                            subcls_mthds
    2.29                            ++
    2.30 @@ -1481,7 +1481,7 @@
    2.31  
    2.32  definition fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
    2.33  "fields G C 
    2.34 -  \<equiv> class_rec (G,C) [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
    2.35 +  \<equiv> class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
    2.36  text {* @{term "fields G C"} 
    2.37       list of fields of a class, including all the fields of the superclasses
    2.38       (private, inherited and hidden ones) not only the accessible ones
    2.39 @@ -1805,7 +1805,7 @@
    2.40                  (\<lambda>_ dynM. G,sig \<turnstile> dynM overrides statM \<or> dynM = statM)
    2.41                  (methd G C)"
    2.42          let "?class_rec C" =
    2.43 -              "(class_rec (G, C) empty
    2.44 +              "(class_rec G C empty
    2.45                             (\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C)))"
    2.46          from statM Subcls ws subclseq_dynC_statC
    2.47          have dynmethd_dynC_def:
    2.48 @@ -2270,7 +2270,7 @@
    2.49  section "calculation of the superclasses of a class"
    2.50  
    2.51  definition superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
    2.52 - "superclasses G C \<equiv> class_rec (G,C) {} 
    2.53 + "superclasses G C \<equiv> class_rec G C {} 
    2.54                         (\<lambda> C c superclss. (if C=Object 
    2.55                                              then {} 
    2.56                                              else insert (super c) superclss))"
     3.1 --- a/src/HOL/Bali/WellForm.thy	Mon Mar 01 18:49:55 2010 +0100
     3.2 +++ b/src/HOL/Bali/WellForm.thy	Tue Mar 02 12:26:50 2010 +0100
     3.3 @@ -730,13 +730,15 @@
     3.4   \<Longrightarrow> \<not>is_static im \<and> accmodi im = Public"
     3.5  proof -
     3.6    assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
     3.7 +
     3.8 +  note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]
     3.9    have "wf_prog G \<longrightarrow> 
    3.10           (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
    3.11                    \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
    3.12 -  proof (rule iface_rec.induct,intro allI impI)
    3.13 +  proof (induct G I rule: iface_rec_induct', intro allI impI)
    3.14      fix G I i im
    3.15 -    assume hyp: "\<forall> J i. J \<in> set (isuperIfs i) \<and> ws_prog G \<and> iface G I = Some i
    3.16 -                 \<longrightarrow> ?P G J"
    3.17 +    assume hyp: "\<And> i J. iface G I = Some i \<Longrightarrow> ws_prog G \<Longrightarrow> J \<in> set (isuperIfs i)
    3.18 +                 \<Longrightarrow> ?P G J"
    3.19      assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 
    3.20             im: "im \<in> imethds G I sig" 
    3.21      show "\<not>is_static im \<and> accmodi im = Public" 
    3.22 @@ -1345,14 +1347,16 @@
    3.23    qed
    3.24  qed
    3.25  
    3.26 +lemmas class_rec_induct' = class_rec.induct[of "%x y z w. P x y", standard]
    3.27 +
    3.28  lemma declclass_widen[rule_format]: 
    3.29   "wf_prog G 
    3.30   \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 
    3.31   \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
    3.32 -proof (rule class_rec.induct,intro allI impI)
    3.33 +proof (induct G C rule: class_rec_induct', intro allI impI)
    3.34    fix G C c m
    3.35 -  assume Hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c 
    3.36 -               \<longrightarrow> ?P G (super c)"
    3.37 +  assume Hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object
    3.38 +               \<Longrightarrow> ?P G (super c)"
    3.39    assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
    3.40           m:  "methd G C sig = Some m"
    3.41    show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 
    3.42 @@ -1976,27 +1980,6 @@
    3.43    qed
    3.44  qed
    3.45  
    3.46 -(* Tactical version *)
    3.47 -(*
    3.48 -lemma declclassD[rule_format]:
    3.49 - "wf_prog G \<longrightarrow>  
    3.50 - (\<forall> c d m. class G C = Some c \<longrightarrow> methd G C sig = Some m \<longrightarrow> 
    3.51 -  class G (declclass m) = Some d
    3.52 - \<longrightarrow> table_of (methods d) sig  = Some (mthd m))"
    3.53 -apply (rule class_rec.induct)
    3.54 -apply (rule impI)
    3.55 -apply (rule allI)+
    3.56 -apply (rule impI)
    3.57 -apply (case_tac "C=Object")
    3.58 -apply   (force simp add: methd_rec)
    3.59 -
    3.60 -apply   (subst methd_rec)
    3.61 -apply     (blast dest: wf_ws_prog)+
    3.62 -apply   (case_tac "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig")
    3.63 -apply     (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
    3.64 -done
    3.65 -*)
    3.66 -
    3.67  lemma dynmethd_Object:
    3.68    assumes statM: "methd G Object sig = Some statM" and
    3.69          private: "accmodi statM = Private" and 
    3.70 @@ -2355,9 +2338,9 @@
    3.71    have "wf_prog G  \<longrightarrow> 
    3.72             (\<forall> c m. class G C = Some c \<longrightarrow>  methd G C sig = Some m 
    3.73                     \<longrightarrow>  methd G (declclass m) sig = Some m)"      (is "?P G C") 
    3.74 -  proof (rule class_rec.induct,intro allI impI)
    3.75 +  proof (induct G C rule: class_rec_induct', intro allI impI)
    3.76      fix G C c m
    3.77 -    assume hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c \<longrightarrow>
    3.78 +    assume hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object \<Longrightarrow>
    3.79                       ?P G (super c)"
    3.80      assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
    3.81              m: "methd G C sig = Some m"
     4.1 --- a/src/HOL/Lambda/ParRed.thy	Mon Mar 01 18:49:55 2010 +0100
     4.2 +++ b/src/HOL/Lambda/ParRed.thy	Tue Mar 02 12:26:50 2010 +0100
     4.3 @@ -85,14 +85,14 @@
     4.4  
     4.5  subsection {* Complete developments *}
     4.6  
     4.7 -consts
     4.8 +fun
     4.9    "cd" :: "dB => dB"
    4.10 -recdef "cd" "measure size"
    4.11 +where
    4.12    "cd (Var n) = Var n"
    4.13 -  "cd (Var n \<degree> t) = Var n \<degree> cd t"
    4.14 -  "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
    4.15 -  "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
    4.16 -  "cd (Abs s) = Abs (cd s)"
    4.17 +| "cd (Var n \<degree> t) = Var n \<degree> cd t"
    4.18 +| "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
    4.19 +| "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
    4.20 +| "cd (Abs s) = Abs (cd s)"
    4.21  
    4.22  lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s"
    4.23    apply (induct s arbitrary: t rule: cd.induct)
     5.1 --- a/src/HOL/Library/Word.thy	Mon Mar 01 18:49:55 2010 +0100
     5.2 +++ b/src/HOL/Library/Word.thy	Tue Mar 02 12:26:50 2010 +0100
     5.3 @@ -311,11 +311,11 @@
     5.4  lemma norm_unsigned_idem [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w"
     5.5    by (rule bit_list_induct [of _ w],simp_all)
     5.6  
     5.7 -consts
     5.8 +fun
     5.9    nat_to_bv_helper :: "nat => bit list => bit list"
    5.10 -recdef nat_to_bv_helper "measure (\<lambda>n. n)"
    5.11 -  "nat_to_bv_helper n = (%bs. (if n = 0 then bs
    5.12 -                               else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
    5.13 +where
    5.14 +  "nat_to_bv_helper n bs = (if n = 0 then bs
    5.15 +                               else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs))"
    5.16  
    5.17  definition
    5.18    nat_to_bv :: "nat => bit list" where
     6.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Mon Mar 01 18:49:55 2010 +0100
     6.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Tue Mar 02 12:26:50 2010 +0100
     6.3 @@ -34,33 +34,34 @@
     6.4  | "succs Throw pc              = [pc]"
     6.5  
     6.6  text "Effect of instruction on the state type:"
     6.7 -consts 
     6.8 -eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
     6.9  
    6.10 -recdef eff' "{}"
    6.11 -"eff' (Load idx,  G, (ST, LT))          = (ok_val (LT ! idx) # ST, LT)"
    6.12 -"eff' (Store idx, G, (ts#ST, LT))       = (ST, LT[idx:= OK ts])"
    6.13 -"eff' (LitPush v, G, (ST, LT))           = (the (typeof (\<lambda>v. None) v) # ST, LT)"
    6.14 -"eff' (Getfield F C, G, (oT#ST, LT))    = (snd (the (field (G,C) F)) # ST, LT)"
    6.15 -"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)"
    6.16 -"eff' (New C, G, (ST,LT))               = (Class C # ST, LT)"
    6.17 -"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)"
    6.18 -"eff' (Pop, G, (ts#ST,LT))              = (ST,LT)"
    6.19 -"eff' (Dup, G, (ts#ST,LT))              = (ts#ts#ST,LT)"
    6.20 -"eff' (Dup_x1, G, (ts1#ts2#ST,LT))      = (ts1#ts2#ts1#ST,LT)"
    6.21 -"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT))  = (ts1#ts2#ts3#ts1#ST,LT)"
    6.22 -"eff' (Swap, G, (ts1#ts2#ST,LT))        = (ts2#ts1#ST,LT)"
    6.23 +fun eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
    6.24 +where
    6.25 +"eff' (Load idx,  G, (ST, LT))          = (ok_val (LT ! idx) # ST, LT)" |
    6.26 +"eff' (Store idx, G, (ts#ST, LT))       = (ST, LT[idx:= OK ts])" |
    6.27 +"eff' (LitPush v, G, (ST, LT))           = (the (typeof (\<lambda>v. None) v) # ST, LT)" |
    6.28 +"eff' (Getfield F C, G, (oT#ST, LT))    = (snd (the (field (G,C) F)) # ST, LT)" |
    6.29 +"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)" |
    6.30 +"eff' (New C, G, (ST,LT))               = (Class C # ST, LT)" |
    6.31 +"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)" |
    6.32 +"eff' (Pop, G, (ts#ST,LT))              = (ST,LT)" |
    6.33 +"eff' (Dup, G, (ts#ST,LT))              = (ts#ts#ST,LT)" |
    6.34 +"eff' (Dup_x1, G, (ts1#ts2#ST,LT))      = (ts1#ts2#ts1#ST,LT)" |
    6.35 +"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT))  = (ts1#ts2#ts3#ts1#ST,LT)" |
    6.36 +"eff' (Swap, G, (ts1#ts2#ST,LT))        = (ts2#ts1#ST,LT)" |
    6.37  "eff' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) 
    6.38 -                                         = (PrimT Integer#ST,LT)"
    6.39 -"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT))   = (ST,LT)"
    6.40 -"eff' (Goto b, G, s)                    = s"
    6.41 +                                         = (PrimT Integer#ST,LT)" |
    6.42 +"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT))   = (ST,LT)" |
    6.43 +"eff' (Goto b, G, s)                    = s" |
    6.44    -- "Return has no successor instruction in the same method"
    6.45 -"eff' (Return, G, s)                    = s" 
    6.46 +"eff' (Return, G, s)                    = s" |
    6.47    -- "Throw always terminates abruptly"
    6.48 -"eff' (Throw, G, s)                     = s"
    6.49 +"eff' (Throw, G, s)                     = s" |
    6.50  "eff' (Invoke C mn fpTs, G, (ST,LT))    = (let ST' = drop (length fpTs) ST 
    6.51    in  (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" 
    6.52  
    6.53 +
    6.54 +
    6.55  primrec match_any :: "jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list" where
    6.56    "match_any G pc [] = []"
    6.57  | "match_any G pc (e#es) = (let (start_pc, end_pc, handler_pc, catch_type) = e;
    6.58 @@ -77,16 +78,16 @@
    6.59    "match G X pc et = (if \<exists>e \<in> set et. match_exception_entry G (Xcpt X) pc e then [Xcpt X] else [])"
    6.60    by (induct et) auto
    6.61  
    6.62 -consts
    6.63 +fun
    6.64    xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table \<Rightarrow> cname list" 
    6.65 -recdef xcpt_names "{}"
    6.66 +where
    6.67    "xcpt_names (Getfield F C, G, pc, et) = match G NullPointer pc et" 
    6.68 -  "xcpt_names (Putfield F C, G, pc, et) = match G NullPointer pc et" 
    6.69 -  "xcpt_names (New C, G, pc, et)        = match G OutOfMemory pc et"
    6.70 -  "xcpt_names (Checkcast C, G, pc, et)  = match G ClassCast pc et"
    6.71 -  "xcpt_names (Throw, G, pc, et)        = match_any G pc et"
    6.72 -  "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et" 
    6.73 -  "xcpt_names (i, G, pc, et)            = []" 
    6.74 +| "xcpt_names (Putfield F C, G, pc, et) = match G NullPointer pc et" 
    6.75 +| "xcpt_names (New C, G, pc, et)        = match G OutOfMemory pc et"
    6.76 +| "xcpt_names (Checkcast C, G, pc, et)  = match G ClassCast pc et"
    6.77 +| "xcpt_names (Throw, G, pc, et)        = match_any G pc et"
    6.78 +| "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et" 
    6.79 +| "xcpt_names (i, G, pc, et)            = []" 
    6.80  
    6.81  
    6.82  definition xcpt_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> state_type option \<Rightarrow> exception_table \<Rightarrow> succ_type" where
    6.83 @@ -118,53 +119,53 @@
    6.84  
    6.85  
    6.86  text "Conditions under which eff is applicable:"
    6.87 -consts
    6.88 +
    6.89 +fun
    6.90  app' :: "instr \<times> jvm_prog \<times> p_count \<times> nat \<times> ty \<times> state_type \<Rightarrow> bool"
    6.91 -
    6.92 -recdef app' "{}"
    6.93 +where
    6.94  "app' (Load idx, G, pc, maxs, rT, s) = 
    6.95 -  (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> length (fst s) < maxs)"
    6.96 +  (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> length (fst s) < maxs)" |
    6.97  "app' (Store idx, G, pc, maxs, rT, (ts#ST, LT)) = 
    6.98 -  (idx < length LT)"
    6.99 +  (idx < length LT)" |
   6.100  "app' (LitPush v, G, pc, maxs, rT, s) = 
   6.101 -  (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)"
   6.102 +  (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)" |
   6.103  "app' (Getfield F C, G, pc, maxs, rT, (oT#ST, LT)) = 
   6.104    (is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and> 
   6.105 -  G \<turnstile> oT \<preceq> (Class C))"
   6.106 +  G \<turnstile> oT \<preceq> (Class C))" |
   6.107  "app' (Putfield F C, G, pc, maxs, rT, (vT#oT#ST, LT)) = 
   6.108    (is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
   6.109 -  G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" 
   6.110 +  G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" |
   6.111  "app' (New C, G, pc, maxs, rT, s) = 
   6.112 -  (is_class G C \<and> length (fst s) < maxs)"
   6.113 +  (is_class G C \<and> length (fst s) < maxs)" |
   6.114  "app' (Checkcast C, G, pc, maxs, rT, (RefT rt#ST,LT)) = 
   6.115 -  (is_class G C)"
   6.116 +  (is_class G C)" |
   6.117  "app' (Pop, G, pc, maxs, rT, (ts#ST,LT)) = 
   6.118 -  True"
   6.119 +  True" |
   6.120  "app' (Dup, G, pc, maxs, rT, (ts#ST,LT)) = 
   6.121 -  (1+length ST < maxs)"
   6.122 +  (1+length ST < maxs)" |
   6.123  "app' (Dup_x1, G, pc, maxs, rT, (ts1#ts2#ST,LT)) = 
   6.124 -  (2+length ST < maxs)"
   6.125 +  (2+length ST < maxs)" |
   6.126  "app' (Dup_x2, G, pc, maxs, rT, (ts1#ts2#ts3#ST,LT)) = 
   6.127 -  (3+length ST < maxs)"
   6.128 +  (3+length ST < maxs)" |
   6.129  "app' (Swap, G, pc, maxs, rT, (ts1#ts2#ST,LT)) = 
   6.130 -  True"
   6.131 +  True" |
   6.132  "app' (IAdd, G, pc, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT)) =
   6.133 -  True"
   6.134 +  True" |
   6.135  "app' (Ifcmpeq b, G, pc, maxs, rT, (ts#ts'#ST,LT)) = 
   6.136 -  (0 \<le> int pc + b \<and> (isPrimT ts \<and> ts' = ts \<or> isRefT ts \<and> isRefT ts'))"
   6.137 +  (0 \<le> int pc + b \<and> (isPrimT ts \<and> ts' = ts \<or> isRefT ts \<and> isRefT ts'))" |
   6.138  "app' (Goto b, G, pc, maxs, rT, s) = 
   6.139 -  (0 \<le> int pc + b)"
   6.140 +  (0 \<le> int pc + b)" |
   6.141  "app' (Return, G, pc, maxs, rT, (T#ST,LT)) = 
   6.142 -  (G \<turnstile> T \<preceq> rT)"
   6.143 +  (G \<turnstile> T \<preceq> rT)" |
   6.144  "app' (Throw, G, pc, maxs, rT, (T#ST,LT)) = 
   6.145 -  isRefT T"
   6.146 +  isRefT T" |
   6.147  "app' (Invoke C mn fpTs, G, pc, maxs, rT, s) = 
   6.148    (length fpTs < length (fst s) \<and> 
   6.149    (let apTs = rev (take (length fpTs) (fst s));
   6.150         X    = hd (drop (length fpTs) (fst s)) 
   6.151     in  
   6.152         G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and>
   6.153 -       list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))"
   6.154 +       list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))" |
   6.155    
   6.156  "app' (i,G, pc,maxs,rT,s) = False"
   6.157  
   6.158 @@ -208,7 +209,7 @@
   6.159  qed auto
   6.160  
   6.161  lemma 2: "\<not>(2 < length a) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
   6.162 -proof -;
   6.163 +proof -
   6.164    assume "\<not>(2 < length a)"
   6.165    hence "length a < (Suc (Suc (Suc 0)))" by simp
   6.166    hence * : "length a = 0 \<or> length a = Suc 0 \<or> length a = Suc (Suc 0)" 
   6.167 @@ -268,7 +269,7 @@
   6.168    "(app (Checkcast C) G maxs rT pc et (Some s)) =  
   6.169    (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C \<and>
   6.170    (\<forall>x \<in> set (match G ClassCast pc et). is_class G x))"
   6.171 -  by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)
   6.172 +  by (cases s, cases "fst s", simp) (cases "hd (fst s)", auto)
   6.173  
   6.174  lemma appPop[simp]: 
   6.175  "(app Pop G maxs rT pc et (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))"
   6.176 @@ -359,7 +360,7 @@
   6.177      assume app: "?app (a,b)"
   6.178      hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> 
   6.179             length fpTs < length a" (is "?a \<and> ?l") 
   6.180 -      by (auto simp add: app_def)
   6.181 +      by auto
   6.182      hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") 
   6.183        by auto
   6.184      hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" 
   6.185 @@ -374,7 +375,7 @@
   6.186      hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs" 
   6.187        by blast
   6.188      with app
   6.189 -    show ?thesis by (unfold app_def, clarsimp) blast
   6.190 +    show ?thesis by clarsimp blast
   6.191    qed
   6.192    with Pair 
   6.193    have "?app s \<Longrightarrow> ?P s" by (simp only:)
     7.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy	Mon Mar 01 18:49:55 2010 +0100
     7.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Mar 02 12:26:50 2010 +0100
     7.3 @@ -8,21 +8,19 @@
     7.4  theory JVMExec imports JVMExecInstr JVMExceptions begin
     7.5  
     7.6  
     7.7 -consts
     7.8 +fun
     7.9    exec :: "jvm_prog \<times> jvm_state => jvm_state option"
    7.10 -
    7.11 -
    7.12 --- "exec is not recursive. recdef is just used for pattern matching"
    7.13 -recdef exec "{}"
    7.14 +-- "exec is not recursive. fun is just used for pattern matching"
    7.15 +where
    7.16    "exec (G, xp, hp, []) = None"
    7.17  
    7.18 -  "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
    7.19 +| "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
    7.20    (let 
    7.21       i = fst(snd(snd(snd(snd(the(method (G,C) sig)))))) ! pc;
    7.22       (xcpt', hp', frs') = exec_instr i G hp stk loc C sig pc frs
    7.23     in Some (find_handler G xcpt' hp' frs'))"
    7.24  
    7.25 -  "exec (G, Some xp, hp, frs) = None" 
    7.26 +| "exec (G, Some xp, hp, frs) = None" 
    7.27  
    7.28  
    7.29  definition exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
     8.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Mon Mar 01 18:49:55 2010 +0100
     8.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Tue Mar 02 12:26:50 2010 +0100
     8.3 @@ -25,20 +25,18 @@
     8.4    | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
     8.5        \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
     8.6  
     8.7 -consts
     8.8 -  BnorRset :: "int * int => int set"
     8.9 -
    8.10 -recdef BnorRset
    8.11 -  "measure ((\<lambda>(a, m). nat a) :: int * int => nat)"
    8.12 -  "BnorRset (a, m) =
    8.13 +fun
    8.14 +  BnorRset :: "int \<Rightarrow> int => int set"
    8.15 +where
    8.16 +  "BnorRset a m =
    8.17     (if 0 < a then
    8.18 -    let na = BnorRset (a - 1, m)
    8.19 +    let na = BnorRset (a - 1) m
    8.20      in (if zgcd a m = 1 then insert a na else na)
    8.21      else {})"
    8.22  
    8.23  definition
    8.24    norRRset :: "int => int set" where
    8.25 -  "norRRset m = BnorRset (m - 1, m)"
    8.26 +  "norRRset m = BnorRset (m - 1) m"
    8.27  
    8.28  definition
    8.29    noXRRset :: "int => int => int set" where
    8.30 @@ -74,28 +72,27 @@
    8.31  
    8.32  lemma BnorRset_induct:
    8.33    assumes "!!a m. P {} a m"
    8.34 -    and "!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m
    8.35 -      ==> P (BnorRset(a,m)) a m"
    8.36 -  shows "P (BnorRset(u,v)) u v"
    8.37 +    and "!!a m :: int. 0 < a ==> P (BnorRset (a - 1) m) (a - 1) m
    8.38 +      ==> P (BnorRset a m) a m"
    8.39 +  shows "P (BnorRset u v) u v"
    8.40    apply (rule BnorRset.induct)
    8.41 -  apply safe
    8.42 -   apply (case_tac [2] "0 < a")
    8.43 -    apply (rule_tac [2] prems)
    8.44 +   apply (case_tac "0 < a")
    8.45 +    apply (rule_tac assms)
    8.46       apply simp_all
    8.47 -   apply (simp_all add: BnorRset.simps prems)
    8.48 +   apply (simp_all add: BnorRset.simps assms)
    8.49    done
    8.50  
    8.51 -lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) \<longrightarrow> b \<le> a"
    8.52 +lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset a m \<longrightarrow> b \<le> a"
    8.53    apply (induct a m rule: BnorRset_induct)
    8.54     apply simp
    8.55    apply (subst BnorRset.simps)
    8.56     apply (unfold Let_def, auto)
    8.57    done
    8.58  
    8.59 -lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
    8.60 +lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset a m"
    8.61    by (auto dest: Bnor_mem_zle)
    8.62  
    8.63 -lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b"
    8.64 +lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset a m --> 0 < b"
    8.65    apply (induct a m rule: BnorRset_induct)
    8.66     prefer 2
    8.67     apply (subst BnorRset.simps)
    8.68 @@ -103,7 +100,7 @@
    8.69    done
    8.70  
    8.71  lemma Bnor_mem_if [rule_format]:
    8.72 -    "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
    8.73 +    "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset a m"
    8.74    apply (induct a m rule: BnorRset.induct, auto)
    8.75     apply (subst BnorRset.simps)
    8.76     defer
    8.77 @@ -111,7 +108,7 @@
    8.78     apply (unfold Let_def, auto)
    8.79    done
    8.80  
    8.81 -lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \<in> RsetR m"
    8.82 +lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset a m \<in> RsetR m"
    8.83    apply (induct a m rule: BnorRset_induct, simp)
    8.84    apply (subst BnorRset.simps)
    8.85    apply (unfold Let_def, auto)
    8.86 @@ -124,7 +121,7 @@
    8.87          apply (rule_tac [5] Bnor_mem_zg, auto)
    8.88    done
    8.89  
    8.90 -lemma Bnor_fin: "finite (BnorRset (a, m))"
    8.91 +lemma Bnor_fin: "finite (BnorRset a m)"
    8.92    apply (induct a m rule: BnorRset_induct)
    8.93     prefer 2
    8.94     apply (subst BnorRset.simps)
    8.95 @@ -258,8 +255,8 @@
    8.96  by (unfold inj_on_def, auto)
    8.97  
    8.98  lemma Bnor_prod_power [rule_format]:
    8.99 -  "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset (a, m)) =
   8.100 -      \<Prod>(BnorRset(a, m)) * x^card (BnorRset (a, m))"
   8.101 +  "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset a m) =
   8.102 +      \<Prod>(BnorRset a m) * x^card (BnorRset a m)"
   8.103    apply (induct a m rule: BnorRset_induct)
   8.104     prefer 2
   8.105     apply (simplesubst BnorRset.simps)  --{*multiple redexes*}
   8.106 @@ -284,7 +281,7 @@
   8.107    done
   8.108  
   8.109  lemma Bnor_prod_zgcd [rule_format]:
   8.110 -    "a < m --> zgcd (\<Prod>(BnorRset(a, m))) m = 1"
   8.111 +    "a < m --> zgcd (\<Prod>(BnorRset a m)) m = 1"
   8.112    apply (induct a m rule: BnorRset_induct)
   8.113     prefer 2
   8.114     apply (subst BnorRset.simps)
   8.115 @@ -299,13 +296,13 @@
   8.116    apply (case_tac "x = 0")
   8.117     apply (case_tac [2] "m = 1")
   8.118      apply (rule_tac [3] iffD1)
   8.119 -     apply (rule_tac [3] k = "\<Prod>(BnorRset(m - 1, m))"
   8.120 +     apply (rule_tac [3] k = "\<Prod>(BnorRset (m - 1) m)"
   8.121         in zcong_cancel2)
   8.122        prefer 5
   8.123        apply (subst Bnor_prod_power [symmetric])
   8.124          apply (rule_tac [7] Bnor_prod_zgcd, simp_all)
   8.125    apply (rule bijzcong_zcong_prod)
   8.126 -  apply (fold norRRset_def noXRRset_def)
   8.127 +  apply (fold norRRset_def, fold noXRRset_def)
   8.128    apply (subst RRset2norRR_eq_norR [symmetric])
   8.129      apply (rule_tac [3] inj_func_bijR, auto)
   8.130       apply (unfold zcongm_def)
   8.131 @@ -319,12 +316,12 @@
   8.132    done
   8.133  
   8.134  lemma Bnor_prime:
   8.135 -  "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset (a, p)) = nat a"
   8.136 +  "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset a p) = nat a"
   8.137    apply (induct a p rule: BnorRset.induct)
   8.138    apply (subst BnorRset.simps)
   8.139    apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime)
   8.140 -  apply (subgoal_tac "finite (BnorRset (a - 1,m))")
   8.141 -   apply (subgoal_tac "a ~: BnorRset (a - 1,m)")
   8.142 +  apply (subgoal_tac "finite (BnorRset (a - 1) m)")
   8.143 +   apply (subgoal_tac "a ~: BnorRset (a - 1) m")
   8.144      apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1)
   8.145     apply (frule Bnor_mem_zle, arith)
   8.146    apply (frule Bnor_fin)
     9.1 --- a/src/HOL/Old_Number_Theory/IntFact.thy	Mon Mar 01 18:49:55 2010 +0100
     9.2 +++ b/src/HOL/Old_Number_Theory/IntFact.thy	Tue Mar 02 12:26:50 2010 +0100
     9.3 @@ -14,14 +14,14 @@
     9.4    \bigskip
     9.5  *}
     9.6  
     9.7 -consts
     9.8 +fun
     9.9    zfact :: "int => int"
    9.10 -  d22set :: "int => int set"
    9.11 -
    9.12 -recdef zfact  "measure ((\<lambda>n. nat n) :: int => nat)"
    9.13 +where
    9.14    "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
    9.15  
    9.16 -recdef d22set  "measure ((\<lambda>a. nat a) :: int => nat)"
    9.17 +fun
    9.18 +  d22set :: "int => int set"
    9.19 +where
    9.20    "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
    9.21  
    9.22  
    9.23 @@ -38,12 +38,10 @@
    9.24      and "!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1) ==> P (d22set a) a"
    9.25    shows "P (d22set u) u"
    9.26    apply (rule d22set.induct)
    9.27 -  apply safe
    9.28 -   prefer 2
    9.29 -   apply (case_tac "1 < a")
    9.30 -    apply (rule_tac prems)
    9.31 -     apply (simp_all (no_asm_simp))
    9.32 -   apply (simp_all (no_asm_simp) add: d22set.simps prems)
    9.33 +  apply (case_tac "1 < a")
    9.34 +   apply (rule_tac assms)
    9.35 +    apply (simp_all (no_asm_simp))
    9.36 +  apply (simp_all (no_asm_simp) add: d22set.simps assms)
    9.37    done
    9.38  
    9.39  lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> 1 < b"
    9.40 @@ -66,7 +64,8 @@
    9.41  lemma d22set_mem: "1 < b \<Longrightarrow> b \<le> a \<Longrightarrow> b \<in> d22set a"
    9.42    apply (induct a rule: d22set.induct)
    9.43    apply auto
    9.44 -   apply (simp_all add: d22set.simps)
    9.45 +  apply (subst d22set.simps)
    9.46 +  apply (case_tac "b < a", auto)
    9.47    done
    9.48  
    9.49  lemma d22set_fin: "finite (d22set a)"
    9.50 @@ -81,8 +80,6 @@
    9.51  
    9.52  lemma d22set_prod_zfact: "\<Prod>(d22set a) = zfact a"
    9.53    apply (induct a rule: d22set.induct)
    9.54 -  apply safe
    9.55 -   apply (simp add: d22set.simps zfact.simps)
    9.56    apply (subst d22set.simps)
    9.57    apply (subst zfact.simps)
    9.58    apply (case_tac "1 < a")
    10.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Mon Mar 01 18:49:55 2010 +0100
    10.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Mar 02 12:26:50 2010 +0100
    10.3 @@ -19,17 +19,14 @@
    10.4  
    10.5  subsection {* Definitions *}
    10.6  
    10.7 -consts
    10.8 -  xzgcda :: "int * int * int * int * int * int * int * int => int * int * int"
    10.9 -
   10.10 -recdef xzgcda
   10.11 -  "measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r)
   10.12 -    :: int * int * int * int *int * int * int * int => nat)"
   10.13 -  "xzgcda (m, n, r', r, s', s, t', t) =
   10.14 +fun
   10.15 +  xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
   10.16 +where
   10.17 +  "xzgcda m n r' r s' s t' t =
   10.18          (if r \<le> 0 then (r', s', t')
   10.19 -         else xzgcda (m, n, r, r' mod r, 
   10.20 -                      s, s' - (r' div r) * s, 
   10.21 -                      t, t' - (r' div r) * t))"
   10.22 +         else xzgcda m n r (r' mod r) 
   10.23 +                      s (s' - (r' div r) * s) 
   10.24 +                      t (t' - (r' div r) * t))"
   10.25  
   10.26  definition
   10.27    zprime :: "int \<Rightarrow> bool" where
   10.28 @@ -37,7 +34,7 @@
   10.29  
   10.30  definition
   10.31    xzgcd :: "int => int => int * int * int" where
   10.32 -  "xzgcd m n = xzgcda (m, n, m, n, 1, 0, 0, 1)"
   10.33 +  "xzgcd m n = xzgcda m n m n 1 0 0 1"
   10.34  
   10.35  definition
   10.36    zcong :: "int => int => int => bool"  ("(1[_ = _] '(mod _'))") where
   10.37 @@ -307,9 +304,8 @@
   10.38  
   10.39  lemma xzgcd_correct_aux1:
   10.40    "zgcd r' r = k --> 0 < r -->
   10.41 -    (\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))"
   10.42 -  apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   10.43 -    z = s and aa = t' and ab = t in xzgcda.induct)
   10.44 +    (\<exists>sn tn. xzgcda m n r' r s' s t' t = (k, sn, tn))"
   10.45 +  apply (induct m n r' r s' s t' t rule: xzgcda.induct)
   10.46    apply (subst zgcd_eq)
   10.47    apply (subst xzgcda.simps, auto)
   10.48    apply (case_tac "r' mod r = 0")
   10.49 @@ -321,17 +317,16 @@
   10.50    done
   10.51  
   10.52  lemma xzgcd_correct_aux2:
   10.53 -  "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r -->
   10.54 +  "(\<exists>sn tn. xzgcda m n r' r s' s t' t = (k, sn, tn)) --> 0 < r -->
   10.55      zgcd r' r = k"
   10.56 -  apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   10.57 -    z = s and aa = t' and ab = t in xzgcda.induct)
   10.58 +  apply (induct m n r' r s' s t' t rule: xzgcda.induct)
   10.59    apply (subst zgcd_eq)
   10.60    apply (subst xzgcda.simps)
   10.61    apply (auto simp add: linorder_not_le)
   10.62    apply (case_tac "r' mod r = 0")
   10.63     prefer 2
   10.64     apply (frule_tac a = "r'" in pos_mod_sign, auto)
   10.65 -  apply (metis Pair_eq simps zle_refl)
   10.66 +  apply (metis Pair_eq xzgcda.simps zle_refl)
   10.67    done
   10.68  
   10.69  lemma xzgcd_correct:
   10.70 @@ -362,10 +357,9 @@
   10.71    by (rule iffD2 [OF order_less_le conjI])
   10.72  
   10.73  lemma xzgcda_linear [rule_format]:
   10.74 -  "0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) -->
   10.75 +  "0 < r --> xzgcda m n r' r s' s t' t = (rn, sn, tn) -->
   10.76      r' = s' * m + t' * n -->  r = s * m + t * n --> rn = sn * m + tn * n"
   10.77 -  apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   10.78 -    z = s and aa = t' and ab = t in xzgcda.induct)
   10.79 +  apply (induct m n r' r s' s t' t rule: xzgcda.induct)
   10.80    apply (subst xzgcda.simps)
   10.81    apply (simp (no_asm))
   10.82    apply (rule impI)+
    11.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Mar 01 18:49:55 2010 +0100
    11.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Mar 02 12:26:50 2010 +0100
    11.3 @@ -17,14 +17,12 @@
    11.4    inv :: "int => int => int" where
    11.5    "inv p a = (a^(nat (p - 2))) mod p"
    11.6  
    11.7 -consts
    11.8 -  wset :: "int * int => int set"
    11.9 -
   11.10 -recdef wset
   11.11 -  "measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
   11.12 -  "wset (a, p) =
   11.13 +fun
   11.14 +  wset :: "int \<Rightarrow> int => int set"
   11.15 +where
   11.16 +  "wset a p =
   11.17      (if 1 < a then
   11.18 -      let ws = wset (a - 1, p)
   11.19 +      let ws = wset (a - 1) p
   11.20        in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})"
   11.21  
   11.22  
   11.23 @@ -163,35 +161,33 @@
   11.24  lemma wset_induct:
   11.25    assumes "!!a p. P {} a p"
   11.26      and "!!a p. 1 < (a::int) \<Longrightarrow>
   11.27 -      P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
   11.28 -  shows "P (wset (u, v)) u v"
   11.29 -  apply (rule wset.induct, safe)
   11.30 -   prefer 2
   11.31 -   apply (case_tac "1 < a")
   11.32 -    apply (rule prems)
   11.33 -     apply simp_all
   11.34 -   apply (simp_all add: wset.simps prems)
   11.35 +      P (wset (a - 1) p) (a - 1) p ==> P (wset a p) a p"
   11.36 +  shows "P (wset u v) u v"
   11.37 +  apply (rule wset.induct)
   11.38 +  apply (case_tac "1 < a")
   11.39 +   apply (rule assms)
   11.40 +    apply (simp_all add: wset.simps assms)
   11.41    done
   11.42  
   11.43  lemma wset_mem_imp_or [rule_format]:
   11.44 -  "1 < a \<Longrightarrow> b \<notin> wset (a - 1, p)
   11.45 -    ==> b \<in> wset (a, p) --> b = a \<or> b = inv p a"
   11.46 +  "1 < a \<Longrightarrow> b \<notin> wset (a - 1) p
   11.47 +    ==> b \<in> wset a p --> b = a \<or> b = inv p a"
   11.48    apply (subst wset.simps)
   11.49    apply (unfold Let_def, simp)
   11.50    done
   11.51  
   11.52 -lemma wset_mem_mem [simp]: "1 < a ==> a \<in> wset (a, p)"
   11.53 +lemma wset_mem_mem [simp]: "1 < a ==> a \<in> wset a p"
   11.54    apply (subst wset.simps)
   11.55    apply (unfold Let_def, simp)
   11.56    done
   11.57  
   11.58 -lemma wset_subset: "1 < a \<Longrightarrow> b \<in> wset (a - 1, p) ==> b \<in> wset (a, p)"
   11.59 +lemma wset_subset: "1 < a \<Longrightarrow> b \<in> wset (a - 1) p ==> b \<in> wset a p"
   11.60    apply (subst wset.simps)
   11.61    apply (unfold Let_def, auto)
   11.62    done
   11.63  
   11.64  lemma wset_g_1 [rule_format]:
   11.65 -    "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> 1 < b"
   11.66 +    "zprime p --> a < p - 1 --> b \<in> wset a p --> 1 < b"
   11.67    apply (induct a p rule: wset_induct, auto)
   11.68    apply (case_tac "b = a")
   11.69     apply (case_tac [2] "b = inv p a")
   11.70 @@ -203,7 +199,7 @@
   11.71    done
   11.72  
   11.73  lemma wset_less [rule_format]:
   11.74 -    "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> b < p - 1"
   11.75 +    "zprime p --> a < p - 1 --> b \<in> wset a p --> b < p - 1"
   11.76    apply (induct a p rule: wset_induct, auto)
   11.77    apply (case_tac "b = a")
   11.78     apply (case_tac [2] "b = inv p a")
   11.79 @@ -216,7 +212,7 @@
   11.80  
   11.81  lemma wset_mem [rule_format]:
   11.82    "zprime p -->
   11.83 -    a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset (a, p)"
   11.84 +    a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset a p"
   11.85    apply (induct a p rule: wset.induct, auto)
   11.86    apply (rule_tac wset_subset)
   11.87    apply (simp (no_asm_simp))
   11.88 @@ -224,8 +220,8 @@
   11.89    done
   11.90  
   11.91  lemma wset_mem_inv_mem [rule_format]:
   11.92 -  "zprime p --> 5 \<le> p --> a < p - 1 --> b \<in> wset (a, p)
   11.93 -    --> inv p b \<in> wset (a, p)"
   11.94 +  "zprime p --> 5 \<le> p --> a < p - 1 --> b \<in> wset a p
   11.95 +    --> inv p b \<in> wset a p"
   11.96    apply (induct a p rule: wset_induct, auto)
   11.97     apply (case_tac "b = a")
   11.98      apply (subst wset.simps)
   11.99 @@ -240,13 +236,13 @@
  11.100  
  11.101  lemma wset_inv_mem_mem:
  11.102    "zprime p \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - 1 \<Longrightarrow> 1 < b \<Longrightarrow> b < p - 1
  11.103 -    \<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
  11.104 +    \<Longrightarrow> inv p b \<in> wset a p \<Longrightarrow> b \<in> wset a p"
  11.105    apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
  11.106     apply (rule_tac [2] wset_mem_inv_mem)
  11.107        apply (rule inv_inv, simp_all)
  11.108    done
  11.109  
  11.110 -lemma wset_fin: "finite (wset (a, p))"
  11.111 +lemma wset_fin: "finite (wset a p)"
  11.112    apply (induct a p rule: wset_induct)
  11.113     prefer 2
  11.114     apply (subst wset.simps)
  11.115 @@ -255,27 +251,27 @@
  11.116  
  11.117  lemma wset_zcong_prod_1 [rule_format]:
  11.118    "zprime p -->
  11.119 -    5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset(a, p). x) = 1] (mod p)"
  11.120 +    5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset a p. x) = 1] (mod p)"
  11.121    apply (induct a p rule: wset_induct)
  11.122     prefer 2
  11.123     apply (subst wset.simps)
  11.124 -   apply (unfold Let_def, auto)
  11.125 +   apply (auto, unfold Let_def, auto)
  11.126    apply (subst setprod_insert)
  11.127      apply (tactic {* stac (thm "setprod_insert") 3 *})
  11.128        apply (subgoal_tac [5]
  11.129 -        "zcong (a * inv p a * (\<Prod>x\<in> wset(a - 1, p). x)) (1 * 1) p")
  11.130 +        "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
  11.131         prefer 5
  11.132         apply (simp add: zmult_assoc)
  11.133        apply (rule_tac [5] zcong_zmult)
  11.134         apply (rule_tac [5] inv_is_inv)
  11.135           apply (tactic "clarify_tac @{claset} 4")
  11.136 -         apply (subgoal_tac [4] "a \<in> wset (a - 1, p)")
  11.137 +         apply (subgoal_tac [4] "a \<in> wset (a - 1) p")
  11.138            apply (rule_tac [5] wset_inv_mem_mem)
  11.139                 apply (simp_all add: wset_fin)
  11.140    apply (rule inv_distinct, auto)
  11.141    done
  11.142  
  11.143 -lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2, p)"
  11.144 +lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2) p"
  11.145    apply safe
  11.146     apply (erule wset_mem)
  11.147       apply (rule_tac [2] d22set_g_1)
    12.1 --- a/src/HOL/ZF/Games.thy	Mon Mar 01 18:49:55 2010 +0100
    12.2 +++ b/src/HOL/ZF/Games.thy	Tue Mar 02 12:26:50 2010 +0100
    12.3 @@ -1,4 +1,4 @@
    12.4 -(*  Title:      HOL/ZF/Games.thy
    12.5 +(*  Title:      HOL/ZF/MainZF.thy/Games.thy
    12.6      Author:     Steven Obua
    12.7  
    12.8  An application of HOLZF: Partizan Games.  See "Partizan Games in
    12.9 @@ -347,13 +347,12 @@
   12.10      right_option_def[symmetric] left_option_def[symmetric])
   12.11    done
   12.12  
   12.13 -consts
   12.14 +function
   12.15    neg_game :: "game \<Rightarrow> game"
   12.16 -
   12.17 -recdef neg_game "option_of"
   12.18 -  "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))"
   12.19 -
   12.20 -declare neg_game.simps[simp del]
   12.21 +where
   12.22 +  [simp del]: "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))"
   12.23 +by auto
   12.24 +termination by (relation "option_of") auto
   12.25  
   12.26  lemma "neg_game (neg_game g) = g"
   12.27    apply (induct g rule: neg_game.induct)
   12.28 @@ -365,17 +364,16 @@
   12.29    apply (auto simp add: zet_ext_eq zimage_iff)
   12.30    done
   12.31  
   12.32 -consts
   12.33 +function
   12.34    ge_game :: "(game * game) \<Rightarrow> bool" 
   12.35 -
   12.36 -recdef ge_game "(gprod_2_1 option_of)"
   12.37 -  "ge_game (G, H) = (\<forall> x. if zin x (right_options G) then (
   12.38 +where
   12.39 +  [simp del]: "ge_game (G, H) = (\<forall> x. if zin x (right_options G) then (
   12.40                            if zin x (left_options H) then \<not> (ge_game (H, x) \<or> (ge_game (x, G))) 
   12.41                                                      else \<not> (ge_game (H, x)))
   12.42                            else (if zin x (left_options H) then \<not> (ge_game (x, G)) else True))"
   12.43 -(hints simp: gprod_2_1_def)
   12.44 -
   12.45 -declare ge_game.simps [simp del]
   12.46 +by auto
   12.47 +termination by (relation "(gprod_2_1 option_of)") 
   12.48 + (simp, auto simp: gprod_2_1_def)
   12.49  
   12.50  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)))"
   12.51    apply (subst ge_game.simps[where G=G and H=H])
   12.52 @@ -506,19 +504,18 @@
   12.53  definition zero_game :: game
   12.54   where  "zero_game \<equiv> Game zempty zempty"
   12.55  
   12.56 -consts 
   12.57 -  plus_game :: "game * game \<Rightarrow> game"
   12.58 +function 
   12.59 +  plus_game :: "game \<Rightarrow> game \<Rightarrow> game"
   12.60 +where
   12.61 +  [simp del]: "plus_game G H = Game (zunion (zimage (\<lambda> g. plus_game g H) (left_options G))
   12.62 +                                   (zimage (\<lambda> h. plus_game G h) (left_options H)))
   12.63 +                           (zunion (zimage (\<lambda> g. plus_game g H) (right_options G))
   12.64 +                                   (zimage (\<lambda> h. plus_game G h) (right_options H)))"
   12.65 +by auto
   12.66 +termination by (relation "gprod_2_2 option_of")
   12.67 +  (simp, auto simp: gprod_2_2_def)
   12.68  
   12.69 -recdef plus_game "gprod_2_2 option_of"
   12.70 -  "plus_game (G, H) = Game (zunion (zimage (\<lambda> g. plus_game (g, H)) (left_options G))
   12.71 -                                   (zimage (\<lambda> h. plus_game (G, h)) (left_options H)))
   12.72 -                           (zunion (zimage (\<lambda> g. plus_game (g, H)) (right_options G))
   12.73 -                                   (zimage (\<lambda> h. plus_game (G, h)) (right_options H)))"
   12.74 -(hints simp add: gprod_2_2_def)
   12.75 -
   12.76 -declare plus_game.simps[simp del]
   12.77 -
   12.78 -lemma plus_game_comm: "plus_game (G, H) = plus_game (H, G)"
   12.79 +lemma plus_game_comm: "plus_game G H = plus_game H G"
   12.80  proof (induct G H rule: plus_game.induct)
   12.81    case (1 G H)
   12.82    show ?case
   12.83 @@ -541,11 +538,11 @@
   12.84  lemma right_zero_game[simp]: "right_options (zero_game) = zempty"
   12.85    by (simp add: zero_game_def)
   12.86  
   12.87 -lemma plus_game_zero_right[simp]: "plus_game (G, zero_game) = G"
   12.88 +lemma plus_game_zero_right[simp]: "plus_game G zero_game = G"
   12.89  proof -
   12.90    { 
   12.91      fix G H
   12.92 -    have "H = zero_game \<longrightarrow> plus_game (G, H) = G "
   12.93 +    have "H = zero_game \<longrightarrow> plus_game G H = G "
   12.94      proof (induct G H rule: plus_game.induct, rule impI)
   12.95        case (goal1 G H)
   12.96        note induct_hyp = prems[simplified goal1, simplified] and prems
   12.97 @@ -553,7 +550,7 @@
   12.98          apply (simp only: plus_game.simps[where G=G and H=H])
   12.99          apply (simp add: game_ext_eq prems)
  12.100          apply (auto simp add: 
  12.101 -          zimage_cong[where f = "\<lambda> g. plus_game (g, zero_game)" and g = "id"] 
  12.102 +          zimage_cong[where f = "\<lambda> g. plus_game g zero_game" and g = "id"] 
  12.103            induct_hyp)
  12.104          done
  12.105      qed
  12.106 @@ -561,7 +558,7 @@
  12.107    then show ?thesis by auto
  12.108  qed
  12.109  
  12.110 -lemma plus_game_zero_left: "plus_game (zero_game, G) = G"
  12.111 +lemma plus_game_zero_left: "plus_game zero_game G = G"
  12.112    by (simp add: plus_game_comm)
  12.113  
  12.114  lemma left_imp_options[simp]: "zin opt (left_options g) \<Longrightarrow> zin opt (options g)"
  12.115 @@ -571,11 +568,11 @@
  12.116    by (simp add: options_def zunion)
  12.117  
  12.118  lemma left_options_plus: 
  12.119 -  "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))" 
  12.120 +  "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))" 
  12.121    by (subst plus_game.simps, simp)
  12.122  
  12.123  lemma right_options_plus:
  12.124 -  "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))"
  12.125 +  "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))"
  12.126    by (subst plus_game.simps, simp)
  12.127  
  12.128  lemma left_options_neg: "left_options (neg_game u) = zimage neg_game (right_options u)"  
  12.129 @@ -584,32 +581,32 @@
  12.130  lemma right_options_neg: "right_options (neg_game u) = zimage neg_game (left_options u)"
  12.131    by (subst neg_game.simps, simp)
  12.132    
  12.133 -lemma plus_game_assoc: "plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))"
  12.134 +lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)"
  12.135  proof -
  12.136    { 
  12.137      fix a
  12.138 -    have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))"
  12.139 +    have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game F G) H = plus_game F (plus_game G H)"
  12.140      proof (induct a rule: induct_game, (rule impI | rule allI)+)
  12.141        case (goal1 x F G H)
  12.142 -      let ?L = "plus_game (plus_game (F, G), H)"
  12.143 -      let ?R = "plus_game (F, plus_game (G, H))"
  12.144 +      let ?L = "plus_game (plus_game F G) H"
  12.145 +      let ?R = "plus_game F (plus_game G H)"
  12.146        note options_plus = left_options_plus right_options_plus
  12.147        {
  12.148          fix opt
  12.149          note hyp = goal1(1)[simplified goal1(2), rule_format] 
  12.150 -        have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game (opt, G), H) = plus_game (opt, plus_game (G, H))"
  12.151 +        have F: "zin opt (options F)  \<Longrightarrow> plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
  12.152            by (blast intro: hyp lprod_3_3)
  12.153 -        have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game (F, opt), H) = plus_game (F, plus_game (opt, H))"
  12.154 +        have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
  12.155            by (blast intro: hyp lprod_3_4)
  12.156 -        have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game (F, G), opt) = plus_game (F, plus_game (G, opt))" 
  12.157 +        have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game F G) opt = plus_game F (plus_game G opt)" 
  12.158            by (blast intro: hyp lprod_3_5)
  12.159          note F and G and H
  12.160        }
  12.161        note induct_hyp = this
  12.162        have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
  12.163          by (auto simp add: 
  12.164 -          plus_game.simps[where G="plus_game (F,G)" and H=H]
  12.165 -          plus_game.simps[where G="F" and H="plus_game (G,H)"] 
  12.166 +          plus_game.simps[where G="plus_game F G" and H=H]
  12.167 +          plus_game.simps[where G="F" and H="plus_game G H"] 
  12.168            zet_ext_eq zunion zimage_iff options_plus
  12.169            induct_hyp left_imp_options right_imp_options)
  12.170        then show ?case
  12.171 @@ -619,7 +616,7 @@
  12.172    then show ?thesis by auto
  12.173  qed
  12.174  
  12.175 -lemma neg_plus_game: "neg_game (plus_game (G, H)) = plus_game(neg_game G, neg_game H)"
  12.176 +lemma neg_plus_game: "neg_game (plus_game G H) = plus_game (neg_game G) (neg_game H)"
  12.177  proof (induct G H rule: plus_game.induct)
  12.178    case (1 G H)
  12.179    note opt_ops = 
  12.180 @@ -627,26 +624,26 @@
  12.181      left_options_neg right_options_neg  
  12.182    show ?case
  12.183      by (auto simp add: opt_ops
  12.184 -      neg_game.simps[of "plus_game (G,H)"]
  12.185 +      neg_game.simps[of "plus_game G H"]
  12.186        plus_game.simps[of "neg_game G" "neg_game H"]
  12.187        Game_ext zet_ext_eq zunion zimage_iff prems)
  12.188  qed
  12.189  
  12.190 -lemma eq_game_plus_inverse: "eq_game (plus_game (x, neg_game x)) zero_game"
  12.191 +lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
  12.192  proof (induct x rule: wf_induct[OF wf_option_of])
  12.193    case (goal1 x)
  12.194    { fix y
  12.195      assume "zin y (options x)"
  12.196 -    then have "eq_game (plus_game (y, neg_game y)) zero_game"
  12.197 +    then have "eq_game (plus_game y (neg_game y)) zero_game"
  12.198        by (auto simp add: prems)
  12.199    }
  12.200    note ihyp = this
  12.201    {
  12.202      fix y
  12.203      assume y: "zin y (right_options x)"
  12.204 -    have "\<not> (ge_game (zero_game, plus_game (y, neg_game x)))"
  12.205 +    have "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
  12.206        apply (subst ge_game.simps, simp)
  12.207 -      apply (rule exI[where x="plus_game (y, neg_game y)"])
  12.208 +      apply (rule exI[where x="plus_game y (neg_game y)"])
  12.209        apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
  12.210        apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: prems)
  12.211        done
  12.212 @@ -655,9 +652,9 @@
  12.213    {
  12.214      fix y
  12.215      assume y: "zin y (left_options x)"
  12.216 -    have "\<not> (ge_game (zero_game, plus_game (x, neg_game y)))"
  12.217 +    have "\<not> (ge_game (zero_game, plus_game x (neg_game y)))"
  12.218        apply (subst ge_game.simps, simp)
  12.219 -      apply (rule exI[where x="plus_game (y, neg_game y)"])
  12.220 +      apply (rule exI[where x="plus_game y (neg_game y)"])
  12.221        apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
  12.222        apply (auto simp add: left_options_plus zunion zimage_iff intro: prems)
  12.223        done
  12.224 @@ -666,9 +663,9 @@
  12.225    {
  12.226      fix y
  12.227      assume y: "zin y (left_options x)"
  12.228 -    have "\<not> (ge_game (plus_game (y, neg_game x), zero_game))"
  12.229 +    have "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
  12.230        apply (subst ge_game.simps, simp)
  12.231 -      apply (rule exI[where x="plus_game (y, neg_game y)"])
  12.232 +      apply (rule exI[where x="plus_game y (neg_game y)"])
  12.233        apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
  12.234        apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: prems)
  12.235        done
  12.236 @@ -677,9 +674,9 @@
  12.237    {
  12.238      fix y
  12.239      assume y: "zin y (right_options x)"
  12.240 -    have "\<not> (ge_game (plus_game (x, neg_game y), zero_game))"
  12.241 +    have "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
  12.242        apply (subst ge_game.simps, simp)
  12.243 -      apply (rule exI[where x="plus_game (y, neg_game y)"])
  12.244 +      apply (rule exI[where x="plus_game y (neg_game y)"])
  12.245        apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
  12.246        apply (auto simp add: right_options_plus zunion zimage_iff intro: prems)
  12.247        done
  12.248 @@ -687,28 +684,28 @@
  12.249    note case4 = this
  12.250    show ?case
  12.251      apply (simp add: eq_game_def)
  12.252 -    apply (simp add: ge_game.simps[of "plus_game (x, neg_game x)" "zero_game"])
  12.253 -    apply (simp add: ge_game.simps[of "zero_game" "plus_game (x, neg_game x)"])
  12.254 +    apply (simp add: ge_game.simps[of "plus_game x (neg_game x)" "zero_game"])
  12.255 +    apply (simp add: ge_game.simps[of "zero_game" "plus_game x (neg_game x)"])
  12.256      apply (simp add: right_options_plus left_options_plus right_options_neg left_options_neg zunion zimage_iff)
  12.257      apply (auto simp add: case1 case2 case3 case4)
  12.258      done
  12.259  qed
  12.260  
  12.261 -lemma ge_plus_game_left: "ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))"
  12.262 +lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
  12.263  proof -
  12.264    { fix a
  12.265 -    have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))"
  12.266 +    have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
  12.267      proof (induct a rule: induct_game, (rule impI | rule allI)+)
  12.268        case (goal1 a x y z)
  12.269        note induct_hyp = goal1(1)[rule_format, simplified goal1(2)]
  12.270        { 
  12.271 -        assume hyp: "ge_game(plus_game (x, y), plus_game (x, z))"
  12.272 +        assume hyp: "ge_game(plus_game x y, plus_game x z)"
  12.273          have "ge_game (y, z)"
  12.274          proof -
  12.275            { fix yr
  12.276              assume yr: "zin yr (right_options y)"
  12.277 -            from hyp have "\<not> (ge_game (plus_game (x, z), plus_game (x, yr)))"
  12.278 -              by (auto simp add: ge_game_eq[of "plus_game (x,y)" "plus_game(x,z)"]
  12.279 +            from hyp have "\<not> (ge_game (plus_game x z, plus_game x yr))"
  12.280 +              by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
  12.281                  right_options_plus zunion zimage_iff intro: yr)
  12.282              then have "\<not> (ge_game (z, yr))"
  12.283                apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
  12.284 @@ -718,8 +715,8 @@
  12.285            note yr = this
  12.286            { fix zl
  12.287              assume zl: "zin zl (left_options z)"
  12.288 -            from hyp have "\<not> (ge_game (plus_game (x, zl), plus_game (x, y)))"
  12.289 -              by (auto simp add: ge_game_eq[of "plus_game (x,y)" "plus_game(x,z)"]
  12.290 +            from hyp have "\<not> (ge_game (plus_game x zl, plus_game x y))"
  12.291 +              by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
  12.292                  left_options_plus zunion zimage_iff intro: zl)
  12.293              then have "\<not> (ge_game (zl, y))"
  12.294                apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
  12.295 @@ -739,11 +736,11 @@
  12.296          {
  12.297            fix x'
  12.298            assume x': "zin x' (right_options x)"
  12.299 -          assume hyp: "ge_game (plus_game (x, z), plus_game (x', y))"
  12.300 -          then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
  12.301 -            by (auto simp add: ge_game_eq[of "plus_game (x,z)" "plus_game (x', y)"] 
  12.302 +          assume hyp: "ge_game (plus_game x z, plus_game x' y)"
  12.303 +          then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
  12.304 +            by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"] 
  12.305                right_options_plus zunion zimage_iff intro: x')
  12.306 -          have t: "ge_game (plus_game (x', y), plus_game (x', z))"
  12.307 +          have t: "ge_game (plus_game x' y, plus_game x' z)"
  12.308              apply (subst induct_hyp[symmetric])
  12.309              apply (auto intro: lprod_3_3 x' yz)
  12.310              done
  12.311 @@ -753,11 +750,11 @@
  12.312          {
  12.313            fix x'
  12.314            assume x': "zin x' (left_options x)"
  12.315 -          assume hyp: "ge_game (plus_game (x', z), plus_game (x, y))"
  12.316 -          then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
  12.317 -            by (auto simp add: ge_game_eq[of "plus_game (x',z)" "plus_game (x, y)"] 
  12.318 +          assume hyp: "ge_game (plus_game x' z, plus_game x y)"
  12.319 +          then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
  12.320 +            by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"] 
  12.321                left_options_plus zunion zimage_iff intro: x')
  12.322 -          have t: "ge_game (plus_game (x', y), plus_game (x', z))"
  12.323 +          have t: "ge_game (plus_game x' y, plus_game x' z)"
  12.324              apply (subst induct_hyp[symmetric])
  12.325              apply (auto intro: lprod_3_3 x' yz)
  12.326              done
  12.327 @@ -767,7 +764,7 @@
  12.328          {
  12.329            fix y'
  12.330            assume y': "zin y' (right_options y)"
  12.331 -          assume hyp: "ge_game (plus_game(x, z), plus_game (x, y'))"
  12.332 +          assume hyp: "ge_game (plus_game x z, plus_game x y')"
  12.333            then have "ge_game(z, y')"
  12.334              apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
  12.335              apply (auto simp add: hyp lprod_3_6 y')
  12.336 @@ -780,7 +777,7 @@
  12.337          {
  12.338            fix z'
  12.339            assume z': "zin z' (left_options z)"
  12.340 -          assume hyp: "ge_game (plus_game(x, z'), plus_game (x, y))"
  12.341 +          assume hyp: "ge_game (plus_game x z', plus_game x y)"
  12.342            then have "ge_game(z', y)"
  12.343              apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
  12.344              apply (auto simp add: hyp lprod_3_7 z')
  12.345 @@ -790,7 +787,7 @@
  12.346            with z' have "False" by (auto simp add: ge_game_leftright_refl)
  12.347          }
  12.348          note case4 = this   
  12.349 -        have "ge_game(plus_game (x, y), plus_game (x, z))"
  12.350 +        have "ge_game(plus_game x y, plus_game x z)"
  12.351            apply (subst ge_game_eq)
  12.352            apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
  12.353            apply (auto intro: case1 case2 case3 case4)
  12.354 @@ -804,7 +801,7 @@
  12.355    then show ?thesis by blast
  12.356  qed
  12.357  
  12.358 -lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game (y, x), plus_game (z, x))"
  12.359 +lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game y x, plus_game z x)"
  12.360    by (simp add: ge_plus_game_left plus_game_comm)
  12.361  
  12.362  lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
  12.363 @@ -865,7 +862,7 @@
  12.364    Pg_minus_def: "- G = contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
  12.365  
  12.366  definition
  12.367 -  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)})})"
  12.368 +  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})})"
  12.369  
  12.370  definition
  12.371    Pg_diff_def: "G - H = G + (- (H::Pg))"
  12.372 @@ -891,14 +888,14 @@
  12.373    apply (simp add: eq_game_rel_def)
  12.374    done
  12.375  
  12.376 -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)})"
  12.377 +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})"
  12.378  proof -
  12.379 -  have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game (g, h)})}) respects2 eq_game_rel" 
  12.380 +  have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game g h})}) respects2 eq_game_rel" 
  12.381      apply (simp add: congruent2_def)
  12.382      apply (auto simp add: eq_game_rel_def eq_game_def)
  12.383 -    apply (rule_tac y="plus_game (y1, z2)" in ge_game_trans)
  12.384 +    apply (rule_tac y="plus_game y1 z2" in ge_game_trans)
  12.385      apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
  12.386 -    apply (rule_tac y="plus_game (z1, y2)" in ge_game_trans)
  12.387 +    apply (rule_tac y="plus_game z1 y2" in ge_game_trans)
  12.388      apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
  12.389      done
  12.390    then show ?thesis
    13.1 --- a/src/HOL/ZF/Zet.thy	Mon Mar 01 18:49:55 2010 +0100
    13.2 +++ b/src/HOL/ZF/Zet.thy	Tue Mar 02 12:26:50 2010 +0100
    13.3 @@ -196,7 +196,7 @@
    13.4  lemma zimage_id[simp]: "zimage id A = A"
    13.5    by (simp add: zet_ext_eq zimage_iff)
    13.6  
    13.7 -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"
    13.8 +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"
    13.9    by (auto simp add: zet_ext_eq zimage_iff)
   13.10  
   13.11  end