src/HOL/MiniML/Type.ML

--- a/src/HOL/MiniML/Type.ML	Fri Dec 08 13:22:55 1995 +0100
+++ b/src/HOL/MiniML/Type.ML	Fri Dec 08 19:48:15 1995 +0100
@@ -13,18 +13,18 @@
 
 (* application of id_subst does not change type expression *)
 goalw thy [id_subst_def]
-  "$ id_subst = (%t::type_expr.t)";
+  "$ id_subst = (%t::typ.t)";
 by (rtac ext 1);
-by (type_expr.induct_tac "t" 1);
+by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_subst_id_te";
 Addsimps [app_subst_id_te];
 
 (* application of id_subst does not change list of type expressions *)
 goalw thy [app_subst_list]
-  "$ id_subst = (%l::type_expr list.l)";
+  "$ id_subst = (%ts::typ list.ts)";
 by (rtac ext 1); 
-by (list.induct_tac "l" 1);
+by (list.induct_tac "ts" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_subst_id_tel";
 Addsimps [app_subst_id_tel];
@@ -60,14 +60,14 @@
 
 (* composition of substitutions *)
 goal thy
-  "$ g ($ f t::type_expr) = $ (%x. $ g (f x) ) t";
-by (type_expr.induct_tac "t" 1);
+  "$ g ($ f t::typ) = $ (%x. $ g (f x) ) t";
+by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "subst_comp_te";
 
 goalw thy [app_subst_list]
-  "$ g ($ f l::type_expr list) = $ (%x. $ g (f x)) l";
-by (list.induct_tac "l" 1);
+  "$ g ($ f ts::typ list) = $ (%x. $ g (f x)) ts";
+by (list.induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case x#xl *)
@@ -82,7 +82,7 @@
 qed "app_subst_Nil";
 
 goalw thy [app_subst_list]
-  "$ s (x#l) = ($ s x)#($ s l)";
+  "$ s (t#ts) = ($ s t)#($ s ts)";
 by (Simp_tac 1);
 qed "app_subst_Cons";
 
@@ -95,7 +95,7 @@
 qed "new_tv_TVar";
 
 goalw thy [new_tv_def]
-  "new_tv n (Fun t1 t2) = (new_tv n t1 & new_tv n t2)";
+  "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)";
 by (fast_tac (HOL_cs addss !simpset) 1);
 qed "new_tv_Fun";
 
@@ -105,7 +105,7 @@
 qed "new_tv_Nil";
 
 goalw thy [new_tv_def]
-  "new_tv n (x#l) = (new_tv n x & new_tv n l)";
+  "new_tv n (t#ts) = (new_tv n t & new_tv n ts)";
 by (fast_tac (HOL_cs addss !simpset) 1);
 qed "new_tv_Cons";
 
@@ -142,23 +142,23 @@
 
 (* substitution affects only variables occurring freely *)
 goal thy
-  "new_tv n (t::type_expr) --> $(%x. if x=n then t' else s x) t = $s t";
-by (type_expr.induct_tac "t" 1);
+  "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
+by (typ.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "subst_te_new_tv";
 Addsimps [subst_te_new_tv];
 
 goal thy
-  "new_tv n (a::type_expr list) --> $(%x. if x=n then t else s x) a = $s a";
-by (list.induct_tac "a" 1);
+  "new_tv n (ts::typ list) --> $(%x. if x=n then t else s x) ts = $s ts";
+by (list.induct_tac "ts" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "subst_tel_new_tv";
 Addsimps [subst_tel_new_tv];
 
 (* all greater variables are also new *)
 goal thy
-  "n<=m --> new_tv n (t::type_expr) --> new_tv m t";
-by (type_expr.induct_tac "t" 1);
+  "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);
 (* case Fun t1 t2 *)
@@ -167,8 +167,8 @@
 Addsimps [lessI RS less_imp_le RS new_tv_le];
 
 goal thy 
-  "n<=m --> new_tv n (a::type_expr list) --> new_tv m a";
-by( list.induct_tac "a" 1);
+  "n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
+by( list.induct_tac "ts" 1);
 (* case [] *)
 by(Simp_tac 1);
 (* case a#al *)
@@ -195,25 +195,25 @@
 qed "new_tv_subst_var";
 
 goal thy
-  "new_tv n s --> new_tv n (t::type_expr) --> new_tv n ($ s t)";
-by (type_expr.induct_tac "t" 1);
+  "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
+by (typ.induct_tac "t" 1);
 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
 bind_thm ("new_tv_subst_te",result() RS mp RS mp);
 Addsimps [new_tv_subst_te];
 
-goal thy 
-  "new_tv n s --> new_tv n (a::type_expr list) --> new_tv n ($ s a)";
+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 (list.induct_tac "a" 1);
+by (list.induct_tac "ts" 1);
 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
 bind_thm ("new_tv_subst_tel",result() RS mp RS mp);
 Addsimps [new_tv_subst_tel];
 
 (* auxilliary lemma *)
 goal thy
-  "new_tv n a --> new_tv (Suc n) ((TVar n)#a)";
+  "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
 by( simp_tac (!simpset addsimps [new_tv_list]) 1);
-by (list.induct_tac "a" 1);
+by (list.induct_tac "ts" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "new_tv_Suc_list";
 
@@ -241,8 +241,8 @@
 Addsimps [new_tv_not_free_tv];
 
 goal thy
-  "(t::type_expr) mem l --> free_tv t <= free_tv l";
-by (list.induct_tac "l" 1);
+  "(t::typ) mem ts --> free_tv t <= free_tv ts";
+by (list.induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case x#xl *)
@@ -255,8 +255,8 @@
    structure the substitutions coincide on the free type variables
    occurring in the type structure *)
 goal thy
-  "$ s1 (t::type_expr) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
-by (type_expr.induct_tac "t" 1);
+  "$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
+by (typ.induct_tac "t" 1);
 (* case TVar n *)
 by (fast_tac (HOL_cs addss !simpset) 1);
 (* case Fun t1 t2 *)
@@ -264,8 +264,8 @@
 bind_thm ("eq_subst_te_eq_free",result() RS mp RS mp);
 
 goal thy
-  "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::type_expr) = $ s2 t";
-by (type_expr.induct_tac "t" 1);
+  "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t";
+by (typ.induct_tac "t" 1);
 (* case TVar n *)
 by (fast_tac (HOL_cs addss !simpset) 1);
 (* case Fun t1 t2 *)
@@ -273,8 +273,8 @@
 bind_thm ("eq_free_eq_subst_te",result() RS mp);
 
 goal thy
-  "$ s1 (l::type_expr list) = $ s2 l --> n:(free_tv l) --> s1 n = s2 n";
-by (list.induct_tac "l" 1);
+  "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
+by (list.induct_tac "ts" 1);
 (* case [] *)
 by (fast_tac (HOL_cs addss !simpset) 1);
 (* case x#xl *)
@@ -282,8 +282,8 @@
 bind_thm ("eq_subst_tel_eq_free",result() RS mp RS mp);
 
 goal thy
-  "(!n. n:(free_tv l) --> s1 n = s2 n) --> $s1 (l::type_expr list) = $s2 l";
-by (list.induct_tac "l" 1); 
+  "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
+by (list.induct_tac "ts" 1); 
 (* case [] *)
 by (fast_tac (HOL_cs addss !simpset) 1);
 (* case x#xl *)
@@ -315,8 +315,8 @@
 qed "free_tv_subst_var";
 
 goal thy 
-     "free_tv ($ s (e::type_expr)) <= cod s Un free_tv e";
-by( type_expr.induct_tac "e" 1);
+     "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
+by( typ.induct_tac "t" 1);
 (* case TVar n *)
 by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
 (* case Fun t1 t2 *)
@@ -324,8 +324,8 @@
 qed "free_tv_app_subst_te";     
 
 goal thy 
-     "free_tv ($ s (l::type_expr list)) <= cod s Un free_tv l";
-by( list.induct_tac "l" 1);
+     "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
+by( list.induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
@@ -334,8 +334,7 @@
 qed "free_tv_app_subst_tel";
 
 goalw thy [free_tv_subst,dom_def] 
-     "free_tv (%u::nat. $ s1 ($ s2 (s3 u)) :: type_expr ) <=   \ 
+     "free_tv (%u::nat. $ s1 ($ s2 (s3 u)) :: typ) <=   \ 
 \     free_tv s1 Un free_tv s2 Un free_tv s3";
 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);
 qed "free_tv_comp_subst";    
-