src/HOL/HOL.thy
 changeset 15103 79846e8792eb parent 15079 2ef899e4526d child 15131 c69542757a4d
```     1.1 --- a/src/HOL/HOL.thy	Tue Aug 03 13:48:00 2004 +0200
1.2 +++ b/src/HOL/HOL.thy	Tue Aug 03 14:47:51 2004 +0200
1.3 @@ -986,7 +986,49 @@
1.4
1.5  ML_setup {*
1.6
1.7 -structure Trans_Tac = Trans_Tac_Fun (
1.8 +(* The setting up of Quasi_Tac serves as a demo.  Since there is no
1.9 +   class for quasi orders, the tactics Quasi_Tac.trans_tac and
1.10 +   Quasi_Tac.quasi_tac are not of much use. *)
1.11 +
1.12 +structure Quasi_Tac = Quasi_Tac_Fun (
1.13 +  struct
1.14 +    val le_trans = thm "order_trans";
1.15 +    val le_refl = thm "order_refl";
1.16 +    val eqD1 = thm "order_eq_refl";
1.17 +    val eqD2 = thm "sym" RS thm "order_eq_refl";
1.18 +    val less_reflE = thm "order_less_irrefl" RS thm "notE";
1.19 +    val less_imp_le = thm "order_less_imp_le";
1.20 +    val le_neq_trans = thm "order_le_neq_trans";
1.21 +    val neq_le_trans = thm "order_neq_le_trans";
1.22 +    val less_imp_neq = thm "less_imp_neq";
1.23 +
1.24 +    fun decomp_gen sort sign (Trueprop \$ t) =
1.25 +      let fun of_sort t = Sign.of_sort sign (type_of t, sort)
1.26 +      fun dec (Const ("Not", _) \$ t) = (
1.27 +              case dec t of
1.28 +                None => None
1.29 +              | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
1.30 +            | dec (Const ("op =",  _) \$ t1 \$ t2) =
1.31 +                if of_sort t1
1.32 +                then Some (t1, "=", t2)
1.33 +                else None
1.34 +            | dec (Const ("op <=",  _) \$ t1 \$ t2) =
1.35 +                if of_sort t1
1.36 +                then Some (t1, "<=", t2)
1.37 +                else None
1.38 +            | dec (Const ("op <",  _) \$ t1 \$ t2) =
1.39 +                if of_sort t1
1.40 +                then Some (t1, "<", t2)
1.41 +                else None
1.42 +            | dec _ = None
1.43 +      in dec t end;
1.44 +
1.45 +    val decomp_trans = decomp_gen ["HOL.order"];
1.46 +    val decomp_quasi = decomp_gen ["HOL.order"];
1.47 +
1.48 +  end);  (* struct *)
1.49 +
1.50 +structure Order_Tac = Order_Tac_Fun (
1.51    struct
1.52      val less_reflE = thm "order_less_irrefl" RS thm "notE";
1.53      val le_refl = thm "order_refl";
1.54 @@ -1034,26 +1076,29 @@
1.55    end);  (* struct *)
1.56
1.57  simpset_ref() := simpset ()
1.58 -    addSolver (mk_solver "Trans_linear" (fn _ => Trans_Tac.linear_tac))
1.59 -    addSolver (mk_solver "Trans_partial" (fn _ => Trans_Tac.partial_tac));
1.60 +    addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac))
1.61 +    addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac));
1.62    (* Adding the transitivity reasoners also as safe solvers showed a slight
1.63       speed up, but the reasoning strength appears to be not higher (at least
1.64       no breaking of additional proofs in the entire HOL distribution, as
1.65       of 5 March 2004, was observed). *)
1.66  *}
1.67
1.68 -(* Optional methods
1.69 +(* Optional setup of methods *)
1.70
1.71 +(*
1.72  method_setup trans_partial =
1.73 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_partial)) *}
1.74 -  {* simple transitivity reasoner *}
1.75 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.partial_tac)) *}
1.76 +  {* transitivity reasoner for partial orders *}
1.77  method_setup trans_linear =
1.78 -  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_linear)) *}
1.79 -  {* simple transitivity reasoner *}
1.80 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.linear_tac)) *}
1.81 +  {* transitivity reasoner for linear orders *}
1.82  *)
1.83
1.84  (*
1.85  declare order.order_refl [simp del] order_less_irrefl [simp del]
1.86 +
1.87 +can currently not be removed, abel_cancel relies on it.
1.88  *)
1.89
1.90  subsubsection "Bounded quantifiers"
```