from simplesubst to new subst
authorpaulson
Mon May 09 16:38:56 2005 +0200 (2005-05-09)
changeset 159449b00875e21f7
parent 15943 dd7b303465a2
child 15945 08e8d3fb9343
from simplesubst to new subst
src/HOL/Algebra/UnivPoly.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Induct/LList.thy
src/HOL/Lambda/WeakNorm.thy
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Mon May 09 16:02:45 2005 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Mon May 09 16:38:56 2005 +0200
     1.3 @@ -357,7 +357,7 @@
     1.4        case 0 then show ?case by (simp add: Pi_def)
     1.5      next
     1.6        case (Suc k) then show ?case
     1.7 -        by (simplesubst finsum_Suc2) (simp add: Pi_def a_comm)+
     1.8 +        by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+
     1.9      qed
    1.10    }
    1.11    note l = this
     2.1 --- a/src/HOL/Hyperreal/Integration.thy	Mon May 09 16:02:45 2005 +0200
     2.2 +++ b/src/HOL/Hyperreal/Integration.thy	Mon May 09 16:38:56 2005 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title       : Integration.thy
     2.5 +(*  ID          : $Id$
     2.6      Author      : Jacques D. Fleuriot
     2.7      Copyright   : 2000  University of Edinburgh
     2.8      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     2.9 @@ -262,12 +262,13 @@
    2.10   apply (drule partition_rhs)
    2.11   apply (drule partition_lhs, auto)
    2.12  apply (simp split: nat_diff_split)
    2.13 -apply (subst partition)
    2.14 -apply (simplesubst lemma_partition_append2, assumption+)
    2.15 -   --{*Need to substitute the last occurrence*}
    2.16 -apply (rule conjI)
    2.17 -apply (drule_tac [2] lemma_partition_append1)
    2.18 -apply (auto simp add: partition_lhs partition_rhs)
    2.19 +apply (subst partition) 
    2.20 +apply (subst (1 2) lemma_partition_append2, assumption+)
    2.21 +apply (rule conjI) 
    2.22 +apply (simp add: partition_lhs)
    2.23 +apply (drule lemma_partition_append1)
    2.24 +apply assumption; 
    2.25 +apply (simp add: partition_rhs)
    2.26  done
    2.27  
    2.28  
     3.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Mon May 09 16:02:45 2005 +0200
     3.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Mon May 09 16:38:56 2005 +0200
     3.3 @@ -1,10 +1,11 @@
     3.4 -(*  Title       : MacLaurin.thy
     3.5 +(*  ID          : $Id$
     3.6      Author      : Jacques D. Fleuriot
     3.7      Copyright   : 2001 University of Edinburgh
     3.8 -    Description : MacLaurin series
     3.9      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    3.10  *)
    3.11  
    3.12 +header{*MacLaurin Series*}
    3.13 +
    3.14  theory MacLaurin
    3.15  imports Log
    3.16  begin
    3.17 @@ -583,7 +584,7 @@
    3.18        in Maclaurin_all_le_objl)
    3.19      apply safe
    3.20      apply simp
    3.21 -    apply (simplesubst mod_Suc_eq_Suc_mod)  --{*simultaneous substitution*}
    3.22 +    apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
    3.23      apply (cut_tac m=m in mod_exhaust_less_4, safe, simp+)
    3.24      apply (rule DERIV_minus, simp+)
    3.25      apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
     4.1 --- a/src/HOL/Induct/LList.thy	Mon May 09 16:02:45 2005 +0200
     4.2 +++ b/src/HOL/Induct/LList.thy	Mon May 09 16:38:56 2005 +0200
     4.3 @@ -865,7 +865,8 @@
     4.4         in llist_equalityI)
     4.5   apply (rule rangeI)
     4.6  apply (safe)
     4.7 -apply (simplesubst iterates, simp)  --{*two redexes*}
     4.8 +apply (subst (1 2) iterates)
     4.9 +apply simp 
    4.10  done
    4.11  
    4.12  subsubsection{* Two proofs that @{text lmap} distributes over lappend *}
     5.1 --- a/src/HOL/Lambda/WeakNorm.thy	Mon May 09 16:02:45 2005 +0200
     5.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Mon May 09 16:38:56 2005 +0200
     5.3 @@ -134,7 +134,7 @@
     5.4  
     5.5  lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
     5.6    apply (induct set: NF)
     5.7 -  apply (simplesubst app_last)
     5.8 +  apply (subst app_last)
     5.9    apply (rule exI)
    5.10    apply (rule conjI)
    5.11    apply (rule rtrancl_refl)