A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
--- a/src/HOL/Integ/Presburger.thy Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/Integ/Presburger.thy Wed May 19 11:23:59 2004 +0200
@@ -978,11 +978,11 @@
\medskip Specific instances of congruence rules, to prevent
simplifier from looping. *}
-theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
+theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
by simp
-theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<and> P) = (0 <= x \<and> P')"
- by simp
+theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
+ by (simp cong: conj_cong)
use "cooper_dec.ML"
use "cooper_proof.ML"
--- a/src/HOL/Integ/cooper_dec.ML Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Wed May 19 11:23:59 2004 +0200
@@ -29,10 +29,16 @@
val aset : term -> term -> term list
val linrep : string list -> term -> term -> term -> term
val list_disj : term list -> term
+ val list_conj : term list -> term
val simpl : term -> term
val fv : term -> string list
val negate : term -> term
val operations : (string * (int * int -> bool)) list
+ val conjuncts : term -> term list
+ val disjuncts : term -> term list
+ val has_bound : term -> bool
+ val minusinf : term -> term -> term
+ val plusinf : term -> term -> term
end;
structure CooperDec : COOPER_DEC =
@@ -183,7 +189,7 @@
else (warning "lint: apparent nonlinearity"; raise COOPER)
end
- |_ => error "lint: unknown term";
+ |_ => (error "COOPER:lint: unknown term ")
--- a/src/HOL/Integ/cooper_proof.ML Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/Integ/cooper_proof.ML Wed May 19 11:23:59 2004 +0200
@@ -16,35 +16,25 @@
val qe_eqI : thm
val qe_exI : thm
val qe_get_terms : thm -> term * term
- val cooper_prv : Sign.sg -> term -> term -> string list -> thm
+ val cooper_prv : Sign.sg -> term -> term -> thm
val proof_of_evalc : Sign.sg -> term -> thm
val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
val proof_of_linform : Sign.sg -> string list -> term -> thm
+ val prove_elementar : Sign.sg -> string -> term -> thm
+ val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
end;
structure CooperProof : COOPER_PROOF =
struct
-
open CooperDec;
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*--- ---*)
-(*--- ---*)
-(*--- Protocoling part ---*)
-(*--- ---*)
-(*--- includes the protocolling datastructure ---*)
-(*--- ---*)
-(*--- and the protocolling fuctions ---*)
-(*--- ---*)
-(*--- ---*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
+(*
+val presburger_ss = simpset_of (theory "Presburger")
+ addsimps [zdiff_def] delsimps [symmetric zdiff_def];
+*)
val presburger_ss = simpset_of (theory "Presburger")
- addsimps [diff_int_def] delsimps [thm"diff_int_def_symmetric"];
+ addsimps[diff_int_def] delsimps [thm"diff_int_def_symmetric"];
val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
(*Theorems that will be used later for the proofgeneration*)
@@ -52,7 +42,7 @@
val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
val unity_coeff_ex = thm "unity_coeff_ex";
-(* Theorems for proving the adjustment of the coefficients*)
+(* Thorems for proving the adjustment of the coeffitients*)
val ac_lt_eq = thm "ac_lt_eq";
val ac_eq_eq = thm "ac_eq_eq";
@@ -68,7 +58,7 @@
val qe_exI = thm "qe_exI";
val qe_ALLI = thm "qe_ALLI";
-(*Modulo D property for Pminusinf and Plusinf *)
+(*Modulo D property for Pminusinf an Plusinf *)
val fm_modd_minf = thm "fm_modd_minf";
val not_dvd_modd_minf = thm "not_dvd_modd_minf";
val dvd_modd_minf = thm "dvd_modd_minf";
@@ -77,7 +67,7 @@
val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
val dvd_modd_pinf = thm "dvd_modd_pinf";
-(* the minusinfinity property*)
+(* the minusinfinity proprty*)
val fm_eq_minf = thm "fm_eq_minf";
val neq_eq_minf = thm "neq_eq_minf";
@@ -87,7 +77,7 @@
val not_dvd_eq_minf = thm "not_dvd_eq_minf";
val dvd_eq_minf = thm "dvd_eq_minf";
-(* the Plusinfinity property*)
+(* the Plusinfinity proprty*)
val fm_eq_pinf = thm "fm_eq_pinf";
val neq_eq_pinf = thm "neq_eq_pinf";
@@ -108,7 +98,6 @@
val modd_pinf_disjI = thm "modd_pinf_disjI";
val modd_pinf_conjI = thm "modd_pinf_conjI";
-
(*Cooper Backwards...*)
(*Bset*)
val not_bst_p_fm = thm "not_bst_p_fm";
@@ -166,81 +155,6 @@
val lf_dvd = thm "lf_dvd";
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the cooperprocedure.*)
-(* ------------------------------------------------------------------------- *)
-
-
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the adjustcoeff step.*)
-(* ------------------------------------------------------------------------- *)
-datatype CpLog = No
- |Simp of term*CpLog
- |Blast of CpLog*CpLog
- |Aset of (term*term*(term list)*term)
- |Bset of (term*term*(term list)*term)
- |Minusinf of CpLog*CpLog
- |Cooper of term*CpLog*CpLog*CpLog
- |Eq_minf of term*term
- |Modd_minf of term*term
- |Eq_minf_conjI of CpLog*CpLog
- |Modd_minf_conjI of CpLog*CpLog
- |Modd_minf_disjI of CpLog*CpLog
- |Eq_minf_disjI of CpLog*CpLog
- |Not_bst_p of term*term*term*term*CpLog
- |Not_bst_p_atomic of term
- |Not_bst_p_conjI of CpLog*CpLog
- |Not_bst_p_disjI of CpLog*CpLog
- |Not_ast_p of term*term*term*term*CpLog
- |Not_ast_p_atomic of term
- |Not_ast_p_conjI of CpLog*CpLog
- |Not_ast_p_disjI of CpLog*CpLog
- |CpLogError;
-
-
-
-datatype ACLog = ACAt of int*term
- |ACPI of int*term
- |ACfm of term
- |ACNeg of ACLog
- |ACConst of string*ACLog*ACLog;
-
-
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the CNNF step.*)
-(* ------------------------------------------------------------------------- *)
-
-
-datatype NNFLog = NNFAt of term
- |NNFSimp of NNFLog
- |NNFNN of NNFLog
- |NNFConst of string*NNFLog*NNFLog;
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the linform step.*)
-(* ------------------------------------------------------------------------- *)
-
-
-datatype LfLog = LfAt of term
- |LfAtdvd of term
- |Lffm of term
- |LfConst of string*LfLog*LfLog
- |LfNot of LfLog
- |LfQ of string*string*typ*LfLog;
-
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the evaluation- evalc- step.*)
-(* ------------------------------------------------------------------------- *)
-
-
-datatype EvalLog = EvalAt of term
- |Evalfm of term
- |EvalConst of string*EvalLog*EvalLog;
-
(* ------------------------------------------------------------------------- *)
(*This function norm_zero_one replaces the occurences of Numeral1 and Numeral0*)
(*Respectively by their abstract representation Const("1",..) and COnst("0",..)*)
@@ -258,214 +172,6 @@
|(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
|_ => fm;
-
-(* ------------------------------------------------------------------------- *)
-(* Intended to tell that here we changed the structure of the formula with respect to the posineq theorem : ~(0 < t) = 0 < 1-t*)
-(* ------------------------------------------------------------------------- *)
-fun adjustcoeffeq_wp x l fm =
- case fm of
- (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $ c $ y ) $z )))) =>
- if (x = y)
- then let
- val m = l div (dest_numeral c)
- val n = abs (m)
- val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
- val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
- in (ACPI(n,fm),rs)
- end
- else let val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt ))
- in (ACPI(1,fm),rs)
- end
-
- |(Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $
- c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
- let val m = l div (dest_numeral c)
- val n = (if p = "op <" then abs(m) else m)
- val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
- val rs = (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
- in (ACAt(n,fm),rs)
- end
- else (ACfm(fm),fm)
- |( Const ("Not", _) $ p) => let val (rsp,rsr) = adjustcoeffeq_wp x l p
- in (ACNeg(rsp),HOLogic.Not $ rsr)
- end
- |( Const ("op &",_) $ p $ q) =>let val (rspp,rspr) = adjustcoeffeq_wp x l p
- val (rsqp,rsqr) = adjustcoeffeq_wp x l q
-
- in (ACConst ("CJ",rspp,rsqp), HOLogic.mk_conj (rspr,rsqr))
- end
- |( Const ("op |",_) $ p $ q) =>let val (rspp,rspr) = adjustcoeffeq_wp x l p
- val (rsqp,rsqr) = adjustcoeffeq_wp x l q
-
- in (ACConst ("DJ",rspp,rsqp), HOLogic.mk_disj (rspr,rsqr))
- end
-
- |_ => (ACfm(fm),fm);
-
-
-(*_________________________________________*)
-(*-----------------------------------------*)
-(* Protocol generation for the liform step *)
-(*_________________________________________*)
-(*-----------------------------------------*)
-
-
-fun linform_wp fm =
- let fun at_linform_wp at =
- case at of
- (Const("op <=",_)$s$t) => LfAt(at)
- |(Const("op <",_)$s$t) => LfAt(at)
- |(Const("op =",_)$s$t) => LfAt(at)
- |(Const("Divides.op dvd",_)$s$t) => LfAtdvd(at)
- in
- if is_arith_rel fm
- then at_linform_wp fm
- else case fm of
- (Const("Not",_) $ A) => LfNot(linform_wp A)
- |(Const("op &",_)$ A $ B) => LfConst("CJ",linform_wp A, linform_wp B)
- |(Const("op |",_)$ A $ B) => LfConst("DJ",linform_wp A, linform_wp B)
- |(Const("op -->",_)$ A $ B) => LfConst("IM",linform_wp A, linform_wp B)
- |(Const("op =",Type ("fun",[Type ("bool", []),_]))$ A $ B) => LfConst("EQ",linform_wp A, linform_wp B)
- |Const("Ex",_)$Abs(x,T,p) =>
- let val (xn,p1) = variant_abs(x,T,p)
- in LfQ("Ex",xn,T,linform_wp p1)
- end
- |Const("All",_)$Abs(x,T,p) =>
- let val (xn,p1) = variant_abs(x,T,p)
- in LfQ("All",xn,T,linform_wp p1)
- end
-end;
-
-
-(* ------------------------------------------------------------------------- *)
-(*For simlified formulas we just notice the original formula, for whitch we habe been
-intendes to make the proof.*)
-(* ------------------------------------------------------------------------- *)
-fun simpl_wp (fm,pr) = let val fm2 = simpl fm
- in (fm2,Simp(fm,pr))
- end;
-
-
-(* ------------------------------------------------------------------------- *)
-(*Help function for the generation of the proof EX.P_{minus \infty} --> EX. P(x) *)
-(* ------------------------------------------------------------------------- *)
-fun minusinf_wph x fm = let fun mk_atomar_minusinf_proof x fm = (Modd_minf(x,fm),Eq_minf(x,fm))
-
- fun combine_minusinf_proofs opr (ppr1,ppr2) (qpr1,qpr2) = case opr of
- "CJ" => (Modd_minf_conjI(ppr1,qpr1),Eq_minf_conjI(ppr2,qpr2))
- |"DJ" => (Modd_minf_disjI(ppr1,qpr1),Eq_minf_disjI(ppr2,qpr2))
- in
-
- case fm of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
- if (x=y) andalso (c1= zero) andalso (c2= one) then (HOLogic.true_const ,(mk_atomar_minusinf_proof x fm))
- else (fm ,(mk_atomar_minusinf_proof x fm))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
- if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
- then (HOLogic.false_const ,(mk_atomar_minusinf_proof x fm))
- else (fm,(mk_atomar_minusinf_proof x fm))
- |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y ) $ z )) =>
- if (y=x) andalso (c1 = zero) then
- if c2 = one then (HOLogic.false_const,(mk_atomar_minusinf_proof x fm)) else
- (HOLogic.true_const,(mk_atomar_minusinf_proof x fm))
- else (fm,(mk_atomar_minusinf_proof x fm))
-
- |(Const("Not",_)$(Const ("Divides.op dvd",_) $_ )) => (fm,mk_atomar_minusinf_proof x fm)
-
- |(Const ("Divides.op dvd",_) $_ ) => (fm,mk_atomar_minusinf_proof x fm)
-
- |(Const ("op &",_) $ p $ q) => let val (pfm,ppr) = minusinf_wph x p
- val (qfm,qpr) = minusinf_wph x q
- val pr = (combine_minusinf_proofs "CJ" ppr qpr)
- in
- (HOLogic.conj $ pfm $qfm , pr)
- end
- |(Const ("op |",_) $ p $ q) => let val (pfm,ppr) = minusinf_wph x p
- val (qfm,qpr) = minusinf_wph x q
- val pr = (combine_minusinf_proofs "DJ" ppr qpr)
- in
- (HOLogic.disj $ pfm $qfm , pr)
- end
-
- |_ => (fm,(mk_atomar_minusinf_proof x fm))
-
- end;
-(* ------------------------------------------------------------------------- *) (* Protokol for the Proof of the property of the minusinfinity formula*)
-(* Just combines the to protokols *)
-(* ------------------------------------------------------------------------- *)
-fun minusinf_wp x fm = let val (fm2,pr) = (minusinf_wph x fm)
- in (fm2,Minusinf(pr))
- end;
-
-(* ------------------------------------------------------------------------- *)
-(*Help function for the generation of the proof EX.P_{plus \infty} --> EX. P(x) *)
-(* ------------------------------------------------------------------------- *)
-
-fun plusinf_wph x fm = let fun mk_atomar_plusinf_proof x fm = (Modd_minf(x,fm),Eq_minf(x,fm))
-
- fun combine_plusinf_proofs opr (ppr1,ppr2) (qpr1,qpr2) = case opr of
- "CJ" => (Modd_minf_conjI(ppr1,qpr1),Eq_minf_conjI(ppr2,qpr2))
- |"DJ" => (Modd_minf_disjI(ppr1,qpr1),Eq_minf_disjI(ppr2,qpr2))
- in
-
- case fm of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
- if (x=y) andalso (c1= zero) andalso (c2= one) then (HOLogic.true_const ,(mk_atomar_plusinf_proof x fm))
- else (fm ,(mk_atomar_plusinf_proof x fm))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
- if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
- then (HOLogic.false_const ,(mk_atomar_plusinf_proof x fm))
- else (fm,(mk_atomar_plusinf_proof x fm))
- |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y ) $ z )) =>
- if (y=x) andalso (c1 = zero) then
- if c2 = one then (HOLogic.true_const,(mk_atomar_plusinf_proof x fm)) else
- (HOLogic.false_const,(mk_atomar_plusinf_proof x fm))
- else (fm,(mk_atomar_plusinf_proof x fm))
-
- |(Const("Not",_)$(Const ("Divides.op dvd",_) $_ )) => (fm,mk_atomar_plusinf_proof x fm)
-
- |(Const ("Divides.op dvd",_) $_ ) => (fm,mk_atomar_plusinf_proof x fm)
-
- |(Const ("op &",_) $ p $ q) => let val (pfm,ppr) = plusinf_wph x p
- val (qfm,qpr) = plusinf_wph x q
- val pr = (combine_plusinf_proofs "CJ" ppr qpr)
- in
- (HOLogic.conj $ pfm $qfm , pr)
- end
- |(Const ("op |",_) $ p $ q) => let val (pfm,ppr) = plusinf_wph x p
- val (qfm,qpr) = plusinf_wph x q
- val pr = (combine_plusinf_proofs "DJ" ppr qpr)
- in
- (HOLogic.disj $ pfm $qfm , pr)
- end
-
- |_ => (fm,(mk_atomar_plusinf_proof x fm))
-
- end;
-(* ------------------------------------------------------------------------- *) (* Protokol for the Proof of the property of the minusinfinity formula*)
-(* Just combines the to protokols *)
-(* ------------------------------------------------------------------------- *)
-fun plusinf_wp x fm = let val (fm2,pr) = (plusinf_wph x fm)
- in (fm2,Minusinf(pr))
- end;
-
-
-(* ------------------------------------------------------------------------- *)
-(*Protocol that we here uses Bset.*)
-(* ------------------------------------------------------------------------- *)
-fun bset_wp x fm = let val bs = bset x fm in
- (bs,Bset(x,fm,bs,mk_numeral (divlcm x fm)))
- end;
-
-(* ------------------------------------------------------------------------- *)
-(*Protocol that we here uses Aset.*)
-(* ------------------------------------------------------------------------- *)
-fun aset_wp x fm = let val ast = aset x fm in
- (ast,Aset(x,fm,ast,mk_numeral (divlcm x fm)))
- end;
-
-
-
(* ------------------------------------------------------------------------- *)
(*function list to Set, constructs a set containing all elements of a given list.*)
(* ------------------------------------------------------------------------- *)
@@ -475,181 +181,11 @@
|(h::t) => Const("insert", T1 --> (T --> T)) $ h $(list_to_set T1 t)
end;
-
-(*====================================================================*)
-(* ------------------------------------------------------------------------- *)
-(* ------------------------------------------------------------------------- *)
-(*Protocol for the proof of the backward direction of the cooper theorem.*)
-(* Helpfunction - Protokols evereything about the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_bst_p_wph fm = case fm of
- Const("Not",_) $ R => if (is_arith_rel R) then (Not_bst_p_atomic (fm)) else CpLogError
- |Const("op &",_) $ ls $ rs => Not_bst_p_conjI((not_bst_p_wph ls),(not_bst_p_wph rs))
- |Const("op |",_) $ ls $ rs => Not_bst_p_disjI((not_bst_p_wph ls),(not_bst_p_wph rs))
- |_ => Not_bst_p_atomic (fm);
-(* ------------------------------------------------------------------------- *)
-(* Main protocoling function for the backward direction gives the Bset and the divlcm and the Formula herself. Needed as inherited attributes for the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_bst_p_wp x fm = let val prt = not_bst_p_wph fm
- val D = mk_numeral (divlcm x fm)
- val B = map norm_zero_one (bset x fm)
- in (Not_bst_p (x,fm,D,(list_to_set HOLogic.intT B) , prt))
- end;
-(*====================================================================*)
-(* ------------------------------------------------------------------------- *)
-(* ------------------------------------------------------------------------- *)
-(*Protocol for the proof of the backward direction of the cooper theorem.*)
-(* Helpfunction - Protokols evereything about the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_ast_p_wph fm = case fm of
- Const("Not",_) $ R => if (is_arith_rel R) then (Not_ast_p_atomic (fm)) else CpLogError
- |Const("op &",_) $ ls $ rs => Not_ast_p_conjI((not_ast_p_wph ls),(not_ast_p_wph rs))
- |Const("op |",_) $ ls $ rs => Not_ast_p_disjI((not_ast_p_wph ls),(not_ast_p_wph rs))
- |_ => Not_ast_p_atomic (fm);
-(* ------------------------------------------------------------------------- *)
-(* Main protocoling function for the backward direction gives the Bset and the divlcm and the Formula herself. Needed as inherited attributes for the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_ast_p_wp x fm = let val prt = not_ast_p_wph fm
- val D = mk_numeral (divlcm x fm)
- val B = map norm_zero_one (aset x fm)
- in (Not_ast_p (x,fm,D,(list_to_set HOLogic.intT B) , prt))
- end;
-
-(*======================================================*)
-(* Protokolgeneration for the formula evaluation process*)
-(*======================================================*)
-
-fun evalc_wp fm =
- let fun evalc_atom_wp at =case at of
- (Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
- Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then EvalAt(HOLogic.mk_eq(at,HOLogic.true_const)) else EvalAt(HOLogic.mk_eq(at, HOLogic.false_const)))
- handle _ => Evalfm(at))
- | _ => Evalfm(at))
- |Const("Not",_)$(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
- Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then
- EvalAt(HOLogic.mk_eq(at, HOLogic.false_const)) else EvalAt(HOLogic.mk_eq(at,HOLogic.true_const)))
- handle _ => Evalfm(at))
- | _ => Evalfm(at))
- | _ => Evalfm(at)
-
- in
- case fm of
- (Const("op &",_)$A$B) => EvalConst("CJ",evalc_wp A,evalc_wp B)
- |(Const("op |",_)$A$B) => EvalConst("DJ",evalc_wp A,evalc_wp B)
- |(Const("op -->",_)$A$B) => EvalConst("IM",evalc_wp A,evalc_wp B)
- |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => EvalConst("EQ",evalc_wp A,evalc_wp B)
- |_ => evalc_atom_wp fm
- end;
-
-
-
-(*======================================================*)
-(* Protokolgeneration for the NNF Transformation *)
-(*======================================================*)
-
-fun cnnf_wp f =
- let fun hcnnf_wp fm =
- case fm of
- (Const ("op &",_) $ p $ q) => NNFConst("CJ",hcnnf_wp p,hcnnf_wp q)
- | (Const ("op |",_) $ p $ q) => NNFConst("DJ",hcnnf_wp p,hcnnf_wp q)
- | (Const ("op -->",_) $ p $q) => NNFConst("IM",hcnnf_wp (HOLogic.Not $ p),hcnnf_wp q)
- | (Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q) => NNFConst("EQ",hcnnf_wp (HOLogic.mk_conj(p,q)),hcnnf_wp (HOLogic.mk_conj((HOLogic.Not $ p), (HOLogic.Not $ q))))
-
- | (Const ("Not",_) $ (Const("Not",_) $ p)) => NNFNN(hcnnf_wp p)
- | (Const ("Not",_) $ (Const ("op &",_) $ p $ q)) => NNFConst ("NCJ",(hcnnf_wp(HOLogic.Not $ p)),(hcnnf_wp(HOLogic.Not $ q)))
- | (Const ("Not",_) $(Const ("op |",_) $ (A as (Const ("op &",_) $ p $ q)) $
- (B as (Const ("op &",_) $ p1 $ r)))) => if p1 = negate p then
- NNFConst("SDJ",
- NNFConst("CJ",hcnnf_wp p,hcnnf_wp(HOLogic.Not $ q)),
- NNFConst("CJ",hcnnf_wp p1,hcnnf_wp(HOLogic.Not $ r)))
- else NNFConst ("NDJ",(hcnnf_wp(HOLogic.Not $ A)),(hcnnf_wp(HOLogic.Not $ B)))
-
- | (Const ("Not",_) $ (Const ("op |",_) $ p $ q)) => NNFConst ("NDJ",(hcnnf_wp(HOLogic.Not $ p)),(hcnnf_wp(HOLogic.Not $ q)))
- | (Const ("Not",_) $ (Const ("op -->",_) $ p $q)) => NNFConst ("NIM",(hcnnf_wp(p)),(hcnnf_wp(HOLogic.Not $ q)))
- | (Const ("Not",_) $ (Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q)) =>NNFConst ("NEQ",(NNFConst("CJ",hcnnf_wp p,hcnnf_wp(HOLogic.Not $ q))),(NNFConst("CJ",hcnnf_wp(HOLogic.Not $ p),hcnnf_wp q)))
- | _ => NNFAt(fm)
- in NNFSimp(hcnnf_wp f)
-end;
-
-
-
-
-
-
-(* ------------------------------------------------------------------------- *)
-(*Cooper decision Procedure with proof protocoling*)
-(* ------------------------------------------------------------------------- *)
-
-fun coopermi_wp vars fm =
- case fm of
- Const ("Ex",_) $ Abs(xo,T,po) => let
- val (xn,np) = variant_abs(xo,T,po)
- val x = (Free(xn , T))
- val p = np (* Is this a legal proof for the P=NP Problem??*)
- val (p_inf,miprt) = simpl_wp (minusinf_wp x p)
- val (bset,bsprt) = bset_wp x p
- val nbst_p_prt = not_bst_p_wp x p
- val dlcm = divlcm x p
- val js = 1 upto dlcm
- fun p_element j b = linrep vars x (linear_add vars b (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) bset)
- in (list_disj (map stage js),Cooper(mk_numeral dlcm,miprt,bsprt,nbst_p_prt))
- end
-
- | _ => (error "cooper: not an existential formula",No);
-
-fun cooperpi_wp vars fm =
- case fm of
- Const ("Ex",_) $ Abs(xo,T,po) => let
- val (xn,np) = variant_abs(xo,T,po)
- val x = (Free(xn , T))
- val p = np (* Is this a legal proof for the P=NP Problem??*)
- val (p_inf,piprt) = simpl_wp (plusinf_wp x p)
- val (aset,asprt) = aset_wp x p
- val nast_p_prt = not_ast_p_wp x p
- val dlcm = divlcm x p
- val js = 1 upto dlcm
- fun p_element j a = linrep vars x (linear_sub vars a (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) aset)
- in (list_disj (map stage js),Cooper(mk_numeral dlcm,piprt,asprt,nast_p_prt))
- end
- | _ => (error "cooper: not an existential formula",No);
-
-
-
-
-
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*--- ---*)
-(*--- ---*)
-(*--- Interpretation and Proofgeneration Part ---*)
-(*--- ---*)
-(*--- Protocole interpretation functions ---*)
-(*--- ---*)
-(*--- and proofgeneration functions ---*)
-(*--- ---*)
-(*--- ---*)
-(*--- ---*)
-(*--- ---*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-
(* ------------------------------------------------------------------------- *)
(* Returns both sides of an equvalence in the theorem*)
(* ------------------------------------------------------------------------- *)
fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end;
-
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-
(* ------------------------------------------------------------------------- *)
(* Modified version of the simple version with minimal amount of checking and postprocessing*)
(* ------------------------------------------------------------------------- *)
@@ -664,9 +200,6 @@
(*-------------------------------------------------------------*)
(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t);
@@ -680,7 +213,8 @@
(*"ss" like simplification with simpset*)
"ss" =>
let
- val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0]
+ val ss = presburger_ss addsimps
+ [zdvd_iff_zmod_eq_0,unity_coeff_ex]
val ct = cert_Trueprop sg fm2
in
simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
@@ -725,6 +259,14 @@
in
simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
end
+ (* like Existance Conjunction *)
+ | "ec" =>
+ let
+ val ss = presburger_ss addsimps zadd_ac
+ val ct = cert_Trueprop sg fm2
+ in
+ simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (blast_tac HOL_cs 1)]
+ end
| "ac" =>
let
@@ -742,80 +284,92 @@
simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
end;
+(*=============================================================*)
+(*-------------------------------------------------------------*)
+(* The new compact model *)
+(*-------------------------------------------------------------*)
+(*=============================================================*)
+fun thm_of sg decomp t =
+ let val (ts,recomb) = decomp t
+ in recomb (map (thm_of sg decomp) ts)
+ end;
+
+(*==================================================*)
+(* Compact Version for adjustcoeffeq *)
+(*==================================================*)
+
+fun decomp_adjustcoeffeq sg x l fm = case fm of
+ (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $ c $ y ) $z )))) =>
+ let
+ val m = l div (dest_numeral c)
+ val n = if (x = y) then abs (m) else 1
+ val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
+ val rs = if (x = y)
+ then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
+ else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
+ val ck = cterm_of sg (mk_numeral n)
+ val cc = cterm_of sg c
+ val ct = cterm_of sg z
+ val cx = cterm_of sg y
+ val pre = prove_elementar sg "lf"
+ (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral n)))
+ val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
+ in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
+ end
-(* ------------------------------------------------------------------------- *)
-(* This function return an Isabelle proof, of the adjustcoffeq result.*)
-(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
-(* ------------------------------------------------------------------------- *)
-fun proof_of_adjustcoeffeq sg (prt,rs) = case prt of
- ACfm fm => instantiate' [Some cboolT]
- [Some (cterm_of sg fm)] refl
- | ACAt (k,at as (Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $
- c $ x ) $t ))) =>
- let
- val ck = cterm_of sg (mk_numeral k)
- val cc = cterm_of sg c
- val ct = cterm_of sg t
- val cx = cterm_of sg x
- val ca = cterm_of sg a
- in case p of
- "op <" => let val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
- val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
- in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
- end
- |"op =" =>let val pre = prove_elementar sg "lf"
+ |(Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $
+ c $ y ) $t )) =>
+ if (is_arith_rel fm) andalso (x = y)
+ then
+ let val m = l div (dest_numeral c)
+ val k = (if p = "op <" then abs(m) else m)
+ val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div k)*l) ), x))
+ val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul k t) ))))
+
+ val ck = cterm_of sg (mk_numeral k)
+ val cc = cterm_of sg c
+ val ct = cterm_of sg t
+ val cx = cterm_of sg x
+ val ca = cterm_of sg a
+
+ in
+ case p of
+ "op <" =>
+ let val pre = prove_elementar sg "lf"
+ (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
+ val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
+ in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
+ end
+
+ |"op =" =>
+ let val pre = prove_elementar sg "lf"
(HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
- in let val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
- in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
- end
- end
- |"Divides.op dvd" =>let val pre = prove_elementar sg "lf"
+ val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
+ in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
+ end
+
+ |"Divides.op dvd" =>
+ let val pre = prove_elementar sg "lf"
(HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
- val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
- in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
+ val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
+ in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
- end
- end
- |ACPI(k,at as (Const("Not",_)$(Const("op <",_) $a $( Const ("op +", _)$(Const ("op *",_) $ c $ x ) $t )))) =>
- let
- val ck = cterm_of sg (mk_numeral k)
- val cc = cterm_of sg c
- val ct = cterm_of sg t
- val cx = cterm_of sg x
- val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
- val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
+ end
+ end
+ else ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl)
+
+ |( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not)
+ |( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+ |( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI)
- in [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
- end
- |ACNeg(pr) => let val (Const("Not",_)$nrs) = rs
- in (proof_of_adjustcoeffeq sg (pr,nrs)) RS (qe_Not)
- end
- |ACConst(s,pr1,pr2) =>
- let val (Const(_,_)$rs1$rs2) = rs
- val th1 = proof_of_adjustcoeffeq sg (pr1,rs1)
- val th2 = proof_of_adjustcoeffeq sg (pr2,rs2)
- in case s of
- "CJ" => [th1,th2] MRS (qe_conjI)
- |"DJ" => [th1,th2] MRS (qe_disjI)
- |"IM" => [th1,th2] MRS (qe_impI)
- |"EQ" => [th1,th2] MRS (qe_eqI)
- end;
+ |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
-
-
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* This function return an Isabelle proof, of some properties on the atoms*)
-(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
-(* This function doese only instantiate the the theorems in the theory *)
-(* ------------------------------------------------------------------------- *)
-fun atomar_minf_proof_of sg dlcm (Modd_minf (x,fm1)) =
- let
+(*==================================================*)
+(* Finding rho for modd_minusinfinity *)
+(*==================================================*)
+fun rho_for_modd_minf x dlcm sg fm1 =
+let
(*Some certified Terms*)
val ctrue = cterm_of sg HOLogic.true_const
@@ -853,10 +407,11 @@
|_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)
- end
-
- |atomar_minf_proof_of sg dlcm (Eq_minf (x,fm1)) = let
- (*Some certified types*)
+ end;
+(*=========================================================================*)
+(*=========================================================================*)
+fun rho_for_eq_minf x dlcm sg fm1 =
+ let
val fm = norm_zero_one fm1
in case fm1 of
(Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
@@ -893,70 +448,24 @@
|_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
end;
-
-(* ------------------------------------------------------------------------- *)
-(* This function combines proofs of some special form already synthetised from the subtrees to make*)
-(* a new proof of the same form. The combination occures whith isabelle theorems which have been already prooved *)
-(*these Theorems are in Presburger.thy and mostly do not relay on the arithmetic.*)
-(* These are Theorems for the Property of P_{-infty}*)
-(* ------------------------------------------------------------------------- *)
-fun combine_minf_proof s pr1 pr2 = case s of
- "ECJ" => [pr1 , pr2] MRS (eq_minf_conjI)
-
- |"EDJ" => [pr1 , pr2] MRS (eq_minf_disjI)
-
- |"MCJ" => [pr1 , pr2] MRS (modd_minf_conjI)
-
- |"MDJ" => [pr1 , pr2] MRS (modd_minf_disjI);
-
-(* ------------------------------------------------------------------------- *)
-(*This function return an isabelle Proof for the minusinfinity theorem*)
-(* It interpretates the protool and gives the protokoles property of P_{...} as a theorem*)
-(* ------------------------------------------------------------------------- *)
-fun minf_proof_ofh sg dlcm prl = case prl of
+(*=====================================================*)
+(*=====================================================*)
+(*=========== minf proofs with the compact version==========*)
+fun decomp_minf_eq x dlcm sg t = case t of
+ Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_conjI)
+ |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_disjI)
+ |_ => ([],fn [] => rho_for_eq_minf x dlcm sg t);
- Eq_minf (_) => atomar_minf_proof_of sg dlcm prl
-
- |Modd_minf (_) => atomar_minf_proof_of sg dlcm prl
-
- |Eq_minf_conjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
- val pr2 = minf_proof_ofh sg dlcm prl2
- in (combine_minf_proof "ECJ" pr1 pr2)
- end
-
- |Eq_minf_disjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
- val pr2 = minf_proof_ofh sg dlcm prl2
- in (combine_minf_proof "EDJ" pr1 pr2)
- end
-
- |Modd_minf_conjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
- val pr2 = minf_proof_ofh sg dlcm prl2
- in (combine_minf_proof "MCJ" pr1 pr2)
- end
-
- |Modd_minf_disjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
- val pr2 = minf_proof_ofh sg dlcm prl2
- in (combine_minf_proof "MDJ" pr1 pr2)
- end;
-(* ------------------------------------------------------------------------- *)
-(* Main function For the rest both properies of P_{..} are needed and here both theorems are returned.*)
-(* ------------------------------------------------------------------------- *)
-fun minf_proof_of sg dlcm (Minusinf (prl1,prl2)) =
- let val pr1 = minf_proof_ofh sg dlcm prl1
- val pr2 = minf_proof_ofh sg dlcm prl2
- in (pr1, pr2)
-end;
-
+fun decomp_minf_modd x dlcm sg t = case t of
+ Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_conjI)
+ |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_disjI)
+ |_ => ([],fn [] => rho_for_modd_minf x dlcm sg t);
-
-
-(* ------------------------------------------------------------------------- *)
-(* This function return an Isabelle proof, of some properties on the atoms*)
-(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
-(* This function doese only instantiate the the theorems in the theory *)
-(* ------------------------------------------------------------------------- *)
-fun atomar_pinf_proof_of sg dlcm (Modd_minf (x,fm1)) =
- let
+(* -------------------------------------------------------------*)
+(* Finding rho for pinf_modd *)
+(* -------------------------------------------------------------*)
+fun rho_for_modd_pinf x dlcm sg fm1 =
+let
(*Some certified Terms*)
val ctrue = cterm_of sg HOLogic.true_const
@@ -996,9 +505,12 @@
|_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf)
- end
-
- |atomar_pinf_proof_of sg dlcm (Eq_minf (x,fm1)) = let
+ end;
+(* -------------------------------------------------------------*)
+(* Finding rho for pinf_eq *)
+(* -------------------------------------------------------------*)
+fun rho_for_eq_pinf x dlcm sg fm1 =
+ let
val fm = norm_zero_one fm1
in case fm1 of
(Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
@@ -1036,67 +548,58 @@
end;
-(* ------------------------------------------------------------------------- *)
-(* This function combines proofs of some special form already synthetised from the subtrees to make*)
-(* a new proof of the same form. The combination occures whith isabelle theorems which have been already prooved *)
-(*these Theorems are in Presburger.thy and mostly do not relay on the arithmetic.*)
-(* These are Theorems for the Property of P_{+infty}*)
-(* ------------------------------------------------------------------------- *)
-fun combine_pinf_proof s pr1 pr2 = case s of
- "ECJ" => [pr1 , pr2] MRS (eq_pinf_conjI)
+
+fun minf_proof_of_c sg x dlcm t =
+ let val minf_eqth = thm_of sg (decomp_minf_eq x dlcm sg) t
+ val minf_moddth = thm_of sg (decomp_minf_modd x dlcm sg) t
+ in (minf_eqth, minf_moddth)
+end;
- |"EDJ" => [pr1 , pr2] MRS (eq_pinf_disjI)
-
- |"MCJ" => [pr1 , pr2] MRS (modd_pinf_conjI)
+(*=========== pinf proofs with the compact version==========*)
+fun decomp_pinf_eq x dlcm sg t = case t of
+ Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_conjI)
+ |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_disjI)
+ |_ =>([],fn [] => rho_for_eq_pinf x dlcm sg t) ;
- |"MDJ" => [pr1 , pr2] MRS (modd_pinf_disjI);
+fun decomp_pinf_modd x dlcm sg t = case t of
+ Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_conjI)
+ |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_disjI)
+ |_ => ([],fn [] => rho_for_modd_pinf x dlcm sg t);
+
+fun pinf_proof_of_c sg x dlcm t =
+ let val pinf_eqth = thm_of sg (decomp_pinf_eq x dlcm sg) t
+ val pinf_moddth = thm_of sg (decomp_pinf_modd x dlcm sg) t
+ in (pinf_eqth,pinf_moddth)
+end;
+
(* ------------------------------------------------------------------------- *)
-(*This function return an isabelle Proof for the minusinfinity theorem*)
-(* It interpretates the protool and gives the protokoles property of P_{...} as a theorem*)
+(* Here we generate the theorem for the Bset Property in the simple direction*)
+(* It is just an instantiation*)
(* ------------------------------------------------------------------------- *)
-fun pinf_proof_ofh sg dlcm prl = case prl of
+(*
+fun bsetproof_of sg (x as Free(xn,xT)) fm bs dlcm =
+ let
+ val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
+ val cdlcm = cterm_of sg dlcm
+ val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
+ in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
+end;
- Eq_minf (_) => atomar_pinf_proof_of sg dlcm prl
-
- |Modd_minf (_) => atomar_pinf_proof_of sg dlcm prl
-
- |Eq_minf_conjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
- val pr2 = pinf_proof_ofh sg dlcm prl2
- in (combine_pinf_proof "ECJ" pr1 pr2)
- end
-
- |Eq_minf_disjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
- val pr2 = pinf_proof_ofh sg dlcm prl2
- in (combine_pinf_proof "EDJ" pr1 pr2)
- end
-
- |Modd_minf_conjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
- val pr2 = pinf_proof_ofh sg dlcm prl2
- in (combine_pinf_proof "MCJ" pr1 pr2)
- end
-
- |Modd_minf_disjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
- val pr2 = pinf_proof_ofh sg dlcm prl2
- in (combine_pinf_proof "MDJ" pr1 pr2)
- end;
-(* ------------------------------------------------------------------------- *)
-(* Main function For the rest both properies of P_{..} are needed and here both theorems are returned.*)
-(* ------------------------------------------------------------------------- *)
-fun pinf_proof_of sg dlcm (Minusinf (prl1,prl2)) =
- let val pr1 = pinf_proof_ofh sg dlcm prl1
- val pr2 = pinf_proof_ofh sg dlcm prl2
- in (pr1, pr2)
+fun asetproof_of sg (x as Free(xn,xT)) fm ast dlcm =
+ let
+ val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
+ val cdlcm = cterm_of sg dlcm
+ val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
+ in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
end;
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* Protokol interpretation function for the backwards direction for cooper's Theorem*)
+*)
(* For the generation of atomic Theorems*)
(* Prove the premisses on runtime and then make RS*)
(* ------------------------------------------------------------------------- *)
+
+(*========= this is rho ============*)
fun generate_atomic_not_bst_p sg (x as Free(xn,xT)) fm dlcm B at =
let
val cdlcm = cterm_of sg dlcm
@@ -1157,28 +660,23 @@
end;
+
(* ------------------------------------------------------------------------- *)
(* Main interpretation function for this backwards dirction*)
(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
(*Help Function*)
(* ------------------------------------------------------------------------- *)
-fun not_bst_p_proof_of_h sg x fm dlcm B prt = case prt of
- (Not_bst_p_atomic(fm2)) => (generate_atomic_not_bst_p sg x fm dlcm B fm2)
-
- |(Not_bst_p_conjI(pr1,pr2)) =>
- let val th1 = (not_bst_p_proof_of_h sg x fm dlcm B pr1)
- val th2 = (not_bst_p_proof_of_h sg x fm dlcm B pr2)
- in ([th1,th2] MRS (not_bst_p_conjI))
- end
+
+(*==================== Proof with the compact version *)
- |(Not_bst_p_disjI(pr1,pr2)) =>
- let val th1 = (not_bst_p_proof_of_h sg x fm dlcm B pr1)
- val th2 = (not_bst_p_proof_of_h sg x fm dlcm B pr2)
- in ([th1,th2] MRS not_bst_p_disjI)
- end;
-(* Main function*)
-fun not_bst_p_proof_of sg (Not_bst_p(x as Free(xn,xT),fm,dlcm,B,prl)) =
- let val th = not_bst_p_proof_of_h sg x fm dlcm B prl
+fun decomp_nbstp sg x dlcm B fm t = case t of
+ Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_conjI )
+ |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_disjI)
+ |_ => ([], fn [] => generate_atomic_not_bst_p sg x fm dlcm B t);
+
+fun not_bst_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm B t =
+ let
+ val th = thm_of sg (decomp_nbstp sg x dlcm (list_to_set xT (map norm_zero_one B)) fm) t
val fma = absfree (xn,xT, norm_zero_one fm)
in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma))
in [th,th1] MRS (not_bst_p_Q_elim)
@@ -1192,6 +690,7 @@
(* For the generation of atomic Theorems*)
(* Prove the premisses on runtime and then make RS*)
(* ------------------------------------------------------------------------- *)
+(*========= this is rho ============*)
fun generate_atomic_not_ast_p sg (x as Free(xn,xT)) fm dlcm A at =
let
val cdlcm = cterm_of sg dlcm
@@ -1250,81 +749,109 @@
|_ => (instantiate' [] [Some cfma, Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
end;
-
-(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------ *)
(* Main interpretation function for this backwards dirction*)
(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
(*Help Function*)
(* ------------------------------------------------------------------------- *)
-fun not_ast_p_proof_of_h sg x fm dlcm A prt = case prt of
- (Not_ast_p_atomic(fm2)) => (generate_atomic_not_ast_p sg x fm dlcm A fm2)
-
- |(Not_ast_p_conjI(pr1,pr2)) =>
- let val th1 = (not_ast_p_proof_of_h sg x fm dlcm A pr1)
- val th2 = (not_ast_p_proof_of_h sg x fm dlcm A pr2)
- in ([th1,th2] MRS (not_ast_p_conjI))
- end
+
+fun decomp_nastp sg x dlcm A fm t = case t of
+ Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_conjI )
+ |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_disjI)
+ |_ => ([], fn [] => generate_atomic_not_ast_p sg x fm dlcm A t);
- |(Not_ast_p_disjI(pr1,pr2)) =>
- let val th1 = (not_ast_p_proof_of_h sg x fm dlcm A pr1)
- val th2 = (not_ast_p_proof_of_h sg x fm dlcm A pr2)
- in ([th1,th2] MRS (not_ast_p_disjI))
- end;
-(* Main function*)
-fun not_ast_p_proof_of sg (Not_ast_p(x as Free(xn,xT),fm,dlcm,A,prl)) =
- let val th = not_ast_p_proof_of_h sg x fm dlcm A prl
+fun not_ast_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm A t =
+ let
+ val th = thm_of sg (decomp_nastp sg x dlcm (list_to_set xT (map norm_zero_one A)) fm) t
val fma = absfree (xn,xT, norm_zero_one fm)
- val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma))
- in [th,th1] MRS (not_ast_p_Q_elim)
-end;
+ in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma))
+ in [th,th1] MRS (not_ast_p_Q_elim)
+ end
+ end;
+(* -------------------------------*)
+(* Finding rho and beta for evalc *)
+(* -------------------------------*)
+fun rho_for_evalc sg at = case at of
+ (Const (p,_) $ s $ t) =>(
+ case assoc (operations,p) of
+ Some f =>
+ ((if (f ((dest_numeral s),(dest_numeral t)))
+ then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const))
+ else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))
+ handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl
+ | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl ))
+ |Const("Not",_)$(Const (p,_) $ s $ t) =>(
+ case assoc (operations,p) of
+ Some f =>
+ ((if (f ((dest_numeral s),(dest_numeral t)))
+ then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))
+ else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))
+ handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl)
+ | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl )
+ | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl;
+
+
+(*=========================================================*)
+fun decomp_evalc sg t = case t of
+ (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+ |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
+ |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
+ |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
+ |_ => ([], fn [] => rho_for_evalc sg t);
+
+
+fun proof_of_evalc sg fm = thm_of sg (decomp_evalc sg) fm;
+
+(*==================================================*)
+(* Proof of linform with the compact model *)
+(*==================================================*)
+
+
+fun decomp_linform sg vars t = case t of
+ (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+ |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
+ |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
+ |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
+ |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
+ |(Const("Divides.op dvd",_)$d$r) => ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd)))
+ |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
+
+fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f;
(* ------------------------------------------------------------------------- *)
(* Interpretaion of Protocols of the cooper procedure : minusinfinity version*)
(* ------------------------------------------------------------------------- *)
-
-
-fun coopermi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nbst_p_prt)) =
+fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
(* Get the Bset thm*)
- let val (mit1,mit2) = minf_proof_of sg dlcm miprt
- val fm1 = norm_zero_one (simpl fm)
+ let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm
val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
- val nbstpthm = not_bst_p_proof_of sg nbst_p_prt
- (* Return the four theorems needed to proove the whole Cooper Theorem*)
- in (dpos,mit2,nbstpthm,mit1)
+ val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
+ in (dpos,minf_eqth,nbstpthm,minf_moddth)
end;
-
(* ------------------------------------------------------------------------- *)
(* Interpretaion of Protocols of the cooper procedure : plusinfinity version *)
(* ------------------------------------------------------------------------- *)
-
-
-fun cooperpi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nast_p_prt)) =
- let val (mit1,mit2) = pinf_proof_of sg dlcm miprt
- val fm1 = norm_zero_one (simpl fm)
+fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
+ let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
- val nastpthm = not_ast_p_proof_of sg nast_p_prt
- in (dpos,mit2,nastpthm,mit1)
+ val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
+ in (dpos,pinf_eqth,nastpthm,pinf_moddth)
end;
-
(* ------------------------------------------------------------------------- *)
(* Interpretaion of Protocols of the cooper procedure : full version*)
(* ------------------------------------------------------------------------- *)
-
-
-
-fun cooper_thm sg s (x as Free(xn,xT)) vars cfm = case s of
- "pi" => let val (rs,prt) = cooperpi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
- val (dpsthm,th1,nbpth,th3) = cooperpi_proof_of sg x prt
- in [dpsthm,th1,nbpth,th3] MRS (cppi_eq)
+fun cooper_thm sg s (x as Free(xn,xT)) cfm dlcm ast bst= case s of
+ "pi" => let val (dpsthm,pinf_eqth,nbpth,pinf_moddth) = cooperpi_proof_of sg x cfm ast dlcm
+ in [dpsthm,pinf_eqth,nbpth,pinf_moddth] MRS (cppi_eq)
end
- |"mi" => let val (rs,prt) = coopermi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
- val (dpsthm,th1,nbpth,th3) = coopermi_proof_of sg x prt
- in [dpsthm,th1,nbpth,th3] MRS (cpmi_eq)
+ |"mi" => let val (dpsthm,minf_eqth,nbpth,minf_moddth) = coopermi_proof_of sg x cfm bst dlcm
+ in [dpsthm,minf_eqth,nbpth,minf_moddth] MRS (cpmi_eq)
end
|_ => error "parameter error";
@@ -1333,9 +860,11 @@
(* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
(* ------------------------------------------------------------------------- *)
-fun cooper_prv sg (x as Free(xn,xT)) efm vars = let
- val l = formlcm x efm
- val ac_thm = proof_of_adjustcoeffeq sg (adjustcoeffeq_wp x l efm)
+fun cooper_prv sg (x as Free(xn,xT)) efm = let
+ val lfm_thm = proof_of_linform sg [xn] efm
+ val efm2 = snd(qe_get_terms lfm_thm)
+ val l = formlcm x efm2
+ val ac_thm = [lfm_thm , (thm_of sg (decomp_adjustcoeffeq sg x l) efm2)] MRS trans
val fm = snd (qe_get_terms ac_thm)
val cfm = unitycoeff x fm
val afm = adjustcoeff x l fm
@@ -1344,8 +873,11 @@
[simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
- val cms = if ((length (aset x cfm)) < (length (bset x cfm))) then "pi" else "mi"
- val cp_thm = cooper_thm sg cms x vars cfm
+ val A = aset x cfm
+ val B = bset x cfm
+ val dlcm = mk_numeral (divlcm x cfm)
+ val cms = if ((length A) < (length B )) then "pi" else "mi"
+ val cp_thm = cooper_thm sg cms x cfm dlcm A B
val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
val (lsuth,rsuth) = qe_get_terms (uth)
val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
@@ -1353,98 +885,46 @@
val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
end
-|cooper_prv _ _ _ _ = error "Parameters format";
+|cooper_prv _ _ _ = error "Parameters format";
+
-(*====================================================*)
-(*Interpretation function for the evaluation protokol *)
-(*====================================================*)
-
-fun proof_of_evalc sg fm =
-let
-fun proof_of_evalch prt = case prt of
- EvalAt(at) => prove_elementar sg "ss" at
- |Evalfm(fm) => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl
- |EvalConst(s,pr1,pr2) =>
- let val th1 = proof_of_evalch pr1
- val th2 = proof_of_evalch pr2
- in case s of
- "CJ" =>[th1,th2] MRS (qe_conjI)
- |"DJ" =>[th1,th2] MRS (qe_disjI)
- |"IM" =>[th1,th2] MRS (qe_impI)
- |"EQ" =>[th1,th2] MRS (qe_eqI)
- end
-in proof_of_evalch (evalc_wp fm)
-end;
-
-(*============================================================*)
-(*Interpretation function for the NNF-Transformation protokol *)
-(*============================================================*)
+fun decomp_cnnf sg lfnp P = case P of
+ Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )
+ |Const ("op |",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_disjI)
+ |Const ("Not",_) $ (Const("Not",_) $ p) => ([p], fn [th] => th RS nnf_nn)
+ |Const("Not",_) $ (Const(opn,T) $ p $ q) =>
+ if opn = "op |"
+ then case (p,q) of
+ (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
+ if r1 = negate r
+ 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)
-fun proof_of_cnnf sg fm pf =
-let fun proof_of_cnnfh prt pat = case prt of
- NNFAt(at) => pat at
- |NNFSimp (pr) => let val th1 = proof_of_cnnfh pr pat
- in let val fm2 = snd (qe_get_terms th1)
- in [th1,prove_elementar sg "ss" (HOLogic.mk_eq(fm2 ,simpl fm2))] MRS trans
- end
- end
- |NNFNN (pr) => (proof_of_cnnfh pr pat) RS (nnf_nn)
- |NNFConst (s,pr1,pr2) =>
- let val th1 = proof_of_cnnfh pr1 pat
- val th2 = proof_of_cnnfh pr2 pat
- in case s of
- "CJ" => [th1,th2] MRS (qe_conjI)
- |"DJ" => [th1,th2] MRS (qe_disjI)
- |"IM" => [th1,th2] MRS (nnf_im)
- |"EQ" => [th1,th2] MRS (nnf_eq)
- |"SDJ" => let val (Const("op &",_)$A$_) = fst (qe_get_terms th1)
- val (Const("op &",_)$C$_) = fst (qe_get_terms th2)
- in [th1,th2,prove_elementar sg "ss" (HOLogic.mk_eq (A,HOLogic.Not $ C))] MRS (nnf_sdj)
- end
- |"NCJ" => [th1,th2] MRS (nnf_ncj)
- |"NIM" => [th1,th2] MRS (nnf_nim)
- |"NEQ" => [th1,th2] MRS (nnf_neq)
- |"NDJ" => [th1,th2] MRS (nnf_ndj)
- end
-in proof_of_cnnfh (cnnf_wp fm) pf
-end;
+ else ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
+ |(_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
+ else (
+ case (opn,T) of
+ ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_ncj )
+ |("op -->",_) => ([p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_nim )
+ |("op =",Type ("fun",[Type ("bool", []),_])) =>
+ ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], fn [th1,th2] => [th1,th2] MRS nnf_neq)
+ |(_,_) => ([], fn [] => lfnp P)
+)
+
+ |(Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], fn [th1,th2] => [th1,th2] MRS nnf_im)
+
+ |(Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) =>
+ ([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], fn [th1,th2] =>[th1,th2] MRS nnf_eq )
+ |_ => ([], fn [] => lfnp P);
-(*====================================================*)
-(* Interpretation function for the linform protokol *)
-(*====================================================*)
-
-
-fun proof_of_linform sg vars f =
- let fun proof_of_linformh prt =
- case prt of
- (LfAt (at)) => prove_elementar sg "lf" (HOLogic.mk_eq (at, linform vars at))
- |(LfAtdvd (Const("Divides.op dvd",_)$d$t)) => (prove_elementar sg "lf" (HOLogic.mk_eq (t, lint vars t))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd))
- |(Lffm (fm)) => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl)
- |(LfConst (s,pr1,pr2)) =>
- let val th1 = proof_of_linformh pr1
- val th2 = proof_of_linformh pr2
- in case s of
- "CJ" => [th1,th2] MRS (qe_conjI)
- |"DJ" =>[th1,th2] MRS (qe_disjI)
- |"IM" =>[th1,th2] MRS (qe_impI)
- |"EQ" =>[th1,th2] MRS (qe_eqI)
- end
- |(LfNot(pr)) =>
- let val th = proof_of_linformh pr
- in (th RS (qe_Not))
- end
- |(LfQ(s,xn,xT,pr)) =>
- let val th = forall_intr (cterm_of sg (Free(xn,xT)))(proof_of_linformh pr)
- in if s = "Ex"
- then (th COMP(qe_exI) )
- else (th COMP(qe_ALLI) )
- end
-in
- proof_of_linformh (linform_wp f)
-end;
+fun proof_of_cnnf sg p lfnp =
+ let val th1 = thm_of sg (decomp_cnnf sg lfnp) p
+ val rs = snd(qe_get_terms th1)
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq(rs,simpl rs))
+ in [th1,th2] MRS trans
+ end;
end;
--- a/src/HOL/Integ/presburger.ML Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/Integ/presburger.ML Wed May 19 11:23:59 2004 +0200
@@ -6,10 +6,13 @@
Tactic for solving arithmetical Goals in Presburger Arithmetic
*)
+(* This version of presburger deals with occurences of functional symbols in the subgoal and abstract over them to try to prove the more general formula. It then resolves with the subgoal. To disable this feature call the procedure with the parameter no_abs
+*)
+
signature PRESBURGER =
sig
- val presburger_tac : bool -> int -> tactic
- val presburger_method : bool -> int -> Proof.method
+ val presburger_tac : bool -> bool -> int -> tactic
+ val presburger_method : bool -> bool -> int -> Proof.method
val setup : (theory -> theory) list
val trace : bool ref
end;
@@ -25,19 +28,18 @@
(* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
(*-----------------------------------------------------------------*)
-val presburger_ss = simpset_of (theory "Presburger");
-
-fun cooper_pp sg vrl (fm as e$Abs(xn,xT,p)) =
+fun cooper_pp sg (fm as e$Abs(xn,xT,p)) =
let val (xn1,p1) = variant_abs (xn,xT,p)
- in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1 vrl) end;
+ in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
(CooperProof.proof_of_evalc sg);
-fun mproof_of_int_qelim sg fm =
- Qelim.proof_of_mlift_qelim sg CooperDec.is_arith_rel
+fun tmproof_of_int_qelim sg fm =
+ Qelim.tproof_of_mlift_qelim sg CooperDec.is_arith_rel
(CooperProof.proof_of_linform sg) (mnnf_pp sg) (cooper_pp sg) fm;
+
(* Theorems to be used in this tactic*)
val zdvd_int = thm "zdvd_int";
@@ -63,6 +65,19 @@
fun term_typed_consts t = add_term_typed_consts(t,[]);
+(* put a term into eta long beta normal form *)
+fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
+ | eta_long Ts t = (case strip_comb t of
+ (Abs _, _) => eta_long Ts (Envir.beta_norm t)
+ | (u, ts) =>
+ let
+ val Us = binder_types (fastype_of1 (Ts, t));
+ val i = length Us
+ in list_abs (map (pair "x") Us,
+ list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
+ (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
+ end);
+
(* Some Types*)
val bT = HOLogic.boolT;
val iT = HOLogic.intT;
@@ -94,8 +109,6 @@
("op *", iT --> iT --> iT),
("HOL.abs", iT --> iT),
("uminus", iT --> iT),
- ("HOL.max", iT --> iT --> iT),
- ("HOL.min", iT --> iT --> iT),
("op <=", nT --> nT --> bT),
("op =", nT --> nT --> bT),
@@ -107,8 +120,6 @@
("op -", nT --> nT --> nT),
("op *", nT --> nT --> nT),
("Suc", nT --> nT),
- ("HOL.max", nT --> nT --> nT),
- ("HOL.min", nT --> nT --> nT),
("Numeral.bin.Bit", binT --> bT --> binT),
("Numeral.bin.Pls", binT),
@@ -119,27 +130,89 @@
("0", iT),
("1", nT),
("1", iT),
-
("False", bT),
("True", bT)];
-(*returns true if the formula is relevant for presburger arithmetic tactic*)
-fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso
- map (fn i => snd (nth_elem (i, ps))) (loose_bnos t) @
- map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
- subset [iT, nT];
-
(* Preparation of the formula to be sent to the Integer quantifier *)
(* elimination procedure *)
(* Transforms meta implications and meta quantifiers to object *)
(* implications and object quantifiers *)
-fun prepare_for_presburger q fm =
+
+(*==================================*)
+(* Abstracting on subterms ========*)
+(*==================================*)
+(* Returns occurences of terms that are function application of type int or nat*)
+
+fun getfuncs fm = case strip_comb fm of
+ (Free (_, T), ts as _ :: _) =>
+ if body_type T mem [iT, nT]
+ andalso not (ts = []) andalso forall (null o loose_bnos) ts
+ then [fm]
+ else foldl op union ([], map getfuncs ts)
+ | (Var (_, T), ts as _ :: _) =>
+ if body_type T mem [iT, nT]
+ andalso not (ts = []) andalso forall (null o loose_bnos) ts then [fm]
+ else foldl op union ([], map getfuncs ts)
+ | (Const (s, T), ts) =>
+ if (s, T) mem allowed_consts orelse not (body_type T mem [iT, nT])
+ then foldl op union ([], map getfuncs ts)
+ else [fm]
+ | (Abs (s, T, t), _) => getfuncs t
+ | _ => [];
+
+
+fun abstract_pres sg fm =
+ foldr (fn (t, u) =>
+ let val T = fastype_of t
+ in all T $ Abs ("x", T, abstract_over (t, u)) end)
+ (getfuncs fm, fm);
+
+
+
+(* hasfuncs_on_bounds dont care of the type of the functions applied!
+ It returns true if there is a subterm coresponding to the application of
+ a function on a bounded variable.
+
+ Function applications are allowed only for well predefined functions a
+ consts*)
+
+fun has_free_funcs fm = case strip_comb fm of
+ (Free (_, T), ts as _ :: _) =>
+ if (body_type T mem [iT,nT]) andalso (not (T mem [iT,nT]))
+ then true
+ else exists (fn x => x) (map has_free_funcs ts)
+ | (Var (_, T), ts as _ :: _) =>
+ if (body_type T mem [iT,nT]) andalso not (T mem [iT,nT])
+ then true
+ else exists (fn x => x) (map has_free_funcs ts)
+ | (Const (s, T), ts) => exists (fn x => x) (map has_free_funcs ts)
+ | (Abs (s, T, t), _) => has_free_funcs t
+ |_ => false;
+
+
+(*returns true if the formula is relevant for presburger arithmetic tactic
+The constants occuring in term t should be a subset of the allowed_consts
+ There also should be no occurences of application of functions on bounded
+ variables. Whenever this function will be used, it will be ensured that t
+ will not contain subterms with function symbols that could have been
+ abstracted over.*)
+
+fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso
+ map (fn i => snd (nth_elem (i, ps))) (loose_bnos t) @
+ map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
+ subset [iT, nT]
+ andalso not (has_free_funcs t);
+
+
+fun prepare_for_presburger sg q fm =
let
val ps = Logic.strip_params fm
val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
- val _ = if relevant (rev ps) c then () else raise CooperDec.COOPER
+ val _ = if relevant (rev ps) c then ()
+ else (trace_msg ("Conclusion is not a presburger term:\n" ^
+ Sign.string_of_term sg c); raise CooperDec.COOPER)
fun mk_all ((s, T), (P,n)) =
if 0 mem loose_bnos P then
(HOLogic.all_const T $ Abs (s, T, P), n)
@@ -161,14 +234,20 @@
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
(* the presburger tactic*)
-fun presburger_tac q i = ObjectLogic.atomize_tac i THEN (fn st =>
+
+(* Parameters : q = flag for quantify ofer free variables ;
+ a = flag for abstracting over function occurences
+ i = subgoal *)
+
+fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
let
- val g = BasisLibrary.List.nth (prems_of st, i - 1);
- val sg = sign_of_thm st;
+ val g = BasisLibrary.List.nth (prems_of st, i - 1)
+ val sg = sign_of_thm st
+ (* The Abstraction step *)
+ val g' = if a then abstract_pres sg g else g
(* Transform the term*)
- val (t,np,nh) = prepare_for_presburger q g
+ val (t,np,nh) = prepare_for_presburger sg q g'
(* Some simpsets for dealing with mod div abs and nat*)
-
val simpset0 = HOL_basic_ss
addsimps [mod_div_equality', Suc_plus1]
addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
@@ -183,37 +262,40 @@
addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
addcongs [conj_le_cong, imp_le_cong]
(* simp rules for elimination of abs *)
-
val simpset3 = HOL_basic_ss addsplits [abs_split]
-
val ct = cterm_of sg (HOLogic.mk_Trueprop t)
-
(* Theorem for the nat --> int transformation *)
val pre_thm = Seq.hd (EVERY
- [simp_tac simpset0 i,
- TRY (simp_tac simpset1 i), TRY (simp_tac simpset2 i),
- TRY (simp_tac simpset3 i), TRY (simp_tac presburger_ss i)]
+ [simp_tac simpset0 1,
+ TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
+ TRY (simp_tac simpset3 1)]
(trivial ct))
-
- fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i);
-
+ fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
(trace_msg ("calling procedure with term:\n" ^
Sign.string_of_term sg t1);
- ((mproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
+ ((tmproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
| _ => (pre_thm, assm_tac i)
- in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st
+ in (rtac (((mp_step nh) o (spec_step np)) th) i
+ THEN tac) st
end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);
fun presburger_args meth =
- Method.simple_args (Scan.optional (Args.$$$ "no_quantify" >> K false) true)
- (fn q => fn _ => meth q 1);
+ let val parse_flag =
+ Args.$$$ "no_quantify" >> K (apfst (K false))
+ || Args.$$$ "no_abs" >> K (apsnd (K false));
+ in
+ Method.simple_args
+ (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
+ curry (foldl op |>) (true, true))
+ (fn (q,a) => fn _ => meth q a 1)
+ end;
-fun presburger_method q i = Method.METHOD (fn facts =>
- Method.insert_tac facts 1 THEN presburger_tac q i)
+fun presburger_method q a i = Method.METHOD (fn facts =>
+ Method.insert_tac facts 1 THEN presburger_tac q a i)
val setup =
[Method.add_method ("presburger",
@@ -221,8 +303,8 @@
"decision procedure for Presburger arithmetic"),
ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
{splits = splits, inj_consts = inj_consts, discrete = discrete,
- presburger = Some (presburger_tac true)})];
+ presburger = Some (presburger_tac true true)})];
end;
-val presburger_tac = Presburger.presburger_tac true;
+val presburger_tac = Presburger.presburger_tac true true;
--- a/src/HOL/Integ/qelim.ML Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/Integ/qelim.ML Wed May 19 11:23:59 2004 +0200
@@ -8,10 +8,11 @@
*)
signature QELIM =
-sig
- val proof_of_mlift_qelim: Sign.sg -> (term -> bool) ->
+ sig
+ val tproof_of_mlift_qelim: Sign.sg -> (term -> bool) ->
(string list -> term -> thm) -> (term -> thm) ->
- (string list -> term -> thm) -> term -> thm
+ (term -> thm) -> term -> thm
+
end;
structure Qelim : QELIM =
@@ -19,24 +20,6 @@
open CooperDec;
open CooperProof;
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*--- ---*)
-(*--- ---*)
-(*--- Protocoling part ---*)
-(*--- ---*)
-(*--- includes the protocolling datastructure ---*)
-(*--- ---*)
-(*--- and the protocolling fuctions ---*)
-(*--- ---*)
-(*--- ---*)
-(*--- ---*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-
-
val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
(* List of the theorems to be used in the following*)
@@ -46,131 +29,35 @@
val qe_ALL = thm "qe_ALL";
-(*Datatype declaration for the protocoling procedure.*)
-
-
-datatype QeLog = AFN of term*(string list)
- |QFN of term*(string list)
- |ExConj of term*QeLog
- |ExDisj of (string*typ*term)*term*QeLog*QeLog
- |QeConst of string*QeLog*QeLog
- |QeNot of QeLog
- |QeAll of QeLog
- |Lift_Qelim of term*QeLog
- |QeUnk of term;
-
-datatype mQeLog = mQeProof of (string list)*mQeLog
- |mAFN of term
- |mNFN of mQeLog
- |mQeConst of string*mQeLog*mQeLog
- |mQeNot of mQeLog
- |mQelim of term*(string list)*mQeLog
- |mQeAll of mQeLog
- |mQefm of term;
-
-(* This is the protokoling my function for the quantifier elimination*)
-fun mlift_qelim_wp isat vars =
- let fun mqelift_wp vars fm = if (isat fm) then mAFN(fm)
- else
- (case fm of
- ( Const ("Not",_) $ p) => mQeNot(mqelift_wp vars p)
- |( Const ("op &",_) $ p $q) => mQeConst("CJ", mqelift_wp vars p,mqelift_wp vars q)
-
- |( Const ("op |",_) $ p $q) => mQeConst("DJ", mqelift_wp vars p,mqelift_wp vars q)
-
- |( Const ("op -->",_) $ p $q) => mQeConst("IM", mqelift_wp vars p,mqelift_wp vars q)
-
- |( Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $q) =>mQeConst("EQ", mqelift_wp vars p,mqelift_wp vars q)
-
-
- |( Const ("All",QT) $ Abs(x,T,p)) =>mQeAll (mqelift_wp vars (Const("Ex",QT) $ Abs(x,T,(HOLogic.Not $ p))))
-
- |(Const ("Ex",_) $ Abs (x,T,p)) =>
- let val (x1,p1) = variant_abs (x,T,p)
- val prt = mqelift_wp (x1::vars) p1
- in mQelim(Free(x1,T),vars,mNFN(prt))
- end
- | _ => mQefm(fm)
- )
-
- in (fn fm => mQeProof(vars,mNFN(mqelift_wp vars fm )))
- end;
-
-
+(*============= Compact version =====*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*--- ---*)
-(*--- ---*)
-(*--- Interpretation and Proofgeneration Part ---*)
-(*--- ---*)
-(*--- Protocole interpretation functions ---*)
-(*--- ---*)
-(*--- and proofgeneration functions ---*)
-(*--- ---*)
-(*--- ---*)
-(*--- ---*)
-(*--- ---*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*function that interpretates the protokol generated by the _wp function*)
-
+fun decomp_qe is_at afnp nfnp qfnp sg P =
+ if is_at P then ([], fn [] => afnp [] P) else
+ case P of
+ (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+ |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
+ |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
+ |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
+ |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
+ |(Const("Ex",_)$Abs(xn,xT,p)) =>
+ let val (xn1,p1) = variant_abs(xn,xT,p)
+ in ([p1],
+ fn [th1_1] =>
+ let val th2 = [th1_1,nfnp (snd (qe_get_terms th1_1))] MRS trans
+ val eth1 = (forall_intr (cterm_of sg (Free(xn1,xT))) th2) COMP qe_exI
+ val th3 = qfnp (snd(qe_get_terms eth1))
+ in [eth1,th3] MRS trans
+ end )
+ end
-(* proof_of_lift_qelim interpretates a protokol for the quantifier elimination one some quantified formula. It uses the functions afnp nfnp and qfnp as proof functions to generate a prove for the hole quantifier elimination.*)
-(* afnp : must retun a proof for the transformations on the atomic formalae*)
-(* nfnp : must return a proof for the post one-quatifiers elimination process*)
-(* qfnp mus return a proof for the one quantifier elimination (existential) *)
-(* All these function are independent of the theory on whitch we are trying to prove quantifier elimination*)
-(* But the following invariants mus be respected : *)
-(* afnp : term -> string list -> thm*)
-(* nfnp : term -> thm*)
-(* qfnp : term -> string list -> thm*)
-(*For all theorms generated by these function must hold :*)
-(* All of them are logical equivalences.*)
-(* on left side of the equivalence must appear the term exactely as ist was given as a parameter (or eventually modulo Gamma, where Gamma are the rules whitch are allowed to be used during unification ex. beta reduction.....)*)
-(* qfnp must take as an argument for the term an existential quantified formula*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
+ |(Const("All",_)$Abs(xn,xT,p)) => ([(HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p)], fn [th] => th RS qe_ALL)
+ | _ => ([],fn [] => instantiate' [Some (ctyp_of sg (type_of P))] [Some (cterm_of sg P)] refl);
+
-fun proof_of_mlift_qelim sg isat afnp nfnp qfnp =
- let fun h_proof_of_mlift_qelim isat afnp nfnp qfnp prtkl vrl =
- (case prtkl of
- mAFN (fm) => afnp vrl fm
- |mNFN (prt) => let val th1 = h_proof_of_mlift_qelim isat afnp nfnp qfnp prt vrl
- val th2 = nfnp (snd (qe_get_terms th1))
- in [th1,th2] MRS trans
- end
- |mQeConst (s,pr1,pr2) =>
- let val th1 = h_proof_of_mlift_qelim isat afnp nfnp qfnp pr1 vrl
- val th2 = h_proof_of_mlift_qelim isat afnp nfnp qfnp pr2 vrl
- in (case s of
- "CJ" => [th1,th2] MRS (qe_conjI)
- |"DJ" => [th1,th2] MRS (qe_disjI)
- |"IM" => [th1,th2] MRS (qe_impI)
- |"EQ" => [th1,th2] MRS (qe_eqI)
- )
- end
- |mQeNot (pr) =>(h_proof_of_mlift_qelim isat afnp nfnp qfnp pr vrl ) RS (qe_Not)
- |mQeAll(pr) => (h_proof_of_mlift_qelim isat afnp nfnp qfnp pr vrl ) RS (qe_ALL)
- |mQelim (x as (Free(xn,xT)),vl,pr) =>
- let val th_1 = h_proof_of_mlift_qelim isat afnp nfnp qfnp pr vl
- val mQeProof(l2,pr2) = mlift_qelim_wp isat (xn::vrl) (snd(qe_get_terms th_1))
- val th_2 = [th_1,(h_proof_of_mlift_qelim isat afnp nfnp qfnp pr2 l2)] MRS trans
- val th1 = (forall_intr (cterm_of sg x) th_2) COMP (qe_exI)
- val th2 = qfnp vl (snd (qe_get_terms th1))
- in [th1,th2] MRS trans
- end
- |mQefm (fm) => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl
-)
-in (fn fm => let val mQeProof(vars,prt) = (mlift_qelim_wp isat (fv fm) fm)
- in (h_proof_of_mlift_qelim isat afnp nfnp qfnp prt vars)
- end)
+fun tproof_of_mlift_qelim sg isat afnp nfnp qfnp p =
+ let val th1 = thm_of sg (decomp_qe isat afnp nfnp qfnp sg) p
+ val th2 = nfnp (snd (qe_get_terms th1))
+ in [th1,th2] MRS trans
+ end;
end;
-
-end;
--- a/src/HOL/Presburger.thy Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/Presburger.thy Wed May 19 11:23:59 2004 +0200
@@ -978,11 +978,11 @@
\medskip Specific instances of congruence rules, to prevent
simplifier from looping. *}
-theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
+theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
by simp
-theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<and> P) = (0 <= x \<and> P')"
- by simp
+theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
+ by (simp cong: conj_cong)
use "cooper_dec.ML"
use "cooper_proof.ML"
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Wed May 19 11:23:59 2004 +0200
@@ -29,10 +29,16 @@
val aset : term -> term -> term list
val linrep : string list -> term -> term -> term -> term
val list_disj : term list -> term
+ val list_conj : term list -> term
val simpl : term -> term
val fv : term -> string list
val negate : term -> term
val operations : (string * (int * int -> bool)) list
+ val conjuncts : term -> term list
+ val disjuncts : term -> term list
+ val has_bound : term -> bool
+ val minusinf : term -> term -> term
+ val plusinf : term -> term -> term
end;
structure CooperDec : COOPER_DEC =
@@ -183,7 +189,7 @@
else (warning "lint: apparent nonlinearity"; raise COOPER)
end
- |_ => error "lint: unknown term";
+ |_ => (error "COOPER:lint: unknown term ")
--- a/src/HOL/Tools/Presburger/cooper_proof.ML Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML Wed May 19 11:23:59 2004 +0200
@@ -16,35 +16,25 @@
val qe_eqI : thm
val qe_exI : thm
val qe_get_terms : thm -> term * term
- val cooper_prv : Sign.sg -> term -> term -> string list -> thm
+ val cooper_prv : Sign.sg -> term -> term -> thm
val proof_of_evalc : Sign.sg -> term -> thm
val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
val proof_of_linform : Sign.sg -> string list -> term -> thm
+ val prove_elementar : Sign.sg -> string -> term -> thm
+ val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
end;
structure CooperProof : COOPER_PROOF =
struct
-
open CooperDec;
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*--- ---*)
-(*--- ---*)
-(*--- Protocoling part ---*)
-(*--- ---*)
-(*--- includes the protocolling datastructure ---*)
-(*--- ---*)
-(*--- and the protocolling fuctions ---*)
-(*--- ---*)
-(*--- ---*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
+(*
+val presburger_ss = simpset_of (theory "Presburger")
+ addsimps [zdiff_def] delsimps [symmetric zdiff_def];
+*)
val presburger_ss = simpset_of (theory "Presburger")
- addsimps [diff_int_def] delsimps [thm"diff_int_def_symmetric"];
+ addsimps[diff_int_def] delsimps [thm"diff_int_def_symmetric"];
val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
(*Theorems that will be used later for the proofgeneration*)
@@ -52,7 +42,7 @@
val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
val unity_coeff_ex = thm "unity_coeff_ex";
-(* Theorems for proving the adjustment of the coefficients*)
+(* Thorems for proving the adjustment of the coeffitients*)
val ac_lt_eq = thm "ac_lt_eq";
val ac_eq_eq = thm "ac_eq_eq";
@@ -68,7 +58,7 @@
val qe_exI = thm "qe_exI";
val qe_ALLI = thm "qe_ALLI";
-(*Modulo D property for Pminusinf and Plusinf *)
+(*Modulo D property for Pminusinf an Plusinf *)
val fm_modd_minf = thm "fm_modd_minf";
val not_dvd_modd_minf = thm "not_dvd_modd_minf";
val dvd_modd_minf = thm "dvd_modd_minf";
@@ -77,7 +67,7 @@
val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
val dvd_modd_pinf = thm "dvd_modd_pinf";
-(* the minusinfinity property*)
+(* the minusinfinity proprty*)
val fm_eq_minf = thm "fm_eq_minf";
val neq_eq_minf = thm "neq_eq_minf";
@@ -87,7 +77,7 @@
val not_dvd_eq_minf = thm "not_dvd_eq_minf";
val dvd_eq_minf = thm "dvd_eq_minf";
-(* the Plusinfinity property*)
+(* the Plusinfinity proprty*)
val fm_eq_pinf = thm "fm_eq_pinf";
val neq_eq_pinf = thm "neq_eq_pinf";
@@ -108,7 +98,6 @@
val modd_pinf_disjI = thm "modd_pinf_disjI";
val modd_pinf_conjI = thm "modd_pinf_conjI";
-
(*Cooper Backwards...*)
(*Bset*)
val not_bst_p_fm = thm "not_bst_p_fm";
@@ -166,81 +155,6 @@
val lf_dvd = thm "lf_dvd";
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the cooperprocedure.*)
-(* ------------------------------------------------------------------------- *)
-
-
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the adjustcoeff step.*)
-(* ------------------------------------------------------------------------- *)
-datatype CpLog = No
- |Simp of term*CpLog
- |Blast of CpLog*CpLog
- |Aset of (term*term*(term list)*term)
- |Bset of (term*term*(term list)*term)
- |Minusinf of CpLog*CpLog
- |Cooper of term*CpLog*CpLog*CpLog
- |Eq_minf of term*term
- |Modd_minf of term*term
- |Eq_minf_conjI of CpLog*CpLog
- |Modd_minf_conjI of CpLog*CpLog
- |Modd_minf_disjI of CpLog*CpLog
- |Eq_minf_disjI of CpLog*CpLog
- |Not_bst_p of term*term*term*term*CpLog
- |Not_bst_p_atomic of term
- |Not_bst_p_conjI of CpLog*CpLog
- |Not_bst_p_disjI of CpLog*CpLog
- |Not_ast_p of term*term*term*term*CpLog
- |Not_ast_p_atomic of term
- |Not_ast_p_conjI of CpLog*CpLog
- |Not_ast_p_disjI of CpLog*CpLog
- |CpLogError;
-
-
-
-datatype ACLog = ACAt of int*term
- |ACPI of int*term
- |ACfm of term
- |ACNeg of ACLog
- |ACConst of string*ACLog*ACLog;
-
-
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the CNNF step.*)
-(* ------------------------------------------------------------------------- *)
-
-
-datatype NNFLog = NNFAt of term
- |NNFSimp of NNFLog
- |NNFNN of NNFLog
- |NNFConst of string*NNFLog*NNFLog;
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the linform step.*)
-(* ------------------------------------------------------------------------- *)
-
-
-datatype LfLog = LfAt of term
- |LfAtdvd of term
- |Lffm of term
- |LfConst of string*LfLog*LfLog
- |LfNot of LfLog
- |LfQ of string*string*typ*LfLog;
-
-
-(* ------------------------------------------------------------------------- *)
-(*Datatatype declarations for Proofprotocol for the evaluation- evalc- step.*)
-(* ------------------------------------------------------------------------- *)
-
-
-datatype EvalLog = EvalAt of term
- |Evalfm of term
- |EvalConst of string*EvalLog*EvalLog;
-
(* ------------------------------------------------------------------------- *)
(*This function norm_zero_one replaces the occurences of Numeral1 and Numeral0*)
(*Respectively by their abstract representation Const("1",..) and COnst("0",..)*)
@@ -258,214 +172,6 @@
|(Abs(x,T,p)) => (Abs(x,T,(norm_zero_one p)))
|_ => fm;
-
-(* ------------------------------------------------------------------------- *)
-(* Intended to tell that here we changed the structure of the formula with respect to the posineq theorem : ~(0 < t) = 0 < 1-t*)
-(* ------------------------------------------------------------------------- *)
-fun adjustcoeffeq_wp x l fm =
- case fm of
- (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $ c $ y ) $z )))) =>
- if (x = y)
- then let
- val m = l div (dest_numeral c)
- val n = abs (m)
- val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
- val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
- in (ACPI(n,fm),rs)
- end
- else let val rs = (HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt ))
- in (ACPI(1,fm),rs)
- end
-
- |(Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $
- c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then
- let val m = l div (dest_numeral c)
- val n = (if p = "op <" then abs(m) else m)
- val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
- val rs = (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
- in (ACAt(n,fm),rs)
- end
- else (ACfm(fm),fm)
- |( Const ("Not", _) $ p) => let val (rsp,rsr) = adjustcoeffeq_wp x l p
- in (ACNeg(rsp),HOLogic.Not $ rsr)
- end
- |( Const ("op &",_) $ p $ q) =>let val (rspp,rspr) = adjustcoeffeq_wp x l p
- val (rsqp,rsqr) = adjustcoeffeq_wp x l q
-
- in (ACConst ("CJ",rspp,rsqp), HOLogic.mk_conj (rspr,rsqr))
- end
- |( Const ("op |",_) $ p $ q) =>let val (rspp,rspr) = adjustcoeffeq_wp x l p
- val (rsqp,rsqr) = adjustcoeffeq_wp x l q
-
- in (ACConst ("DJ",rspp,rsqp), HOLogic.mk_disj (rspr,rsqr))
- end
-
- |_ => (ACfm(fm),fm);
-
-
-(*_________________________________________*)
-(*-----------------------------------------*)
-(* Protocol generation for the liform step *)
-(*_________________________________________*)
-(*-----------------------------------------*)
-
-
-fun linform_wp fm =
- let fun at_linform_wp at =
- case at of
- (Const("op <=",_)$s$t) => LfAt(at)
- |(Const("op <",_)$s$t) => LfAt(at)
- |(Const("op =",_)$s$t) => LfAt(at)
- |(Const("Divides.op dvd",_)$s$t) => LfAtdvd(at)
- in
- if is_arith_rel fm
- then at_linform_wp fm
- else case fm of
- (Const("Not",_) $ A) => LfNot(linform_wp A)
- |(Const("op &",_)$ A $ B) => LfConst("CJ",linform_wp A, linform_wp B)
- |(Const("op |",_)$ A $ B) => LfConst("DJ",linform_wp A, linform_wp B)
- |(Const("op -->",_)$ A $ B) => LfConst("IM",linform_wp A, linform_wp B)
- |(Const("op =",Type ("fun",[Type ("bool", []),_]))$ A $ B) => LfConst("EQ",linform_wp A, linform_wp B)
- |Const("Ex",_)$Abs(x,T,p) =>
- let val (xn,p1) = variant_abs(x,T,p)
- in LfQ("Ex",xn,T,linform_wp p1)
- end
- |Const("All",_)$Abs(x,T,p) =>
- let val (xn,p1) = variant_abs(x,T,p)
- in LfQ("All",xn,T,linform_wp p1)
- end
-end;
-
-
-(* ------------------------------------------------------------------------- *)
-(*For simlified formulas we just notice the original formula, for whitch we habe been
-intendes to make the proof.*)
-(* ------------------------------------------------------------------------- *)
-fun simpl_wp (fm,pr) = let val fm2 = simpl fm
- in (fm2,Simp(fm,pr))
- end;
-
-
-(* ------------------------------------------------------------------------- *)
-(*Help function for the generation of the proof EX.P_{minus \infty} --> EX. P(x) *)
-(* ------------------------------------------------------------------------- *)
-fun minusinf_wph x fm = let fun mk_atomar_minusinf_proof x fm = (Modd_minf(x,fm),Eq_minf(x,fm))
-
- fun combine_minusinf_proofs opr (ppr1,ppr2) (qpr1,qpr2) = case opr of
- "CJ" => (Modd_minf_conjI(ppr1,qpr1),Eq_minf_conjI(ppr2,qpr2))
- |"DJ" => (Modd_minf_disjI(ppr1,qpr1),Eq_minf_disjI(ppr2,qpr2))
- in
-
- case fm of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
- if (x=y) andalso (c1= zero) andalso (c2= one) then (HOLogic.true_const ,(mk_atomar_minusinf_proof x fm))
- else (fm ,(mk_atomar_minusinf_proof x fm))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
- if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
- then (HOLogic.false_const ,(mk_atomar_minusinf_proof x fm))
- else (fm,(mk_atomar_minusinf_proof x fm))
- |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y ) $ z )) =>
- if (y=x) andalso (c1 = zero) then
- if c2 = one then (HOLogic.false_const,(mk_atomar_minusinf_proof x fm)) else
- (HOLogic.true_const,(mk_atomar_minusinf_proof x fm))
- else (fm,(mk_atomar_minusinf_proof x fm))
-
- |(Const("Not",_)$(Const ("Divides.op dvd",_) $_ )) => (fm,mk_atomar_minusinf_proof x fm)
-
- |(Const ("Divides.op dvd",_) $_ ) => (fm,mk_atomar_minusinf_proof x fm)
-
- |(Const ("op &",_) $ p $ q) => let val (pfm,ppr) = minusinf_wph x p
- val (qfm,qpr) = minusinf_wph x q
- val pr = (combine_minusinf_proofs "CJ" ppr qpr)
- in
- (HOLogic.conj $ pfm $qfm , pr)
- end
- |(Const ("op |",_) $ p $ q) => let val (pfm,ppr) = minusinf_wph x p
- val (qfm,qpr) = minusinf_wph x q
- val pr = (combine_minusinf_proofs "DJ" ppr qpr)
- in
- (HOLogic.disj $ pfm $qfm , pr)
- end
-
- |_ => (fm,(mk_atomar_minusinf_proof x fm))
-
- end;
-(* ------------------------------------------------------------------------- *) (* Protokol for the Proof of the property of the minusinfinity formula*)
-(* Just combines the to protokols *)
-(* ------------------------------------------------------------------------- *)
-fun minusinf_wp x fm = let val (fm2,pr) = (minusinf_wph x fm)
- in (fm2,Minusinf(pr))
- end;
-
-(* ------------------------------------------------------------------------- *)
-(*Help function for the generation of the proof EX.P_{plus \infty} --> EX. P(x) *)
-(* ------------------------------------------------------------------------- *)
-
-fun plusinf_wph x fm = let fun mk_atomar_plusinf_proof x fm = (Modd_minf(x,fm),Eq_minf(x,fm))
-
- fun combine_plusinf_proofs opr (ppr1,ppr2) (qpr1,qpr2) = case opr of
- "CJ" => (Modd_minf_conjI(ppr1,qpr1),Eq_minf_conjI(ppr2,qpr2))
- |"DJ" => (Modd_minf_disjI(ppr1,qpr1),Eq_minf_disjI(ppr2,qpr2))
- in
-
- case fm of
- (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
- if (x=y) andalso (c1= zero) andalso (c2= one) then (HOLogic.true_const ,(mk_atomar_plusinf_proof x fm))
- else (fm ,(mk_atomar_plusinf_proof x fm))
- |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
- if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one)
- then (HOLogic.false_const ,(mk_atomar_plusinf_proof x fm))
- else (fm,(mk_atomar_plusinf_proof x fm))
- |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y ) $ z )) =>
- if (y=x) andalso (c1 = zero) then
- if c2 = one then (HOLogic.true_const,(mk_atomar_plusinf_proof x fm)) else
- (HOLogic.false_const,(mk_atomar_plusinf_proof x fm))
- else (fm,(mk_atomar_plusinf_proof x fm))
-
- |(Const("Not",_)$(Const ("Divides.op dvd",_) $_ )) => (fm,mk_atomar_plusinf_proof x fm)
-
- |(Const ("Divides.op dvd",_) $_ ) => (fm,mk_atomar_plusinf_proof x fm)
-
- |(Const ("op &",_) $ p $ q) => let val (pfm,ppr) = plusinf_wph x p
- val (qfm,qpr) = plusinf_wph x q
- val pr = (combine_plusinf_proofs "CJ" ppr qpr)
- in
- (HOLogic.conj $ pfm $qfm , pr)
- end
- |(Const ("op |",_) $ p $ q) => let val (pfm,ppr) = plusinf_wph x p
- val (qfm,qpr) = plusinf_wph x q
- val pr = (combine_plusinf_proofs "DJ" ppr qpr)
- in
- (HOLogic.disj $ pfm $qfm , pr)
- end
-
- |_ => (fm,(mk_atomar_plusinf_proof x fm))
-
- end;
-(* ------------------------------------------------------------------------- *) (* Protokol for the Proof of the property of the minusinfinity formula*)
-(* Just combines the to protokols *)
-(* ------------------------------------------------------------------------- *)
-fun plusinf_wp x fm = let val (fm2,pr) = (plusinf_wph x fm)
- in (fm2,Minusinf(pr))
- end;
-
-
-(* ------------------------------------------------------------------------- *)
-(*Protocol that we here uses Bset.*)
-(* ------------------------------------------------------------------------- *)
-fun bset_wp x fm = let val bs = bset x fm in
- (bs,Bset(x,fm,bs,mk_numeral (divlcm x fm)))
- end;
-
-(* ------------------------------------------------------------------------- *)
-(*Protocol that we here uses Aset.*)
-(* ------------------------------------------------------------------------- *)
-fun aset_wp x fm = let val ast = aset x fm in
- (ast,Aset(x,fm,ast,mk_numeral (divlcm x fm)))
- end;
-
-
-
(* ------------------------------------------------------------------------- *)
(*function list to Set, constructs a set containing all elements of a given list.*)
(* ------------------------------------------------------------------------- *)
@@ -475,181 +181,11 @@
|(h::t) => Const("insert", T1 --> (T --> T)) $ h $(list_to_set T1 t)
end;
-
-(*====================================================================*)
-(* ------------------------------------------------------------------------- *)
-(* ------------------------------------------------------------------------- *)
-(*Protocol for the proof of the backward direction of the cooper theorem.*)
-(* Helpfunction - Protokols evereything about the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_bst_p_wph fm = case fm of
- Const("Not",_) $ R => if (is_arith_rel R) then (Not_bst_p_atomic (fm)) else CpLogError
- |Const("op &",_) $ ls $ rs => Not_bst_p_conjI((not_bst_p_wph ls),(not_bst_p_wph rs))
- |Const("op |",_) $ ls $ rs => Not_bst_p_disjI((not_bst_p_wph ls),(not_bst_p_wph rs))
- |_ => Not_bst_p_atomic (fm);
-(* ------------------------------------------------------------------------- *)
-(* Main protocoling function for the backward direction gives the Bset and the divlcm and the Formula herself. Needed as inherited attributes for the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_bst_p_wp x fm = let val prt = not_bst_p_wph fm
- val D = mk_numeral (divlcm x fm)
- val B = map norm_zero_one (bset x fm)
- in (Not_bst_p (x,fm,D,(list_to_set HOLogic.intT B) , prt))
- end;
-(*====================================================================*)
-(* ------------------------------------------------------------------------- *)
-(* ------------------------------------------------------------------------- *)
-(*Protocol for the proof of the backward direction of the cooper theorem.*)
-(* Helpfunction - Protokols evereything about the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_ast_p_wph fm = case fm of
- Const("Not",_) $ R => if (is_arith_rel R) then (Not_ast_p_atomic (fm)) else CpLogError
- |Const("op &",_) $ ls $ rs => Not_ast_p_conjI((not_ast_p_wph ls),(not_ast_p_wph rs))
- |Const("op |",_) $ ls $ rs => Not_ast_p_disjI((not_ast_p_wph ls),(not_ast_p_wph rs))
- |_ => Not_ast_p_atomic (fm);
-(* ------------------------------------------------------------------------- *)
-(* Main protocoling function for the backward direction gives the Bset and the divlcm and the Formula herself. Needed as inherited attributes for the proof reconstruction*)
-(* ------------------------------------------------------------------------- *)
-fun not_ast_p_wp x fm = let val prt = not_ast_p_wph fm
- val D = mk_numeral (divlcm x fm)
- val B = map norm_zero_one (aset x fm)
- in (Not_ast_p (x,fm,D,(list_to_set HOLogic.intT B) , prt))
- end;
-
-(*======================================================*)
-(* Protokolgeneration for the formula evaluation process*)
-(*======================================================*)
-
-fun evalc_wp fm =
- let fun evalc_atom_wp at =case at of
- (Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
- Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then EvalAt(HOLogic.mk_eq(at,HOLogic.true_const)) else EvalAt(HOLogic.mk_eq(at, HOLogic.false_const)))
- handle _ => Evalfm(at))
- | _ => Evalfm(at))
- |Const("Not",_)$(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
- Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then
- EvalAt(HOLogic.mk_eq(at, HOLogic.false_const)) else EvalAt(HOLogic.mk_eq(at,HOLogic.true_const)))
- handle _ => Evalfm(at))
- | _ => Evalfm(at))
- | _ => Evalfm(at)
-
- in
- case fm of
- (Const("op &",_)$A$B) => EvalConst("CJ",evalc_wp A,evalc_wp B)
- |(Const("op |",_)$A$B) => EvalConst("DJ",evalc_wp A,evalc_wp B)
- |(Const("op -->",_)$A$B) => EvalConst("IM",evalc_wp A,evalc_wp B)
- |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => EvalConst("EQ",evalc_wp A,evalc_wp B)
- |_ => evalc_atom_wp fm
- end;
-
-
-
-(*======================================================*)
-(* Protokolgeneration for the NNF Transformation *)
-(*======================================================*)
-
-fun cnnf_wp f =
- let fun hcnnf_wp fm =
- case fm of
- (Const ("op &",_) $ p $ q) => NNFConst("CJ",hcnnf_wp p,hcnnf_wp q)
- | (Const ("op |",_) $ p $ q) => NNFConst("DJ",hcnnf_wp p,hcnnf_wp q)
- | (Const ("op -->",_) $ p $q) => NNFConst("IM",hcnnf_wp (HOLogic.Not $ p),hcnnf_wp q)
- | (Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q) => NNFConst("EQ",hcnnf_wp (HOLogic.mk_conj(p,q)),hcnnf_wp (HOLogic.mk_conj((HOLogic.Not $ p), (HOLogic.Not $ q))))
-
- | (Const ("Not",_) $ (Const("Not",_) $ p)) => NNFNN(hcnnf_wp p)
- | (Const ("Not",_) $ (Const ("op &",_) $ p $ q)) => NNFConst ("NCJ",(hcnnf_wp(HOLogic.Not $ p)),(hcnnf_wp(HOLogic.Not $ q)))
- | (Const ("Not",_) $(Const ("op |",_) $ (A as (Const ("op &",_) $ p $ q)) $
- (B as (Const ("op &",_) $ p1 $ r)))) => if p1 = negate p then
- NNFConst("SDJ",
- NNFConst("CJ",hcnnf_wp p,hcnnf_wp(HOLogic.Not $ q)),
- NNFConst("CJ",hcnnf_wp p1,hcnnf_wp(HOLogic.Not $ r)))
- else NNFConst ("NDJ",(hcnnf_wp(HOLogic.Not $ A)),(hcnnf_wp(HOLogic.Not $ B)))
-
- | (Const ("Not",_) $ (Const ("op |",_) $ p $ q)) => NNFConst ("NDJ",(hcnnf_wp(HOLogic.Not $ p)),(hcnnf_wp(HOLogic.Not $ q)))
- | (Const ("Not",_) $ (Const ("op -->",_) $ p $q)) => NNFConst ("NIM",(hcnnf_wp(p)),(hcnnf_wp(HOLogic.Not $ q)))
- | (Const ("Not",_) $ (Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q)) =>NNFConst ("NEQ",(NNFConst("CJ",hcnnf_wp p,hcnnf_wp(HOLogic.Not $ q))),(NNFConst("CJ",hcnnf_wp(HOLogic.Not $ p),hcnnf_wp q)))
- | _ => NNFAt(fm)
- in NNFSimp(hcnnf_wp f)
-end;
-
-
-
-
-
-
-(* ------------------------------------------------------------------------- *)
-(*Cooper decision Procedure with proof protocoling*)
-(* ------------------------------------------------------------------------- *)
-
-fun coopermi_wp vars fm =
- case fm of
- Const ("Ex",_) $ Abs(xo,T,po) => let
- val (xn,np) = variant_abs(xo,T,po)
- val x = (Free(xn , T))
- val p = np (* Is this a legal proof for the P=NP Problem??*)
- val (p_inf,miprt) = simpl_wp (minusinf_wp x p)
- val (bset,bsprt) = bset_wp x p
- val nbst_p_prt = not_bst_p_wp x p
- val dlcm = divlcm x p
- val js = 1 upto dlcm
- fun p_element j b = linrep vars x (linear_add vars b (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) bset)
- in (list_disj (map stage js),Cooper(mk_numeral dlcm,miprt,bsprt,nbst_p_prt))
- end
-
- | _ => (error "cooper: not an existential formula",No);
-
-fun cooperpi_wp vars fm =
- case fm of
- Const ("Ex",_) $ Abs(xo,T,po) => let
- val (xn,np) = variant_abs(xo,T,po)
- val x = (Free(xn , T))
- val p = np (* Is this a legal proof for the P=NP Problem??*)
- val (p_inf,piprt) = simpl_wp (plusinf_wp x p)
- val (aset,asprt) = aset_wp x p
- val nast_p_prt = not_ast_p_wp x p
- val dlcm = divlcm x p
- val js = 1 upto dlcm
- fun p_element j a = linrep vars x (linear_sub vars a (mk_numeral j)) p
- fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) aset)
- in (list_disj (map stage js),Cooper(mk_numeral dlcm,piprt,asprt,nast_p_prt))
- end
- | _ => (error "cooper: not an existential formula",No);
-
-
-
-
-
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*--- ---*)
-(*--- ---*)
-(*--- Interpretation and Proofgeneration Part ---*)
-(*--- ---*)
-(*--- Protocole interpretation functions ---*)
-(*--- ---*)
-(*--- and proofgeneration functions ---*)
-(*--- ---*)
-(*--- ---*)
-(*--- ---*)
-(*--- ---*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-
(* ------------------------------------------------------------------------- *)
(* Returns both sides of an equvalence in the theorem*)
(* ------------------------------------------------------------------------- *)
fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end;
-
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-
(* ------------------------------------------------------------------------- *)
(* Modified version of the simple version with minimal amount of checking and postprocessing*)
(* ------------------------------------------------------------------------- *)
@@ -664,9 +200,6 @@
(*-------------------------------------------------------------*)
(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
-(*-------------------------------------------------------------*)
fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t);
@@ -680,7 +213,8 @@
(*"ss" like simplification with simpset*)
"ss" =>
let
- val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0]
+ val ss = presburger_ss addsimps
+ [zdvd_iff_zmod_eq_0,unity_coeff_ex]
val ct = cert_Trueprop sg fm2
in
simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
@@ -725,6 +259,14 @@
in
simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
end
+ (* like Existance Conjunction *)
+ | "ec" =>
+ let
+ val ss = presburger_ss addsimps zadd_ac
+ val ct = cert_Trueprop sg fm2
+ in
+ simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (blast_tac HOL_cs 1)]
+ end
| "ac" =>
let
@@ -742,80 +284,92 @@
simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
end;
+(*=============================================================*)
+(*-------------------------------------------------------------*)
+(* The new compact model *)
+(*-------------------------------------------------------------*)
+(*=============================================================*)
+fun thm_of sg decomp t =
+ let val (ts,recomb) = decomp t
+ in recomb (map (thm_of sg decomp) ts)
+ end;
+
+(*==================================================*)
+(* Compact Version for adjustcoeffeq *)
+(*==================================================*)
+
+fun decomp_adjustcoeffeq sg x l fm = case fm of
+ (Const("Not",_)$(Const("op <",_) $(Const("0",_)) $(rt as (Const ("op +", _)$(Const ("op *",_) $ c $ y ) $z )))) =>
+ let
+ val m = l div (dest_numeral c)
+ val n = if (x = y) then abs (m) else 1
+ val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x))
+ val rs = if (x = y)
+ then (HOLogic.mk_binrel "op <" (zero,linear_sub [] (mk_numeral n) (HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) ))))
+ else HOLogic.mk_binrel "op <" (zero,linear_sub [] one rt )
+ val ck = cterm_of sg (mk_numeral n)
+ val cc = cterm_of sg c
+ val ct = cterm_of sg z
+ val cx = cterm_of sg y
+ val pre = prove_elementar sg "lf"
+ (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral n)))
+ val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
+ in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
+ end
-(* ------------------------------------------------------------------------- *)
-(* This function return an Isabelle proof, of the adjustcoffeq result.*)
-(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
-(* ------------------------------------------------------------------------- *)
-fun proof_of_adjustcoeffeq sg (prt,rs) = case prt of
- ACfm fm => instantiate' [Some cboolT]
- [Some (cterm_of sg fm)] refl
- | ACAt (k,at as (Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $
- c $ x ) $t ))) =>
- let
- val ck = cterm_of sg (mk_numeral k)
- val cc = cterm_of sg c
- val ct = cterm_of sg t
- val cx = cterm_of sg x
- val ca = cterm_of sg a
- in case p of
- "op <" => let val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
- val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
- in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
- end
- |"op =" =>let val pre = prove_elementar sg "lf"
+ |(Const(p,_) $a $( Const ("op +", _)$(Const ("op *",_) $
+ c $ y ) $t )) =>
+ if (is_arith_rel fm) andalso (x = y)
+ then
+ let val m = l div (dest_numeral c)
+ val k = (if p = "op <" then abs(m) else m)
+ val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div k)*l) ), x))
+ val rs = (HOLogic.mk_binrel p ((linear_cmul k a),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul k t) ))))
+
+ val ck = cterm_of sg (mk_numeral k)
+ val cc = cterm_of sg c
+ val ct = cterm_of sg t
+ val cx = cterm_of sg x
+ val ca = cterm_of sg a
+
+ in
+ case p of
+ "op <" =>
+ let val pre = prove_elementar sg "lf"
+ (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
+ val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
+ in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
+ end
+
+ |"op =" =>
+ let val pre = prove_elementar sg "lf"
(HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
- in let val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
- in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
- end
- end
- |"Divides.op dvd" =>let val pre = prove_elementar sg "lf"
+ val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
+ in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
+ end
+
+ |"Divides.op dvd" =>
+ let val pre = prove_elementar sg "lf"
(HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
- val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
- in [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
+ val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
+ in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
- end
- end
- |ACPI(k,at as (Const("Not",_)$(Const("op <",_) $a $( Const ("op +", _)$(Const ("op *",_) $ c $ x ) $t )))) =>
- let
- val ck = cterm_of sg (mk_numeral k)
- val cc = cterm_of sg c
- val ct = cterm_of sg t
- val cx = cterm_of sg x
- val pre = prove_elementar sg "lf"
- (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
- val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
+ end
+ end
+ else ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl)
+
+ |( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not)
+ |( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+ |( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI)
- in [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans
- end
- |ACNeg(pr) => let val (Const("Not",_)$nrs) = rs
- in (proof_of_adjustcoeffeq sg (pr,nrs)) RS (qe_Not)
- end
- |ACConst(s,pr1,pr2) =>
- let val (Const(_,_)$rs1$rs2) = rs
- val th1 = proof_of_adjustcoeffeq sg (pr1,rs1)
- val th2 = proof_of_adjustcoeffeq sg (pr2,rs2)
- in case s of
- "CJ" => [th1,th2] MRS (qe_conjI)
- |"DJ" => [th1,th2] MRS (qe_disjI)
- |"IM" => [th1,th2] MRS (qe_impI)
- |"EQ" => [th1,th2] MRS (qe_eqI)
- end;
+ |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
-
-
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* This function return an Isabelle proof, of some properties on the atoms*)
-(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
-(* This function doese only instantiate the the theorems in the theory *)
-(* ------------------------------------------------------------------------- *)
-fun atomar_minf_proof_of sg dlcm (Modd_minf (x,fm1)) =
- let
+(*==================================================*)
+(* Finding rho for modd_minusinfinity *)
+(*==================================================*)
+fun rho_for_modd_minf x dlcm sg fm1 =
+let
(*Some certified Terms*)
val ctrue = cterm_of sg HOLogic.true_const
@@ -853,10 +407,11 @@
|_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)
- end
-
- |atomar_minf_proof_of sg dlcm (Eq_minf (x,fm1)) = let
- (*Some certified types*)
+ end;
+(*=========================================================================*)
+(*=========================================================================*)
+fun rho_for_eq_minf x dlcm sg fm1 =
+ let
val fm = norm_zero_one fm1
in case fm1 of
(Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
@@ -893,70 +448,24 @@
|_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
end;
-
-(* ------------------------------------------------------------------------- *)
-(* This function combines proofs of some special form already synthetised from the subtrees to make*)
-(* a new proof of the same form. The combination occures whith isabelle theorems which have been already prooved *)
-(*these Theorems are in Presburger.thy and mostly do not relay on the arithmetic.*)
-(* These are Theorems for the Property of P_{-infty}*)
-(* ------------------------------------------------------------------------- *)
-fun combine_minf_proof s pr1 pr2 = case s of
- "ECJ" => [pr1 , pr2] MRS (eq_minf_conjI)
-
- |"EDJ" => [pr1 , pr2] MRS (eq_minf_disjI)
-
- |"MCJ" => [pr1 , pr2] MRS (modd_minf_conjI)
-
- |"MDJ" => [pr1 , pr2] MRS (modd_minf_disjI);
-
-(* ------------------------------------------------------------------------- *)
-(*This function return an isabelle Proof for the minusinfinity theorem*)
-(* It interpretates the protool and gives the protokoles property of P_{...} as a theorem*)
-(* ------------------------------------------------------------------------- *)
-fun minf_proof_ofh sg dlcm prl = case prl of
+(*=====================================================*)
+(*=====================================================*)
+(*=========== minf proofs with the compact version==========*)
+fun decomp_minf_eq x dlcm sg t = case t of
+ Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_conjI)
+ |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_minf_disjI)
+ |_ => ([],fn [] => rho_for_eq_minf x dlcm sg t);
- Eq_minf (_) => atomar_minf_proof_of sg dlcm prl
-
- |Modd_minf (_) => atomar_minf_proof_of sg dlcm prl
-
- |Eq_minf_conjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
- val pr2 = minf_proof_ofh sg dlcm prl2
- in (combine_minf_proof "ECJ" pr1 pr2)
- end
-
- |Eq_minf_disjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
- val pr2 = minf_proof_ofh sg dlcm prl2
- in (combine_minf_proof "EDJ" pr1 pr2)
- end
-
- |Modd_minf_conjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
- val pr2 = minf_proof_ofh sg dlcm prl2
- in (combine_minf_proof "MCJ" pr1 pr2)
- end
-
- |Modd_minf_disjI (prl1,prl2) => let val pr1 = minf_proof_ofh sg dlcm prl1
- val pr2 = minf_proof_ofh sg dlcm prl2
- in (combine_minf_proof "MDJ" pr1 pr2)
- end;
-(* ------------------------------------------------------------------------- *)
-(* Main function For the rest both properies of P_{..} are needed and here both theorems are returned.*)
-(* ------------------------------------------------------------------------- *)
-fun minf_proof_of sg dlcm (Minusinf (prl1,prl2)) =
- let val pr1 = minf_proof_ofh sg dlcm prl1
- val pr2 = minf_proof_ofh sg dlcm prl2
- in (pr1, pr2)
-end;
-
+fun decomp_minf_modd x dlcm sg t = case t of
+ Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_conjI)
+ |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_minf_disjI)
+ |_ => ([],fn [] => rho_for_modd_minf x dlcm sg t);
-
-
-(* ------------------------------------------------------------------------- *)
-(* This function return an Isabelle proof, of some properties on the atoms*)
-(* The proofs are in Presburger.thy and are generally based on the arithmetic *)
-(* This function doese only instantiate the the theorems in the theory *)
-(* ------------------------------------------------------------------------- *)
-fun atomar_pinf_proof_of sg dlcm (Modd_minf (x,fm1)) =
- let
+(* -------------------------------------------------------------*)
+(* Finding rho for pinf_modd *)
+(* -------------------------------------------------------------*)
+fun rho_for_modd_pinf x dlcm sg fm1 =
+let
(*Some certified Terms*)
val ctrue = cterm_of sg HOLogic.true_const
@@ -996,9 +505,12 @@
|_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf)
- end
-
- |atomar_pinf_proof_of sg dlcm (Eq_minf (x,fm1)) = let
+ end;
+(* -------------------------------------------------------------*)
+(* Finding rho for pinf_eq *)
+(* -------------------------------------------------------------*)
+fun rho_for_eq_pinf x dlcm sg fm1 =
+ let
val fm = norm_zero_one fm1
in case fm1 of
(Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) =>
@@ -1036,67 +548,58 @@
end;
-(* ------------------------------------------------------------------------- *)
-(* This function combines proofs of some special form already synthetised from the subtrees to make*)
-(* a new proof of the same form. The combination occures whith isabelle theorems which have been already prooved *)
-(*these Theorems are in Presburger.thy and mostly do not relay on the arithmetic.*)
-(* These are Theorems for the Property of P_{+infty}*)
-(* ------------------------------------------------------------------------- *)
-fun combine_pinf_proof s pr1 pr2 = case s of
- "ECJ" => [pr1 , pr2] MRS (eq_pinf_conjI)
+
+fun minf_proof_of_c sg x dlcm t =
+ let val minf_eqth = thm_of sg (decomp_minf_eq x dlcm sg) t
+ val minf_moddth = thm_of sg (decomp_minf_modd x dlcm sg) t
+ in (minf_eqth, minf_moddth)
+end;
- |"EDJ" => [pr1 , pr2] MRS (eq_pinf_disjI)
-
- |"MCJ" => [pr1 , pr2] MRS (modd_pinf_conjI)
+(*=========== pinf proofs with the compact version==========*)
+fun decomp_pinf_eq x dlcm sg t = case t of
+ Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_conjI)
+ |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS eq_pinf_disjI)
+ |_ =>([],fn [] => rho_for_eq_pinf x dlcm sg t) ;
- |"MDJ" => [pr1 , pr2] MRS (modd_pinf_disjI);
+fun decomp_pinf_modd x dlcm sg t = case t of
+ Const ("op &",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_conjI)
+ |Const ("op |",_) $ p $q => ([p,q],fn [th1,th2] => [th1,th2] MRS modd_pinf_disjI)
+ |_ => ([],fn [] => rho_for_modd_pinf x dlcm sg t);
+
+fun pinf_proof_of_c sg x dlcm t =
+ let val pinf_eqth = thm_of sg (decomp_pinf_eq x dlcm sg) t
+ val pinf_moddth = thm_of sg (decomp_pinf_modd x dlcm sg) t
+ in (pinf_eqth,pinf_moddth)
+end;
+
(* ------------------------------------------------------------------------- *)
-(*This function return an isabelle Proof for the minusinfinity theorem*)
-(* It interpretates the protool and gives the protokoles property of P_{...} as a theorem*)
+(* Here we generate the theorem for the Bset Property in the simple direction*)
+(* It is just an instantiation*)
(* ------------------------------------------------------------------------- *)
-fun pinf_proof_ofh sg dlcm prl = case prl of
+(*
+fun bsetproof_of sg (x as Free(xn,xT)) fm bs dlcm =
+ let
+ val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
+ val cdlcm = cterm_of sg dlcm
+ val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
+ in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
+end;
- Eq_minf (_) => atomar_pinf_proof_of sg dlcm prl
-
- |Modd_minf (_) => atomar_pinf_proof_of sg dlcm prl
-
- |Eq_minf_conjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
- val pr2 = pinf_proof_ofh sg dlcm prl2
- in (combine_pinf_proof "ECJ" pr1 pr2)
- end
-
- |Eq_minf_disjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
- val pr2 = pinf_proof_ofh sg dlcm prl2
- in (combine_pinf_proof "EDJ" pr1 pr2)
- end
-
- |Modd_minf_conjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
- val pr2 = pinf_proof_ofh sg dlcm prl2
- in (combine_pinf_proof "MCJ" pr1 pr2)
- end
-
- |Modd_minf_disjI (prl1,prl2) => let val pr1 = pinf_proof_ofh sg dlcm prl1
- val pr2 = pinf_proof_ofh sg dlcm prl2
- in (combine_pinf_proof "MDJ" pr1 pr2)
- end;
-(* ------------------------------------------------------------------------- *)
-(* Main function For the rest both properies of P_{..} are needed and here both theorems are returned.*)
-(* ------------------------------------------------------------------------- *)
-fun pinf_proof_of sg dlcm (Minusinf (prl1,prl2)) =
- let val pr1 = pinf_proof_ofh sg dlcm prl1
- val pr2 = pinf_proof_ofh sg dlcm prl2
- in (pr1, pr2)
+fun asetproof_of sg (x as Free(xn,xT)) fm ast dlcm =
+ let
+ val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
+ val cdlcm = cterm_of sg dlcm
+ val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
+ in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
end;
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* Protokol interpretation function for the backwards direction for cooper's Theorem*)
+*)
(* For the generation of atomic Theorems*)
(* Prove the premisses on runtime and then make RS*)
(* ------------------------------------------------------------------------- *)
+
+(*========= this is rho ============*)
fun generate_atomic_not_bst_p sg (x as Free(xn,xT)) fm dlcm B at =
let
val cdlcm = cterm_of sg dlcm
@@ -1157,28 +660,23 @@
end;
+
(* ------------------------------------------------------------------------- *)
(* Main interpretation function for this backwards dirction*)
(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
(*Help Function*)
(* ------------------------------------------------------------------------- *)
-fun not_bst_p_proof_of_h sg x fm dlcm B prt = case prt of
- (Not_bst_p_atomic(fm2)) => (generate_atomic_not_bst_p sg x fm dlcm B fm2)
-
- |(Not_bst_p_conjI(pr1,pr2)) =>
- let val th1 = (not_bst_p_proof_of_h sg x fm dlcm B pr1)
- val th2 = (not_bst_p_proof_of_h sg x fm dlcm B pr2)
- in ([th1,th2] MRS (not_bst_p_conjI))
- end
+
+(*==================== Proof with the compact version *)
- |(Not_bst_p_disjI(pr1,pr2)) =>
- let val th1 = (not_bst_p_proof_of_h sg x fm dlcm B pr1)
- val th2 = (not_bst_p_proof_of_h sg x fm dlcm B pr2)
- in ([th1,th2] MRS not_bst_p_disjI)
- end;
-(* Main function*)
-fun not_bst_p_proof_of sg (Not_bst_p(x as Free(xn,xT),fm,dlcm,B,prl)) =
- let val th = not_bst_p_proof_of_h sg x fm dlcm B prl
+fun decomp_nbstp sg x dlcm B fm t = case t of
+ Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_conjI )
+ |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_bst_p_disjI)
+ |_ => ([], fn [] => generate_atomic_not_bst_p sg x fm dlcm B t);
+
+fun not_bst_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm B t =
+ let
+ val th = thm_of sg (decomp_nbstp sg x dlcm (list_to_set xT (map norm_zero_one B)) fm) t
val fma = absfree (xn,xT, norm_zero_one fm)
in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma))
in [th,th1] MRS (not_bst_p_Q_elim)
@@ -1192,6 +690,7 @@
(* For the generation of atomic Theorems*)
(* Prove the premisses on runtime and then make RS*)
(* ------------------------------------------------------------------------- *)
+(*========= this is rho ============*)
fun generate_atomic_not_ast_p sg (x as Free(xn,xT)) fm dlcm A at =
let
val cdlcm = cterm_of sg dlcm
@@ -1250,81 +749,109 @@
|_ => (instantiate' [] [Some cfma, Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
end;
-
-(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------ *)
(* Main interpretation function for this backwards dirction*)
(* if atomic do generate atomis formulae else Construct theorems and then make RS with the construction theorems*)
(*Help Function*)
(* ------------------------------------------------------------------------- *)
-fun not_ast_p_proof_of_h sg x fm dlcm A prt = case prt of
- (Not_ast_p_atomic(fm2)) => (generate_atomic_not_ast_p sg x fm dlcm A fm2)
-
- |(Not_ast_p_conjI(pr1,pr2)) =>
- let val th1 = (not_ast_p_proof_of_h sg x fm dlcm A pr1)
- val th2 = (not_ast_p_proof_of_h sg x fm dlcm A pr2)
- in ([th1,th2] MRS (not_ast_p_conjI))
- end
+
+fun decomp_nastp sg x dlcm A fm t = case t of
+ Const("op &",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_conjI )
+ |Const("op |",_) $ ls $ rs => ([ls,rs],fn [th1,th2] => [th1,th2] MRS not_ast_p_disjI)
+ |_ => ([], fn [] => generate_atomic_not_ast_p sg x fm dlcm A t);
- |(Not_ast_p_disjI(pr1,pr2)) =>
- let val th1 = (not_ast_p_proof_of_h sg x fm dlcm A pr1)
- val th2 = (not_ast_p_proof_of_h sg x fm dlcm A pr2)
- in ([th1,th2] MRS (not_ast_p_disjI))
- end;
-(* Main function*)
-fun not_ast_p_proof_of sg (Not_ast_p(x as Free(xn,xT),fm,dlcm,A,prl)) =
- let val th = not_ast_p_proof_of_h sg x fm dlcm A prl
+fun not_ast_p_proof_of_c sg (x as Free(xn,xT)) fm dlcm A t =
+ let
+ val th = thm_of sg (decomp_nastp sg x dlcm (list_to_set xT (map norm_zero_one A)) fm) t
val fma = absfree (xn,xT, norm_zero_one fm)
- val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma))
- in [th,th1] MRS (not_ast_p_Q_elim)
-end;
+ in let val th1 = prove_elementar sg "ss" (HOLogic.mk_eq (fma,fma))
+ in [th,th1] MRS (not_ast_p_Q_elim)
+ end
+ end;
+(* -------------------------------*)
+(* Finding rho and beta for evalc *)
+(* -------------------------------*)
+fun rho_for_evalc sg at = case at of
+ (Const (p,_) $ s $ t) =>(
+ case assoc (operations,p) of
+ Some f =>
+ ((if (f ((dest_numeral s),(dest_numeral t)))
+ then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const))
+ else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))
+ handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl
+ | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl ))
+ |Const("Not",_)$(Const (p,_) $ s $ t) =>(
+ case assoc (operations,p) of
+ Some f =>
+ ((if (f ((dest_numeral s),(dest_numeral t)))
+ then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))
+ else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))
+ handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl)
+ | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl )
+ | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl;
+
+
+(*=========================================================*)
+fun decomp_evalc sg t = case t of
+ (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+ |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
+ |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
+ |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
+ |_ => ([], fn [] => rho_for_evalc sg t);
+
+
+fun proof_of_evalc sg fm = thm_of sg (decomp_evalc sg) fm;
+
+(*==================================================*)
+(* Proof of linform with the compact model *)
+(*==================================================*)
+
+
+fun decomp_linform sg vars t = case t of
+ (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+ |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
+ |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
+ |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
+ |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
+ |(Const("Divides.op dvd",_)$d$r) => ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd)))
+ |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
+
+fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f;
(* ------------------------------------------------------------------------- *)
(* Interpretaion of Protocols of the cooper procedure : minusinfinity version*)
(* ------------------------------------------------------------------------- *)
-
-
-fun coopermi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nbst_p_prt)) =
+fun coopermi_proof_of sg (x as Free(xn,xT)) fm B dlcm =
(* Get the Bset thm*)
- let val (mit1,mit2) = minf_proof_of sg dlcm miprt
- val fm1 = norm_zero_one (simpl fm)
+ let val (minf_eqth, minf_moddth) = minf_proof_of_c sg x dlcm fm
val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
- val nbstpthm = not_bst_p_proof_of sg nbst_p_prt
- (* Return the four theorems needed to proove the whole Cooper Theorem*)
- in (dpos,mit2,nbstpthm,mit1)
+ val nbstpthm = not_bst_p_proof_of_c sg x fm dlcm B fm
+ in (dpos,minf_eqth,nbstpthm,minf_moddth)
end;
-
(* ------------------------------------------------------------------------- *)
(* Interpretaion of Protocols of the cooper procedure : plusinfinity version *)
(* ------------------------------------------------------------------------- *)
-
-
-fun cooperpi_proof_of sg x (Cooper (dlcm,Simp(fm,miprt),bsprt,nast_p_prt)) =
- let val (mit1,mit2) = pinf_proof_of sg dlcm miprt
- val fm1 = norm_zero_one (simpl fm)
+fun cooperpi_proof_of sg (x as Free(xn,xT)) fm A dlcm =
+ let val (pinf_eqth,pinf_moddth) = pinf_proof_of_c sg x dlcm fm
val dpos = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm));
- val nastpthm = not_ast_p_proof_of sg nast_p_prt
- in (dpos,mit2,nastpthm,mit1)
+ val nastpthm = not_ast_p_proof_of_c sg x fm dlcm A fm
+ in (dpos,pinf_eqth,nastpthm,pinf_moddth)
end;
-
(* ------------------------------------------------------------------------- *)
(* Interpretaion of Protocols of the cooper procedure : full version*)
(* ------------------------------------------------------------------------- *)
-
-
-
-fun cooper_thm sg s (x as Free(xn,xT)) vars cfm = case s of
- "pi" => let val (rs,prt) = cooperpi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
- val (dpsthm,th1,nbpth,th3) = cooperpi_proof_of sg x prt
- in [dpsthm,th1,nbpth,th3] MRS (cppi_eq)
+fun cooper_thm sg s (x as Free(xn,xT)) cfm dlcm ast bst= case s of
+ "pi" => let val (dpsthm,pinf_eqth,nbpth,pinf_moddth) = cooperpi_proof_of sg x cfm ast dlcm
+ in [dpsthm,pinf_eqth,nbpth,pinf_moddth] MRS (cppi_eq)
end
- |"mi" => let val (rs,prt) = coopermi_wp (xn::vars) (HOLogic.mk_exists(xn,xT,cfm))
- val (dpsthm,th1,nbpth,th3) = coopermi_proof_of sg x prt
- in [dpsthm,th1,nbpth,th3] MRS (cpmi_eq)
+ |"mi" => let val (dpsthm,minf_eqth,nbpth,minf_moddth) = coopermi_proof_of sg x cfm bst dlcm
+ in [dpsthm,minf_eqth,nbpth,minf_moddth] MRS (cpmi_eq)
end
|_ => error "parameter error";
@@ -1333,9 +860,11 @@
(* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
(* ------------------------------------------------------------------------- *)
-fun cooper_prv sg (x as Free(xn,xT)) efm vars = let
- val l = formlcm x efm
- val ac_thm = proof_of_adjustcoeffeq sg (adjustcoeffeq_wp x l efm)
+fun cooper_prv sg (x as Free(xn,xT)) efm = let
+ val lfm_thm = proof_of_linform sg [xn] efm
+ val efm2 = snd(qe_get_terms lfm_thm)
+ val l = formlcm x efm2
+ val ac_thm = [lfm_thm , (thm_of sg (decomp_adjustcoeffeq sg x l) efm2)] MRS trans
val fm = snd (qe_get_terms ac_thm)
val cfm = unitycoeff x fm
val afm = adjustcoeff x l fm
@@ -1344,8 +873,11 @@
[simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
- val cms = if ((length (aset x cfm)) < (length (bset x cfm))) then "pi" else "mi"
- val cp_thm = cooper_thm sg cms x vars cfm
+ val A = aset x cfm
+ val B = bset x cfm
+ val dlcm = mk_numeral (divlcm x cfm)
+ val cms = if ((length A) < (length B )) then "pi" else "mi"
+ val cp_thm = cooper_thm sg cms x cfm dlcm A B
val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
val (lsuth,rsuth) = qe_get_terms (uth)
val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
@@ -1353,98 +885,46 @@
val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
end
-|cooper_prv _ _ _ _ = error "Parameters format";
+|cooper_prv _ _ _ = error "Parameters format";
+
-(*====================================================*)
-(*Interpretation function for the evaluation protokol *)
-(*====================================================*)
-
-fun proof_of_evalc sg fm =
-let
-fun proof_of_evalch prt = case prt of
- EvalAt(at) => prove_elementar sg "ss" at
- |Evalfm(fm) => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl
- |EvalConst(s,pr1,pr2) =>
- let val th1 = proof_of_evalch pr1
- val th2 = proof_of_evalch pr2
- in case s of
- "CJ" =>[th1,th2] MRS (qe_conjI)
- |"DJ" =>[th1,th2] MRS (qe_disjI)
- |"IM" =>[th1,th2] MRS (qe_impI)
- |"EQ" =>[th1,th2] MRS (qe_eqI)
- end
-in proof_of_evalch (evalc_wp fm)
-end;
-
-(*============================================================*)
-(*Interpretation function for the NNF-Transformation protokol *)
-(*============================================================*)
+fun decomp_cnnf sg lfnp P = case P of
+ Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )
+ |Const ("op |",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_disjI)
+ |Const ("Not",_) $ (Const("Not",_) $ p) => ([p], fn [th] => th RS nnf_nn)
+ |Const("Not",_) $ (Const(opn,T) $ p $ q) =>
+ if opn = "op |"
+ then case (p,q) of
+ (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
+ if r1 = negate r
+ 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)
-fun proof_of_cnnf sg fm pf =
-let fun proof_of_cnnfh prt pat = case prt of
- NNFAt(at) => pat at
- |NNFSimp (pr) => let val th1 = proof_of_cnnfh pr pat
- in let val fm2 = snd (qe_get_terms th1)
- in [th1,prove_elementar sg "ss" (HOLogic.mk_eq(fm2 ,simpl fm2))] MRS trans
- end
- end
- |NNFNN (pr) => (proof_of_cnnfh pr pat) RS (nnf_nn)
- |NNFConst (s,pr1,pr2) =>
- let val th1 = proof_of_cnnfh pr1 pat
- val th2 = proof_of_cnnfh pr2 pat
- in case s of
- "CJ" => [th1,th2] MRS (qe_conjI)
- |"DJ" => [th1,th2] MRS (qe_disjI)
- |"IM" => [th1,th2] MRS (nnf_im)
- |"EQ" => [th1,th2] MRS (nnf_eq)
- |"SDJ" => let val (Const("op &",_)$A$_) = fst (qe_get_terms th1)
- val (Const("op &",_)$C$_) = fst (qe_get_terms th2)
- in [th1,th2,prove_elementar sg "ss" (HOLogic.mk_eq (A,HOLogic.Not $ C))] MRS (nnf_sdj)
- end
- |"NCJ" => [th1,th2] MRS (nnf_ncj)
- |"NIM" => [th1,th2] MRS (nnf_nim)
- |"NEQ" => [th1,th2] MRS (nnf_neq)
- |"NDJ" => [th1,th2] MRS (nnf_ndj)
- end
-in proof_of_cnnfh (cnnf_wp fm) pf
-end;
+ else ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
+ |(_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] => [th1,th2] MRS nnf_ndj)
+ else (
+ case (opn,T) of
+ ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_ncj )
+ |("op -->",_) => ([p,HOLogic.Not $ q ], fn [th1,th2] =>[th1,th2] MRS nnf_nim )
+ |("op =",Type ("fun",[Type ("bool", []),_])) =>
+ ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], fn [th1,th2] => [th1,th2] MRS nnf_neq)
+ |(_,_) => ([], fn [] => lfnp P)
+)
+
+ |(Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], fn [th1,th2] => [th1,th2] MRS nnf_im)
+
+ |(Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) =>
+ ([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], fn [th1,th2] =>[th1,th2] MRS nnf_eq )
+ |_ => ([], fn [] => lfnp P);
-(*====================================================*)
-(* Interpretation function for the linform protokol *)
-(*====================================================*)
-
-
-fun proof_of_linform sg vars f =
- let fun proof_of_linformh prt =
- case prt of
- (LfAt (at)) => prove_elementar sg "lf" (HOLogic.mk_eq (at, linform vars at))
- |(LfAtdvd (Const("Divides.op dvd",_)$d$t)) => (prove_elementar sg "lf" (HOLogic.mk_eq (t, lint vars t))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd))
- |(Lffm (fm)) => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl)
- |(LfConst (s,pr1,pr2)) =>
- let val th1 = proof_of_linformh pr1
- val th2 = proof_of_linformh pr2
- in case s of
- "CJ" => [th1,th2] MRS (qe_conjI)
- |"DJ" =>[th1,th2] MRS (qe_disjI)
- |"IM" =>[th1,th2] MRS (qe_impI)
- |"EQ" =>[th1,th2] MRS (qe_eqI)
- end
- |(LfNot(pr)) =>
- let val th = proof_of_linformh pr
- in (th RS (qe_Not))
- end
- |(LfQ(s,xn,xT,pr)) =>
- let val th = forall_intr (cterm_of sg (Free(xn,xT)))(proof_of_linformh pr)
- in if s = "Ex"
- then (th COMP(qe_exI) )
- else (th COMP(qe_ALLI) )
- end
-in
- proof_of_linformh (linform_wp f)
-end;
+fun proof_of_cnnf sg p lfnp =
+ let val th1 = thm_of sg (decomp_cnnf sg lfnp) p
+ val rs = snd(qe_get_terms th1)
+ val th2 = prove_elementar sg "ss" (HOLogic.mk_eq(rs,simpl rs))
+ in [th1,th2] MRS trans
+ end;
end;
--- a/src/HOL/Tools/Presburger/presburger.ML Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Wed May 19 11:23:59 2004 +0200
@@ -6,10 +6,13 @@
Tactic for solving arithmetical Goals in Presburger Arithmetic
*)
+(* This version of presburger deals with occurences of functional symbols in the subgoal and abstract over them to try to prove the more general formula. It then resolves with the subgoal. To disable this feature call the procedure with the parameter no_abs
+*)
+
signature PRESBURGER =
sig
- val presburger_tac : bool -> int -> tactic
- val presburger_method : bool -> int -> Proof.method
+ val presburger_tac : bool -> bool -> int -> tactic
+ val presburger_method : bool -> bool -> int -> Proof.method
val setup : (theory -> theory) list
val trace : bool ref
end;
@@ -25,19 +28,18 @@
(* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
(*-----------------------------------------------------------------*)
-val presburger_ss = simpset_of (theory "Presburger");
-
-fun cooper_pp sg vrl (fm as e$Abs(xn,xT,p)) =
+fun cooper_pp sg (fm as e$Abs(xn,xT,p)) =
let val (xn1,p1) = variant_abs (xn,xT,p)
- in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1 vrl) end;
+ in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
(CooperProof.proof_of_evalc sg);
-fun mproof_of_int_qelim sg fm =
- Qelim.proof_of_mlift_qelim sg CooperDec.is_arith_rel
+fun tmproof_of_int_qelim sg fm =
+ Qelim.tproof_of_mlift_qelim sg CooperDec.is_arith_rel
(CooperProof.proof_of_linform sg) (mnnf_pp sg) (cooper_pp sg) fm;
+
(* Theorems to be used in this tactic*)
val zdvd_int = thm "zdvd_int";
@@ -63,6 +65,19 @@
fun term_typed_consts t = add_term_typed_consts(t,[]);
+(* put a term into eta long beta normal form *)
+fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
+ | eta_long Ts t = (case strip_comb t of
+ (Abs _, _) => eta_long Ts (Envir.beta_norm t)
+ | (u, ts) =>
+ let
+ val Us = binder_types (fastype_of1 (Ts, t));
+ val i = length Us
+ in list_abs (map (pair "x") Us,
+ list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
+ (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
+ end);
+
(* Some Types*)
val bT = HOLogic.boolT;
val iT = HOLogic.intT;
@@ -94,8 +109,6 @@
("op *", iT --> iT --> iT),
("HOL.abs", iT --> iT),
("uminus", iT --> iT),
- ("HOL.max", iT --> iT --> iT),
- ("HOL.min", iT --> iT --> iT),
("op <=", nT --> nT --> bT),
("op =", nT --> nT --> bT),
@@ -107,8 +120,6 @@
("op -", nT --> nT --> nT),
("op *", nT --> nT --> nT),
("Suc", nT --> nT),
- ("HOL.max", nT --> nT --> nT),
- ("HOL.min", nT --> nT --> nT),
("Numeral.bin.Bit", binT --> bT --> binT),
("Numeral.bin.Pls", binT),
@@ -119,27 +130,89 @@
("0", iT),
("1", nT),
("1", iT),
-
("False", bT),
("True", bT)];
-(*returns true if the formula is relevant for presburger arithmetic tactic*)
-fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso
- map (fn i => snd (nth_elem (i, ps))) (loose_bnos t) @
- map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
- subset [iT, nT];
-
(* Preparation of the formula to be sent to the Integer quantifier *)
(* elimination procedure *)
(* Transforms meta implications and meta quantifiers to object *)
(* implications and object quantifiers *)
-fun prepare_for_presburger q fm =
+
+(*==================================*)
+(* Abstracting on subterms ========*)
+(*==================================*)
+(* Returns occurences of terms that are function application of type int or nat*)
+
+fun getfuncs fm = case strip_comb fm of
+ (Free (_, T), ts as _ :: _) =>
+ if body_type T mem [iT, nT]
+ andalso not (ts = []) andalso forall (null o loose_bnos) ts
+ then [fm]
+ else foldl op union ([], map getfuncs ts)
+ | (Var (_, T), ts as _ :: _) =>
+ if body_type T mem [iT, nT]
+ andalso not (ts = []) andalso forall (null o loose_bnos) ts then [fm]
+ else foldl op union ([], map getfuncs ts)
+ | (Const (s, T), ts) =>
+ if (s, T) mem allowed_consts orelse not (body_type T mem [iT, nT])
+ then foldl op union ([], map getfuncs ts)
+ else [fm]
+ | (Abs (s, T, t), _) => getfuncs t
+ | _ => [];
+
+
+fun abstract_pres sg fm =
+ foldr (fn (t, u) =>
+ let val T = fastype_of t
+ in all T $ Abs ("x", T, abstract_over (t, u)) end)
+ (getfuncs fm, fm);
+
+
+
+(* hasfuncs_on_bounds dont care of the type of the functions applied!
+ It returns true if there is a subterm coresponding to the application of
+ a function on a bounded variable.
+
+ Function applications are allowed only for well predefined functions a
+ consts*)
+
+fun has_free_funcs fm = case strip_comb fm of
+ (Free (_, T), ts as _ :: _) =>
+ if (body_type T mem [iT,nT]) andalso (not (T mem [iT,nT]))
+ then true
+ else exists (fn x => x) (map has_free_funcs ts)
+ | (Var (_, T), ts as _ :: _) =>
+ if (body_type T mem [iT,nT]) andalso not (T mem [iT,nT])
+ then true
+ else exists (fn x => x) (map has_free_funcs ts)
+ | (Const (s, T), ts) => exists (fn x => x) (map has_free_funcs ts)
+ | (Abs (s, T, t), _) => has_free_funcs t
+ |_ => false;
+
+
+(*returns true if the formula is relevant for presburger arithmetic tactic
+The constants occuring in term t should be a subset of the allowed_consts
+ There also should be no occurences of application of functions on bounded
+ variables. Whenever this function will be used, it will be ensured that t
+ will not contain subterms with function symbols that could have been
+ abstracted over.*)
+
+fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso
+ map (fn i => snd (nth_elem (i, ps))) (loose_bnos t) @
+ map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
+ subset [iT, nT]
+ andalso not (has_free_funcs t);
+
+
+fun prepare_for_presburger sg q fm =
let
val ps = Logic.strip_params fm
val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
- val _ = if relevant (rev ps) c then () else raise CooperDec.COOPER
+ val _ = if relevant (rev ps) c then ()
+ else (trace_msg ("Conclusion is not a presburger term:\n" ^
+ Sign.string_of_term sg c); raise CooperDec.COOPER)
fun mk_all ((s, T), (P,n)) =
if 0 mem loose_bnos P then
(HOLogic.all_const T $ Abs (s, T, P), n)
@@ -161,14 +234,20 @@
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
(* the presburger tactic*)
-fun presburger_tac q i = ObjectLogic.atomize_tac i THEN (fn st =>
+
+(* Parameters : q = flag for quantify ofer free variables ;
+ a = flag for abstracting over function occurences
+ i = subgoal *)
+
+fun presburger_tac q a i = ObjectLogic.atomize_tac i THEN (fn st =>
let
- val g = BasisLibrary.List.nth (prems_of st, i - 1);
- val sg = sign_of_thm st;
+ val g = BasisLibrary.List.nth (prems_of st, i - 1)
+ val sg = sign_of_thm st
+ (* The Abstraction step *)
+ val g' = if a then abstract_pres sg g else g
(* Transform the term*)
- val (t,np,nh) = prepare_for_presburger q g
+ val (t,np,nh) = prepare_for_presburger sg q g'
(* Some simpsets for dealing with mod div abs and nat*)
-
val simpset0 = HOL_basic_ss
addsimps [mod_div_equality', Suc_plus1]
addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
@@ -183,37 +262,40 @@
addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
addcongs [conj_le_cong, imp_le_cong]
(* simp rules for elimination of abs *)
-
val simpset3 = HOL_basic_ss addsplits [abs_split]
-
val ct = cterm_of sg (HOLogic.mk_Trueprop t)
-
(* Theorem for the nat --> int transformation *)
val pre_thm = Seq.hd (EVERY
- [simp_tac simpset0 i,
- TRY (simp_tac simpset1 i), TRY (simp_tac simpset2 i),
- TRY (simp_tac simpset3 i), TRY (simp_tac presburger_ss i)]
+ [simp_tac simpset0 1,
+ TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
+ TRY (simp_tac simpset3 1)]
(trivial ct))
-
- fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i);
-
+ fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
(trace_msg ("calling procedure with term:\n" ^
Sign.string_of_term sg t1);
- ((mproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
+ ((tmproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
| _ => (pre_thm, assm_tac i)
- in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st
+ in (rtac (((mp_step nh) o (spec_step np)) th) i
+ THEN tac) st
end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);
fun presburger_args meth =
- Method.simple_args (Scan.optional (Args.$$$ "no_quantify" >> K false) true)
- (fn q => fn _ => meth q 1);
+ let val parse_flag =
+ Args.$$$ "no_quantify" >> K (apfst (K false))
+ || Args.$$$ "no_abs" >> K (apsnd (K false));
+ in
+ Method.simple_args
+ (Scan.optional (Args.$$$ "(" |-- Args.list1 parse_flag --| Args.$$$ ")") [] >>
+ curry (foldl op |>) (true, true))
+ (fn (q,a) => fn _ => meth q a 1)
+ end;
-fun presburger_method q i = Method.METHOD (fn facts =>
- Method.insert_tac facts 1 THEN presburger_tac q i)
+fun presburger_method q a i = Method.METHOD (fn facts =>
+ Method.insert_tac facts 1 THEN presburger_tac q a i)
val setup =
[Method.add_method ("presburger",
@@ -221,8 +303,8 @@
"decision procedure for Presburger arithmetic"),
ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
{splits = splits, inj_consts = inj_consts, discrete = discrete,
- presburger = Some (presburger_tac true)})];
+ presburger = Some (presburger_tac true true)})];
end;
-val presburger_tac = Presburger.presburger_tac true;
+val presburger_tac = Presburger.presburger_tac true true;
--- a/src/HOL/Tools/Presburger/qelim.ML Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/Tools/Presburger/qelim.ML Wed May 19 11:23:59 2004 +0200
@@ -8,10 +8,11 @@
*)
signature QELIM =
-sig
- val proof_of_mlift_qelim: Sign.sg -> (term -> bool) ->
+ sig
+ val tproof_of_mlift_qelim: Sign.sg -> (term -> bool) ->
(string list -> term -> thm) -> (term -> thm) ->
- (string list -> term -> thm) -> term -> thm
+ (term -> thm) -> term -> thm
+
end;
structure Qelim : QELIM =
@@ -19,24 +20,6 @@
open CooperDec;
open CooperProof;
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*--- ---*)
-(*--- ---*)
-(*--- Protocoling part ---*)
-(*--- ---*)
-(*--- includes the protocolling datastructure ---*)
-(*--- ---*)
-(*--- and the protocolling fuctions ---*)
-(*--- ---*)
-(*--- ---*)
-(*--- ---*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-
-
val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
(* List of the theorems to be used in the following*)
@@ -46,131 +29,35 @@
val qe_ALL = thm "qe_ALL";
-(*Datatype declaration for the protocoling procedure.*)
-
-
-datatype QeLog = AFN of term*(string list)
- |QFN of term*(string list)
- |ExConj of term*QeLog
- |ExDisj of (string*typ*term)*term*QeLog*QeLog
- |QeConst of string*QeLog*QeLog
- |QeNot of QeLog
- |QeAll of QeLog
- |Lift_Qelim of term*QeLog
- |QeUnk of term;
-
-datatype mQeLog = mQeProof of (string list)*mQeLog
- |mAFN of term
- |mNFN of mQeLog
- |mQeConst of string*mQeLog*mQeLog
- |mQeNot of mQeLog
- |mQelim of term*(string list)*mQeLog
- |mQeAll of mQeLog
- |mQefm of term;
-
-(* This is the protokoling my function for the quantifier elimination*)
-fun mlift_qelim_wp isat vars =
- let fun mqelift_wp vars fm = if (isat fm) then mAFN(fm)
- else
- (case fm of
- ( Const ("Not",_) $ p) => mQeNot(mqelift_wp vars p)
- |( Const ("op &",_) $ p $q) => mQeConst("CJ", mqelift_wp vars p,mqelift_wp vars q)
-
- |( Const ("op |",_) $ p $q) => mQeConst("DJ", mqelift_wp vars p,mqelift_wp vars q)
-
- |( Const ("op -->",_) $ p $q) => mQeConst("IM", mqelift_wp vars p,mqelift_wp vars q)
-
- |( Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $q) =>mQeConst("EQ", mqelift_wp vars p,mqelift_wp vars q)
-
-
- |( Const ("All",QT) $ Abs(x,T,p)) =>mQeAll (mqelift_wp vars (Const("Ex",QT) $ Abs(x,T,(HOLogic.Not $ p))))
-
- |(Const ("Ex",_) $ Abs (x,T,p)) =>
- let val (x1,p1) = variant_abs (x,T,p)
- val prt = mqelift_wp (x1::vars) p1
- in mQelim(Free(x1,T),vars,mNFN(prt))
- end
- | _ => mQefm(fm)
- )
-
- in (fn fm => mQeProof(vars,mNFN(mqelift_wp vars fm )))
- end;
-
-
+(*============= Compact version =====*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*--- ---*)
-(*--- ---*)
-(*--- Interpretation and Proofgeneration Part ---*)
-(*--- ---*)
-(*--- Protocole interpretation functions ---*)
-(*--- ---*)
-(*--- and proofgeneration functions ---*)
-(*--- ---*)
-(*--- ---*)
-(*--- ---*)
-(*--- ---*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
-(*function that interpretates the protokol generated by the _wp function*)
-
+fun decomp_qe is_at afnp nfnp qfnp sg P =
+ if is_at P then ([], fn [] => afnp [] P) else
+ case P of
+ (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+ |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
+ |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
+ |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
+ |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
+ |(Const("Ex",_)$Abs(xn,xT,p)) =>
+ let val (xn1,p1) = variant_abs(xn,xT,p)
+ in ([p1],
+ fn [th1_1] =>
+ let val th2 = [th1_1,nfnp (snd (qe_get_terms th1_1))] MRS trans
+ val eth1 = (forall_intr (cterm_of sg (Free(xn1,xT))) th2) COMP qe_exI
+ val th3 = qfnp (snd(qe_get_terms eth1))
+ in [eth1,th3] MRS trans
+ end )
+ end
-(* proof_of_lift_qelim interpretates a protokol for the quantifier elimination one some quantified formula. It uses the functions afnp nfnp and qfnp as proof functions to generate a prove for the hole quantifier elimination.*)
-(* afnp : must retun a proof for the transformations on the atomic formalae*)
-(* nfnp : must return a proof for the post one-quatifiers elimination process*)
-(* qfnp mus return a proof for the one quantifier elimination (existential) *)
-(* All these function are independent of the theory on whitch we are trying to prove quantifier elimination*)
-(* But the following invariants mus be respected : *)
-(* afnp : term -> string list -> thm*)
-(* nfnp : term -> thm*)
-(* qfnp : term -> string list -> thm*)
-(*For all theorms generated by these function must hold :*)
-(* All of them are logical equivalences.*)
-(* on left side of the equivalence must appear the term exactely as ist was given as a parameter (or eventually modulo Gamma, where Gamma are the rules whitch are allowed to be used during unification ex. beta reduction.....)*)
-(* qfnp must take as an argument for the term an existential quantified formula*)
-(*-----------------------------------------------------------------*)
-(*-----------------------------------------------------------------*)
+ |(Const("All",_)$Abs(xn,xT,p)) => ([(HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p)], fn [th] => th RS qe_ALL)
+ | _ => ([],fn [] => instantiate' [Some (ctyp_of sg (type_of P))] [Some (cterm_of sg P)] refl);
+
-fun proof_of_mlift_qelim sg isat afnp nfnp qfnp =
- let fun h_proof_of_mlift_qelim isat afnp nfnp qfnp prtkl vrl =
- (case prtkl of
- mAFN (fm) => afnp vrl fm
- |mNFN (prt) => let val th1 = h_proof_of_mlift_qelim isat afnp nfnp qfnp prt vrl
- val th2 = nfnp (snd (qe_get_terms th1))
- in [th1,th2] MRS trans
- end
- |mQeConst (s,pr1,pr2) =>
- let val th1 = h_proof_of_mlift_qelim isat afnp nfnp qfnp pr1 vrl
- val th2 = h_proof_of_mlift_qelim isat afnp nfnp qfnp pr2 vrl
- in (case s of
- "CJ" => [th1,th2] MRS (qe_conjI)
- |"DJ" => [th1,th2] MRS (qe_disjI)
- |"IM" => [th1,th2] MRS (qe_impI)
- |"EQ" => [th1,th2] MRS (qe_eqI)
- )
- end
- |mQeNot (pr) =>(h_proof_of_mlift_qelim isat afnp nfnp qfnp pr vrl ) RS (qe_Not)
- |mQeAll(pr) => (h_proof_of_mlift_qelim isat afnp nfnp qfnp pr vrl ) RS (qe_ALL)
- |mQelim (x as (Free(xn,xT)),vl,pr) =>
- let val th_1 = h_proof_of_mlift_qelim isat afnp nfnp qfnp pr vl
- val mQeProof(l2,pr2) = mlift_qelim_wp isat (xn::vrl) (snd(qe_get_terms th_1))
- val th_2 = [th_1,(h_proof_of_mlift_qelim isat afnp nfnp qfnp pr2 l2)] MRS trans
- val th1 = (forall_intr (cterm_of sg x) th_2) COMP (qe_exI)
- val th2 = qfnp vl (snd (qe_get_terms th1))
- in [th1,th2] MRS trans
- end
- |mQefm (fm) => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl
-)
-in (fn fm => let val mQeProof(vars,prt) = (mlift_qelim_wp isat (fv fm) fm)
- in (h_proof_of_mlift_qelim isat afnp nfnp qfnp prt vars)
- end)
+fun tproof_of_mlift_qelim sg isat afnp nfnp qfnp p =
+ let val th1 = thm_of sg (decomp_qe isat afnp nfnp qfnp sg) p
+ val th2 = nfnp (snd (qe_get_terms th1))
+ in [th1,th2] MRS trans
+ end;
end;
-
-end;
--- a/src/HOL/ex/PresburgerEx.thy Wed May 19 11:21:19 2004 +0200
+++ b/src/HOL/ex/PresburgerEx.thy Wed May 19 11:23:59 2004 +0200
@@ -39,18 +39,18 @@
by presburger
theorem "\<forall>(x::int). b < x --> a \<le> x"
- apply (presburger no_quantify)
+ apply (presburger (no_quantify))
oops
theorem "\<forall>(x::int). b < x --> a \<le> x"
- apply (presburger no_quantify)
+ apply (presburger (no_quantify))
oops
theorem "~ (\<exists>(x::int). False)"
by presburger
theorem "\<forall>(x::int). (a::int) < 3 * x --> b < 3 * x"
- apply (presburger no_quantify)
+ apply (presburger (no_quantify))
oops
theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)" by presburger