1.1 --- a/src/HOL/Integ/cooper_dec.ML Sat Jun 05 13:08:53 2004 +0200
1.2 +++ b/src/HOL/Integ/cooper_dec.ML Sat Jun 05 18:34:06 2004 +0200
1.3 @@ -39,6 +39,8 @@
1.4 val has_bound : term -> bool
1.5 val minusinf : term -> term -> term
1.6 val plusinf : term -> term -> term
1.7 + val onatoms : (term -> term) -> term -> term
1.8 + val evalc : term -> term
1.9 end;
1.10
1.11 structure CooperDec : COOPER_DEC =
2.1 --- a/src/HOL/Integ/cooper_proof.ML Sat Jun 05 13:08:53 2004 +0200
2.2 +++ b/src/HOL/Integ/cooper_proof.ML Sat Jun 05 18:34:06 2004 +0200
2.3 @@ -15,11 +15,13 @@
2.4 val qe_impI : thm
2.5 val qe_eqI : thm
2.6 val qe_exI : thm
2.7 + val list_to_set : typ -> term list -> term
2.8 val qe_get_terms : thm -> term * term
2.9 val cooper_prv : Sign.sg -> term -> term -> thm
2.10 val proof_of_evalc : Sign.sg -> term -> thm
2.11 val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
2.12 val proof_of_linform : Sign.sg -> string list -> term -> thm
2.13 + val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
2.14 val prove_elementar : Sign.sg -> string -> term -> thm
2.15 val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
2.16 end;
2.17 @@ -365,6 +367,10 @@
2.18
2.19 |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
2.20
2.21 +fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l);
2.22 +
2.23 +
2.24 +
2.25 (*==================================================*)
2.26 (* Finding rho for modd_minusinfinity *)
2.27 (*==================================================*)
2.28 @@ -861,28 +867,51 @@
2.29 (* ------------------------------------------------------------------------- *)
2.30
2.31 fun cooper_prv sg (x as Free(xn,xT)) efm = let
2.32 + (* lfm_thm : efm = linearized form of efm*)
2.33 val lfm_thm = proof_of_linform sg [xn] efm
2.34 + (*efm2 is the linearized form of efm *)
2.35 val efm2 = snd(qe_get_terms lfm_thm)
2.36 + (* l is the lcm of all coefficients of x *)
2.37 val l = formlcm x efm2
2.38 - val ac_thm = [lfm_thm , (thm_of sg (decomp_adjustcoeffeq sg x l) efm2)] MRS trans
2.39 + (*ac_thm: efm = efm2 with adjusted coefficients of x *)
2.40 + val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
2.41 + (* fm is efm2 with adjusted coefficients of x *)
2.42 val fm = snd (qe_get_terms ac_thm)
2.43 + (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
2.44 val cfm = unitycoeff x fm
2.45 + (*afm is fm where c*x is replaced by 1*x or -1*x *)
2.46 val afm = adjustcoeff x l fm
2.47 + (* P = %x.afm*)
2.48 val P = absfree(xn,xT,afm)
2.49 + (* This simpset allows the elimination of the sets in bex {1..d} *)
2.50 val ss = presburger_ss addsimps
2.51 [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
2.52 + (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
2.53 val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
2.54 + (* e_ac_thm : Ex x. efm = EX x. fm*)
2.55 val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
2.56 + (* A and B set of the formula*)
2.57 val A = aset x cfm
2.58 val B = bset x cfm
2.59 + (* the divlcm (delta) of the formula*)
2.60 val dlcm = mk_numeral (divlcm x cfm)
2.61 + (* Which set is smaller to generate the (hoepfully) shorter proof*)
2.62 val cms = if ((length A) < (length B )) then "pi" else "mi"
2.63 + (* synthesize the proof of cooper's theorem*)
2.64 + (* cp_thm: EX x. cfm = Q*)
2.65 val cp_thm = cooper_thm sg cms x cfm dlcm A B
2.66 + (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
2.67 + (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
2.68 val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
2.69 + (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
2.70 val (lsuth,rsuth) = qe_get_terms (uth)
2.71 + (* lseacth = EX x. efm; rseacth = EX x. fm*)
2.72 val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
2.73 + (* lscth = EX x. cfm; rscth = Q' *)
2.74 val (lscth,rscth) = qe_get_terms (exp_cp_thm)
2.75 + (* u_c_thm: EX x. P(l*x) = Q'*)
2.76 val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
2.77 + (* result: EX x. efm = Q'*)
2.78 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
2.79 end
2.80 |cooper_prv _ _ _ = error "Parameters format";
3.1 --- a/src/HOL/Integ/presburger.ML Sat Jun 05 13:08:53 2004 +0200
3.2 +++ b/src/HOL/Integ/presburger.ML Sat Jun 05 18:34:06 2004 +0200
3.3 @@ -282,7 +282,7 @@
3.4 || Args.$$$ "abs" >> K (apsnd (K true));
3.5 in
3.6 Method.simple_args
3.7 - (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
3.8 + (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
3.9 curry (foldl op |>) (true, false))
3.10 (fn (q,a) => fn _ => meth q a 1)
3.11 end;
4.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML Sat Jun 05 13:08:53 2004 +0200
4.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML Sat Jun 05 18:34:06 2004 +0200
4.3 @@ -39,6 +39,8 @@
4.4 val has_bound : term -> bool
4.5 val minusinf : term -> term -> term
4.6 val plusinf : term -> term -> term
4.7 + val onatoms : (term -> term) -> term -> term
4.8 + val evalc : term -> term
4.9 end;
4.10
4.11 structure CooperDec : COOPER_DEC =
5.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML Sat Jun 05 13:08:53 2004 +0200
5.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML Sat Jun 05 18:34:06 2004 +0200
5.3 @@ -15,11 +15,13 @@
5.4 val qe_impI : thm
5.5 val qe_eqI : thm
5.6 val qe_exI : thm
5.7 + val list_to_set : typ -> term list -> term
5.8 val qe_get_terms : thm -> term * term
5.9 val cooper_prv : Sign.sg -> term -> term -> thm
5.10 val proof_of_evalc : Sign.sg -> term -> thm
5.11 val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
5.12 val proof_of_linform : Sign.sg -> string list -> term -> thm
5.13 + val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
5.14 val prove_elementar : Sign.sg -> string -> term -> thm
5.15 val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
5.16 end;
5.17 @@ -365,6 +367,10 @@
5.18
5.19 |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
5.20
5.21 +fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l);
5.22 +
5.23 +
5.24 +
5.25 (*==================================================*)
5.26 (* Finding rho for modd_minusinfinity *)
5.27 (*==================================================*)
5.28 @@ -861,28 +867,51 @@
5.29 (* ------------------------------------------------------------------------- *)
5.30
5.31 fun cooper_prv sg (x as Free(xn,xT)) efm = let
5.32 + (* lfm_thm : efm = linearized form of efm*)
5.33 val lfm_thm = proof_of_linform sg [xn] efm
5.34 + (*efm2 is the linearized form of efm *)
5.35 val efm2 = snd(qe_get_terms lfm_thm)
5.36 + (* l is the lcm of all coefficients of x *)
5.37 val l = formlcm x efm2
5.38 - val ac_thm = [lfm_thm , (thm_of sg (decomp_adjustcoeffeq sg x l) efm2)] MRS trans
5.39 + (*ac_thm: efm = efm2 with adjusted coefficients of x *)
5.40 + val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
5.41 + (* fm is efm2 with adjusted coefficients of x *)
5.42 val fm = snd (qe_get_terms ac_thm)
5.43 + (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
5.44 val cfm = unitycoeff x fm
5.45 + (*afm is fm where c*x is replaced by 1*x or -1*x *)
5.46 val afm = adjustcoeff x l fm
5.47 + (* P = %x.afm*)
5.48 val P = absfree(xn,xT,afm)
5.49 + (* This simpset allows the elimination of the sets in bex {1..d} *)
5.50 val ss = presburger_ss addsimps
5.51 [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
5.52 + (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
5.53 val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
5.54 + (* e_ac_thm : Ex x. efm = EX x. fm*)
5.55 val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
5.56 + (* A and B set of the formula*)
5.57 val A = aset x cfm
5.58 val B = bset x cfm
5.59 + (* the divlcm (delta) of the formula*)
5.60 val dlcm = mk_numeral (divlcm x cfm)
5.61 + (* Which set is smaller to generate the (hoepfully) shorter proof*)
5.62 val cms = if ((length A) < (length B )) then "pi" else "mi"
5.63 + (* synthesize the proof of cooper's theorem*)
5.64 + (* cp_thm: EX x. cfm = Q*)
5.65 val cp_thm = cooper_thm sg cms x cfm dlcm A B
5.66 + (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
5.67 + (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
5.68 val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
5.69 + (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
5.70 val (lsuth,rsuth) = qe_get_terms (uth)
5.71 + (* lseacth = EX x. efm; rseacth = EX x. fm*)
5.72 val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
5.73 + (* lscth = EX x. cfm; rscth = Q' *)
5.74 val (lscth,rscth) = qe_get_terms (exp_cp_thm)
5.75 + (* u_c_thm: EX x. P(l*x) = Q'*)
5.76 val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
5.77 + (* result: EX x. efm = Q'*)
5.78 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
5.79 end
5.80 |cooper_prv _ _ _ = error "Parameters format";
6.1 --- a/src/HOL/Tools/Presburger/presburger.ML Sat Jun 05 13:08:53 2004 +0200
6.2 +++ b/src/HOL/Tools/Presburger/presburger.ML Sat Jun 05 18:34:06 2004 +0200
6.3 @@ -282,7 +282,7 @@
6.4 || Args.$$$ "abs" >> K (apsnd (K true));
6.5 in
6.6 Method.simple_args
6.7 - (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
6.8 + (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
6.9 curry (foldl op |>) (true, false))
6.10 (fn (q,a) => fn _ => meth q a 1)
6.11 end;