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
```