1.1 --- a/src/HOL/Algebra/Divisibility.thy Wed Jul 02 17:34:45 2014 +0200
1.2 +++ b/src/HOL/Algebra/Divisibility.thy Wed Jun 11 14:24:23 2014 +1000
1.3 @@ -1655,6 +1655,7 @@
1.4 using assms
1.5 unfolding factors_def
1.6 apply (safe, force)
1.7 +apply hypsubst_thin
1.8 apply (induct fa)
1.9 apply simp
1.10 apply (simp add: m_assoc)
2.1 --- a/src/HOL/Auth/ZhouGollmann.thy Wed Jul 02 17:34:45 2014 +0200
2.2 +++ b/src/HOL/Auth/ZhouGollmann.thy Wed Jun 11 14:24:23 2014 +1000
2.3 @@ -367,6 +367,7 @@
2.4 A \<notin> bad; evs \<in> zg |]
2.5 ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
2.6 apply clarify
2.7 +apply hypsubst_thin
2.8 apply (erule rev_mp)
2.9 apply (erule rev_mp)
2.10 apply (erule zg.induct)
3.1 --- a/src/HOL/Bali/AxCompl.thy Wed Jul 02 17:34:45 2014 +0200
3.2 +++ b/src/HOL/Bali/AxCompl.thy Wed Jun 11 14:24:23 2014 +1000
3.3 @@ -1381,6 +1381,7 @@
3.4 apply (rule MGF_nested_Methd)
3.5 apply (rule ballI)
3.6 apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec)
3.7 +apply hypsubst_thin
3.8 apply fast
3.9 apply (drule finite_subset)
3.10 apply (erule finite_imageI)
4.1 --- a/src/HOL/Bali/Conform.thy Wed Jul 02 17:34:45 2014 +0200
4.2 +++ b/src/HOL/Bali/Conform.thy Wed Jun 11 14:24:23 2014 +1000
4.3 @@ -440,8 +440,8 @@
4.4 apply (case_tac a)
4.5 apply (case_tac "absorb j a")
4.6 apply auto
4.7 -apply (rename_tac a)
4.8 -apply (case_tac "absorb j (Some a)",auto)
4.9 +apply (rename_tac a')
4.10 +apply (case_tac "absorb j (Some a')",auto)
4.11 apply (erule conforms_NormI)
4.12 done
4.13
5.1 --- a/src/HOL/Decision_Procs/MIR.thy Wed Jul 02 17:34:45 2014 +0200
5.2 +++ b/src/HOL/Decision_Procs/MIR.thy Wed Jun 11 14:24:23 2014 +1000
5.3 @@ -5272,7 +5272,7 @@
5.4 from ee' have tt': "Inum (a#bs) (Add e (C j)) = Inum (a#bs) (Add e' (C j))" by simp
5.5
5.6 from \<sigma>_cong[OF lp tt', where c="c"] px have px':"?sp c e' j" by simp
5.7 - from ecRo jD px' cc' show ?rhs apply auto
5.8 + from ecRo jD px' show ?rhs apply (auto simp: cc')
5.9 by (rule_tac x="(e', c')" in bexI,simp_all)
5.10 (rule_tac x="j" in bexI, simp_all add: cc'[symmetric])
5.11 next
5.12 @@ -5286,7 +5286,7 @@
5.13 and cc':"c = c'" by blast
5.14 from ee' have tt': "Inum (a#bs) (Add e (C j)) = Inum (a#bs) (Add e' (C j))" by simp
5.15 from \<sigma>_cong[OF lp tt', where c="c"] px have px':"?sp c e' j" by simp
5.16 - from ecRo jD px' cc' show ?lhs apply auto
5.17 + from ecRo jD px' show ?lhs apply (auto simp: cc')
5.18 by (rule_tac x="(e', c')" in bexI,simp_all)
5.19 (rule_tac x="j" in bexI, simp_all add: cc'[symmetric])
5.20 qed
6.1 --- a/src/HOL/Divides.thy Wed Jul 02 17:34:45 2014 +0200
6.2 +++ b/src/HOL/Divides.thy Wed Jun 11 14:24:23 2014 +1000
6.3 @@ -461,7 +461,7 @@
6.4 apply (case_tac "y = 0") apply simp
6.5 apply (auto simp add: dvd_def)
6.6 apply (subgoal_tac "-(y * k) = y * - k")
6.7 - apply (erule ssubst)
6.8 + apply (simp only:)
6.9 apply (erule div_mult_self1_is_id)
6.10 apply simp
6.11 done
6.12 @@ -470,8 +470,7 @@
6.13 apply (case_tac "y = 0") apply simp
6.14 apply (auto simp add: dvd_def)
6.15 apply (subgoal_tac "y * k = -y * -k")
6.16 - apply (erule ssubst)
6.17 - apply (rule div_mult_self1_is_id)
6.18 + apply (erule ssubst, rule div_mult_self1_is_id)
6.19 apply simp
6.20 apply simp
6.21 done
7.1 --- a/src/HOL/HOLCF/Library/Stream.thy Wed Jul 02 17:34:45 2014 +0200
7.2 +++ b/src/HOL/HOLCF/Library/Stream.thy Wed Jun 11 14:24:23 2014 +1000
7.3 @@ -5,7 +5,7 @@
7.4 header {* General Stream domain *}
7.5
7.6 theory Stream
7.7 -imports HOLCF "~~/src/HOL/Library/Extended_Nat"
7.8 +imports "../HOLCF" "~~/src/HOL/Library/Extended_Nat"
7.9 begin
7.10
7.11 default_sort pcpo
7.12 @@ -792,8 +792,8 @@
7.13 apply (drule ex_sconc, simp)
7.14 apply (rule someI2_ex, auto)
7.15 apply (simp add: i_rt_Suc_forw)
7.16 - apply (rule_tac x="a && x" in exI, auto)
7.17 - apply (case_tac "xa=UU",auto)
7.18 + apply (rule_tac x="a && xa" in exI, auto)
7.19 + apply (case_tac "xaa=UU",auto)
7.20 apply (drule stream_exhaust_eq [THEN iffD1],auto)
7.21 apply (drule streams_prefix_lemma1,simp+)
7.22 apply (simp add: sconc_def)
8.1 --- a/src/HOL/Hoare_Parallel/OG_Examples.thy Wed Jul 02 17:34:45 2014 +0200
8.2 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Wed Jun 11 14:24:23 2014 +1000
8.3 @@ -443,7 +443,7 @@
8.4 apply (simp_all (*asm_lr*) del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
8.5 --{* 9 subgoals left *}
8.6 apply (force simp add:less_Suc_eq)
8.7 -apply(drule sym)
8.8 +apply(hypsubst_thin, drule sym)
8.9 apply (force simp add:less_Suc_eq)+
8.10 done
8.11
9.1 --- a/src/HOL/IMP/Abs_Int2.thy Wed Jul 02 17:34:45 2014 +0200
9.2 +++ b/src/HOL/IMP/Abs_Int2.thy Wed Jun 11 14:24:23 2014 +1000
9.3 @@ -132,8 +132,10 @@
9.4 by simp (metis And(1) And(2) in_gamma_sup_UpI)
9.5 next
9.6 case (Less e1 e2) thus ?case
9.7 - by(auto split: prod.split)
9.8 - (metis (lifting) inv_aval'_correct aval''_correct inv_less')
9.9 + apply hypsubst_thin
9.10 + apply (auto split: prod.split)
9.11 + apply (metis (lifting) inv_aval'_correct aval''_correct inv_less')
9.12 + done
9.13 qed
9.14
9.15 definition "step' = Step
10.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Wed Jul 02 17:34:45 2014 +0200
10.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Wed Jun 11 14:24:23 2014 +1000
10.3 @@ -166,8 +166,10 @@
10.4 case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI)
10.5 next
10.6 case (Less e1 e2) thus ?case
10.7 - by (auto split: prod.split)
10.8 - (metis afilter_sound filter_less' aval'_sound Less)
10.9 + apply hypsubst_thin
10.10 + apply (auto split: prod.split)
10.11 + apply (metis afilter_sound filter_less' aval'_sound Less)
10.12 + done
10.13 qed
10.14
10.15 fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
11.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Wed Jul 02 17:34:45 2014 +0200
11.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Wed Jun 11 14:24:23 2014 +1000
11.3 @@ -135,11 +135,16 @@
11.4 next
11.5 case (Not b) thus ?case by simp
11.6 next
11.7 - case (And b1 b2) thus ?case by(fastforce simp: in_gamma_join_UpI)
11.8 + case (And b1 b2) thus ?case
11.9 + apply hypsubst_thin
11.10 + apply (fastforce simp: in_gamma_join_UpI)
11.11 + done
11.12 next
11.13 case (Less e1 e2) thus ?case
11.14 - by (auto split: prod.split)
11.15 - (metis afilter_sound filter_less' aval''_sound Less)
11.16 + apply hypsubst_thin
11.17 + apply (auto split: prod.split)
11.18 + apply (metis afilter_sound filter_less' aval''_sound Less)
11.19 + done
11.20 qed
11.21
11.22
12.1 --- a/src/HOL/Library/Float.thy Wed Jul 02 17:34:45 2014 +0200
12.2 +++ b/src/HOL/Library/Float.thy Wed Jun 11 14:24:23 2014 +1000
12.3 @@ -75,6 +75,7 @@
12.4
12.5 lemma uminus_float[simp]: "x \<in> float \<Longrightarrow> -x \<in> float"
12.6 apply (auto simp: float_def)
12.7 + apply hypsubst_thin
12.8 apply (rule_tac x="-x" in exI)
12.9 apply (rule_tac x="xa" in exI)
12.10 apply (simp add: field_simps)
12.11 @@ -82,6 +83,7 @@
12.12
12.13 lemma times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> float"
12.14 apply (auto simp: float_def)
12.15 + apply hypsubst_thin
12.16 apply (rule_tac x="x * xa" in exI)
12.17 apply (rule_tac x="xb + xc" in exI)
12.18 apply (simp add: powr_add)
12.19 @@ -98,6 +100,7 @@
12.20
12.21 lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float"
12.22 apply (auto simp add: float_def)
12.23 + apply hypsubst_thin
12.24 apply (rule_tac x="x" in exI)
12.25 apply (rule_tac x="xa - d" in exI)
12.26 apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
12.27 @@ -105,6 +108,7 @@
12.28
12.29 lemma div_power_2_int_float[simp]: "x \<in> float \<Longrightarrow> x / (2::int)^d \<in> float"
12.30 apply (auto simp add: float_def)
12.31 + apply hypsubst_thin
12.32 apply (rule_tac x="x" in exI)
12.33 apply (rule_tac x="xa - d" in exI)
12.34 apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
13.1 --- a/src/HOL/Library/Multiset.thy Wed Jul 02 17:34:45 2014 +0200
13.2 +++ b/src/HOL/Library/Multiset.thy Wed Jun 11 14:24:23 2014 +1000
13.3 @@ -1653,7 +1653,7 @@
13.4 apply (simp (no_asm))
13.5 apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
13.6 apply (simp (no_asm_simp) add: add_assoc [symmetric])
13.7 - apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
13.8 + apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong)
13.9 apply (simp add: diff_union_single_conv)
13.10 apply (simp (no_asm_use) add: trans_def)
13.11 apply blast
13.12 @@ -1664,7 +1664,7 @@
13.13 apply (rule conjI)
13.14 apply (simp add: multiset_eq_iff split: nat_diff_split)
13.15 apply (rule conjI)
13.16 - apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
13.17 + apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong, simp)
13.18 apply (simp add: multiset_eq_iff split: nat_diff_split)
13.19 apply (simp (no_asm_use) add: trans_def)
13.20 apply blast
13.21 @@ -2760,7 +2760,9 @@
13.22 using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
13.23 also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric]
13.24 apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b1 set2)
13.25 - using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
13.26 + using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1]
13.27 + [[hypsubst_thin = true]]
13.28 + by fastforce
13.29 finally show ?thesis .
13.30 qed
13.31 thus "count (mmap p1 M) b1 = count N1 b1" by transfer
13.32 @@ -2796,7 +2798,9 @@
13.33 also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
13.34 also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
13.35 apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
13.36 - using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
13.37 + using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def
13.38 + [[hypsubst_thin = true]]
13.39 + by fastforce
13.40 finally show ?thesis .
13.41 qed
13.42 thus "count (mmap p2 M) b2 = count N2 b2" by transfer
14.1 --- a/src/HOL/MacLaurin.thy Wed Jul 02 17:34:45 2014 +0200
14.2 +++ b/src/HOL/MacLaurin.thy Wed Jun 11 14:24:23 2014 +1000
14.3 @@ -419,8 +419,7 @@
14.4 apply (simp (no_asm))
14.5 apply (simp (no_asm) add: sin_expansion_lemma)
14.6 apply (force intro!: derivative_eq_intros)
14.7 -apply (subst (asm) setsum.neutral, clarify, case_tac "x", simp, simp)
14.8 -apply (cases n, simp, simp)
14.9 +apply (subst (asm) setsum.neutral, auto)[1]
14.10 apply (rule ccontr, simp)
14.11 apply (drule_tac x = x in spec, simp)
14.12 apply (erule ssubst)
15.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy Wed Jul 02 17:34:45 2014 +0200
15.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Wed Jun 11 14:24:23 2014 +1000
15.3 @@ -93,7 +93,7 @@
15.4 apply( rule oconf_obj [THEN iffD2])
15.5 apply( simp (no_asm))
15.6 apply( intro strip)
15.7 -apply( case_tac "(aaa, b) = (fn, fd)")
15.8 +apply( case_tac "(ab, b) = (fn, fd)")
15.9 apply( simp)
15.10 apply( fast intro: conf_widen)
15.11 apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD)
16.1 --- a/src/HOL/Nat.thy Wed Jul 02 17:34:45 2014 +0200
16.2 +++ b/src/HOL/Nat.thy Wed Jun 11 14:24:23 2014 +1000
16.3 @@ -1168,7 +1168,7 @@
16.4 -- {* elimination of @{text -} on @{text nat} *}
16.5 by (cases "a < b")
16.6 (auto simp add: diff_is_0_eq [THEN iffD2] diff_add_inverse
16.7 - not_less le_less dest!: sym [of a] sym [of b] add_eq_self_zero)
16.8 + not_less le_less dest!: add_eq_self_zero add_eq_self_zero[OF sym])
16.9
16.10 lemma nat_diff_split_asm:
16.11 "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
17.1 --- a/src/HOL/Nominal/Examples/Class1.thy Wed Jul 02 17:34:45 2014 +0200
17.2 +++ b/src/HOL/Nominal/Examples/Class1.thy Wed Jun 11 14:24:23 2014 +1000
17.3 @@ -4720,7 +4720,7 @@
17.4 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.5 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.6 apply(auto)
17.7 -apply(rotate_tac 1)
17.8 +apply(rotate_tac 2)
17.9 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
17.10 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.11 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.12 @@ -4741,7 +4741,7 @@
17.13 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.14 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.15 apply(auto)
17.16 -apply(rotate_tac 1)
17.17 +apply(rotate_tac 2)
17.18 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
17.19 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.20 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.21 @@ -4851,7 +4851,7 @@
17.22 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.23 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.24 apply(auto)
17.25 -apply(rotate_tac 2)
17.26 +apply(rotate_tac 3)
17.27 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
17.28 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.29 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.30 @@ -4872,7 +4872,7 @@
17.31 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.32 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.33 apply(auto)
17.34 -apply(rotate_tac 2)
17.35 +apply(rotate_tac 3)
17.36 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
17.37 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.38 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.39 @@ -4982,7 +4982,7 @@
17.40 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.41 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.42 apply(auto)
17.43 -apply(rotate_tac 2)
17.44 +apply(rotate_tac 3)
17.45 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
17.46 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.47 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.48 @@ -5003,7 +5003,7 @@
17.49 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.50 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.51 apply(auto)
17.52 -apply(rotate_tac 2)
17.53 +apply(rotate_tac 3)
17.54 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
17.55 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.56 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.57 @@ -5113,7 +5113,7 @@
17.58 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.59 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
17.60 apply(auto)
17.61 -apply(rotate_tac 2)
17.62 +apply(rotate_tac 3)
17.63 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
17.64 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
17.65 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
18.1 --- a/src/HOL/Nominal/Examples/Class2.thy Wed Jul 02 17:34:45 2014 +0200
18.2 +++ b/src/HOL/Nominal/Examples/Class2.thy Wed Jun 11 14:24:23 2014 +1000
18.3 @@ -3491,7 +3491,7 @@
18.4 using a
18.5 apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
18.6 apply(drule_tac x="x" in meta_spec)
18.7 -apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
18.8 +apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
18.9 apply(simp)
18.10 apply(drule meta_mp)
18.11 apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
18.12 @@ -3508,7 +3508,7 @@
18.13 using a
18.14 apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
18.15 apply(drule_tac x="a" in meta_spec)
18.16 -apply(drule_tac x="[(x,xa)]\<bullet>M" in meta_spec)
18.17 +apply(drule_tac x="[(x,xa)]\<bullet>Ma" in meta_spec)
18.18 apply(simp)
18.19 apply(drule meta_mp)
18.20 apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
18.21 @@ -3526,7 +3526,7 @@
18.22 using a
18.23 apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm fresh_atm)
18.24 apply(drule_tac x="c" in meta_spec)
18.25 -apply(drule_tac x="[(a,c)]\<bullet>M" in meta_spec)
18.26 +apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
18.27 apply(drule_tac x="c" in meta_spec)
18.28 apply(drule_tac x="[(a,c)]\<bullet>N" in meta_spec)
18.29 apply(simp)
18.30 @@ -3543,7 +3543,7 @@
18.31 apply(case_tac "a=b")
18.32 apply(simp)
18.33 apply(drule_tac x="c" in meta_spec)
18.34 -apply(drule_tac x="[(b,c)]\<bullet>M" in meta_spec)
18.35 +apply(drule_tac x="[(b,c)]\<bullet>Ma" in meta_spec)
18.36 apply(drule_tac x="c" in meta_spec)
18.37 apply(drule_tac x="[(b,c)]\<bullet>N" in meta_spec)
18.38 apply(simp)
18.39 @@ -3561,7 +3561,7 @@
18.40 apply(case_tac "c=b")
18.41 apply(simp)
18.42 apply(drule_tac x="b" in meta_spec)
18.43 -apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
18.44 +apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
18.45 apply(drule_tac x="a" in meta_spec)
18.46 apply(drule_tac x="[(a,b)]\<bullet>N" in meta_spec)
18.47 apply(simp)
18.48 @@ -3577,7 +3577,7 @@
18.49 apply(simp)
18.50 apply(simp)
18.51 apply(drule_tac x="c" in meta_spec)
18.52 -apply(drule_tac x="[(a,c)]\<bullet>M" in meta_spec)
18.53 +apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
18.54 apply(drule_tac x="b" in meta_spec)
18.55 apply(drule_tac x="[(a,c)]\<bullet>N" in meta_spec)
18.56 apply(simp)
18.57 @@ -3594,7 +3594,7 @@
18.58 apply(case_tac "a=aa")
18.59 apply(simp)
18.60 apply(drule_tac x="c" in meta_spec)
18.61 -apply(drule_tac x="[(aa,c)]\<bullet>M" in meta_spec)
18.62 +apply(drule_tac x="[(aa,c)]\<bullet>Ma" in meta_spec)
18.63 apply(drule_tac x="c" in meta_spec)
18.64 apply(drule_tac x="[(aa,c)]\<bullet>N" in meta_spec)
18.65 apply(simp)
18.66 @@ -3612,7 +3612,7 @@
18.67 apply(case_tac "c=aa")
18.68 apply(simp)
18.69 apply(drule_tac x="a" in meta_spec)
18.70 -apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
18.71 +apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
18.72 apply(drule_tac x="aa" in meta_spec)
18.73 apply(drule_tac x="[(a,aa)]\<bullet>N" in meta_spec)
18.74 apply(simp)
18.75 @@ -3628,7 +3628,7 @@
18.76 apply(simp)
18.77 apply(simp)
18.78 apply(drule_tac x="aa" in meta_spec)
18.79 -apply(drule_tac x="[(a,c)]\<bullet>M" in meta_spec)
18.80 +apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
18.81 apply(drule_tac x="c" in meta_spec)
18.82 apply(drule_tac x="[(a,c)]\<bullet>N" in meta_spec)
18.83 apply(simp)
18.84 @@ -3647,7 +3647,7 @@
18.85 apply(case_tac "aa=b")
18.86 apply(simp)
18.87 apply(drule_tac x="c" in meta_spec)
18.88 -apply(drule_tac x="[(b,c)]\<bullet>M" in meta_spec)
18.89 +apply(drule_tac x="[(b,c)]\<bullet>Ma" in meta_spec)
18.90 apply(drule_tac x="c" in meta_spec)
18.91 apply(drule_tac x="[(b,c)]\<bullet>N" in meta_spec)
18.92 apply(simp)
18.93 @@ -3665,7 +3665,7 @@
18.94 apply(case_tac "c=b")
18.95 apply(simp)
18.96 apply(drule_tac x="b" in meta_spec)
18.97 -apply(drule_tac x="[(aa,b)]\<bullet>M" in meta_spec)
18.98 +apply(drule_tac x="[(aa,b)]\<bullet>Ma" in meta_spec)
18.99 apply(drule_tac x="aa" in meta_spec)
18.100 apply(drule_tac x="[(aa,b)]\<bullet>N" in meta_spec)
18.101 apply(simp)
18.102 @@ -3681,7 +3681,7 @@
18.103 apply(simp)
18.104 apply(simp)
18.105 apply(drule_tac x="c" in meta_spec)
18.106 -apply(drule_tac x="[(aa,c)]\<bullet>M" in meta_spec)
18.107 +apply(drule_tac x="[(aa,c)]\<bullet>Ma" in meta_spec)
18.108 apply(drule_tac x="b" in meta_spec)
18.109 apply(drule_tac x="[(aa,c)]\<bullet>N" in meta_spec)
18.110 apply(simp)
18.111 @@ -3701,7 +3701,7 @@
18.112 apply(case_tac "a=b")
18.113 apply(simp)
18.114 apply(drule_tac x="b" in meta_spec)
18.115 -apply(drule_tac x="[(b,aa)]\<bullet>M" in meta_spec)
18.116 +apply(drule_tac x="[(b,aa)]\<bullet>Ma" in meta_spec)
18.117 apply(drule_tac x="aa" in meta_spec)
18.118 apply(drule_tac x="[(b,aa)]\<bullet>N" in meta_spec)
18.119 apply(simp)
18.120 @@ -3719,7 +3719,7 @@
18.121 apply(case_tac "aa=b")
18.122 apply(simp)
18.123 apply(drule_tac x="a" in meta_spec)
18.124 -apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
18.125 +apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
18.126 apply(drule_tac x="a" in meta_spec)
18.127 apply(drule_tac x="[(a,b)]\<bullet>N" in meta_spec)
18.128 apply(simp)
18.129 @@ -3735,7 +3735,7 @@
18.130 apply(simp)
18.131 apply(simp)
18.132 apply(drule_tac x="a" in meta_spec)
18.133 -apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
18.134 +apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
18.135 apply(drule_tac x="b" in meta_spec)
18.136 apply(drule_tac x="[(a,aa)]\<bullet>N" in meta_spec)
18.137 apply(simp)
18.138 @@ -3753,7 +3753,7 @@
18.139 apply(case_tac "a=b")
18.140 apply(simp)
18.141 apply(drule_tac x="aa" in meta_spec)
18.142 -apply(drule_tac x="[(b,c)]\<bullet>M" in meta_spec)
18.143 +apply(drule_tac x="[(b,c)]\<bullet>Ma" in meta_spec)
18.144 apply(drule_tac x="c" in meta_spec)
18.145 apply(drule_tac x="[(b,c)]\<bullet>N" in meta_spec)
18.146 apply(simp)
18.147 @@ -3771,7 +3771,7 @@
18.148 apply(case_tac "c=b")
18.149 apply(simp)
18.150 apply(drule_tac x="aa" in meta_spec)
18.151 -apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
18.152 +apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
18.153 apply(drule_tac x="a" in meta_spec)
18.154 apply(drule_tac x="[(a,b)]\<bullet>N" in meta_spec)
18.155 apply(simp)
18.156 @@ -3787,7 +3787,7 @@
18.157 apply(simp)
18.158 apply(simp)
18.159 apply(drule_tac x="aa" in meta_spec)
18.160 -apply(drule_tac x="[(a,c)]\<bullet>M" in meta_spec)
18.161 +apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
18.162 apply(drule_tac x="b" in meta_spec)
18.163 apply(drule_tac x="[(a,c)]\<bullet>N" in meta_spec)
18.164 apply(simp)
18.165 @@ -3806,7 +3806,7 @@
18.166 lemma ANDLEFT1_elim:
18.167 assumes a: "(x):M \<in> ANDLEFT1 (B AND C) (\<parallel>(B)\<parallel>)"
18.168 obtains x' M' where "M = AndL1 (x').M' x" and "fin (AndL1 (x').M' x) x" and "(x'):M' \<in> (\<parallel>(B)\<parallel>)"
18.169 -using a
18.170 +using a [[ hypsubst_thin = true ]]
18.171 apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
18.172 apply(drule_tac x="y" in meta_spec)
18.173 apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
18.174 @@ -3859,7 +3859,7 @@
18.175 lemma ANDLEFT2_elim:
18.176 assumes a: "(x):M \<in> ANDLEFT2 (B AND C) (\<parallel>(C)\<parallel>)"
18.177 obtains x' M' where "M = AndL2 (x').M' x" and "fin (AndL2 (x').M' x) x" and "(x'):M' \<in> (\<parallel>(C)\<parallel>)"
18.178 -using a
18.179 +using a [[ hypsubst_thin = true ]]
18.180 apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
18.181 apply(drule_tac x="y" in meta_spec)
18.182 apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
18.183 @@ -3915,7 +3915,7 @@
18.184 using a
18.185 apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
18.186 apply(drule_tac x="b" in meta_spec)
18.187 -apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
18.188 +apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
18.189 apply(simp)
18.190 apply(drule meta_mp)
18.191 apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
18.192 @@ -3927,7 +3927,7 @@
18.193 apply(case_tac "a=aa")
18.194 apply(simp)
18.195 apply(drule_tac x="b" in meta_spec)
18.196 -apply(drule_tac x="[(aa,b)]\<bullet>M" in meta_spec)
18.197 +apply(drule_tac x="[(aa,b)]\<bullet>Ma" in meta_spec)
18.198 apply(simp)
18.199 apply(drule meta_mp)
18.200 apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2))
18.201 @@ -3940,7 +3940,7 @@
18.202 apply(case_tac "b=aa")
18.203 apply(simp)
18.204 apply(drule_tac x="a" in meta_spec)
18.205 -apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
18.206 +apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
18.207 apply(simp)
18.208 apply(drule meta_mp)
18.209 apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
18.210 @@ -3951,7 +3951,7 @@
18.211 apply(simp)
18.212 apply(simp)
18.213 apply(drule_tac x="aa" in meta_spec)
18.214 -apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
18.215 +apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
18.216 apply(simp)
18.217 apply(drule meta_mp)
18.218 apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
18.219 @@ -3968,7 +3968,7 @@
18.220 using a
18.221 apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
18.222 apply(drule_tac x="b" in meta_spec)
18.223 -apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
18.224 +apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
18.225 apply(simp)
18.226 apply(drule meta_mp)
18.227 apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
18.228 @@ -3980,7 +3980,7 @@
18.229 apply(case_tac "a=aa")
18.230 apply(simp)
18.231 apply(drule_tac x="b" in meta_spec)
18.232 -apply(drule_tac x="[(aa,b)]\<bullet>M" in meta_spec)
18.233 +apply(drule_tac x="[(aa,b)]\<bullet>Ma" in meta_spec)
18.234 apply(simp)
18.235 apply(drule meta_mp)
18.236 apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2))
18.237 @@ -3993,7 +3993,7 @@
18.238 apply(case_tac "b=aa")
18.239 apply(simp)
18.240 apply(drule_tac x="a" in meta_spec)
18.241 -apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
18.242 +apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
18.243 apply(simp)
18.244 apply(drule meta_mp)
18.245 apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
18.246 @@ -4004,7 +4004,7 @@
18.247 apply(simp)
18.248 apply(simp)
18.249 apply(drule_tac x="aa" in meta_spec)
18.250 -apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
18.251 +apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
18.252 apply(simp)
18.253 apply(drule meta_mp)
18.254 apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
18.255 @@ -4022,7 +4022,7 @@
18.256 using a
18.257 apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm fresh_atm)
18.258 apply(drule_tac x="z" in meta_spec)
18.259 -apply(drule_tac x="[(x,z)]\<bullet>M" in meta_spec)
18.260 +apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
18.261 apply(drule_tac x="z" in meta_spec)
18.262 apply(drule_tac x="[(x,z)]\<bullet>N" in meta_spec)
18.263 apply(simp)
18.264 @@ -4039,7 +4039,7 @@
18.265 apply(case_tac "x=y")
18.266 apply(simp)
18.267 apply(drule_tac x="z" in meta_spec)
18.268 -apply(drule_tac x="[(y,z)]\<bullet>M" in meta_spec)
18.269 +apply(drule_tac x="[(y,z)]\<bullet>Ma" in meta_spec)
18.270 apply(drule_tac x="z" in meta_spec)
18.271 apply(drule_tac x="[(y,z)]\<bullet>N" in meta_spec)
18.272 apply(simp)
18.273 @@ -4057,7 +4057,7 @@
18.274 apply(case_tac "z=y")
18.275 apply(simp)
18.276 apply(drule_tac x="y" in meta_spec)
18.277 -apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
18.278 +apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
18.279 apply(drule_tac x="x" in meta_spec)
18.280 apply(drule_tac x="[(x,y)]\<bullet>N" in meta_spec)
18.281 apply(simp)
18.282 @@ -4073,7 +4073,7 @@
18.283 apply(simp)
18.284 apply(simp)
18.285 apply(drule_tac x="z" in meta_spec)
18.286 -apply(drule_tac x="[(x,z)]\<bullet>M" in meta_spec)
18.287 +apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
18.288 apply(drule_tac x="y" in meta_spec)
18.289 apply(drule_tac x="[(x,z)]\<bullet>N" in meta_spec)
18.290 apply(simp)
18.291 @@ -4090,7 +4090,7 @@
18.292 apply(case_tac "x=xa")
18.293 apply(simp)
18.294 apply(drule_tac x="z" in meta_spec)
18.295 -apply(drule_tac x="[(xa,z)]\<bullet>M" in meta_spec)
18.296 +apply(drule_tac x="[(xa,z)]\<bullet>Ma" in meta_spec)
18.297 apply(drule_tac x="z" in meta_spec)
18.298 apply(drule_tac x="[(xa,z)]\<bullet>N" in meta_spec)
18.299 apply(simp)
18.300 @@ -4108,7 +4108,7 @@
18.301 apply(case_tac "z=xa")
18.302 apply(simp)
18.303 apply(drule_tac x="x" in meta_spec)
18.304 -apply(drule_tac x="[(x,xa)]\<bullet>M" in meta_spec)
18.305 +apply(drule_tac x="[(x,xa)]\<bullet>Ma" in meta_spec)
18.306 apply(drule_tac x="xa" in meta_spec)
18.307 apply(drule_tac x="[(x,xa)]\<bullet>N" in meta_spec)
18.308 apply(simp)
18.309 @@ -4124,7 +4124,7 @@
18.310 apply(simp)
18.311 apply(simp)
18.312 apply(drule_tac x="xa" in meta_spec)
18.313 -apply(drule_tac x="[(x,z)]\<bullet>M" in meta_spec)
18.314 +apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
18.315 apply(drule_tac x="z" in meta_spec)
18.316 apply(drule_tac x="[(x,z)]\<bullet>N" in meta_spec)
18.317 apply(simp)
18.318 @@ -4143,7 +4143,7 @@
18.319 apply(case_tac "xa=y")
18.320 apply(simp)
18.321 apply(drule_tac x="z" in meta_spec)
18.322 -apply(drule_tac x="[(y,z)]\<bullet>M" in meta_spec)
18.323 +apply(drule_tac x="[(y,z)]\<bullet>Ma" in meta_spec)
18.324 apply(drule_tac x="z" in meta_spec)
18.325 apply(drule_tac x="[(y,z)]\<bullet>N" in meta_spec)
18.326 apply(simp)
18.327 @@ -4161,7 +4161,7 @@
18.328 apply(case_tac "z=y")
18.329 apply(simp)
18.330 apply(drule_tac x="y" in meta_spec)
18.331 -apply(drule_tac x="[(xa,y)]\<bullet>M" in meta_spec)
18.332 +apply(drule_tac x="[(xa,y)]\<bullet>Ma" in meta_spec)
18.333 apply(drule_tac x="xa" in meta_spec)
18.334 apply(drule_tac x="[(xa,y)]\<bullet>N" in meta_spec)
18.335 apply(simp)
18.336 @@ -4177,7 +4177,7 @@
18.337 apply(simp)
18.338 apply(simp)
18.339 apply(drule_tac x="z" in meta_spec)
18.340 -apply(drule_tac x="[(xa,z)]\<bullet>M" in meta_spec)
18.341 +apply(drule_tac x="[(xa,z)]\<bullet>Ma" in meta_spec)
18.342 apply(drule_tac x="y" in meta_spec)
18.343 apply(drule_tac x="[(xa,z)]\<bullet>N" in meta_spec)
18.344 apply(simp)
18.345 @@ -4197,7 +4197,7 @@
18.346 apply(case_tac "x=y")
18.347 apply(simp)
18.348 apply(drule_tac x="y" in meta_spec)
18.349 -apply(drule_tac x="[(y,xa)]\<bullet>M" in meta_spec)
18.350 +apply(drule_tac x="[(y,xa)]\<bullet>Ma" in meta_spec)
18.351 apply(drule_tac x="xa" in meta_spec)
18.352 apply(drule_tac x="[(y,xa)]\<bullet>N" in meta_spec)
18.353 apply(simp)
18.354 @@ -4215,7 +4215,7 @@
18.355 apply(case_tac "xa=y")
18.356 apply(simp)
18.357 apply(drule_tac x="x" in meta_spec)
18.358 -apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
18.359 +apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
18.360 apply(drule_tac x="x" in meta_spec)
18.361 apply(drule_tac x="[(x,y)]\<bullet>N" in meta_spec)
18.362 apply(simp)
18.363 @@ -4231,7 +4231,7 @@
18.364 apply(simp)
18.365 apply(simp)
18.366 apply(drule_tac x="x" in meta_spec)
18.367 -apply(drule_tac x="[(x,xa)]\<bullet>M" in meta_spec)
18.368 +apply(drule_tac x="[(x,xa)]\<bullet>Ma" in meta_spec)
18.369 apply(drule_tac x="y" in meta_spec)
18.370 apply(drule_tac x="[(x,xa)]\<bullet>N" in meta_spec)
18.371 apply(simp)
18.372 @@ -4249,7 +4249,7 @@
18.373 apply(case_tac "x=y")
18.374 apply(simp)
18.375 apply(drule_tac x="xa" in meta_spec)
18.376 -apply(drule_tac x="[(y,z)]\<bullet>M" in meta_spec)
18.377 +apply(drule_tac x="[(y,z)]\<bullet>Ma" in meta_spec)
18.378 apply(drule_tac x="z" in meta_spec)
18.379 apply(drule_tac x="[(y,z)]\<bullet>N" in meta_spec)
18.380 apply(simp)
18.381 @@ -4267,7 +4267,7 @@
18.382 apply(case_tac "z=y")
18.383 apply(simp)
18.384 apply(drule_tac x="xa" in meta_spec)
18.385 -apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
18.386 +apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
18.387 apply(drule_tac x="x" in meta_spec)
18.388 apply(drule_tac x="[(x,y)]\<bullet>N" in meta_spec)
18.389 apply(simp)
18.390 @@ -4283,7 +4283,7 @@
18.391 apply(simp)
18.392 apply(simp)
18.393 apply(drule_tac x="xa" in meta_spec)
18.394 -apply(drule_tac x="[(x,z)]\<bullet>M" in meta_spec)
18.395 +apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
18.396 apply(drule_tac x="y" in meta_spec)
18.397 apply(drule_tac x="[(x,z)]\<bullet>N" in meta_spec)
18.398 apply(simp)
18.399 @@ -4308,7 +4308,7 @@
18.400 apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
18.401 apply(drule_tac x="x" in meta_spec)
18.402 apply(drule_tac x="b" in meta_spec)
18.403 -apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
18.404 +apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
18.405 apply(simp)
18.406 apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
18.407 apply(simp add: calc_atm)
18.408 @@ -4319,7 +4319,7 @@
18.409 apply(drule_tac x="z" in spec)
18.410 apply(drule_tac x="[(a,b)]\<bullet>P" in spec)
18.411 apply(simp add: fresh_prod fresh_left calc_atm)
18.412 -apply(drule_tac pi="[(a,b)]" and x="(x):M{a:=(z).([(a,b)]\<bullet>P)}"
18.413 +apply(drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]\<bullet>P)}"
18.414 in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
18.415 apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)
18.416 apply(drule meta_mp)
18.417 @@ -4332,7 +4332,7 @@
18.418 apply(simp add: fresh_prod fresh_left)
18.419 apply(drule mp)
18.420 apply(simp add: calc_atm)
18.421 -apply(drule_tac pi="[(a,b)]" and x="<a>:M{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
18.422 +apply(drule_tac pi="[(a,b)]" and x="<a>:Ma{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
18.423 in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
18.424 apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
18.425 apply(simp add: calc_atm)
18.426 @@ -4340,7 +4340,7 @@
18.427 apply(simp)
18.428 apply(drule_tac x="x" in meta_spec)
18.429 apply(drule_tac x="b" in meta_spec)
18.430 -apply(drule_tac x="[(aa,b)]\<bullet>M" in meta_spec)
18.431 +apply(drule_tac x="[(aa,b)]\<bullet>Ma" in meta_spec)
18.432 apply(simp)
18.433 apply(drule meta_mp)
18.434 apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2))
18.435 @@ -4352,7 +4352,7 @@
18.436 apply(drule_tac x="z" in spec)
18.437 apply(drule_tac x="[(a,b)]\<bullet>P" in spec)
18.438 apply(simp add: fresh_prod fresh_left calc_atm)
18.439 -apply(drule_tac pi="[(a,b)]" and x="(x):M{a:=(z).([(a,b)]\<bullet>P)}"
18.440 +apply(drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]\<bullet>P)}"
18.441 in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
18.442 apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)
18.443 apply(drule meta_mp)
18.444 @@ -4365,7 +4365,7 @@
18.445 apply(simp add: fresh_prod fresh_left)
18.446 apply(drule mp)
18.447 apply(simp add: calc_atm)
18.448 -apply(drule_tac pi="[(a,b)]" and x="<a>:M{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
18.449 +apply(drule_tac pi="[(a,b)]" and x="<a>:Ma{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
18.450 in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
18.451 apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
18.452 apply(simp add: calc_atm)
18.453 @@ -4374,7 +4374,7 @@
18.454 apply(simp)
18.455 apply(drule_tac x="x" in meta_spec)
18.456 apply(drule_tac x="a" in meta_spec)
18.457 -apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
18.458 +apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
18.459 apply(simp)
18.460 apply(drule meta_mp)
18.461 apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
18.462 @@ -4386,7 +4386,7 @@
18.463 apply(drule_tac x="z" in spec)
18.464 apply(drule_tac x="[(a,aa)]\<bullet>P" in spec)
18.465 apply(simp add: fresh_prod fresh_left calc_atm)
18.466 -apply(drule_tac pi="[(a,aa)]" and x="(x):M{aa:=(z).([(a,aa)]\<bullet>P)}"
18.467 +apply(drule_tac pi="[(a,aa)]" and x="(x):Ma{aa:=(z).([(a,aa)]\<bullet>P)}"
18.468 in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
18.469 apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)
18.470 apply(drule meta_mp)
18.471 @@ -4399,14 +4399,14 @@
18.472 apply(simp add: fresh_prod fresh_left)
18.473 apply(drule mp)
18.474 apply(simp add: calc_atm)
18.475 -apply(drule_tac pi="[(a,aa)]" and x="<aa>:M{x:=<([(a,aa)]\<bullet>c)>.([(a,aa)]\<bullet>Q)}"
18.476 +apply(drule_tac pi="[(a,aa)]" and x="<aa>:Ma{x:=<([(a,aa)]\<bullet>c)>.([(a,aa)]\<bullet>Q)}"
18.477 in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
18.478 apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
18.479 apply(simp add: calc_atm)
18.480 apply(simp)
18.481 apply(drule_tac x="x" in meta_spec)
18.482 apply(drule_tac x="aa" in meta_spec)
18.483 -apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
18.484 +apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
18.485 apply(simp)
18.486 apply(drule meta_mp)
18.487 apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
18.488 @@ -4418,7 +4418,7 @@
18.489 apply(drule_tac x="z" in spec)
18.490 apply(drule_tac x="[(a,b)]\<bullet>P" in spec)
18.491 apply(simp add: fresh_prod fresh_left calc_atm)
18.492 -apply(drule_tac pi="[(a,b)]" and x="(x):M{aa:=(z).([(a,b)]\<bullet>P)}"
18.493 +apply(drule_tac pi="[(a,b)]" and x="(x):Ma{aa:=(z).([(a,b)]\<bullet>P)}"
18.494 in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
18.495 apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)
18.496 apply(drule meta_mp)
18.497 @@ -4430,7 +4430,7 @@
18.498 apply(simp add: fresh_prod fresh_left)
18.499 apply(drule mp)
18.500 apply(simp add: calc_atm)
18.501 -apply(drule_tac pi="[(a,b)]" and x="<aa>:M{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
18.502 +apply(drule_tac pi="[(a,b)]" and x="<aa>:Ma{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
18.503 in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
18.504 apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
18.505 apply(simp add: calc_atm)
18.506 @@ -4443,7 +4443,7 @@
18.507 using a
18.508 apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
18.509 apply(drule_tac x="a" in meta_spec)
18.510 -apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
18.511 +apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
18.512 apply(drule_tac x="y" in meta_spec)
18.513 apply(drule_tac x="[(x,y)]\<bullet>N" in meta_spec)
18.514 apply(simp)
18.515 @@ -4460,7 +4460,7 @@
18.516 apply(case_tac "x=xa")
18.517 apply(simp)
18.518 apply(drule_tac x="a" in meta_spec)
18.519 -apply(drule_tac x="[(xa,y)]\<bullet>M" in meta_spec)
18.520 +apply(drule_tac x="[(xa,y)]\<bullet>Ma" in meta_spec)
18.521 apply(drule_tac x="y" in meta_spec)
18.522 apply(drule_tac x="[(xa,y)]\<bullet>N" in meta_spec)
18.523 apply(simp)
18.524 @@ -4478,7 +4478,7 @@
18.525 apply(case_tac "y=xa")
18.526 apply(simp)
18.527 apply(drule_tac x="a" in meta_spec)
18.528 -apply(drule_tac x="[(x,xa)]\<bullet>M" in meta_spec)
18.529 +apply(drule_tac x="[(x,xa)]\<bullet>Ma" in meta_spec)
18.530 apply(drule_tac x="x" in meta_spec)
18.531 apply(drule_tac x="[(x,xa)]\<bullet>N" in meta_spec)
18.532 apply(simp)
18.533 @@ -4486,7 +4486,7 @@
18.534 apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
18.535 apply(simp add: calc_atm)
18.536 apply(drule meta_mp)
18.537 -apply(drule_tac pi="[(x,xa)]" and x="<a>:M" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
18.538 +apply(drule_tac pi="[(x,xa)]" and x="<a>:Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
18.539 apply(simp add: calc_atm CAND_eqvt_name)
18.540 apply(drule meta_mp)
18.541 apply(drule_tac pi="[(x,xa)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
18.542 @@ -4494,7 +4494,7 @@
18.543 apply(simp)
18.544 apply(simp)
18.545 apply(drule_tac x="a" in meta_spec)
18.546 -apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
18.547 +apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
18.548 apply(drule_tac x="xa" in meta_spec)
18.549 apply(drule_tac x="[(x,y)]\<bullet>N" in meta_spec)
18.550 apply(simp)
19.1 --- a/src/HOL/Old_Number_Theory/Chinese.thy Wed Jul 02 17:34:45 2014 +0200
19.2 +++ b/src/HOL/Old_Number_Theory/Chinese.thy Wed Jun 11 14:24:23 2014 +1000
19.3 @@ -174,7 +174,7 @@
19.4 apply (rule_tac [!] funprod_zgcd)
19.5 apply safe
19.6 apply simp_all
19.7 - apply (subgoal_tac "i<n")
19.8 + apply (subgoal_tac "ia<n")
19.9 prefer 2
19.10 apply arith
19.11 apply (case_tac [2] i)
20.1 --- a/src/HOL/Old_Number_Theory/Euler.thy Wed Jul 02 17:34:45 2014 +0200
20.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy Wed Jun 11 14:24:23 2014 +1000
20.3 @@ -138,6 +138,7 @@
20.4 [\<Prod>x = a] (mod p)"
20.5 apply (auto simp add: SetS_def MultInvPair_def)
20.6 apply (frule StandardRes_SRStar_prop1a)
20.7 + apply hypsubst_thin
20.8 apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)")
20.9 apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
20.10 apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in
21.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy Wed Jul 02 17:34:45 2014 +0200
21.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy Wed Jun 11 14:24:23 2014 +1000
21.3 @@ -170,7 +170,7 @@
21.4 apply (auto simp add: B_def)
21.5 apply (frule A_ncong_p)
21.6 apply (insert p_a_relprime p_prime a_nonzero)
21.7 - apply (frule_tac a = x and b = a in zcong_zprime_prod_zero_contra)
21.8 + apply (frule_tac a = xa and b = a in zcong_zprime_prod_zero_contra)
21.9 apply (auto simp add: A_greater_zero)
21.10 done
21.11
21.12 @@ -180,9 +180,9 @@
21.13 lemma C_ncong_p: "x \<in> C ==> ~[x = 0](mod p)"
21.14 apply (auto simp add: C_def)
21.15 apply (frule B_ncong_p)
21.16 - apply (subgoal_tac "[x = StandardRes p x](mod p)")
21.17 + apply (subgoal_tac "[xa = StandardRes p xa](mod p)")
21.18 defer apply (simp add: StandardRes_prop1)
21.19 - apply (frule_tac a = x and b = "StandardRes p x" and c = 0 in zcong_trans)
21.20 + apply (frule_tac a = xa and b = "StandardRes p xa" and c = 0 in zcong_trans)
21.21 apply auto
21.22 done
21.23
22.1 --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Jul 02 17:34:45 2014 +0200
22.2 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Jun 11 14:24:23 2014 +1000
22.3 @@ -239,7 +239,7 @@
22.4 ultimately
22.5 have "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} =
22.6 {(Some i, zs), (Some i, map Not zs)}"
22.7 - using `i < n`
22.8 + using `i < n` [[ hypsubst_thin = true ]]
22.9 proof (safe, simp_all add:dc_crypto payer_def)
22.10 fix b assume [simp]: "length b = n"
22.11 and *: "inversion (Some i, b) = xs" and "b \<noteq> zs"
23.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Jul 02 17:34:45 2014 +0200
23.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Jun 11 14:24:23 2014 +1000
23.3 @@ -57,6 +57,7 @@
23.4 using a
23.5 apply(cases x, cases y, cases z)
23.6 apply(auto simp add: times_int_raw.simps intrel.simps)
23.7 + apply(hypsubst_thin)
23.8 apply(rename_tac u v w x y z)
23.9 apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
23.10 apply(simp add: mult_ac)
23.11 @@ -69,6 +70,7 @@
23.12 using a
23.13 apply(cases x, cases y, cases z)
23.14 apply(auto simp add: times_int_raw.simps intrel.simps)
23.15 + apply(hypsubst_thin)
23.16 apply(rename_tac u v w x y z)
23.17 apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
23.18 apply(simp add: mult_ac)
24.1 --- a/src/HOL/SET_Protocol/Purchase.thy Wed Jul 02 17:34:45 2014 +0200
24.2 +++ b/src/HOL/SET_Protocol/Purchase.thy Wed Jun 11 14:24:23 2014 +1000
24.3 @@ -1119,6 +1119,7 @@
24.4 OIData, Hash PIData|}
24.5 \<in> set evs"
24.6 apply clarify
24.7 +apply hypsubst_thin
24.8 apply (erule rev_mp)
24.9 apply (erule rev_mp)
24.10 apply (erule set_pur.induct, simp_all, auto)
25.1 --- a/src/HOL/Transcendental.thy Wed Jul 02 17:34:45 2014 +0200
25.2 +++ b/src/HOL/Transcendental.thy Wed Jun 11 14:24:23 2014 +1000
25.3 @@ -3046,6 +3046,7 @@
25.4
25.5 lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
25.6 apply (cut_tac y = y in lemma_tan_total1, auto)
25.7 + apply hypsubst_thin
25.8 apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
25.9 apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
25.10 apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
26.1 --- a/src/HOL/UNITY/Comp/Priority.thy Wed Jul 02 17:34:45 2014 +0200
26.2 +++ b/src/HOL/UNITY/Comp/Priority.thy Wed Jun 11 14:24:23 2014 +1000
26.3 @@ -209,7 +209,7 @@
26.4 leadsTo {s. above i s < x}"
26.5 apply (rule leadsTo_UN)
26.6 apply (rule single_leadsTo_I, clarify)
26.7 -apply (rule_tac x = "above i x" in above_decreases_lemma)
26.8 +apply (rule_tac x = "above i xa" in above_decreases_lemma)
26.9 apply (simp_all (no_asm_use) add: Highest_iff_above0)
26.10 apply blast+
26.11 done
27.1 --- a/src/HOL/Word/Bool_List_Representation.thy Wed Jul 02 17:34:45 2014 +0200
27.2 +++ b/src/HOL/Word/Bool_List_Representation.thy Wed Jun 11 14:24:23 2014 +1000
27.3 @@ -595,7 +595,7 @@
27.4
27.5 lemma takefill_same':
27.6 "l = length xs ==> takefill fill l xs = xs"
27.7 - by clarify (induct xs, auto)
27.8 + by (induct xs arbitrary: l, auto)
27.9
27.10 lemmas takefill_same [simp] = takefill_same' [OF refl]
27.11
28.1 --- a/src/HOL/Word/Misc_Typedef.thy Wed Jul 02 17:34:45 2014 +0200
28.2 +++ b/src/HOL/Word/Misc_Typedef.thy Wed Jun 11 14:24:23 2014 +1000
28.3 @@ -194,7 +194,7 @@
28.4 prefer 2
28.5 apply (simp add: comp_assoc)
28.6 apply (rule ext)
28.7 - apply (drule fun_cong)
28.8 + apply (drule_tac f="?a o ?b" in fun_cong)
28.9 apply simp
28.10 done
28.11
29.1 --- a/src/HOL/Word/Word.thy Wed Jul 02 17:34:45 2014 +0200
29.2 +++ b/src/HOL/Word/Word.thy Wed Jun 11 14:24:23 2014 +1000
29.3 @@ -3176,6 +3176,12 @@
29.4 of_bl_rep_False [where n=1 and bs="[]", simplified])
29.5 done
29.6
29.7 +lemma zip_replicate:
29.8 + "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
29.9 + apply (induct ys arbitrary: n, simp_all)
29.10 + apply (case_tac n, simp_all)
29.11 + done
29.12 +
29.13 lemma align_lem_or [rule_format] :
29.14 "ALL x m. length x = n + m --> length y = n + m -->
29.15 drop m x = replicate n False --> take m y = replicate m False -->
29.16 @@ -3185,9 +3191,8 @@
29.17 apply clarsimp
29.18 apply (case_tac x, force)
29.19 apply (case_tac m, auto)
29.20 - apply (drule sym)
29.21 - apply auto
29.22 - apply (induct_tac list, auto)
29.23 + apply (drule_tac t="length ?xs" in sym)
29.24 + apply (clarsimp simp: map2_def zip_replicate o_def)
29.25 done
29.26
29.27 lemma align_lem_and [rule_format] :
29.28 @@ -3199,9 +3204,8 @@
29.29 apply clarsimp
29.30 apply (case_tac x, force)
29.31 apply (case_tac m, auto)
29.32 - apply (drule sym)
29.33 - apply auto
29.34 - apply (induct_tac list, auto)
29.35 + apply (drule_tac t="length ?xs" in sym)
29.36 + apply (clarsimp simp: map2_def zip_replicate o_def map_replicate_const)
29.37 done
29.38
29.39 lemma aligned_bl_add_size [OF refl]:
29.40 @@ -3676,6 +3680,7 @@
29.41 apply safe
29.42 defer
29.43 apply (clarsimp split: prod.splits)
29.44 + apply hypsubst_thin
29.45 apply (drule word_ubin.norm_Rep [THEN ssubst])
29.46 apply (drule split_bintrunc)
29.47 apply (simp add : of_bl_def bl2bin_drop word_size
30.1 --- a/src/HOL/ZF/HOLZF.thy Wed Jul 02 17:34:45 2014 +0200
30.2 +++ b/src/HOL/ZF/HOLZF.thy Wed Jun 11 14:24:23 2014 +1000
30.3 @@ -168,7 +168,7 @@
30.4
30.5 theorem Domain: "Elem x (Domain f) = (? y. Elem (Opair x y) f)"
30.6 apply (auto simp add: Domain_def Replacement)
30.7 - apply (rule_tac x="Snd x" in exI)
30.8 + apply (rule_tac x="Snd xa" in exI)
30.9 apply (simp add: FstSnd)
30.10 apply (rule_tac x="Opair x y" in exI)
30.11 apply (simp add: isOpair Fst)
31.1 --- a/src/HOL/ex/Dedekind_Real.thy Wed Jul 02 17:34:45 2014 +0200
31.2 +++ b/src/HOL/ex/Dedekind_Real.thy Wed Jun 11 14:24:23 2014 +1000
31.3 @@ -313,7 +313,7 @@
31.4 "[|A \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u \<in> add_set A B. y < u"
31.5 apply (auto simp add: add_set_def)
31.6 apply (frule preal_exists_greater [of A], auto)
31.7 -apply (rule_tac x="u + y" in exI)
31.8 +apply (rule_tac x="u + ya" in exI)
31.9 apply (auto intro: add_strict_left_mono)
31.10 done
31.11
31.12 @@ -439,7 +439,7 @@
31.13 "[|A \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u \<in> mult_set A B. y < u"
31.14 apply (auto simp add: mult_set_def)
31.15 apply (frule preal_exists_greater [of A], auto)
31.16 -apply (rule_tac x="u * y" in exI)
31.17 +apply (rule_tac x="u * ya" in exI)
31.18 apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B]
31.19 mult_strict_right_mono)
31.20 done
31.21 @@ -1590,7 +1590,7 @@
31.22 "\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
31.23 apply (simp add: real_of_preal_def real_zero_def, cases x)
31.24 apply (auto simp add: real_minus add_ac)
31.25 -apply (cut_tac x = x and y = y in linorder_less_linear)
31.26 +apply (cut_tac x = xa and y = y in linorder_less_linear)
31.27 apply (auto dest!: less_add_left_Ex simp add: add_assoc [symmetric])
31.28 done
31.29
32.1 --- a/src/Provers/hypsubst.ML Wed Jul 02 17:34:45 2014 +0200
32.2 +++ b/src/Provers/hypsubst.ML Wed Jun 11 14:24:23 2014 +1000
32.3 @@ -47,6 +47,8 @@
32.4 signature HYPSUBST =
32.5 sig
32.6 val bound_hyp_subst_tac : Proof.context -> int -> tactic
32.7 + val hyp_subst_tac_thin : bool -> Proof.context -> int -> tactic
32.8 + val hyp_subst_thins : bool Config.T
32.9 val hyp_subst_tac : Proof.context -> int -> tactic
32.10 val blast_hyp_subst_tac : bool -> int -> tactic
32.11 val stac : thm -> int -> tactic
32.12 @@ -77,7 +79,8 @@
32.13 Not if it involves a variable free in the premises,
32.14 but we can't check for this -- hence bnd and bound_hyp_subst_tac
32.15 Prefer to eliminate Bound variables if possible.
32.16 - Result: true = use as is, false = reorient first *)
32.17 + Result: true = use as is, false = reorient first
32.18 + also returns var to substitute, relevant if it is Free *)
32.19 fun inspect_pair bnd novars (t, u) =
32.20 if novars andalso (has_tvars t orelse has_tvars u)
32.21 then raise Match (*variables in the type!*)
32.22 @@ -86,55 +89,75 @@
32.23 (Bound i, _) =>
32.24 if loose_bvar1 (u, i) orelse novars andalso has_vars u
32.25 then raise Match
32.26 - else true (*eliminates t*)
32.27 + else (true, Bound i) (*eliminates t*)
32.28 | (_, Bound i) =>
32.29 if loose_bvar1 (t, i) orelse novars andalso has_vars t
32.30 then raise Match
32.31 - else false (*eliminates u*)
32.32 + else (false, Bound i) (*eliminates u*)
32.33 | (t' as Free _, _) =>
32.34 if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u
32.35 then raise Match
32.36 - else true (*eliminates t*)
32.37 + else (true, t') (*eliminates t*)
32.38 | (_, u' as Free _) =>
32.39 if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t
32.40 then raise Match
32.41 - else false (*eliminates u*)
32.42 + else (false, u') (*eliminates u*)
32.43 | _ => raise Match);
32.44
32.45 (*Locates a substitutable variable on the left (resp. right) of an equality
32.46 assumption. Returns the number of intervening assumptions. *)
32.47 -fun eq_var bnd novars =
32.48 - let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
32.49 - | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) =
32.50 - ((k, inspect_pair bnd novars
32.51 - (Data.dest_eq (Data.dest_Trueprop A)))
32.52 - handle TERM _ => eq_var_aux (k+1) B
32.53 - | Match => eq_var_aux (k+1) B)
32.54 - | eq_var_aux k _ = raise EQ_VAR
32.55 - in eq_var_aux 0 end;
32.56 +fun eq_var bnd novars check_frees t =
32.57 + let
32.58 + fun check_free ts (orient, Free f)
32.59 + = if not check_frees orelse not orient
32.60 + orelse exists (curry Logic.occs (Free f)) ts
32.61 + then (orient, true) else raise Match
32.62 + | check_free ts (orient, _) = (orient, false)
32.63 + fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) hs = eq_var_aux k t hs
32.64 + | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) hs =
32.65 + ((k, check_free (B :: hs) (inspect_pair bnd novars
32.66 + (Data.dest_eq (Data.dest_Trueprop A))))
32.67 + handle TERM _ => eq_var_aux (k+1) B (A :: hs)
32.68 + | Match => eq_var_aux (k+1) B (A :: hs))
32.69 + | eq_var_aux k _ _ = raise EQ_VAR
32.70 +
32.71 + in eq_var_aux 0 t [] end;
32.72 +
32.73 +val thin_free_eq_tac = SUBGOAL (fn (t, i) => let
32.74 + val (k, _) = eq_var false false false t
32.75 + val ok = (eq_var false false true t |> fst) > k
32.76 + handle EQ_VAR => true
32.77 + in if ok then EVERY [rotate_tac k i, etac thin_rl i, rotate_tac (~k) i]
32.78 + else no_tac
32.79 + end handle EQ_VAR => no_tac)
32.80
32.81 (*For the simpset. Adds ALL suitable equalities, even if not first!
32.82 No vars are allowed here, as simpsets are built from meta-assumptions*)
32.83 fun mk_eqs bnd th =
32.84 - [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th)))
32.85 + [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th))) |> fst
32.86 then th RS Data.eq_reflection
32.87 else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
32.88 handle TERM _ => [] | Match => [];
32.89
32.90 +fun bool2s true = "true" | bool2s false = "false"
32.91 +
32.92 local
32.93 in
32.94
32.95 (*Select a suitable equality assumption; substitute throughout the subgoal
32.96 If bnd is true, then it replaces Bound variables only. *)
32.97 fun gen_hyp_subst_tac ctxt bnd =
32.98 - let fun tac i st = SUBGOAL (fn (Bi, _) =>
32.99 + SUBGOAL (fn (Bi, i) =>
32.100 let
32.101 - val (k, _) = eq_var bnd true Bi
32.102 + val (k, (orient, is_free)) = eq_var bnd true true Bi
32.103 val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
32.104 in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
32.105 - etac thin_rl i, rotate_tac (~k) i]
32.106 - end handle THM _ => no_tac | EQ_VAR => no_tac) i st
32.107 - in REPEAT_DETERM1 o tac end;
32.108 + if not is_free then etac thin_rl i
32.109 + else if orient then etac Data.rev_mp i
32.110 + else etac (Data.sym RS Data.rev_mp) i,
32.111 + rotate_tac (~k) i,
32.112 + if is_free then rtac Data.imp_intr i else all_tac]
32.113 + end handle THM _ => no_tac | EQ_VAR => no_tac)
32.114
32.115 end;
32.116
32.117 @@ -174,6 +197,9 @@
32.118
32.119 val imp_intr_tac = rtac Data.imp_intr;
32.120
32.121 +fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
32.122 +val dup_subst = rev_dup_elim ssubst
32.123 +
32.124 (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
32.125 (* premises containing meta-implications or quantifiers *)
32.126
32.127 @@ -181,26 +207,37 @@
32.128 to handle equalities containing Vars.*)
32.129 fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
32.130 let val n = length(Logic.strip_assums_hyp Bi) - 1
32.131 - val (k,symopt) = eq_var bnd false Bi
32.132 + val (k, (orient, is_free)) = eq_var bnd false true Bi
32.133 + val rl = if is_free then dup_subst else ssubst
32.134 + val rl = if orient then rl else Data.sym RS rl
32.135 in
32.136 DETERM
32.137 (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
32.138 rotate_tac 1 i,
32.139 REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
32.140 - inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
32.141 + inst_subst_tac orient rl i,
32.142 REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
32.143 end
32.144 handle THM _ => no_tac | EQ_VAR => no_tac);
32.145
32.146 -(*Substitutes for Free or Bound variables*)
32.147 -fun hyp_subst_tac ctxt =
32.148 - FIRST' [ematch_tac [Data.thin_refl],
32.149 - gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false];
32.150 +(*Substitutes for Free or Bound variables,
32.151 + discarding equalities on Bound variables
32.152 + and on Free variables if thin=true*)
32.153 +fun hyp_subst_tac_thin thin ctxt =
32.154 + REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
32.155 + gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
32.156 + if thin then thin_free_eq_tac else K no_tac];
32.157 +
32.158 +val (hyp_subst_thins, hyp_subst_thins_setup) = Attrib.config_bool
32.159 + @{binding hypsubst_thin} (K false);
32.160 +
32.161 +fun hyp_subst_tac ctxt = hyp_subst_tac_thin
32.162 + (Config.get ctxt hyp_subst_thins) ctxt
32.163
32.164 (*Substitutes for Bound variables only -- this is always safe*)
32.165 fun bound_hyp_subst_tac ctxt =
32.166 - gen_hyp_subst_tac ctxt true ORELSE' vars_gen_hyp_subst_tac true;
32.167 -
32.168 + REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
32.169 + ORELSE' vars_gen_hyp_subst_tac true);
32.170
32.171 (** Version for Blast_tac. Hyps that are affected by the substitution are
32.172 moved to the front. Defect: even trivial changes are noticed, such as
32.173 @@ -236,7 +273,7 @@
32.174
32.175
32.176 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
32.177 - let val (k,symopt) = eq_var false false Bi
32.178 + let val (k, (symopt, _)) = eq_var false false false Bi
32.179 val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
32.180 (*omit selected equality, returning other hyps*)
32.181 val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
32.182 @@ -252,7 +289,6 @@
32.183 end
32.184 handle THM _ => no_tac | EQ_VAR => no_tac);
32.185
32.186 -
32.187 (*apply an equality or definition ONCE;
32.188 fails unless the substitution has an effect*)
32.189 fun stac th =
32.190 @@ -266,6 +302,11 @@
32.191 Method.setup @{binding hypsubst}
32.192 (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
32.193 "substitution using an assumption (improper)" #>
32.194 + Method.setup @{binding hypsubst_thin}
32.195 + (Scan.succeed (fn ctxt => SIMPLE_METHOD'
32.196 + (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
32.197 + "substitution using an assumption, eliminating assumptions" #>
32.198 + hyp_subst_thins_setup #>
32.199 Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
32.200 "simple substitution";
32.201
33.1 --- a/src/ZF/Coind/ECR.thy Wed Jul 02 17:34:45 2014 +0200
33.2 +++ b/src/ZF/Coind/ECR.thy Wed Jun 11 14:24:23 2014 +1000
33.3 @@ -100,6 +100,7 @@
33.4 <cl,t> \<in> HasTyRel"
33.5 apply (unfold hastyenv_def)
33.6 apply (erule elab_fixE, safe)
33.7 +apply hypsubst_thin
33.8 apply (rule subst, assumption)
33.9 apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI)
33.10 apply simp_all
34.1 --- a/src/ZF/Induct/Multiset.thy Wed Jul 02 17:34:45 2014 +0200
34.2 +++ b/src/ZF/Induct/Multiset.thy Wed Jun 11 14:24:23 2014 +1000
34.3 @@ -931,6 +931,7 @@
34.4 apply (rule_tac x = M0 in exI, force)
34.5 (* Subgoal 2 *)
34.6 apply clarify
34.7 +apply hypsubst_thin
34.8 apply (case_tac "a \<in> mset_of (Ka) ")
34.9 apply (rule_tac x = I in exI, simp (no_asm_simp))
34.10 apply (rule_tac x = J in exI, simp (no_asm_simp))
35.1 --- a/src/ZF/Int_ZF.thy Wed Jul 02 17:34:45 2014 +0200
35.2 +++ b/src/ZF/Int_ZF.thy Wed Jun 11 14:24:23 2014 +1000
35.3 @@ -661,7 +661,7 @@
35.4 apply (simp add: zless_def znegative_def zdiff_def int_def)
35.5 apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def)
35.6 apply (rule_tac x = k in bexI)
35.7 -apply (erule add_left_cancel, auto)
35.8 +apply (erule_tac i="succ (?v)" in add_left_cancel, auto)
35.9 done
35.10
35.11 lemma zless_imp_succ_zadd:
35.12 @@ -703,6 +703,7 @@
35.13 apply (rule_tac x = "y1#+y2" in exI)
35.14 apply (auto simp add: add_lt_mono)
35.15 apply (rule sym)
35.16 +apply hypsubst_thin
35.17 apply (erule add_left_cancel)+
35.18 apply auto
35.19 done
36.1 --- a/src/ZF/ex/LList.thy Wed Jul 02 17:34:45 2014 +0200
36.2 +++ b/src/ZF/ex/LList.thy Wed Jun 11 14:24:23 2014 +1000
36.3 @@ -173,7 +173,7 @@
36.4 apply (rule_tac X = "{<l,l>. l \<in> llist (A) }" in lleq.coinduct)
36.5 apply blast
36.6 apply safe
36.7 -apply (erule_tac a=l in llist.cases, fast+)
36.8 +apply (erule_tac a=la in llist.cases, fast+)
36.9 done
36.10
36.11
37.1 --- a/src/ZF/ex/Primes.thy Wed Jul 02 17:34:45 2014 +0200
37.2 +++ b/src/ZF/ex/Primes.thy Wed Jun 11 14:24:23 2014 +1000
37.3 @@ -71,7 +71,7 @@
37.4
37.5 lemma dvd_mult_right: "[|(i#*j) dvd k; j \<in> nat|] ==> j dvd k"
37.6 apply (simp add: divides_def, clarify)
37.7 -apply (rule_tac x = "i#*k" in bexI)
37.8 +apply (rule_tac x = "i#*ka" in bexI)
37.9 apply (simp add: mult_ac)
37.10 apply (rule mult_type)
37.11 done