# HG changeset patch
# User paulson
# Date 865246513 -7200
# Node ID f59e64fe4058b16820e8430b3cc0834a7f7f878a
# Parent  5ef99c94e1fbef0ed140eb443d07faf0416ddcc8
New statement and proof of free_tv_subst_var in order to cope with new
rewrite rules Un_insert_left, Un_insert_right

diff -r 5ef99c94e1fb -r f59e64fe4058 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Mon Jun 02 12:14:15 1997 +0200
+++ b/src/HOL/MiniML/Type.ML	Mon Jun 02 12:15:13 1997 +0200
@@ -253,17 +253,17 @@
 
 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";
 
 goalw thy [dom_def,cod_def,UNION_def,Bex_def]
@@ -277,27 +277,26 @@
 Addsimps [cod_app_subst];
 
 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]) );
+     "free_tv (S (v::nat)) <= insert v (cod S)";
+by (expand_case_tac "v:dom S" 1);
+by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1);
 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 (sch::type_scheme)) <= cod S Un free_tv sch";
-by ( type_scheme.induct_tac "sch" 1);
+by (type_scheme.induct_tac "sch" 1);
 (* case FVar n *)
-by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
+by (simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
 (* case BVar n *)
 by (Simp_tac 1);
 (* case Fun t1 t2 *)
@@ -306,12 +305,12 @@
 
 goal thy 
      "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
-by ( list.induct_tac "A" 1);
+by (list.induct_tac "A" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
-by ( cut_facts_tac [free_tv_app_subst_type_scheme] 1);
-by ( fast_tac (set_cs addss !simpset) 1);
+by (cut_facts_tac [free_tv_app_subst_type_scheme] 1);
+by (fast_tac (set_cs addss !simpset) 1);
 qed "free_tv_app_subst_scheme_list";
 
 goalw thy [free_tv_subst,dom_def]
@@ -396,22 +395,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 
@@ -501,7 +500,7 @@
 
 goal thy
   "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
-by ( simp_tac (!simpset addsimps [new_tv_list]) 1);
+by (simp_tac (!simpset addsimps [new_tv_list]) 1);
 by (list.induct_tac "A" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "new_tv_Suc_list";
@@ -646,7 +645,7 @@
 goalw thy [new_tv_def] 
       "!! n. [|mgu t1 t2 = Some 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";
 
 
diff -r 5ef99c94e1fb -r f59e64fe4058 src/HOL/W0/Type.ML
--- a/src/HOL/W0/Type.ML	Mon Jun 02 12:14:15 1997 +0200
+++ b/src/HOL/W0/Type.ML	Mon Jun 02 12:15:13 1997 +0200
@@ -319,12 +319,11 @@
 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]) );
+goal thy
+     "free_tv (s (v::nat)) <= insert v (cod s)";
+by (expand_case_tac "v:dom s" 1);
+by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1);
 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