26 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}

    26 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}

    27 

    27 

    28 term "supp (x :: lam)"

    28 term "supp (x :: lam)"

    29 lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted]

    29 lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted]

    30 

    30 

    31 lemma infinite_Un:

    32 lemma infinite_Un:

    32   shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"

    33   shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"

    35 

    35 

    36 lemma bi_eqvt:

    36 lemma bi_eqvt:

    37   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"

    37   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"

    39 

    45 

    40 lemma supp_fv:

    46 lemma supp_fv:

    41   "supp t = fv_lam t" and 

    47   "supp t = fv_lam t" and 

    42   "supp b = fv_bp b"

    48   "supp b = fv_bp b"

    43 apply(induct t and b rule: lam_bp_inducts)

    49 apply(induct t and b rule: lam_bp_inducts)