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