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