tuning
authorblanchet
Tue Mar 20 00:44:30 2012 +0100 (2012-03-20)
changeset 470355248fae40f09
parent 47034 77da780ddd6b
child 47036 fc958d7138be
tuning
src/HOL/Tools/Meson/meson.ML
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Mar 20 00:44:30 2012 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Mar 20 00:44:30 2012 +0100
     1.3 @@ -349,10 +349,6 @@
     1.4    (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
     1.5  fun resop nf [prem] = resolve_tac (nf prem) 1;
     1.6  
     1.7 -(* Any need to extend this list with "HOL.type_class", "HOL.eq_class",
     1.8 -   and "Pure.term"? *)
     1.9 -val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
    1.10 -
    1.11  fun apply_skolem_theorem (th, rls) =
    1.12    let
    1.13      fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
    1.14 @@ -423,39 +419,6 @@
    1.15      make_goal (tryres(th, clause_rules))
    1.16    handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]);
    1.17  
    1.18 -(*Sort clauses by number of literals*)
    1.19 -fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
    1.20 -
    1.21 -fun sort_clauses ths = sort (make_ord fewerlits) ths;
    1.22 -
    1.23 -fun has_bool @{typ bool} = true
    1.24 -  | has_bool (Type (_, Ts)) = exists has_bool Ts
    1.25 -  | has_bool _ = false
    1.26 -
    1.27 -fun has_fun (Type (@{type_name fun}, _)) = true
    1.28 -  | has_fun (Type (_, Ts)) = exists has_fun Ts
    1.29 -  | has_fun _ = false
    1.30 -
    1.31 -(*Is the string the name of a connective? Really only | and Not can remain,
    1.32 -  since this code expects to be called on a clause form.*)
    1.33 -val is_conn = member (op =)
    1.34 -    [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
    1.35 -     @{const_name HOL.implies}, @{const_name Not},
    1.36 -     @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
    1.37 -
    1.38 -(*True if the term contains a function--not a logical connective--where the type
    1.39 -  of any argument contains bool.*)
    1.40 -val has_bool_arg_const =
    1.41 -    exists_Const
    1.42 -      (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
    1.43 -
    1.44 -(*A higher-order instance of a first-order constant? Example is the definition of
    1.45 -  one, 1, at a function type in theory Function_Algebras.*)
    1.46 -fun higher_inst_const thy (c,T) =
    1.47 -  case binder_types T of
    1.48 -      [] => false (*not a function type, OK*)
    1.49 -    | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
    1.50 -
    1.51  fun rigid t = not (is_Var (head_of t));
    1.52  
    1.53  fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t
    1.54 @@ -640,10 +603,13 @@
    1.55        val (cnfs, ctxt) = make_cnf [] th ctxt ctxt0
    1.56    in Variable.export ctxt ctxt0 cnfs @ cls end;
    1.57  
    1.58 +(*Sort clauses by number of literals*)
    1.59 +fun fewerlits (th1, th2) = nliterals (prop_of th1) < nliterals (prop_of th2)
    1.60 +
    1.61  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
    1.62    The resulting clauses are HOL disjunctions.*)
    1.63  fun make_clauses_unsorted ctxt ths = fold_rev (add_clauses ctxt) ths [];
    1.64 -val make_clauses = sort_clauses oo make_clauses_unsorted;
    1.65 +val make_clauses = sort (make_ord fewerlits) oo make_clauses_unsorted;
    1.66  
    1.67  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
    1.68  fun make_horns ths =