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