src/HOL/Relation.ML
author paulson
Fri, 29 Oct 2004 15:16:02 +0200
changeset 15270 8b3f707a78a7
parent 13639 8ee6ea6627e1
permissions -rw-r--r--
fixed reference to renamed theorem
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
     1
12905
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
     2
(* legacy ML bindings *)
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
     3
12905
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
     4
val DomainE = thm "DomainE";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
     5
val DomainI = thm "DomainI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
     6
val Domain_Collect_split = thm "Domain_Collect_split";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
     7
val Domain_Diff_subset = thm "Domain_Diff_subset";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
     8
val Domain_Id = thm "Domain_Id";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
     9
val Domain_Int_subset = thm "Domain_Int_subset";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    10
val Domain_Un_eq = thm "Domain_Un_eq";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    11
val Domain_Union = thm "Domain_Union";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    12
val Domain_def = thm "Domain_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    13
val Domain_diag = thm "Domain_diag";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    14
val Domain_empty = thm "Domain_empty";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    15
val Domain_iff = thm "Domain_iff";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    16
val Domain_insert = thm "Domain_insert";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    17
val Domain_mono = thm "Domain_mono";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    18
val Field_def = thm "Field_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    19
val IdE = thm "IdE";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    20
val IdI = thm "IdI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    21
val Id_O_R = thm "Id_O_R";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    22
val Id_def = thm "Id_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    23
val ImageE = thm "ImageE";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    24
val ImageI = thm "ImageI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    25
val Image_Collect_split = thm "Image_Collect_split";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    26
val Image_INT_subset = thm "Image_INT_subset";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    27
val Image_Id = thm "Image_Id";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    28
val Image_Int_subset = thm "Image_Int_subset";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    29
val Image_UN = thm "Image_UN";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    30
val Image_Un = thm "Image_Un";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    31
val Image_def = thm "Image_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    32
val Image_diag = thm "Image_diag";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    33
val Image_empty = thm "Image_empty";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    34
val Image_eq_UN = thm "Image_eq_UN";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    35
val Image_iff = thm "Image_iff";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    36
val Image_mono = thm "Image_mono";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    37
val Image_singleton = thm "Image_singleton";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    38
val Image_singleton_iff = thm "Image_singleton_iff";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    39
val Image_subset = thm "Image_subset";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    40
val Image_subset_eq = thm "Image_subset_eq";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    41
val O_assoc = thm "O_assoc";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    42
val R_O_Id = thm "R_O_Id";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    43
val RangeE = thm "RangeE";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    44
val RangeI = thm "RangeI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    45
val Range_Collect_split = thm "Range_Collect_split";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    46
val Range_Diff_subset = thm "Range_Diff_subset";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    47
val Range_Id = thm "Range_Id";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    48
val Range_Int_subset = thm "Range_Int_subset";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    49
val Range_Un_eq = thm "Range_Un_eq";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    50
val Range_Union = thm "Range_Union";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    51
val Range_def = thm "Range_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    52
val Range_diag = thm "Range_diag";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    53
val Range_empty = thm "Range_empty";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    54
val Range_iff = thm "Range_iff";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    55
val Range_insert = thm "Range_insert";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    56
val antisymD = thm "antisymD";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    57
val antisymI = thm "antisymI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    58
val antisym_Id = thm "antisym_Id";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    59
val antisym_converse = thm "antisym_converse";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    60
val antisym_def = thm "antisym_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    61
val converseD = thm "converseD";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    62
val converseE = thm "converseE";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    63
val converseI = thm "converseI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    64
val converse_Id = thm "converse_Id";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    65
val converse_converse = thm "converse_converse";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    66
val converse_def = thm "converse_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    67
val converse_diag = thm "converse_diag";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    68
val converse_iff = thm "converse_iff";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    69
val converse_rel_comp = thm "converse_rel_comp";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    70
val diagE = thm "diagE";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    71
val diagI = thm "diagI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    72
val diag_def = thm "diag_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    73
val diag_eqI = thm "diag_eqI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    74
val diag_iff = thm "diag_iff";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    75
val diag_subset_Times = thm "diag_subset_Times";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    76
val inv_image_def = thm "inv_image_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    77
val pair_in_Id_conv = thm "pair_in_Id_conv";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    78
val reflD = thm "reflD";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    79
val reflI = thm "reflI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    80
val refl_converse = thm "refl_converse";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    81
val refl_def = thm "refl_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    82
val reflexive_Id = thm "reflexive_Id";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    83
val rel_compE = thm "rel_compE";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    84
val rel_compEpair = thm "rel_compEpair";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    85
val rel_compI = thm "rel_compI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    86
val rel_comp_def = thm "rel_comp_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    87
val rel_comp_mono = thm "rel_comp_mono";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    88
val rel_comp_subset_Sigma = thm "rel_comp_subset_Sigma";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    89
val rev_ImageI = thm "rev_ImageI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    90
val single_valuedD = thm "single_valuedD";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    91
val single_valuedI = thm "single_valuedI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    92
val single_valued_def = thm "single_valued_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    93
val sym_def = thm "sym_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    94
val transD = thm "transD";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    95
val transI = thm "transI";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    96
val trans_Id = thm "trans_Id";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    97
val trans_O_subset = thm "trans_O_subset";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    98
val trans_converse = thm "trans_converse";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
    99
val trans_def = thm "trans_def";
bbbae3f359e6 Converted to new theory format.
berghofe
parents: 12487
diff changeset
   100
val trans_inv_image = thm "trans_inv_image";