# HG changeset patch # User lcp # Date 785718035 -3600 # Node ID 9dcce140bdfce7b284a7e2b374ae6fe8998faf6d # Parent faa3efc1d130754bcdaf897c7a42db28bcbad942 prove_fun: new; no longer depends upon the version in simpdata.ML diff -r faa3efc1d130 -r 9dcce140bdfc src/FOL/ex/mini.ML --- a/src/FOL/ex/mini.ML Thu Nov 24 10:57:24 1994 +0100 +++ b/src/FOL/ex/mini.ML Fri Nov 25 00:00:35 1994 +0100 @@ -16,136 +16,58 @@ (*** de Morgan laws ***) -val not_conjD = prove_fun "~(P&Q) ==> ~P | ~Q"; -val not_disjD = prove_fun "~(P|Q) ==> ~P & ~Q"; -val not_notD = prove_fun "~~P ==> P"; -val not_allD = prove_fun "~(ALL x.P(x)) ==> EX x. ~P(x)"; -val not_exD = prove_fun "~(EX x.P(x)) ==> ALL x. ~P(x)"; +fun prove_fun s = + (writeln s; + prove_goal FOL.thy s + (fn prems => [ (cut_facts_tac prems 1), + (Cla.fast_tac FOL_cs 1) ])); +val demorgans = map prove_fun + ["~(P&Q) <-> ~P | ~Q", + "~(P|Q) <-> ~P & ~Q", + "~~P <-> P", + "~(ALL x.P(x)) <-> (EX x. ~P(x))", + "~(EX x.P(x)) <-> (ALL x. ~P(x))"]; (*** Removal of --> and <-> (positive and negative occurrences) ***) - -val imp_to_disjD = prove_fun "P-->Q ==> ~P | Q"; -val not_impD = prove_fun "~(P-->Q) ==> P & ~Q"; +(*Last one is important for computing a compact CNF*) +val nnf_rews = map prove_fun + ["(P-->Q) <-> (~P | Q)", + "~(P-->Q) <-> (P & ~Q)", + "(P<->Q) <-> (~P | Q) & (~Q | P)", + "~(P<->Q) <-> (P | Q) & (~P | ~Q)"]; -val iff_to_disjD = prove_fun "P<->Q ==> (~P | Q) & (~Q | P)"; - -(*Much more efficient than (P & ~Q) | (Q & ~P) for computing CNF*) -val not_iffD = prove_fun "~(P<->Q) ==> (P | Q) & (~P | ~Q)"; - +(* BEWARE: rewrite rules for <-> can confuse the simplifier!! *) (*** Pushing in the existential quantifiers ***) -val null_exD = prove_fun "EX x. P ==> P"; - -(** Conjunction **) - -val conj_exD1 = prove_fun "EX x. P(x) & Q ==> (EX x.P(x)) & Q"; -val conj_exD2 = prove_fun "EX x. P & Q(x) ==> P & (EX x.Q(x))"; - -(** Disjunction **) - -val disj_exD = prove_fun "EX x. P(x) | Q(x) ==> (EX x.P(x)) | (EX x.Q(x))"; -val disj_exD1 = prove_fun "EX x. P(x) | Q ==> (EX x.P(x)) | Q"; -val disj_exD2 = prove_fun "EX x. P | Q(x) ==> P | (EX x.Q(x))"; - +val ex_rews = map prove_fun + ["(EX x. P) <-> P", + "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q", + "(EX x. P & Q(x)) <-> P & (EX x.Q(x))", + "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))", + "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q", + "(EX x. P | Q(x)) <-> P | (EX x.Q(x))"]; (*** Pushing in the universal quantifiers ***) -val null_allD = prove_fun "ALL x. P ==> P"; - -(** Conjunction **) - -val conj_allD = prove_fun "ALL x. P(x) & Q(x) ==> (ALL x.P(x)) & (ALL x.Q(x))"; -val conj_allD1 = prove_fun "ALL x. P(x) & Q ==> (ALL x.P(x)) & Q"; -val conj_allD2 = prove_fun "ALL x. P & Q(x) ==> P & (ALL x.Q(x))"; - -(** Disjunction **) - -val disj_allD1 = prove_fun "ALL x. P(x) | Q ==> (ALL x.P(x)) | Q"; -val disj_allD2 = prove_fun "ALL x. P | Q(x) ==> P | (ALL x.Q(x))"; - - -(**** Lemmas for forward proof (like congruence rules) ****) - -(*NOTE: could handle conjunctions (faster?) by - nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) -val major::prems = goal FOL.thy - "[| P'&Q'; P' ==> P; Q' ==> Q |] ==> P&Q"; -by (rtac (major RS conjE) 1); -by (rtac conjI 1); -by (ALLGOALS (eresolve_tac prems)); -val conj_forward = result(); - -val major::prems = goal FOL.thy - "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q"; -by (rtac (major RS disjE) 1); -by (ALLGOALS (dresolve_tac prems)); -by (ALLGOALS (eresolve_tac [disjI1,disjI2])); -val disj_forward = result(); - -val major::prems = goal FOL.thy - "[| ALL x. P'(x); !!x. P'(x) ==> P(x) |] ==> ALL x. P(x)"; -by (rtac allI 1); -by (resolve_tac prems 1); -by (rtac (major RS spec) 1); -val all_forward = result(); - -val major::prems = goal FOL.thy - "[| EX x. P'(x); !!x. P'(x) ==> P(x) |] ==> EX x. P(x)"; -by (rtac (major RS exE) 1); -by (rtac exI 1); -by (eresolve_tac prems 1); -val ex_forward = result(); +val all_rews = map prove_fun + ["(ALL x. P) <-> P", + "(ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))", + "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q", + "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))", + "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q", + "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"]; -val mini_rls = - [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, - not_impD, not_iffD, not_allD, not_exD, not_notD, - null_exD, conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2, - null_allD, conj_allD, conj_allD1, conj_allD2, disj_allD1, disj_allD2]; - -val forward_rls = [conj_forward, disj_forward, all_forward, ex_forward]; - -(*** The transformation is done by forward proof: resolution. - A tactic approach using dresolve_tac seems to be MUCH slower. - The simplifier could compute nnf but not miniscope. -***) - -(*Permits forward proof from rules that discharge assumptions*) -fun forward_res nf state = - Sequence.hd - (tapply(ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)), - state)); - -(**** Operators for forward proof ****) - -(*raises exception if no rules apply -- unlike RL*) -fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) - | tryres (th, []) = raise THM("tryres", 0, [th]); +val mini_ss = + empty_ss + setmksimps (map mk_meta_eq o atomize o gen_all) + setsolver (fn prems => resolve_tac (triv_rls@prems) + ORELSE' assume_tac + ORELSE' etac FalseE) + setsubgoaler asm_simp_tac + addsimps (demorgans @ nnf_rews @ ex_rews @ all_rews); -(*insert one destruction rule into the net*) -fun insert_D_rl (th, net) = - Net.insert_term ((hd (prems_of th), th), net, K false); - -fun net_tryres rls = - let val net = foldr insert_D_rl (rls, Net.empty) - fun tfun th = tryres (th, Net.unify_term net (concl_of th)) - in tfun end; - -val try_mini = net_tryres mini_rls -and try_forward = net_tryres forward_rls; +val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss; -fun make_mini th = sub_mini (try_mini th) - handle THM _ => th -and sub_mini th = sub_mini (try_mini th) - handle THM _ => make_mini (forward_res sub_mini (try_forward th)) - handle THM _ => th; - -fun mini_tac prems = cut_facts_tac (map sub_mini prems); - -fun MINI tac = SELECT_GOAL - (EVERY1 [rtac ccontr, - METAHYPS (fn negs => - EVERY1 [mini_tac negs, tac])]); -