src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
author Philipp Meyer
Mon, 21 Sep 2009 15:05:26 +0200
changeset 32645 1cc5b24f5a01
child 32646 962b4354ed90
permissions -rw-r--r--
sos method generates and uses proof certificates
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32645
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
     1
(* Title:      positivstellensatz_tools.ML
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
     2
   Author:     Philipp Meyer, TU Muenchen
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
     3
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
     4
Functions for generating a certificate from a positivstellensatz and vice versa
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
     5
*)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
     6
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
     7
signature POSITIVSTELLENSATZ_TOOLS =
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
     8
sig
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
     9
  val pss_tree_to_cert : RealArith.pss_tree -> string
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    10
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    11
  val cert_to_pss_tree : Proof.context -> string -> RealArith.pss_tree
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    12
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    13
end
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    14
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    15
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    16
structure PositivstellensatzTools : POSITIVSTELLENSATZ_TOOLS =
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    17
struct
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    18
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    19
open RealArith FuncUtil
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    20
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    21
(*** certificate generation ***)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    22
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    23
fun string_of_rat r =
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    24
  let
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    25
    val (nom, den) = Rat.quotient_of_rat r
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    26
  in
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    27
    if den = 1 then string_of_int nom
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    28
    else string_of_int nom ^ "/" ^ string_of_int den
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    29
  end
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    30
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    31
(* map polynomials to strings *)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    32
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    33
fun string_of_varpow x k =
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    34
  let
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    35
    val term = term_of x
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    36
    val name = case term of
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    37
      Free (n, _) => n
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    38
    | _ => error "Term in monomial not free variable"
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    39
  in
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    40
    if k = 1 then name else name ^ "^" ^ string_of_int k 
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    41
  end
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    42
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    43
fun string_of_monomial m = 
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    44
 if Ctermfunc.is_undefined m then "1" 
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    45
 else 
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    46
  let 
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    47
   val m' = dest_monomial m
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    48
   val vps = fold_rev (fn (x,k) => cons (string_of_varpow x k)) m' [] 
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    49
  in foldr1 (fn (s, t) => s ^ "*" ^ t) vps
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    50
  end
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    51
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    52
fun string_of_cmonomial (m,c) =
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    53
  if Ctermfunc.is_undefined m then string_of_rat c
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    54
  else if c = Rat.one then string_of_monomial m
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    55
  else (string_of_rat c) ^ "*" ^ (string_of_monomial m);
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    56
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    57
fun string_of_poly p = 
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    58
 if Monomialfunc.is_undefined p then "0" 
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    59
 else
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    60
  let 
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    61
   val cms = map string_of_cmonomial
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    62
     (sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p))
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    63
  in foldr1 (fn (t1, t2) => t1 ^ " + " ^ t2) cms
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    64
  end;
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    65
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    66
fun pss_to_cert (Axiom_eq i) = "A=" ^ string_of_int i
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    67
  | pss_to_cert (Axiom_le i) = "A<=" ^ string_of_int i
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    68
  | pss_to_cert (Axiom_lt i) = "A<" ^ string_of_int i
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    69
  | pss_to_cert (Rational_eq r) = "R=" ^ string_of_rat r
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    70
  | pss_to_cert (Rational_le r) = "R<=" ^ string_of_rat r
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    71
  | pss_to_cert (Rational_lt r) = "R<" ^ string_of_rat r
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    72
  | pss_to_cert (Square p) = "[" ^ string_of_poly p ^ "]^2"
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    73
  | pss_to_cert (Eqmul (p, pss)) = "([" ^ string_of_poly p ^ "] * " ^ pss_to_cert pss ^ ")"
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    74
  | pss_to_cert (Sum (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " + " ^ pss_to_cert pss2 ^ ")"
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    75
  | pss_to_cert (Product (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " * " ^ pss_to_cert pss2 ^ ")"
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    76
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    77
fun pss_tree_to_cert Trivial = "()"
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    78
  | pss_tree_to_cert (Cert pss) = "(" ^ pss_to_cert pss ^ ")"
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    79
  | pss_tree_to_cert (Branch (t1, t2)) = "(" ^ pss_tree_to_cert t1 ^ " & " ^ pss_tree_to_cert t2 ^ ")"
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    80
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    81
(*** certificate parsing ***)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    82
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    83
(* basic parser *)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    84
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    85
fun $$ k = Scan.this_string k
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    86
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    87
val number = Scan.repeat1 (Scan.one Symbol.is_ascii_digit >>
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    88
  (fn s => ord s - ord "0")) >>
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    89
  foldl1 (fn (n, d) => n * 10 + d)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    90
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    91
val nat = number
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    92
val int = Scan.optional ($$ "~" >> K ~1) 1 -- nat >> op *;
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    93
val rat = int --| $$ "/" -- int >> Rat.rat_of_quotient
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    94
val rat_int = rat || int >> Rat.rat_of_int
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    95
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    96
(* polynomial parser *)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    97
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    98
fun repeat_sep s f = f ::: Scan.repeat ($$ s |-- f)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
    99
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   100
val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   101
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   102
fun parse_varpow ctxt = parse_id -- Scan.optional ($$ "^" |-- nat) 1 >>
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   103
  (fn (x, k) => (cterm_of (Context.theory_of_proof ctxt) (Free (x, @{typ real})), k)) 
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   104
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   105
fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   106
  foldl (uncurry Ctermfunc.update) Ctermfunc.undefined
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   107
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   108
fun parse_cmonomial ctxt =
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   109
  rat_int --| $$ "*" -- (parse_monomial ctxt) >> swap ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   110
  (parse_monomial ctxt) >> (fn m => (m, Rat.one)) ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   111
  rat_int >> (fn r => (Ctermfunc.undefined, r))
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   112
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   113
fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   114
  foldl (uncurry Monomialfunc.update) Monomialfunc.undefined
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   115
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   116
(* positivstellensatz parser *)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   117
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   118
val parse_axiom =
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   119
  ($$ "A=" |-- int >> Axiom_eq) ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   120
  ($$ "A<=" |-- int >> Axiom_le) ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   121
  ($$ "A<" |-- int >> Axiom_lt)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   122
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   123
val parse_rational =
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   124
  ($$ "R=" |-- rat_int >> Rational_eq) ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   125
  ($$ "R<=" |-- rat_int >> Rational_le) ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   126
  ($$ "R<" |-- rat_int >> Rational_lt)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   127
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   128
fun parse_cert ctxt input =
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   129
  let
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   130
    val pc = parse_cert ctxt
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   131
    val pp = parse_poly ctxt
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   132
  in
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   133
  (parse_axiom ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   134
   parse_rational ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   135
   $$ "[" |-- pp --| $$ "]^2" >> Square ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   136
   $$ "([" |-- pp --| $$ "]*" -- pc --| $$ ")" >> Eqmul ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   137
   $$ "(" |-- pc --| $$ "*" -- pc --| $$ ")" >> Product ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   138
   $$ "(" |-- pc --| $$ "+" -- pc --| $$ ")" >> Sum) input
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   139
  end
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   140
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   141
fun parse_cert_tree ctxt input =
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   142
  let
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   143
    val pc = parse_cert ctxt
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   144
    val pt = parse_cert_tree ctxt
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   145
  in
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   146
  ($$ "()" >> K Trivial ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   147
   $$ "(" |-- pc --| $$ ")" >> Cert ||
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   148
   $$ "(" |-- pt --| $$ "&" -- pt --| $$ ")" >> Branch) input
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   149
  end
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   150
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   151
(* scanner *)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   152
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   153
fun cert_to_pss_tree ctxt str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   154
  (filter_out Symbol.is_blank (Symbol.explode str))
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   155
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   156
end
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   157
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents:
diff changeset
   158