equal
deleted
inserted
replaced
108 (NONE, _) => [] |
108 (NONE, _) => [] |
109 | (SOME bn, i) => |
109 | (SOME bn, i) => |
110 if member (op=) bodies i then [] |
110 if member (op=) bodies i then [] |
111 else [lookup alpha_bn_map bn $ nth args i $ nth args' i] |
111 else [lookup alpha_bn_map bn $ nth args i $ nth args' i] |
112 |
112 |
113 (* generat the premises for an alpha rule; mk_frees is used |
113 (* generate the premises for an alpha rule; mk_frees is used |
114 if no binders are present *) |
114 if no binders are present *) |
115 fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause = |
115 fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause = |
116 let |
116 let |
117 fun mk_frees i = |
117 fun mk_frees i = |
118 let |
118 let |
624 val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) |
624 val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) |
625 val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns |
625 val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns |
626 |
626 |
627 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} |
627 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} |
628 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) |
628 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) |
|
629 |
629 in |
630 in |
630 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
631 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
631 (K (asm_full_simp_tac ss)) ctxt |
632 (K (asm_full_simp_tac ss)) ctxt |
632 end |
633 end |
633 |
634 |