Subversion Repositories TPPL

Rev

Rev 47 | Blame | Compare with Previous | Last modification | View Log | RSS feed

theory Test_Cancel_Add imports Complex_Main begin

lemma cancel:
  fixes x y :: real
  assumes asm1: "(x^2 - y^2) = (x + y) * (x - y)"
    and asm2: "x^2 - x * y = x * (x - y)"
    and asm3: "x^2 - x * y \<noteq> 0"
  shows "(x^2 - y^2) / (x^2 - x * y) = (x + y) * (x - y) / (x  * (x - (y::real))) \<and> 
                         (x + y) / x = (x + y) * (x - y) / (x  * (x - y))"
  using asm1 asm2 asm3
  apply simp
done

text {* The essential ML function working behind the scenes is:

gcd_poly :: multipoly * multipoly -> (multipoly * multipoly) * multipoly
gcd_poly a b = ((ac, bc), c)
  assumes  a \<noteq> [0]  \<and>  b \<noteq> [0]
  yields  c = gcd a b  \<and>  a = c * ac \<and> b = c * bc

What is presented to the user can be assembled from the function's result:

 a     ac * c
--- = --------   \<and>  bc \<noteq> 0  \<and>  c \<noteq> 0
 b     bc * c

example:
"gcd_poly (x^2 - y^2) (x^2 - x * y) = ((x + y, x), x - y)"

 x\<twosuperior> - y\<twosuperior>       (x + y) * (x - y)
------------ = -----------------     \<and>  x \<noteq> 0  \<and>  x - y \<noteq> 0
 x\<twosuperior> - x * y     x * (x - y)
*}

lemma add:
  assumes asm1: "(x^2 - y^2) = (x + y) * (x - y)" and asm2: "x^2 - x*y = x * (x - y)"
    and asm3: "x^2 - y^2 \<noteq> 0" and asm4: "x^2 + x * y \<noteq> 0"
  shows "x / (x^2 - y^2) + y / (x^2 + x * (y::real)) = 
    x * x / (x * (x + y) * (x - y)) + y * (x - y) / (x * (x + y) * (x - y))"
  apply (insert asm1 asm2 asm3 asm4)
  apply simp
  apply (simp add: algebra_simps)
done

text {* The essential ML function working behind the scenes is the same as above.

What is presented to the user can be assembled from the function's result:

 n1     n2     bc * n1          n2 * ac
---- + ---- = ------------ + -------------------   \<and>  bc \<noteq> 0  \<and>  c \<noteq> 0  \<and>  ac \<noteq> 0
 a      b     bc * c * ac     bc * c * ac

example:
    x           y           x * x                              y * (x + y)
--------- + ------------ = ----------------------- + -----------------------  \<and> ...
 x\<twosuperior> - y\<twosuperior>     x\<twosuperior> - x * y     x * (x - y) * (x + y)     x * (x - y) * (x + y)

                                             ... \<and> x \<noteq> 0  \<and>  x - y \<noteq> 0  \<and>  x + y \<noteq> 0
*}

ML {* @{thms algebra_simps} *}

text {* algebra_simps need improvement for addition:
======= lemma add:
  assumes asm1: "(x^2 - y^2) = (x + y) * (x - y)" and asm2: "x^2 - x*y = x * (x - y)"
    and asm3: "x^2 - y^2 \<noteq> 0" and asm4: "x^2 + x * y \<noteq> 0"
  shows "x / (x^2 - y^2) + y / (x^2 + x * (y::real)) = 
    x * x / (x * (x + y) * (x - y)) + y * (x - y) / (x * (x + y) * (x - y)) \<and> 
    x * x / (x * (x + y) * (x - y)) + y * (x - y) / (x * (x + y) * (x - y)) =
         (x * x + y * (x - y)) / (x * (x + y) * (x - y))"
  apply (insert asm1 asm2 asm3 asm4)
  apply simp
  apply (simp add: algebra_simps)
  done

======= leads to:
proof (prove): step 3

goal (1 subgoal):
 1. y * y = y\<twosuperior> \<Longrightarrow>
    x\<twosuperior> = x * x \<Longrightarrow>
    x + y \<noteq> 0 \<and> x \<noteq> y \<Longrightarrow>
    x * x + x * y \<noteq> 0 \<Longrightarrow>
    x \<noteq> 0 \<longrightarrow> y / (x * x + x * y) + x / (x * x - y\<twosuperior>) = (x * x + x * y - y\<twosuperior>) / (x * (x * x) - x * y\<twosuperior>) 
*}

end