src/Pure/drule.ML
changeset 52223 5bb6ae8acb87
parent 52131 366fa32ee2a3
child 52224 6ba76ad4e679
equal deleted inserted replaced
52222:0fa3b456a267 52223:5bb6ae8acb87
   357 
   357 
   358 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
   358 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
   359   with no lifting or renaming!  Q may contain ==> or meta-quants
   359   with no lifting or renaming!  Q may contain ==> or meta-quants
   360   ALWAYS deletes premise i *)
   360   ALWAYS deletes premise i *)
   361 fun compose(tha,i,thb) =
   361 fun compose(tha,i,thb) =
   362   distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb));
   362   distinct Thm.eq_thm
       
   363     (Seq.list_of
       
   364       (Thm.bicompose {flatten = true, match = false, incremented = false} (false, tha, 0) i thb));
   363 
   365 
   364 fun compose_single (tha,i,thb) =
   366 fun compose_single (tha,i,thb) =
   365   (case compose (tha,i,thb) of
   367   (case compose (tha,i,thb) of
   366     [th] => th
   368     [th] => th
   367   | _ => raise THM ("compose: unique result expected", i, [tha,thb]));
   369   | _ => raise THM ("compose: unique result expected", i, [tha,thb]));
   741 fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2;
   743 fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2;
   742 fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2;
   744 fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2;
   743 
   745 
   744 fun comp_no_flatten (th, n) i rule =
   746 fun comp_no_flatten (th, n) i rule =
   745   (case distinct Thm.eq_thm (Seq.list_of
   747   (case distinct Thm.eq_thm (Seq.list_of
   746       (Thm.compose_no_flatten false (th, n) i (incr_indexes th rule))) of
   748       (Thm.bicompose {flatten = false, match = false, incremented = true}
       
   749         (false, th, n) i (incr_indexes th rule))) of
   747     [th'] => th'
   750     [th'] => th'
   748   | [] => raise THM ("comp_no_flatten", i, [th, rule])
   751   | [] => raise THM ("comp_no_flatten", i, [th, rule])
   749   | _ => raise THM ("comp_no_flatten: unique result expected", i, [th, rule]));
   752   | _ => raise THM ("comp_no_flatten: unique result expected", i, [th, rule]));
   750 
   753 
   751 
   754