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