src/HOL/Tools/Meson/meson.ML
 changeset 47035 5248fae40f09 parent 47022 8eac39af4ec0 child 47953 a2c3706c4cb1
```     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 =
```