src/HOL/HOL.thy
 changeset 14398 c5c47703f763 parent 14365 3d4df8c166ae child 14430 5cb24165a2e1
```     1.1 --- a/src/HOL/HOL.thy	Thu Feb 19 10:41:32 2004 +0100
1.2 +++ b/src/HOL/HOL.thy	Thu Feb 19 15:57:34 2004 +0100
1.3 @@ -946,6 +946,93 @@
1.5
1.6
1.7 +subsubsection {* Transitivity rules for calculational reasoning *}
1.8 +
1.9 +
1.10 +lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
1.11 +  by (simp add: order_less_le)
1.12 +
1.13 +lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
1.14 +  by (simp add: order_less_le)
1.15 +
1.16 +lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
1.17 +  by (rule order_less_asym)
1.18 +
1.19 +
1.20 +subsubsection {* Setup of transitivity reasoner *}
1.21 +
1.22 +lemma less_imp_neq: "[| (x::'a::order) < y |] ==> x ~= y"
1.23 +  by (erule contrapos_pn, erule subst, rule order_less_irrefl)
1.24 +
1.25 +lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
1.26 +  by (erule subst, erule ssubst, assumption)
1.27 +
1.28 +ML_setup {*
1.29 +
1.30 +structure Trans_Tac = Trans_Tac_Fun (
1.31 +  struct
1.32 +    val less_reflE = thm "order_less_irrefl" RS thm "notE";
1.33 +    val le_refl = thm "order_refl";
1.34 +    val less_imp_le = thm "order_less_imp_le";
1.35 +    val not_lessI = thm "linorder_not_less" RS thm "iffD2";
1.36 +    val not_leI = thm "linorder_not_le" RS thm "iffD2";
1.37 +    val not_lessD = thm "linorder_not_less" RS thm "iffD1";
1.38 +    val not_leD = thm "linorder_not_le" RS thm "iffD1";
1.39 +    val eqI = thm "order_antisym";
1.40 +    val eqD1 = thm "order_eq_refl";
1.41 +    val eqD2 = thm "sym" RS thm "order_eq_refl";
1.42 +    val less_trans = thm "order_less_trans";
1.43 +    val less_le_trans = thm "order_less_le_trans";
1.44 +    val le_less_trans = thm "order_le_less_trans";
1.45 +    val le_trans = thm "order_trans";
1.46 +    val le_neq_trans = thm "order_le_neq_trans";
1.47 +    val neq_le_trans = thm "order_neq_le_trans";
1.48 +    val less_imp_neq = thm "less_imp_neq";
1.49 +    val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
1.50 +
1.51 +    fun decomp_gen sort sign (Trueprop \$ t) =
1.52 +      let fun of_sort t = Sign.of_sort sign (type_of t, sort)
1.53 +      fun dec (Const ("Not", _) \$ t) = (
1.54 +              case dec t of
1.55 +                None => None
1.56 +              | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
1.57 +            | dec (Const ("op =",  _) \$ t1 \$ t2) =
1.58 +                if of_sort t1
1.59 +                then Some (t1, "=", t2)
1.60 +                else None
1.61 +            | dec (Const ("op <=",  _) \$ t1 \$ t2) =
1.62 +                if of_sort t1
1.63 +                then Some (t1, "<=", t2)
1.64 +                else None
1.65 +            | dec (Const ("op <",  _) \$ t1 \$ t2) =
1.66 +                if of_sort t1
1.67 +                then Some (t1, "<", t2)
1.68 +                else None
1.69 +            | dec _ = None
1.70 +      in dec t end;
1.71 +
1.72 +    val decomp_part = decomp_gen ["HOL.order"];
1.73 +    val decomp_lin = decomp_gen ["HOL.linorder"];
1.74 +
1.75 +  end);  (* struct *)
1.76 +
1.77 +Context.>> (fn thy => (simpset_ref_of thy :=
1.78 +  simpset_of thy
1.79 +    addSolver (mk_solver "Trans_linear" (fn _ => Trans_Tac.linear_tac))
1.80 +    addSolver (mk_solver "Trans_partial" (fn _ => Trans_Tac.partial_tac));
1.81 +  thy))
1.82 +*}
1.83 +
1.84 +(* Optional methods
1.85 +
1.86 +method_setup trans_partial =
1.87 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_partial)) *}
1.88 +  {* simple transitivity reasoner *}
1.89 +method_setup trans_linear =
1.90 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac_linear)) *}
1.91 +  {* simple transitivity reasoner *}
1.92 +*)
1.93 +
1.94  subsubsection "Bounded quantifiers"
1.95
1.96  syntax
```