--- a/src/HOL/Bali/AxCompl.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/AxCompl.thy Tue Aug 27 11:03:05 2002 +0200
@@ -766,15 +766,6 @@
apply (auto intro: MGFNormalI)
done
-lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
-apply (rule MGF_asm)
-apply (intro strip)
-apply (rule MGFNormalI)
-apply (rule ax_derivs.weaken)
-apply (erule MGF_simult_Methd)
-apply auto
-done
-
section "corollaries"
--- a/src/HOL/Bali/DeclConcepts.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy Tue Aug 27 11:03:05 2002 +0200
@@ -567,11 +567,6 @@
fid fn \<Rightarrow> cdeclaredfield G C fn = None
| mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
-lemma method_declared_inI:
- "\<lbrakk>class G C = Some c; table_of (methods c) sig = Some m\<rbrakk>
- \<Longrightarrow> G\<turnstile>mdecl (sig,m) declared_in C"
-by (auto simp add: declared_in_def cdeclaredmethd_def)
-
subsubsection "members"
--- a/src/HOL/Bali/Example.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/Example.thy Tue Aug 27 11:03:05 2002 +0200
@@ -126,7 +126,7 @@
lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn"
by (simp add: SXcpt_def)
-lemma neq_Main_Object [simp]: "Main\<noteq>SXcpt xn"
+lemma neq_Main_SXcpt [simp]: "Main\<noteq>SXcpt xn"
by (simp add: SXcpt_def)
section "classes and interfaces"
@@ -687,10 +687,6 @@
"tprg\<turnstile>(Base,mdecl Base_foo) member_in Base"
by (rule member_of_to_member_in [OF Base_foo_member_of_Base])
-lemma Base_foo_member_of_Base:
- "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
-by (auto intro!: members.Immediate Base_declares_foo)
-
lemma Ext_foo_member_of_Ext:
"tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
by (auto intro!: members.Immediate Ext_declares_foo)
--- a/src/HOL/Bali/State.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/State.thy Tue Aug 27 11:03:05 2002 +0200
@@ -577,7 +577,7 @@
apply auto
done
-lemma raise_if_SomeD [dest!]:
+lemma error_if_SomeD [dest!]:
"error_if c e y = Some z \<Longrightarrow> c \<and> z=(Error e) \<and> y=None \<or> (y=Some z)"
apply (case_tac y)
apply (case_tac c)
@@ -773,7 +773,7 @@
"\<not> (\<exists> err. x=Error err) \<Longrightarrow> error_free ((Some x),s)"
by (auto simp add: error_free_def)
-lemma error_free_absorb [simp,intro]:
+lemma error_free_abupd_absorb [simp,intro]:
"error_free s \<Longrightarrow> error_free (abupd (absorb j) s)"
by (cases s)
(auto simp add: error_free_def absorb_def
--- a/src/HOL/Bali/WellType.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Bali/WellType.thy Tue Aug 27 11:03:05 2002 +0200
@@ -518,14 +518,15 @@
lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
by (auto simp add: is_acc_iface_def)
-lemma is_acc_iface_is_accessible:
+lemma is_acc_iface_Iface_is_accessible:
"is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
by (auto simp add: is_acc_iface_def)
lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
by (auto simp add: is_acc_type_def)
-lemma is_acc_iface_is_accessible: "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
+lemma is_acc_iface_is_accessible:
+ "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
by (auto simp add: is_acc_type_def)
lemma wt_Methd_is_methd:
@@ -539,13 +540,6 @@
* conclusion (no selectors in the conclusion\<dots>)
*)
-lemma wt_Super:
-"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
- class (prg E) C = Some c;D=super c\<rbrakk>
- \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
-by (auto elim: wt.Super)
-
-
lemma wt_Call:
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr>
--- a/src/HOL/HoareParallel/RG_Hoare.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy Tue Aug 27 11:03:05 2002 +0200
@@ -764,15 +764,6 @@
apply simp
done
-lemma last_lift_not_None: "fst ((lift Q) ((x#xs)!(length xs))) \<noteq> None"
-apply(subgoal_tac "length xs<length (x # xs)")
- apply(drule_tac Q=Q in lift_nth)
- apply(erule ssubst)
- apply (simp add:lift_def)
- apply(case_tac "(x # xs) ! length xs",simp)
-apply simp
-done
-
lemma Seq_sound:
"\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk>
\<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
@@ -915,37 +906,6 @@
subsubsection{* Soundness of the While rule *}
-lemma assum_after_body:
- "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre];
- (Some P, s) # xs \<in> cptn_mod; fst (((Some P, s) # xs)!length xs) = None;
- s \<in> b; (Some (While b P), s) # (Some (Seq P (While b P)), s) #
- map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk>
- \<Longrightarrow> (Some (While b P), snd (((Some P, s) # xs)!length xs)) # ys
- \<in> assum (pre, rely)"
-apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod)
-apply clarify
-apply(erule_tac x=s in allE)
-apply(drule_tac c="(Some P, s) # xs" in subsetD,simp)
- apply clarify
- apply(erule_tac x="Suc i" in allE)
- apply simp
- apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
- apply(erule mp)
- apply(erule etran.elims,simp)
- apply(case_tac "fst(((Some P, s) # xs) ! i)")
- apply(force intro:Env simp add:lift_def)
- apply(force intro:Env simp add:lift_def)
-apply(rule conjI)
- apply(simp add:comm_def last_length)
-apply clarify
-apply(erule_tac x="Suc(length xs + i)" in allE,simp)
-apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift del:map.simps)
- apply(erule mp)
- apply(case_tac "((Some P, s) # xs) ! length xs")
- apply(simp add:lift_def)
-apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
-done
-
lemma last_append[rule_format]:
"\<forall>xs. ys\<noteq>[] \<longrightarrow> ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))"
apply(induct ys)
--- a/src/HOL/Hyperreal/EvenOdd.ML Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Hyperreal/EvenOdd.ML Tue Aug 27 11:03:05 2002 +0200
@@ -204,8 +204,8 @@
Goal "0 < n & even n --> 1 < n";
by (induct_tac "n" 1);
by Auto_tac;
-qed_spec_mp "even_gt_zero_gt_one";
-bind_thm ("even_gt_zero_gt_one",conjI RS even_gt_zero_gt_one);
+qed_spec_mp "even_gt_zero_gt_one_aux";
+bind_thm ("even_gt_zero_gt_one",conjI RS even_gt_zero_gt_one_aux);
(* more general *)
Goal "n div 2 <= (Suc n) div 2";
--- a/src/HOL/IMP/Transition.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/IMP/Transition.thy Tue Aug 27 11:03:05 2002 +0200
@@ -604,7 +604,7 @@
ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
qed
-lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
+lemma evalc_impl_evalc1': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
apply (erule evalc.induct)
-- SKIP
@@ -680,7 +680,7 @@
apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
done
-lemma evalc1_impl_evalc: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+lemma evalc1_impl_evalc': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
apply (fastsimp dest: FB_lemma2)
done
--- a/src/HOL/IMPP/Hoare.ML Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/IMPP/Hoare.ML Tue Aug 27 11:03:05 2002 +0200
@@ -352,10 +352,10 @@
by (Simp_tac 1);
by (eatac MGF_lemma2_simult 1 1);
by (rtac subset_refl 1);
-qed "MGF";
+qed "MGF'";
(* requires Body+empty+insert / BodyN, com_det *)
-bind_thm ("hoare_complete", MGF RS MGF_complete);
+bind_thm ("hoare_complete", MGF' RS MGF_complete);
section "unused derived rules";
--- a/src/HOL/Induct/LList.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Induct/LList.thy Tue Aug 27 11:03:05 2002 +0200
@@ -502,7 +502,7 @@
apply (auto simp add: Rep_LList_inject)
done
-lemma LList_fun_equalityI: "CONS M N \<in> llist(A) ==> M \<in> A & N \<in> llist(A)"
+lemma CONS_D2: "CONS M N \<in> llist(A) ==> M \<in> A & N \<in> llist(A)"
apply (erule llist.cases)
apply (erule CONS_neq_NIL, fast)
done
@@ -613,7 +613,7 @@
done
text{*strong co-induction: bisimulation and case analysis on one variable*}
-lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
+lemma Lappend_type': "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
apply (rule_tac X = " (%u. Lappend u N) `llist (A) " in llist_coinduct)
apply (erule imageI)
apply (rule image_subsetI)
@@ -893,14 +893,14 @@
done
text{*Shorter proof of theorem above using @{text llist_equalityI} as strong coinduction*}
-lemma lmap_lappend_distrib:
+lemma lmap_lappend_distrib':
"lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
apply (rule_tac l = "l" in llist_fun_equalityI, simp)
apply simp
done
text{*Without strong coinduction, three case analyses might be needed*}
-lemma lappend_assoc: "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
+lemma lappend_assoc': "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
apply (rule_tac l = "l1" in llist_fun_equalityI, simp)
apply simp
done
--- a/src/HOL/Integ/IntDiv.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Integ/IntDiv.thy Tue Aug 27 11:03:05 2002 +0200
@@ -352,12 +352,12 @@
(*** division of a number by itself ***)
-lemma lemma1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
+lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
apply (subgoal_tac "0 < a*q")
apply (simp add: int_0_less_mult_iff, arith)
done
-lemma lemma2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"
+lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"
apply (subgoal_tac "0 <= a* (1-q) ")
apply (simp add: int_0_le_mult_iff)
apply (simp add: zdiff_zmult_distrib2)
@@ -366,9 +366,9 @@
lemma self_quotient: "[| quorem((a,a),(q,r)); a ~= (0::int) |] ==> q = 1"
apply (simp add: split_ifs quorem_def linorder_neq_iff)
apply (rule order_antisym, auto)
-apply (rule_tac [3] a = "-a" and r = "-r" in lemma1)
-apply (rule_tac a = "-a" and r = "-r" in lemma2)
-apply (force intro: lemma1 lemma2 simp add: zadd_commute zmult_zminus)+
+apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
+apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
+apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: zadd_commute zmult_zminus)+
done
lemma self_remainder: "[| quorem((a,a),(q,r)); a ~= (0::int) |] ==> r = 0"
@@ -699,7 +699,7 @@
(** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
-lemma lemma1: "[| (0::int) < c; b < r; r <= 0 |] ==> b*c < b*(q mod c) + r"
+lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r <= 0 |] ==> b*c < b*(q mod c) + r"
apply (subgoal_tac "b * (c - q mod c) < r * 1")
apply (simp add: zdiff_zmult_distrib2)
apply (rule order_le_less_trans)
@@ -709,19 +709,19 @@
add1_zle_eq pos_mod_bound)
done
-lemma lemma2: "[| (0::int) < c; b < r; r <= 0 |] ==> b * (q mod c) + r <= 0"
+lemma zmult2_lemma_aux2: "[| (0::int) < c; b < r; r <= 0 |] ==> b * (q mod c) + r <= 0"
apply (subgoal_tac "b * (q mod c) <= 0")
apply arith
apply (simp add: zmult_le_0_iff pos_mod_sign)
done
-lemma lemma3: "[| (0::int) < c; 0 <= r; r < b |] ==> 0 <= b * (q mod c) + r"
+lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 <= r; r < b |] ==> 0 <= b * (q mod c) + r"
apply (subgoal_tac "0 <= b * (q mod c) ")
apply arith
apply (simp add: int_0_le_mult_iff pos_mod_sign)
done
-lemma lemma4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
+lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
apply (simp add: zdiff_zmult_distrib2)
apply (rule order_less_le_trans)
@@ -735,7 +735,7 @@
==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
by (auto simp add: zmult_ac quorem_def linorder_neq_iff
int_0_less_mult_iff zadd_zmult_distrib2 [symmetric]
- lemma1 lemma2 lemma3 lemma4)
+ zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
@@ -751,17 +751,17 @@
(*** Cancellation of common factors in div ***)
-lemma lemma1: "[| (0::int) < b; c ~= 0 |] ==> (c*a) div (c*b) = a div b"
+lemma zdiv_zmult_zmult1_aux1: "[| (0::int) < b; c ~= 0 |] ==> (c*a) div (c*b) = a div b"
by (subst zdiv_zmult2_eq, auto)
-lemma lemma2: "[| b < (0::int); c ~= 0 |] ==> (c*a) div (c*b) = a div b"
+lemma zdiv_zmult_zmult1_aux2: "[| b < (0::int); c ~= 0 |] ==> (c*a) div (c*b) = a div b"
apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ")
-apply (rule_tac [2] lemma1, auto)
+apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto)
done
lemma zdiv_zmult_zmult1: "c ~= (0::int) ==> (c*a) div (c*b) = a div b"
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
-apply (auto simp add: linorder_neq_iff lemma1 lemma2)
+apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
done
lemma zdiv_zmult_zmult2: "c ~= (0::int) ==> (a*c) div (b*c) = a div b"
@@ -773,18 +773,18 @@
(*** Distribution of factors over mod ***)
-lemma lemma1: "[| (0::int) < b; c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
+lemma zmod_zmult_zmult1_aux1: "[| (0::int) < b; c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
by (subst zmod_zmult2_eq, auto)
-lemma lemma2: "[| b < (0::int); c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
+lemma zmod_zmult_zmult1_aux2: "[| b < (0::int); c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))")
-apply (rule_tac [2] lemma1, auto)
+apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto)
done
lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
-apply (auto simp add: linorder_neq_iff lemma1 lemma2)
+apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
done
lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"
--- a/src/HOL/Isar_examples/ExprCompiler.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy Tue Aug 27 11:03:05 2002 +0200
@@ -148,7 +148,7 @@
better idea of what is actually going on.
*}
-lemma exec_append:
+lemma exec_append':
"ALL stack. exec (xs @ ys) stack env
= exec ys (exec xs stack env) env" (is "?P xs")
proof (induct xs)
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Aug 27 11:03:05 2002 +0200
@@ -643,7 +643,7 @@
apply (auto intro: rtrancl_trans)
done
-lemmas defs1 = defs1 raise_system_xcpt_def
+lemmas defs2 = defs1 raise_system_xcpt_def
lemma Checkcast_correct:
"\<lbrakk> wt_jvm_prog G phi;
@@ -654,7 +654,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
+apply (clarsimp simp add: defs2 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
apply (blast intro: Cast_conf2)
done
@@ -668,12 +668,12 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons wt_jvm_prog_def
+apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def
split: option.split split_if_asm)
apply (frule conf_widen)
apply assumption+
apply (drule conf_RefTD)
-apply (clarsimp simp add: defs1)
+apply (clarsimp simp add: defs2)
apply (rule conjI)
apply (drule widen_cfs_fields)
apply assumption+
@@ -700,7 +700,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 split_beta split: option.split List.split split_if_asm)
+apply (clarsimp simp add: defs2 split_beta split: option.split List.split split_if_asm)
apply (frule conf_widen)
prefer 2
apply assumption
@@ -1110,7 +1110,7 @@
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1)
+apply (clarsimp simp add: defs2)
apply fast
done
@@ -1123,7 +1123,7 @@
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1)
+apply (clarsimp simp add: defs2)
apply fast
done
@@ -1135,7 +1135,7 @@
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1)
+apply (clarsimp simp add: defs2)
apply fast
done
@@ -1147,7 +1147,7 @@
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (clarsimp simp add: defs2 map_eq_Cons)
apply (blast intro: conf_widen)
done
@@ -1159,7 +1159,7 @@
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (clarsimp simp add: defs2 map_eq_Cons)
apply (blast intro: conf_widen)
done
@@ -1171,7 +1171,7 @@
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (clarsimp simp add: defs2 map_eq_Cons)
apply (blast intro: conf_widen)
done
@@ -1183,7 +1183,7 @@
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (clarsimp simp add: defs2 map_eq_Cons)
apply (blast intro: conf_widen)
done
@@ -1195,7 +1195,7 @@
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
+apply (clarsimp simp add: defs2 map_eq_Cons approx_val_def conf_def)
apply blast
done
--- a/src/HOL/NanoJava/State.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NanoJava/State.thy Tue Aug 27 11:03:05 2002 +0200
@@ -121,7 +121,7 @@
"get_field (set_locs l s) a f = get_field s a f"
by (simp add: lupd_def get_field_def set_locs_def get_obj_def)
-lemma get_field_set_locs [simp]:
+lemma get_field_del_locs [simp]:
"get_field (del_locs s) a f = get_field s a f"
by (simp add: lupd_def get_field_def del_locs_def get_obj_def)
--- a/src/HOL/NumberTheory/BijectionRel.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NumberTheory/BijectionRel.thy Tue Aug 27 11:03:05 2002 +0200
@@ -77,26 +77,27 @@
done
qed
-lemma aux: "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
+lemma inj_func_bijR_aux1:
+ "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
apply (unfold inj_on_def)
apply auto
done
-lemma aux:
+lemma inj_func_bijR_aux2:
"\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A ==> F <= A
==> (F, f ` F) \<in> bijR P"
apply (rule_tac F = F and A = A in aux_induct)
apply (rule finite_subset)
apply auto
apply (rule bijR.insert)
- apply (rule_tac [3] aux)
+ apply (rule_tac [3] inj_func_bijR_aux1)
apply auto
done
lemma inj_func_bijR:
"\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A
==> (A, f ` A) \<in> bijR P"
- apply (rule aux)
+ apply (rule inj_func_bijR_aux2)
apply auto
done
@@ -166,14 +167,14 @@
apply auto
done
-lemma aux: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b"
+lemma aux_foo: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b"
apply auto
done
lemma aux_bij: "bijP P F ==> symP P ==> P a b ==> (a \<in> F) = (b \<in> F)"
apply (unfold bijP_def)
apply (rule iffI)
- apply (erule_tac [!] aux)
+ apply (erule_tac [!] aux_foo)
apply simp_all
apply (rule iffD2)
apply (rule_tac P = P in aux_sym)
--- a/src/HOL/NumberTheory/Chinese.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy Tue Aug 27 11:03:05 2002 +0200
@@ -139,7 +139,7 @@
subsection {* Chinese: uniqueness *}
-lemma aux:
+lemma zcong_funprod_aux:
"m_cond n mf ==> km_cond n kf mf
==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y
==> [x = y] (mod mf n)"
@@ -160,10 +160,10 @@
[x = y] (mod funprod mf 0 n)"
apply (induct n)
apply (simp_all (no_asm))
- apply (blast intro: aux)
+ apply (blast intro: zcong_funprod_aux)
apply (rule impI)+
apply (rule zcong_zgcd_zmult_zmod)
- apply (blast intro: aux)
+ apply (blast intro: zcong_funprod_aux)
prefer 2
apply (subst zgcd_commute)
apply (rule funprod_zgcd)
@@ -192,7 +192,7 @@
apply simp_all
done
-lemma aux:
+lemma x_sol_lin_aux:
"0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i"
apply (unfold mhf_def)
apply (case_tac "i = 0")
@@ -215,7 +215,7 @@
apply auto
apply (subst zdvd_iff_zmod_eq_0 [symmetric])
apply (rule zdvd_zmult)
- apply (rule aux)
+ apply (rule x_sol_lin_aux)
apply auto
done
--- a/src/HOL/NumberTheory/EulerFermat.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy Tue Aug 27 11:03:05 2002 +0200
@@ -142,7 +142,7 @@
apply auto
done
-lemma aux: "a \<le> b - 1 ==> a < (b::int)"
+lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)"
apply auto
done
@@ -154,7 +154,7 @@
apply auto
apply (rule_tac [2] m = m in zcong_zless_imp_eq)
apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
- order_less_imp_le aux simp add: zcong_sym)
+ order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
apply (rule_tac "x" = "b" in exI)
apply safe
apply (rule Bnor_mem_if)
@@ -280,7 +280,7 @@
done
-lemma aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
+lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
apply (unfold inj_on_def)
apply auto
done
@@ -295,7 +295,7 @@
apply auto
apply (simp add: Bnor_fin Bnor_mem_zle_swap)
apply (subst setprod_insert)
- apply (rule_tac [2] aux)
+ apply (rule_tac [2] Bnor_prod_power_aux)
apply (unfold inj_on_def)
apply (simp_all add: zmult_ac Bnor_fin finite_imageI
Bnor_mem_zle_swap)
--- a/src/HOL/NumberTheory/IntPrimes.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Tue Aug 27 11:03:05 2002 +0200
@@ -343,7 +343,7 @@
apply simp_all
done
-lemma aux: "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
+lemma zrelprime_zdvd_zmult_aux: "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
apply (subgoal_tac "m = zgcd (m * n, m * k)")
apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2])
apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff)
@@ -351,9 +351,9 @@
lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m"
apply (case_tac "0 \<le> m")
- apply (blast intro: aux)
+ apply (blast intro: zrelprime_zdvd_zmult_aux)
apply (subgoal_tac "k dvd -m")
- apply (rule_tac [2] aux)
+ apply (rule_tac [2] zrelprime_zdvd_zmult_aux)
apply auto
done
@@ -618,18 +618,13 @@
apply (auto simp add: zcong_iff_lin)
done
-lemma aux: "a = c ==> b = d ==> a - b = c - (d::int)"
- apply auto
- done
-
-lemma aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
+lemma zcong_zmod_aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
by(simp add: zdiff_zmult_distrib2 zadd_zdiff_eq eq_zdiff_eq zadd_ac)
-
lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
apply (unfold zcong_def)
apply (rule_tac t = "a - b" in ssubst)
- apply (rule_tac "m" = "m" in aux)
+ apply (rule_tac "m" = "m" in zcong_zmod_aux)
apply (rule trans)
apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce)
apply (simp add: zadd_commute)
@@ -643,7 +638,7 @@
apply (simp_all add: pos_mod_bound pos_mod_sign)
apply (unfold zcong_def dvd_def)
apply (rule_tac x = "a div m - b div m" in exI)
- apply (rule_tac m1 = m in aux [THEN trans])
+ apply (rule_tac m1 = m in zcong_zmod_aux [THEN trans])
apply auto
done
@@ -688,7 +683,7 @@
declare xzgcda.simps [simp del]
-lemma aux1:
+lemma xzgcd_correct_aux1:
"zgcd (r', r) = k --> 0 < r -->
(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))"
apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
@@ -707,7 +702,7 @@
apply (simp add: zabs_def)
done
-lemma aux2:
+lemma xzgcd_correct_aux2:
"(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r -->
zgcd (r', r) = k"
apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
@@ -729,25 +724,25 @@
"0 < n ==> (zgcd (m, n) = k) = (\<exists>s t. xzgcd m n = (k, s, t))"
apply (unfold xzgcd_def)
apply (rule iffI)
- apply (rule_tac [2] aux2 [THEN mp, THEN mp])
- apply (rule aux1 [THEN mp, THEN mp])
+ apply (rule_tac [2] xzgcd_correct_aux2 [THEN mp, THEN mp])
+ apply (rule xzgcd_correct_aux1 [THEN mp, THEN mp])
apply auto
done
text {* \medskip @{term xzgcd} linear *}
-lemma aux:
+lemma xzgcda_linear_aux1:
"(a - r * b) * m + (c - r * d) * (n::int) =
(a * m + c * n) - r * (b * m + d * n)"
apply (simp add: zdiff_zmult_distrib zadd_zmult_distrib2 zmult_assoc)
done
-lemma aux:
+lemma xzgcda_linear_aux2:
"r' = s' * m + t' * n ==> r = s * m + t * n
==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)"
apply (rule trans)
- apply (rule_tac [2] aux [symmetric])
+ apply (rule_tac [2] xzgcda_linear_aux1 [symmetric])
apply (simp add: eq_zdiff_eq zmult_commute)
done
@@ -769,7 +764,7 @@
apply (rule_tac [2] order_le_neq_implies_less)
apply (rule_tac [2] pos_mod_sign)
apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and
- s = s and t' = t' and t = t in aux)
+ s = s and t' = t' and t = t in xzgcda_linear_aux2)
apply auto
done
--- a/src/HOL/NumberTheory/WilsonRuss.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Tue Aug 27 11:03:05 2002 +0200
@@ -32,7 +32,7 @@
text {* \medskip @{term [source] inv} *}
-lemma aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
+lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
apply (subst int_int_eq [symmetric])
apply auto
done
@@ -44,7 +44,7 @@
apply (subst zmod_zmult1_eq [symmetric])
apply (subst zcong_zmod [symmetric])
apply (subst power_Suc [symmetric])
- apply (subst aux)
+ apply (subst inv_is_inv_aux)
apply (erule_tac [2] Little_Fermat)
apply (erule_tac [2] zdvd_not_zless)
apply (unfold zprime_def)
@@ -89,7 +89,7 @@
apply auto
done
-lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
+lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
apply (unfold zcong_def)
apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
@@ -106,7 +106,7 @@
apply safe
apply (cut_tac a = a and p = p in inv_is_inv)
apply auto
- apply (simp add: aux)
+ apply (simp add: inv_not_p_minus_1_aux)
apply (subgoal_tac "a = p - 1")
apply (rule_tac [2] zcong_zless_imp_eq)
apply auto
@@ -137,7 +137,7 @@
apply (simp add: pos_mod_bound)
done
-lemma aux: "5 \<le> p ==>
+lemma inv_inv_aux: "5 \<le> p ==>
nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
apply (subst int_int_eq [symmetric])
apply (simp add: zmult_int [symmetric])
@@ -163,7 +163,7 @@
apply (subst zcong_zmod)
apply (subst mod_mod_trivial)
apply (subst zcong_zmod [symmetric])
- apply (subst aux)
+ apply (subst inv_inv_aux)
apply (subgoal_tac [2]
"zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p")
apply (rule_tac [3] zcong_zmult)
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Aug 27 11:03:05 2002 +0200
@@ -161,7 +161,7 @@
from this and b show ?thesis ..
qed
-lemma (in functional_vectorspace) function_norm_least [intro?]:
+lemma (in functional_vectorspace) function_norm_least' [intro?]:
includes continuous
assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
@@ -234,7 +234,7 @@
includes continuous
assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
-proof (rule function_norm_least)
+proof (rule function_norm_least')
fix b assume b: "b \<in> B V f"
show "b \<le> c"
proof cases
--- a/src/HOLCF/FOCUS/Buffer_adm.ML Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML Tue Aug 27 11:03:05 2002 +0200
@@ -268,11 +268,11 @@
b y Clarsimp_tac 1;
b y ftac BufAC_Asm_d3 1;
b y Force_tac 1;
-qed "adm_non_BufAC_Asm";
+qed "adm_non_BufAC_Asm'";
Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
by (rtac triv_admI 1);
by (Clarify_tac 1);
by (eatac Buf_Eq_imp_AC_lemma 1 1);
(* this is what we originally aimed to show, using admissibilty :-( *)
-qed "adm_BufAC";
+qed "adm_BufAC'";
--- a/src/HOLCF/Fix.ML Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/Fix.ML Tue Aug 27 11:03:05 2002 +0200
@@ -697,10 +697,6 @@
by (atac 1);
qed "adm_disj";
-
-bind_thm("adm_lemma11",adm_lemma11);
-bind_thm("adm_disj",adm_disj);
-
Goal "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)";
by (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1);
by (etac ssubst 1);
--- a/src/HOLCF/IOA/ABP/Lemmas.ML Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML Tue Aug 27 11:03:05 2002 +0200
@@ -6,10 +6,6 @@
(* Logic *)
-val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by (fast_tac (claset() addDs prems) 1);
-qed "imp_conj_lemma";
-
goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
by (Fast_tac 1);
val and_de_morgan_and_absorbe = result();
--- a/src/HOLCF/IOA/NTP/Lemmas.ML Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML Tue Aug 27 11:03:05 2002 +0200
@@ -6,10 +6,6 @@
(* Logic *)
-val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by (fast_tac (claset() addDs prems) 1);
-qed "imp_conj_lemma";
-
goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
by (Fast_tac 1);
qed "fork_lemma";
--- a/src/HOLCF/IOA/ex/TrivEx.ML Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/IOA/ex/TrivEx.ML Tue Aug 27 11:03:05 2002 +0200
@@ -6,11 +6,6 @@
Trivial Abstraction Example.
*)
-val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by (fast_tac (claset() addDs prems) 1);
-qed "imp_conj_lemma";
-
-
Goalw [is_abstraction_def]
"is_abstraction h_abs C_ioa A_ioa";
by (rtac conjI 1);
--- a/src/HOLCF/IOA/ex/TrivEx2.ML Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/IOA/ex/TrivEx2.ML Tue Aug 27 11:03:05 2002 +0200
@@ -6,11 +6,6 @@
Trivial Abstraction Example.
*)
-val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by (fast_tac (claset() addDs prems) 1);
-qed "imp_conj_lemma";
-
-
Goalw [is_abstraction_def]
"is_abstraction h_abs C_ioa A_ioa";
by (rtac conjI 1);
--- a/src/HOLCF/ex/loeckx.ML Tue Aug 27 11:03:02 2002 +0200
+++ b/src/HOLCF/ex/loeckx.ML Tue Aug 27 11:03:05 2002 +0200
@@ -66,7 +66,7 @@
by (rtac cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (rtac (chain_iterate RS chainE) 1);
-qed "cont_Ifix2";
+qed "cont_Ifix2'";
(* the proof in little steps *)
@@ -98,5 +98,5 @@
by (rtac cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (rtac (chain_iterate RS chainE) 1);
-qed "cont_Ifix2";
+qed "cont_Ifix2''";
--- a/src/ZF/Cardinal.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/Cardinal.thy Tue Aug 27 11:03:05 2002 +0200
@@ -892,7 +892,7 @@
done
(* Induction principle for Finite(A), by Sidi Ehmety *)
-lemma Finite_induct:
+lemma Finite_induct [case_names 0 cons, induct set: Finite]:
"[| Finite(A); P(0);
!! x B. [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |]
==> P(A)"
@@ -900,8 +900,6 @@
apply (blast intro: Fin_into_Finite)+
done
-lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]
-
(*Sidi Ehmety. The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
apply (unfold Finite_def)
--- a/src/ZF/Epsilon.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/Epsilon.thy Tue Aug 27 11:03:05 2002 +0200
@@ -96,7 +96,7 @@
done
(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
-lemma eclose_induct_down:
+lemma eclose_induct_down [consumes 1]:
"[| a: eclose(b);
!!y. [| y: b |] ==> P(y);
!!y z. [| y: eclose(b); P(y); z: y |] ==> P(z)
@@ -108,9 +108,6 @@
apply (blast intro: arg_subset_eclose [THEN subsetD])
done
-(*fixed up for induct method*)
-lemmas eclose_induct_down = eclose_induct_down [consumes 1]
-
lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
apply (erule equalityI [OF eclose_least arg_subset_eclose])
apply (rule subset_refl)
--- a/src/ZF/Finite.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/Finite.thy Tue Aug 27 11:03:05 2002 +0200
@@ -56,7 +56,7 @@
(** Induction on finite sets **)
(*Discharging x~:y entails extra work*)
-lemma Fin_induct:
+lemma Fin_induct [case_names 0 cons, induct set: Fin]:
"[| b: Fin(A);
P(0);
!!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y))
@@ -67,9 +67,6 @@
apply simp
done
-(*fixed up for induct method*)
-lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin]
-
(** Simplification for Fin **)
declare Fin.intros [simp]
--- a/src/ZF/List.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/List.thy Tue Aug 27 11:03:05 2002 +0200
@@ -425,7 +425,7 @@
(** New induction rules **)
-lemma list_append_induct:
+lemma list_append_induct [case_names Nil snoc, consumes 1]:
"[| l: list(A);
P(Nil);
!!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x])
@@ -434,8 +434,6 @@
apply (erule rev_type [THEN list.induct], simp_all)
done
-lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]
-
lemma list_complete_induct_lemma [rule_format]:
assumes ih:
"\<And>l. [| l \<in> list(A);
--- a/src/ZF/Nat.thy Tue Aug 27 11:03:02 2002 +0200
+++ b/src/ZF/Nat.thy Tue Aug 27 11:03:05 2002 +0200
@@ -79,13 +79,10 @@
subsection{*Injectivity Properties and Induction*}
(*Mathematical induction*)
-lemma nat_induct:
+lemma nat_induct [case_names 0 succ, induct set: nat]:
"[| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)"
by (erule def_induct [OF nat_def nat_bnd_mono], blast)
-(*fixed up for induct method*)
-lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat]
-
lemma natE:
"[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto)
@@ -168,7 +165,7 @@
done
(*Induction suitable for subtraction and less-than*)
-lemma diff_induct:
+lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
"[| m: nat; n: nat;
!!x. x: nat ==> P(x,0);
!!y. y: nat ==> P(0,succ(y));
@@ -181,8 +178,6 @@
apply (erule_tac n=j in nat_induct, auto)
done
-(*fixed up for induct method*)
-lemmas diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2]
(** Induction principle analogous to trancl_induct **)