23 section {* Strong Induction Lemma via Induct_schema *}

    24 

    25 

    26 lemma strong_induct:

    27   fixes c::"'a::fs"

    28   assumes a1: "\<And>name c. P c (Var name)"

    29   and     a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"

    30   and     a3: "\<And>name lam c. \<lbrakk>{atom name} \<sharp>* c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"

    31   shows "P c lam"

    32 using assms

    33 apply(induction_schema)

    34 apply(rule_tac y="lam" in lam.strong_exhaust)

    35 apply(blast)

    36 apply(blast)

    37 apply(blast)

    38 apply(relation "measure (\<lambda>(x,y). size y)")

    39 apply(simp_all add: lam.size)

    40 done

    41