used standard fold function and type aliases
authorPhilipp Meyer
Tue Sep 22 11:26:46 2009 +0200 (2009-09-22)
changeset 32646962b4354ed90
parent 32645 1cc5b24f5a01
child 32647 e54f47f9e28b
child 32699 250b4d8342ca
used standard fold function and type aliases
src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Mon Sep 21 15:05:26 2009 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Tue Sep 22 11:26:46 2009 +0200
     1.3 @@ -82,31 +82,31 @@
     1.4  
     1.5  (* basic parser *)
     1.6  
     1.7 -fun $$ k = Scan.this_string k
     1.8 +val str = Scan.this_string
     1.9  
    1.10  val number = Scan.repeat1 (Scan.one Symbol.is_ascii_digit >>
    1.11    (fn s => ord s - ord "0")) >>
    1.12    foldl1 (fn (n, d) => n * 10 + d)
    1.13  
    1.14  val nat = number
    1.15 -val int = Scan.optional ($$ "~" >> K ~1) 1 -- nat >> op *;
    1.16 -val rat = int --| $$ "/" -- int >> Rat.rat_of_quotient
    1.17 +val int = Scan.optional (str "~" >> K ~1) 1 -- nat >> op *;
    1.18 +val rat = int --| str "/" -- int >> Rat.rat_of_quotient
    1.19  val rat_int = rat || int >> Rat.rat_of_int
    1.20  
    1.21  (* polynomial parser *)
    1.22  
    1.23 -fun repeat_sep s f = f ::: Scan.repeat ($$ s |-- f)
    1.24 +fun repeat_sep s f = f ::: Scan.repeat (str s |-- f)
    1.25  
    1.26  val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
    1.27  
    1.28 -fun parse_varpow ctxt = parse_id -- Scan.optional ($$ "^" |-- nat) 1 >>
    1.29 +fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
    1.30    (fn (x, k) => (cterm_of (Context.theory_of_proof ctxt) (Free (x, @{typ real})), k)) 
    1.31  
    1.32  fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
    1.33    foldl (uncurry Ctermfunc.update) Ctermfunc.undefined
    1.34  
    1.35  fun parse_cmonomial ctxt =
    1.36 -  rat_int --| $$ "*" -- (parse_monomial ctxt) >> swap ||
    1.37 +  rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
    1.38    (parse_monomial ctxt) >> (fn m => (m, Rat.one)) ||
    1.39    rat_int >> (fn r => (Ctermfunc.undefined, r))
    1.40  
    1.41 @@ -116,14 +116,14 @@
    1.42  (* positivstellensatz parser *)
    1.43  
    1.44  val parse_axiom =
    1.45 -  ($$ "A=" |-- int >> Axiom_eq) ||
    1.46 -  ($$ "A<=" |-- int >> Axiom_le) ||
    1.47 -  ($$ "A<" |-- int >> Axiom_lt)
    1.48 +  (str "A=" |-- int >> Axiom_eq) ||
    1.49 +  (str "A<=" |-- int >> Axiom_le) ||
    1.50 +  (str "A<" |-- int >> Axiom_lt)
    1.51  
    1.52  val parse_rational =
    1.53 -  ($$ "R=" |-- rat_int >> Rational_eq) ||
    1.54 -  ($$ "R<=" |-- rat_int >> Rational_le) ||
    1.55 -  ($$ "R<" |-- rat_int >> Rational_lt)
    1.56 +  (str "R=" |-- rat_int >> Rational_eq) ||
    1.57 +  (str "R<=" |-- rat_int >> Rational_le) ||
    1.58 +  (str "R<" |-- rat_int >> Rational_lt)
    1.59  
    1.60  fun parse_cert ctxt input =
    1.61    let
    1.62 @@ -132,10 +132,10 @@
    1.63    in
    1.64    (parse_axiom ||
    1.65     parse_rational ||
    1.66 -   $$ "[" |-- pp --| $$ "]^2" >> Square ||
    1.67 -   $$ "([" |-- pp --| $$ "]*" -- pc --| $$ ")" >> Eqmul ||
    1.68 -   $$ "(" |-- pc --| $$ "*" -- pc --| $$ ")" >> Product ||
    1.69 -   $$ "(" |-- pc --| $$ "+" -- pc --| $$ ")" >> Sum) input
    1.70 +   str "[" |-- pp --| str "]^2" >> Square ||
    1.71 +   str "([" |-- pp --| str "]*" -- pc --| str ")" >> Eqmul ||
    1.72 +   str "(" |-- pc --| str "*" -- pc --| str ")" >> Product ||
    1.73 +   str "(" |-- pc --| str "+" -- pc --| str ")" >> Sum) input
    1.74    end
    1.75  
    1.76  fun parse_cert_tree ctxt input =
    1.77 @@ -143,15 +143,15 @@
    1.78      val pc = parse_cert ctxt
    1.79      val pt = parse_cert_tree ctxt
    1.80    in
    1.81 -  ($$ "()" >> K Trivial ||
    1.82 -   $$ "(" |-- pc --| $$ ")" >> Cert ||
    1.83 -   $$ "(" |-- pt --| $$ "&" -- pt --| $$ ")" >> Branch) input
    1.84 +  (str "()" >> K Trivial ||
    1.85 +   str "(" |-- pc --| str ")" >> Cert ||
    1.86 +   str "(" |-- pt --| str "&" -- pt --| str ")" >> Branch) input
    1.87    end
    1.88  
    1.89  (* scanner *)
    1.90  
    1.91 -fun cert_to_pss_tree ctxt str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt)
    1.92 -  (filter_out Symbol.is_blank (Symbol.explode str))
    1.93 +fun cert_to_pss_tree ctxt input_str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt)
    1.94 +  (filter_out Symbol.is_blank (Symbol.explode input_str))
    1.95  
    1.96  end
    1.97  
     2.1 --- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Mon Sep 21 15:05:26 2009 +0200
     2.2 +++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Tue Sep 22 11:26:46 2009 +0200
     2.3 @@ -141,29 +141,19 @@
     2.4  fun output_line cert = "To repeat this proof with a certifiate use this command:\n" ^
     2.5          (Markup.markup Markup.sendback) ("by (sos_cert \"" ^ cert ^ "\")")
     2.6  
     2.7 -fun print_certs pss_tree =
     2.8 -  let
     2.9 -    val cert = PositivstellensatzTools.pss_tree_to_cert pss_tree
    2.10 -    val str = output_line cert
    2.11 -  in
    2.12 -    Output.writeln str
    2.13 -  end
    2.14 +val print_cert = Output.writeln o output_line o PositivstellensatzTools.pss_tree_to_cert
    2.15  
    2.16  (* setup tactic *)
    2.17  
    2.18 -fun parse_cert (ctxt, tk) =
    2.19 -  let
    2.20 -    val (str, tk') = OuterParse.string tk
    2.21 -    val cert = PositivstellensatzTools.cert_to_pss_tree (Context.proof_of ctxt) str
    2.22 -  in
    2.23 -    (cert, (ctxt, tk'))
    2.24 -  end
    2.25 +fun parse_cert (input as (ctxt, _)) = 
    2.26 +  (Scan.lift OuterParse.string >>
    2.27 +    PositivstellensatzTools.cert_to_pss_tree (Context.proof_of ctxt)) input
    2.28  
    2.29  fun sos_solver print method = (SIMPLE_METHOD' o (Sos.sos_tac print method)) 
    2.30  
    2.31  val sos_method =
    2.32     Scan.lift (Scan.option OuterParse.xname) >> (fn n => Sos.Prover (call_solver n)) >>
    2.33 -   sos_solver print_certs
    2.34 +   sos_solver print_cert
    2.35  
    2.36  val sos_cert_method =
    2.37    parse_cert >> Sos.Certificate >> sos_solver ignore
     3.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Mon Sep 21 15:05:26 2009 +0200
     3.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Tue Sep 22 11:26:46 2009 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4    | Prover of (string -> string)
     3.5  
     3.6    val sos_tac : (RealArith.pss_tree -> unit) ->
     3.7 -    proof_method -> Proof.context -> int -> Tactical.tactic
     3.8 +    proof_method -> Proof.context -> int -> tactic
     3.9  
    3.10    val debugging : bool ref;
    3.11    
    3.12 @@ -345,8 +345,6 @@
    3.13    sort humanorder_varpow (Ctermfunc.graph m2))
    3.14  end;
    3.15  
    3.16 -fun fold1 f = foldr1 (uncurry f) 
    3.17 -
    3.18  (* Conversions to strings.                                                   *)
    3.19  
    3.20  fun string_of_vector min_size max_size (v:vector) =
    3.21 @@ -355,7 +353,7 @@
    3.22    let 
    3.23     val n = max min_size (min n_raw max_size) 
    3.24     val xs = map (Rat.string_of_rat o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
    3.25 -  in "[" ^ fold1 (fn s => fn t => s ^ ", " ^ t) xs ^
    3.26 +  in "[" ^ foldr1 (fn (s, t) => s ^ ", " ^ t) xs ^
    3.27    (if n_raw > max_size then ", ...]" else "]")
    3.28    end
    3.29   end;
    3.30 @@ -366,7 +364,7 @@
    3.31    val i = min max_size i_raw 
    3.32    val j = min max_size j_raw
    3.33    val rstr = map (fn k => string_of_vector j j (row k m)) (1 upto i) 
    3.34 - in "["^ fold1 (fn s => fn t => s^";\n "^t) rstr ^
    3.35 + in "["^ foldr1 (fn (s, t) => s^";\n "^t) rstr ^
    3.36    (if j > max_size then "\n ...]" else "]")
    3.37   end;
    3.38  
    3.39 @@ -392,7 +390,7 @@
    3.40   if Ctermfunc.is_undefined m then "1" else
    3.41   let val vps = fold_rev (fn (x,k) => fn a => string_of_varpow x k :: a)
    3.42    (sort humanorder_varpow (Ctermfunc.graph m)) [] 
    3.43 - in fold1 (fn s => fn t => s^"*"^t) vps
    3.44 + in foldr1 (fn (s, t) => s^"*"^t) vps
    3.45   end;
    3.46  
    3.47  fun string_of_cmonomial (c,m) =
    3.48 @@ -474,7 +472,7 @@
    3.49   let 
    3.50    val n = dim v
    3.51    val strs = map (decimalize 20 o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
    3.52 - in fold1 (fn x => fn y => x ^ " " ^ y) strs ^ "\n"
    3.53 + in foldr1 (fn (x, y) => x ^ " " ^ y) strs ^ "\n"
    3.54   end;
    3.55  
    3.56  fun triple_int_ord ((a,b,c),(a',b',c')) = 
    3.57 @@ -984,7 +982,7 @@
    3.58   let val alts =
    3.59    map (fn k => let val oths = enumerate_monomials (d - k) (tl vars) 
    3.60                 in map (fn ks => if k = 0 then ks else Ctermfunc.update (hd vars, k) ks) oths end) (0 upto d) 
    3.61 - in fold1 (curry op @) alts
    3.62 + in foldr1 op @ alts
    3.63   end;
    3.64  
    3.65  (* Enumerate products of distinct input polys with degree <= d.              *)
    3.66 @@ -1035,7 +1033,7 @@
    3.67   in
    3.68    string_of_int m ^ "\n" ^
    3.69    string_of_int nblocks ^ "\n" ^
    3.70 -  (fold1 (fn s => fn t => s^" "^t) (map string_of_int blocksizes)) ^
    3.71 +  (foldr1 (fn (s, t) => s^" "^t) (map string_of_int blocksizes)) ^
    3.72    "\n" ^
    3.73    sdpa_of_vector obj ^
    3.74    fold_rev2 (fn k => fn m => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a)
    3.75 @@ -1210,7 +1208,7 @@
    3.76  fun cterm_of_sqterm (c,p) = Product(Rational_lt c,Square p);
    3.77  
    3.78  fun cterm_of_sos (pr,sqs) = if null sqs then pr
    3.79 -  else Product(pr,fold1 (fn a => fn b => Sum(a,b)) (map cterm_of_sqterm sqs));
    3.80 +  else Product(pr,foldr1 (fn (a, b) => Sum(a,b)) (map cterm_of_sqterm sqs));
    3.81  
    3.82  end
    3.83  
    3.84 @@ -1283,11 +1281,11 @@
    3.85             map2 (fn q => fn (p,ax) => Eqmul(q,ax)) cert_ideal eq
    3.86           val proofs_cone = map cterm_of_sos cert_cone
    3.87           val proof_ne = if null ltp then Rational_lt Rat.one else
    3.88 -           let val p = fold1 (fn s => fn t => Product(s,t)) (map snd ltp) 
    3.89 +           let val p = foldr1 (fn (s, t) => Product(s,t)) (map snd ltp) 
    3.90             in  funpow i (fn q => Product(p,q)) (Rational_lt Rat.one)
    3.91             end
    3.92           in 
    3.93 -           fold1 (fn s => fn t => Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) 
    3.94 +           foldr1 (fn (s, t) => Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) 
    3.95           end)
    3.96       in
    3.97          (translator (eqs,les,lts) proof, Cert proof)
    3.98 @@ -1426,12 +1424,12 @@
    3.99                else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs))
   3.100  in () end
   3.101  
   3.102 -fun core_sos_tac print_certs prover ctxt = CSUBGOAL (fn (ct, i) => 
   3.103 +fun core_sos_tac print_cert prover ctxt = CSUBGOAL (fn (ct, i) => 
   3.104    let val _ = check_sos known_sos_constants ct
   3.105        val (avs, p) = strip_all ct
   3.106        val (ths, certificates) = real_sos prover ctxt (Thm.dest_arg p)
   3.107        val th = standard (fold_rev forall_intr avs ths)
   3.108 -      val _ = print_certs certificates
   3.109 +      val _ = print_cert certificates
   3.110    in rtac th i end);
   3.111  
   3.112  fun default_SOME f NONE v = SOME v
   3.113 @@ -1469,7 +1467,7 @@
   3.114  
   3.115  fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
   3.116  
   3.117 -fun sos_tac print_certs prover ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac print_certs prover ctxt
   3.118 +fun sos_tac print_cert prover ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac print_cert prover ctxt
   3.119  
   3.120  
   3.121  end;
     4.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Sep 21 15:05:26 2009 +0200
     4.2 +++ b/src/HOL/Library/positivstellensatz.ML	Tue Sep 22 11:26:46 2009 +0200
     4.3 @@ -146,19 +146,19 @@
     4.4  type cert_conv = cterm -> thm * pss_tree
     4.5  
     4.6  val gen_gen_real_arith :
     4.7 -  Proof.context -> (Rat.rat -> Thm.cterm) * conv * conv * conv *
     4.8 +  Proof.context -> (Rat.rat -> cterm) * conv * conv * conv *
     4.9     conv * conv * conv * conv * conv * conv * prover -> cert_conv
    4.10  val real_linear_prover : (thm list * thm list * thm list -> positivstellensatz -> thm) ->
    4.11    thm list * thm list * thm list -> thm * pss_tree
    4.12  
    4.13  val gen_real_arith : Proof.context ->
    4.14 -  (Rat.rat -> Thm.cterm) * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv
    4.15 +  (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv
    4.16  
    4.17  val gen_prover_real_arith : Proof.context -> prover -> cert_conv
    4.18  
    4.19 -val is_ratconst : Thm.cterm -> bool
    4.20 -val dest_ratconst : Thm.cterm -> Rat.rat
    4.21 -val cterm_of_rat : Rat.rat -> Thm.cterm
    4.22 +val is_ratconst : cterm -> bool
    4.23 +val dest_ratconst : cterm -> Rat.rat
    4.24 +val cterm_of_rat : Rat.rat -> cterm
    4.25  
    4.26  end
    4.27