43 qed "rtrancl_beta_App"; |
43 qed "rtrancl_beta_App"; |
44 AddIs [rtrancl_beta_App]; |
44 AddIs [rtrancl_beta_App]; |
45 |
45 |
46 (*** subst and lift ***) |
46 (*** subst and lift ***) |
47 |
47 |
48 fun addsplit ss = ss addsimps [subst_Var] |
48 fun addsplit ss = ss addsimps [subst_Var] |
49 setloop (split_inside_tac [expand_if]); |
49 setloop (split_inside_tac [expand_if]); |
50 |
50 |
51 goal Lambda.thy "(Var k)[u/k] = u"; |
51 goal Lambda.thy "(Var k)[u/k] = u"; |
52 by (asm_full_simp_tac(addsplit(!simpset)) 1); |
52 by (asm_full_simp_tac(addsplit(!simpset)) 1); |
53 qed "subst_eq"; |
53 qed "subst_eq"; |
54 |
54 |
64 Addsimps [subst_eq,subst_gt,subst_lt]; |
64 Addsimps [subst_eq,subst_gt,subst_lt]; |
65 |
65 |
66 goal Lambda.thy |
66 goal Lambda.thy |
67 "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i"; |
67 "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i"; |
68 by (dB.induct_tac "t" 1); |
68 by (dB.induct_tac "t" 1); |
69 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]) |
69 by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if] |
70 addSolver cut_trans_tac))); |
70 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 Lambda.thy "!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 [pred_def,subst_Var,lift_lift] |
78 by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift] |
79 setloop (split_tac [expand_if,expand_nat_case]) |
79 addsplits [expand_if,expand_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]; |
86 goal Lambda.thy |
86 goal Lambda.thy |
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 setloop (split_tac [expand_if]) |
91 addsplits [expand_if] |
92 addSolver cut_trans_tac))); |
92 addSolver cut_trans_tac))); |
93 by (safe_tac (HOL_cs addSEs [nat_neqE])); |
93 by (safe_tac (HOL_cs addSEs [nat_neqE])); |
94 by (ALLGOALS trans_tac); |
94 by (ALLGOALS trans_tac); |
95 qed "lift_subst_lt"; |
95 qed "lift_subst_lt"; |
96 |
96 |
97 goal Lambda.thy "!k s. (lift t k)[s/k] = t"; |
97 goal Lambda.thy "!k s. (lift t k)[s/k] = t"; |
98 by (dB.induct_tac "t" 1); |
98 by (dB.induct_tac "t" 1); |
99 by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])))); |
99 by (ALLGOALS (asm_full_simp_tac (!simpset addsplits [expand_if]))); |
100 qed "subst_lift"; |
100 qed "subst_lift"; |
101 Addsimps [subst_lift]; |
101 Addsimps [subst_lift]; |
102 |
102 |
103 |
103 |
104 goal Lambda.thy "!i j u v. i < Suc j --> \ |
104 goal Lambda.thy "!i j u v. i < Suc j --> \ |
105 \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"; |
105 \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"; |
106 by (dB.induct_tac "t" 1); |
106 by (dB.induct_tac "t" 1); |
107 by (ALLGOALS(asm_simp_tac |
107 by (ALLGOALS(asm_simp_tac |
108 (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt] |
108 (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt] |
109 setloop (split_tac [expand_if,expand_nat_case]) |
109 addsplits [expand_if,expand_nat_case] |
110 addSolver cut_trans_tac))); |
110 addSolver cut_trans_tac))); |
111 by (safe_tac (HOL_cs addSEs [nat_neqE])); |
111 by (safe_tac (HOL_cs addSEs [nat_neqE])); |
112 by (ALLGOALS trans_tac); |
112 by (ALLGOALS trans_tac); |
113 qed_spec_mp "subst_subst"; |
113 qed_spec_mp "subst_subst"; |
114 |
114 |