--- a/src/HOL/MiniML/Type.ML Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/Type.ML Fri Jan 17 18:50:04 1997 +0100
@@ -1,37 +1,116 @@
-open Type;
+(* Title: HOL/MiniML/Type.thy
+ ID: $Id$
+ Author: Wolfgang Naraschewski and Tobias Nipkow
+ Copyright 1996 TU Muenchen
+*)
Addsimps [mgu_eq,mgu_mg,mgu_free];
-(* mgu does not introduce new type variables *)
-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);
-qed "mgu_new";
+
+(* lemmata for make scheme *)
+
+goal thy "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)";
+by (typ.induct_tac "t" 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "mk_scheme_Fun";
-(* application of id_subst does not change type expression *)
-goalw thy [id_subst_def]
- "$ id_subst = (%t::typ.t)";
-by (rtac ext 1);
+goal Type.thy "!t'.mk_scheme t = mk_scheme t' --> t=t'";
+by (typ.induct_tac "t" 1);
+ br allI 1;
+ by (typ.induct_tac "t'" 1);
+ by(Simp_tac 1);
+ by(Asm_full_simp_tac 1);
+br allI 1;
+by (typ.induct_tac "t'" 1);
+ by(Simp_tac 1);
+by(Asm_full_simp_tac 1);
+by(Fast_tac 1);
+qed_spec_mp "mk_scheme_injective";
+
+goal thy "!!t. free_tv (mk_scheme t) = free_tv t";
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "free_tv_mk_scheme";
+
+Addsimps [free_tv_mk_scheme];
+
+goal thy "!!t. $ S (mk_scheme t) = mk_scheme ($ S t)";
by (typ.induct_tac "t" 1);
by (ALLGOALS Asm_simp_tac);
-qed "app_subst_id_te";
-Addsimps [app_subst_id_te];
+qed "subst_mk_scheme";
+
+Addsimps [subst_mk_scheme];
+
-(* application of id_subst does not change list of type expressions *)
+(* constructor laws for app_subst *)
+
+goalw thy [app_subst_list]
+ "$ S [] = []";
+by (Simp_tac 1);
+qed "app_subst_Nil";
+
goalw thy [app_subst_list]
- "$ id_subst = (%ts::typ list.ts)";
-by (rtac ext 1);
-by (list.induct_tac "ts" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "app_subst_id_tel";
-Addsimps [app_subst_id_tel];
+ "$ S (x#l) = ($ S x)#($ S l)";
+by (Simp_tac 1);
+qed "app_subst_Cons";
+
+Addsimps [app_subst_Nil,app_subst_Cons];
+
+
+(* constructor laws for new_tv *)
+
+goalw thy [new_tv_def]
+ "new_tv n (TVar m) = (m<n)";
+by (fast_tac (HOL_cs addss !simpset) 1);
+qed "new_tv_TVar";
+
+goalw thy [new_tv_def]
+ "new_tv n (FVar m) = (m<n)";
+by (fast_tac (HOL_cs addss !simpset) 1);
+qed "new_tv_FVar";
+
+goalw thy [new_tv_def]
+ "new_tv n (BVar m) = True";
+by (Simp_tac 1);
+qed "new_tv_BVar";
+
+goalw thy [new_tv_def]
+ "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";
-goalw Type.thy [id_subst_def,o_def] "$s o id_subst = s";
-by (rtac ext 1);
+goalw thy [new_tv_def]
+ "new_tv n (t1 =-> t2) = (new_tv n t1 & new_tv n t2)";
+by (fast_tac (HOL_cs addss !simpset) 1);
+qed "new_tv_Fun2";
+
+goalw thy [new_tv_def]
+ "new_tv n []";
by (Simp_tac 1);
-qed "o_id_subst";
-Addsimps[o_id_subst];
+qed "new_tv_Nil";
+
+goalw thy [new_tv_def]
+ "new_tv n (x#l) = (new_tv n x & new_tv n l)";
+by (fast_tac (HOL_cs addss !simpset) 1);
+qed "new_tv_Cons";
+
+goalw Type.thy [new_tv_def] "!!n. new_tv n TVar";
+by (strip_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1);
+qed "new_tv_TVar_subst";
+
+Addsimps [new_tv_TVar,new_tv_FVar,new_tv_BVar,new_tv_Fun,new_tv_Fun2,new_tv_Nil,new_tv_Cons,new_tv_TVar_subst];
+
+goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
+ "new_tv n id_subst";
+by(Simp_tac 1);
+qed "new_tv_id_subst";
+Addsimps[new_tv_id_subst];
+
+
+(* constructor laws for dom and cod *)
goalw thy [dom_def,id_subst_def,empty_def]
"dom id_subst = {}";
@@ -45,14 +124,136 @@
qed "cod_id_subst";
Addsimps [cod_id_subst];
+
+(* lemmata for free_tv *)
+
goalw thy [free_tv_subst]
"free_tv id_subst = {}";
by (Simp_tac 1);
qed "free_tv_id_subst";
Addsimps [free_tv_id_subst];
+goal thy "!!A. !n. n < length A --> x : free_tv (nth n A) --> x : free_tv A";
+by (list.induct_tac "A" 1);
+by (Asm_full_simp_tac 1);
+by (rtac allI 1);
+by (res_inst_tac [("n","n")] nat_induct 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "free_tv_nth_A_impl_free_tv_A";
+
+Addsimps [free_tv_nth_A_impl_free_tv_A];
+
+goal thy "!!A. !nat. nat < length A --> x : free_tv (nth nat A) --> x : free_tv A";
+by (list.induct_tac "A" 1);
+by (Asm_full_simp_tac 1);
+by (rtac allI 1);
+by (res_inst_tac [("n","nat")] nat_induct 1);
+by (strip_tac 1);
+by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
+qed_spec_mp "free_tv_nth_nat_A";
+
+
+(* if two substitutions yield the same result if applied to a type
+ structure the substitutions coincide on the free type variables
+ occurring in the type structure *)
+
+goal thy "!!S S'. (!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t";
+by (typ.induct_tac "t" 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "typ_substitutions_only_on_free_variables";
+
+goal thy
+ "!!t. (!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t";
+by (rtac typ_substitutions_only_on_free_variables 1);
+by (simp_tac (!simpset addsimps [Ball_def]) 1);
+qed "eq_free_eq_subst_te";
+
+goal thy "!!S S'. (!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch";
+by (type_scheme.induct_tac "sch" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "scheme_substitutions_only_on_free_variables";
+
+goal thy
+ "!!sch. (!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch";
+by (rtac scheme_substitutions_only_on_free_variables 1);
+by (simp_tac (!simpset addsimps [Ball_def]) 1);
+qed "eq_free_eq_subst_type_scheme";
+
+goal thy
+ "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A";
+by (list.induct_tac "A" 1);
+(* case [] *)
+by (fast_tac (HOL_cs addss !simpset) 1);
+(* case x#xl *)
+by (fast_tac (HOL_cs addIs [eq_free_eq_subst_type_scheme] addss (!simpset)) 1);
+qed_spec_mp "eq_free_eq_subst_scheme_list";
+
+goal thy "!!P Q. ((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)";
+by (Fast_tac 1);
+val weaken_asm_Un = result ();
+
+goal thy "!!S S'. (!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A";
+by (list.induct_tac "A" 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac weaken_asm_Un 1);
+by (strip_tac 1);
+by (etac scheme_substitutions_only_on_free_variables 1);
+qed_spec_mp "scheme_list_substitutions_only_on_free_variables";
+
+goal thy
+ "$ 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 *)
+by (fast_tac (HOL_cs addss !simpset) 1);
+qed_spec_mp "eq_subst_te_eq_free";
+
+goal thy
+ "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n";
+by (type_scheme.induct_tac "sch" 1);
+(* case TVar n *)
+by (Asm_simp_tac 1);
+(* case BVar n *)
+by (strip_tac 1);
+by (etac mk_scheme_injective 1);
+by (Asm_simp_tac 1);
+(* case Fun t1 t2 *)
+by (Asm_full_simp_tac 1);
+qed_spec_mp "eq_subst_type_scheme_eq_free";
+
+goal thy
+ "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n";
+by (list.induct_tac "A" 1);
+(* case [] *)
+by (fast_tac (HOL_cs addss !simpset) 1);
+(* case x#xl *)
+by (fast_tac (HOL_cs addIs [eq_subst_type_scheme_eq_free] addss (!simpset)) 1);
+qed_spec_mp "eq_subst_scheme_list_eq_free";
+
+goalw thy [free_tv_subst]
+ "!!v. v : cod S ==> v : free_tv S";
+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);
+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 );
+qed "free_tv_le_new_tv";
+
goalw thy [dom_def,cod_def,UNION_def,Bex_def]
- "!!v. [| v : free_tv(s n); v~=n |] ==> v : cod s";
+ "!!v. [| v : free_tv(S n); v~=n |] ==> v : cod S";
by (Simp_tac 1);
by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
by (assume_tac 2);
@@ -61,286 +262,43 @@
qed "cod_app_subst";
Addsimps [cod_app_subst];
-
-(* composition of substitutions *)
-goal thy
- "$ 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 ts::typ list) = $ (%x. $ g (f x)) ts";
-by (list.induct_tac "ts" 1);
-(* case [] *)
-by (Simp_tac 1);
-(* case x#xl *)
-by (asm_full_simp_tac (!simpset addsimps [subst_comp_te]) 1);
-qed "subst_comp_tel";
-
-
-(* constructor laws for app_subst *)
-goalw thy [app_subst_list]
- "$ s [] = []";
-by (Simp_tac 1);
-qed "app_subst_Nil";
-
-goalw thy [app_subst_list]
- "$ s (t#ts) = ($ s t)#($ s ts)";
-by (Simp_tac 1);
-qed "app_subst_Cons";
-
-Addsimps [app_subst_Nil,app_subst_Cons];
-
-(* constructor laws for new_tv *)
-goalw thy [new_tv_def]
- "new_tv n (TVar m) = (m<n)";
-by (fast_tac (HOL_cs addss !simpset) 1);
-qed "new_tv_TVar";
-
-goalw thy [new_tv_def]
- "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";
-
-goalw thy [new_tv_def]
- "new_tv n []";
-by (Simp_tac 1);
-qed "new_tv_Nil";
-
-goalw thy [new_tv_def]
- "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";
-
-Addsimps [new_tv_TVar,new_tv_Fun,new_tv_Nil,new_tv_Cons];
-
-goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
- "new_tv n id_subst";
-by (Simp_tac 1);
-qed "new_tv_id_subst";
-Addsimps[new_tv_id_subst];
-
-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 (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);
-qed "new_tv_subst";
-
goal thy
- "new_tv n = list_all (new_tv n)";
-by (rtac ext 1);
-by (list.induct_tac "x" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "new_tv_list";
-
-(* substitution affects only variables occurring freely *)
-goal thy
- "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 (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::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 *)
-by (Asm_simp_tac 1);
-qed_spec_mp "new_tv_le";
-Addsimps [lessI RS less_imp_le RS new_tv_le];
-
-goal thy
- "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 *)
-by (fast_tac (HOL_cs addIs [new_tv_le] addss !simpset) 1);
-qed_spec_mp "new_tv_list_le";
-Addsimps [lessI RS less_imp_le RS new_tv_list_le];
-
-goal thy
- "!! n. [| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
-by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
-by (rtac conjI 1);
-by (slow_tac (HOL_cs addIs [le_trans]) 1);
-by (safe_tac HOL_cs );
-by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1);
-by (fast_tac (HOL_cs addss (HOL_ss addsimps [le_def])) 1);
-by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [new_tv_le])) );
-qed "new_tv_subst_le";
-Addsimps [lessI RS less_imp_le RS new_tv_subst_le];
-
-(* new_tv property remains if a substitution is applied *)
-goal thy
- "!!n. [| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)";
-by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
-qed "new_tv_subst_var";
-
-goal thy
- "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]))));
-qed_spec_mp "new_tv_subst_te";
-Addsimps [new_tv_subst_te];
-
-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 "ts" 1);
-by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
-qed_spec_mp "new_tv_subst_tel";
-Addsimps [new_tv_subst_tel];
-
-(* 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 (list.induct_tac "ts" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "new_tv_Suc_list";
-
-
-(* composition of substitutions preserves new_tv proposition *)
-goal thy
- "!! n. [| new_tv n (s::subst); new_tv n r |] ==> \
-\ new_tv n (($ r) o s)";
-by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
-qed "new_tv_subst_comp_1";
-
-goal thy
- "!! n. [| new_tv n (s::subst); new_tv n r |] ==> \
-\ new_tv n (%v.$ r (s v))";
-by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
-qed "new_tv_subst_comp_2";
-
-Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2];
-
-(* new type variables do not occur freely in a type structure *)
-goalw thy [new_tv_def]
- "!!n. new_tv n ts ==> n~:(free_tv ts)";
-by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
-qed "new_tv_not_free_tv";
-Addsimps [new_tv_not_free_tv];
-
-goal thy
- "(t::typ) mem ts --> free_tv t <= free_tv ts";
-by (list.induct_tac "ts" 1);
-(* case [] *)
-by (Simp_tac 1);
-(* case x#xl *)
-by (fast_tac (set_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
-qed_spec_mp "ftv_mem_sub_ftv_list";
-Addsimps [ftv_mem_sub_ftv_list];
-
-
-(* if two substitutions yield the same result if applied to a type
- structure the substitutions coincide on the free type variables
- occurring in the type structure *)
-goal thy
- "$ 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 *)
-by (fast_tac (HOL_cs addss !simpset) 1);
-qed_spec_mp "eq_subst_te_eq_free";
-
-goal thy
- "(!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 *)
-by (fast_tac (HOL_cs addss !simpset) 1);
-qed_spec_mp "eq_free_eq_subst_te";
-
-goal thy
- "$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 *)
-by (fast_tac (HOL_cs addIs [eq_subst_te_eq_free] addss (!simpset)) 1);
-qed_spec_mp "eq_subst_tel_eq_free";
-
-goal thy
- "(!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 *)
-by (fast_tac (HOL_cs addIs [eq_free_eq_subst_te] addss (!simpset)) 1);
-qed_spec_mp "eq_free_eq_subst_tel";
-
-(* some useful theorems *)
-goalw thy [free_tv_subst]
- "!!v. v : cod s ==> v : free_tv s";
-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);
-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 );
-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]) );
+ "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 (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);
+ "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);
+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);
+ "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
+by( type_scheme.induct_tac "sch" 1);
+(* case FVar n *)
+by( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
+(* case BVar n *)
+by (Simp_tac 1);
+(* case Fun t1 t2 *)
+by (fast_tac (set_cs addss !simpset) 1);
+qed "free_tv_app_subst_type_scheme";
+
+goal thy
+ "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
+by( list.induct_tac "A" 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);
-qed "free_tv_app_subst_tel";
+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]
"free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \
@@ -351,3 +309,440 @@
addsimps [cod_def,dom_def])) 1);
qed "free_tv_comp_subst";
+goalw thy [o_def]
+ "free_tv ($ S1 o S2) <= free_tv S1 Un free_tv (S2 :: nat => typ)";
+by (rtac free_tv_comp_subst 1);
+qed "free_tv_o_subst";
+
+goal thy "!!n. n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)";
+by (typ.induct_tac "t" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "free_tv_of_substitutions_extend_to_types";
+
+goal thy "!!n. n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)";
+by (type_scheme.induct_tac "sch" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed_spec_mp "free_tv_of_substitutions_extend_to_schemes";
+
+goal thy "!!n. n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)";
+by (list.induct_tac "A" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (fast_tac (!claset addDs [free_tv_of_substitutions_extend_to_schemes]) 1);
+qed_spec_mp "free_tv_of_substitutions_extend_to_scheme_lists";
+
+Addsimps [free_tv_of_substitutions_extend_to_scheme_lists];
+
+goal thy "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (strip_tac 1);
+by (Fast_tac 1);
+qed "free_tv_ML_scheme";
+
+goal thy "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
+by (list.induct_tac "A" 1);
+by (Simp_tac 1);
+by (asm_simp_tac (!simpset addsimps [free_tv_ML_scheme]) 1);
+qed "free_tv_ML_scheme_list";
+
+
+(* lemmata for bound_tv *)
+
+goal thy "!!t. bound_tv (mk_scheme t) = {}";
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "bound_tv_mk_scheme";
+
+Addsimps [bound_tv_mk_scheme];
+
+goal thy "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "bound_tv_subst_scheme";
+
+Addsimps [bound_tv_subst_scheme];
+
+goal thy "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A";
+by (rtac list.induct 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "bound_tv_subst_scheme_list";
+
+Addsimps [bound_tv_subst_scheme_list];
+
+
+(* lemmata for new_tv *)
+
+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( 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);
+qed "new_tv_subst";
+
+goal thy
+ "new_tv n = list_all (new_tv n)";
+by (rtac ext 1);
+by(list.induct_tac "x" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "new_tv_list";
+
+(* substitution affects only variables occurring freely *)
+goal thy
+ "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 (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+qed_spec_mp "subst_te_new_type_scheme";
+Addsimps [subst_te_new_type_scheme];
+
+goal thy
+ "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A";
+by (list.induct_tac "A" 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed_spec_mp "subst_tel_new_scheme_list";
+Addsimps [subst_tel_new_scheme_list];
+
+(* all greater variables are also new *)
+goalw thy [new_tv_def]
+ "!!n m. n<=m ==> new_tv n t ==> new_tv m t";
+by (safe_tac (!claset));
+by (dtac spec 1);
+by (mp_tac 1);
+by (trans_tac 1);
+qed "new_tv_le";
+Addsimps [lessI RS less_imp_le RS new_tv_le];
+
+goal thy "!!n m. n<=m ==> new_tv n (t::typ) ==> new_tv m t";
+by (asm_simp_tac (!simpset addsimps [new_tv_le]) 1);
+qed "new_tv_typ_le";
+
+goal thy "!!n m. n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A";
+by (asm_simp_tac (!simpset addsimps [new_tv_le]) 1);
+qed "new_scheme_list_le";
+
+goal thy "!!n m. n<=m ==> new_tv n (S::subst) ==> new_tv m S";
+by (asm_simp_tac (!simpset addsimps [new_tv_le]) 1);
+qed "new_tv_subst_le";
+
+(* new_tv property remains if a substitution is applied *)
+goal thy
+ "!!n. [| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)";
+by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
+qed "new_tv_subst_var";
+
+goal thy
+ "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]))));
+qed_spec_mp "new_tv_subst_te";
+Addsimps [new_tv_subst_te];
+
+goal thy "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS (Asm_full_simp_tac));
+by (rewrite_goals_tac [new_tv_def]);
+by (simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1);
+by (strip_tac 1);
+by (case_tac "S nat = TVar nat" 1);
+by (rotate_tac 3 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("x","m")] spec 1);
+by (Fast_tac 1);
+qed_spec_mp "new_tv_subst_type_scheme";
+Addsimps [new_tv_subst_type_scheme];
+
+goal thy
+ "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)";
+by (list.induct_tac "A" 1);
+by (ALLGOALS(fast_tac (HOL_cs addss (!simpset))));
+qed_spec_mp "new_tv_subst_scheme_list";
+Addsimps [new_tv_subst_scheme_list];
+
+goal thy
+ "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
+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";
+
+goalw thy [new_tv_def] "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')";
+by (Asm_simp_tac 1);
+qed_spec_mp "new_tv_only_depends_on_free_tv_type_scheme";
+
+goalw thy [new_tv_def] "!!A::type_scheme list. (free_tv A) = (free_tv A') --> (new_tv n A --> new_tv n A')";
+by (Asm_simp_tac 1);
+qed_spec_mp "new_tv_only_depends_on_free_tv_scheme_list";
+
+goalw thy [new_tv_def] "!!A. !nat. nat < length A --> new_tv n A --> (new_tv n (nth nat A))";
+by (list.induct_tac "A" 1);
+by (Asm_full_simp_tac 1);
+by (rtac allI 1);
+by (res_inst_tac [("n","nat")] nat_induct 1);
+by (strip_tac 1);
+by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
+qed_spec_mp "new_tv_nth_nat_A";
+
+
+(* composition of substitutions preserves new_tv proposition *)
+goal thy
+ "!! n. [| new_tv n (S::subst); new_tv n R |] ==> \
+\ new_tv n (($ R) o S)";
+by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
+qed "new_tv_subst_comp_1";
+
+goal thy
+ "!! n. [| new_tv n (S::subst); new_tv n R |] ==> \
+\ new_tv n (%v.$ R (S v))";
+by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
+qed "new_tv_subst_comp_2";
+
+Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2];
+
+(* new type variables do not occur freely in a type structure *)
+goalw thy [new_tv_def]
+ "!!n. new_tv n A ==> n~:(free_tv A)";
+by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
+qed "new_tv_not_free_tv";
+Addsimps [new_tv_not_free_tv];
+
+goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (safe_tac (!claset));
+by (trans_tac 1);
+qed "less_maxL";
+
+goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (fast_tac (!claset addDs [not_leE] addIs [less_trans]) 1);
+qed "less_maxR";
+
+goalw thy [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
+by (typ.induct_tac "t" 1);
+by (res_inst_tac [("x","Suc nat")] exI 1);
+by (Asm_simp_tac 1);
+by (REPEAT (etac exE 1));
+by (rename_tac "n'" 1);
+by (res_inst_tac [("x","max n n'")] exI 1);
+by (Simp_tac 1);
+by (fast_tac (!claset addIs [less_maxR,less_maxL]) 1);
+qed "fresh_variable_types";
+
+Addsimps [fresh_variable_types];
+
+goalw thy [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)";
+by (type_scheme.induct_tac "sch" 1);
+by (res_inst_tac [("x","Suc nat")] exI 1);
+by (Simp_tac 1);
+by (res_inst_tac [("x","Suc nat")] exI 1);
+by (Simp_tac 1);
+by (REPEAT (etac exE 1));
+by (rename_tac "n'" 1);
+by (res_inst_tac [("x","max n n'")] exI 1);
+by (Simp_tac 1);
+by (fast_tac (!claset addIs [less_maxR,less_maxL]) 1);
+qed "fresh_variable_type_schemes";
+
+Addsimps [fresh_variable_type_schemes];
+
+goalw thy [max_def] "!!n::nat. n <= (max n n')";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+qed "le_maxL";
+
+goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (fast_tac (!claset addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
+qed "le_maxR";
+
+goal thy "!!A::type_scheme list. ? n. (new_tv n A)";
+by (list.induct_tac "A" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (etac exE 1);
+by (cut_inst_tac [("sch","a")] fresh_variable_type_schemes 1);
+by (etac exE 1);
+by (rename_tac "n'" 1);
+by (res_inst_tac [("x","(max n n')")] exI 1);
+by (subgoal_tac "n <= (max n n')" 1);
+by (subgoal_tac "n' <= (max n n')" 1);
+by (fast_tac (!claset addDs [new_tv_le]) 1);
+by (ALLGOALS (simp_tac (!simpset addsimps [le_maxR,le_maxL])));
+qed "fresh_variable_type_scheme_lists";
+
+Addsimps [fresh_variable_type_scheme_lists];
+
+goal thy "!!x y. [| ? n1. (new_tv n1 x); ? n2. (new_tv n2 y)|] ==> ? n. (new_tv n x) & (new_tv n y)";
+by (REPEAT (etac exE 1));
+by (rename_tac "n1 n2" 1);
+by (res_inst_tac [("x","(max n1 n2)")] exI 1);
+by (subgoal_tac "n1 <= max n1 n2" 1);
+by (subgoal_tac "n2 <= max n1 n2" 1);
+by (fast_tac (!claset addDs [new_tv_le]) 1);
+by (ALLGOALS (simp_tac (!simpset addsimps [le_maxL,le_maxR])));
+qed "make_one_new_out_of_two";
+
+goal thy "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ). \
+\ ? n. (new_tv n A) & (new_tv n A') & (new_tv n t) & (new_tv n t')" ;
+by (cut_inst_tac [("t","t")] fresh_variable_types 1);
+by (cut_inst_tac [("t","t'")] fresh_variable_types 1);
+by (dtac make_one_new_out_of_two 1);
+ba 1;
+by (thin_tac "? n. new_tv n t'" 1);
+by (cut_inst_tac [("A","A")] fresh_variable_type_scheme_lists 1);
+by (cut_inst_tac [("A","A'")] fresh_variable_type_scheme_lists 1);
+by (rotate_tac 1 1);
+by (dtac make_one_new_out_of_two 1);
+ba 1;
+by (thin_tac "? n. new_tv n A'" 1);
+by (REPEAT (etac exE 1));
+by (rename_tac "n2 n1" 1);
+by (res_inst_tac [("x","(max n1 n2)")] exI 1);
+by (rewrite_goals_tac [new_tv_def]);
+by (fast_tac (!claset addIs [less_maxL,less_maxR]) 1);
+qed "ex_fresh_variable";
+
+(* mgu does not introduce new type variables *)
+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);
+qed "mgu_new";
+
+
+(* lemmata for substitutions *)
+
+goalw Type.thy [app_subst_list] "length ($ S A) = length A";
+by(Simp_tac 1);
+qed "length_app_subst_list";
+Addsimps [length_app_subst_list];
+
+goal thy "!!sch::type_scheme. $ TVar sch = sch";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "subst_TVar_scheme";
+
+Addsimps [subst_TVar_scheme];
+
+goal thy "!!A::type_scheme list. $ TVar A = A";
+by (rtac list.induct 1);
+by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [app_subst_list])));
+qed "subst_TVar_scheme_list";
+
+Addsimps [subst_TVar_scheme_list];
+
+(* application of id_subst does not change type expression *)
+goalw thy [id_subst_def]
+ "$ id_subst = (%t::typ.t)";
+by (rtac ext 1);
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "app_subst_id_te";
+Addsimps [app_subst_id_te];
+
+goalw thy [id_subst_def]
+ "$ id_subst = (%sch::type_scheme.sch)";
+by (rtac ext 1);
+by (type_scheme.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "app_subst_id_type_scheme";
+Addsimps [app_subst_id_type_scheme];
+
+(* application of id_subst does not change list of type expressions *)
+goalw thy [app_subst_list]
+ "$ id_subst = (%A::type_scheme list.A)";
+by (rtac ext 1);
+by (list.induct_tac "A" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "app_subst_id_tel";
+Addsimps [app_subst_id_tel];
+
+goal thy "!!sch::type_scheme. $ id_subst sch = sch";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [id_subst_def])));
+qed "id_subst_sch";
+
+Addsimps [id_subst_sch];
+
+goal thy "!!A::type_scheme list. $ id_subst A = A";
+by (list.induct_tac "A" 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed "id_subst_A";
+
+Addsimps [id_subst_A];
+
+(* composition of substitutions *)
+goalw Type.thy [id_subst_def,o_def] "$S o id_subst = S";
+br ext 1;
+by(Simp_tac 1);
+qed "o_id_subst";
+Addsimps[o_id_subst];
+
+goal thy
+ "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t";
+by (typ.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "subst_comp_te";
+
+goal thy
+ "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch";
+by (type_scheme.induct_tac "sch" 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "subst_comp_type_scheme";
+
+goalw thy [app_subst_list]
+ "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A";
+by (list.induct_tac "A" 1);
+(* case [] *)
+by (Simp_tac 1);
+(* case x#xl *)
+by (asm_full_simp_tac (!simpset addsimps [subst_comp_type_scheme]) 1);
+qed "subst_comp_scheme_list";
+
+goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = $ id_subst A";
+by (rtac scheme_list_substitutions_only_on_free_variables 1);
+by (asm_full_simp_tac (!simpset addsimps [id_subst_def]) 1);
+qed "subst_id_on_type_scheme_list'";
+
+goal thy "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A";
+by (stac subst_id_on_type_scheme_list' 1);
+ba 1;
+by (Simp_tac 1);
+qed "subst_id_on_type_scheme_list";
+
+goal thy "!!n. !n. n < length A --> nth n ($ S A) = $S (nth n A)";
+by (list.induct_tac "A" 1);
+by (Asm_full_simp_tac 1);
+by (rtac allI 1);
+by (rename_tac "n1" 1);
+by (res_inst_tac[("n","n1")] nat_induct 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "nth_subst";
--- a/src/HOL/MiniML/W.ML Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/W.ML Fri Jan 17 18:50:04 1997 +0100
@@ -8,204 +8,296 @@
open W;
-Addsimps [Suc_le_lessD];
-Delsimps (ex_simps @ all_simps);
-
-(* correctness of W with respect to has_type *)
-goal W.thy
- "!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);
-(* case Abs e *)
-by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
- setloop (split_tac [expand_bind])) 1);
-by (strip_tac 1);
-by (eres_inst_tac [("x","TVar(n) # a")] allE 1);
-by ( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);
-(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
-by (strip_tac 1);
-by ( rename_tac "sa ta na sb tb nb sc" 1);
-by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
-by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);
-by (rtac (app_subst_Fun RS subst) 1);
-by (res_inst_tac [("t","$sc(tb -> (TVar nb))"),("s","$sc($sb ta)")] subst 1);
-by (Asm_full_simp_tac 1);
-by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1);
-by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
-by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
-by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
-qed_spec_mp "W_correct";
+Addsimps [diff_add_inverse,diff_add_inverse2,Suc_le_lessD];
val has_type_casesE = map(has_type.mk_cases expr.simps)
- [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
-
+ [" A |- Var n :: t"," A |- Abs e :: t","A |- App e1 e2 ::t","A |- LET 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 = Some (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);
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (strip_tac 1);
+by (etac conjE 1);
+by (etac conjE 1);
+by (dtac sym 1);
+by (dtac sym 1);
+by (dtac sym 1);
+by (Asm_full_simp_tac 1);
(* case Abs e *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
by (strip_tac 1);
-by (rename_tac "s t na sa ta nb sb sc tb m" 1);
-by (eres_inst_tac [("x","a")] allE 1);
+by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
+by (eres_inst_tac [("x","A")] allE 1);
by (eres_inst_tac [("x","n")] allE 1);
-by (eres_inst_tac [("x","$ s a")] allE 1);
-by (eres_inst_tac [("x","s")] allE 1);
+by (eres_inst_tac [("x","$ S A")] allE 1);
+by (eres_inst_tac [("x","S")] allE 1);
by (eres_inst_tac [("x","t")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
by (etac conjE 1);
-by (eres_inst_tac [("x","sa")] allE 1);
-by (eres_inst_tac [("x","ta")] allE 1);
-by (eres_inst_tac [("x","nb")] allE 1);
+by (eres_inst_tac [("x","S1")] allE 1);
+by (eres_inst_tac [("x","t1")] allE 1);
+by (eres_inst_tac [("x","n2")] allE 1);
by (etac conjE 1);
-by (res_inst_tac [("j","na")] le_trans 1);
+by (res_inst_tac [("j","n1")] le_trans 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
+(* case LET e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (strip_tac 1);
+by (rename_tac "A n1 S t2 m1 S2 t3 m2 S3 t1 m" 1);
+by (REPEAT (etac conjE 1));
+by (REPEAT (etac allE 1));
+by (mp_tac 1);
+by (mp_tac 1);
+by (best_tac (!claset addEs [le_trans]) 1);
qed_spec_mp "W_var_ge";
Addsimps [W_var_ge];
goal thy
- "!! s. Ok (s,t,m) = W e a n ==> n<=m";
+ "!! s. Some (S,t,m) = W e A n ==> n<=m";
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
qed "W_var_geD";
+goal thy "!! s. new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A";
+by (dtac W_var_geD 1);
+by (rtac new_scheme_list_le 1);
+ba 1;
+ba 1;
+qed "new_tv_compatible_W";
(* auxiliary lemma *)
-goal Maybe.thy "(y = Ok x) = (Ok x = y)";
-by ( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
-qed "rotate_Ok";
+goal Maybe.thy "(y = Some x) = (Some x = y)";
+by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+qed "rotate_Some";
+goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
+by (type_scheme.induct_tac "sch" 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
+by (strip_tac 1);
+by (Asm_full_simp_tac 1);
+by (etac conjE 1);
+by (rtac conjI 1);
+by (rtac new_tv_le 1);
+by (mp_tac 2);
+by (mp_tac 2);
+ba 2;
+by (rtac add_le_mono 1);
+by (Simp_tac 1);
+by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
+by (strip_tac 1);
+by (rtac new_tv_le 1);
+by (mp_tac 2);
+by (mp_tac 2);
+ba 2;
+by (rtac add_le_mono 1);
+by (Simp_tac 1);
+by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
+by (strip_tac 1);
+by (dtac not_leE 1);
+by (rtac less_or_eq_imp_le 1);
+by (Fast_tac 1);
+qed_spec_mp "new_tv_bound_typ_inst_sch";
+
+Addsimps [new_tv_bound_typ_inst_sch];
(* resulting type variable is new *)
goal thy
- "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) --> \
-\ new_tv m s & new_tv m t";
+ "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) --> \
+\ new_tv m S & new_tv m t";
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]
- setloop (split_tac [expand_if]))) 1);
-
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (strip_tac 1);
+by (REPEAT (etac conjE 1));
+by (rtac conjI 1);
+by (dtac sym 1);
+by (Asm_full_simp_tac 1);
+by (dtac sym 1);
+by (dtac sym 1);
+by (dtac sym 1);
+by (dtac new_tv_nth_nat_A 1);
+ba 1;
+by (Asm_full_simp_tac 1);
(* case Abs e *)
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list]
- setloop (split_tac [expand_bind])) 1);
+ setloop (split_tac [expand_option_bind])) 1);
by (strip_tac 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
-by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
+by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
by (fast_tac (HOL_cs addss (!simpset
addsimps [new_tv_subst,new_tv_Suc_list])) 1);
-
(* case App e1 e2 *)
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
by (strip_tac 1);
-by (rename_tac "s t na sa ta nb sb sc tb m" 1);
+by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
by (eres_inst_tac [("x","n")] allE 1);
-by (eres_inst_tac [("x","a")] allE 1);
-by (eres_inst_tac [("x","s")] allE 1);
+by (eres_inst_tac [("x","A")] allE 1);
+by (eres_inst_tac [("x","S")] allE 1);
by (eres_inst_tac [("x","t")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
-by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
-by (eres_inst_tac [("x","$ s a")] allE 1);
-by (eres_inst_tac [("x","sa")] allE 1);
-by (eres_inst_tac [("x","ta")] allE 1);
-by (eres_inst_tac [("x","nb")] allE 1);
-by ( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
+by (eres_inst_tac [("x","n1")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv] delsimps all_simps) 1);
+by (eres_inst_tac [("x","$ S A")] allE 1);
+by (eres_inst_tac [("x","S1")] allE 1);
+by (eres_inst_tac [("x","t1")] allE 1);
+by (eres_inst_tac [("x","n2")] allE 1);
+by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Some]) 1);
by (rtac conjI 1);
by (rtac new_tv_subst_comp_2 1);
by (rtac new_tv_subst_comp_2 1);
-by (rtac (lessI RS less_imp_le RS new_tv_subst_le) 1);
-by (res_inst_tac [("n","na")] new_tv_subst_le 1);
-by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
+by (rtac (lessI RS less_imp_le RS new_tv_le) 1);
+by (res_inst_tac [("n","n1")] new_tv_subst_le 1);
+by (asm_full_simp_tac (!simpset addsimps [rotate_Some]) 1);
by (Asm_simp_tac 1);
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])
+ [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS new_tv_subst_le])
1);
by (etac (sym RS mgu_new) 1);
-by (best_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);
+by (best_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_scheme_list_le,
+ new_tv_subst_scheme_list,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_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
+ addss (!simpset)) 1);
by (rtac (lessI RS new_tv_subst_var) 1);
by (etac (sym RS mgu_new) 1);
by (best_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 new_tv_subst_le,
- new_tv_le]
- addss !simpset) 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);
+ addDs [W_var_geD] addIs
+ [new_scheme_list_le,new_tv_subst_scheme_list,lessI RS less_imp_le RS
+ new_tv_subst_le,new_tv_le] addss !simpset) 1);
+by (fast_tac (HOL_cs addDs [W_var_geD] addIs
+ [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
+ addss (!simpset)) 1);
+(* case LET e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (strip_tac 1);
+by (rename_tac "n1 A S1 t1 n2 S2 t2 m2 S t m" 1);
+by (REPEAT (etac conjE 1));
+by (eres_inst_tac [("x","n1")] allE 1);
+by (eres_inst_tac [("x","A")] allE 1);
+by (eres_inst_tac [("x","S1")] allE 1);
+by (eres_inst_tac [("x","t1")] allE 1);
+by (rotate_tac 1 1);
+by (eres_inst_tac [("x","n2")] allE 1);
+by (mp_tac 1);
+by (mp_tac 1);
+by (etac conjE 1);
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv] delsimps all_simps) 1);
+by (dtac sym 1);
+by (eres_inst_tac [("x","n2")] allE 1);
+by (eres_inst_tac [("x","gen ($ S1 A) t1 # $ S1 A")] allE 1);
+by (eres_inst_tac [("x","S2")] allE 1);
+by (eres_inst_tac [("x","t2")] allE 1);
+by (eres_inst_tac [("x","m2")] allE 1);
+by (subgoal_tac "new_tv n2 (gen ($ S1 A) t1 # $ S1 A)" 1);
+by (mp_tac 1);
+by (mp_tac 1);
+by (etac conjE 1);
+by (rtac conjI 1);
+by (simp_tac (!simpset addsimps [o_def]) 1);
+by (rtac new_tv_subst_comp_2 1);
+by (res_inst_tac [("n","n2")] new_tv_subst_le 1);
+by (etac W_var_ge 1);
+ba 1;
+ba 1;
+ba 1;
+by (rewrite_goals_tac [new_tv_def]);
+by (Asm_simp_tac 1);
+by (dtac W_var_ge 1);
+by (rtac allI 1);
+by (rename_tac "p" 1);
+by (strip_tac 1);
+by (rewrite_goals_tac [free_tv_subst]);
+by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
+fun restrict_prems is tacf =
+ METAHYPS(fn prems =>
+ let val iprems = map (fn i => nth_elem(i,prems)) is
+ in cut_facts_tac iprems 1 THEN tacf 1 end);
+by (restrict_prems [0,4,8,9] (best_tac (!claset addEs [less_le_trans])) 1);
qed_spec_mp "new_tv_W";
+goal thy "!!sch. (v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)";
+by (type_scheme.induct_tac "sch" 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (strip_tac 1);
+by (rtac exI 1);
+by (rtac refl 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "free_tv_bound_typ_inst1";
+
+Addsimps [free_tv_bound_typ_inst1];
goal thy
- "!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";
+ "!n A S t m v. W e A n = Some (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 *)
-by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list]
- addss (!simpset setloop (split_tac [expand_if]))) 1);
-
+by (simp_tac (!simpset addsimps
+ [free_tv_subst] setloop (split_tac [expand_option_bind,expand_if])) 1);
+by (strip_tac 1);
+by (REPEAT (etac conjE 1));
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [dom_def,cod_def,id_subst_def]) 1);
+by (case_tac "v : free_tv (nth nat A)" 1);
+by (Asm_full_simp_tac 1);
+by (strip_tac 1);
+by (dtac free_tv_bound_typ_inst1 1);
+by (simp_tac (!simpset addsimps [o_def]) 1);
+by (rotate_tac 3 1);
+by (etac exE 1);
+by (rotate_tac 3 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
+by (dtac add_lessD1 1);
+by (fast_tac (!claset addIs [less_irrefl]) 1);
(* case Abs e *)
by (asm_full_simp_tac (!simpset addsimps
- [free_tv_subst] setloop (split_tac [expand_bind])) 1);
+ [free_tv_subst] setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
by (strip_tac 1);
-by (rename_tac "s t na sa ta m v" 1);
+by (rename_tac "S t n1 S1 t1 m v" 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
-by (eres_inst_tac [("x","TVar n # a")] allE 1);
-by (eres_inst_tac [("x","s")] allE 1);
+by (eres_inst_tac [("x","FVar n # A")] allE 1);
+by (eres_inst_tac [("x","S")] allE 1);
by (eres_inst_tac [("x","t")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
by (eres_inst_tac [("x","v")] allE 1);
-by (fast_tac (HOL_cs addSEs [allE]
- addIs [cod_app_subst]
+by (best_tac (HOL_cs 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 (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
by (strip_tac 1);
-by (rename_tac "s t na sa ta nb sb sc tb m v" 1);
+by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1);
by (eres_inst_tac [("x","n")] allE 1);
-by (eres_inst_tac [("x","a")] allE 1);
-by (eres_inst_tac [("x","s")] allE 1);
+by (eres_inst_tac [("x","A")] allE 1);
+by (eres_inst_tac [("x","S")] allE 1);
by (eres_inst_tac [("x","t")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
+by (eres_inst_tac [("x","n1")] 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);
-by (eres_inst_tac [("x","ta")] allE 1);
-by (eres_inst_tac [("x","nb")] allE 1);
+by (eres_inst_tac [("x","$ S A")] allE 1);
+by (eres_inst_tac [("x","S1")] allE 1);
+by (eres_inst_tac [("x","t1")] allE 1);
+by (eres_inst_tac [("x","n2")] allE 1);
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,o_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps [rotate_Some,o_def]) 1);
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,
+ codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
less_le_trans,less_not_refl2,subsetD]
addEs [UnE]
addss !simpset) 1);
@@ -214,54 +306,224 @@
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]
- addSEs [UnE]
- addss !simpset) 1);
+ free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
+ less_le_trans,subsetD]
+ addEs [UnE]
+ addss !simpset) 1);
+(* LET e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
+by (strip_tac 1);
+by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
+by (eres_inst_tac [("x","nat")] allE 1);
+by (eres_inst_tac [("x","A")] allE 1);
+by (eres_inst_tac [("x","S1")] allE 1);
+by (eres_inst_tac [("x","t1")] allE 1);
+by (rotate_tac 1 1);
+by (eres_inst_tac [("x","n2")] allE 1);
+by (rotate_tac 4 1);
+by (eres_inst_tac [("x","v")] allE 1);
+by (mp_tac 1);
+by (EVERY1 [etac allE,etac allE,etac allE,etac allE,etac allE,eres_inst_tac [("x","v")] allE]);
+by (mp_tac 1);
+by (Asm_full_simp_tac 1);
+by (rtac conjI 1);
+by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,free_tv_o_subst RS subsetD,W_var_ge]
+ addDs [less_le_trans]) 1);
+by (fast_tac (!claset addSDs [codD,free_tv_app_subst_scheme_list RS subsetD,W_var_ge]
+ addDs [less_le_trans]) 1);
qed_spec_mp "free_tv_W";
+goal thy "!!A. (!x. x : A --> x ~: B) ==> A Int B = {}";
+by (Fast_tac 1);
+qed "weaken_A_Int_B_eq_empty";
+
+goal thy "!!A. x ~: A | x : B ==> x ~: A - B";
+by (Fast_tac 1);
+qed "weaken_not_elem_A_minus_B";
+
+(* correctness of W with respect to has_type *)
+goal W.thy
+ "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
+by (expr.induct_tac "e" 1);
+(* case Var n *)
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (strip_tac 1);
+by (rtac has_type.VarI 1);
+by (Simp_tac 1);
+by (simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
+by (rtac exI 1);
+by (rtac refl 1);
+(* case Abs e *)
+by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
+ setloop (split_tac [expand_option_bind])) 1);
+by (strip_tac 1);
+by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1);
+by (Asm_full_simp_tac 1);
+by (rtac has_type.AbsI 1);
+by (dtac (le_refl RS le_SucI RS new_scheme_list_le) 1);
+bd sym 1;
+by (REPEAT (etac allE 1));
+by (etac impE 1);
+by (mp_tac 2);
+by (Asm_simp_tac 1);
+ba 1;
+(* case App e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (strip_tac 1);
+by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
+by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1);
+by (res_inst_tac [("S1","S3")] (app_subst_TVar RS subst) 1);
+by (rtac (app_subst_Fun RS subst) 1);
+by (res_inst_tac [("t","$S3 (t2 -> (TVar n2))"),("s","$S3 ($S2 t1)")] subst 1);
+by (Asm_full_simp_tac 1);
+by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
+by ((rtac (has_type_cl_sub RS spec) 1) THEN (rtac (has_type_cl_sub RS spec) 1));
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+by (asm_full_simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
+by (rtac (has_type_cl_sub RS spec) 1);
+by (forward_tac [new_tv_W] 1);
+ba 1;
+by (dtac conjunct1 1);
+by (dtac conjunct1 1);
+by (forward_tac [new_tv_subst_scheme_list] 1);
+by (rtac new_scheme_list_le 1);
+by (rtac W_var_ge 1);
+ba 1;
+ba 1;
+by (etac thin_rl 1);
+by (REPEAT (etac allE 1));
+bd sym 1;
+bd sym 1;
+by (etac thin_rl 1);
+by (etac thin_rl 1);
+by (mp_tac 1);
+by (mp_tac 1);
+ba 1;
+(* case Let e1 e2 *)
+by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+by (strip_tac 1);
+by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1);
+by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
+by (simp_tac (!simpset addsimps [o_def]) 1);
+by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
+by (rtac (has_type_cl_sub RS spec) 1);
+by (dres_inst_tac [("x","A")] spec 1);
+by (dres_inst_tac [("x","S1")] spec 1);
+by (dres_inst_tac [("x","t1")] spec 1);
+by (dres_inst_tac [("x","m2")] spec 1);
+by (rotate_tac 4 1);
+by (dres_inst_tac [("x","m1")] spec 1);
+by (mp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+by (simp_tac (!simpset addsimps [o_def]) 1);
+by (simp_tac (HOL_ss addsimps [subst_comp_scheme_list RS sym]) 1);
+by (rtac (gen_subst_commutes RS sym RS subst) 1);
+by (rtac (app_subst_Cons RS subst) 2);
+by (etac thin_rl 2);
+by (dres_inst_tac [("x","gen ($S1 A) t1 # $ S1 A")] spec 2);
+by (dres_inst_tac [("x","S2")] spec 2);
+by (dres_inst_tac [("x","t")] spec 2);
+by (dres_inst_tac [("x","n2")] spec 2);
+by (dres_inst_tac [("x","m2")] spec 2);
+by (forward_tac [new_tv_W] 2);
+ba 2;
+by (dtac conjunct1 2);
+by (dtac conjunct1 2);
+by (forward_tac [new_tv_subst_scheme_list] 2);
+by (rtac new_scheme_list_le 2);
+by (rtac W_var_ge 2);
+ba 2;
+ba 2;
+by (etac impE 2);
+by (res_inst_tac [("A","$ S1 A")] new_tv_only_depends_on_free_tv_scheme_list 2);
+by (Simp_tac 2);
+by (Fast_tac 2);
+ba 2;
+by (Asm_full_simp_tac 2);
+by (rtac weaken_A_Int_B_eq_empty 1);
+by (rtac allI 1);
+by (strip_tac 1);
+by (rtac weaken_not_elem_A_minus_B 1);
+by (case_tac "x < m2" 1);
+by (rtac disjI2 1);
+by (rtac (free_tv_gen_cons RS subst) 1);
+by (rtac free_tv_W 1);
+ba 1;
+by (Asm_full_simp_tac 1);
+ba 1;
+by (rtac disjI1 1);
+by (dtac new_tv_W 1);
+ba 1;
+by (dtac conjunct2 1);
+by (dtac conjunct2 1);
+by (rtac new_tv_not_free_tv 1);
+by (rtac new_tv_le 1);
+ba 2;
+by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1);
+qed_spec_mp "W_correct_lemma";
+
+goal Type.thy "new_tv n (sch::type_scheme) --> \
+\ $(%k.if k<n then S k else S' k) sch = $S sch";
+by (type_scheme.induct_tac "sch" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "new_if_subst_type_scheme";
+Addsimps [new_if_subst_type_scheme];
+
+goal Type.thy "new_tv n (A::type_scheme list) --> \
+\ $(%k.if k<n then S k else S' k) A = $S A";
+by (list.induct_tac "A" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "new_if_subst_type_scheme_list";
+Addsimps [new_if_subst_type_scheme_list];
+
+goal Arith.thy "!!n::nat. ~ k+n < n";
+by (nat_ind_tac "k" 1);
+by(ALLGOALS Asm_simp_tac);
+by(trans_tac 1);
+qed "not_add_less1";
+Addsimps [not_add_less1];
(* 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 = Some (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);
by (simp_tac (!simpset addcongs [conj_cong]
- setloop (split_tac [expand_if])) 1);
+ setloop (split_tac [expand_if])) 1);
by (eresolve_tac has_type_casesE 1);
-by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);
-by (res_inst_tac [("x","id_subst")] exI 1);
-by (res_inst_tac [("x","nth nat a")] exI 1);
-by (Simp_tac 1);
-by (res_inst_tac [("x","s'")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
+by (etac exE 1);
+by (hyp_subst_tac 1);
+by (rename_tac "S" 1);
+by (res_inst_tac [("x","%x. (if x < n then S' x else S (x - n))")] exI 1);
+by (rtac conjI 1);
by (Asm_simp_tac 1);
+by (asm_simp_tac (!simpset addsimps [(bound_typ_inst_composed_subst RS sym),new_tv_nth_nat_A,o_def,nth_subst]
+ delsimps [bound_typ_inst_composed_subst]) 1);
-(** LEVEL 10 **)
(* case Abs e *)
by (strip_tac 1);
by (eresolve_tac has_type_casesE 1);
-by (eres_inst_tac [("x","%x.if x=n then t1 else (s' x)")] allE 1);
-by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
+by (eres_inst_tac [("x","%x.if x=n then t1 else (S' x)")] allE 1);
+by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
by (eres_inst_tac [("x","t2")] allE 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
-by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong]
- setloop (split_tac [expand_bind]))) 1);
+by (best_tac (HOL_cs addSDs [mk_scheme_injective] addss (!simpset addcongs [conj_cong]
+ setloop (split_tac [expand_option_bind]))) 1);
-(** LEVEL 17 **)
(* case App e1 e2 *)
by (strip_tac 1);
by (eresolve_tac has_type_casesE 1);
-by (eres_inst_tac [("x","s'")] allE 1);
-by (eres_inst_tac [("x","a")] allE 1);
+by (eres_inst_tac [("x","S'")] allE 1);
+by (eres_inst_tac [("x","A")] allE 1);
by (eres_inst_tac [("x","t2 -> t'")] allE 1);
by (eres_inst_tac [("x","n")] allE 1);
by (safe_tac HOL_cs);
-by (eres_inst_tac [("x","r")] allE 1);
-by (eres_inst_tac [("x","$ s a")] allE 1);
+by (eres_inst_tac [("x","R")] allE 1);
+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);
by (dtac asm_rl 1);
@@ -271,119 +533,140 @@
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_scheme_list_le,new_tv_subst_scheme_list]) 1);
-(** LEVEL 35 **)
by (subgoal_tac
- "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
-\ else ra x)) ($ sa t) = \
-\ $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
-\ else ra x)) (ta -> (TVar ma))" 1);
+ "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
+\ else Ra x)) ($ Sa t) = \
+\ $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
+\ else Ra x)) (ta -> (TVar ma))" 1);
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
-\ (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
- ("s","($ ra ta) -> t'")] ssubst 2);
+\ (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);
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,
- new_tv_not_free_tv,new_tv_le]) 3);
-(** LEVEL 42 **)
-by (case_tac "na:free_tv sa" 2);
-(* na ~: free_tv sa *)
-by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
- setloop (split_tac [expand_if])) 3);
-(* na : free_tv sa *)
-by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
-by (dtac eq_subst_tel_eq_free 2);
+ new_tv_not_free_tv,new_tv_le]) 3);
+by (case_tac "na:free_tv Sa" 2);
+(* n1 ~: free_tv S1 *)
+by (forward_tac [not_free_impl_id] 3);
+by (asm_simp_tac (!simpset
+ setloop (split_tac [expand_if])) 3);
+(* na : free_tv Sa *)
+by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
+by (dtac eq_subst_scheme_list_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);
-(* na ~: dom sa *)
+by (case_tac "na:dom Sa" 2);
+(* na ~: dom Sa *)
by (asm_full_simp_tac (!simpset addsimps [dom_def]
- setloop (split_tac [expand_if])) 3);
-(** LEVEL 50 **)
-(* na : dom sa *)
+ setloop (split_tac [expand_if])) 3);
+(* na : dom Sa *)
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));
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 (dtac new_tv_subst_scheme_list 3);
+by (fast_tac (HOL_cs addIs [new_scheme_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);
+ (!simpset addsimps [cod_def,free_tv_subst])) 3);
by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst]
- setloop (split_tac [expand_if]))) 2);
-
+ setloop (split_tac [expand_if]))) 2);
by (Simp_tac 2);
-(** LEVEL 60 **)
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));
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);
-(** LEVEL 68 **)
-(* case na ~: free_tv t - free_tv sa *)
-by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
-(* 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);
-by (dtac eq_subst_tel_eq_free 2);
+by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,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 *)
+by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
+(* case na : free_tv t - free_tv Sa *)
+by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
+by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
+by (dtac eq_subst_scheme_list_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,de_Morgan_disj]) 2);
-(** LEVEL 74 **)
-by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
+by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
+
+by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
by (safe_tac HOL_cs );
-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_Some 1);
+by( fast_tac (HOL_cs addss !simpset) 1);
+
by ((dtac mgu_mg 1) THEN (atac 1));
by (etac exE 1);
-by (res_inst_tac [("x","rb")] exI 1);
+by (res_inst_tac [("x","Rb")] exI 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
+by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
+by (simp_tac (!simpset addsimps [subst_comp_scheme_list]) 1);
+by (simp_tac (!simpset addsimps [subst_comp_scheme_list RS sym]) 1);
+by (res_inst_tac [("A2","($ Sa ($ S A))")] ((subst_comp_scheme_list RS sym) RSN
(2,trans)) 1);
-by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
-(** LEVEL 90 **)
-by (rtac eq_free_eq_subst_tel 1);
-by ( safe_tac HOL_cs );
+by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
+by (rtac eq_free_eq_subst_scheme_list 1);
+by( safe_tac HOL_cs );
by (subgoal_tac "ma ~= na" 1);
by ((forward_tac [new_tv_W] 2) THEN (atac 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 (dtac new_tv_subst_scheme_list 2);
+by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2);
by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
by (etac conjE 2);
-by (dtac (free_tv_app_subst_tel RS subsetD) 2);
-(** LEVEL 100 **)
-by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD,
+by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2);
+by (fast_tac (set_cs addDs [W_var_geD,new_scheme_list_le,codD,
new_tv_not_free_tv]) 2);
-by (case_tac "na: free_tv t - free_tv sa" 1);
-(* case na ~: free_tv t - free_tv sa *)
+by (case_tac "na: free_tv t - free_tv Sa" 1);
+(* case na ~: free_tv t - free_tv Sa *)
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
-(* case na : free_tv t - free_tv sa *)
+(* case na : free_tv t - free_tv Sa *)
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 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 [de_Morgan_disj,free_tv_subst,dom_def]))) 1);
-(** LEVEL 106 **)
+by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
+by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
+ eq_subst_scheme_list_eq_free] addss ((!simpset addsimps
+ [free_tv_subst,dom_def]))) 1);
by (Fast_tac 1);
+(* case Let e1 e2 *)
+by (eresolve_tac has_type_casesE 1);
+by (eres_inst_tac [("x","S'")] allE 1);
+by (eres_inst_tac [("x","A")] allE 1);
+by (eres_inst_tac [("x","t1")] allE 1);
+by (eres_inst_tac [("x","n")] allE 1);
+by (mp_tac 1);
+by (mp_tac 1);
+by (safe_tac HOL_cs);
+by (Asm_simp_tac 1);
+by (eres_inst_tac [("x","R")] allE 1);
+by (eres_inst_tac [("x","gen ($ S A) t # $ S A")] allE 1);
+by (eres_inst_tac [("x","t'")] allE 1);
+by (eres_inst_tac [("x","m")] allE 1);
+by (rotate_tac 4 1);
+by (Asm_full_simp_tac 1);
+by (dtac mp 1);
+by (rtac has_type_le_env 1);
+ba 1;
+by (Simp_tac 1);
+by (rtac gen_bound_typ_instance 1);
+by (dtac mp 1);
+by (forward_tac [new_tv_compatible_W] 1);
+by (rtac sym 1);
+ba 1;
+by (fast_tac (!claset addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1);
+by (safe_tac HOL_cs);
+by (Asm_full_simp_tac 1);
+by (res_inst_tac [("x","Ra")] exI 1);
+by (simp_tac (!simpset addsimps [o_def,subst_comp_scheme_list RS sym]) 1);
qed_spec_mp "W_complete_lemma";
goal W.thy
- "!!e. [] |- e :: t' ==> (? s t. (? m. W e [] n = Ok(s,t,m)) & \
-\ (? r. t' = $r t))";
-by (cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]
+ "!!e. [] |- e :: t' ==> (? S t. (? m. W e [] n = Some(S,t,m)) & \
+\ (? R. t' = $ R t))";
+by(cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
W_complete_lemma 1);
-by (ALLGOALS Asm_full_simp_tac);
+by(ALLGOALS Asm_full_simp_tac);
qed "W_complete";