16 |
16 |
17 (* binding modes and binding clauses *) |
17 (* binding modes and binding clauses *) |
18 datatype bmode = Lst | Res | Set |
18 datatype bmode = Lst | Res | Set |
19 datatype bclause = BC of bmode * (term option * int) list * int list |
19 datatype bclause = BC of bmode * (term option * int) list * int list |
20 |
20 |
21 val is_atom: Proof.context -> typ -> bool |
|
22 val is_atom_set: Proof.context -> typ -> bool |
|
23 val is_atom_fset: Proof.context -> typ -> bool |
|
24 val is_atom_list: Proof.context -> typ -> bool |
|
25 val mk_atom_set: term -> term |
|
26 val mk_atom_fset: term -> term |
|
27 |
|
28 val setify: Proof.context -> term -> term |
|
29 val listify: Proof.context -> term -> term |
|
30 |
|
31 val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> |
21 val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> |
32 (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> |
22 (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> |
33 (term list * thm list * bn_info list * thm list * local_theory) |
23 (term list * thm list * bn_info list * thm list * local_theory) |
34 |
|
35 |
24 |
36 val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> |
25 val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> |
37 thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory |
26 thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory |
38 |
27 |
39 val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list -> |
28 val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list -> |
67 |
56 |
68 datatype bmode = Lst | Res | Set |
57 datatype bmode = Lst | Res | Set |
69 datatype bclause = BC of bmode * (term option * int) list * int list |
58 datatype bclause = BC of bmode * (term option * int) list * int list |
70 |
59 |
71 fun lookup xs x = the (AList.lookup (op=) xs x) |
60 fun lookup xs x = the (AList.lookup (op=) xs x) |
72 |
|
73 |
|
74 (* testing for concrete atom types *) |
|
75 fun is_atom ctxt ty = |
|
76 Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) |
|
77 |
|
78 fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t |
|
79 | is_atom_set _ _ = false; |
|
80 |
|
81 fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t |
|
82 | is_atom_fset _ _ = false; |
|
83 |
|
84 fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t |
|
85 | is_atom_list _ _ = false |
|
86 |
|
87 |
|
88 (* functions for producing sets, fsets and lists of general atom type |
|
89 out from concrete atom types *) |
|
90 fun mk_atom_set t = |
|
91 let |
|
92 val ty = fastype_of t; |
|
93 val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; |
|
94 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
|
95 in |
|
96 Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t |
|
97 end |
|
98 |
|
99 |
|
100 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
|
101 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
|
102 |
|
103 fun mk_atom_fset t = |
|
104 let |
|
105 val ty = fastype_of t; |
|
106 val atom_ty = dest_fsetT ty |
|
107 val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; |
|
108 val fset = @{term "fset :: atom fset => atom set"} |
|
109 in |
|
110 fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t) |
|
111 end |
|
112 |
|
113 fun mk_atom_list t = |
|
114 let |
|
115 val ty = fastype_of t |
|
116 val atom_ty = dest_listT ty |
|
117 val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"} |
|
118 in |
|
119 Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t |
|
120 end |
|
121 |
|
122 (* functions that coerces singletons, sets and fsets of concrete atoms |
|
123 into sets of general atoms *) |
|
124 fun setify ctxt t = |
|
125 let |
|
126 val ty = fastype_of t; |
|
127 in |
|
128 if is_atom ctxt ty |
|
129 then HOLogic.mk_set @{typ atom} [mk_atom t] |
|
130 else if is_atom_set ctxt ty |
|
131 then mk_atom_set t |
|
132 else if is_atom_fset ctxt ty |
|
133 then mk_atom_fset t |
|
134 else raise TERM ("setify", [t]) |
|
135 end |
|
136 |
|
137 (* functions that coerces singletons and lists of concrete atoms |
|
138 into lists of general atoms *) |
|
139 fun listify ctxt t = |
|
140 let |
|
141 val ty = fastype_of t; |
|
142 in |
|
143 if is_atom ctxt ty |
|
144 then HOLogic.mk_list @{typ atom} [mk_atom t] |
|
145 else if is_atom_list ctxt ty |
|
146 then mk_atom_list t |
|
147 else raise TERM ("listify", [t]) |
|
148 end |
|
149 |
61 |
150 |
62 |
151 (** functions that define the raw binding functions **) |
63 (** functions that define the raw binding functions **) |
152 |
64 |
153 (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or |
65 (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or |