--- a/NEWS Thu Aug 29 16:15:11 2002 +0200
+++ b/NEWS Fri Aug 30 16:42:45 2002 +0200
@@ -33,6 +33,10 @@
"foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from
the goal statement); "foo" still refers to all facts collectively;
+* Provers: the function blast.overloaded has been removed: all constants
+are regarded as potentially overloaded, which improves robustness in exchange
+for slight decrease in efficiency;
+
* Isar: preview of problems to finish 'show' now produce an error
rather than just a warning (in interactive mode);
--- a/doc-src/TutorialI/Rules/Basic.thy Thu Aug 29 16:15:11 2002 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy Fri Aug 30 16:42:45 2002 +0200
@@ -40,7 +40,7 @@
by eliminates uses of assumption and done
*}
-lemma imp_uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
+lemma imp_uncurry': "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
apply (rule impI)
apply (erule conjE)
apply (drule mp)
@@ -353,7 +353,7 @@
apply (simp add: Least_def LeastM_def)
by (blast intro: some_equality order_antisym);
-theorem axiom_of_choice: "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
+theorem axiom_of_choice': "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
apply (rule exI [of _ "\<lambda>x. SOME y. P x y"])
by (blast intro: someI);
--- a/doc-src/TutorialI/Rules/Forward.thy Thu Aug 29 16:15:11 2002 +0200
+++ b/doc-src/TutorialI/Rules/Forward.thy Fri Aug 30 16:42:45 2002 +0200
@@ -71,20 +71,21 @@
\rulename{sym}
*};
-lemmas gcd_mult = gcd_mult_1 [THEN sym];
+lemmas gcd_mult0 = gcd_mult_1 [THEN sym];
+ (*not quite right: we need ?k but this gives k*)
-lemmas gcd_mult = gcd_mult_distrib2 [of k 1, simplified, THEN sym];
+lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym];
(*better in one step!*)
text {*
-more legible
+more legible, and variables properly generalized
*};
lemma gcd_mult [simp]: "gcd(k, k*n) = k"
by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
-lemmas gcd_self = gcd_mult [of k 1, simplified];
+lemmas gcd_self0 = gcd_mult [of k 1, simplified];
text {*
@@ -99,7 +100,7 @@
text {*
-again: more legible
+again: more legible, and variables properly generalized
*};
lemma gcd_self [simp]: "gcd(k,k) = k"
--- a/src/FOL/FOL.thy Thu Aug 29 16:15:11 2002 +0200
+++ b/src/FOL/FOL.thy Fri Aug 30 16:42:45 2002 +0200
@@ -28,7 +28,14 @@
use "blastdata.ML"
setup Blast.setup
-use "FOL_lemmas2.ML"
+
+
+lemma ex1_functional: "[| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c"
+by blast
+
+ML {*
+val ex1_functional = thm "ex1_functional";
+*}
use "simpdata.ML"
setup simpsetup
--- a/src/FOL/FOL_lemmas2.ML Thu Aug 29 16:15:11 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-
-Goal "[| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c";
- by (Blast_tac 1);
-qed "ex1_functional";
--- a/src/FOL/IsaMakefile Thu Aug 29 16:15:11 2002 +0200
+++ b/src/FOL/IsaMakefile Fri Aug 30 16:42:45 2002 +0200
@@ -32,7 +32,7 @@
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \
$(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/quantifier1.ML\
- FOL.ML FOL.thy FOL_lemmas1.ML FOL_lemmas2.ML IFOL.ML IFOL.thy \
+ FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML IFOL.thy \
IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML document/root.tex \
fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
@$(ISATOOL) usedir -b $(OUT)/Pure FOL
--- a/src/HOL/Algebra/abstract/Ring.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/Algebra/abstract/Ring.ML Fri Aug 30 16:42:45 2002 +0200
@@ -4,8 +4,6 @@
Author: Clemens Ballarin, started 9 December 1996
*)
-Blast.overloaded ("Divides.op dvd", domain_type);
-
val a_assoc = thm "plus_ac0.assoc";
val l_zero = thm "plus_ac0.zero";
val a_comm = thm "plus_ac0.commute";
--- a/src/HOL/Auth/ROOT.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/Auth/ROOT.ML Fri Aug 30 16:42:45 2002 +0200
@@ -7,6 +7,7 @@
*)
goals_limit := 1;
+set timing;
(*Shared-key protocols*)
time_use_thy "NS_Shared";
--- a/src/HOL/Bali/ROOT.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/Bali/ROOT.ML Fri Aug 30 16:42:45 2002 +0200
@@ -1,4 +1,4 @@
-
+set timing;
update_thy "AxExample";
update_thy "AxSound";
update_thy "AxCompl";
--- a/src/HOL/HOL.thy Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/HOL.thy Fri Aug 30 16:42:45 2002 +0200
@@ -603,13 +603,6 @@
"op <=" :: "['a::ord, 'a] => bool" ("op \<le>")
"op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
-(*Tell blast about overloading of < and <= to reduce the risk of
- its applying a rule for the wrong type*)
-ML {*
-Blast.overloaded ("op <" , domain_type);
-Blast.overloaded ("op <=", domain_type);
-*}
-
subsubsection {* Monotonicity *}
--- a/src/HOL/Lambda/Commutation.thy Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/Lambda/Commutation.thy Fri Aug 30 16:42:45 2002 +0200
@@ -225,7 +225,8 @@
with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
by (blast dest:lc)
from yb u y'c show ?thesis
- by(blast intro:rtrancl_trans
+ by(blast del: rtrancl_refl
+ intro:rtrancl_trans
dest:IH[OF xy[symmetric]] IH[OF xy'[symmetric]])
qed
qed
--- a/src/HOL/Lambda/ROOT.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/Lambda/ROOT.ML Fri Aug 30 16:42:45 2002 +0200
@@ -6,6 +6,7 @@
Syntax.ambiguity_level := 100;
+set timing;
time_use_thy "Eta";
no_document time_use_thy "Accessible_Part";
time_use_thy "Type";
--- a/src/HOL/Real/RealDef.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/Real/RealDef.ML Fri Aug 30 16:42:45 2002 +0200
@@ -5,9 +5,6 @@
Description : The reals
*)
-(*Ensures that Blast_tac can cope with real*)
-Blast.overloaded ("RealDef.real", domain_type);
-
(*** Proving that realrel is an equivalence relation ***)
Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
--- a/src/HOL/Relation.thy Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/Relation.thy Fri Aug 30 16:42:45 2002 +0200
@@ -300,8 +300,6 @@
subsection {* Image of a set under a relation *}
-ML {* overload_1st_set "Relation.Image" *}
-
lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
by (simp add: Image_def)
--- a/src/HOL/Set.thy Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/Set.thy Fri Aug 30 16:42:45 2002 +0200
@@ -343,22 +343,6 @@
"'a set"}.
*}
-ML {*
- fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type);
-*}
-
-ML "
- (* While (:) is not, its type must be kept
- for overloading of = to work. *)
- Blast.overloaded (\"op :\", domain_type);
-
- overload_1st_set \"Ball\"; (*need UNION, INTER also?*)
- overload_1st_set \"Bex\";
-
- (*Image: retain the type of the set being expressed*)
- Blast.overloaded (\"image\", domain_type);
-"
-
lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
-- {* Rule in Modus Ponens style. *}
by (unfold subset_def) blast
--- a/src/HOL/UNITY/Constrains.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/UNITY/Constrains.ML Fri Aug 30 16:42:45 2002 +0200
@@ -45,9 +45,6 @@
(*** Co ***)
-(*Needed because its operands are sets*)
-overload_1st_set "Constrains.Constrains";
-
(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
bind_thm ("constrains_reachable_Int",
subset_refl RS
--- a/src/HOL/UNITY/Extend.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/UNITY/Extend.ML Fri Aug 30 16:42:45 2002 +0200
@@ -750,7 +750,9 @@
qed "ok_extend_imp_ok_project";
Goal "(extend h F ok extend h G) = (F ok G)";
-by (auto_tac (claset(), simpset() addsimps [ok_def]));
+by (asm_full_simp_tac (simpset() addsimps [ok_def]) 1);
+by Safe_tac;
+by (REPEAT (Force_tac 1));
qed "ok_extend_iff";
Goalw [OK_def] "OK I (%i. extend h (F i)) = (OK I F)";
--- a/src/HOL/UNITY/Rename.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/UNITY/Rename.ML Fri Aug 30 16:42:45 2002 +0200
@@ -69,8 +69,9 @@
by (rtac bijI 1);
by (rtac (export inj_extend_act) 1);
by (auto_tac (claset(), simpset() addsimps [bij_extend_act_eq_project_act]));
-by (blast_tac (claset() addIs [bij_imp_bij_inv, surjI,
- export extend_act_inverse]) 1);
+by (rtac surjI 1);
+by (rtac (export extend_act_inverse) 1);
+by (blast_tac (claset() addIs [bij_imp_bij_inv, good_map_bij]) 1);
qed "bij_extend_act";
Goal "bij h ==> bij (project_act (%(x,u::'c). h x))";
--- a/src/HOL/UNITY/SubstAx.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Fri Aug 30 16:42:45 2002 +0200
@@ -6,9 +6,6 @@
LeadsTo relation, restricted to the set of reachable states.
*)
-overload_1st_set "SubstAx.op LeadsTo";
-
-
(*Resembles the previous definition of LeadsTo*)
Goalw [LeadsTo_def]
"A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}";
--- a/src/HOL/UNITY/UNITY.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/UNITY/UNITY.ML Fri Aug 30 16:42:45 2002 +0200
@@ -131,12 +131,6 @@
(*** co ***)
-(*These operators are not overloaded, but their operands are sets, and
- ultimately there's a risk of reaching equality, which IS overloaded*)
-overload_1st_set "UNITY.constrains";
-overload_1st_set "UNITY.stable";
-overload_1st_set "UNITY.unless";
-
val prems = Goalw [constrains_def]
"(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \
\ ==> F : A co A'";
--- a/src/HOL/UNITY/WFair.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/UNITY/WFair.ML Fri Aug 30 16:42:45 2002 +0200
@@ -9,10 +9,6 @@
*)
-overload_1st_set "WFair.transient";
-overload_1st_set "WFair.ensures";
-overload_1st_set "WFair.op leadsTo";
-
(*** transient ***)
Goalw [stable_def, constrains_def, transient_def]
--- a/src/HOL/blastdata.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/blastdata.ML Fri Aug 30 16:42:45 2002 +0200
@@ -28,7 +28,6 @@
end;
structure Blast = BlastFun(Blast_Data);
-Blast.overloaded ("op =", domain_type); (*overloading of equality as iff*)
val Blast_tac = Blast.Blast_tac
and blast_tac = Blast.blast_tac;
--- a/src/Provers/blast.ML Thu Aug 29 16:15:11 2002 +0200
+++ b/src/Provers/blast.ML Fri Aug 30 16:42:45 2002 +0200
@@ -27,12 +27,6 @@
such as transitivity are treated specially to prevent this. Sometimes
the formulae get into the wrong order (see WRONG below).
- With overloading:
- Calls to Blast.overloaded (see HOL/Set.ML for examples) are needed
- to tell Blast_tac when to retain some type information. Make sure
- you know the constant's internal name, which might be "op <=" or
- "Relation.op ^^".
-
With substition for equalities (hyp_subst_tac):
When substitution affects a haz formula or literal, it is moved
back to the list of safe formulae.
@@ -88,8 +82,6 @@
val depth_tac : claset -> int -> int -> tactic
val blast_tac : claset -> int -> tactic
val Blast_tac : int -> tactic
- val overloaded : string * (Term.typ -> Term.typ) -> unit
- val get_overloads : unit -> (string * (Term.typ -> Term.typ)) list
val setup : (theory -> theory) list
(*debugging tools*)
val stats : bool ref
@@ -186,26 +178,21 @@
end
| Some v => v)
-local
-val overloads = ref ([]: (string * (Term.typ -> Term.typ)) list)
-in
+(*Monomorphic constants used in blast, plus binary propositional connectives.*)
+val standard_consts =
+ ["Not", "op &", "op |", "op -->", "op <->",
+ "*Goal*", "*False*", "==>", "all", "Trueprop"];
-fun overloaded arg = (overloads := arg :: (!overloads));
-
-fun get_overloads() = !overloads;
+val standard_const_table = Symtab.make (map (rpair()) standard_consts)
-(*Convert a possibly overloaded Term.Const to a Blast.Const or Blast.TConst,
- converting its type to a Blast.term in the latter case.*)
-fun fromConst alist (a,T) =
- case assoc_string (!overloads, a) of
- None => Const a (*not overloaded*)
- | Some f =>
- let val T' = f T
- handle Match => error
- ("Blast_tac: unexpected type for overloaded constant " ^ a)
- in TConst(a, fromType alist T') end;
-
-end;
+(*Convert a Term.Const to a Blast.Const or Blast.TConst,
+ converting its type to a Blast.term in the latter case.
+ Const is used for a small number of built-in operators that are
+ known to be monomorphic, which promotes efficiency. *)
+fun fromConst alist (a,T) =
+ case Symtab.lookup(standard_const_table, a) of
+ None => TConst(a, fromType alist T)
+ | Some() => Const(a)
(*Tests whether 2 terms are alpha-convertible; chases instantiations*)