author | oheimb |
Sat, 15 Feb 1997 17:52:31 +0100 | |
changeset 2637 | e9b203f854ae |
parent 2159 | e650a3f6f600 |
child 2891 | d8f254ad1ab9 |
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); |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
26 |
by (ALLGOALS(fast_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); |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
32 |
by (ALLGOALS(fast_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); |
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
37 |
by (ALLGOALS(fast_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'"; |
|
1974
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
41 |
by (deepen_tac (!claset addSIs [rtrancl_beta_AppL,rtrancl_beta_AppR] |
b50f96543dec
Removed refs to clasets like rel_cs etc. Used implicit claset.
nipkow
parents:
1759
diff
changeset
|
42 |
addIs [rtrancl_trans]) 3 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 |
||
1723 | 48 |
fun addsplit ss = ss addsimps [subst_Var] setloop (split_inside_tac [expand_if]); |
1120 | 49 |
|
1153 | 50 |
goal Lambda.thy "(Var k)[u/k] = u"; |
1269 | 51 |
by (asm_full_simp_tac(addsplit(!simpset)) 1); |
1120 | 52 |
qed "subst_eq"; |
53 |
||
1153 | 54 |
goal Lambda.thy "!!s. i<j ==> (Var j)[u/i] = Var(pred j)"; |
1269 | 55 |
by (asm_full_simp_tac(addsplit(!simpset)) 1); |
1120 | 56 |
qed "subst_gt"; |
57 |
||
1153 | 58 |
goal Lambda.thy "!!s. j<i ==> (Var j)[u/i] = Var(j)"; |
1269 | 59 |
by (asm_full_simp_tac (addsplit(!simpset) addsimps |
1120 | 60 |
[less_not_refl2 RS not_sym,less_SucI]) 1); |
61 |
qed "subst_lt"; |
|
62 |
||
1266 | 63 |
Addsimps [subst_eq,subst_gt,subst_lt]; |
1120 | 64 |
|
65 |
goal Lambda.thy |
|
1172 | 66 |
"!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
|
67 |
by (dB.induct_tac "t" 1); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
68 |
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]) |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2159
diff
changeset
|
69 |
addSolver cut_trans_tac))); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
70 |
by (safe_tac HOL_cs); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
71 |
by (ALLGOALS trans_tac); |
1486 | 72 |
qed_spec_mp "lift_lift"; |
1120 | 73 |
|
1153 | 74 |
goal Lambda.thy "!i j s. j < Suc i --> \ |
75 |
\ 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
|
76 |
by (dB.induct_tac "t" 1); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
77 |
by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift] |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
78 |
setloop (split_tac [expand_if,expand_nat_case]) |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2159
diff
changeset
|
79 |
addSolver cut_trans_tac))); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
80 |
by (safe_tac HOL_cs); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
81 |
by (ALLGOALS trans_tac); |
1120 | 82 |
qed "lift_subst"; |
1266 | 83 |
Addsimps [lift_subst]; |
1120 | 84 |
|
85 |
goal Lambda.thy |
|
1172 | 86 |
"!i j s. i < Suc j -->\ |
87 |
\ 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
|
88 |
by (dB.induct_tac "t" 1); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
89 |
by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift] |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
90 |
setloop (split_tac [expand_if]) |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2159
diff
changeset
|
91 |
addSolver cut_trans_tac))); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
92 |
by(safe_tac (HOL_cs addSEs [nat_neqE])); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
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); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
98 |
by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])))); |
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 |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
107 |
(!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt] |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
108 |
setloop (split_tac [expand_if,expand_nat_case]) |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2159
diff
changeset
|
109 |
addSolver cut_trans_tac))); |
2116
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
110 |
by(safe_tac (HOL_cs addSEs [nat_neqE])); |
73bbf2cc7651
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
nipkow
parents:
2031
diff
changeset
|
111 |
by(ALLGOALS trans_tac); |
1486 | 112 |
qed_spec_mp "subst_subst"; |
1153 | 113 |
|
114 |
||
115 |
(*** Equivalence proof for optimized substitution ***) |
|
116 |
||
117 |
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
|
118 |
by (dB.induct_tac "t" 1); |
2031 | 119 |
by (ALLGOALS(asm_simp_tac(addsplit(!simpset)))); |
1153 | 120 |
qed "liftn_0"; |
1266 | 121 |
Addsimps [liftn_0]; |
1153 | 122 |
|
123 |
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
|
124 |
by (dB.induct_tac "t" 1); |
2031 | 125 |
by (ALLGOALS(asm_simp_tac(addsplit(!simpset)))); |
126 |
by (fast_tac (HOL_cs addDs [add_lessD1]) 1); |
|
1153 | 127 |
qed "liftn_lift"; |
1266 | 128 |
Addsimps [liftn_lift]; |
1153 | 129 |
|
130 |
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
|
131 |
by (dB.induct_tac "t" 1); |
2031 | 132 |
by (ALLGOALS(asm_simp_tac(addsplit(!simpset)))); |
1153 | 133 |
qed "substn_subst_n"; |
1266 | 134 |
Addsimps [substn_subst_n]; |
1153 | 135 |
|
136 |
goal Lambda.thy "substn t s 0 = t[s/0]"; |
|
2031 | 137 |
by (Simp_tac 1); |
1153 | 138 |
qed "substn_subst_0"; |