equal
deleted
inserted
replaced
64 by (REPEAT ((dtac mp 1) THEN (Fast_tac 1))); |
64 by (REPEAT ((dtac mp 1) THEN (Fast_tac 1))); |
65 by Safe_tac; |
65 by Safe_tac; |
66 by (rename_tac "S1 S2" 1); |
66 by (rename_tac "S1 S2" 1); |
67 by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1); |
67 by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1); |
68 by Safe_tac; |
68 by Safe_tac; |
69 by (asm_simp_tac (simpset() addsplits [expand_if]) 1); |
69 by (Asm_simp_tac 1); |
70 by (asm_simp_tac (simpset() addsplits [expand_if]) 1); |
70 by (Asm_simp_tac 1); |
71 by (strip_tac 1); |
71 by (strip_tac 1); |
72 by (dres_inst_tac [("x","x")] bspec 1); |
72 by (dres_inst_tac [("x","x")] bspec 1); |
73 by (assume_tac 1); |
73 by (assume_tac 1); |
74 by (dres_inst_tac [("x","x")] bspec 1); |
74 by (dres_inst_tac [("x","x")] bspec 1); |
75 by (Asm_simp_tac 1); |
75 by (Asm_simp_tac 1); |
80 (* lemmatas for subst_to_scheme *) |
80 (* lemmatas for subst_to_scheme *) |
81 |
81 |
82 goal thy "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \ |
82 goal thy "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \ |
83 \ (bound_typ_inst (%k. TVar (k + n)) sch) = sch"; |
83 \ (bound_typ_inst (%k. TVar (k + n)) sch) = sch"; |
84 by (type_scheme.induct_tac "sch" 1); |
84 by (type_scheme.induct_tac "sch" 1); |
85 by (simp_tac (simpset() addsimps [leD] addsplits [expand_if]) 1); |
85 by (simp_tac (simpset() addsimps [leD]) 1); |
86 by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2] addsplits [expand_if]) 1); |
86 by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1); |
87 by (Asm_simp_tac 1); |
87 by (Asm_simp_tac 1); |
88 qed_spec_mp "subst_to_scheme_inverse"; |
88 qed_spec_mp "subst_to_scheme_inverse"; |
89 |
89 |
90 goal thy "!!t t'. t = t' ==> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t = \ |
90 goal thy "!!t t'. t = t' ==> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t = \ |
91 \ subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t'"; |
91 \ subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t'"; |
94 |
94 |
95 goal thy "new_tv n sch --> \ |
95 goal thy "new_tv n sch --> \ |
96 \ (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \ |
96 \ (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \ |
97 \ bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)"; |
97 \ bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)"; |
98 by (type_scheme.induct_tac "sch" 1); |
98 by (type_scheme.induct_tac "sch" 1); |
99 by (simp_tac (simpset() addsplits [expand_if] addsimps [leD]) 1); |
99 by (simp_tac (simpset() addsimps [leD]) 1); |
100 by (Asm_simp_tac 1); |
100 by (Asm_simp_tac 1); |
101 by (asm_full_simp_tac (simpset() addsplits [expand_if] addsimps [leD]) 1); |
101 by (asm_full_simp_tac (simpset() addsimps [leD]) 1); |
102 val aux2 = result () RS mp; |
102 val aux2 = result () RS mp; |
103 |
103 |
104 |
104 |
105 (* lemmata for <= *) |
105 (* lemmata for <= *) |
106 |
106 |