src/HOL/Calculation.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10311 3b53ed2c846f
child 11089 0f6f1cd500e5
permissions -rw-r--r--
improved theory reference in comment
     1 (*  Title:      HOL/Calculation.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Setup transitivity rules for calculational proofs.
     7 *)
     8 
     9 theory Calculation = IntArith:
    10 
    11 lemma forw_subst: "a = b ==> P b ==> P a"
    12   by (rule ssubst)
    13 
    14 lemma back_subst: "P a ==> a = b ==> P b"
    15   by (rule subst)
    16 
    17 lemma set_rev_mp: "x:A ==> A <= B ==> x:B"
    18   by (rule subsetD)
    19 
    20 lemma set_mp: "A <= B ==> x:A ==> x:B"
    21   by (rule subsetD)
    22 
    23 lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
    24   by (simp add: order_less_le)
    25 
    26 lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b"
    27   by (simp add: order_less_le)
    28 
    29 lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P"
    30   by (rule order_less_asym)
    31 
    32 lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
    33   by (rule subst)
    34 
    35 lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
    36   by (rule ssubst)
    37 
    38 lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"
    39   by (rule subst)
    40 
    41 lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"
    42   by (rule ssubst)
    43 
    44 lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
    45   (!!x y. x < y ==> f x < f y) ==> f a < c"
    46 proof -
    47   assume r: "!!x y. x < y ==> f x < f y"
    48   assume "a < b" hence "f a < f b" by (rule r)
    49   also assume "f b < c"
    50   finally (order_less_trans) show ?thesis .
    51 qed
    52 
    53 lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
    54   (!!x y. x < y ==> f x < f y) ==> a < f c"
    55 proof -
    56   assume r: "!!x y. x < y ==> f x < f y"
    57   assume "a < f b"
    58   also assume "b < c" hence "f b < f c" by (rule r)
    59   finally (order_less_trans) show ?thesis .
    60 qed
    61 
    62 lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
    63   (!!x y. x <= y ==> f x <= f y) ==> f a < c"
    64 proof -
    65   assume r: "!!x y. x <= y ==> f x <= f y"
    66   assume "a <= b" hence "f a <= f b" by (rule r)
    67   also assume "f b < c"
    68   finally (order_le_less_trans) show ?thesis .
    69 qed
    70 
    71 lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
    72   (!!x y. x < y ==> f x < f y) ==> a < f c"
    73 proof -
    74   assume r: "!!x y. x < y ==> f x < f y"
    75   assume "a <= f b"
    76   also assume "b < c" hence "f b < f c" by (rule r)
    77   finally (order_le_less_trans) show ?thesis .
    78 qed
    79 
    80 lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
    81   (!!x y. x < y ==> f x < f y) ==> f a < c"
    82 proof -
    83   assume r: "!!x y. x < y ==> f x < f y"
    84   assume "a < b" hence "f a < f b" by (rule r)
    85   also assume "f b <= c"
    86   finally (order_less_le_trans) show ?thesis .
    87 qed
    88 
    89 lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
    90   (!!x y. x <= y ==> f x <= f y) ==> a < f c"
    91 proof -
    92   assume r: "!!x y. x <= y ==> f x <= f y"
    93   assume "a < f b"
    94   also assume "b <= c" hence "f b <= f c" by (rule r)
    95   finally (order_less_le_trans) show ?thesis .
    96 qed
    97 
    98 lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
    99   (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
   100 proof -
   101   assume r: "!!x y. x <= y ==> f x <= f y"
   102   assume "a <= f b"
   103   also assume "b <= c" hence "f b <= f c" by (rule r)
   104   finally (order_trans) show ?thesis .
   105 qed
   106 
   107 lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>
   108   (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
   109 proof -
   110   assume r: "!!x y. x <= y ==> f x <= f y"
   111   assume "a <= b" hence "f a <= f b" by (rule r)
   112   also assume "f b <= c"
   113   finally (order_trans) show ?thesis .
   114 qed
   115 
   116 lemma ord_le_eq_subst: "a <= b ==> f b = c ==>
   117   (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
   118 proof -
   119   assume r: "!!x y. x <= y ==> f x <= f y"
   120   assume "a <= b" hence "f a <= f b" by (rule r)
   121   also assume "f b = c"
   122   finally (ord_le_eq_trans) show ?thesis .
   123 qed
   124 
   125 lemma ord_eq_le_subst: "a = f b ==> b <= c ==>
   126   (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
   127 proof -
   128   assume r: "!!x y. x <= y ==> f x <= f y"
   129   assume "a = f b"
   130   also assume "b <= c" hence "f b <= f c" by (rule r)
   131   finally (ord_eq_le_trans) show ?thesis .
   132 qed
   133 
   134 lemma ord_less_eq_subst: "a < b ==> f b = c ==>
   135   (!!x y. x < y ==> f x < f y) ==> f a < c"
   136 proof -
   137   assume r: "!!x y. x < y ==> f x < f y"
   138   assume "a < b" hence "f a < f b" by (rule r)
   139   also assume "f b = c"
   140   finally (ord_less_eq_trans) show ?thesis .
   141 qed
   142 
   143 lemma ord_eq_less_subst: "a = f b ==> b < c ==>
   144   (!!x y. x < y ==> f x < f y) ==> a < f c"
   145 proof -
   146   assume r: "!!x y. x < y ==> f x < f y"
   147   assume "a = f b"
   148   also assume "b < c" hence "f b < f c" by (rule r)
   149   finally (ord_eq_less_trans) show ?thesis .
   150 qed
   151 
   152 text {*
   153   Note that this list of rules is in reverse order of priorities.
   154 *}
   155 
   156 lemmas basic_trans_rules [trans] =
   157   order_less_subst2
   158   order_less_subst1
   159   order_le_less_subst2
   160   order_le_less_subst1
   161   order_less_le_subst2
   162   order_less_le_subst1
   163   order_subst2
   164   order_subst1
   165   ord_le_eq_subst
   166   ord_eq_le_subst
   167   ord_less_eq_subst
   168   ord_eq_less_subst
   169   forw_subst
   170   back_subst
   171   dvd_trans
   172   rev_mp
   173   mp
   174   set_rev_mp
   175   set_mp
   176   order_neq_le_trans
   177   order_le_neq_trans
   178   order_less_asym'
   179   order_less_trans
   180   order_le_less_trans
   181   order_less_le_trans
   182   order_trans
   183   order_antisym
   184   ord_le_eq_trans
   185   ord_eq_le_trans
   186   ord_less_eq_trans
   187   ord_eq_less_trans
   188   trans
   189   transitive
   190 
   191 end