author | desharna |
Sat, 22 Jan 2022 14:00:36 +0100 | |
changeset 75005 | 4106bc2a9cc8 |
parent 74561 | 8e6c973003c8 |
child 77879 | dd222e2af01a |
permissions | -rw-r--r-- |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
1 |
(* Title: Provers/Arith/fast_lin_arith.ML |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
2 |
Author: Tobias Nipkow and Tjark Weber and Sascha Boehme |
6102 | 3 |
|
46709
65a9b30bff00
clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;
wenzelm
parents:
44654
diff
changeset
|
4 |
A generic linear arithmetic package. |
6102 | 5 |
|
24076 | 6 |
Only take premises and conclusions into account that are already |
7 |
(negated) (in)equations. lin_arith_simproc tries to prove or disprove |
|
8 |
the term. |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
9 |
*) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
10 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
11 |
(*** Data needed for setting up the linear arithmetic package ***) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
12 |
|
6102 | 13 |
signature LIN_ARITH_LOGIC = |
14 |
sig |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
15 |
val conjI : thm (* P ==> Q ==> P & Q *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
16 |
val ccontr : thm (* (~ P ==> False) ==> P *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
17 |
val notI : thm (* (P ==> False) ==> ~ P *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
18 |
val not_lessD : thm (* ~(m < n) ==> n <= m *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
19 |
val not_leD : thm (* ~(m <= n) ==> n < m *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
20 |
val sym : thm (* x = y ==> y = x *) |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
21 |
val trueI : thm (* True *) |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
22 |
val mk_Eq : thm -> thm |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
23 |
val atomize : thm -> thm list |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
24 |
val mk_Trueprop : term -> term |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
25 |
val neg_prop : term -> term |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
26 |
val is_False : thm -> bool |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
27 |
val is_nat : typ list * term -> bool |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
28 |
val mk_nat_thm : theory -> term -> thm |
6102 | 29 |
end; |
30 |
(* |
|
31 |
mk_Eq(~in) = `in == False' |
|
32 |
mk_Eq(in) = `in == True' |
|
33 |
where `in' is an (in)equality. |
|
34 |
||
23190 | 35 |
neg_prop(t) = neg if t is wrapped up in Trueprop and neg is the |
36 |
(logically) negated version of t (again wrapped up in Trueprop), |
|
37 |
where the negation of a negative term is the term itself (no |
|
38 |
double negation!); raises TERM ("neg_prop", [t]) if t is not of |
|
39 |
the form 'Trueprop $ _' |
|
6128 | 40 |
|
41 |
is_nat(parameter-types,t) = t:nat |
|
42 |
mk_nat_thm(t) = "0 <= t" |
|
6102 | 43 |
*) |
44 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
45 |
signature LIN_ARITH_DATA = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
46 |
sig |
24076 | 47 |
(*internal representation of linear (in-)equations:*) |
26945 | 48 |
type decomp = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool |
49 |
val decomp: Proof.context -> term -> decomp option |
|
24076 | 50 |
val domain_is_nat: term -> bool |
51 |
||
66035
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
52 |
(*abstraction for proof replay*) |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
53 |
val abstract_arith: term -> (term * term) list * Proof.context -> |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
54 |
term * ((term * term) list * Proof.context) |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
55 |
val abstract: term -> (term * term) list * Proof.context -> |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
56 |
term * ((term * term) list * Proof.context) |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
57 |
|
24076 | 58 |
(*preprocessing, performed on a representation of subgoals as list of premises:*) |
59 |
val pre_decomp: Proof.context -> typ list * term list -> (typ list * term list) list |
|
60 |
||
61 |
(*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
62 |
val pre_tac: Proof.context -> int -> tactic |
24076 | 63 |
|
64 |
(*the limit on the number of ~= allowed; because each ~= is split |
|
65 |
into two cases, this can lead to an explosion*) |
|
44654 | 66 |
val neq_limit: int Config.T |
43607
119767e1ccb4
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents:
43568
diff
changeset
|
67 |
|
44654 | 68 |
val trace: bool Config.T |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
69 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
70 |
(* |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
71 |
decomp(`x Rel y') should yield (p,i,Rel,q,j,d) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
72 |
where Rel is one of "<", "~<", "<=", "~<=" and "=" and |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
73 |
p (q, respectively) is the decomposition of the sum term x |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
74 |
(y, respectively) into a list of summand * multiplicity |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
75 |
pairs and a constant summand and d indicates if the domain |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
76 |
is discrete. |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
77 |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
78 |
domain_is_nat(`x Rel y') t should yield true iff x is of type "nat". |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
79 |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
80 |
The relationship between pre_decomp and pre_tac is somewhat tricky. The |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
81 |
internal representation of a subgoal and the corresponding theorem must |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
82 |
be modified by pre_decomp (pre_tac, resp.) in a corresponding way. See |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
83 |
the comment for split_items below. (This is even necessary for eta- and |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
84 |
beta-equivalent modifications, as some of the lin. arith. code is not |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
85 |
insensitive to them.) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
86 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
87 |
Simpset must reduce contradictory <= to False. |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
88 |
It should also cancel common summands to keep <= reduced; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
89 |
otherwise <= can grow to massive proportions. |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
90 |
*) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
91 |
|
6062 | 92 |
signature FAST_LIN_ARITH = |
93 |
sig |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
94 |
val prems_lin_arith_tac: Proof.context -> int -> tactic |
59656 | 95 |
val lin_arith_tac: Proof.context -> int -> tactic |
61144 | 96 |
val lin_arith_simproc: Proof.context -> cterm -> thm option |
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
97 |
val map_data: |
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
98 |
({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
99 |
lessD: thm list, neqE: thm list, simpset: simpset, |
59996 | 100 |
number_of: (Proof.context -> typ -> int -> cterm) option} -> |
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
101 |
{add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
102 |
lessD: thm list, neqE: thm list, simpset: simpset, |
59996 | 103 |
number_of: (Proof.context -> typ -> int -> cterm) option}) -> |
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
104 |
Context.generic -> Context.generic |
38762
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
105 |
val add_inj_thms: thm list -> Context.generic -> Context.generic |
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
106 |
val add_lessD: thm -> Context.generic -> Context.generic |
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
107 |
val add_simps: thm list -> Context.generic -> Context.generic |
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
108 |
val add_simprocs: simproc list -> Context.generic -> Context.generic |
59996 | 109 |
val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic |
6062 | 110 |
end; |
111 |
||
24076 | 112 |
functor Fast_Lin_Arith |
113 |
(structure LA_Logic: LIN_ARITH_LOGIC and LA_Data: LIN_ARITH_DATA): FAST_LIN_ARITH = |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
114 |
struct |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
115 |
|
9420 | 116 |
|
117 |
(** theory data **) |
|
118 |
||
33519 | 119 |
structure Data = Generic_Data |
22846 | 120 |
( |
24076 | 121 |
type T = |
122 |
{add_mono_thms: thm list, |
|
123 |
mult_mono_thms: thm list, |
|
124 |
inj_thms: thm list, |
|
125 |
lessD: thm list, |
|
126 |
neqE: thm list, |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
127 |
simpset: simpset, |
59996 | 128 |
number_of: (Proof.context -> typ -> int -> cterm) option}; |
9420 | 129 |
|
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
130 |
val empty : T = |
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
131 |
{add_mono_thms = [], mult_mono_thms = [], inj_thms = [], |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
132 |
lessD = [], neqE = [], simpset = empty_ss, |
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
133 |
number_of = NONE}; |
33519 | 134 |
fun merge |
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
135 |
({add_mono_thms = add_mono_thms1, mult_mono_thms = mult_mono_thms1, inj_thms = inj_thms1, |
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
136 |
lessD = lessD1, neqE = neqE1, simpset = simpset1, number_of = number_of1}, |
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
137 |
{add_mono_thms = add_mono_thms2, mult_mono_thms = mult_mono_thms2, inj_thms = inj_thms2, |
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
138 |
lessD = lessD2, neqE = neqE2, simpset = simpset2, number_of = number_of2}) : T = |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset
|
139 |
{add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2), |
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset
|
140 |
mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2), |
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset
|
141 |
inj_thms = Thm.merge_thms (inj_thms1, inj_thms2), |
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset
|
142 |
lessD = Thm.merge_thms (lessD1, lessD2), |
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23577
diff
changeset
|
143 |
neqE = Thm.merge_thms (neqE1, neqE2), |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
144 |
simpset = merge_ss (simpset1, simpset2), |
41493 | 145 |
number_of = merge_options (number_of1, number_of2)}; |
22846 | 146 |
); |
9420 | 147 |
|
148 |
val map_data = Data.map; |
|
24076 | 149 |
val get_data = Data.get o Context.Proof; |
9420 | 150 |
|
67649 | 151 |
fun get_neqE ctxt = map (Thm.transfer' ctxt) (#neqE (get_data ctxt)); |
61097 | 152 |
|
38762
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
153 |
fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = |
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
154 |
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms, |
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
155 |
lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of}; |
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
156 |
|
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
157 |
fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = |
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
158 |
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, |
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
159 |
lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of}; |
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
160 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
161 |
fun map_simpset f context = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
162 |
map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} => |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
163 |
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
164 |
lessD = lessD, neqE = neqE, simpset = simpset_map (Context.proof_of context) f simpset, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
165 |
number_of = number_of}) context; |
38762
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
166 |
|
61097 | 167 |
fun add_inj_thms thms = map_data (map_inj_thms (append (map Thm.trim_context thms))); |
168 |
fun add_lessD thm = map_data (map_lessD (fn thms => thms @ [Thm.trim_context thm])); |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
169 |
fun add_simps thms = map_simpset (fn ctxt => ctxt addsimps thms); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
170 |
fun add_simprocs procs = map_simpset (fn ctxt => ctxt addsimprocs procs); |
38762
996afaa9254a
slightly more abstract data handling in Fast_Lin_Arith;
wenzelm
parents:
38052
diff
changeset
|
171 |
|
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
172 |
fun set_number_of f = |
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
173 |
map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, ...} => |
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
174 |
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, |
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
175 |
lessD = lessD, neqE = neqE, simpset = simpset, number_of = SOME f}); |
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
176 |
|
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
177 |
fun number_of ctxt = |
61097 | 178 |
(case get_data ctxt of |
59996 | 179 |
{number_of = SOME f, ...} => f ctxt |
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
180 |
| _ => fn _ => fn _ => raise CTERM ("number_of", [])); |
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
181 |
|
9420 | 182 |
|
183 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
184 |
(*** A fast decision procedure ***) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
185 |
(*** Code ported from HOL Light ***) |
6056 | 186 |
(* possible optimizations: |
187 |
use (var,coeff) rep or vector rep tp save space; |
|
188 |
treat non-negative atoms separately rather than adding 0 <= atom |
|
189 |
*) |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
190 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
191 |
datatype lineq_type = Eq | Le | Lt; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
192 |
|
6056 | 193 |
datatype injust = Asm of int |
194 |
| Nat of int (* index of atom *) |
|
6128 | 195 |
| LessD of injust |
196 |
| NotLessD of injust |
|
197 |
| NotLeD of injust |
|
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
198 |
| NotLeDD of injust |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset
|
199 |
| Multiplied of int * injust |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
200 |
| Added of injust * injust; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
201 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset
|
202 |
datatype lineq = Lineq of int * lineq_type * int list * injust; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
203 |
|
13498 | 204 |
(* ------------------------------------------------------------------------- *) |
205 |
(* Finding a (counter) example from the trace of a failed elimination *) |
|
206 |
(* ------------------------------------------------------------------------- *) |
|
207 |
(* Examples are represented as rational numbers, *) |
|
208 |
(* Dont blame John Harrison for this code - it is entirely mine. TN *) |
|
209 |
||
210 |
exception NoEx; |
|
211 |
||
14372
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
212 |
(* Coding: (i,true,cs) means i <= cs and (i,false,cs) means i < cs. |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
213 |
In general, true means the bound is included, false means it is excluded. |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
214 |
Need to know if it is a lower or upper bound for unambiguous interpretation! |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
215 |
*) |
51ddf8963c95
Finally fixed the counterexample finder. Can now deal with < on real.
nipkow
parents:
14360
diff
changeset
|
216 |
|
13498 | 217 |
(* ------------------------------------------------------------------------- *) |
23197 | 218 |
(* End of counterexample finder. The actual decision procedure starts here. *) |
13498 | 219 |
(* ------------------------------------------------------------------------- *) |
220 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
221 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
222 |
(* Calculate new (in)equality type after addition. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
223 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
224 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
225 |
fun find_add_type(Eq,x) = x |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
226 |
| find_add_type(x,Eq) = x |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
227 |
| find_add_type(_,Lt) = Lt |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
228 |
| find_add_type(Lt,_) = Lt |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
229 |
| find_add_type(Le,Le) = Le; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
230 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
231 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
232 |
(* Multiply out an (in)equation. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
233 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
234 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
235 |
fun multiply_ineq n (i as Lineq(k,ty,l,just)) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
236 |
if n = 1 then i |
40316
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
38763
diff
changeset
|
237 |
else if n = 0 andalso ty = Lt then raise Fail "multiply_ineq" |
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
38763
diff
changeset
|
238 |
else if n < 0 andalso (ty=Le orelse ty=Lt) then raise Fail "multiply_ineq" |
33002 | 239 |
else Lineq (n * k, ty, map (Integer.mult n) l, Multiplied (n, just)); |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
240 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
241 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
242 |
(* Add together (in)equations. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
243 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
244 |
|
38052 | 245 |
fun add_ineq (Lineq (k1,ty1,l1,just1)) (Lineq (k2,ty2,l2,just2)) = |
33002 | 246 |
let val l = map2 Integer.add l1 l2 |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
247 |
in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
248 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
249 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
250 |
(* Elimination of variable between a single pair of (in)equations. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
251 |
(* If they're both inequalities, 1st coefficient must be +ve, 2nd -ve. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
252 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
253 |
|
49387 | 254 |
fun elim_var v (i1 as Lineq(_,ty1,l1,_)) (i2 as Lineq(_,ty2,l2,_)) = |
23063 | 255 |
let val c1 = nth l1 v and c2 = nth l2 v |
63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
63201
diff
changeset
|
256 |
val m = Integer.lcm c1 c2 |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
257 |
val m1 = m div (abs c1) and m2 = m div (abs c2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
258 |
val (n1,n2) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
259 |
if (c1 >= 0) = (c2 >= 0) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
260 |
then if ty1 = Eq then (~m1,m2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
261 |
else if ty2 = Eq then (m1,~m2) |
40316
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
38763
diff
changeset
|
262 |
else raise Fail "elim_var" |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
263 |
else (m1,m2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
264 |
val (p1,p2) = if ty1=Eq andalso ty2=Eq andalso (n1 = ~1 orelse n2 = ~1) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
265 |
then (~n1,~n2) else (n1,n2) |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
266 |
in add_ineq (multiply_ineq p1 i1) (multiply_ineq p2 i2) end; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
267 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
268 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
269 |
(* The main refutation-finding code. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
270 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
271 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
272 |
fun is_trivial (Lineq(_,_,l,_)) = forall (fn i => i=0) l; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
273 |
|
38052 | 274 |
fun is_contradictory (Lineq(k,ty,_,_)) = |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
275 |
case ty of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
276 |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset
|
277 |
fun calc_blowup l = |
33317 | 278 |
let val (p,n) = List.partition (curry (op <) 0) (filter (curry (op <>) 0) l) |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset
|
279 |
in length p * length n end; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
280 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
281 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
282 |
(* Main elimination code: *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
283 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
284 |
(* (1) Looks for immediate solutions (false assertions with no variables). *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
285 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
286 |
(* (2) If there are any equations, picks a variable with the lowest absolute *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
287 |
(* coefficient in any of them, and uses it to eliminate. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
288 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
289 |
(* (3) Otherwise, chooses a variable in the inequality to minimize the *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
290 |
(* blowup (number of consequences generated) and eliminates it. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
291 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
292 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
293 |
fun extract_first p = |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
294 |
let |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
295 |
fun extract xs (y::ys) = if p y then (y, xs @ ys) else extract (y::xs) ys |
66035
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
296 |
| extract _ [] = raise List.Empty |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
297 |
in extract [] end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
298 |
|
44654 | 299 |
fun print_ineqs ctxt ineqs = |
300 |
if Config.get ctxt LA_Data.trace then |
|
12262 | 301 |
tracing(cat_lines(""::map (fn Lineq(c,t,l,_) => |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset
|
302 |
string_of_int c ^ |
9073 | 303 |
(case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^ |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24112
diff
changeset
|
304 |
commas(map string_of_int l)) ineqs)) |
9073 | 305 |
else (); |
6056 | 306 |
|
13498 | 307 |
type history = (int * lineq list) list; |
308 |
datatype result = Success of injust | Failure of history; |
|
309 |
||
44654 | 310 |
fun elim ctxt (ineqs, hist) = |
311 |
let val _ = print_ineqs ctxt ineqs |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
312 |
val (triv, nontriv) = List.partition is_trivial ineqs in |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
313 |
if not (null triv) |
59584 | 314 |
then case find_first is_contradictory triv of |
44654 | 315 |
NONE => elim ctxt (nontriv, hist) |
15531 | 316 |
| SOME(Lineq(_,_,_,j)) => Success j |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
317 |
else |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
318 |
if null nontriv then Failure hist |
13498 | 319 |
else |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
320 |
let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
321 |
if not (null eqs) then |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
322 |
let val c = |
33042 | 323 |
fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs [] |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
324 |
|> filter (fn i => i <> 0) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58839
diff
changeset
|
325 |
|> sort (int_ord o apply2 abs) |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
326 |
|> hd |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
327 |
val (eq as Lineq(_,_,ceq,_),othereqs) = |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
35872
diff
changeset
|
328 |
extract_first (fn Lineq(_,_,l,_) => member (op =) l c) eqs |
31986 | 329 |
val v = find_index (fn v => v = c) ceq |
23063 | 330 |
val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
331 |
(othereqs @ noneqs) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
332 |
val others = map (elim_var v eq) roth @ ioth |
44654 | 333 |
in elim ctxt (others,(v,nontriv)::hist) end |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
334 |
else |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
335 |
let val lists = map (fn (Lineq(_,_,l,_)) => l) noneqs |
23063 | 336 |
val numlist = 0 upto (length (hd lists) - 1) |
337 |
val coeffs = map (fn i => map (fn xs => nth xs i) lists) numlist |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
338 |
val blows = map calc_blowup coeffs |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
339 |
val iblows = blows ~~ numlist |
23063 | 340 |
val nziblows = filter_out (fn (i, _) => i = 0) iblows |
13498 | 341 |
in if null nziblows then Failure((~1,nontriv)::hist) |
342 |
else |
|
60348 | 343 |
let val (_,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows) |
23063 | 344 |
val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ineqs |
345 |
val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => nth l v > 0) yes |
|
44654 | 346 |
in elim ctxt (no @ map_product (elim_var v) pos neg, (v,nontriv)::hist) end |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
347 |
end |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
348 |
end |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
349 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
350 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
351 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
352 |
(* Translate back a proof. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
353 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
354 |
|
44654 | 355 |
fun trace_thm ctxt msgs th = |
356 |
(if Config.get ctxt LA_Data.trace |
|
61268 | 357 |
then tracing (cat_lines (msgs @ [Thm.string_of_thm ctxt th])) |
44654 | 358 |
else (); th); |
9073 | 359 |
|
44654 | 360 |
fun trace_term ctxt msgs t = |
361 |
(if Config.get ctxt LA_Data.trace |
|
362 |
then tracing (cat_lines (msgs @ [Syntax.string_of_term ctxt t])) |
|
363 |
else (); t); |
|
24076 | 364 |
|
44654 | 365 |
fun trace_msg ctxt msg = |
366 |
if Config.get ctxt LA_Data.trace then tracing msg else (); |
|
9073 | 367 |
|
52131 | 368 |
val union_term = union Envir.aeconv; |
26835
404550067389
Lookup and union operations on terms are now modulo eta conversion.
berghofe
parents:
24920
diff
changeset
|
369 |
|
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
370 |
fun add_atoms (lhs, _, _, rhs, _, _) = |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
371 |
union_term (map fst lhs) o union_term (map fst rhs); |
6056 | 372 |
|
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
373 |
fun atoms_of ds = fold add_atoms ds []; |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
374 |
|
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
375 |
(* |
6056 | 376 |
Simplification may detect a contradiction 'prematurely' due to type |
377 |
information: n+1 <= 0 is simplified to False and does not need to be crossed |
|
378 |
with 0 <= n. |
|
379 |
*) |
|
380 |
local |
|
66035
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
381 |
exception FalseE of thm * (int * cterm) list * Proof.context |
6056 | 382 |
in |
27020
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset
|
383 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
384 |
fun mkthm ctxt asms (just: injust) = |
24076 | 385 |
let |
42361 | 386 |
val thy = Proof_Context.theory_of ctxt; |
61097 | 387 |
val {add_mono_thms = add_mono_thms0, mult_mono_thms = mult_mono_thms0, |
388 |
inj_thms = inj_thms0, lessD = lessD0, simpset, ...} = get_data ctxt; |
|
389 |
val add_mono_thms = map (Thm.transfer thy) add_mono_thms0; |
|
390 |
val mult_mono_thms = map (Thm.transfer thy) mult_mono_thms0; |
|
391 |
val inj_thms = map (Thm.transfer thy) inj_thms0; |
|
392 |
val lessD = map (Thm.transfer thy) lessD0; |
|
393 |
||
38763
283f1f9969ba
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
wenzelm
parents:
38762
diff
changeset
|
394 |
val number_of = number_of ctxt; |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
395 |
val simpset_ctxt = put_simpset simpset ctxt; |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
396 |
fun only_concl f thm = |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
397 |
if Thm.no_prems thm then f (Thm.concl_of thm) else NONE; |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
398 |
val atoms = atoms_of (map_filter (only_concl (LA_Data.decomp ctxt)) asms); |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
399 |
|
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
400 |
fun use_first rules thm = |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
401 |
get_first (fn th => SOME (thm RS th) handle THM _ => NONE) rules |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
402 |
|
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
403 |
fun add2 thm1 thm2 = |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
404 |
use_first add_mono_thms (thm1 RS (thm2 RS LA_Logic.conjI)); |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
405 |
fun try_add thms thm = get_first (fn th => add2 th thm) thms; |
6056 | 406 |
|
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
407 |
fun add_thms thm1 thm2 = |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
408 |
(case add2 thm1 thm2 of |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
409 |
NONE => |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
410 |
(case try_add ([thm1] RL inj_thms) thm2 of |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
411 |
NONE => |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
412 |
(the (try_add ([thm2] RL inj_thms) thm1) |
51930
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents:
51717
diff
changeset
|
413 |
handle Option.Option => |
44654 | 414 |
(trace_thm ctxt [] thm1; trace_thm ctxt [] thm2; |
40316
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
38763
diff
changeset
|
415 |
raise Fail "Linear arithmetic: failed to add thms")) |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
416 |
| SOME thm => thm) |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
417 |
| SOME thm => thm); |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
418 |
|
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
419 |
fun mult_by_add n thm = |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
420 |
let fun mul i th = if i = 1 then th else mul (i - 1) (add_thms thm th) |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
421 |
in mul n thm end; |
10575 | 422 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
423 |
val rewr = Simplifier.rewrite simpset_ctxt; |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
424 |
val rewrite_concl = Conv.fconv_rule (Conv.concl_conv ~1 (Conv.arg_conv |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
425 |
(Conv.binop_conv rewr))); |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
426 |
fun discharge_prem thm = if Thm.nprems_of thm = 0 then thm else |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
427 |
let val cv = Conv.arg1_conv (Conv.arg_conv rewr) |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
428 |
in Thm.implies_elim (Conv.fconv_rule cv thm) LA_Logic.trueI end |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
429 |
|
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
430 |
fun mult n thm = |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
431 |
(case use_first mult_mono_thms thm of |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
432 |
NONE => mult_by_add n thm |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
433 |
| SOME mth => |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
434 |
let |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
435 |
val cv = mth |> Thm.cprop_of |> Drule.strip_imp_concl |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
436 |
|> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg1 |
59586 | 437 |
val T = Thm.typ_of_cterm cv |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
438 |
in |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
439 |
mth |
74282 | 440 |
|> Thm.instantiate (TVars.empty, Vars.make [(dest_Var (Thm.term_of cv), number_of T n)]) |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
441 |
|> rewrite_concl |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
442 |
|> discharge_prem |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
443 |
handle CTERM _ => mult_by_add n thm |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
444 |
| THM _ => mult_by_add n thm |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
445 |
end); |
10691 | 446 |
|
66035
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
447 |
fun mult_thm n thm = |
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
448 |
if n = ~1 then thm RS LA_Logic.sym |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
449 |
else if n < 0 then mult (~n) thm RS LA_Logic.sym |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
450 |
else mult n thm; |
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
451 |
|
66035
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
452 |
fun simp thm (cx as (_, hyps, ctxt')) = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
453 |
let val thm' = trace_thm ctxt ["Simplified:"] (full_simplify simpset_ctxt thm) |
66035
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
454 |
in if LA_Logic.is_False thm' then raise FalseE (thm', hyps, ctxt') else (thm', cx) end; |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
455 |
|
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
456 |
fun abs_thm i (cx as (terms, hyps, ctxt)) = |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
457 |
(case AList.lookup (op =) hyps i of |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
458 |
SOME ct => (Thm.assume ct, cx) |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
459 |
| NONE => |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
460 |
let |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
461 |
val thm = nth asms i |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
462 |
val (t, (terms', ctxt')) = LA_Data.abstract (Thm.prop_of thm) (terms, ctxt) |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
463 |
val ct = Thm.cterm_of ctxt' t |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
464 |
in (Thm.assume ct, (terms', (i, ct) :: hyps, ctxt')) end); |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
465 |
|
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
466 |
fun nat_thm t (terms, hyps, ctxt) = |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
467 |
let val (t', (terms', ctxt')) = LA_Data.abstract_arith t (terms, ctxt) |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
468 |
in (LA_Logic.mk_nat_thm thy t', (terms', hyps, ctxt')) end; |
6056 | 469 |
|
66035
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
470 |
fun step0 msg (thm, cx) = (trace_thm ctxt [msg] thm, cx) |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
471 |
fun step1 msg j f cx = mk j cx |>> f |>> trace_thm ctxt [msg] |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
472 |
and step2 msg j1 j2 f cx = mk j1 cx ||>> mk j2 |>> f |>> trace_thm ctxt [msg] |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
473 |
|
66035
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
474 |
and mk (Asm i) cx = step0 ("Asm " ^ string_of_int i) (abs_thm i cx) |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
475 |
| mk (Nat i) cx = step0 ("Nat " ^ string_of_int i) (nat_thm (nth atoms i) cx) |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
476 |
| mk (LessD j) cx = step1 "L" j (fn thm => hd ([thm] RL lessD)) cx |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
477 |
| mk (NotLeD j) cx = step1 "NLe" j (fn thm => thm RS LA_Logic.not_leD) cx |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
478 |
| mk (NotLeDD j) cx = step1 "NLeD" j (fn thm => hd ([thm RS LA_Logic.not_leD] RL lessD)) cx |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
479 |
| mk (NotLessD j) cx = step1 "NL" j (fn thm => thm RS LA_Logic.not_lessD) cx |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
480 |
| mk (Added (j1, j2)) cx = step2 "+" j1 j2 (uncurry add_thms) cx |-> simp |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
481 |
| mk (Multiplied (n, j)) cx = |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
482 |
(trace_msg ctxt ("*" ^ string_of_int n); step1 "*" j (mult_thm n) cx) |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
483 |
|
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
484 |
fun finish ctxt' hyps thm = |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
485 |
thm |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
486 |
|> fold_rev (Thm.implies_intr o snd) hyps |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
487 |
|> singleton (Variable.export ctxt' ctxt) |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
488 |
|> fold (fn (i, _) => fn thm => nth asms i RS thm) hyps |
27020
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset
|
489 |
in |
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset
|
490 |
let |
44654 | 491 |
val _ = trace_msg ctxt "mkthm"; |
66035
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
492 |
val (thm, (_, hyps, ctxt')) = mk just ([], [], ctxt); |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
493 |
val _ = trace_thm ctxt ["Final thm:"] thm; |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
494 |
val fls = simplify simpset_ctxt thm; |
44654 | 495 |
val _ = trace_thm ctxt ["After simplification:"] fls; |
27020
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset
|
496 |
val _ = |
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset
|
497 |
if LA_Logic.is_False fls then () |
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset
|
498 |
else |
35872
9b579860d59b
removed warning_count (known causes for warnings have been resolved)
boehmes
parents:
35861
diff
changeset
|
499 |
(tracing (cat_lines |
61268 | 500 |
(["Assumptions:"] @ map (Thm.string_of_thm ctxt) asms @ [""] @ |
501 |
["Proved:", Thm.string_of_thm ctxt fls, ""])); |
|
35872
9b579860d59b
removed warning_count (known causes for warnings have been resolved)
boehmes
parents:
35861
diff
changeset
|
502 |
warning "Linear arithmetic should have refuted the assumptions.\n\ |
9b579860d59b
removed warning_count (known causes for warnings have been resolved)
boehmes
parents:
35861
diff
changeset
|
503 |
\Please inform Tobias Nipkow.") |
66035
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
504 |
in finish ctxt' hyps fls end |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
505 |
handle FalseE (thm, hyps, ctxt') => |
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
506 |
trace_thm ctxt ["False reached early:"] (finish ctxt' hyps thm) |
27020
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset
|
507 |
end; |
b5b8afc9fdcd
added warning_count for issued reconstruction failure messages (limit 10);
wenzelm
parents:
26945
diff
changeset
|
508 |
|
6056 | 509 |
end; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
510 |
|
23261 | 511 |
fun coeff poly atom = |
52131 | 512 |
AList.lookup Envir.aeconv poly atom |> the_default 0; |
10691 | 513 |
|
514 |
fun integ(rlhs,r,rel,rrhs,s,d) = |
|
63201 | 515 |
let val (rn,rd) = Rat.dest r and (sn,sd) = Rat.dest s |
63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
63201
diff
changeset
|
516 |
val m = Integer.lcms(map (snd o Rat.dest) (r :: s :: map snd rlhs @ map snd rrhs)) |
22846 | 517 |
fun mult(t,r) = |
63201 | 518 |
let val (i,j) = Rat.dest r |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15922
diff
changeset
|
519 |
in (t,i * (m div j)) end |
12932 | 520 |
in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end |
10691 | 521 |
|
38052 | 522 |
fun mklineq atoms = |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
523 |
fn (item, k) => |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
524 |
let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item |
13498 | 525 |
val lhsa = map (coeff lhs) atoms |
526 |
and rhsa = map (coeff rhs) atoms |
|
18330 | 527 |
val diff = map2 (curry (op -)) rhsa lhsa |
13498 | 528 |
val c = i-j |
529 |
val just = Asm k |
|
31511 | 530 |
fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied(m,j)) |
13498 | 531 |
in case rel of |
532 |
"<=" => lineq(c,Le,diff,just) |
|
533 |
| "~<=" => if discrete |
|
534 |
then lineq(1-c,Le,map (op ~) diff,NotLeDD(just)) |
|
535 |
else lineq(~c,Lt,map (op ~) diff,NotLeD(just)) |
|
536 |
| "<" => if discrete |
|
537 |
then lineq(c+1,Le,diff,LessD(just)) |
|
538 |
else lineq(c,Lt,diff,just) |
|
539 |
| "~<" => lineq(~c,Le,map (op~) diff,NotLessD(just)) |
|
540 |
| "=" => lineq(c,Eq,diff,just) |
|
40316
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
38763
diff
changeset
|
541 |
| _ => raise Fail ("mklineq" ^ rel) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
542 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
543 |
|
13498 | 544 |
(* ------------------------------------------------------------------------- *) |
545 |
(* Print (counter) example *) |
|
546 |
(* ------------------------------------------------------------------------- *) |
|
547 |
||
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
548 |
(* ------------------------------------------------------------------------- *) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
549 |
|
20268 | 550 |
fun mknat (pTs : typ list) (ixs : int list) (atom : term, i : int) : lineq option = |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
551 |
if LA_Logic.is_nat (pTs, atom) |
6056 | 552 |
then let val l = map (fn j => if j=i then 1 else 0) ixs |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
553 |
in SOME (Lineq (0, Le, l, Nat i)) end |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
554 |
else NONE; |
6056 | 555 |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
556 |
(* This code is tricky. It takes a list of premises in the order they occur |
15531 | 557 |
in the subgoal. Numerical premises are coded as SOME(tuple), non-numerical |
558 |
ones as NONE. Going through the premises, each numeric one is converted into |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
559 |
a Lineq. The tricky bit is to convert ~= which is split into two cases < and |
13498 | 560 |
>. Thus split_items returns a list of equation systems. This may blow up if |
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
561 |
there are many ~=, but in practice it does not seem to happen. The really |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
562 |
tricky bit is to arrange the order of the cases such that they coincide with |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
563 |
the order in which the cases are in the end generated by the tactic that |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
564 |
applies the generated refutation thms (see function 'refute_tac'). |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
565 |
|
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
566 |
For variables n of type nat, a constraint 0 <= n is added. |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
567 |
*) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
568 |
|
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
569 |
(* FIXME: To optimize, the splitting of cases and the search for refutations *) |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
570 |
(* could be intertwined: separate the first (fully split) case, *) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
571 |
(* refute it, continue with splitting and refuting. Terminate with *) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
572 |
(* failure as soon as a case could not be refuted; i.e. delay further *) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
573 |
(* splitting until after a refutation for other cases has been found. *) |
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
574 |
|
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
575 |
fun split_items ctxt do_pre split_neq (Ts, terms) : (typ list * (LA_Data.decomp * int) list) list = |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
576 |
let |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
577 |
(* splits inequalities '~=' into '<' and '>'; this corresponds to *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
578 |
(* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
579 |
(* level *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
580 |
(* FIXME: this is currently sensitive to the order of theorems in *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
581 |
(* neqE: The theorem for type "nat" must come first. A *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
582 |
(* better (i.e. less likely to break when neqE changes) *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
583 |
(* implementation should *test* which theorem from neqE *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
584 |
(* can be applied, and split the premise accordingly. *) |
26945 | 585 |
fun elim_neq (ineqs : (LA_Data.decomp option * bool) list) : |
586 |
(LA_Data.decomp option * bool) list list = |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
587 |
let |
66035
de6cd60b1226
replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
boehmes
parents:
63227
diff
changeset
|
588 |
fun elim_neq' _ ([] : (LA_Data.decomp option * bool) list) : |
26945 | 589 |
(LA_Data.decomp option * bool) list list = |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
590 |
[[]] |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
591 |
| elim_neq' nat_only ((NONE, is_nat) :: ineqs) = |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
592 |
map (cons (NONE, is_nat)) (elim_neq' nat_only ineqs) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
593 |
| elim_neq' nat_only ((ineq as (SOME (l, i, rel, r, j, d), is_nat)) :: ineqs) = |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
594 |
if rel = "~=" andalso (not nat_only orelse is_nat) then |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
595 |
(* [| ?l ~= ?r; ?l < ?r ==> ?R; ?r < ?l ==> ?R |] ==> ?R *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
596 |
elim_neq' nat_only (ineqs @ [(SOME (l, i, "<", r, j, d), is_nat)]) @ |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
597 |
elim_neq' nat_only (ineqs @ [(SOME (r, j, "<", l, i, d), is_nat)]) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
598 |
else |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
599 |
map (cons ineq) (elim_neq' nat_only ineqs) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
600 |
in |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
601 |
ineqs |> elim_neq' true |
26945 | 602 |
|> maps (elim_neq' false) |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
603 |
end |
13464 | 604 |
|
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
605 |
fun ignore_neq (NONE, bool) = (NONE, bool) |
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
606 |
| ignore_neq (ineq as SOME (_, _, rel, _, _, _), bool) = |
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
607 |
if rel = "~=" then (NONE, bool) else (ineq, bool) |
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
608 |
|
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
609 |
fun number_hyps _ [] = [] |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
610 |
| number_hyps n (NONE::xs) = number_hyps (n+1) xs |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
611 |
| number_hyps n ((SOME x)::xs) = (x, n) :: number_hyps (n+1) xs |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
612 |
|
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
613 |
val result = (Ts, terms) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
614 |
|> (* user-defined preprocessing of the subgoal *) |
24076 | 615 |
(if do_pre then LA_Data.pre_decomp ctxt else Library.single) |
44654 | 616 |
|> tap (fn subgoals => trace_msg ctxt ("Preprocessing yields " ^ |
23195 | 617 |
string_of_int (length subgoals) ^ " subgoal(s) total.")) |
22846 | 618 |
|> (* produce the internal encoding of (in-)equalities *) |
24076 | 619 |
map (apsnd (map (fn t => (LA_Data.decomp ctxt t, LA_Data.domain_is_nat t)))) |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
620 |
|> (* splitting of inequalities *) |
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
621 |
map (apsnd (if split_neq then elim_neq else |
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
622 |
Library.single o map ignore_neq)) |
22846 | 623 |
|> maps (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals) |
20276
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
624 |
|> (* numbering of hypotheses, ignoring irrelevant ones *) |
d94dc40673b1
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
webertj
parents:
20268
diff
changeset
|
625 |
map (apsnd (number_hyps 0)) |
23195 | 626 |
in |
44654 | 627 |
trace_msg ctxt ("Splitting of inequalities yields " ^ |
23195 | 628 |
string_of_int (length result) ^ " subgoal(s) total."); |
629 |
result |
|
630 |
end; |
|
13464 | 631 |
|
59656 | 632 |
fun refutes ctxt : |
26945 | 633 |
(typ list * (LA_Data.decomp * int) list) list -> injust list -> injust list option = |
634 |
let |
|
635 |
fun refute ((Ts, initems : (LA_Data.decomp * int) list) :: initemss) (js: injust list) = |
|
636 |
let |
|
31510
e0f2bb4b0021
fast_lin_arith uses proper multiplication instead of unfolding to additions
boehmes
parents:
31102
diff
changeset
|
637 |
val atoms = atoms_of (map fst initems) |
26945 | 638 |
val n = length atoms |
38052 | 639 |
val mkleq = mklineq atoms |
26945 | 640 |
val ixs = 0 upto (n - 1) |
641 |
val iatoms = atoms ~~ ixs |
|
32952 | 642 |
val natlineqs = map_filter (mknat Ts ixs) iatoms |
26945 | 643 |
val ineqs = map mkleq initems @ natlineqs |
59656 | 644 |
in |
645 |
(case elim ctxt (ineqs, []) of |
|
26945 | 646 |
Success j => |
44654 | 647 |
(trace_msg ctxt ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")"); |
26945 | 648 |
refute initemss (js @ [j])) |
59656 | 649 |
| Failure _ => NONE) |
26945 | 650 |
end |
651 |
| refute [] js = SOME js |
|
652 |
in refute end; |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
653 |
|
59656 | 654 |
fun refute ctxt params do_pre split_neq terms : injust list option = |
655 |
refutes ctxt (split_items ctxt do_pre split_neq (map snd params, terms)) []; |
|
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
656 |
|
22950 | 657 |
fun count P xs = length (filter P xs); |
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
658 |
|
59656 | 659 |
fun prove ctxt params do_pre Hs concl : bool * injust list option = |
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
660 |
let |
44654 | 661 |
val _ = trace_msg ctxt "prove:" |
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
662 |
(* append the negated conclusion to 'Hs' -- this corresponds to *) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
663 |
(* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
664 |
(* theorem/tactic level *) |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
665 |
val Hs' = Hs @ [LA_Logic.neg_prop concl] |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
666 |
fun is_neq NONE = false |
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
667 |
| is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") |
44654 | 668 |
val neq_limit = Config.get ctxt LA_Data.neq_limit |
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
669 |
val split_neq = count is_neq (map (LA_Data.decomp ctxt) Hs') <= neq_limit |
20254
58b71535ed00
lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents:
20217
diff
changeset
|
670 |
in |
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
671 |
if split_neq then () |
24076 | 672 |
else |
44654 | 673 |
trace_msg ctxt ("neq_limit exceeded (current value is " ^ |
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
674 |
string_of_int neq_limit ^ "), ignoring all inequalities"); |
59656 | 675 |
(split_neq, refute ctxt params do_pre split_neq Hs') |
23190 | 676 |
end handle TERM ("neg_prop", _) => |
677 |
(* since no meta-logic negation is available, we can only fail if *) |
|
678 |
(* the conclusion is not of the form 'Trueprop $ _' (simply *) |
|
679 |
(* dropping the conclusion doesn't work either, because even *) |
|
680 |
(* 'False' does not imply arbitrary 'concl::prop') *) |
|
44654 | 681 |
(trace_msg ctxt "prove failed (cannot negate conclusion)."; |
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
682 |
(false, NONE)); |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
683 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
684 |
fun refute_tac ctxt (i, split_neq, justs) = |
6074 | 685 |
fn state => |
24076 | 686 |
let |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset
|
687 |
val _ = trace_thm ctxt |
44654 | 688 |
["refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^ |
689 |
string_of_int (length justs) ^ " justification(s)):"] state |
|
61097 | 690 |
val neqE = get_neqE ctxt; |
24076 | 691 |
fun just1 j = |
692 |
(* eliminate inequalities *) |
|
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
693 |
(if split_neq then |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
694 |
REPEAT_DETERM (eresolve_tac ctxt neqE i) |
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
695 |
else |
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
696 |
all_tac) THEN |
44654 | 697 |
PRIMITIVE (trace_thm ctxt ["State after neqE:"]) THEN |
24076 | 698 |
(* use theorems generated from the actual justifications *) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
699 |
Subgoal.FOCUS (fn {prems, ...} => resolve_tac ctxt [mkthm ctxt prems j] 1) ctxt i |
24076 | 700 |
in |
701 |
(* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
702 |
DETERM (resolve_tac ctxt [LA_Logic.notI, LA_Logic.ccontr] i) THEN |
24076 | 703 |
(* user-defined preprocessing of the subgoal *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
704 |
DETERM (LA_Data.pre_tac ctxt i) THEN |
44654 | 705 |
PRIMITIVE (trace_thm ctxt ["State after pre_tac:"]) THEN |
24076 | 706 |
(* prove every resulting subgoal, using its justification *) |
707 |
EVERY (map just1 justs) |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19618
diff
changeset
|
708 |
end state; |
6074 | 709 |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
710 |
(* |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
711 |
Fast but very incomplete decider. Only premises and conclusions |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
712 |
that are already (negated) (in)equations are taken into account. |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
713 |
*) |
59656 | 714 |
fun simpset_lin_arith_tac ctxt = SUBGOAL (fn (A, i) => |
24076 | 715 |
let |
716 |
val params = rev (Logic.strip_params A) |
|
717 |
val Hs = Logic.strip_assums_hyp A |
|
718 |
val concl = Logic.strip_assums_concl A |
|
44654 | 719 |
val _ = trace_term ctxt ["Trying to refute subgoal " ^ string_of_int i] A |
24076 | 720 |
in |
59656 | 721 |
case prove ctxt params true Hs concl of |
44654 | 722 |
(_, NONE) => (trace_msg ctxt "Refutation failed."; no_tac) |
723 |
| (split_neq, SOME js) => (trace_msg ctxt "Refutation succeeded."; |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
724 |
refute_tac ctxt (i, split_neq, js)) |
24076 | 725 |
end); |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
726 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
727 |
fun prems_lin_arith_tac ctxt = |
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61268
diff
changeset
|
728 |
Method.insert_tac ctxt (Simplifier.prems_of ctxt) THEN' |
59656 | 729 |
simpset_lin_arith_tac ctxt; |
17613 | 730 |
|
24076 | 731 |
fun lin_arith_tac ctxt = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
732 |
simpset_lin_arith_tac (empty_simpset ctxt); |
24076 | 733 |
|
734 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
735 |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
736 |
(** Forward proof from theorems **) |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
737 |
|
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
738 |
(* More tricky code. Needs to arrange the proofs of the multiple cases (due |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
739 |
to splits of ~= premises) such that it coincides with the order of the cases |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
740 |
generated by function split_items. *) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
741 |
|
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
742 |
datatype splittree = Tip of thm list |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
743 |
| Spl of thm * cterm * splittree * cterm * splittree; |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
744 |
|
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
745 |
(* "(ct1 ==> ?R) ==> (ct2 ==> ?R) ==> ?R" is taken to (ct1, ct2) *) |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
746 |
|
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
747 |
fun extract (imp : cterm) : cterm * cterm = |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
748 |
let val (Il, r) = Thm.dest_comb imp |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
749 |
val (_, imp1) = Thm.dest_comb Il |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
750 |
val (Ict1, _) = Thm.dest_comb imp1 |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
751 |
val (_, ct1) = Thm.dest_comb Ict1 |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
752 |
val (Ir, _) = Thm.dest_comb r |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
753 |
val (_, Ict2r) = Thm.dest_comb Ir |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
754 |
val (Ict2, _) = Thm.dest_comb Ict2r |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
755 |
val (_, ct2) = Thm.dest_comb Ict2 |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
756 |
in (ct1, ct2) end; |
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
757 |
|
24076 | 758 |
fun splitasms ctxt (asms : thm list) : splittree = |
61097 | 759 |
let val neqE = get_neqE ctxt |
35693
d58a4ac1ca1c
Use same order of neq-elimination as in proof search.
hoelzl
parents:
35230
diff
changeset
|
760 |
fun elim_neq [] (asms', []) = Tip (rev asms') |
d58a4ac1ca1c
Use same order of neq-elimination as in proof search.
hoelzl
parents:
35230
diff
changeset
|
761 |
| elim_neq [] (asms', asms) = Tip (rev asms' @ asms) |
49387 | 762 |
| elim_neq (_ :: neqs) (asms', []) = elim_neq neqs ([],rev asms') |
35693
d58a4ac1ca1c
Use same order of neq-elimination as in proof search.
hoelzl
parents:
35230
diff
changeset
|
763 |
| elim_neq (neqs as (neq :: _)) (asms', asm::asms) = |
d58a4ac1ca1c
Use same order of neq-elimination as in proof search.
hoelzl
parents:
35230
diff
changeset
|
764 |
(case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) [neq] of |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
765 |
SOME spl => |
59582 | 766 |
let val (ct1, ct2) = extract (Thm.cprop_of spl) |
36945 | 767 |
val thm1 = Thm.assume ct1 |
768 |
val thm2 = Thm.assume ct2 |
|
35693
d58a4ac1ca1c
Use same order of neq-elimination as in proof search.
hoelzl
parents:
35230
diff
changeset
|
769 |
in Spl (spl, ct1, elim_neq neqs (asms', asms@[thm1]), |
d58a4ac1ca1c
Use same order of neq-elimination as in proof search.
hoelzl
parents:
35230
diff
changeset
|
770 |
ct2, elim_neq neqs (asms', asms@[thm2])) |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
771 |
end |
35693
d58a4ac1ca1c
Use same order of neq-elimination as in proof search.
hoelzl
parents:
35230
diff
changeset
|
772 |
| NONE => elim_neq neqs (asm::asms', asms)) |
d58a4ac1ca1c
Use same order of neq-elimination as in proof search.
hoelzl
parents:
35230
diff
changeset
|
773 |
in elim_neq neqE ([], asms) end; |
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
774 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
775 |
fun fwdproof ctxt (Tip asms : splittree) (j::js : injust list) = (mkthm ctxt asms j, js) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
776 |
| fwdproof ctxt (Spl (thm, ct1, tree1, ct2, tree2)) js = |
24076 | 777 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
778 |
val (thm1, js1) = fwdproof ctxt tree1 js |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
779 |
val (thm2, js2) = fwdproof ctxt tree2 js1 |
36945 | 780 |
val thm1' = Thm.implies_intr ct1 thm1 |
781 |
val thm2' = Thm.implies_intr ct2 thm2 |
|
24076 | 782 |
in (thm2' COMP (thm1' COMP thm), js2) end; |
783 |
(* FIXME needs handle THM _ => NONE ? *) |
|
20433
55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20280
diff
changeset
|
784 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
785 |
fun prover ctxt thms Tconcl (js : injust list) split_neq pos : thm option = |
24076 | 786 |
let |
787 |
val nTconcl = LA_Logic.neg_prop Tconcl |
|
59642 | 788 |
val cnTconcl = Thm.cterm_of ctxt nTconcl |
36945 | 789 |
val nTconclthm = Thm.assume cnTconcl |
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
790 |
val tree = (if split_neq then splitasms ctxt else Tip) (thms @ [nTconclthm]) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
791 |
val (Falsethm, _) = fwdproof ctxt tree js |
24076 | 792 |
val contr = if pos then LA_Logic.ccontr else LA_Logic.notI |
36945 | 793 |
val concl = Thm.implies_intr cnTconcl Falsethm COMP contr |
44654 | 794 |
in SOME (trace_thm ctxt ["Proved by lin. arith. prover:"] (LA_Logic.mk_Eq concl)) end |
24076 | 795 |
(*in case concl contains ?-var, which makes assume fail:*) (* FIXME Variable.import_terms *) |
796 |
handle THM _ => NONE; |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
797 |
|
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
798 |
(* PRE: concl is not negated! |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
799 |
This assumption is OK because |
24076 | 800 |
1. lin_arith_simproc tries both to prove and disprove concl and |
801 |
2. lin_arith_simproc is applied by the Simplifier which |
|
13186
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
802 |
dives into terms and will thus try the non-negated concl anyway. |
ef8ed6adcb38
Big update. Allows case splitting on ~= now (trying both < and >).
nipkow
parents:
13105
diff
changeset
|
803 |
*) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
804 |
fun lin_arith_simproc ctxt concl = |
24076 | 805 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
806 |
val thms = maps LA_Logic.atomize (Simplifier.prems_of ctxt) |
24076 | 807 |
val Hs = map Thm.prop_of thms |
61144 | 808 |
val Tconcl = LA_Logic.mk_Trueprop (Thm.term_of concl) |
24076 | 809 |
in |
59656 | 810 |
case prove ctxt [] false Hs Tconcl of (* concl provable? *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
811 |
(split_neq, SOME js) => prover ctxt thms Tconcl js split_neq true |
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
812 |
| (_, NONE) => |
24076 | 813 |
let val nTconcl = LA_Logic.neg_prop Tconcl in |
59656 | 814 |
case prove ctxt [] false Hs nTconcl of (* ~concl provable? *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49387
diff
changeset
|
815 |
(split_neq, SOME js) => prover ctxt thms nTconcl js split_neq false |
30406
15dc25f8a0e2
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
27020
diff
changeset
|
816 |
| (_, NONE) => NONE |
24076 | 817 |
end |
818 |
end; |
|
6074 | 819 |
|
820 |
end; |