# HG changeset patch
# User nipkow
# Date 853516739 -3600
# Node ID aecaa76e7eff596c20f416e130f947b41c64c647
# Parent  761e3094e32f06e243d07499b0c33bad6f3a3867
Incorporated Larry's changes.

diff -r 761e3094e32f -r aecaa76e7eff src/HOL/W0/I.ML
--- a/src/HOL/W0/I.ML	Fri Jan 17 16:17:31 1997 +0100
+++ b/src/HOL/W0/I.ML	Fri Jan 17 16:58:59 1997 +0100
@@ -1,3 +1,11 @@
+(* Title:     HOL/W0/I.ML
+   ID:        $Id$
+   Author:    Thomas Stauner
+   Copyright  1995 TU Muenchen
+
+Equivalence of W and I.
+*)
+
 open I;
 
 goal thy
diff -r 761e3094e32f -r aecaa76e7eff src/HOL/W0/I.thy
--- a/src/HOL/W0/I.thy	Fri Jan 17 16:17:31 1997 +0100
+++ b/src/HOL/W0/I.thy	Fri Jan 17 16:58:59 1997 +0100
@@ -1,8 +1,9 @@
-(*   Title:         MiniML.thy
-     Author:        Thomas Stauner
-     Copyright      1995 TU Muenchen
+(* Title:     HOL/W0/I.thy
+   ID:        $Id$
+   Author:    Thomas Stauner
+   Copyright  1995 TU Muenchen
 
-     Recursive definition of type inference algorithm I for Mini_ML.
+   Recursive definition of type inference algorithm I for Mini_ML.
 *)
 
 I = W +
diff -r 761e3094e32f -r aecaa76e7eff src/HOL/W0/Maybe.ML
--- a/src/HOL/W0/Maybe.ML	Fri Jan 17 16:17:31 1997 +0100
+++ b/src/HOL/W0/Maybe.ML	Fri Jan 17 16:58:59 1997 +0100
@@ -1,4 +1,9 @@
-open Maybe;
+(* Title:     HOL/W0/Maybe.ML
+   ID:        $Id$
+   Author:    Dieter Nazareth and Tobias Nipkow
+   Copyright  1995 TU Muenchen
+*)
+
 
 (* constructor laws for bind *)
 goalw thy [bind_def] "(Ok s) bind f = (f s)";
diff -r 761e3094e32f -r aecaa76e7eff src/HOL/W0/Maybe.thy
--- a/src/HOL/W0/Maybe.thy	Fri Jan 17 16:17:31 1997 +0100
+++ b/src/HOL/W0/Maybe.thy	Fri Jan 17 16:58:59 1997 +0100
@@ -1,4 +1,4 @@
-(* Title:     HOL/MiniML/Maybe.thy
+(* Title:     HOL/W0/Maybe.thy
    ID:        $Id$
    Author:    Dieter Nazareth and Tobias Nipkow
    Copyright  1995 TU Muenchen
diff -r 761e3094e32f -r aecaa76e7eff src/HOL/W0/MiniML.ML
--- a/src/HOL/W0/MiniML.ML	Fri Jan 17 16:17:31 1997 +0100
+++ b/src/HOL/W0/MiniML.ML	Fri Jan 17 16:58:59 1997 +0100
@@ -1,4 +1,4 @@
-(* Title:     HOL/MiniML/MiniML.ML
+(* Title:     HOL/W0/MiniML.ML
    ID:        $Id$
    Author:    Dieter Nazareth and Tobias Nipkow
    Copyright  1995 TU Muenchen
diff -r 761e3094e32f -r aecaa76e7eff src/HOL/W0/MiniML.thy
--- a/src/HOL/W0/MiniML.thy	Fri Jan 17 16:17:31 1997 +0100
+++ b/src/HOL/W0/MiniML.thy	Fri Jan 17 16:58:59 1997 +0100
@@ -1,4 +1,4 @@
-(* Title:     HOL/MiniML/MiniML.thy
+(* Title:     HOL/W0/MiniML.thy
    ID:        $Id$
    Author:    Dieter Nazareth and Tobias Nipkow
    Copyright  1995 TU Muenchen
diff -r 761e3094e32f -r aecaa76e7eff src/HOL/W0/ROOT.ML
--- a/src/HOL/W0/ROOT.ML	Fri Jan 17 16:17:31 1997 +0100
+++ b/src/HOL/W0/ROOT.ML	Fri Jan 17 16:58:59 1997 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MiniML/ROOT.ML
+(*  Title:      HOL/W0/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1995 TUM
diff -r 761e3094e32f -r aecaa76e7eff src/HOL/W0/Type.ML
--- a/src/HOL/W0/Type.ML	Fri Jan 17 16:17:31 1997 +0100
+++ b/src/HOL/W0/Type.ML	Fri Jan 17 16:58:59 1997 +0100
@@ -1,4 +1,8 @@
-open Type;
+(* Title:     HOL/W0/Type.ML
+   ID:        $Id$
+   Author:    Dieter Nazareth and Tobias Nipkow
+   Copyright  1995 TU Muenchen
+*)
 
 Addsimps [mgu_eq,mgu_mg,mgu_free];
 
@@ -6,7 +10,7 @@
 goalw thy [new_tv_def] 
       "!! n. [|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
 \            new_tv n u";
-by ( fast_tac (set_cs addDs [mgu_free]) 1);
+by (fast_tac (set_cs addDs [mgu_free]) 1);
 qed "mgu_new";
 
 (* application of id_subst does not change type expression *)
@@ -124,22 +128,22 @@
 goalw thy [new_tv_def]
   "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \
 \                (! l. l < n --> new_tv n (s l) ))";
-by ( safe_tac HOL_cs );
+by (safe_tac HOL_cs );
 (* ==> *)
-by ( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
-by ( subgoal_tac "m:cod s | s l = TVar l" 1);
-by ( safe_tac HOL_cs );
+by (fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
+by (subgoal_tac "m:cod s | s l = TVar l" 1);
+by (safe_tac HOL_cs );
 by (fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1);
 by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
 by (Asm_full_simp_tac 1);
 by (fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1);
 (* <== *)
-by ( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
-by ( safe_tac set_cs );
-by ( cut_inst_tac [("m","m"),("n","n")] less_linear 1);
-by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
-by ( cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
-by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
+by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
+by (safe_tac set_cs );
+by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
+by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
+by (cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
+by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
 qed "new_tv_subst";
 
 goal thy 
@@ -169,7 +173,7 @@
   "n<=m --> new_tv n (t::typ) --> new_tv m t";
 by (typ.induct_tac "t" 1);
 (* case TVar n *)
-by ( fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1);
+by (fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1);
 (* case Fun t1 t2 *)
 by (Asm_simp_tac 1);
 qed_spec_mp "new_tv_le";
@@ -177,7 +181,7 @@
 
 goal thy 
   "n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
-by ( list.induct_tac "ts" 1);
+by (list.induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
@@ -212,7 +216,7 @@
 
 goal thy
   "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
-by ( simp_tac (!simpset addsimps [new_tv_list]) 1);
+by (simp_tac (!simpset addsimps [new_tv_list]) 1);
 by (list.induct_tac "ts" 1);
 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
 qed_spec_mp "new_tv_subst_tel";
@@ -221,7 +225,7 @@
 (* auxilliary lemma *)
 goal thy
   "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
-by ( simp_tac (!simpset addsimps [new_tv_list]) 1);
+by (simp_tac (!simpset addsimps [new_tv_list]) 1);
 by (list.induct_tac "ts" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "new_tv_Suc_list";
@@ -302,51 +306,51 @@
 (* some useful theorems *)
 goalw thy [free_tv_subst] 
       "!!v. v : cod s ==> v : free_tv s";
-by ( fast_tac set_cs 1);
+by (fast_tac set_cs 1);
 qed "codD";
  
 goalw thy [free_tv_subst,dom_def] 
       "!! x. x ~: free_tv s ==> s x = TVar x";
-by ( fast_tac set_cs 1);
+by (fast_tac set_cs 1);
 qed "not_free_impl_id";
 
 goalw thy [new_tv_def] 
       "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
-by ( fast_tac HOL_cs 1 );
+by (fast_tac HOL_cs 1 );
 qed "free_tv_le_new_tv";
 
 goal thy 
      "free_tv (s (v::nat)) <= cod s Un {v}";
-by ( cut_inst_tac [("P","v:dom s")] excluded_middle 1);
-by ( safe_tac (HOL_cs addSIs [subsetI]) );
+by (cut_inst_tac [("P","v:dom s")] excluded_middle 1);
+by (safe_tac (HOL_cs addSIs [subsetI]) );
 by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1);
 by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1);
 qed "free_tv_subst_var";
 
 goal thy 
      "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
-by ( typ.induct_tac "t" 1);
+by (typ.induct_tac "t" 1);
 (* case TVar n *)
-by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
+by (simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
 (* case Fun t1 t2 *)
-by ( fast_tac (set_cs addss !simpset) 1);
+by (fast_tac (set_cs addss !simpset) 1);
 qed "free_tv_app_subst_te";     
 
 goal thy 
      "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
-by ( list.induct_tac "ts" 1);
+by (list.induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
-by ( cut_facts_tac [free_tv_app_subst_te] 1);
-by ( fast_tac (set_cs addss !simpset) 1);
+by (cut_facts_tac [free_tv_app_subst_te] 1);
+by (fast_tac (set_cs addss !simpset) 1);
 qed "free_tv_app_subst_tel";
 
 goalw thy [free_tv_subst,dom_def]
      "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=   \
 \     free_tv s1 Un free_tv s2";
-by ( fast_tac (set_cs addSDs [free_tv_app_subst_te RS
-subsetD,free_tv_subst_var RS subsetD] addss (
-!simpset addsimps [cod_def,dom_def])) 1);
+by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,
+			     free_tv_subst_var RS subsetD] 
+	             addss (!simpset delsimps bex_simps
+				     addsimps [cod_def,dom_def])) 1);
 qed "free_tv_comp_subst";
-
diff -r 761e3094e32f -r aecaa76e7eff src/HOL/W0/Type.thy
--- a/src/HOL/W0/Type.thy	Fri Jan 17 16:17:31 1997 +0100
+++ b/src/HOL/W0/Type.thy	Fri Jan 17 16:58:59 1997 +0100
@@ -1,4 +1,4 @@
-(* Title:     HOL/MiniML/Type.thy
+(* Title:     HOL/W0/Type.thy
    ID:        $Id$
    Author:    Dieter Nazareth and Tobias Nipkow
    Copyright  1995 TU Muenchen
diff -r 761e3094e32f -r aecaa76e7eff src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Fri Jan 17 16:17:31 1997 +0100
+++ b/src/HOL/W0/W.ML	Fri Jan 17 16:58:59 1997 +0100
@@ -1,4 +1,4 @@
-(* Title:     HOL/MiniML/W.ML
+(* Title:     HOL/W0/W.ML
    ID:        $Id$
    Author:    Dieter Nazareth and Tobias Nipkow
    Copyright  1995 TU Muenchen
@@ -6,8 +6,6 @@
 Correctness and completeness of type inference algorithm W
 *)
 
-open W;
-
 Addsimps [Suc_le_lessD];
 Delsimps (ex_simps @ all_simps);
 
@@ -176,9 +174,10 @@
 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 addIs [cod_app_subst]
+by (fast_tac (HOL_cs addSEs [allE]
+	             addIs [cod_app_subst]
                      addss (!simpset addsimps [less_Suc_eq])) 1);
-
+(** LEVEL 12 **)
 (* case App e1 e2 *)
 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
 by (strip_tac 1); 
@@ -190,6 +189,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 **)
 (* second case *)
 by (eres_inst_tac [("x","$ s a")] allE 1);
 by (eres_inst_tac [("x","sa")] allE 1);
@@ -201,6 +201,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 **)
 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]
@@ -211,10 +212,11 @@
 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,
-    less_le_trans,subsetD]
-  addEs [UnE]
-  addss !simpset) 1); 
+			    free_tv_app_subst_te RS subsetD,
+			    free_tv_app_subst_tel RS subsetD,
+			    less_le_trans,subsetD]
+	             addSEs [UnE]
+		     addss !simpset) 1); 
 qed_spec_mp "free_tv_W";