equal
deleted
inserted
replaced
27 Addsimps [subst_not_free RS eqTrueI]; |
27 Addsimps [subst_not_free RS eqTrueI]; |
28 |
28 |
29 Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))"; |
29 Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))"; |
30 by (induct_tac "t" 1); |
30 by (induct_tac "t" 1); |
31 by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong]))); |
31 by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong]))); |
32 by (Blast_tac 2); |
32 by(Auto_tac); |
33 by (simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1); |
33 by (simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1); |
34 by (safe_tac HOL_cs); |
34 by(Auto_tac); |
35 by (ALLGOALS trans_tac); |
|
36 qed "free_lift"; |
35 qed "free_lift"; |
37 Addsimps [free_lift]; |
36 Addsimps [free_lift]; |
38 |
37 |
39 Goal "!i k t. free (s[t/k]) i = \ |
38 Goal "!i k t. free (s[t/k]) i = \ |
40 \ (free s k & free t i | free s (if i<k then i else Suc i))"; |
39 \ (free s k & free t i | free s (if i<k then i else Suc i))"; |
43 by (Blast_tac 2); |
42 by (Blast_tac 2); |
44 by (asm_full_simp_tac (addsplit (simpset())) 2); |
43 by (asm_full_simp_tac (addsplit (simpset())) 2); |
45 by (simp_tac (simpset() addsimps [diff_Suc,subst_Var] |
44 by (simp_tac (simpset() addsimps [diff_Suc,subst_Var] |
46 addsplits [nat.split]) 1); |
45 addsplits [nat.split]) 1); |
47 by (safe_tac (HOL_cs addSEs [linorder_neqE])); |
46 by (safe_tac (HOL_cs addSEs [linorder_neqE])); |
48 by (ALLGOALS trans_tac); |
47 by (ALLGOALS Simp_tac); |
49 qed "free_subst"; |
48 qed "free_subst"; |
50 Addsimps [free_subst]; |
49 Addsimps [free_subst]; |
51 |
50 |
52 Goal "s -e> t ==> !i. free t i = free s i"; |
51 Goal "s -e> t ==> !i. free t i = free s i"; |
53 by (etac eta.induct 1); |
52 by (etac eta.induct 1); |
116 qed_spec_mp "beta_subst"; |
115 qed_spec_mp "beta_subst"; |
117 AddIs [beta_subst]; |
116 AddIs [beta_subst]; |
118 |
117 |
119 Goal "!i. t[Var i/i] = t[Var(i)/Suc i]"; |
118 Goal "!i. t[Var i/i] = t[Var(i)/Suc i]"; |
120 by (induct_tac "t" 1); |
119 by (induct_tac "t" 1); |
121 by (ALLGOALS (asm_simp_tac (addsplit (simpset())))); |
120 by(auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset()))); |
122 by (safe_tac (HOL_cs addSEs [linorder_neqE])); |
|
123 by (ALLGOALS trans_tac); |
|
124 qed_spec_mp "subst_Var_Suc"; |
121 qed_spec_mp "subst_Var_Suc"; |
125 Addsimps [subst_Var_Suc]; |
122 Addsimps [subst_Var_Suc]; |
126 |
123 |
127 Goal "s -e> t ==> (!i. lift s i -e> lift t i)"; |
124 Goal "s -e> t ==> (!i. lift s i -e> lift t i)"; |
128 by (etac eta.induct 1); |
125 by (etac eta.induct 1); |