src/HOL/Integ/cooper_proof.ML
changeset 15107 f233706d9fce
parent 14981 e73f8140af78
child 15122 4b52eeb62807
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Wed Aug 04 11:25:08 2004 +0200
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Wed Aug 04 17:43:55 2004 +0200
     1.3 @@ -219,7 +219,8 @@
     1.4          [zdvd_iff_zmod_eq_0,unity_coeff_ex]
     1.5        val ct =  cert_Trueprop sg fm2
     1.6      in 
     1.7 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
     1.8 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] 
     1.9 +
    1.10      end
    1.11  
    1.12    (*"bl" like blast tactic*)
    1.13 @@ -251,7 +252,8 @@
    1.14  
    1.15    | "fa" =>
    1.16      let val ct = cert_Trueprop sg fm2
    1.17 -    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
    1.18 +    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]  
    1.19 +
    1.20      end
    1.21  
    1.22    | "sa" =>
    1.23 @@ -259,7 +261,8 @@
    1.24        val ss = presburger_ss addsimps zadd_ac
    1.25        val ct = cert_Trueprop sg fm2
    1.26      in 
    1.27 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
    1.28 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
    1.29 +
    1.30      end
    1.31    (* like Existance Conjunction *)
    1.32    | "ec" =>
    1.33 @@ -283,7 +286,8 @@
    1.34        val ss = presburger_ss addsimps zadd_ac
    1.35        val ct = cert_Trueprop sg fm2
    1.36      in 
    1.37 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
    1.38 +      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
    1.39 +
    1.40      end;
    1.41  
    1.42  (*=============================================================*)
    1.43 @@ -917,6 +921,71 @@
    1.44  |cooper_prv _ _ _ =  error "Parameters format";
    1.45  
    1.46  
    1.47 +(* **************************************** *)
    1.48 +(*    An Other Version of cooper proving    *)
    1.49 +(*     by giving a withness for EX          *)
    1.50 +(* **************************************** *)
    1.51 +
    1.52 +
    1.53 +
    1.54 +fun cooper_prv_w sg (x as Free(xn,xT)) efm = let 
    1.55 +   (* lfm_thm : efm = linearized form of efm*)
    1.56 +   val lfm_thm = proof_of_linform sg [xn] efm
    1.57 +   (*efm2 is the linearized form of efm *) 
    1.58 +   val efm2 = snd(qe_get_terms lfm_thm)
    1.59 +   (* l is the lcm of all coefficients of x *)
    1.60 +   val l = formlcm x efm2
    1.61 +   (*ac_thm: efm = efm2 with adjusted coefficients of x *)
    1.62 +   val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
    1.63 +   (* fm is efm2 with adjusted coefficients of x *)
    1.64 +   val fm = snd (qe_get_terms ac_thm)
    1.65 +  (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
    1.66 +   val  cfm = unitycoeff x fm
    1.67 +   (*afm is fm where c*x is replaced by 1*x or -1*x *)
    1.68 +   val afm = adjustcoeff x l fm
    1.69 +   (* P = %x.afm*)
    1.70 +   val P = absfree(xn,xT,afm)
    1.71 +   (* This simpset allows the elimination of the sets in bex {1..d} *)
    1.72 +   val ss = presburger_ss addsimps
    1.73 +     [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
    1.74 +   (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
    1.75 +   val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
    1.76 +   (* e_ac_thm : Ex x. efm = EX x. fm*)
    1.77 +   val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
    1.78 +   (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    1.79 +   val (lsuth,rsuth) = qe_get_terms (uth)
    1.80 +   (* lseacth = EX x. efm; rseacth = EX x. fm*)
    1.81 +   val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
    1.82 +
    1.83 +   val (w,rs) = cooper_w [] cfm
    1.84 +   val exp_cp_thm =  case w of 
    1.85 +     (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*)
    1.86 +    Some n =>  e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*)
    1.87 +   |_ => let 
    1.88 +    (* A and B set of the formula*)
    1.89 +    val A = aset x cfm
    1.90 +    val B = bset x cfm
    1.91 +    (* the divlcm (delta) of the formula*)
    1.92 +    val dlcm = mk_numeral (divlcm x cfm)
    1.93 +    (* Which set is smaller to generate the (hoepfully) shorter proof*)
    1.94 +    val cms = if ((length A) < (length B )) then "pi" else "mi"
    1.95 +    (* synthesize the proof of cooper's theorem*)
    1.96 +     (* cp_thm: EX x. cfm = Q*)
    1.97 +    val cp_thm = cooper_thm sg cms x cfm dlcm A B
    1.98 +     (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    1.99 +    (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
   1.100 +    in refl RS (simplify ss (cp_thm RSN (2,trans)))
   1.101 +    end
   1.102 +   (* lscth = EX x. cfm; rscth = Q' *)
   1.103 +   val (lscth,rscth) = qe_get_terms (exp_cp_thm)
   1.104 +   (* u_c_thm: EX x. P(l*x) = Q'*)
   1.105 +   val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
   1.106 +   (* result: EX x. efm = Q'*)
   1.107 + in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
   1.108 +   end
   1.109 +|cooper_prv_w _ _ _ =  error "Parameters format";
   1.110 +
   1.111 +
   1.112  
   1.113  fun decomp_cnnf sg lfnp P = case P of 
   1.114       Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )