Hypsubst preserves equality hypotheses
authorThomas Sewell <thomas.sewell@nicta.com.au>
Wed Jun 11 14:24:23 2014 +1000 (2014-06-11)
changeset 5749274bf65a1910a
parent 57491 9eedaafc05c8
child 57495 b627e76cc5cc
Hypsubst preserves equality hypotheses

Fixes included for various theories affected by this change.
src/HOL/Algebra/Divisibility.thy
src/HOL/Auth/ZhouGollmann.thy
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/Conform.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Divides.thy
src/HOL/HOLCF/Library/Stream.thy
src/HOL/Hoare_Parallel/OG_Examples.thy
src/HOL/IMP/Abs_Int2.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy
src/HOL/Library/Float.thy
src/HOL/Library/Multiset.thy
src/HOL/MacLaurin.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/Nat.thy
src/HOL/Nominal/Examples/Class1.thy
src/HOL/Nominal/Examples/Class2.thy
src/HOL/Old_Number_Theory/Chinese.thy
src/HOL/Old_Number_Theory/Euler.thy
src/HOL/Old_Number_Theory/Gauss.thy
src/HOL/Probability/ex/Dining_Cryptographers.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/SET_Protocol/Purchase.thy
src/HOL/Transcendental.thy
src/HOL/UNITY/Comp/Priority.thy
src/HOL/Word/Bool_List_Representation.thy
src/HOL/Word/Misc_Typedef.thy
src/HOL/Word/Word.thy
src/HOL/ZF/HOLZF.thy
src/HOL/ex/Dedekind_Real.thy
src/Provers/hypsubst.ML
src/ZF/Coind/ECR.thy
src/ZF/Induct/Multiset.thy
src/ZF/Int_ZF.thy
src/ZF/ex/LList.thy
src/ZF/ex/Primes.thy
     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