equal
deleted
inserted
replaced
80 (* lemmas for subst_to_scheme *) |
80 (* lemmas for subst_to_scheme *) |
81 |
81 |
82 Goal "new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \ |
82 Goal "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 (induct_tac "sch" 1); |
84 by (induct_tac "sch" 1); |
85 by (simp_tac (simpset() addsimps [leD]) 1); |
85 by (simp_tac (simpset() addsimps [le_def]) 1); |
86 by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 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 "t = t' ==> \ |
90 Goal "t = t' ==> \ |
95 |
95 |
96 Goal "new_tv n sch --> \ |
96 Goal "new_tv n sch --> \ |
97 \ subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \ |
97 \ subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \ |
98 \ bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch"; |
98 \ bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch"; |
99 by (induct_tac "sch" 1); |
99 by (induct_tac "sch" 1); |
100 by (simp_tac (simpset() addsimps [leD]) 1); |
100 by Auto_tac; |
101 by (Asm_simp_tac 1); |
101 by (ALLGOALS trans_tac); |
102 by (asm_full_simp_tac (simpset() addsimps [leD]) 1); |
|
103 val aux2 = result () RS mp; |
102 val aux2 = result () RS mp; |
104 |
103 |
105 |
104 |
106 (* lemmata for <= *) |
105 (* lemmata for <= *) |
107 |
106 |