src/HOL/Lambda/Commutation.thy
author wenzelm
Wed Jul 10 13:55:32 2002 +0200 (2002-07-10)
changeset 13331 47e9950a502d
parent 13089 c8c28a1dc787
child 13343 3b2b18c58d80
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Lambda/Commutation.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995  TU Muenchen
     5 *)
     6 
     7 header {* Abstract commutation and confluence notions *}
     8 
     9 theory Commutation = Main:
    10 
    11 subsection {* Basic definitions *}
    12 
    13 constdefs
    14   square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
    15   "square R S T U ==
    16     \<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U))"
    17 
    18   commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
    19   "commute R S == square R S S R"
    20 
    21   diamond :: "('a \<times> 'a) set => bool"
    22   "diamond R == commute R R"
    23 
    24   Church_Rosser :: "('a \<times> 'a) set => bool"
    25   "Church_Rosser R ==
    26     \<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*)"
    27 
    28 syntax
    29   confluent :: "('a \<times> 'a) set => bool"
    30 translations
    31   "confluent R" == "diamond (R^*)"
    32 
    33 
    34 subsection {* Basic lemmas *}
    35 
    36 subsubsection {* square *}
    37 
    38 lemma square_sym: "square R S T U ==> square S R U T"
    39   apply (unfold square_def)
    40   apply blast
    41   done
    42 
    43 lemma square_subset:
    44     "[| square R S T U; T \<subseteq> T' |] ==> square R S T' U"
    45   apply (unfold square_def)
    46   apply blast
    47   done
    48 
    49 lemma square_reflcl:
    50     "[| square R S T (R^=); S \<subseteq> T |] ==> square (R^=) S T (R^=)"
    51   apply (unfold square_def)
    52   apply blast
    53   done
    54 
    55 lemma square_rtrancl:
    56     "square R S S T ==> square (R^*) S S (T^*)"
    57   apply (unfold square_def)
    58   apply (intro strip)
    59   apply (erule rtrancl_induct)
    60    apply blast
    61   apply (blast intro: rtrancl_into_rtrancl)
    62   done
    63 
    64 lemma square_rtrancl_reflcl_commute:
    65     "square R S (S^*) (R^=) ==> commute (R^*) (S^*)"
    66   apply (unfold commute_def)
    67   apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]
    68     elim: r_into_rtrancl)
    69   done
    70 
    71 
    72 subsubsection {* commute *}
    73 
    74 lemma commute_sym: "commute R S ==> commute S R"
    75   apply (unfold commute_def)
    76   apply (blast intro: square_sym)
    77   done
    78 
    79 lemma commute_rtrancl: "commute R S ==> commute (R^*) (S^*)"
    80   apply (unfold commute_def)
    81   apply (blast intro: square_rtrancl square_sym)
    82   done
    83 
    84 lemma commute_Un:
    85     "[| commute R T; commute S T |] ==> commute (R \<union> S) T"
    86   apply (unfold commute_def square_def)
    87   apply blast
    88   done
    89 
    90 
    91 subsubsection {* diamond, confluence, and union *}
    92 
    93 lemma diamond_Un:
    94     "[| diamond R; diamond S; commute R S |] ==> diamond (R \<union> S)"
    95   apply (unfold diamond_def)
    96   apply (assumption | rule commute_Un commute_sym)+
    97   done
    98 
    99 lemma diamond_confluent: "diamond R ==> confluent R"
   100   apply (unfold diamond_def)
   101   apply (erule commute_rtrancl)
   102   done
   103 
   104 lemma square_reflcl_confluent:
   105     "square R R (R^=) (R^=) ==> confluent R"
   106   apply (unfold diamond_def)
   107   apply (fast intro: square_rtrancl_reflcl_commute r_into_rtrancl
   108     elim: square_subset)
   109   done
   110 
   111 lemma confluent_Un:
   112     "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (R \<union> S)"
   113   apply (rule rtrancl_Un_rtrancl [THEN subst])
   114   apply (blast dest: diamond_Un intro: diamond_confluent)
   115   done
   116 
   117 lemma diamond_to_confluence:
   118     "[| diamond R; T \<subseteq> R; R \<subseteq> T^* |] ==> confluent T"
   119   apply (force intro: diamond_confluent
   120     dest: rtrancl_subset [symmetric])
   121   done
   122 
   123 
   124 subsection {* Church-Rosser *}
   125 
   126 lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
   127   apply (unfold square_def commute_def diamond_def Church_Rosser_def)
   128   apply (tactic {* safe_tac HOL_cs *})
   129    apply (tactic {*
   130      blast_tac (HOL_cs addIs
   131        [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
   132        rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
   133   apply (erule rtrancl_induct)
   134    apply blast
   135   apply (blast del: rtrancl_refl intro: rtrancl_trans)
   136   done
   137 
   138 
   139 subsection {* Newman's lemma *}
   140 
   141 theorem Newman:
   142   assumes wf: "wf (R\<inverse>)"
   143   and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
   144     \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
   145   shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
   146     \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
   147   using wf
   148 proof induct
   149   case (less x b c)
   150   have xc: "(x, c) \<in> R\<^sup>*" .
   151   have xb: "(x, b) \<in> R\<^sup>*" . thus ?case
   152   proof (rule converse_rtranclE)
   153     assume "x = b"
   154     with xc have "(b, c) \<in> R\<^sup>*" by simp
   155     thus ?thesis by rules
   156   next
   157     fix y
   158     assume xy: "(x, y) \<in> R"
   159     assume yb: "(y, b) \<in> R\<^sup>*"
   160     from xc show ?thesis
   161     proof (rule converse_rtranclE)
   162       assume "x = c"
   163       with xb have "(c, b) \<in> R\<^sup>*" by simp
   164       thus ?thesis by rules
   165     next
   166       fix y'
   167       assume y'c: "(y', c) \<in> R\<^sup>*"
   168       assume xy': "(x, y') \<in> R"
   169       with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
   170       then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules
   171       from xy have "(y, x) \<in> R\<inverse>" ..
   172       from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
   173       then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules
   174       from xy' have "(y', x) \<in> R\<inverse>" ..
   175       moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
   176       moreover note y'c
   177       ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
   178       then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules
   179       from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
   180       with cw show ?thesis by rules
   181     qed
   182   qed
   183 qed
   184 
   185 end