--- 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";
-