src/HOL/Multivariate_Analysis/normarith.ML
author wenzelm
Fri, 26 Nov 2010 20:52:21 +0100
changeset 40718 4d7211968607
parent 39032 548e933b90ad
child 40721 e5089e903e39
permissions -rw-r--r--
eliminated some clones of eq_list;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37744
3daaf23b9ab4 tuned titles
haftmann
parents: 36945
diff changeset
     1
(*  Title:      HOL/Multivariate_Analysis/normarith.ML
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
     2
    Author:     Amine Chaieb, University of Cambridge
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
     3
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
     4
Simple decision procedure for linear problems in Euclidean space.
31118
541d43bee678 Isolated decision procedure for noms and the general arithmetic solver
chaieb
parents: 30868
diff changeset
     5
*)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
     6
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
     7
signature NORM_ARITH =
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
     8
sig
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
     9
 val norm_arith : Proof.context -> conv
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    10
 val norm_arith_tac : Proof.context -> int -> tactic
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    11
end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    12
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    13
structure NormArith : NORM_ARITH =
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    14
struct
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    15
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    16
 open Conv;
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    17
 val bool_eq = op = : bool *bool -> bool
30868
1040425c86a2 fixed usage of rational constants
chaieb
parents: 30373
diff changeset
    18
  fun dest_ratconst t = case term_of t of
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    19
   Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
30868
1040425c86a2 fixed usage of rational constants
chaieb
parents: 30373
diff changeset
    20
 | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    21
 | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    22
 fun is_ratconst t = can dest_ratconst t
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    23
 fun augment_norm b t acc = case term_of t of
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    24
     Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    25
   | _ => acc
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    26
 fun find_normedterms t acc = case term_of t of
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    27
    @{term "op + :: real => _"}$_$_ =>
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    28
            find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    29
      | @{term "op * :: real => _"}$_$n =>
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    30
            if not (is_ratconst (Thm.dest_arg1 t)) then acc else
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    31
            augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero)
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    32
                      (Thm.dest_arg t) acc
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    33
      | _ => augment_norm true t acc
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    34
39032
548e933b90ad Table.map replaces Table.map'
haftmann
parents: 37744
diff changeset
    35
 val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    36
 fun cterm_lincomb_cmul c t =
39032
548e933b90ad Table.map replaces Table.map'
haftmann
parents: 37744
diff changeset
    37
    if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x */ c) t
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    38
 fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    39
 fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    40
 fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    41
39032
548e933b90ad Table.map replaces Table.map'
haftmann
parents: 37744
diff changeset
    42
 val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    43
 fun int_lincomb_cmul c t =
39032
548e933b90ad Table.map replaces Table.map'
haftmann
parents: 37744
diff changeset
    44
    if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x */ c) t
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    45
 fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    46
 fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    47
 fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    48
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    49
fun vector_lincomb t = case term_of t of
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
    50
   Const(@{const_name plus}, _) $ _ $ _ =>
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    51
    cterm_lincomb_add (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t))
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
    52
 | Const(@{const_name minus}, _) $ _ $ _ =>
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    53
    cterm_lincomb_sub (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t))
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
    54
 | Const(@{const_name scaleR}, _)$_$_ =>
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    55
    cterm_lincomb_cmul (dest_ratconst (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t))
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
    56
 | Const(@{const_name uminus}, _)$_ =>
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    57
     cterm_lincomb_neg (vector_lincomb (Thm.dest_arg t))
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
    58
(* FIXME: how should we handle numerals?
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    59
 | Const(@ {const_name vec},_)$_ =>
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    60
   let
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    61
     val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    62
               handle TERM _=> false)
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    63
   in if b then FuncUtil.Ctermfunc.onefunc (t,Rat.one)
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    64
      else FuncUtil.Ctermfunc.empty
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    65
   end
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
    66
*)
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    67
 | _ => FuncUtil.Ctermfunc.onefunc (t,Rat.one)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    68
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    69
 fun vector_lincombs ts =
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    70
  fold_rev
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    71
   (fn t => fn fns => case AList.lookup (op aconvc) fns t of
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    72
     NONE =>
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    73
       let val f = vector_lincomb t
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    74
       in case find_first (fn (_,f') => cterm_lincomb_eq f f') fns of
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    75
           SOME (_,f') => (t,f') :: fns
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    76
         | NONE => (t,f) :: fns
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    77
       end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    78
   | SOME _ => fns) ts []
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    79
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    80
fun replacenegnorms cv t = case term_of t of
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    81
  @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    82
| @{term "op * :: real => _"}$_$_ =>
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36939
diff changeset
    83
    if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive t
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36939
diff changeset
    84
| _ => Thm.reflexive t
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    85
fun flip v eq =
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    86
  if FuncUtil.Ctermfunc.defined eq v
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    87
  then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    88
fun allsubsets s = case s of
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    89
  [] => [[]]
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    90
|(a::t) => let val res = allsubsets t in
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    91
               map (cons a) res @ res end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    92
fun evaluate env lin =
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    93
 FuncUtil.Intfunc.fold (fn (x,c) => fn s => s +/ c */ (FuncUtil.Intfunc.apply env x))
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    94
   lin Rat.zero
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    95
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
    96
fun solve (vs,eqs) = case (vs,eqs) of
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    97
  ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,Rat.one))
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
    98
 |(_,eq::oeqs) =>
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
    99
   (case filter (member (op =) vs) (FuncUtil.Intfunc.dom eq) of (*FIXME use find_first here*)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   100
     [] => NONE
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   101
    | v::_ =>
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   102
       if FuncUtil.Intfunc.defined eq v
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   103
       then
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   104
        let
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   105
         val c = FuncUtil.Intfunc.apply eq v
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   106
         val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   107
         fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   108
                             else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 33039
diff changeset
   109
        in (case solve (remove (op =) v vs, map eliminate oeqs) of
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   110
            NONE => NONE
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   111
          | SOME soln => SOME (FuncUtil.Intfunc.update (v, evaluate soln (FuncUtil.Intfunc.delete_safe v vdef)) soln))
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   112
        end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   113
       else NONE)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   114
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   115
fun combinations k l = if k = 0 then [[]] else
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   116
 case l of
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   117
  [] => []
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   118
| h::t => map (cons h) (combinations (k - 1) t) @ combinations k t
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   119
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   120
fun vertices vs eqs =
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   121
 let
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   122
  fun vertex cmb = case solve(vs,cmb) of
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   123
    NONE => NONE
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   124
   | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   125
  val rawvs = map_filter vertex (combinations (length vs) eqs)
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   126
  val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs
40718
4d7211968607 eliminated some clones of eq_list;
wenzelm
parents: 39032
diff changeset
   127
 in fold_rev (insert (eq_list op =/)) unset []
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   128
 end
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   129
40718
4d7211968607 eliminated some clones of eq_list;
wenzelm
parents: 39032
diff changeset
   130
val subsumes = eq_list (fn (x, y) => Rat.abs x <=/ Rat.abs y)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   131
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   132
fun subsume todo dun = case todo of
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   133
 [] => dun
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   134
|v::ovs =>
40718
4d7211968607 eliminated some clones of eq_list;
wenzelm
parents: 39032
diff changeset
   135
   let val dun' = if exists (fn w => subsumes (w, v)) dun then dun
4d7211968607 eliminated some clones of eq_list;
wenzelm
parents: 39032
diff changeset
   136
                  else v:: filter (fn w => not (subsumes (v, w))) dun
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   137
   in subsume ovs dun'
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   138
   end;
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   139
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   140
fun match_mp PQ P = P RS PQ;
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   141
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   142
fun cterm_of_rat x =
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   143
let val (a, b) = Rat.quotient_of_rat x
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   144
in
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   145
 if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   146
  else Thm.capply (Thm.capply @{cterm "op / :: real => _"}
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   147
                   (Numeral.mk_cnumber @{ctyp "real"} a))
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   148
        (Numeral.mk_cnumber @{ctyp "real"} b)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   149
end;
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   150
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   151
fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   152
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   153
fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm};
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   154
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   155
  (* I think here the static context should be sufficient!! *)
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   156
fun inequality_canon_rule ctxt =
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   157
 let
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   158
  (* FIXME : Should be computed statically!! *)
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   159
  val real_poly_conv =
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36751
diff changeset
   160
    Semiring_Normalizer.semiring_normalize_wrapper ctxt
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36751
diff changeset
   161
     (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36721
diff changeset
   162
 in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Numeral_Simprocs.field_comp_conv then_conv real_poly_conv)))
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   163
end;
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   164
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   165
 val apply_pth1 = rewr_conv @{thm pth_1};
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   166
 val apply_pth2 = rewr_conv @{thm pth_2};
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   167
 val apply_pth3 = rewr_conv @{thm pth_3};
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   168
 val apply_pth4 = rewrs_conv @{thms pth_4};
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   169
 val apply_pth5 = rewr_conv @{thm pth_5};
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   170
 val apply_pth6 = rewr_conv @{thm pth_6};
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   171
 val apply_pth7 = rewrs_conv @{thms pth_7};
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36721
diff changeset
   172
 val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Numeral_Simprocs.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left})));
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36721
diff changeset
   173
 val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Numeral_Simprocs.field_comp_conv);
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   174
 val apply_ptha = rewr_conv @{thm pth_a};
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   175
 val apply_pthb = rewrs_conv @{thms pth_b};
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   176
 val apply_pthc = rewrs_conv @{thms pth_c};
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   177
 val apply_pthd = try_conv (rewr_conv @{thm pth_d});
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   178
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   179
fun headvector t = case t of
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
   180
  Const(@{const_name plus}, _)$
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
   181
   (Const(@{const_name scaleR}, _)$l$v)$r => v
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
   182
 | Const(@{const_name scaleR}, _)$l$v => v
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   183
 | _ => error "headvector: non-canonical term"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   184
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   185
fun vector_cmul_conv ct =
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36721
diff changeset
   186
   ((apply_pth5 then_conv arg1_conv Numeral_Simprocs.field_comp_conv) else_conv
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   187
    (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   188
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   189
fun vector_add_conv ct = apply_pth7 ct
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   190
 handle CTERM _ =>
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   191
  (apply_pth8 ct
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   192
   handle CTERM _ =>
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   193
    (case term_of ct of
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   194
     Const(@{const_name plus},_)$lt$rt =>
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   195
      let
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   196
       val l = headvector lt
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   197
       val r = headvector rt
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 33043
diff changeset
   198
      in (case Term_Ord.fast_term_ord (l,r) of
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   199
         LESS => (apply_pthb then_conv arg_conv vector_add_conv
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   200
                  then_conv apply_pthd) ct
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   201
        | GREATER => (apply_pthc then_conv arg_conv vector_add_conv
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   202
                     then_conv apply_pthd) ct
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   203
        | EQUAL => (apply_pth9 then_conv
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   204
                ((apply_ptha then_conv vector_add_conv) else_conv
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   205
              arg_conv vector_add_conv then_conv apply_pthd)) ct)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   206
      end
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36939
diff changeset
   207
     | _ => Thm.reflexive ct))
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   208
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   209
fun vector_canon_conv ct = case term_of ct of
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   210
 Const(@{const_name plus},_)$_$_ =>
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   211
  let
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   212
   val ((p,l),r) = Thm.dest_comb ct |>> Thm.dest_comb
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   213
   val lth = vector_canon_conv l
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   214
   val rth = vector_canon_conv r
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   215
   val th = Drule.binop_cong_rule p lth rth
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   216
  in fconv_rule (arg_conv vector_add_conv) th end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   217
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
   218
| Const(@{const_name scaleR}, _)$_$_ =>
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   219
  let
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   220
   val (p,r) = Thm.dest_comb ct
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   221
   val rth = Drule.arg_cong_rule p (vector_canon_conv r)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   222
  in fconv_rule (arg_conv (apply_pth4 else_conv vector_cmul_conv)) rth
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   223
  end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   224
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   225
| Const(@{const_name minus},_)$_$_ => (apply_pth2 then_conv vector_canon_conv) ct
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   226
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   227
| Const(@{const_name uminus},_)$_ => (apply_pth3 then_conv vector_canon_conv) ct
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   228
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
   229
(* FIXME
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   230
| Const(@{const_name vec},_)$n =>
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   231
  let val n = Thm.dest_arg ct
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   232
  in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36939
diff changeset
   233
     then Thm.reflexive ct else apply_pth1 ct
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   234
  end
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
   235
*)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   236
| _ => apply_pth1 ct
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   237
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   238
fun norm_canon_conv ct = case term_of ct of
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   239
  Const(@{const_name norm},_)$_ => arg_conv vector_canon_conv ct
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   240
 | _ => raise CTERM ("norm_canon_conv", [ct])
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   241
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   242
fun fold_rev2 f [] [] z = z
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   243
 | fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   244
 | fold_rev2 f _ _ _ = raise UnequalLengths;
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   245
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   246
fun int_flip v eq =
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   247
  if FuncUtil.Intfunc.defined eq v
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   248
  then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   249
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   250
local
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
   251
 val pth_zero = @{thm norm_zero}
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   252
 val tv_n = (ctyp_of_term o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o cprop_of)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   253
             pth_zero
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   254
 val concl = Thm.dest_arg o cprop_of
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   255
 fun real_vector_combo_prover ctxt translator (nubs,ges,gts) =
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   256
  let
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   257
   (* FIXME: Should be computed statically!!*)
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   258
   val real_poly_conv =
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36751
diff changeset
   259
      Semiring_Normalizer.semiring_normalize_wrapper ctxt
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36751
diff changeset
   260
       (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   261
   val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   262
   val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) []
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   263
   val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check"
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   264
           else ()
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   265
   val dests = distinct (op aconvc) (map snd rawdests)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   266
   val srcfuns = map vector_lincomb sources
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   267
   val destfuns = map vector_lincomb dests
33042
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33039
diff changeset
   268
   val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   269
   val n = length srcfuns
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   270
   val nvs = 1 upto n
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   271
   val srccombs = srcfuns ~~ nvs
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   272
   fun consider d =
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   273
    let
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   274
     fun coefficients x =
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   275
      let
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   276
       val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x))
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   277
                      else FuncUtil.Intfunc.empty
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   278
      in fold_rev (fn (f,v) => fn g => if FuncUtil.Ctermfunc.defined f x then FuncUtil.Intfunc.update (v, FuncUtil.Ctermfunc.apply f x) g else g) srccombs inp
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   279
      end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   280
     val equations = map coefficients vvs
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   281
     val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,Rat.one)) nvs
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   282
     fun plausiblevertices f =
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   283
      let
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   284
       val flippedequations = map (fold_rev int_flip f) equations
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   285
       val constraints = flippedequations @ inequalities
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   286
       val rawverts = vertices nvs constraints
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   287
       fun check_solution v =
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   288
        let
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   289
          val f = fold_rev2 (curry FuncUtil.Intfunc.update) nvs v (FuncUtil.Intfunc.onefunc (0, Rat.one))
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   290
        in forall (fn e => evaluate f e =/ Rat.zero) flippedequations
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   291
        end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   292
       val goodverts = filter check_solution rawverts
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   293
       val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   294
      in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   295
      end
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   296
     val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) []
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   297
    in subsume allverts []
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   298
    end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   299
   fun compute_ineq v =
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   300
    let
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   301
     val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   302
                                     else SOME(norm_cmul_rule v t))
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   303
                            (v ~~ nubs)
32402
5731300da417 added further conversions and conversionals
boehmes
parents: 31446
diff changeset
   304
     fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   305
    in inequality_canon_rule ctxt (end_itlist norm_add_rule ths)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   306
    end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   307
   val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   308
                 map (inequality_canon_rule ctxt) nubs @ ges
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   309
   val zerodests = filter
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   310
        (fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   311
32645
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32402
diff changeset
   312
  in fst (RealArith.real_linear_prover translator
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
   313
        (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   314
            zerodests,
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36753
diff changeset
   315
        map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   316
                       arg_conv (arg_conv real_poly_conv))) ges',
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   317
        map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
32645
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32402
diff changeset
   318
                       arg_conv (arg_conv real_poly_conv))) gts))
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   319
  end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   320
in val real_vector_combo_prover = real_vector_combo_prover
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   321
end;
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   322
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   323
local
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   324
 val pth = @{thm norm_imp_pos_and_ge}
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   325
 val norm_mp = match_mp pth
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   326
 val concl = Thm.dest_arg o cprop_of
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   327
 fun conjunct1 th = th RS @{thm conjunct1}
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   328
 fun conjunct2 th = th RS @{thm conjunct2}
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   329
fun real_vector_ineq_prover ctxt translator (ges,gts) =
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   330
 let
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   331
(*   val _ = error "real_vector_ineq_prover: pause" *)
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   332
  val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) []
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   333
  val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   334
  val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
32402
5731300da417 added further conversions and conversionals
boehmes
parents: 31446
diff changeset
   335
  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   336
  fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   337
  fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36939
diff changeset
   338
  val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   339
  val replace_conv = try_conv (rewrs_conv asl)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   340
  val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   341
  val ges' =
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   342
       fold_rev (fn th => fn ths => conjunct1(norm_mp th)::ths)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   343
              asl (map replace_rule ges)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   344
  val gts' = map replace_rule gts
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   345
  val nubs = map (conjunct2 o norm_mp) asl
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   346
  val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   347
  val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36939
diff changeset
   348
  val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   349
  val cps = map (swap o Thm.dest_equals) (cprems_of th11)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   350
  val th12 = instantiate ([], cps) th11
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36939
diff changeset
   351
  val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   352
 in hd (Variable.export ctxt' ctxt [th13])
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   353
 end
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   354
in val real_vector_ineq_prover = real_vector_ineq_prover
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   355
end;
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   356
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   357
local
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   358
 val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0}))
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   359
 fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 33043
diff changeset
   360
 fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   361
  (* FIXME: Lookup in the context every time!!! Fix this !!!*)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   362
 fun splitequation ctxt th acc =
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   363
  let
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   364
   val real_poly_neg_conv = #neg
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36751
diff changeset
   365
       (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36751
diff changeset
   366
        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   367
   val (th1,th2) = conj_pair(rawrule th)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   368
  in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   369
  end
32645
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32402
diff changeset
   370
in fun real_vector_prover ctxt _ translator (eqs,ges,gts) =
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32402
diff changeset
   371
     (real_vector_ineq_prover ctxt translator
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32402
diff changeset
   372
         (fold_rev (splitequation ctxt) eqs ges,gts), RealArith.Trivial)
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   373
end;
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   374
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   375
  fun init_conv ctxt =
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   376
   Simplifier.rewrite (Simplifier.context ctxt
36587
534418d8d494 remove redundant lemma vector_dist_norm
huffman
parents: 35625
diff changeset
   377
     (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   378
   then_conv Numeral_Simprocs.field_comp_conv
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   379
   then_conv nnf_conv
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   380
32645
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32402
diff changeset
   381
 fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt);
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   382
 fun norm_arith ctxt ct =
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   383
  let
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   384
   val ctxt' = Variable.declare_term (term_of ct) ctxt
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   385
   val th = init_conv ctxt' ct
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36939
diff changeset
   386
  in Thm.equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (Thm.symmetric th))
32832
4602cb6ae0b5 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents: 32645
diff changeset
   387
                (pure ctxt' (Thm.rhs_of th))
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   388
 end
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   389
36938
278029c8a462 tuned header;
wenzelm
parents: 36937
diff changeset
   390
 fun norm_arith_tac ctxt =
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   391
   clarify_tac HOL_cs THEN'
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35408
diff changeset
   392
   Object_Logic.full_atomize_tac THEN'
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   393
   CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff changeset
   394
31445
c8a474a919a7 generalize norm method to work over class real_normed_vector
huffman
parents: 31344
diff changeset
   395
end;