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