removal of blast.overloaded
authorpaulson
Fri Aug 30 16:42:45 2002 +0200 (2002-08-30)
changeset 135505a176b8dda84
parent 13549 f1522b892a4c
child 13551 b7f64ee8da84
removal of blast.overloaded
NEWS
doc-src/TutorialI/Rules/Basic.thy
doc-src/TutorialI/Rules/Forward.thy
src/FOL/FOL.thy
src/FOL/FOL_lemmas2.ML
src/FOL/IsaMakefile
src/HOL/Algebra/abstract/Ring.ML
src/HOL/Auth/ROOT.ML
src/HOL/Bali/ROOT.ML
src/HOL/HOL.thy
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/ROOT.ML
src/HOL/Real/RealDef.ML
src/HOL/Relation.thy
src/HOL/Set.thy
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Rename.ML
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/WFair.ML
src/HOL/blastdata.ML
src/Provers/blast.ML
     1.1 --- a/NEWS	Thu Aug 29 16:15:11 2002 +0200
     1.2 +++ b/NEWS	Fri Aug 30 16:42:45 2002 +0200
     1.3 @@ -33,6 +33,10 @@
     1.4  "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from
     1.5  the goal statement); "foo" still refers to all facts collectively;
     1.6  
     1.7 +* Provers: the function blast.overloaded has been removed: all constants
     1.8 +are regarded as potentially overloaded, which improves robustness in exchange
     1.9 +for slight decrease in efficiency;
    1.10 +
    1.11  * Isar: preview of problems to finish 'show' now produce an error
    1.12  rather than just a warning (in interactive mode);
    1.13  
     2.1 --- a/doc-src/TutorialI/Rules/Basic.thy	Thu Aug 29 16:15:11 2002 +0200
     2.2 +++ b/doc-src/TutorialI/Rules/Basic.thy	Fri Aug 30 16:42:45 2002 +0200
     2.3 @@ -40,7 +40,7 @@
     2.4  by eliminates uses of assumption and done
     2.5  *}
     2.6  
     2.7 -lemma imp_uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
     2.8 +lemma imp_uncurry': "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
     2.9  apply (rule impI)
    2.10  apply (erule conjE)
    2.11  apply (drule mp)
    2.12 @@ -353,7 +353,7 @@
    2.13  apply (simp add: Least_def LeastM_def)
    2.14  by (blast intro: some_equality order_antisym);
    2.15  
    2.16 -theorem axiom_of_choice: "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
    2.17 +theorem axiom_of_choice': "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
    2.18  apply (rule exI [of _  "\<lambda>x. SOME y. P x y"])
    2.19  by (blast intro: someI);
    2.20  
     3.1 --- a/doc-src/TutorialI/Rules/Forward.thy	Thu Aug 29 16:15:11 2002 +0200
     3.2 +++ b/doc-src/TutorialI/Rules/Forward.thy	Fri Aug 30 16:42:45 2002 +0200
     3.3 @@ -71,20 +71,21 @@
     3.4  \rulename{sym}
     3.5  *};
     3.6  
     3.7 -lemmas gcd_mult = gcd_mult_1 [THEN sym];
     3.8 +lemmas gcd_mult0 = gcd_mult_1 [THEN sym];
     3.9 +      (*not quite right: we need ?k but this gives k*)
    3.10  
    3.11 -lemmas gcd_mult = gcd_mult_distrib2 [of k 1, simplified, THEN sym];
    3.12 +lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym];
    3.13        (*better in one step!*)
    3.14  
    3.15  text {*
    3.16 -more legible
    3.17 +more legible, and variables properly generalized
    3.18  *};
    3.19  
    3.20  lemma gcd_mult [simp]: "gcd(k, k*n) = k"
    3.21  by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
    3.22  
    3.23  
    3.24 -lemmas gcd_self = gcd_mult [of k 1, simplified];
    3.25 +lemmas gcd_self0 = gcd_mult [of k 1, simplified];
    3.26  
    3.27  
    3.28  text {*
    3.29 @@ -99,7 +100,7 @@
    3.30  
    3.31  
    3.32  text {*
    3.33 -again: more legible
    3.34 +again: more legible, and variables properly generalized
    3.35  *};
    3.36  
    3.37  lemma gcd_self [simp]: "gcd(k,k) = k"
     4.1 --- a/src/FOL/FOL.thy	Thu Aug 29 16:15:11 2002 +0200
     4.2 +++ b/src/FOL/FOL.thy	Fri Aug 30 16:42:45 2002 +0200
     4.3 @@ -28,7 +28,14 @@
     4.4  
     4.5  use "blastdata.ML"
     4.6  setup Blast.setup
     4.7 -use "FOL_lemmas2.ML"
     4.8 +
     4.9 +
    4.10 +lemma ex1_functional: "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
    4.11 +by blast
    4.12 +
    4.13 +ML {*
    4.14 +val ex1_functional = thm "ex1_functional";
    4.15 +*}
    4.16  
    4.17  use "simpdata.ML"
    4.18  setup simpsetup
     5.1 --- a/src/FOL/FOL_lemmas2.ML	Thu Aug 29 16:15:11 2002 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,4 +0,0 @@
     5.4 -
     5.5 -Goal "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c";
     5.6 -  by (Blast_tac 1);
     5.7 -qed "ex1_functional";
     6.1 --- a/src/FOL/IsaMakefile	Thu Aug 29 16:15:11 2002 +0200
     6.2 +++ b/src/FOL/IsaMakefile	Fri Aug 30 16:42:45 2002 +0200
     6.3 @@ -32,7 +32,7 @@
     6.4    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
     6.5    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \
     6.6    $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/quantifier1.ML\
     6.7 -  FOL.ML FOL.thy FOL_lemmas1.ML FOL_lemmas2.ML IFOL.ML IFOL.thy \
     6.8 +  FOL.ML FOL.thy FOL_lemmas1.ML IFOL.ML IFOL.thy \
     6.9    IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML document/root.tex \
    6.10    fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
    6.11  	@$(ISATOOL) usedir -b $(OUT)/Pure FOL
     7.1 --- a/src/HOL/Algebra/abstract/Ring.ML	Thu Aug 29 16:15:11 2002 +0200
     7.2 +++ b/src/HOL/Algebra/abstract/Ring.ML	Fri Aug 30 16:42:45 2002 +0200
     7.3 @@ -4,8 +4,6 @@
     7.4      Author: Clemens Ballarin, started 9 December 1996
     7.5  *)
     7.6  
     7.7 -Blast.overloaded ("Divides.op dvd", domain_type);
     7.8 -
     7.9  val a_assoc = thm "plus_ac0.assoc";
    7.10  val l_zero = thm "plus_ac0.zero";
    7.11  val a_comm = thm "plus_ac0.commute";
     8.1 --- a/src/HOL/Auth/ROOT.ML	Thu Aug 29 16:15:11 2002 +0200
     8.2 +++ b/src/HOL/Auth/ROOT.ML	Fri Aug 30 16:42:45 2002 +0200
     8.3 @@ -7,6 +7,7 @@
     8.4  *)
     8.5  
     8.6  goals_limit := 1;
     8.7 +set timing;
     8.8  
     8.9  (*Shared-key protocols*)
    8.10  time_use_thy "NS_Shared";
     9.1 --- a/src/HOL/Bali/ROOT.ML	Thu Aug 29 16:15:11 2002 +0200
     9.2 +++ b/src/HOL/Bali/ROOT.ML	Fri Aug 30 16:42:45 2002 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -
     9.5 +set timing;
     9.6  update_thy "AxExample";
     9.7  update_thy "AxSound";
     9.8  update_thy "AxCompl";
    10.1 --- a/src/HOL/HOL.thy	Thu Aug 29 16:15:11 2002 +0200
    10.2 +++ b/src/HOL/HOL.thy	Fri Aug 30 16:42:45 2002 +0200
    10.3 @@ -603,13 +603,6 @@
    10.4    "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
    10.5    "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
    10.6  
    10.7 -(*Tell blast about overloading of < and <= to reduce the risk of
    10.8 -  its applying a rule for the wrong type*)
    10.9 -ML {*
   10.10 -Blast.overloaded ("op <" , domain_type);
   10.11 -Blast.overloaded ("op <=", domain_type);
   10.12 -*}
   10.13 -
   10.14  
   10.15  subsubsection {* Monotonicity *}
   10.16  
    11.1 --- a/src/HOL/Lambda/Commutation.thy	Thu Aug 29 16:15:11 2002 +0200
    11.2 +++ b/src/HOL/Lambda/Commutation.thy	Fri Aug 30 16:42:45 2002 +0200
    11.3 @@ -225,7 +225,8 @@
    11.4        with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
    11.5  	by (blast dest:lc)
    11.6        from yb u y'c show ?thesis
    11.7 -	by(blast intro:rtrancl_trans
    11.8 +	by(blast del: rtrancl_refl
    11.9 +		 intro:rtrancl_trans
   11.10                   dest:IH[OF xy[symmetric]] IH[OF xy'[symmetric]])
   11.11      qed
   11.12    qed
    12.1 --- a/src/HOL/Lambda/ROOT.ML	Thu Aug 29 16:15:11 2002 +0200
    12.2 +++ b/src/HOL/Lambda/ROOT.ML	Fri Aug 30 16:42:45 2002 +0200
    12.3 @@ -6,6 +6,7 @@
    12.4  
    12.5  Syntax.ambiguity_level := 100;
    12.6  
    12.7 +set timing;
    12.8  time_use_thy "Eta";
    12.9  no_document time_use_thy "Accessible_Part";
   12.10  time_use_thy "Type";
    13.1 --- a/src/HOL/Real/RealDef.ML	Thu Aug 29 16:15:11 2002 +0200
    13.2 +++ b/src/HOL/Real/RealDef.ML	Fri Aug 30 16:42:45 2002 +0200
    13.3 @@ -5,9 +5,6 @@
    13.4      Description : The reals
    13.5  *)
    13.6  
    13.7 -(*Ensures that Blast_tac can cope with real*)
    13.8 -Blast.overloaded ("RealDef.real", domain_type); 
    13.9 -
   13.10  (*** Proving that realrel is an equivalence relation ***)
   13.11  
   13.12  Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
    14.1 --- a/src/HOL/Relation.thy	Thu Aug 29 16:15:11 2002 +0200
    14.2 +++ b/src/HOL/Relation.thy	Fri Aug 30 16:42:45 2002 +0200
    14.3 @@ -300,8 +300,6 @@
    14.4  
    14.5  subsection {* Image of a set under a relation *}
    14.6  
    14.7 -ML {* overload_1st_set "Relation.Image" *}
    14.8 -
    14.9  lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
   14.10    by (simp add: Image_def)
   14.11  
    15.1 --- a/src/HOL/Set.thy	Thu Aug 29 16:15:11 2002 +0200
    15.2 +++ b/src/HOL/Set.thy	Fri Aug 30 16:42:45 2002 +0200
    15.3 @@ -343,22 +343,6 @@
    15.4    "'a set"}.
    15.5  *}
    15.6  
    15.7 -ML {*
    15.8 -  fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type);
    15.9 -*}
   15.10 -
   15.11 -ML "
   15.12 -  (* While (:) is not, its type must be kept
   15.13 -    for overloading of = to work. *)
   15.14 -  Blast.overloaded (\"op :\", domain_type);
   15.15 -
   15.16 -  overload_1st_set \"Ball\";            (*need UNION, INTER also?*)
   15.17 -  overload_1st_set \"Bex\";
   15.18 -
   15.19 -  (*Image: retain the type of the set being expressed*)
   15.20 -  Blast.overloaded (\"image\", domain_type);
   15.21 -"
   15.22 -
   15.23  lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
   15.24    -- {* Rule in Modus Ponens style. *}
   15.25    by (unfold subset_def) blast
    16.1 --- a/src/HOL/UNITY/Constrains.ML	Thu Aug 29 16:15:11 2002 +0200
    16.2 +++ b/src/HOL/UNITY/Constrains.ML	Fri Aug 30 16:42:45 2002 +0200
    16.3 @@ -45,9 +45,6 @@
    16.4  
    16.5  (*** Co ***)
    16.6  
    16.7 -(*Needed because its operands are sets*)
    16.8 -overload_1st_set "Constrains.Constrains";
    16.9 -
   16.10  (*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
   16.11  bind_thm ("constrains_reachable_Int",
   16.12  	  subset_refl RS
    17.1 --- a/src/HOL/UNITY/Extend.ML	Thu Aug 29 16:15:11 2002 +0200
    17.2 +++ b/src/HOL/UNITY/Extend.ML	Fri Aug 30 16:42:45 2002 +0200
    17.3 @@ -750,7 +750,9 @@
    17.4  qed "ok_extend_imp_ok_project";
    17.5  
    17.6  Goal "(extend h F ok extend h G) = (F ok G)";
    17.7 -by (auto_tac (claset(), simpset() addsimps [ok_def]));  
    17.8 +by (asm_full_simp_tac (simpset() addsimps [ok_def]) 1);
    17.9 +by Safe_tac;
   17.10 +by (REPEAT (Force_tac 1));
   17.11  qed "ok_extend_iff";
   17.12  
   17.13  Goalw [OK_def] "OK I (%i. extend h (F i)) = (OK I F)";
    18.1 --- a/src/HOL/UNITY/Rename.ML	Thu Aug 29 16:15:11 2002 +0200
    18.2 +++ b/src/HOL/UNITY/Rename.ML	Fri Aug 30 16:42:45 2002 +0200
    18.3 @@ -69,8 +69,9 @@
    18.4  by (rtac bijI 1);
    18.5  by (rtac (export inj_extend_act) 1);
    18.6  by (auto_tac (claset(), simpset() addsimps [bij_extend_act_eq_project_act]));  
    18.7 -by (blast_tac (claset() addIs [bij_imp_bij_inv, surjI, 
    18.8 -                               export extend_act_inverse]) 1); 
    18.9 +by (rtac surjI 1); 
   18.10 +by (rtac (export extend_act_inverse) 1); 
   18.11 +by (blast_tac (claset() addIs [bij_imp_bij_inv, good_map_bij]) 1); 
   18.12  qed "bij_extend_act";
   18.13  
   18.14  Goal "bij h ==> bij (project_act (%(x,u::'c). h x))";
    19.1 --- a/src/HOL/UNITY/SubstAx.ML	Thu Aug 29 16:15:11 2002 +0200
    19.2 +++ b/src/HOL/UNITY/SubstAx.ML	Fri Aug 30 16:42:45 2002 +0200
    19.3 @@ -6,9 +6,6 @@
    19.4  LeadsTo relation, restricted to the set of reachable states.
    19.5  *)
    19.6  
    19.7 -overload_1st_set "SubstAx.op LeadsTo";
    19.8 -
    19.9 -
   19.10  (*Resembles the previous definition of LeadsTo*)
   19.11  Goalw [LeadsTo_def]
   19.12       "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}";
    20.1 --- a/src/HOL/UNITY/UNITY.ML	Thu Aug 29 16:15:11 2002 +0200
    20.2 +++ b/src/HOL/UNITY/UNITY.ML	Fri Aug 30 16:42:45 2002 +0200
    20.3 @@ -131,12 +131,6 @@
    20.4  
    20.5  (*** co ***)
    20.6  
    20.7 -(*These operators are not overloaded, but their operands are sets, and 
    20.8 -  ultimately there's a risk of reaching equality, which IS overloaded*)
    20.9 -overload_1st_set "UNITY.constrains";
   20.10 -overload_1st_set "UNITY.stable";
   20.11 -overload_1st_set "UNITY.unless";
   20.12 -
   20.13  val prems = Goalw [constrains_def]
   20.14      "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A') \
   20.15  \    ==> F : A co A'";
    21.1 --- a/src/HOL/UNITY/WFair.ML	Thu Aug 29 16:15:11 2002 +0200
    21.2 +++ b/src/HOL/UNITY/WFair.ML	Fri Aug 30 16:42:45 2002 +0200
    21.3 @@ -9,10 +9,6 @@
    21.4  *)
    21.5  
    21.6  
    21.7 -overload_1st_set "WFair.transient";
    21.8 -overload_1st_set "WFair.ensures";
    21.9 -overload_1st_set "WFair.op leadsTo";
   21.10 -
   21.11  (*** transient ***)
   21.12  
   21.13  Goalw [stable_def, constrains_def, transient_def]
    22.1 --- a/src/HOL/blastdata.ML	Thu Aug 29 16:15:11 2002 +0200
    22.2 +++ b/src/HOL/blastdata.ML	Fri Aug 30 16:42:45 2002 +0200
    22.3 @@ -28,7 +28,6 @@
    22.4    end;
    22.5  
    22.6  structure Blast = BlastFun(Blast_Data);
    22.7 -Blast.overloaded ("op =", domain_type);	(*overloading of equality as iff*)
    22.8  
    22.9  val Blast_tac = Blast.Blast_tac
   22.10  and blast_tac = Blast.blast_tac;
    23.1 --- a/src/Provers/blast.ML	Thu Aug 29 16:15:11 2002 +0200
    23.2 +++ b/src/Provers/blast.ML	Fri Aug 30 16:42:45 2002 +0200
    23.3 @@ -27,12 +27,6 @@
    23.4  	such as transitivity are treated specially to prevent this.  Sometimes
    23.5  	the formulae get into the wrong order (see WRONG below).
    23.6  
    23.7 -  With overloading:
    23.8 -        Calls to Blast.overloaded (see HOL/Set.ML for examples) are needed
    23.9 -	to tell Blast_tac when to retain some type information.  Make sure
   23.10 -	you know the constant's internal name, which might be "op <=" or 
   23.11 -	"Relation.op ^^".
   23.12 -
   23.13    With substition for equalities (hyp_subst_tac):
   23.14          When substitution affects a haz formula or literal, it is moved
   23.15          back to the list of safe formulae.
   23.16 @@ -88,8 +82,6 @@
   23.17    val depth_tac 	: claset -> int -> int -> tactic
   23.18    val blast_tac 	: claset -> int -> tactic
   23.19    val Blast_tac 	: int -> tactic
   23.20 -  val overloaded 	: string * (Term.typ -> Term.typ) -> unit
   23.21 -  val get_overloads	: unit -> (string * (Term.typ -> Term.typ)) list
   23.22    val setup		: (theory -> theory) list
   23.23    (*debugging tools*)
   23.24    val stats	        : bool ref
   23.25 @@ -186,26 +178,21 @@
   23.26  			   end
   23.27  		 | Some v => v)
   23.28  
   23.29 -local
   23.30 -val overloads = ref ([]: (string * (Term.typ -> Term.typ)) list)
   23.31 -in
   23.32 +(*Monomorphic constants used in blast, plus binary propositional connectives.*)
   23.33 +val standard_consts = 
   23.34 +    ["Not", "op &", "op |", "op -->", "op <->", 
   23.35 +     "*Goal*", "*False*", "==>", "all", "Trueprop"];
   23.36  
   23.37 -fun overloaded arg = (overloads := arg :: (!overloads));
   23.38 -
   23.39 -fun get_overloads() = !overloads;
   23.40 +val standard_const_table = Symtab.make (map (rpair()) standard_consts)
   23.41  
   23.42 -(*Convert a possibly overloaded Term.Const to a Blast.Const or Blast.TConst,
   23.43 -  converting its type to a Blast.term in the latter case.*)
   23.44 -fun fromConst alist (a,T) =
   23.45 -  case assoc_string (!overloads, a) of
   23.46 -      None   => Const a		(*not overloaded*)
   23.47 -    | Some f => 
   23.48 -	let val T' = f T
   23.49 -		     handle Match => error
   23.50 -                ("Blast_tac: unexpected type for overloaded constant " ^ a)
   23.51 -        in  TConst(a, fromType alist T')  end;
   23.52 -
   23.53 -end;
   23.54 +(*Convert a Term.Const to a Blast.Const or Blast.TConst,
   23.55 +  converting its type to a Blast.term in the latter case.
   23.56 +  Const is used for a small number of built-in operators that are
   23.57 +  known to be monomorphic, which promotes efficiency. *)
   23.58 +fun fromConst alist (a,T) = 
   23.59 +    case Symtab.lookup(standard_const_table, a) of
   23.60 +	None => TConst(a, fromType alist T)
   23.61 +      | Some() => Const(a)
   23.62  
   23.63  
   23.64  (*Tests whether 2 terms are alpha-convertible; chases instantiations*)