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