src/HOL/Calculation.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8855 ef4848bb0696
child 9035 371f023d3dbd
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
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
2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff changeset
     4
6873
wenzelm
parents: 6863
diff changeset
     5
Setup transitivity rules for calculational proofs.  Note that in the
wenzelm
parents: 6863
diff changeset
     6
list below later rules have priority.
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
8855
ef4848bb0696 base on IntArith instead of Int (in order to leave out deleted simproc!);
wenzelm
parents: 8301
diff changeset
     9
theory Calculation = IntArith:;
6779
2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff changeset
    10
8301
d9345bad5e5c theorems [trans] = rev_mp mp;
wenzelm
parents: 8229
diff changeset
    11
theorems [trans] = rev_mp mp;
6945
eeeef70c8fe3 added HOL.trans;
wenzelm
parents: 6873
diff changeset
    12
7381
wenzelm
parents: 7202
diff changeset
    13
theorem [trans]: "[| s = t; P t |] ==> P s"; 		    (*  =  x  x  *)
wenzelm
parents: 7202
diff changeset
    14
  by (rule ssubst);
6873
wenzelm
parents: 6863
diff changeset
    15
7381
wenzelm
parents: 7202
diff changeset
    16
theorem [trans]: "[| P s; s = t |] ==> P t";		    (*  x  =  x  *)
wenzelm
parents: 7202
diff changeset
    17
  by (rule subst);
wenzelm
parents: 7202
diff changeset
    18
wenzelm
parents: 7202
diff changeset
    19
theorems [trans] = dvd_trans;                               (* dvd dvd dvd *)
7202
6fcaf006cc40 added asym rule;
wenzelm
parents: 6945
diff changeset
    20
7657
dbbf7721126e subsetD;
wenzelm
parents: 7561
diff changeset
    21
theorem [trans]: "[| c:A; A <= B |] ==> c:B";
dbbf7721126e subsetD;
wenzelm
parents: 7561
diff changeset
    22
  by (rule subsetD);
dbbf7721126e subsetD;
wenzelm
parents: 7561
diff changeset
    23
dbbf7721126e subsetD;
wenzelm
parents: 7561
diff changeset
    24
theorem [trans]: "[| A <= B; c:A |] ==> c:B";
dbbf7721126e subsetD;
wenzelm
parents: 7561
diff changeset
    25
  by (rule subsetD);
dbbf7721126e subsetD;
wenzelm
parents: 7561
diff changeset
    26
7561
ff8dbd0589aa added some ~= rules;
wenzelm
parents: 7381
diff changeset
    27
theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y";     (*  ~=  <=  < *)
ff8dbd0589aa added some ~= rules;
wenzelm
parents: 7381
diff changeset
    28
  by (simp! add: order_less_le);
ff8dbd0589aa added some ~= rules;
wenzelm
parents: 7381
diff changeset
    29
ff8dbd0589aa added some ~= rules;
wenzelm
parents: 7381
diff changeset
    30
theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y";     (*  <=  ~=  < *)
ff8dbd0589aa added some ~= rules;
wenzelm
parents: 7381
diff changeset
    31
  by (simp! add: order_less_le);
ff8dbd0589aa added some ~= rules;
wenzelm
parents: 7381
diff changeset
    32
7202
6fcaf006cc40 added asym rule;
wenzelm
parents: 6945
diff changeset
    33
theorem [trans]: "[| (x::'a::order) < y; y < x |] ==> P";   (*  <  >  P  *)
7381
wenzelm
parents: 7202
diff changeset
    34
  by (rule order_less_asym);
6873
wenzelm
parents: 6863
diff changeset
    35
7381
wenzelm
parents: 7202
diff changeset
    36
theorems [trans] = order_less_trans;                        (*  <  <  <  *)
wenzelm
parents: 7202
diff changeset
    37
theorems [trans] = order_le_less_trans;                     (*  <= <  <  *)
wenzelm
parents: 7202
diff changeset
    38
theorems [trans] = order_less_le_trans;                     (*  <  <= <  *)
wenzelm
parents: 7202
diff changeset
    39
theorems [trans] = order_trans;                             (*  <= <= <= *)
wenzelm
parents: 7202
diff changeset
    40
theorems [trans] = order_antisym;                           (*  <= >= =  *)
6862
f80091bdc992 more robust trans rules;
wenzelm
parents: 6791
diff changeset
    41
7202
6fcaf006cc40 added asym rule;
wenzelm
parents: 6945
diff changeset
    42
theorem [trans]: "[| x <= y; y = z |] ==> x <= z";	    (*  <= =  <= *)
7381
wenzelm
parents: 7202
diff changeset
    43
  by (rule subst);
6779
2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff changeset
    44
7202
6fcaf006cc40 added asym rule;
wenzelm
parents: 6945
diff changeset
    45
theorem [trans]: "[| x = y; y <= z |] ==> x <= z";	    (*  =  <= <= *)
7381
wenzelm
parents: 7202
diff changeset
    46
  by (rule ssubst);
6862
f80091bdc992 more robust trans rules;
wenzelm
parents: 6791
diff changeset
    47
7202
6fcaf006cc40 added asym rule;
wenzelm
parents: 6945
diff changeset
    48
theorem [trans]: "[| x < y; y = z |] ==> x < z";	    (*  <  =  <  *)
7381
wenzelm
parents: 7202
diff changeset
    49
  by (rule subst);
6779
2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff changeset
    50
7202
6fcaf006cc40 added asym rule;
wenzelm
parents: 6945
diff changeset
    51
theorem [trans]: "[| x = y; y < z |] ==> x < z";	    (*  =  <  <  *)
7381
wenzelm
parents: 7202
diff changeset
    52
  by (rule ssubst);
6779
2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff changeset
    53
7381
wenzelm
parents: 7202
diff changeset
    54
theorems [trans] = trans                                    (*  =  =  =  *)
6945
eeeef70c8fe3 added HOL.trans;
wenzelm
parents: 6873
diff changeset
    55
8229
38f453607c61 theorems [elim??] = sym;
wenzelm
parents: 7657
diff changeset
    56
theorems [elim??] = sym
38f453607c61 theorems [elim??] = sym;
wenzelm
parents: 7657
diff changeset
    57
6779
2912aff958bd Calculation.thy: Setup transitivity rules for calculational proofs.
wenzelm
parents:
diff changeset
    58
6862
f80091bdc992 more robust trans rules;
wenzelm
parents: 6791
diff changeset
    59
end;