15 val qe_impI : thm |
15 val qe_impI : thm |
16 val qe_eqI : thm |
16 val qe_eqI : thm |
17 val qe_exI : thm |
17 val qe_exI : thm |
18 val list_to_set : typ -> term list -> term |
18 val list_to_set : typ -> term list -> term |
19 val qe_get_terms : thm -> term * term |
19 val qe_get_terms : thm -> term * term |
20 val cooper_prv : Sign.sg -> term -> term -> thm |
20 val cooper_prv : Sign.sg -> term -> term -> thm |
|
21 val cooper_prv2 : Sign.sg -> term -> term -> thm |
21 val proof_of_evalc : Sign.sg -> term -> thm |
22 val proof_of_evalc : Sign.sg -> term -> thm |
22 val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm |
23 val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm |
23 val proof_of_linform : Sign.sg -> string list -> term -> thm |
24 val proof_of_linform : Sign.sg -> string list -> term -> thm |
24 val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm |
25 val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm |
25 val prove_elementar : Sign.sg -> string -> term -> thm |
26 val prove_elementar : Sign.sg -> string -> term -> thm |
790 case assoc (operations,p) of |
791 case assoc (operations,p) of |
791 Some f => |
792 Some f => |
792 ((if (f ((dest_numeral s),(dest_numeral t))) |
793 ((if (f ((dest_numeral s),(dest_numeral t))) |
793 then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) |
794 then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) |
794 else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))) |
795 else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))) |
795 handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl |
796 handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl) |
796 | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl )) |
797 | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl ) |
797 |Const("Not",_)$(Const (p,_) $ s $ t) =>( |
798 |Const("Not",_)$(Const (p,_) $ s $ t) =>( |
798 case assoc (operations,p) of |
799 case assoc (operations,p) of |
799 Some f => |
800 Some f => |
800 ((if (f ((dest_numeral s),(dest_numeral t))) |
801 ((if (f ((dest_numeral s),(dest_numeral t))) |
801 then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)) |
802 then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)) |
918 (* result: EX x. efm = Q'*) |
919 (* result: EX x. efm = Q'*) |
919 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) |
920 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) |
920 end |
921 end |
921 |cooper_prv _ _ _ = error "Parameters format"; |
922 |cooper_prv _ _ _ = error "Parameters format"; |
922 |
923 |
|
924 (* ********************************** *) |
|
925 (* cooper_prv2 is just copy and paste *) |
|
926 (* And only generates proof with *) |
|
927 (* bset and minusinfity *) |
|
928 (* ********************************** *) |
|
929 |
|
930 |
|
931 |
|
932 fun cooper_prv2 sg (x as Free(xn,xT)) efm = let |
|
933 (* lfm_thm : efm = linearized form of efm*) |
|
934 val lfm_thm = proof_of_linform sg [xn] efm |
|
935 (*efm2 is the linearized form of efm *) |
|
936 val efm2 = snd(qe_get_terms lfm_thm) |
|
937 (* l is the lcm of all coefficients of x *) |
|
938 val l = formlcm x efm2 |
|
939 (*ac_thm: efm = efm2 with adjusted coefficients of x *) |
|
940 val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans |
|
941 (* fm is efm2 with adjusted coefficients of x *) |
|
942 val fm = snd (qe_get_terms ac_thm) |
|
943 (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*) |
|
944 val cfm = unitycoeff x fm |
|
945 (*afm is fm where c*x is replaced by 1*x or -1*x *) |
|
946 val afm = adjustcoeff x l fm |
|
947 (* P = %x.afm*) |
|
948 val P = absfree(xn,xT,afm) |
|
949 (* This simpset allows the elimination of the sets in bex {1..d} *) |
|
950 val ss = presburger_ss addsimps |
|
951 [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff] |
|
952 (* uth : EX x.P(l*x) = EX x. l dvd x & P x*) |
|
953 val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex) |
|
954 (* e_ac_thm : Ex x. efm = EX x. fm*) |
|
955 val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI) |
|
956 (* A and B set of the formula*) |
|
957 val B = bset x cfm |
|
958 val A = [] |
|
959 (* the divlcm (delta) of the formula*) |
|
960 val dlcm = mk_numeral (divlcm x cfm) |
|
961 (* Which set is smaller to generate the (hoepfully) shorter proof*) |
|
962 val cms = "mi" |
|
963 (* synthesize the proof of cooper's theorem*) |
|
964 (* cp_thm: EX x. cfm = Q*) |
|
965 val cp_thm = cooper_thm sg cms x cfm dlcm A B |
|
966 (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*) |
|
967 (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*) |
|
968 val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans))) |
|
969 (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*) |
|
970 val (lsuth,rsuth) = qe_get_terms (uth) |
|
971 (* lseacth = EX x. efm; rseacth = EX x. fm*) |
|
972 val (lseacth,rseacth) = qe_get_terms(e_ac_thm) |
|
973 (* lscth = EX x. cfm; rscth = Q' *) |
|
974 val (lscth,rscth) = qe_get_terms (exp_cp_thm) |
|
975 (* u_c_thm: EX x. P(l*x) = Q'*) |
|
976 val u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans |
|
977 (* result: EX x. efm = Q'*) |
|
978 in ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans) |
|
979 end |
|
980 |cooper_prv2 _ _ _ = error "Parameters format"; |
|
981 |
923 |
982 |
924 (* **************************************** *) |
983 (* **************************************** *) |
925 (* An Other Version of cooper proving *) |
984 (* An Other Version of cooper proving *) |
926 (* by giving a withness for EX *) |
985 (* by giving a withness for EX *) |
927 (* **************************************** *) |
986 (* **************************************** *) |