9 sig |
9 sig |
10 (* info of raw datatypes *) |
10 (* info of raw datatypes *) |
11 type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list |
11 type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list |
12 |
12 |
13 (* info of raw binding functions *) |
13 (* info of raw binding functions *) |
14 type bn_info = (term * int * (int * term option) list list) list |
14 type bn_info = term * int * (int * term option) list list |
15 |
15 |
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 |
26 val mk_atom_fset: term -> term |
26 val mk_atom_fset: term -> term |
27 |
27 |
28 val setify: Proof.context -> term -> term |
28 val setify: Proof.context -> term -> term |
29 val listify: Proof.context -> term -> term |
29 val listify: Proof.context -> term -> term |
30 |
30 |
31 (* TODO: should be here |
31 (* FIXME: should be here - currently in Nominal2.thy |
32 val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list -> |
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 -> |
33 (Attrib.binding * term) list -> thm list -> thm list -> local_theory -> |
34 (term list * thm list * bn_info * thm list * local_theory) *) |
34 (term list * thm list * bn_info list * thm list * local_theory) |
35 |
35 *) |
36 val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> |
36 |
|
37 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 |
38 thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory |
|
39 |
|
40 val define_raw_bn_perms: typ list -> bn_info list -> cns_info list -> thm list -> thm list -> |
|
41 local_theory -> (term list * thm list * local_theory) |
38 |
42 |
39 val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list |
43 val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list |
40 end |
44 end |
41 |
45 |
42 |
46 |
54 (* term - is constant of the bn-function |
58 (* term - is constant of the bn-function |
55 int - is datatype number over which the bn-function is defined |
59 int - is datatype number over which the bn-function is defined |
56 int * term option - is number of the corresponding argument with possibly |
60 int * term option - is number of the corresponding argument with possibly |
57 recursive call with bn-function term |
61 recursive call with bn-function term |
58 *) |
62 *) |
59 type bn_info = (term * int * (int * term option) list list) list |
63 type bn_info = term * int * (int * term option) list list |
60 |
64 |
61 |
65 |
62 datatype bmode = Lst | Res | Set |
66 datatype bmode = Lst | Res | Set |
63 datatype bclause = BC of bmode * (term option * int) list * int list |
67 datatype bclause = BC of bmode * (term option * int) list * int list |
64 |
68 |
144 (* coerces a list into a set *) |
148 (* coerces a list into a set *) |
145 fun to_set t = |
149 fun to_set t = |
146 if fastype_of t = @{typ "atom list"} |
150 if fastype_of t = @{typ "atom list"} |
147 then @{term "set::atom list => atom set"} $ t |
151 then @{term "set::atom list => atom set"} $ t |
148 else t |
152 else t |
149 |
|
150 |
153 |
151 |
154 |
152 (** functions that construct the equations for fv and fv_bn **) |
155 (** functions that construct the equations for fv and fv_bn **) |
153 |
156 |
154 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = |
157 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = |
282 in |
285 in |
283 (fvs', fv_bns', simps_exp, inducts_exp, lthy'') |
286 (fvs', fv_bns', simps_exp, inducts_exp, lthy'') |
284 end |
287 end |
285 |
288 |
286 |
289 |
|
290 (** definition of raw permute_bn functions **) |
|
291 |
|
292 fun mk_perm_bn_eq_rhs p perm_bn_map bn_args (i, arg) = |
|
293 case AList.lookup (op=) bn_args i of |
|
294 NONE => arg |
|
295 | SOME (NONE) => mk_perm p arg |
|
296 | SOME (SOME bn) => (lookup perm_bn_map bn) $ p $ arg |
|
297 |
|
298 |
|
299 fun mk_perm_bn_eq lthy bn_trm perm_bn_map bn_args (constr, _, arg_tys, _) = |
|
300 let |
|
301 val p = Free ("p", @{typ perm}) |
|
302 val arg_names = Datatype_Prop.make_tnames arg_tys |
|
303 val args = map Free (arg_names ~~ arg_tys) |
|
304 val perm_bn = lookup perm_bn_map bn_trm |
|
305 val lhs = perm_bn $ p $ list_comb (constr, args) |
|
306 val rhs = list_comb (constr, map_index (mk_perm_bn_eq_rhs p perm_bn_map bn_args) args) |
|
307 in |
|
308 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
309 end |
|
310 |
|
311 fun mk_perm_bn_eqs lthy perm_bn_map cns_info (bn_trm, bn_n, bn_argss) = |
|
312 let |
|
313 val nth_cns_info = nth cns_info bn_n |
|
314 in |
|
315 map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info |
|
316 end |
|
317 |
|
318 fun define_raw_bn_perms raw_tys bn_info cns_info cns_thms size_thms lthy = |
|
319 if null bn_info |
|
320 then ([], [], lthy) |
|
321 else |
|
322 let |
|
323 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) |
|
324 val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns |
|
325 val perm_bn_names = map (prefix "permute_") bn_names |
|
326 val perm_bn_arg_tys = map (nth raw_tys) bn_tys |
|
327 val perm_bn_tys = map (fn ty => @{typ "perm"} --> ty --> ty) perm_bn_arg_tys |
|
328 val perm_bn_frees = map Free (perm_bn_names ~~ perm_bn_tys) |
|
329 val perm_bn_map = bns ~~ perm_bn_frees |
|
330 |
|
331 val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map cns_info) bn_info |
|
332 |
|
333 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names |
|
334 val all_fun_eqs = map (pair Attrib.empty_binding) (flat perm_bn_eqs) |
|
335 |
|
336 val prod_simps = @{thms prod.inject HOL.simp_thms} |
|
337 |
|
338 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
|
339 Function_Common.default_config (pat_completeness_simp (prod_simps @ cns_thms)) lthy |
|
340 |
|
341 val (info, lthy'') = prove_termination size_thms (Local_Theory.restore lthy') |
|
342 |
|
343 val {fs, simps, ...} = info; |
|
344 |
|
345 val morphism = ProofContext.export_morphism lthy'' lthy |
|
346 val simps_exp = map (Morphism.thm morphism) (the simps) |
|
347 in |
|
348 (fs, simps_exp, lthy'') |
|
349 end |
|
350 |
|
351 |
287 (** equivarance proofs **) |
352 (** equivarance proofs **) |
288 |
353 |
289 val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} |
354 val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} |
290 |
355 |
291 fun subproof_tac const_names simps = |
356 fun subproof_tac const_names simps = |