272 |
271 |
273 subsection {* Constructors are injective *} |
272 subsection {* Constructors are injective *} |
274 |
273 |
275 ML {* |
274 ML {* |
276 |
275 |
277 bind_thms ("term_injs", map (mk_inj_rl (the_context ()) |
276 bind_thms ("term_injs", map (mk_inj_rl @{theory} |
278 [thm "applyB", thm "splitB", thm "whenBinl", thm "whenBinr", thm "ncaseBsucc", thm "lcaseBcons"]) |
277 [@{thm applyB}, @{thm splitB}, @{thm whenBinl}, @{thm whenBinr}, |
|
278 @{thm ncaseBsucc}, @{thm lcaseBcons}]) |
279 ["(inl(a) = inl(a')) <-> (a=a')", |
279 ["(inl(a) = inl(a')) <-> (a=a')", |
280 "(inr(a) = inr(a')) <-> (a=a')", |
280 "(inr(a) = inr(a')) <-> (a=a')", |
281 "(succ(a) = succ(a')) <-> (a=a')", |
281 "(succ(a) = succ(a')) <-> (a=a')", |
282 "(a$b = a'$b') <-> (a=a' & b=b')"]) |
282 "(a$b = a'$b') <-> (a=a' & b=b')"]) |
283 *} |
283 *} |
285 |
285 |
286 subsection {* Constructors are distinct *} |
286 subsection {* Constructors are distinct *} |
287 |
287 |
288 ML {* |
288 ML {* |
289 bind_thms ("term_dstncts", |
289 bind_thms ("term_dstncts", |
290 mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs") |
290 mkall_dstnct_thms @{theory} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs}) |
291 [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]); |
291 [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]); |
292 *} |
292 *} |
293 |
293 |
294 |
294 |
295 subsection {* Rules for pre-order @{text "[="} *} |
295 subsection {* Rules for pre-order @{text "[="} *} |
296 |
296 |
297 ML {* |
297 ML {* |
298 |
298 |
299 local |
299 local |
300 fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ => |
300 fun mk_thm s = prove_goalw @{theory} @{thms data_defs} s (fn _ => |
301 [simp_tac (@{simpset} addsimps (thms "ccl_porews")) 1]) |
301 [simp_tac (@{simpset} addsimps @{thms ccl_porews}) 1]) |
302 in |
302 in |
303 val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'", |
303 val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'", |
304 "inr(b) [= inr(b') <-> b [= b'", |
304 "inr(b) [= inr(b') <-> b [= b'", |
305 "succ(n) [= succ(n') <-> n [= n'", |
305 "succ(n) [= succ(n') <-> n [= n'", |
306 "x$xs [= x'$xs' <-> x [= x' & xs [= xs'"] |
306 "x$xs [= x'$xs' <-> x [= x' & xs [= xs'"] |