5 Definitions of the raw fv and fv_bn functions |
5 Definitions of the raw fv and fv_bn functions |
6 *) |
6 *) |
7 |
7 |
8 signature NOMINAL_DT_RAWFUNS = |
8 signature NOMINAL_DT_RAWFUNS = |
9 sig |
9 sig |
10 (* info of binding functions *) |
10 (* info of raw datatypes *) |
|
11 type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list |
|
12 |
|
13 (* info of raw binding functions *) |
11 type bn_info = (term * int * (int * term option) list list) list |
14 type bn_info = (term * int * (int * term option) list list) list |
12 |
15 |
|
16 |
13 (* binding modes and binding clauses *) |
17 (* binding modes and binding clauses *) |
14 datatype bmode = Lst | Res | Set |
18 datatype bmode = Lst | Res | Set |
15 datatype bclause = BC of bmode * (term option * int) list * int list |
19 datatype bclause = BC of bmode * (term option * int) list * int list |
16 |
20 |
17 val is_atom: Proof.context -> typ -> bool |
21 val is_atom: Proof.context -> typ -> bool |
22 val mk_atom_fset: term -> term |
26 val mk_atom_fset: term -> term |
23 |
27 |
24 val setify: Proof.context -> term -> term |
28 val setify: Proof.context -> term -> term |
25 val listify: Proof.context -> term -> term |
29 val listify: Proof.context -> term -> term |
26 |
30 |
|
31 (* TODO: should be here |
|
32 val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> |
|
33 (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> |
|
34 (term list * thm list * bn_info * thm list * local_theory) *) |
|
35 |
27 val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> |
36 val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> |
28 thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory |
37 thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory |
29 |
38 |
30 val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list |
39 val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list |
31 end |
40 end |
32 |
41 |
33 |
42 |
34 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
43 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
35 struct |
44 struct |
|
45 |
|
46 (* string list - type variables of a datatype |
|
47 binding - name of the datatype |
|
48 mixfix - its mixfix |
|
49 (binding * typ list * mixfix) list - datatype constructors of the type |
|
50 *) |
|
51 type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list |
|
52 |
36 |
53 |
37 (* term - is constant of the bn-function |
54 (* term - is constant of the bn-function |
38 int - is datatype number over which the bn-function is defined |
55 int - is datatype number over which the bn-function is defined |
39 int * term option - is number of the corresponding argument with possibly |
56 int * term option - is number of the corresponding argument with possibly |
40 recursive call with bn-function term |
57 recursive call with bn-function term |
41 *) |
58 *) |
42 type bn_info = (term * int * (int * term option) list list) list |
59 type bn_info = (term * int * (int * term option) list list) list |
|
60 |
43 |
61 |
44 datatype bmode = Lst | Res | Set |
62 datatype bmode = Lst | Res | Set |
45 datatype bclause = BC of bmode * (term option * int) list * int list |
63 datatype bclause = BC of bmode * (term option * int) list * int list |
46 |
64 |
47 (* testing for concrete atom types *) |
65 (* testing for concrete atom types *) |
123 (* coerces a list into a set *) |
141 (* coerces a list into a set *) |
124 fun to_set t = |
142 fun to_set t = |
125 if fastype_of t = @{typ "atom list"} |
143 if fastype_of t = @{typ "atom list"} |
126 then @{term "set::atom list => atom set"} $ t |
144 then @{term "set::atom list => atom set"} $ t |
127 else t |
145 else t |
|
146 |
128 |
147 |
129 |
148 |
130 (** functions that construct the equations for fv and fv_bn **) |
149 (** functions that construct the equations for fv and fv_bn **) |
131 |
150 |
132 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = |
151 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = |
237 val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy') |
256 val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy') |
238 |
257 |
239 val {fs, simps, inducts, ...} = info; |
258 val {fs, simps, inducts, ...} = info; |
240 |
259 |
241 val morphism = ProofContext.export_morphism lthy'' lthy |
260 val morphism = ProofContext.export_morphism lthy'' lthy |
242 val fs_exp = map (Morphism.term morphism) fs |
|
243 val simps_exp = map (Morphism.thm morphism) (the simps) |
261 val simps_exp = map (Morphism.thm morphism) (the simps) |
244 val inducts_exp = map (Morphism.thm morphism) (the inducts) |
262 val inducts_exp = map (Morphism.thm morphism) (the inducts) |
245 val (fvs_exp, fv_bns_exp) = chop (length fv_frees) fs_exp |
263 |
246 in |
264 val (fvs', fv_bns') = chop (length fv_frees) fs |
247 (fvs_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'') |
265 in |
|
266 (fvs', fv_bns', simps_exp, inducts_exp, lthy'') |
248 end |
267 end |
249 |
268 |
250 |
269 |
251 (** equivarance proofs **) |
270 (** equivarance proofs **) |
252 |
271 |