--- 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: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))"
-by meson
-
-lemma choiceP2: "\<forall>x. P(x) --> (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
- \<exists>f fa. (\<forall>x. P(x) --> R(f x) & Q x (f x) (fa x))"
-by meson
+lemma choiceP: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))"
+by (insert bchoice [of "Collect P" Q], simp)
(*UNUSED
lemma choice2: "\<forall>x. (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
--- 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
--- 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
--- 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#"
--- 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) =
--- 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 @@
==> \<exists>k. \<forall>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