# HG changeset patch
# User Philipp Meyer
# Date 1253611606 -7200
# Node ID 962b4354ed90a6dd1545b2b7ab848519e4d4bc7c
# Parent  1cc5b24f5a01ae68c2e806206235eda6b391f1ce
used standard fold function and type aliases

diff -r 1cc5b24f5a01 -r 962b4354ed90 src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
--- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Mon Sep 21 15:05:26 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Tue Sep 22 11:26:46 2009 +0200
@@ -82,31 +82,31 @@
 
 (* basic parser *)
 
-fun $$ k = Scan.this_string k
+val str = Scan.this_string
 
 val number = Scan.repeat1 (Scan.one Symbol.is_ascii_digit >>
   (fn s => ord s - ord "0")) >>
   foldl1 (fn (n, d) => n * 10 + d)
 
 val nat = number
-val int = Scan.optional ($$ "~" >> K ~1) 1 -- nat >> op *;
-val rat = int --| $$ "/" -- int >> Rat.rat_of_quotient
+val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op *;
+val rat = int --| str "/" -- int >> Rat.rat_of_quotient
 val rat_int = rat || int >> Rat.rat_of_int
 
 (* polynomial parser *)
 
-fun repeat_sep s f = f ::: Scan.repeat ($$ s |-- f)
+fun repeat_sep s f = f ::: Scan.repeat (str s |-- f)
 
 val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
 
-fun parse_varpow ctxt = parse_id -- Scan.optional ($$ "^" |-- nat) 1 >>
+fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
   (fn (x, k) => (cterm_of (Context.theory_of_proof ctxt) (Free (x, @{typ real})), k)) 
 
 fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
   foldl (uncurry Ctermfunc.update) Ctermfunc.undefined
 
 fun parse_cmonomial ctxt =
-  rat_int --| $$ "*" -- (parse_monomial ctxt) >> swap ||
+  rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
   (parse_monomial ctxt) >> (fn m => (m, Rat.one)) ||
   rat_int >> (fn r => (Ctermfunc.undefined, r))
 
@@ -116,14 +116,14 @@
 (* positivstellensatz parser *)
 
 val parse_axiom =
-  ($$ "A=" |-- int >> Axiom_eq) ||
-  ($$ "A<=" |-- int >> Axiom_le) ||
-  ($$ "A<" |-- int >> Axiom_lt)
+  (str "A=" |-- int >> Axiom_eq) ||
+  (str "A<=" |-- int >> Axiom_le) ||
+  (str "A<" |-- int >> Axiom_lt)
 
 val parse_rational =
-  ($$ "R=" |-- rat_int >> Rational_eq) ||
-  ($$ "R<=" |-- rat_int >> Rational_le) ||
-  ($$ "R<" |-- rat_int >> Rational_lt)
+  (str "R=" |-- rat_int >> Rational_eq) ||
+  (str "R<=" |-- rat_int >> Rational_le) ||
+  (str "R<" |-- rat_int >> Rational_lt)
 
 fun parse_cert ctxt input =
   let
@@ -132,10 +132,10 @@
   in
   (parse_axiom ||
    parse_rational ||
-   $$ "[" |-- pp --| $$ "]^2" >> Square ||
-   $$ "([" |-- pp --| $$ "]*" -- pc --| $$ ")" >> Eqmul ||
-   $$ "(" |-- pc --| $$ "*" -- pc --| $$ ")" >> Product ||
-   $$ "(" |-- pc --| $$ "+" -- pc --| $$ ")" >> Sum) input
+   str "[" |-- pp --| str "]^2" >> Square ||
+   str "([" |-- pp --| str "]*" -- pc --| str ")" >> Eqmul ||
+   str "(" |-- pc --| str "*" -- pc --| str ")" >> Product ||
+   str "(" |-- pc --| str "+" -- pc --| str ")" >> Sum) input
   end
 
 fun parse_cert_tree ctxt input =
@@ -143,15 +143,15 @@
     val pc = parse_cert ctxt
     val pt = parse_cert_tree ctxt
   in
-  ($$ "()" >> K Trivial ||
-   $$ "(" |-- pc --| $$ ")" >> Cert ||
-   $$ "(" |-- pt --| $$ "&" -- pt --| $$ ")" >> Branch) input
+  (str "()" >> K Trivial ||
+   str "(" |-- pc --| str ")" >> Cert ||
+   str "(" |-- pt --| str "&" -- pt --| str ")" >> Branch) input
   end
 
 (* scanner *)
 
-fun cert_to_pss_tree ctxt str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt)
-  (filter_out Symbol.is_blank (Symbol.explode str))
+fun cert_to_pss_tree ctxt input_str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt)
+  (filter_out Symbol.is_blank (Symbol.explode input_str))
 
 end
 
diff -r 1cc5b24f5a01 -r 962b4354ed90 src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Mon Sep 21 15:05:26 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Tue Sep 22 11:26:46 2009 +0200
@@ -141,29 +141,19 @@
 fun output_line cert = "To repeat this proof with a certifiate use this command:\n" ^
         (Markup.markup Markup.sendback) ("by (sos_cert \"" ^ cert ^ "\")")
 
-fun print_certs pss_tree =
-  let
-    val cert = PositivstellensatzTools.pss_tree_to_cert pss_tree
-    val str = output_line cert
-  in
-    Output.writeln str
-  end
+val print_cert = Output.writeln o output_line o PositivstellensatzTools.pss_tree_to_cert
 
 (* setup tactic *)
 
-fun parse_cert (ctxt, tk) =
-  let
-    val (str, tk') = OuterParse.string tk
-    val cert = PositivstellensatzTools.cert_to_pss_tree (Context.proof_of ctxt) str
-  in
-    (cert, (ctxt, tk'))
-  end
+fun parse_cert (input as (ctxt, _)) = 
+  (Scan.lift OuterParse.string >>
+    PositivstellensatzTools.cert_to_pss_tree (Context.proof_of ctxt)) input
 
 fun sos_solver print method = (SIMPLE_METHOD' o (Sos.sos_tac print method)) 
 
 val sos_method =
    Scan.lift (Scan.option OuterParse.xname) >> (fn n => Sos.Prover (call_solver n)) >>
-   sos_solver print_certs
+   sos_solver print_cert
 
 val sos_cert_method =
   parse_cert >> Sos.Certificate >> sos_solver ignore
diff -r 1cc5b24f5a01 -r 962b4354ed90 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Mon Sep 21 15:05:26 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Tue Sep 22 11:26:46 2009 +0200
@@ -13,7 +13,7 @@
   | Prover of (string -> string)
 
   val sos_tac : (RealArith.pss_tree -> unit) ->
-    proof_method -> Proof.context -> int -> Tactical.tactic
+    proof_method -> Proof.context -> int -> tactic
 
   val debugging : bool ref;
   
@@ -345,8 +345,6 @@
   sort humanorder_varpow (Ctermfunc.graph m2))
 end;
 
-fun fold1 f = foldr1 (uncurry f) 
-
 (* Conversions to strings.                                                   *)
 
 fun string_of_vector min_size max_size (v:vector) =
@@ -355,7 +353,7 @@
   let 
    val n = max min_size (min n_raw max_size) 
    val xs = map (Rat.string_of_rat o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
-  in "[" ^ fold1 (fn s => fn t => s ^ ", " ^ t) xs ^
+  in "[" ^ foldr1 (fn (s, t) => s ^ ", " ^ t) xs ^
   (if n_raw > max_size then ", ...]" else "]")
   end
  end;
@@ -366,7 +364,7 @@
   val i = min max_size i_raw 
   val j = min max_size j_raw
   val rstr = map (fn k => string_of_vector j j (row k m)) (1 upto i) 
- in "["^ fold1 (fn s => fn t => s^";\n "^t) rstr ^
+ in "["^ foldr1 (fn (s, t) => s^";\n "^t) rstr ^
   (if j > max_size then "\n ...]" else "]")
  end;
 
@@ -392,7 +390,7 @@
  if Ctermfunc.is_undefined m then "1" else
  let val vps = fold_rev (fn (x,k) => fn a => string_of_varpow x k :: a)
   (sort humanorder_varpow (Ctermfunc.graph m)) [] 
- in fold1 (fn s => fn t => s^"*"^t) vps
+ in foldr1 (fn (s, t) => s^"*"^t) vps
  end;
 
 fun string_of_cmonomial (c,m) =
@@ -474,7 +472,7 @@
  let 
   val n = dim v
   val strs = map (decimalize 20 o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
- in fold1 (fn x => fn y => x ^ " " ^ y) strs ^ "\n"
+ in foldr1 (fn (x, y) => x ^ " " ^ y) strs ^ "\n"
  end;
 
 fun triple_int_ord ((a,b,c),(a',b',c')) = 
@@ -984,7 +982,7 @@
  let val alts =
   map (fn k => let val oths = enumerate_monomials (d - k) (tl vars) 
                in map (fn ks => if k = 0 then ks else Ctermfunc.update (hd vars, k) ks) oths end) (0 upto d) 
- in fold1 (curry op @) alts
+ in foldr1 op @ alts
  end;
 
 (* Enumerate products of distinct input polys with degree <= d.              *)
@@ -1035,7 +1033,7 @@
  in
   string_of_int m ^ "\n" ^
   string_of_int nblocks ^ "\n" ^
-  (fold1 (fn s => fn t => s^" "^t) (map string_of_int blocksizes)) ^
+  (foldr1 (fn (s, t) => s^" "^t) (map string_of_int blocksizes)) ^
   "\n" ^
   sdpa_of_vector obj ^
   fold_rev2 (fn k => fn m => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a)
@@ -1210,7 +1208,7 @@
 fun cterm_of_sqterm (c,p) = Product(Rational_lt c,Square p);
 
 fun cterm_of_sos (pr,sqs) = if null sqs then pr
-  else Product(pr,fold1 (fn a => fn b => Sum(a,b)) (map cterm_of_sqterm sqs));
+  else Product(pr,foldr1 (fn (a, b) => Sum(a,b)) (map cterm_of_sqterm sqs));
 
 end
 
@@ -1283,11 +1281,11 @@
            map2 (fn q => fn (p,ax) => Eqmul(q,ax)) cert_ideal eq
          val proofs_cone = map cterm_of_sos cert_cone
          val proof_ne = if null ltp then Rational_lt Rat.one else
-           let val p = fold1 (fn s => fn t => Product(s,t)) (map snd ltp) 
+           let val p = foldr1 (fn (s, t) => Product(s,t)) (map snd ltp) 
            in  funpow i (fn q => Product(p,q)) (Rational_lt Rat.one)
            end
          in 
-           fold1 (fn s => fn t => Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) 
+           foldr1 (fn (s, t) => Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) 
          end)
      in
         (translator (eqs,les,lts) proof, Cert proof)
@@ -1426,12 +1424,12 @@
               else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs))
 in () end
 
-fun core_sos_tac print_certs prover ctxt = CSUBGOAL (fn (ct, i) => 
+fun core_sos_tac print_cert prover ctxt = CSUBGOAL (fn (ct, i) => 
   let val _ = check_sos known_sos_constants ct
       val (avs, p) = strip_all ct
       val (ths, certificates) = real_sos prover ctxt (Thm.dest_arg p)
       val th = standard (fold_rev forall_intr avs ths)
-      val _ = print_certs certificates
+      val _ = print_cert certificates
   in rtac th i end);
 
 fun default_SOME f NONE v = SOME v
@@ -1469,7 +1467,7 @@
 
 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
 
-fun sos_tac print_certs prover ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac print_certs prover ctxt
+fun sos_tac print_cert prover ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac print_cert prover ctxt
 
 
 end;
diff -r 1cc5b24f5a01 -r 962b4354ed90 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Mon Sep 21 15:05:26 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Tue Sep 22 11:26:46 2009 +0200
@@ -146,19 +146,19 @@
 type cert_conv = cterm -> thm * pss_tree
 
 val gen_gen_real_arith :
-  Proof.context -> (Rat.rat -> Thm.cterm) * conv * conv * conv *
+  Proof.context -> (Rat.rat -> cterm) * conv * conv * conv *
    conv * conv * conv * conv * conv * conv * prover -> cert_conv
 val real_linear_prover : (thm list * thm list * thm list -> positivstellensatz -> thm) ->
   thm list * thm list * thm list -> thm * pss_tree
 
 val gen_real_arith : Proof.context ->
-  (Rat.rat -> Thm.cterm) * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv
+  (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv
 
 val gen_prover_real_arith : Proof.context -> prover -> cert_conv
 
-val is_ratconst : Thm.cterm -> bool
-val dest_ratconst : Thm.cterm -> Rat.rat
-val cterm_of_rat : Rat.rat -> Thm.cterm
+val is_ratconst : cterm -> bool
+val dest_ratconst : cterm -> Rat.rat
+val cterm_of_rat : Rat.rat -> cterm
 
 end