isabelle: src/HOL/MiniML/W.ML@5d909faf0e04 (annotated)

1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	1	(* Title: HOL/MiniML/W.ML
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	2	ID: $Id$
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	3	Author: Dieter Nazareth and Tobias Nipkow
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	4	Copyright 1995 TU Muenchen
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	5
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	6	Correctness and completeness of type inference algorithm W
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	7	*)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	8
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	9	open W;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	10
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	11
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	12	(* stronger version of Suc_leD *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	13	goalw Nat.thy [le_def]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	14	"!!m. Suc m <= n ==> m < n";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	15	by (Asm_full_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	16	by (cut_facts_tac [less_linear] 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	17	by (fast_tac HOL_cs 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	18	qed "Suc_le_lessD";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	19	Addsimps [Suc_le_lessD];
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	20
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	21	(* correctness of W with respect to has_type *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	22	goal thy
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	23	"!a s t m n . Ok (s,t,m) = W e a n --> ($ s a \|- e :: t)";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	24	by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	25	(* case Var n *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	26	by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	27	(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	28	by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	29	setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	30	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	31	by (eres_inst_tac [("x","TVar(n) # a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	32	by( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	33	(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	34	by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	35	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	36	by( rename_tac "sa ta na sb tb nb sc" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	37	by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	38	by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	39	by (rtac (app_subst_Fun RS subst) 1);
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1300 diff changeset	40	by (res_inst_tac [("t","$ sc (tb -> (TVar nb))"),("s","$ sc ($ sb ta)")] subst 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	41	by (Asm_full_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	42	by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	43	by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	44	by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	45	by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,has_type_cl_sub,eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	46	qed "W_correct";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	47
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	48	val has_type_casesE = map(has_type.mk_cases expr.simps)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	49	[" s \|- Var n :: t"," s \|- Abs e :: t","s \|- App e1 e2 ::t"];
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	50
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	51
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	52	(* the resulting type variable is always greater or equal than the given one *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	53	goal thy
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	54	"!a n s t m. W e a n = Ok (s,t,m) --> n<=m";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	55	by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	56	(* case Var(n) *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	57	by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	58	(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	59	by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	60	by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	61	(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	62	by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	63	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	64	by (rename_tac "s t na sa ta nb sb sc tb m" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	65	by (eres_inst_tac [("x","a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	66	by (eres_inst_tac [("x","n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	67	by (eres_inst_tac [("x","$ s a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	68	by (eres_inst_tac [("x","s")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	69	by (eres_inst_tac [("x","t")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	70	by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	71	by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	72	by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	73	by (etac conjE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	74	by (eres_inst_tac [("x","sa")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	75	by (eres_inst_tac [("x","ta")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	76	by (eres_inst_tac [("x","nb")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	77	by (etac conjE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	78	by (res_inst_tac [("j","na")] le_trans 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	79	by (Asm_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	80	by (asm_simp_tac (!simpset addsimps [Suc_leD]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	81	qed "W_var_ge";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	82
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	83	Addsimps [W_var_ge];
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	84
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	85	goal thy
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	86	"!! s. Ok (s,t,m) = W e a n ==> n<=m";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	87	by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	88	qed "W_var_geD";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	89
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	90
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	91	(* auxiliary lemma *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	92	goal Maybe.thy "(y = Ok x) = (Ok x = y)";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	93	by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	94	qed "rotate_Ok";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	95
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	96
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	97	(* resulting type variable is new *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	98	goal thy
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	99	"!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) --> \
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	100	\ (new_tv m s & new_tv m t)";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	101	by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	102	(* case Var n *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	103	by (fast_tac (HOL_cs addss (!simpset
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	104	addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	105	setloop (split_tac [expand_if]))) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	106
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	107	(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	108	by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	109	setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	110	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	111	by (eres_inst_tac [("x","Suc n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	112	by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	113	by (fast_tac (HOL_cs addss (!simpset
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	114	addsimps [new_tv_subst,new_tv_Suc_list])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	115
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	116	(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	117	by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	118	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	119	by (rename_tac "s t na sa ta nb sb sc tb m" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	120	by (eres_inst_tac [("x","n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	121	by (eres_inst_tac [("x","a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	122	by (eres_inst_tac [("x","s")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	123	by (eres_inst_tac [("x","t")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	124	by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	125	by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	126	by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	127	by (eres_inst_tac [("x","$ s a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	128	by (eres_inst_tac [("x","sa")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	129	by (eres_inst_tac [("x","ta")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	130	by (eres_inst_tac [("x","nb")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	131	by( asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	132	by (rtac conjI 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	133	by (rtac new_tv_subst_comp_2 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	134	by (rtac new_tv_subst_comp_2 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	135	by (rtac (lessI RS less_imp_le RS new_tv_subst_le) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	136	by (res_inst_tac [("n","na")] new_tv_subst_le 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	137	by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	138	by (Asm_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	139	by (fast_tac (HOL_cs addDs [W_var_geD] addIs
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	140	[new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le])
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	141	1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	142	be (sym RS mgu_new) 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	143	by (fast_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_tv_list_le,
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	144	new_tv_subst_tel,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	145	new_tv_subst_le,new_tv_le]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	146	by (fast_tac (HOL_cs addDs [W_var_geD] addIs
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	147	[new_tv_list_le,new_tv_subst_tel,new_tv_le]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	148	addss (!simpset)) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	149	br (lessI RS new_tv_subst_var) 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	150	be (sym RS mgu_new) 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	151	by (fast_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	152	addDs [W_var_geD] addIs
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	153	[new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	154	new_tv_subst_le,new_tv_le] addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	155	by (fast_tac (HOL_cs addDs [W_var_geD] addIs
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	156	[new_tv_list_le,new_tv_subst_tel,new_tv_le]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	157	addss (!simpset)) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	158	bind_thm ("new_tv_W",result() RS spec RS spec RS spec RS spec RS spec RS mp RS mp);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	159
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	160
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	161	goal thy
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	162	"!n a s t m v. W e a n = Ok (s,t,m) --> \
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	163	\ (v:free_tv s \| v:free_tv t) --> v<n --> v:free_tv a";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	164	by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	165	(* case Var n *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	166	by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	167	addss (!simpset setloop (split_tac [expand_if]))) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	168
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	169	(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	170	by (asm_full_simp_tac (!simpset addsimps
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	171	[free_tv_subst] setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	172	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	173	by (rename_tac "s t na sa ta m v" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	174	by (eres_inst_tac [("x","Suc n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	175	by (eres_inst_tac [("x","TVar n # a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	176	by (eres_inst_tac [("x","s")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	177	by (eres_inst_tac [("x","t")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	178	by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	179	by (eres_inst_tac [("x","v")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	180	by (fast_tac (HOL_cs addIs [cod_app_subst] addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	181
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	182	(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	183	by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	184	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	185	by (rename_tac "s t na sa ta nb sb sc tb m v" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	186	by (eres_inst_tac [("x","n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	187	by (eres_inst_tac [("x","a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	188	by (eres_inst_tac [("x","s")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	189	by (eres_inst_tac [("x","t")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	190	by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	191	by (eres_inst_tac [("x","na")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	192	by (eres_inst_tac [("x","v")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	193	(* second case *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	194	by (eres_inst_tac [("x","$ s a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	195	by (eres_inst_tac [("x","sa")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	196	by (eres_inst_tac [("x","ta")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	197	by (eres_inst_tac [("x","nb")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	198	by (eres_inst_tac [("x","v")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	199	by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) );
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	200	by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	201	bd W_var_geD 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	202	bd W_var_geD 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	203	by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	204	by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free,
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	205	codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	206	less_le_trans,less_not_refl2,subsetD]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	207	addEs [UnE]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	208	addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	209	by (Asm_full_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	210	bd (sym RS W_var_geD) 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	211	bd (sym RS W_var_geD) 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	212	by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	213	by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	214	free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	215	less_le_trans,subsetD]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	216	addEs [UnE]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	217	addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	218	bind_thm ("free_tv_W",result() RS spec RS spec RS spec RS spec RS spec RS spec RS mp RS mp RS mp);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	219
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	220	goal HOL.thy "(~(P \| Q)) = (~P & ~Q)";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	221	by( fast_tac HOL_cs 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	222	qed "not_disj";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	223
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	224	(* Completeness of W w.r.t. has_type *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	225	goal thy
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	226	"!s' a t' n. ($ s' a \|- e :: t') --> new_tv n a --> \
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	227	\ (? s t. (? m. W e a n = Ok (s,t,m) ) & \
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	228	\ (? r. $ s' a = $ r ($ s a) & \
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	229	\ t' = $ r t ) )";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	230	by (expr.induct_tac "e" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	231	(* case Var n *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	232	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	233	by (simp_tac (!simpset addcongs [conj_cong]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	234	setloop (split_tac [expand_if])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	235	by (eresolve_tac has_type_casesE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	236	by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	237	by (res_inst_tac [("x","id_subst")] exI 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	238	by (res_inst_tac [("x","nth nat a")] exI 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	239	by (Simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	240	by (res_inst_tac [("x","s'")] exI 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	241	by (Asm_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	242
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	243	(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	244	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	245	by (eresolve_tac has_type_casesE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	246	by (eres_inst_tac [("x","%x.if x=n then t1 else (s' x)")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	247	by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	248	by (eres_inst_tac [("x","t2")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	249	by (eres_inst_tac [("x","Suc n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	250	by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	251	setloop (split_tac [expand_bind]))) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	252
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	253	(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	254	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	255	by (eresolve_tac has_type_casesE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	256	by (eres_inst_tac [("x","s'")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	257	by (eres_inst_tac [("x","a")] allE 1);
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1300 diff changeset	258	by (eres_inst_tac [("x","t2 -> t'")] allE 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	259	by (eres_inst_tac [("x","n")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	260	by (safe_tac HOL_cs);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	261	by (eres_inst_tac [("x","r")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	262	by (eres_inst_tac [("x","$ s a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	263	by (eres_inst_tac [("x","t2")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	264	by (eres_inst_tac [("x","m")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	265	bd asm_rl 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	266	bd asm_rl 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	267	bd asm_rl 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	268	by (Asm_full_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	269	by (safe_tac HOL_cs);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	270	by (fast_tac HOL_cs 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	271	by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	272	conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	273
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	274	by (subgoal_tac
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	275	"$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	276	\ else ra x)) ($ sa t) = \
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	277	\ $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1300 diff changeset	278	\ else ra x)) (ta -> (TVar ma))" 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	279	by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	280	\ (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1300 diff changeset	281	("s","($ ra ta) -> t'")] ssubst 2);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	282	by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	283	br eq_free_eq_subst_te 2;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	284	by (strip_tac 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	285	by (subgoal_tac "na ~=ma" 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	286	by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD,
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	287	new_tv_not_free_tv,new_tv_le]) 3);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	288	by (case_tac "na:free_tv sa" 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	289	(* na ~: free_tv sa *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	290	by (asm_simp_tac (!simpset addsimps [not_free_impl_id]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	291	setloop (split_tac [expand_if])) 3);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	292	(* na : free_tv sa *)
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1300 diff changeset	293	by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	294	bd eq_subst_tel_eq_free 2;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	295	by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	296	by (Asm_simp_tac 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	297	by (case_tac "na:dom sa" 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	298	(* na ~: dom sa *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	299	by (asm_full_simp_tac (!simpset addsimps [dom_def]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	300	setloop (split_tac [expand_if])) 3);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	301	(* na : dom sa *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	302	br eq_free_eq_subst_te 2;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	303	by (strip_tac 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	304	by (subgoal_tac "nb ~= ma" 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	305	by ((forward_tac [new_tv_W] 3) THEN (atac 3));
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	306	be conjE 3;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	307	bd new_tv_subst_tel 3;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	308	by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	309	by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	310	(!simpset addsimps [cod_def,free_tv_subst])) 3);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	311	by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	312	setloop (split_tac [expand_if]))) 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	313
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	314	by (Simp_tac 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	315	br eq_free_eq_subst_te 2;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	316	by (strip_tac 2 );
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	317	by (subgoal_tac "na ~= ma" 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	318	by ((forward_tac [new_tv_W] 3) THEN (atac 3));
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	319	be conjE 3;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	320	bd (sym RS W_var_geD) 3;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	321	by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	322	by (case_tac "na: free_tv t - free_tv sa" 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	323	(* case na ~: free_tv t - free_tv sa *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	324	by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	325	(* case na : free_tv t - free_tv sa *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	326	by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1300 diff changeset	327	by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	328	bd eq_subst_tel_eq_free 2;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	329	by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	330	by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,not_disj]) 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	331
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	332	by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	333	by (safe_tac HOL_cs );
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	334	bd mgu_Ok 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	335	by( fast_tac (HOL_cs addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	336	by (REPEAT (resolve_tac [exI,conjI] 1));
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	337	by (fast_tac HOL_cs 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	338	by (fast_tac HOL_cs 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	339	by ((dtac mgu_mg 1) THEN (atac 1));
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	340	be exE 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	341	by (res_inst_tac [("x","rb")] exI 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	342	br conjI 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	343	by (dres_inst_tac [("x","ma")] fun_cong 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	344	by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	345	by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1300 diff changeset	346	by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	347	(2,trans)) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	348	by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	349	br eq_free_eq_subst_tel 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	350	by( safe_tac HOL_cs );
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	351	by (subgoal_tac "ma ~= na" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	352	by ((forward_tac [new_tv_W] 2) THEN (atac 2));
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	353	be conjE 2;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	354	bd new_tv_subst_tel 2;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	355	by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	356	by (( forw_inst_tac [("xd","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	357	be conjE 2;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	358	bd (free_tv_app_subst_tel RS subsetD) 2;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	359	by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD,
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	360	new_tv_not_free_tv]) 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	361	by (case_tac "na: free_tv t - free_tv sa" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	362	(* case na ~: free_tv t - free_tv sa *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	363	by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	364	(* case na : free_tv t - free_tv sa *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	365	by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	366	bd (free_tv_app_subst_tel RS subsetD) 1;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	367	by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	368	eq_subst_tel_eq_free] addss ((!simpset addsimps
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	369	[not_disj,free_tv_subst,dom_def]))) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	370	qed "W_complete";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	371
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	372
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	373
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	374
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	375
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	376
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	377
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	378
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	379

author	nipkow
	Fri, 08 Dec 1995 19:48:15 +0100
changeset 1400	5d909faf0e04
parent 1300	c7a8f374339b
child 1465	5d7a7e439cec
permissions	-rw-r--r--