86 lemma

    87   fixes c::"'a::fs"

    88   assumes "\<And>name c. P1 c (Var name)"

    89   and "\<And>c. P1 c Unit"

    90   and "\<And>exp1 exp2 c. \<lbrakk>\<And>c. P1 c exp1; \<And>c. P1 c exp2\<rbrakk> \<Longrightarrow> P1 c (Multi_Recs2.Pair exp1 exp2)"

    91   and "\<And>lrbs exp c. \<lbrakk>b_lrbs lrbs \<sharp>* c; \<And>c. P5 c lrbs; \<And>c. P1 c exp\<rbrakk> \<Longrightarrow> P1 c (LetRec lrbs exp)"

    92   and "\<And>name pat exp c. \<lbrakk>b_pat pat \<sharp>* c; \<And>c. P6 c pat; \<And>c. P1 c exp\<rbrakk> \<Longrightarrow> P2 c (K name pat exp)"

    93   and "\<And>fnclause c. (\<And>c. P2 c fnclause) \<Longrightarrow> P3 c (S fnclause)"

    94   and "\<And>fnclause fnclauses c. \<lbrakk>\<And>c. P2 c fnclause; \<And>c. P3 c fnclauses\<rbrakk> \<Longrightarrow> 

    95     P3 c (ORs fnclause fnclauses)"

    96   and "\<And>fnclauses c. (\<And>c. P3 c fnclauses) \<Longrightarrow> P4 c (Clause fnclauses)"

    97   and "\<And>lrb c. (\<And>c. P4 c lrb) \<Longrightarrow> P5 c (Single lrb)"

    98   and "\<And>lrb lrbs c. \<lbrakk>\<And>c. P4 c lrb; \<And>c. P5 c lrbs\<rbrakk> \<Longrightarrow> P5 c (More lrb lrbs)"

    99   and "\<And>name c. P6 c (PVar name)"

   100   and "\<And>c. P6 c PUnit"

   101   and "\<And>pat1 pat2 c. \<lbrakk>\<And>c. P6 c pat1; \<And>c. P6 c pat2\<rbrakk> \<Longrightarrow> P6 c (PPair pat1 pat2)"

   102   shows "P1 c exp" and "P2 c fnclause" and "P3 c fnclauses" and "P4 c lrb" and "P5 c lrbs" and "P6 c pat"

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

   104   apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1))

   105   apply(simp_all)[4]

   106   apply(blast)

   107   apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2))

   108   apply(blast)

   109   apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3))

   110   apply(blast)

   111   apply(blast)

   112   apply(rule_tac yc="lrb" in fun_recs.strong_exhaust(4))

   113   apply(blast)

   114   apply(rule_tac yd="lrbs" in fun_recs.strong_exhaust(5))

   115   apply(blast)

   116   apply(blast)

   117   apply(rule_tac ye="pat" in fun_recs.strong_exhaust(6))

   118   apply(blast)

   119   apply(blast)

   120   apply(blast)

   121   apply(tactic {* prove_termination_ind @{context} 1 *})

   122   apply(simp_all add: fun_recs.size)

   123   done