src/HOL/Transitive_Closure.ML
author berghofe
Wed, 13 Nov 2002 15:24:42 +0100
changeset 13704 854501b1e957
parent 12691 d21db58bcdc2
permissions -rw-r--r--
Transitive closure is now defined inductively as well.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12691
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
     1
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
     2
(* legacy ML bindings *)
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
     3
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
     4
val converse_rtranclE = thm "converse_rtranclE";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
     5
val converse_rtranclE2 = thm "converse_rtranclE2";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
     6
val converse_rtrancl_induct = thm "converse_rtrancl_induct";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
     7
val converse_rtrancl_induct2 = thm "converse_rtrancl_induct2";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
     8
val converse_rtrancl_into_rtrancl = thm "converse_rtrancl_into_rtrancl";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
     9
val converse_trancl_induct = thm "converse_trancl_induct";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    10
val irrefl_tranclI = thm "irrefl_tranclI";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    11
val irrefl_trancl_rD = thm "irrefl_trancl_rD";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    12
val r_comp_rtrancl_eq = thm "r_comp_rtrancl_eq";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    13
val r_into_rtrancl = thm "r_into_rtrancl";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    14
val r_into_trancl = thm "r_into_trancl";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    15
val rtranclE = thm "rtranclE";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    16
val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    17
val rtrancl_converse = thm "rtrancl_converse";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    18
val rtrancl_converseD = thm "rtrancl_converseD";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    19
val rtrancl_converseI = thm "rtrancl_converseI";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    20
val rtrancl_idemp = thm "rtrancl_idemp";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    21
val rtrancl_idemp_self_comp = thm "rtrancl_idemp_self_comp";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    22
val rtrancl_induct = thm "rtrancl_induct";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    23
val rtrancl_induct2 = thm "rtrancl_induct2";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    24
val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    25
val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    26
val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    27
val rtrancl_mono = thm "rtrancl_mono";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    28
val rtrancl_r_diff_Id = thm "rtrancl_r_diff_Id";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    29
val rtrancl_refl = thm "rtrancl_refl";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    30
val rtrancl_reflcl = thm "rtrancl_reflcl";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    31
val rtrancl_subset = thm "rtrancl_subset";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    32
val rtrancl_subset_rtrancl = thm "rtrancl_subset_rtrancl";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    33
val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    34
val rtrancl_trans = thm "rtrancl_trans";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    35
val tranclD = thm "tranclD";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    36
val tranclE = thm "tranclE";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    37
val trancl_converse = thm "trancl_converse";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    38
val trancl_converseD = thm "trancl_converseD";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    39
val trancl_converseI = thm "trancl_converseI";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    40
val trancl_induct = thm "trancl_induct";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    41
val trancl_insert = thm "trancl_insert";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    42
val trancl_into_rtrancl = thm "trancl_into_rtrancl";
13704
854501b1e957 Transitive closure is now defined inductively as well.
berghofe
parents: 12691
diff changeset
    43
val trancl_into_trancl = thm "trancl_into_trancl";
12691
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    44
val trancl_into_trancl2 = thm "trancl_into_trancl2";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    45
val trancl_mono = thm "trancl_mono";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    46
val trancl_subset_Sigma = thm "trancl_subset_Sigma";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    47
val trancl_trans = thm "trancl_trans";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    48
val trancl_trans_induct = thm "trancl_trans_induct";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    49
val trans_rtrancl = thm "trans_rtrancl";
d21db58bcdc2 converted theory Transitive_Closure;
wenzelm
parents:
diff changeset
    50
val trans_trancl = thm "trans_trancl";