# HG changeset patch # User paulson # Date 1119965284 -7200 # Node ID 8de7581437866f235dd8df8b5f0d3ae3b30a5eda # Parent b34c8aa657a5fdc25999fd45d195da3ff42fd5d4 stricter first-order check for meson diff -r b34c8aa657a5 -r 8de758143786 src/HOL/Hyperreal/Integration.thy --- a/src/HOL/Hyperreal/Integration.thy Tue Jun 28 15:27:45 2005 +0200 +++ b/src/HOL/Hyperreal/Integration.thy Tue Jun 28 15:28:04 2005 +0200 @@ -368,12 +368,8 @@ text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *} -lemma choiceP: "\x. P(x) --> (\y. Q x y) ==> \f. (\x. P(x) --> Q x (f x))" -by meson - -lemma choiceP2: "\x. P(x) --> (\y. R(y) & (\z. Q x y z)) ==> - \f fa. (\x. P(x) --> R(f x) & Q x (f x) (fa x))" -by meson +lemma choiceP: "\x. P(x) --> (\y. Q x y) ==> \f. (\x. P(x) --> Q x (f x))" +by (insert bchoice [of "Collect P" Q], simp) (*UNUSED lemma choice2: "\x. (\y. R(y) & (\z. Q x y z)) ==> diff -r b34c8aa657a5 -r 8de758143786 src/HOL/Induct/Comb.thy --- a/src/HOL/Induct/Comb.thy Tue Jun 28 15:27:45 2005 +0200 +++ b/src/HOL/Induct/Comb.thy Tue Jun 28 15:28:04 2005 +0200 @@ -104,8 +104,7 @@ apply (simp (no_asm_simp) add: diamond_def) apply (rule impI [THEN allI, THEN allI]) apply (erule rtrancl_induct, blast) -apply (best intro: rtrancl_trans [OF _ r_into_rtrancl] - elim: diamond_strip_lemmaE [THEN exE]) +apply (meson rtrancl_trans r_into_rtrancl diamond_strip_lemmaE) done diff -r b34c8aa657a5 -r 8de758143786 src/HOL/Reconstruction.thy --- a/src/HOL/Reconstruction.thy Tue Jun 28 15:27:45 2005 +0200 +++ b/src/HOL/Reconstruction.thy Tue Jun 28 15:28:04 2005 +0200 @@ -9,25 +9,24 @@ theory Reconstruction imports Hilbert_Choice Map Infinite_Set Extraction uses "Tools/res_lib.ML" - "Tools/res_clause.ML" - "Tools/res_skolem_function.ML" - "Tools/res_axioms.ML" - "Tools/res_types_sorts.ML" + "Tools/res_clause.ML" + "Tools/res_skolem_function.ML" + "Tools/res_axioms.ML" + "Tools/res_types_sorts.ML" - "Tools/ATP/recon_prelim.ML" - "Tools/ATP/recon_order_clauses.ML" - "Tools/ATP/recon_translate_proof.ML" - "Tools/ATP/recon_parse.ML" - "Tools/ATP/recon_transfer_proof.ML" - "Tools/ATP/VampCommunication.ML" - "Tools/ATP/VampireCommunication.ML" - "Tools/ATP/SpassCommunication.ML" - "Tools/ATP/watcher.sig" - "Tools/ATP/watcher.ML" - "Tools/ATP/res_clasimpset.ML" - "Tools/res_atp.ML" - - "Tools/reconstruction.ML" + "Tools/ATP/recon_prelim.ML" + "Tools/ATP/recon_order_clauses.ML" + "Tools/ATP/recon_translate_proof.ML" + "Tools/ATP/recon_parse.ML" + "Tools/ATP/recon_transfer_proof.ML" + "Tools/ATP/VampCommunication.ML" + "Tools/ATP/VampireCommunication.ML" + "Tools/ATP/SpassCommunication.ML" + "Tools/ATP/watcher.sig" + "Tools/ATP/watcher.ML" + "Tools/ATP/res_clasimpset.ML" + "Tools/res_atp.ML" + "Tools/reconstruction.ML" begin diff -r b34c8aa657a5 -r 8de758143786 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Tue Jun 28 15:27:45 2005 +0200 +++ b/src/HOL/Tools/meson.ML Tue Jun 28 15:28:04 2005 +0200 @@ -138,19 +138,23 @@ then ths (*tautology ignored*) else if not (has_consts ["All","Ex","op &"] (prop_of th)) then th::ths (*no work to do, terminate*) - else (*conjunction?*) - cnf_aux seen (th RS conjunct1, - cnf_aux seen (th RS conjunct2, ths)) - handle THM _ => (*universal quantifier?*) - cnf_aux seen (freeze_spec th, ths) - handle THM _ => (*existential quantifier? Insert Skolem functions.*) + else case head_of (HOLogic.dest_Trueprop (concl_of th)) of + Const ("op &", _) => (*conjunction*) + cnf_aux seen (th RS conjunct1, + cnf_aux seen (th RS conjunct2, ths)) + | Const ("All", _) => (*universal quantifier*) + cnf_aux seen (freeze_spec th, ths) + | Const ("Ex", _) => + (*existential quantifier: Insert Skolem functions*) cnf_aux seen (tryres (th,skoths), ths) - handle THM _ => (*disjunction?*) - let val tac = - (METAHYPS (resop (cnf_nil seen)) 1) THEN - (fn st' => st' |> - METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1) - in Seq.list_of (tac (th RS disj_forward)) @ ths end + | Const ("op |", _) => (*disjunction*) + let val tac = + (METAHYPS (resop (cnf_nil seen)) 1) THEN + (fn st' => st' |> + METAHYPS + (resop (cnf_nil (literals (concl_of st') @ seen))) 1) + in Seq.list_of (tac (th RS disj_forward)) @ ths end + | _ => (*no work to do*) th::ths and cnf_nil seen th = (cnf_aux seen (th,[])) in name_ref := 19; (*It's safe to reset this in a top-level call to cnf*) @@ -235,15 +239,16 @@ val has_meta_conn = exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "Goal"]); -(*Raises an exception if any Vars in the theorem mention type bool. That would mean - they are higher-order, and in addition, they could cause make_horn to loop! - Functions taking Boolean arguments are also rejected.*) -fun check_no_bool th = +(*Raises an exception if any Vars in the theorem mention type bool; they + could cause make_horn to loop! Also rejects functions whose arguments are + Booleans or other functions.*) +fun check_is_fol th = let val {prop,...} = rep_thm th in if exists (has_bool o fastype_of) (term_vars prop) orelse + not (Term.is_first_order ["all","All","Ex"] prop) orelse has_bool_arg_const prop orelse has_meta_conn prop - then raise THM ("check_no_bool", 0, [th]) else th + then raise THM ("check_is_fol", 0, [th]) else th end; (*Create a meta-level Horn clause*) @@ -330,7 +335,7 @@ val nnf_ss = HOL_basic_ss addsimps Ex1_def::Ball_def::Bex_def::simp_thms; fun make_nnf th = th |> simplify nnf_ss - |> check_no_bool |> make_nnf1 + |> check_is_fol |> make_nnf1 (*Pull existential quantifiers to front. This accomplishes Skolemization for clauses that arise from a subgoal.*) @@ -371,12 +376,14 @@ cut_facts_tac (map (skolemize o make_nnf) prems) THEN' REPEAT o (etac exE); -(*Shell of all meson-tactics. Supplies cltac with clauses: HOL disjunctions*) -fun MESON cltac = SELECT_GOAL - (EVERY1 [rtac ccontr, - METAHYPS (fn negs => - EVERY1 [skolemize_prems_tac negs, - METAHYPS (cltac o make_clauses)])]); +(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions*) +fun MESON cltac i st = + SELECT_GOAL + (EVERY1 [rtac ccontr, + METAHYPS (fn negs => + EVERY1 [skolemize_prems_tac negs, + METAHYPS (cltac o make_clauses)])]) i st + handle THM _ => no_tac st; (*probably from check_is_fol*) (** Best-first search versions **) @@ -446,7 +453,7 @@ (*Converting one clause*) fun make_meta_clause th = - negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th)); + negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th)); fun make_meta_clauses ths = name_thms "MClause#" diff -r b34c8aa657a5 -r 8de758143786 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Tue Jun 28 15:27:45 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Tue Jun 28 15:28:04 2005 +0200 @@ -38,14 +38,7 @@ (* a tactic used to prove an elim-rule. *) fun elimRule_tac th = ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac th 1) THEN - REPEAT(Fast_tac 1); - - -(* This following version fails sometimes, need to investigate, do not use it now. *) -fun elimRule_tac' th = - ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac th 1) THEN - REPEAT(SOLVE((etac exI 1) ORELSE (rtac conjI 1) ORELSE (rtac disjI1 1) ORELSE (rtac disjI2 1))); - + REPEAT(fast_tac HOL_cs 1); exception ELIMR2FOL of string; @@ -138,7 +131,6 @@ let val tm = elimR2Fol th val ctm = cterm_of (sign_of_thm th) tm in - prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th]) end else th; @@ -159,12 +151,9 @@ (*Convert a theorem into NNF and also skolemize it. Original version, using Hilbert's epsilon in the resulting clauses.*) fun skolem_axiom th = - if Term.is_first_order (prop_of th) then - let val th' = (skolemize o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) th - in - repeat_RS th' someI_ex - end - else raise THM ("skolem_axiom: not first-order", 0, [th]); + let val th' = (skolemize o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) th + in repeat_RS th' someI_ex + end; fun cnf_rule th = make_clauses [skolem_axiom (transform_elim th)]; @@ -240,11 +229,11 @@ (*Given the definition of a Skolem function, return a theorem to replace an existential formula by a use of that function.*) -fun skolem_of_def def = +fun skolem_of_def def = let val (c,rhs) = Drule.dest_equals (cprop_of (Drule.freeze_all def)) val (ch, frees) = c_variant_abs_multi (rhs, []) val (chil,cabs) = Thm.dest_comb ch - val {sign, t, ...} = rep_cterm chil + val {sign,t, ...} = rep_cterm chil val (Const ("Hilbert_Choice.Eps", Type("fun",[_,T]))) = t val cex = Thm.cterm_of sign (HOLogic.exists_const T) val ex_tm = c_mkTrueprop (Thm.capply cex cabs) @@ -256,11 +245,9 @@ (*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*) fun to_nnf thy th = - if Term.is_first_order (prop_of th) then - th |> Thm.transfer thy - |> transform_elim |> Drule.freeze_all - |> ObjectLogic.atomize_thm |> make_nnf - else raise THM ("to_nnf: not first-order", 0, [th]); + th |> Thm.transfer thy + |> transform_elim |> Drule.freeze_all + |> ObjectLogic.atomize_thm |> make_nnf; (*The cache prevents repeated clausification of a theorem, and also repeated declaration of Skolem functions*) @@ -268,8 +255,7 @@ (*Declare Skolem functions for a theorem, supplied in nnf and with its name*) fun skolem thy (name,th) = - let val cname = (case name of - "" => gensym "sko" | s => Sign.base_name s) + let val cname = (case name of "" => gensym "sko" | s => Sign.base_name s) val thy' = declare_skofuns cname (#prop (rep_thm th)) thy in (map (skolem_of_def o #2) (axioms_of thy'), thy') end; @@ -278,14 +264,19 @@ | skolemlist ((name,th)::nths) thy = (case Symtab.lookup (!clause_cache,name) of NONE => - let val nnfth = to_nnf thy th - val (skoths,thy') = skolem thy (name, nnfth) - val cls = Meson.make_cnf skoths nnfth - in clause_cache := Symtab.update ((name, (th,cls)), !clause_cache); - skolemlist nths thy' - end + let val (nnfth,ok) = (to_nnf thy th, true) + handle THM _ => (asm_rl, false) + in + if ok then + let val (skoths,thy') = skolem thy (name, nnfth) + val cls = Meson.make_cnf skoths nnfth + in clause_cache := + Symtab.update ((name, (th,cls)), !clause_cache); + skolemlist nths thy' + end + else skolemlist nths thy + end | SOME _ => skolemlist nths thy) (*FIXME: check for duplicate names?*) - handle THM _ => skolemlist nths thy; (*Exported function to convert Isabelle theorems into axiom clauses*) fun cnf_axiom (name,th) = diff -r b34c8aa657a5 -r 8de758143786 src/HOL/ex/Primrec.thy --- a/src/HOL/ex/Primrec.thy Tue Jun 28 15:27:45 2005 +0200 +++ b/src/HOL/ex/Primrec.thy Tue Jun 28 15:28:04 2005 +0200 @@ -286,8 +286,14 @@ ==> \k. \l. COMP g fs l < ack(k, list_add l)" apply (unfold COMP_def) apply (frule Int_lower1 [THEN lists_mono, THEN subsetD]) - apply (drule COMP_map_aux) - apply (meson ack_less_mono2 ack_nest_bound less_trans) + --{*Now, if meson tolerated map, we could finish with + @{text "(drule COMP_map_aux, meson ack_less_mono2 ack_nest_bound less_trans).*} + apply (erule COMP_map_aux [THEN exE]) + apply (rule exI) + apply (rule allI) + apply (drule spec)+ + apply (erule less_trans) + apply (blast intro: ack_less_mono2 ack_nest_bound less_trans) done