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