162 | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS |
162 | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS |
163 |
163 |
164 (* ('a * bool option) list -> bool *) |
164 (* ('a * bool option) list -> bool *) |
165 fun none_true asgns = forall (not_equal (SOME true) o snd) asgns |
165 fun none_true asgns = forall (not_equal (SOME true) o snd) asgns |
166 |
166 |
167 val weaselly_sorts = |
167 val syntactic_sorts = |
168 [@{sort default}, @{sort zero}, @{sort one}, @{sort plus}, @{sort minus}, |
168 @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @ |
169 @{sort uminus}, @{sort times}, @{sort inverse}, @{sort abs}, @{sort sgn}, |
169 @{sort number} |
170 @{sort ord}, @{sort eq}, @{sort number}] |
170 (* typ -> bool *) |
171 (* theory -> typ -> bool *) |
171 fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) = |
172 fun is_tfree_with_weaselly_sort thy (TFree (_, S)) = |
172 subset (op =) (S, syntactic_sorts) |
173 exists (curry (Sign.subsort thy) S) weaselly_sorts |
173 | has_tfree_syntactic_sort _ = false |
174 | is_tfree_with_weaselly_sort _ _ = false |
174 (* term -> bool *) |
175 (* theory term -> bool *) |
175 val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort) |
176 val has_weaselly_sorts = |
|
177 exists_type o exists_subtype o is_tfree_with_weaselly_sort |
|
178 |
176 |
179 (* (unit -> string) -> Pretty.T *) |
177 (* (unit -> string) -> Pretty.T *) |
180 fun plazy f = Pretty.blk (0, pstrs (f ())) |
178 fun plazy f = Pretty.blk (0, pstrs (f ())) |
181 |
179 |
182 (* Time.time -> Proof.state -> params -> bool -> term -> string * Proof.state *) |
180 (* Time.time -> Proof.state -> params -> bool -> term -> string * Proof.state *) |
573 print ("Refutation by \"auto\": The above " ^ word_model ^ |
571 print ("Refutation by \"auto\": The above " ^ word_model ^ |
574 " is spurious.") |
572 " is spurious.") |
575 | NONE => print "No confirmation by \"auto\".") |
573 | NONE => print "No confirmation by \"auto\".") |
576 else |
574 else |
577 (); |
575 (); |
578 if has_weaselly_sorts thy orig_t then |
576 if has_syntactic_sorts orig_t then |
579 print "Hint: Maybe you forgot a type constraint?" |
577 print "Hint: Maybe you forgot a type constraint?" |
580 else |
578 else |
581 (); |
579 (); |
582 if not would_be_genuine then |
580 if not would_be_genuine then |
583 if no_poly_user_axioms then |
581 if no_poly_user_axioms then |