Proofs needed to be updated because induction now preserves name of
induction variable.
--- a/src/HOL/Auth/Guard/Extensions.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy Mon Oct 11 07:42:22 2004 +0200
@@ -589,11 +589,11 @@
apply (case_tac "A=Spy", blast dest: parts_knows_Spy_subset_used)
apply (induct evs)
apply (simp add: used.simps, blast)
-apply (frule_tac ev=a and evs=list in one_step_Cons, simp, clarify)
+apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe)
apply (erule initState_used)
apply (case_tac a, auto)
-apply (drule_tac B=A and X=msg and evs=list in Gets_correct_Says)
+apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
by (auto dest: Says_imp_used intro: used_ConsI)
lemma known_max_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
@@ -602,10 +602,10 @@
apply (simp, blast dest: parts_knows_Spy_subset_used)
apply (induct evs)
apply (simp add: knows_max_def used.simps, blast)
-apply (frule_tac ev=a and evs=list in one_step_Cons, simp, clarify)
+apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe)
apply (case_tac a, auto)
-apply (drule_tac B=A and X=msg and evs=list in Gets_correct_Says)
+apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
by (auto simp: knows_max'_Cons dest: Says_imp_used intro: used_ConsI)
lemma not_used_not_known: "[| evs:p; X ~:used evs;
--- a/src/HOL/Auth/Guard/Guard.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy Mon Oct 11 07:42:22 2004 +0200
@@ -210,7 +210,7 @@
lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
apply (induct l, auto)
-by (erule_tac l1=list and x1=x in mem_cnb_minus_substI, simp)
+by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
lemma parts_cnb: "Z:parts (set l) ==>
cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
@@ -227,15 +227,15 @@
apply (rule_tac x="[Number nat]" in exI, simp)
apply (rule_tac x="[Nonce nat]" in exI, simp)
apply (rule_tac x="[Key nat]" in exI, simp)
-apply (rule_tac x="[Hash msg]" in exI, simp)
+apply (rule_tac x="[Hash X]" in exI, simp)
apply (clarify, rule_tac x="l@la" in exI, simp)
-by (clarify, rule_tac x="[Crypt nat msg]" in exI, simp)
+by (clarify, rule_tac x="[Crypt nat X]" in exI, simp)
lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
apply (induct l)
apply (rule_tac x="[]" in exI, simp, clarsimp)
-apply (subgoal_tac "EX l. kparts {a} = set l & cnb l = crypt_nb a", clarify)
-apply (rule_tac x="l@l'" in exI, simp)
+apply (subgoal_tac "EX l''. kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
+apply (rule_tac x="l''@l'" in exI, simp)
apply (rule kparts_insert_substI, simp)
by (rule kparts_msg_set)
--- a/src/HOL/Auth/Guard/GuardK.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy Mon Oct 11 07:42:22 2004 +0200
@@ -206,7 +206,7 @@
lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
apply (induct l, auto)
-by (erule_tac l1=list and x1=x in mem_cnb_minus_substI, simp)
+by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
lemma parts_cnb: "Z:parts (set l) ==>
cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
@@ -223,15 +223,15 @@
apply (rule_tac x="[Number nat]" in exI, simp)
apply (rule_tac x="[Nonce nat]" in exI, simp)
apply (rule_tac x="[Key nat]" in exI, simp)
-apply (rule_tac x="[Hash msg]" in exI, simp)
+apply (rule_tac x="[Hash X]" in exI, simp)
apply (clarify, rule_tac x="l@la" in exI, simp)
-by (clarify, rule_tac x="[Crypt nat msg]" in exI, simp)
+by (clarify, rule_tac x="[Crypt nat X]" in exI, simp)
lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
apply (induct l)
apply (rule_tac x="[]" in exI, simp, clarsimp)
-apply (subgoal_tac "EX l. kparts {a} = set l & cnb l = crypt_nb a", clarify)
-apply (rule_tac x="l@l'" in exI, simp)
+apply (subgoal_tac "EX l''. kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
+apply (rule_tac x="l''@l'" in exI, simp)
apply (rule kparts_insert_substI, simp)
by (rule kparts_msg_set)
--- a/src/HOL/HoareParallel/RG_Hoare.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy Mon Oct 11 07:42:22 2004 +0200
@@ -528,7 +528,7 @@
lemma last_length2 [rule_format]: "xs\<noteq>[] \<longrightarrow> (last xs)=(xs!(length xs - (Suc 0)))"
apply(induct xs,simp+)
-apply(case_tac "length list",simp+)
+apply(case_tac "length xs",simp+)
done
lemma last_drop: "Suc m<length x \<Longrightarrow> last(drop (Suc m) x) = last x"
--- a/src/HOL/HoareParallel/RG_Tran.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Tran.thy Mon Oct 11 07:42:22 2004 +0200
@@ -129,7 +129,7 @@
lemma last_length: "((a#xs)!(length xs))=last (a#xs)"
apply simp
apply(induct xs,simp+)
-apply(case_tac list)
+apply(case_tac xs)
apply simp_all
done
--- a/src/HOL/Hyperreal/SEQ.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Mon Oct 11 07:42:22 2004 +0200
@@ -6,7 +6,7 @@
*)
theory SEQ
-imports NatStar HyperPow
+imports NatStar
begin
constdefs
@@ -739,12 +739,12 @@
"\<exists>m. m \<le> M & (\<forall>n. n \<le> M --> \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)"
apply (induct M)
apply (rule_tac x = 0 in exI, simp, safe)
-apply (cut_tac x = "\<bar>X (Suc n)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
+apply (cut_tac x = "\<bar>X (Suc M)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
apply safe
apply (rule_tac x = m in exI)
apply (rule_tac [2] x = m in exI)
-apply (rule_tac [3] x = "Suc n" in exI, simp_all, safe)
-apply (erule_tac [!] m1 = na in le_imp_less_or_eq [THEN disjE])
+apply (rule_tac [3] x = "Suc M" in exI, simp_all, safe)
+apply (erule_tac [!] m1 = n in le_imp_less_or_eq [THEN disjE])
apply (simp_all add: less_Suc_cancel_iff)
apply (blast intro: order_le_less_trans [THEN order_less_imp_le])
done
--- a/src/HOL/Lambda/Type.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Lambda/Type.thy Mon Oct 11 07:42:22 2004 +0200
@@ -121,7 +121,7 @@
apply (case_tac Ts)
apply simp+
apply (case_tac Ts)
- apply (case_tac "list @ [t]")
+ apply (case_tac "ts @ [t]")
apply simp+
done
@@ -185,7 +185,7 @@
apply simp
apply (erule_tac x = "t \<degree> a" in allE)
apply (erule_tac x = T in allE)
- apply (erule_tac x = lista in allE)
+ apply (erule_tac x = list in allE)
apply (erule impE)
apply (erule conjE)
apply (erule typing.App)
--- a/src/HOL/Lambda/WeakNorm.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Mon Oct 11 07:42:22 2004 +0200
@@ -83,14 +83,14 @@
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
apply (induct m)
apply (case_tac n)
- apply (case_tac [3] na)
+ apply (case_tac [3] n)
apply (simp only: nat.simps, rules?)+
done
lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)"
apply (induct m)
apply (case_tac n)
- apply (case_tac [3] na)
+ apply (case_tac [3] n)
apply (simp del: simp_thms, rules?)+
done
--- a/src/HOL/List.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/List.thy Mon Oct 11 07:42:22 2004 +0200
@@ -1007,7 +1007,7 @@
lemma take_take [simp]: "!!xs n. take n (take m xs) = take (min n m) xs"
apply (induct m, auto)
apply (case_tac xs, auto)
-apply (case_tac na, auto)
+apply (case_tac n, auto)
done
lemma drop_drop [simp]: "!!xs. drop n (drop m xs) = drop (n + m) xs"
--- a/src/HOL/Matrix/Float.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Matrix/Float.thy Mon Oct 11 07:42:22 2004 +0200
@@ -25,7 +25,7 @@
apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
apply (auto simp add: h)
apply arith
- done
+ done
show ?thesis
proof (induct a)
case (1 n)
@@ -38,7 +38,7 @@
apply (subst pow2_neg[of "-1 - int n"])
apply (auto simp add: g pos)
done
- qed
+ qed
qed
lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
@@ -54,10 +54,10 @@
qed
next
case (2 n)
- show ?case
+ show ?case
proof (induct n)
case 0
- show ?case
+ show ?case
apply (auto)
apply (subst pow2_neg[of "a + -1"])
apply (subst pow2_neg[of "-1"])
@@ -68,7 +68,7 @@
apply (simp)
done
case (Suc m)
- have a: "int m - (a + -2) = 1 + (int m - a + 1)" by arith
+ have a: "int m - (a + -2) = 1 + (int m - a + 1)" by arith
have b: "int m - -2 = 1 + (int m + 1)" by arith
show ?case
apply (auto)
--- a/src/HOL/Matrix/MatrixGeneral.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy Mon Oct 11 07:42:22 2004 +0200
@@ -1064,7 +1064,7 @@
apply (induct m, simp)
apply (simp)
apply (insert tworows)
- apply (drule_tac x="% j i. (if j = 0 then (foldseq_transposed g (\<lambda>u. A u i) na) else (A (Suc na) i))" in spec)
+ apply (drule_tac x="% j i. (if j = 0 then (foldseq_transposed g (\<lambda>u. A u i) m) else (A (Suc m) i))" in spec)
by (simp add: foldmatrix_def foldmatrix_transposed_def)
qed
--- a/src/HOL/Matrix/SparseMatrix.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy Mon Oct 11 07:42:22 2004 +0200
@@ -124,7 +124,7 @@
apply (simp only: Rep_matrix_inject[symmetric])
apply (rule ext)+
apply auto
- apply (subgoal_tac "Rep_matrix (sparse_row_vector list) 0 a = 0")
+ apply (subgoal_tac "Rep_matrix (sparse_row_vector v) 0 a = 0")
apply (simp)
apply (rule sorted_sparse_row_vector_zero)
apply auto
@@ -135,9 +135,7 @@
apply (induct v)
apply (simp)
apply (frule sorted_spvec_cons1, simp)
- apply (simp add: sorted_spvec.simps)
- apply (case_tac list)
- apply (simp_all)
+ apply (simp add: sorted_spvec.simps split:list.split_asm)
done
lemma sorted_spvec_abs_spvec:
@@ -145,9 +143,7 @@
apply (induct v)
apply (simp)
apply (frule sorted_spvec_cons1, simp)
- apply (simp add: sorted_spvec.simps)
- apply (case_tac list)
- apply (simp_all)
+ apply (simp add: sorted_spvec.simps split:list.split_asm)
done
defs
@@ -193,9 +189,7 @@
lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)"
apply (auto simp add: smult_spvec_def)
apply (induct a)
- apply (auto simp add: sorted_spvec.simps)
- apply (case_tac list)
- apply (auto)
+ apply (auto simp add: sorted_spvec.simps split:list.split_asm)
done
lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec (y, (a, b) # arr, brr)); aa < a; sorted_spvec ((a, b) # arr);
@@ -370,7 +364,7 @@
apply (induct A)
apply (auto)
apply (drule sorted_spvec_cons1, simp)
- apply (case_tac list)
+ apply (case_tac A)
apply (auto simp add: sorted_spvec.simps)
done
@@ -821,18 +815,14 @@
apply (induct A)
apply (simp)
apply (frule sorted_spvec_cons1, simp)
- apply (simp add: sorted_spvec.simps)
- apply (case_tac list)
- apply (simp_all)
+ apply (simp add: sorted_spvec.simps split:list.split_asm)
done
lemma sorted_spvec_abs_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (abs_spmat A)"
apply (induct A)
apply (simp)
apply (frule sorted_spvec_cons1, simp)
- apply (simp add: sorted_spvec.simps)
- apply (case_tac list)
- apply (simp_all)
+ apply (simp add: sorted_spvec.simps split:list.split_asm)
done
lemma sorted_spmat_minus_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (minus_spmat A)"
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Mon Oct 11 07:42:22 2004 +0200
@@ -521,7 +521,7 @@
apply (case_tac lvals) apply simp
apply (simp (no_asm_simp) )
-apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ list" in progression_transitive, rule HOL.refl)
apply (case_tac a) apply (simp (no_asm_simp) add: compInit_def)
apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
apply (rule progression_one_step)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Mon Oct 11 07:42:22 2004 +0200
@@ -116,7 +116,7 @@
apply (clarify)
apply (drule_tac x=kr in spec)
apply (simp only: rev.simps)
-apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev list @ [a])) = empty (rev kr[\<mapsto>]rev list)([k'][\<mapsto>][a])")
+apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
apply (simp only:)
apply (case_tac "k' = k")
apply simp
@@ -1531,9 +1531,9 @@
apply (induct m)
apply simp
apply (intro strip)
-apply (subgoal_tac "na \<le> n \<or> na = Suc n")
+apply (subgoal_tac "n \<le> m \<or> n = Suc m")
apply (erule disjE)
-apply (frule_tac x=na in spec, drule_tac x=xs in spec, drule mp, assumption)
+apply (frule_tac x=n in spec, drule_tac x=xs in spec, drule mp, assumption)
apply (rule set_drop_Suc [THEN subset_trans], assumption)
apply auto
done
@@ -2310,7 +2310,7 @@
apply (drule_tac x="lvars_pre @ [a]" in spec)
apply (drule_tac x="lvars0" in spec)
apply (simp (no_asm_simp) add: compInitLvars_def)
-apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb list"
+apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb lvars"
in bc_mt_corresp_comb)
apply (simp (no_asm_simp) add: compInitLvars_def)+
--- a/src/HOL/NumberTheory/Chinese.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy Mon Oct 11 07:42:22 2004 +0200
@@ -94,7 +94,7 @@
apply auto
apply (rule_tac [1] zdvd_zmult2)
apply (rule_tac [2] zdvd_zmult)
- apply (subgoal_tac "i = Suc (k + n)")
+ apply (subgoal_tac "i = Suc (k + l)")
apply (simp_all (no_asm_simp))
done
@@ -125,11 +125,11 @@
apply clarify
apply (subgoal_tac "k = j")
apply (simp_all (no_asm_simp))
- apply (case_tac "Suc (k + n) = j")
- apply (subgoal_tac "funsum f k n = 0")
+ apply (case_tac "Suc (k + l) = j")
+ apply (subgoal_tac "funsum f k l = 0")
apply (rule_tac [2] funsum_zero)
- apply (subgoal_tac [3] "f (Suc (k + n)) = 0")
- apply (subgoal_tac [3] "j \<le> k + n")
+ apply (subgoal_tac [3] "f (Suc (k + l)) = 0")
+ apply (subgoal_tac [3] "j \<le> k + l")
prefer 4
apply arith
apply auto
--- a/src/HOL/NumberTheory/Factorization.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/NumberTheory/Factorization.thy Mon Oct 11 07:42:22 2004 +0200
@@ -149,7 +149,7 @@
lemma nondec_oinsert [rule_format]: "nondec xs --> nondec (oinsert x xs)"
apply (induct xs)
- apply (case_tac [2] list)
+ apply (case_tac [2] xs)
apply (simp_all cong del: list.weak_case_cong)
done
@@ -167,11 +167,11 @@
apply (induct xs)
apply safe
apply simp_all
- apply (case_tac list)
+ apply (case_tac xs)
apply simp_all
- apply (case_tac list)
+ apply (case_tac xs)
apply simp
- apply (rule_tac y = aa and ys = lista in x_less_y_oinsert)
+ apply (rule_tac y = aa and ys = list in x_less_y_oinsert)
apply simp_all
done
--- a/src/HOL/NumberTheory/WilsonRuss.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Mon Oct 11 07:42:22 2004 +0200
@@ -136,7 +136,7 @@
"[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)"
apply (induct z)
apply (auto simp add: zpower_zadd_distrib)
- apply (subgoal_tac "zcong (x^y * x^(y * n)) (1 * 1) p")
+ apply (subgoal_tac "zcong (x^y * x^(y * z)) (1 * 1) p")
apply (rule_tac [2] zcong_zmult, simp_all)
done
--- a/src/HOL/UNITY/Transformers.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/UNITY/Transformers.thy Mon Oct 11 07:42:22 2004 +0200
@@ -403,21 +403,21 @@
lemma wens_single_finite_subset_wens_single:
"wens_single_finite act B k \<subseteq> wens_single act B"
-by (simp add: wens_single_eq_Union, blast)
+by (simp add: wens_single_eq_Union, blast)
lemma subset_wens_single_finite:
"[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|]
==> \<exists>m. \<Union>W = wens_single_finite act B m"
apply (induct k)
- apply (rule_tac x=0 in exI, simp, blast)
-apply (auto simp add: atMost_Suc)
-apply (case_tac "wens_single_finite act B (Suc n) \<in> W")
- prefer 2 apply blast
-apply (drule_tac x="Suc n" in spec)
+ apply (rule_tac x=0 in exI, simp, blast)
+apply (auto simp add: atMost_Suc)
+apply (case_tac "wens_single_finite act B (Suc k) \<in> W")
+ prefer 2 apply blast
+apply (drule_tac x="Suc k" in spec)
apply (erule notE, rule equalityI)
- prefer 2 apply blast
-apply (subst wens_single_finite_eq_Union)
-apply (simp add: atMost_Suc, blast)
+ prefer 2 apply blast
+apply (subst wens_single_finite_eq_Union)
+apply (simp add: atMost_Suc, blast)
done
text{*lemma for Union case*}
--- a/src/HOL/W0/W0.thy Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/W0/W0.thy Mon Oct 11 07:42:22 2004 +0200
@@ -890,7 +890,7 @@
apply (tactic "safe_tac HOL_cs")
apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
- apply (drule_tac e = expr1 in sym [THEN W_var_geD])
+ apply (drule_tac e = e1 in sym [THEN W_var_geD])
apply (drule new_tv_subst_tel, assumption)
apply (drule_tac ts = "$s a" in new_tv_list_le, assumption)
apply (drule new_tv_subst_tel, assumption)