| author | lcp |
| Wed, 03 May 1995 13:55:05 +0200 | |
| changeset 1091 | f55f54a032ce |
| parent 71 | 729fe026c5f3 |
| permissions | -rw-r--r-- |
| 0 | 1 |
(* Title: ZF/ex/bin.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Datatype of binary integers |
|
7 |
*) |
|
8 |
||
9 |
(*Example of a datatype with an infix constructor*) |
|
10 |
structure Bin = Datatype_Fun |
|
11 |
(val thy = Univ.thy; |
|
12 |
val rec_specs = |
|
13 |
[("bin", "univ(0)",
|
|
14 |
[(["Plus", "Minus"], "i"), |
|
15 |
(["op $$"], "[i,i]=>i")])]; |
|
16 |
val rec_styp = "i"; |
|
|
16
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
17 |
val ext = Some (Syntax.simple_sext [Infixl("$$", "[i,i] => i", 60)]);
|
| 0 | 18 |
val sintrs = |
19 |
["Plus : bin", |
|
20 |
"Minus : bin", |
|
21 |
"[| w: bin; b: bool |] ==> w$$b : bin"]; |
|
22 |
val monos = []; |
|
|
71
729fe026c5f3
sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents:
56
diff
changeset
|
23 |
val type_intrs = datatype_intrs @ [bool_into_univ]; |
| 0 | 24 |
val type_elims = []); |
25 |
||
26 |
(*Perform induction on l, then prove the major premise using prems. *) |
|
27 |
fun bin_ind_tac a prems i = |
|
28 |
EVERY [res_inst_tac [("x",a)] Bin.induct i,
|
|
29 |
rename_last_tac a ["1"] (i+3), |
|
30 |
ares_tac prems i]; |
|
31 |