--- 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];
--- 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
--- 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";
--- 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
--- 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";
--- 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
--- 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";
--- 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
--- 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<n)";
-by (fast_tac (HOL_cs addss simpset()) 1);
-qed "new_tv_TVar";
-
-Goalw [new_tv_def]
- "new_tv n (FVar m) = (m<n)";
-by (fast_tac (HOL_cs addss simpset()) 1);
-qed "new_tv_FVar";
-
-Goalw [new_tv_def]
- "new_tv n (BVar m) = True";
-by (Simp_tac 1);
-qed "new_tv_BVar";
-
-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_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<n then S k else S' k) sch = $S sch";
-by (induct_tac "sch" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "new_if_subst_type_scheme";
-Addsimps [new_if_subst_type_scheme];
-
-Goal "new_tv n (A::type_scheme list) --> \
-\ $(%k. if k<n then S k else S' k) A = $S A";
-by (induct_tac "A" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "new_if_subst_type_scheme_list";
-Addsimps [new_if_subst_type_scheme_list];
-
-
-(* constructor laws for dom and cod *)
-
-Goalw [dom_def,id_subst_def,empty_def]
- "dom id_subst = {}";
-by (Simp_tac 1);
-qed "dom_id_subst";
-Addsimps [dom_id_subst];
-
-Goalw [cod_def]
- "cod id_subst = {}";
-by (Simp_tac 1);
-qed "cod_id_subst";
-Addsimps [cod_id_subst];
-
-
-(* lemmata for free_tv *)
-
-Goalw [free_tv_subst]
- "free_tv id_subst = {}";
-by (Simp_tac 1);
-qed "free_tv_id_subst";
-Addsimps [free_tv_id_subst];
-
-Goal "!n. n < length A --> 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<n";
-by (fast_tac HOL_cs 1 );
-qed "free_tv_le_new_tv";
-
-Goalw [dom_def,cod_def,UNION_def,Bex_def]
- "[| v : free_tv(S n); v~=n |] ==> v : cod S";
-by (Simp_tac 1);
-by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
-by (assume_tac 2);
-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<m; new_tv m (S::subst) |] ==> new_tv m (S n)";
-by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
-qed "new_tv_subst_var";
-
-Goal
- "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";
--- 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<n"
(* bound_tv s: the type variables occuring bound in the type structure s *)
consts
- bound_tv :: ['a::type_struct] => 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<n)"
+
+apply (unfold new_tv_def)
+apply (fastsimp)
+done
+
+lemma new_tv_FVar:
+ "new_tv n (FVar m) = (m<n)"
+apply (unfold new_tv_def)
+apply (fastsimp)
+done
+
+lemma new_tv_BVar:
+ "new_tv n (BVar m) = True"
+apply (unfold new_tv_def)
+apply (simp (no_asm))
+done
+
+lemma new_tv_Fun:
+ "new_tv n (t1 -> 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<n then S k else S' k) sch = $S sch"
+apply (induct_tac "sch")
+apply (simp_all (no_asm_simp))
+done
+declare new_if_subst_type_scheme [simp]
+
+lemma new_if_subst_type_scheme_list: "new_tv n (A::type_scheme list) -->
+ $(%k. if k<n then S k else S' k) A = $S A"
+apply (induct_tac "A")
+apply (simp_all (no_asm_simp))
+done
+declare new_if_subst_type_scheme_list [simp]
+
+
+(* constructor laws for dom and cod *)
+
+lemma dom_id_subst:
+ "dom id_subst = {}"
+
+apply (unfold dom_def id_subst_def empty_def)
+apply (simp (no_asm))
+done
+declare dom_id_subst [simp]
+
+lemma cod_id_subst:
+ "cod id_subst = {}"
+apply (unfold cod_def)
+apply (simp (no_asm))
+done
+declare cod_id_subst [simp]
+
+
+(* lemmata for free_tv *)
+
+lemma free_tv_id_subst:
+ "free_tv id_subst = {}"
+
+apply (unfold free_tv_subst)
+apply (simp (no_asm))
+done
+declare free_tv_id_subst [simp]
+
+lemma free_tv_nth_A_impl_free_tv_A [rule_format (no_asm)]: "!n. n < length A --> 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<n"
+apply (unfold new_tv_def)
+apply (fast)
+done
+
+lemma cod_app_subst:
+ "[| v : free_tv(S n); v~=n |] ==> 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<m; new_tv m (S::subst) |] ==> 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
--- 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<n --> 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";
--- 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<n --> 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