# HG changeset patch
# User oheimb
# Date 906411891 -7200
# Node ID 54e313ed22baa9ef16f44a52b77e6193fbdf71f2
# Parent  654ead0ba4f7f2bed2bc73c7619adccc58b2a34b
re-added mem and list_all
improved indentation
improved addbefore and addSbefore
improved mechanism for unsafe wrappers

diff -r 654ead0ba4f7 -r 54e313ed22ba src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Mon Sep 21 23:03:11 1998 +0200
+++ b/src/HOL/W0/W.ML	Mon Sep 21 23:04:51 1998 +0200
@@ -44,7 +44,7 @@
 Goal "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
 by (induct_tac "e" 1);
 (* case Var(n) *)
-by (fast_tac (HOL_cs addss simpset()) 1);
+by (Clarsimp_tac 1);
 (* case Abs e *)
 by (simp_tac (simpset() addsplits [split_bind]) 1);
 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
@@ -87,15 +87,16 @@
 \                 new_tv m s & new_tv m t";
 by (induct_tac "e" 1);
 (* case Var n *)
-by (fast_tac (HOL_cs addDs [list_all_nth] addss (simpset() 
-        addsimps [id_subst_def,new_tv_list,new_tv_subst])) 1);
+  by (Clarsimp_tac 1);
+  by (force_tac (claset() addEs [list_ball_nth],
+		simpset() addsimps [id_subst_def,new_tv_list,new_tv_subst])1);
 (* case Abs e *)
-by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] 
+ by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] 
     addsplits [split_bind]) 1);
-by (strip_tac 1);
-by (eres_inst_tac [("x","Suc n")] allE 1);
-by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
-by (fast_tac (HOL_cs addss (simpset()
+ by (strip_tac 1);
+ by (eres_inst_tac [("x","Suc n")] allE 1);
+ by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
+ by (fast_tac (HOL_cs addss (simpset()
               addsimps [new_tv_subst,new_tv_Suc_list])) 1);
 
 (* case App e1 e2 *)
@@ -153,8 +154,8 @@
 \         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
 by (induct_tac "e" 1);
 (* case Var n *)
-by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
-    addss simpset()) 1);
+by (Clarsimp_tac 1);
+by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list])1);
 
 (* case Abs e *)
 by (asm_full_simp_tac (simpset() addsimps
@@ -167,10 +168,9 @@
 by (eres_inst_tac [("x","t")] allE 1);
 by (eres_inst_tac [("x","na")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
-by (fast_tac (HOL_cs addSEs [allE]
-                     addIs [cod_app_subst]
-                     addss (simpset() addsimps [less_Suc_eq])) 1);
-(** LEVEL 12 **)
+by (force_tac (claset() addSEs [allE] addIs [cod_app_subst],
+                     simpset() addsimps [less_Suc_eq]) 1);
+(** LEVEL 13 **)
 (* case App e1 e2 *)
 by (simp_tac (simpset() addsplits [split_bind]) 1);
 by (strip_tac 1); 
@@ -182,7 +182,7 @@
 by (eres_inst_tac [("x","na")] allE 1);
 by (eres_inst_tac [("x","na")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
-(** LEVEL 22 **)
+(** LEVEL 23 **)
 (* second case *)
 by (eres_inst_tac [("x","$ s a")] allE 1);
 by (eres_inst_tac [("x","sa")] allE 1);
@@ -194,7 +194,7 @@
 by (dtac W_var_geD 1);
 by (dtac W_var_geD 1);
 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
-(** LEVEL 32 **)
+(** LEVEL 33 **)
 by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
     codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
     less_le_trans,less_not_refl2,subsetD]