wneuper/isa: comparison src/Tools/isac/Knowledge/GCD_Poly

equal deleted inserted replaced

-:145e45cd7a0f
+:b125dcf14489
 ([1,2,1] %*% [1,3,3,1]) = [1, 5, 10, 10, 5, 1];
 replicate 3 0 = [0, 0, 0];
 replicate 0 0 = [];
-val trace_div = Unsynchronized.ref true;
+val trace_div = Attrib.setup_config_bool \<^binding>\<open>trace_div\<close> (K true);
-val trace_div_invariant = Unsynchronized.ref false; (*.. true expects !trace_div = false *)
+val trace_div_invariant = Attrib.setup_config_bool \<^binding>\<open>trace_div_invariant\<close>
+(K false); (*.. true expects !trace_div = false *)
+val trace_Euclid = Attrib.setup_config_bool \<^binding>\<open>trace_Euclid\<close> (K true);
 fun div_invariant2 p1 p2 n ns zeros q quot remd =
 (@{make_string} p1 ^ " * "  ^ @{make_string} (n * ns) ^ " = " ^
 @{make_string} (mult_to_deg (deg_up p1 - deg_up p2)
 ((zeros @ [q] @ (quot %* n)))) ^
 " ** " ^ @{make_string} p2 ^ " ++ " ^
 @{make_string} ((rev o (mult_to_deg (deg_up p1)) o rev) remd))
 fun writeln_trace p1 p1' p2 quot n q (zeros:int) remd (ns: int) =
-(if (! trace_div) then
+(if Config.get @{context} trace_div then
 ( writeln ("  div   " ^ @{make_string} p1' ^ " * " ^ @{make_string} n);
 writeln  "  div   ~~~~~~~~~~~~~~~~~~~~~~~~~~~";
 writeln ("  div   " ^ @{make_string} (p1' %* n));
 writeln ("  div-- " ^ @{make_string} (mult_to_deg (deg_up p1') p2 %* q) ^
 " <--- " ^ @{make_string} p2 ^ " * " ^ @{make_string} q);
 (*invariant 2: initial p1 *\<^isub>s ns = quot *\<^isub>p p2   +\<^isub>p  remd *)
 if (p1 %* (n * ns)) =
 ((mult_to_deg (deg_up p1 - deg_up p2)
 ((replicate zeros 0) @ [q] @ (quot %* n)) %*% p2 %+% remd))
 then
-if (! trace_div_invariant)
+if Config.get @{context} trace_div_invariant
 then writeln ("  div   " ^ div_invariant2 p1 p2 n ns (replicate zeros 0) q quot remd)
 else ()
 else raise ERROR ("invariant 2 does not hold: " ^ div_invariant2 p1 p2 n ns (replicate zeros 0) q quot remd)
 )
 end
 fun p1 %*/% p2 =
 let
 val (n, q, r) = div_int_up p1 p1 p2 [] 1
-val _ = if (! trace_div) then
+val _ = if Config.get @{context} trace_div then
 (writeln  "  div   .....................................................................";
 writeln ("  div   " ^ @{make_string} n ^ " * " ^ @{make_string} p1 ^ " = " ^
 @{make_string} q ^ " ** " ^ @{make_string} p2 ^ " ++ " ^ @{make_string} r);
 writeln  "  div   ....................................................................."
 ) else ()
 in (n, q, r) end;
 \<close>
 text \<open>Here is the check of the algorithm with the values from above: [[1]]\<close>
-ML \<open>
+declare [[trace_div = true]]
-trace_div := true;
+declare [[trace_div_invariant = false]]
-trace_div_invariant := false;
+ML \<open>
 val p1 = [2, 2, 2, 2, 2];
 val p2 = [1, 2, 3];
 val (n (* = 27*),
 q (* = [8, 6, 18]*),
 r (* = [46, 32]*)) = p1 %*/% p2;
 text \<open>
 The generalized division implemented above really can replace the
 division of integers in the Euclidean Algorithm:
 \<close>
 ML \<open>
-val trace_Euclid = Unsynchronized.ref true;
 fun writeln_trace_Euclid (a: int list) (b: int list) (n: int) (q: int list) (r: int list) =
-if (! trace_Euclid) then
+if Config.get @{context} trace_Euclid then
 writeln ("Euclid "  ^ @{make_string} a ^ "  *  "  ^ @{make_string} n ^
 "  ==  "  ^ @{make_string} q  ^
 "  **  "  ^ @{make_string} b ^ "  ++  "  ^ @{make_string} r)
 else ();
 let
 val (n, q, r) = a %*/% b
 val _ = writeln_trace_Euclid a b n q r
 in EUCLID_naive_up b r : unipoly end;
 \<close>
+declare [[trace_div = false]]
+declare [[trace_div_invariant = false]]
+declare [[trace_Euclid = true]]
 ML \<open>
 (*The example used in the inital mail to Tobias Nipkow made univariate: y -> 1*)
-trace_div := false;
-trace_div_invariant := false;
-trace_Euclid := true;
 "--------------------------------";
 val a = [0,~1,1]: unipoly; (* -x + x^2 =  x   *(-1 + x) *)
 val b = [~1,0,1]: unipoly; (* -1 + x^2 = (1+x)*(-1 + x) *)
 "--------------------------------";
 EUCLID_naive_up a b; (* = [1, ~1]*)          (*( 1 - x) *)
 subsubsection \<open>Interactivity on Euclids Algorithm\<close>
 text \<open>
 Euclids Algorithm in modern algebraic notation explains itself if presented
 this way:
 \<close>
-ML \<open>
+declare [[trace_div = false]]
-trace_div := false;
+declare [[trace_div_invariant = false]]
-trace_div_invariant := false;
+declare [[trace_Euclid = true]]
-trace_Euclid := true;
+ML \<open>
 "--------------------------------";
 val a = [~1,0,0,1]: unipoly; (* -1 + x^3 = (1+x+x^2)*(-1 + x) *)
 val b = [0,~1,1]: unipoly;   (* -x + x^2 = x        *(-1 + x) *)
 "--------------------------------";
 EUCLID_naive_up a b; (*  = [~1, 1]*)      (*(-1 + x)     [[2]]*)
 (*
 Euclid [~1, 0, 0, 1]  *  1  ==  [1, 1]  **  [0, ~1, 1]  ++  [~1, 1]
 Euclid [0, ~1, 1]  *  1  ==  [0, 1]  **  [~1, 1]  ++  []
 *)
 \<close>
-ML \<open>
+declare [[trace_Euclid = true]]
-trace_Euclid := true;
+ML \<open>
 (* from [1].p.94 *)
 "--------------------------------";
 val a = [~18, ~15, ~20, 12, 20, ~13, 2]: unipoly;
 val b = [8, 28, 22, ~11, ~14, 1, 2]: unipoly;
 "--------------------------------";
 (1) a student wants to roughly understand what happens in the algorithm
 (2) a student wants to reproduce the algorithm by hand.
 Case (1) again calls for the fixpoint:
 \<close>
-ML \<open>
+declare [[trace_div = false]]
-trace_div := false;
+declare [[trace_div_invariant = true]]
-trace_div_invariant := true;
+ML \<open>
 val p1 = [2, 2, 2, 2, 2];
 val p2 = [1, 2, 3];
 val (n (* = 27*),
 q (* = [8, 6, 18]*),
 r (* = [46, 32]*)) = p1 %*/% p2;
 divisor.
 This representation, however, is inappropriate for reproduction by hand.
 Dividing polynomials by hand is taught in this format:
 \<close>
-ML \<open>
+declare [[trace_div = true]]
-trace_div := true;
+declare [[trace_div_invariant = false]]
-trace_div_invariant := false;
+ML \<open>
 val p1 = [2, 2, 2, 2, 2];
 val p2 = [1, 2, 3];
 val (n (* = 27*),
 q (* = [8, 6, 18]*),
 r (* = [46, 32]*)) = p1 %*/% p2;
 The above algorithm is unusual in that the dividend first is multiplied
 such that the quotient can have integer coefficients ("generalised division").
 Thus the quotient needs to be multiplied subsequently as well.
 The algorithm also has to handle cases, where zeros occur in the quotient:
 \<close>
-ML \<open>
+declare [[trace_div = true]]
-trace_div := true;
+ML \<open>
 val p1 = [3,2,2,2,1,1,1,1];
 val p2 = [1,1,1,1];
 val (n (* = 1*),
 q (* = [2, 0, 0, 0, 1]*),
 r (* = [1]*)) = p1 %*/% p2;
 text \<open>
 Respective ML code and further examples are at [[1]] above.
 PSEUDO-division is "%*/%";
 we set switches to create output as found in the extended abstract:
 \<close>
-ML \<open>
+declare [[trace_div = false]]
-trace_div_invariant := true;
+declare [[trace_div_invariant = true]]
-trace_div := false;
+ML \<open>
 \<close> ML \<open>
 [1, 2, 3, 4, 5, 6] %*/% [7, 8, 9]
 \<close>
 text \<open>
 We need a notepad for interactive trials!
 And this gives the invariant of the GCD:
 \<close>
-ML \<open>
+declare [[trace_div = true]]
-trace_Euclid := true;
+declare [[trace_div_invariant = false]]
-trace_div_invariant := false;
+ML \<open>
-trace_div := false;
 EUCLID_naive_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2]
 \<close>
 thm gcd_add_mult
 subsection \<open>Step-wise Construction of DIV and GCD\<close>
 text \<open>
 We take smaller polynomials for DIV;
 \<close>
-ML \<open>
+declare [[trace_div = true]]
-trace_div := true;
+declare [[trace_div_invariant = false]]
-trace_div_invariant := false;
+ML \<open>
 [4, 3, 2, 1] %*/% [2, 1]
 \<close>
 text \<open>
 For GCD fill-in gaps in the invariant seem appropriate;
 additionally a notepad is required.

changeset 60507	b125dcf14489
parent 60354	716dd4a05cc8