src/HOL/Relation_Power.thy
author nipkow
Mon, 01 Sep 2008 22:10:42 +0200
changeset 28072 a45e8c872dc1
parent 26799 5bd38256ce5b
child 28517 dd46786d4f95
permissions -rw-r--r--
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Relation_Power.thy
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     4
    Copyright   1996  TU Muenchen
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
     5
*)
11306
6f4ed75b2dca added comments
nipkow
parents: 11305
diff changeset
     6
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
     7
header{*Powers of Relations and Functions*}
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     8
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15112
diff changeset
     9
theory Relation_Power
26072
f65a7fa2da6c <= and < on nat no longer depend on wellfounded relations
haftmann
parents: 25861
diff changeset
    10
imports Power Transitive_Closure
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15112
diff changeset
    11
begin
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    12
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    13
instance
26799
5bd38256ce5b Deleted instance "set :: (type) power" and moved instance
berghofe
parents: 26072
diff changeset
    14
  "fun" :: (type, type) power ..
5bd38256ce5b Deleted instance "set :: (type) power" and moved instance
berghofe
parents: 26072
diff changeset
    15
      --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    16
25861
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    17
overloading
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    18
  relpow \<equiv> "power \<Colon> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set"  (unchecked)
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    19
begin
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    20
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    21
text {* @{text "R ^ n = R O ... O R"}, the n-fold composition of @{text R} *}
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    22
25861
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    23
primrec relpow where
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    24
  "(R \<Colon> ('a \<times> 'a) set)  ^ 0 = Id"
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    25
  | "(R \<Colon> ('a \<times> 'a) set) ^ Suc n = R O (R ^ n)"
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    26
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    27
end
11305
2ce86fccc95b added ^ on functions.
nipkow
parents: 10213
diff changeset
    28
25861
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    29
overloading
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    30
  funpow \<equiv> "power \<Colon>  ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (unchecked)
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    31
begin
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    32
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    33
text {* @{text "f ^ n = f o ... o f"}, the n-fold composition of @{text f} *}
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    34
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    35
primrec funpow where
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    36
  "(f \<Colon> 'a \<Rightarrow> 'a) ^ 0 = id"
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    37
  | "(f \<Colon> 'a \<Rightarrow> 'a) ^ Suc n = f o (f ^ n)"
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    38
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    39
end
11305
2ce86fccc95b added ^ on functions.
nipkow
parents: 10213
diff changeset
    40
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    41
text{*WARNING: due to the limits of Isabelle's type classes, exponentiation on
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    42
functions and relations has too general a domain, namely @{typ "('a * 'b)set"}
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    43
and @{typ "'a => 'b"}.  Explicit type constraints may therefore be necessary.
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    44
For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    45
constraints.*}
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    46
21414
4cb808163adc workaround for definition violating type discipline
haftmann
parents: 20503
diff changeset
    47
text {*
4cb808163adc workaround for definition violating type discipline
haftmann
parents: 20503
diff changeset
    48
  Circumvent this problem for code generation:
4cb808163adc workaround for definition violating type discipline
haftmann
parents: 20503
diff changeset
    49
*}
4cb808163adc workaround for definition violating type discipline
haftmann
parents: 20503
diff changeset
    50
25861
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    51
primrec
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    52
  fun_pow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
22737
haftmann
parents: 21414
diff changeset
    53
where
25861
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    54
  "fun_pow 0 f = id"
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    55
  | "fun_pow (Suc n) f = f o fun_pow n f"
21414
4cb808163adc workaround for definition violating type discipline
haftmann
parents: 20503
diff changeset
    56
25861
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    57
lemma funpow_fun_pow [code inline]: "f ^ n = fun_pow n f"
494d9301cc75 refined overloading target
haftmann
parents: 25295
diff changeset
    58
  unfolding funpow_def fun_pow_def ..
21414
4cb808163adc workaround for definition violating type discipline
haftmann
parents: 20503
diff changeset
    59
15112
6f0772a94299 added a thm
nipkow
parents: 12338
diff changeset
    60
lemma funpow_add: "f ^ (m+n) = f^m o f^n"
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    61
  by (induct m) simp_all
15112
6f0772a94299 added a thm
nipkow
parents: 12338
diff changeset
    62
18049
156bba334c12 A few new lemmas
nipkow
parents: 15410
diff changeset
    63
lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
156bba334c12 A few new lemmas
nipkow
parents: 15410
diff changeset
    64
proof -
156bba334c12 A few new lemmas
nipkow
parents: 15410
diff changeset
    65
  have "f((f^n) x) = (f^(n+1)) x" by simp
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    66
  also have "\<dots>  = (f^n o f^1) x" by (simp only: funpow_add)
18049
156bba334c12 A few new lemmas
nipkow
parents: 15410
diff changeset
    67
  also have "\<dots> = (f^n)(f x)" by simp
156bba334c12 A few new lemmas
nipkow
parents: 15410
diff changeset
    68
  finally show ?thesis .
156bba334c12 A few new lemmas
nipkow
parents: 15410
diff changeset
    69
qed
156bba334c12 A few new lemmas
nipkow
parents: 15410
diff changeset
    70
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    71
lemma rel_pow_1 [simp]:
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    72
  fixes R :: "('a*'a)set"
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    73
  shows "R^1 = R"
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    74
  by simp
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    75
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    76
lemma rel_pow_0_I: "(x,x) : R^0"
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    77
  by simp
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    78
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    79
lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    80
  by auto
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    81
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    82
lemma rel_pow_Suc_I2:
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    83
    "(x, y) : R \<Longrightarrow> (y, z) : R^n \<Longrightarrow> (x,z) : R^(Suc n)"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 18398
diff changeset
    84
  apply (induct n arbitrary: z)
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    85
   apply simp
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    86
  apply fastsimp
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    87
  done
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    88
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    89
lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P"
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    90
  by simp
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    91
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    92
lemma rel_pow_Suc_E:
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    93
    "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    94
  by auto
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    95
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    96
lemma rel_pow_E:
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    97
    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
    98
        !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
    99
     |] ==> P"
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   100
  by (cases n) auto
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   101
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   102
lemma rel_pow_Suc_D2:
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   103
    "(x, z) : R^(Suc n) \<Longrightarrow> (\<exists>y. (x,y) : R & (y,z) : R^n)"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 18398
diff changeset
   104
  apply (induct n arbitrary: x z)
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   105
   apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   106
  apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   107
  done
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   108
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   109
lemma rel_pow_Suc_D2':
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   110
    "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   111
  by (induct n) (simp_all, blast)
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   112
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   113
lemma rel_pow_E2:
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   114
    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   115
        !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   116
     |] ==> P"
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   117
  apply (case_tac n, simp)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   118
  apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   119
  done
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   120
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   121
lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)"
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   122
  apply (simp only: split_tupled_all)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   123
  apply (erule rtrancl_induct)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   124
   apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   125
  done
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   126
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   127
lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*"
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   128
  apply (simp only: split_tupled_all)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   129
  apply (induct n)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   130
   apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   131
  apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   132
  done
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   133
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   134
lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   135
  by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   136
25295
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   137
lemma trancl_power:
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   138
  "x \<in> r^+ = (\<exists>n > 0. x \<in> r^n)"
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   139
  apply (cases x)
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   140
  apply simp
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   141
  apply (rule iffI)
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   142
   apply (drule tranclD2)
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   143
   apply (clarsimp simp: rtrancl_is_UN_rel_pow)
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   144
   apply (rule_tac x="Suc x" in exI)
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   145
   apply (clarsimp simp: rel_comp_def)
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   146
   apply fastsimp
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   147
  apply clarsimp
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   148
  apply (case_tac n, simp)
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   149
  apply clarsimp
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   150
  apply (drule rel_pow_imp_rtrancl)
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   151
  apply fastsimp
12985023be5e tranclD2 (tranclD at the other end) + trancl_power
kleing
parents: 24996
diff changeset
   152
  done
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   153
18398
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   154
lemma single_valued_rel_pow:
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   155
    "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   156
  apply (rule single_valuedI)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   157
  apply (induct n)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   158
   apply simp
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   159
  apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
5d63a8b35688 tuned proofs;
wenzelm
parents: 18049
diff changeset
   160
  done
15410
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   161
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   162
ML
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   163
{*
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   164
val funpow_add = thm "funpow_add";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   165
val rel_pow_1 = thm "rel_pow_1";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   166
val rel_pow_0_I = thm "rel_pow_0_I";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   167
val rel_pow_Suc_I = thm "rel_pow_Suc_I";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   168
val rel_pow_Suc_I2 = thm "rel_pow_Suc_I2";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   169
val rel_pow_0_E = thm "rel_pow_0_E";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   170
val rel_pow_Suc_E = thm "rel_pow_Suc_E";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   171
val rel_pow_E = thm "rel_pow_E";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   172
val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   173
val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   174
val rel_pow_E2 = thm "rel_pow_E2";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   175
val rtrancl_imp_UN_rel_pow = thm "rtrancl_imp_UN_rel_pow";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   176
val rel_pow_imp_rtrancl = thm "rel_pow_imp_rtrancl";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   177
val rtrancl_is_UN_rel_pow = thm "rtrancl_is_UN_rel_pow";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   178
val single_valued_rel_pow = thm "single_valued_rel_pow";
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   179
*}
18914688a5fd converted Relation_Power to new-style theory
paulson
parents: 15140
diff changeset
   180
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   181
end