HomogeneousDiffEqn.ml

(* Copyright INRIA and Microsoft Corporation, 2008-2013. *)
(* DDMF is distributed under CeCILL-B license, *)
(* however this file is distributed under the LGPL version 2.1. *)

INCLUDE "preamble.ml"

(* Converts a differential equation to a homogeneous equation. *)
(* Input: *)
(*     Deq: differential equation *)
(*     yofx: its unknown function *)
(* Output: *)
(*   a homogeneous linear differential equation having the solutions *)
(*   of deq as solutions *)

(* TODO this function does not display its input at the beginning of the *)
(* proof.  Be consistent with diffeqtorec! *)

let diffeqtohomdiffeq initial_deq yofx =
  (* Have to return to the Maple code, if extracted. *)
  (*   option `Copyright (c) 1992-2009 by Algorithms Project, INRIA France. \
All rights reserved.`; *)
  (*   local deq, y, x, ini, c, dc, n, i, iszero; *)
  <:unit<
    deq := gfun:-formatdiffeq([$(initial_deq),$(yofx)],'y','x','ini')
  >> ;
  if <:bool< deq[1]=0 >> then begin
    (<:par< The differential equation is homogenous. >>, initial_deq)
  end else begin
    <:unit<
      n:=nops(deq);
      c:=deq[1];
      dc:=-diff(c,x)
    >> ;

    let text =
      if <:bool< has(c,x) >> then
        <:par<
          Dividing the differential equation by its inhomogeneous part
          results in <:isymb< gfun:-makediffeq(map(t -> t/c,deq),y,x) = 0 >>
        >>
      else
        <:par< Differentiating the equation yields
          <:dmath<
            <<
              gfun:-makediffeq(
                map(t -> numer(t)/denom(t),
                    [0, dc*deq[2]/c^2+diff(deq[2],x)/c,
                     seq(dc*deq[i]/c^2 + diff(deq[i],x)/c + deq[i-1]/c,
                       i=3..n),
                     deq[n]/c],
                     x),
                y, x)
            >> = 0 .
          >>
        >> @:@
        (if <:bool< c^2 <> 1 >> then
          <:par<
            After multiplying by <:isymb< c^2 >>, the equation becomes
            <:isymb<
              gfun:-makediffeq(
                map(collect,
                  [0, dc*deq[2]+c*diff(deq[2],x),
                   seq(dc*deq[i]+c*diff(deq[i],x)+c*deq[i-1], i=3..n),
                   c*deq[n]],
                  x),
                y,x) = 0 >>
          >>
        else <:par<>>) in

    let par, res =
      if <:bool< ini <> {} or n=2 >> then begin
        <:unit<
          ini,iszero := gfun:-`goodinitvalues/diffeq`(deq,y,x,ini,n-2)
        >> ;
        if <:bool< iszero >> then
          (text, Some << [0,1] >>)
        else begin
          let ending = Wording.ending_of_seq << ini >> in
          (text @:@
           <:par<
             From the given initial condition$(str:ending), and from evaluating
             the inhomogeneous equation at <:isymb<  x=0 >>, we obtain the
             initial conditions <:dmath< << op(ini) >> . >>
           >>,
           None)
        end
      end else (text, None) in

    (par,
     match res with
     | Some r -> r
     | None ->
        <<
          gfun:-makediffeq(
            map(collect,
              [0, dc*deq[2]+c*diff(deq[2],x),
               seq(dc*deq[i]+c*diff(deq[i],x)+c*deq[i-1], i=3..n),
               c*deq[n]],
              x),
            y,x,ini)
        >>)
  end

Generated by GNU Enscript 1.6.5.90.