proper signature constraint;
authorwenzelm
Fri Sep 21 22:51:08 2007 +0200 (2007-09-21)
changeset 246694579eac2c997
parent 24668 4058b7b0925c
child 24670 9aae962b1d56
proper signature constraint;
minor tuning;
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Sep 20 20:58:40 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Sep 21 22:51:08 2007 +0200
     1.3 @@ -7,23 +7,25 @@
     1.4  
     1.5  signature RES_AXIOMS =
     1.6  sig
     1.7 -  val cnf_axiom : string * thm -> thm list
     1.8 -  val cnf_name : string -> thm list
     1.9 -  val meta_cnf_axiom : thm -> thm list
    1.10 -  val pairname : thm -> string * thm
    1.11 -  val skolem_thm : thm -> thm list
    1.12 -  val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list
    1.13 -  val meson_method_setup : theory -> theory
    1.14 -  val setup : theory -> theory
    1.15 -  val clause_cache_setup : theory -> theory
    1.16 +  val cnf_axiom: thm -> thm list
    1.17 +  val meta_cnf_axiom: thm -> thm list
    1.18 +  val pairname: thm -> string * thm
    1.19 +  val skolem_thm: thm -> thm list
    1.20 +  val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
    1.21 +  val cnf_rules_of_ths: thm list -> thm list
    1.22 +  val neg_clausify: thm list -> thm list
    1.23 +  val expand_defs_tac: thm -> tactic
    1.24    val assume_abstract_list: string -> thm list -> thm list
    1.25    val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
    1.26    val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)
    1.27    val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
    1.28    val atpset_rules_of: Proof.context -> (string * thm) list
    1.29 +  val meson_method_setup: theory -> theory
    1.30 +  val clause_cache_setup: theory -> theory
    1.31 +  val setup: theory -> theory
    1.32  end;
    1.33  
    1.34 -structure ResAxioms =
    1.35 +structure ResAxioms: RES_AXIOMS =
    1.36  struct
    1.37  
    1.38  (*For running the comparison between combinators and abstractions.
    1.39 @@ -49,11 +51,11 @@
    1.40    let val (_,ct) = Thm.dest_abs NONE (Thm.rhs_of th)
    1.41        val t = Logic.legacy_varify (term_of ct)
    1.42    in  Net.insert_term Thm.eq_thm (t, th) net end;
    1.43 -  
    1.44 -val abstraction_cache = ref 
    1.45 -      (seed (thm"ATP_Linkup.I_simp") 
    1.46 -       (seed (thm"ATP_Linkup.B_simp") 
    1.47 -	(seed (thm"ATP_Linkup.K_simp") Net.empty)));
    1.48 +
    1.49 +val abstraction_cache = ref
    1.50 +      (seed (thm"ATP_Linkup.I_simp")
    1.51 +       (seed (thm"ATP_Linkup.B_simp")
    1.52 +        (seed (thm"ATP_Linkup.K_simp") Net.empty)));
    1.53  
    1.54  
    1.55  (**** Transformation of Elimination Rules into First-Order Formulas****)
    1.56 @@ -66,9 +68,9 @@
    1.57    conclusion variable to False.*)
    1.58  fun transform_elim th =
    1.59    case concl_of th of    (*conclusion variable*)
    1.60 -       Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) => 
    1.61 +       Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
    1.62             Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th
    1.63 -    | v as Var(_, Type("prop",[])) => 
    1.64 +    | v as Var(_, Type("prop",[])) =>
    1.65             Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th
    1.66      | _ => th;
    1.67  
    1.68 @@ -167,11 +169,11 @@
    1.69  (*Removes the lambdas from an equation of the form t = (%x. u).  A non-negative n,
    1.70    serves as an upper bound on how many to remove.*)
    1.71  fun strip_lambdas 0 th = th
    1.72 -  | strip_lambdas n th = 
    1.73 +  | strip_lambdas n th =
    1.74        case prop_of th of
    1.75 -	  _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
    1.76 -	      strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
    1.77 -	| _ => th;
    1.78 +          _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
    1.79 +              strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
    1.80 +        | _ => th;
    1.81  
    1.82  (*Convert meta- to object-equality. Fails for theorems like split_comp_eq,
    1.83    where some types have the empty sort.*)
    1.84 @@ -202,12 +204,9 @@
    1.85      Context.joinable (theory_of_thm th1, theory_of_thm th2)  andalso
    1.86      rhs_of th1 aconv rhs_of th2;
    1.87  
    1.88 -fun lambda_free (Abs _) = false
    1.89 -  | lambda_free (t $ u) = lambda_free t andalso lambda_free u
    1.90 -  | lambda_free _ = true;
    1.91 +val lambda_free = not o Term.has_abs;
    1.92  
    1.93 -fun monomorphic t =
    1.94 -  Term.fold_types (Term.fold_atyps (fn TVar _ => K false | _ => I)) t true;
    1.95 +val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
    1.96  
    1.97  fun dest_abs_list ct =
    1.98    let val (cv,ct') = Thm.dest_abs NONE ct
    1.99 @@ -215,9 +214,6 @@
   1.100    in (cv::cvs, cu) end
   1.101    handle CTERM _ => ([],ct);
   1.102  
   1.103 -fun lambda_list [] u = u
   1.104 -  | lambda_list (v::vs) u = lambda v (lambda_list vs u);
   1.105 -
   1.106  fun abstract_rule_list [] [] th = th
   1.107    | abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th)
   1.108    | abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]);
   1.109 @@ -228,12 +224,12 @@
   1.110  (*Does an existing abstraction definition have an RHS that matches the one we need now?
   1.111    thy is the current theory, which must extend that of theorem th.*)
   1.112  fun match_rhs thy t th =
   1.113 -  let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^ 
   1.114 +  let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^
   1.115                                     " against\n" ^ string_of_thm th);
   1.116        val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
   1.117        val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
   1.118 -      val ct_pairs = if subthy (theory_of_thm th, thy) andalso 
   1.119 -                        forall lambda_free (map #2 term_insts) 
   1.120 +      val ct_pairs = if subthy (theory_of_thm th, thy) andalso
   1.121 +                        forall lambda_free (map #2 term_insts)
   1.122                       then map (pairself (cterm_of thy)) term_insts
   1.123                       else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*)
   1.124        fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
   1.125 @@ -259,7 +255,7 @@
   1.126                  val _ = Output.debug (fn()=>"Returned " ^ string_of_thm u'_th);
   1.127                  val cu' = Thm.rhs_of u'_th
   1.128                  val u' = term_of cu'
   1.129 -                val abs_v_u = lambda_list (map term_of cvs) u'
   1.130 +                val abs_v_u = fold_rev (lambda o term_of) cvs u'
   1.131                  (*get the formal parameters: ALL variables free in the term*)
   1.132                  val args = term_frees abs_v_u
   1.133                  val _ = Output.debug (fn()=>Int.toString (length args) ^ " arguments");
   1.134 @@ -268,9 +264,9 @@
   1.135                  val _ = Output.debug (fn()=>"Looking up " ^ string_of_cterm cu');
   1.136                  val thy = theory_of_thm u'_th
   1.137                  val (ax,ax',thy) =
   1.138 -                 case List.mapPartial (match_rhs thy abs_v_u) 
   1.139 +                 case List.mapPartial (match_rhs thy abs_v_u)
   1.140                           (Net.match_term (!abstraction_cache) u') of
   1.141 -                     (ax,ax')::_ => 
   1.142 +                     (ax,ax')::_ =>
   1.143                         (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
   1.144                          (ax,ax',thy))
   1.145                     | [] =>
   1.146 @@ -291,7 +287,7 @@
   1.147                            val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
   1.148                            val _ = Output.debug (fn()=> "Declaring: " ^ string_of_thm ax ^ "\n" ^
   1.149                                                         "Instance: " ^ string_of_thm ax');
   1.150 -                          val _ = abstraction_cache := Net.insert_term eq_absdef 
   1.151 +                          val _ = abstraction_cache := Net.insert_term eq_absdef
   1.152                                              ((Logic.varify u'), ax) (!abstraction_cache)
   1.153                              handle Net.INSERT =>
   1.154                                raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
   1.155 @@ -332,7 +328,7 @@
   1.156                  val cu' = Thm.rhs_of u'_th
   1.157                  val u' = term_of cu'
   1.158                  (*Could use Thm.cabs instead of lambda to work at level of cterms*)
   1.159 -                val abs_v_u = lambda_list (map term_of cvs) (term_of cu')
   1.160 +                val abs_v_u = fold_rev (lambda o term_of) cvs (term_of cu')
   1.161                  (*get the formal parameters: free variables not present in the defs
   1.162                    (to avoid taking abstraction function names as parameters) *)
   1.163                  val args = filter (valid_name defs) (term_frees abs_v_u)
   1.164 @@ -340,9 +336,9 @@
   1.165                        (*Forms a lambda-abstraction over the formal parameters*)
   1.166                  val rhs = term_of crhs
   1.167                  val (ax,ax') =
   1.168 -                 case List.mapPartial (match_rhs thy abs_v_u) 
   1.169 +                 case List.mapPartial (match_rhs thy abs_v_u)
   1.170                          (Net.match_term (!abstraction_cache) u') of
   1.171 -                     (ax,ax')::_ => 
   1.172 +                     (ax,ax')::_ =>
   1.173                         (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
   1.174                          (ax,ax'))
   1.175                     | [] =>
   1.176 @@ -416,7 +412,7 @@
   1.177  fun skolem_of_nnf s th =
   1.178    map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
   1.179  
   1.180 -fun assert_lambda_free ths msg = 
   1.181 +fun assert_lambda_free ths msg =
   1.182    case filter (not o lambda_free o prop_of) ths of
   1.183        [] => ()
   1.184      | ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths'));
   1.185 @@ -451,7 +447,7 @@
   1.186  fun flatten_name s = space_implode "_X" (NameSpace.explode s);
   1.187  
   1.188  fun fake_name th =
   1.189 -  if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th) 
   1.190 +  if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th)
   1.191    else gensym "unknown_thm_";
   1.192  
   1.193  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   1.194 @@ -483,7 +479,7 @@
   1.195    fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2));
   1.196  );
   1.197  
   1.198 -(*The cache prevents repeated clausification of a theorem, and also repeated declaration of 
   1.199 +(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
   1.200    Skolem functions. The global one holds theorems proved prior to this point. Theory data
   1.201    holds the remaining ones.*)
   1.202  val global_clause_cache = ref (Thmtab.empty : (thm list) Thmtab.table);
   1.203 @@ -495,11 +491,11 @@
   1.204        NONE =>
   1.205          (case skolem thy (Thm.transfer thy th) of
   1.206               NONE => ([th],thy)
   1.207 -           | SOME (cls,thy') => 
   1.208 -                 (if null cls 
   1.209 +           | SOME (cls,thy') =>
   1.210 +                 (if null cls
   1.211                    then warning ("skolem_cache: empty clause set for " ^ string_of_thm th)
   1.212                    else ();
   1.213 -                  change clause_cache (Thmtab.update (th, cls)); 
   1.214 +                  change clause_cache (Thmtab.update (th, cls));
   1.215                    (cls,thy')))
   1.216      | SOME cls => (cls,thy);
   1.217  
   1.218 @@ -510,16 +506,16 @@
   1.219        val in_cache = if cache = global_clause_cache then NONE else Thmtab.lookup (!cache) th
   1.220    in
   1.221       case in_cache of
   1.222 -       NONE => 
   1.223 -	 (case Thmtab.lookup (!global_clause_cache) th of
   1.224 -	   NONE => 
   1.225 -	     let val cls = map Goal.close_result (skolem_thm th)
   1.226 -	     in Output.debug (fn () => Int.toString (length cls) ^ " clauses inserted into cache: " ^ 
   1.227 -	                         (if PureThy.has_name_hint th then PureThy.get_name_hint th
   1.228 -	                          else string_of_thm th));
   1.229 -		change cache (Thmtab.update (th, cls)); cls 
   1.230 -	     end
   1.231 -	 | SOME cls => cls)
   1.232 +       NONE =>
   1.233 +         (case Thmtab.lookup (!global_clause_cache) th of
   1.234 +           NONE =>
   1.235 +             let val cls = map Goal.close_result (skolem_thm th)
   1.236 +             in Output.debug (fn () => Int.toString (length cls) ^ " clauses inserted into cache: " ^
   1.237 +                                 (if PureThy.has_name_hint th then PureThy.get_name_hint th
   1.238 +                                  else string_of_thm th));
   1.239 +                change cache (Thmtab.update (th, cls)); cls
   1.240 +             end
   1.241 +         | SOME cls => cls)
   1.242       | SOME cls => cls
   1.243    end;
   1.244  
   1.245 @@ -581,7 +577,7 @@
   1.246  (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
   1.247    lambda_free, but then the individual theory caches become much bigger.*)
   1.248  
   1.249 -fun clause_cache_setup thy = 
   1.250 +fun clause_cache_setup thy =
   1.251    fold (skolem_cache global_clause_cache) (map #2 (PureThy.all_thms_of thy)) thy;
   1.252  
   1.253  
   1.254 @@ -605,7 +601,7 @@
   1.255        val hyps = #hyps (crep_thm st)
   1.256        val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
   1.257        val defs = filter (is_absko o Thm.term_of) newhyps
   1.258 -      val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) 
   1.259 +      val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
   1.260                                        (map Thm.term_of hyps)
   1.261        val fixed = term_frees (concl_of st) @
   1.262                    foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps)
   1.263 @@ -652,19 +648,19 @@
   1.264    in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end
   1.265    handle Option => raise ERROR "unable to Skolemize subgoal";
   1.266  
   1.267 -(*Conversion of a subgoal to conjecture clauses. Each clause has  
   1.268 +(*Conversion of a subgoal to conjecture clauses. Each clause has
   1.269    leading !!-bound universal variables, to express generality. *)
   1.270 -val neg_clausify_tac = 
   1.271 -  neg_skolemize_tac THEN' 
   1.272 +val neg_clausify_tac =
   1.273 +  neg_skolemize_tac THEN'
   1.274    SUBGOAL
   1.275      (fn (prop,_) =>
   1.276       let val ts = Logic.strip_assums_hyp prop
   1.277 -     in EVERY1 
   1.278 -	 [METAHYPS
   1.279 -	    (fn hyps => 
   1.280 +     in EVERY1
   1.281 +         [METAHYPS
   1.282 +            (fn hyps =>
   1.283                (Method.insert_tac
   1.284                  (map forall_intr_vars (neg_clausify hyps)) 1)),
   1.285 -	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   1.286 +          REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   1.287       end);
   1.288  
   1.289  (** The Skolemization attribute **)
   1.290 @@ -685,9 +681,9 @@
   1.291     ("clausify", clausify, "conversion of theorem to clauses")];
   1.292  
   1.293  val setup_methods = Method.add_methods
   1.294 -  [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), 
   1.295 +  [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
   1.296      "conversion of goal to conjecture clauses")];
   1.297 -     
   1.298 +
   1.299  val setup = clause_cache_setup #> ThmCache.init #> setup_attrs #> setup_methods;
   1.300  
   1.301  end;