src/HOL/Tools/meson.ML
changeset 16588 8de758143786
parent 16563 a92f96951355
child 16801 4bb13fa6ae72
     1.1 --- a/src/HOL/Tools/meson.ML	Tue Jun 28 15:27:45 2005 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Tue Jun 28 15:28:04 2005 +0200
     1.3 @@ -138,19 +138,23 @@
     1.4  	then ths     (*tautology ignored*)
     1.5  	else if not (has_consts ["All","Ex","op &"] (prop_of th))  
     1.6  	then th::ths (*no work to do, terminate*)
     1.7 -	else (*conjunction?*)
     1.8 -	      cnf_aux seen (th RS conjunct1,
     1.9 -			    cnf_aux seen (th RS conjunct2, ths))
    1.10 -	handle THM _ => (*universal quantifier?*)
    1.11 -	      cnf_aux seen (freeze_spec th,  ths)
    1.12 -	handle THM _ => (*existential quantifier? Insert Skolem functions.*)
    1.13 +	else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
    1.14 +	    Const ("op &", _) => (*conjunction*)
    1.15 +		cnf_aux seen (th RS conjunct1,
    1.16 +			      cnf_aux seen (th RS conjunct2, ths))
    1.17 +	  | Const ("All", _) => (*universal quantifier*)
    1.18 +	        cnf_aux seen (freeze_spec th,  ths)
    1.19 +	  | Const ("Ex", _) => 
    1.20 +	      (*existential quantifier: Insert Skolem functions*)
    1.21  	      cnf_aux seen (tryres (th,skoths), ths)
    1.22 -	handle THM _ => (*disjunction?*)
    1.23 -	  let val tac =
    1.24 -	      (METAHYPS (resop (cnf_nil seen)) 1) THEN
    1.25 -	     (fn st' => st' |>  
    1.26 -		METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
    1.27 -	  in  Seq.list_of (tac (th RS disj_forward)) @ ths  end 
    1.28 +	  | Const ("op |", _) => (*disjunction*)
    1.29 +	      let val tac =
    1.30 +		  (METAHYPS (resop (cnf_nil seen)) 1) THEN
    1.31 +		   (fn st' => st' |>  
    1.32 +		      METAHYPS 
    1.33 +		        (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
    1.34 +	      in  Seq.list_of (tac (th RS disj_forward)) @ ths  end 
    1.35 +	  | _ => (*no work to do*) th::ths 
    1.36        and cnf_nil seen th = (cnf_aux seen (th,[]))
    1.37    in 
    1.38      name_ref := 19;  (*It's safe to reset this in a top-level call to cnf*)
    1.39 @@ -235,15 +239,16 @@
    1.40  val has_meta_conn = 
    1.41      exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "Goal"]);
    1.42    
    1.43 -(*Raises an exception if any Vars in the theorem mention type bool. That would mean
    1.44 -  they are higher-order, and in addition, they could cause make_horn to loop!
    1.45 -  Functions taking Boolean arguments are also rejected.*)
    1.46 -fun check_no_bool th =
    1.47 +(*Raises an exception if any Vars in the theorem mention type bool; they
    1.48 +  could cause make_horn to loop! Also rejects functions whose arguments are 
    1.49 +  Booleans or other functions.*)
    1.50 +fun check_is_fol th = 
    1.51    let val {prop,...} = rep_thm th
    1.52    in if exists (has_bool o fastype_of) (term_vars prop)  orelse
    1.53 +        not (Term.is_first_order ["all","All","Ex"] prop) orelse
    1.54          has_bool_arg_const prop  orelse  
    1.55          has_meta_conn prop
    1.56 -  then raise THM ("check_no_bool", 0, [th]) else th
    1.57 +  then raise THM ("check_is_fol", 0, [th]) else th
    1.58    end;
    1.59  
    1.60  (*Create a meta-level Horn clause*)
    1.61 @@ -330,7 +335,7 @@
    1.62  val nnf_ss = HOL_basic_ss addsimps Ex1_def::Ball_def::Bex_def::simp_thms;
    1.63  
    1.64  fun make_nnf th = th |> simplify nnf_ss
    1.65 -                     |> check_no_bool |> make_nnf1
    1.66 +                     |> check_is_fol |> make_nnf1
    1.67  
    1.68  (*Pull existential quantifiers to front. This accomplishes Skolemization for
    1.69    clauses that arise from a subgoal.*)
    1.70 @@ -371,12 +376,14 @@
    1.71      cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
    1.72      REPEAT o (etac exE);
    1.73  
    1.74 -(*Shell of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
    1.75 -fun MESON cltac = SELECT_GOAL
    1.76 - (EVERY1 [rtac ccontr,
    1.77 -          METAHYPS (fn negs =>
    1.78 -                    EVERY1 [skolemize_prems_tac negs,
    1.79 -                            METAHYPS (cltac o make_clauses)])]);
    1.80 +(*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
    1.81 +fun MESON cltac i st = 
    1.82 +  SELECT_GOAL
    1.83 +   (EVERY1 [rtac ccontr,
    1.84 +	    METAHYPS (fn negs =>
    1.85 +		      EVERY1 [skolemize_prems_tac negs,
    1.86 +			      METAHYPS (cltac o make_clauses)])]) i st
    1.87 +  handle THM _ => no_tac st;	(*probably from check_is_fol*)		      
    1.88  
    1.89  (** Best-first search versions **)
    1.90  
    1.91 @@ -446,7 +453,7 @@
    1.92  
    1.93  (*Converting one clause*)
    1.94  fun make_meta_clause th = 
    1.95 -	negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th));
    1.96 +    negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th));
    1.97  
    1.98  fun make_meta_clauses ths =
    1.99      name_thms "MClause#"