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