src/ZF/Trancl.thy
author wenzelm
Sun, 21 Mar 2010 19:28:25 +0100
changeset 35852 4e3fe0b8687b
parent 35762 af3ff2ba4c54
child 45602 2a858377c3d2
permissions -rw-r--r--
minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
     1
(*  Title:      ZF/Trancl.thy
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
     6
header{*Relations: Their General Properties and Transitive Closure*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14653
diff changeset
     8
theory Trancl imports Fixedpt Perm begin
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
     9
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    10
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    11
  refl     :: "[i,i]=>o"  where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    12
    "refl(A,r) == (ALL x: A. <x,x> : r)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    13
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    14
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    15
  irrefl   :: "[i,i]=>o"  where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    16
    "irrefl(A,r) == ALL x: A. <x,x> ~: r"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    17
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    18
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    19
  sym      :: "i=>o"  where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    20
    "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    21
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    22
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    23
  asym     :: "i=>o"  where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    24
    "asym(r) == ALL x y. <x,y>:r --> ~ <y,x>:r"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    25
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    26
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    27
  antisym  :: "i=>o"  where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    28
    "antisym(r) == ALL x y.<x,y>:r --> <y,x>:r --> x=y"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    29
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    30
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    31
  trans    :: "i=>o"  where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    32
    "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    33
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    34
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    35
  trans_on :: "[i,i]=>o"  ("trans[_]'(_')")  where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    36
    "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.       
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    37
                          <x,y>: r --> <y,z>: r --> <x,z>: r"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    38
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    39
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    40
  rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)  where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    41
    "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    42
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    43
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    44
  trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)  where
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    45
    "r^+ == r O r^*"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    46
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    47
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    48
  equiv    :: "[i,i]=>o"  where
14653
0848ab6fe5fc constdefs: proper order;
wenzelm
parents: 13784
diff changeset
    49
    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
0848ab6fe5fc constdefs: proper order;
wenzelm
parents: 13784
diff changeset
    50
0848ab6fe5fc constdefs: proper order;
wenzelm
parents: 13784
diff changeset
    51
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    52
subsection{*General properties of relations*}
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    53
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    54
subsubsection{*irreflexivity*}
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    55
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    56
lemma irreflI:
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    57
    "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
    58
by (simp add: irrefl_def) 
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    59
13534
ca6debb89d77 avoid duplicate fact bindings;
wenzelm
parents: 13357
diff changeset
    60
lemma irreflE: "[| irrefl(A,r);  x:A |] ==>  <x,x> ~: r"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
    61
by (simp add: irrefl_def)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    62
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    63
subsubsection{*symmetry*}
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    64
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    65
lemma symI:
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    66
     "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    67
by (unfold sym_def, blast) 
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    68
13534
ca6debb89d77 avoid duplicate fact bindings;
wenzelm
parents: 13357
diff changeset
    69
lemma symE: "[| sym(r); <x,y>: r |]  ==>  <y,x>: r"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
    70
by (unfold sym_def, blast)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    71
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    72
subsubsection{*antisymmetry*}
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    73
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    74
lemma antisymI:
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    75
     "[| !!x y.[| <x,y>: r;  <y,x>: r |] ==> x=y |] ==> antisym(r)"
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    76
by (simp add: antisym_def, blast) 
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    77
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    78
lemma antisymE: "[| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
    79
by (simp add: antisym_def, blast)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    80
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    81
subsubsection{*transitivity*}
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    82
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    83
lemma transD: "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
    84
by (unfold trans_def, blast)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    85
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    86
lemma trans_onD: 
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    87
    "[| trans[A](r);  <a,b>:r;  <b,c>:r;  a:A;  b:A;  c:A |] ==> <a,c>:r"
13243
ba53d07d32d5 new lemmas
paulson
parents: 13240
diff changeset
    88
by (unfold trans_on_def, blast)
ba53d07d32d5 new lemmas
paulson
parents: 13240
diff changeset
    89
ba53d07d32d5 new lemmas
paulson
parents: 13240
diff changeset
    90
lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
ba53d07d32d5 new lemmas
paulson
parents: 13240
diff changeset
    91
by (unfold trans_def trans_on_def, blast)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    92
13248
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
    93
lemma trans_on_imp_trans: "[|trans[A](r); r <= A*A|] ==> trans(r)";
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
    94
by (simp add: trans_on_def trans_def, blast)
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
    95
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
    96
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    97
subsection{*Transitive closure of a relation*}
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    98
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
    99
lemma rtrancl_bnd_mono:
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   100
     "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))"
13248
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   101
by (rule bnd_monoI, blast+)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   102
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   103
lemma rtrancl_mono: "r<=s ==> r^* <= s^*"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   104
apply (unfold rtrancl_def)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   105
apply (rule lfp_mono)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   106
apply (rule rtrancl_bnd_mono)+
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
   107
apply blast 
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   108
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   109
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   110
(* r^* = id(field(r)) Un ( r O r^* )    *)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   111
lemmas rtrancl_unfold =
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   112
     rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold], standard]
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   113
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   114
(** The relation rtrancl **)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   115
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   116
(*  r^* <= field(r) * field(r)  *)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   117
lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset, standard]
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   118
13248
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   119
lemma relation_rtrancl: "relation(r^*)"
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   120
apply (simp add: relation_def) 
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   121
apply (blast dest: rtrancl_type [THEN subsetD]) 
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   122
done
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   123
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   124
(*Reflexivity of rtrancl*)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   125
lemma rtrancl_refl: "[| a: field(r) |] ==> <a,a> : r^*"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   126
apply (rule rtrancl_unfold [THEN ssubst])
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   127
apply (erule idI [THEN UnI1])
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   128
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   129
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   130
(*Closure under composition with r  *)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   131
lemma rtrancl_into_rtrancl: "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   132
apply (rule rtrancl_unfold [THEN ssubst])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13248
diff changeset
   133
apply (rule compI [THEN UnI2], assumption, assumption)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   134
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   135
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   136
(*rtrancl of r contains all pairs in r  *)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   137
lemma r_into_rtrancl: "<a,b> : r ==> <a,b> : r^*"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
   138
by (rule rtrancl_refl [THEN rtrancl_into_rtrancl], blast+)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   139
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   140
(*The premise ensures that r consists entirely of pairs*)
13248
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   141
lemma r_subset_rtrancl: "relation(r) ==> r <= r^*"
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   142
by (simp add: relation_def, blast intro: r_into_rtrancl)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   143
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   144
lemma rtrancl_field: "field(r^*) = field(r)"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
   145
by (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD])
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   146
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   147
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   148
(** standard induction rule **)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   149
13534
ca6debb89d77 avoid duplicate fact bindings;
wenzelm
parents: 13357
diff changeset
   150
lemma rtrancl_full_induct [case_names initial step, consumes 1]:
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   151
  "[| <a,b> : r^*;  
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   152
      !!x. x: field(r) ==> P(<x,x>);  
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   153
      !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |]  
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   154
   ==>  P(<a,b>)"
13248
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   155
by (erule def_induct [OF rtrancl_def rtrancl_bnd_mono], blast) 
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   156
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   157
(*nice induction rule.
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   158
  Tried adding the typing hypotheses y,z:field(r), but these
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   159
  caused expensive case splits!*)
13534
ca6debb89d77 avoid duplicate fact bindings;
wenzelm
parents: 13357
diff changeset
   160
lemma rtrancl_induct [case_names initial step, induct set: rtrancl]:
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   161
  "[| <a,b> : r^*;                                               
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   162
      P(a);                                                      
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   163
      !!y z.[| <a,y> : r^*;  <y,z> : r;  P(y) |] ==> P(z)        
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   164
   |] ==> P(b)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   165
(*by induction on this formula*)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   166
apply (subgoal_tac "ALL y. <a,b> = <a,y> --> P (y) ")
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   167
(*now solve first subgoal: this formula is sufficient*)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   168
apply (erule spec [THEN mp], rule refl)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   169
(*now do the induction*)
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
   170
apply (erule rtrancl_full_induct, blast+)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   171
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   172
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   173
(*transitivity of transitive closure!! -- by induction.*)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   174
lemma trans_rtrancl: "trans(r^*)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   175
apply (unfold trans_def)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   176
apply (intro allI impI)
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13534
diff changeset
   177
apply (erule_tac b = z in rtrancl_induct, assumption)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   178
apply (blast intro: rtrancl_into_rtrancl) 
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   179
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   180
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   181
lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   182
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   183
(*elimination of rtrancl -- by induction on a special formula*)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   184
lemma rtranclE:
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   185
    "[| <a,b> : r^*;  (a=b) ==> P;                        
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   186
        !!y.[| <a,y> : r^*;   <y,b> : r |] ==> P |]       
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   187
     ==> P"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   188
apply (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r) ")
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   189
(*see HOL/trancl*)
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
   190
apply blast 
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
   191
apply (erule rtrancl_induct, blast+)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   192
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   193
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   194
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   195
(**** The relation trancl ****)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   196
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   197
(*Transitivity of r^+ is proved by transitivity of r^*  *)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   198
lemma trans_trancl: "trans(r^+)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   199
apply (unfold trans_def trancl_def)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   200
apply (blast intro: rtrancl_into_rtrancl
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   201
                    trans_rtrancl [THEN transD, THEN compI])
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   202
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   203
13243
ba53d07d32d5 new lemmas
paulson
parents: 13240
diff changeset
   204
lemmas trans_on_trancl = trans_trancl [THEN trans_imp_trans_on]
ba53d07d32d5 new lemmas
paulson
parents: 13240
diff changeset
   205
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   206
lemmas trancl_trans = trans_trancl [THEN transD, standard]
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   207
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   208
(** Conversions between trancl and rtrancl **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   210
lemma trancl_into_rtrancl: "<a,b> : r^+ ==> <a,b> : r^*"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   211
apply (unfold trancl_def)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   212
apply (blast intro: rtrancl_into_rtrancl)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   213
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   214
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   215
(*r^+ contains all pairs in r  *)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   216
lemma r_into_trancl: "<a,b> : r ==> <a,b> : r^+"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   217
apply (unfold trancl_def)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   218
apply (blast intro!: rtrancl_refl)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   219
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   220
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   221
(*The premise ensures that r consists entirely of pairs*)
13248
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   222
lemma r_subset_trancl: "relation(r) ==> r <= r^+"
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   223
by (simp add: relation_def, blast intro: r_into_trancl)
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   224
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   225
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   226
(*intro rule by definition: from r^* and r  *)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   227
lemma rtrancl_into_trancl1: "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
   228
by (unfold trancl_def, blast)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   229
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   230
(*intro rule from r and r^*  *)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   231
lemma rtrancl_into_trancl2:
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   232
    "[| <a,b> : r;  <b,c> : r^* |]   ==>  <a,c> : r^+"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   233
apply (erule rtrancl_induct)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   234
 apply (erule r_into_trancl)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   235
apply (blast intro: r_into_trancl trancl_trans) 
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   236
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   237
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   238
(*Nice induction rule for trancl*)
13534
ca6debb89d77 avoid duplicate fact bindings;
wenzelm
parents: 13357
diff changeset
   239
lemma trancl_induct [case_names initial step, induct set: trancl]:
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   240
  "[| <a,b> : r^+;                                       
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   241
      !!y.  [| <a,y> : r |] ==> P(y);                    
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   242
      !!y z.[| <a,y> : r^+;  <y,z> : r;  P(y) |] ==> P(z)        
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   243
   |] ==> P(b)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   244
apply (rule compEpair)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   245
apply (unfold trancl_def, assumption)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   246
(*by induction on this formula*)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   247
apply (subgoal_tac "ALL z. <y,z> : r --> P (z) ")
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   248
(*now solve first subgoal: this formula is sufficient*)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   249
 apply blast
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   250
apply (erule rtrancl_induct)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   251
apply (blast intro: rtrancl_into_trancl1)+
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   252
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   253
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   254
(*elimination of r^+ -- NOT an induction rule*)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   255
lemma tranclE:
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   256
    "[| <a,b> : r^+;   
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   257
        <a,b> : r ==> P;  
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   258
        !!y.[| <a,y> : r^+; <y,b> : r |] ==> P   
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   259
     |] ==> P"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   260
apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r) ")
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
   261
apply blast 
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   262
apply (rule compEpair)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   263
apply (unfold trancl_def, assumption)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   264
apply (erule rtranclE)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   265
apply (blast intro: rtrancl_into_trancl1)+
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   266
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   267
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   268
lemma trancl_type: "r^+ <= field(r)*field(r)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   269
apply (unfold trancl_def)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   270
apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2])
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   271
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   272
13248
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   273
lemma relation_trancl: "relation(r^+)"
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   274
apply (simp add: relation_def) 
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   275
apply (blast dest: trancl_type [THEN subsetD]) 
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   276
done
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   277
13243
ba53d07d32d5 new lemmas
paulson
parents: 13240
diff changeset
   278
lemma trancl_subset_times: "r \<subseteq> A * A ==> r^+ \<subseteq> A * A"
ba53d07d32d5 new lemmas
paulson
parents: 13240
diff changeset
   279
by (insert trancl_type [of r], blast)
ba53d07d32d5 new lemmas
paulson
parents: 13240
diff changeset
   280
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   281
lemma trancl_mono: "r<=s ==> r^+ <= s^+"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   282
by (unfold trancl_def, intro comp_mono rtrancl_mono)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   283
13248
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   284
lemma trancl_eq_r: "[|relation(r); trans(r)|] ==> r^+ = r"
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   285
apply (rule equalityI)
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   286
 prefer 2 apply (erule r_subset_trancl, clarify) 
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   287
apply (frule trancl_type [THEN subsetD], clarify) 
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   288
apply (erule trancl_induct, assumption)
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   289
apply (blast dest: transD) 
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   290
done
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   291
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   292
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   293
(** Suggested by Sidi Ould Ehmety **)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   294
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   295
lemma rtrancl_idemp [simp]: "(r^*)^* = r^*"
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
   296
apply (rule equalityI, auto)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   297
 prefer 2
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   298
 apply (frule rtrancl_type [THEN subsetD])
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
   299
 apply (blast intro: r_into_rtrancl ) 
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   300
txt{*converse direction*}
13240
bb5f4faea1f3 conversion of Sum, pair to Isar script
paulson
parents: 13239
diff changeset
   301
apply (frule rtrancl_type [THEN subsetD], clarify) 
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   302
apply (erule rtrancl_induct)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   303
apply (simp add: rtrancl_refl rtrancl_field)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   304
apply (blast intro: rtrancl_trans)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   305
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   306
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   307
lemma rtrancl_subset: "[| R <= S; S <= R^* |] ==> S^* = R^*"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   308
apply (drule rtrancl_mono)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13248
diff changeset
   309
apply (drule rtrancl_mono, simp_all, blast)
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   310
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   311
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   312
lemma rtrancl_Un_rtrancl:
13248
ae66c22ed52e new theorems
paulson
parents: 13243
diff changeset
   313
     "[| relation(r); relation(s) |] ==> (r^* Un s^*)^* = (r Un s)^*"
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   314
apply (rule rtrancl_subset)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   315
apply (blast dest: r_subset_rtrancl)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   316
apply (blast intro: rtrancl_mono [THEN subsetD])
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   317
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   318
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   319
(*** "converse" laws by Sidi Ould Ehmety ***)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   320
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   321
(** rtrancl **)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   322
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   323
lemma rtrancl_converseD: "<x,y>:converse(r)^* ==> <x,y>:converse(r^*)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   324
apply (rule converseI)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   325
apply (frule rtrancl_type [THEN subsetD])
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   326
apply (erule rtrancl_induct)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   327
apply (blast intro: rtrancl_refl)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   328
apply (blast intro: r_into_rtrancl rtrancl_trans)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   329
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   330
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   331
lemma rtrancl_converseI: "<x,y>:converse(r^*) ==> <x,y>:converse(r)^*"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   332
apply (drule converseD)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   333
apply (frule rtrancl_type [THEN subsetD])
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   334
apply (erule rtrancl_induct)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   335
apply (blast intro: rtrancl_refl)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   336
apply (blast intro: r_into_rtrancl rtrancl_trans)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   337
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   338
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   339
lemma rtrancl_converse: "converse(r)^* = converse(r^*)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   340
apply (safe intro!: equalityI)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   341
apply (frule rtrancl_type [THEN subsetD])
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   342
apply (safe dest!: rtrancl_converseD intro!: rtrancl_converseI)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   343
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   344
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   345
(** trancl **)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   346
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   347
lemma trancl_converseD: "<a, b>:converse(r)^+ ==> <a, b>:converse(r^+)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   348
apply (erule trancl_induct)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   349
apply (auto intro: r_into_trancl trancl_trans)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   350
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   351
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   352
lemma trancl_converseI: "<x,y>:converse(r^+) ==> <x,y>:converse(r)^+"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   353
apply (drule converseD)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   354
apply (erule trancl_induct)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   355
apply (auto intro: r_into_trancl trancl_trans)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   356
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   357
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   358
lemma trancl_converse: "converse(r)^+ = converse(r^+)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   359
apply (safe intro!: equalityI)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   360
apply (frule trancl_type [THEN subsetD])
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   361
apply (safe dest!: trancl_converseD intro!: trancl_converseI)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   362
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   363
13534
ca6debb89d77 avoid duplicate fact bindings;
wenzelm
parents: 13357
diff changeset
   364
lemma converse_trancl_induct [case_names initial step, consumes 1]:
13239
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   365
"[| <a, b>:r^+; !!y. <y, b> :r ==> P(y);  
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   366
      !!y z. [| <y, z> : r; <z, b> : r^+; P(z) |] ==> P(y) |]  
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   367
       ==> P(a)"
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   368
apply (drule converseI)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   369
apply (simp (no_asm_use) add: trancl_converse [symmetric])
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   370
apply (erule trancl_induct)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   371
apply (auto simp add: trancl_converse)
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   372
done
f599984ec4c2 converted Bool, Trancl, Rel to Isar format
paulson
parents: 13220
diff changeset
   373
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
end