author | nipkow |
Mon, 22 May 1995 14:12:40 +0200 | |
changeset 1124 | a6233ea105a4 |
parent 1120 | ff7dd80513e6 |
child 1153 | 5c5daf97cf2d |
permissions | -rw-r--r-- |
1120 | 1 |
(* Title: HOL/Lambda.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
||
6 |
Substitution-lemmas. Most of the proofs, esp. those about natural numbers, |
|
7 |
are ported from Ole Rasmussen's ZF development. In ZF, m<=n is syntactic |
|
8 |
sugar for m<Suc(n). In HOL <= is a separate operator. Hence we have to prove |
|
9 |
some compatibility lemmas. |
|
10 |
||
11 |
*) |
|
12 |
||
13 |
(*** Nat ***) |
|
14 |
||
15 |
goal Nat.thy "!!i. [| i < Suc j; j < k |] ==> i < k"; |
|
16 |
br le_less_trans 1; |
|
17 |
ba 2; |
|
18 |
by(asm_full_simp_tac (nat_ss addsimps [le_def]) 1); |
|
19 |
by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1); |
|
20 |
qed "lt_trans1"; |
|
21 |
||
22 |
goal Nat.thy "!!i. [| i < j; j < Suc(k) |] ==> i < k"; |
|
23 |
be less_le_trans 1; |
|
24 |
by(asm_full_simp_tac (nat_ss addsimps [le_def]) 1); |
|
25 |
by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1); |
|
26 |
qed "lt_trans2"; |
|
27 |
||
28 |
val major::prems = goal Nat.thy |
|
29 |
"[| i < Suc j; i < j ==> P; i = j ==> P |] ==> P"; |
|
30 |
br (major RS lessE) 1; |
|
31 |
by(ALLGOALS(asm_full_simp_tac nat_ss)); |
|
32 |
by(resolve_tac prems 1 THEN etac sym 1); |
|
33 |
by(fast_tac (HOL_cs addIs prems) 1); |
|
34 |
qed "leqE"; |
|
35 |
||
36 |
goal Arith.thy "!!i. i < j ==> Suc(pred j) = j"; |
|
37 |
by(fast_tac (HOL_cs addEs [lessE] addss arith_ss) 1); |
|
38 |
qed "Suc_pred"; |
|
39 |
||
40 |
goal Arith.thy "!!i. Suc i < j ==> i < pred j "; |
|
41 |
by (resolve_tac [Suc_less_SucD] 1); |
|
42 |
by (asm_simp_tac (arith_ss addsimps [Suc_pred]) 1); |
|
43 |
qed "lt_pred"; |
|
44 |
||
45 |
goal Arith.thy "!!i. [| i < Suc j; k < i |] ==> pred i < j "; |
|
46 |
by (resolve_tac [Suc_less_SucD] 1); |
|
47 |
by (asm_simp_tac (arith_ss addsimps [Suc_pred]) 1); |
|
48 |
qed "gt_pred"; |
|
49 |
||
50 |
(*** Lambda ***) |
|
51 |
||
52 |
open Lambda; |
|
53 |
||
54 |
val lambda_ss = arith_ss delsimps [less_Suc_eq] addsimps |
|
55 |
db.simps @ beta.intrs @ |
|
56 |
[if_not_P, not_less_eq, |
|
57 |
subst_App,subst_Fun, |
|
58 |
lift_Var,lift_App,lift_Fun]; |
|
59 |
||
60 |
val lambda_cs = HOL_cs addSIs beta.intrs; |
|
61 |
||
62 |
(*** Congruence rules for ->> ***) |
|
63 |
||
64 |
goal Lambda.thy "!!s. s ->> s' ==> Fun s ->> Fun s'"; |
|
65 |
be rtrancl_induct 1; |
|
66 |
by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
|
67 |
qed "rtrancl_beta_Fun"; |
|
68 |
||
69 |
goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t"; |
|
70 |
be rtrancl_induct 1; |
|
71 |
by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
|
72 |
qed "rtrancl_beta_AppL"; |
|
73 |
||
74 |
goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'"; |
|
75 |
be rtrancl_induct 1; |
|
76 |
by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); |
|
77 |
qed "rtrancl_beta_AppR"; |
|
78 |
||
79 |
goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'"; |
|
80 |
by (fast_tac (lambda_cs addIs |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
81 |
[rtrancl_beta_AppL,rtrancl_beta_AppR,rtrancl_trans]) 1); |
1120 | 82 |
qed "rtrancl_beta_App"; |
83 |
||
84 |
(*** subst and lift ***) |
|
85 |
||
86 |
fun addsplit ss = ss addsimps [subst_Var] setloop (split_tac [expand_if]); |
|
87 |
||
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
88 |
goal Lambda.thy "(Var n)[u/n] = u"; |
1120 | 89 |
by (asm_full_simp_tac (addsplit lambda_ss) 1); |
90 |
qed "subst_eq"; |
|
91 |
||
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
92 |
goal Lambda.thy "!!s. m<n ==> (Var n)[u/m] = Var(pred n)"; |
1120 | 93 |
by (asm_full_simp_tac (addsplit lambda_ss) 1); |
94 |
qed "subst_gt"; |
|
95 |
||
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
96 |
goal Lambda.thy "!!s. n<m ==> (Var n)[u/m] = Var(n)"; |
1120 | 97 |
by (asm_full_simp_tac (addsplit lambda_ss addsimps |
98 |
[less_not_refl2 RS not_sym,less_SucI]) 1); |
|
99 |
qed "subst_lt"; |
|
100 |
||
101 |
val lambda_ss = lambda_ss addsimps [subst_eq,subst_gt,subst_lt]; |
|
102 |
||
103 |
goal Lambda.thy |
|
104 |
"!n i. i < Suc n --> lift (lift s i) (Suc n) = lift (lift s n) i"; |
|
105 |
by(db.induct_tac "s" 1); |
|
106 |
by(ALLGOALS(asm_simp_tac lambda_ss)); |
|
107 |
by(strip_tac 1); |
|
108 |
by (excluded_middle_tac "nat < i" 1); |
|
109 |
by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); |
|
110 |
by (ALLGOALS(asm_full_simp_tac ((addsplit lambda_ss) addsimps [less_SucI]))); |
|
111 |
qed"lift_lift"; |
|
112 |
||
113 |
goal Lambda.thy "!m n s. n < Suc m --> \ |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
114 |
\ lift (t[s/n]) m = (lift t (Suc m)) [lift s m / n]"; |
1120 | 115 |
by(db.induct_tac "t" 1); |
116 |
by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift]))); |
|
117 |
by(strip_tac 1); |
|
118 |
by (excluded_middle_tac "nat < n" 1); |
|
119 |
by (asm_full_simp_tac lambda_ss 1); |
|
120 |
by (eres_inst_tac [("j","nat")] leqE 1); |
|
121 |
by (asm_full_simp_tac ((addsplit lambda_ss) |
|
122 |
addsimps [less_SucI,gt_pred,Suc_pred]) 1); |
|
123 |
by (hyp_subst_tac 1); |
|
124 |
by (asm_simp_tac lambda_ss 1); |
|
125 |
by (forw_inst_tac [("j","n")] lt_trans2 1); |
|
126 |
by (assume_tac 1); |
|
127 |
by (asm_full_simp_tac (addsplit lambda_ss addsimps [less_SucI]) 1); |
|
128 |
qed "lift_subst"; |
|
129 |
val lambda_ss = lambda_ss addsimps [lift_subst]; |
|
130 |
||
131 |
goal Lambda.thy |
|
132 |
"!n m u. m < Suc n -->\ |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
133 |
\ lift (v[u/n]) m = (lift v m) [lift u m / Suc n]"; |
1120 | 134 |
by(db.induct_tac "v" 1); |
135 |
by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift]))); |
|
136 |
by(strip_tac 1); |
|
137 |
by (excluded_middle_tac "nat < n" 1); |
|
138 |
by (asm_full_simp_tac lambda_ss 1); |
|
139 |
by (eres_inst_tac [("i","n")] leqE 1); |
|
140 |
by (forward_tac [lt_trans1] 1 THEN assume_tac 1); |
|
141 |
by (ALLGOALS(asm_full_simp_tac |
|
142 |
(lambda_ss addsimps [Suc_pred,less_SucI,gt_pred]))); |
|
143 |
by (hyp_subst_tac 1); |
|
144 |
by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1); |
|
145 |
by(split_tac [expand_if] 1); |
|
146 |
by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1); |
|
147 |
qed "lift_subst_lt"; |
|
148 |
||
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
149 |
goal Lambda.thy "!n v. (lift u n)[v/n] = u"; |
1120 | 150 |
by(db.induct_tac "u" 1); |
151 |
by(ALLGOALS(asm_simp_tac lambda_ss)); |
|
152 |
by(split_tac [expand_if] 1); |
|
153 |
by(ALLGOALS(asm_full_simp_tac lambda_ss)); |
|
154 |
qed "subst_lift"; |
|
155 |
val lambda_ss = lambda_ss addsimps [subst_lift]; |
|
156 |
||
157 |
||
158 |
goal Lambda.thy "!m n u w. m < Suc n --> \ |
|
1124
a6233ea105a4
Polished the presentation making it completely definitional.
nipkow
parents:
1120
diff
changeset
|
159 |
\ (v[lift w m / Suc n]) [u[w/n]/m] = (v[u/m])[w/n]"; |
1120 | 160 |
by(db.induct_tac "v" 1); |
161 |
by (ALLGOALS(asm_simp_tac (lambda_ss addsimps |
|
162 |
[lift_lift RS spec RS spec RS mp RS sym,lift_subst_lt]))); |
|
163 |
by(strip_tac 1); |
|
164 |
by (excluded_middle_tac "nat < Suc(Suc n)" 1); |
|
165 |
by(asm_full_simp_tac lambda_ss 1); |
|
166 |
by (forward_tac [lessI RS less_trans] 1); |
|
167 |
by (eresolve_tac [leqE] 1); |
|
168 |
by (asm_simp_tac (lambda_ss addsimps [Suc_pred,lt_pred]) 2); |
|
169 |
by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1); |
|
170 |
by (forw_inst_tac [("i","m")] (lessI RS less_trans) 1); |
|
171 |
by (asm_simp_tac (lambda_ss addsimps [Suc_pred,lt_pred]) 1); |
|
172 |
by (eres_inst_tac [("i","nat")] leqE 1); |
|
173 |
by (asm_full_simp_tac (lambda_ss addsimps [Suc_pred,less_SucI]) 2); |
|
174 |
by (excluded_middle_tac "nat < m" 1); |
|
175 |
by (asm_full_simp_tac lambda_ss 1); |
|
176 |
by (eres_inst_tac [("j","nat")] leqE 1); |
|
177 |
by (asm_simp_tac (lambda_ss addsimps [gt_pred]) 1); |
|
178 |
by (asm_simp_tac lambda_ss 1); |
|
179 |
by (forward_tac [lt_trans2] 1 THEN assume_tac 1); |
|
180 |
by (asm_simp_tac (lambda_ss addsimps [gt_pred]) 1); |
|
181 |
bind_thm("subst_subst", result() RS spec RS spec RS spec RS spec RS mp); |