meson now checks that problems are first-order
authorpaulson
Thu Mar 17 15:12:03 2005 +0100 (2005-03-17 ago)
changeset 15613ab90e95ae02e
parent 15612 431b281078b3
child 15614 b098158a3f39
meson now checks that problems are first-order
src/HOL/MicroJava/BV/Product.thy
src/HOL/Tools/meson.ML
     1.1 --- a/src/HOL/MicroJava/BV/Product.thy	Thu Mar 17 12:19:50 2005 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/Product.thy	Thu Mar 17 15:12:03 2005 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4    "order(Product.le rA rB) = (order rA & order rB)"
     1.5  apply (unfold order_def)
     1.6  apply simp
     1.7 -apply meson
     1.8 +apply blast
     1.9  done 
    1.10  
    1.11  
     2.1 --- a/src/HOL/Tools/meson.ML	Thu Mar 17 12:19:50 2005 +0100
     2.2 +++ b/src/HOL/Tools/meson.ML	Thu Mar 17 15:12:03 2005 +0100
     2.3 @@ -202,11 +202,28 @@
     2.4    | has_bool (Type(_, Ts)) = exists has_bool Ts
     2.5    | has_bool _ = false;
     2.6    
     2.7 +(*Is the string the name of a connective? It doesn't matter if this list is
     2.8 +  incomplete, since when actually called, the only connectives likely to
     2.9 +  remain are & | Not.*)  
    2.10 +fun is_conn c = c mem_string
    2.11 +    ["Trueprop", "op &", "op |", "op -->", "op =", "Not", 
    2.12 +     "All", "Ex", "Ball", "Bex"];
    2.13 +
    2.14 +(*True if the term contains a function where the type of any argument contains
    2.15 +  bool.*)
    2.16 +val has_bool_arg_const = 
    2.17 +    exists_Const
    2.18 +      (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
    2.19 +  
    2.20  (*Raises an exception if any Vars in the theorem mention type bool. That would mean
    2.21 -  they are higher-order, and in addition, they could cause make_horn to loop!*)
    2.22 +  they are higher-order, and in addition, they could cause make_horn to loop!
    2.23 +  Functions taking Boolean arguments are also rejected.*)
    2.24  fun check_no_bool th =
    2.25 -  if exists (has_bool o fastype_of) (term_vars (#prop (rep_thm th)))
    2.26 -  then raise THM ("check_no_bool", 0, [th]) else th;
    2.27 +  let val {prop,...} = rep_thm th
    2.28 +  in if exists (has_bool o fastype_of) (term_vars prop) orelse
    2.29 +        has_bool_arg_const prop
    2.30 +  then raise THM ("check_no_bool", 0, [th]) else th
    2.31 +  end;
    2.32  
    2.33  (*Create a meta-level Horn clause*)
    2.34  fun make_horn crules th = make_horn crules (tryres(th,crules))
    2.35 @@ -271,10 +288,6 @@
    2.36      (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
    2.37      TRYALL eq_assume_tac;
    2.38  
    2.39 -
    2.40 -
    2.41 -
    2.42 -
    2.43  (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
    2.44  fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
    2.45