stricter first-order check for meson
authorpaulson
Tue Jun 28 15:28:04 2005 +0200 (2005-06-28)
changeset 165888de758143786
parent 16587 b34c8aa657a5
child 16589 24c32abc8b84
stricter first-order check for meson
src/HOL/Hyperreal/Integration.thy
src/HOL/Induct/Comb.thy
src/HOL/Reconstruction.thy
src/HOL/Tools/meson.ML
src/HOL/Tools/res_axioms.ML
src/HOL/ex/Primrec.thy
     1.1 --- a/src/HOL/Hyperreal/Integration.thy	Tue Jun 28 15:27:45 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/Integration.thy	Tue Jun 28 15:28:04 2005 +0200
     1.3 @@ -368,12 +368,8 @@
     1.4  
     1.5  text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *}
     1.6  
     1.7 -lemma choiceP: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))"
     1.8 -by meson
     1.9 -
    1.10 -lemma choiceP2: "\<forall>x. P(x) --> (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
    1.11 -      \<exists>f fa. (\<forall>x. P(x) --> R(f x) & Q x (f x) (fa x))"
    1.12 -by meson
    1.13 +lemma choiceP: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))" 
    1.14 +by (insert bchoice [of "Collect P" Q], simp) 
    1.15  
    1.16  (*UNUSED
    1.17  lemma choice2: "\<forall>x. (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
     2.1 --- a/src/HOL/Induct/Comb.thy	Tue Jun 28 15:27:45 2005 +0200
     2.2 +++ b/src/HOL/Induct/Comb.thy	Tue Jun 28 15:28:04 2005 +0200
     2.3 @@ -104,8 +104,7 @@
     2.4  apply (simp (no_asm_simp) add: diamond_def)
     2.5  apply (rule impI [THEN allI, THEN allI])
     2.6  apply (erule rtrancl_induct, blast)
     2.7 -apply (best intro: rtrancl_trans [OF _ r_into_rtrancl] 
     2.8 -            elim: diamond_strip_lemmaE [THEN exE])
     2.9 +apply (meson rtrancl_trans r_into_rtrancl diamond_strip_lemmaE)
    2.10  done
    2.11  
    2.12  
     3.1 --- a/src/HOL/Reconstruction.thy	Tue Jun 28 15:27:45 2005 +0200
     3.2 +++ b/src/HOL/Reconstruction.thy	Tue Jun 28 15:28:04 2005 +0200
     3.3 @@ -9,25 +9,24 @@
     3.4  theory Reconstruction
     3.5      imports Hilbert_Choice Map Infinite_Set Extraction
     3.6      uses "Tools/res_lib.ML"
     3.7 -	  "Tools/res_clause.ML"
     3.8 -	  "Tools/res_skolem_function.ML"
     3.9 -	  "Tools/res_axioms.ML"
    3.10 -	  "Tools/res_types_sorts.ML"
    3.11 +	 "Tools/res_clause.ML"
    3.12 +	 "Tools/res_skolem_function.ML"
    3.13 +	 "Tools/res_axioms.ML"
    3.14 +	 "Tools/res_types_sorts.ML"
    3.15  
    3.16 -      "Tools/ATP/recon_prelim.ML"
    3.17 - 	  "Tools/ATP/recon_order_clauses.ML"
    3.18 - 	  "Tools/ATP/recon_translate_proof.ML"
    3.19 - 	  "Tools/ATP/recon_parse.ML"
    3.20 - 	  "Tools/ATP/recon_transfer_proof.ML"
    3.21 -	  "Tools/ATP/VampCommunication.ML"
    3.22 -	  "Tools/ATP/VampireCommunication.ML"
    3.23 -	  "Tools/ATP/SpassCommunication.ML"
    3.24 -	  "Tools/ATP/watcher.sig"
    3.25 -	  "Tools/ATP/watcher.ML"
    3.26 -	  "Tools/ATP/res_clasimpset.ML"
    3.27 -	  "Tools/res_atp.ML"
    3.28 -
    3.29 -      "Tools/reconstruction.ML"
    3.30 +	 "Tools/ATP/recon_prelim.ML"
    3.31 +	 "Tools/ATP/recon_order_clauses.ML"
    3.32 +	 "Tools/ATP/recon_translate_proof.ML"
    3.33 +	 "Tools/ATP/recon_parse.ML"
    3.34 +	 "Tools/ATP/recon_transfer_proof.ML"
    3.35 +	 "Tools/ATP/VampCommunication.ML"
    3.36 +	 "Tools/ATP/VampireCommunication.ML"
    3.37 +	 "Tools/ATP/SpassCommunication.ML"
    3.38 +	 "Tools/ATP/watcher.sig"
    3.39 +	 "Tools/ATP/watcher.ML"
    3.40 +	 "Tools/ATP/res_clasimpset.ML"
    3.41 +	 "Tools/res_atp.ML"
    3.42 +	 "Tools/reconstruction.ML"
    3.43  
    3.44  begin
    3.45  
     4.1 --- a/src/HOL/Tools/meson.ML	Tue Jun 28 15:27:45 2005 +0200
     4.2 +++ b/src/HOL/Tools/meson.ML	Tue Jun 28 15:28:04 2005 +0200
     4.3 @@ -138,19 +138,23 @@
     4.4  	then ths     (*tautology ignored*)
     4.5  	else if not (has_consts ["All","Ex","op &"] (prop_of th))  
     4.6  	then th::ths (*no work to do, terminate*)
     4.7 -	else (*conjunction?*)
     4.8 -	      cnf_aux seen (th RS conjunct1,
     4.9 -			    cnf_aux seen (th RS conjunct2, ths))
    4.10 -	handle THM _ => (*universal quantifier?*)
    4.11 -	      cnf_aux seen (freeze_spec th,  ths)
    4.12 -	handle THM _ => (*existential quantifier? Insert Skolem functions.*)
    4.13 +	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
    4.14 +	    Const ("op &", _) => (*conjunction*)
    4.15 +		cnf_aux seen (th RS conjunct1,
    4.16 +			      cnf_aux seen (th RS conjunct2, ths))
    4.17 +	  | Const ("All", _) => (*universal quantifier*)
    4.18 +	        cnf_aux seen (freeze_spec th,  ths)
    4.19 +	  | Const ("Ex", _) => 
    4.20 +	      (*existential quantifier: Insert Skolem functions*)
    4.21  	      cnf_aux seen (tryres (th,skoths), ths)
    4.22 -	handle THM _ => (*disjunction?*)
    4.23 -	  let val tac =
    4.24 -	      (METAHYPS (resop (cnf_nil seen)) 1) THEN
    4.25 -	     (fn st' => st' |>  
    4.26 -		METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
    4.27 -	  in  Seq.list_of (tac (th RS disj_forward)) @ ths  end 
    4.28 +	  | Const ("op |", _) => (*disjunction*)
    4.29 +	      let val tac =
    4.30 +		  (METAHYPS (resop (cnf_nil seen)) 1) THEN
    4.31 +		   (fn st' => st' |>  
    4.32 +		      METAHYPS 
    4.33 +		        (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
    4.34 +	      in  Seq.list_of (tac (th RS disj_forward)) @ ths  end 
    4.35 +	  | _ => (*no work to do*) th::ths 
    4.36        and cnf_nil seen th = (cnf_aux seen (th,[]))
    4.37    in 
    4.38      name_ref := 19;  (*It's safe to reset this in a top-level call to cnf*)
    4.39 @@ -235,15 +239,16 @@
    4.40  val has_meta_conn = 
    4.41      exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "Goal"]);
    4.42    
    4.43 -(*Raises an exception if any Vars in the theorem mention type bool. That would mean
    4.44 -  they are higher-order, and in addition, they could cause make_horn to loop!
    4.45 -  Functions taking Boolean arguments are also rejected.*)
    4.46 -fun check_no_bool th =
    4.47 +(*Raises an exception if any Vars in the theorem mention type bool; they
    4.48 +  could cause make_horn to loop! Also rejects functions whose arguments are 
    4.49 +  Booleans or other functions.*)
    4.50 +fun check_is_fol th = 
    4.51    let val {prop,...} = rep_thm th
    4.52    in if exists (has_bool o fastype_of) (term_vars prop)  orelse
    4.53 +        not (Term.is_first_order ["all","All","Ex"] prop) orelse
    4.54          has_bool_arg_const prop  orelse  
    4.55          has_meta_conn prop
    4.56 -  then raise THM ("check_no_bool", 0, [th]) else th
    4.57 +  then raise THM ("check_is_fol", 0, [th]) else th
    4.58    end;
    4.59  
    4.60  (*Create a meta-level Horn clause*)
    4.61 @@ -330,7 +335,7 @@
    4.62  val nnf_ss = HOL_basic_ss addsimps Ex1_def::Ball_def::Bex_def::simp_thms;
    4.63  
    4.64  fun make_nnf th = th |> simplify nnf_ss
    4.65 -                     |> check_no_bool |> make_nnf1
    4.66 +                     |> check_is_fol |> make_nnf1
    4.67  
    4.68  (*Pull existential quantifiers to front. This accomplishes Skolemization for
    4.69    clauses that arise from a subgoal.*)
    4.70 @@ -371,12 +376,14 @@
    4.71      cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
    4.72      REPEAT o (etac exE);
    4.73  
    4.74 -(*Shell of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
    4.75 -fun MESON cltac = SELECT_GOAL
    4.76 - (EVERY1 [rtac ccontr,
    4.77 -          METAHYPS (fn negs =>
    4.78 -                    EVERY1 [skolemize_prems_tac negs,
    4.79 -                            METAHYPS (cltac o make_clauses)])]);
    4.80 +(*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
    4.81 +fun MESON cltac i st = 
    4.82 +  SELECT_GOAL
    4.83 +   (EVERY1 [rtac ccontr,
    4.84 +	    METAHYPS (fn negs =>
    4.85 +		      EVERY1 [skolemize_prems_tac negs,
    4.86 +			      METAHYPS (cltac o make_clauses)])]) i st
    4.87 +  handle THM _ => no_tac st;	(*probably from check_is_fol*)		      
    4.88  
    4.89  (** Best-first search versions **)
    4.90  
    4.91 @@ -446,7 +453,7 @@
    4.92  
    4.93  (*Converting one clause*)
    4.94  fun make_meta_clause th = 
    4.95 -	negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th));
    4.96 +    negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th));
    4.97  
    4.98  fun make_meta_clauses ths =
    4.99      name_thms "MClause#"
     5.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Jun 28 15:27:45 2005 +0200
     5.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Jun 28 15:28:04 2005 +0200
     5.3 @@ -38,14 +38,7 @@
     5.4  (* a tactic used to prove an elim-rule. *)
     5.5  fun elimRule_tac th =
     5.6      ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac th 1) THEN
     5.7 -    REPEAT(Fast_tac 1);
     5.8 -
     5.9 -
    5.10 -(* This following version fails sometimes, need to investigate, do not use it now. *)
    5.11 -fun elimRule_tac' th =
    5.12 -   ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac th 1) THEN
    5.13 -   REPEAT(SOLVE((etac exI 1) ORELSE (rtac conjI 1) ORELSE (rtac disjI1 1) ORELSE (rtac disjI2 1))); 
    5.14 -
    5.15 +    REPEAT(fast_tac HOL_cs 1);
    5.16  
    5.17  exception ELIMR2FOL of string;
    5.18  
    5.19 @@ -138,7 +131,6 @@
    5.20      let val tm = elimR2Fol th
    5.21  	val ctm = cterm_of (sign_of_thm th) tm	
    5.22      in
    5.23 -
    5.24  	prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
    5.25      end
    5.26   else th;
    5.27 @@ -159,12 +151,9 @@
    5.28  (*Convert a theorem into NNF and also skolemize it. Original version, using
    5.29    Hilbert's epsilon in the resulting clauses.*)
    5.30  fun skolem_axiom th = 
    5.31 -  if Term.is_first_order (prop_of th) then
    5.32 -    let val th' = (skolemize o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) th
    5.33 -    in 
    5.34 -	repeat_RS th' someI_ex
    5.35 -    end
    5.36 -  else raise THM ("skolem_axiom: not first-order", 0, [th]);
    5.37 +  let val th' = (skolemize o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) th
    5.38 +  in  repeat_RS th' someI_ex
    5.39 +  end;
    5.40  
    5.41  
    5.42  fun cnf_rule th = make_clauses [skolem_axiom (transform_elim th)];
    5.43 @@ -240,11 +229,11 @@
    5.44  
    5.45  (*Given the definition of a Skolem function, return a theorem to replace 
    5.46    an existential formula by a use of that function.*)
    5.47 -fun skolem_of_def def =
    5.48 +fun skolem_of_def def =  
    5.49    let val (c,rhs) = Drule.dest_equals (cprop_of (Drule.freeze_all def))
    5.50        val (ch, frees) = c_variant_abs_multi (rhs, [])
    5.51        val (chil,cabs) = Thm.dest_comb ch
    5.52 -      val {sign, t, ...} = rep_cterm chil
    5.53 +      val {sign,t, ...} = rep_cterm chil
    5.54        val (Const ("Hilbert_Choice.Eps", Type("fun",[_,T]))) = t
    5.55        val cex = Thm.cterm_of sign (HOLogic.exists_const T)
    5.56        val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
    5.57 @@ -256,11 +245,9 @@
    5.58  
    5.59  (*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*)
    5.60  fun to_nnf thy th = 
    5.61 -    if Term.is_first_order (prop_of th) then
    5.62 -      th |> Thm.transfer thy
    5.63 -         |> transform_elim |> Drule.freeze_all
    5.64 -	 |> ObjectLogic.atomize_thm |> make_nnf
    5.65 -    else raise THM ("to_nnf: not first-order", 0, [th]);
    5.66 +    th |> Thm.transfer thy
    5.67 +       |> transform_elim |> Drule.freeze_all
    5.68 +       |> ObjectLogic.atomize_thm |> make_nnf;
    5.69  
    5.70  (*The cache prevents repeated clausification of a theorem, 
    5.71    and also repeated declaration of Skolem functions*)  
    5.72 @@ -268,8 +255,7 @@
    5.73  
    5.74  (*Declare Skolem functions for a theorem, supplied in nnf and with its name*)
    5.75  fun skolem thy (name,th) =
    5.76 -  let val cname = (case name of
    5.77 -                         "" => gensym "sko" | s => Sign.base_name s)
    5.78 +  let val cname = (case name of "" => gensym "sko" | s => Sign.base_name s)
    5.79        val thy' = declare_skofuns cname (#prop (rep_thm th)) thy
    5.80    in (map (skolem_of_def o #2) (axioms_of thy'), thy') end;
    5.81  
    5.82 @@ -278,14 +264,19 @@
    5.83    | skolemlist ((name,th)::nths) thy = 
    5.84        (case Symtab.lookup (!clause_cache,name) of
    5.85  	  NONE => 
    5.86 -	    let val nnfth = to_nnf thy th
    5.87 -		val (skoths,thy') = skolem thy (name, nnfth)
    5.88 -		val cls = Meson.make_cnf skoths nnfth
    5.89 -	    in  clause_cache := Symtab.update ((name, (th,cls)), !clause_cache);
    5.90 -		skolemlist nths thy'
    5.91 -	    end
    5.92 +	    let val (nnfth,ok) = (to_nnf thy th, true)  
    5.93 +	                 handle THM _ => (asm_rl, false)
    5.94 +            in
    5.95 +                if ok then
    5.96 +                    let val (skoths,thy') = skolem thy (name, nnfth)
    5.97 +			val cls = Meson.make_cnf skoths nnfth
    5.98 +		    in  clause_cache := 
    5.99 +		     	  Symtab.update ((name, (th,cls)), !clause_cache);
   5.100 +			skolemlist nths thy'
   5.101 +		    end
   5.102 +		else skolemlist nths thy
   5.103 +            end
   5.104  	| SOME _ => skolemlist nths thy) (*FIXME: check for duplicate names?*)
   5.105 -      handle THM _ => skolemlist nths thy;
   5.106  
   5.107  (*Exported function to convert Isabelle theorems into axiom clauses*) 
   5.108  fun cnf_axiom (name,th) =
     6.1 --- a/src/HOL/ex/Primrec.thy	Tue Jun 28 15:27:45 2005 +0200
     6.2 +++ b/src/HOL/ex/Primrec.thy	Tue Jun 28 15:28:04 2005 +0200
     6.3 @@ -286,8 +286,14 @@
     6.4    ==> \<exists>k. \<forall>l. COMP g fs  l < ack(k, list_add l)"
     6.5    apply (unfold COMP_def)
     6.6    apply (frule Int_lower1 [THEN lists_mono, THEN subsetD])
     6.7 -  apply (drule COMP_map_aux)
     6.8 -  apply (meson ack_less_mono2 ack_nest_bound less_trans)
     6.9 +    --{*Now, if meson tolerated map, we could finish with
    6.10 +  @{text "(drule COMP_map_aux, meson ack_less_mono2 ack_nest_bound less_trans).*}
    6.11 +  apply (erule COMP_map_aux [THEN exE])
    6.12 +  apply (rule exI)
    6.13 +  apply (rule allI)
    6.14 +  apply (drule spec)+
    6.15 +  apply (erule less_trans)
    6.16 +  apply (blast intro: ack_less_mono2 ack_nest_bound less_trans)
    6.17    done
    6.18  
    6.19