# HG changeset patch # User desharna # Date 1404379885 -7200 # Node ID b627e76cc5cc5fa1a458f14081a7be629c16f95d # Parent c29729f764b1c64b66b84dc768ed5dd887e55688# Parent 74bf65a1910a3709f447322908923fc4f6ae3d92 merge diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Thu Jul 03 11:31:25 2014 +0200 @@ -1655,6 +1655,7 @@ using assms unfolding factors_def apply (safe, force) +apply hypsubst_thin apply (induct fa) apply simp apply (simp add: m_assoc) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Auth/ZhouGollmann.thy --- a/src/HOL/Auth/ZhouGollmann.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Auth/ZhouGollmann.thy Thu Jul 03 11:31:25 2014 +0200 @@ -367,6 +367,7 @@ A \ bad; evs \ zg |] ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \ set evs" apply clarify +apply hypsubst_thin apply (erule rev_mp) apply (erule rev_mp) apply (erule zg.induct) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Bali/AxCompl.thy --- a/src/HOL/Bali/AxCompl.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Bali/AxCompl.thy Thu Jul 03 11:31:25 2014 +0200 @@ -1381,6 +1381,7 @@ apply (rule MGF_nested_Methd) apply (rule ballI) apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec) +apply hypsubst_thin apply fast apply (drule finite_subset) apply (erule finite_imageI) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Bali/Conform.thy --- a/src/HOL/Bali/Conform.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Bali/Conform.thy Thu Jul 03 11:31:25 2014 +0200 @@ -440,8 +440,8 @@ apply (case_tac a) apply (case_tac "absorb j a") apply auto -apply (rename_tac a) -apply (case_tac "absorb j (Some a)",auto) +apply (rename_tac a') +apply (case_tac "absorb j (Some a')",auto) apply (erule conforms_NormI) done diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Jul 03 11:31:25 2014 +0200 @@ -5272,7 +5272,7 @@ from ee' have tt': "Inum (a#bs) (Add e (C j)) = Inum (a#bs) (Add e' (C j))" by simp from \_cong[OF lp tt', where c="c"] px have px':"?sp c e' j" by simp - from ecRo jD px' cc' show ?rhs apply auto + from ecRo jD px' show ?rhs apply (auto simp: cc') by (rule_tac x="(e', c')" in bexI,simp_all) (rule_tac x="j" in bexI, simp_all add: cc'[symmetric]) next @@ -5286,7 +5286,7 @@ and cc':"c = c'" by blast from ee' have tt': "Inum (a#bs) (Add e (C j)) = Inum (a#bs) (Add e' (C j))" by simp from \_cong[OF lp tt', where c="c"] px have px':"?sp c e' j" by simp - from ecRo jD px' cc' show ?lhs apply auto + from ecRo jD px' show ?lhs apply (auto simp: cc') by (rule_tac x="(e', c')" in bexI,simp_all) (rule_tac x="j" in bexI, simp_all add: cc'[symmetric]) qed diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Divides.thy --- a/src/HOL/Divides.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Divides.thy Thu Jul 03 11:31:25 2014 +0200 @@ -461,7 +461,7 @@ apply (case_tac "y = 0") apply simp apply (auto simp add: dvd_def) apply (subgoal_tac "-(y * k) = y * - k") - apply (erule ssubst) + apply (simp only:) apply (erule div_mult_self1_is_id) apply simp done @@ -470,8 +470,7 @@ apply (case_tac "y = 0") apply simp apply (auto simp add: dvd_def) apply (subgoal_tac "y * k = -y * -k") - apply (erule ssubst) - apply (rule div_mult_self1_is_id) + apply (erule ssubst, rule div_mult_self1_is_id) apply simp apply simp done diff -r c29729f764b1 -r b627e76cc5cc src/HOL/HOLCF/Library/Stream.thy --- a/src/HOL/HOLCF/Library/Stream.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/HOLCF/Library/Stream.thy Thu Jul 03 11:31:25 2014 +0200 @@ -5,7 +5,7 @@ header {* General Stream domain *} theory Stream -imports HOLCF "~~/src/HOL/Library/Extended_Nat" +imports "../HOLCF" "~~/src/HOL/Library/Extended_Nat" begin default_sort pcpo @@ -792,8 +792,8 @@ apply (drule ex_sconc, simp) apply (rule someI2_ex, auto) apply (simp add: i_rt_Suc_forw) - apply (rule_tac x="a && x" in exI, auto) - apply (case_tac "xa=UU",auto) + apply (rule_tac x="a && xa" in exI, auto) + apply (case_tac "xaa=UU",auto) apply (drule stream_exhaust_eq [THEN iffD1],auto) apply (drule streams_prefix_lemma1,simp+) apply (simp add: sconc_def) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Hoare_Parallel/OG_Examples.thy --- a/src/HOL/Hoare_Parallel/OG_Examples.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Thu Jul 03 11:31:25 2014 +0200 @@ -443,7 +443,7 @@ apply (simp_all (*asm_lr*) del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma) --{* 9 subgoals left *} apply (force simp add:less_Suc_eq) -apply(drule sym) +apply(hypsubst_thin, drule sym) apply (force simp add:less_Suc_eq)+ done diff -r c29729f764b1 -r b627e76cc5cc src/HOL/IMP/Abs_Int2.thy --- a/src/HOL/IMP/Abs_Int2.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/IMP/Abs_Int2.thy Thu Jul 03 11:31:25 2014 +0200 @@ -132,8 +132,10 @@ by simp (metis And(1) And(2) in_gamma_sup_UpI) next case (Less e1 e2) thus ?case - by(auto split: prod.split) - (metis (lifting) inv_aval'_correct aval''_correct inv_less') + apply hypsubst_thin + apply (auto split: prod.split) + apply (metis (lifting) inv_aval'_correct aval''_correct inv_less') + done qed definition "step' = Step diff -r c29729f764b1 -r b627e76cc5cc src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Jul 03 11:31:25 2014 +0200 @@ -166,8 +166,10 @@ case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI) next case (Less e1 e2) thus ?case - by (auto split: prod.split) - (metis afilter_sound filter_less' aval'_sound Less) + apply hypsubst_thin + apply (auto split: prod.split) + apply (metis afilter_sound filter_less' aval'_sound Less) + done qed fun AI :: "com \ 'a astate up \ 'a astate up" where diff -r c29729f764b1 -r b627e76cc5cc src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Thu Jul 03 11:31:25 2014 +0200 @@ -135,11 +135,16 @@ next case (Not b) thus ?case by simp next - case (And b1 b2) thus ?case by(fastforce simp: in_gamma_join_UpI) + case (And b1 b2) thus ?case + apply hypsubst_thin + apply (fastforce simp: in_gamma_join_UpI) + done next case (Less e1 e2) thus ?case - by (auto split: prod.split) - (metis afilter_sound filter_less' aval''_sound Less) + apply hypsubst_thin + apply (auto split: prod.split) + apply (metis afilter_sound filter_less' aval''_sound Less) + done qed diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Library/Float.thy Thu Jul 03 11:31:25 2014 +0200 @@ -75,6 +75,7 @@ lemma uminus_float[simp]: "x \ float \ -x \ float" apply (auto simp: float_def) + apply hypsubst_thin apply (rule_tac x="-x" in exI) apply (rule_tac x="xa" in exI) apply (simp add: field_simps) @@ -82,6 +83,7 @@ lemma times_float[simp]: "x \ float \ y \ float \ x * y \ float" apply (auto simp: float_def) + apply hypsubst_thin apply (rule_tac x="x * xa" in exI) apply (rule_tac x="xb + xc" in exI) apply (simp add: powr_add) @@ -98,6 +100,7 @@ lemma div_power_2_float[simp]: "x \ float \ x / 2^d \ float" apply (auto simp add: float_def) + apply hypsubst_thin apply (rule_tac x="x" in exI) apply (rule_tac x="xa - d" in exI) apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric]) @@ -105,6 +108,7 @@ lemma div_power_2_int_float[simp]: "x \ float \ x / (2::int)^d \ float" apply (auto simp add: float_def) + apply hypsubst_thin apply (rule_tac x="x" in exI) apply (rule_tac x="xa - d" in exI) apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric]) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Library/Multiset.thy Thu Jul 03 11:31:25 2014 +0200 @@ -1653,7 +1653,7 @@ apply (simp (no_asm)) apply (rule_tac x = "(K - {#a#}) + Ka" in exI) apply (simp (no_asm_simp) add: add_assoc [symmetric]) - apply (drule_tac f = "\M. M - {#a#}" in arg_cong) + apply (drule_tac f = "\M. M - {#a#}" and x="?S + ?T" in arg_cong) apply (simp add: diff_union_single_conv) apply (simp (no_asm_use) add: trans_def) apply blast @@ -1664,7 +1664,7 @@ apply (rule conjI) apply (simp add: multiset_eq_iff split: nat_diff_split) apply (rule conjI) - apply (drule_tac f = "\M. M - {#a#}" in arg_cong, simp) + apply (drule_tac f = "\M. M - {#a#}" and x="?S + ?T" in arg_cong, simp) apply (simp add: multiset_eq_iff split: nat_diff_split) apply (simp (no_asm_use) add: trans_def) apply blast @@ -2760,7 +2760,9 @@ using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric] apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b1 set2) - using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce + using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] + [[hypsubst_thin = true]] + by fastforce finally show ?thesis . qed thus "count (mmap p1 M) b1 = count N1 b1" by transfer @@ -2796,7 +2798,9 @@ also have "... = setsum (\ b1. count M (u c b1 b2)) (set1 c)" by simp also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b2 set1) - using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce + using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def + [[hypsubst_thin = true]] + by fastforce finally show ?thesis . qed thus "count (mmap p2 M) b2 = count N2 b2" by transfer diff -r c29729f764b1 -r b627e76cc5cc src/HOL/MacLaurin.thy --- a/src/HOL/MacLaurin.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/MacLaurin.thy Thu Jul 03 11:31:25 2014 +0200 @@ -419,8 +419,7 @@ apply (simp (no_asm)) apply (simp (no_asm) add: sin_expansion_lemma) apply (force intro!: derivative_eq_intros) -apply (subst (asm) setsum.neutral, clarify, case_tac "x", simp, simp) -apply (cases n, simp, simp) +apply (subst (asm) setsum.neutral, auto)[1] apply (rule ccontr, simp) apply (drule_tac x = x in spec, simp) apply (erule ssubst) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/MicroJava/J/JTypeSafe.thy --- a/src/HOL/MicroJava/J/JTypeSafe.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Jul 03 11:31:25 2014 +0200 @@ -93,7 +93,7 @@ apply( rule oconf_obj [THEN iffD2]) apply( simp (no_asm)) apply( intro strip) -apply( case_tac "(aaa, b) = (fn, fd)") +apply( case_tac "(ab, b) = (fn, fd)") apply( simp) apply( fast intro: conf_widen) apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Nat.thy Thu Jul 03 11:31:25 2014 +0200 @@ -1168,7 +1168,7 @@ -- {* elimination of @{text -} on @{text nat} *} by (cases "a < b") (auto simp add: diff_is_0_eq [THEN iffD2] diff_add_inverse - not_less le_less dest!: sym [of a] sym [of b] add_eq_self_zero) + not_less le_less dest!: add_eq_self_zero add_eq_self_zero[OF sym]) lemma nat_diff_split_asm: "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))" diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Nominal/Examples/Class1.thy --- a/src/HOL/Nominal/Examples/Class1.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Nominal/Examples/Class1.thy Thu Jul 03 11:31:25 2014 +0200 @@ -4720,7 +4720,7 @@ apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply(auto) -apply(rotate_tac 1) +apply(rotate_tac 2) apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -4741,7 +4741,7 @@ apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply(auto) -apply(rotate_tac 1) +apply(rotate_tac 2) apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -4851,7 +4851,7 @@ apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply(auto) -apply(rotate_tac 2) +apply(rotate_tac 3) apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -4872,7 +4872,7 @@ apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply(auto) -apply(rotate_tac 2) +apply(rotate_tac 3) apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -4982,7 +4982,7 @@ apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply(auto) -apply(rotate_tac 2) +apply(rotate_tac 3) apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -5003,7 +5003,7 @@ apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply(auto) -apply(rotate_tac 2) +apply(rotate_tac 3) apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -5113,7 +5113,7 @@ apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) apply(auto) -apply(rotate_tac 2) +apply(rotate_tac 3) apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Nominal/Examples/Class2.thy --- a/src/HOL/Nominal/Examples/Class2.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Nominal/Examples/Class2.thy Thu Jul 03 11:31:25 2014 +0200 @@ -3491,7 +3491,7 @@ using a apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm) apply(drule_tac x="x" in meta_spec) -apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(drule_tac x="[(a,aa)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) @@ -3508,7 +3508,7 @@ using a apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm) apply(drule_tac x="a" in meta_spec) -apply(drule_tac x="[(x,xa)]\M" in meta_spec) +apply(drule_tac x="[(x,xa)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1)) @@ -3526,7 +3526,7 @@ using a apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm fresh_atm) apply(drule_tac x="c" in meta_spec) -apply(drule_tac x="[(a,c)]\M" in meta_spec) +apply(drule_tac x="[(a,c)]\Ma" in meta_spec) apply(drule_tac x="c" in meta_spec) apply(drule_tac x="[(a,c)]\N" in meta_spec) apply(simp) @@ -3543,7 +3543,7 @@ apply(case_tac "a=b") apply(simp) apply(drule_tac x="c" in meta_spec) -apply(drule_tac x="[(b,c)]\M" in meta_spec) +apply(drule_tac x="[(b,c)]\Ma" in meta_spec) apply(drule_tac x="c" in meta_spec) apply(drule_tac x="[(b,c)]\N" in meta_spec) apply(simp) @@ -3561,7 +3561,7 @@ apply(case_tac "c=b") apply(simp) apply(drule_tac x="b" in meta_spec) -apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="[(a,b)]\Ma" in meta_spec) apply(drule_tac x="a" in meta_spec) apply(drule_tac x="[(a,b)]\N" in meta_spec) apply(simp) @@ -3577,7 +3577,7 @@ apply(simp) apply(simp) apply(drule_tac x="c" in meta_spec) -apply(drule_tac x="[(a,c)]\M" in meta_spec) +apply(drule_tac x="[(a,c)]\Ma" in meta_spec) apply(drule_tac x="b" in meta_spec) apply(drule_tac x="[(a,c)]\N" in meta_spec) apply(simp) @@ -3594,7 +3594,7 @@ apply(case_tac "a=aa") apply(simp) apply(drule_tac x="c" in meta_spec) -apply(drule_tac x="[(aa,c)]\M" in meta_spec) +apply(drule_tac x="[(aa,c)]\Ma" in meta_spec) apply(drule_tac x="c" in meta_spec) apply(drule_tac x="[(aa,c)]\N" in meta_spec) apply(simp) @@ -3612,7 +3612,7 @@ apply(case_tac "c=aa") apply(simp) apply(drule_tac x="a" in meta_spec) -apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(drule_tac x="[(a,aa)]\Ma" in meta_spec) apply(drule_tac x="aa" in meta_spec) apply(drule_tac x="[(a,aa)]\N" in meta_spec) apply(simp) @@ -3628,7 +3628,7 @@ apply(simp) apply(simp) apply(drule_tac x="aa" in meta_spec) -apply(drule_tac x="[(a,c)]\M" in meta_spec) +apply(drule_tac x="[(a,c)]\Ma" in meta_spec) apply(drule_tac x="c" in meta_spec) apply(drule_tac x="[(a,c)]\N" in meta_spec) apply(simp) @@ -3647,7 +3647,7 @@ apply(case_tac "aa=b") apply(simp) apply(drule_tac x="c" in meta_spec) -apply(drule_tac x="[(b,c)]\M" in meta_spec) +apply(drule_tac x="[(b,c)]\Ma" in meta_spec) apply(drule_tac x="c" in meta_spec) apply(drule_tac x="[(b,c)]\N" in meta_spec) apply(simp) @@ -3665,7 +3665,7 @@ apply(case_tac "c=b") apply(simp) apply(drule_tac x="b" in meta_spec) -apply(drule_tac x="[(aa,b)]\M" in meta_spec) +apply(drule_tac x="[(aa,b)]\Ma" in meta_spec) apply(drule_tac x="aa" in meta_spec) apply(drule_tac x="[(aa,b)]\N" in meta_spec) apply(simp) @@ -3681,7 +3681,7 @@ apply(simp) apply(simp) apply(drule_tac x="c" in meta_spec) -apply(drule_tac x="[(aa,c)]\M" in meta_spec) +apply(drule_tac x="[(aa,c)]\Ma" in meta_spec) apply(drule_tac x="b" in meta_spec) apply(drule_tac x="[(aa,c)]\N" in meta_spec) apply(simp) @@ -3701,7 +3701,7 @@ apply(case_tac "a=b") apply(simp) apply(drule_tac x="b" in meta_spec) -apply(drule_tac x="[(b,aa)]\M" in meta_spec) +apply(drule_tac x="[(b,aa)]\Ma" in meta_spec) apply(drule_tac x="aa" in meta_spec) apply(drule_tac x="[(b,aa)]\N" in meta_spec) apply(simp) @@ -3719,7 +3719,7 @@ apply(case_tac "aa=b") apply(simp) apply(drule_tac x="a" in meta_spec) -apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="[(a,b)]\Ma" in meta_spec) apply(drule_tac x="a" in meta_spec) apply(drule_tac x="[(a,b)]\N" in meta_spec) apply(simp) @@ -3735,7 +3735,7 @@ apply(simp) apply(simp) apply(drule_tac x="a" in meta_spec) -apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(drule_tac x="[(a,aa)]\Ma" in meta_spec) apply(drule_tac x="b" in meta_spec) apply(drule_tac x="[(a,aa)]\N" in meta_spec) apply(simp) @@ -3753,7 +3753,7 @@ apply(case_tac "a=b") apply(simp) apply(drule_tac x="aa" in meta_spec) -apply(drule_tac x="[(b,c)]\M" in meta_spec) +apply(drule_tac x="[(b,c)]\Ma" in meta_spec) apply(drule_tac x="c" in meta_spec) apply(drule_tac x="[(b,c)]\N" in meta_spec) apply(simp) @@ -3771,7 +3771,7 @@ apply(case_tac "c=b") apply(simp) apply(drule_tac x="aa" in meta_spec) -apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="[(a,b)]\Ma" in meta_spec) apply(drule_tac x="a" in meta_spec) apply(drule_tac x="[(a,b)]\N" in meta_spec) apply(simp) @@ -3787,7 +3787,7 @@ apply(simp) apply(simp) apply(drule_tac x="aa" in meta_spec) -apply(drule_tac x="[(a,c)]\M" in meta_spec) +apply(drule_tac x="[(a,c)]\Ma" in meta_spec) apply(drule_tac x="b" in meta_spec) apply(drule_tac x="[(a,c)]\N" in meta_spec) apply(simp) @@ -3806,7 +3806,7 @@ lemma ANDLEFT1_elim: assumes a: "(x):M \ ANDLEFT1 (B AND C) ($B)$" obtains x' M' where "M = AndL1 (x').M' x" and "fin (AndL1 (x').M' x) x" and "(x'):M' \ ($B)$" -using a +using a [[ hypsubst_thin = true ]] apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm) apply(drule_tac x="y" in meta_spec) apply(drule_tac x="[(x,y)]\M" in meta_spec) @@ -3859,7 +3859,7 @@ lemma ANDLEFT2_elim: assumes a: "(x):M \ ANDLEFT2 (B AND C) ($C)$" obtains x' M' where "M = AndL2 (x').M' x" and "fin (AndL2 (x').M' x) x" and "(x'):M' \ ($C)$" -using a +using a [[ hypsubst_thin = true ]] apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm) apply(drule_tac x="y" in meta_spec) apply(drule_tac x="[(x,y)]\M" in meta_spec) @@ -3915,7 +3915,7 @@ using a apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm) apply(drule_tac x="b" in meta_spec) -apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="[(a,b)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) @@ -3927,7 +3927,7 @@ apply(case_tac "a=aa") apply(simp) apply(drule_tac x="b" in meta_spec) -apply(drule_tac x="[(aa,b)]\M" in meta_spec) +apply(drule_tac x="[(aa,b)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2)) @@ -3940,7 +3940,7 @@ apply(case_tac "b=aa") apply(simp) apply(drule_tac x="a" in meta_spec) -apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(drule_tac x="[(a,aa)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) @@ -3951,7 +3951,7 @@ apply(simp) apply(simp) apply(drule_tac x="aa" in meta_spec) -apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="[(a,b)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) @@ -3968,7 +3968,7 @@ using a apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm) apply(drule_tac x="b" in meta_spec) -apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="[(a,b)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) @@ -3980,7 +3980,7 @@ apply(case_tac "a=aa") apply(simp) apply(drule_tac x="b" in meta_spec) -apply(drule_tac x="[(aa,b)]\M" in meta_spec) +apply(drule_tac x="[(aa,b)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2)) @@ -3993,7 +3993,7 @@ apply(case_tac "b=aa") apply(simp) apply(drule_tac x="a" in meta_spec) -apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(drule_tac x="[(a,aa)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) @@ -4004,7 +4004,7 @@ apply(simp) apply(simp) apply(drule_tac x="aa" in meta_spec) -apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="[(a,b)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) @@ -4022,7 +4022,7 @@ using a apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm fresh_atm) apply(drule_tac x="z" in meta_spec) -apply(drule_tac x="[(x,z)]\M" in meta_spec) +apply(drule_tac x="[(x,z)]\Ma" in meta_spec) apply(drule_tac x="z" in meta_spec) apply(drule_tac x="[(x,z)]\N" in meta_spec) apply(simp) @@ -4039,7 +4039,7 @@ apply(case_tac "x=y") apply(simp) apply(drule_tac x="z" in meta_spec) -apply(drule_tac x="[(y,z)]\M" in meta_spec) +apply(drule_tac x="[(y,z)]\Ma" in meta_spec) apply(drule_tac x="z" in meta_spec) apply(drule_tac x="[(y,z)]\N" in meta_spec) apply(simp) @@ -4057,7 +4057,7 @@ apply(case_tac "z=y") apply(simp) apply(drule_tac x="y" in meta_spec) -apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(drule_tac x="[(x,y)]\Ma" in meta_spec) apply(drule_tac x="x" in meta_spec) apply(drule_tac x="[(x,y)]\N" in meta_spec) apply(simp) @@ -4073,7 +4073,7 @@ apply(simp) apply(simp) apply(drule_tac x="z" in meta_spec) -apply(drule_tac x="[(x,z)]\M" in meta_spec) +apply(drule_tac x="[(x,z)]\Ma" in meta_spec) apply(drule_tac x="y" in meta_spec) apply(drule_tac x="[(x,z)]\N" in meta_spec) apply(simp) @@ -4090,7 +4090,7 @@ apply(case_tac "x=xa") apply(simp) apply(drule_tac x="z" in meta_spec) -apply(drule_tac x="[(xa,z)]\M" in meta_spec) +apply(drule_tac x="[(xa,z)]\Ma" in meta_spec) apply(drule_tac x="z" in meta_spec) apply(drule_tac x="[(xa,z)]\N" in meta_spec) apply(simp) @@ -4108,7 +4108,7 @@ apply(case_tac "z=xa") apply(simp) apply(drule_tac x="x" in meta_spec) -apply(drule_tac x="[(x,xa)]\M" in meta_spec) +apply(drule_tac x="[(x,xa)]\Ma" in meta_spec) apply(drule_tac x="xa" in meta_spec) apply(drule_tac x="[(x,xa)]\N" in meta_spec) apply(simp) @@ -4124,7 +4124,7 @@ apply(simp) apply(simp) apply(drule_tac x="xa" in meta_spec) -apply(drule_tac x="[(x,z)]\M" in meta_spec) +apply(drule_tac x="[(x,z)]\Ma" in meta_spec) apply(drule_tac x="z" in meta_spec) apply(drule_tac x="[(x,z)]\N" in meta_spec) apply(simp) @@ -4143,7 +4143,7 @@ apply(case_tac "xa=y") apply(simp) apply(drule_tac x="z" in meta_spec) -apply(drule_tac x="[(y,z)]\M" in meta_spec) +apply(drule_tac x="[(y,z)]\Ma" in meta_spec) apply(drule_tac x="z" in meta_spec) apply(drule_tac x="[(y,z)]\N" in meta_spec) apply(simp) @@ -4161,7 +4161,7 @@ apply(case_tac "z=y") apply(simp) apply(drule_tac x="y" in meta_spec) -apply(drule_tac x="[(xa,y)]\M" in meta_spec) +apply(drule_tac x="[(xa,y)]\Ma" in meta_spec) apply(drule_tac x="xa" in meta_spec) apply(drule_tac x="[(xa,y)]\N" in meta_spec) apply(simp) @@ -4177,7 +4177,7 @@ apply(simp) apply(simp) apply(drule_tac x="z" in meta_spec) -apply(drule_tac x="[(xa,z)]\M" in meta_spec) +apply(drule_tac x="[(xa,z)]\Ma" in meta_spec) apply(drule_tac x="y" in meta_spec) apply(drule_tac x="[(xa,z)]\N" in meta_spec) apply(simp) @@ -4197,7 +4197,7 @@ apply(case_tac "x=y") apply(simp) apply(drule_tac x="y" in meta_spec) -apply(drule_tac x="[(y,xa)]\M" in meta_spec) +apply(drule_tac x="[(y,xa)]\Ma" in meta_spec) apply(drule_tac x="xa" in meta_spec) apply(drule_tac x="[(y,xa)]\N" in meta_spec) apply(simp) @@ -4215,7 +4215,7 @@ apply(case_tac "xa=y") apply(simp) apply(drule_tac x="x" in meta_spec) -apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(drule_tac x="[(x,y)]\Ma" in meta_spec) apply(drule_tac x="x" in meta_spec) apply(drule_tac x="[(x,y)]\N" in meta_spec) apply(simp) @@ -4231,7 +4231,7 @@ apply(simp) apply(simp) apply(drule_tac x="x" in meta_spec) -apply(drule_tac x="[(x,xa)]\M" in meta_spec) +apply(drule_tac x="[(x,xa)]\Ma" in meta_spec) apply(drule_tac x="y" in meta_spec) apply(drule_tac x="[(x,xa)]\N" in meta_spec) apply(simp) @@ -4249,7 +4249,7 @@ apply(case_tac "x=y") apply(simp) apply(drule_tac x="xa" in meta_spec) -apply(drule_tac x="[(y,z)]\M" in meta_spec) +apply(drule_tac x="[(y,z)]\Ma" in meta_spec) apply(drule_tac x="z" in meta_spec) apply(drule_tac x="[(y,z)]\N" in meta_spec) apply(simp) @@ -4267,7 +4267,7 @@ apply(case_tac "z=y") apply(simp) apply(drule_tac x="xa" in meta_spec) -apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(drule_tac x="[(x,y)]\Ma" in meta_spec) apply(drule_tac x="x" in meta_spec) apply(drule_tac x="[(x,y)]\N" in meta_spec) apply(simp) @@ -4283,7 +4283,7 @@ apply(simp) apply(simp) apply(drule_tac x="xa" in meta_spec) -apply(drule_tac x="[(x,z)]\M" in meta_spec) +apply(drule_tac x="[(x,z)]\Ma" in meta_spec) apply(drule_tac x="y" in meta_spec) apply(drule_tac x="[(x,z)]\N" in meta_spec) apply(simp) @@ -4308,7 +4308,7 @@ apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm) apply(drule_tac x="x" in meta_spec) apply(drule_tac x="b" in meta_spec) -apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="[(a,b)]\Ma" in meta_spec) apply(simp) apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) apply(simp add: calc_atm) @@ -4319,7 +4319,7 @@ apply(drule_tac x="z" in spec) apply(drule_tac x="[(a,b)]\P" in spec) apply(simp add: fresh_prod fresh_left calc_atm) -apply(drule_tac pi="[(a,b)]" and x="(x):M{a:=(z).([(a,b)]\P)}" +apply(drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]\P)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname) apply(drule meta_mp) @@ -4332,7 +4332,7 @@ apply(simp add: fresh_prod fresh_left) apply(drule mp) apply(simp add: calc_atm) -apply(drule_tac pi="[(a,b)]" and x=":M{x:=<([(a,b)]\c)>.([(a,b)]\Q)}" +apply(drule_tac pi="[(a,b)]" and x=":Ma{x:=<([(a,b)]\c)>.([(a,b)]\Q)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname) apply(simp add: calc_atm) @@ -4340,7 +4340,7 @@ apply(simp) apply(drule_tac x="x" in meta_spec) apply(drule_tac x="b" in meta_spec) -apply(drule_tac x="[(aa,b)]\M" in meta_spec) +apply(drule_tac x="[(aa,b)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2)) @@ -4352,7 +4352,7 @@ apply(drule_tac x="z" in spec) apply(drule_tac x="[(a,b)]\P" in spec) apply(simp add: fresh_prod fresh_left calc_atm) -apply(drule_tac pi="[(a,b)]" and x="(x):M{a:=(z).([(a,b)]\P)}" +apply(drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]\P)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname) apply(drule meta_mp) @@ -4365,7 +4365,7 @@ apply(simp add: fresh_prod fresh_left) apply(drule mp) apply(simp add: calc_atm) -apply(drule_tac pi="[(a,b)]" and x=":M{x:=<([(a,b)]\c)>.([(a,b)]\Q)}" +apply(drule_tac pi="[(a,b)]" and x=":Ma{x:=<([(a,b)]\c)>.([(a,b)]\Q)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname) apply(simp add: calc_atm) @@ -4374,7 +4374,7 @@ apply(simp) apply(drule_tac x="x" in meta_spec) apply(drule_tac x="a" in meta_spec) -apply(drule_tac x="[(a,aa)]\M" in meta_spec) +apply(drule_tac x="[(a,aa)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2)) @@ -4386,7 +4386,7 @@ apply(drule_tac x="z" in spec) apply(drule_tac x="[(a,aa)]\P" in spec) apply(simp add: fresh_prod fresh_left calc_atm) -apply(drule_tac pi="[(a,aa)]" and x="(x):M{aa:=(z).([(a,aa)]\P)}" +apply(drule_tac pi="[(a,aa)]" and x="(x):Ma{aa:=(z).([(a,aa)]\P)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname) apply(drule meta_mp) @@ -4399,14 +4399,14 @@ apply(simp add: fresh_prod fresh_left) apply(drule mp) apply(simp add: calc_atm) -apply(drule_tac pi="[(a,aa)]" and x=":M{x:=<([(a,aa)]\c)>.([(a,aa)]\Q)}" +apply(drule_tac pi="[(a,aa)]" and x=":Ma{x:=<([(a,aa)]\c)>.([(a,aa)]\Q)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname) apply(simp add: calc_atm) apply(simp) apply(drule_tac x="x" in meta_spec) apply(drule_tac x="aa" in meta_spec) -apply(drule_tac x="[(a,b)]\M" in meta_spec) +apply(drule_tac x="[(a,b)]\Ma" in meta_spec) apply(simp) apply(drule meta_mp) apply(drule_tac pi="[(a,b)]" in fic.eqvt(2)) @@ -4418,7 +4418,7 @@ apply(drule_tac x="z" in spec) apply(drule_tac x="[(a,b)]\P" in spec) apply(simp add: fresh_prod fresh_left calc_atm) -apply(drule_tac pi="[(a,b)]" and x="(x):M{aa:=(z).([(a,b)]\P)}" +apply(drule_tac pi="[(a,b)]" and x="(x):Ma{aa:=(z).([(a,b)]\P)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname) apply(drule meta_mp) @@ -4430,7 +4430,7 @@ apply(simp add: fresh_prod fresh_left) apply(drule mp) apply(simp add: calc_atm) -apply(drule_tac pi="[(a,b)]" and x=":M{x:=<([(a,b)]\c)>.([(a,b)]\Q)}" +apply(drule_tac pi="[(a,b)]" and x=":Ma{x:=<([(a,b)]\c)>.([(a,b)]\Q)}" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst]) apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname) apply(simp add: calc_atm) @@ -4443,7 +4443,7 @@ using a apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm) apply(drule_tac x="a" in meta_spec) -apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(drule_tac x="[(x,y)]\Ma" in meta_spec) apply(drule_tac x="y" in meta_spec) apply(drule_tac x="[(x,y)]\N" in meta_spec) apply(simp) @@ -4460,7 +4460,7 @@ apply(case_tac "x=xa") apply(simp) apply(drule_tac x="a" in meta_spec) -apply(drule_tac x="[(xa,y)]\M" in meta_spec) +apply(drule_tac x="[(xa,y)]\Ma" in meta_spec) apply(drule_tac x="y" in meta_spec) apply(drule_tac x="[(xa,y)]\N" in meta_spec) apply(simp) @@ -4478,7 +4478,7 @@ apply(case_tac "y=xa") apply(simp) apply(drule_tac x="a" in meta_spec) -apply(drule_tac x="[(x,xa)]\M" in meta_spec) +apply(drule_tac x="[(x,xa)]\Ma" in meta_spec) apply(drule_tac x="x" in meta_spec) apply(drule_tac x="[(x,xa)]\N" in meta_spec) apply(simp) @@ -4486,7 +4486,7 @@ apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1)) apply(simp add: calc_atm) apply(drule meta_mp) -apply(drule_tac pi="[(x,xa)]" and x=":M" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(x,xa)]" and x=":Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: calc_atm CAND_eqvt_name) apply(drule meta_mp) apply(drule_tac pi="[(x,xa)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) @@ -4494,7 +4494,7 @@ apply(simp) apply(simp) apply(drule_tac x="a" in meta_spec) -apply(drule_tac x="[(x,y)]\M" in meta_spec) +apply(drule_tac x="[(x,y)]\Ma" in meta_spec) apply(drule_tac x="xa" in meta_spec) apply(drule_tac x="[(x,y)]\N" in meta_spec) apply(simp) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Old_Number_Theory/Chinese.thy --- a/src/HOL/Old_Number_Theory/Chinese.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Old_Number_Theory/Chinese.thy Thu Jul 03 11:31:25 2014 +0200 @@ -174,7 +174,7 @@ apply (rule_tac [!] funprod_zgcd) apply safe apply simp_all - apply (subgoal_tac "ix = a] (mod p)" apply (auto simp add: SetS_def MultInvPair_def) apply (frule StandardRes_SRStar_prop1a) + apply hypsubst_thin apply (subgoal_tac "StandardRes p x \ StandardRes p (a * MultInv p x)") apply (auto simp add: StandardRes_prop2 MultInvPair_distinct) apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Old_Number_Theory/Gauss.thy --- a/src/HOL/Old_Number_Theory/Gauss.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Old_Number_Theory/Gauss.thy Thu Jul 03 11:31:25 2014 +0200 @@ -170,7 +170,7 @@ apply (auto simp add: B_def) apply (frule A_ncong_p) apply (insert p_a_relprime p_prime a_nonzero) - apply (frule_tac a = x and b = a in zcong_zprime_prod_zero_contra) + apply (frule_tac a = xa and b = a in zcong_zprime_prod_zero_contra) apply (auto simp add: A_greater_zero) done @@ -180,9 +180,9 @@ lemma C_ncong_p: "x \ C ==> ~[x = 0](mod p)" apply (auto simp add: C_def) apply (frule B_ncong_p) - apply (subgoal_tac "[x = StandardRes p x](mod p)") + apply (subgoal_tac "[xa = StandardRes p xa](mod p)") defer apply (simp add: StandardRes_prop1) - apply (frule_tac a = x and b = "StandardRes p x" and c = 0 in zcong_trans) + apply (frule_tac a = xa and b = "StandardRes p xa" and c = 0 in zcong_trans) apply auto done diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Probability/ex/Dining_Cryptographers.thy --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Jul 03 11:31:25 2014 +0200 @@ -239,7 +239,7 @@ ultimately have "{dc \ dc_crypto. payer dc = Some i \ inversion dc = xs} = {(Some i, zs), (Some i, map Not zs)}" - using `i < n` + using `i < n` [[ hypsubst_thin = true ]] proof (safe, simp_all add:dc_crypto payer_def) fix b assume [simp]: "length b = n" and *: "inversion (Some i, b) = xs" and "b \ zs" diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Quotient_Examples/Quotient_Int.thy --- a/src/HOL/Quotient_Examples/Quotient_Int.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Thu Jul 03 11:31:25 2014 +0200 @@ -57,6 +57,7 @@ using a apply(cases x, cases y, cases z) apply(auto simp add: times_int_raw.simps intrel.simps) + apply(hypsubst_thin) apply(rename_tac u v w x y z) apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") apply(simp add: mult_ac) @@ -69,6 +70,7 @@ using a apply(cases x, cases y, cases z) apply(auto simp add: times_int_raw.simps intrel.simps) + apply(hypsubst_thin) apply(rename_tac u v w x y z) apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") apply(simp add: mult_ac) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/SET_Protocol/Purchase.thy --- a/src/HOL/SET_Protocol/Purchase.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/SET_Protocol/Purchase.thy Thu Jul 03 11:31:25 2014 +0200 @@ -1119,6 +1119,7 @@ OIData, Hash PIData|} \ set evs" apply clarify +apply hypsubst_thin apply (erule rev_mp) apply (erule rev_mp) apply (erule set_pur.induct, simp_all, auto) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Transcendental.thy Thu Jul 03 11:31:25 2014 +0200 @@ -3046,6 +3046,7 @@ lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y" apply (cut_tac y = y in lemma_tan_total1, auto) + apply hypsubst_thin apply (cut_tac x = xa and y = y in linorder_less_linear, auto) apply (subgoal_tac [2] "\z. y < z & z < xa & DERIV tan z :> 0") apply (subgoal_tac "\z. xa < z & z < y & DERIV tan z :> 0") diff -r c29729f764b1 -r b627e76cc5cc src/HOL/UNITY/Comp/Priority.thy --- a/src/HOL/UNITY/Comp/Priority.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/UNITY/Comp/Priority.thy Thu Jul 03 11:31:25 2014 +0200 @@ -209,7 +209,7 @@ leadsTo {s. above i s < x}" apply (rule leadsTo_UN) apply (rule single_leadsTo_I, clarify) -apply (rule_tac x = "above i x" in above_decreases_lemma) +apply (rule_tac x = "above i xa" in above_decreases_lemma) apply (simp_all (no_asm_use) add: Highest_iff_above0) apply blast+ done diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Word/Bool_List_Representation.thy --- a/src/HOL/Word/Bool_List_Representation.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Word/Bool_List_Representation.thy Thu Jul 03 11:31:25 2014 +0200 @@ -595,7 +595,7 @@ lemma takefill_same': "l = length xs ==> takefill fill l xs = xs" - by clarify (induct xs, auto) + by (induct xs arbitrary: l, auto) lemmas takefill_same [simp] = takefill_same' [OF refl] diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Word/Misc_Typedef.thy --- a/src/HOL/Word/Misc_Typedef.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Word/Misc_Typedef.thy Thu Jul 03 11:31:25 2014 +0200 @@ -194,7 +194,7 @@ prefer 2 apply (simp add: comp_assoc) apply (rule ext) - apply (drule fun_cong) + apply (drule_tac f="?a o ?b" in fun_cong) apply simp done diff -r c29729f764b1 -r b627e76cc5cc src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/Word/Word.thy Thu Jul 03 11:31:25 2014 +0200 @@ -3176,6 +3176,12 @@ of_bl_rep_False [where n=1 and bs="[]", simplified]) done +lemma zip_replicate: + "n \ length ys \ zip (replicate n x) ys = map (\y. (x, y)) ys" + apply (induct ys arbitrary: n, simp_all) + apply (case_tac n, simp_all) + done + lemma align_lem_or [rule_format] : "ALL x m. length x = n + m --> length y = n + m --> drop m x = replicate n False --> take m y = replicate m False --> @@ -3185,9 +3191,8 @@ apply clarsimp apply (case_tac x, force) apply (case_tac m, auto) - apply (drule sym) - apply auto - apply (induct_tac list, auto) + apply (drule_tac t="length ?xs" in sym) + apply (clarsimp simp: map2_def zip_replicate o_def) done lemma align_lem_and [rule_format] : @@ -3199,9 +3204,8 @@ apply clarsimp apply (case_tac x, force) apply (case_tac m, auto) - apply (drule sym) - apply auto - apply (induct_tac list, auto) + apply (drule_tac t="length ?xs" in sym) + apply (clarsimp simp: map2_def zip_replicate o_def map_replicate_const) done lemma aligned_bl_add_size [OF refl]: @@ -3676,6 +3680,7 @@ apply safe defer apply (clarsimp split: prod.splits) + apply hypsubst_thin apply (drule word_ubin.norm_Rep [THEN ssubst]) apply (drule split_bintrunc) apply (simp add : of_bl_def bl2bin_drop word_size diff -r c29729f764b1 -r b627e76cc5cc src/HOL/ZF/HOLZF.thy --- a/src/HOL/ZF/HOLZF.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/ZF/HOLZF.thy Thu Jul 03 11:31:25 2014 +0200 @@ -168,7 +168,7 @@ theorem Domain: "Elem x (Domain f) = (? y. Elem (Opair x y) f)" apply (auto simp add: Domain_def Replacement) - apply (rule_tac x="Snd x" in exI) + apply (rule_tac x="Snd xa" in exI) apply (simp add: FstSnd) apply (rule_tac x="Opair x y" in exI) apply (simp add: isOpair Fst) diff -r c29729f764b1 -r b627e76cc5cc src/HOL/ex/Dedekind_Real.thy --- a/src/HOL/ex/Dedekind_Real.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/HOL/ex/Dedekind_Real.thy Thu Jul 03 11:31:25 2014 +0200 @@ -313,7 +313,7 @@ "[|A \ preal; B \ preal; y \ add_set A B|] ==> \u \ add_set A B. y < u" apply (auto simp add: add_set_def) apply (frule preal_exists_greater [of A], auto) -apply (rule_tac x="u + y" in exI) +apply (rule_tac x="u + ya" in exI) apply (auto intro: add_strict_left_mono) done @@ -439,7 +439,7 @@ "[|A \ preal; B \ preal; y \ mult_set A B|] ==> \u \ mult_set A B. y < u" apply (auto simp add: mult_set_def) apply (frule preal_exists_greater [of A], auto) -apply (rule_tac x="u * y" in exI) +apply (rule_tac x="u * ya" in exI) apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B] mult_strict_right_mono) done @@ -1590,7 +1590,7 @@ "\m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)" apply (simp add: real_of_preal_def real_zero_def, cases x) apply (auto simp add: real_minus add_ac) -apply (cut_tac x = x and y = y in linorder_less_linear) +apply (cut_tac x = xa and y = y in linorder_less_linear) apply (auto dest!: less_add_left_Ex simp add: add_assoc [symmetric]) done diff -r c29729f764b1 -r b627e76cc5cc src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Thu Jul 03 11:30:23 2014 +0200 +++ b/src/Provers/hypsubst.ML Thu Jul 03 11:31:25 2014 +0200 @@ -47,6 +47,8 @@ signature HYPSUBST = sig val bound_hyp_subst_tac : Proof.context -> int -> tactic + val hyp_subst_tac_thin : bool -> Proof.context -> int -> tactic + val hyp_subst_thins : bool Config.T val hyp_subst_tac : Proof.context -> int -> tactic val blast_hyp_subst_tac : bool -> int -> tactic val stac : thm -> int -> tactic @@ -77,7 +79,8 @@ Not if it involves a variable free in the premises, but we can't check for this -- hence bnd and bound_hyp_subst_tac Prefer to eliminate Bound variables if possible. - Result: true = use as is, false = reorient first *) + Result: true = use as is, false = reorient first + also returns var to substitute, relevant if it is Free *) fun inspect_pair bnd novars (t, u) = if novars andalso (has_tvars t orelse has_tvars u) then raise Match (*variables in the type!*) @@ -86,55 +89,75 @@ (Bound i, _) => if loose_bvar1 (u, i) orelse novars andalso has_vars u then raise Match - else true (*eliminates t*) + else (true, Bound i) (*eliminates t*) | (_, Bound i) => if loose_bvar1 (t, i) orelse novars andalso has_vars t then raise Match - else false (*eliminates u*) + else (false, Bound i) (*eliminates u*) | (t' as Free _, _) => if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u then raise Match - else true (*eliminates t*) + else (true, t') (*eliminates t*) | (_, u' as Free _) => if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t then raise Match - else false (*eliminates u*) + else (false, u') (*eliminates u*) | _ => raise Match); (*Locates a substitutable variable on the left (resp. right) of an equality assumption. Returns the number of intervening assumptions. *) -fun eq_var bnd novars = - let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t - | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) = - ((k, inspect_pair bnd novars - (Data.dest_eq (Data.dest_Trueprop A))) - handle TERM _ => eq_var_aux (k+1) B - | Match => eq_var_aux (k+1) B) - | eq_var_aux k _ = raise EQ_VAR - in eq_var_aux 0 end; +fun eq_var bnd novars check_frees t = + let + fun check_free ts (orient, Free f) + = if not check_frees orelse not orient + orelse exists (curry Logic.occs (Free f)) ts + then (orient, true) else raise Match + | check_free ts (orient, _) = (orient, false) + fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) hs = eq_var_aux k t hs + | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) hs = + ((k, check_free (B :: hs) (inspect_pair bnd novars + (Data.dest_eq (Data.dest_Trueprop A)))) + handle TERM _ => eq_var_aux (k+1) B (A :: hs) + | Match => eq_var_aux (k+1) B (A :: hs)) + | eq_var_aux k _ _ = raise EQ_VAR + + in eq_var_aux 0 t [] end; + +val thin_free_eq_tac = SUBGOAL (fn (t, i) => let + val (k, _) = eq_var false false false t + val ok = (eq_var false false true t |> fst) > k + handle EQ_VAR => true + in if ok then EVERY [rotate_tac k i, etac thin_rl i, rotate_tac (~k) i] + else no_tac + end handle EQ_VAR => no_tac) (*For the simpset. Adds ALL suitable equalities, even if not first! No vars are allowed here, as simpsets are built from meta-assumptions*) fun mk_eqs bnd th = - [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th))) + [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th))) |> fst then th RS Data.eq_reflection else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ] handle TERM _ => [] | Match => []; +fun bool2s true = "true" | bool2s false = "false" + local in (*Select a suitable equality assumption; substitute throughout the subgoal If bnd is true, then it replaces Bound variables only. *) fun gen_hyp_subst_tac ctxt bnd = - let fun tac i st = SUBGOAL (fn (Bi, _) => + SUBGOAL (fn (Bi, i) => let - val (k, _) = eq_var bnd true Bi + val (k, (orient, is_free)) = eq_var bnd true true Bi val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd)) in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i, - etac thin_rl i, rotate_tac (~k) i] - end handle THM _ => no_tac | EQ_VAR => no_tac) i st - in REPEAT_DETERM1 o tac end; + if not is_free then etac thin_rl i + else if orient then etac Data.rev_mp i + else etac (Data.sym RS Data.rev_mp) i, + rotate_tac (~k) i, + if is_free then rtac Data.imp_intr i else all_tac] + end handle THM _ => no_tac | EQ_VAR => no_tac) end; @@ -174,6 +197,9 @@ val imp_intr_tac = rtac Data.imp_intr; +fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd; +val dup_subst = rev_dup_elim ssubst + (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *) (* premises containing meta-implications or quantifiers *) @@ -181,26 +207,37 @@ to handle equalities containing Vars.*) fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => let val n = length(Logic.strip_assums_hyp Bi) - 1 - val (k,symopt) = eq_var bnd false Bi + val (k, (orient, is_free)) = eq_var bnd false true Bi + val rl = if is_free then dup_subst else ssubst + val rl = if orient then rl else Data.sym RS rl in DETERM (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), rotate_tac 1 i, REPEAT_DETERM_N (n-k) (etac Data.rev_mp i), - inst_subst_tac symopt (if symopt then ssubst else Data.subst) i, + inst_subst_tac orient rl i, REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)]) end handle THM _ => no_tac | EQ_VAR => no_tac); -(*Substitutes for Free or Bound variables*) -fun hyp_subst_tac ctxt = - FIRST' [ematch_tac [Data.thin_refl], - gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false]; +(*Substitutes for Free or Bound variables, + discarding equalities on Bound variables + and on Free variables if thin=true*) +fun hyp_subst_tac_thin thin ctxt = + REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl], + gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false, + if thin then thin_free_eq_tac else K no_tac]; + +val (hyp_subst_thins, hyp_subst_thins_setup) = Attrib.config_bool + @{binding hypsubst_thin} (K false); + +fun hyp_subst_tac ctxt = hyp_subst_tac_thin + (Config.get ctxt hyp_subst_thins) ctxt (*Substitutes for Bound variables only -- this is always safe*) fun bound_hyp_subst_tac ctxt = - gen_hyp_subst_tac ctxt true ORELSE' vars_gen_hyp_subst_tac true; - + REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true + ORELSE' vars_gen_hyp_subst_tac true); (** Version for Blast_tac. Hyps that are affected by the substitution are moved to the front. Defect: even trivial changes are noticed, such as @@ -236,7 +273,7 @@ fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) => - let val (k,symopt) = eq_var false false Bi + let val (k, (symopt, _)) = eq_var false false false Bi val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi) (*omit selected equality, returning other hyps*) val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1) @@ -252,7 +289,6 @@ end handle THM _ => no_tac | EQ_VAR => no_tac); - (*apply an equality or definition ONCE; fails unless the substitution has an effect*) fun stac th = @@ -266,6 +302,11 @@ Method.setup @{binding hypsubst} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt))) "substitution using an assumption (improper)" #> + Method.setup @{binding hypsubst_thin} + (Scan.succeed (fn ctxt => SIMPLE_METHOD' + (CHANGED_PROP o hyp_subst_tac_thin true ctxt))) + "substitution using an assumption, eliminating assumptions" #> + hyp_subst_thins_setup #> Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th)))) "simple substitution"; diff -r c29729f764b1 -r b627e76cc5cc src/ZF/Coind/ECR.thy --- a/src/ZF/Coind/ECR.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/ZF/Coind/ECR.thy Thu Jul 03 11:31:25 2014 +0200 @@ -100,6 +100,7 @@ \ HasTyRel" apply (unfold hastyenv_def) apply (erule elab_fixE, safe) +apply hypsubst_thin apply (rule subst, assumption) apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI) apply simp_all diff -r c29729f764b1 -r b627e76cc5cc src/ZF/Induct/Multiset.thy --- a/src/ZF/Induct/Multiset.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/ZF/Induct/Multiset.thy Thu Jul 03 11:31:25 2014 +0200 @@ -931,6 +931,7 @@ apply (rule_tac x = M0 in exI, force) (* Subgoal 2 *) apply clarify +apply hypsubst_thin apply (case_tac "a \ mset_of (Ka) ") apply (rule_tac x = I in exI, simp (no_asm_simp)) apply (rule_tac x = J in exI, simp (no_asm_simp)) diff -r c29729f764b1 -r b627e76cc5cc src/ZF/Int_ZF.thy --- a/src/ZF/Int_ZF.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/ZF/Int_ZF.thy Thu Jul 03 11:31:25 2014 +0200 @@ -661,7 +661,7 @@ apply (simp add: zless_def znegative_def zdiff_def int_def) apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def) apply (rule_tac x = k in bexI) -apply (erule add_left_cancel, auto) +apply (erule_tac i="succ (?v)" in add_left_cancel, auto) done lemma zless_imp_succ_zadd: @@ -703,6 +703,7 @@ apply (rule_tac x = "y1#+y2" in exI) apply (auto simp add: add_lt_mono) apply (rule sym) +apply hypsubst_thin apply (erule add_left_cancel)+ apply auto done diff -r c29729f764b1 -r b627e76cc5cc src/ZF/ex/LList.thy --- a/src/ZF/ex/LList.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/ZF/ex/LList.thy Thu Jul 03 11:31:25 2014 +0200 @@ -173,7 +173,7 @@ apply (rule_tac X = "{. l \ llist (A) }" in lleq.coinduct) apply blast apply safe -apply (erule_tac a=l in llist.cases, fast+) +apply (erule_tac a=la in llist.cases, fast+) done diff -r c29729f764b1 -r b627e76cc5cc src/ZF/ex/Primes.thy --- a/src/ZF/ex/Primes.thy Thu Jul 03 11:30:23 2014 +0200 +++ b/src/ZF/ex/Primes.thy Thu Jul 03 11:31:25 2014 +0200 @@ -71,7 +71,7 @@ lemma dvd_mult_right: "[|(i#*j) dvd k; j \ nat|] ==> j dvd k" apply (simp add: divides_def, clarify) -apply (rule_tac x = "i#*k" in bexI) +apply (rule_tac x = "i#*ka" in bexI) apply (simp add: mult_ac) apply (rule mult_type) done