*** empty log message ***
authorwenzelm
Tue Aug 27 11:03:05 2002 +0200 (2002-08-27)
changeset 13524604d0f3622d6
parent 13523 079af5c90d1c
child 13525 cafd1f98d658
*** empty log message ***
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/State.thy
src/HOL/Bali/WellType.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/Hyperreal/EvenOdd.ML
src/HOL/IMP/Transition.thy
src/HOL/IMPP/Hoare.ML
src/HOL/Induct/LList.thy
src/HOL/Integ/IntDiv.thy
src/HOL/Isar_examples/ExprCompiler.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/NanoJava/State.thy
src/HOL/NumberTheory/BijectionRel.thy
src/HOL/NumberTheory/Chinese.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/NumberTheory/WilsonRuss.thy
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOLCF/FOCUS/Buffer_adm.ML
src/HOLCF/Fix.ML
src/HOLCF/IOA/ABP/Lemmas.ML
src/HOLCF/IOA/NTP/Lemmas.ML
src/HOLCF/IOA/ex/TrivEx.ML
src/HOLCF/IOA/ex/TrivEx2.ML
src/HOLCF/ex/loeckx.ML
src/ZF/Cardinal.thy
src/ZF/Epsilon.thy
src/ZF/Finite.thy
src/ZF/List.thy
src/ZF/Nat.thy
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -766,15 +766,6 @@
     1.4  apply   (auto intro: MGFNormalI)
     1.5  done
     1.6  
     1.7 -lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
     1.8 -apply (rule MGF_asm)
     1.9 -apply (intro strip)
    1.10 -apply (rule MGFNormalI)
    1.11 -apply (rule ax_derivs.weaken)
    1.12 -apply  (erule MGF_simult_Methd)
    1.13 -apply auto
    1.14 -done
    1.15 -
    1.16  
    1.17  section "corollaries"
    1.18  
     2.1 --- a/src/HOL/Bali/DeclConcepts.thy	Tue Aug 27 11:03:02 2002 +0200
     2.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Tue Aug 27 11:03:05 2002 +0200
     2.3 @@ -567,11 +567,6 @@
     2.4                              fid fn  \<Rightarrow> cdeclaredfield G C fn  = None
     2.5                            | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
     2.6  
     2.7 -lemma method_declared_inI:
     2.8 -  "\<lbrakk>class G C = Some c; table_of (methods c) sig = Some m\<rbrakk> 
     2.9 -   \<Longrightarrow> G\<turnstile>mdecl (sig,m) declared_in C"
    2.10 -by (auto simp add: declared_in_def cdeclaredmethd_def)
    2.11 -
    2.12  
    2.13  subsubsection "members"
    2.14  
     3.1 --- a/src/HOL/Bali/Example.thy	Tue Aug 27 11:03:02 2002 +0200
     3.2 +++ b/src/HOL/Bali/Example.thy	Tue Aug 27 11:03:05 2002 +0200
     3.3 @@ -126,7 +126,7 @@
     3.4  lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn"
     3.5  by (simp add: SXcpt_def)
     3.6  
     3.7 -lemma neq_Main_Object [simp]: "Main\<noteq>SXcpt xn"
     3.8 +lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
     3.9  by (simp add: SXcpt_def)
    3.10  
    3.11  section "classes and interfaces"
    3.12 @@ -687,10 +687,6 @@
    3.13    "tprg\<turnstile>(Base,mdecl Base_foo) member_in Base"
    3.14  by (rule member_of_to_member_in [OF Base_foo_member_of_Base])
    3.15  
    3.16 -lemma Base_foo_member_of_Base: 
    3.17 -  "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
    3.18 -by (auto intro!: members.Immediate Base_declares_foo)
    3.19 -
    3.20  lemma Ext_foo_member_of_Ext: 
    3.21    "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
    3.22  by (auto intro!: members.Immediate Ext_declares_foo)
     4.1 --- a/src/HOL/Bali/State.thy	Tue Aug 27 11:03:02 2002 +0200
     4.2 +++ b/src/HOL/Bali/State.thy	Tue Aug 27 11:03:05 2002 +0200
     4.3 @@ -577,7 +577,7 @@
     4.4  apply auto
     4.5  done
     4.6  
     4.7 -lemma raise_if_SomeD [dest!]:
     4.8 +lemma error_if_SomeD [dest!]:
     4.9    "error_if c e y = Some z \<Longrightarrow> c \<and> z=(Error e) \<and> y=None \<or> (y=Some z)"
    4.10  apply (case_tac y)
    4.11  apply (case_tac c)
    4.12 @@ -773,7 +773,7 @@
    4.13   "\<not> (\<exists> err. x=Error err) \<Longrightarrow> error_free ((Some x),s)"
    4.14  by (auto simp add: error_free_def)
    4.15  
    4.16 -lemma error_free_absorb [simp,intro]: 
    4.17 +lemma error_free_abupd_absorb [simp,intro]: 
    4.18   "error_free s \<Longrightarrow> error_free (abupd (absorb j) s)"
    4.19  by (cases s) 
    4.20     (auto simp add: error_free_def absorb_def
     5.1 --- a/src/HOL/Bali/WellType.thy	Tue Aug 27 11:03:02 2002 +0200
     5.2 +++ b/src/HOL/Bali/WellType.thy	Tue Aug 27 11:03:05 2002 +0200
     5.3 @@ -518,14 +518,15 @@
     5.4  lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
     5.5  by (auto simp add: is_acc_iface_def)
     5.6  
     5.7 -lemma is_acc_iface_is_accessible: 
     5.8 +lemma is_acc_iface_Iface_is_accessible: 
     5.9    "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
    5.10  by (auto simp add: is_acc_iface_def)
    5.11  
    5.12  lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
    5.13  by (auto simp add: is_acc_type_def)
    5.14  
    5.15 -lemma is_acc_iface_is_accessible: "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
    5.16 +lemma is_acc_iface_is_accessible:
    5.17 +  "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
    5.18  by (auto simp add: is_acc_type_def)
    5.19  
    5.20  lemma wt_Methd_is_methd: 
    5.21 @@ -539,13 +540,6 @@
    5.22   * conclusion (no selectors in the conclusion\<dots>)
    5.23   *)
    5.24  
    5.25 -lemma wt_Super:
    5.26 -"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
    5.27 -  class (prg E) C = Some c;D=super c\<rbrakk> 
    5.28 - \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
    5.29 -by (auto elim: wt.Super)
    5.30 - 
    5.31 -
    5.32  lemma wt_Call: 
    5.33  "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
    5.34    max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
     6.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue Aug 27 11:03:02 2002 +0200
     6.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Tue Aug 27 11:03:05 2002 +0200
     6.3 @@ -764,15 +764,6 @@
     6.4  apply simp
     6.5  done
     6.6  
     6.7 -lemma last_lift_not_None: "fst ((lift Q) ((x#xs)!(length xs))) \<noteq> None"
     6.8 -apply(subgoal_tac "length xs<length (x # xs)")
     6.9 - apply(drule_tac Q=Q in  lift_nth)
    6.10 - apply(erule ssubst)
    6.11 - apply (simp add:lift_def)
    6.12 - apply(case_tac "(x # xs) ! length xs",simp)
    6.13 -apply simp
    6.14 -done
    6.15 -
    6.16  lemma Seq_sound: 
    6.17    "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk>
    6.18    \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
    6.19 @@ -915,37 +906,6 @@
    6.20  
    6.21  subsubsection{* Soundness of the While rule *}
    6.22  
    6.23 -lemma assum_after_body: 
    6.24 -  "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; 
    6.25 -  (Some P, s) # xs \<in> cptn_mod; fst (((Some P, s) # xs)!length xs) = None; 
    6.26 -   s \<in> b;  (Some (While b P), s) # (Some (Seq P (While b P)), s) # 
    6.27 -            map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
    6.28 -  \<Longrightarrow> (Some (While b P), snd (((Some P, s) # xs)!length xs)) # ys 
    6.29 -      \<in> assum (pre, rely)"
    6.30 -apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
    6.31 -apply clarify
    6.32 -apply(erule_tac x=s in allE)
    6.33 -apply(drule_tac c="(Some P, s) # xs" in subsetD,simp)
    6.34 - apply clarify
    6.35 - apply(erule_tac x="Suc i" in allE)
    6.36 - apply simp
    6.37 - apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
    6.38 - apply(erule mp)
    6.39 - apply(erule etran.elims,simp)
    6.40 - apply(case_tac "fst(((Some P, s) # xs) ! i)")
    6.41 -  apply(force intro:Env simp add:lift_def)
    6.42 - apply(force intro:Env simp add:lift_def)
    6.43 -apply(rule conjI)
    6.44 - apply(simp add:comm_def last_length)
    6.45 -apply clarify
    6.46 -apply(erule_tac x="Suc(length xs + i)" in allE,simp)
    6.47 -apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift del:map.simps)
    6.48 - apply(erule mp)
    6.49 - apply(case_tac "((Some P, s) # xs) ! length xs")
    6.50 - apply(simp add:lift_def)
    6.51 -apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
    6.52 -done
    6.53 -
    6.54  lemma last_append[rule_format]:
    6.55    "\<forall>xs. ys\<noteq>[] \<longrightarrow> ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))"
    6.56  apply(induct ys)
     7.1 --- a/src/HOL/Hyperreal/EvenOdd.ML	Tue Aug 27 11:03:02 2002 +0200
     7.2 +++ b/src/HOL/Hyperreal/EvenOdd.ML	Tue Aug 27 11:03:05 2002 +0200
     7.3 @@ -204,8 +204,8 @@
     7.4  Goal "0 < n & even n --> 1 < n";
     7.5  by (induct_tac "n" 1);
     7.6  by Auto_tac;
     7.7 -qed_spec_mp "even_gt_zero_gt_one";
     7.8 -bind_thm ("even_gt_zero_gt_one",conjI RS even_gt_zero_gt_one);
     7.9 +qed_spec_mp "even_gt_zero_gt_one_aux";
    7.10 +bind_thm ("even_gt_zero_gt_one",conjI RS even_gt_zero_gt_one_aux);
    7.11  
    7.12  (* more general *)
    7.13  Goal "n div 2 <= (Suc n) div 2";
     8.1 --- a/src/HOL/IMP/Transition.thy	Tue Aug 27 11:03:02 2002 +0200
     8.2 +++ b/src/HOL/IMP/Transition.thy	Tue Aug 27 11:03:05 2002 +0200
     8.3 @@ -604,7 +604,7 @@
     8.4    ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
     8.5  qed
     8.6  
     8.7 -lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
     8.8 +lemma evalc_impl_evalc1': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
     8.9  apply (erule evalc.induct)
    8.10  
    8.11  -- SKIP 
    8.12 @@ -680,7 +680,7 @@
    8.13    apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
    8.14    done
    8.15  
    8.16 -lemma evalc1_impl_evalc: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    8.17 +lemma evalc1_impl_evalc': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    8.18    apply (fastsimp dest: FB_lemma2)
    8.19    done
    8.20  
     9.1 --- a/src/HOL/IMPP/Hoare.ML	Tue Aug 27 11:03:02 2002 +0200
     9.2 +++ b/src/HOL/IMPP/Hoare.ML	Tue Aug 27 11:03:05 2002 +0200
     9.3 @@ -352,10 +352,10 @@
     9.4  by (Simp_tac 1);
     9.5  by (eatac MGF_lemma2_simult 1 1);
     9.6  by (rtac subset_refl 1);
     9.7 -qed "MGF";
     9.8 +qed "MGF'";
     9.9  
    9.10  (* requires Body+empty+insert / BodyN, com_det *)
    9.11 -bind_thm ("hoare_complete", MGF RS MGF_complete); 
    9.12 +bind_thm ("hoare_complete", MGF' RS MGF_complete); 
    9.13  
    9.14  section "unused derived rules";
    9.15  
    10.1 --- a/src/HOL/Induct/LList.thy	Tue Aug 27 11:03:02 2002 +0200
    10.2 +++ b/src/HOL/Induct/LList.thy	Tue Aug 27 11:03:05 2002 +0200
    10.3 @@ -502,7 +502,7 @@
    10.4  apply (auto simp add: Rep_LList_inject)
    10.5  done
    10.6  
    10.7 -lemma LList_fun_equalityI: "CONS M N \<in> llist(A) ==> M \<in> A & N \<in> llist(A)"
    10.8 +lemma CONS_D2: "CONS M N \<in> llist(A) ==> M \<in> A & N \<in> llist(A)"
    10.9  apply (erule llist.cases)
   10.10  apply (erule CONS_neq_NIL, fast)
   10.11  done
   10.12 @@ -613,7 +613,7 @@
   10.13  done
   10.14  
   10.15  text{*strong co-induction: bisimulation and case analysis on one variable*}
   10.16 -lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
   10.17 +lemma Lappend_type': "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
   10.18  apply (rule_tac X = " (%u. Lappend u N) `llist (A) " in llist_coinduct)
   10.19  apply (erule imageI)
   10.20  apply (rule image_subsetI)
   10.21 @@ -893,14 +893,14 @@
   10.22  done
   10.23  
   10.24  text{*Shorter proof of theorem above using @{text llist_equalityI} as strong coinduction*}
   10.25 -lemma lmap_lappend_distrib:
   10.26 +lemma lmap_lappend_distrib':
   10.27       "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
   10.28  apply (rule_tac l = "l" in llist_fun_equalityI, simp)
   10.29  apply simp
   10.30  done
   10.31  
   10.32  text{*Without strong coinduction, three case analyses might be needed*}
   10.33 -lemma lappend_assoc: "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
   10.34 +lemma lappend_assoc': "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
   10.35  apply (rule_tac l = "l1" in llist_fun_equalityI, simp)
   10.36  apply simp
   10.37  done
    11.1 --- a/src/HOL/Integ/IntDiv.thy	Tue Aug 27 11:03:02 2002 +0200
    11.2 +++ b/src/HOL/Integ/IntDiv.thy	Tue Aug 27 11:03:05 2002 +0200
    11.3 @@ -352,12 +352,12 @@
    11.4  
    11.5  (*** division of a number by itself ***)
    11.6  
    11.7 -lemma lemma1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
    11.8 +lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
    11.9  apply (subgoal_tac "0 < a*q")
   11.10   apply (simp add: int_0_less_mult_iff, arith)
   11.11  done
   11.12  
   11.13 -lemma lemma2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"
   11.14 +lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"
   11.15  apply (subgoal_tac "0 <= a* (1-q) ")
   11.16   apply (simp add: int_0_le_mult_iff)
   11.17  apply (simp add: zdiff_zmult_distrib2)
   11.18 @@ -366,9 +366,9 @@
   11.19  lemma self_quotient: "[| quorem((a,a),(q,r));  a ~= (0::int) |] ==> q = 1"
   11.20  apply (simp add: split_ifs quorem_def linorder_neq_iff)
   11.21  apply (rule order_antisym, auto)
   11.22 -apply (rule_tac [3] a = "-a" and r = "-r" in lemma1)
   11.23 -apply (rule_tac a = "-a" and r = "-r" in lemma2)
   11.24 -apply (force intro: lemma1 lemma2 simp add: zadd_commute zmult_zminus)+
   11.25 +apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
   11.26 +apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
   11.27 +apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: zadd_commute zmult_zminus)+
   11.28  done
   11.29  
   11.30  lemma self_remainder: "[| quorem((a,a),(q,r));  a ~= (0::int) |] ==> r = 0"
   11.31 @@ -699,7 +699,7 @@
   11.32  
   11.33  (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
   11.34  
   11.35 -lemma lemma1: "[| (0::int) < c;  b < r;  r <= 0 |] ==> b*c < b*(q mod c) + r"
   11.36 +lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r <= 0 |] ==> b*c < b*(q mod c) + r"
   11.37  apply (subgoal_tac "b * (c - q mod c) < r * 1")
   11.38  apply (simp add: zdiff_zmult_distrib2)
   11.39  apply (rule order_le_less_trans)
   11.40 @@ -709,19 +709,19 @@
   11.41                        add1_zle_eq pos_mod_bound)
   11.42  done
   11.43  
   11.44 -lemma lemma2: "[| (0::int) < c;   b < r;  r <= 0 |] ==> b * (q mod c) + r <= 0"
   11.45 +lemma zmult2_lemma_aux2: "[| (0::int) < c;   b < r;  r <= 0 |] ==> b * (q mod c) + r <= 0"
   11.46  apply (subgoal_tac "b * (q mod c) <= 0")
   11.47   apply arith
   11.48  apply (simp add: zmult_le_0_iff pos_mod_sign)
   11.49  done
   11.50  
   11.51 -lemma lemma3: "[| (0::int) < c;  0 <= r;  r < b |] ==> 0 <= b * (q mod c) + r"
   11.52 +lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 <= r;  r < b |] ==> 0 <= b * (q mod c) + r"
   11.53  apply (subgoal_tac "0 <= b * (q mod c) ")
   11.54  apply arith
   11.55  apply (simp add: int_0_le_mult_iff pos_mod_sign)
   11.56  done
   11.57  
   11.58 -lemma lemma4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
   11.59 +lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
   11.60  apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
   11.61  apply (simp add: zdiff_zmult_distrib2)
   11.62  apply (rule order_less_le_trans)
   11.63 @@ -735,7 +735,7 @@
   11.64        ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
   11.65  by (auto simp add: zmult_ac quorem_def linorder_neq_iff
   11.66                     int_0_less_mult_iff zadd_zmult_distrib2 [symmetric] 
   11.67 -                   lemma1 lemma2 lemma3 lemma4)
   11.68 +                   zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
   11.69  
   11.70  lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
   11.71  apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
   11.72 @@ -751,17 +751,17 @@
   11.73  
   11.74  (*** Cancellation of common factors in div ***)
   11.75  
   11.76 -lemma lemma1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
   11.77 +lemma zdiv_zmult_zmult1_aux1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
   11.78  by (subst zdiv_zmult2_eq, auto)
   11.79  
   11.80 -lemma lemma2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
   11.81 +lemma zdiv_zmult_zmult1_aux2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) div (c*b) = a div b"
   11.82  apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ")
   11.83 -apply (rule_tac [2] lemma1, auto)
   11.84 +apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto)
   11.85  done
   11.86  
   11.87  lemma zdiv_zmult_zmult1: "c ~= (0::int) ==> (c*a) div (c*b) = a div b"
   11.88  apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
   11.89 -apply (auto simp add: linorder_neq_iff lemma1 lemma2)
   11.90 +apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
   11.91  done
   11.92  
   11.93  lemma zdiv_zmult_zmult2: "c ~= (0::int) ==> (a*c) div (b*c) = a div b"
   11.94 @@ -773,18 +773,18 @@
   11.95  
   11.96  (*** Distribution of factors over mod ***)
   11.97  
   11.98 -lemma lemma1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
   11.99 +lemma zmod_zmult_zmult1_aux1: "[| (0::int) < b;  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
  11.100  by (subst zmod_zmult2_eq, auto)
  11.101  
  11.102 -lemma lemma2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
  11.103 +lemma zmod_zmult_zmult1_aux2: "[| b < (0::int);  c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
  11.104  apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))")
  11.105 -apply (rule_tac [2] lemma1, auto)
  11.106 +apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto)
  11.107  done
  11.108  
  11.109  lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
  11.110  apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
  11.111  apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
  11.112 -apply (auto simp add: linorder_neq_iff lemma1 lemma2)
  11.113 +apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
  11.114  done
  11.115  
  11.116  lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"
    12.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 11:03:02 2002 +0200
    12.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 11:03:05 2002 +0200
    12.3 @@ -148,7 +148,7 @@
    12.4   better idea of what is actually going on.
    12.5  *}
    12.6  
    12.7 -lemma exec_append:
    12.8 +lemma exec_append':
    12.9    "ALL stack. exec (xs @ ys) stack env
   12.10      = exec ys (exec xs stack env) env" (is "?P xs")
   12.11  proof (induct xs)
    13.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Aug 27 11:03:02 2002 +0200
    13.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Aug 27 11:03:05 2002 +0200
    13.3 @@ -643,7 +643,7 @@
    13.4  apply (auto intro: rtrancl_trans)
    13.5  done
    13.6  
    13.7 -lemmas defs1 = defs1 raise_system_xcpt_def
    13.8 +lemmas defs2 = defs1 raise_system_xcpt_def
    13.9  
   13.10  lemma Checkcast_correct:
   13.11  "\<lbrakk> wt_jvm_prog G phi;
   13.12 @@ -654,7 +654,7 @@
   13.13      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   13.14      fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   13.15  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   13.16 -apply (clarsimp simp add: defs1 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
   13.17 +apply (clarsimp simp add: defs2 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
   13.18  apply (blast intro: Cast_conf2)
   13.19  done
   13.20  
   13.21 @@ -668,12 +668,12 @@
   13.22    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   13.23    fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   13.24  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   13.25 -apply (clarsimp simp add: defs1 map_eq_Cons wt_jvm_prog_def 
   13.26 +apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def 
   13.27                  split: option.split split_if_asm)
   13.28  apply (frule conf_widen)
   13.29  apply assumption+
   13.30  apply (drule conf_RefTD)
   13.31 -apply (clarsimp simp add: defs1)
   13.32 +apply (clarsimp simp add: defs2)
   13.33  apply (rule conjI)
   13.34   apply (drule widen_cfs_fields)
   13.35   apply assumption+
   13.36 @@ -700,7 +700,7 @@
   13.37    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   13.38    fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   13.39  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   13.40 -apply (clarsimp simp add: defs1 split_beta split: option.split List.split split_if_asm)
   13.41 +apply (clarsimp simp add: defs2 split_beta split: option.split List.split split_if_asm)
   13.42  apply (frule conf_widen)
   13.43  prefer 2
   13.44    apply assumption
   13.45 @@ -1110,7 +1110,7 @@
   13.46    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   13.47    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   13.48  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   13.49 -apply (clarsimp simp add: defs1)
   13.50 +apply (clarsimp simp add: defs2)
   13.51  apply fast
   13.52  done
   13.53  
   13.54 @@ -1123,7 +1123,7 @@
   13.55    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   13.56    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   13.57  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   13.58 -apply (clarsimp simp add: defs1)
   13.59 +apply (clarsimp simp add: defs2)
   13.60  apply fast
   13.61  done
   13.62  
   13.63 @@ -1135,7 +1135,7 @@
   13.64    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   13.65    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   13.66  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   13.67 -apply (clarsimp simp add: defs1)
   13.68 +apply (clarsimp simp add: defs2)
   13.69  apply fast
   13.70  done
   13.71  
   13.72 @@ -1147,7 +1147,7 @@
   13.73    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   13.74    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   13.75  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   13.76 -apply (clarsimp simp add: defs1 map_eq_Cons)
   13.77 +apply (clarsimp simp add: defs2 map_eq_Cons)
   13.78  apply (blast intro: conf_widen)
   13.79  done
   13.80  
   13.81 @@ -1159,7 +1159,7 @@
   13.82    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   13.83    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   13.84  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   13.85 -apply (clarsimp simp add: defs1 map_eq_Cons)
   13.86 +apply (clarsimp simp add: defs2 map_eq_Cons)
   13.87  apply (blast intro: conf_widen)
   13.88  done
   13.89  
   13.90 @@ -1171,7 +1171,7 @@
   13.91    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   13.92    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   13.93  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   13.94 -apply (clarsimp simp add: defs1 map_eq_Cons)
   13.95 +apply (clarsimp simp add: defs2 map_eq_Cons)
   13.96  apply (blast intro: conf_widen)
   13.97  done
   13.98  
   13.99 @@ -1183,7 +1183,7 @@
  13.100    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  13.101    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  13.102  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  13.103 -apply (clarsimp simp add: defs1 map_eq_Cons)
  13.104 +apply (clarsimp simp add: defs2 map_eq_Cons)
  13.105  apply (blast intro: conf_widen)
  13.106  done
  13.107  
  13.108 @@ -1195,7 +1195,7 @@
  13.109    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  13.110    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  13.111  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  13.112 -apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
  13.113 +apply (clarsimp simp add: defs2 map_eq_Cons approx_val_def conf_def)
  13.114  apply blast
  13.115  done
  13.116  
    14.1 --- a/src/HOL/NanoJava/State.thy	Tue Aug 27 11:03:02 2002 +0200
    14.2 +++ b/src/HOL/NanoJava/State.thy	Tue Aug 27 11:03:05 2002 +0200
    14.3 @@ -121,7 +121,7 @@
    14.4    "get_field (set_locs l s) a f = get_field s a f"
    14.5  by (simp add: lupd_def get_field_def set_locs_def get_obj_def)
    14.6  
    14.7 -lemma get_field_set_locs [simp]:
    14.8 +lemma get_field_del_locs [simp]:
    14.9    "get_field (del_locs s) a f = get_field s a f"
   14.10  by (simp add: lupd_def get_field_def del_locs_def get_obj_def)
   14.11  
    15.1 --- a/src/HOL/NumberTheory/BijectionRel.thy	Tue Aug 27 11:03:02 2002 +0200
    15.2 +++ b/src/HOL/NumberTheory/BijectionRel.thy	Tue Aug 27 11:03:05 2002 +0200
    15.3 @@ -77,26 +77,27 @@
    15.4      done
    15.5  qed
    15.6  
    15.7 -lemma aux: "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
    15.8 +lemma inj_func_bijR_aux1:
    15.9 +    "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
   15.10    apply (unfold inj_on_def)
   15.11    apply auto
   15.12    done
   15.13  
   15.14 -lemma aux:
   15.15 +lemma inj_func_bijR_aux2:
   15.16    "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A ==> F <= A
   15.17      ==> (F, f ` F) \<in> bijR P"
   15.18    apply (rule_tac F = F and A = A in aux_induct)
   15.19       apply (rule finite_subset)
   15.20        apply auto
   15.21    apply (rule bijR.insert)
   15.22 -     apply (rule_tac [3] aux)
   15.23 +     apply (rule_tac [3] inj_func_bijR_aux1)
   15.24          apply auto
   15.25    done
   15.26  
   15.27  lemma inj_func_bijR:
   15.28    "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A
   15.29      ==> (A, f ` A) \<in> bijR P"
   15.30 -  apply (rule aux)
   15.31 +  apply (rule inj_func_bijR_aux2)
   15.32       apply auto
   15.33    done
   15.34  
   15.35 @@ -166,14 +167,14 @@
   15.36        apply auto
   15.37    done
   15.38  
   15.39 -lemma aux: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b"
   15.40 +lemma aux_foo: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b"
   15.41    apply auto
   15.42    done
   15.43  
   15.44  lemma aux_bij: "bijP P F ==> symP P ==> P a b ==> (a \<in> F) = (b \<in> F)"
   15.45    apply (unfold bijP_def)
   15.46    apply (rule iffI)
   15.47 -  apply (erule_tac [!] aux)
   15.48 +  apply (erule_tac [!] aux_foo)
   15.49        apply simp_all
   15.50    apply (rule iffD2)
   15.51     apply (rule_tac P = P in aux_sym)
    16.1 --- a/src/HOL/NumberTheory/Chinese.thy	Tue Aug 27 11:03:02 2002 +0200
    16.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Tue Aug 27 11:03:05 2002 +0200
    16.3 @@ -139,7 +139,7 @@
    16.4  
    16.5  subsection {* Chinese: uniqueness *}
    16.6  
    16.7 -lemma aux:
    16.8 +lemma zcong_funprod_aux:
    16.9    "m_cond n mf ==> km_cond n kf mf
   16.10      ==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y
   16.11      ==> [x = y] (mod mf n)"
   16.12 @@ -160,10 +160,10 @@
   16.13      [x = y] (mod funprod mf 0 n)"
   16.14    apply (induct n)
   16.15     apply (simp_all (no_asm))
   16.16 -   apply (blast intro: aux)
   16.17 +   apply (blast intro: zcong_funprod_aux)
   16.18    apply (rule impI)+
   16.19    apply (rule zcong_zgcd_zmult_zmod)
   16.20 -    apply (blast intro: aux)
   16.21 +    apply (blast intro: zcong_funprod_aux)
   16.22      prefer 2
   16.23      apply (subst zgcd_commute)
   16.24      apply (rule funprod_zgcd)
   16.25 @@ -192,7 +192,7 @@
   16.26      apply simp_all
   16.27    done
   16.28  
   16.29 -lemma aux:
   16.30 +lemma x_sol_lin_aux:
   16.31      "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i"
   16.32    apply (unfold mhf_def)
   16.33    apply (case_tac "i = 0")
   16.34 @@ -215,7 +215,7 @@
   16.35       apply auto
   16.36    apply (subst zdvd_iff_zmod_eq_0 [symmetric])
   16.37    apply (rule zdvd_zmult)
   16.38 -  apply (rule aux)
   16.39 +  apply (rule x_sol_lin_aux)
   16.40    apply auto
   16.41    done
   16.42  
    17.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Tue Aug 27 11:03:02 2002 +0200
    17.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Tue Aug 27 11:03:05 2002 +0200
    17.3 @@ -142,7 +142,7 @@
    17.4     apply auto
    17.5    done
    17.6  
    17.7 -lemma aux: "a \<le> b - 1 ==> a < (b::int)"
    17.8 +lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)"
    17.9    apply auto
   17.10    done
   17.11  
   17.12 @@ -154,7 +154,7 @@
   17.13     apply auto
   17.14     apply (rule_tac [2] m = m in zcong_zless_imp_eq)
   17.15         apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
   17.16 -	 order_less_imp_le aux simp add: zcong_sym)
   17.17 +	 order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
   17.18    apply (rule_tac "x" = "b" in exI)
   17.19    apply safe
   17.20    apply (rule Bnor_mem_if)
   17.21 @@ -280,7 +280,7 @@
   17.22    done
   17.23  
   17.24  
   17.25 -lemma aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
   17.26 +lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
   17.27    apply (unfold inj_on_def)
   17.28    apply auto
   17.29    done
   17.30 @@ -295,7 +295,7 @@
   17.31     apply auto
   17.32    apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   17.33    apply (subst setprod_insert)
   17.34 -    apply (rule_tac [2] aux)
   17.35 +    apply (rule_tac [2] Bnor_prod_power_aux)
   17.36       apply (unfold inj_on_def)
   17.37       apply (simp_all add: zmult_ac Bnor_fin finite_imageI
   17.38         Bnor_mem_zle_swap)
    18.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Tue Aug 27 11:03:02 2002 +0200
    18.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Aug 27 11:03:05 2002 +0200
    18.3 @@ -343,7 +343,7 @@
    18.4     apply simp_all
    18.5    done
    18.6  
    18.7 -lemma aux: "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
    18.8 +lemma zrelprime_zdvd_zmult_aux: "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
    18.9    apply (subgoal_tac "m = zgcd (m * n, m * k)")
   18.10     apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2])
   18.11     apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff)
   18.12 @@ -351,9 +351,9 @@
   18.13  
   18.14  lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m"
   18.15    apply (case_tac "0 \<le> m")
   18.16 -   apply (blast intro: aux)
   18.17 +   apply (blast intro: zrelprime_zdvd_zmult_aux)
   18.18    apply (subgoal_tac "k dvd -m")
   18.19 -   apply (rule_tac [2] aux)
   18.20 +   apply (rule_tac [2] zrelprime_zdvd_zmult_aux)
   18.21       apply auto
   18.22    done
   18.23  
   18.24 @@ -618,18 +618,13 @@
   18.25    apply (auto simp add: zcong_iff_lin)
   18.26    done
   18.27  
   18.28 -lemma aux: "a = c ==> b = d ==> a - b = c - (d::int)"
   18.29 -  apply auto
   18.30 -  done
   18.31 -
   18.32 -lemma aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
   18.33 +lemma zcong_zmod_aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
   18.34  by(simp add: zdiff_zmult_distrib2 zadd_zdiff_eq eq_zdiff_eq zadd_ac)
   18.35  
   18.36 -
   18.37  lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
   18.38    apply (unfold zcong_def)
   18.39    apply (rule_tac t = "a - b" in ssubst)
   18.40 -  apply (rule_tac "m" = "m" in aux)
   18.41 +  apply (rule_tac "m" = "m" in zcong_zmod_aux)
   18.42    apply (rule trans)
   18.43     apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce)
   18.44    apply (simp add: zadd_commute)
   18.45 @@ -643,7 +638,7 @@
   18.46         apply (simp_all add: pos_mod_bound pos_mod_sign)
   18.47    apply (unfold zcong_def dvd_def)
   18.48    apply (rule_tac x = "a div m - b div m" in exI)
   18.49 -  apply (rule_tac m1 = m in aux [THEN trans])
   18.50 +  apply (rule_tac m1 = m in zcong_zmod_aux [THEN trans])
   18.51    apply auto
   18.52    done
   18.53  
   18.54 @@ -688,7 +683,7 @@
   18.55  
   18.56  declare xzgcda.simps [simp del]
   18.57  
   18.58 -lemma aux1:
   18.59 +lemma xzgcd_correct_aux1:
   18.60    "zgcd (r', r) = k --> 0 < r -->
   18.61      (\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))"
   18.62    apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   18.63 @@ -707,7 +702,7 @@
   18.64    apply (simp add: zabs_def)
   18.65    done
   18.66  
   18.67 -lemma aux2:
   18.68 +lemma xzgcd_correct_aux2:
   18.69    "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r -->
   18.70      zgcd (r', r) = k"
   18.71    apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
   18.72 @@ -729,25 +724,25 @@
   18.73      "0 < n ==> (zgcd (m, n) = k) = (\<exists>s t. xzgcd m n = (k, s, t))"
   18.74    apply (unfold xzgcd_def)
   18.75    apply (rule iffI)
   18.76 -   apply (rule_tac [2] aux2 [THEN mp, THEN mp])
   18.77 -    apply (rule aux1 [THEN mp, THEN mp])
   18.78 +   apply (rule_tac [2] xzgcd_correct_aux2 [THEN mp, THEN mp])
   18.79 +    apply (rule xzgcd_correct_aux1 [THEN mp, THEN mp])
   18.80       apply auto
   18.81    done
   18.82  
   18.83  
   18.84  text {* \medskip @{term xzgcd} linear *}
   18.85  
   18.86 -lemma aux:
   18.87 +lemma xzgcda_linear_aux1:
   18.88    "(a - r * b) * m + (c - r * d) * (n::int) =
   18.89      (a * m + c * n) - r * (b * m + d * n)"
   18.90    apply (simp add: zdiff_zmult_distrib zadd_zmult_distrib2 zmult_assoc)
   18.91    done
   18.92  
   18.93 -lemma aux:
   18.94 +lemma xzgcda_linear_aux2:
   18.95    "r' = s' * m + t' * n ==> r = s * m + t * n
   18.96      ==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)"
   18.97    apply (rule trans)
   18.98 -   apply (rule_tac [2] aux [symmetric])
   18.99 +   apply (rule_tac [2] xzgcda_linear_aux1 [symmetric])
  18.100    apply (simp add: eq_zdiff_eq zmult_commute)
  18.101    done
  18.102  
  18.103 @@ -769,7 +764,7 @@
  18.104     apply (rule_tac [2] order_le_neq_implies_less)
  18.105     apply (rule_tac [2] pos_mod_sign)
  18.106      apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and
  18.107 -      s = s and t' = t' and t = t in aux)
  18.108 +      s = s and t' = t' and t = t in xzgcda_linear_aux2)
  18.109        apply auto
  18.110    done
  18.111  
    19.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Tue Aug 27 11:03:02 2002 +0200
    19.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Tue Aug 27 11:03:05 2002 +0200
    19.3 @@ -32,7 +32,7 @@
    19.4  
    19.5  text {* \medskip @{term [source] inv} *}
    19.6  
    19.7 -lemma aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
    19.8 +lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
    19.9    apply (subst int_int_eq [symmetric])
   19.10    apply auto
   19.11    done
   19.12 @@ -44,7 +44,7 @@
   19.13    apply (subst zmod_zmult1_eq [symmetric])
   19.14    apply (subst zcong_zmod [symmetric])
   19.15    apply (subst power_Suc [symmetric])
   19.16 -  apply (subst aux)
   19.17 +  apply (subst inv_is_inv_aux)
   19.18     apply (erule_tac [2] Little_Fermat)
   19.19     apply (erule_tac [2] zdvd_not_zless)
   19.20     apply (unfold zprime_def)
   19.21 @@ -89,7 +89,7 @@
   19.22            apply auto
   19.23    done
   19.24  
   19.25 -lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
   19.26 +lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
   19.27    apply (unfold zcong_def)
   19.28    apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2)
   19.29    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
   19.30 @@ -106,7 +106,7 @@
   19.31    apply safe
   19.32    apply (cut_tac a = a and p = p in inv_is_inv)
   19.33       apply auto
   19.34 -  apply (simp add: aux)
   19.35 +  apply (simp add: inv_not_p_minus_1_aux)
   19.36    apply (subgoal_tac "a = p - 1")
   19.37     apply (rule_tac [2] zcong_zless_imp_eq)
   19.38         apply auto
   19.39 @@ -137,7 +137,7 @@
   19.40    apply (simp add: pos_mod_bound)
   19.41    done
   19.42  
   19.43 -lemma aux: "5 \<le> p ==>
   19.44 +lemma inv_inv_aux: "5 \<le> p ==>
   19.45      nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
   19.46    apply (subst int_int_eq [symmetric])
   19.47    apply (simp add: zmult_int [symmetric])
   19.48 @@ -163,7 +163,7 @@
   19.49        apply (subst zcong_zmod)
   19.50        apply (subst mod_mod_trivial)
   19.51        apply (subst zcong_zmod [symmetric])
   19.52 -      apply (subst aux)
   19.53 +      apply (subst inv_inv_aux)
   19.54         apply (subgoal_tac [2]
   19.55  	 "zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p")
   19.56          apply (rule_tac [3] zcong_zmult)
    20.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Aug 27 11:03:02 2002 +0200
    20.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Aug 27 11:03:05 2002 +0200
    20.3 @@ -161,7 +161,7 @@
    20.4    from this and b show ?thesis ..
    20.5  qed
    20.6  
    20.7 -lemma (in functional_vectorspace) function_norm_least [intro?]:
    20.8 +lemma (in functional_vectorspace) function_norm_least' [intro?]:
    20.9    includes continuous
   20.10    assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
   20.11    shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
   20.12 @@ -234,7 +234,7 @@
   20.13    includes continuous
   20.14    assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
   20.15    shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
   20.16 -proof (rule function_norm_least)
   20.17 +proof (rule function_norm_least')
   20.18    fix b assume b: "b \<in> B V f"
   20.19    show "b \<le> c"
   20.20    proof cases
    21.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML	Tue Aug 27 11:03:02 2002 +0200
    21.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Tue Aug 27 11:03:05 2002 +0200
    21.3 @@ -268,11 +268,11 @@
    21.4  b y Clarsimp_tac 1;
    21.5  b y ftac BufAC_Asm_d3 1;
    21.6  b y Force_tac 1;
    21.7 -qed "adm_non_BufAC_Asm";
    21.8 +qed "adm_non_BufAC_Asm'";
    21.9  
   21.10  Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
   21.11  by (rtac triv_admI 1);
   21.12  by (Clarify_tac 1);
   21.13  by (eatac Buf_Eq_imp_AC_lemma 1 1); 
   21.14        (* this is what we originally aimed to show, using admissibilty :-( *)
   21.15 -qed "adm_BufAC";
   21.16 +qed "adm_BufAC'";
    22.1 --- a/src/HOLCF/Fix.ML	Tue Aug 27 11:03:02 2002 +0200
    22.2 +++ b/src/HOLCF/Fix.ML	Tue Aug 27 11:03:05 2002 +0200
    22.3 @@ -697,10 +697,6 @@
    22.4  by (atac 1);
    22.5  qed "adm_disj";
    22.6  
    22.7 -
    22.8 -bind_thm("adm_lemma11",adm_lemma11);
    22.9 -bind_thm("adm_disj",adm_disj);
   22.10 -
   22.11  Goal "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)";
   22.12  by (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1);
   22.13  by (etac ssubst 1);
    23.1 --- a/src/HOLCF/IOA/ABP/Lemmas.ML	Tue Aug 27 11:03:02 2002 +0200
    23.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Tue Aug 27 11:03:05 2002 +0200
    23.3 @@ -6,10 +6,6 @@
    23.4  
    23.5  (* Logic *)
    23.6  
    23.7 -val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    23.8 -  by (fast_tac (claset() addDs prems) 1);
    23.9 -qed "imp_conj_lemma";
   23.10 -
   23.11  goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
   23.12  by (Fast_tac 1);
   23.13  val and_de_morgan_and_absorbe = result();
    24.1 --- a/src/HOLCF/IOA/NTP/Lemmas.ML	Tue Aug 27 11:03:02 2002 +0200
    24.2 +++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Tue Aug 27 11:03:05 2002 +0200
    24.3 @@ -6,10 +6,6 @@
    24.4  
    24.5  (* Logic *)
    24.6  
    24.7 -val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    24.8 -  by (fast_tac (claset() addDs prems) 1);
    24.9 -qed "imp_conj_lemma";
   24.10 -
   24.11  goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
   24.12    by (Fast_tac 1);
   24.13  qed "fork_lemma";
    25.1 --- a/src/HOLCF/IOA/ex/TrivEx.ML	Tue Aug 27 11:03:02 2002 +0200
    25.2 +++ b/src/HOLCF/IOA/ex/TrivEx.ML	Tue Aug 27 11:03:05 2002 +0200
    25.3 @@ -6,11 +6,6 @@
    25.4  Trivial Abstraction Example.
    25.5  *)
    25.6  
    25.7 -val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    25.8 -  by (fast_tac (claset() addDs prems) 1);
    25.9 -qed "imp_conj_lemma";
   25.10 -
   25.11 -
   25.12  Goalw [is_abstraction_def] 
   25.13  "is_abstraction h_abs C_ioa A_ioa";
   25.14  by (rtac conjI 1);
    26.1 --- a/src/HOLCF/IOA/ex/TrivEx2.ML	Tue Aug 27 11:03:02 2002 +0200
    26.2 +++ b/src/HOLCF/IOA/ex/TrivEx2.ML	Tue Aug 27 11:03:05 2002 +0200
    26.3 @@ -6,11 +6,6 @@
    26.4  Trivial Abstraction Example.
    26.5  *)
    26.6  
    26.7 -val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    26.8 -  by (fast_tac (claset() addDs prems) 1);
    26.9 -qed "imp_conj_lemma";
   26.10 -
   26.11 -
   26.12  Goalw [is_abstraction_def] 
   26.13  "is_abstraction h_abs C_ioa A_ioa";
   26.14  by (rtac conjI 1);
    27.1 --- a/src/HOLCF/ex/loeckx.ML	Tue Aug 27 11:03:02 2002 +0200
    27.2 +++ b/src/HOLCF/ex/loeckx.ML	Tue Aug 27 11:03:05 2002 +0200
    27.3 @@ -66,7 +66,7 @@
    27.4  by (rtac  cont2cont_CF1L 1);
    27.5  by (rtac cont_iterate 1);
    27.6  by (rtac (chain_iterate RS chainE) 1);
    27.7 -qed "cont_Ifix2";
    27.8 +qed "cont_Ifix2'";
    27.9  
   27.10  (* the proof in little steps *)
   27.11  
   27.12 @@ -98,5 +98,5 @@
   27.13  by (rtac  cont2cont_CF1L 1);
   27.14  by (rtac cont_iterate 1);
   27.15  by (rtac (chain_iterate RS chainE) 1);
   27.16 -qed "cont_Ifix2";
   27.17 +qed "cont_Ifix2''";
   27.18  
    28.1 --- a/src/ZF/Cardinal.thy	Tue Aug 27 11:03:02 2002 +0200
    28.2 +++ b/src/ZF/Cardinal.thy	Tue Aug 27 11:03:05 2002 +0200
    28.3 @@ -892,7 +892,7 @@
    28.4  done
    28.5  
    28.6  (* Induction principle for Finite(A), by Sidi Ehmety *)
    28.7 -lemma Finite_induct:
    28.8 +lemma Finite_induct [case_names 0 cons, induct set: Finite]:
    28.9  "[| Finite(A); P(0);
   28.10      !! x B.   [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |]
   28.11   ==> P(A)"
   28.12 @@ -900,8 +900,6 @@
   28.13  apply (blast intro: Fin_into_Finite)+
   28.14  done
   28.15  
   28.16 -lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]
   28.17 -
   28.18  (*Sidi Ehmety.  The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
   28.19  lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
   28.20  apply (unfold Finite_def)
    29.1 --- a/src/ZF/Epsilon.thy	Tue Aug 27 11:03:02 2002 +0200
    29.2 +++ b/src/ZF/Epsilon.thy	Tue Aug 27 11:03:05 2002 +0200
    29.3 @@ -96,7 +96,7 @@
    29.4  done
    29.5  
    29.6  (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
    29.7 -lemma eclose_induct_down: 
    29.8 +lemma eclose_induct_down [consumes 1]:
    29.9      "[| a: eclose(b);                                            
   29.10          !!y.   [| y: b |] ==> P(y);                              
   29.11          !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)         
   29.12 @@ -108,9 +108,6 @@
   29.13  apply (blast intro: arg_subset_eclose [THEN subsetD])
   29.14  done
   29.15  
   29.16 -(*fixed up for induct method*)
   29.17 -lemmas eclose_induct_down = eclose_induct_down [consumes 1]
   29.18 -
   29.19  lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
   29.20  apply (erule equalityI [OF eclose_least arg_subset_eclose])
   29.21  apply (rule subset_refl)
    30.1 --- a/src/ZF/Finite.thy	Tue Aug 27 11:03:02 2002 +0200
    30.2 +++ b/src/ZF/Finite.thy	Tue Aug 27 11:03:05 2002 +0200
    30.3 @@ -56,7 +56,7 @@
    30.4  (** Induction on finite sets **)
    30.5  
    30.6  (*Discharging x~:y entails extra work*)
    30.7 -lemma Fin_induct:
    30.8 +lemma Fin_induct [case_names 0 cons, induct set: Fin]:
    30.9      "[| b: Fin(A);
   30.10          P(0);
   30.11          !!x y. [| x: A;  y: Fin(A);  x~:y;  P(y) |] ==> P(cons(x,y))
   30.12 @@ -67,9 +67,6 @@
   30.13  apply simp
   30.14  done
   30.15  
   30.16 -(*fixed up for induct method*)
   30.17 -lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin]
   30.18 -
   30.19  
   30.20  (** Simplification for Fin **)
   30.21  declare Fin.intros [simp]
    31.1 --- a/src/ZF/List.thy	Tue Aug 27 11:03:02 2002 +0200
    31.2 +++ b/src/ZF/List.thy	Tue Aug 27 11:03:05 2002 +0200
    31.3 @@ -425,7 +425,7 @@
    31.4  
    31.5  (** New induction rules **)
    31.6  
    31.7 -lemma list_append_induct:
    31.8 +lemma list_append_induct [case_names Nil snoc, consumes 1]:
    31.9      "[| l: list(A);
   31.10          P(Nil);
   31.11          !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x])
   31.12 @@ -434,8 +434,6 @@
   31.13  apply (erule rev_type [THEN list.induct], simp_all)
   31.14  done
   31.15  
   31.16 -lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]
   31.17 -
   31.18  lemma list_complete_induct_lemma [rule_format]:
   31.19   assumes ih: 
   31.20      "\<And>l. [| l \<in> list(A); 
    32.1 --- a/src/ZF/Nat.thy	Tue Aug 27 11:03:02 2002 +0200
    32.2 +++ b/src/ZF/Nat.thy	Tue Aug 27 11:03:05 2002 +0200
    32.3 @@ -79,13 +79,10 @@
    32.4  subsection{*Injectivity Properties and Induction*}
    32.5  
    32.6  (*Mathematical induction*)
    32.7 -lemma nat_induct:
    32.8 +lemma nat_induct [case_names 0 succ, induct set: nat]:
    32.9      "[| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)"
   32.10  by (erule def_induct [OF nat_def nat_bnd_mono], blast)
   32.11  
   32.12 -(*fixed up for induct method*)
   32.13 -lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat]
   32.14 -
   32.15  lemma natE:
   32.16      "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
   32.17  by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) 
   32.18 @@ -168,7 +165,7 @@
   32.19  done
   32.20  
   32.21  (*Induction suitable for subtraction and less-than*)
   32.22 -lemma diff_induct: 
   32.23 +lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
   32.24      "[| m: nat;  n: nat;   
   32.25          !!x. x: nat ==> P(x,0);   
   32.26          !!y. y: nat ==> P(0,succ(y));   
   32.27 @@ -181,8 +178,6 @@
   32.28  apply (erule_tac n=j in nat_induct, auto)  
   32.29  done
   32.30  
   32.31 -(*fixed up for induct method*)
   32.32 -lemmas diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2]
   32.33  
   32.34  (** Induction principle analogous to trancl_induct **)
   32.35