author | oheimb |
Mon, 27 Apr 1998 19:29:19 +0200 | |
changeset 4836 | fc5773ae2790 |
parent 4831 | dae4d63a1318 |
child 5069 | 3ea049f7979d |
permissions | -rw-r--r-- |
1269 | 1 |
(* Title: HOL/Lambda/Lambda.ML |
1120 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
||
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
6 |
Substitution-lemmas. |
1120 | 7 |
*) |
8 |
||
9 |
(*** Lambda ***) |
|
10 |
||
11 |
open Lambda; |
|
12 |
||
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
13 |
Delsimps [subst_Var]; |
1269 | 14 |
Addsimps ([if_not_P, not_less_eq] @ beta.intrs); |
1120 | 15 |
|
1302 | 16 |
(* don't add r_into_rtrancl! *) |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
17 |
AddSIs beta.intrs; |
1120 | 18 |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
19 |
val dB_case_distinction = |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
20 |
rule_by_tactic(EVERY[etac thin_rl 2,etac thin_rl 2,etac thin_rl 3])dB.induct; |
1759
a42d6c537f4a
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow
parents:
1723
diff
changeset
|
21 |
|
1120 | 22 |
(*** Congruence rules for ->> ***) |
23 |
||
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
24 |
goal Lambda.thy "!!s. s ->> s' ==> Abs s ->> Abs s'"; |
1465 | 25 |
by (etac rtrancl_induct 1); |
4089 | 26 |
by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
27 |
qed "rtrancl_beta_Abs"; |
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
28 |
AddSIs [rtrancl_beta_Abs]; |
1120 | 29 |
|
30 |
goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t"; |
|
1465 | 31 |
by (etac rtrancl_induct 1); |
4089 | 32 |
by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
1120 | 33 |
qed "rtrancl_beta_AppL"; |
34 |
||
35 |
goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'"; |
|
1465 | 36 |
by (etac rtrancl_induct 1); |
4089 | 37 |
by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl]))); |
1120 | 38 |
qed "rtrancl_beta_AppR"; |
39 |
||
40 |
goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'"; |
|
4089 | 41 |
by (blast_tac (claset() addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR] |
2922 | 42 |
addIs [rtrancl_trans]) 1); |
1120 | 43 |
qed "rtrancl_beta_App"; |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
44 |
AddIs [rtrancl_beta_App]; |
1120 | 45 |
|
46 |
(*** subst and lift ***) |
|
47 |
||
3919 | 48 |
fun addsplit ss = ss addsimps [subst_Var] |
4831 | 49 |
delsplits [split_if] |
50 |
setloop (split_inside_tac [split_if]); |
|
1120 | 51 |
|
1153 | 52 |
goal Lambda.thy "(Var k)[u/k] = u"; |
4089 | 53 |
by (asm_full_simp_tac(addsplit(simpset())) 1); |
1120 | 54 |
qed "subst_eq"; |
55 |
||
4360 | 56 |
goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(j-1)"; |
4089 | 57 |
by (asm_full_simp_tac(addsplit(simpset())) 1); |
1120 | 58 |
qed "subst_gt"; |
59 |
||
1153 | 60 |
goal Lambda.thy "!!s. j<i ==> (Var j)[u/i] = Var(j)"; |
4089 | 61 |
by (asm_full_simp_tac (addsplit(simpset()) addsimps |
1120 | 62 |
[less_not_refl2 RS not_sym,less_SucI]) 1); |
63 |
qed "subst_lt"; |
|
64 |
||
1266 | 65 |
Addsimps [subst_eq,subst_gt,subst_lt]; |
1120 | 66 |
|
67 |
goal Lambda.thy |
|
1172 | 68 |
"!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i"; |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
69 |
by (dB.induct_tac "t" 1); |
4686 | 70 |
by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac))); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
71 |
by (safe_tac HOL_cs); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
72 |
by (ALLGOALS trans_tac); |
1486 | 73 |
qed_spec_mp "lift_lift"; |
1120 | 74 |
|
1153 | 75 |
goal Lambda.thy "!i j s. j < Suc i --> \ |
76 |
\ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]"; |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
77 |
by (dB.induct_tac "t" 1); |
4360 | 78 |
by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift] |
4831 | 79 |
addsplits [split_nat_case] |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2159
diff
changeset
|
80 |
addSolver cut_trans_tac))); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
81 |
by (safe_tac HOL_cs); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
82 |
by (ALLGOALS trans_tac); |
1120 | 83 |
qed "lift_subst"; |
1266 | 84 |
Addsimps [lift_subst]; |
1120 | 85 |
|
86 |
goal Lambda.thy |
|
1172 | 87 |
"!i j s. i < Suc j -->\ |
88 |
\ lift (t[s/j]) i = (lift t i) [lift s i / Suc j]"; |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
89 |
by (dB.induct_tac "t" 1); |
4089 | 90 |
by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift] |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2159
diff
changeset
|
91 |
addSolver cut_trans_tac))); |
2922 | 92 |
by (safe_tac (HOL_cs addSEs [nat_neqE])); |
93 |
by (ALLGOALS trans_tac); |
|
1120 | 94 |
qed "lift_subst_lt"; |
95 |
||
1172 | 96 |
goal Lambda.thy "!k s. (lift t k)[s/k] = t"; |
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
97 |
by (dB.induct_tac "t" 1); |
4686 | 98 |
by (ALLGOALS Asm_full_simp_tac); |
1120 | 99 |
qed "subst_lift"; |
1266 | 100 |
Addsimps [subst_lift]; |
1120 | 101 |
|
102 |
||
1172 | 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]"; |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
105 |
by (dB.induct_tac "t" 1); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
106 |
by (ALLGOALS(asm_simp_tac |
4360 | 107 |
(simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt] |
4831 | 108 |
delsplits [split_if] |
109 |
addsplits [split_nat_case] |
|
110 |
addloop ("if",split_inside_tac[split_if]) |
|
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2159
diff
changeset
|
111 |
addSolver cut_trans_tac))); |
2922 | 112 |
by (safe_tac (HOL_cs addSEs [nat_neqE])); |
113 |
by (ALLGOALS trans_tac); |
|
1486 | 114 |
qed_spec_mp "subst_subst"; |
1153 | 115 |
|
116 |
||
117 |
(*** Equivalence proof for optimized substitution ***) |
|
118 |
||
119 |
goal Lambda.thy "!k. liftn 0 t k = t"; |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
120 |
by (dB.induct_tac "t" 1); |
4089 | 121 |
by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
1153 | 122 |
qed "liftn_0"; |
1266 | 123 |
Addsimps [liftn_0]; |
1153 | 124 |
|
125 |
goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k"; |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
126 |
by (dB.induct_tac "t" 1); |
4089 | 127 |
by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
128 |
by (blast_tac (claset() addDs [add_lessD1]) 1); |
|
1153 | 129 |
qed "liftn_lift"; |
1266 | 130 |
Addsimps [liftn_lift]; |
1153 | 131 |
|
132 |
goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]"; |
|
2159
e650a3f6f600
Used nat_trans_tac. New Eta. various smaller changes.
nipkow
parents:
2116
diff
changeset
|
133 |
by (dB.induct_tac "t" 1); |
4089 | 134 |
by (ALLGOALS(asm_simp_tac(addsplit(simpset())))); |
1153 | 135 |
qed "substn_subst_n"; |
1266 | 136 |
Addsimps [substn_subst_n]; |
1153 | 137 |
|
138 |
goal Lambda.thy "substn t s 0 = t[s/0]"; |
|
2031 | 139 |
by (Simp_tac 1); |
1153 | 140 |
qed "substn_subst_0"; |