src/HOL/MiniML/W.ML

--- a/src/HOL/MiniML/W.ML	Tue Jan 30 15:19:20 1996 +0100
+++ b/src/HOL/MiniML/W.ML	Tue Jan 30 15:24:36 1996 +0100
@@ -11,7 +11,7 @@
 
 (* stronger version of Suc_leD *)
 goalw Nat.thy [le_def] 
-	"!!m. Suc m <= n ==> m < n";
+        "!!m. Suc m <= n ==> m < n";
 by (Asm_full_simp_tac 1);
 by (cut_facts_tac [less_linear] 1);
 by (fast_tac HOL_cs 1);
@@ -20,7 +20,7 @@
 
 (* correctness of W with respect to has_type *)
 goal thy
-	"!a s t m n . Ok (s,t,m) = W e a n --> ($ s a |- e :: t)";
+        "!a s t m n . Ok (s,t,m) = W e a n --> ($ s a |- e :: t)";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
@@ -46,12 +46,12 @@
 qed "W_correct";
 
 val has_type_casesE = map(has_type.mk_cases expr.simps)
-	[" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
+        [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
 
 
 (* the resulting type variable is always greater or equal than the given one *)
 goal thy
-	"!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
+        "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
 by (expr.induct_tac "e" 1);
 (* case Var(n) *)
 by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
@@ -83,7 +83,7 @@
 Addsimps [W_var_ge];
 
 goal thy
-	"!! s. Ok (s,t,m) = W e a n ==> n<=m";
+        "!! s. Ok (s,t,m) = W e a n ==> n<=m";
 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
 qed "W_var_geD";
 
@@ -101,7 +101,7 @@
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (fast_tac (HOL_cs addss (!simpset 
-	addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] 
+        addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] 
         setloop (split_tac [expand_if]))) 1);
 
 (* case Abs e *)
@@ -111,7 +111,7 @@
 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);
+              addsimps [new_tv_subst,new_tv_Suc_list])) 1);
 
 (* case App e1 e2 *)
 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
@@ -139,15 +139,15 @@
 by (fast_tac (HOL_cs addDs [W_var_geD] addIs
      [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le])
     1);
-be (sym RS mgu_new) 1;
+by (etac (sym RS mgu_new) 1);
 by (fast_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_tv_list_le,
    new_tv_subst_tel,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS 
    new_tv_subst_le,new_tv_le]) 1);
 by (fast_tac (HOL_cs addDs [W_var_geD] addIs
      [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
-	addss (!simpset)) 1);
-br (lessI RS new_tv_subst_var) 1;
-be (sym RS mgu_new) 1;
+        addss (!simpset)) 1);
+by (rtac (lessI RS new_tv_subst_var) 1);
+by (etac (sym RS mgu_new) 1);
 by (fast_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
    addDs [W_var_geD] addIs
    [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS
@@ -159,7 +159,7 @@
 
 
 goal thy
-     "!n a s t m v. W e a n = Ok (s,t,m) -->    	\
+     "!n a s t m v. W e a n = Ok (s,t,m) -->            \
 \         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
@@ -198,8 +198,8 @@
 by (eres_inst_tac [("x","v")] allE 1);
 by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
 by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
-bd W_var_geD 1;
-bd W_var_geD 1;
+by (dtac W_var_geD 1);
+by (dtac W_var_geD 1);
 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
 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,
@@ -207,8 +207,8 @@
   addEs [UnE] 
   addss !simpset) 1);
 by (Asm_full_simp_tac 1); 
-bd (sym RS W_var_geD) 1;
-bd (sym RS W_var_geD) 1;
+by (dtac (sym RS W_var_geD) 1);
+by (dtac (sym RS W_var_geD) 1);
 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
 by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
     free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
@@ -223,10 +223,10 @@
 
 (* Completeness of W w.r.t. has_type *)
 goal thy
-	"!s' a t' n. ($ s' a |- e :: t') --> new_tv n a --> 	\
-\		(? s t. (? m. W e a n = Ok (s,t,m) ) &	\
-\		 (? r. $ s' a = $ r ($ s a) &	\
-\		       t' = $ r t ) )";
+        "!s' a t' n. ($ s' a |- e :: t') --> new_tv n a -->     \
+\               (? s t. (? m. W e a n = Ok (s,t,m) ) &  \
+\                (? r. $ s' a = $ r ($ s a) &   \
+\                      t' = $ r t ) )";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (strip_tac 1);
@@ -262,14 +262,14 @@
 by (eres_inst_tac [("x","$ s a")] allE 1);
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","m")] allE 1);
-bd asm_rl 1;
-bd asm_rl 1;
-bd asm_rl 1;
+by (dtac asm_rl 1);
+by (dtac asm_rl 1);
+by (dtac asm_rl 1);
 by (Asm_full_simp_tac 1);
 by (safe_tac HOL_cs);
 by (fast_tac HOL_cs 1);
 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
-	conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
+        conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
 
 by (subgoal_tac
   "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
@@ -280,7 +280,7 @@
 \   (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
     ("s","($ ra ta) -> t'")] ssubst 2);
 by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2);
-br eq_free_eq_subst_te 2;  
+by (rtac eq_free_eq_subst_te 2);  
 by (strip_tac 2);
 by (subgoal_tac "na ~=ma" 2);
 by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
@@ -291,7 +291,7 @@
     setloop (split_tac [expand_if])) 3);
 (* na : free_tv sa *)
 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
-bd eq_subst_tel_eq_free 2;
+by (dtac eq_subst_tel_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
 by (Asm_simp_tac 2); 
 by (case_tac "na:dom sa" 2);
@@ -299,12 +299,12 @@
 by (asm_full_simp_tac (!simpset addsimps [dom_def] 
     setloop (split_tac [expand_if])) 3);
 (* na : dom sa *)
-br eq_free_eq_subst_te 2;
+by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2);
 by (subgoal_tac "nb ~= ma" 2);
 by ((forward_tac [new_tv_W] 3) THEN (atac 3));
-be conjE 3;
-bd new_tv_subst_tel 3;
+by (etac conjE 3);
+by (dtac new_tv_subst_tel 3);
 by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
 by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
     (!simpset addsimps [cod_def,free_tv_subst])) 3);
@@ -312,12 +312,12 @@
     setloop (split_tac [expand_if]))) 2);
 
 by (Simp_tac 2);  
-br eq_free_eq_subst_te 2;
+by (rtac eq_free_eq_subst_te 2);
 by (strip_tac 2 );
 by (subgoal_tac "na ~= ma" 2);
 by ((forward_tac [new_tv_W] 3) THEN (atac 3));
-be conjE 3;
-bd (sym RS W_var_geD) 3;
+by (etac conjE 3);
+by (dtac (sym RS W_var_geD) 3);
 by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);
 by (case_tac "na: free_tv t - free_tv sa" 2);
 (* case na ~: free_tv t - free_tv sa *)
@@ -325,37 +325,37 @@
 (* case na : free_tv t - free_tv sa *)
 by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
-bd eq_subst_tel_eq_free 2;
+by (dtac eq_subst_tel_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
 by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,not_disj]) 2);
 
 by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 
 by (safe_tac HOL_cs );
-bd mgu_Ok 1;
+by (dtac mgu_Ok 1);
 by( fast_tac (HOL_cs addss !simpset) 1);
 by (REPEAT (resolve_tac [exI,conjI] 1));
 by (fast_tac HOL_cs 1);
 by (fast_tac HOL_cs 1);
 by ((dtac mgu_mg 1) THEN (atac 1));
-be exE 1;
+by (etac exE 1);
 by (res_inst_tac [("x","rb")] exI 1);
-br conjI 1;
+by (rtac conjI 1);
 by (dres_inst_tac [("x","ma")] fun_cong 2);
 by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
 by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
 by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
     (2,trans)) 1);
 by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
-br eq_free_eq_subst_tel 1;
+by (rtac eq_free_eq_subst_tel 1);
 by( safe_tac HOL_cs );
 by (subgoal_tac "ma ~= na" 1);
 by ((forward_tac [new_tv_W] 2) THEN (atac 2));
-be conjE 2;
-bd new_tv_subst_tel 2;
+by (etac conjE 2);
+by (dtac new_tv_subst_tel 2);
 by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2);
 by (( forw_inst_tac [("xd","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
-be conjE 2;
-bd (free_tv_app_subst_tel RS subsetD) 2;
+by (etac conjE 2);
+by (dtac (free_tv_app_subst_tel RS subsetD) 2);
 by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD,
     new_tv_not_free_tv]) 2);
 by (case_tac "na: free_tv t - free_tv sa" 1);
@@ -363,7 +363,7 @@
 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
 (* case na : free_tv t - free_tv sa *)
 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-bd (free_tv_app_subst_tel RS subsetD) 1;
+by (dtac (free_tv_app_subst_tel RS subsetD) 1);
 by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
     eq_subst_tel_eq_free] addss ((!simpset addsimps 
     [not_disj,free_tv_subst,dom_def]))) 1);