src/HOL/Lambda/Commutation.thy
author wenzelm
Wed Dec 06 01:12:36 2006 +0100 (2006-12-06)
changeset 21669 c68717c16013
parent 21404 eb85850d3eb7
child 22270 4ccb7e6be929
permissions -rw-r--r--
removed legacy ML bindings;
     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 imports Main begin
    10 
    11 subsection {* Basic definitions *}
    12 
    13 definition
    14   square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool" where
    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 definition
    19   commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool" where
    20   "commute R S = square R S S R"
    21 
    22 definition
    23   diamond :: "('a \<times> 'a) set => bool" where
    24   "diamond R = commute R R"
    25 
    26 definition
    27   Church_Rosser :: "('a \<times> 'a) set => bool" where
    28   "Church_Rosser R =
    29     (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
    30 
    31 abbreviation
    32   confluent :: "('a \<times> 'a) set => bool" where
    33   "confluent R == diamond (R^*)"
    34 
    35 
    36 subsection {* Basic lemmas *}
    37 
    38 subsubsection {* square *}
    39 
    40 lemma square_sym: "square R S T U ==> square S R U T"
    41   apply (unfold square_def)
    42   apply blast
    43   done
    44 
    45 lemma square_subset:
    46     "[| square R S T U; T \<subseteq> T' |] ==> square R S T' U"
    47   apply (unfold square_def)
    48   apply blast
    49   done
    50 
    51 lemma square_reflcl:
    52     "[| square R S T (R^=); S \<subseteq> T |] ==> square (R^=) S T (R^=)"
    53   apply (unfold square_def)
    54   apply blast
    55   done
    56 
    57 lemma square_rtrancl:
    58     "square R S S T ==> square (R^*) S S (T^*)"
    59   apply (unfold square_def)
    60   apply (intro strip)
    61   apply (erule rtrancl_induct)
    62    apply blast
    63   apply (blast intro: rtrancl_into_rtrancl)
    64   done
    65 
    66 lemma square_rtrancl_reflcl_commute:
    67     "square R S (S^*) (R^=) ==> commute (R^*) (S^*)"
    68   apply (unfold commute_def)
    69   apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]
    70     elim: r_into_rtrancl)
    71   done
    72 
    73 
    74 subsubsection {* commute *}
    75 
    76 lemma commute_sym: "commute R S ==> commute S R"
    77   apply (unfold commute_def)
    78   apply (blast intro: square_sym)
    79   done
    80 
    81 lemma commute_rtrancl: "commute R S ==> commute (R^*) (S^*)"
    82   apply (unfold commute_def)
    83   apply (blast intro: square_rtrancl square_sym)
    84   done
    85 
    86 lemma commute_Un:
    87     "[| commute R T; commute S T |] ==> commute (R \<union> S) T"
    88   apply (unfold commute_def square_def)
    89   apply blast
    90   done
    91 
    92 
    93 subsubsection {* diamond, confluence, and union *}
    94 
    95 lemma diamond_Un:
    96     "[| diamond R; diamond S; commute R S |] ==> diamond (R \<union> S)"
    97   apply (unfold diamond_def)
    98   apply (assumption | rule commute_Un commute_sym)+
    99   done
   100 
   101 lemma diamond_confluent: "diamond R ==> confluent R"
   102   apply (unfold diamond_def)
   103   apply (erule commute_rtrancl)
   104   done
   105 
   106 lemma square_reflcl_confluent:
   107     "square R R (R^=) (R^=) ==> confluent R"
   108   apply (unfold diamond_def)
   109   apply (fast intro: square_rtrancl_reflcl_commute r_into_rtrancl
   110     elim: square_subset)
   111   done
   112 
   113 lemma confluent_Un:
   114     "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (R \<union> S)"
   115   apply (rule rtrancl_Un_rtrancl [THEN subst])
   116   apply (blast dest: diamond_Un intro: diamond_confluent)
   117   done
   118 
   119 lemma diamond_to_confluence:
   120     "[| diamond R; T \<subseteq> R; R \<subseteq> T^* |] ==> confluent T"
   121   apply (force intro: diamond_confluent
   122     dest: rtrancl_subset [symmetric])
   123   done
   124 
   125 
   126 subsection {* Church-Rosser *}
   127 
   128 lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
   129   apply (unfold square_def commute_def diamond_def Church_Rosser_def)
   130   apply (tactic {* safe_tac HOL_cs *})
   131    apply (tactic {*
   132      blast_tac (HOL_cs addIs
   133        [thm "Un_upper2" RS thm "rtrancl_mono" RS thm "subsetD" RS thm "rtrancl_trans",
   134         thm "rtrancl_converseI", thm "converseI",
   135         thm "Un_upper1" RS thm "rtrancl_mono" RS thm "subsetD"]) 1 *})
   136   apply (erule rtrancl_induct)
   137    apply blast
   138   apply (blast del: rtrancl_refl intro: rtrancl_trans)
   139   done
   140 
   141 
   142 subsection {* Newman's lemma *}
   143 
   144 text {* Proof by Stefan Berghofer *}
   145 
   146 theorem newman:
   147   assumes wf: "wf (R\<inverse>)"
   148   and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
   149     \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
   150   shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
   151     \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
   152   using wf
   153 proof induct
   154   case (less x b c)
   155   have xc: "(x, c) \<in> R\<^sup>*" .
   156   have xb: "(x, b) \<in> R\<^sup>*" . thus ?case
   157   proof (rule converse_rtranclE)
   158     assume "x = b"
   159     with xc have "(b, c) \<in> R\<^sup>*" by simp
   160     thus ?thesis by iprover
   161   next
   162     fix y
   163     assume xy: "(x, y) \<in> R"
   164     assume yb: "(y, b) \<in> R\<^sup>*"
   165     from xc show ?thesis
   166     proof (rule converse_rtranclE)
   167       assume "x = c"
   168       with xb have "(c, b) \<in> R\<^sup>*" by simp
   169       thus ?thesis by iprover
   170     next
   171       fix y'
   172       assume y'c: "(y', c) \<in> R\<^sup>*"
   173       assume xy': "(x, y') \<in> R"
   174       with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
   175       then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by iprover
   176       from xy have "(y, x) \<in> R\<inverse>" ..
   177       from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
   178       then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by iprover
   179       from xy' have "(y', x) \<in> R\<inverse>" ..
   180       moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
   181       moreover note y'c
   182       ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
   183       then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by iprover
   184       from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
   185       with cw show ?thesis by iprover
   186     qed
   187   qed
   188 qed
   189 
   190 text {*
   191   \medskip Alternative version.  Partly automated by Tobias
   192   Nipkow. Takes 2 minutes (2002).
   193 
   194   This is the maximal amount of automation possible at the moment.
   195 *}
   196 
   197 theorem newman':
   198   assumes wf: "wf (R\<inverse>)"
   199   and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
   200     \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
   201   shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
   202     \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
   203   using wf
   204 proof induct
   205   case (less x b c)
   206   note IH = `\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
   207                      \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*`
   208   have xc: "(x, c) \<in> R\<^sup>*" .
   209   have xb: "(x, b) \<in> R\<^sup>*" .
   210   thus ?case
   211   proof (rule converse_rtranclE)
   212     assume "x = b"
   213     with xc have "(b, c) \<in> R\<^sup>*" by simp
   214     thus ?thesis by iprover
   215   next
   216     fix y
   217     assume xy: "(x, y) \<in> R"
   218     assume yb: "(y, b) \<in> R\<^sup>*"
   219     from xc show ?thesis
   220     proof (rule converse_rtranclE)
   221       assume "x = c"
   222       with xb have "(c, b) \<in> R\<^sup>*" by simp
   223       thus ?thesis by iprover
   224     next
   225       fix y'
   226       assume y'c: "(y', c) \<in> R\<^sup>*"
   227       assume xy': "(x, y') \<in> R"
   228       with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
   229         by (blast dest: lc)
   230       from yb u y'c show ?thesis
   231         by (blast del: rtrancl_refl
   232             intro: rtrancl_trans
   233             dest: IH [OF xy [symmetric]] IH [OF xy' [symmetric]])
   234     qed
   235   qed
   236 qed
   237 
   238 end