equal
deleted
inserted
replaced
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 delsplits [expand_if] |
49 delsplits [split_if] |
50 setloop (split_inside_tac [expand_if]); |
50 setloop (split_inside_tac [split_if]); |
51 |
51 |
52 goal Lambda.thy "(Var k)[u/k] = u"; |
52 goal Lambda.thy "(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 |
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 [diff_Suc,subst_Var,lift_lift] |
78 by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift] |
79 addsplits [expand_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]; |
103 goal Lambda.thy "!i j u v. i < Suc j --> \ |
103 goal Lambda.thy "!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 [expand_if] |
108 delsplits [split_if] |
109 addsplits [expand_nat_case] |
109 addsplits [split_nat_case] |
110 addloop ("if",split_inside_tac[expand_if]) |
110 addloop ("if",split_inside_tac[split_if]) |
111 addSolver cut_trans_tac))); |
111 addSolver cut_trans_tac))); |
112 by (safe_tac (HOL_cs addSEs [nat_neqE])); |
112 by (safe_tac (HOL_cs addSEs [nat_neqE])); |
113 by (ALLGOALS trans_tac); |
113 by (ALLGOALS trans_tac); |
114 qed_spec_mp "subst_subst"; |
114 qed_spec_mp "subst_subst"; |
115 |
115 |