Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* ========================================================================= *) (* Equality elimination including Brand transformation and relatives. *) (* *) (* Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.) *) (* ========================================================================= *) START_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* The x^2 = 1 implies Abelian problem. *) (* ------------------------------------------------------------------------- *) meson <<(forall x. P(1,x,x)) /\ (forall x. P(x,x,1)) /\ (forall u v w x y z. P(x,y,u) /\ P(y,z,w) ==> (P(x,w,v) <=> P(u,z,v))) ==> forall a b c. P(a,b,c) ==> P(b,a,c)>>;; (* ------------------------------------------------------------------------- *) (* Lemma for equivalence elimination. *) (* ------------------------------------------------------------------------- *) meson <<(forall x. R(x,x)) /\ (forall x y. R(x,y) ==> R(y,x)) /\ (forall x y z. R(x,y) /\ R(y,z) ==> R(x,z)) <=> (forall x y. R(x,y) <=> (forall z. R(x,z) <=> R(y,z)))>>;; END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* Brand's S and T modifications on clauses. *) (* ------------------------------------------------------------------------- *) let rec modify_S cl = try let (s,t) = tryfind dest_eq cl in let eq1 = mk_eq s t and eq2 = mk_eq t s in let sub = modify_S (subtract cl [eq1]) in map (insert eq1) sub @ map (insert eq2) sub with Failure _ -> [cl];; let rec modify_T cl = match cl with (Atom(R("=",[s;t])) as eq)::ps -> let ps' = modify_T ps in let w = Var(variant "w" (itlist (union ** fv) ps' (fv eq))) in Not(mk_eq t w)::(mk_eq s w)::ps' | p::ps -> p::(modify_T ps) | [] -> [];; (* ------------------------------------------------------------------------- *) (* Finding nested non-variable subterms. *) (* ------------------------------------------------------------------------- *) let is_nonvar = function (Var x) -> false | _ -> true;; let find_nestnonvar tm = match tm with Var x -> failwith "findnvsubt" | Fn(f,args) -> find is_nonvar args;; let rec find_nvsubterm fm = match fm with Atom(R("=",[s;t])) -> tryfind find_nestnonvar [s;t] | Atom(R(p,args)) -> find is_nonvar args | Not p -> find_nvsubterm p;; (* ------------------------------------------------------------------------- *) (* Replacement (substitution for non-variable) in term and literal. *) (* ------------------------------------------------------------------------- *) let rec replacet rfn tm = try apply rfn tm with Failure _ -> match tm with Fn(f,args) -> Fn(f,map (replacet rfn) args) | _ -> tm;; let replace rfn = onformula (replacet rfn);; (* ------------------------------------------------------------------------- *) (* E-modification of a clause. *) (* ------------------------------------------------------------------------- *) let rec emodify fvs cls = try let t = tryfind find_nvsubterm cls in let w = variant "w" fvs in let cls' = map (replace (t |=> Var w)) cls in emodify (w::fvs) (Not(mk_eq t (Var w))::cls') with Failure _ -> cls;; let modify_E cls = emodify (itlist (union ** fv) cls []) cls;; (* ------------------------------------------------------------------------- *) (* Overall Brand transformation. *) (* ------------------------------------------------------------------------- *) let brand cls = let cls1 = map modify_E cls in let cls2 = itlist (union ** modify_S) cls1 [] in [mk_eq (Var "x") (Var "x")]::(map modify_T cls2);; (* ------------------------------------------------------------------------- *) (* Incorporation into MESON. *) (* ------------------------------------------------------------------------- *) let bpuremeson fm = let cls = brand(simpcnf(specialize(pnf fm))) in let rules = itlist ((@) ** contrapositives) cls [] in deepen (fun n -> mexpand rules [] False (fun x -> x) (undefined,n,0); n) 0;; let bmeson fm = let fm1 = askolemize(Not(generalize fm)) in map (bpuremeson ** list_conj) (simpdnf fm1);; (* ------------------------------------------------------------------------- *) (* Examples. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; time bmeson <<(exists x. x = f(g(x)) /\ forall x'. x' = f(g(x')) ==> x = x') <=> (exists y. y = g(f(y)) /\ forall y'. y' = g(f(y')) ==> y = y')>>;; time emeson <<(exists x. x = f(g(x)) /\ forall x'. x' = f(g(x')) ==> x = x') <=> (exists y. y = g(f(y)) /\ forall y'. y' = g(f(y')) ==> y = y')>>;; time bmeson <<(forall x y z. x * (y * z) = (x * y) * z) /\ (forall x. e * x = x) /\ (forall x. i(x) * x = e) ==> forall x. x * i(x) = e>>;; END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* Older stuff not now in the text. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; let emeson fm = meson (equalitize fm);; let ewd = <<(forall x. f(x) ==> g(x)) /\ (exists x. f(x)) /\ (forall x y. g(x) /\ g(y) ==> x = y) ==> forall y. g(y) ==> f(y)>>;; let wishnu = <<(exists x. x = f(g(x)) /\ forall x'. x' = f(g(x')) ==> x = x') <=> (exists y. y = g(f(y)) /\ forall y'. y' = g(f(y')) ==> y = y')>>;; let group1 = <<(forall x y z. x * (y * z) = (x * y) * z) /\ (forall x. e * x = x) /\ (forall x. i(x) * x = e) ==> forall x. x * e = x>>;; let group2 = <<(forall x y z. x * (y * z) = (x * y) * z) /\ (forall x. e * x = x) /\ (forall x. i(x) * x = e) ==> forall x. x * i(x) = e>>;; time bmeson ewd;; time emeson ewd;; (*********** time bmeson wishnu;; time emeson wishnu;; time bmeson group1;; time emeson group1;; time bmeson group2;; time emeson group2;; *************) (* ------------------------------------------------------------------------- *) (* Nice function composition exercise from "Conceptual Mathematics". *) (* ------------------------------------------------------------------------- *) (************** let fm = <<(forall x y z. x * (y * z) = (x * y) * z) /\ p * q * p = p ==> exists q'. p * q' * p = p /\ q' * p * q' = q'>>;; time bmeson fm;; (** Seems to take a bit longer than below version **) time emeson fm;; (** Works in 64275 seconds(!), depth 30, on laptop **) ****************) (**** Some other predicate formulations no longer in the main text meson <<(forall x. P(1,x,x)) /\ (forall x. P(i(x),x,1)) /\ (forall u v w x y z. P(x,y,u) /\ P(y,z,w) ==> (P(x,w,v) <=> P(u,z,v))) ==> forall x. P(x,1,x)>>;; meson <<(forall x. P(1,x,x)) /\ (forall x. P(i(x),x,1)) /\ (forall u v w x y z. P(x,y,u) /\ P(y,z,w) ==> (P(x,w,v) <=> P(u,z,v))) ==> forall x. P(x,i(x),1)>>;; (* ------------------------------------------------------------------------- *) (* See how efficiency drops when we assert completeness. *) (* ------------------------------------------------------------------------- *) meson <<(forall x. P(1,x,x)) /\ (forall x. P(x,x,1)) /\ (forall x y. exists z. P(x,y,z)) /\ (forall u v w x y z. P(x,y,u) /\ P(y,z,w) ==> (P(x,w,v) <=> P(u,z,v))) ==> forall a b c. P(a,b,c) ==> P(b,a,c)>>;; ****) (*** More reductions, not now explicitly in the text. meson <<(forall x. R(x,x)) /\ (forall x y z. R(x,y) /\ R(y,z) ==> R(x,z)) <=> (forall x y. R(x,y) <=> (forall z. R(y,z) ==> R(x,z)))>>;; meson <<(forall x y. R(x,y) ==> R(y,x)) <=> (forall x y. R(x,y) <=> R(x,y) /\ R(y,x))>>;; (* ------------------------------------------------------------------------- *) (* Show how Equiv' reduces to triviality. *) (* ------------------------------------------------------------------------- *) meson <<(forall x. (forall w. R'(x,w) <=> R'(x,w))) /\ (forall x y. (forall w. R'(x,w) <=> R'(y,w)) ==> (forall w. R'(y,w) <=> R'(x,w))) /\ (forall x y z. (forall w. R'(x,w) <=> R'(y,w)) /\ (forall w. R'(y,w) <=> R'(z,w)) ==> (forall w. R'(x,w) <=> R'(z,w)))>>;; (* ------------------------------------------------------------------------- *) (* More auxiliary proofs for Brand's S and T modification. *) (* ------------------------------------------------------------------------- *) meson <<(forall x y. R(x,y) <=> (forall z. R'(x,z) <=> R'(y,z))) /\ (forall x. R'(x,x)) ==> forall x y. ~R'(x,y) ==> ~R(x,y)>>;; meson <<(forall x y. R(x,y) <=> (forall z. R'(y,z) ==> R'(x,z))) /\ (forall x. R'(x,x)) ==> forall x y. ~R'(x,y) ==> ~R(x,y)>>;; meson <<(forall x y. R(x,y) <=> R'(x,y) /\ R'(y,x)) ==> forall x y. ~R'(x,y) ==> ~R(x,y)>>;; ***) END_INTERACTIVE;;