259 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
259 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
260 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; |
261 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 *) |
262 (* We assume that a bn is either recursive or not *) |
263 val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; |
263 val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns; |
264 |
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_bnfrees = map (fst o snd) (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 |
266 val alpha_bn_frees = map snd bn_alpha_bns; |
|
267 val alpha_bn_types = map fastype_of alpha_bn_frees; |
267 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
268 fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = |
268 let |
269 let |
269 val Ts = map (typ_of_dtyp descr sorts) dts; |
270 val Ts = map (typ_of_dtyp descr sorts) dts; |
270 val bindslen = length bindcs |
271 val bindslen = length bindcs |
271 val pi_strs_same = replicate bindslen "pi" |
272 val pi_strs_same = replicate bindslen "pi" |
327 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
328 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
328 else (HOLogic.mk_eq (arg, arg2)) |
329 else (HOLogic.mk_eq (arg, arg2)) |
329 (* TODO: if more then check and accept *) |
330 (* TODO: if more then check and accept *) |
330 | (_, [], []) => @{term True} |
331 | (_, [], []) => @{term True} |
331 | ([], [(((SOME (bn, _)), _, _), pi)], []) => |
332 | ([], [(((SOME (bn, _)), _, _), pi)], []) => |
332 nth alpha_bnfrees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
333 nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
333 | ([], [], relevant) => |
334 | ([], [], relevant) => |
334 let |
335 let |
335 val (rbinds, rpis) = split_list relevant |
336 val (rbinds, rpis) = split_list relevant |
336 val lhs_binds = fv_binds args rbinds |
337 val lhs_binds = fv_binds args rbinds |
337 val lhs = mk_pair (lhs_binds, arg); |
338 val lhs = mk_pair (lhs_binds, arg); |
378 (Primrec.add_primrec |
379 (Primrec.add_primrec |
379 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy') |
380 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy') |
380 val (alphas, lthy''') = (Inductive.add_inductive_i |
381 val (alphas, lthy''') = (Inductive.add_inductive_i |
381 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
382 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
382 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
383 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
383 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] |
384 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) (alpha_names @ alpha_bn_names) |
384 (add_binds alpha_eqs) [] lthy'') |
385 (alpha_types @ alpha_bn_types)) [] |
|
386 (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'') |
385 val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) |
387 val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2) |
386 in |
388 in |
387 ((all_fvs, alphas), lthy''') |
389 ((all_fvs, alphas), lthy''') |
388 end |
390 end |
389 *} |
391 *} |
390 |
392 |
391 (* |
393 (* |
392 atom_decl name |
394 atom_decl name |
393 |
|
394 datatype lam = |
395 datatype lam = |
395 VAR "name" |
396 VAR "name" |
396 | APP "lam" "lam" |
397 | APP "lam" "lam" |
397 | LET "bp" "lam" |
398 | LET "bp" "lam" |
398 and bp = |
399 and bp = |
399 BP "name" "lam" |
400 BP "name" "lam" |
400 |
|
401 primrec |
401 primrec |
402 bi::"bp \<Rightarrow> atom set" |
402 bi::"bp \<Rightarrow> atom set" |
403 where |
403 where |
404 "bi (BP x t) = {atom x}" |
404 "bi (BP x t) = {atom x}" |
405 |
|
406 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *} |
405 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *} |
407 |
|
408 |
|
409 local_setup {* |
406 local_setup {* |
410 snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam") |
407 snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam") |
411 [[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *} |
408 [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *} |
412 print_theorems |
409 print_theorems |
413 *) |
410 *) |
414 |
411 |
415 (* |
412 (*atom_decl name |
416 datatype rtrm1 = |
413 datatype rtrm1 = |
417 rVr1 "name" |
414 rVr1 "name" |
418 | rAp1 "rtrm1" "rtrm1" |
415 | rAp1 "rtrm1" "rtrm1" |
419 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
416 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
420 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
417 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
421 and bp = |
418 and bp = |
422 BUnit |
419 BUnit |
423 | BVr "name" |
420 | BVr "name" |
424 | BPr "bp" "bp" |
421 | BPr "bp" "bp" |
425 |
|
426 (* to be given by the user *) |
|
427 |
|
428 primrec |
422 primrec |
429 bv1 |
423 bv1 |
430 where |
424 where |
431 "bv1 (BUnit) = {}" |
425 "bv1 (BUnit) = {}" |
432 | "bv1 (BVr x) = {atom x}" |
426 | "bv1 (BVr x) = {atom x}" |
433 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
427 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
434 |
428 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm1") 2 *} |
435 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *} |
429 local_setup {* |
436 |
430 snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm1") |
437 local_setup {* define_fv_alpha "Fv.rtrm1" |
431 [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, false), 0, 2)]], |
438 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
432 [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *} |
439 [[], [[]], [[], []]]] *} |
|
440 print_theorems |
433 print_theorems |
441 *) |
434 *) |
442 |
435 |
|
436 (* |
|
437 atom_decl name |
|
438 datatype rtrm5 = |
|
439 rVr5 "name" |
|
440 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
|
441 and rlts = |
|
442 rLnil |
|
443 | rLcons "name" "rtrm5" "rlts" |
|
444 primrec |
|
445 rbv5 |
|
446 where |
|
447 "rbv5 rLnil = {}" |
|
448 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
|
449 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm5") 2 *} |
|
450 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm5") |
|
451 [[[], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *} |
|
452 print_theorems |
|
453 *) |
443 |
454 |
444 ML {* |
455 ML {* |
445 fun alpha_inj_tac dist_inj intrs elims = |
456 fun alpha_inj_tac dist_inj intrs elims = |
446 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' |
457 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' |
447 (rtac @{thm iffI} THEN' RANGE [ |
458 (rtac @{thm iffI} THEN' RANGE [ |