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