19 val dB_case_distinction = |
19 val dB_case_distinction = |
20 rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])dB.induct; |
20 rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])dB.induct; |
21 |
21 |
22 (*** Congruence rules for ->> ***) |
22 (*** Congruence rules for ->> ***) |
23 |
23 |
24 goal Lambda.thy "!!s. s ->> s' ==> Abs s ->> Abs s'"; |
24 Goal "!!s. s ->> s' ==> Abs s ->> Abs s'"; |
25 by (etac rtrancl_induct 1); |
25 by (etac rtrancl_induct 1); |
26 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
26 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
27 qed "rtrancl_beta_Abs"; |
27 qed "rtrancl_beta_Abs"; |
28 AddSIs [rtrancl_beta_Abs]; |
28 AddSIs [rtrancl_beta_Abs]; |
29 |
29 |
30 goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t"; |
30 Goal "!!s. s ->> s' ==> s @ t ->> s' @ t"; |
31 by (etac rtrancl_induct 1); |
31 by (etac rtrancl_induct 1); |
32 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
32 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
33 qed "rtrancl_beta_AppL"; |
33 qed "rtrancl_beta_AppL"; |
34 |
34 |
35 goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'"; |
35 Goal "!!s. t ->> t' ==> s @ t ->> s @ t'"; |
36 by (etac rtrancl_induct 1); |
36 by (etac rtrancl_induct 1); |
37 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
37 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
38 qed "rtrancl_beta_AppR"; |
38 qed "rtrancl_beta_AppR"; |
39 |
39 |
40 goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'"; |
40 Goal "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'"; |
41 by (blast_tac (claset() addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR] |
41 by (blast_tac (claset() addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR] |
42 addIs [rtrancl_trans]) 1); |
42 addIs [rtrancl_trans]) 1); |
43 qed "rtrancl_beta_App"; |
43 qed "rtrancl_beta_App"; |
44 AddIs [rtrancl_beta_App]; |
44 AddIs [rtrancl_beta_App]; |
45 |
45 |
47 |
47 |
48 fun addsplit ss = ss addsimps [subst_Var] |
48 fun addsplit ss = ss addsimps [subst_Var] |
49 delsplits [split_if] |
49 delsplits [split_if] |
50 setloop (split_inside_tac [split_if]); |
50 setloop (split_inside_tac [split_if]); |
51 |
51 |
52 goal Lambda.thy "(Var k)[u/k] = u"; |
52 Goal "(Var k)[u/k] = u"; |
53 by (asm_full_simp_tac(addsplit(simpset())) 1); |
53 by (asm_full_simp_tac(addsplit(simpset())) 1); |
54 qed "subst_eq"; |
54 qed "subst_eq"; |
55 |
55 |
56 goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(j-1)"; |
56 Goal "!!s. i<j ==> (Var j)[u/i] = Var(j-1)"; |
57 by (asm_full_simp_tac(addsplit(simpset())) 1); |
57 by (asm_full_simp_tac(addsplit(simpset())) 1); |
58 qed "subst_gt"; |
58 qed "subst_gt"; |
59 |
59 |
60 goal Lambda.thy "!!s. j<i ==> (Var j)[u/i] = Var(j)"; |
60 Goal "!!s. j<i ==> (Var j)[u/i] = Var(j)"; |
61 by (asm_full_simp_tac (addsplit(simpset()) addsimps |
61 by (asm_full_simp_tac (addsplit(simpset()) addsimps |
62 [less_not_refl2 RS not_sym,less_SucI]) 1); |
62 [less_not_refl2 RS not_sym,less_SucI]) 1); |
63 qed "subst_lt"; |
63 qed "subst_lt"; |
64 |
64 |
65 Addsimps [subst_eq,subst_gt,subst_lt]; |
65 Addsimps [subst_eq,subst_gt,subst_lt]; |
66 |
66 |
67 goal Lambda.thy |
67 Goal |
68 "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i"; |
68 "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i"; |
69 by (dB.induct_tac "t" 1); |
69 by (dB.induct_tac "t" 1); |
70 by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac))); |
70 by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac))); |
71 by (safe_tac HOL_cs); |
71 by (safe_tac HOL_cs); |
72 by (ALLGOALS trans_tac); |
72 by (ALLGOALS trans_tac); |
73 qed_spec_mp "lift_lift"; |
73 qed_spec_mp "lift_lift"; |
74 |
74 |
75 goal Lambda.thy "!i j s. j < Suc i --> \ |
75 Goal "!i j s. j < Suc i --> \ |
76 \ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]"; |
76 \ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]"; |
77 by (dB.induct_tac "t" 1); |
77 by (dB.induct_tac "t" 1); |
78 by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift] |
78 by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift] |
79 addsplits [split_nat_case] |
79 addsplits [split_nat_case] |
80 addSolver cut_trans_tac))); |
80 addSolver cut_trans_tac))); |
81 by (safe_tac HOL_cs); |
81 by (safe_tac HOL_cs); |
82 by (ALLGOALS trans_tac); |
82 by (ALLGOALS trans_tac); |
83 qed "lift_subst"; |
83 qed "lift_subst"; |
84 Addsimps [lift_subst]; |
84 Addsimps [lift_subst]; |
85 |
85 |
86 goal Lambda.thy |
86 Goal |
87 "!i j s. i < Suc j -->\ |
87 "!i j s. i < Suc j -->\ |
88 \ lift (t[s/j]) i = (lift t i) [lift s i / Suc j]"; |
88 \ lift (t[s/j]) i = (lift t i) [lift s i / Suc j]"; |
89 by (dB.induct_tac "t" 1); |
89 by (dB.induct_tac "t" 1); |
90 by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift] |
90 by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift] |
91 addSolver cut_trans_tac))); |
91 addSolver cut_trans_tac))); |
92 by (safe_tac (HOL_cs addSEs [nat_neqE])); |
92 by (safe_tac (HOL_cs addSEs [nat_neqE])); |
93 by (ALLGOALS trans_tac); |
93 by (ALLGOALS trans_tac); |
94 qed "lift_subst_lt"; |
94 qed "lift_subst_lt"; |
95 |
95 |
96 goal Lambda.thy "!k s. (lift t k)[s/k] = t"; |
96 Goal "!k s. (lift t k)[s/k] = t"; |
97 by (dB.induct_tac "t" 1); |
97 by (dB.induct_tac "t" 1); |
98 by (ALLGOALS Asm_full_simp_tac); |
98 by (ALLGOALS Asm_full_simp_tac); |
99 qed "subst_lift"; |
99 qed "subst_lift"; |
100 Addsimps [subst_lift]; |
100 Addsimps [subst_lift]; |
101 |
101 |
102 |
102 |
103 goal Lambda.thy "!i j u v. i < Suc j --> \ |
103 Goal "!i j u v. i < Suc j --> \ |
104 \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"; |
104 \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"; |
105 by (dB.induct_tac "t" 1); |
105 by (dB.induct_tac "t" 1); |
106 by (ALLGOALS(asm_simp_tac |
106 by (ALLGOALS(asm_simp_tac |
107 (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt] |
107 (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt] |
108 delsplits [split_if] |
108 delsplits [split_if] |
114 qed_spec_mp "subst_subst"; |
114 qed_spec_mp "subst_subst"; |
115 |
115 |
116 |
116 |
117 (*** Equivalence proof for optimized substitution ***) |
117 (*** Equivalence proof for optimized substitution ***) |
118 |
118 |
119 goal Lambda.thy "!k. liftn 0 t k = t"; |
119 Goal "!k. liftn 0 t k = t"; |
120 by (dB.induct_tac "t" 1); |
120 by (dB.induct_tac "t" 1); |
121 by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
121 by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
122 qed "liftn_0"; |
122 qed "liftn_0"; |
123 Addsimps [liftn_0]; |
123 Addsimps [liftn_0]; |
124 |
124 |
125 goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k"; |
125 Goal "!k. liftn (Suc n) t k = lift (liftn n t k) k"; |
126 by (dB.induct_tac "t" 1); |
126 by (dB.induct_tac "t" 1); |
127 by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
127 by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
128 by (blast_tac (claset() addDs [add_lessD1]) 1); |
128 by (blast_tac (claset() addDs [add_lessD1]) 1); |
129 qed "liftn_lift"; |
129 qed "liftn_lift"; |
130 Addsimps [liftn_lift]; |
130 Addsimps [liftn_lift]; |
131 |
131 |
132 goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]"; |
132 Goal "!n. substn t s n = t[liftn n s 0 / n]"; |
133 by (dB.induct_tac "t" 1); |
133 by (dB.induct_tac "t" 1); |
134 by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
134 by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
135 qed "substn_subst_n"; |
135 qed "substn_subst_n"; |
136 Addsimps [substn_subst_n]; |
136 Addsimps [substn_subst_n]; |
137 |
137 |
138 goal Lambda.thy "substn t s 0 = t[s/0]"; |
138 Goal "substn t s 0 = t[s/0]"; |
139 by (Simp_tac 1); |
139 by (Simp_tac 1); |
140 qed "substn_subst_0"; |
140 qed "substn_subst_0"; |