author  chaieb 
Mon, 09 Feb 2009 16:43:52 +0000  
changeset 29841  86d94bb79226 
child 29843  4bb780545478 
permissions  rwrr 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1 
(* A functor for finite mappings based on Tables *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

2 
signature FUNC = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

3 
sig 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

4 
type 'a T 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

5 
type key 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

6 
val apply : 'a T > key > 'a 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

7 
val applyd :'a T > (key > 'a) > key > 'a 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

8 
val combine : ('a > 'a > 'a) > ('a > bool) > 'a T > 'a T > 'a T 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

9 
val defined : 'a T > key > bool 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

10 
val dom : 'a T > key list 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

11 
val fold : (key * 'a > 'b > 'b) > 'a T > 'b > 'b 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

12 
val graph : 'a T > (key * 'a) list 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

13 
val is_undefined : 'a T > bool 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

14 
val mapf : ('a > 'b) > 'a T > 'b T 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

15 
val tryapplyd : 'a T > key > 'a > 'a 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

16 
val undefine : key > 'a T > 'a T 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

17 
val undefined : 'a T 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

18 
val update : key * 'a > 'a T > 'a T 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

19 
val updatep : (key * 'a > bool) > key * 'a > 'a T > 'a T 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

20 
val choose : 'a T > key * 'a 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

21 
val onefunc : key * 'a > 'a T 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

22 
val get_first: (key*'a > 'a option) > 'a T > 'a option 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

23 
val fns: 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

24 
{key_ord: key*key > order, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

25 
apply : 'a T > key > 'a, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

26 
applyd :'a T > (key > 'a) > key > 'a, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

27 
combine : ('a > 'a > 'a) > ('a > bool) > 'a T > 'a T > 'a T, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

28 
defined : 'a T > key > bool, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

29 
dom : 'a T > key list, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

30 
fold : (key * 'a > 'b > 'b) > 'a T > 'b > 'b, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

31 
graph : 'a T > (key * 'a) list, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

32 
is_undefined : 'a T > bool, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

33 
mapf : ('a > 'b) > 'a T > 'b T, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

34 
tryapplyd : 'a T > key > 'a > 'a, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

35 
undefine : key > 'a T > 'a T, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

36 
undefined : 'a T, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

37 
update : key * 'a > 'a T > 'a T, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

38 
updatep : (key * 'a > bool) > key * 'a > 'a T > 'a T, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

39 
choose : 'a T > key * 'a, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

40 
onefunc : key * 'a > 'a T, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

41 
get_first: (key*'a > 'a option) > 'a T > 'a option} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

42 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

43 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

44 
functor FuncFun(Key: KEY) : FUNC= 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

45 
struct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

46 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

47 
type key = Key.key; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

48 
structure Tab = TableFun(Key); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

49 
type 'a T = 'a Tab.table; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

50 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

51 
val undefined = Tab.empty; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

52 
val is_undefined = Tab.is_empty; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

53 
val mapf = Tab.map; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

54 
val fold = Tab.fold; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

55 
val graph = Tab.dest; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

56 
val dom = Tab.keys; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

57 
fun applyd f d x = case Tab.lookup f x of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

58 
SOME y => y 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

59 
 NONE => d x; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

60 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

61 
fun apply f x = applyd f (fn _ => raise Tab.UNDEF x) x; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

62 
fun tryapplyd f a d = applyd f (K d) a; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

63 
val defined = Tab.defined; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

64 
fun undefine x t = (Tab.delete x t handle UNDEF => t); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

65 
val update = Tab.update; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

66 
fun updatep p (k,v) t = if p (k, v) then t else update (k,v) t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

67 
fun combine f z a b = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

68 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

69 
fun h (k,v) t = case Tab.lookup t k of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

70 
NONE => Tab.update (k,v) t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

71 
 SOME v' => let val w = f v v' 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

72 
in if z w then Tab.delete k t else Tab.update (k,w) t end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

73 
in Tab.fold h a b end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

74 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

75 
fun choose f = case Tab.max_key f of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

76 
SOME k => (k,valOf (Tab.lookup f k)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

77 
 NONE => error "FuncFun.choose : Completely undefined function" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

78 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

79 
fun onefunc kv = update kv undefined 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

80 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

81 
local 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

82 
fun find f (k,v) NONE = f (k,v) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

83 
 find f (k,v) r = r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

84 
in 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

85 
fun get_first f t = fold (find f) t NONE 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

86 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

87 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

88 
val fns = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

89 
{key_ord = Key.ord, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

90 
apply = apply, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

91 
applyd = applyd, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

92 
combine = combine, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

93 
defined = defined, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

94 
dom = dom, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

95 
fold = fold, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

96 
graph = graph, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

97 
is_undefined = is_undefined, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

98 
mapf = mapf, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

99 
tryapplyd = tryapplyd, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

100 
undefine = undefine, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

101 
undefined = undefined, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

102 
update = update, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

103 
updatep = updatep, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

104 
choose = choose, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

105 
onefunc = onefunc, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

106 
get_first = get_first} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

107 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

108 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

109 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

110 
structure Intfunc = FuncFun(type key = int val ord = int_ord); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

111 
structure Symfunc = FuncFun(type key = string val ord = fast_string_ord); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

112 
structure Termfunc = FuncFun(type key = term val ord = TermOrd.fast_term_ord); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

113 
structure Ctermfunc = FuncFun(type key = cterm val ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t))); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

114 
structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

115 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

116 
(* Some conversionsrelated stuff which has been forbidden entrance into Pure/conv.ML*) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

117 
structure Conv2 = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

118 
struct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

119 
open Conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

120 
fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

121 
fun is_comb t = case (term_of t) of _$_ => true  _ => false; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

122 
fun is_abs t = case (term_of t) of Abs _ => true  _ => false; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

123 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

124 
fun end_itlist f l = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

125 
case l of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

126 
[] => error "end_itlist" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

127 
 [x] => x 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

128 
 (h::t) => f h (end_itlist f t); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

129 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

130 
fun absc cv ct = case term_of ct of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

131 
Abs (v,_, _) => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

132 
let val (x,t) = Thm.dest_abs (SOME v) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

133 
in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

134 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

135 
 _ => all_conv ct; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

136 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

137 
fun cache_conv conv = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

138 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

139 
val tab = ref Termtab.empty 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

140 
fun cconv t = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

141 
case Termtab.lookup (!tab) (term_of t) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

142 
SOME th => th 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

143 
 NONE => let val th = conv t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

144 
in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

145 
in cconv end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

146 
fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct')) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

147 
handle CTERM _ => false; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

148 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

149 
local 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

150 
fun thenqc conv1 conv2 tm = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

151 
case try conv1 tm of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

152 
SOME th1 => (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2  NONE => th1) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

153 
 NONE => conv2 tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

154 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

155 
fun thencqc conv1 conv2 tm = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

156 
let val th1 = conv1 tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

157 
in (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2  NONE => th1) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

158 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

159 
fun comb_qconv conv tm = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

160 
let val (l,r) = Thm.dest_comb tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

161 
in (case try conv l of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

162 
SOME th1 => (case try conv r of SOME th2 => Thm.combination th1 th2 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

163 
 NONE => Drule.fun_cong_rule th1 r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

164 
 NONE => Drule.arg_cong_rule l (conv r)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

165 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

166 
fun repeatqc conv tm = thencqc conv (repeatqc conv) tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

167 
fun sub_qconv conv tm = if is_abs tm then absc conv tm else comb_qconv conv tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

168 
fun once_depth_qconv conv tm = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

169 
(conv else_conv (sub_qconv (once_depth_qconv conv))) tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

170 
fun depth_qconv conv tm = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

171 
thenqc (sub_qconv (depth_qconv conv)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

172 
(repeatqc conv) tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

173 
fun redepth_qconv conv tm = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

174 
thenqc (sub_qconv (redepth_qconv conv)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

175 
(thencqc conv (redepth_qconv conv)) tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

176 
fun top_depth_qconv conv tm = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

177 
thenqc (repeatqc conv) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

178 
(thencqc (sub_qconv (top_depth_qconv conv)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

179 
(thencqc conv (top_depth_qconv conv))) tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

180 
fun top_sweep_qconv conv tm = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

181 
thenqc (repeatqc conv) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

182 
(sub_qconv (top_sweep_qconv conv)) tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

183 
in 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

184 
val (once_depth_conv, depth_conv, rdepth_conv, top_depth_conv, top_sweep_conv) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

185 
(fn c => try_conv (once_depth_qconv c), 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

186 
fn c => try_conv (depth_qconv c), 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

187 
fn c => try_conv (redepth_qconv c), 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

188 
fn c => try_conv (top_depth_qconv c), 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

189 
fn c => try_conv (top_sweep_qconv c)); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

190 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

191 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

192 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

193 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

194 
(* Some useful derived rules *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

195 
fun deduct_antisym_rule tha thb = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

196 
equal_intr (implies_intr (cprop_of thb) tha) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

197 
(implies_intr (cprop_of tha) thb); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

198 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

199 
fun prove_hyp tha thb = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

200 
if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

201 
then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

202 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

203 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

204 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

205 
signature REAL_ARITH = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

206 
sig 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

207 
datatype positivstellensatz = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

208 
Axiom_eq of int 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

209 
 Axiom_le of int 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

210 
 Axiom_lt of int 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

211 
 Rational_eq of Rat.rat 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

212 
 Rational_le of Rat.rat 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

213 
 Rational_lt of Rat.rat 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

214 
 Square of cterm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

215 
 Eqmul of cterm * positivstellensatz 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

216 
 Sum of positivstellensatz * positivstellensatz 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

217 
 Product of positivstellensatz * positivstellensatz; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

218 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

219 
val gen_gen_real_arith : 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

220 
Proof.context > (Rat.rat > Thm.cterm) * conv * conv * conv * 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

221 
conv * conv * conv * conv * conv * conv * 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

222 
( (thm list * thm list * thm list > positivstellensatz > thm) > 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

223 
thm list * thm list * thm list > thm) > conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

224 
val real_linear_prover : 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

225 
(thm list * thm list * thm list > positivstellensatz > thm) > 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

226 
thm list * thm list * thm list > thm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

227 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

228 
val gen_real_arith : Proof.context > 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

229 
(Rat.rat > cterm) * conv * conv * conv * conv * conv * conv * conv * 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

230 
( (thm list * thm list * thm list > positivstellensatz > thm) > 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

231 
thm list * thm list * thm list > thm) > conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

232 
val gen_prover_real_arith : Proof.context > 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

233 
((thm list * thm list * thm list > positivstellensatz > thm) > 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

234 
thm list * thm list * thm list > thm) > conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

235 
val real_arith : Proof.context > conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

236 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

237 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

238 
structure RealArith (* : REAL_ARITH *)= 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

239 
struct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

240 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

241 
open Conv Thm Conv2;; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

242 
(*  *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

243 
(* Data structure for Positivstellensatz refutations. *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

244 
(*  *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

245 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

246 
datatype positivstellensatz = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

247 
Axiom_eq of int 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

248 
 Axiom_le of int 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

249 
 Axiom_lt of int 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

250 
 Rational_eq of Rat.rat 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

251 
 Rational_le of Rat.rat 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

252 
 Rational_lt of Rat.rat 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

253 
 Square of cterm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

254 
 Eqmul of cterm * positivstellensatz 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

255 
 Sum of positivstellensatz * positivstellensatz 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

256 
 Product of positivstellensatz * positivstellensatz; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

257 
(* Theorems used in the procedure *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

258 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

259 
fun conjunctions th = case try Conjunction.elim th of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

260 
SOME (th1,th2) => (conjunctions th1) @ conjunctions th2 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

261 
 NONE => [th]; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

262 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

263 
val pth = @{lemma "(((x::real) < y) == (y  x > 0)) &&& ((x <= y) == (y  x >= 0)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

264 
&&& ((x = y) == (x  y = 0)) &&& ((~(x < y)) == (x  y >= 0)) &&& ((~(x <= y)) == (x  y > 0)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

265 
&&& ((~(x = y)) == (x  y > 0  (x  y) > 0))" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

266 
by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)} > 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

267 
conjunctions; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

268 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

269 
val pth_final = @{lemma "(~p ==> False) ==> p" by blast} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

270 
val pth_add = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

271 
@{lemma "(x = (0::real) ==> y = 0 ==> x + y = 0 ) &&& ( x = 0 ==> y >= 0 ==> x + y >= 0) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

272 
&&& (x = 0 ==> y > 0 ==> x + y > 0) &&& (x >= 0 ==> y = 0 ==> x + y >= 0) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

273 
&&& (x >= 0 ==> y >= 0 ==> x + y >= 0) &&& (x >= 0 ==> y > 0 ==> x + y > 0) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

274 
&&& (x > 0 ==> y = 0 ==> x + y > 0) &&& (x > 0 ==> y >= 0 ==> x + y > 0) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

275 
&&& (x > 0 ==> y > 0 ==> x + y > 0)" by simp_all} > conjunctions ; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

276 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

277 
val pth_mul = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

278 
@{lemma "(x = (0::real) ==> y = 0 ==> x * y = 0) &&& (x = 0 ==> y >= 0 ==> x * y = 0) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

279 
(x = 0 ==> y > 0 ==> x * y = 0) &&& (x >= 0 ==> y = 0 ==> x * y = 0) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

280 
(x >= 0 ==> y >= 0 ==> x * y >= 0 ) &&& ( x >= 0 ==> y > 0 ==> x * y >= 0 ) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

281 
(x > 0 ==> y = 0 ==> x * y = 0 ) &&& ( x > 0 ==> y >= 0 ==> x * y >= 0 ) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

282 
(x > 0 ==> y > 0 ==> x * y > 0)" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

283 
by (auto intro: mult_mono[where a="0::real" and b="x" and d="y" and c="0", simplified] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

284 
mult_strict_mono[where b="x" and d="y" and a="0" and c="0", simplified])} > conjunctions; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

285 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

286 
val pth_emul = @{lemma "y = (0::real) ==> x * y = 0" by simp}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

287 
val pth_square = @{lemma "x * x >= (0::real)" by simp}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

288 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

289 
val weak_dnf_simps = List.take (simp_thms, 34) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

290 
@ 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+}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

291 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

292 
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+} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

293 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

294 
val choice_iff = @{lemma "(ALL x. EX y. P x y) = (EX f. ALL x. P x (f x))" by metis}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

295 
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)}); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

296 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

297 
val real_abs_thms1 = conjunctions @{lemma 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

298 
"((1 * abs(x::real) >= r) = (1 * x >= r & 1 * x >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

299 
((1 * abs(x) + a >= r) = (a + 1 * x >= r & a + 1 * x >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

300 
((a + 1 * abs(x) >= r) = (a + 1 * x >= r & a + 1 * x >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

301 
((a + 1 * abs(x) + b >= r) = (a + 1 * x + b >= r & a + 1 * x + b >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

302 
((a + b + 1 * abs(x) >= r) = (a + b + 1 * x >= r & a + b + 1 * x >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

303 
((a + b + 1 * abs(x) + c >= r) = (a + b + 1 * x + c >= r & a + b + 1 * x + c >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

304 
((1 * max x y >= r) = (1 * x >= r & 1 * y >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

305 
((1 * max x y + a >= r) = (a + 1 * x >= r & a + 1 * y >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

306 
((a + 1 * max x y >= r) = (a + 1 * x >= r & a + 1 * y >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

307 
((a + 1 * max x y + b >= r) = (a + 1 * x + b >= r & a + 1 * y + b >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

308 
((a + b + 1 * max x y >= r) = (a + b + 1 * x >= r & a + b + 1 * y >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

309 
((a + b + 1 * max x y + c >= r) = (a + b + 1 * x + c >= r & a + b + 1 * y + c >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

310 
((1 * min x y >= r) = (1 * x >= r & 1 * y >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

311 
((1 * min x y + a >= r) = (a + 1 * x >= r & a + 1 * y >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

312 
((a + 1 * min x y >= r) = (a + 1 * x >= r & a + 1 * y >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

313 
((a + 1 * min x y + b >= r) = (a + 1 * x + b >= r & a + 1 * y + b >= r) )&&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

314 
((a + b + 1 * min x y >= r) = (a + b + 1 * x >= r & a + b + 1 * y >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

315 
((a + b + 1 * min x y + c >= r) = (a + b + 1 * x + c >= r & a + b + 1 * y + c >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

316 
((min x y >= r) = (x >= r & y >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

317 
((min x y + a >= r) = (a + x >= r & a + y >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

318 
((a + min x y >= r) = (a + x >= r & a + y >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

319 
((a + min x y + b >= r) = (a + x + b >= r & a + y + b >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

320 
((a + b + min x y >= r) = (a + b + x >= r & a + b + y >= r) )&&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

321 
((a + b + min x y + c >= r) = (a + b + x + c >= r & a + b + y + c >= r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

322 
((1 * abs(x) > r) = (1 * x > r & 1 * x > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

323 
((1 * abs(x) + a > r) = (a + 1 * x > r & a + 1 * x > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

324 
((a + 1 * abs(x) > r) = (a + 1 * x > r & a + 1 * x > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

325 
((a + 1 * abs(x) + b > r) = (a + 1 * x + b > r & a + 1 * x + b > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

326 
((a + b + 1 * abs(x) > r) = (a + b + 1 * x > r & a + b + 1 * x > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

327 
((a + b + 1 * abs(x) + c > r) = (a + b + 1 * x + c > r & a + b + 1 * x + c > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

328 
((1 * max x y > r) = ((1 * x > r) & 1 * y > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

329 
((1 * max x y + a > r) = (a + 1 * x > r & a + 1 * y > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

330 
((a + 1 * max x y > r) = (a + 1 * x > r & a + 1 * y > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

331 
((a + 1 * max x y + b > r) = (a + 1 * x + b > r & a + 1 * y + b > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

332 
((a + b + 1 * max x y > r) = (a + b + 1 * x > r & a + b + 1 * y > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

333 
((a + b + 1 * max x y + c > r) = (a + b + 1 * x + c > r & a + b + 1 * y + c > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

334 
((min x y > r) = (x > r & y > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

335 
((min x y + a > r) = (a + x > r & a + y > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

336 
((a + min x y > r) = (a + x > r & a + y > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

337 
((a + min x y + b > r) = (a + x + b > r & a + y + b > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

338 
((a + b + min x y > r) = (a + b + x > r & a + b + y > r)) &&& 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

339 
((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

340 
by auto}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

341 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

342 
val abs_split' = @{lemma "P (abs (x::'a::ordered_idom)) == (x >= 0 & P x  x < 0 & P (x))" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

343 
by (atomize (full)) (auto split add: abs_split)}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

344 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

345 
val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y  x > y & P x)" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

346 
by (atomize (full)) (cases "x <= y", auto simp add: max_def)}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

347 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

348 
val min_split = @{lemma "P (min x y) == ((x::'a::linorder) <= y & P x  x > y & P y)" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

349 
by (atomize (full)) (cases "x <= y", auto simp add: min_def)}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

350 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

351 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

352 
(* Miscalineous *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

353 
fun literals_conv bops uops cv = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

354 
let fun h t = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

355 
case (term_of t) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

356 
b$_$_ => if member (op aconv) bops b then binop_conv h t else cv t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

357 
 u$_ => if member (op aconv) uops u then arg_conv h t else cv t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

358 
 _ => cv t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

359 
in h end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

360 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

361 
fun cterm_of_rat x = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

362 
let val (a, b) = Rat.quotient_of_rat x 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

363 
in 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

364 
if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

365 
else Thm.capply (Thm.capply @{cterm "op / :: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

366 
(Numeral.mk_cnumber @{ctyp "real"} a)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

367 
(Numeral.mk_cnumber @{ctyp "real"} b) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

368 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

369 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

370 
fun dest_ratconst t = case term_of t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

371 
Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a > snd, HOLogic.dest_number b > snd) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

372 
 _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) > snd) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

373 
fun is_ratconst t = can dest_ratconst t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

374 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

375 
fun find_term p t = if p t then t else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

376 
case t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

377 
a$b => (find_term p a handle TERM _ => find_term p b) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

378 
 Abs (_,_,t') => find_term p t' 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

379 
 _ => raise TERM ("find_term",[t]); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

380 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

381 
fun find_cterm p t = if p t then t else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

382 
case term_of t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

383 
a$b => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

384 
 Abs (_,_,t') => find_cterm p (Thm.dest_abs NONE t > snd) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

385 
 _ => raise CTERM ("find_cterm",[t]); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

386 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

387 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

388 
(* A general real arithmetic prover *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

389 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

390 
fun gen_gen_real_arith ctxt (mk_numeric, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

391 
numeric_eq_conv,numeric_ge_conv,numeric_gt_conv, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

392 
poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

393 
absconv1,absconv2,prover) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

394 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

395 
open Conv Thm; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

396 
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}] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

397 
val prenex_ss = HOL_basic_ss addsimps prenex_simps 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

398 
val skolemize_ss = HOL_basic_ss addsimps [choice_iff] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

399 
val presimp_conv = Simplifier.rewrite (Simplifier.context ctxt pre_ss) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

400 
val prenex_conv = Simplifier.rewrite (Simplifier.context ctxt prenex_ss) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

401 
val skolemize_conv = Simplifier.rewrite (Simplifier.context ctxt skolemize_ss) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

402 
val weak_dnf_ss = HOL_basic_ss addsimps weak_dnf_simps 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

403 
val weak_dnf_conv = Simplifier.rewrite (Simplifier.context ctxt weak_dnf_ss) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

404 
fun eqT_elim th = equal_elim (symmetric th) @{thm TrueI} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

405 
fun oprconv cv ct = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

406 
let val g = Thm.dest_fun2 ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

407 
in if g aconvc @{cterm "op <= :: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

408 
orelse g aconvc @{cterm "op < :: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

409 
then arg_conv cv ct else arg1_conv cv ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

410 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

411 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

412 
fun real_ineq_conv th ct = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

413 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

414 
val th' = (instantiate (match (lhs_of th, ct)) th 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

415 
handle MATCH => raise CTERM ("real_ineq_conv", [ct])) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

416 
in transitive th' (oprconv poly_conv (Thm.rhs_of th')) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

417 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

418 
val [real_lt_conv, real_le_conv, real_eq_conv, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

419 
real_not_lt_conv, real_not_le_conv, _] = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

420 
map real_ineq_conv pth 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

421 
fun match_mp_rule ths ths' = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

422 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

423 
fun f ths ths' = case ths of [] => raise THM("match_mp_rule",0,ths) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

424 
 th::ths => (ths' MRS th handle THM _ => f ths ths') 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

425 
in f ths ths' end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

426 
fun mul_rule th th' = fconv_rule (arg_conv (oprconv poly_mul_conv)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

427 
(match_mp_rule pth_mul [th, th']) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

428 
fun add_rule th th' = fconv_rule (arg_conv (oprconv poly_add_conv)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

429 
(match_mp_rule pth_add [th, th']) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

430 
fun emul_rule ct th = fconv_rule (arg_conv (oprconv poly_mul_conv)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

431 
(instantiate' [] [SOME ct] (th RS pth_emul)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

432 
fun square_rule t = fconv_rule (arg_conv (oprconv poly_mul_conv)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

433 
(instantiate' [] [SOME t] pth_square) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

434 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

435 
fun hol_of_positivstellensatz(eqs,les,lts) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

436 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

437 
fun translate prf = case prf of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

438 
Axiom_eq n => nth eqs n 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

439 
 Axiom_le n => nth les n 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

440 
 Axiom_lt n => nth lts n 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

441 
 Rational_eq x => eqT_elim(numeric_eq_conv(capply @{cterm Trueprop} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

442 
(capply (capply @{cterm "op =::real => _"} (mk_numeric x)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

443 
@{cterm "0::real"}))) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

444 
 Rational_le x => eqT_elim(numeric_ge_conv(capply @{cterm Trueprop} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

445 
(capply (capply @{cterm "op <=::real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

446 
@{cterm "0::real"}) (mk_numeric x)))) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

447 
 Rational_lt x => eqT_elim(numeric_gt_conv(capply @{cterm Trueprop} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

448 
(capply (capply @{cterm "op <::real => _"} @{cterm "0::real"}) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

449 
(mk_numeric x)))) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

450 
 Square t => square_rule t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

451 
 Eqmul(t,p) => emul_rule t (translate p) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

452 
 Sum(p1,p2) => add_rule (translate p1) (translate p2) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

453 
 Product(p1,p2) => mul_rule (translate p1) (translate p2) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

454 
in fn prf => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

455 
fconv_rule (first_conv [numeric_ge_conv, numeric_gt_conv, numeric_eq_conv, all_conv]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

456 
(translate prf) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

457 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

458 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

459 
val init_conv = presimp_conv then_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

460 
nnf_conv then_conv skolemize_conv then_conv prenex_conv then_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

461 
weak_dnf_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

462 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

463 
val concl = dest_arg o cprop_of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

464 
fun is_binop opr ct = (dest_fun2 ct aconvc opr handle CTERM _ => false) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

465 
val is_req = is_binop @{cterm "op =:: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

466 
val is_ge = is_binop @{cterm "op <=:: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

467 
val is_gt = is_binop @{cterm "op <:: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

468 
val is_conj = is_binop @{cterm "op &"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

469 
val is_disj = is_binop @{cterm "op "} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

470 
fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2}) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

471 
fun disj_cases th th1 th2 = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

472 
let val (p,q) = dest_binop (concl th) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

473 
val c = concl th1 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

474 
val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

475 
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) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

476 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

477 
fun overall dun ths = case ths of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

478 
[] => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

479 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

480 
val (eq,ne) = List.partition (is_req o concl) dun 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

481 
val (le,nl) = List.partition (is_ge o concl) ne 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

482 
val lt = filter (is_gt o concl) nl 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

483 
in prover hol_of_positivstellensatz (eq,le,lt) end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

484 
 th::oths => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

485 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

486 
val ct = concl th 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

487 
in 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

488 
if is_conj ct then 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

489 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

490 
val (th1,th2) = conj_pair th in 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

491 
overall dun (th1::th2::oths) end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

492 
else if is_disj ct then 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

493 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

494 
val th1 = overall dun (assume (capply @{cterm Trueprop} (dest_arg1 ct))::oths) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

495 
val th2 = overall dun (assume (capply @{cterm Trueprop} (dest_arg ct))::oths) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

496 
in disj_cases th th1 th2 end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

497 
else overall (th::dun) oths 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

498 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

499 
fun dest_binary b ct = if is_binop b ct then dest_binop ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

500 
else raise CTERM ("dest_binary",[b,ct]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

501 
val dest_eq = dest_binary @{cterm "op = :: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

502 
val neq_th = nth pth 5 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

503 
fun real_not_eq_conv ct = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

504 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

505 
val (l,r) = dest_eq (dest_arg ct) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

506 
val th = instantiate ([],[(@{cpat "?x::real"},l),(@{cpat "?y::real"},r)]) neq_th 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

507 
val th_p = poly_conv(dest_arg(dest_arg1(Thm.rhs_of th))) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

508 
val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

509 
val th_n = fconv_rule (arg_conv poly_neg_conv) th_x 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

510 
val th' = Drule.binop_cong_rule @{cterm "op "} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

511 
(Drule.arg_cong_rule (capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

512 
(Drule.arg_cong_rule (capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

513 
in transitive th th' 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

514 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

515 
fun equal_implies_1_rule PQ = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

516 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

517 
val P = lhs_of PQ 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

518 
in implies_intr P (equal_elim PQ (assume P)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

519 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

520 
(* FIXME!!! Copied from groebner.ml *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

521 
val strip_exists = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

522 
let fun h (acc, t) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

523 
case (term_of t) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

524 
Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) >> (fn v => v::acc)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

525 
 _ => (acc,t) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

526 
in fn t => h ([],t) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

527 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

528 
fun name_of x = case term_of x of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

529 
Free(s,_) => s 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

530 
 Var ((s,_),_) => s 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

531 
 _ => "x" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

532 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

533 
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) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

534 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

535 
val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec)); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

536 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

537 
fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

538 
fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

539 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

540 
fun choose v th th' = case concl_of th of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

541 
@{term Trueprop} $ (Const("Ex",_)$_) => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

542 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

543 
val p = (funpow 2 Thm.dest_arg o cprop_of) th 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

544 
val T = (hd o Thm.dest_ctyp o ctyp_of_term) p 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

545 
val th0 = fconv_rule (Thm.beta_conversion true) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

546 
(instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

547 
val pv = (Thm.rhs_of o Thm.beta_conversion true) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

548 
(Thm.capply @{cterm Trueprop} (Thm.capply p v)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

549 
val th1 = forall_intr v (implies_intr pv th') 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

550 
in implies_elim (implies_elim th0 th) th1 end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

551 
 _ => raise THM ("choose",0,[th, th']) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

552 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

553 
fun simple_choose v th = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

554 
choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

555 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

556 
val strip_forall = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

557 
let fun h (acc, t) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

558 
case (term_of t) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

559 
Const("All",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) >> (fn v => v::acc)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

560 
 _ => (acc,t) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

561 
in fn t => h ([],t) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

562 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

563 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

564 
fun f ct = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

565 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

566 
val nnf_norm_conv' = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

567 
nnf_conv then_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

568 
literals_conv [@{term "op &"}, @{term "op "}] [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

569 
(cache_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

570 
(first_conv [real_lt_conv, real_le_conv, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

571 
real_eq_conv, real_not_lt_conv, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

572 
real_not_le_conv, real_not_eq_conv, all_conv])) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

573 
fun absremover ct = (literals_conv [@{term "op &"}, @{term "op "}] [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

574 
(try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

575 
try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

576 
val nct = capply @{cterm Trueprop} (capply @{cterm "Not"} ct) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

577 
val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

578 
val tm0 = dest_arg (Thm.rhs_of th0) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

579 
val th = if tm0 aconvc @{cterm False} then equal_implies_1_rule th0 else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

580 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

581 
val (evs,bod) = strip_exists tm0 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

582 
val (avs,ibod) = strip_forall bod 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

583 
val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

584 
val th2 = overall [] [specl avs (assume (Thm.rhs_of th1))] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

585 
val th3 = fold simple_choose evs (prove_hyp (equal_elim th1 (assume (capply @{cterm Trueprop} bod))) th2) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

586 
in Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

587 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

588 
in implies_elim (instantiate' [] [SOME ct] pth_final) th 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

589 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

590 
in f 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

591 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

592 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

593 
(* A linear arithmetic prover *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

594 
local 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

595 
val linear_add = Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

596 
fun linear_cmul c = Ctermfunc.mapf (fn x => c */ x) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

597 
val one_tm = @{cterm "1::real"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

598 
fun contradictory p (e,_) = ((Ctermfunc.is_undefined e) andalso not(p Rat.zero)) orelse 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

599 
((gen_eq_set (op aconvc) (Ctermfunc.dom e, [one_tm])) andalso not(p(Ctermfunc.apply e one_tm))) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

600 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

601 
fun linear_ineqs vars (les,lts) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

602 
case find_first (contradictory (fn x => x >/ Rat.zero)) lts of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

603 
SOME r => r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

604 
 NONE => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

605 
(case find_first (contradictory (fn x => x >/ Rat.zero)) les of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

606 
SOME r => r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

607 
 NONE => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

608 
if null vars then error "linear_ineqs: no contradiction" else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

609 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

610 
val ineqs = les @ lts 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

611 
fun blowup v = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

612 
length(filter (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) ineqs) + 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

613 
length(filter (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) ineqs) * 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

614 
length(filter (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero </ Rat.zero) ineqs) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

615 
val v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

616 
(map (fn v => (v,blowup v)) vars))) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

617 
fun addup (e1,p1) (e2,p2) acc = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

618 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

619 
val c1 = Ctermfunc.tryapplyd e1 v Rat.zero 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

620 
val c2 = Ctermfunc.tryapplyd e2 v Rat.zero 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

621 
in if c1 */ c2 >=/ Rat.zero then acc else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

622 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

623 
val e1' = linear_cmul (Rat.abs c2) e1 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

624 
val e2' = linear_cmul (Rat.abs c1) e2 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

625 
val p1' = Product(Rational_lt(Rat.abs c2),p1) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

626 
val p2' = Product(Rational_lt(Rat.abs c1),p2) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

627 
in (linear_add e1' e2',Sum(p1',p2'))::acc 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

628 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

629 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

630 
val (les0,les1) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

631 
List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) les 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

632 
val (lts0,lts1) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

633 
List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) lts 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

634 
val (lesp,lesn) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

635 
List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) les1 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

636 
val (ltsp,ltsn) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

637 
List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) lts1 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

638 
val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

639 
val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

640 
(fold_rev (fn ep1 => fold_rev (addup ep1) (lesn@ltsn)) ltsp lts0) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

641 
in linear_ineqs (remove (op aconvc) v vars) (les',lts') 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

642 
end) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

643 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

644 
fun linear_eqs(eqs,les,lts) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

645 
case find_first (contradictory (fn x => x =/ Rat.zero)) eqs of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

646 
SOME r => r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

647 
 NONE => (case eqs of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

648 
[] => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

649 
let val vars = remove (op aconvc) one_tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

650 
(fold_rev (curry (gen_union (op aconvc)) o Ctermfunc.dom o fst) (les@lts) []) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

651 
in linear_ineqs vars (les,lts) end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

652 
 (e,p)::es => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

653 
if Ctermfunc.is_undefined e then linear_eqs (es,les,lts) else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

654 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

655 
val (x,c) = Ctermfunc.choose (Ctermfunc.undefine one_tm e) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

656 
fun xform (inp as (t,q)) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

657 
let val d = Ctermfunc.tryapplyd t x Rat.zero in 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

658 
if d =/ Rat.zero then inp else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

659 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

660 
val k = (Rat.neg d) */ Rat.abs c // c 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

661 
val e' = linear_cmul k e 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

662 
val t' = linear_cmul (Rat.abs c) t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

663 
val p' = Eqmul(cterm_of_rat k,p) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

664 
val q' = Product(Rational_lt(Rat.abs c),q) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

665 
in (linear_add e' t',Sum(p',q')) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

666 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

667 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

668 
in linear_eqs(map xform es,map xform les,map xform lts) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

669 
end) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

670 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

671 
fun linear_prover (eq,le,lt) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

672 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

673 
val eqs = map2 (fn p => fn n => (p,Axiom_eq n)) eq (0 upto (length eq  1)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

674 
val les = map2 (fn p => fn n => (p,Axiom_le n)) le (0 upto (length le  1)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

675 
val lts = map2 (fn p => fn n => (p,Axiom_lt n)) lt (0 upto (length lt  1)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

676 
in linear_eqs(eqs,les,lts) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

677 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

678 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

679 
fun lin_of_hol ct = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

680 
if ct aconvc @{cterm "0::real"} then Ctermfunc.undefined 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

681 
else if not (is_comb ct) then Ctermfunc.onefunc (ct, Rat.one) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

682 
else if is_ratconst ct then Ctermfunc.onefunc (one_tm, dest_ratconst ct) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

683 
else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

684 
let val (lop,r) = Thm.dest_comb ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

685 
in if not (is_comb lop) then Ctermfunc.onefunc (ct, Rat.one) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

686 
else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

687 
let val (opr,l) = Thm.dest_comb lop 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

688 
in if opr aconvc @{cterm "op + :: real =>_"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

689 
then linear_add (lin_of_hol l) (lin_of_hol r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

690 
else if opr aconvc @{cterm "op * :: real =>_"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

691 
andalso is_ratconst l then Ctermfunc.onefunc (r, dest_ratconst l) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

692 
else Ctermfunc.onefunc (ct, Rat.one) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

693 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

694 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

695 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

696 
fun is_alien ct = case term_of ct of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

697 
Const(@{const_name "real"}, _)$ n => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

698 
if can HOLogic.dest_number n then false else true 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

699 
 _ => false 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

700 
open Thm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

701 
in 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

702 
fun real_linear_prover translator (eq,le,lt) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

703 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

704 
val lhs = lin_of_hol o dest_arg1 o dest_arg o cprop_of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

705 
val rhs = lin_of_hol o dest_arg o dest_arg o cprop_of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

706 
val eq_pols = map lhs eq 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

707 
val le_pols = map rhs le 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

708 
val lt_pols = map rhs lt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

709 
val aliens = filter is_alien 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

710 
(fold_rev (curry (gen_union (op aconvc)) o Ctermfunc.dom) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

711 
(eq_pols @ le_pols @ lt_pols) []) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

712 
val le_pols' = le_pols @ map (fn v => Ctermfunc.onefunc (v,Rat.one)) aliens 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

713 
val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

714 
val le' = le @ map (fn a => instantiate' [] [SOME (dest_arg a)] @{thm real_of_nat_ge_zero}) aliens 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

715 
in (translator (eq,le',lt) proof) : thm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

716 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

717 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

718 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

719 
(* A less general generic arithmetic prover dealing with abs,max and min*) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

720 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

721 
local 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

722 
val absmaxmin_elim_ss1 = HOL_basic_ss addsimps real_abs_thms1 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

723 
fun absmaxmin_elim_conv1 ctxt = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

724 
Simplifier.rewrite (Simplifier.context ctxt absmaxmin_elim_ss1) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

725 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

726 
val absmaxmin_elim_conv2 = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

727 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

728 
val pth_abs = instantiate' [SOME @{ctyp real}] [] abs_split' 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

729 
val pth_max = instantiate' [SOME @{ctyp real}] [] max_split 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

730 
val pth_min = instantiate' [SOME @{ctyp real}] [] min_split 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

731 
val abs_tm = @{cterm "abs :: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

732 
val p_tm = @{cpat "?P :: real => bool"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

733 
val x_tm = @{cpat "?x :: real"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

734 
val y_tm = @{cpat "?y::real"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

735 
val is_max = is_binop @{cterm "max :: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

736 
val is_min = is_binop @{cterm "min :: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

737 
fun is_abs t = is_comb t andalso dest_fun t aconvc abs_tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

738 
fun eliminate_construct p c tm = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

739 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

740 
val t = find_cterm p tm 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

741 
val th0 = (symmetric o beta_conversion false) (capply (cabs t tm) t) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

742 
val (p,ax) = (dest_comb o Thm.rhs_of) th0 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

743 
in fconv_rule(arg_conv(binop_conv (arg_conv (beta_conversion false)))) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

744 
(transitive th0 (c p ax)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

745 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

746 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

747 
val elim_abs = eliminate_construct is_abs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

748 
(fn p => fn ax => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

749 
instantiate ([], [(p_tm,p), (x_tm, dest_arg ax)]) pth_abs) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

750 
val elim_max = eliminate_construct is_max 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

751 
(fn p => fn ax => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

752 
let val (ax,y) = dest_comb ax 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

753 
in instantiate ([], [(p_tm,p), (x_tm, dest_arg ax), (y_tm,y)]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

754 
pth_max end) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

755 
val elim_min = eliminate_construct is_min 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

756 
(fn p => fn ax => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

757 
let val (ax,y) = dest_comb ax 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

758 
in instantiate ([], [(p_tm,p), (x_tm, dest_arg ax), (y_tm,y)]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

759 
pth_min end) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

760 
in first_conv [elim_abs, elim_max, elim_min, all_conv] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

761 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

762 
in fun gen_real_arith ctxt (mkconst,eq,ge,gt,norm,neg,add,mul,prover) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

763 
gen_gen_real_arith ctxt (mkconst,eq,ge,gt,norm,neg,add,mul, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

764 
absmaxmin_elim_conv1 ctxt,absmaxmin_elim_conv2,prover) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

765 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

766 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

767 
(* An instance for reals*) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

768 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

769 
fun gen_prover_real_arith ctxt prover = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

770 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

771 
fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

772 
val {add,mul,neg,pow,sub,main} = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

773 
Normalizer.semiring_normalizers_ord_wrapper ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

774 
(valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

775 
simple_cterm_ord 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

776 
in gen_real_arith ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

777 
(cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

778 
main,neg,add,mul, prover) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

779 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

780 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

781 
fun real_arith ctxt = gen_prover_real_arith ctxt real_linear_prover; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

782 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

783 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

784 
(* Now the norm procedure for euclidean spaces *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

785 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

786 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

787 
signature NORM_ARITH = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

788 
sig 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

789 
val norm_arith : Proof.context > conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

790 
val norm_arith_tac : Proof.context > int > tactic 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

791 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

792 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

793 
structure NormArith : NORM_ARITH = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

794 
struct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

795 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

796 
open Conv Thm Conv2; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

797 
val bool_eq = op = : bool *bool > bool 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

798 
fun dest_ratconst t = case term_of t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

799 
Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a > snd, HOLogic.dest_number b > snd) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

800 
 _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) > snd) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

801 
fun is_ratconst t = can dest_ratconst t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

802 
fun augment_norm b t acc = case term_of t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

803 
Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,dest_arg t) acc 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

804 
 _ => acc 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

805 
fun find_normedterms t acc = case term_of t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

806 
@{term "op + :: real => _"}$_$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

807 
find_normedterms (dest_arg1 t) (find_normedterms (dest_arg t) acc) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

808 
 @{term "op * :: real => _"}$_$n => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

809 
if not (is_ratconst (dest_arg1 t)) then acc else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

810 
augment_norm (dest_ratconst (dest_arg1 t) >=/ Rat.zero) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

811 
(dest_arg t) acc 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

812 
 _ => augment_norm true t acc 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

813 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

814 
val cterm_lincomb_neg = Ctermfunc.mapf Rat.neg 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

815 
fun cterm_lincomb_cmul c t = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

816 
if c =/ Rat.zero then Ctermfunc.undefined else Ctermfunc.mapf (fn x => x */ c) t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

817 
fun cterm_lincomb_add l r = Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

818 
fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

819 
fun cterm_lincomb_eq l r = Ctermfunc.is_undefined (cterm_lincomb_sub l r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

820 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

821 
val int_lincomb_neg = Intfunc.mapf Rat.neg 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

822 
fun int_lincomb_cmul c t = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

823 
if c =/ Rat.zero then Intfunc.undefined else Intfunc.mapf (fn x => x */ c) t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

824 
fun int_lincomb_add l r = Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

825 
fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

826 
fun int_lincomb_eq l r = Intfunc.is_undefined (int_lincomb_sub l r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

827 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

828 
fun vector_lincomb t = case term_of t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

829 
Const(@{const_name plus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_])) $ _ $ _ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

830 
cterm_lincomb_add (vector_lincomb (dest_arg1 t)) (vector_lincomb (dest_arg t)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

831 
 Const(@{const_name minus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_])) $ _ $ _ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

832 
cterm_lincomb_sub (vector_lincomb (dest_arg1 t)) (vector_lincomb (dest_arg t)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

833 
 Const(@{const_name vector_scalar_mult},Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))$_$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

834 
cterm_lincomb_cmul (dest_ratconst (dest_arg1 t)) (vector_lincomb (dest_arg t)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

835 
 Const(@{const_name uminus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

836 
cterm_lincomb_neg (vector_lincomb (dest_arg t)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

837 
 Const(@{const_name vec},_)$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

838 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

839 
val b = ((snd o HOLogic.dest_number o term_of o dest_arg) t = 0 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

840 
handle TERM _=> false) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

841 
in if b then Ctermfunc.onefunc (t,Rat.one) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

842 
else Ctermfunc.undefined 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

843 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

844 
 _ => Ctermfunc.onefunc (t,Rat.one) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

845 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

846 
fun vector_lincombs ts = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

847 
fold_rev 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

848 
(fn t => fn fns => case AList.lookup (op aconvc) fns t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

849 
NONE => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

850 
let val f = vector_lincomb t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

851 
in case find_first (fn (_,f') => cterm_lincomb_eq f f') fns of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

852 
SOME (_,f') => (t,f') :: fns 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

853 
 NONE => (t,f) :: fns 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

854 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

855 
 SOME _ => fns) ts [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

856 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

857 
fun replacenegnorms cv t = case term_of t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

858 
@{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

859 
 @{term "op * :: real => _"}$_$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

860 
if dest_ratconst (dest_arg1 t) </ Rat.zero then arg_conv cv t else reflexive t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

861 
 _ => reflexive t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

862 
fun flip v eq = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

863 
if Ctermfunc.defined eq v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

864 
then Ctermfunc.update (v, Rat.neg (Ctermfunc.apply eq v)) eq else eq 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

865 
fun allsubsets s = case s of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

866 
[] => [[]] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

867 
(a::t) => let val res = allsubsets t in 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

868 
map (cons a) res @ res end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

869 
fun evaluate env lin = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

870 
Intfunc.fold (fn (x,c) => fn s => s +/ c */ (Intfunc.apply env x)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

871 
lin Rat.zero 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

872 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

873 
fun solve (vs,eqs) = case (vs,eqs) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

874 
([],[]) => SOME (Intfunc.onefunc (0,Rat.one)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

875 
(_,eq::oeqs) => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

876 
(case vs inter (Intfunc.dom eq) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

877 
[] => NONE 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

878 
 v::_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

879 
if Intfunc.defined eq v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

880 
then 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

881 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

882 
val c = Intfunc.apply eq v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

883 
val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

884 
fun eliminate eqn = if not (Intfunc.defined eqn v) then eqn 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

885 
else int_lincomb_add (int_lincomb_cmul (Intfunc.apply eqn v) vdef) eqn 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

886 
in (case solve (vs \ v,map eliminate oeqs) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

887 
NONE => NONE 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

888 
 SOME soln => SOME (Intfunc.update (v, evaluate soln (Intfunc.undefine v vdef)) soln)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

889 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

890 
else NONE) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

891 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

892 
fun combinations k l = if k = 0 then [[]] else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

893 
case l of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

894 
[] => [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

895 
 h::t => map (cons h) (combinations (k  1) t) @ combinations k t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

896 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

897 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

898 
fun forall2 p l1 l2 = case (l1,l2) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

899 
([],[]) => true 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

900 
 (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

901 
 _ => false; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

902 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

903 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

904 
fun vertices vs eqs = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

905 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

906 
fun vertex cmb = case solve(vs,cmb) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

907 
NONE => NONE 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

908 
 SOME soln => SOME (map (fn v => Intfunc.tryapplyd soln v Rat.zero) vs) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

909 
val rawvs = map_filter vertex (combinations (length vs) eqs) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

910 
val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

911 
in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

912 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

913 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

914 
fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

915 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

916 
fun subsume todo dun = case todo of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

917 
[] => dun 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

918 
v::ovs => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

919 
let val dun' = if exists (fn w => subsumes w v) dun then dun 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

920 
else v::(filter (fn w => not(subsumes v w)) dun) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

921 
in subsume ovs dun' 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

922 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

923 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

924 
fun match_mp PQ P = P RS PQ; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

925 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

926 
fun cterm_of_rat x = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

927 
let val (a, b) = Rat.quotient_of_rat x 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

928 
in 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

929 
if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

930 
else Thm.capply (Thm.capply @{cterm "op / :: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

931 
(Numeral.mk_cnumber @{ctyp "real"} a)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

932 
(Numeral.mk_cnumber @{ctyp "real"} b) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

933 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

934 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

935 
fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm}); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

936 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

937 
fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

938 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

939 
(* I think here the static context should be sufficient!! *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

940 
fun inequality_canon_rule ctxt = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

941 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

942 
(* FIXME : Should be computed statically!! *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

943 
val real_poly_conv = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

944 
Normalizer.semiring_normalize_wrapper ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

945 
(valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

946 
in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv))) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

947 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

948 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

949 
fun absc cv ct = case term_of ct of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

950 
Abs (v,_, _) => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

951 
let val (x,t) = Thm.dest_abs (SOME v) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

952 
in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

953 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

954 
 _ => all_conv ct; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

955 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

956 
fun sub_conv cv ct = (comb_conv cv else_conv absc cv) ct; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

957 
fun botc1 conv ct = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

958 
((sub_conv (botc1 conv)) then_conv (conv else_conv all_conv)) ct; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

959 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

960 
fun rewrs_conv eqs ct = first_conv (map rewr_conv eqs) ct; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

961 
val apply_pth1 = rewr_conv @{thm pth_1}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

962 
val apply_pth2 = rewr_conv @{thm pth_2}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

963 
val apply_pth3 = rewr_conv @{thm pth_3}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

964 
val apply_pth4 = rewrs_conv @{thms pth_4}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

965 
val apply_pth5 = rewr_conv @{thm pth_5}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

966 
val apply_pth6 = rewr_conv @{thm pth_6}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

967 
val apply_pth7 = rewrs_conv @{thms pth_7}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

968 
val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm vector_smult_lzero}))); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

969 
val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv field_comp_conv); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

970 
val apply_ptha = rewr_conv @{thm pth_a}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

971 
val apply_pthb = rewrs_conv @{thms pth_b}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

972 
val apply_pthc = rewrs_conv @{thms pth_c}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

973 
val apply_pthd = try_conv (rewr_conv @{thm pth_d}); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

974 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

975 
fun headvector t = case t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

976 
Const(@{const_name plus}, Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))$ 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

977 
(Const(@{const_name vector_scalar_mult}, _)$l$v)$r => v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

978 
 Const(@{const_name vector_scalar_mult}, _)$l$v => v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

979 
 _ => error "headvector: noncanonical term" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

980 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

981 
fun vector_cmul_conv ct = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

982 
((apply_pth5 then_conv arg1_conv field_comp_conv) else_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

983 
(apply_pth6 then_conv binop_conv vector_cmul_conv)) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

984 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

985 
fun vector_add_conv ct = apply_pth7 ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

986 
handle CTERM _ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

987 
(apply_pth8 ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

988 
handle CTERM _ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

989 
(case term_of ct of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

990 
Const(@{const_name plus},_)$lt$rt => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

991 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

992 
val l = headvector lt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

993 
val r = headvector rt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

994 
in (case TermOrd.fast_term_ord (l,r) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

995 
LESS => (apply_pthb then_conv arg_conv vector_add_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

996 
then_conv apply_pthd) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

997 
 GREATER => (apply_pthc then_conv arg_conv vector_add_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

998 
then_conv apply_pthd) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

999 
 EQUAL => (apply_pth9 then_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1000 
((apply_ptha then_conv vector_add_conv) else_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1001 
arg_conv vector_add_conv then_conv apply_pthd)) ct) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1002 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1003 
 _ => reflexive ct)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1004 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1005 
fun vector_canon_conv ct = case term_of ct of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1006 
Const(@{const_name plus},_)$_$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1007 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1008 
val ((p,l),r) = Thm.dest_comb ct >> Thm.dest_comb 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1009 
val lth = vector_canon_conv l 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1010 
val rth = vector_canon_conv r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1011 
val th = Drule.binop_cong_rule p lth rth 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1012 
in fconv_rule (arg_conv vector_add_conv) th end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1013 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1014 
 Const(@{const_name vector_scalar_mult}, _)$_$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1015 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1016 
val (p,r) = Thm.dest_comb ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1017 
val rth = Drule.arg_cong_rule p (vector_canon_conv r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1018 
in fconv_rule (arg_conv (apply_pth4 else_conv vector_cmul_conv)) rth 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1019 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1020 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1021 
 Const(@{const_name minus},_)$_$_ => (apply_pth2 then_conv vector_canon_conv) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1022 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1023 
 Const(@{const_name uminus},_)$_ => (apply_pth3 then_conv vector_canon_conv) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1024 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1025 
 Const(@{const_name vec},_)$n => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1026 
let val n = Thm.dest_arg ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1027 
in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1028 
then reflexive ct else apply_pth1 ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1029 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1030 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1031 
 _ => apply_pth1 ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1032 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1033 
fun norm_canon_conv ct = case term_of ct of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1034 
Const(@{const_name norm},_)$_ => arg_conv vector_canon_conv ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1035 
 _ => raise CTERM ("norm_canon_conv", [ct]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1036 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1037 
fun fold_rev2 f [] [] z = z 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1038 
 fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1039 
 fold_rev2 f _ _ _ = raise UnequalLengths; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1040 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1041 
fun int_flip v eq = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1042 
if Intfunc.defined eq v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1043 
then Intfunc.update (v, Rat.neg (Intfunc.apply eq v)) eq else eq; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1044 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1045 
local 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1046 
val pth_zero = @{thm "Vectors.norm_0"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1047 
val tv_n = (hd o tl o dest_ctyp o ctyp_of_term o dest_arg o dest_arg1 o dest_arg o cprop_of) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1048 
pth_zero 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1049 
val concl = dest_arg o cprop_of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1050 
fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1051 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1052 
(* FIXME: Should be computed statically!!*) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1053 
val real_poly_conv = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1054 
Normalizer.semiring_normalize_wrapper ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1055 
(valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1056 
val sources = map (dest_arg o dest_arg1 o concl) nubs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1057 
val rawdests = fold_rev (find_normedterms o dest_arg o concl) (ges @ gts) [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1058 
val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1059 
else () 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1060 
val dests = distinct (op aconvc) (map snd rawdests) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1061 
val srcfuns = map vector_lincomb sources 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1062 
val destfuns = map vector_lincomb dests 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1063 
val vvs = fold_rev (curry (gen_union op aconvc) o Ctermfunc.dom) (srcfuns @ destfuns) [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1064 
val n = length srcfuns 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1065 
val nvs = 1 upto n 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1066 
val srccombs = srcfuns ~~ nvs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1067 
fun consider d = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1068 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1069 
fun coefficients x = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1070 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1071 
val inp = if Ctermfunc.defined d x then Intfunc.onefunc (0, Rat.neg(Ctermfunc.apply d x)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1072 
else Intfunc.undefined 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1073 
in fold_rev (fn (f,v) => fn g => if Ctermfunc.defined f x then Intfunc.update (v, Ctermfunc.apply f x) g else g) srccombs inp 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1074 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1075 
val equations = map coefficients vvs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1076 
val inequalities = map (fn n => Intfunc.onefunc (n,Rat.one)) nvs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1077 
fun plausiblevertices f = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1078 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1079 
val flippedequations = map (fold_rev int_flip f) equations 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1080 
val constraints = flippedequations @ inequalities 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1081 
val rawverts = vertices nvs constraints 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1082 
fun check_solution v = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1083 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1084 
val f = fold_rev2 (curry Intfunc.update) nvs v (Intfunc.onefunc (0, Rat.one)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1085 
in forall (fn e => evaluate f e =/ Rat.zero) flippedequations 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1086 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1087 
val goodverts = filter check_solution rawverts 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1088 
val signfixups = map (fn n => if n mem_int f then ~1 else 1) nvs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1089 
in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1090 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1091 
val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1092 
in subsume allverts [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1093 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1094 
fun compute_ineq v = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1095 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1096 
val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1097 
else SOME(norm_cmul_rule v t)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1098 
(v ~~ nubs) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1099 
in inequality_canon_rule ctxt (end_itlist norm_add_rule ths) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1100 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1101 
val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @ 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1102 
map (inequality_canon_rule ctxt) nubs @ ges 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1103 
val zerodests = filter 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1104 
(fn t => null (Ctermfunc.dom (vector_lincomb t))) (map snd rawdests) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1105 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1106 
in RealArith.real_linear_prover translator 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1107 
(map (fn t => instantiate ([(tv_n,(hd o tl o dest_ctyp o ctyp_of_term) t)],[]) pth_zero) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1108 
zerodests, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1109 
map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1110 
arg_conv (arg_conv real_poly_conv))) ges', 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1111 
map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1112 
arg_conv (arg_conv real_poly_conv))) gts) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1113 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1114 
in val real_vector_combo_prover = real_vector_combo_prover 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1115 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1116 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1117 
local 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1118 
val pth = @{thm norm_imp_pos_and_ge} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1119 
val norm_mp = match_mp pth 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1120 
val concl = dest_arg o cprop_of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1121 
fun conjunct1 th = th RS @{thm conjunct1} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1122 
fun conjunct2 th = th RS @{thm conjunct2} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1123 
fun C f x y = f y x 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1124 
fun real_vector_ineq_prover ctxt translator (ges,gts) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1125 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1126 
(* val _ = error "real_vector_ineq_prover: pause" *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1127 
val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1128 
val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1129 
val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1130 
fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: norm) => real"}) t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1131 
fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1132 
val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1133 
val replace_conv = try_conv (rewrs_conv asl) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1134 
val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1135 
val ges' = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1136 
fold_rev (fn th => fn ths => conjunct1(norm_mp th)::ths) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1137 
asl (map replace_rule ges) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1138 
val gts' = map replace_rule gts 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1139 
val nubs = map (conjunct2 o norm_mp) asl 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1140 
val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts') 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1141 
val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1142 
val th11 = hd (Variable.export ctxt' ctxt [fold implies_intr shs th1]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1143 
val cps = map (swap o dest_equals) (cprems_of th11) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1144 
val th12 = instantiate ([], cps) th11 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1145 
val th13 = fold (C implies_elim) (map (reflexive o snd) cps) th12; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1146 
in hd (Variable.export ctxt' ctxt [th13]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1147 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1148 
in val real_vector_ineq_prover = real_vector_ineq_prover 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1149 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1150 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1151 
local 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1152 
val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0})) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1153 
fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2}) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1154 
fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1155 
(* FIXME: Lookup in the context every time!!! Fix this !!!*) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1156 
fun splitequation ctxt th acc = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1157 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1158 
val real_poly_neg_conv = #neg 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1159 
(Normalizer.semiring_normalizers_ord_wrapper ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1160 
(valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1161 
val (th1,th2) = conj_pair(rawrule th) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1162 
in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1163 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1164 
in fun real_vector_prover ctxt translator (eqs,ges,gts) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1165 
real_vector_ineq_prover ctxt translator 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1166 
(fold_rev (splitequation ctxt) eqs ges,gts) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1167 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1168 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1169 
fun init_conv ctxt = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1170 
Simplifier.rewrite (Simplifier.context ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1171 
(HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm dist_def}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1172 
then_conv field_comp_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1173 
then_conv nnf_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1174 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1175 
fun pure ctxt = RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1176 
fun norm_arith ctxt ct = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1177 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1178 
val ctxt' = Variable.declare_term (term_of ct) ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1179 
val th = init_conv ctxt' ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1180 
in equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (symmetric th)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1181 
(pure ctxt' (rhs_of th)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1182 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1183 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1184 
fun norm_arith_tac ctxt = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1185 
clarify_tac HOL_cs THEN' 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1186 
ObjectLogic.full_atomize_tac THEN' 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1187 
CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1188 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

1189 
end; 