# HG changeset patch # User paulson # Date 1030718565 -7200 # Node ID 5a176b8dda84308cef08ac7094055da3e7c7d407 # Parent f1522b892a4c9fe3ccdd65718dfb412c3461ece0 removal of blast.overloaded diff -r f1522b892a4c -r 5a176b8dda84 NEWS --- 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); diff -r f1522b892a4c -r 5a176b8dda84 doc-src/TutorialI/Rules/Basic.thy --- 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 \ Q \ R \ P \ Q \ R" +lemma imp_uncurry': "P \ Q \ R \ P \ Q \ 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: "(\x. \y. P x y) \ \f. \x. P x (f x)" +theorem axiom_of_choice': "(\x. \y. P x y) \ \f. \x. P x (f x)" apply (rule exI [of _ "\x. SOME y. P x y"]) by (blast intro: someI); diff -r f1522b892a4c -r 5a176b8dda84 doc-src/TutorialI/Rules/Forward.thy --- 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" diff -r f1522b892a4c -r 5a176b8dda84 src/FOL/FOL.thy --- 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 diff -r f1522b892a4c -r 5a176b8dda84 src/FOL/FOL_lemmas2.ML --- 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"; diff -r f1522b892a4c -r 5a176b8dda84 src/FOL/IsaMakefile --- 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 diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/Algebra/abstract/Ring.ML --- 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"; diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/Auth/ROOT.ML --- 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"; diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/Bali/ROOT.ML --- 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"; diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/HOL.thy --- 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 \") "op <=" :: "['a::ord, 'a] => bool" ("(_/ \ _)" [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 *} diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/Lambda/Commutation.thy --- 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) \ R\<^sup>*" "(y', u) \ 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 diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/Lambda/ROOT.ML --- 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"; diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/Real/RealDef.ML --- 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 |] \ diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/Relation.thy --- 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) diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/Set.thy --- 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 \ B ==> c \ A ==> c \ B" -- {* Rule in Modus Ponens style. *} by (unfold subset_def) blast diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/UNITY/Constrains.ML --- 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 diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/UNITY/Extend.ML --- 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)"; diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/UNITY/Rename.ML --- 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))"; diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/UNITY/SubstAx.ML --- 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)}"; diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/UNITY/UNITY.ML --- 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'"; diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/UNITY/WFair.ML --- 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] diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/blastdata.ML --- 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; diff -r f1522b892a4c -r 5a176b8dda84 src/Provers/blast.ML --- 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*)