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"