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