87 

    88 

    89 lemma

    90   fixes c::"'a::fs"

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

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

    93   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)"

    94   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)"

    95   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)"

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

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

    98     P3 c (ORs fnclause fnclauses)"

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

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

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

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

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

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

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

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

   107 oops

   108 

   109 ML {*

   110   val trm1 = @{prop "P1 &&& P2 &&& P3"}

   111   val trm2 = @{prop "(P1 &&& P2) &&& P3 &&& P4"}

   112 *}

   113 

   114 ML {*

   115   Logic.dest_conjunction_list trm1;

   116   Logic.dest_conjunction_list trm2

   117 *}

   118 

   119 ML {*

   120   Logic.dest_conjunctions trm1;

   121   Logic.dest_conjunctions trm2

   122 *}

   123 

   124