author  chaieb 
Tue, 12 May 2009 17:32:50 +0100  
changeset 31120  fc654c95c29e 
child 31971  8c1b845ed105 
permissions  rwrr 
31120
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

1 
(* Title: Library/positivstellensatz 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

2 
Author: Amine Chaieb, University of Cambridge 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

3 
Description: A generic arithmetic prover based on Positivstellensatz certificates  
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

4 
also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination. 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

5 
*) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

6 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

7 
(* A functor for finite mappings based on Tables *) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

8 
signature FUNC = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

9 
sig 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

10 
type 'a T 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

11 
type key 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

12 
val apply : 'a T > key > 'a 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

13 
val applyd :'a T > (key > 'a) > key > 'a 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

14 
val combine : ('a > 'a > 'a) > ('a > bool) > 'a T > 'a T > 'a T 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

15 
val defined : 'a T > key > bool 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

16 
val dom : 'a T > key list 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

17 
val fold : (key * 'a > 'b > 'b) > 'a T > 'b > 'b 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

18 
val fold_rev : (key * 'a > 'b > 'b) > 'a T > 'b > 'b 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

19 
val graph : 'a T > (key * 'a) list 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

20 
val is_undefined : 'a T > bool 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

21 
val mapf : ('a > 'b) > 'a T > 'b T 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

22 
val tryapplyd : 'a T > key > 'a > 'a 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

23 
val undefine : key > 'a T > 'a T 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

24 
val undefined : 'a T 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

25 
val update : key * 'a > 'a T > 'a T 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

26 
val updatep : (key * 'a > bool) > key * 'a > 'a T > 'a T 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

27 
val choose : 'a T > key * 'a 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

28 
val onefunc : key * 'a > 'a T 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

29 
val get_first: (key*'a > 'a option) > 'a T > 'a option 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

30 
end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

31 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

32 
functor FuncFun(Key: KEY) : FUNC= 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

33 
struct 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

34 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

35 
type key = Key.key; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

36 
structure Tab = TableFun(Key); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

37 
type 'a T = 'a Tab.table; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

38 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

39 
val undefined = Tab.empty; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

40 
val is_undefined = Tab.is_empty; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

41 
val mapf = Tab.map; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

42 
val fold = Tab.fold; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

43 
val fold_rev = Tab.fold_rev; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

44 
val graph = Tab.dest; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

45 
fun dom a = sort Key.ord (Tab.keys a); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

46 
fun applyd f d x = case Tab.lookup f x of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

47 
SOME y => y 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

48 
 NONE => d x; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

49 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

50 
fun apply f x = applyd f (fn _ => raise Tab.UNDEF x) x; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

51 
fun tryapplyd f a d = applyd f (K d) a; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

52 
val defined = Tab.defined; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

53 
fun undefine x t = (Tab.delete x t handle UNDEF => t); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

54 
val update = Tab.update; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

55 
fun updatep p (k,v) t = if p (k, v) then t else update (k,v) t 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

56 
fun combine f z a b = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

57 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

58 
fun h (k,v) t = case Tab.lookup t k of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

59 
NONE => Tab.update (k,v) t 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

60 
 SOME v' => let val w = f v v' 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

61 
in if z w then Tab.delete k t else Tab.update (k,w) t end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

62 
in Tab.fold h a b end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

63 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

64 
fun choose f = case Tab.min_key f of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

65 
SOME k => (k,valOf (Tab.lookup f k)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

66 
 NONE => error "FuncFun.choose : Completely undefined function" 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

67 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

68 
fun onefunc kv = update kv undefined 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

69 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

70 
local 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

71 
fun find f (k,v) NONE = f (k,v) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

72 
 find f (k,v) r = r 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

73 
in 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

74 
fun get_first f t = fold (find f) t NONE 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

75 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

76 
end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

77 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

78 
structure Intfunc = FuncFun(type key = int val ord = int_ord); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

79 
structure Symfunc = FuncFun(type key = string val ord = fast_string_ord); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

80 
structure Termfunc = FuncFun(type key = term val ord = TermOrd.fast_term_ord); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

81 
structure Ctermfunc = FuncFun(type key = cterm val ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t))); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

82 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

83 
structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

84 
(* Some conversionsrelated stuff which has been forbidden entrance into Pure/conv.ML*) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

85 
structure Conv2 = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

86 
struct 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

87 
open Conv 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

88 
fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

89 
fun is_comb t = case (term_of t) of _$_ => true  _ => false; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

90 
fun is_abs t = case (term_of t) of Abs _ => true  _ => false; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

91 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

92 
fun end_itlist f l = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

93 
case l of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

94 
[] => error "end_itlist" 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

95 
 [x] => x 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

96 
 (h::t) => f h (end_itlist f t); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

97 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

98 
fun absc cv ct = case term_of ct of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

99 
Abs (v,_, _) => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

100 
let val (x,t) = Thm.dest_abs (SOME v) ct 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

101 
in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

102 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

103 
 _ => all_conv ct; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

104 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

105 
fun cache_conv conv = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

106 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

107 
val tab = ref Termtab.empty 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

108 
fun cconv t = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

109 
case Termtab.lookup (!tab) (term_of t) of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

110 
SOME th => th 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

111 
 NONE => let val th = conv t 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

112 
in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

113 
in cconv end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

114 
fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct')) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

115 
handle CTERM _ => false; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

116 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

117 
local 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

118 
fun thenqc conv1 conv2 tm = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

119 
case try conv1 tm of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

120 
SOME th1 => (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2  NONE => th1) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

121 
 NONE => conv2 tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

122 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

123 
fun thencqc conv1 conv2 tm = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

124 
let val th1 = conv1 tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

125 
in (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2  NONE => th1) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

126 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

127 
fun comb_qconv conv tm = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

128 
let val (l,r) = Thm.dest_comb tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

129 
in (case try conv l of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

130 
SOME th1 => (case try conv r of SOME th2 => Thm.combination th1 th2 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

131 
 NONE => Drule.fun_cong_rule th1 r) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

132 
 NONE => Drule.arg_cong_rule l (conv r)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

133 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

134 
fun repeatqc conv tm = thencqc conv (repeatqc conv) tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

135 
fun sub_qconv conv tm = if is_abs tm then absc conv tm else comb_qconv conv tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

136 
fun once_depth_qconv conv tm = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

137 
(conv else_conv (sub_qconv (once_depth_qconv conv))) tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

138 
fun depth_qconv conv tm = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

139 
thenqc (sub_qconv (depth_qconv conv)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

140 
(repeatqc conv) tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

141 
fun redepth_qconv conv tm = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

142 
thenqc (sub_qconv (redepth_qconv conv)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

143 
(thencqc conv (redepth_qconv conv)) tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

144 
fun top_depth_qconv conv tm = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

145 
thenqc (repeatqc conv) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

146 
(thencqc (sub_qconv (top_depth_qconv conv)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

147 
(thencqc conv (top_depth_qconv conv))) tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

148 
fun top_sweep_qconv conv tm = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

149 
thenqc (repeatqc conv) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

150 
(sub_qconv (top_sweep_qconv conv)) tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

151 
in 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

152 
val (once_depth_conv, depth_conv, rdepth_conv, top_depth_conv, top_sweep_conv) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

153 
(fn c => try_conv (once_depth_qconv c), 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

154 
fn c => try_conv (depth_qconv c), 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

155 
fn c => try_conv (redepth_qconv c), 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

156 
fn c => try_conv (top_depth_qconv c), 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

157 
fn c => try_conv (top_sweep_qconv c)); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

158 
end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

159 
end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

160 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

161 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

162 
(* Some useful derived rules *) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

163 
fun deduct_antisym_rule tha thb = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

164 
equal_intr (implies_intr (cprop_of thb) tha) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

165 
(implies_intr (cprop_of tha) thb); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

166 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

167 
fun prove_hyp tha thb = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

168 
if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

169 
then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

170 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

171 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

172 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

173 
signature REAL_ARITH = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

174 
sig 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

175 
datatype positivstellensatz = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

176 
Axiom_eq of int 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

177 
 Axiom_le of int 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

178 
 Axiom_lt of int 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

179 
 Rational_eq of Rat.rat 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

180 
 Rational_le of Rat.rat 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

181 
 Rational_lt of Rat.rat 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

182 
 Square of cterm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

183 
 Eqmul of cterm * positivstellensatz 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

184 
 Sum of positivstellensatz * positivstellensatz 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

185 
 Product of positivstellensatz * positivstellensatz; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

186 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

187 
val gen_gen_real_arith : 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

188 
Proof.context > (Rat.rat > Thm.cterm) * conv * conv * conv * 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

189 
conv * conv * conv * conv * conv * conv * 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

190 
( (thm list * thm list * thm list > positivstellensatz > thm) > 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

191 
thm list * thm list * thm list > thm) > conv 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

192 
val real_linear_prover : 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

193 
(thm list * thm list * thm list > positivstellensatz > thm) > 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

194 
thm list * thm list * thm list > thm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

195 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

196 
val gen_real_arith : Proof.context > 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

197 
(Rat.rat > cterm) * conv * conv * conv * conv * conv * conv * conv * 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

198 
( (thm list * thm list * thm list > positivstellensatz > thm) > 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

199 
thm list * thm list * thm list > thm) > conv 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

200 
val gen_prover_real_arith : Proof.context > 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

201 
((thm list * thm list * thm list > positivstellensatz > thm) > 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

202 
thm list * thm list * thm list > thm) > conv 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

203 
val real_arith : Proof.context > conv 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

204 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

205 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

206 
structure RealArith (* : REAL_ARITH *)= 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

207 
struct 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

208 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

209 
open Conv Thm;; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

210 
(*  *) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

211 
(* Data structure for Positivstellensatz refutations. *) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

212 
(*  *) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

213 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

214 
datatype positivstellensatz = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

215 
Axiom_eq of int 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

216 
 Axiom_le of int 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

217 
 Axiom_lt of int 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

218 
 Rational_eq of Rat.rat 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

219 
 Rational_le of Rat.rat 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

220 
 Rational_lt of Rat.rat 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

221 
 Square of cterm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

222 
 Eqmul of cterm * positivstellensatz 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

223 
 Sum of positivstellensatz * positivstellensatz 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

224 
 Product of positivstellensatz * positivstellensatz; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

225 
(* Theorems used in the procedure *) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

226 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

227 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

228 
val my_eqs = ref ([] : thm list); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

229 
val my_les = ref ([] : thm list); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

230 
val my_lts = ref ([] : thm list); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

231 
val my_proof = ref (Axiom_eq 0); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

232 
val my_context = ref @{context}; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

233 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

234 
val my_mk_numeric = ref ((K @{cterm True}) :Rat.rat > cterm); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

235 
val my_numeric_eq_conv = ref no_conv; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

236 
val my_numeric_ge_conv = ref no_conv; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

237 
val my_numeric_gt_conv = ref no_conv; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

238 
val my_poly_conv = ref no_conv; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

239 
val my_poly_neg_conv = ref no_conv; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

240 
val my_poly_add_conv = ref no_conv; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

241 
val my_poly_mul_conv = ref no_conv; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

242 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

243 
fun conjunctions th = case try Conjunction.elim th of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

244 
SOME (th1,th2) => (conjunctions th1) @ conjunctions th2 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

245 
 NONE => [th]; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

246 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

247 
val pth = @{lemma "(((x::real) < y) == (y  x > 0)) &&& ((x <= y) == (y  x >= 0)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

248 
&&& ((x = y) == (x  y = 0)) &&& ((~(x < y)) == (x  y >= 0)) &&& ((~(x <= y)) == (x  y > 0)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

249 
&&& ((~(x = y)) == (x  y > 0  (x  y) > 0))" 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

250 
by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)} > 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

251 
conjunctions; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

252 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

253 
val pth_final = @{lemma "(~p ==> False) ==> p" by blast} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

254 
val pth_add = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

255 
@{lemma "(x = (0::real) ==> y = 0 ==> x + y = 0 ) &&& ( x = 0 ==> y >= 0 ==> x + y >= 0) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

256 
&&& (x = 0 ==> y > 0 ==> x + y > 0) &&& (x >= 0 ==> y = 0 ==> x + y >= 0) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

257 
&&& (x >= 0 ==> y >= 0 ==> x + y >= 0) &&& (x >= 0 ==> y > 0 ==> x + y > 0) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

258 
&&& (x > 0 ==> y = 0 ==> x + y > 0) &&& (x > 0 ==> y >= 0 ==> x + y > 0) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

259 
&&& (x > 0 ==> y > 0 ==> x + y > 0)" by simp_all} > conjunctions ; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

260 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

261 
val pth_mul = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

262 
@{lemma "(x = (0::real) ==> y = 0 ==> x * y = 0) &&& (x = 0 ==> y >= 0 ==> x * y = 0) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

263 
(x = 0 ==> y > 0 ==> x * y = 0) &&& (x >= 0 ==> y = 0 ==> x * y = 0) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

264 
(x >= 0 ==> y >= 0 ==> x * y >= 0 ) &&& ( x >= 0 ==> y > 0 ==> x * y >= 0 ) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

265 
(x > 0 ==> y = 0 ==> x * y = 0 ) &&& ( x > 0 ==> y >= 0 ==> x * y >= 0 ) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

266 
(x > 0 ==> y > 0 ==> x * y > 0)" 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

267 
by (auto intro: mult_mono[where a="0::real" and b="x" and d="y" and c="0", simplified] 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

268 
mult_strict_mono[where b="x" and d="y" and a="0" and c="0", simplified])} > conjunctions; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

269 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

270 
val pth_emul = @{lemma "y = (0::real) ==> x * y = 0" by simp}; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

271 
val pth_square = @{lemma "x * x >= (0::real)" by simp}; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

272 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

273 
val weak_dnf_simps = List.take (simp_thms, 34) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

274 
@ conjunctions @{lemma "((P & (Q  R)) = ((P&Q)  (P&R))) &&& ((Q  R) & P) = ((Q&P)  (R&P)) &&& (P & Q) = (Q & P) &&& ((P  Q) = (Q  P))" by blast+}; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

275 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

276 
val nnfD_simps = conjunctions @{lemma "((~(P & Q)) = (~P  ~Q)) &&& ((~(P  Q)) = (~P & ~Q) ) &&& ((P > Q) = (~P  Q) ) &&& ((P = Q) = ((P & Q)  (~P & ~ Q))) &&& ((~(P = Q)) = ((P & ~ Q)  (~P & Q)) ) &&& ((~ ~(P)) = P)" by blast+} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

277 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

278 
val choice_iff = @{lemma "(ALL x. EX y. P x y) = (EX f. ALL x. P x (f x))" by metis}; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

279 
val prenex_simps = map (fn th => th RS sym) ([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @ @{thms "all_simps"(14)} @ @{thms "ex_simps"(14)}); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

280 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

281 
val real_abs_thms1 = conjunctions @{lemma 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

282 
"((1 * abs(x::real) >= r) = (1 * x >= r & 1 * x >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

283 
((1 * abs(x) + a >= r) = (a + 1 * x >= r & a + 1 * x >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

284 
((a + 1 * abs(x) >= r) = (a + 1 * x >= r & a + 1 * x >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

285 
((a + 1 * abs(x) + b >= r) = (a + 1 * x + b >= r & a + 1 * x + b >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

286 
((a + b + 1 * abs(x) >= r) = (a + b + 1 * x >= r & a + b + 1 * x >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

287 
((a + b + 1 * abs(x) + c >= r) = (a + b + 1 * x + c >= r & a + b + 1 * x + c >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

288 
((1 * max x y >= r) = (1 * x >= r & 1 * y >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

289 
((1 * max x y + a >= r) = (a + 1 * x >= r & a + 1 * y >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

290 
((a + 1 * max x y >= r) = (a + 1 * x >= r & a + 1 * y >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

291 
((a + 1 * max x y + b >= r) = (a + 1 * x + b >= r & a + 1 * y + b >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

292 
((a + b + 1 * max x y >= r) = (a + b + 1 * x >= r & a + b + 1 * y >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

293 
((a + b + 1 * max x y + c >= r) = (a + b + 1 * x + c >= r & a + b + 1 * y + c >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

294 
((1 * min x y >= r) = (1 * x >= r & 1 * y >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

295 
((1 * min x y + a >= r) = (a + 1 * x >= r & a + 1 * y >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

296 
((a + 1 * min x y >= r) = (a + 1 * x >= r & a + 1 * y >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

297 
((a + 1 * min x y + b >= r) = (a + 1 * x + b >= r & a + 1 * y + b >= r) )&&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

298 
((a + b + 1 * min x y >= r) = (a + b + 1 * x >= r & a + b + 1 * y >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

299 
((a + b + 1 * min x y + c >= r) = (a + b + 1 * x + c >= r & a + b + 1 * y + c >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

300 
((min x y >= r) = (x >= r & y >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

301 
((min x y + a >= r) = (a + x >= r & a + y >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

302 
((a + min x y >= r) = (a + x >= r & a + y >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

303 
((a + min x y + b >= r) = (a + x + b >= r & a + y + b >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

304 
((a + b + min x y >= r) = (a + b + x >= r & a + b + y >= r) )&&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

305 
((a + b + min x y + c >= r) = (a + b + x + c >= r & a + b + y + c >= r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

306 
((1 * abs(x) > r) = (1 * x > r & 1 * x > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

307 
((1 * abs(x) + a > r) = (a + 1 * x > r & a + 1 * x > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

308 
((a + 1 * abs(x) > r) = (a + 1 * x > r & a + 1 * x > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

309 
((a + 1 * abs(x) + b > r) = (a + 1 * x + b > r & a + 1 * x + b > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

310 
((a + b + 1 * abs(x) > r) = (a + b + 1 * x > r & a + b + 1 * x > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

311 
((a + b + 1 * abs(x) + c > r) = (a + b + 1 * x + c > r & a + b + 1 * x + c > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

312 
((1 * max x y > r) = ((1 * x > r) & 1 * y > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

313 
((1 * max x y + a > r) = (a + 1 * x > r & a + 1 * y > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

314 
((a + 1 * max x y > r) = (a + 1 * x > r & a + 1 * y > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

315 
((a + 1 * max x y + b > r) = (a + 1 * x + b > r & a + 1 * y + b > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

316 
((a + b + 1 * max x y > r) = (a + b + 1 * x > r & a + b + 1 * y > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

317 
((a + b + 1 * max x y + c > r) = (a + b + 1 * x + c > r & a + b + 1 * y + c > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

318 
((min x y > r) = (x > r & y > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

319 
((min x y + a > r) = (a + x > r & a + y > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

320 
((a + min x y > r) = (a + x > r & a + y > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

321 
((a + min x y + b > r) = (a + x + b > r & a + y + b > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

322 
((a + b + min x y > r) = (a + b + x > r & a + b + y > r)) &&& 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

323 
((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))" 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

324 
by auto}; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

325 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

326 
val abs_split' = @{lemma "P (abs (x::'a::ordered_idom)) == (x >= 0 & P x  x < 0 & P (x))" 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

327 
by (atomize (full)) (auto split add: abs_split)}; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

328 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

329 
val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y  x > y & P x)" 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

330 
by (atomize (full)) (cases "x <= y", auto simp add: max_def)}; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

331 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

332 
val min_split = @{lemma "P (min x y) == ((x::'a::linorder) <= y & P x  x > y & P y)" 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

333 
by (atomize (full)) (cases "x <= y", auto simp add: min_def)}; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

334 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

335 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

336 
(* Miscalineous *) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

337 
fun literals_conv bops uops cv = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

338 
let fun h t = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

339 
case (term_of t) of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

340 
b$_$_ => if member (op aconv) bops b then binop_conv h t else cv t 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

341 
 u$_ => if member (op aconv) uops u then arg_conv h t else cv t 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

342 
 _ => cv t 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

343 
in h end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

344 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

345 
fun cterm_of_rat x = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

346 
let val (a, b) = Rat.quotient_of_rat x 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

347 
in 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

348 
if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

349 
else Thm.capply (Thm.capply @{cterm "op / :: real => _"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

350 
(Numeral.mk_cnumber @{ctyp "real"} a)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

351 
(Numeral.mk_cnumber @{ctyp "real"} b) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

352 
end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

353 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

354 
fun dest_ratconst t = case term_of t of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

355 
Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a > snd, HOLogic.dest_number b > snd) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

356 
 _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) > snd) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

357 
fun is_ratconst t = can dest_ratconst t 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

358 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

359 
fun find_term p t = if p t then t else 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

360 
case t of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

361 
a$b => (find_term p a handle TERM _ => find_term p b) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

362 
 Abs (_,_,t') => find_term p t' 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

363 
 _ => raise TERM ("find_term",[t]); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

364 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

365 
fun find_cterm p t = if p t then t else 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

366 
case term_of t of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

367 
a$b => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

368 
 Abs (_,_,t') => find_cterm p (Thm.dest_abs NONE t > snd) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

369 
 _ => raise CTERM ("find_cterm",[t]); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

370 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

371 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

372 
(* Some conversionsrelated stuff which has been forbidden entrance into Pure/conv.ML*) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

373 
fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

374 
fun is_comb t = case (term_of t) of _$_ => true  _ => false; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

375 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

376 
fun cache_conv conv = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

377 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

378 
val tab = ref Termtab.empty 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

379 
fun cconv t = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

380 
case Termtab.lookup (!tab) (term_of t) of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

381 
SOME th => th 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

382 
 NONE => let val th = conv t 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

383 
in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

384 
in cconv end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

385 
fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct')) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

386 
handle CTERM _ => false; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

387 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

388 
(* A general real arithmetic prover *) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

389 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

390 
fun gen_gen_real_arith ctxt (mk_numeric, 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

391 
numeric_eq_conv,numeric_ge_conv,numeric_gt_conv, 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

392 
poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv, 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

393 
absconv1,absconv2,prover) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

394 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

395 
open Conv Thm; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

396 
val _ = my_context := ctxt 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

397 
val _ = (my_mk_numeric := mk_numeric ; my_numeric_eq_conv := numeric_eq_conv ; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

398 
my_numeric_ge_conv := numeric_ge_conv; my_numeric_gt_conv := numeric_gt_conv ; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

399 
my_poly_conv := poly_conv; my_poly_neg_conv := poly_neg_conv; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

400 
my_poly_add_conv := poly_add_conv; my_poly_mul_conv := poly_mul_conv) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

401 
val pre_ss = HOL_basic_ss addsimps simp_thms@ ex_simps@ all_simps@[@{thm not_all},@{thm not_ex},ex_disj_distrib, all_conj_distrib, @{thm if_bool_eq_disj}] 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

402 
val prenex_ss = HOL_basic_ss addsimps prenex_simps 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

403 
val skolemize_ss = HOL_basic_ss addsimps [choice_iff] 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

404 
val presimp_conv = Simplifier.rewrite (Simplifier.context ctxt pre_ss) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

405 
val prenex_conv = Simplifier.rewrite (Simplifier.context ctxt prenex_ss) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

406 
val skolemize_conv = Simplifier.rewrite (Simplifier.context ctxt skolemize_ss) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

407 
val weak_dnf_ss = HOL_basic_ss addsimps weak_dnf_simps 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

408 
val weak_dnf_conv = Simplifier.rewrite (Simplifier.context ctxt weak_dnf_ss) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

409 
fun eqT_elim th = equal_elim (symmetric th) @{thm TrueI} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

410 
fun oprconv cv ct = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

411 
let val g = Thm.dest_fun2 ct 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

412 
in if g aconvc @{cterm "op <= :: real => _"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

413 
orelse g aconvc @{cterm "op < :: real => _"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

414 
then arg_conv cv ct else arg1_conv cv ct 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

415 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

416 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

417 
fun real_ineq_conv th ct = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

418 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

419 
val th' = (instantiate (match (lhs_of th, ct)) th 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

420 
handle MATCH => raise CTERM ("real_ineq_conv", [ct])) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

421 
in transitive th' (oprconv poly_conv (Thm.rhs_of th')) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

422 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

423 
val [real_lt_conv, real_le_conv, real_eq_conv, 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

424 
real_not_lt_conv, real_not_le_conv, _] = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

425 
map real_ineq_conv pth 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

426 
fun match_mp_rule ths ths' = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

427 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

428 
fun f ths ths' = case ths of [] => raise THM("match_mp_rule",0,ths) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

429 
 th::ths => (ths' MRS th handle THM _ => f ths ths') 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

430 
in f ths ths' end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

431 
fun mul_rule th th' = fconv_rule (arg_conv (oprconv poly_mul_conv)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

432 
(match_mp_rule pth_mul [th, th']) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

433 
fun add_rule th th' = fconv_rule (arg_conv (oprconv poly_add_conv)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

434 
(match_mp_rule pth_add [th, th']) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

435 
fun emul_rule ct th = fconv_rule (arg_conv (oprconv poly_mul_conv)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

436 
(instantiate' [] [SOME ct] (th RS pth_emul)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

437 
fun square_rule t = fconv_rule (arg_conv (oprconv poly_conv)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

438 
(instantiate' [] [SOME t] pth_square) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

439 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

440 
fun hol_of_positivstellensatz(eqs,les,lts) proof = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

441 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

442 
val _ = (my_eqs := eqs ; my_les := les ; my_lts := lts ; my_proof := proof) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

443 
fun translate prf = case prf of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

444 
Axiom_eq n => nth eqs n 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

445 
 Axiom_le n => nth les n 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

446 
 Axiom_lt n => nth lts n 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

447 
 Rational_eq x => eqT_elim(numeric_eq_conv(capply @{cterm Trueprop} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

448 
(capply (capply @{cterm "op =::real => _"} (mk_numeric x)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

449 
@{cterm "0::real"}))) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

450 
 Rational_le x => eqT_elim(numeric_ge_conv(capply @{cterm Trueprop} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

451 
(capply (capply @{cterm "op <=::real => _"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

452 
@{cterm "0::real"}) (mk_numeric x)))) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

453 
 Rational_lt x => eqT_elim(numeric_gt_conv(capply @{cterm Trueprop} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

454 
(capply (capply @{cterm "op <::real => _"} @{cterm "0::real"}) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

455 
(mk_numeric x)))) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

456 
 Square t => square_rule t 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

457 
 Eqmul(t,p) => emul_rule t (translate p) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

458 
 Sum(p1,p2) => add_rule (translate p1) (translate p2) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

459 
 Product(p1,p2) => mul_rule (translate p1) (translate p2) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

460 
in fconv_rule (first_conv [numeric_ge_conv, numeric_gt_conv, numeric_eq_conv, all_conv]) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

461 
(translate proof) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

462 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

463 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

464 
val init_conv = presimp_conv then_conv 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

465 
nnf_conv then_conv skolemize_conv then_conv prenex_conv then_conv 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

466 
weak_dnf_conv 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

467 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

468 
val concl = dest_arg o cprop_of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

469 
fun is_binop opr ct = (dest_fun2 ct aconvc opr handle CTERM _ => false) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

470 
val is_req = is_binop @{cterm "op =:: real => _"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

471 
val is_ge = is_binop @{cterm "op <=:: real => _"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

472 
val is_gt = is_binop @{cterm "op <:: real => _"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

473 
val is_conj = is_binop @{cterm "op &"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

474 
val is_disj = is_binop @{cterm "op "} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

475 
fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2}) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

476 
fun disj_cases th th1 th2 = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

477 
let val (p,q) = dest_binop (concl th) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

478 
val c = concl th1 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

479 
val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible" 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

480 
in implies_elim (implies_elim (implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th) (implies_intr (capply @{cterm Trueprop} p) th1)) (implies_intr (capply @{cterm Trueprop} q) th2) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

481 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

482 
fun overall dun ths = case ths of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

483 
[] => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

484 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

485 
val (eq,ne) = List.partition (is_req o concl) dun 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

486 
val (le,nl) = List.partition (is_ge o concl) ne 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

487 
val lt = filter (is_gt o concl) nl 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

488 
in prover hol_of_positivstellensatz (eq,le,lt) end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

489 
 th::oths => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

490 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

491 
val ct = concl th 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

492 
in 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

493 
if is_conj ct then 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

494 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

495 
val (th1,th2) = conj_pair th in 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

496 
overall dun (th1::th2::oths) end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

497 
else if is_disj ct then 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

498 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

499 
val th1 = overall dun (assume (capply @{cterm Trueprop} (dest_arg1 ct))::oths) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

500 
val th2 = overall dun (assume (capply @{cterm Trueprop} (dest_arg ct))::oths) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

501 
in disj_cases th th1 th2 end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

502 
else overall (th::dun) oths 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

503 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

504 
fun dest_binary b ct = if is_binop b ct then dest_binop ct 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

505 
else raise CTERM ("dest_binary",[b,ct]) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

506 
val dest_eq = dest_binary @{cterm "op = :: real => _"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

507 
val neq_th = nth pth 5 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

508 
fun real_not_eq_conv ct = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

509 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

510 
val (l,r) = dest_eq (dest_arg ct) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

511 
val th = instantiate ([],[(@{cpat "?x::real"},l),(@{cpat "?y::real"},r)]) neq_th 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

512 
val th_p = poly_conv(dest_arg(dest_arg1(rhs_of th))) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

513 
val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

514 
val th_n = fconv_rule (arg_conv poly_neg_conv) th_x 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

515 
val th' = Drule.binop_cong_rule @{cterm "op "} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

516 
(Drule.arg_cong_rule (capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

517 
(Drule.arg_cong_rule (capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

518 
in transitive th th' 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

519 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

520 
fun equal_implies_1_rule PQ = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

521 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

522 
val P = lhs_of PQ 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

523 
in implies_intr P (equal_elim PQ (assume P)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

524 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

525 
(* FIXME!!! Copied from groebner.ml *) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

526 
val strip_exists = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

527 
let fun h (acc, t) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

528 
case (term_of t) of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

529 
Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) >> (fn v => v::acc)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

530 
 _ => (acc,t) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

531 
in fn t => h ([],t) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

532 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

533 
fun name_of x = case term_of x of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

534 
Free(s,_) => s 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

535 
 Var ((s,_),_) => s 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

536 
 _ => "x" 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

537 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

538 
fun mk_forall x th = Drule.arg_cong_rule (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) (abstract_rule (name_of x) x th) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

539 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

540 
val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec)); 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

541 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

542 
fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

543 
fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

544 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

545 
fun choose v th th' = case concl_of th of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

546 
@{term Trueprop} $ (Const("Ex",_)$_) => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

547 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

548 
val p = (funpow 2 Thm.dest_arg o cprop_of) th 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

549 
val T = (hd o Thm.dest_ctyp o ctyp_of_term) p 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

550 
val th0 = fconv_rule (Thm.beta_conversion true) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

551 
(instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

552 
val pv = (Thm.rhs_of o Thm.beta_conversion true) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

553 
(Thm.capply @{cterm Trueprop} (Thm.capply p v)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

554 
val th1 = forall_intr v (implies_intr pv th') 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

555 
in implies_elim (implies_elim th0 th) th1 end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

556 
 _ => raise THM ("choose",0,[th, th']) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

557 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

558 
fun simple_choose v th = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

559 
choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

560 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

561 
val strip_forall = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

562 
let fun h (acc, t) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

563 
case (term_of t) of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

564 
Const("All",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) >> (fn v => v::acc)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

565 
 _ => (acc,t) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

566 
in fn t => h ([],t) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

567 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

568 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

569 
fun f ct = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

570 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

571 
val nnf_norm_conv' = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

572 
nnf_conv then_conv 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

573 
literals_conv [@{term "op &"}, @{term "op "}] [] 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

574 
(cache_conv 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

575 
(first_conv [real_lt_conv, real_le_conv, 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

576 
real_eq_conv, real_not_lt_conv, 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

577 
real_not_le_conv, real_not_eq_conv, all_conv])) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

578 
fun absremover ct = (literals_conv [@{term "op &"}, @{term "op "}] [] 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

579 
(try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

580 
try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

581 
val nct = capply @{cterm Trueprop} (capply @{cterm "Not"} ct) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

582 
val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

583 
val tm0 = dest_arg (rhs_of th0) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

584 
val th = if tm0 aconvc @{cterm False} then equal_implies_1_rule th0 else 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

585 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

586 
val (evs,bod) = strip_exists tm0 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

587 
val (avs,ibod) = strip_forall bod 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

588 
val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

589 
val th2 = overall [] [specl avs (assume (rhs_of th1))] 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

590 
val th3 = fold simple_choose evs (prove_hyp (equal_elim th1 (assume (capply @{cterm Trueprop} bod))) th2) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

591 
in Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

592 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

593 
in implies_elim (instantiate' [] [SOME ct] pth_final) th 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

594 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

595 
in f 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

596 
end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

597 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

598 
(* A linear arithmetic prover *) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

599 
local 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

600 
val linear_add = Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

601 
fun linear_cmul c = Ctermfunc.mapf (fn x => c */ x) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

602 
val one_tm = @{cterm "1::real"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

603 
fun contradictory p (e,_) = ((Ctermfunc.is_undefined e) andalso not(p Rat.zero)) orelse 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

604 
((gen_eq_set (op aconvc) (Ctermfunc.dom e, [one_tm])) andalso not(p(Ctermfunc.apply e one_tm))) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

605 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

606 
fun linear_ineqs vars (les,lts) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

607 
case find_first (contradictory (fn x => x >/ Rat.zero)) lts of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

608 
SOME r => r 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

609 
 NONE => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

610 
(case find_first (contradictory (fn x => x >/ Rat.zero)) les of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

611 
SOME r => r 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

612 
 NONE => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

613 
if null vars then error "linear_ineqs: no contradiction" else 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

614 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

615 
val ineqs = les @ lts 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

616 
fun blowup v = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

617 
length(filter (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) ineqs) + 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

618 
length(filter (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) ineqs) * 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

619 
length(filter (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero </ Rat.zero) ineqs) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

620 
val v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

621 
(map (fn v => (v,blowup v)) vars))) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

622 
fun addup (e1,p1) (e2,p2) acc = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

623 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

624 
val c1 = Ctermfunc.tryapplyd e1 v Rat.zero 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

625 
val c2 = Ctermfunc.tryapplyd e2 v Rat.zero 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

626 
in if c1 */ c2 >=/ Rat.zero then acc else 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

627 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

628 
val e1' = linear_cmul (Rat.abs c2) e1 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

629 
val e2' = linear_cmul (Rat.abs c1) e2 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

630 
val p1' = Product(Rational_lt(Rat.abs c2),p1) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

631 
val p2' = Product(Rational_lt(Rat.abs c1),p2) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

632 
in (linear_add e1' e2',Sum(p1',p2'))::acc 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

633 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

634 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

635 
val (les0,les1) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

636 
List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) les 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

637 
val (lts0,lts1) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

638 
List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) lts 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

639 
val (lesp,lesn) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

640 
List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) les1 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

641 
val (ltsp,ltsn) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

642 
List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) lts1 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

643 
val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

644 
val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

645 
(fold_rev (fn ep1 => fold_rev (addup ep1) (lesn@ltsn)) ltsp lts0) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

646 
in linear_ineqs (remove (op aconvc) v vars) (les',lts') 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

647 
end) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

648 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

649 
fun linear_eqs(eqs,les,lts) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

650 
case find_first (contradictory (fn x => x =/ Rat.zero)) eqs of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

651 
SOME r => r 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

652 
 NONE => (case eqs of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

653 
[] => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

654 
let val vars = remove (op aconvc) one_tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

655 
(fold_rev (curry (gen_union (op aconvc)) o Ctermfunc.dom o fst) (les@lts) []) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

656 
in linear_ineqs vars (les,lts) end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

657 
 (e,p)::es => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

658 
if Ctermfunc.is_undefined e then linear_eqs (es,les,lts) else 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

659 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

660 
val (x,c) = Ctermfunc.choose (Ctermfunc.undefine one_tm e) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

661 
fun xform (inp as (t,q)) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

662 
let val d = Ctermfunc.tryapplyd t x Rat.zero in 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

663 
if d =/ Rat.zero then inp else 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

664 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

665 
val k = (Rat.neg d) */ Rat.abs c // c 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

666 
val e' = linear_cmul k e 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

667 
val t' = linear_cmul (Rat.abs c) t 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

668 
val p' = Eqmul(cterm_of_rat k,p) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

669 
val q' = Product(Rational_lt(Rat.abs c),q) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

670 
in (linear_add e' t',Sum(p',q')) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

671 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

672 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

673 
in linear_eqs(map xform es,map xform les,map xform lts) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

674 
end) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

675 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

676 
fun linear_prover (eq,le,lt) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

677 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

678 
val eqs = map2 (fn p => fn n => (p,Axiom_eq n)) eq (0 upto (length eq  1)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

679 
val les = map2 (fn p => fn n => (p,Axiom_le n)) le (0 upto (length le  1)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

680 
val lts = map2 (fn p => fn n => (p,Axiom_lt n)) lt (0 upto (length lt  1)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

681 
in linear_eqs(eqs,les,lts) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

682 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

683 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

684 
fun lin_of_hol ct = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

685 
if ct aconvc @{cterm "0::real"} then Ctermfunc.undefined 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

686 
else if not (is_comb ct) then Ctermfunc.onefunc (ct, Rat.one) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

687 
else if is_ratconst ct then Ctermfunc.onefunc (one_tm, dest_ratconst ct) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

688 
else 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

689 
let val (lop,r) = Thm.dest_comb ct 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

690 
in if not (is_comb lop) then Ctermfunc.onefunc (ct, Rat.one) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

691 
else 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

692 
let val (opr,l) = Thm.dest_comb lop 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

693 
in if opr aconvc @{cterm "op + :: real =>_"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

694 
then linear_add (lin_of_hol l) (lin_of_hol r) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

695 
else if opr aconvc @{cterm "op * :: real =>_"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

696 
andalso is_ratconst l then Ctermfunc.onefunc (r, dest_ratconst l) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

697 
else Ctermfunc.onefunc (ct, Rat.one) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

698 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

699 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

700 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

701 
fun is_alien ct = case term_of ct of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

702 
Const(@{const_name "real"}, _)$ n => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

703 
if can HOLogic.dest_number n then false else true 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

704 
 _ => false 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

705 
open Thm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

706 
in 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

707 
fun real_linear_prover translator (eq,le,lt) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

708 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

709 
val lhs = lin_of_hol o dest_arg1 o dest_arg o cprop_of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

710 
val rhs = lin_of_hol o dest_arg o dest_arg o cprop_of 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

711 
val eq_pols = map lhs eq 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

712 
val le_pols = map rhs le 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

713 
val lt_pols = map rhs lt 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

714 
val aliens = filter is_alien 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

715 
(fold_rev (curry (gen_union (op aconvc)) o Ctermfunc.dom) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

716 
(eq_pols @ le_pols @ lt_pols) []) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

717 
val le_pols' = le_pols @ map (fn v => Ctermfunc.onefunc (v,Rat.one)) aliens 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

718 
val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

719 
val le' = le @ map (fn a => instantiate' [] [SOME (dest_arg a)] @{thm real_of_nat_ge_zero}) aliens 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

720 
in (translator (eq,le',lt) proof) : thm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

721 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

722 
end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

723 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

724 
(* A less general generic arithmetic prover dealing with abs,max and min*) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

725 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

726 
local 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

727 
val absmaxmin_elim_ss1 = HOL_basic_ss addsimps real_abs_thms1 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

728 
fun absmaxmin_elim_conv1 ctxt = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

729 
Simplifier.rewrite (Simplifier.context ctxt absmaxmin_elim_ss1) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

730 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

731 
val absmaxmin_elim_conv2 = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

732 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

733 
val pth_abs = instantiate' [SOME @{ctyp real}] [] abs_split' 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

734 
val pth_max = instantiate' [SOME @{ctyp real}] [] max_split 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

735 
val pth_min = instantiate' [SOME @{ctyp real}] [] min_split 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

736 
val abs_tm = @{cterm "abs :: real => _"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

737 
val p_tm = @{cpat "?P :: real => bool"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

738 
val x_tm = @{cpat "?x :: real"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

739 
val y_tm = @{cpat "?y::real"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

740 
val is_max = is_binop @{cterm "max :: real => _"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

741 
val is_min = is_binop @{cterm "min :: real => _"} 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

742 
fun is_abs t = is_comb t andalso dest_fun t aconvc abs_tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

743 
fun eliminate_construct p c tm = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

744 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

745 
val t = find_cterm p tm 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

746 
val th0 = (symmetric o beta_conversion false) (capply (cabs t tm) t) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

747 
val (p,ax) = (dest_comb o rhs_of) th0 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

748 
in fconv_rule(arg_conv(binop_conv (arg_conv (beta_conversion false)))) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

749 
(transitive th0 (c p ax)) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

750 
end 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

751 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

752 
val elim_abs = eliminate_construct is_abs 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

753 
(fn p => fn ax => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

754 
instantiate ([], [(p_tm,p), (x_tm, dest_arg ax)]) pth_abs) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

755 
val elim_max = eliminate_construct is_max 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

756 
(fn p => fn ax => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

757 
let val (ax,y) = dest_comb ax 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

758 
in instantiate ([], [(p_tm,p), (x_tm, dest_arg ax), (y_tm,y)]) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

759 
pth_max end) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

760 
val elim_min = eliminate_construct is_min 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

761 
(fn p => fn ax => 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

762 
let val (ax,y) = dest_comb ax 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

763 
in instantiate ([], [(p_tm,p), (x_tm, dest_arg ax), (y_tm,y)]) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

764 
pth_min end) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

765 
in first_conv [elim_abs, elim_max, elim_min, all_conv] 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

766 
end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

767 
in fun gen_real_arith ctxt (mkconst,eq,ge,gt,norm,neg,add,mul,prover) = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

768 
gen_gen_real_arith ctxt (mkconst,eq,ge,gt,norm,neg,add,mul, 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

769 
absmaxmin_elim_conv1 ctxt,absmaxmin_elim_conv2,prover) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

770 
end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

771 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

772 
(* An instance for reals*) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

773 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

774 
fun gen_prover_real_arith ctxt prover = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

775 
let 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

776 
fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

777 
val {add,mul,neg,pow,sub,main} = 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

778 
Normalizer.semiring_normalizers_ord_wrapper ctxt 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

779 
(valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

780 
simple_cterm_ord 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

781 
in gen_real_arith ctxt 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

782 
(cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv, 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

783 
main,neg,add,mul, prover) 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

784 
end; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

785 

fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

786 
fun real_arith ctxt = gen_prover_real_arith ctxt real_linear_prover; 
fc654c95c29e
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
chaieb
parents:
diff
changeset

787 
end 