src/CCL/Trancl.thy
author wenzelm
Wed, 03 Nov 2010 21:53:56 +0100
changeset 40335 3e4bb6e7c3ca
parent 32153 a0e57fb1b930
child 42156 df219e736a5d
permissions -rw-r--r--
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
     1
(*  Title:      CCL/Trancl.thy
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 0
diff changeset
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
     6
header {* Transitive closure of a relation *}
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
     7
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
     8
theory Trancl
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
     9
imports CCL
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    10
begin
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
consts
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    13
  trans   :: "i set => o"                   (*transitivity predicate*)
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    14
  id      :: "i set"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    15
  rtrancl :: "i set => i set"               ("(_^*)" [100] 100)
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    16
  trancl  :: "i set => i set"               ("(_^+)" [100] 100)
24825
c4f13ab78f9d avoid unnamed infixes;
wenzelm
parents: 20140
diff changeset
    17
  relcomp :: "[i set,i set] => i set"       (infixr "O" 60)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    19
axioms
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    20
  trans_def:       "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
24825
c4f13ab78f9d avoid unnamed infixes;
wenzelm
parents: 20140
diff changeset
    21
  relcomp_def:     (*composition of relations*)
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    22
                   "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    23
  id_def:          (*the identity relation*)
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    24
                   "id == {p. EX x. p = <x,x>}"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    25
  rtrancl_def:     "r^* == lfp(%s. id Un (r O s))"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    26
  trancl_def:      "r^+ == r O rtrancl(r)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    27
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    28
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    29
subsection {* Natural deduction for @{text "trans(r)"} *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    30
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    31
lemma transI:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    32
  "(!! x y z. [| <x,y>:r;  <y,z>:r |] ==> <x,z>:r) ==> trans(r)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    33
  unfolding trans_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    34
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    35
lemma transD: "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    36
  unfolding trans_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    37
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    38
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    39
subsection {* Identity relation *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    40
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    41
lemma idI: "<a,a> : id"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    42
  apply (unfold id_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    43
  apply (rule CollectI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    44
  apply (rule exI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    45
  apply (rule refl)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    46
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    47
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    48
lemma idE:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    49
    "[| p: id;  !!x.[| p = <x,x> |] ==> P |] ==>  P"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    50
  apply (unfold id_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    51
  apply (erule CollectE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    52
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    53
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    54
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    55
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    56
subsection {* Composition of two relations *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    57
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    58
lemma compI: "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"
24825
c4f13ab78f9d avoid unnamed infixes;
wenzelm
parents: 20140
diff changeset
    59
  unfolding relcomp_def by blast
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    60
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    61
(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    62
lemma compE:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    63
    "[| xz : r O s;
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    64
        !!x y z. [| xz = <x,z>;  <x,y>:s;  <y,z>:r |] ==> P
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    65
     |] ==> P"
24825
c4f13ab78f9d avoid unnamed infixes;
wenzelm
parents: 20140
diff changeset
    66
  unfolding relcomp_def by blast
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    67
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    68
lemma compEpair:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    69
  "[| <a,c> : r O s;
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    70
      !!y. [| <a,y>:s;  <y,c>:r |] ==> P
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    71
   |] ==> P"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    72
  apply (erule compE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    73
  apply (simp add: pair_inject)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    74
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    75
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    76
lemmas [intro] = compI idI
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    77
  and [elim] = compE idE
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    78
  and [elim!] = pair_inject
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    79
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    80
lemma comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    81
  by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    82
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    83
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    84
subsection {* The relation rtrancl *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    85
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    86
lemma rtrancl_fun_mono: "mono(%s. id Un (r O s))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    87
  apply (rule monoI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    88
  apply (rule monoI subset_refl comp_mono Un_mono)+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    89
  apply assumption
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    90
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    91
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    92
lemma rtrancl_unfold: "r^* = id Un (r O r^*)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    93
  by (rule rtrancl_fun_mono [THEN rtrancl_def [THEN def_lfp_Tarski]])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    94
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    95
(*Reflexivity of rtrancl*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    96
lemma rtrancl_refl: "<a,a> : r^*"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    97
  apply (subst rtrancl_unfold)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    98
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    99
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   100
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   101
(*Closure under composition with r*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   102
lemma rtrancl_into_rtrancl: "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   103
  apply (subst rtrancl_unfold)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   104
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   105
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   106
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   107
(*rtrancl of r contains r*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   108
lemma r_into_rtrancl: "[| <a,b> : r |] ==> <a,b> : r^*"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   109
  apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   110
  apply assumption
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   111
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   112
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   113
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   114
subsection {* standard induction rule *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   115
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   116
lemma rtrancl_full_induct:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   117
  "[| <a,b> : r^*;
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   118
      !!x. P(<x,x>);
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   119
      !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |]
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   120
   ==>  P(<a,b>)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   121
  apply (erule def_induct [OF rtrancl_def])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   122
   apply (rule rtrancl_fun_mono)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   123
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   124
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   125
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   126
(*nice induction rule*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   127
lemma rtrancl_induct:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   128
  "[| <a,b> : r^*;
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   129
      P(a);
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   130
      !!y z.[| <a,y> : r^*;  <y,z> : r;  P(y) |] ==> P(z) |]
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   131
    ==> P(b)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   132
(*by induction on this formula*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   133
  apply (subgoal_tac "ALL y. <a,b> = <a,y> --> P(y)")
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   134
(*now solve first subgoal: this formula is sufficient*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   135
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   136
(*now do the induction*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   137
  apply (erule rtrancl_full_induct)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   138
   apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   139
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   140
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   141
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   142
(*transitivity of transitive closure!! -- by induction.*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   143
lemma trans_rtrancl: "trans(r^*)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   144
  apply (rule transI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   145
  apply (rule_tac b = z in rtrancl_induct)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   146
    apply (fast elim: rtrancl_into_rtrancl)+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   147
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   148
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   149
(*elimination of rtrancl -- by induction on a special formula*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   150
lemma rtranclE:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   151
  "[| <a,b> : r^*;  (a = b) ==> P;
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   152
      !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |]
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   153
   ==> P"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   154
  apply (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r)")
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   155
   prefer 2
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   156
   apply (erule rtrancl_induct)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   157
    apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   158
   apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   159
  apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   160
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   161
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   162
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   163
subsection {* The relation trancl *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   164
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   165
subsubsection {* Conversions between trancl and rtrancl *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   166
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   167
lemma trancl_into_rtrancl: "[| <a,b> : r^+ |] ==> <a,b> : r^*"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   168
  apply (unfold trancl_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   169
  apply (erule compEpair)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   170
  apply (erule rtrancl_into_rtrancl)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   171
  apply assumption
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   172
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   173
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   174
(*r^+ contains r*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   175
lemma r_into_trancl: "[| <a,b> : r |] ==> <a,b> : r^+"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   176
  unfolding trancl_def by (blast intro: rtrancl_refl)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   177
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   178
(*intro rule by definition: from rtrancl and r*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   179
lemma rtrancl_into_trancl1: "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   180
  unfolding trancl_def by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   181
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   182
(*intro rule from r and rtrancl*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   183
lemma rtrancl_into_trancl2: "[| <a,b> : r;  <b,c> : r^* |]   ==>  <a,c> : r^+"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   184
  apply (erule rtranclE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   185
   apply (erule subst)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   186
   apply (erule r_into_trancl)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   187
  apply (rule trans_rtrancl [THEN transD, THEN rtrancl_into_trancl1])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   188
    apply (assumption | rule r_into_rtrancl)+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   189
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   190
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   191
(*elimination of r^+ -- NOT an induction rule*)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   192
lemma tranclE:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   193
  "[| <a,b> : r^+;
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   194
      <a,b> : r ==> P;
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   195
      !!y.[| <a,y> : r^+;  <y,b> : r |] ==> P
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   196
   |] ==> P"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   197
  apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r)")
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   198
   apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   199
  apply (unfold trancl_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   200
  apply (erule compEpair)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   201
  apply (erule rtranclE)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   202
   apply blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   203
  apply (blast intro!: rtrancl_into_trancl1)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   204
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   205
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   206
(*Transitivity of r^+.
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   207
  Proved by unfolding since it uses transitivity of rtrancl. *)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   208
lemma trans_trancl: "trans(r^+)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   209
  apply (unfold trancl_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   210
  apply (rule transI)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   211
  apply (erule compEpair)+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   212
  apply (erule rtrancl_into_rtrancl [THEN trans_rtrancl [THEN transD, THEN compI]])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   213
    apply assumption+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   214
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   215
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   216
lemma trancl_into_trancl2: "[| <a,b> : r;  <b,c> : r^+ |]   ==>  <a,c> : r^+"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   217
  apply (rule r_into_trancl [THEN trans_trancl [THEN transD]])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   218
   apply assumption+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
   219
  done
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
end