intro_classes by default;
authorwenzelm
Mon Oct 23 22:10:36 2000 +0200 (2000-10-23)
changeset 10309a7f961fb62c6
parent 10308 c50fc8023ac0
child 10310 d78de58fe368
intro_classes by default;
doc-src/AxClass/Group/Group.thy
doc-src/AxClass/Group/Product.thy
src/HOL/Lattice/CompleteLattice.thy
src/HOL/Lattice/Lattice.thy
src/HOL/Lattice/Orders.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/RealPow.thy
src/HOL/Record.thy
src/Provers/classical.ML
src/Pure/Isar/method.ML
src/Pure/axclass.ML
     1.1 --- a/doc-src/AxClass/Group/Group.thy	Mon Oct 23 22:09:52 2000 +0200
     1.2 +++ b/doc-src/AxClass/Group/Group.thy	Mon Oct 23 22:10:36 2000 +0200
     1.3 @@ -182,14 +182,14 @@
     1.4  *}
     1.5  
     1.6  instance monoid < semigroup
     1.7 -proof intro_classes
     1.8 +proof
     1.9    fix x y z :: "'a\<Colon>monoid"
    1.10    show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
    1.11      by (rule monoid.assoc)
    1.12  qed
    1.13  
    1.14  instance group < monoid
    1.15 -proof intro_classes
    1.16 +proof
    1.17    fix x y z :: "'a\<Colon>group"
    1.18    show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
    1.19      by (rule semigroup.assoc)
    1.20 @@ -203,12 +203,12 @@
    1.21   \medskip The $\INSTANCE$ command sets up an appropriate goal that
    1.22   represents the class inclusion (or type arity, see
    1.23   \secref{sec:inst-arity}) to be proven (see also
    1.24 - \cite{isabelle-isar-ref}).  The @{text intro_classes} proof method
    1.25 - does back-chaining of class membership statements wrt.\ the hierarchy
    1.26 - of any classes defined in the current theory; the effect is to reduce
    1.27 - to the initial statement to a number of goals that directly
    1.28 - correspond to any class axioms encountered on the path upwards
    1.29 - through the class hierarchy.
    1.30 + \cite{isabelle-isar-ref}).  The initial proof step causes
    1.31 + back-chaining of class membership statements wrt.\ the hierarchy of
    1.32 + any classes defined in the current theory; the effect is to reduce to
    1.33 + the initial statement to a number of goals that directly correspond
    1.34 + to any class axioms encountered on the path upwards through the class
    1.35 + hierarchy.
    1.36  *}
    1.37  
    1.38  
     2.1 --- a/doc-src/AxClass/Group/Product.thy	Mon Oct 23 22:09:52 2000 +0200
     2.2 +++ b/doc-src/AxClass/Group/Product.thy	Mon Oct 23 22:10:36 2000 +0200
     2.3 @@ -41,8 +41,7 @@
     2.4   Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
     2.5   type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
     2.6   type signature.  In our example, this arity may be always added when
     2.7 - required by means of an $\INSTANCE$ with the trivial proof
     2.8 - $\BY{intro_classes}$.
     2.9 + required by means of an $\INSTANCE$ with the default proof $\DDOT$.
    2.10  
    2.11   \medskip Thus, we may observe the following discipline of using
    2.12   syntactic classes.  Overloaded polymorphic constants have their type
    2.13 @@ -54,8 +53,7 @@
    2.14   follows.
    2.15  *}
    2.16  
    2.17 -instance bool :: product
    2.18 -  by intro_classes
    2.19 +instance bool :: product ..
    2.20  defs (overloaded)
    2.21    product_bool_def: "x \<odot> y \<equiv> x \<and> y"
    2.22  
     3.1 --- a/src/HOL/Lattice/CompleteLattice.thy	Mon Oct 23 22:09:52 2000 +0200
     3.2 +++ b/src/HOL/Lattice/CompleteLattice.thy	Mon Oct 23 22:10:36 2000 +0200
     3.3 @@ -197,7 +197,7 @@
     3.4  *}
     3.5  
     3.6  instance dual :: (complete_lattice) complete_lattice
     3.7 -proof intro_classes
     3.8 +proof
     3.9    fix A' :: "'a::complete_lattice dual set"
    3.10    show "\<exists>inf'. is_Inf A' inf'"
    3.11    proof -
    3.12 @@ -275,7 +275,7 @@
    3.13  qed
    3.14  
    3.15  instance complete_lattice < lattice
    3.16 -proof intro_classes
    3.17 +proof
    3.18    fix x y :: "'a::complete_lattice"
    3.19    from is_inf_binary show "\<exists>inf. is_inf x y inf" ..
    3.20    from is_sup_binary show "\<exists>sup. is_sup x y sup" ..
     4.1 --- a/src/HOL/Lattice/Lattice.thy	Mon Oct 23 22:09:52 2000 +0200
     4.2 +++ b/src/HOL/Lattice/Lattice.thy	Mon Oct 23 22:10:36 2000 +0200
     4.3 @@ -109,7 +109,7 @@
     4.4  *}
     4.5  
     4.6  instance dual :: (lattice) lattice
     4.7 -proof intro_classes
     4.8 +proof
     4.9    fix x' y' :: "'a::lattice dual"
    4.10    show "\<exists>inf'. is_inf x' y' inf'"
    4.11    proof -
    4.12 @@ -361,7 +361,7 @@
    4.13  qed
    4.14  
    4.15  instance linear_order < lattice
    4.16 -proof intro_classes
    4.17 +proof
    4.18    fix x y :: "'a::linear_order"
    4.19    from is_inf_minimum show "\<exists>inf. is_inf x y inf" ..
    4.20    from is_sup_maximum show "\<exists>sup. is_sup x y sup" ..
    4.21 @@ -450,7 +450,7 @@
    4.22  qed
    4.23  
    4.24  instance * :: (lattice, lattice) lattice
    4.25 -proof intro_classes
    4.26 +proof
    4.27    fix p q :: "'a::lattice \<times> 'b::lattice"
    4.28    from is_inf_prod show "\<exists>inf. is_inf p q inf" ..
    4.29    from is_sup_prod show "\<exists>sup. is_sup p q sup" ..
    4.30 @@ -520,7 +520,7 @@
    4.31  qed
    4.32  
    4.33  instance fun :: ("term", lattice) lattice
    4.34 -proof intro_classes
    4.35 +proof
    4.36    fix f g :: "'a \<Rightarrow> 'b::lattice"
    4.37    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!? *)
    4.38    show "\<exists>sup. is_sup f g sup" by rule (rule is_sup_fun)
     5.1 --- a/src/HOL/Lattice/Orders.thy	Mon Oct 23 22:09:52 2000 +0200
     5.2 +++ b/src/HOL/Lattice/Orders.thy	Mon Oct 23 22:10:36 2000 +0200
     5.3 @@ -54,8 +54,7 @@
     5.4  primrec
     5.5    undual_dual: "undual (dual x) = x"
     5.6  
     5.7 -instance dual :: (leq) leq
     5.8 -  by intro_classes
     5.9 +instance dual :: (leq) leq ..
    5.10  
    5.11  defs (overloaded)
    5.12    leq_dual_def: "x' \<sqsubseteq> y' \<equiv> undual y' \<sqsubseteq> undual x'"
    5.13 @@ -155,7 +154,7 @@
    5.14  *}
    5.15  
    5.16  instance dual :: (quasi_order) quasi_order
    5.17 -proof intro_classes
    5.18 +proof
    5.19    fix x' y' z' :: "'a::quasi_order dual"
    5.20    have "undual x' \<sqsubseteq> undual x'" .. thus "x' \<sqsubseteq> x'" ..
    5.21    assume "y' \<sqsubseteq> z'" hence "undual z' \<sqsubseteq> undual y'" ..
    5.22 @@ -164,7 +163,7 @@
    5.23  qed
    5.24  
    5.25  instance dual :: (partial_order) partial_order
    5.26 -proof intro_classes
    5.27 +proof
    5.28    fix x' y' :: "'a::partial_order dual"
    5.29    assume "y' \<sqsubseteq> x'" hence "undual x' \<sqsubseteq> undual y'" ..
    5.30    also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..
    5.31 @@ -172,7 +171,7 @@
    5.32  qed
    5.33  
    5.34  instance dual :: (linear_order) linear_order
    5.35 -proof intro_classes
    5.36 +proof
    5.37    fix x' y' :: "'a::linear_order dual"
    5.38    show "x' \<sqsubseteq> y' \<or> y' \<sqsubseteq> x'"
    5.39    proof (rule linear_order_cases)
    5.40 @@ -193,8 +192,7 @@
    5.41    \emph{not} be linear in general.
    5.42  *}
    5.43  
    5.44 -instance * :: (leq, leq) leq
    5.45 -  by intro_classes
    5.46 +instance * :: (leq, leq) leq ..
    5.47  
    5.48  defs (overloaded)
    5.49    leq_prod_def: "p \<sqsubseteq> q \<equiv> fst p \<sqsubseteq> fst q \<and> snd p \<sqsubseteq> snd q"
    5.50 @@ -208,7 +206,7 @@
    5.51    by (unfold leq_prod_def) blast
    5.52  
    5.53  instance * :: (quasi_order, quasi_order) quasi_order
    5.54 -proof intro_classes
    5.55 +proof
    5.56    fix p q r :: "'a::quasi_order \<times> 'b::quasi_order"
    5.57    show "p \<sqsubseteq> p"
    5.58    proof
    5.59 @@ -228,7 +226,7 @@
    5.60  qed
    5.61  
    5.62  instance * :: (partial_order, partial_order) partial_order
    5.63 -proof intro_classes
    5.64 +proof
    5.65    fix p q :: "'a::partial_order \<times> 'b::partial_order"
    5.66    assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"
    5.67    show "p = q"
    5.68 @@ -251,8 +249,7 @@
    5.69    orders need \emph{not} be linear in general.
    5.70  *}
    5.71  
    5.72 -instance fun :: ("term", leq) leq
    5.73 -  by intro_classes
    5.74 +instance fun :: ("term", leq) leq ..
    5.75  
    5.76  defs (overloaded)
    5.77    leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
    5.78 @@ -264,7 +261,7 @@
    5.79    by (unfold leq_fun_def) blast
    5.80  
    5.81  instance fun :: ("term", quasi_order) quasi_order
    5.82 -proof intro_classes
    5.83 +proof
    5.84    fix f g h :: "'a \<Rightarrow> 'b::quasi_order"
    5.85    show "f \<sqsubseteq> f"
    5.86    proof
    5.87 @@ -280,7 +277,7 @@
    5.88  qed
    5.89  
    5.90  instance fun :: ("term", partial_order) partial_order
    5.91 -proof intro_classes
    5.92 +proof
    5.93    fix f g :: "'a \<Rightarrow> 'b::partial_order"
    5.94    assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"
    5.95    show "f = g"
     6.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 23 22:09:52 2000 +0200
     6.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 23 22:10:36 2000 +0200
     6.3 @@ -212,7 +212,7 @@
     6.4  text {* The \emph{sum} of two vectorspaces $U$ and $V$ is the set of
     6.5  all sums of elements from $U$ and $V$. *}
     6.6  
     6.7 -instance set :: (plus) plus by intro_classes
     6.8 +instance set :: (plus) plus ..
     6.9  
    6.10  defs vs_sum_def:
    6.11    "U + V == {u + v | u v. u \<in> U \<and> v \<in> V}" (***
     7.1 --- a/src/HOL/Real/RealPow.thy	Mon Oct 23 22:09:52 2000 +0200
     7.2 +++ b/src/HOL/Real/RealPow.thy	Mon Oct 23 22:10:36 2000 +0200
     7.3 @@ -12,8 +12,7 @@
     7.4  lemmas [arith_split] = abs_split
     7.5  
     7.6  
     7.7 -instance real :: power
     7.8 -  by intro_classes
     7.9 +instance real :: power ..
    7.10  
    7.11  primrec (realpow)
    7.12       realpow_0:   "r ^ 0       = #1"
     8.1 --- a/src/HOL/Record.thy	Mon Oct 23 22:09:52 2000 +0200
     8.2 +++ b/src/HOL/Record.thy	Mon Oct 23 22:10:36 2000 +0200
     8.3 @@ -51,8 +51,7 @@
     8.4  (* type class for record extensions *)
     8.5  
     8.6  axclass more < "term"
     8.7 -instance unit :: more
     8.8 -  by intro_classes
     8.9 +instance unit :: more ..
    8.10  
    8.11  
    8.12  (* initialize the package *)
     9.1 --- a/src/Provers/classical.ML	Mon Oct 23 22:09:52 2000 +0200
     9.2 +++ b/src/Provers/classical.ML	Mon Oct 23 22:10:36 2000 +0200
     9.3 @@ -1111,8 +1111,12 @@
     9.4  fun rule_tac [] cs facts = some_rule_tac cs facts
     9.5    | rule_tac rules _ facts = Method.rule_tac rules facts;
     9.6  
     9.7 +fun default_tac rules cs facts =
     9.8 +  rule_tac rules cs facts ORELSE' AxClass.default_intro_classes_tac facts;
     9.9 +
    9.10  in
    9.11    val rule = METHOD_CLASET' o rule_tac;
    9.12 +  val default = METHOD_CLASET' o default_tac;
    9.13  end;
    9.14  
    9.15  
    9.16 @@ -1169,7 +1173,7 @@
    9.17  (** setup_methods **)
    9.18  
    9.19  val setup_methods = Method.add_methods
    9.20 - [("default", Method.thms_ctxt_args rule, "apply some rule (classical)"),
    9.21 + [("default", Method.thms_ctxt_args default, "apply some rule (classical)"),
    9.22    ("rule", Method.thms_ctxt_args rule, "apply some rule (classical)"),
    9.23    ("contradiction", Method.no_args contradiction, "proof by contradiction"),
    9.24    ("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"),
    10.1 --- a/src/Pure/Isar/method.ML	Mon Oct 23 22:09:52 2000 +0200
    10.2 +++ b/src/Pure/Isar/method.ML	Mon Oct 23 22:10:36 2000 +0200
    10.3 @@ -48,6 +48,7 @@
    10.4      -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq
    10.5    val rule_tac: thm list -> thm list -> int -> tactic
    10.6    val erule_tac: thm list -> thm list -> int -> tactic
    10.7 +  val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
    10.8    val rule: thm list -> Proof.method
    10.9    val erule: thm list -> Proof.method
   10.10    val drule: thm list -> Proof.method
   10.11 @@ -323,14 +324,15 @@
   10.12  fun gen_rule_tac tac rules [] = tac rules
   10.13    | gen_rule_tac tac erules facts = gen_resolveq_tac (tac o single) (multi_resolves facts erules);
   10.14  
   10.15 -fun gen_rule tac rules = METHOD (HEADGOAL o tac rules);
   10.16 -
   10.17 -fun gen_rule' tac arg_rules ctxt = METHOD (fn facts =>
   10.18 +fun gen_some_rule_tac tac arg_rules ctxt facts =
   10.19    let val rules =
   10.20      if not (null arg_rules) then arg_rules
   10.21      else if null facts then #1 (LocalRules.get ctxt)
   10.22      else op @ (LocalRules.get ctxt);
   10.23 -  in HEADGOAL (tac rules facts) end);
   10.24 +  in tac rules facts end;
   10.25 +
   10.26 +fun gen_rule tac rules = METHOD (HEADGOAL o tac rules);
   10.27 +fun gen_rule' tac arg_rules ctxt = METHOD (HEADGOAL o gen_some_rule_tac tac arg_rules ctxt);
   10.28  
   10.29  fun setup raw_tac =
   10.30    let val tac = gen_rule_tac raw_tac
   10.31 @@ -338,6 +340,7 @@
   10.32  
   10.33  in
   10.34  
   10.35 +val some_rule_tac = gen_some_rule_tac (gen_rule_tac Tactic.resolve_tac);
   10.36  val (rule_tac, rule, some_rule) = setup Tactic.resolve_tac;
   10.37  val (erule_tac, erule, some_erule) = setup Tactic.eresolve_tac;
   10.38  val (drule_tac, drule, some_drule) = setup Tactic.dresolve_tac;
   10.39 @@ -648,7 +651,6 @@
   10.40    ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
   10.41    ("unfold", thms_args unfold, "unfold definitions"),
   10.42    ("fold", thms_args fold, "fold definitions"),
   10.43 -  ("default", thms_ctxt_args some_rule, "apply some rule"),
   10.44    ("rule", thms_ctxt_args some_rule, "apply some rule"),
   10.45    ("erule", thms_ctxt_args some_erule, "apply some rule in elimination manner (improper)"),
   10.46    ("drule", thms_ctxt_args some_drule, "apply some rule in destruct manner (improper)"),
    11.1 --- a/src/Pure/axclass.ML	Mon Oct 23 22:09:52 2000 +0200
    11.2 +++ b/src/Pure/axclass.ML	Mon Oct 23 22:10:36 2000 +0200
    11.3 @@ -23,6 +23,7 @@
    11.4      -> thm list -> tactic option -> theory -> theory
    11.5    val add_inst_arity_i: string * sort list * sort -> string list
    11.6      -> thm list -> tactic option -> theory -> theory
    11.7 +  val default_intro_classes_tac: thm list -> int -> tactic
    11.8    val axclass_tac: thm list -> tactic
    11.9    val prove_subclass: theory -> class * class -> thm list
   11.10      -> tactic option -> thm
   11.11 @@ -306,15 +307,27 @@
   11.12  
   11.13  (* intro_classes *)
   11.14  
   11.15 -fun intro_classes_tac facts st =
   11.16 -  HEADGOAL (Method.insert_tac facts THEN'
   11.17 -      REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) st;
   11.18 +fun intro_classes_tac facts i st =
   11.19 +  (Method.insert_tac facts THEN'
   11.20 +    REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) i st;
   11.21  
   11.22  val intro_classes_method =
   11.23 -  ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   11.24 +  ("intro_classes", Method.no_args (Method.METHOD (HEADGOAL o intro_classes_tac)),
   11.25      "back-chain introduction rules of axiomatic type classes");
   11.26  
   11.27  
   11.28 +(* default method *)
   11.29 +
   11.30 +fun default_intro_classes_tac [] = intro_classes_tac []
   11.31 +  | default_intro_classes_tac _ = K Tactical.no_tac;    (*no error message!*)
   11.32 +
   11.33 +fun default_tac rules ctxt facts =
   11.34 +  HEADGOAL (Method.some_rule_tac rules ctxt facts ORELSE' default_intro_classes_tac facts);
   11.35 +
   11.36 +val default_method =
   11.37 +  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some rule")
   11.38 +
   11.39 +
   11.40  (* axclass_tac *)
   11.41  
   11.42  (*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
   11.43 @@ -327,7 +340,7 @@
   11.44      val defs = filter is_def thms;
   11.45      val non_defs = filter_out is_def thms;
   11.46    in
   11.47 -    intro_classes_tac [] THEN
   11.48 +    HEADGOAL (intro_classes_tac []) THEN
   11.49      TRY (rewrite_goals_tac defs) THEN
   11.50      TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
   11.51    end;
   11.52 @@ -442,7 +455,7 @@
   11.53  
   11.54  val setup =
   11.55   [AxclassesData.init,
   11.56 -  Method.add_methods [intro_classes_method]];
   11.57 +  Method.add_methods [intro_classes_method, default_method]];
   11.58  
   11.59  
   11.60  (* outer syntax *)