60 lemma 

    61   fixes t::trm

    62   and   as::assg

    63   and   as'::assg'

    64   and   c::"'a::fs"

    65   assumes a1: "\<And>x c. P1 c (Var x)"

    66   and     a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"

    67   and     a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"

    68   and     a4: "\<And>as t c. \<lbrakk>set (bn1 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let1 as t)"

    69   and     a5: "\<And>as t c. \<lbrakk>set (bn2 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let2 as t)"

    70   and     a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)"

    71   and     a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" 

    72   and     a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)"

    73   and     a9: "\<And>c. P3 c (BNil)"

    74   and     a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)"

    75   shows "P1 c t" "P2 c as" "P3 c as'"

    76 apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})

    77 apply(rule_tac y="t" and c="c" in foo.strong_exhaust(1))

    78 apply(simp_all)[7]

    79 apply(rule_tac ya="as"in foo.strong_exhaust(2))

    80 apply(simp_all)[1]

    81 apply(rule_tac yb="as'" in foo.strong_exhaust(3))

    82 apply(simp_all)[2]

    83 apply(relation "measure (sum_case (size o snd) (sum_case (size o snd) (size o snd)))")

    84 apply(simp_all add: foo.size)

    85 done