# HG changeset patch
# User wenzelm
# Date 972331836 -7200
# Node ID a7f961fb62c665b3f6b5c48ab55880667a136bf1
# Parent  c50fc8023ac08cd0600769ff4c697b35cf93b96e
intro_classes by default;

diff -r c50fc8023ac0 -r a7f961fb62c6 doc-src/AxClass/Group/Group.thy
--- a/doc-src/AxClass/Group/Group.thy	Mon Oct 23 22:09:52 2000 +0200
+++ b/doc-src/AxClass/Group/Group.thy	Mon Oct 23 22:10:36 2000 +0200
@@ -182,14 +182,14 @@
 *}
 
 instance monoid < semigroup
-proof intro_classes
+proof
   fix x y z :: "'a\<Colon>monoid"
   show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
     by (rule monoid.assoc)
 qed
 
 instance group < monoid
-proof intro_classes
+proof
   fix x y z :: "'a\<Colon>group"
   show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
     by (rule semigroup.assoc)
@@ -203,12 +203,12 @@
  \medskip The $\INSTANCE$ command sets up an appropriate goal that
  represents the class inclusion (or type arity, see
  \secref{sec:inst-arity}) to be proven (see also
- \cite{isabelle-isar-ref}).  The @{text intro_classes} proof method
- does back-chaining of class membership statements wrt.\ the hierarchy
- of any classes defined in the current theory; the effect is to reduce
- to the initial statement to a number of goals that directly
- correspond to any class axioms encountered on the path upwards
- through the class hierarchy.
+ \cite{isabelle-isar-ref}).  The initial proof step causes
+ back-chaining of class membership statements wrt.\ the hierarchy of
+ any classes defined in the current theory; the effect is to reduce to
+ the initial statement to a number of goals that directly correspond
+ to any class axioms encountered on the path upwards through the class
+ hierarchy.
 *}
 
 
diff -r c50fc8023ac0 -r a7f961fb62c6 doc-src/AxClass/Group/Product.thy
--- a/doc-src/AxClass/Group/Product.thy	Mon Oct 23 22:09:52 2000 +0200
+++ b/doc-src/AxClass/Group/Product.thy	Mon Oct 23 22:10:36 2000 +0200
@@ -41,8 +41,7 @@
  Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
  type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
  type signature.  In our example, this arity may be always added when
- required by means of an $\INSTANCE$ with the trivial proof
- $\BY{intro_classes}$.
+ required by means of an $\INSTANCE$ with the default proof $\DDOT$.
 
  \medskip Thus, we may observe the following discipline of using
  syntactic classes.  Overloaded polymorphic constants have their type
@@ -54,8 +53,7 @@
  follows.
 *}
 
-instance bool :: product
-  by intro_classes
+instance bool :: product ..
 defs (overloaded)
   product_bool_def: "x \<odot> y \<equiv> x \<and> y"
 
diff -r c50fc8023ac0 -r a7f961fb62c6 src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Mon Oct 23 22:09:52 2000 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy	Mon Oct 23 22:10:36 2000 +0200
@@ -197,7 +197,7 @@
 *}
 
 instance dual :: (complete_lattice) complete_lattice
-proof intro_classes
+proof
   fix A' :: "'a::complete_lattice dual set"
   show "\<exists>inf'. is_Inf A' inf'"
   proof -
@@ -275,7 +275,7 @@
 qed
 
 instance complete_lattice < lattice
-proof intro_classes
+proof
   fix x y :: "'a::complete_lattice"
   from is_inf_binary show "\<exists>inf. is_inf x y inf" ..
   from is_sup_binary show "\<exists>sup. is_sup x y sup" ..
diff -r c50fc8023ac0 -r a7f961fb62c6 src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Mon Oct 23 22:09:52 2000 +0200
+++ b/src/HOL/Lattice/Lattice.thy	Mon Oct 23 22:10:36 2000 +0200
@@ -109,7 +109,7 @@
 *}
 
 instance dual :: (lattice) lattice
-proof intro_classes
+proof
   fix x' y' :: "'a::lattice dual"
   show "\<exists>inf'. is_inf x' y' inf'"
   proof -
@@ -361,7 +361,7 @@
 qed
 
 instance linear_order < lattice
-proof intro_classes
+proof
   fix x y :: "'a::linear_order"
   from is_inf_minimum show "\<exists>inf. is_inf x y inf" ..
   from is_sup_maximum show "\<exists>sup. is_sup x y sup" ..
@@ -450,7 +450,7 @@
 qed
 
 instance * :: (lattice, lattice) lattice
-proof intro_classes
+proof
   fix p q :: "'a::lattice \<times> 'b::lattice"
   from is_inf_prod show "\<exists>inf. is_inf p q inf" ..
   from is_sup_prod show "\<exists>sup. is_sup p q sup" ..
@@ -520,7 +520,7 @@
 qed
 
 instance fun :: ("term", lattice) lattice
-proof intro_classes
+proof
   fix f g :: "'a \<Rightarrow> 'b::lattice"
   show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)
   show "\<exists>sup. is_sup f g sup" by rule (rule is_sup_fun)
diff -r c50fc8023ac0 -r a7f961fb62c6 src/HOL/Lattice/Orders.thy
--- a/src/HOL/Lattice/Orders.thy	Mon Oct 23 22:09:52 2000 +0200
+++ b/src/HOL/Lattice/Orders.thy	Mon Oct 23 22:10:36 2000 +0200
@@ -54,8 +54,7 @@
 primrec
   undual_dual: "undual (dual x) = x"
 
-instance dual :: (leq) leq
-  by intro_classes
+instance dual :: (leq) leq ..
 
 defs (overloaded)
   leq_dual_def: "x' \<sqsubseteq> y' \<equiv> undual y' \<sqsubseteq> undual x'"
@@ -155,7 +154,7 @@
 *}
 
 instance dual :: (quasi_order) quasi_order
-proof intro_classes
+proof
   fix x' y' z' :: "'a::quasi_order dual"
   have "undual x' \<sqsubseteq> undual x'" .. thus "x' \<sqsubseteq> x'" ..
   assume "y' \<sqsubseteq> z'" hence "undual z' \<sqsubseteq> undual y'" ..
@@ -164,7 +163,7 @@
 qed
 
 instance dual :: (partial_order) partial_order
-proof intro_classes
+proof
   fix x' y' :: "'a::partial_order dual"
   assume "y' \<sqsubseteq> x'" hence "undual x' \<sqsubseteq> undual y'" ..
   also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..
@@ -172,7 +171,7 @@
 qed
 
 instance dual :: (linear_order) linear_order
-proof intro_classes
+proof
   fix x' y' :: "'a::linear_order dual"
   show "x' \<sqsubseteq> y' \<or> y' \<sqsubseteq> x'"
   proof (rule linear_order_cases)
@@ -193,8 +192,7 @@
   \emph{not} be linear in general.
 *}
 
-instance * :: (leq, leq) leq
-  by intro_classes
+instance * :: (leq, leq) leq ..
 
 defs (overloaded)
   leq_prod_def: "p \<sqsubseteq> q \<equiv> fst p \<sqsubseteq> fst q \<and> snd p \<sqsubseteq> snd q"
@@ -208,7 +206,7 @@
   by (unfold leq_prod_def) blast
 
 instance * :: (quasi_order, quasi_order) quasi_order
-proof intro_classes
+proof
   fix p q r :: "'a::quasi_order \<times> 'b::quasi_order"
   show "p \<sqsubseteq> p"
   proof
@@ -228,7 +226,7 @@
 qed
 
 instance * :: (partial_order, partial_order) partial_order
-proof intro_classes
+proof
   fix p q :: "'a::partial_order \<times> 'b::partial_order"
   assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"
   show "p = q"
@@ -251,8 +249,7 @@
   orders need \emph{not} be linear in general.
 *}
 
-instance fun :: ("term", leq) leq
-  by intro_classes
+instance fun :: ("term", leq) leq ..
 
 defs (overloaded)
   leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
@@ -264,7 +261,7 @@
   by (unfold leq_fun_def) blast
 
 instance fun :: ("term", quasi_order) quasi_order
-proof intro_classes
+proof
   fix f g h :: "'a \<Rightarrow> 'b::quasi_order"
   show "f \<sqsubseteq> f"
   proof
@@ -280,7 +277,7 @@
 qed
 
 instance fun :: ("term", partial_order) partial_order
-proof intro_classes
+proof
   fix f g :: "'a \<Rightarrow> 'b::partial_order"
   assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"
   show "f = g"
diff -r c50fc8023ac0 -r a7f961fb62c6 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 23 22:09:52 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 23 22:10:36 2000 +0200
@@ -212,7 +212,7 @@
 text {* The \emph{sum} of two vectorspaces $U$ and $V$ is the set of
 all sums of elements from $U$ and $V$. *}
 
-instance set :: (plus) plus by intro_classes
+instance set :: (plus) plus ..
 
 defs vs_sum_def:
   "U + V == {u + v | u v. u \<in> U \<and> v \<in> V}" (***
diff -r c50fc8023ac0 -r a7f961fb62c6 src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Mon Oct 23 22:09:52 2000 +0200
+++ b/src/HOL/Real/RealPow.thy	Mon Oct 23 22:10:36 2000 +0200
@@ -12,8 +12,7 @@
 lemmas [arith_split] = abs_split
 
 
-instance real :: power
-  by intro_classes
+instance real :: power ..
 
 primrec (realpow)
      realpow_0:   "r ^ 0       = #1"
diff -r c50fc8023ac0 -r a7f961fb62c6 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Mon Oct 23 22:09:52 2000 +0200
+++ b/src/HOL/Record.thy	Mon Oct 23 22:10:36 2000 +0200
@@ -51,8 +51,7 @@
 (* type class for record extensions *)
 
 axclass more < "term"
-instance unit :: more
-  by intro_classes
+instance unit :: more ..
 
 
 (* initialize the package *)
diff -r c50fc8023ac0 -r a7f961fb62c6 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Oct 23 22:09:52 2000 +0200
+++ b/src/Provers/classical.ML	Mon Oct 23 22:10:36 2000 +0200
@@ -1111,8 +1111,12 @@
 fun rule_tac [] cs facts = some_rule_tac cs facts
   | rule_tac rules _ facts = Method.rule_tac rules facts;
 
+fun default_tac rules cs facts =
+  rule_tac rules cs facts ORELSE' AxClass.default_intro_classes_tac facts;
+
 in
   val rule = METHOD_CLASET' o rule_tac;
+  val default = METHOD_CLASET' o default_tac;
 end;
 
 
@@ -1169,7 +1173,7 @@
 (** setup_methods **)
 
 val setup_methods = Method.add_methods
- [("default", Method.thms_ctxt_args rule, "apply some rule (classical)"),
+ [("default", Method.thms_ctxt_args default, "apply some rule (classical)"),
   ("rule", Method.thms_ctxt_args rule, "apply some rule (classical)"),
   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
   ("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"),
diff -r c50fc8023ac0 -r a7f961fb62c6 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Oct 23 22:09:52 2000 +0200
+++ b/src/Pure/Isar/method.ML	Mon Oct 23 22:10:36 2000 +0200
@@ -48,6 +48,7 @@
     -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq
   val rule_tac: thm list -> thm list -> int -> tactic
   val erule_tac: thm list -> thm list -> int -> tactic
+  val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
   val rule: thm list -> Proof.method
   val erule: thm list -> Proof.method
   val drule: thm list -> Proof.method
@@ -323,14 +324,15 @@
 fun gen_rule_tac tac rules [] = tac rules
   | gen_rule_tac tac erules facts = gen_resolveq_tac (tac o single) (multi_resolves facts erules);
 
-fun gen_rule tac rules = METHOD (HEADGOAL o tac rules);
-
-fun gen_rule' tac arg_rules ctxt = METHOD (fn facts =>
+fun gen_some_rule_tac tac arg_rules ctxt facts =
   let val rules =
     if not (null arg_rules) then arg_rules
     else if null facts then #1 (LocalRules.get ctxt)
     else op @ (LocalRules.get ctxt);
-  in HEADGOAL (tac rules facts) end);
+  in tac rules facts end;
+
+fun gen_rule tac rules = METHOD (HEADGOAL o tac rules);
+fun gen_rule' tac arg_rules ctxt = METHOD (HEADGOAL o gen_some_rule_tac tac arg_rules ctxt);
 
 fun setup raw_tac =
   let val tac = gen_rule_tac raw_tac
@@ -338,6 +340,7 @@
 
 in
 
+val some_rule_tac = gen_some_rule_tac (gen_rule_tac Tactic.resolve_tac);
 val (rule_tac, rule, some_rule) = setup Tactic.resolve_tac;
 val (erule_tac, erule, some_erule) = setup Tactic.eresolve_tac;
 val (drule_tac, drule, some_drule) = setup Tactic.dresolve_tac;
@@ -648,7 +651,6 @@
   ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
   ("unfold", thms_args unfold, "unfold definitions"),
   ("fold", thms_args fold, "fold definitions"),
-  ("default", thms_ctxt_args some_rule, "apply some rule"),
   ("rule", thms_ctxt_args some_rule, "apply some rule"),
   ("erule", thms_ctxt_args some_erule, "apply some rule in elimination manner (improper)"),
   ("drule", thms_ctxt_args some_drule, "apply some rule in destruct manner (improper)"),
diff -r c50fc8023ac0 -r a7f961fb62c6 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Oct 23 22:09:52 2000 +0200
+++ b/src/Pure/axclass.ML	Mon Oct 23 22:10:36 2000 +0200
@@ -23,6 +23,7 @@
     -> thm list -> tactic option -> theory -> theory
   val add_inst_arity_i: string * sort list * sort -> string list
     -> thm list -> tactic option -> theory -> theory
+  val default_intro_classes_tac: thm list -> int -> tactic
   val axclass_tac: thm list -> tactic
   val prove_subclass: theory -> class * class -> thm list
     -> tactic option -> thm
@@ -306,15 +307,27 @@
 
 (* intro_classes *)
 
-fun intro_classes_tac facts st =
-  HEADGOAL (Method.insert_tac facts THEN'
-      REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) st;
+fun intro_classes_tac facts i st =
+  (Method.insert_tac facts THEN'
+    REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) i st;
 
 val intro_classes_method =
-  ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
+  ("intro_classes", Method.no_args (Method.METHOD (HEADGOAL o intro_classes_tac)),
     "back-chain introduction rules of axiomatic type classes");
 
 
+(* default method *)
+
+fun default_intro_classes_tac [] = intro_classes_tac []
+  | default_intro_classes_tac _ = K Tactical.no_tac;    (*no error message!*)
+
+fun default_tac rules ctxt facts =
+  HEADGOAL (Method.some_rule_tac rules ctxt facts ORELSE' default_intro_classes_tac facts);
+
+val default_method =
+  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some rule")
+
+
 (* axclass_tac *)
 
 (*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
@@ -327,7 +340,7 @@
     val defs = filter is_def thms;
     val non_defs = filter_out is_def thms;
   in
-    intro_classes_tac [] THEN
+    HEADGOAL (intro_classes_tac []) THEN
     TRY (rewrite_goals_tac defs) THEN
     TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
   end;
@@ -442,7 +455,7 @@
 
 val setup =
  [AxclassesData.init,
-  Method.add_methods [intro_classes_method]];
+  Method.add_methods [intro_classes_method, default_method]];
 
 
 (* outer syntax *)