Ran expandshort; used stac instead of ssubst
authorpaulson
Thu Sep 26 16:12:25 1996 +0200 (1996-09-26)
changeset 2035e329b36d9136
parent 2034 5079fdf938dd
child 2036 62ff902eeffc
Ran expandshort; used stac instead of ssubst
src/CCL/Fix.ML
src/CCL/Gfp.ML
src/CCL/Term.ML
src/CCL/Trancl.ML
src/CCL/Type.ML
src/CCL/coinduction.ML
src/CCL/ex/Stream.ML
src/CCL/genrec.ML
src/CCL/subset.ML
     1.1 --- a/src/CCL/Fix.ML	Thu Sep 26 15:49:54 1996 +0200
     1.2 +++ b/src/CCL/Fix.ML	Thu Sep 26 16:12:25 1996 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  by (etac contrapos 1);
     1.5  by (rtac po_trans 1);
     1.6  by (assume_tac 2);
     1.7 -by (rtac (napplyBzero RS ssubst) 1);
     1.8 +by (stac napplyBzero 1);
     1.9  by (rtac po_cong 1 THEN rtac po_bot 1);
    1.10  qed "npo_INCL";
    1.11  
    1.12 @@ -117,8 +117,8 @@
    1.13  
    1.14  val [p1,p2,p3] = goal CCL.thy
    1.15      "[| ALL x.t ` x [= u ` x;  EX f.t=lam x.f(x);  EX f.u=lam x.f(x) |] ==> t [= u";
    1.16 -by (rtac (p2 RS cond_eta RS ssubst) 1);
    1.17 -by (rtac (p3 RS cond_eta RS ssubst) 1);
    1.18 +by (stac (p2 RS cond_eta) 1);
    1.19 +by (stac (p3 RS cond_eta) 1);
    1.20  by (rtac (p1 RS (po_lam RS iffD2)) 1);
    1.21  qed "po_eta";
    1.22  
    1.23 @@ -184,7 +184,7 @@
    1.24  by (rtac fix_ind 1);
    1.25  by (rewtac idgen_def);
    1.26  by (REPEAT_SOME (ares_tac [allI]));
    1.27 -by (rtac (applyBbot RS ssubst) 1);
    1.28 +by (stac applyBbot 1);
    1.29  by (resolve_tac prems 1);
    1.30  br (applyB RS ssubst )1;
    1.31  by (res_inst_tac [("t","xa")] term_case 1);
     2.1 --- a/src/CCL/Gfp.ML	Thu Sep 26 15:49:54 1996 +0200
     2.2 +++ b/src/CCL/Gfp.ML	Thu Sep 26 16:12:25 1996 +0200
     2.3 @@ -85,7 +85,7 @@
     2.4  by (rtac prem 1);
     2.5  by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1);
     2.6  by (rtac (mono RS monoD) 1);
     2.7 -by (rtac (mono RS coinduct3_mono_lemma RS lfp_Tarski RS ssubst) 1);
     2.8 +by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1);
     2.9  by (rtac Un_upper2 1);
    2.10  qed "coinduct3_lemma";
    2.11  
     3.1 --- a/src/CCL/Term.ML	Thu Sep 26 15:49:54 1996 +0200
     3.2 +++ b/src/CCL/Term.ML	Thu Sep 26 16:12:25 1996 +0200
     3.3 @@ -56,13 +56,13 @@
     3.4  val rawBs = caseBs @ [applyB,applyBbot];
     3.5  
     3.6  fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
     3.7 -           (fn _ => [rtac (letrecB RS ssubst) 1,
     3.8 +           (fn _ => [stac letrecB 1,
     3.9                       simp_tac (CCL_ss addsimps rawBs) 1]);
    3.10  fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
    3.11  
    3.12  fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
    3.13             (fn _ => [simp_tac (CCL_ss addsimps rawBs 
    3.14 -                               setloop (rtac (letrecB RS ssubst))) 1]);
    3.15 +                               setloop (stac letrecB)) 1]);
    3.16  fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
    3.17  
    3.18  val ifBtrue    = mk_beta_rl "if true then t else u = t";
     4.1 --- a/src/CCL/Trancl.ML	Thu Sep 26 15:49:54 1996 +0200
     4.2 +++ b/src/CCL/Trancl.ML	Thu Sep 26 16:12:25 1996 +0200
     4.3 @@ -86,14 +86,14 @@
     4.4  
     4.5  (*Reflexivity of rtrancl*)
     4.6  goal Trancl.thy "<a,a> : r^*";
     4.7 -by (rtac (rtrancl_unfold RS ssubst) 1);
     4.8 +by (stac rtrancl_unfold 1);
     4.9  by (fast_tac comp_cs 1);
    4.10  qed "rtrancl_refl";
    4.11  
    4.12  (*Closure under composition with r*)
    4.13  val prems = goal Trancl.thy
    4.14      "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*";
    4.15 -by (rtac (rtrancl_unfold RS ssubst) 1);
    4.16 +by (stac rtrancl_unfold 1);
    4.17  by (fast_tac (comp_cs addIs prems) 1);
    4.18  qed "rtrancl_into_rtrancl";
    4.19  
     5.1 --- a/src/CCL/Type.ML	Thu Sep 26 15:49:54 1996 +0200
     5.2 +++ b/src/CCL/Type.ML	Thu Sep 26 16:12:25 1996 +0200
     5.3 @@ -302,7 +302,7 @@
     5.4  val prems = goal Type.thy 
     5.5      "letrec g x be zero$g(x) in g(bot) : Lists(Nat)";
     5.6  by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
     5.7 -by (rtac (letrecB RS ssubst) 1);
     5.8 +by (stac letrecB 1);
     5.9  by (rewtac cons_def);
    5.10  by (fast_tac type_cs 1);
    5.11  result();
     6.1 --- a/src/CCL/coinduction.ML	Thu Sep 26 15:49:54 1996 +0200
     6.2 +++ b/src/CCL/coinduction.ML	Thu Sep 26 16:12:25 1996 +0200
     6.3 @@ -7,7 +7,7 @@
     6.4  *)
     6.5  
     6.6  val [mono,prem] = goal Lfp.thy "[| mono(f);  a : f(lfp(f)) |] ==> a : lfp(f)";
     6.7 -by (rtac ((mono RS lfp_Tarski) RS ssubst) 1);
     6.8 +by (stac (mono RS lfp_Tarski) 1);
     6.9  by (rtac prem 1);
    6.10  qed "lfpI";
    6.11  
     7.1 --- a/src/CCL/ex/Stream.ML	Thu Sep 26 15:49:54 1996 +0200
     7.2 +++ b/src/CCL/ex/Stream.ML	Thu Sep 26 16:12:25 1996 +0200
     7.3 @@ -108,7 +108,7 @@
     7.4  by (fast_tac (type_cs addSIs [napplyBzero RS sym,
     7.5                                napplyBzero RS sym RS arg_cong]) 1);
     7.6  by (EQgen_tac list_ss [iter1B,iter2Blemma] 1);
     7.7 -by (rtac (napply_f RS ssubst) 1 THEN atac 1);
     7.8 +by (stac napply_f 1 THEN atac 1);
     7.9  by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1);
    7.10  by (fast_tac type_cs 1);
    7.11  qed "iter1_iter2_eq";
     8.1 --- a/src/CCL/genrec.ML	Thu Sep 26 15:49:54 1996 +0200
     8.2 +++ b/src/CCL/genrec.ML	Thu Sep 26 16:12:25 1996 +0200
     8.3 @@ -14,7 +14,7 @@
     8.4  \    letrec g x be h(x,g) in g(a) : D(a)";
     8.5  by (rtac (major RS rev_mp) 1);
     8.6  by (rtac (wf_wf RS wfd_induct) 1);
     8.7 -by (rtac (letrecB RS ssubst) 1);
     8.8 +by (stac letrecB 1);
     8.9  by (rtac impI 1);
    8.10  by (eresolve_tac prems 1);
    8.11  by (rtac ballI 1);
    8.12 @@ -35,7 +35,7 @@
    8.13  \    letrec g x y be h(x,y,g) in g(a,b) : D(a,b)";
    8.14  by (rtac (SPLITB RS subst) 1);
    8.15  by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1));
    8.16 -by (rtac (SPLITB RS ssubst) 1);
    8.17 +by (stac SPLITB 1);
    8.18  by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1));
    8.19  by (rtac (SPLITB RS subst) 1);
    8.20  by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
     9.1 --- a/src/CCL/subset.ML	Thu Sep 26 15:49:54 1996 +0200
     9.2 +++ b/src/CCL/subset.ML	Thu Sep 26 16:12:25 1996 +0200
     9.3 @@ -121,4 +121,4 @@
     9.4  
     9.5  val set_ss = FOL_ss addcongs set_congs
     9.6                      delsimps (ex_simps @ all_simps)  (*NO miniscoping*)
     9.7 -		    addsimps mem_rews;
     9.8 +                    addsimps mem_rews;