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--
more precise headers;
     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