191 in |
191 in |
192 ((bn, fvbn), (fvbn_name, eqs)) |
192 ((bn, fvbn), (fvbn_name, eqs)) |
193 end |
193 end |
194 *} |
194 *} |
195 |
195 |
|
196 ML {* |
|
197 fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) = |
|
198 let |
|
199 val {descr, sorts, ...} = dt_info; |
|
200 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
|
201 val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
|
202 val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} |
|
203 val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type); |
|
204 fun alpha_bn_constr (cname, dts) args_in_bn = |
|
205 let |
|
206 val Ts = map (typ_of_dtyp descr sorts) dts; |
|
207 val pi = Free("pi", @{typ perm}) |
|
208 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
|
209 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
|
210 val args = map Free (names ~~ Ts); |
|
211 val args2 = map Free (names2 ~~ Ts); |
|
212 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
|
213 val rhs = HOLogic.mk_Trueprop |
|
214 (alpha_bn_free $ pi $ (list_comb (c, args)) $ (list_comb (c, args2))); |
|
215 fun lhs_arg ((dt, arg_no), (arg, arg2)) = |
|
216 let |
|
217 val argty = fastype_of arg; |
|
218 val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty); |
|
219 val permarg = if is_rec then permute $ pi $ arg else arg |
|
220 in |
|
221 if is_rec_type dt then |
|
222 if arg_no mem args_in_bn then alpha_bn_free $ pi $ arg $ arg2 |
|
223 else (nth alpha_frees (body_index dt)) $ permarg $ arg2 |
|
224 else |
|
225 if arg_no mem args_in_bn then @{term True} |
|
226 else HOLogic.mk_eq (permarg, arg2) |
|
227 end |
|
228 val arg_nos = 0 upto (length dts - 1) |
|
229 val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2))) |
|
230 val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs) |
|
231 in |
|
232 eq |
|
233 end |
|
234 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
|
235 val eqs = map2i alpha_bn_constr constrs args_in_bns |
|
236 in |
|
237 ((bn, alpha_bn_free), (alpha_bn_name, eqs)) |
|
238 end |
|
239 *} |
|
240 |
196 ML {* fn x => split_list(flat x) *} |
241 ML {* fn x => split_list(flat x) *} |
197 ML {* fn x => apsnd flat (split_list (map split_list x)) *} |
242 ML {* fn x => apsnd flat (split_list (map split_list x)) *} |
198 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
243 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
199 ML {* |
244 ML {* |
200 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = |
245 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = |
207 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
252 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
208 val fv_frees = map Free (fv_names ~~ fv_types); |
253 val fv_frees = map Free (fv_names ~~ fv_types); |
209 val nr_bns = non_rec_binds bindsall; |
254 val nr_bns = non_rec_binds bindsall; |
210 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
255 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
211 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
256 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
212 val fv_bns = map snd bn_fv_bns; |
|
213 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
257 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
214 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
258 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
215 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
259 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
216 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
260 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
217 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
261 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
|
262 (* We assume that a bn is either recursive or not *) |
|
263 val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; |
|
264 val (bn_alpha_bns, alpha_bn_names_eqs) = split_list (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec)) |
|
265 val (alpha_bn_names, alpha_bn_eqs) = split_list alpha_bn_names_eqs; |
|
266 val alpha_bn_frees = map snd bn_alpha_bns; |
|
267 val alpha_bn_types = map fastype_of alpha_bn_frees; |
218 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
268 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
219 let |
269 let |
220 val Ts = map (typ_of_dtyp descr sorts) dts; |
270 val Ts = map (typ_of_dtyp descr sorts) dts; |
221 val bindslen = length bindcs |
271 val bindslen = length bindcs |
222 val pi_strs_same = replicate bindslen "pi" |
272 val pi_strs_same = replicate bindslen "pi" |
267 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
317 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
268 val alpha_rhs = |
318 val alpha_rhs = |
269 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
319 HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))); |
270 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
320 fun alpha_arg ((dt, arg_no), (arg, arg2)) = |
271 let |
321 let |
272 val relevant = filter (fn ((_, i, j), _) => i = arg_no orelse j = arg_no) bind_pis; |
322 val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis; |
|
323 val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis; |
|
324 val rel_has_binds = filter (fn ((SOME _, _, j), _) => j = arg_no | _ => false) bind_pis; |
273 in |
325 in |
274 if relevant = [] then ( |
326 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of |
275 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
327 ([], [], []) => |
276 else (HOLogic.mk_eq (arg, arg2))) |
328 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
277 else |
329 else (HOLogic.mk_eq (arg, arg2)) |
278 if is_rec_type dt then let |
330 (* TODO: if more then check and accept *) |
279 (* THE HARD CASE *) |
331 | (_, [], []) => @{term True} |
|
332 | ([], [(((SOME (bn, _)), _, _), pi)], []) => |
|
333 let |
|
334 val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
|
335 val ty = fastype_of (bn $ arg) |
|
336 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
|
337 in |
|
338 HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2))) |
|
339 end |
|
340 | ([], [], relevant) => |
|
341 let |
280 val (rbinds, rpis) = split_list relevant |
342 val (rbinds, rpis) = split_list relevant |
281 val lhs_binds = fv_binds args rbinds |
343 val lhs_binds = fv_binds args rbinds |
282 val lhs = mk_pair (lhs_binds, arg); |
344 val lhs = mk_pair (lhs_binds, arg); |
283 val rhs_binds = fv_binds args2 rbinds; |
345 val rhs_binds = fv_binds args2 rbinds; |
284 val rhs = mk_pair (rhs_binds, arg2); |
346 val rhs = mk_pair (rhs_binds, arg2); |
288 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
350 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
289 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
351 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
290 (* val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
352 (* val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
291 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) |
353 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) |
292 in |
354 in |
293 (*if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) |
355 (* if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) |
294 alpha_gen |
356 alpha_gen |
295 (* TODO Add some test that is makes sense *) |
357 end |
296 end else @{term "True"} |
358 | _ => error "Fv.alpha: not supported binding structure" |
297 end |
359 end |
298 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
360 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
299 val alpha_lhss = mk_conjl alphas |
361 val alpha_lhss = mk_conjl alphas |
300 val alpha_lhss_ex = |
362 val alpha_lhss_ex = |
301 fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss |
363 fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss |
305 end; |
367 end; |
306 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
368 fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; |
307 val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall) |
369 val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall) |
308 val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs)) |
370 val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs)) |
309 val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; |
371 val rel_bns_nos = map (fn (_, i, _) => i) rel_bns; |
310 fun filter_fun (a, b) = b mem rel_bns_nos; |
372 fun filter_fun (_, b) = b mem rel_bns_nos; |
311 val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1)) |
373 val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1)) |
312 val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs))) |
374 val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs))) |
313 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
375 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
314 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
376 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
315 val fv_names_all = fv_names_fst @ fv_bn_names; |
377 val fv_names_all = fv_names_fst @ fv_bn_names; |
323 (Primrec.add_primrec |
385 (Primrec.add_primrec |
324 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy') |
386 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy') |
325 val (alphas, lthy''') = (Inductive.add_inductive_i |
387 val (alphas, lthy''') = (Inductive.add_inductive_i |
326 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
388 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
327 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
389 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
328 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
390 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names) |
329 (add_binds alpha_eqs) [] lthy'') |
391 (alpha_types @ alpha_bn_types)) [] |
330 in |
392 (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'') |
331 ((fvs, alphas), lthy''') |
393 val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) |
|
394 in |
|
395 ((all_fvs, alphas), lthy''') |
332 end |
396 end |
333 *} |
397 *} |
334 |
398 |
335 (* |
399 (* |
336 atom_decl name |
400 atom_decl name |
337 |
|
338 datatype lam = |
401 datatype lam = |
339 VAR "name" |
402 VAR "name" |
340 | APP "lam" "lam" |
403 | APP "lam" "lam" |
341 | LET "bp" "lam" |
404 | LET "bp" "lam" |
342 and bp = |
405 and bp = |
343 BP "name" "lam" |
406 BP "name" "lam" |
344 |
|
345 primrec |
407 primrec |
346 bi::"bp \<Rightarrow> atom set" |
408 bi::"bp \<Rightarrow> atom set" |
347 where |
409 where |
348 "bi (BP x t) = {atom x}" |
410 "bi (BP x t) = {atom x}" |
349 |
|
350 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *} |
411 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *} |
351 |
|
352 |
|
353 local_setup {* |
412 local_setup {* |
354 snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam") |
413 snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam") |
355 [[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *} |
414 [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *} |
356 print_theorems |
415 print_theorems |
357 *) |
416 *) |
358 |
417 |
359 (* |
418 (*atom_decl name |
360 datatype rtrm1 = |
419 datatype rtrm1 = |
361 rVr1 "name" |
420 rVr1 "name" |
362 | rAp1 "rtrm1" "rtrm1" |
421 | rAp1 "rtrm1" "rtrm1" |
363 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
422 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
364 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
423 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
365 and bp = |
424 and bp = |
366 BUnit |
425 BUnit |
367 | BVr "name" |
426 | BVr "name" |
368 | BPr "bp" "bp" |
427 | BPr "bp" "bp" |
369 |
|
370 (* to be given by the user *) |
|
371 |
|
372 primrec |
428 primrec |
373 bv1 |
429 bv1 |
374 where |
430 where |
375 "bv1 (BUnit) = {}" |
431 "bv1 (BUnit) = {}" |
376 | "bv1 (BVr x) = {atom x}" |
432 | "bv1 (BVr x) = {atom x}" |
377 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
433 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
378 |
434 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm1") 2 *} |
379 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *} |
435 local_setup {* |
380 |
436 snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm1") |
381 local_setup {* define_fv_alpha "Fv.rtrm1" |
437 [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, false), 0, 2)]], |
382 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
438 [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *} |
383 [[], [[]], [[], []]]] *} |
|
384 print_theorems |
439 print_theorems |
385 *) |
440 *) |
386 |
441 |
|
442 (* |
|
443 atom_decl name |
|
444 datatype rtrm5 = |
|
445 rVr5 "name" |
|
446 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
|
447 and rlts = |
|
448 rLnil |
|
449 | rLcons "name" "rtrm5" "rlts" |
|
450 primrec |
|
451 rbv5 |
|
452 where |
|
453 "rbv5 rLnil = {}" |
|
454 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
|
455 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm5") 2 *} |
|
456 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm5") |
|
457 [[[], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} |
|
458 print_theorems |
|
459 *) |
387 |
460 |
388 ML {* |
461 ML {* |
389 fun alpha_inj_tac dist_inj intrs elims = |
462 fun alpha_inj_tac dist_inj intrs elims = |
390 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' |
463 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' |
391 (rtac @{thm iffI} THEN' RANGE [ |
464 (rtac @{thm iffI} THEN' RANGE [ |