src/ZF/ex/Commutation.thy
 author wenzelm Fri Feb 18 16:22:27 2011 +0100 (2011-02-18) changeset 41777 1f7cbe39d425 parent 35762 af3ff2ba4c54 child 46822 95f1e700b712 permissions -rw-r--r--
```     1 (*  Title:      ZF/ex/Commutation.thy
```
```     2     Author:     Tobias Nipkow & Sidi Ould Ehmety
```
```     3     Copyright   1995  TU Muenchen
```
```     4
```
```     5 Commutation theory for proving the Church Rosser theorem.
```
```     6 *)
```
```     7
```
```     8 theory Commutation imports Main begin
```
```     9
```
```    10 definition
```
```    11   square  :: "[i, i, i, i] => o" where
```
```    12   "square(r,s,t,u) ==
```
```    13     (\<forall>a b. <a,b> \<in> r --> (\<forall>c. <a, c> \<in> s --> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
```
```    14
```
```    15 definition
```
```    16   commute :: "[i, i] => o" where
```
```    17   "commute(r,s) == square(r,s,s,r)"
```
```    18
```
```    19 definition
```
```    20   diamond :: "i=>o" where
```
```    21   "diamond(r)   == commute(r, r)"
```
```    22
```
```    23 definition
```
```    24   strip :: "i=>o" where
```
```    25   "strip(r) == commute(r^*, r)"
```
```    26
```
```    27 definition
```
```    28   Church_Rosser :: "i => o" where
```
```    29   "Church_Rosser(r) == (\<forall>x y. <x,y> \<in>  (r Un converse(r))^* -->
```
```    30                         (\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))"
```
```    31
```
```    32 definition
```
```    33   confluent :: "i=>o" where
```
```    34   "confluent(r) == diamond(r^*)"
```
```    35
```
```    36
```
```    37 lemma square_sym: "square(r,s,t,u) ==> square(s,r,u,t)"
```
```    38   unfolding square_def by blast
```
```    39
```
```    40 lemma square_subset: "[| square(r,s,t,u); t \<subseteq> t' |] ==> square(r,s,t',u)"
```
```    41   unfolding square_def by blast
```
```    42
```
```    43
```
```    44 lemma square_rtrancl:
```
```    45   "square(r,s,s,t) ==> field(s)<=field(t) ==> square(r^*,s,s,t^*)"
```
```    46 apply (unfold square_def, clarify)
```
```    47 apply (erule rtrancl_induct)
```
```    48 apply (blast intro: rtrancl_refl)
```
```    49 apply (blast intro: rtrancl_into_rtrancl)
```
```    50 done
```
```    51
```
```    52 (* A special case of square_rtrancl_on *)
```
```    53 lemma diamond_strip:
```
```    54   "diamond(r) ==> strip(r)"
```
```    55 apply (unfold diamond_def commute_def strip_def)
```
```    56 apply (rule square_rtrancl, simp_all)
```
```    57 done
```
```    58
```
```    59 (*** commute ***)
```
```    60
```
```    61 lemma commute_sym: "commute(r,s) ==> commute(s,r)"
```
```    62   unfolding commute_def by (blast intro: square_sym)
```
```    63
```
```    64 lemma commute_rtrancl:
```
```    65   "commute(r,s) ==> field(r)=field(s) ==> commute(r^*,s^*)"
```
```    66 apply (unfold commute_def)
```
```    67 apply (rule square_rtrancl)
```
```    68 apply (rule square_sym [THEN square_rtrancl, THEN square_sym])
```
```    69 apply (simp_all add: rtrancl_field)
```
```    70 done
```
```    71
```
```    72
```
```    73 lemma confluentD: "confluent(r) ==> diamond(r^*)"
```
```    74 by (simp add: confluent_def)
```
```    75
```
```    76 lemma strip_confluent: "strip(r) ==> confluent(r)"
```
```    77 apply (unfold strip_def confluent_def diamond_def)
```
```    78 apply (drule commute_rtrancl)
```
```    79 apply (simp_all add: rtrancl_field)
```
```    80 done
```
```    81
```
```    82 lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)"
```
```    83   unfolding commute_def square_def by blast
```
```    84
```
```    85 lemma diamond_Un:
```
```    86      "[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r Un s)"
```
```    87   unfolding diamond_def by (blast intro: commute_Un commute_sym)
```
```    88
```
```    89 lemma diamond_confluent:
```
```    90     "diamond(r) ==> confluent(r)"
```
```    91 apply (unfold diamond_def confluent_def)
```
```    92 apply (erule commute_rtrancl, simp)
```
```    93 done
```
```    94
```
```    95 lemma confluent_Un:
```
```    96  "[| confluent(r); confluent(s); commute(r^*, s^*);
```
```    97      relation(r); relation(s) |] ==> confluent(r Un s)"
```
```    98 apply (unfold confluent_def)
```
```    99 apply (rule rtrancl_Un_rtrancl [THEN subst], auto)
```
```   100 apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD])
```
```   101 done
```
```   102
```
```   103
```
```   104 lemma diamond_to_confluence:
```
```   105      "[| diamond(r); s \<subseteq> r; r<= s^* |] ==> confluent(s)"
```
```   106 apply (drule rtrancl_subset [symmetric], assumption)
```
```   107 apply (simp_all add: confluent_def)
```
```   108 apply (blast intro: diamond_confluent [THEN confluentD])
```
```   109 done
```
```   110
```
```   111
```
```   112 (*** Church_Rosser ***)
```
```   113
```
```   114 lemma Church_Rosser1:
```
```   115      "Church_Rosser(r) ==> confluent(r)"
```
```   116 apply (unfold confluent_def Church_Rosser_def square_def
```
```   117               commute_def diamond_def, auto)
```
```   118 apply (drule converseI)
```
```   119 apply (simp (no_asm_use) add: rtrancl_converse [symmetric])
```
```   120 apply (drule_tac x = b in spec)
```
```   121 apply (drule_tac x1 = c in spec [THEN mp])
```
```   122 apply (rule_tac b = a in rtrancl_trans)
```
```   123 apply (blast intro: rtrancl_mono [THEN subsetD])+
```
```   124 done
```
```   125
```
```   126
```
```   127 lemma Church_Rosser2:
```
```   128      "confluent(r) ==> Church_Rosser(r)"
```
```   129 apply (unfold confluent_def Church_Rosser_def square_def
```
```   130               commute_def diamond_def, auto)
```
```   131 apply (frule fieldI1)
```
```   132 apply (simp add: rtrancl_field)
```
```   133 apply (erule rtrancl_induct, auto)
```
```   134 apply (blast intro: rtrancl_refl)
```
```   135 apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)+
```
```   136 done
```
```   137
```
```   138
```
```   139 lemma Church_Rosser: "Church_Rosser(r) <-> confluent(r)"
```
```   140   by (blast intro: Church_Rosser1 Church_Rosser2)
```
```   141
```
```   142 end
```