author | wenzelm |
Sat, 08 Jul 2006 12:54:40 +0200 | |
changeset 20052 | 3d4ff822d0b3 |
parent 19277 | f7602e74d948 |
child 20713 | 823967ef47f1 |
permissions | -rw-r--r-- |
13876 | 1 |
(* Title: HOL/Integ/cooper_proof.ML |
2 |
ID: $Id$ |
|
3 |
Author: Amine Chaieb and Tobias Nipkow, TU Muenchen |
|
4 |
||
5 |
File containing the implementation of the proof |
|
6 |
generation for Cooper Algorithm |
|
7 |
*) |
|
8 |
||
14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14877
diff
changeset
|
9 |
|
13876 | 10 |
signature COOPER_PROOF = |
11 |
sig |
|
12 |
val qe_Not : thm |
|
13 |
val qe_conjI : thm |
|
14 |
val qe_disjI : thm |
|
15 |
val qe_impI : thm |
|
16 |
val qe_eqI : thm |
|
17 |
val qe_exI : thm |
|
14877 | 18 |
val list_to_set : typ -> term list -> term |
13876 | 19 |
val qe_get_terms : thm -> term * term |
19250 | 20 |
val cooper_prv : theory -> term -> term -> thm |
21 |
val proof_of_evalc : theory -> term -> thm |
|
22 |
val proof_of_cnnf : theory -> term -> (term -> thm) -> thm |
|
23 |
val proof_of_linform : theory -> string list -> term -> thm |
|
24 |
val proof_of_adjustcoeffeq : theory -> term -> IntInf.int -> term -> thm |
|
25 |
val prove_elementar : theory -> string -> term -> thm |
|
26 |
val thm_of : theory -> (term -> (term list * (thm list -> thm))) -> term -> thm |
|
13876 | 27 |
end; |
28 |
||
29 |
structure CooperProof : COOPER_PROOF = |
|
30 |
struct |
|
31 |
open CooperDec; |
|
32 |
||
20052 | 33 |
val presburger_ss = simpset () |
34 |
addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"]; |
|
13876 | 35 |
|
36 |
val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT; |
|
37 |
||
38 |
(*Theorems that will be used later for the proofgeneration*) |
|
39 |
||
40 |
val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0"; |
|
41 |
val unity_coeff_ex = thm "unity_coeff_ex"; |
|
42 |
||
20052 | 43 |
(* Theorems for proving the adjustment of the coefficients*) |
13876 | 44 |
|
45 |
val ac_lt_eq = thm "ac_lt_eq"; |
|
46 |
val ac_eq_eq = thm "ac_eq_eq"; |
|
47 |
val ac_dvd_eq = thm "ac_dvd_eq"; |
|
48 |
val ac_pi_eq = thm "ac_pi_eq"; |
|
49 |
||
50 |
(* The logical compination of the sythetised properties*) |
|
51 |
val qe_Not = thm "qe_Not"; |
|
52 |
val qe_conjI = thm "qe_conjI"; |
|
53 |
val qe_disjI = thm "qe_disjI"; |
|
54 |
val qe_impI = thm "qe_impI"; |
|
55 |
val qe_eqI = thm "qe_eqI"; |
|
56 |
val qe_exI = thm "qe_exI"; |
|
57 |
val qe_ALLI = thm "qe_ALLI"; |
|
58 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
59 |
(*Modulo D property for Pminusinf an Plusinf *) |
13876 | 60 |
val fm_modd_minf = thm "fm_modd_minf"; |
61 |
val not_dvd_modd_minf = thm "not_dvd_modd_minf"; |
|
62 |
val dvd_modd_minf = thm "dvd_modd_minf"; |
|
63 |
||
64 |
val fm_modd_pinf = thm "fm_modd_pinf"; |
|
65 |
val not_dvd_modd_pinf = thm "not_dvd_modd_pinf"; |
|
66 |
val dvd_modd_pinf = thm "dvd_modd_pinf"; |
|
67 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
68 |
(* the minusinfinity proprty*) |
13876 | 69 |
|
70 |
val fm_eq_minf = thm "fm_eq_minf"; |
|
71 |
val neq_eq_minf = thm "neq_eq_minf"; |
|
72 |
val eq_eq_minf = thm "eq_eq_minf"; |
|
73 |
val le_eq_minf = thm "le_eq_minf"; |
|
74 |
val len_eq_minf = thm "len_eq_minf"; |
|
75 |
val not_dvd_eq_minf = thm "not_dvd_eq_minf"; |
|
76 |
val dvd_eq_minf = thm "dvd_eq_minf"; |
|
77 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
78 |
(* the Plusinfinity proprty*) |
13876 | 79 |
|
80 |
val fm_eq_pinf = thm "fm_eq_pinf"; |
|
81 |
val neq_eq_pinf = thm "neq_eq_pinf"; |
|
82 |
val eq_eq_pinf = thm "eq_eq_pinf"; |
|
83 |
val le_eq_pinf = thm "le_eq_pinf"; |
|
84 |
val len_eq_pinf = thm "len_eq_pinf"; |
|
85 |
val not_dvd_eq_pinf = thm "not_dvd_eq_pinf"; |
|
86 |
val dvd_eq_pinf = thm "dvd_eq_pinf"; |
|
87 |
||
88 |
(*Logical construction of the Property*) |
|
89 |
val eq_minf_conjI = thm "eq_minf_conjI"; |
|
90 |
val eq_minf_disjI = thm "eq_minf_disjI"; |
|
91 |
val modd_minf_disjI = thm "modd_minf_disjI"; |
|
92 |
val modd_minf_conjI = thm "modd_minf_conjI"; |
|
93 |
||
94 |
val eq_pinf_conjI = thm "eq_pinf_conjI"; |
|
95 |
val eq_pinf_disjI = thm "eq_pinf_disjI"; |
|
96 |
val modd_pinf_disjI = thm "modd_pinf_disjI"; |
|
97 |
val modd_pinf_conjI = thm "modd_pinf_conjI"; |
|
98 |
||
99 |
(*Cooper Backwards...*) |
|
100 |
(*Bset*) |
|
101 |
val not_bst_p_fm = thm "not_bst_p_fm"; |
|
102 |
val not_bst_p_ne = thm "not_bst_p_ne"; |
|
103 |
val not_bst_p_eq = thm "not_bst_p_eq"; |
|
104 |
val not_bst_p_gt = thm "not_bst_p_gt"; |
|
105 |
val not_bst_p_lt = thm "not_bst_p_lt"; |
|
106 |
val not_bst_p_ndvd = thm "not_bst_p_ndvd"; |
|
107 |
val not_bst_p_dvd = thm "not_bst_p_dvd"; |
|
108 |
||
109 |
(*Aset*) |
|
110 |
val not_ast_p_fm = thm "not_ast_p_fm"; |
|
111 |
val not_ast_p_ne = thm "not_ast_p_ne"; |
|
112 |
val not_ast_p_eq = thm "not_ast_p_eq"; |
|
113 |
val not_ast_p_gt = thm "not_ast_p_gt"; |
|
114 |
val not_ast_p_lt = thm "not_ast_p_lt"; |
|
115 |
val not_ast_p_ndvd = thm "not_ast_p_ndvd"; |
|
116 |
val not_ast_p_dvd = thm "not_ast_p_dvd"; |
|
117 |
||
118 |
(*Logical construction of the prop*) |
|
119 |
(*Bset*) |
|
120 |
val not_bst_p_conjI = thm "not_bst_p_conjI"; |
|
121 |
val not_bst_p_disjI = thm "not_bst_p_disjI"; |
|
122 |
val not_bst_p_Q_elim = thm "not_bst_p_Q_elim"; |
|
123 |
||
124 |
(*Aset*) |
|
125 |
val not_ast_p_conjI = thm "not_ast_p_conjI"; |
|
126 |
val not_ast_p_disjI = thm "not_ast_p_disjI"; |
|
127 |
val not_ast_p_Q_elim = thm "not_ast_p_Q_elim"; |
|
128 |
||
129 |
(*Cooper*) |
|
130 |
val cppi_eq = thm "cppi_eq"; |
|
131 |
val cpmi_eq = thm "cpmi_eq"; |
|
132 |
||
133 |
(*Others*) |
|
134 |
val simp_from_to = thm "simp_from_to"; |
|
135 |
val P_eqtrue = thm "P_eqtrue"; |
|
136 |
val P_eqfalse = thm "P_eqfalse"; |
|
137 |
||
138 |
(*For Proving NNF*) |
|
139 |
||
140 |
val nnf_nn = thm "nnf_nn"; |
|
141 |
val nnf_im = thm "nnf_im"; |
|
142 |
val nnf_eq = thm "nnf_eq"; |
|
143 |
val nnf_sdj = thm "nnf_sdj"; |
|
144 |
val nnf_ncj = thm "nnf_ncj"; |
|
145 |
val nnf_nim = thm "nnf_nim"; |
|
146 |
val nnf_neq = thm "nnf_neq"; |
|
147 |
val nnf_ndj = thm "nnf_ndj"; |
|
148 |
||
149 |
(*For Proving term linearizition*) |
|
150 |
val linearize_dvd = thm "linearize_dvd"; |
|
151 |
val lf_lt = thm "lf_lt"; |
|
152 |
val lf_eq = thm "lf_eq"; |
|
153 |
val lf_dvd = thm "lf_dvd"; |
|
154 |
||
155 |
||
156 |
(* ------------------------------------------------------------------------- *) |
|
157 |
(*This function norm_zero_one replaces the occurences of Numeral1 and Numeral0*) |
|
158 |
(*Respectively by their abstract representation Const("1",..) and COnst("0",..)*) |
|
159 |
(*this is necessary because the theorems use this representation.*) |
|
160 |
(* This function should be elminated in next versions...*) |
|
161 |
(* ------------------------------------------------------------------------- *) |
|
162 |
||
163 |
fun norm_zero_one fm = case fm of |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
164 |
(Const ("HOL.times",_) $ c $ t) => |
13876 | 165 |
if c = one then (norm_zero_one t) |
166 |
else if (dest_numeral c = ~1) |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
167 |
then (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $ (norm_zero_one t)) |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
168 |
else (HOLogic.mk_binop "HOL.times" (norm_zero_one c,norm_zero_one t)) |
13876 | 169 |
|(node $ rest) => ((norm_zero_one node)$(norm_zero_one rest)) |
170 |
|(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p))) |
|
171 |
|_ => fm; |
|
172 |
||
173 |
(* ------------------------------------------------------------------------- *) |
|
174 |
(*function list to Set, constructs a set containing all elements of a given list.*) |
|
175 |
(* ------------------------------------------------------------------------- *) |
|
176 |
fun list_to_set T1 l = let val T = (HOLogic.mk_setT T1) in |
|
177 |
case l of |
|
178 |
[] => Const ("{}",T) |
|
179 |
|(h::t) => Const("insert", T1 --> (T --> T)) $ h $(list_to_set T1 t) |
|
180 |
end; |
|
181 |
||
182 |
(* ------------------------------------------------------------------------- *) |
|
183 |
(* Returns both sides of an equvalence in the theorem*) |
|
184 |
(* ------------------------------------------------------------------------- *) |
|
185 |
fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end; |
|
186 |
||
187 |
(* ------------------------------------------------------------------------- *) |
|
17985 | 188 |
(*This function proove elementar will be used to generate proofs at |
189 |
runtime*) (*It is thought to prove properties such as a dvd b |
|
190 |
(essentially) that are only to make at runtime.*) |
|
13876 | 191 |
(* ------------------------------------------------------------------------- *) |
17985 | 192 |
fun prove_elementar thy s fm2 = |
20052 | 193 |
Goal.prove (ProofContext.init thy) [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY |
17985 | 194 |
(case s of |
13876 | 195 |
(*"ss" like simplification with simpset*) |
196 |
"ss" => |
|
17985 | 197 |
let val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0,unity_coeff_ex] |
198 |
in [simp_tac ss 1, TRY (simple_arith_tac 1)] end |
|
13876 | 199 |
|
200 |
(*"bl" like blast tactic*) |
|
201 |
(* Is only used in the harrisons like proof procedure *) |
|
17985 | 202 |
| "bl" => [blast_tac HOL_cs 1] |
13876 | 203 |
|
204 |
(*"ed" like Existence disjunctions ...*) |
|
205 |
(* Is only used in the harrisons like proof procedure *) |
|
206 |
| "ed" => |
|
207 |
let |
|
208 |
val ex_disj_tacs = |
|
209 |
let |
|
210 |
val tac1 = EVERY[REPEAT(resolve_tac [disjI1,disjI2] 1), etac exI 1] |
|
211 |
val tac2 = EVERY[etac exE 1, rtac exI 1, |
|
212 |
REPEAT(resolve_tac [disjI1,disjI2] 1), assumption 1] |
|
213 |
in [rtac iffI 1, |
|
214 |
etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1, |
|
215 |
REPEAT(EVERY[etac disjE 1, tac2]), tac2] |
|
216 |
end |
|
17985 | 217 |
in ex_disj_tacs end |
13876 | 218 |
|
17985 | 219 |
| "fa" => [simple_arith_tac 1] |
13876 | 220 |
|
221 |
| "sa" => |
|
17985 | 222 |
let val ss = presburger_ss addsimps zadd_ac |
223 |
in [simp_tac ss 1, TRY (simple_arith_tac 1)] end |
|
15107 | 224 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
225 |
(* like Existance Conjunction *) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
226 |
| "ec" => |
17985 | 227 |
let val ss = presburger_ss addsimps zadd_ac |
228 |
in [simp_tac ss 1, TRY (blast_tac HOL_cs 1)] end |
|
13876 | 229 |
|
230 |
| "ac" => |
|
17985 | 231 |
let val ss = HOL_basic_ss addsimps zadd_ac |
232 |
in [simp_tac ss 1] end |
|
13876 | 233 |
|
234 |
| "lf" => |
|
17985 | 235 |
let val ss = presburger_ss addsimps zadd_ac |
236 |
in [simp_tac ss 1, TRY (simple_arith_tac 1)] end)); |
|
13876 | 237 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
238 |
(*=============================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
239 |
(*-------------------------------------------------------------*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
240 |
(* The new compact model *) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
241 |
(*-------------------------------------------------------------*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
242 |
(*=============================================================*) |
13876 | 243 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
244 |
fun thm_of sg decomp t = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
245 |
let val (ts,recomb) = decomp t |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
246 |
in recomb (map (thm_of sg decomp) ts) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
247 |
end; |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
248 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
249 |
(*==================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
250 |
(* Compact Version for adjustcoeffeq *) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
251 |
(*==================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
252 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
253 |
fun decomp_adjustcoeffeq sg x l fm = case fm of |
19277 | 254 |
(Const("Not",_)$(Const("Orderings.less",_) $(Const("0",_)) $(rt as (Const ("HOL.plus", _)$(Const ("HOL.times",_) $ c $ y ) $z )))) => |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
255 |
let |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
256 |
val m = l div (dest_numeral c) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
257 |
val n = if (x = y) then abs (m) else 1 |
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
258 |
val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x)) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
259 |
val rs = if (x = y) |
19277 | 260 |
then (HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) |
261 |
else HOLogic.mk_binrel "Orderings.less" (zero,linear_sub [] one rt ) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
262 |
val ck = cterm_of sg (mk_numeral n) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
263 |
val cc = cterm_of sg c |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
264 |
val ct = cterm_of sg z |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
265 |
val cx = cterm_of sg y |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
266 |
val pre = prove_elementar sg "lf" |
19277 | 267 |
(HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral n))) |
15531 | 268 |
val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq))) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
269 |
in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
270 |
end |
13876 | 271 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
272 |
|(Const(p,_) $a $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
273 |
c $ y ) $t )) => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
274 |
if (is_arith_rel fm) andalso (x = y) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
275 |
then |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
276 |
let val m = l div (dest_numeral c) |
19277 | 277 |
val k = (if p = "Orderings.less" then abs(m) else m) |
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
278 |
val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div k)*l) ), x)) |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
279 |
val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul k t) )))) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
280 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
281 |
val ck = cterm_of sg (mk_numeral k) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
282 |
val cc = cterm_of sg c |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
283 |
val ct = cterm_of sg t |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
284 |
val cx = cterm_of sg x |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
285 |
val ca = cterm_of sg a |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
286 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
287 |
in |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
288 |
case p of |
19277 | 289 |
"Orderings.less" => |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
290 |
let val pre = prove_elementar sg "lf" |
19277 | 291 |
(HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),(mk_numeral k))) |
15531 | 292 |
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq))) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
293 |
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
294 |
end |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
295 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
296 |
|"op =" => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
297 |
let val pre = prove_elementar sg "lf" |
13876 | 298 |
(HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k)))) |
15531 | 299 |
val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq))) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
300 |
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
301 |
end |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
302 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
303 |
|"Divides.op dvd" => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
304 |
let val pre = prove_elementar sg "lf" |
13876 | 305 |
(HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k)))) |
15531 | 306 |
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq)) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
307 |
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans) |
13876 | 308 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
309 |
end |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
310 |
end |
15531 | 311 |
else ([], fn [] => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] refl) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
312 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
313 |
|( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
314 |
|( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
315 |
|( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI) |
13876 | 316 |
|
15531 | 317 |
|_ => ([], fn [] => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] refl); |
13876 | 318 |
|
14877 | 319 |
fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l); |
320 |
||
321 |
||
322 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
323 |
(*==================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
324 |
(* Finding rho for modd_minusinfinity *) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
325 |
(*==================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
326 |
fun rho_for_modd_minf x dlcm sg fm1 = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
327 |
let |
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset
|
328 |
(*Some certified Terms*) |
13876 | 329 |
|
330 |
val ctrue = cterm_of sg HOLogic.true_const |
|
331 |
val cfalse = cterm_of sg HOLogic.false_const |
|
332 |
val fm = norm_zero_one fm1 |
|
333 |
in case fm1 of |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
334 |
(Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => |
15531 | 335 |
if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf)) |
336 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) |
|
13876 | 337 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
338 |
|(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => |
13876 | 339 |
if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) |
15531 | 340 |
then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) |
341 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) |
|
13876 | 342 |
|
19277 | 343 |
|(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) => |
13876 | 344 |
if (y=x) andalso (c1 = zero) then |
15531 | 345 |
if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else |
346 |
(instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf)) |
|
347 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) |
|
13876 | 348 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
349 |
|Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => |
13876 | 350 |
if y=x then let val cz = cterm_of sg (norm_zero_one z) |
351 |
val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero) |
|
15531 | 352 |
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf))) |
13876 | 353 |
end |
15531 | 354 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) |
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
355 |
|(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ |
13876 | 356 |
c $ y ) $ z))) => |
357 |
if y=x then let val cz = cterm_of sg (norm_zero_one z) |
|
358 |
val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero) |
|
15531 | 359 |
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf))) |
13876 | 360 |
end |
15531 | 361 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) |
13876 | 362 |
|
363 |
||
15531 | 364 |
|_ => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
365 |
end; |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
366 |
(*=========================================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
367 |
(*=========================================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
368 |
fun rho_for_eq_minf x dlcm sg fm1 = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
369 |
let |
13876 | 370 |
val fm = norm_zero_one fm1 |
371 |
in case fm1 of |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
372 |
(Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => |
13876 | 373 |
if (x=y) andalso (c1=zero) andalso (c2=one) |
15531 | 374 |
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf)) |
375 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
|
13876 | 376 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
377 |
|(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => |
13876 | 378 |
if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one)) |
15531 | 379 |
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf)) |
380 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
|
13876 | 381 |
|
19277 | 382 |
|(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) => |
13876 | 383 |
if (y=x) andalso (c1 =zero) then |
15531 | 384 |
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else |
385 |
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf)) |
|
386 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
387 |
|Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => |
13876 | 388 |
if y=x then let val cd = cterm_of sg (norm_zero_one d) |
389 |
val cz = cterm_of sg (norm_zero_one z) |
|
15531 | 390 |
in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_minf)) |
13876 | 391 |
end |
392 |
||
15531 | 393 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
13876 | 394 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
395 |
|(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => |
13876 | 396 |
if y=x then let val cd = cterm_of sg (norm_zero_one d) |
397 |
val cz = cterm_of sg (norm_zero_one z) |
|
15531 | 398 |
in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf)) |
13876 | 399 |
end |
15531 | 400 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
13876 | 401 |
|
402 |
||
15531 | 403 |
|_ => (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) |
13876 | 404 |
end; |
405 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
406 |
(*=====================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
407 |
(*=====================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
408 |
(*=========== minf proofs with the compact version==========*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
409 |
fun decomp_minf_eq x dlcm sg t = case t of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
410 |
Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_conjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
411 |
|Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_disjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
412 |
|_ => ([],fn [] => rho_for_eq_minf x dlcm sg t); |
13876 | 413 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
414 |
fun decomp_minf_modd x dlcm sg t = case t of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
415 |
Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_conjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
416 |
|Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_disjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
417 |
|_ => ([],fn [] => rho_for_modd_minf x dlcm sg t); |
13876 | 418 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
419 |
(* -------------------------------------------------------------*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
420 |
(* Finding rho for pinf_modd *) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
421 |
(* -------------------------------------------------------------*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
422 |
fun rho_for_modd_pinf x dlcm sg fm1 = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
423 |
let |
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset
|
424 |
(*Some certified Terms*) |
13876 | 425 |
|
426 |
val ctrue = cterm_of sg HOLogic.true_const |
|
427 |
val cfalse = cterm_of sg HOLogic.false_const |
|
428 |
val fm = norm_zero_one fm1 |
|
429 |
in case fm1 of |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
430 |
(Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => |
13876 | 431 |
if ((x=y) andalso (c1= zero) andalso (c2= one)) |
15531 | 432 |
then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) |
433 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) |
|
13876 | 434 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
435 |
|(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => |
13876 | 436 |
if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero) andalso (c2 = one)) |
15531 | 437 |
then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf)) |
438 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) |
|
13876 | 439 |
|
19277 | 440 |
|(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) => |
13876 | 441 |
if ((y=x) andalso (c1 = zero)) then |
442 |
if (pm1 = one) |
|
15531 | 443 |
then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) |
444 |
else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf)) |
|
445 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) |
|
13876 | 446 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
447 |
|Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => |
13876 | 448 |
if y=x then let val cz = cterm_of sg (norm_zero_one z) |
449 |
val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero) |
|
15531 | 450 |
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf))) |
13876 | 451 |
end |
15531 | 452 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) |
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
453 |
|(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ |
13876 | 454 |
c $ y ) $ z))) => |
455 |
if y=x then let val cz = cterm_of sg (norm_zero_one z) |
|
456 |
val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero) |
|
15531 | 457 |
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf))) |
13876 | 458 |
end |
15531 | 459 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)) |
13876 | 460 |
|
461 |
||
15531 | 462 |
|_ => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
463 |
end; |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
464 |
(* -------------------------------------------------------------*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
465 |
(* Finding rho for pinf_eq *) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
466 |
(* -------------------------------------------------------------*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
467 |
fun rho_for_eq_pinf x dlcm sg fm1 = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
468 |
let |
13876 | 469 |
val fm = norm_zero_one fm1 |
470 |
in case fm1 of |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
471 |
(Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => |
13876 | 472 |
if (x=y) andalso (c1=zero) andalso (c2=one) |
15531 | 473 |
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf)) |
474 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
|
13876 | 475 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
476 |
|(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => |
13876 | 477 |
if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one)) |
15531 | 478 |
then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf)) |
479 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
|
13876 | 480 |
|
19277 | 481 |
|(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) => |
13876 | 482 |
if (y=x) andalso (c1 =zero) then |
15531 | 483 |
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else |
484 |
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf)) |
|
485 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
486 |
|Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => |
13876 | 487 |
if y=x then let val cd = cterm_of sg (norm_zero_one d) |
488 |
val cz = cterm_of sg (norm_zero_one z) |
|
15531 | 489 |
in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_pinf)) |
13876 | 490 |
end |
491 |
||
15531 | 492 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
13876 | 493 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
494 |
|(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => |
13876 | 495 |
if y=x then let val cd = cterm_of sg (norm_zero_one d) |
496 |
val cz = cterm_of sg (norm_zero_one z) |
|
15531 | 497 |
in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf)) |
13876 | 498 |
end |
15531 | 499 |
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
13876 | 500 |
|
501 |
||
15531 | 502 |
|_ => (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) |
13876 | 503 |
end; |
504 |
||
505 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
506 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
507 |
fun minf_proof_of_c sg x dlcm t = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
508 |
let val minf_eqth = thm_of sg (decomp_minf_eq x dlcm sg) t |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
509 |
val minf_moddth = thm_of sg (decomp_minf_modd x dlcm sg) t |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
510 |
in (minf_eqth, minf_moddth) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
511 |
end; |
13876 | 512 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
513 |
(*=========== pinf proofs with the compact version==========*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
514 |
fun decomp_pinf_eq x dlcm sg t = case t of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
515 |
Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_conjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
516 |
|Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_disjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
517 |
|_ =>([],fn [] => rho_for_eq_pinf x dlcm sg t) ; |
13876 | 518 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
519 |
fun decomp_pinf_modd x dlcm sg t = case t of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
520 |
Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_conjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
521 |
|Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_disjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
522 |
|_ => ([],fn [] => rho_for_modd_pinf x dlcm sg t); |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
523 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
524 |
fun pinf_proof_of_c sg x dlcm t = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
525 |
let val pinf_eqth = thm_of sg (decomp_pinf_eq x dlcm sg) t |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
526 |
val pinf_moddth = thm_of sg (decomp_pinf_modd x dlcm sg) t |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
527 |
in (pinf_eqth,pinf_moddth) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
528 |
end; |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
529 |
|
13876 | 530 |
|
531 |
(* ------------------------------------------------------------------------- *) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
532 |
(* Here we generate the theorem for the Bset Property in the simple direction*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
533 |
(* It is just an instantiation*) |
13876 | 534 |
(* ------------------------------------------------------------------------- *) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
535 |
(* |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
536 |
fun bsetproof_of sg (x as Free(xn,xT)) fm bs dlcm = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
537 |
let |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
538 |
val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
539 |
val cdlcm = cterm_of sg dlcm |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
540 |
val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs)) |
15531 | 541 |
in instantiate' [] [SOME cdlcm,SOME cB, SOME cp] (bst_thm) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
542 |
end; |
13876 | 543 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
544 |
fun asetproof_of sg (x as Free(xn,xT)) fm ast dlcm = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
545 |
let |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
546 |
val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
547 |
val cdlcm = cterm_of sg dlcm |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
548 |
val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast)) |
15531 | 549 |
in instantiate' [] [SOME cdlcm,SOME cA, SOME cp] (ast_thm) |
13876 | 550 |
end; |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
551 |
*) |
13876 | 552 |
|
553 |
(* For the generation of atomic Theorems*) |
|
554 |
(* Prove the premisses on runtime and then make RS*) |
|
555 |
(* ------------------------------------------------------------------------- *) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
556 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
557 |
(*========= this is rho ============*) |
13876 | 558 |
fun generate_atomic_not_bst_p sg (x as Free(xn,xT)) fm dlcm B at = |
559 |
let |
|
560 |
val cdlcm = cterm_of sg dlcm |
|
561 |
val cB = cterm_of sg B |
|
562 |
val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) |
|
563 |
val cat = cterm_of sg (norm_zero_one at) |
|
564 |
in |
|
565 |
case at of |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
566 |
(Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => |
13876 | 567 |
if (x=y) andalso (c1=zero) andalso (c2=one) |
568 |
then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B) |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
569 |
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z))) |
19277 | 570 |
val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm)) |
15531 | 571 |
in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne))) |
13876 | 572 |
end |
15531 | 573 |
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
13876 | 574 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
575 |
|(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) => |
13876 | 576 |
if (is_arith_rel at) andalso (x=y) |
577 |
then let val bst_z = norm_zero_one (linear_neg (linear_add [] z (mk_numeral 1))) |
|
578 |
in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B) |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
579 |
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("HOL.minus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT)))) |
19277 | 580 |
val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm)) |
15531 | 581 |
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq))) |
13876 | 582 |
end |
583 |
end |
|
15531 | 584 |
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
13876 | 585 |
|
19277 | 586 |
|(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) => |
13876 | 587 |
if (y=x) andalso (c1 =zero) then |
588 |
if pm1 = one then |
|
589 |
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B) |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
590 |
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z))) |
15531 | 591 |
in (instantiate' [] [SOME cfma, SOME cdlcm]([th1,th2] MRS (not_bst_p_gt))) |
13876 | 592 |
end |
19277 | 593 |
else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm)) |
15531 | 594 |
in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt))) |
13876 | 595 |
end |
15531 | 596 |
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
13876 | 597 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
598 |
|Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => |
13876 | 599 |
if y=x then |
600 |
let val cz = cterm_of sg (norm_zero_one z) |
|
601 |
val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) |
|
15531 | 602 |
in (instantiate' [] [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd))) |
13876 | 603 |
end |
15531 | 604 |
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
13876 | 605 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
606 |
|(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => |
13876 | 607 |
if y=x then |
608 |
let val cz = cterm_of sg (norm_zero_one z) |
|
609 |
val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) |
|
15531 | 610 |
in (instantiate' [] [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd))) |
13876 | 611 |
end |
15531 | 612 |
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
13876 | 613 |
|
15531 | 614 |
|_ => (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm)) |
13876 | 615 |
|
616 |
end; |
|
617 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
618 |
|
13876 | 619 |
(* ------------------------------------------------------------------------- *) |
620 |
(* Main interpretation function for this backwards dirction*) |
|
621 |
(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*) |
|
622 |
(*Help Function*) |
|
623 |
(* ------------------------------------------------------------------------- *) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
624 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
625 |
(*==================== Proof with the compact version *) |
13876 | 626 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
627 |
fun decomp_nbstp sg x dlcm B fm t = case t of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
628 |
Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_conjI ) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
629 |
|Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_disjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
630 |
|_ => ([], fn [] => generate_atomic_not_bst_p sg x fm dlcm B t); |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
631 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
632 |
fun not_bst_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm B t = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
633 |
let |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
634 |
val th = thm_of sg (decomp_nbstp sg x dlcm (list_to_set xT (map norm_zero_one B)) fm) t |
13876 | 635 |
val fma = absfree (xn,xT, norm_zero_one fm) |
636 |
in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma)) |
|
637 |
in [th,th1] MRS (not_bst_p_Q_elim) |
|
638 |
end |
|
639 |
end; |
|
640 |
||
641 |
||
642 |
(* ------------------------------------------------------------------------- *) |
|
643 |
(* Protokol interpretation function for the backwards direction for cooper's Theorem*) |
|
644 |
||
645 |
(* For the generation of atomic Theorems*) |
|
646 |
(* Prove the premisses on runtime and then make RS*) |
|
647 |
(* ------------------------------------------------------------------------- *) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
648 |
(*========= this is rho ============*) |
13876 | 649 |
fun generate_atomic_not_ast_p sg (x as Free(xn,xT)) fm dlcm A at = |
650 |
let |
|
651 |
val cdlcm = cterm_of sg dlcm |
|
652 |
val cA = cterm_of sg A |
|
653 |
val cfma = cterm_of sg (absfree (xn,xT,(norm_zero_one fm))) |
|
654 |
val cat = cterm_of sg (norm_zero_one at) |
|
655 |
in |
|
656 |
case at of |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
657 |
(Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z))) => |
13876 | 658 |
if (x=y) andalso (c1=zero) andalso (c2=one) |
659 |
then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A) |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
660 |
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z))) |
19277 | 661 |
val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm)) |
15531 | 662 |
in (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne))) |
13876 | 663 |
end |
15531 | 664 |
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
13876 | 665 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
666 |
|(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("HOL.plus", T) $(Const ("HOL.times",_) $ c2 $ y) $z)) => |
13876 | 667 |
if (is_arith_rel at) andalso (x=y) |
668 |
then let val ast_z = norm_zero_one (linear_sub [] one z ) |
|
669 |
val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A) |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
670 |
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("HOL.plus",T) $ (Const("HOL.uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT)))) |
19277 | 671 |
val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm)) |
15531 | 672 |
in (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq))) |
13876 | 673 |
end |
15531 | 674 |
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
13876 | 675 |
|
19277 | 676 |
|(Const("Orderings.less",_) $ c1 $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z )) => |
13876 | 677 |
if (y=x) andalso (c1 =zero) then |
678 |
if pm1 = (mk_numeral ~1) then |
|
679 |
let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A) |
|
19277 | 680 |
val th2 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm)) |
15531 | 681 |
in (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt))) |
13876 | 682 |
end |
19277 | 683 |
else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (Const("0",HOLogic.intT),dlcm)) |
15531 | 684 |
in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt))) |
13876 | 685 |
end |
15531 | 686 |
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
13876 | 687 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
688 |
|Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => |
13876 | 689 |
if y=x then |
690 |
let val cz = cterm_of sg (norm_zero_one z) |
|
691 |
val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) |
|
15531 | 692 |
in (instantiate' [] [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd))) |
13876 | 693 |
end |
15531 | 694 |
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
13876 | 695 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17985
diff
changeset
|
696 |
|(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) => |
13876 | 697 |
if y=x then |
698 |
let val cz = cterm_of sg (norm_zero_one z) |
|
699 |
val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) |
|
15531 | 700 |
in (instantiate' [] [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd))) |
13876 | 701 |
end |
15531 | 702 |
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
13876 | 703 |
|
15531 | 704 |
|_ => (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm)) |
13876 | 705 |
|
706 |
end; |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
707 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
708 |
(* ------------------------------------------------------------------------ *) |
13876 | 709 |
(* Main interpretation function for this backwards dirction*) |
710 |
(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*) |
|
711 |
(*Help Function*) |
|
712 |
(* ------------------------------------------------------------------------- *) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
713 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
714 |
fun decomp_nastp sg x dlcm A fm t = case t of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
715 |
Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_conjI ) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
716 |
|Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_disjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
717 |
|_ => ([], fn [] => generate_atomic_not_ast_p sg x fm dlcm A t); |
13876 | 718 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
719 |
fun not_ast_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm A t = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
720 |
let |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
721 |
val th = thm_of sg (decomp_nastp sg x dlcm (list_to_set xT (map norm_zero_one A)) fm) t |
13876 | 722 |
val fma = absfree (xn,xT, norm_zero_one fm) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
723 |
in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma)) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
724 |
in [th,th1] MRS (not_ast_p_Q_elim) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
725 |
end |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
726 |
end; |
13876 | 727 |
|
728 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
729 |
(* -------------------------------*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
730 |
(* Finding rho and beta for evalc *) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
731 |
(* -------------------------------*) |
13876 | 732 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
733 |
fun rho_for_evalc sg at = case at of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
734 |
(Const (p,_) $ s $ t) =>( |
17485 | 735 |
case AList.lookup (op =) operations p of |
15531 | 736 |
SOME f => |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
737 |
((if (f ((dest_numeral s),(dest_numeral t))) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
738 |
then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
739 |
else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))) |
15531 | 740 |
handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl) |
741 |
| _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl ) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
742 |
|Const("Not",_)$(Const (p,_) $ s $ t) =>( |
17485 | 743 |
case AList.lookup (op =) operations p of |
15531 | 744 |
SOME f => |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
745 |
((if (f ((dest_numeral s),(dest_numeral t))) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
746 |
then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
747 |
else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const))) |
15531 | 748 |
handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl) |
749 |
| _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl ) |
|
750 |
| _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl; |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
751 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
752 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
753 |
(*=========================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
754 |
fun decomp_evalc sg t = case t of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
755 |
(Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
756 |
|(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
757 |
|(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
758 |
|(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
759 |
|_ => ([], fn [] => rho_for_evalc sg t); |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
760 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
761 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
762 |
fun proof_of_evalc sg fm = thm_of sg (decomp_evalc sg) fm; |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
763 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
764 |
(*==================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
765 |
(* Proof of linform with the compact model *) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
766 |
(*==================================================*) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
767 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
768 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
769 |
fun decomp_linform sg vars t = case t of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
770 |
(Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
771 |
|(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
772 |
|(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
773 |
|(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
774 |
|(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not) |
15164 | 775 |
|(Const("Divides.op dvd",_)$d$r) => |
15531 | 776 |
if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd))) |
15164 | 777 |
else (warning "Nonlinear Term --- Non numeral leftside at dvd"; |
778 |
raise COOPER) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
779 |
|_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t))); |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
780 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
781 |
fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f; |
13876 | 782 |
|
783 |
(* ------------------------------------------------------------------------- *) |
|
784 |
(* Interpretaion of Protocols of the cooper procedure : minusinfinity version*) |
|
785 |
(* ------------------------------------------------------------------------- *) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
786 |
fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm = |
13876 | 787 |
(* Get the Bset thm*) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
788 |
let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm |
19277 | 789 |
val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm)); |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
790 |
val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
791 |
in (dpos,minf_eqth,nbstpthm,minf_moddth) |
13876 | 792 |
end; |
793 |
||
794 |
(* ------------------------------------------------------------------------- *) |
|
795 |
(* Interpretaion of Protocols of the cooper procedure : plusinfinity version *) |
|
796 |
(* ------------------------------------------------------------------------- *) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
797 |
fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
798 |
let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm |
19277 | 799 |
val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "Orderings.less" (zero,dlcm)); |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
800 |
val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
801 |
in (dpos,pinf_eqth,nastpthm,pinf_moddth) |
13876 | 802 |
end; |
803 |
||
804 |
(* ------------------------------------------------------------------------- *) |
|
805 |
(* Interpretaion of Protocols of the cooper procedure : full version*) |
|
806 |
(* ------------------------------------------------------------------------- *) |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
807 |
fun cooper_thm sg s (x as Free(xn,xT)) cfm dlcm ast bst= case s of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
808 |
"pi" => let val (dpsthm,pinf_eqth,nbpth,pinf_moddth) = cooperpi_proof_of sg x cfm ast dlcm |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
809 |
in [dpsthm,pinf_eqth,nbpth,pinf_moddth] MRS (cppi_eq) |
13876 | 810 |
end |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
811 |
|"mi" => let val (dpsthm,minf_eqth,nbpth,minf_moddth) = coopermi_proof_of sg x cfm bst dlcm |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
812 |
in [dpsthm,minf_eqth,nbpth,minf_moddth] MRS (cpmi_eq) |
13876 | 813 |
end |
814 |
|_ => error "parameter error"; |
|
815 |
||
816 |
(* ------------------------------------------------------------------------- *) |
|
817 |
(* This function should evoluate to the end prove Procedure for one quantifier elimination for Presburger arithmetic*) |
|
818 |
(* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*) |
|
819 |
(* ------------------------------------------------------------------------- *) |
|
820 |
||
15165 | 821 |
(* val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();*) |
822 |
(* val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer(); *) |
|
15164 | 823 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
824 |
fun cooper_prv sg (x as Free(xn,xT)) efm = let |
14877 | 825 |
(* lfm_thm : efm = linearized form of efm*) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
826 |
val lfm_thm = proof_of_linform sg [xn] efm |
14877 | 827 |
(*efm2 is the linearized form of efm *) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
828 |
val efm2 = snd(qe_get_terms lfm_thm) |
14877 | 829 |
(* l is the lcm of all coefficients of x *) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
830 |
val l = formlcm x efm2 |
14877 | 831 |
(*ac_thm: efm = efm2 with adjusted coefficients of x *) |
832 |
val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans |
|
833 |
(* fm is efm2 with adjusted coefficients of x *) |
|
13876 | 834 |
val fm = snd (qe_get_terms ac_thm) |
14877 | 835 |
(* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*) |
13876 | 836 |
val cfm = unitycoeff x fm |
14877 | 837 |
(*afm is fm where c*x is replaced by 1*x or -1*x *) |
13876 | 838 |
val afm = adjustcoeff x l fm |
14877 | 839 |
(* P = %x.afm*) |
13876 | 840 |
val P = absfree(xn,xT,afm) |
14877 | 841 |
(* This simpset allows the elimination of the sets in bex {1..d} *) |
13876 | 842 |
val ss = presburger_ss addsimps |
843 |
[simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff] |
|
14877 | 844 |
(* uth : EX x.P(l*x) = EX x. l dvd x & P x*) |
15531 | 845 |
val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex) |
14877 | 846 |
(* e_ac_thm : Ex x. efm = EX x. fm*) |
13876 | 847 |
val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI) |
14877 | 848 |
(* A and B set of the formula*) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
849 |
val A = aset x cfm |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
850 |
val B = bset x cfm |
14877 | 851 |
(* the divlcm (delta) of the formula*) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
852 |
val dlcm = mk_numeral (divlcm x cfm) |
14877 | 853 |
(* Which set is smaller to generate the (hoepfully) shorter proof*) |
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
854 |
val cms = if ((length A) < (length B )) then "pi" else "mi" |
15165 | 855 |
(* val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*) |
14877 | 856 |
(* synthesize the proof of cooper's theorem*) |
857 |
(* cp_thm: EX x. cfm = Q*) |
|
15165 | 858 |
val cp_thm = cooper_thm sg cms x cfm dlcm A B |
14877 | 859 |
(* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*) |
860 |
(* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*) |
|
15165 | 861 |
(* |
15164 | 862 |
val _ = prth cp_thm |
863 |
val _ = writeln "Expanding the bounded EX..." |
|
15165 | 864 |
*) |
865 |
val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans))) |
|
866 |
(* |
|
867 |
val _ = writeln "Expanded" *) |
|
14877 | 868 |
(* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*) |
13876 | 869 |
val (lsuth,rsuth) = qe_get_terms (uth) |
14877 | 870 |
(* lseacth = EX x. efm; rseacth = EX x. fm*) |
13876 | 871 |
val (lseacth,rseacth) = qe_get_terms(e_ac_thm) |
14877 | 872 |
(* lscth = EX x. cfm; rscth = Q' *) |
13876 | 873 |
val (lscth,rscth) = qe_get_terms (exp_cp_thm) |
14877 | 874 |
(* u_c_thm: EX x. P(l*x) = Q'*) |
13876 | 875 |
val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans |
14877 | 876 |
(* result: EX x. efm = Q'*) |
13876 | 877 |
in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) |
878 |
end |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
879 |
|cooper_prv _ _ _ = error "Parameters format"; |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
880 |
|
15107 | 881 |
(* **************************************** *) |
882 |
(* An Other Version of cooper proving *) |
|
883 |
(* by giving a withness for EX *) |
|
884 |
(* **************************************** *) |
|
885 |
||
886 |
||
887 |
||
888 |
fun cooper_prv_w sg (x as Free(xn,xT)) efm = let |
|
889 |
(* lfm_thm : efm = linearized form of efm*) |
|
890 |
val lfm_thm = proof_of_linform sg [xn] efm |
|
891 |
(*efm2 is the linearized form of efm *) |
|
892 |
val efm2 = snd(qe_get_terms lfm_thm) |
|
893 |
(* l is the lcm of all coefficients of x *) |
|
894 |
val l = formlcm x efm2 |
|
895 |
(*ac_thm: efm = efm2 with adjusted coefficients of x *) |
|
896 |
val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans |
|
897 |
(* fm is efm2 with adjusted coefficients of x *) |
|
898 |
val fm = snd (qe_get_terms ac_thm) |
|
899 |
(* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*) |
|
900 |
val cfm = unitycoeff x fm |
|
901 |
(*afm is fm where c*x is replaced by 1*x or -1*x *) |
|
902 |
val afm = adjustcoeff x l fm |
|
903 |
(* P = %x.afm*) |
|
904 |
val P = absfree(xn,xT,afm) |
|
905 |
(* This simpset allows the elimination of the sets in bex {1..d} *) |
|
906 |
val ss = presburger_ss addsimps |
|
907 |
[simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff] |
|
908 |
(* uth : EX x.P(l*x) = EX x. l dvd x & P x*) |
|
15531 | 909 |
val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex) |
15107 | 910 |
(* e_ac_thm : Ex x. efm = EX x. fm*) |
911 |
val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI) |
|
912 |
(* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*) |
|
913 |
val (lsuth,rsuth) = qe_get_terms (uth) |
|
914 |
(* lseacth = EX x. efm; rseacth = EX x. fm*) |
|
915 |
val (lseacth,rseacth) = qe_get_terms(e_ac_thm) |
|
916 |
||
917 |
val (w,rs) = cooper_w [] cfm |
|
918 |
val exp_cp_thm = case w of |
|
919 |
(* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*) |
|
15531 | 920 |
SOME n => e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*) |
15107 | 921 |
|_ => let |
922 |
(* A and B set of the formula*) |
|
923 |
val A = aset x cfm |
|
924 |
val B = bset x cfm |
|
925 |
(* the divlcm (delta) of the formula*) |
|
926 |
val dlcm = mk_numeral (divlcm x cfm) |
|
927 |
(* Which set is smaller to generate the (hoepfully) shorter proof*) |
|
928 |
val cms = if ((length A) < (length B )) then "pi" else "mi" |
|
929 |
(* synthesize the proof of cooper's theorem*) |
|
930 |
(* cp_thm: EX x. cfm = Q*) |
|
931 |
val cp_thm = cooper_thm sg cms x cfm dlcm A B |
|
932 |
(* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*) |
|
933 |
(* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*) |
|
934 |
in refl RS (simplify ss (cp_thm RSN (2,trans))) |
|
935 |
end |
|
936 |
(* lscth = EX x. cfm; rscth = Q' *) |
|
937 |
val (lscth,rscth) = qe_get_terms (exp_cp_thm) |
|
938 |
(* u_c_thm: EX x. P(l*x) = Q'*) |
|
939 |
val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans |
|
940 |
(* result: EX x. efm = Q'*) |
|
941 |
in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) |
|
942 |
end |
|
943 |
|cooper_prv_w _ _ _ = error "Parameters format"; |
|
944 |
||
945 |
||
13876 | 946 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
947 |
fun decomp_cnnf sg lfnp P = case P of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
948 |
Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI ) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
949 |
|Const ("op |",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_disjI) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
950 |
|Const ("Not",_) $ (Const("Not",_) $ p) => ([p], fn [th] => th RS nnf_nn) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
951 |
|Const("Not",_) $ (Const(opn,T) $ p $ q) => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
952 |
if opn = "op |" |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
953 |
then case (p,q) of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
954 |
(A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
955 |
if r1 = negate r |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
956 |
then ([r,HOLogic.Not$s,r1,HOLogic.Not$t],fn [th1_1,th1_2,th2_1,th2_2] => [[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj) |
13876 | 957 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
958 |
else ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
959 |
|(_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
960 |
else ( |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
961 |
case (opn,T) of |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
962 |
("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_ncj ) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
963 |
|("op -->",_) => ([p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_nim ) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
964 |
|("op =",Type ("fun",[Type ("bool", []),_])) => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
965 |
([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], fn [th1,th2] => [th1,th2] MRS nnf_neq) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
966 |
|(_,_) => ([], fn [] => lfnp P) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
967 |
) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
968 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
969 |
|(Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], fn [th1,th2] => [th1,th2] MRS nnf_im) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
970 |
|
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
971 |
|(Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) => |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
972 |
([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], fn [th1,th2] =>[th1,th2] MRS nnf_eq ) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
973 |
|_ => ([], fn [] => lfnp P); |
13876 | 974 |
|
975 |
||
976 |
||
977 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
978 |
fun proof_of_cnnf sg p lfnp = |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
979 |
let val th1 = thm_of sg (decomp_cnnf sg lfnp) p |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
980 |
val rs = snd(qe_get_terms th1) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
981 |
val th2 = prove_elementar sg "ss" (HOLogic.mk_eq(rs,simpl rs)) |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
982 |
in [th1,th2] MRS trans |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14479
diff
changeset
|
983 |
end; |
13876 | 984 |
|
985 |
end; |
|
14920
a7525235e20f
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
chaieb
parents:
14877
diff
changeset
|
986 |