--- 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)
--- 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 \<notin> bad; evs \<in> zg |]
==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
apply clarify
+apply hypsubst_thin
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule zg.induct)
--- 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)
--- 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
--- 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 \<sigma>_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 \<sigma>_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
--- 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
--- 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)
--- 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
--- 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
--- 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 \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
--- 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
--- 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 \<in> float \<Longrightarrow> -x \<in> 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 \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> 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 \<in> float \<Longrightarrow> x / 2^d \<in> 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 \<in> float \<Longrightarrow> x / (2::int)^d \<in> 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])
--- 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 = "\<lambda>M. M - {#a#}" in arg_cong)
+ apply (drule_tac f = "\<lambda>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 = "\<lambda>M. M - {#a#}" in arg_cong, simp)
+ apply (drule_tac f = "\<lambda>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 (\<lambda> 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
--- 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)
--- 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)
--- 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)))"
--- 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)
--- 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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,xa)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(a,c)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(b,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(b,c)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,c)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(aa,c)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(a,aa)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(a,c)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(b,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(b,c)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,b)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(aa,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(aa,c)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(b,aa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(b,aa)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,aa)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(b,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(b,c)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,c)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3806,7 +3806,7 @@
lemma ANDLEFT1_elim:
assumes a: "(x):M \<in> ANDLEFT1 (B AND C) (\<parallel>(B)\<parallel>)"
obtains x' M' where "M = AndL1 (x').M' x" and "fin (AndL1 (x').M' x) x" and "(x'):M' \<in> (\<parallel>(B)\<parallel>)"
-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)]\<bullet>M" in meta_spec)
@@ -3859,7 +3859,7 @@
lemma ANDLEFT2_elim:
assumes a: "(x):M \<in> ANDLEFT2 (B AND C) (\<parallel>(C)\<parallel>)"
obtains x' M' where "M = AndL2 (x').M' x" and "fin (AndL2 (x').M' x) x" and "(x'):M' \<in> (\<parallel>(C)\<parallel>)"
-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)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(x,z)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(y,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(y,z)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,z)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(xa,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(xa,z)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,xa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(x,xa)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(x,z)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(y,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(y,z)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(xa,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(xa,y)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(xa,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(xa,z)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(y,xa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(y,xa)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,xa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,xa)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(y,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(y,z)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,z)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>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)]\<bullet>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)]\<bullet>P)}"
+apply(drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]\<bullet>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="<a>:M{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
+apply(drule_tac pi="[(a,b)]" and x="<a>:Ma{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,b)]\<bullet>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)]\<bullet>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)]\<bullet>P)}"
+apply(drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]\<bullet>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="<a>:M{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
+apply(drule_tac pi="[(a,b)]" and x="<a>:Ma{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>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)]\<bullet>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)]\<bullet>P)}"
+apply(drule_tac pi="[(a,aa)]" and x="(x):Ma{aa:=(z).([(a,aa)]\<bullet>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="<aa>:M{x:=<([(a,aa)]\<bullet>c)>.([(a,aa)]\<bullet>Q)}"
+apply(drule_tac pi="[(a,aa)]" and x="<aa>:Ma{x:=<([(a,aa)]\<bullet>c)>.([(a,aa)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>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)]\<bullet>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)]\<bullet>P)}"
+apply(drule_tac pi="[(a,b)]" and x="(x):Ma{aa:=(z).([(a,b)]\<bullet>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="<aa>:M{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
+apply(drule_tac pi="[(a,b)]" and x="<aa>:Ma{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(xa,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(xa,y)]\<bullet>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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,xa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,xa)]\<bullet>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="<a>:M" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,xa)]" and x="<a>: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)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>N" in meta_spec)
apply(simp)
--- 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 "i<n")
+ apply (subgoal_tac "ia<n")
prefer 2
apply arith
apply (case_tac [2] i)
--- a/src/HOL/Old_Number_Theory/Euler.thy Thu Jul 03 11:30:23 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy Thu Jul 03 11:31:25 2014 +0200
@@ -138,6 +138,7 @@
[\<Prod>x = 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 \<noteq> 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
--- 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 \<in> 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
--- 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 \<in> dc_crypto. payer dc = Some i \<and> 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 \<noteq> zs"
--- 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)
--- 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|}
\<in> set evs"
apply clarify
+apply hypsubst_thin
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule set_pur.induct, simp_all, auto)
--- 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] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
--- 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
--- 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]
--- 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
--- 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 \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>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
--- 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)
--- 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 \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u \<in> 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 \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u \<in> 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 @@
"\<exists>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
--- 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";
--- 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 @@
<cl,t> \<in> 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
--- 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 \<in> 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))
--- 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
--- 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,l>. l \<in> 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
--- 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 \<in> 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