src/HOL/Proofs/Lambda/Commutation.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 46512 4f9f61f9b535
child 58372 bfd497f2f4c2
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Proofs/Lambda/Commutation.thy
     2     Author:     Tobias Nipkow
     3     Copyright   1995  TU Muenchen
     4 *)
     5 
     6 header {* Abstract commutation and confluence notions *}
     7 
     8 theory Commutation imports Main begin
     9 
    10 declare [[syntax_ambiguity_warning = false]]
    11 
    12 
    13 subsection {* Basic definitions *}
    14 
    15 definition
    16   square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
    17   "square R S T U =
    18     (\<forall>x y. R x y --> (\<forall>z. S x z --> (\<exists>u. T y u \<and> U z u)))"
    19 
    20 definition
    21   commute :: "['a => 'a => bool, 'a => 'a => bool] => bool" where
    22   "commute R S = square R S S R"
    23 
    24 definition
    25   diamond :: "('a => 'a => bool) => bool" where
    26   "diamond R = commute R R"
    27 
    28 definition
    29   Church_Rosser :: "('a => 'a => bool) => bool" where
    30   "Church_Rosser R =
    31     (\<forall>x y. (sup R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
    32 
    33 abbreviation
    34   confluent :: "('a => 'a => bool) => bool" where
    35   "confluent R == diamond (R^**)"
    36 
    37 
    38 subsection {* Basic lemmas *}
    39 
    40 subsubsection {* @{text "square"} *}
    41 
    42 lemma square_sym: "square R S T U ==> square S R U T"
    43   apply (unfold square_def)
    44   apply blast
    45   done
    46 
    47 lemma square_subset:
    48     "[| square R S T U; T \<le> T' |] ==> square R S T' U"
    49   apply (unfold square_def)
    50   apply (blast dest: predicate2D)
    51   done
    52 
    53 lemma square_reflcl:
    54     "[| square R S T (R^==); S \<le> T |] ==> square (R^==) S T (R^==)"
    55   apply (unfold square_def)
    56   apply (blast dest: predicate2D)
    57   done
    58 
    59 lemma square_rtrancl:
    60     "square R S S T ==> square (R^**) S S (T^**)"
    61   apply (unfold square_def)
    62   apply (intro strip)
    63   apply (erule rtranclp_induct)
    64    apply blast
    65   apply (blast intro: rtranclp.rtrancl_into_rtrancl)
    66   done
    67 
    68 lemma square_rtrancl_reflcl_commute:
    69     "square R S (S^**) (R^==) ==> commute (R^**) (S^**)"
    70   apply (unfold commute_def)
    71   apply (fastforce dest: square_reflcl square_sym [THEN square_rtrancl])
    72   done
    73 
    74 
    75 subsubsection {* @{text "commute"} *}
    76 
    77 lemma commute_sym: "commute R S ==> commute S R"
    78   apply (unfold commute_def)
    79   apply (blast intro: square_sym)
    80   done
    81 
    82 lemma commute_rtrancl: "commute R S ==> commute (R^**) (S^**)"
    83   apply (unfold commute_def)
    84   apply (blast intro: square_rtrancl square_sym)
    85   done
    86 
    87 lemma commute_Un:
    88     "[| commute R T; commute S T |] ==> commute (sup R S) T"
    89   apply (unfold commute_def square_def)
    90   apply blast
    91   done
    92 
    93 
    94 subsubsection {* @{text "diamond"}, @{text "confluence"}, and @{text "union"} *}
    95 
    96 lemma diamond_Un:
    97     "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
    98   apply (unfold diamond_def)
    99   apply (blast intro: commute_Un commute_sym) 
   100   done
   101 
   102 lemma diamond_confluent: "diamond R ==> confluent R"
   103   apply (unfold diamond_def)
   104   apply (erule commute_rtrancl)
   105   done
   106 
   107 lemma square_reflcl_confluent:
   108     "square R R (R^==) (R^==) ==> confluent R"
   109   apply (unfold diamond_def)
   110   apply (fast intro: square_rtrancl_reflcl_commute elim: square_subset)
   111   done
   112 
   113 lemma confluent_Un:
   114     "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (sup R S)"
   115   apply (rule rtranclp_sup_rtranclp [THEN subst])
   116   apply (blast dest: diamond_Un intro: diamond_confluent)
   117   done
   118 
   119 lemma diamond_to_confluence:
   120     "[| diamond R; T \<le> R; R \<le> T^** |] ==> confluent T"
   121   apply (force intro: diamond_confluent
   122     dest: rtranclp_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 (put_claset HOL_cs @{context}) *})
   131    apply (tactic {*
   132      blast_tac (put_claset HOL_cs @{context} addIs
   133        [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
   134         @{thm rtranclp_converseI}, @{thm conversepI},
   135         @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *})
   136   apply (erule rtranclp_induct)
   137    apply blast
   138   apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans)
   139   done
   140 
   141 
   142 subsection {* Newman's lemma *}
   143 
   144 text {* Proof by Stefan Berghofer *}
   145 
   146 theorem newman:
   147   assumes wf: "wfP (R\<inverse>\<inverse>)"
   148   and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
   149     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   150   shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
   151     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   152   using wf
   153 proof induct
   154   case (less x b c)
   155   have xc: "R\<^sup>*\<^sup>* x c" by fact
   156   have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case
   157   proof (rule converse_rtranclpE)
   158     assume "x = b"
   159     with xc have "R\<^sup>*\<^sup>* b c" by simp
   160     thus ?thesis by iprover
   161   next
   162     fix y
   163     assume xy: "R x y"
   164     assume yb: "R\<^sup>*\<^sup>* y b"
   165     from xc show ?thesis
   166     proof (rule converse_rtranclpE)
   167       assume "x = c"
   168       with xb have "R\<^sup>*\<^sup>* c b" by simp
   169       thus ?thesis by iprover
   170     next
   171       fix y'
   172       assume y'c: "R\<^sup>*\<^sup>* y' c"
   173       assume xy': "R x y'"
   174       with xy have "\<exists>u. R\<^sup>*\<^sup>* y u \<and> R\<^sup>*\<^sup>* y' u" by (rule lc)
   175       then obtain u where yu: "R\<^sup>*\<^sup>* y u" and y'u: "R\<^sup>*\<^sup>* y' u" by iprover
   176       from xy have "R\<inverse>\<inverse> y x" ..
   177       from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
   178       then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
   179       from xy' have "R\<inverse>\<inverse> y' x" ..
   180       moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtranclp_trans)
   181       moreover note y'c
   182       ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
   183       then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
   184       from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtranclp_trans)
   185       with cw show ?thesis by iprover
   186     qed
   187   qed
   188 qed
   189 
   190 text {*
   191   Alternative version.  Partly automated by Tobias
   192   Nipkow. Takes 2 minutes (2002).
   193 
   194   This is the maximal amount of automation possible using @{text blast}.
   195 *}
   196 
   197 theorem newman':
   198   assumes wf: "wfP (R\<inverse>\<inverse>)"
   199   and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
   200     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   201   shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
   202     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   203   using wf
   204 proof induct
   205   case (less x b c)
   206   note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
   207                      \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
   208   have xc: "R\<^sup>*\<^sup>* x c" by fact
   209   have xb: "R\<^sup>*\<^sup>* x b" by fact
   210   thus ?case
   211   proof (rule converse_rtranclpE)
   212     assume "x = b"
   213     with xc have "R\<^sup>*\<^sup>* b c" by simp
   214     thus ?thesis by iprover
   215   next
   216     fix y
   217     assume xy: "R x y"
   218     assume yb: "R\<^sup>*\<^sup>* y b"
   219     from xc show ?thesis
   220     proof (rule converse_rtranclpE)
   221       assume "x = c"
   222       with xb have "R\<^sup>*\<^sup>* c b" by simp
   223       thus ?thesis by iprover
   224     next
   225       fix y'
   226       assume y'c: "R\<^sup>*\<^sup>* y' c"
   227       assume xy': "R x y'"
   228       with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
   229         by (blast dest: lc)
   230       from yb u y'c show ?thesis
   231         by (blast del: rtranclp.rtrancl_refl
   232             intro: rtranclp_trans
   233             dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
   234     qed
   235   qed
   236 qed
   237 
   238 text {*
   239   Using the coherent logic prover, the proof of the induction step
   240   is completely automatic.
   241 *}
   242 
   243 lemma eq_imp_rtranclp: "x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y"
   244   by simp
   245 
   246 theorem newman'':
   247   assumes wf: "wfP (R\<inverse>\<inverse>)"
   248   and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
   249     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   250   shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
   251     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   252   using wf
   253 proof induct
   254   case (less x b c)
   255   note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
   256                      \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
   257   show ?case
   258     by (coherent
   259       `R\<^sup>*\<^sup>* x c` `R\<^sup>*\<^sup>* x b`
   260       refl [where 'a='a] sym
   261       eq_imp_rtranclp
   262       r_into_rtranclp [of R]
   263       rtranclp_trans
   264       lc IH [OF conversepI]
   265       converse_rtranclpE)
   266 qed
   267 
   268 end