isabelle: src/HOL/MiniML/I.ML@7b95d7b49f7a (annotated)

1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	1	open I;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	2
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	3	Unify.trace_bound := 45;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	4	Unify.search_bound := 50;
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	goal thy
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	7	"! a m s s' t n. \
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	8	\ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	9	\ ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	10	by (expr.induct_tac "e" 1);
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	(* case Var n *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	13	by (simp_tac (!simpset addsimps [app_subst_list]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	14	setloop (split_tac [expand_if])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	15	by (fast_tac (HOL_cs addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	16
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	17	(* case Abs e *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	18	by (asm_full_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	19	by (strip_tac 1);
1465 5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	20	by (rtac conjI 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	21
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	22	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	23	by (REPEAT (etac allE 1));
1465 5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	24	by (etac impE 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	25	by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	26	by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	27	less_imp_le,lessI]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	28
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	29	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	30	by (REPEAT (etac allE 1));
1465 5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	31	by (etac impE 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	32	by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	33	by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	34	less_imp_le,lessI]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	35
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	36	(* case App e1 e2 *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	37	by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	38	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	39	by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1);
1465 5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	40	by (rtac conjI 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	41	by (fast_tac (HOL_cs addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	42
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	43	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	44	by (rename_tac "s1 t1' n1'" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	45	by (eres_inst_tac [("x","a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	46	by (eres_inst_tac [("x","m")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	47	by (eres_inst_tac [("x","s")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	48	by (eres_inst_tac [("x","s1'")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	49	by (eres_inst_tac [("x","t1")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	50	by (eres_inst_tac [("x","n1")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	51	by (eres_inst_tac [("x","a")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	52	by (eres_inst_tac [("x","n1")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	53	by (eres_inst_tac [("x","s1'")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	54	by (eres_inst_tac [("x","s2'")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	55	by (eres_inst_tac [("x","t2")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	56	by (eres_inst_tac [("x","n2")] allE 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	57
1465 5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	58	by (rtac conjI 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	59	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	60	by (mp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	61	by (mp_tac 1);
1465 5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	62	by (etac exE 1);
5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	63	by (etac conjE 1);
5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	64	by (etac impE 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	65	by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
1486 7b95d7b49f7a Introduced qed_spec_mp. nipkow parents: 1465 diff changeset	66	by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	67	by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	68	addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	69	by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	70
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	71	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	72	by (rename_tac "s2 t2' n2'" 1);
1465 5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	73	by (rtac conjI 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	74	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	75	by (mp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	76	by (mp_tac 1);
1465 5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	77	by (etac exE 1);
5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	78	by (etac conjE 1);
5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	79	by (etac impE 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	80	by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
1486 7b95d7b49f7a Introduced qed_spec_mp. nipkow parents: 1465 diff changeset	81	by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	82	by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	83	addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	84	by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel,subst_comp_te])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	85
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	86	by (strip_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	87	by (mp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	88	by (mp_tac 1);
1465 5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	89	by (etac exE 1);
5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	90	by (etac conjE 1);
5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	91	by (etac impE 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	92	by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
1486 7b95d7b49f7a Introduced qed_spec_mp. nipkow parents: 1465 diff changeset	93	by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	94	by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	95	addss !simpset) 1);
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	by (mp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	98	by (REPEAT (eresolve_tac [exE,conjE] 1));
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	99	by (REPEAT
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	100	((asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]) 1) THEN
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	101	(REPEAT (etac conjE 1)) THEN (hyp_subst_tac 1) ));
1465 5d7a7e439cec expanded tabs clasohm parents: 1400 diff changeset	102	by (rtac exI 1);
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	103	by (safe_tac HOL_cs);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	104	by (fast_tac HOL_cs 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	105	by (Simp_tac 2);
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	by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	108	by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	109	by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
1486 7b95d7b49f7a Introduced qed_spec_mp. nipkow parents: 1465 diff changeset	110	by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	111	by (safe_tac HOL_cs);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	112	by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	113	addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	114	by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	115	addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	116	by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	117	by ((dtac new_tv_subst_tel 1) THEN (atac 1));
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1300 diff changeset	118	by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1));
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	119	by ((dtac new_tv_subst_tel 1) THEN (atac 1));
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	120	by (fast_tac (HOL_cs addDs [new_tv_W] addss
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	121	(!simpset addsimps [subst_comp_tel])) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	122
1486 7b95d7b49f7a Introduced qed_spec_mp. nipkow parents: 1465 diff changeset	123	qed_spec_mp "I_correct_wrt_W";

author	nipkow
	Fri, 09 Feb 1996 13:41:59 +0100
changeset 1486	7b95d7b49f7a
parent 1465	5d7a7e439cec
child 1669	e56cdf711729
permissions	-rw-r--r--