src/HOL/Lambda/Commutation.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 19363 667b5ea637dd
child 21669 c68717c16013
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
     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        [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
   134        rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
   135   apply (erule rtrancl_induct)
   136    apply blast
   137   apply (blast del: rtrancl_refl intro: rtrancl_trans)
   138   done
   139 
   140 
   141 subsection {* Newman's lemma *}
   142 
   143 text {* Proof by Stefan Berghofer *}
   144 
   145 theorem newman:
   146   assumes wf: "wf (R\<inverse>)"
   147   and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
   148     \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
   149   shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
   150     \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
   151   using wf
   152 proof induct
   153   case (less x b c)
   154   have xc: "(x, c) \<in> R\<^sup>*" .
   155   have xb: "(x, b) \<in> R\<^sup>*" . thus ?case
   156   proof (rule converse_rtranclE)
   157     assume "x = b"
   158     with xc have "(b, c) \<in> R\<^sup>*" by simp
   159     thus ?thesis by iprover
   160   next
   161     fix y
   162     assume xy: "(x, y) \<in> R"
   163     assume yb: "(y, b) \<in> R\<^sup>*"
   164     from xc show ?thesis
   165     proof (rule converse_rtranclE)
   166       assume "x = c"
   167       with xb have "(c, b) \<in> R\<^sup>*" by simp
   168       thus ?thesis by iprover
   169     next
   170       fix y'
   171       assume y'c: "(y', c) \<in> R\<^sup>*"
   172       assume xy': "(x, y') \<in> R"
   173       with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
   174       then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by iprover
   175       from xy have "(y, x) \<in> R\<inverse>" ..
   176       from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
   177       then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by iprover
   178       from xy' have "(y', x) \<in> R\<inverse>" ..
   179       moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
   180       moreover note y'c
   181       ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
   182       then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by iprover
   183       from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
   184       with cw show ?thesis by iprover
   185     qed
   186   qed
   187 qed
   188 
   189 text {*
   190   \medskip Alternative version.  Partly automated by Tobias
   191   Nipkow. Takes 2 minutes (2002).
   192 
   193   This is the maximal amount of automation possible at the moment.
   194 *}
   195 
   196 theorem newman':
   197   assumes wf: "wf (R\<inverse>)"
   198   and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
   199     \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
   200   shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
   201     \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
   202   using wf
   203 proof induct
   204   case (less x b c)
   205   note IH = `\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
   206                      \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*`
   207   have xc: "(x, c) \<in> R\<^sup>*" .
   208   have xb: "(x, b) \<in> R\<^sup>*" .
   209   thus ?case
   210   proof (rule converse_rtranclE)
   211     assume "x = b"
   212     with xc have "(b, c) \<in> R\<^sup>*" by simp
   213     thus ?thesis by iprover
   214   next
   215     fix y
   216     assume xy: "(x, y) \<in> R"
   217     assume yb: "(y, b) \<in> R\<^sup>*"
   218     from xc show ?thesis
   219     proof (rule converse_rtranclE)
   220       assume "x = c"
   221       with xb have "(c, b) \<in> R\<^sup>*" by simp
   222       thus ?thesis by iprover
   223     next
   224       fix y'
   225       assume y'c: "(y', c) \<in> R\<^sup>*"
   226       assume xy': "(x, y') \<in> R"
   227       with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
   228         by (blast dest: lc)
   229       from yb u y'c show ?thesis
   230         by (blast del: rtrancl_refl
   231             intro: rtrancl_trans
   232             dest: IH [OF xy [symmetric]] IH [OF xy' [symmetric]])
   233     qed
   234   qed
   235 qed
   236 
   237 end