--- 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
--- 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
--- 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;
--- 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