# HomogeneousDiffEqn.ml

```(* Copyright INRIA and Microsoft Corporation, 2008-2013. *)
(* 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 =
(*   option `Copyright (c) 1992-2009 by Algorithms Project, INRIA France. \
(*   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.