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.4    by (simp add: max_def)
     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