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