src/HOL/Lambda/Commutation.thy
author berghofe
Wed Feb 07 17:41:11 2007 +0100 (2007-02-07)
changeset 22270 4ccb7e6be929
parent 21669 c68717c16013
child 22422 ee19cdb07528
permissions -rw-r--r--
Converted to predicate 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 => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
    15   "square R S T U =
    16     (\<forall>x y. R x y --> (\<forall>z. S x z --> (\<exists>u. T y u \<and> U z u)))"
    17 
    18 definition
    19   commute :: "['a => 'a => bool, 'a => 'a => bool] => bool" where
    20   "commute R S = square R S S R"
    21 
    22 definition
    23   diamond :: "('a => 'a => bool) => bool" where
    24   "diamond R = commute R R"
    25 
    26 definition
    27   Church_Rosser :: "('a => 'a => bool) => bool" where
    28   "Church_Rosser R =
    29     (\<forall>x y. (join R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
    30 
    31 abbreviation
    32   confluent :: "('a => 'a => bool) => 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 \<le> T' |] ==> square R S T' U"
    47   apply (unfold square_def)
    48   apply (blast dest: predicate2D)
    49   done
    50 
    51 lemma square_reflcl:
    52     "[| square R S T (R^==); S \<le> T |] ==> square (R^==) S T (R^==)"
    53   apply (unfold square_def)
    54   apply (blast dest: predicate2D)
    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.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   done
    71 
    72 
    73 subsubsection {* commute *}
    74 
    75 lemma commute_sym: "commute R S ==> commute S R"
    76   apply (unfold commute_def)
    77   apply (blast intro: square_sym)
    78   done
    79 
    80 lemma commute_rtrancl: "commute R S ==> commute (R^**) (S^**)"
    81   apply (unfold commute_def)
    82   apply (blast intro: square_rtrancl square_sym)
    83   done
    84 
    85 lemma commute_Un:
    86     "[| commute R T; commute S T |] ==> commute (join R S) T"
    87   apply (unfold commute_def square_def)
    88   apply blast
    89   done
    90 
    91 
    92 subsubsection {* diamond, confluence, and union *}
    93 
    94 lemma diamond_Un:
    95     "[| diamond R; diamond S; commute R S |] ==> diamond (join R S)"
    96   apply (unfold diamond_def)
    97   apply (assumption | rule commute_Un commute_sym)+
    98   done
    99 
   100 lemma diamond_confluent: "diamond R ==> confluent R"
   101   apply (unfold diamond_def)
   102   apply (erule commute_rtrancl)
   103   done
   104 
   105 lemma square_reflcl_confluent:
   106     "square R R (R^==) (R^==) ==> confluent R"
   107   apply (unfold diamond_def)
   108   apply (fast intro: square_rtrancl_reflcl_commute elim: square_subset)
   109   done
   110 
   111 lemma confluent_Un:
   112     "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (join R 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 \<le> R; R \<le> 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        [thm "join_right_le" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
   132         thm "rtrancl_converseI'", thm "conversepI",
   133         thm "join_left_le" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
   134   apply (erule rtrancl_induct')
   135    apply blast
   136   apply (blast del: rtrancl.rtrancl_refl intro: rtrancl_trans')
   137   done
   138 
   139 
   140 subsection {* Newman's lemma *}
   141 
   142 text {* Proof by Stefan Berghofer *}
   143 
   144 theorem newman:
   145   assumes wf: "wfP (R\<inverse>\<inverse>)"
   146   and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
   147     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   148   shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
   149     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   150   using wf
   151 proof induct
   152   case (less x b c)
   153   have xc: "R\<^sup>*\<^sup>* x c" .
   154   have xb: "R\<^sup>*\<^sup>* x b" . thus ?case
   155   proof (rule converse_rtranclE')
   156     assume "x = b"
   157     with xc have "R\<^sup>*\<^sup>* b c" by simp
   158     thus ?thesis by iprover
   159   next
   160     fix y
   161     assume xy: "R x y"
   162     assume yb: "R\<^sup>*\<^sup>* y b"
   163     from xc show ?thesis
   164     proof (rule converse_rtranclE')
   165       assume "x = c"
   166       with xb have "R\<^sup>*\<^sup>* c b" by simp
   167       thus ?thesis by iprover
   168     next
   169       fix y'
   170       assume y'c: "R\<^sup>*\<^sup>* y' c"
   171       assume xy': "R x y'"
   172       with xy have "\<exists>u. R\<^sup>*\<^sup>* y u \<and> R\<^sup>*\<^sup>* y' u" by (rule lc)
   173       then obtain u where yu: "R\<^sup>*\<^sup>* y u" and y'u: "R\<^sup>*\<^sup>* y' u" by iprover
   174       from xy have "R\<inverse>\<inverse> y x" ..
   175       from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
   176       then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
   177       from xy' have "R\<inverse>\<inverse> y' x" ..
   178       moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtrancl_trans')
   179       moreover note y'c
   180       ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
   181       then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
   182       from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtrancl_trans')
   183       with cw show ?thesis by iprover
   184     qed
   185   qed
   186 qed
   187 
   188 text {*
   189   \medskip Alternative version.  Partly automated by Tobias
   190   Nipkow. Takes 2 minutes (2002).
   191 
   192   This is the maximal amount of automation possible at the moment.
   193 *}
   194 
   195 theorem newman':
   196   assumes wf: "wfP (R\<inverse>\<inverse>)"
   197   and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
   198     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   199   shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
   200     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   201   using wf
   202 proof induct
   203   case (less x b c)
   204   note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
   205                      \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
   206   have xc: "R\<^sup>*\<^sup>* x c" .
   207   have xb: "R\<^sup>*\<^sup>* x b" .
   208   thus ?case
   209   proof (rule converse_rtranclE')
   210     assume "x = b"
   211     with xc have "R\<^sup>*\<^sup>* b c" by simp
   212     thus ?thesis by iprover
   213   next
   214     fix y
   215     assume xy: "R x y"
   216     assume yb: "R\<^sup>*\<^sup>* y b"
   217     from xc show ?thesis
   218     proof (rule converse_rtranclE')
   219       assume "x = c"
   220       with xb have "R\<^sup>*\<^sup>* c b" by simp
   221       thus ?thesis by iprover
   222     next
   223       fix y'
   224       assume y'c: "R\<^sup>*\<^sup>* y' c"
   225       assume xy': "R x y'"
   226       with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
   227         by (blast dest: lc)
   228       from yb u y'c show ?thesis
   229         by (blast del: rtrancl.rtrancl_refl
   230             intro: rtrancl_trans'
   231             dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
   232     qed
   233   qed
   234 qed
   235 
   236 end