equal
deleted
inserted
replaced
32 by (Auto_tac); |
32 by (Auto_tac); |
33 qed "free_lift"; |
33 qed "free_lift"; |
34 Addsimps [free_lift]; |
34 Addsimps [free_lift]; |
35 |
35 |
36 Goal "!i k t. free (s[t/k]) i = \ |
36 Goal "!i k t. free (s[t/k]) i = \ |
37 \ (free s k & free t i | free s (if i<k then i else Suc i))"; |
37 \ (free s k & free t i | free s (if i<k then i else i+1))"; |
38 by (induct_tac "s" 1); |
38 by (induct_tac "s" 1); |
39 by (Asm_simp_tac 2); |
39 by (Asm_simp_tac 2); |
40 by (Blast_tac 2); |
40 by (Blast_tac 2); |
41 by (asm_full_simp_tac (addsplit (simpset())) 2); |
41 by (asm_full_simp_tac (addsplit (simpset())) 2); |
42 by (simp_tac (simpset() addsimps [diff_Suc,subst_Var] |
42 by (simp_tac (simpset() addsimps [diff_Suc,subst_Var] |
111 by (etac beta.induct 1); |
111 by (etac beta.induct 1); |
112 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_subst RS sym]))); |
112 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_subst RS sym]))); |
113 qed_spec_mp "beta_subst"; |
113 qed_spec_mp "beta_subst"; |
114 AddIs [beta_subst]; |
114 AddIs [beta_subst]; |
115 |
115 |
116 Goal "!i. t[Var i/i] = t[Var(i)/Suc i]"; |
116 Goal "!i. t[Var i/i] = t[Var(i)/i+1]"; |
117 by (induct_tac "t" 1); |
117 by (induct_tac "t" 1); |
118 by (auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset()))); |
118 by (auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset()))); |
119 qed_spec_mp "subst_Var_Suc"; |
119 qed_spec_mp "subst_Var_Suc"; |
120 Addsimps [subst_Var_Suc]; |
120 Addsimps [subst_Var_Suc]; |
121 |
121 |