# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1379321211 -7200
# Node ID 0d13f07d8e2a7261235325c347692d4c5f2d48f2
# Parent  cd5494eb08fd335f4c19f80bf1aa0afcebac8cbc
tolerate Var in rewriting

diff -r cd5494eb08fd -r 0d13f07d8e2a src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Fri Sep 13 18:57:11 2013 +0200
+++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Sep 16 10:46:51 2013 +0200
@@ -112,7 +112,9 @@
       handle ERROR _ => NONE)
 
 fun is_poly t =
-  let val vs = t |> vars |> map free2str |> sort string_ord
+  let 
+    val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
+      |> filter is_some |> map the |> sort string_ord
   in 
     case poly_of_term vs t of SOME _ => true | NONE => false
   end
@@ -310,7 +312,8 @@
       NONE => NONE
     | SOME (numerator, denominator) =>
       let 
-        val vs = t |> vars |> map free2str |> sort string_ord
+        val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
+          |> filter is_some |> map the |> sort string_ord
         val baseT = type_of numerator
         val expT = HOLogic.realT
       in
@@ -353,7 +356,8 @@
       NONE => NONE
     | SOME (numerator, denominator) =>
       let 
-        val vs = t |> vars |> map free2str |> sort string_ord
+        val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
+          |> filter is_some |> map the |> sort string_ord
         val baseT = type_of numerator
         val expT = HOLogic.realT
       in
@@ -405,7 +409,9 @@
     case opt of 
       NONE => NONE
     | SOME ((n1, d1), (n2, d2)) =>
-      let val vs = t |> vars |> map free2str |> sort string_ord
+      let 
+        val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
+          |> filter is_some |> map the |> sort string_ord
       in
         case (poly_of_term vs d1, poly_of_term vs d2) of
           (SOME a, SOME b) =>
@@ -442,7 +448,8 @@
     NONE => NONE
   | SOME ((n1, d1), (n2, d2)) =>
     let 
-      val vs = t |> vars |> map free2str |> sort string_ord
+      val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
+        |> filter is_some |> map the |> sort string_ord
     in
       case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
         (SOME _, SOME a, SOME _, SOME b) =>
diff -r cd5494eb08fd -r 0d13f07d8e2a src/Tools/isac/ProgLang/termC.sml
--- a/src/Tools/isac/ProgLang/termC.sml	Fri Sep 13 18:57:11 2013 +0200
+++ b/src/Tools/isac/ProgLang/termC.sml	Mon Sep 16 10:46:51 2013 +0200
@@ -261,6 +261,8 @@
 
 fun free2str (Free (s,_)) = s
   | free2str t = error ("free2str not for "^ term2str t);
+fun str_of_free_opt (Free (s,_)) = SOME s
+  | str_of_free_opt _ = NONE
 fun free2int (t as Free (s, _)) = ((str2int s)
     handle _ => error ("free2int: "^term_detail2str t))
   | free2int t = error ("free2int: "^term_detail2str t);
diff -r cd5494eb08fd -r 0d13f07d8e2a test/Tools/isac/Knowledge/partial_fractions.sml
--- a/test/Tools/isac/Knowledge/partial_fractions.sml	Fri Sep 13 18:57:11 2013 +0200
+++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Mon Sep 16 10:46:51 2013 +0200
@@ -322,9 +322,9 @@
 term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
   "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
 
-val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
-if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then ()
-else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
+val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t''; 
+if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then () 
+else error "ansatz_rls - multiply_ansatz - norm_Rational broken"; 
 
 (*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
 val xxx = append_rls "multiply_ansatz_erls" norm_Rational