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