--- a/src/HOL/Integ/cooper_dec.ML Wed Aug 04 11:25:08 2004 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Wed Aug 04 17:43:55 2004 +0200
@@ -42,6 +42,7 @@
val plusinf : term -> term -> term
val onatoms : (term -> term) -> term -> term
val evalc : term -> term
+ val cooper_w : string list -> term -> (term option * term)
val integer_qelim : Term.term -> Term.term
val mk_presburger_oracle : (Sign.sg * exn) -> term
end;
@@ -197,7 +198,7 @@
else (warning "lint: apparent nonlinearity"; raise COOPER)
end
- |_ => (error "COOPER:lint: unknown term ")
+ |_ => error ("COOPER:lint: unknown term \n");
@@ -414,7 +415,31 @@
(* ------------------------------------------------------------------------- *)
(* Evaluation of constant expressions. *)
(* ------------------------------------------------------------------------- *)
-
+
+(* An other implementation of divides, that covers more cases*)
+
+exception DVD_UNKNOWN
+
+fun dvd_op (d, t) =
+ if not(is_numeral d) then raise DVD_UNKNOWN
+ else let
+ val dn = dest_numeral d
+ fun coeffs_of x = case x of
+ Const(p,_) $ tl $ tr =>
+ if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
+ else if p = "op *"
+ then if (is_numeral tr)
+ then [(dest_numeral tr) * (dest_numeral tl)]
+ else [dest_numeral tl]
+ else []
+ |_ => if (is_numeral t) then [dest_numeral t] else []
+ val ts = coeffs_of t
+ in case ts of
+ [] => raise DVD_UNKNOWN
+ |_ => foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
+ end;
+
+
val operations =
[("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=),
("Divides.op dvd",fn (x,y) =>((y mod x) = 0))];
@@ -423,22 +448,44 @@
|applyoperation _ (_, _) = false;
(*Evaluation of constant atomic formulas*)
-
+ (*FIXME : This is an optimation but still incorrect !! *)
+(*
fun evalc_atom at = case at of
- (Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
- Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)
- handle _ => at)
- | _ => at)
- |Const("Not",_)$(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
- Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then
- HOLogic.false_const else HOLogic.true_const)
- handle _ => at)
- | _ => at)
- | _ => at;
-
-(*Function onatoms apllys function f on the atomic formulas involved in a.*)
+ (Const (p,_) $ s $ t) =>
+ (if p="Divides.op dvd" then
+ ((if dvd_op(s,t) then HOLogic.true_const
+ else HOLogic.false_const)
+ handle _ => at)
+ else
+ case assoc (operations,p) of
+ Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)
+ handle _ => at)
+ | _ => at)
+ |Const("Not",_)$(Const (p,_) $ s $ t) =>(
+ case assoc (operations,p) of
+ Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then
+ HOLogic.false_const else HOLogic.true_const)
+ handle _ => at)
+ | _ => at)
+ | _ => at;
+
+*)
+
+fun evalc_atom at = case at of
+ (Const (p,_) $ s $ t) =>
+ ( case assoc (operations,p) of
+ Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)
+ handle _ => at)
+ | _ => at)
+ |Const("Not",_)$(Const (p,_) $ s $ t) =>(
+ case assoc (operations,p) of
+ Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then
+ HOLogic.false_const else HOLogic.true_const)
+ handle _ => at)
+ | _ => at)
+ | _ => at;
+
+ (*Function onatoms apllys function f on the atomic formulas involved in a.*)
fun onatoms f a = if (is_arith_rel a) then f a else case a of
@@ -653,6 +700,48 @@
| _ => error "cooper: not an existential formula";
+(* Try to find a withness for the formula *)
+
+fun inf_w mi d vars x p =
+ let val f = if mi then minusinf else plusinf in
+ case (simpl (minusinf x p)) of
+ Const("True",_) => (Some (mk_numeral 1), HOLogic.true_const)
+ |Const("False",_) => (None,HOLogic.false_const)
+ |F =>
+ let
+ fun h n =
+ case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of
+ Const("True",_) => (Some (mk_numeral n),HOLogic.true_const)
+ |F' => if n=1 then (None,F')
+ else let val (rw,rf) = h (n-1) in
+ (rw,HOLogic.mk_disj(F',rf))
+ end
+
+ in (h d)
+ end
+ end;
+
+fun set_w d b st vars x p = let
+ fun h ns = case ns of
+ [] => (None,HOLogic.false_const)
+ |n::nl => ( case ((simpl o evalc) (linrep vars x n p)) of
+ Const("True",_) => (Some n,HOLogic.true_const)
+ |F' => let val (rw,rf) = h nl
+ in (rw,HOLogic.mk_disj(F',rf))
+ end)
+ val f = if b then linear_add else linear_sub
+ val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
+ in h p_elements
+ end;
+
+fun withness d b st vars x p = case (inf_w b d vars x p) of
+ (Some n,_) => (Some n,HOLogic.true_const)
+ |(None,Pinf) => (case (set_w d b st vars x p) of
+ (Some n,_) => (Some n,HOLogic.true_const)
+ |(_,Pst) => (None,HOLogic.mk_disj(Pinf,Pst)));
+
+
+
(*Cooper main procedure*)
@@ -678,6 +767,29 @@
| _ => error "cooper: not an existential formula";
+(* A Version of cooper that returns a withness *)
+fun cooper_w vars1 fm =
+ case fm of
+ Const ("Ex",_) $ Abs(x0,T,p0) => let
+ val (xn,p1) = variant_abs (x0,T,p0)
+ val x = Free (xn,T)
+ val vars = (xn::vars1)
+(* val p = unitycoeff x (posineq (simpl p1)) *)
+ val p = unitycoeff x p1
+ val ast = aset x p
+ val bst = bset x p
+ val d = divlcm x p
+ val (p_inf,S ) =
+ if (length bst) <= (length ast)
+ then (true,bst)
+ else (false,ast)
+ in withness d p_inf S vars x p
+(* fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
+ fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+ in (list_disj (map stage js))
+*)
+ end
+ | _ => error "cooper: not an existential formula";
(*Function itlist applys a double parametred function f : 'a->'b->b iteratively to a List l : 'a
@@ -811,8 +923,8 @@
fun mk_presburger_oracle (sg,COOPER_ORACLE t) =
if (!quick_and_dirty)
then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t))
- else raise COOPER_ORACLE t;
-
+ else raise COOPER_ORACLE t
+ |mk_presburger_oracle (sg,_) = error "Oops";
end;
--- a/src/HOL/Integ/cooper_proof.ML Wed Aug 04 11:25:08 2004 +0200
+++ b/src/HOL/Integ/cooper_proof.ML Wed Aug 04 17:43:55 2004 +0200
@@ -219,7 +219,8 @@
[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)]
+ simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+
end
(*"bl" like blast tactic*)
@@ -251,7 +252,8 @@
| "fa" =>
let val ct = cert_Trueprop sg fm2
- in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
+ in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
+
end
| "sa" =>
@@ -259,7 +261,8 @@
val ss = presburger_ss addsimps zadd_ac
val ct = cert_Trueprop sg fm2
in
- simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+ simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+
end
(* like Existance Conjunction *)
| "ec" =>
@@ -283,7 +286,8 @@
val ss = presburger_ss addsimps zadd_ac
val ct = cert_Trueprop sg fm2
in
- simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+ simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+
end;
(*=============================================================*)
@@ -917,6 +921,71 @@
|cooper_prv _ _ _ = error "Parameters format";
+(* **************************************** *)
+(* An Other Version of cooper proving *)
+(* by giving a withness for EX *)
+(* **************************************** *)
+
+
+
+fun cooper_prv_w sg (x as Free(xn,xT)) efm = let
+ (* lfm_thm : efm = linearized form of efm*)
+ val lfm_thm = proof_of_linform sg [xn] efm
+ (*efm2 is the linearized form of efm *)
+ val efm2 = snd(qe_get_terms lfm_thm)
+ (* l is the lcm of all coefficients of x *)
+ val l = formlcm x efm2
+ (*ac_thm: efm = efm2 with adjusted coefficients of x *)
+ val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
+ (* fm is efm2 with adjusted coefficients of x *)
+ val fm = snd (qe_get_terms ac_thm)
+ (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
+ val cfm = unitycoeff x fm
+ (*afm is fm where c*x is replaced by 1*x or -1*x *)
+ val afm = adjustcoeff x l fm
+ (* P = %x.afm*)
+ val P = absfree(xn,xT,afm)
+ (* This simpset allows the elimination of the sets in bex {1..d} *)
+ val ss = presburger_ss addsimps
+ [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
+ (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
+ val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+ (* e_ac_thm : Ex x. efm = EX x. fm*)
+ val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
+ (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
+ val (lsuth,rsuth) = qe_get_terms (uth)
+ (* lseacth = EX x. efm; rseacth = EX x. fm*)
+ val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
+
+ val (w,rs) = cooper_w [] cfm
+ val exp_cp_thm = case w of
+ (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*)
+ Some n => e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*)
+ |_ => let
+ (* A and B set of the formula*)
+ val A = aset x cfm
+ val B = bset x cfm
+ (* the divlcm (delta) of the formula*)
+ val dlcm = mk_numeral (divlcm x cfm)
+ (* Which set is smaller to generate the (hoepfully) shorter proof*)
+ val cms = if ((length A) < (length B )) then "pi" else "mi"
+ (* synthesize the proof of cooper's theorem*)
+ (* cp_thm: EX x. cfm = Q*)
+ val cp_thm = cooper_thm sg cms x cfm dlcm A B
+ (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
+ (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
+ in refl RS (simplify ss (cp_thm RSN (2,trans)))
+ end
+ (* lscth = EX x. cfm; rscth = Q' *)
+ val (lscth,rscth) = qe_get_terms (exp_cp_thm)
+ (* u_c_thm: EX x. P(l*x) = Q'*)
+ val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
+ (* result: EX x. efm = Q'*)
+ in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
+ end
+|cooper_prv_w _ _ _ = error "Parameters format";
+
+
fun decomp_cnnf sg lfnp P = case P of
Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Wed Aug 04 11:25:08 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Wed Aug 04 17:43:55 2004 +0200
@@ -42,6 +42,7 @@
val plusinf : term -> term -> term
val onatoms : (term -> term) -> term -> term
val evalc : term -> term
+ val cooper_w : string list -> term -> (term option * term)
val integer_qelim : Term.term -> Term.term
val mk_presburger_oracle : (Sign.sg * exn) -> term
end;
@@ -197,7 +198,7 @@
else (warning "lint: apparent nonlinearity"; raise COOPER)
end
- |_ => (error "COOPER:lint: unknown term ")
+ |_ => error ("COOPER:lint: unknown term \n");
@@ -414,7 +415,31 @@
(* ------------------------------------------------------------------------- *)
(* Evaluation of constant expressions. *)
(* ------------------------------------------------------------------------- *)
-
+
+(* An other implementation of divides, that covers more cases*)
+
+exception DVD_UNKNOWN
+
+fun dvd_op (d, t) =
+ if not(is_numeral d) then raise DVD_UNKNOWN
+ else let
+ val dn = dest_numeral d
+ fun coeffs_of x = case x of
+ Const(p,_) $ tl $ tr =>
+ if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
+ else if p = "op *"
+ then if (is_numeral tr)
+ then [(dest_numeral tr) * (dest_numeral tl)]
+ else [dest_numeral tl]
+ else []
+ |_ => if (is_numeral t) then [dest_numeral t] else []
+ val ts = coeffs_of t
+ in case ts of
+ [] => raise DVD_UNKNOWN
+ |_ => foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
+ end;
+
+
val operations =
[("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=),
("Divides.op dvd",fn (x,y) =>((y mod x) = 0))];
@@ -423,22 +448,44 @@
|applyoperation _ (_, _) = false;
(*Evaluation of constant atomic formulas*)
-
+ (*FIXME : This is an optimation but still incorrect !! *)
+(*
fun evalc_atom at = case at of
- (Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
- Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)
- handle _ => at)
- | _ => at)
- |Const("Not",_)$(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
- Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then
- HOLogic.false_const else HOLogic.true_const)
- handle _ => at)
- | _ => at)
- | _ => at;
-
-(*Function onatoms apllys function f on the atomic formulas involved in a.*)
+ (Const (p,_) $ s $ t) =>
+ (if p="Divides.op dvd" then
+ ((if dvd_op(s,t) then HOLogic.true_const
+ else HOLogic.false_const)
+ handle _ => at)
+ else
+ case assoc (operations,p) of
+ Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)
+ handle _ => at)
+ | _ => at)
+ |Const("Not",_)$(Const (p,_) $ s $ t) =>(
+ case assoc (operations,p) of
+ Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then
+ HOLogic.false_const else HOLogic.true_const)
+ handle _ => at)
+ | _ => at)
+ | _ => at;
+
+*)
+
+fun evalc_atom at = case at of
+ (Const (p,_) $ s $ t) =>
+ ( case assoc (operations,p) of
+ Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)
+ handle _ => at)
+ | _ => at)
+ |Const("Not",_)$(Const (p,_) $ s $ t) =>(
+ case assoc (operations,p) of
+ Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then
+ HOLogic.false_const else HOLogic.true_const)
+ handle _ => at)
+ | _ => at)
+ | _ => at;
+
+ (*Function onatoms apllys function f on the atomic formulas involved in a.*)
fun onatoms f a = if (is_arith_rel a) then f a else case a of
@@ -653,6 +700,48 @@
| _ => error "cooper: not an existential formula";
+(* Try to find a withness for the formula *)
+
+fun inf_w mi d vars x p =
+ let val f = if mi then minusinf else plusinf in
+ case (simpl (minusinf x p)) of
+ Const("True",_) => (Some (mk_numeral 1), HOLogic.true_const)
+ |Const("False",_) => (None,HOLogic.false_const)
+ |F =>
+ let
+ fun h n =
+ case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of
+ Const("True",_) => (Some (mk_numeral n),HOLogic.true_const)
+ |F' => if n=1 then (None,F')
+ else let val (rw,rf) = h (n-1) in
+ (rw,HOLogic.mk_disj(F',rf))
+ end
+
+ in (h d)
+ end
+ end;
+
+fun set_w d b st vars x p = let
+ fun h ns = case ns of
+ [] => (None,HOLogic.false_const)
+ |n::nl => ( case ((simpl o evalc) (linrep vars x n p)) of
+ Const("True",_) => (Some n,HOLogic.true_const)
+ |F' => let val (rw,rf) = h nl
+ in (rw,HOLogic.mk_disj(F',rf))
+ end)
+ val f = if b then linear_add else linear_sub
+ val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
+ in h p_elements
+ end;
+
+fun withness d b st vars x p = case (inf_w b d vars x p) of
+ (Some n,_) => (Some n,HOLogic.true_const)
+ |(None,Pinf) => (case (set_w d b st vars x p) of
+ (Some n,_) => (Some n,HOLogic.true_const)
+ |(_,Pst) => (None,HOLogic.mk_disj(Pinf,Pst)));
+
+
+
(*Cooper main procedure*)
@@ -678,6 +767,29 @@
| _ => error "cooper: not an existential formula";
+(* A Version of cooper that returns a withness *)
+fun cooper_w vars1 fm =
+ case fm of
+ Const ("Ex",_) $ Abs(x0,T,p0) => let
+ val (xn,p1) = variant_abs (x0,T,p0)
+ val x = Free (xn,T)
+ val vars = (xn::vars1)
+(* val p = unitycoeff x (posineq (simpl p1)) *)
+ val p = unitycoeff x p1
+ val ast = aset x p
+ val bst = bset x p
+ val d = divlcm x p
+ val (p_inf,S ) =
+ if (length bst) <= (length ast)
+ then (true,bst)
+ else (false,ast)
+ in withness d p_inf S vars x p
+(* fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
+ fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+ in (list_disj (map stage js))
+*)
+ end
+ | _ => error "cooper: not an existential formula";
(*Function itlist applys a double parametred function f : 'a->'b->b iteratively to a List l : 'a
@@ -811,8 +923,8 @@
fun mk_presburger_oracle (sg,COOPER_ORACLE t) =
if (!quick_and_dirty)
then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t))
- else raise COOPER_ORACLE t;
-
+ else raise COOPER_ORACLE t
+ |mk_presburger_oracle (sg,_) = error "Oops";
end;
--- a/src/HOL/Tools/Presburger/cooper_proof.ML Wed Aug 04 11:25:08 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML Wed Aug 04 17:43:55 2004 +0200
@@ -219,7 +219,8 @@
[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)]
+ simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+
end
(*"bl" like blast tactic*)
@@ -251,7 +252,8 @@
| "fa" =>
let val ct = cert_Trueprop sg fm2
- in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
+ in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
+
end
| "sa" =>
@@ -259,7 +261,8 @@
val ss = presburger_ss addsimps zadd_ac
val ct = cert_Trueprop sg fm2
in
- simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+ simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+
end
(* like Existance Conjunction *)
| "ec" =>
@@ -283,7 +286,8 @@
val ss = presburger_ss addsimps zadd_ac
val ct = cert_Trueprop sg fm2
in
- simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+ simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+
end;
(*=============================================================*)
@@ -917,6 +921,71 @@
|cooper_prv _ _ _ = error "Parameters format";
+(* **************************************** *)
+(* An Other Version of cooper proving *)
+(* by giving a withness for EX *)
+(* **************************************** *)
+
+
+
+fun cooper_prv_w sg (x as Free(xn,xT)) efm = let
+ (* lfm_thm : efm = linearized form of efm*)
+ val lfm_thm = proof_of_linform sg [xn] efm
+ (*efm2 is the linearized form of efm *)
+ val efm2 = snd(qe_get_terms lfm_thm)
+ (* l is the lcm of all coefficients of x *)
+ val l = formlcm x efm2
+ (*ac_thm: efm = efm2 with adjusted coefficients of x *)
+ val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
+ (* fm is efm2 with adjusted coefficients of x *)
+ val fm = snd (qe_get_terms ac_thm)
+ (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
+ val cfm = unitycoeff x fm
+ (*afm is fm where c*x is replaced by 1*x or -1*x *)
+ val afm = adjustcoeff x l fm
+ (* P = %x.afm*)
+ val P = absfree(xn,xT,afm)
+ (* This simpset allows the elimination of the sets in bex {1..d} *)
+ val ss = presburger_ss addsimps
+ [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
+ (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
+ val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+ (* e_ac_thm : Ex x. efm = EX x. fm*)
+ val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
+ (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
+ val (lsuth,rsuth) = qe_get_terms (uth)
+ (* lseacth = EX x. efm; rseacth = EX x. fm*)
+ val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
+
+ val (w,rs) = cooper_w [] cfm
+ val exp_cp_thm = case w of
+ (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*)
+ Some n => e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*)
+ |_ => let
+ (* A and B set of the formula*)
+ val A = aset x cfm
+ val B = bset x cfm
+ (* the divlcm (delta) of the formula*)
+ val dlcm = mk_numeral (divlcm x cfm)
+ (* Which set is smaller to generate the (hoepfully) shorter proof*)
+ val cms = if ((length A) < (length B )) then "pi" else "mi"
+ (* synthesize the proof of cooper's theorem*)
+ (* cp_thm: EX x. cfm = Q*)
+ val cp_thm = cooper_thm sg cms x cfm dlcm A B
+ (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
+ (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
+ in refl RS (simplify ss (cp_thm RSN (2,trans)))
+ end
+ (* lscth = EX x. cfm; rscth = Q' *)
+ val (lscth,rscth) = qe_get_terms (exp_cp_thm)
+ (* u_c_thm: EX x. P(l*x) = Q'*)
+ val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
+ (* result: EX x. efm = Q'*)
+ in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
+ end
+|cooper_prv_w _ _ _ = error "Parameters format";
+
+
fun decomp_cnnf sg lfnp P = case P of
Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )