equal
deleted
inserted
replaced
28 |
28 |
29 structure CooperProof : COOPER_PROOF = |
29 structure CooperProof : COOPER_PROOF = |
30 struct |
30 struct |
31 open CooperDec; |
31 open CooperDec; |
32 |
32 |
33 (* |
33 val presburger_ss = simpset () |
34 val presburger_ss = simpset_of (theory "Presburger") |
34 addsimps [diff_int_def] delsimps [thm "diff_int_def_symmetric"]; |
35 addsimps [zdiff_def] delsimps [symmetric zdiff_def]; |
35 |
36 *) |
|
37 |
|
38 val presburger_ss = simpset_of (theory "Presburger") |
|
39 addsimps[diff_int_def] delsimps [thm"diff_int_def_symmetric"]; |
|
40 val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT; |
36 val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT; |
41 |
37 |
42 (*Theorems that will be used later for the proofgeneration*) |
38 (*Theorems that will be used later for the proofgeneration*) |
43 |
39 |
44 val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0"; |
40 val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0"; |
45 val unity_coeff_ex = thm "unity_coeff_ex"; |
41 val unity_coeff_ex = thm "unity_coeff_ex"; |
46 |
42 |
47 (* Thorems for proving the adjustment of the coeffitients*) |
43 (* Theorems for proving the adjustment of the coefficients*) |
48 |
44 |
49 val ac_lt_eq = thm "ac_lt_eq"; |
45 val ac_lt_eq = thm "ac_lt_eq"; |
50 val ac_eq_eq = thm "ac_eq_eq"; |
46 val ac_eq_eq = thm "ac_eq_eq"; |
51 val ac_dvd_eq = thm "ac_dvd_eq"; |
47 val ac_dvd_eq = thm "ac_dvd_eq"; |
52 val ac_pi_eq = thm "ac_pi_eq"; |
48 val ac_pi_eq = thm "ac_pi_eq"; |
192 (*This function proove elementar will be used to generate proofs at |
188 (*This function proove elementar will be used to generate proofs at |
193 runtime*) (*It is thought to prove properties such as a dvd b |
189 runtime*) (*It is thought to prove properties such as a dvd b |
194 (essentially) that are only to make at runtime.*) |
190 (essentially) that are only to make at runtime.*) |
195 (* ------------------------------------------------------------------------- *) |
191 (* ------------------------------------------------------------------------- *) |
196 fun prove_elementar thy s fm2 = |
192 fun prove_elementar thy s fm2 = |
197 Goal.prove thy [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY |
193 Goal.prove (ProofContext.init thy) [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY |
198 (case s of |
194 (case s of |
199 (*"ss" like simplification with simpset*) |
195 (*"ss" like simplification with simpset*) |
200 "ss" => |
196 "ss" => |
201 let val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0,unity_coeff_ex] |
197 let val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0,unity_coeff_ex] |
202 in [simp_tac ss 1, TRY (simple_arith_tac 1)] end |
198 in [simp_tac ss 1, TRY (simple_arith_tac 1)] end |