27 thm permute_trm_raw_permute_assg_raw.simps[no_vars]

    28 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars]

    29 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]

    30 

    31 ML {* val {inducts, ... } = Function.get_info @{context} @{term "fv_trm_raw"}*}

    32 ML {* Rule_Cases.strict_mutual_rule @{context} (the inducts) *}

    33 

    34 lemma

    35  shows "p1 \<bullet> fv_trm_raw trm_raw = fv_trm_raw (p1 \<bullet> trm_raw)"

    36  and "p1 \<bullet> fv_assg_raw assg_raw = fv_assg_raw (p1 \<bullet> assg_raw)"

    37  and "p1 \<bullet> fv_bn_raw assg_raw = fv_bn_raw (p1 \<bullet> assg_raw)"

    38 apply(induct trm_raw and assg_raw and assg_raw rule: fv_trm_raw_fv_assg_raw_fv_bn_raw.induct)

    39 apply(perm_simp add: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps, rule refl)+

    40 done

    41 

    42 

    43