equal
deleted
inserted
replaced
14 |
14 |
15 datatype bclause = BC of bmode * (term option * int) list * int list |
15 datatype bclause = BC of bmode * (term option * int) list * int list |
16 |
16 |
17 val setify: Proof.context -> term -> term |
17 val setify: Proof.context -> term -> term |
18 val listify: Proof.context -> term -> term |
18 val listify: Proof.context -> term -> term |
19 val fold_union: term list -> term |
|
20 |
19 |
21 val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> |
20 val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> |
22 (term * 'a * 'b) list -> (term * int * (int * term option) list list) list -> |
21 (term * 'a * 'b) list -> (term * int * (int * term option) list list) list -> |
23 bclause list list list -> Proof.context -> term list * term list * thm list * local_theory |
22 bclause list list list -> Proof.context -> term list * term list * thm list * local_theory |
24 end |
23 end |
27 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
26 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
28 struct |
27 struct |
29 |
28 |
30 datatype bmode = Lst | Res | Set |
29 datatype bmode = Lst | Res | Set |
31 datatype bclause = BC of bmode * (term option * int) list * int list |
30 datatype bclause = BC of bmode * (term option * int) list * int list |
32 |
|
33 (* functions that construct differences and unions |
|
34 but avoid producing empty atom sets *) |
|
35 |
|
36 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} |
|
37 | mk_diff (t1, @{term "{}::atom set"}) = t1 |
|
38 | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) |
|
39 |
|
40 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"} |
|
41 | mk_union (t1 , @{term "{}::atom set"}) = t1 |
|
42 | mk_union (@{term "{}::atom set"}, t2) = t2 |
|
43 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2) |
|
44 |
|
45 fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"} |
|
46 |
|
47 |
31 |
48 (* atom types *) |
32 (* atom types *) |
49 fun is_atom ctxt ty = |
33 fun is_atom ctxt ty = |
50 Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) |
34 Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) |
51 |
35 |