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