author paulson Tue, 28 Jun 2005 15:28:04 +0200 changeset 16588 8de758143786 parent 16587 b34c8aa657a5 child 16589 24c32abc8b84
stricter first-order check for meson
 src/HOL/Hyperreal/Integration.thy file | annotate | diff | comparison | revisions src/HOL/Induct/Comb.thy file | annotate | diff | comparison | revisions src/HOL/Reconstruction.thy file | annotate | diff | comparison | revisions src/HOL/Tools/meson.ML file | annotate | diff | comparison | revisions src/HOL/Tools/res_axioms.ML file | annotate | diff | comparison | revisions src/HOL/ex/Primrec.thy file | annotate | diff | comparison | revisions
```--- 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 (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

```