# HG changeset patch # User kleing # Date 1078187543 -3600 # Node ID b8da5f258b0424bc33ded3c02553a1b74416aa6a # Parent ee97b6463cb4d772768f43f8c91287b8a2622d2b converted to Isar diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/Generalize.ML --- a/src/HOL/MiniML/Generalize.ML Mon Mar 01 13:51:21 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,134 +0,0 @@ -(* Title: HOL/MiniML/Generalize.ML - ID: $Id$ - Author: Wolfgang Naraschewski and Tobias Nipkow - Copyright 1996 TU Muenchen -*) - -AddSEs [equalityE]; - -Goal "free_tv A = free_tv B ==> gen A t = gen B t"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "gen_eq_on_free_tv"; - -Goal "(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)"; -by (induct_tac "t" 1); -by (Asm_simp_tac 1); -by (Simp_tac 1); -by (Fast_tac 1); -qed_spec_mp "gen_without_effect"; - -Addsimps [gen_without_effect]; - -Goal "free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)"; -by (induct_tac "t" 1); -by (Simp_tac 1); -by (case_tac "nat : free_tv ($ S A)" 1); -by (Asm_simp_tac 1); -by (Fast_tac 1); -by (Asm_simp_tac 1); -by (Fast_tac 1); -by (Asm_full_simp_tac 1); -by (Fast_tac 1); -qed "free_tv_gen"; - -Addsimps [free_tv_gen]; - -Goal "free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)"; -by (Simp_tac 1); -by (Fast_tac 1); -qed "free_tv_gen_cons"; - -Addsimps [free_tv_gen_cons]; - -Goal "bound_tv (gen A t1) = (free_tv t1) - (free_tv A)"; -by (induct_tac "t1" 1); -by (Simp_tac 1); -by (case_tac "nat : free_tv A" 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Fast_tac 1); -by (Asm_simp_tac 1); -by (Fast_tac 1); -qed "bound_tv_gen"; - -Addsimps [bound_tv_gen]; - -Goal "new_tv n t --> new_tv n (gen A t)"; -by (induct_tac "t" 1); -by Auto_tac; -qed_spec_mp "new_tv_compatible_gen"; - -Goalw [gen_ML_def] "gen A t = gen_ML A t"; -by (induct_tac "t" 1); - by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1); -by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1); -qed "gen_eq_gen_ML"; - -Goal "(free_tv S) Int ((free_tv t) - (free_tv A)) = {} \ -\ --> gen ($ S A) ($ S t) = $ S (gen A t)"; -by (induct_tac "t" 1); - by (strip_tac 1); - by (case_tac "nat:(free_tv A)" 1); - by (Asm_simp_tac 1); - by (Asm_full_simp_tac 1); - by (subgoal_tac "nat ~: free_tv S" 1); - by (Fast_tac 2); - by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 1); - by (cut_facts_tac [free_tv_app_subst_scheme_list] 1); - by (Fast_tac 1); -by (Asm_simp_tac 1); -by (Blast_tac 1); -qed_spec_mp "gen_subst_commutes"; - -Goal "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -by (Fast_tac 1); -qed_spec_mp "bound_typ_inst_gen"; -Addsimps [bound_typ_inst_gen]; - -Goalw [le_type_scheme_def,is_bound_typ_instance] - "gen ($ S A) ($ S t) <= $ S (gen A t)"; -by Safe_tac; -by (rename_tac "R" 1); -by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1); -by (induct_tac "t" 1); - by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "gen_bound_typ_instance"; - -Goalw [le_type_scheme_def,is_bound_typ_instance] - "free_tv B <= free_tv A ==> gen A t <= gen B t"; -by Safe_tac; -by (rename_tac "S" 1); -by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1); -by (induct_tac "t" 1); - by (Asm_simp_tac 1); - by (Fast_tac 1); -by (Asm_simp_tac 1); -qed "free_tv_subset_gen_le"; - -Goalw [le_type_scheme_def,is_bound_typ_instance] - "new_tv n A --> \ -\ gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)"; -by (strip_tac 1); -by (etac exE 1); -by (hyp_subst_tac 1); -by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1); -by (induct_tac "t" 1); -by (Simp_tac 1); -by (case_tac "nat : free_tv A" 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (subgoal_tac "n <= n + nat" 1); -by (forw_inst_tac [("t","A")] new_tv_le 1); -by (assume_tac 1); -by (dtac new_tv_not_free_tv 1); -by (dtac new_tv_not_free_tv 1); -by (asm_simp_tac (simpset() addsimps [diff_add_inverse]) 1); -by (simp_tac (simpset() addsimps [le_add1]) 1); -by (Asm_simp_tac 1); -qed_spec_mp "gen_t_le_gen_alpha_t"; - -Addsimps [gen_t_le_gen_alpha_t]; diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/Generalize.thy --- a/src/HOL/MiniML/Generalize.thy Mon Mar 01 13:51:21 2004 +0100 +++ b/src/HOL/MiniML/Generalize.thy Tue Mar 02 01:32:23 2004 +0100 @@ -6,15 +6,15 @@ Generalizing type schemes with respect to a context *) -Generalize = Instance + +theory Generalize = Instance: (* gen: binding (generalising) the variables which are not free in the context *) -types ctxt = type_scheme list +types ctxt = "type_scheme list" consts - gen :: [ctxt, typ] => type_scheme + gen :: "[ctxt, typ] => type_scheme" primrec "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))" @@ -23,16 +23,149 @@ (* executable version of gen: Implementation with free_tv_ML *) consts - gen_ML_aux :: [nat list, typ] => type_scheme - + gen_ML_aux :: "[nat list, typ] => type_scheme" primrec "gen_ML_aux A (TVar n) = (if (n: set A) then (FVar n) else (BVar n))" "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)" consts - gen_ML :: [ctxt, typ] => type_scheme + gen_ML :: "[ctxt, typ] => type_scheme" +defs + gen_ML_def: "gen_ML A t == gen_ML_aux (free_tv_ML A) t" + + +declare equalityE [elim!] + +lemma gen_eq_on_free_tv: "free_tv A = free_tv B ==> gen A t = gen B t" +apply (induct_tac "t") +apply (simp_all (no_asm_simp)) +done + +lemma gen_without_effect [rule_format (no_asm)]: "(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)" +apply (induct_tac "t") +apply (simp (no_asm_simp)) +apply (simp (no_asm)) +apply fast +done + +declare gen_without_effect [simp] + +lemma free_tv_gen: "free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)" +apply (induct_tac "t") +apply (simp (no_asm)) +apply (case_tac "nat : free_tv ($ S A) ") +apply (simp (no_asm_simp)) +apply fast +apply (simp (no_asm_simp)) +apply fast +apply simp +apply fast +done + +declare free_tv_gen [simp] + +lemma free_tv_gen_cons: "free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)" +apply (simp (no_asm)) +apply fast +done + +declare free_tv_gen_cons [simp] + +lemma bound_tv_gen: "bound_tv (gen A t1) = (free_tv t1) - (free_tv A)" +apply (induct_tac "t1") +apply (simp (no_asm)) +apply (case_tac "nat : free_tv A") +apply (simp (no_asm_simp)) +apply (simp (no_asm_simp)) +apply fast +apply (simp (no_asm_simp)) +apply fast +done + +declare bound_tv_gen [simp] + +lemma new_tv_compatible_gen [rule_format (no_asm)]: "new_tv n t --> new_tv n (gen A t)" +apply (induct_tac "t") +apply auto +done + +lemma gen_eq_gen_ML: "gen A t = gen_ML A t" +apply (unfold gen_ML_def) +apply (induct_tac "t") + apply (simp (no_asm) add: free_tv_ML_scheme_list) +apply (simp (no_asm_simp) add: free_tv_ML_scheme_list) +done -defs - gen_ML_def "gen_ML A t == gen_ML_aux (free_tv_ML A) t" +lemma gen_subst_commutes [rule_format (no_asm)]: "(free_tv S) Int ((free_tv t) - (free_tv A)) = {} + --> gen ($ S A) ($ S t) = $ S (gen A t)" +apply (induct_tac "t") + apply (intro strip) + apply (case_tac "nat: (free_tv A) ") + apply (simp (no_asm_simp)) + apply simp + apply (subgoal_tac "nat ~: free_tv S") + prefer 2 apply (fast) + apply (simp add: free_tv_subst dom_def) + apply (cut_tac free_tv_app_subst_scheme_list) + apply fast +apply (simp (no_asm_simp)) +apply blast +done + +lemma bound_typ_inst_gen [rule_format (no_asm)]: "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t" +apply (induct_tac "t") +apply (simp_all (no_asm_simp)) +apply fast +done +declare bound_typ_inst_gen [simp] + +lemma gen_bound_typ_instance: + "gen ($ S A) ($ S t) <= $ S (gen A t)" +apply (unfold le_type_scheme_def is_bound_typ_instance) +apply safe +apply (rename_tac "R") +apply (rule_tac x = " (%a. bound_typ_inst R (gen ($S A) (S a))) " in exI) +apply (induct_tac "t") + apply (simp (no_asm)) +apply (simp (no_asm_simp)) +done + +lemma free_tv_subset_gen_le: + "free_tv B <= free_tv A ==> gen A t <= gen B t" +apply (unfold le_type_scheme_def is_bound_typ_instance) +apply safe +apply (rename_tac "S") +apply (rule_tac x = "%b. if b:free_tv A then TVar b else S b" in exI) +apply (induct_tac "t") + apply (simp (no_asm_simp)) + apply fast +apply (simp (no_asm_simp)) +done + +lemma gen_t_le_gen_alpha_t [rule_format (no_asm)]: + "new_tv n A --> + gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)" +apply (unfold le_type_scheme_def is_bound_typ_instance) +apply (intro strip) +apply (erule exE) +apply (hypsubst) +apply (rule_tac x = " (%x. S (if n <= x then x - n else x))" in exI) +apply (induct_tac "t") +apply (simp (no_asm)) +apply (case_tac "nat : free_tv A") +apply (simp (no_asm_simp)) +apply (simp (no_asm_simp)) +apply (subgoal_tac "n <= n + nat") +apply (frule_tac t = "A" in new_tv_le) +apply assumption +apply (drule new_tv_not_free_tv) +apply (drule new_tv_not_free_tv) +apply (simp (no_asm_simp) add: diff_add_inverse) +apply (simp (no_asm) add: le_add1) +apply (simp (no_asm_simp)) +done + +declare gen_t_le_gen_alpha_t [simp] + end diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/Instance.ML --- a/src/HOL/MiniML/Instance.ML Mon Mar 01 13:51:21 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,278 +0,0 @@ -(* Title: HOL/MiniML/Instance.ML - ID: $Id$ - Author: Wolfgang Naraschewski and Tobias Nipkow - Copyright 1996 TU Muenchen -*) - -(* lemmatas for instatiation *) - - -(* lemmatas for bound_typ_inst *) - -Goal "bound_typ_inst S (mk_scheme t) = t"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "bound_typ_inst_mk_scheme"; - -Addsimps [bound_typ_inst_mk_scheme]; - -Goal "bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)"; -by (induct_tac "sch" 1); -by (ALLGOALS Asm_full_simp_tac); -qed "bound_typ_inst_composed_subst"; - -Addsimps [bound_typ_inst_composed_subst]; - -Goal "S = S' ==> sch = sch' ==> bound_typ_inst S sch = bound_typ_inst S' sch'"; -by (Asm_full_simp_tac 1); -qed "bound_typ_inst_eq"; - - - -(* lemmatas for bound_scheme_inst *) - -Goal "bound_scheme_inst B (mk_scheme t) = mk_scheme t"; -by (induct_tac "t" 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "bound_scheme_inst_mk_scheme"; - -Addsimps [bound_scheme_inst_mk_scheme]; - -Goal "$S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))"; -by (induct_tac "sch" 1); -by (Simp_tac 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "substitution_lemma"; - -Goal "!t. mk_scheme t = bound_scheme_inst B sch --> \ -\ (? S. !x:bound_tv sch. B x = mk_scheme (S x))"; -by (induct_tac "sch" 1); -by (Simp_tac 1); -by Safe_tac; -by (rtac exI 1); -by (rtac ballI 1); -by (rtac sym 1); -by (Asm_full_simp_tac 1); -by (Asm_full_simp_tac 1); -by (dtac mk_scheme_Fun 1); -by (REPEAT (etac exE 1)); -by (etac conjE 1); -by (dtac sym 1); -by (dtac sym 1); -by (REPEAT ((dtac mp 1) THEN (Fast_tac 1))); -by Safe_tac; -by (rename_tac "S1 S2" 1); -by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1); -by (Auto_tac); -qed_spec_mp "bound_scheme_inst_type"; - - -(* lemmas for subst_to_scheme *) - -Goal "new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \ -\ (bound_typ_inst (%k. TVar (k + n)) sch) = sch"; -by (induct_tac "sch" 1); -by (simp_tac (simpset() addsimps [le_def]) 1); -by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1); -by (Asm_simp_tac 1); -qed_spec_mp "subst_to_scheme_inverse"; - -Goal "t = t' ==> \ -\ subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t = \ -\ subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t'"; -by (Fast_tac 1); -val aux = result (); - -Goal "new_tv n sch --> \ -\ subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \ -\ bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch"; -by (induct_tac "sch" 1); -by Auto_tac; -val aux2 = result () RS mp; - - -(* lemmata for <= *) - -Goalw [le_type_scheme_def,is_bound_typ_instance] - "!!(sch::type_scheme) sch'. \ -\ (sch' <= sch) = (? B. sch' = bound_scheme_inst B sch)"; -by (rtac iffI 1); -by (cut_inst_tac [("sch","sch")] fresh_variable_type_schemes 1); -by (cut_inst_tac [("sch","sch'")] fresh_variable_type_schemes 1); -by (dtac make_one_new_out_of_two 1); -by (assume_tac 1); -by (thin_tac "? n. new_tv n sch'" 1); -by (etac exE 1); -by (etac allE 1); -by (dtac mp 1); -by (res_inst_tac [("x","(%k. TVar (k + n))")] exI 1); -by (rtac refl 1); -by (etac exE 1); -by (REPEAT (etac conjE 1)); -by (dres_inst_tac [("n","n")] aux 1); -by (asm_full_simp_tac (simpset() addsimps [subst_to_scheme_inverse]) 1); -by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1); -by (asm_simp_tac (simpset() addsimps [aux2]) 1); -by Safe_tac; -by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1); -by (induct_tac "sch" 1); -by (Simp_tac 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "le_type_scheme_def2"; - -Goalw [is_bound_typ_instance] "(mk_scheme t) <= sch = t <| sch"; -by (simp_tac (simpset() addsimps [le_type_scheme_def2]) 1); -by (rtac iffI 1); -by (etac exE 1); -by (ftac bound_scheme_inst_type 1); -by (etac exE 1); -by (rtac exI 1); -by (rtac mk_scheme_injective 1); -by (Asm_full_simp_tac 1); -by (rotate_tac 1 1); -by (rtac mp 1); -by (assume_tac 2); -by (induct_tac "sch" 1); -by (Simp_tac 1); -by (Asm_full_simp_tac 1); -by (Fast_tac 1); -by (strip_tac 1); -by (Asm_full_simp_tac 1); -by (etac exE 1); -by (Asm_full_simp_tac 1); -by (rtac exI 1); -by (induct_tac "sch" 1); -by (Simp_tac 1); -by (Simp_tac 1); -by (Asm_full_simp_tac 1); -qed_spec_mp "le_type_eq_is_bound_typ_instance"; - -Goalw [le_env_def] - "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)"; -by (Simp_tac 1); -by (rtac iffI 1); - by (SELECT_GOAL Safe_tac 1); - by (eres_inst_tac [("x","0")] allE 1); - by (Asm_full_simp_tac 1); - by (eres_inst_tac [("x","Suc i")] allE 1); - by (Asm_full_simp_tac 1); -by (rtac conjI 1); - by (Fast_tac 1); -by (rtac allI 1); -by (induct_tac "i" 1); -by (ALLGOALS Asm_simp_tac); -qed "le_env_Cons"; -AddIffs [le_env_Cons]; - -Goalw [is_bound_typ_instance]"t <| sch ==> $S t <| $S sch"; -by (etac exE 1); -by (rename_tac "SA" 1); -by (hyp_subst_tac 1); -by (res_inst_tac [("x","$S o SA")] exI 1); -by (Simp_tac 1); -qed "is_bound_typ_instance_closed_subst"; - -Goal "!!(sch::type_scheme) sch'. sch' <= sch ==> $S sch' <= $ S sch"; -by (asm_full_simp_tac (simpset() addsimps [le_type_scheme_def2]) 1); -by (etac exE 1); -by (asm_full_simp_tac (simpset() addsimps [substitution_lemma]) 1); -by (Fast_tac 1); -qed "S_compatible_le_scheme"; - -Goalw [le_env_def,app_subst_list] - "!!(A::type_scheme list) A'. A' <= A ==> $S A' <= $ S A"; -by (simp_tac (simpset() addcongs [conj_cong]) 1); -by (fast_tac (claset() addSIs [S_compatible_le_scheme]) 1); -qed "S_compatible_le_scheme_lists"; - -Goalw [le_type_scheme_def] "[| t <| sch; sch <= sch' |] ==> t <| sch'"; -by (Fast_tac 1); -qed "bound_typ_instance_trans"; - -Goalw [le_type_scheme_def] "sch <= (sch::type_scheme)"; -by (Fast_tac 1); -qed "le_type_scheme_refl"; -AddIffs [le_type_scheme_refl]; - -Goalw [le_env_def] "A <= (A::type_scheme list)"; -by (Fast_tac 1); -qed "le_env_refl"; -AddIffs [le_env_refl]; - -Goalw [le_type_scheme_def,is_bound_typ_instance] "sch <= BVar n"; -by (strip_tac 1); -by (res_inst_tac [("x","%a. t")]exI 1); -by (Simp_tac 1); -qed "bound_typ_instance_BVar"; -AddIffs [bound_typ_instance_BVar]; - -Goalw [le_type_scheme_def,is_bound_typ_instance] - "(sch <= FVar n) = (sch = FVar n)"; -by (induct_tac "sch" 1); - by (Simp_tac 1); - by (Simp_tac 1); - by (Fast_tac 1); -by (Asm_full_simp_tac 1); -by (Fast_tac 1); -qed "le_FVar"; -Addsimps [le_FVar]; - -Goalw [le_type_scheme_def,is_bound_typ_instance] "~(FVar n <= sch1 =-> sch2)"; -by (Simp_tac 1); -qed "not_FVar_le_Fun"; -AddIffs [not_FVar_le_Fun]; - -Goalw [le_type_scheme_def,is_bound_typ_instance] "~(BVar n <= sch1 =-> sch2)"; -by (Simp_tac 1); -by (res_inst_tac [("x","TVar n")] exI 1); -by (Simp_tac 1); -by (Fast_tac 1); -qed "not_BVar_le_Fun"; -AddIffs [not_BVar_le_Fun]; - -Goalw [le_type_scheme_def,is_bound_typ_instance] - "(sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'"; -by (fast_tac (claset() addss simpset()) 1); -qed "Fun_le_FunD"; - -Goal "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)"; -by (induct_tac "sch'" 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Fast_tac 1); -qed_spec_mp "scheme_le_Fun"; - -Goal "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch"; -by (induct_tac "sch" 1); - by (rtac allI 1); - by (induct_tac "sch'" 1); - by (Simp_tac 1); - by (Simp_tac 1); - by (Simp_tac 1); - by (rtac allI 1); - by (induct_tac "sch'" 1); - by (Simp_tac 1); - by (Simp_tac 1); - by (Simp_tac 1); -by (rtac allI 1); -by (induct_tac "sch'" 1); - by (Simp_tac 1); - by (Simp_tac 1); -by (Asm_full_simp_tac 1); -by (strip_tac 1); -by (dtac Fun_le_FunD 1); -by (Fast_tac 1); -qed_spec_mp "le_type_scheme_free_tv"; - -Goal "!A::type_scheme list. A <= B --> free_tv B <= free_tv A"; -by (induct_tac "B" 1); - by (Simp_tac 1); -by (rtac allI 1); -by (induct_tac "A" 1); - by (simp_tac (simpset() addsimps [le_env_def]) 1); -by (Simp_tac 1); -by (fast_tac (claset() addDs [le_type_scheme_free_tv]) 1); -qed_spec_mp "le_env_free_tv"; diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/Instance.thy --- a/src/HOL/MiniML/Instance.thy Mon Mar 01 13:51:21 2004 +0100 +++ b/src/HOL/MiniML/Instance.thy Tue Mar 02 01:32:23 2004 +0100 @@ -6,13 +6,13 @@ Instances of type schemes *) -Instance = Type + +theory Instance = Type: (* generic instances of a type scheme *) consts - bound_typ_inst :: [subst, type_scheme] => typ + bound_typ_inst :: "[subst, type_scheme] => typ" primrec "bound_typ_inst S (FVar n) = (TVar n)" @@ -20,7 +20,7 @@ "bound_typ_inst S (sch1 =-> sch2) = ((bound_typ_inst S sch1) -> (bound_typ_inst S sch2))" consts - bound_scheme_inst :: [nat => type_scheme, type_scheme] => type_scheme + bound_scheme_inst :: "[nat => type_scheme, type_scheme] => type_scheme" primrec "bound_scheme_inst S (FVar n) = (FVar n)" @@ -28,22 +28,314 @@ "bound_scheme_inst S (sch1 =-> sch2) = ((bound_scheme_inst S sch1) =-> (bound_scheme_inst S sch2))" consts - "<|" :: [typ, type_scheme] => bool (infixr 70) + "<|" :: "[typ, type_scheme] => bool" (infixr 70) defs - is_bound_typ_instance "t <| sch == ? S. t = (bound_typ_inst S sch)" + is_bound_typ_instance: "t <| sch == ? S. t = (bound_typ_inst S sch)" -instance type_scheme :: ord -defs le_type_scheme_def "sch' <= (sch::type_scheme) == !t. t <| sch' --> t <| sch" +instance type_scheme :: ord .. +defs le_type_scheme_def: "sch' <= (sch::type_scheme) == !t. t <| sch' --> t <| sch" consts - subst_to_scheme :: [nat => type_scheme, typ] => type_scheme + subst_to_scheme :: "[nat => type_scheme, typ] => type_scheme" primrec "subst_to_scheme B (TVar n) = (B n)" "subst_to_scheme B (t1 -> t2) = ((subst_to_scheme B t1) =-> (subst_to_scheme B t2))" -instance list :: (ord)ord -defs le_env_def +instance list :: (ord)ord .. +defs le_env_def: "A <= B == length B = length A & (!i. i < length A --> A!i <= B!i)" + +(* lemmatas for instatiation *) + + +(* lemmatas for bound_typ_inst *) + +lemma bound_typ_inst_mk_scheme: "bound_typ_inst S (mk_scheme t) = t" +apply (induct_tac "t") +apply (simp_all (no_asm_simp)) +done + +declare bound_typ_inst_mk_scheme [simp] + +lemma bound_typ_inst_composed_subst: "bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)" +apply (induct_tac "sch") +apply simp_all +done + +declare bound_typ_inst_composed_subst [simp] + +lemma bound_typ_inst_eq: "S = S' ==> sch = sch' ==> bound_typ_inst S sch = bound_typ_inst S' sch'" +apply simp +done + + + +(* lemmatas for bound_scheme_inst *) + +lemma bound_scheme_inst_mk_scheme: "bound_scheme_inst B (mk_scheme t) = mk_scheme t" +apply (induct_tac "t") +apply (simp (no_asm)) +apply (simp (no_asm_simp)) +done + +declare bound_scheme_inst_mk_scheme [simp] + +lemma substitution_lemma: "$S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))" +apply (induct_tac "sch") +apply (simp (no_asm)) +apply (simp (no_asm)) +apply (simp (no_asm_simp)) +done + +lemma bound_scheme_inst_type [rule_format (no_asm)]: "!t. mk_scheme t = bound_scheme_inst B sch --> + (? S. !x:bound_tv sch. B x = mk_scheme (S x))" +apply (induct_tac "sch") +apply (simp (no_asm)) +apply safe +apply (rule exI) +apply (rule ballI) +apply (rule sym) +apply simp +apply simp +apply (drule mk_scheme_Fun) +apply (erule exE)+ +apply (erule conjE) +apply (drule sym) +apply (drule sym) +apply (drule mp, fast)+ +apply safe +apply (rename_tac S1 S2) +apply (rule_tac x = "%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x) " in exI) +apply auto +done + + +(* lemmas for subst_to_scheme *) + +lemma subst_to_scheme_inverse [rule_format (no_asm)]: "new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) + (bound_typ_inst (%k. TVar (k + n)) sch) = sch" +apply (induct_tac "sch") +apply (simp (no_asm) add: le_def) +apply (simp (no_asm) add: le_add2 diff_add_inverse2) +apply (simp (no_asm_simp)) +done + +lemma aux: "t = t' ==> + subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t = + subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t'" +apply fast +done + +lemma aux2 [rule_format]: "new_tv n sch --> + subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = + bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch" +apply (induct_tac "sch") +apply auto +done + + +(* lemmata for <= *) + +lemma le_type_scheme_def2: + "!!(sch::type_scheme) sch'. + (sch' <= sch) = (? B. sch' = bound_scheme_inst B sch)" + +apply (unfold le_type_scheme_def is_bound_typ_instance) +apply (rule iffI) +apply (cut_tac sch = "sch" in fresh_variable_type_schemes) +apply (cut_tac sch = "sch'" in fresh_variable_type_schemes) +apply (drule make_one_new_out_of_two) +apply assumption +apply (erule_tac V = "? n. new_tv n sch'" in thin_rl) +apply (erule exE) +apply (erule allE) +apply (drule mp) +apply (rule_tac x = " (%k. TVar (k + n))" in exI) +apply (rule refl) +apply (erule exE) +apply (erule conjE)+ +apply (drule_tac n = "n" in aux) +apply (simp add: subst_to_scheme_inverse) +apply (rule_tac x = " (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S" in exI) +apply (simp (no_asm_simp) add: aux2) +apply safe +apply (rule_tac x = "%n. bound_typ_inst S (B n) " in exI) +apply (induct_tac "sch") +apply (simp (no_asm)) +apply (simp (no_asm)) +apply (simp (no_asm_simp)) +done + +lemma le_type_eq_is_bound_typ_instance [rule_format (no_asm)]: "(mk_scheme t) <= sch = t <| sch" +apply (unfold is_bound_typ_instance) +apply (simp (no_asm) add: le_type_scheme_def2) +apply (rule iffI) +apply (erule exE) +apply (frule bound_scheme_inst_type) +apply (erule exE) +apply (rule exI) +apply (rule mk_scheme_injective) +apply simp +apply (rotate_tac 1) +apply (rule mp) +prefer 2 apply (assumption) +apply (induct_tac "sch") +apply (simp (no_asm)) +apply simp +apply fast +apply (intro strip) +apply simp +apply (erule exE) +apply simp +apply (rule exI) +apply (induct_tac "sch") +apply (simp (no_asm)) +apply (simp (no_asm)) +apply simp +done + +lemma le_env_Cons: + "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)" +apply (unfold le_env_def) +apply (simp (no_asm)) +apply (rule iffI) + apply clarify + apply (rule conjI) + apply (erule_tac x = "0" in allE) + apply simp + apply (rule conjI, assumption) + apply clarify + apply (erule_tac x = "Suc i" in allE) + apply simp +apply (rule conjI) + apply fast +apply (rule allI) +apply (induct_tac "i") +apply (simp_all (no_asm_simp)) +done +declare le_env_Cons [iff] + +lemma is_bound_typ_instance_closed_subst: "t <| sch ==> $S t <| $S sch" +apply (unfold is_bound_typ_instance) +apply (erule exE) +apply (rename_tac "SA") +apply (simp) +apply (rule_tac x = "$S o SA" in exI) +apply (simp (no_asm)) +done + +lemma S_compatible_le_scheme: "!!(sch::type_scheme) sch'. sch' <= sch ==> $S sch' <= $ S sch" +apply (simp add: le_type_scheme_def2) +apply (erule exE) +apply (simp add: substitution_lemma) +apply fast +done + +lemma S_compatible_le_scheme_lists: + "!!(A::type_scheme list) A'. A' <= A ==> $S A' <= $ S A" +apply (unfold le_env_def app_subst_list) +apply (simp (no_asm) cong add: conj_cong) +apply (fast intro!: S_compatible_le_scheme) +done + +lemma bound_typ_instance_trans: "[| t <| sch; sch <= sch' |] ==> t <| sch'" +apply (unfold le_type_scheme_def) +apply fast +done + +lemma le_type_scheme_refl: "sch <= (sch::type_scheme)" +apply (unfold le_type_scheme_def) +apply fast +done +declare le_type_scheme_refl [iff] + +lemma le_env_refl: "A <= (A::type_scheme list)" +apply (unfold le_env_def) +apply fast +done +declare le_env_refl [iff] + +lemma bound_typ_instance_BVar: "sch <= BVar n" +apply (unfold le_type_scheme_def is_bound_typ_instance) +apply (intro strip) +apply (rule_tac x = "%a. t" in exI) +apply (simp (no_asm)) +done +declare bound_typ_instance_BVar [iff] + +lemma le_FVar: + "(sch <= FVar n) = (sch = FVar n)" +apply (unfold le_type_scheme_def is_bound_typ_instance) +apply (induct_tac "sch") + apply (simp (no_asm)) + apply (simp (no_asm)) + apply fast +apply simp +apply fast +done +declare le_FVar [simp] + +lemma not_FVar_le_Fun: "~(FVar n <= sch1 =-> sch2)" +apply (unfold le_type_scheme_def is_bound_typ_instance) +apply (simp (no_asm)) +done +declare not_FVar_le_Fun [iff] + +lemma not_BVar_le_Fun: "~(BVar n <= sch1 =-> sch2)" +apply (unfold le_type_scheme_def is_bound_typ_instance) +apply (simp (no_asm)) +apply (rule_tac x = "TVar n" in exI) +apply (simp (no_asm)) +apply fast +done +declare not_BVar_le_Fun [iff] + +lemma Fun_le_FunD: + "(sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'" +apply (unfold le_type_scheme_def is_bound_typ_instance) +apply (fastsimp) +done + +lemma scheme_le_Fun [rule_format (no_asm)]: "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)" +apply (induct_tac "sch'") +apply (simp (no_asm_simp)) +apply (simp (no_asm_simp)) +apply fast +done + +lemma le_type_scheme_free_tv [rule_format (no_asm)]: "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch" +apply (induct_tac "sch") + apply (rule allI) + apply (induct_tac "sch'") + apply (simp (no_asm)) + apply (simp (no_asm)) + apply (simp (no_asm)) + apply (rule allI) + apply (induct_tac "sch'") + apply (simp (no_asm)) + apply (simp (no_asm)) + apply (simp (no_asm)) +apply (rule allI) +apply (induct_tac "sch'") + apply (simp (no_asm)) + apply (simp (no_asm)) +apply simp +apply (intro strip) +apply (drule Fun_le_FunD) +apply fast +done + +lemma le_env_free_tv [rule_format (no_asm)]: "!A::type_scheme list. A <= B --> free_tv B <= free_tv A" +apply (induct_tac "B") + apply (simp (no_asm)) +apply (rule allI) +apply (induct_tac "A") + apply (simp (no_asm) add: le_env_def) +apply (simp (no_asm)) +apply (fast dest: le_type_scheme_free_tv) +done + + end diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/Maybe.ML --- a/src/HOL/MiniML/Maybe.ML Mon Mar 01 13:51:21 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -(* Title: HOL/MiniML/Maybe.ML - ID: $Id$ - Author: Wolfgang Naraschewski and Tobias Nipkow - Copyright 1996 TU Muenchen -*) - -(* constructor laws for option_bind *) -Goalw [option_bind_def] "option_bind (Some s) f = (f s)"; -by (Simp_tac 1); -qed "option_bind_Some"; - -Goalw [option_bind_def] "option_bind None f = None"; -by (Simp_tac 1); -qed "option_bind_None"; - -Addsimps [option_bind_Some,option_bind_None]; - -(* expansion of option_bind *) -Goalw [option_bind_def] "P(option_bind res f) = \ -\ ((res = None --> P None) & (!s. res = Some s --> P(f s)))"; -by (rtac option.split 1); -qed "split_option_bind"; - -Goal - "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))"; -by (simp_tac (simpset() addsplits [split_option_bind]) 1); -qed "option_bind_eq_None"; - -Addsimps [option_bind_eq_None]; - -(* auxiliary lemma *) -Goal "(y = Some x) = (Some x = y)"; -by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1); -qed "rotate_Some"; diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/Maybe.thy --- a/src/HOL/MiniML/Maybe.thy Mon Mar 01 13:51:21 2004 +0100 +++ b/src/HOL/MiniML/Maybe.thy Tue Mar 02 01:32:23 2004 +0100 @@ -6,13 +6,46 @@ Universal error monad. *) -Maybe = Main + +theory Maybe = Main: constdefs - option_bind :: ['a option, 'a => 'b option] => 'b option + option_bind :: "['a option, 'a => 'b option] => 'b option" "option_bind m f == case m of None => None | Some r => f r" -syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0) +syntax "@option_bind" :: "[pttrns,'a option,'b] => 'c" ("(_ := _;//_)" 0) translations "P := E; F" == "option_bind E (%P. F)" + +(* constructor laws for option_bind *) +lemma option_bind_Some: "option_bind (Some s) f = (f s)" +apply (unfold option_bind_def) +apply (simp (no_asm)) +done + +lemma option_bind_None: "option_bind None f = None" +apply (unfold option_bind_def) +apply (simp (no_asm)) +done + +declare option_bind_Some [simp] option_bind_None [simp] + +(* expansion of option_bind *) +lemma split_option_bind: "P(option_bind res f) = + ((res = None --> P None) & (!s. res = Some s --> P(f s)))" +apply (unfold option_bind_def) +apply (rule option.split) +done + +lemma option_bind_eq_None: + "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))" +apply (simp (no_asm) split add: split_option_bind) +done + +declare option_bind_eq_None [simp] + +(* auxiliary lemma *) +lemma rotate_Some: "(y = Some x) = (Some x = y)" +apply ( simp (no_asm) add: eq_sym_conv) +done + end diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/MiniML.ML --- a/src/HOL/MiniML/MiniML.ML Mon Mar 01 13:51:21 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,243 +0,0 @@ -(* Title: HOL/MiniML/MiniML.ML - ID: $Id$ - Author: Dieter Nazareth and Tobias Nipkow - Copyright 1995 TU Muenchen -*) - -Addsimps has_type.intrs; -Addsimps [Un_upper1,Un_upper2]; - -Addsimps [is_bound_typ_instance_closed_subst]; - - -Goal "!!t::typ. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t = $S t"; -by (rtac typ_substitutions_only_on_free_variables 1); -by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1); -qed "s'_t_equals_s_t"; - -Addsimps [s'_t_equals_s_t]; - -Goal "!!A::type_scheme list. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A = $S A"; -by (rtac scheme_list_substitutions_only_on_free_variables 1); -by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1); -qed "s'_a_equals_s_a"; - -Addsimps [s'_a_equals_s_a]; - -Goal - "$(%n. if n : (free_tv A) Un (free_tv t) then S n else TVar n) A |- \ -\ e :: $(%n. if n : (free_tv A) Un (free_tv t) then S n else TVar n) t \ -\ ==> $S A |- e :: $S t"; - -by (res_inst_tac [("P","%A. A |- e :: $S t")] ssubst 1); -by (rtac (s'_a_equals_s_a RS sym) 1); -by (res_inst_tac [("P","%t. $ (%n. if n : free_tv A Un free_tv (?t1 S) then S n else TVar n) A |- e :: t")] ssubst 1); -by (rtac (s'_t_equals_s_t RS sym) 1); -by (Asm_full_simp_tac 1); -qed "replace_s_by_s'"; - -Goal "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) 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 "alpha_A'"; - -Goal "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = A"; -by (rtac (alpha_A' RS ssubst) 1); -by (Asm_full_simp_tac 1); -qed "alpha_A"; - -Goal "$ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)"; -by (induct_tac "t" 1); -by (ALLGOALS (Asm_full_simp_tac)); -qed "S_o_alpha_typ"; - -Goal "$ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)"; -by (induct_tac "t" 1); -by (ALLGOALS (Asm_full_simp_tac)); -val S_o_alpha_typ' = result (); - -Goal "$ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)"; -by (induct_tac "sch" 1); -by (ALLGOALS (Asm_full_simp_tac)); -qed "S_o_alpha_type_scheme"; - -Goal "$ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)"; -by (induct_tac "A" 1); -by (ALLGOALS (Asm_full_simp_tac)); -by (rtac (rewrite_rule [o_def] S_o_alpha_type_scheme) 1); -qed "S_o_alpha_type_scheme_list"; - -Goal "!!A::type_scheme list. \ -\ $ (%n. if n : free_tv A Un free_tv t then S n else TVar n) A = \ -\ $ ((%x. if x : free_tv A Un free_tv t then S x else TVar x) o \ -\ (%x. if x : free_tv A then x else n + x)) A"; -by (stac S_o_alpha_type_scheme_list 1); -by (stac alpha_A 1); -by (rtac refl 1); -qed "S'_A_eq_S'_alpha_A"; - -Goalw [free_tv_subst,dom_def] - "dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \ -\ free_tv A Un free_tv t"; -by (Simp_tac 1); -by (Fast_tac 1); -qed "dom_S'"; - -Goalw [free_tv_subst,cod_def,subset_def] - "!!(A::type_scheme list) (t::typ). \ -\ cod (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \ -\ free_tv ($ S A) Un free_tv ($ S t)"; -by (rtac ballI 1); -by (etac UN_E 1); -by (dtac (dom_S' RS subsetD) 1); -by (Asm_full_simp_tac 1); -by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_scheme_lists] - addIs [free_tv_of_substitutions_extend_to_types RS subsetD]) 1); -qed "cod_S'"; - -Goalw [free_tv_subst] - "!!(A::type_scheme list) (t::typ). \ -\ free_tv (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \ -\ free_tv A Un free_tv ($ S A) Un free_tv t Un free_tv ($ S t)"; -by (fast_tac (claset() addDs [dom_S' RS subsetD,cod_S' RS subsetD]) 1); -qed "free_tv_S'"; - -Goal "!!t1::typ. \ -\ (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \ -\ {x. ? y. x = n + y}"; -by (induct_tac "t1" 1); -by (Simp_tac 1); -by (Fast_tac 1); -by (Simp_tac 1); -by (Fast_tac 1); -qed "free_tv_alpha"; - -Goal "!!(k::nat). n <= n + k"; -by (induct_thm_tac nat_induct "k" 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -val aux_plus = result(); - -Addsimps [aux_plus]; - -Goal "!!t::typ. new_tv n t ==> {x. ? y. x = n + y} Int free_tv t = {}"; -by Safe_tac; -by (cut_facts_tac [aux_plus] 1); -by (dtac new_tv_le 1); -by (assume_tac 1); -by (rotate_tac 1 1); -by (dtac new_tv_not_free_tv 1); -by (Fast_tac 1); -val new_tv_Int_free_tv_empty_type = result (); - -Goal "!!sch::type_scheme. new_tv n sch ==> {x. ? y. x = n + y} Int free_tv sch = {}"; -by Safe_tac; -by (cut_facts_tac [aux_plus] 1); -by (dtac new_tv_le 1); -by (assume_tac 1); -by (rotate_tac 1 1); -by (dtac new_tv_not_free_tv 1); -by (Fast_tac 1); -val new_tv_Int_free_tv_empty_scheme = result (); - -Goal "!A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}"; -by (rtac allI 1); -by (induct_tac "A" 1); -by (Simp_tac 1); -by (Simp_tac 1); -by (fast_tac (claset() addDs [new_tv_Int_free_tv_empty_scheme ]) 1); -val new_tv_Int_free_tv_empty_scheme_list = result (); - -Goalw [le_type_scheme_def,is_bound_typ_instance] - "new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)"; -by (strip_tac 1); -by (etac exE 1); -by (hyp_subst_tac 1); -by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1); -by (induct_tac "t" 1); -by (Simp_tac 1); -by (case_tac "nat : free_tv A" 1); -by (Asm_simp_tac 1); -by (subgoal_tac "n <= n + nat" 1); -by (dtac new_tv_le 1); -by (assume_tac 1); -by (dtac new_tv_not_free_tv 1); -by (dtac new_tv_not_free_tv 1); -by (asm_simp_tac (simpset() addsimps [diff_add_inverse ]) 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed_spec_mp "gen_t_le_gen_alpha_t"; - -AddSIs has_type.intrs; - -Goal "A |- e::t ==> !B. A <= B --> B |- e::t"; -by (etac has_type.induct 1); - by (simp_tac (simpset() addsimps [le_env_def]) 1); - by (fast_tac (claset() addEs [bound_typ_instance_trans] addss simpset()) 1); - by (Asm_full_simp_tac 1); - by (Fast_tac 1); -by (slow_tac (claset() addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1); -qed_spec_mp "has_type_le_env"; - -(* has_type is closed w.r.t. substitution *) -Goal "A |- e :: t ==> !S. $S A |- e :: $S t"; -by (etac has_type.induct 1); -(* case VarI *) - by (rtac allI 1); - by (rtac has_type.VarI 1); - by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1); - by (asm_simp_tac (simpset() addsimps [app_subst_list]) 1); - (* case AbsI *) - by (rtac allI 1); - by (Simp_tac 1); - by (rtac has_type.AbsI 1); - by (Asm_full_simp_tac 1); - (* case AppI *) - by (rtac allI 1); - by (rtac has_type.AppI 1); - by (Asm_full_simp_tac 1); - by (etac spec 1); - by (etac spec 1); -(* case LetI *) -by (rtac allI 1); -by (rtac replace_s_by_s' 1); -by (cut_inst_tac [("A","$ S A"), - ("A'","A"), - ("t","t"), - ("t'","$ S t")] - ex_fresh_variable 1); -by (etac exE 1); -by (REPEAT (etac conjE 1)); -by (res_inst_tac [("t1.0","$((%x. if x : free_tv A Un free_tv t then S x else TVar x) o \ -\ (%x. if x : free_tv A then x else n + x)) t1")] - has_type.LETI 1); - by (dres_inst_tac [("x","(%x. if x : free_tv A Un free_tv t then S x else TVar x) o \ -\ (%x. if x : free_tv A then x else n + x)")] spec 1); - by (stac (S'_A_eq_S'_alpha_A) 1); - by (assume_tac 1); -by (stac S_o_alpha_typ 1); -by (stac gen_subst_commutes 1); - by (rtac subset_antisym 1); - by (rtac subsetI 1); - by (etac IntE 1); - by (dtac (free_tv_S' RS subsetD) 1); - by (dtac (free_tv_alpha RS subsetD) 1); - by (asm_full_simp_tac (simpset() delsimps [full_SetCompr_eq]) 1); - by (etac exE 1); - by (hyp_subst_tac 1); - by (subgoal_tac "new_tv (n + y) ($ S A)" 1); - by (subgoal_tac "new_tv (n + y) ($ S t)" 1); - by (subgoal_tac "new_tv (n + y) A" 1); - by (subgoal_tac "new_tv (n + y) t" 1); - by (REPEAT (dtac new_tv_not_free_tv 1)); - by (Fast_tac 1); - by (REPEAT ((rtac new_tv_le 1) THEN (assume_tac 2) THEN (Simp_tac 1))); - by (Fast_tac 1); -by (rtac has_type_le_env 1); - by (dtac spec 1); - by (dtac spec 1); - by (assume_tac 1); -by (rtac (app_subst_Cons RS subst) 1); -by (rtac S_compatible_le_scheme_lists 1); -by (Asm_simp_tac 1); -qed "has_type_cl_sub"; diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/MiniML.thy --- a/src/HOL/MiniML/MiniML.thy Mon Mar 01 13:51:21 2004 +0100 +++ b/src/HOL/MiniML/MiniML.thy Tue Mar 02 01:32:23 2004 +0100 @@ -1,12 +1,12 @@ (* Title: HOL/MiniML/MiniML.thy ID: $Id$ - Author: Wolfgang Naraschewski and Tobias Nipkow + Author: Dieter Nazareth, Wolfgang Naraschewski and Tobias Nipkow Copyright 1996 TU Muenchen Mini_ML with type inference rules. *) -MiniML = Generalize + +theory MiniML = Generalize: (* expressions *) datatype @@ -16,17 +16,256 @@ consts has_type :: "(ctxt * expr * typ)set" syntax - "@has_type" :: [ctxt, expr, typ] => bool + "@has_type" :: "[ctxt, expr, typ] => bool" ("((_) |-/ (_) :: (_))" [60,0,60] 60) translations "A |- e :: t" == "(A,e,t):has_type" inductive has_type -intrs - VarI "[| n < length A; t <| A!n |] ==> A |- Var n :: t" - AbsI "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2" - AppI "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] - ==> A |- App e1 e2 :: t1" - LETI "[| A |- e1 :: t1; (gen A t1)#A |- e2 :: t |] ==> A |- LET e1 e2 :: t" +intros + VarI: "[| n < length A; t <| A!n |] ==> A |- Var n :: t" + AbsI: "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2" + AppI: "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] + ==> A |- App e1 e2 :: t1" + LETI: "[| A |- e1 :: t1; (gen A t1)#A |- e2 :: t |] ==> A |- LET e1 e2 :: t" + + +declare has_type.intros [simp] +declare Un_upper1 [simp] Un_upper2 [simp] + +declare is_bound_typ_instance_closed_subst [simp] + + +lemma s'_t_equals_s_t: "!!t::typ. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t = $S t" +apply (rule typ_substitutions_only_on_free_variables) +apply (simp add: Ball_def) +done + +declare s'_t_equals_s_t [simp] + +lemma s'_a_equals_s_a: "!!A::type_scheme list. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A = $S A" +apply (rule scheme_list_substitutions_only_on_free_variables) +apply (simp add: Ball_def) +done + +declare s'_a_equals_s_a [simp] + +lemma replace_s_by_s': + "$(%n. if n : (free_tv A) Un (free_tv t) then S n else TVar n) A |- + e :: $(%n. if n : (free_tv A) Un (free_tv t) then S n else TVar n) t + ==> $S A |- e :: $S t" + +apply (rule_tac P = "%A. A |- e :: $S t" in ssubst) +apply (rule s'_a_equals_s_a [symmetric]) +apply (rule_tac P = "%t. $ (%n. if n : free_tv A Un free_tv (?t1 S) then S n else TVar n) A |- e :: t" in ssubst) +apply (rule s'_t_equals_s_t [symmetric]) +apply simp +done + +lemma alpha_A': "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = $ id_subst A" +apply (rule scheme_list_substitutions_only_on_free_variables) +apply (simp add: id_subst_def) +done + +lemma alpha_A: "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = A" +apply (rule alpha_A' [THEN ssubst]) +apply simp +done + +lemma S_o_alpha_typ: "$ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)" +apply (induct_tac "t") +apply (simp_all) +done + +lemma S_o_alpha_typ': "$ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)" +apply (induct_tac "t") +apply (simp_all) +done + +lemma S_o_alpha_type_scheme: "$ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)" +apply (induct_tac "sch") +apply (simp_all) +done + +lemma S_o_alpha_type_scheme_list: "$ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)" +apply (induct_tac "A") +apply (simp_all) +apply (rule S_o_alpha_type_scheme [unfolded o_def]) +done + +lemma S'_A_eq_S'_alpha_A: "!!A::type_scheme list. + $ (%n. if n : free_tv A Un free_tv t then S n else TVar n) A = + $ ((%x. if x : free_tv A Un free_tv t then S x else TVar x) o + (%x. if x : free_tv A then x else n + x)) A" +apply (subst S_o_alpha_type_scheme_list) +apply (subst alpha_A) +apply (rule refl) +done + +lemma dom_S': + "dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= + free_tv A Un free_tv t" +apply (unfold free_tv_subst dom_def) +apply (simp (no_asm)) +apply fast +done + +lemma cod_S': + "!!(A::type_scheme list) (t::typ). + cod (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= + free_tv ($ S A) Un free_tv ($ S t)" +apply (unfold free_tv_subst cod_def subset_def) +apply (rule ballI) +apply (erule UN_E) +apply (drule dom_S' [THEN subsetD]) +apply simp +apply (fast dest: free_tv_of_substitutions_extend_to_scheme_lists intro: free_tv_of_substitutions_extend_to_types [THEN subsetD]) +done + +lemma free_tv_S': + "!!(A::type_scheme list) (t::typ). + free_tv (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= + free_tv A Un free_tv ($ S A) Un free_tv t Un free_tv ($ S t)" +apply (unfold free_tv_subst) +apply (fast dest: dom_S' [THEN subsetD] cod_S' [THEN subsetD]) +done + +lemma free_tv_alpha: "!!t1::typ. + (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= + {x. ? y. x = n + y}" +apply (induct_tac "t1") +apply (simp (no_asm)) +apply fast +apply (simp (no_asm)) +apply fast +done + +lemma aux_plus: "!!(k::nat). n <= n + k" +apply (induct_tac "k" rule: nat_induct) +apply (simp (no_asm)) +apply (simp (no_asm_simp)) +done + +declare aux_plus [simp] + +lemma new_tv_Int_free_tv_empty_type: "!!t::typ. new_tv n t ==> {x. ? y. x = n + y} Int free_tv t = {}" +apply safe +apply (cut_tac aux_plus) +apply (drule new_tv_le) +apply assumption +apply (rotate_tac 1) +apply (drule new_tv_not_free_tv) +apply fast +done + +lemma new_tv_Int_free_tv_empty_scheme: "!!sch::type_scheme. new_tv n sch ==> {x. ? y. x = n + y} Int free_tv sch = {}" +apply safe +apply (cut_tac aux_plus) +apply (drule new_tv_le) +apply assumption +apply (rotate_tac 1) +apply (drule new_tv_not_free_tv) +apply fast +done + +lemma new_tv_Int_free_tv_empty_scheme_list: "!A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}" +apply (rule allI) +apply (induct_tac "A") +apply (simp (no_asm)) +apply (simp (no_asm)) +apply (fast dest: new_tv_Int_free_tv_empty_scheme) +done + +lemma gen_t_le_gen_alpha_t [rule_format (no_asm)]: + "new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)" +apply (unfold le_type_scheme_def is_bound_typ_instance) +apply (intro strip) +apply (erule exE) +apply (hypsubst) +apply (rule_tac x = " (%x. S (if n <= x then x - n else x))" in exI) +apply (induct_tac "t") +apply (simp (no_asm)) +apply (case_tac "nat : free_tv A") +apply (simp (no_asm_simp)) +apply (subgoal_tac "n <= n + nat") +apply (drule new_tv_le) +apply assumption +apply (drule new_tv_not_free_tv) +apply (drule new_tv_not_free_tv) +apply (simp (no_asm_simp) add: diff_add_inverse) +apply (simp (no_asm)) +apply (simp (no_asm_simp)) +done + +declare has_type.intros [intro!] + +lemma has_type_le_env [rule_format (no_asm)]: "A |- e::t ==> !B. A <= B --> B |- e::t" +apply (erule has_type.induct) + apply (simp (no_asm) add: le_env_def) + apply (fastsimp elim: bound_typ_instance_trans) + apply simp + apply fast +apply (slow elim: le_env_free_tv [THEN free_tv_subset_gen_le]) +done + +(* has_type is closed w.r.t. substitution *) +lemma has_type_cl_sub: "A |- e :: t ==> !S. $S A |- e :: $S t" +apply (erule has_type.induct) +(* case VarI *) + apply (rule allI) + apply (rule has_type.VarI) + apply (simp add: app_subst_list) + apply (simp (no_asm_simp) add: app_subst_list) + (* case AbsI *) + apply (rule allI) + apply (simp (no_asm)) + apply (rule has_type.AbsI) + apply simp + (* case AppI *) + apply (rule allI) + apply (rule has_type.AppI) + apply simp + apply (erule spec) + apply (erule spec) +(* case LetI *) +apply (rule allI) +apply (rule replace_s_by_s') +apply (cut_tac A = "$ S A" and A' = "A" and t = "t" and t' = "$ S t" in ex_fresh_variable) +apply (erule exE) +apply (erule conjE)+ +apply (rule_tac ?t1.0 = "$ ((%x. if x : free_tv A Un free_tv t then S x else TVar x) o (%x. if x : free_tv A then x else n + x)) t1" in has_type.LETI) + apply (drule_tac x = " (%x. if x : free_tv A Un free_tv t then S x else TVar x) o (%x. if x : free_tv A then x else n + x) " in spec) + apply (subst S'_A_eq_S'_alpha_A) + apply assumption +apply (subst S_o_alpha_typ) +apply (subst gen_subst_commutes) + apply (rule subset_antisym) + apply (rule subsetI) + apply (erule IntE) + apply (drule free_tv_S' [THEN subsetD]) + apply (drule free_tv_alpha [THEN subsetD]) + apply (simp del: full_SetCompr_eq) + apply (erule exE) + apply (hypsubst) + apply (subgoal_tac "new_tv (n + y) ($ S A) ") + apply (subgoal_tac "new_tv (n + y) ($ S t) ") + apply (subgoal_tac "new_tv (n + y) A") + apply (subgoal_tac "new_tv (n + y) t") + apply (drule new_tv_not_free_tv)+ + apply fast + apply (rule new_tv_le) prefer 2 apply assumption apply simp + apply (rule new_tv_le) prefer 2 apply assumption apply simp + apply (rule new_tv_le) prefer 2 apply assumption apply simp + apply (rule new_tv_le) prefer 2 apply assumption apply simp + apply fast +apply (rule has_type_le_env) + apply (drule spec) + apply (drule spec) + apply assumption +apply (rule app_subst_Cons [THEN subst]) +apply (rule S_compatible_le_scheme_lists) +apply (simp (no_asm_simp)) +done + end diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/Type.ML --- a/src/HOL/MiniML/Type.ML Mon Mar 01 13:51:21 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,722 +0,0 @@ -(* Title: HOL/MiniML/Type.thy - ID: $Id$ - Author: Wolfgang Naraschewski and Tobias Nipkow - Copyright 1996 TU Muenchen -*) - -Addsimps [mgu_eq,mgu_mg,mgu_free]; - - -(* lemmata for make scheme *) - -Goal "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)"; -by (induct_tac "t" 1); -by (Simp_tac 1); -by (Asm_full_simp_tac 1); -by (Fast_tac 1); -qed_spec_mp "mk_scheme_Fun"; - -Goal "!t'. mk_scheme t = mk_scheme t' --> t=t'"; -by (induct_tac "t" 1); - by (rtac allI 1); - by (induct_tac "t'" 1); - by (Simp_tac 1); - by (Asm_full_simp_tac 1); -by (rtac allI 1); -by (induct_tac "t'" 1); - by (Simp_tac 1); -by (Asm_full_simp_tac 1); -qed_spec_mp "mk_scheme_injective"; - -Goal "free_tv (mk_scheme t) = free_tv t"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "free_tv_mk_scheme"; - -Addsimps [free_tv_mk_scheme]; - -Goal "$ S (mk_scheme t) = mk_scheme ($ S t)"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "subst_mk_scheme"; - -Addsimps [subst_mk_scheme]; - - -(* constructor laws for app_subst *) - -Goalw [app_subst_list] - "$ S [] = []"; -by (Simp_tac 1); -qed "app_subst_Nil"; - -Goalw [app_subst_list] - "$ 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 [new_tv_def] - "new_tv n (TVar m) = (m t2) = (new_tv n t1 & new_tv n t2)"; -by (fast_tac (HOL_cs addss simpset()) 1); -qed "new_tv_Fun"; - -Goalw [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 [new_tv_def] - "new_tv n []"; -by (Simp_tac 1); -qed "new_tv_Nil"; - -Goalw [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 [new_tv_def] "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 [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]; - -Goal "new_tv n (sch::type_scheme) --> \ -\ $(%k. if k \ -\ $(%k. if k x : free_tv (A!n) --> x : free_tv A"; -by (induct_tac "A" 1); -by (Asm_full_simp_tac 1); -by (rtac allI 1); -by (induct_thm_tac nat_induct "n" 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 "!nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A"; -by (induct_tac "A" 1); -by (Asm_full_simp_tac 1); -by (rtac allI 1); -by (induct_thm_tac nat_induct "nat" 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 "(!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t"; -by (induct_tac "t" 1); -by (Simp_tac 1); -by (Asm_full_simp_tac 1); -qed_spec_mp "typ_substitutions_only_on_free_variables"; - -Goal "(!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 "(!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch"; -by (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 - "(!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 - "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A"; -by (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 "((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)"; -by (Fast_tac 1); -val weaken_asm_Un = result (); - -Goal "(!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A"; -by (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 - "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n"; -by (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 - "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n"; -by (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 - "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n"; -by (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 [free_tv_subst] - "v : cod S ==> v : free_tv S"; -by (fast_tac set_cs 1); -qed "codD"; - -Goalw [free_tv_subst,dom_def] - "x ~: free_tv S ==> S x = TVar x"; -by (fast_tac set_cs 1); -qed "not_free_impl_id"; - -Goalw [new_tv_def] - "[| new_tv n t; m:free_tv t |] ==> m v : cod S"; -by (Simp_tac 1); -by (safe_tac (empty_cs addSIs [exI,conjI,notI])); -by (assume_tac 2); -by (Asm_full_simp_tac 1); -qed "cod_app_subst"; -Addsimps [cod_app_subst]; - -Goal "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); -qed "free_tv_subst_var"; - -Goal "free_tv ($ S (t::typ)) <= cod S Un free_tv t"; -by (induct_tac "t" 1); -(* case TVar n *) -by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1); -(* case Fun t1 t2 *) -by (fast_tac (set_cs addss simpset()) 1); -qed "free_tv_app_subst_te"; - -Goal "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch"; -by (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 "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A"; -by (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); -qed "free_tv_app_subst_scheme_list"; - -Goalw [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() delsimps bex_simps - addsimps [cod_def,dom_def])) 1); -qed "free_tv_comp_subst"; - -Goalw [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 "n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)"; -by (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 "n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)"; -by (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 "n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)"; -by (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 "!!sch::type_scheme. (n : free_tv sch) = (n: set (free_tv_ML sch))"; -by (induct_tac "sch" 1); -by (ALLGOALS Asm_simp_tac); -qed "free_tv_ML_scheme"; - -Goal "!!A::type_scheme list. (n : free_tv A) = (n: set (free_tv_ML A))"; -by (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 "bound_tv (mk_scheme t) = {}"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "bound_tv_mk_scheme"; - -Addsimps [bound_tv_mk_scheme]; - -Goal "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch"; -by (induct_tac "sch" 1); -by (ALLGOALS Asm_simp_tac); -qed "bound_tv_subst_scheme"; - -Addsimps [bound_tv_subst_scheme]; - -Goal "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A"; -by (rtac (thm"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 [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 "new_tv n x = (!y:set x. new_tv n y)"; -by (induct_tac "x" 1); -by (ALLGOALS Asm_simp_tac); -qed "new_tv_list"; - -(* substitution affects only variables occurring freely *) -Goal - "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "subst_te_new_tv"; -Addsimps [subst_te_new_tv]; - -Goal - "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch"; -by (induct_tac "sch" 1); -by (ALLGOALS Asm_simp_tac); -qed_spec_mp "subst_te_new_type_scheme"; -Addsimps [subst_te_new_type_scheme]; - -Goal - "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A"; -by (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 [new_tv_def] - "n<=m ==> new_tv n t ==> new_tv m t"; -by Safe_tac; -by (dtac spec 1); -by (mp_tac 1); -by (Simp_tac 1); -qed "new_tv_le"; -Addsimps [lessI RS less_imp_le RS new_tv_le]; - -Goal "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 "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 "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 - "[| n new_tv m (S n)"; -by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); -qed "new_tv_subst_var"; - -Goal - "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)"; -by (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 "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)"; -by (induct_tac "sch" 1); -by (ALLGOALS (Asm_full_simp_tac)); -by (rewtac 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 (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 - "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)"; -by (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 "new_tv n A --> new_tv (Suc n) ((TVar n)#A)"; -by (simp_tac (simpset() addsimps [new_tv_list]) 1); -qed "new_tv_Suc_list"; - -Goalw [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 [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 [new_tv_def] - "!nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))"; -by (induct_tac "A" 1); -by (Asm_full_simp_tac 1); -by (rtac allI 1); -by (induct_thm_tac nat_induct "nat" 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 "[| 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 "[| 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 [new_tv_def] - "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 [new_tv_def] "!!t::typ. ? n. (new_tv n t)"; -by (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 (simpset() addsimps [less_max_iff_disj]) 1); -by (Blast_tac 1); -qed "fresh_variable_types"; - -Addsimps [fresh_variable_types]; - -Goalw [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)"; -by (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 (simpset() addsimps [less_max_iff_disj]) 1); -by (Blast_tac 1); -qed "fresh_variable_type_schemes"; - -Addsimps [fresh_variable_type_schemes]; - -Goal "!!A::type_scheme list. ? n. (new_tv n A)"; -by (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_max_iff_disj]))); -qed "fresh_variable_type_scheme_lists"; - -Addsimps [fresh_variable_type_scheme_lists]; - -Goal "[| ? 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_max_iff_disj]))); -qed "make_one_new_out_of_two"; - -Goal "!!(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); -by (assume_tac 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); -by (assume_tac 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 (rewtac new_tv_def); -by (simp_tac (simpset() addsimps [less_max_iff_disj]) 1); -by (Blast_tac 1); -qed "ex_fresh_variable"; - -(* mgu does not introduce new type variables *) -Goalw [new_tv_def] - "[|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 [app_subst_list] - "!!A:: ('a::type_struct) list. length ($ S A) = length A"; -by (Simp_tac 1); -qed "length_app_subst_list"; -Addsimps [length_app_subst_list]; - -Goal "!!sch::type_scheme. $ TVar sch = sch"; -by (induct_tac "sch" 1); -by (ALLGOALS Asm_simp_tac); -qed "subst_TVar_scheme"; - -Addsimps [subst_TVar_scheme]; - -Goal "!!A::type_scheme list. $ TVar A = A"; -by (rtac (thm"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 [id_subst_def] - "$ id_subst = (%t::typ. t)"; -by (rtac ext 1); -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "app_subst_id_te"; -Addsimps [app_subst_id_te]; - -Goalw [id_subst_def] - "$ id_subst = (%sch::type_scheme. sch)"; -by (rtac ext 1); -by (induct_tac "sch" 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 [app_subst_list] - "$ id_subst = (%A::type_scheme list. A)"; -by (rtac ext 1); -by (induct_tac "A" 1); -by (ALLGOALS Asm_simp_tac); -qed "app_subst_id_tel"; -Addsimps [app_subst_id_tel]; - -Goal "!!sch::type_scheme. $ id_subst sch = sch"; -by (induct_tac "sch" 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [id_subst_def]))); -qed "id_subst_sch"; - -Addsimps [id_subst_sch]; - -Goal "!!A::type_scheme list. $ id_subst A = A"; -by (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 [id_subst_def,o_def] "$S o id_subst = S"; -by (rtac ext 1); -by (Simp_tac 1); -qed "o_id_subst"; -Addsimps[o_id_subst]; - -Goal "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "subst_comp_te"; - -Goal "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch"; -by (induct_tac "sch" 1); -by (ALLGOALS Asm_full_simp_tac); -qed "subst_comp_type_scheme"; - -Goalw [app_subst_list] - "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A"; -by (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 "!!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 "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A"; -by (stac subst_id_on_type_scheme_list' 1); -by (assume_tac 1); -by (Simp_tac 1); -qed "subst_id_on_type_scheme_list"; - -Goal "!n. n < length A --> ($ S A)!n = $S (A!n)"; -by (induct_tac "A" 1); -by (Asm_full_simp_tac 1); -by (rtac allI 1); -by (rename_tac "n1" 1); -by (induct_thm_tac nat_induct "n1" 1); -by (Asm_full_simp_tac 1); -by (Asm_full_simp_tac 1); -qed_spec_mp "nth_subst"; diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/Type.thy --- a/src/HOL/MiniML/Type.thy Mon Mar 01 13:51:21 2004 +0100 +++ b/src/HOL/MiniML/Type.thy Tue Mar 02 01:32:23 2004 +0100 @@ -6,44 +6,42 @@ MiniML-types and type substitutions. *) -Type = Maybe + +theory Type = Maybe: (* new class for structures containing type variables *) axclass type_struct < type (* type expressions *) -datatype - typ = TVar nat | "->" typ typ (infixr 70) +datatype "typ" = TVar nat | "->" "typ" "typ" (infixr 70) (* type schemata *) -datatype - type_scheme = FVar nat | BVar nat | "=->" type_scheme type_scheme (infixr 70) +datatype type_scheme = FVar nat | BVar nat | "=->" type_scheme type_scheme (infixr 70) (* embedding types into type schemata *) consts - mk_scheme :: typ => type_scheme + mk_scheme :: "typ => type_scheme" primrec "mk_scheme (TVar n) = (FVar n)" "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))" -instance typ::type_struct -instance type_scheme::type_struct -instance list::(type_struct)type_struct -instance fun::(type,type_struct)type_struct +instance "typ"::type_struct .. +instance type_scheme::type_struct .. +instance list::(type_struct)type_struct .. +instance fun::(type,type_struct)type_struct .. (* free_tv s: the type variables occuring freely in the type structure s *) consts - free_tv :: ['a::type_struct] => nat set + free_tv :: "['a::type_struct] => nat set" primrec (free_tv_typ) - free_tv_TVar "free_tv (TVar m) = {m}" - free_tv_Fun "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)" + free_tv_TVar: "free_tv (TVar m) = {m}" + free_tv_Fun: "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)" primrec (free_tv_type_scheme) "free_tv (FVar m) = {m}" @@ -57,7 +55,7 @@ (* executable version of free_tv: Implementation with lists *) consts - free_tv_ML :: ['a::type_struct] => nat list + free_tv_ML :: "['a::type_struct] => nat list" primrec (free_tv_ML_type_scheme) "free_tv_ML (FVar m) = [m]" @@ -73,14 +71,14 @@ structure s, i.e. whether n is greater than any type variable occuring in the type structure *) constdefs - new_tv :: [nat,'a::type_struct] => bool + new_tv :: "[nat,'a::type_struct] => bool" "new_tv n ts == ! m. m:(free_tv ts) --> m nat set + bound_tv :: "['a::type_struct] => nat set" primrec (bound_tv_type_scheme) "bound_tv (FVar m) = {}" @@ -95,7 +93,7 @@ (* minimal new free / bound variable *) consts - min_new_bound_tv :: 'a::type_struct => nat + min_new_bound_tv :: "'a::type_struct => nat" primrec (min_new_bound_tv_type_scheme) "min_new_bound_tv (FVar n) = 0" @@ -107,7 +105,7 @@ (* type variable substitution *) types - subst = nat => typ + subst = "nat => typ" (* identity *) constdefs @@ -116,11 +114,11 @@ (* extension of substitution to type structures *) consts - app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$") + app_subst :: "[subst, 'a::type_struct] => 'a::type_struct" ("$") primrec (app_subst_typ) - app_subst_TVar "$ S (TVar n) = S n" - app_subst_Fun "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" + app_subst_TVar: "$ S (TVar n) = S n" + app_subst_Fun: "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" primrec (app_subst_type_scheme) "$ S (FVar n) = mk_scheme (S n)" @@ -128,32 +126,793 @@ "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)" defs - app_subst_list "$ S == map ($ S)" + app_subst_list: "$ S == map ($ S)" (* domain of a substitution *) constdefs - dom :: subst => nat set + dom :: "subst => nat set" "dom S == {n. S n ~= TVar n}" (* codomain of a substitution: the introduced variables *) constdefs - cod :: subst => nat set + cod :: "subst => nat set" "cod S == (UN m:dom S. (free_tv (S m)))" defs - free_tv_subst "free_tv S == (dom S) Un (cod S)" + free_tv_subst: "free_tv S == (dom S) Un (cod S)" (* unification algorithm mgu *) consts - mgu :: [typ,typ] => subst option -rules - mgu_eq "mgu t1 t2 = Some U ==> $U t1 = $U t2" - mgu_mg "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==> - ? R. S = $R o U" - mgu_Some "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U" - mgu_free "mgu t1 t2 = Some U ==> \ -\ (free_tv U) <= (free_tv t1) Un (free_tv t2)" + mgu :: "[typ,typ] => subst option" +axioms + mgu_eq: "mgu t1 t2 = Some U ==> $U t1 = $U t2" + mgu_mg: "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==> ? R. S = $R o U" + mgu_Some: "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U" + mgu_free: "mgu t1 t2 = Some U ==> (free_tv U) <= (free_tv t1) Un (free_tv t2)" + + +declare mgu_eq [simp] mgu_mg [simp] mgu_free [simp] + + +(* lemmata for make scheme *) + +lemma mk_scheme_Fun [rule_format (no_asm)]: "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)" +apply (induct_tac "t") +apply (simp (no_asm)) +apply simp +apply fast +done + +lemma mk_scheme_injective [rule_format (no_asm)]: "!t'. mk_scheme t = mk_scheme t' --> t=t'" +apply (induct_tac "t") + apply (rule allI) + apply (induct_tac "t'") + apply (simp (no_asm)) + apply simp +apply (rule allI) +apply (induct_tac "t'") + apply (simp (no_asm)) +apply simp +done + +lemma free_tv_mk_scheme: "free_tv (mk_scheme t) = free_tv t" +apply (induct_tac "t") +apply (simp_all (no_asm_simp)) +done + +declare free_tv_mk_scheme [simp] + +lemma subst_mk_scheme: "$ S (mk_scheme t) = mk_scheme ($ S t)" +apply (induct_tac "t") +apply (simp_all (no_asm_simp)) +done + +declare subst_mk_scheme [simp] + + +(* constructor laws for app_subst *) + +lemma app_subst_Nil: + "$ S [] = []" + +apply (unfold app_subst_list) +apply (simp (no_asm)) +done + +lemma app_subst_Cons: + "$ S (x#l) = ($ S x)#($ S l)" +apply (unfold app_subst_list) +apply (simp (no_asm)) +done + +declare app_subst_Nil [simp] app_subst_Cons [simp] + + +(* constructor laws for new_tv *) + +lemma new_tv_TVar: + "new_tv n (TVar m) = (m t2) = (new_tv n t1 & new_tv n t2)" +apply (unfold new_tv_def) +apply (fastsimp) +done + +lemma new_tv_Fun2: + "new_tv n (t1 =-> t2) = (new_tv n t1 & new_tv n t2)" +apply (unfold new_tv_def) +apply (fastsimp) +done + +lemma new_tv_Nil: + "new_tv n []" +apply (unfold new_tv_def) +apply (simp (no_asm)) +done + +lemma new_tv_Cons: + "new_tv n (x#l) = (new_tv n x & new_tv n l)" +apply (unfold new_tv_def) +apply (fastsimp) +done + +lemma new_tv_TVar_subst: "new_tv n TVar" +apply (unfold new_tv_def) +apply (intro strip) +apply (simp add: free_tv_subst dom_def cod_def) +done + +declare new_tv_TVar [simp] new_tv_FVar [simp] new_tv_BVar [simp] new_tv_Fun [simp] new_tv_Fun2 [simp] new_tv_Nil [simp] new_tv_Cons [simp] new_tv_TVar_subst [simp] + +lemma new_tv_id_subst: + "new_tv n id_subst" +apply (unfold id_subst_def new_tv_def free_tv_subst dom_def cod_def) +apply (simp (no_asm)) +done +declare new_tv_id_subst [simp] + +lemma new_if_subst_type_scheme: "new_tv n (sch::type_scheme) --> + $(%k. if k + $(%k. if k x : free_tv (A!n) --> x : free_tv A" +apply (induct_tac "A") +apply simp +apply (rule allI) +apply (induct_tac "n" rule: nat_induct) +apply simp +apply simp +done + +declare free_tv_nth_A_impl_free_tv_A [simp] + +lemma free_tv_nth_nat_A [rule_format (no_asm)]: "!nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A" +apply (induct_tac "A") +apply simp +apply (rule allI) +apply (induct_tac "nat" rule: nat_induct) +apply (intro strip) +apply simp +apply (simp (no_asm)) +done + + +(* 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 *) + +lemma typ_substitutions_only_on_free_variables [rule_format (no_asm)]: "(!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t" +apply (induct_tac "t") +apply (simp (no_asm)) +apply simp +done + +lemma eq_free_eq_subst_te: "(!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t" +apply (rule typ_substitutions_only_on_free_variables) +apply (simp (no_asm) add: Ball_def) +done + +lemma scheme_substitutions_only_on_free_variables [rule_format (no_asm)]: "(!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch" +apply (induct_tac "sch") +apply (simp (no_asm)) +apply (simp (no_asm)) +apply simp +done + +lemma eq_free_eq_subst_type_scheme: + "(!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch" +apply (rule scheme_substitutions_only_on_free_variables) +apply (simp (no_asm) add: Ball_def) +done + +lemma eq_free_eq_subst_scheme_list [rule_format (no_asm)]: + "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A" +apply (induct_tac "A") +(* case [] *) +apply (fastsimp) +(* case x#xl *) +apply (fastsimp intro: eq_free_eq_subst_type_scheme) +done + +lemma weaken_asm_Un: "((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)" +apply fast +done + +lemma scheme_list_substitutions_only_on_free_variables [rule_format (no_asm)]: "(!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A" +apply (induct_tac "A") +apply (simp (no_asm)) +apply simp +apply (rule weaken_asm_Un) +apply (intro strip) +apply (erule scheme_substitutions_only_on_free_variables) +done + +lemma eq_subst_te_eq_free [rule_format (no_asm)]: + "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n" +apply (induct_tac "t") +(* case TVar n *) +apply (fastsimp) +(* case Fun t1 t2 *) +apply (fastsimp) +done + +lemma eq_subst_type_scheme_eq_free [rule_format (no_asm)]: + "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n" +apply (induct_tac "sch") +(* case TVar n *) +apply (simp (no_asm_simp)) +(* case BVar n *) +apply (intro strip) +apply (erule mk_scheme_injective) +apply (simp (no_asm_simp)) +(* case Fun t1 t2 *) +apply simp +done + +lemma eq_subst_scheme_list_eq_free [rule_format (no_asm)]: + "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n" +apply (induct_tac "A") +(* case [] *) +apply (fastsimp) +(* case x#xl *) +apply (fastsimp intro: eq_subst_type_scheme_eq_free) +done + +lemma codD: + "v : cod S ==> v : free_tv S" +apply (unfold free_tv_subst) +apply (fast) +done + +lemma not_free_impl_id: + "x ~: free_tv S ==> S x = TVar x" + +apply (unfold free_tv_subst dom_def) +apply (fast) +done + +lemma free_tv_le_new_tv: + "[| new_tv n t; m:free_tv t |] ==> m v : cod S" +apply (unfold dom_def cod_def UNION_def Bex_def) +apply (simp (no_asm)) +apply (safe intro!: exI conjI notI) +prefer 2 apply (assumption) +apply simp +done +declare cod_app_subst [simp] + +lemma free_tv_subst_var: "free_tv (S (v::nat)) <= insert v (cod S)" +apply (case_tac "v:dom S") +apply (fastsimp simp add: cod_def) +apply (fastsimp simp add: dom_def) +done + +lemma free_tv_app_subst_te: "free_tv ($ S (t::typ)) <= cod S Un free_tv t" +apply (induct_tac "t") +(* case TVar n *) +apply (simp (no_asm) add: free_tv_subst_var) +(* case Fun t1 t2 *) +apply (fastsimp) +done + +lemma free_tv_app_subst_type_scheme: "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch" +apply (induct_tac "sch") +(* case FVar n *) +apply (simp (no_asm) add: free_tv_subst_var) +(* case BVar n *) +apply (simp (no_asm)) +(* case Fun t1 t2 *) +apply (fastsimp) +done + +lemma free_tv_app_subst_scheme_list: "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A" +apply (induct_tac "A") +(* case [] *) +apply (simp (no_asm)) +(* case a#al *) +apply (cut_tac free_tv_app_subst_type_scheme) +apply (fastsimp) +done + +lemma free_tv_comp_subst: + "free_tv (%u::nat. $ s1 (s2 u) :: typ) <= + free_tv s1 Un free_tv s2" +apply (unfold free_tv_subst dom_def) +apply (clarsimp simp add: cod_def dom_def) +apply (drule free_tv_app_subst_te [THEN subsetD]) +apply clarsimp +apply (auto simp add: cod_def dom_def) +apply (drule free_tv_subst_var [THEN subsetD]) +apply (auto simp add: cod_def dom_def) +done + +lemma free_tv_o_subst: + "free_tv ($ S1 o S2) <= free_tv S1 Un free_tv (S2 :: nat => typ)" +apply (unfold o_def) +apply (rule free_tv_comp_subst) +done + +lemma free_tv_of_substitutions_extend_to_types [rule_format (no_asm)]: "n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)" +apply (induct_tac "t") +apply (simp (no_asm)) +apply (simp (no_asm)) +apply fast +done + +lemma free_tv_of_substitutions_extend_to_schemes [rule_format (no_asm)]: "n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)" +apply (induct_tac "sch") +apply (simp (no_asm)) +apply (simp (no_asm)) +apply (simp (no_asm)) +apply fast +done + +lemma free_tv_of_substitutions_extend_to_scheme_lists [rule_format (no_asm)]: "n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)" +apply (induct_tac "A") +apply (simp (no_asm)) +apply (simp (no_asm)) +apply (fast dest: free_tv_of_substitutions_extend_to_schemes) +done + +declare free_tv_of_substitutions_extend_to_scheme_lists [simp] + +lemma free_tv_ML_scheme: "!!sch::type_scheme. (n : free_tv sch) = (n: set (free_tv_ML sch))" +apply (induct_tac "sch") +apply (simp_all (no_asm_simp)) +done + +lemma free_tv_ML_scheme_list: "!!A::type_scheme list. (n : free_tv A) = (n: set (free_tv_ML A))" +apply (induct_tac "A") +apply (simp (no_asm)) +apply (simp (no_asm_simp) add: free_tv_ML_scheme) +done + + +(* lemmata for bound_tv *) + +lemma bound_tv_mk_scheme: "bound_tv (mk_scheme t) = {}" +apply (induct_tac "t") +apply (simp_all (no_asm_simp)) +done + +declare bound_tv_mk_scheme [simp] + +lemma bound_tv_subst_scheme: "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch" +apply (induct_tac "sch") +apply (simp_all (no_asm_simp)) +done + +declare bound_tv_subst_scheme [simp] + +lemma bound_tv_subst_scheme_list: "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A" +apply (rule list.induct) +apply (simp (no_asm)) +apply (simp (no_asm_simp)) +done + +declare bound_tv_subst_scheme_list [simp] + + +(* lemmata for new_tv *) + +lemma new_tv_subst: + "new_tv n S = ((!m. n <= m --> (S m = TVar m)) & + (! l. l < n --> new_tv n (S l) ))" + +apply (unfold new_tv_def) +apply (safe) + (* ==> *) + apply (fastsimp dest: leD simp add: free_tv_subst dom_def) + apply (subgoal_tac "m:cod S | S l = TVar l") + apply safe + apply (fastsimp dest: UnI2 simp add: free_tv_subst) + apply (drule_tac P = "%x. m:free_tv x" in subst , assumption) + apply simp + apply (fastsimp simp add: free_tv_subst cod_def dom_def) +(* <== *) +apply (unfold free_tv_subst cod_def dom_def) +apply safe + apply (cut_tac m = "m" and n = "n" in less_linear) + apply (fast intro!: less_or_eq_imp_le) +apply (cut_tac m = "ma" and n = "n" in less_linear) +apply (fast intro!: less_or_eq_imp_le) +done + +lemma new_tv_list: "new_tv n x = (!y:set x. new_tv n y)" +apply (induct_tac "x") +apply (simp_all (no_asm_simp)) +done + +(* substitution affects only variables occurring freely *) +lemma subst_te_new_tv: + "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t" +apply (induct_tac "t") +apply (simp_all (no_asm_simp)) +done +declare subst_te_new_tv [simp] + +lemma subst_te_new_type_scheme [rule_format (no_asm)]: + "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch" +apply (induct_tac "sch") +apply (simp_all (no_asm_simp)) +done +declare subst_te_new_type_scheme [simp] + +lemma subst_tel_new_scheme_list [rule_format (no_asm)]: + "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A" +apply (induct_tac "A") +apply simp_all +done +declare subst_tel_new_scheme_list [simp] + +(* all greater variables are also new *) +lemma new_tv_le: + "n<=m ==> new_tv n t ==> new_tv m t" +apply (unfold new_tv_def) +apply safe +apply (drule spec) +apply (erule (1) notE impE) +apply (simp (no_asm)) +done +declare lessI [THEN less_imp_le [THEN new_tv_le], simp] + +lemma new_tv_typ_le: "n<=m ==> new_tv n (t::typ) ==> new_tv m t" +apply (simp (no_asm_simp) add: new_tv_le) +done + +lemma new_scheme_list_le: "n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A" +apply (simp (no_asm_simp) add: new_tv_le) +done + +lemma new_tv_subst_le: "n<=m ==> new_tv n (S::subst) ==> new_tv m S" +apply (simp (no_asm_simp) add: new_tv_le) +done + +(* new_tv property remains if a substitution is applied *) +lemma new_tv_subst_var: + "[| n new_tv m (S n)" +apply (simp add: new_tv_subst) +done + +lemma new_tv_subst_te [rule_format (no_asm)]: + "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)" +apply (induct_tac "t") +apply (fastsimp simp add: new_tv_subst)+ +done +declare new_tv_subst_te [simp] + +lemma new_tv_subst_type_scheme [rule_format (no_asm)]: "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)" +apply (induct_tac "sch") +apply (simp_all) +apply (unfold new_tv_def) +apply (simp (no_asm) add: free_tv_subst dom_def cod_def) +apply (intro strip) +apply (case_tac "S nat = TVar nat") +apply simp +apply (drule_tac x = "m" in spec) +apply fast +done +declare new_tv_subst_type_scheme [simp] + +lemma new_tv_subst_scheme_list [rule_format (no_asm)]: + "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)" +apply (induct_tac "A") +apply (fastsimp)+ +done +declare new_tv_subst_scheme_list [simp] + +lemma new_tv_Suc_list: "new_tv n A --> new_tv (Suc n) ((TVar n)#A)" +apply (simp (no_asm) add: new_tv_list) +done + +lemma new_tv_only_depends_on_free_tv_type_scheme [rule_format (no_asm)]: "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')" +apply (unfold new_tv_def) +apply (simp (no_asm_simp)) +done + +lemma new_tv_only_depends_on_free_tv_scheme_list [rule_format (no_asm)]: "!!A::type_scheme list. (free_tv A) = (free_tv A') --> (new_tv n A --> new_tv n A')" +apply (unfold new_tv_def) +apply (simp (no_asm_simp)) +done + +lemma new_tv_nth_nat_A [rule_format (no_asm)]: + "!nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))" +apply (unfold new_tv_def) +apply (induct_tac "A") +apply simp +apply (rule allI) +apply (induct_tac "nat" rule: nat_induct) +apply (intro strip) +apply simp +apply (simp (no_asm)) +done + + +(* composition of substitutions preserves new_tv proposition *) +lemma new_tv_subst_comp_1: "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (($ R) o S)" +apply (simp add: new_tv_subst) +done + +lemma new_tv_subst_comp_2: "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (%v.$ R (S v))" +apply (simp add: new_tv_subst) +done + +declare new_tv_subst_comp_1 [simp] new_tv_subst_comp_2 [simp] + +(* new type variables do not occur freely in a type structure *) +lemma new_tv_not_free_tv: + "new_tv n A ==> n~:(free_tv A)" +apply (unfold new_tv_def) +apply (fast elim: less_irrefl) +done +declare new_tv_not_free_tv [simp] + +lemma fresh_variable_types: "!!t::typ. ? n. (new_tv n t)" +apply (unfold new_tv_def) +apply (induct_tac "t") +apply (rule_tac x = "Suc nat" in exI) +apply (simp (no_asm_simp)) +apply (erule exE)+ +apply (rename_tac "n'") +apply (rule_tac x = "max n n'" in exI) +apply (simp (no_asm) add: less_max_iff_disj) +apply blast +done + +declare fresh_variable_types [simp] + +lemma fresh_variable_type_schemes: "!!sch::type_scheme. ? n. (new_tv n sch)" +apply (unfold new_tv_def) +apply (induct_tac "sch") +apply (rule_tac x = "Suc nat" in exI) +apply (simp (no_asm)) +apply (rule_tac x = "Suc nat" in exI) +apply (simp (no_asm)) +apply (erule exE)+ +apply (rename_tac "n'") +apply (rule_tac x = "max n n'" in exI) +apply (simp (no_asm) add: less_max_iff_disj) +apply blast +done + +declare fresh_variable_type_schemes [simp] + +lemma fresh_variable_type_scheme_lists: "!!A::type_scheme list. ? n. (new_tv n A)" +apply (induct_tac "A") +apply (simp (no_asm)) +apply (simp (no_asm)) +apply (erule exE) +apply (cut_tac sch = "a" in fresh_variable_type_schemes) +apply (erule exE) +apply (rename_tac "n'") +apply (rule_tac x = " (max n n') " in exI) +apply (subgoal_tac "n <= (max n n') ") +apply (subgoal_tac "n' <= (max n n') ") +apply (fast dest: new_tv_le) +apply (simp_all (no_asm) add: le_max_iff_disj) +done + +declare fresh_variable_type_scheme_lists [simp] + +lemma make_one_new_out_of_two: "[| ? n1. (new_tv n1 x); ? n2. (new_tv n2 y)|] ==> ? n. (new_tv n x) & (new_tv n y)" +apply (erule exE)+ +apply (rename_tac "n1" "n2") +apply (rule_tac x = " (max n1 n2) " in exI) +apply (subgoal_tac "n1 <= max n1 n2") +apply (subgoal_tac "n2 <= max n1 n2") +apply (fast dest: new_tv_le) +apply (simp_all (no_asm) add: le_max_iff_disj) +done + +lemma ex_fresh_variable: "!!(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')" +apply (cut_tac t = "t" in fresh_variable_types) +apply (cut_tac t = "t'" in fresh_variable_types) +apply (drule make_one_new_out_of_two) +apply assumption +apply (erule_tac V = "? n. new_tv n t'" in thin_rl) +apply (cut_tac A = "A" in fresh_variable_type_scheme_lists) +apply (cut_tac A = "A'" in fresh_variable_type_scheme_lists) +apply (rotate_tac 1) +apply (drule make_one_new_out_of_two) +apply assumption +apply (erule_tac V = "? n. new_tv n A'" in thin_rl) +apply (erule exE)+ +apply (rename_tac n2 n1) +apply (rule_tac x = " (max n1 n2) " in exI) +apply (unfold new_tv_def) +apply (simp (no_asm) add: less_max_iff_disj) +apply blast +done + +(* mgu does not introduce new type variables *) +lemma mgu_new: + "[|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> new_tv n u" +apply (unfold new_tv_def) +apply (fast dest: mgu_free) +done + + +(* lemmata for substitutions *) + +lemma length_app_subst_list: + "!!A:: ('a::type_struct) list. length ($ S A) = length A" + +apply (unfold app_subst_list) +apply (simp (no_asm)) +done +declare length_app_subst_list [simp] + +lemma subst_TVar_scheme: "!!sch::type_scheme. $ TVar sch = sch" +apply (induct_tac "sch") +apply (simp_all (no_asm_simp)) +done + +declare subst_TVar_scheme [simp] + +lemma subst_TVar_scheme_list: "!!A::type_scheme list. $ TVar A = A" +apply (rule list.induct) +apply (simp_all add: app_subst_list) +done + +declare subst_TVar_scheme_list [simp] + +(* application of id_subst does not change type expression *) +lemma app_subst_id_te: + "$ id_subst = (%t::typ. t)" +apply (unfold id_subst_def) +apply (rule ext) +apply (induct_tac "t") +apply (simp_all (no_asm_simp)) +done +declare app_subst_id_te [simp] + +lemma app_subst_id_type_scheme: + "$ id_subst = (%sch::type_scheme. sch)" +apply (unfold id_subst_def) +apply (rule ext) +apply (induct_tac "sch") +apply (simp_all (no_asm_simp)) +done +declare app_subst_id_type_scheme [simp] + +(* application of id_subst does not change list of type expressions *) +lemma app_subst_id_tel: + "$ id_subst = (%A::type_scheme list. A)" +apply (unfold app_subst_list) +apply (rule ext) +apply (induct_tac "A") +apply (simp_all (no_asm_simp)) +done +declare app_subst_id_tel [simp] + +lemma id_subst_sch: "!!sch::type_scheme. $ id_subst sch = sch" +apply (induct_tac "sch") +apply (simp_all add: id_subst_def) +done + +declare id_subst_sch [simp] + +lemma id_subst_A: "!!A::type_scheme list. $ id_subst A = A" +apply (induct_tac "A") +apply simp +apply simp +done + +declare id_subst_A [simp] + +(* composition of substitutions *) +lemma o_id_subst: "$S o id_subst = S" +apply (unfold id_subst_def o_def) +apply (rule ext) +apply (simp (no_asm)) +done +declare o_id_subst [simp] + +lemma subst_comp_te: "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t" +apply (induct_tac "t") +apply (simp_all (no_asm_simp)) +done + +lemma subst_comp_type_scheme: "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch" +apply (induct_tac "sch") +apply simp_all +done + +lemma subst_comp_scheme_list: + "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A" +apply (unfold app_subst_list) +apply (induct_tac "A") +(* case [] *) +apply (simp (no_asm)) +(* case x#xl *) +apply (simp add: subst_comp_type_scheme) +done + +lemma subst_id_on_type_scheme_list': "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = $ id_subst A" +apply (rule scheme_list_substitutions_only_on_free_variables) +apply (simp add: id_subst_def) +done + +lemma subst_id_on_type_scheme_list: "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A" +apply (subst subst_id_on_type_scheme_list') +apply assumption +apply (simp (no_asm)) +done + +lemma nth_subst [rule_format (no_asm)]: "!n. n < length A --> ($ S A)!n = $S (A!n)" +apply (induct_tac "A") +apply simp +apply (rule allI) +apply (rename_tac "n1") +apply (induct_tac "n1" rule: nat_induct) +apply simp +apply simp +done + end diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/W.ML --- a/src/HOL/MiniML/W.ML Mon Mar 01 13:51:21 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,556 +0,0 @@ -(* Title: HOL/MiniML/W.ML - ID: $Id$ - Author: Dieter Nazareth and Tobias Nipkow - Copyright 1995 TU Muenchen - -Correctness and completeness of type inference algorithm W -*) - -Addsimps [Suc_le_lessD]; Delsimps [less_imp_le]; (*the combination loops*) - -val has_type_casesE = - map has_type.mk_cases - [" 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 "!A n S t m. W e A n = Some (S,t,m) --> n<=m"; -by (induct_tac "e" 1); -(* case Var(n) *) -by (simp_tac (simpset() addsplits [split_option_bind]) 1); -(* case Abs e *) -by (simp_tac (simpset() addsplits [split_option_bind]) 1); -by (fast_tac (HOL_cs addDs [Suc_leD]) 1); -(* case App e1 e2 *) -by (simp_tac (simpset() addsplits [split_option_bind]) 1); -by (blast_tac (claset() addIs [le_SucI,le_trans]) 1); -(* case LET e1 e2 *) -by (simp_tac (simpset() addsplits [split_option_bind]) 1); -by (blast_tac (claset() addIs [le_trans]) 1); -qed_spec_mp "W_var_ge"; - -Addsimps [W_var_ge]; - -Goal "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 "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); -by (assume_tac 1); -by (assume_tac 1); -qed "new_tv_compatible_W"; - -Goal "new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)"; -by (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 (assume_tac 2); - by (rtac add_le_mono 1); - by (Simp_tac 1); - by (simp_tac (simpset() addsimps [max_def]) 1); -by (rtac new_tv_le 1); - by (assume_tac 2); -by (rtac add_le_mono 1); - by (Simp_tac 1); -by (simp_tac (simpset() addsimps [max_def]) 1); -qed_spec_mp "new_tv_bound_typ_inst_sch"; - -Addsimps [new_tv_bound_typ_inst_sch]; - -(* resulting type variable is new *) -Goal "!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 (induct_tac "e" 1); -(* case Var n *) -by (simp_tac (simpset() addsplits [split_option_bind]) 1); -by (strip_tac 1); -by (dtac new_tv_nth_nat_A 1); -by (assume_tac 1); -by (Asm_simp_tac 1); -(* case Abs e *) -by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] - addsplits [split_option_bind]) 1); -by (strip_tac 1); -by (eres_inst_tac [("x","Suc n")] 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() addsplits [split_option_bind]) 1); -by (strip_tac 1); -by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1); -by (eres_inst_tac [("x","n")] 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 (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","$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","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_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_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_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_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); -(* 41: case LET e1 e2 *) -by (simp_tac (simpset() addsplits [split_option_bind]) 1); -by (strip_tac 1); -by (EVERY1[etac allE,etac allE,etac allE,etac allE,etac allE,mp_tac,mp_tac]); -by (etac conjE 1); -by (EVERY[etac allE 1,etac allE 1,etac allE 1,etac allE 1,etac allE 1, - etac impE 1, mp_tac 2]); -by (SELECT_GOAL(rewtac new_tv_def)1); -by (Asm_simp_tac 1); -by (REPEAT(dtac W_var_ge 1)); -by (rtac allI 1); -by (strip_tac 1); -by (SELECT_GOAL(rewtac free_tv_subst) 1); -by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1); -by (best_tac (claset() addEs [less_le_trans]) 1); -by (etac conjE 1); -by (rtac conjI 1); -by (SELECT_GOAL(rewtac o_def)1); -by (rtac new_tv_subst_comp_2 1); -by (etac (W_var_ge RS new_tv_subst_le) 1); -by (assume_tac 1); -by (assume_tac 1); -by (assume_tac 1); -qed_spec_mp "new_tv_W"; - -Goal "(v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)"; -by (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 "!n A S t m v. W e A n = Some (S,t,m) --> \ -\ (v:free_tv S | v:free_tv t) --> v v:free_tv A"; -by (induct_tac "e" 1); -(* case Var n *) -by (simp_tac (simpset() addsimps - [free_tv_subst] addsplits [split_option_bind]) 1); -by (strip_tac 1); -by (case_tac "v : free_tv (A!nat)" 1); - by (Asm_full_simp_tac 1); -by (dtac free_tv_bound_typ_inst1 1); - by (simp_tac (simpset() addsimps [o_def]) 1); -by (etac exE 1); -by (Asm_full_simp_tac 1); -(* case Abs e *) -by (asm_full_simp_tac (simpset() addsimps - [free_tv_subst] addsplits [split_option_bind] delsimps all_simps) 1); -by (strip_tac 1); -by (rename_tac "S t n1 v" 1); -by (eres_inst_tac [("x","Suc n")] 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","n1")] allE 1); -by (eres_inst_tac [("x","v")] allE 1); -by (best_tac (HOL_cs addIs [cod_app_subst] - addss (simpset() addsimps [less_Suc_eq])) 1); -(* case App e1 e2 *) -by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1); -by (strip_tac 1); -by (rename_tac "S t n1 S1 t1 n2 S2 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","t")] 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); -(* second case *) -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_Some,o_def]) 1); - by (dtac W_var_geD 1); - by (dtac W_var_geD 1); - by ( (ftac less_le_trans 1) THEN (assume_tac 1) ); - 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_scheme_list RS subsetD, - less_le_trans,less_not_refl2,subsetD] - addEs [UnE] - addss simpset()) 1); -by (Asm_full_simp_tac 1); -by (dtac (sym RS W_var_geD) 1); -by (dtac (sym RS W_var_geD) 1); -by ( (ftac 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_scheme_list RS subsetD, - less_le_trans,subsetD] - addEs [UnE] - addss (simpset() setSolver unsafe_solver)) 1); -(* LET e1 e2 *) -by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1); -by (strip_tac 1); -by (rename_tac "S1 t1 n2 S2 t2 n3 v" 1); -by (eres_inst_tac [("x","n")] 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 ~1 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 "(!x. x : A --> x ~: B) ==> A Int B = {}"; -by (Fast_tac 1); -val weaken_A_Int_B_eq_empty = result(); - -Goal "x ~: A | x : B ==> x ~: A - B"; -by (Fast_tac 1); -val weaken_not_elem_A_minus_B = result(); - -(* correctness of W with respect to has_type *) -Goal "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t"; -by (induct_tac "e" 1); -(* case Var n *) -by (Asm_full_simp_tac 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] - addsplits [split_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); -by (dtac sym 1); -by (REPEAT (etac allE 1)); -by (etac impE 1); -by (mp_tac 2); -by (Asm_simp_tac 1); -by (assume_tac 1); -(* case App e1 e2 *) -by (simp_tac (simpset() addsplits [split_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,o_def]) 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 (ftac new_tv_W 1); -by (assume_tac 1); -by (dtac conjunct1 1); -by (ftac new_tv_subst_scheme_list 1); -by (rtac new_scheme_list_le 1); -by (rtac W_var_ge 1); -by (assume_tac 1); -by (assume_tac 1); -by (etac thin_rl 1); -by (REPEAT (etac allE 1)); -by (dtac sym 1); -by (dtac sym 1); -by (etac thin_rl 1); -by (etac thin_rl 1); -by (mp_tac 1); -by (mp_tac 1); -by (assume_tac 1); -(* case Let e1 e2 *) -by (simp_tac (simpset() addsplits [split_option_bind]) 1); -by (strip_tac 1); -(*by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); *) -by (rename_tac "S1 t1 m1 S2" 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","m1")] spec 1); - by (dres_inst_tac [("x","n")] 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","m")] spec 2); - by (dres_inst_tac [("x","m1")] spec 2); - by (ftac new_tv_W 2); - by (assume_tac 2); - by (dtac conjunct1 2); - by (ftac new_tv_subst_scheme_list 2); - by (rtac new_scheme_list_le 2); - by (rtac W_var_ge 2); - by (assume_tac 2); - by (assume_tac 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); - by (assume_tac 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 < m1" 1); - by (rtac disjI2 1); - by (rtac (free_tv_gen_cons RS subst) 1); - by (rtac free_tv_W 1); - by (assume_tac 1); - by (Asm_full_simp_tac 1); - by (assume_tac 1); -by (rtac disjI1 1); -by (dtac new_tv_W 1); -by (assume_tac 1); -by (dtac conjunct2 1); -by (rtac new_tv_not_free_tv 1); -by (rtac new_tv_le 1); - by (assume_tac 2); -by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le]) 1); -qed_spec_mp "W_correct_lemma"; - -(* Completeness of W w.r.t. has_type *) -Goal "!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 (induct_tac "e" 1); -(* case Var n *) -by (strip_tac 1); -by (simp_tac (simpset() addcongs [conj_cong]) 1); -by (eresolve_tac has_type_casesE 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 12 **) -(* 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","(FVar n)#A")] allE 1); -by (eres_inst_tac [("x","t2")] allE 1); -by (eres_inst_tac [("x","Suc n")] allE 1); -by (best_tac (HOL_cs addSDs [mk_scheme_injective] - addss (simpset() addcongs [conj_cong] - addsplits [split_option_bind])) 1); -(** LEVEL 19 **) - -(* 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","t2 -> t'")] allE 1); -by (eres_inst_tac [("x","n")] allE 1); -by (safe_tac HOL_cs); -(** LEVEL 26 **) -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 (Asm_full_simp_tac 1); -by (safe_tac HOL_cs); -by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS - conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1); -(** LEVEL 33 **) -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); -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); -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 (best_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD, - new_tv_not_free_tv,new_tv_le]) 3); -by (case_tac "na:free_tv Sa" 2); -(* n1 ~: free_tv S1 *) -by (ftac not_free_impl_id 3); -by (Asm_simp_tac 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 (asm_full_simp_tac (simpset() addsimps [dom_def]) 3); -(* na : dom Sa *) -by (rtac eq_free_eq_subst_te 2); -by (strip_tac 2); -by (subgoal_tac "nb ~= ma" 2); -by ((ftac new_tv_W 3) THEN (atac 3)); -by (etac conjE 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); -by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2); -by (Simp_tac 2); -by (rtac eq_free_eq_subst_te 2); -by (strip_tac 2 ); -by (subgoal_tac "na ~= ma" 2); -by ((ftac 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_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 3); -by (Fast_tac 3); -(* case na : free_tv t - free_tv Sa *) -by (Asm_full_simp_tac 2); -by (dres_inst_tac [("A1", "$ S A"), ("r", "$ R ($ 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); -(** LEVEL 73 **) -by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 2); -by (asm_simp_tac (simpset() addsplits [split_option_bind]) 1); -by (safe_tac HOL_cs ); -by (dtac mgu_Some 1); -by ( fast_tac (HOL_cs addss simpset()) 1); -(** LEVEL 78 *) -by ((dtac mgu_mg 1) THEN (atac 1)); -by (etac exE 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_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); -by (dres_inst_tac [("s","Some ?X")] sym 1); -by (rtac eq_free_eq_subst_scheme_list 1); -by ( safe_tac HOL_cs ); -by (subgoal_tac "ma ~= na" 1); -by ((ftac new_tv_W 2) THEN (atac 2)); -by (etac conjE 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")] new_tv_W 2 THEN atac 2); -by (etac conjE 2); -by (dtac (free_tv_app_subst_scheme_list RS subsetD) 2); -by (fast_tac (set_cs addDs [sym RS 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 (Asm_full_simp_tac 2); -(* case na : free_tv t - free_tv Sa *) -by (Asm_full_simp_tac 1); -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 (Asm_full_simp_tac 1); -by (dtac mp 1); -by (rtac has_type_le_env 1); -by (assume_tac 1); -by (Simp_tac 1); -by (rtac gen_bound_typ_instance 1); -by (dtac mp 1); -by (ftac new_tv_compatible_W 1); -by (rtac sym 1); -by (assume_tac 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 "[] |- 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); -qed "W_complete"; diff -r ee97b6463cb4 -r b8da5f258b04 src/HOL/MiniML/W.thy --- a/src/HOL/MiniML/W.thy Mon Mar 01 13:51:21 2004 +0100 +++ b/src/HOL/MiniML/W.thy Tue Mar 02 01:32:23 2004 +0100 @@ -1,21 +1,18 @@ (* Title: HOL/MiniML/W.thy ID: $Id$ - Author: Wolfgang Naraschewski and Tobias Nipkow + Author: Dieter Nazareth, Wolfgang Naraschewski and Tobias Nipkow Copyright 1996 TU Muenchen -Type inference algorithm W +Correctness and completeness of type inference algorithm W *) -W = MiniML + - -types - result_W = "(subst * typ * nat)option" +theory W = MiniML: -(* type inference algorithm W *) +types result_W = "(subst * typ * nat)option" -consts - W :: [expr, ctxt, nat] => result_W +-- "type inference algorithm W" +consts W :: "[expr, ctxt, nat] => result_W" primrec "W (Var i) A n = @@ -35,4 +32,554 @@ "W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n; (S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1; Some( $S2 o S1, t2, m2) )" + + +lemmas W_rules = + le_env_Cons + le_type_scheme_refl + le_env_refl + bound_typ_instance_BVar + not_FVar_le_Fun + not_BVar_le_Fun + le_env_Cons + le_type_scheme_refl + le_env_refl + bound_typ_instance_BVar + not_FVar_le_Fun + not_BVar_le_Fun + has_type.intros + equalityE + + +declare Suc_le_lessD [simp] +declare less_imp_le [simp del] (*the combination loops*) + +inductive_cases has_type_casesE: +"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 *) +lemma W_var_ge [rule_format (no_asm)]: "!A n S t m. W e A n = Some (S,t,m) --> n<=m" +apply (induct_tac "e") +(* case Var(n) *) +apply (simp (no_asm) split add: split_option_bind) +(* case Abs e *) +apply (simp (no_asm) split add: split_option_bind) +apply (fast dest: Suc_leD) +(* case App e1 e2 *) +apply (simp (no_asm) split add: split_option_bind) +apply (blast intro: le_SucI le_trans) +(* case LET e1 e2 *) +apply (simp (no_asm) split add: split_option_bind) +apply (blast intro: le_trans) +done + +declare W_var_ge [simp] + +lemma W_var_geD: "Some (S,t,m) = W e A n ==> n<=m" +apply (simp add: eq_sym_conv) +done + +lemma new_tv_compatible_W: "new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A" +apply (drule W_var_geD) +apply (rule new_scheme_list_le) +apply assumption +apply assumption +done + +lemma new_tv_bound_typ_inst_sch [rule_format (no_asm)]: "new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)" +apply (induct_tac "sch") + apply simp + apply (simp add: add_commute) +apply (intro strip) +apply simp +apply (erule conjE) +apply (rule conjI) + apply (rule new_tv_le) + prefer 2 apply (assumption) + apply (rule add_le_mono) + apply (simp (no_asm)) + apply (simp (no_asm) add: max_def) +apply (rule new_tv_le) + prefer 2 apply (assumption) +apply (rule add_le_mono) + apply (simp (no_asm)) +apply (simp (no_asm) add: max_def) +done + +declare new_tv_bound_typ_inst_sch [simp] + +(* resulting type variable is new *) +lemma new_tv_W [rule_format (no_asm)]: "!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" +apply (induct_tac "e") +(* case Var n *) +apply (simp (no_asm) split add: split_option_bind) +apply (intro strip) +apply (drule new_tv_nth_nat_A) +apply assumption +apply (simp (no_asm_simp)) +(* case Abs e *) +apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_option_bind) +apply (intro strip) +apply (erule_tac x = "Suc n" in allE) +apply (erule_tac x = " (FVar n) #A" in allE) +apply (fastsimp simp add: new_tv_subst new_tv_Suc_list) +(* case App e1 e2 *) +apply (simp (no_asm) split add: split_option_bind) +apply (intro strip) +apply (rename_tac S1 t1 n1 S2 t2 n2 S3) +apply (erule_tac x = "n" in allE) +apply (erule_tac x = "A" in allE) +apply (erule_tac x = "S1" in allE) +apply (erule_tac x = "t1" in allE) +apply (erule_tac x = "n1" in allE) +apply (erule_tac x = "n1" in allE) +apply (simp add: eq_sym_conv del: all_simps) +apply (erule_tac x = "$S1 A" in allE) +apply (erule_tac x = "S2" in allE) +apply (erule_tac x = "t2" in allE) +apply (erule_tac x = "n2" in allE) +apply ( simp add: o_def rotate_Some) +apply (rule conjI) +apply (rule new_tv_subst_comp_2) +apply (rule new_tv_subst_comp_2) +apply (rule lessI [THEN less_imp_le, THEN new_tv_le]) +apply (rule_tac n = "n1" in new_tv_subst_le) +apply (simp add: rotate_Some) +apply (simp (no_asm_simp)) +apply (fast dest: W_var_geD intro: new_scheme_list_le new_tv_subst_scheme_list lessI [THEN less_imp_le [THEN new_tv_subst_le]]) +apply (erule sym [THEN mgu_new]) +apply (blast dest!: W_var_geD + intro: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te + new_tv_subst_scheme_list new_scheme_list_le new_tv_le) + +apply (erule impE) +apply (blast dest: W_var_geD intro: new_tv_subst_scheme_list new_scheme_list_le new_tv_le) +apply clarsimp + +apply (rule lessI [THEN new_tv_subst_var]) +apply (erule sym [THEN mgu_new]) +apply (blast dest!: W_var_geD + intro: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te + new_tv_subst_scheme_list new_scheme_list_le new_tv_le) + +apply (erule impE) +apply (blast dest: W_var_geD intro: new_tv_subst_scheme_list new_scheme_list_le new_tv_le) +apply clarsimp + +-- "41: case LET e1 e2" +apply (simp (no_asm) split add: split_option_bind) +apply (intro strip) +apply (erule allE,erule allE,erule allE,erule allE,erule allE, erule impE, assumption, erule impE, assumption) +apply (erule conjE) +apply (erule allE,erule allE,erule allE,erule allE,erule allE, erule impE, erule_tac [2] notE impE, tactic "assume_tac 2") +apply (simp only: new_tv_def) +apply (simp (no_asm_simp)) +apply (drule W_var_ge)+ +apply (rule allI) +apply (intro strip) +apply (simp only: free_tv_subst) +apply (drule free_tv_app_subst_scheme_list [THEN subsetD]) +apply (best elim: less_le_trans) +apply (erule conjE) +apply (rule conjI) +apply (simp only: o_def) +apply (rule new_tv_subst_comp_2) +apply (erule W_var_ge [THEN new_tv_subst_le]) +apply assumption +apply assumption +apply assumption +done + + +lemma free_tv_bound_typ_inst1 [rule_format (no_asm)]: "(v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)" +apply (induct_tac "sch") +apply simp +apply simp +apply (intro strip) +apply (rule exI) +apply (rule refl) +apply simp +done + +declare free_tv_bound_typ_inst1 [simp] + +lemma free_tv_W [rule_format (no_asm)]: "!n A S t m v. W e A n = Some (S,t,m) --> + (v:free_tv S | v:free_tv t) --> v v:free_tv A" +apply (induct_tac "e") +(* case Var n *) +apply (simp (no_asm) add: free_tv_subst split add: split_option_bind) +apply (intro strip) +apply (case_tac "v : free_tv (A!nat) ") + apply simp +apply (drule free_tv_bound_typ_inst1) + apply (simp (no_asm) add: o_def) +apply (erule exE) +apply simp +(* case Abs e *) +apply (simp add: free_tv_subst split add: split_option_bind del: all_simps) +apply (intro strip) +apply (rename_tac S t n1 v) +apply (erule_tac x = "Suc n" in allE) +apply (erule_tac x = "FVar n # A" in allE) +apply (erule_tac x = "S" in allE) +apply (erule_tac x = "t" in allE) +apply (erule_tac x = "n1" in allE) +apply (erule_tac x = "v" in allE) +apply (bestsimp del: W_rules intro: cod_app_subst simp add: less_Suc_eq) +(* case App e1 e2 *) +apply (simp (no_asm) split add: split_option_bind del: all_simps) +apply (intro strip) +apply (rename_tac S t n1 S1 t1 n2 S2 v) +apply (erule_tac x = "n" in allE) +apply (erule_tac x = "A" in allE) +apply (erule_tac x = "S" in allE) +apply (erule_tac x = "t" in allE) +apply (erule_tac x = "n1" in allE) +apply (erule_tac x = "n1" in allE) +apply (erule_tac x = "v" in allE) +(* second case *) +apply (erule_tac x = "$ S A" in allE) +apply (erule_tac x = "S1" in allE) +apply (erule_tac x = "t1" in allE) +apply (erule_tac x = "n2" in allE) +apply (erule_tac x = "v" in allE) +apply (intro conjI impI | elim conjE)+ + apply (simp add: rotate_Some o_def) + apply (drule W_var_geD) + apply (drule W_var_geD) + apply ( (frule less_le_trans) , (assumption)) + apply clarsimp + apply (drule free_tv_comp_subst [THEN subsetD]) + apply (drule sym [THEN mgu_free]) + apply clarsimp + apply (fastsimp dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_scheme_list [THEN subsetD] less_le_trans less_not_refl2 subsetD) +apply simp +apply (drule sym [THEN W_var_geD]) +apply (drule sym [THEN W_var_geD]) +apply ( (frule less_le_trans) , (assumption)) +apply clarsimp +apply (drule mgu_free) +apply (fastsimp dest: mgu_free codD free_tv_subst_var [THEN subsetD] free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_scheme_list [THEN subsetD] less_le_trans subsetD) +(* LET e1 e2 *) +apply (simp (no_asm) split add: split_option_bind del: all_simps) +apply (intro strip) +apply (rename_tac S1 t1 n2 S2 t2 n3 v) +apply (erule_tac x = "n" in allE) +apply (erule_tac x = "A" in allE) +apply (erule_tac x = "S1" in allE) +apply (erule_tac x = "t1" in allE) +apply (rotate_tac -1) +apply (erule_tac x = "n2" in allE) +apply (rotate_tac -1) +apply (erule_tac x = "v" in allE) +apply (erule (1) notE impE) +apply (erule allE,erule allE,erule allE,erule allE,erule allE,erule_tac x = "v" in allE) +apply (erule (1) notE impE) +apply simp +apply (rule conjI) +apply (fast dest!: codD free_tv_app_subst_scheme_list [THEN subsetD] free_tv_o_subst [THEN subsetD] W_var_ge dest: less_le_trans) +apply (fast dest!: codD free_tv_app_subst_scheme_list [THEN subsetD] W_var_ge dest: less_le_trans) +done + +lemma weaken_A_Int_B_eq_empty: "(!x. x : A --> x ~: B) ==> A Int B = {}" +apply fast +done + +lemma weaken_not_elem_A_minus_B: "x ~: A | x : B ==> x ~: A - B" +apply fast +done + +(* correctness of W with respect to has_type *) +lemma W_correct_lemma [rule_format (no_asm)]: "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t" +apply (induct_tac "e") +(* case Var n *) +apply simp +apply (intro strip) +apply (rule has_type.VarI) +apply (simp (no_asm)) +apply (simp (no_asm) add: is_bound_typ_instance) +apply (rule exI) +apply (rule refl) +(* case Abs e *) +apply (simp add: app_subst_list split add: split_option_bind) +apply (intro strip) +apply (erule_tac x = " (mk_scheme (TVar n)) # A" in allE) +apply simp +apply (rule has_type.AbsI) +apply (drule le_refl [THEN le_SucI, THEN new_scheme_list_le]) +apply (drule sym) +apply (erule allE)+ +apply (erule impE) +apply (erule_tac [2] notE impE, tactic "assume_tac 2") +apply (simp (no_asm_simp)) +apply assumption +(* case App e1 e2 *) +apply (simp (no_asm) split add: split_option_bind) +apply (intro strip) +apply (rename_tac S1 t1 n1 S2 t2 n2 S3) +apply (rule_tac ?t2.0 = "$ S3 t2" in has_type.AppI) +apply (rule_tac S1 = "S3" in app_subst_TVar [THEN subst]) +apply (rule app_subst_Fun [THEN subst]) +apply (rule_tac t = "$S3 (t2 -> (TVar n2))" and s = "$S3 ($S2 t1) " in subst) +apply simp +apply (simp only: subst_comp_scheme_list [symmetric] o_def) +apply ((rule has_type_cl_sub [THEN spec]) , (rule has_type_cl_sub [THEN spec])) +apply (simp add: eq_sym_conv) +apply (simp add: subst_comp_scheme_list [symmetric] o_def has_type_cl_sub eq_sym_conv) +apply (rule has_type_cl_sub [THEN spec]) +apply (frule new_tv_W) +apply assumption +apply (drule conjunct1) +apply (frule new_tv_subst_scheme_list) +apply (rule new_scheme_list_le) +apply (rule W_var_ge) +apply assumption +apply assumption +apply (erule thin_rl) +apply (erule allE)+ +apply (drule sym) +apply (drule sym) +apply (erule thin_rl) +apply (erule thin_rl) +apply (erule (1) notE impE) +apply (erule (1) notE impE) +apply assumption +(* case Let e1 e2 *) +apply (simp (no_asm) split add: split_option_bind) +apply (intro strip) +(*by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); *) +apply (rename_tac S1 t1 m1 S2) +apply (rule_tac ?t1.0 = "$ S2 t1" in has_type.LETI) + apply (simp (no_asm) add: o_def) + apply (simp only: subst_comp_scheme_list [symmetric]) + apply (rule has_type_cl_sub [THEN spec]) + apply (drule_tac x = "A" in spec) + apply (drule_tac x = "S1" in spec) + apply (drule_tac x = "t1" in spec) + apply (drule_tac x = "m1" in spec) + apply (drule_tac x = "n" in spec) + apply (erule (1) notE impE) + apply (simp add: eq_sym_conv) +apply (simp (no_asm) add: o_def) +apply (simp only: subst_comp_scheme_list [symmetric]) +apply (rule gen_subst_commutes [symmetric, THEN subst]) + apply (rule_tac [2] app_subst_Cons [THEN subst]) + apply (erule_tac [2] thin_rl) + apply (drule_tac [2] x = "gen ($S1 A) t1 # $ S1 A" in spec) + apply (drule_tac [2] x = "S2" in spec) + apply (drule_tac [2] x = "t" in spec) + apply (drule_tac [2] x = "m" in spec) + apply (drule_tac [2] x = "m1" in spec) + apply (frule_tac [2] new_tv_W) + prefer 2 apply (assumption) + apply (drule_tac [2] conjunct1) + apply (frule_tac [2] new_tv_subst_scheme_list) + apply (rule_tac [2] new_scheme_list_le) + apply (rule_tac [2] W_var_ge) + prefer 2 apply (assumption) + prefer 2 apply (assumption) + apply (erule_tac [2] impE) + apply (rule_tac [2] A = "$ S1 A" in new_tv_only_depends_on_free_tv_scheme_list) + prefer 2 apply simp + apply (fast) + prefer 2 apply (assumption) + prefer 2 apply simp +apply (rule weaken_A_Int_B_eq_empty) +apply (rule allI) +apply (intro strip) +apply (rule weaken_not_elem_A_minus_B) +apply (case_tac "x < m1") + apply (rule disjI2) + apply (rule free_tv_gen_cons [THEN subst]) + apply (rule free_tv_W) + apply assumption + apply simp + apply assumption +apply (rule disjI1) +apply (drule new_tv_W) +apply assumption +apply (drule conjunct2) +apply (rule new_tv_not_free_tv) +apply (rule new_tv_le) + prefer 2 apply (assumption) +apply (simp add: not_less_iff_le) +done + +(* Completeness of W w.r.t. has_type *) +lemma W_complete_lemma [rule_format (no_asm)]: + "ALL S' A t' n. $S' A |- e :: t' --> new_tv n A --> + (EX S t. (EX m. W e A n = Some (S,t,m)) & + (EX R. $S' A = $R ($S A) & t' = $R t))" +apply (induct_tac "e") + (* case Var n *) + apply (intro strip) + apply (simp (no_asm) cong add: conj_cong) + apply (erule has_type_casesE) + apply (simp add: is_bound_typ_instance) + apply (erule exE) + apply (hypsubst) + apply (rename_tac "S") + apply (rule_tac x = "%x. (if x < n then S' x else S (x - n))" in exI) + apply (rule conjI) + apply (simp (no_asm_simp)) + apply (simp (no_asm_simp) add: bound_typ_inst_composed_subst [symmetric] new_tv_nth_nat_A o_def nth_subst + del: bound_typ_inst_composed_subst) + + (* case Abs e *) + apply (intro strip) + apply (erule has_type_casesE) + apply (erule_tac x = "%x. if x=n then t1 else (S' x) " in allE) + apply (erule_tac x = " (FVar n) #A" in allE) + apply (erule_tac x = "t2" in allE) + apply (erule_tac x = "Suc n" in allE) + apply (bestsimp dest!: mk_scheme_injective cong: conj_cong split: split_option_bind) + + (* case App e1 e2 *) + apply (intro strip) + apply (erule has_type_casesE) + apply (erule_tac x = "S'" in allE) + apply (erule_tac x = "A" in allE) + apply (erule_tac x = "t2 -> t'" in allE) + apply (erule_tac x = "n" in allE) + apply safe + apply (erule_tac x = "R" in allE) + apply (erule_tac x = "$ S A" in allE) + apply (erule_tac x = "t2" in allE) + apply (erule_tac x = "m" in allE) + apply simp + apply safe + apply (blast intro: sym [THEN W_var_geD] new_tv_W [THEN conjunct1] new_scheme_list_le new_tv_subst_scheme_list) + + (** LEVEL 33 **) +apply (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))") +apply (rule_tac [2] t = "$ (%x. if x = ma then t' else (if x: (free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t) " and s = " ($ Ra ta) -> t'" in ssubst) +prefer 2 apply (simp (no_asm_simp) add: subst_comp_te) prefer 2 +apply (rule_tac [2] eq_free_eq_subst_te) +prefer 2 apply (intro strip) prefer 2 +apply (subgoal_tac [2] "na ~=ma") + prefer 3 apply (best dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le) +apply (case_tac [2] "na:free_tv Sa") +(* n1 ~: free_tv S1 *) +apply (frule_tac [3] not_free_impl_id) + prefer 3 apply (simp) +(* na : free_tv Sa *) +apply (drule_tac [2] A1 = "$ S A" in trans [OF _ subst_comp_scheme_list]) +apply (drule_tac [2] eq_subst_scheme_list_eq_free) + prefer 2 apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W) +prefer 2 apply (simp (no_asm_simp)) prefer 2 +apply (case_tac [2] "na:dom Sa") +(* na ~: dom Sa *) + prefer 3 apply (simp add: dom_def) +(* na : dom Sa *) +apply (rule_tac [2] eq_free_eq_subst_te) +prefer 2 apply (intro strip) prefer 2 +apply (subgoal_tac [2] "nb ~= ma") +apply (frule_tac [3] new_tv_W) prefer 3 apply assumption +apply (erule_tac [3] conjE) +apply (drule_tac [3] new_tv_subst_scheme_list) + prefer 3 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD]) + prefer 3 apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst) + prefer 2 apply (fastsimp simp add: cod_def free_tv_subst) +prefer 2 apply (simp (no_asm)) prefer 2 +apply (rule_tac [2] eq_free_eq_subst_te) +prefer 2 apply (intro strip) prefer 2 +apply (subgoal_tac [2] "na ~= ma") +apply (frule_tac [3] new_tv_W) prefer 3 apply assumption +apply (erule_tac [3] conjE) +apply (drule_tac [3] sym [THEN W_var_geD]) + prefer 3 apply (fast dest: new_scheme_list_le new_tv_subst_scheme_list new_tv_W new_tv_not_free_tv) +apply (case_tac [2] "na: free_tv t - free_tv Sa") +(* case na ~: free_tv t - free_tv Sa *) + prefer 3 + apply simp + apply fast +(* case na : free_tv t - free_tv Sa *) +prefer 2 apply simp prefer 2 +apply (drule_tac [2] A1 = "$ S A" and r = "$ R ($ S A)" in trans [OF _ subst_comp_scheme_list]) +apply (drule_tac [2] eq_subst_scheme_list_eq_free) + prefer 2 + apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W) +(** LEVEL 73 **) + prefer 2 apply (simp add: free_tv_subst dom_def) +apply (simp (no_asm_simp) split add: split_option_bind) +apply safe +apply (drule mgu_Some) + apply fastsimp +(** LEVEL 78 *) +apply (drule mgu_mg, assumption) +apply (erule exE) +apply (rule_tac x = "Rb" in exI) +apply (rule conjI) +apply (drule_tac [2] x = "ma" in fun_cong) + prefer 2 apply (simp add: eq_sym_conv) +apply (simp (no_asm) add: subst_comp_scheme_list) +apply (simp (no_asm) add: subst_comp_scheme_list [symmetric]) +apply (rule_tac A2 = "($ Sa ($ S A))" in trans [OF _ subst_comp_scheme_list [symmetric]]) +apply (simp add: o_def eq_sym_conv) +apply (drule_tac s = "Some ?X" in sym) +apply (rule eq_free_eq_subst_scheme_list) +apply safe +apply (subgoal_tac "ma ~= na") +apply (frule_tac [2] new_tv_W) prefer 2 apply assumption +apply (erule_tac [2] conjE) +apply (drule_tac [2] new_tv_subst_scheme_list) + prefer 2 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD]) +apply (frule_tac [2] n = "m" in new_tv_W) prefer 2 apply assumption +apply (erule_tac [2] conjE) +apply (drule_tac [2] free_tv_app_subst_scheme_list [THEN subsetD]) + apply (tactic {* + (fast_tac (set_cs addDs [sym RS thm "W_var_geD", thm "new_scheme_list_le", thm "codD", + thm "new_tv_not_free_tv"]) 2) *}) +apply (case_tac "na: free_tv t - free_tv Sa") +(* case na ~: free_tv t - free_tv Sa *) + prefer 2 apply simp apply blast +(* case na : free_tv t - free_tv Sa *) +apply simp +apply (drule free_tv_app_subst_scheme_list [THEN subsetD]) + apply (fastsimp dest: codD trans [OF _ subst_comp_scheme_list] + eq_subst_scheme_list_eq_free + simp add: free_tv_subst dom_def) +(* case Let e1 e2 *) +apply (erule has_type_casesE) +apply (erule_tac x = "S'" in allE) +apply (erule_tac x = "A" in allE) +apply (erule_tac x = "t1" in allE) +apply (erule_tac x = "n" in allE) +apply (erule (1) notE impE) +apply (erule (1) notE impE) +apply safe +apply (simp (no_asm_simp)) +apply (erule_tac x = "R" in allE) +apply (erule_tac x = "gen ($ S A) t # $ S A" in allE) +apply (erule_tac x = "t'" in allE) +apply (erule_tac x = "m" in allE) +apply simp +apply (drule mp) +apply (rule has_type_le_env) +apply assumption +apply (simp (no_asm)) +apply (rule gen_bound_typ_instance) +apply (drule mp) +apply (frule new_tv_compatible_W) +apply (rule sym) +apply assumption +apply (fast dest: new_tv_compatible_gen new_tv_subst_scheme_list new_tv_W) +apply safe +apply simp +apply (rule_tac x = "Ra" in exI) +apply (simp (no_asm) add: o_def subst_comp_scheme_list [symmetric]) +done + + +lemma W_complete: "[] |- e :: t' ==> (? S t. (? m. W e [] n = Some(S,t,m)) & + (? R. t' = $ R t))" +apply (cut_tac A = "[]" and S' = "id_subst" and e = "e" and t' = "t'" in W_complete_lemma) +apply simp_all +done + end