author | huffman |
Thu, 17 Dec 2009 07:02:13 -0800 | |
changeset 34111 | 1b015caba46c |
parent 32154 | 9721e8e4d48c |
child 35113 | 1a0c129bb2e0 |
permissions | -rw-r--r-- |
17456 | 1 |
(* Title: CCL/Term.thy |
1474 | 2 |
Author: Martin Coen |
0 | 3 |
Copyright 1993 University of Cambridge |
4 |
*) |
|
5 |
||
17456 | 6 |
header {* Definitions of usual program constructs in CCL *} |
7 |
||
8 |
theory Term |
|
9 |
imports CCL |
|
10 |
begin |
|
0 | 11 |
|
12 |
consts |
|
13 |
||
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
14 |
one :: "i" |
0 | 15 |
|
19796 | 16 |
"if" :: "[i,i,i]=>i" ("(3if _/ then _/ else _)" [0,0,60] 60) |
0 | 17 |
|
17456 | 18 |
inl :: "i=>i" |
19 |
inr :: "i=>i" |
|
20 |
when :: "[i,i=>i,i=>i]=>i" |
|
0 | 21 |
|
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
22 |
split :: "[i,[i,i]=>i]=>i" |
17456 | 23 |
fst :: "i=>i" |
24 |
snd :: "i=>i" |
|
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
25 |
thd :: "i=>i" |
0 | 26 |
|
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
27 |
zero :: "i" |
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
28 |
succ :: "i=>i" |
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
29 |
ncase :: "[i,i,i=>i]=>i" |
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
30 |
nrec :: "[i,i,[i,i]=>i]=>i" |
0 | 31 |
|
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
32 |
nil :: "i" ("([])") |
24825 | 33 |
cons :: "[i,i]=>i" (infixr "$" 80) |
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
34 |
lcase :: "[i,i,[i,i]=>i]=>i" |
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
35 |
lrec :: "[i,i,[i,i,i]=>i]=>i" |
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
36 |
|
17456 | 37 |
"let" :: "[i,i=>i]=>i" |
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
38 |
letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" |
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
39 |
letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" |
17456 | 40 |
letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" |
0 | 41 |
|
14765 | 42 |
syntax |
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
43 |
"@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" |
1474 | 44 |
[0,0,60] 60) |
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
45 |
|
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
46 |
"@letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)" |
1474 | 47 |
[0,0,0,60] 60) |
0 | 48 |
|
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
49 |
"@letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" |
1474 | 50 |
[0,0,0,0,60] 60) |
0 | 51 |
|
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
52 |
"@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" |
1474 | 53 |
[0,0,0,0,0,60] 60) |
998
91d09e262799
Gave tighter priorities to if, napply and the let-forms to
lcp
parents:
610
diff
changeset
|
54 |
|
17456 | 55 |
ML {* |
0 | 56 |
(** Quantifier translations: variable binding **) |
57 |
||
17781 | 58 |
(* FIXME does not handle "_idtdummy" *) |
2709 | 59 |
(* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *) |
60 |
||
0 | 61 |
fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b); |
62 |
fun let_tr' [a,Abs(id,T,b)] = |
|
63 |
let val (id',b') = variant_abs(id,T,b) |
|
64 |
in Const("@let",dummyT) $ Free(id',T) $ a $ b' end; |
|
65 |
||
17456 | 66 |
fun letrec_tr [Free(f,S),Free(x,T),a,b] = |
0 | 67 |
Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b); |
17456 | 68 |
fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] = |
0 | 69 |
Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b); |
17456 | 70 |
fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] = |
0 | 71 |
Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b); |
72 |
||
73 |
fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] = |
|
74 |
let val (f',b') = variant_abs(ff,SS,b) |
|
75 |
val (_,a'') = variant_abs(f,S,a) |
|
76 |
val (x',a') = variant_abs(x,T,a'') |
|
77 |
in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end; |
|
78 |
fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] = |
|
79 |
let val (f',b') = variant_abs(ff,SS,b) |
|
80 |
val ( _,a1) = variant_abs(f,S,a) |
|
81 |
val (y',a2) = variant_abs(y,U,a1) |
|
82 |
val (x',a') = variant_abs(x,T,a2) |
|
83 |
in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b' |
|
84 |
end; |
|
85 |
fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] = |
|
86 |
let val (f',b') = variant_abs(ff,SS,b) |
|
87 |
val ( _,a1) = variant_abs(f,S,a) |
|
88 |
val (z',a2) = variant_abs(z,V,a1) |
|
89 |
val (y',a3) = variant_abs(y,U,a2) |
|
90 |
val (x',a') = variant_abs(x,T,a3) |
|
91 |
in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b' |
|
92 |
end; |
|
93 |
||
17456 | 94 |
*} |
95 |
||
96 |
parse_translation {* |
|
97 |
[("@let", let_tr), |
|
98 |
("@letrec", letrec_tr), |
|
99 |
("@letrec2", letrec2_tr), |
|
100 |
("@letrec3", letrec3_tr)] *} |
|
101 |
||
102 |
print_translation {* |
|
103 |
[("let", let_tr'), |
|
104 |
("letrec", letrec_tr'), |
|
105 |
("letrec2", letrec2_tr'), |
|
106 |
("letrec3", letrec3_tr')] *} |
|
107 |
||
108 |
consts |
|
109 |
napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) |
|
110 |
||
111 |
axioms |
|
112 |
||
113 |
one_def: "one == true" |
|
114 |
if_def: "if b then t else u == case(b,t,u,% x y. bot,%v. bot)" |
|
115 |
inl_def: "inl(a) == <true,a>" |
|
116 |
inr_def: "inr(b) == <false,b>" |
|
117 |
when_def: "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))" |
|
118 |
split_def: "split(t,f) == case(t,bot,bot,f,%u. bot)" |
|
119 |
fst_def: "fst(t) == split(t,%x y. x)" |
|
120 |
snd_def: "snd(t) == split(t,%x y. y)" |
|
121 |
thd_def: "thd(t) == split(t,%x p. split(p,%y z. z))" |
|
122 |
zero_def: "zero == inl(one)" |
|
123 |
succ_def: "succ(n) == inr(n)" |
|
124 |
ncase_def: "ncase(n,b,c) == when(n,%x. b,%y. c(y))" |
|
125 |
nrec_def: " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)" |
|
126 |
nil_def: "[] == inl(one)" |
|
127 |
cons_def: "h$t == inr(<h,t>)" |
|
128 |
lcase_def: "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))" |
|
129 |
lrec_def: "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)" |
|
130 |
||
131 |
let_def: "let x be t in f(x) == case(t,f(true),f(false),%x y. f(<x,y>),%u. f(lam x. u(x)))" |
|
132 |
letrec_def: |
|
133 |
"letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)" |
|
134 |
||
135 |
letrec2_def: "letrec g x y be h(x,y,g) in f(g)== |
|
136 |
letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>))) |
|
137 |
in f(%x y. g'(<x,y>))" |
|
138 |
||
139 |
letrec3_def: "letrec g x y z be h(x,y,z,g) in f(g) == |
|
140 |
letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>)))) |
|
141 |
in f(%x y z. g'(<x,<y,z>>))" |
|
142 |
||
143 |
napply_def: "f ^n` a == nrec(n,a,%x g. f(g))" |
|
144 |
||
20140 | 145 |
|
146 |
lemmas simp_can_defs = one_def inl_def inr_def |
|
147 |
and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def |
|
148 |
lemmas simp_defs = simp_can_defs simp_ncan_defs |
|
149 |
||
150 |
lemmas ind_can_defs = zero_def succ_def nil_def cons_def |
|
151 |
and ind_ncan_defs = ncase_def nrec_def lcase_def lrec_def |
|
152 |
lemmas ind_defs = ind_can_defs ind_ncan_defs |
|
153 |
||
154 |
lemmas data_defs = simp_defs ind_defs napply_def |
|
155 |
and genrec_defs = letrec_def letrec2_def letrec3_def |
|
156 |
||
157 |
||
158 |
subsection {* Beta Rules, including strictness *} |
|
159 |
||
160 |
lemma letB: "~ t=bot ==> let x be t in f(x) = f(t)" |
|
161 |
apply (unfold let_def) |
|
162 |
apply (erule rev_mp) |
|
163 |
apply (rule_tac t = "t" in term_case) |
|
164 |
apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam) |
|
165 |
done |
|
166 |
||
167 |
lemma letBabot: "let x be bot in f(x) = bot" |
|
168 |
apply (unfold let_def) |
|
169 |
apply (rule caseBbot) |
|
170 |
done |
|
171 |
||
172 |
lemma letBbbot: "let x be t in bot = bot" |
|
173 |
apply (unfold let_def) |
|
174 |
apply (rule_tac t = t in term_case) |
|
175 |
apply (rule caseBbot) |
|
176 |
apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam) |
|
177 |
done |
|
178 |
||
179 |
lemma applyB: "(lam x. b(x)) ` a = b(a)" |
|
180 |
apply (unfold apply_def) |
|
181 |
apply (simp add: caseBtrue caseBfalse caseBpair caseBlam) |
|
182 |
done |
|
183 |
||
184 |
lemma applyBbot: "bot ` a = bot" |
|
185 |
apply (unfold apply_def) |
|
186 |
apply (rule caseBbot) |
|
187 |
done |
|
188 |
||
189 |
lemma fixB: "fix(f) = f(fix(f))" |
|
190 |
apply (unfold fix_def) |
|
191 |
apply (rule applyB [THEN ssubst], rule refl) |
|
192 |
done |
|
193 |
||
194 |
lemma letrecB: |
|
195 |
"letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))" |
|
196 |
apply (unfold letrec_def) |
|
197 |
apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl) |
|
198 |
done |
|
199 |
||
200 |
lemmas rawBs = caseBs applyB applyBbot |
|
201 |
||
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
202 |
method_setup beta_rl = {* |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
203 |
Scan.succeed (fn ctxt => |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
204 |
SIMPLE_METHOD' (CHANGED o |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
205 |
simp_tac (simpset_of ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB})))) |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
206 |
*} "" |
20140 | 207 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
208 |
lemma ifBtrue: "if true then t else u = t" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
209 |
and ifBfalse: "if false then t else u = u" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
210 |
and ifBbot: "if bot then t else u = bot" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
211 |
unfolding data_defs by beta_rl+ |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
212 |
|
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
213 |
lemma whenBinl: "when(inl(a),t,u) = t(a)" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
214 |
and whenBinr: "when(inr(a),t,u) = u(a)" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
215 |
and whenBbot: "when(bot,t,u) = bot" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
216 |
unfolding data_defs by beta_rl+ |
20140 | 217 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
218 |
lemma splitB: "split(<a,b>,h) = h(a,b)" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
219 |
and splitBbot: "split(bot,h) = bot" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
220 |
unfolding data_defs by beta_rl+ |
17456 | 221 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
222 |
lemma fstB: "fst(<a,b>) = a" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
223 |
and fstBbot: "fst(bot) = bot" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
224 |
unfolding data_defs by beta_rl+ |
20140 | 225 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
226 |
lemma sndB: "snd(<a,b>) = b" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
227 |
and sndBbot: "snd(bot) = bot" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
228 |
unfolding data_defs by beta_rl+ |
20140 | 229 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
230 |
lemma thdB: "thd(<a,<b,c>>) = c" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
231 |
and thdBbot: "thd(bot) = bot" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
232 |
unfolding data_defs by beta_rl+ |
20140 | 233 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
234 |
lemma ncaseBzero: "ncase(zero,t,u) = t" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
235 |
and ncaseBsucc: "ncase(succ(n),t,u) = u(n)" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
236 |
and ncaseBbot: "ncase(bot,t,u) = bot" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
237 |
unfolding data_defs by beta_rl+ |
20140 | 238 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
239 |
lemma nrecBzero: "nrec(zero,t,u) = t" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
240 |
and nrecBsucc: "nrec(succ(n),t,u) = u(n,nrec(n,t,u))" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
241 |
and nrecBbot: "nrec(bot,t,u) = bot" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
242 |
unfolding data_defs by beta_rl+ |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
243 |
|
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
244 |
lemma lcaseBnil: "lcase([],t,u) = t" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
245 |
and lcaseBcons: "lcase(x$xs,t,u) = u(x,xs)" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
246 |
and lcaseBbot: "lcase(bot,t,u) = bot" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
247 |
unfolding data_defs by beta_rl+ |
20140 | 248 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
249 |
lemma lrecBnil: "lrec([],t,u) = t" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
250 |
and lrecBcons: "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
251 |
and lrecBbot: "lrec(bot,t,u) = bot" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
252 |
unfolding data_defs by beta_rl+ |
20140 | 253 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
254 |
lemma letrec2B: |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
255 |
"letrec g x y be h(x,y,g) in g(p,q) = h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
256 |
unfolding data_defs letrec2_def by beta_rl+ |
20140 | 257 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
258 |
lemma letrec3B: |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
259 |
"letrec g x y z be h(x,y,z,g) in g(p,q,r) = |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
260 |
h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
261 |
unfolding data_defs letrec3_def by beta_rl+ |
20140 | 262 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
263 |
lemma napplyBzero: "f^zero`a = a" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
264 |
and napplyBsucc: "f^succ(n)`a = f(f^n`a)" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
265 |
unfolding data_defs by beta_rl+ |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
266 |
|
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
267 |
lemmas termBs = letB applyB applyBbot splitB splitBbot fstB fstBbot |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
268 |
sndB sndBbot thdB thdBbot ifBtrue ifBfalse ifBbot whenBinl whenBinr |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
269 |
whenBbot ncaseBzero ncaseBsucc ncaseBbot nrecBzero nrecBsucc |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
270 |
nrecBbot lcaseBnil lcaseBcons lcaseBbot lrecBnil lrecBcons lrecBbot |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32010
diff
changeset
|
271 |
napplyBzero napplyBsucc |
20140 | 272 |
|
273 |
||
274 |
subsection {* Constructors are injective *} |
|
275 |
||
32154 | 276 |
lemma term_injs: |
277 |
"(inl(a) = inl(a')) <-> (a=a')" |
|
278 |
"(inr(a) = inr(a')) <-> (a=a')" |
|
279 |
"(succ(a) = succ(a')) <-> (a=a')" |
|
280 |
"(a$b = a'$b') <-> (a=a' & b=b')" |
|
281 |
by (inj_rl applyB splitB whenBinl whenBinr ncaseBsucc lcaseBcons) |
|
20140 | 282 |
|
283 |
||
284 |
subsection {* Constructors are distinct *} |
|
285 |
||
26480 | 286 |
ML {* |
20140 | 287 |
bind_thms ("term_dstncts", |
32010 | 288 |
mkall_dstnct_thms @{theory} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs}) |
24825 | 289 |
[["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]); |
20140 | 290 |
*} |
291 |
||
292 |
||
293 |
subsection {* Rules for pre-order @{text "[="} *} |
|
294 |
||
32154 | 295 |
lemma term_porews: |
296 |
"inl(a) [= inl(a') <-> a [= a'" |
|
297 |
"inr(b) [= inr(b') <-> b [= b'" |
|
298 |
"succ(n) [= succ(n') <-> n [= n'" |
|
299 |
"x$xs [= x'$xs' <-> x [= x' & xs [= xs'" |
|
300 |
by (simp_all add: data_defs ccl_porews) |
|
20140 | 301 |
|
302 |
||
303 |
subsection {* Rewriting and Proving *} |
|
304 |
||
26480 | 305 |
ML {* |
24790 | 306 |
bind_thms ("term_injDs", XH_to_Ds @{thms term_injs}); |
20140 | 307 |
*} |
308 |
||
20917 | 309 |
lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews |
310 |
||
20140 | 311 |
lemmas [simp] = term_rews |
20917 | 312 |
lemmas [elim!] = term_dstncts [THEN notE] |
313 |
lemmas [dest!] = term_injDs |
|
20140 | 314 |
|
315 |
end |