src/HOL/Lambda/Commutation.thy
 author berghofe Wed Jul 11 11:23:24 2007 +0200 (2007-07-11) changeset 23750 a1db5f819d00 parent 23464 bc2563c37b1a child 23815 73dbab55d283 permissions -rw-r--r--
- Renamed inductive2 to inductive
- Renamed some theorems about transitive closure for predicates
```     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. (sup 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 rtranclp_induct)
```
```    62    apply blast
```
```    63   apply (blast intro: rtranclp.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 (sup 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 (sup 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 (sup R S)"
```
```   113   apply (rule rtranclp_sup_rtranclp [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: rtranclp_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 "sup_ge2" RS thm "rtranclp_mono" RS thm "predicate2D" RS thm "rtranclp_trans",
```
```   132         thm "rtranclp_converseI", thm "conversepI",
```
```   133         thm "sup_ge1" RS thm "rtranclp_mono" RS thm "predicate2D"]) 1 *})
```
```   134   apply (erule rtranclp_induct)
```
```   135    apply blast
```
```   136   apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_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" by fact
```
```   154   have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case
```
```   155   proof (rule converse_rtranclpE)
```
```   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_rtranclpE)
```
```   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 rtranclp_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 rtranclp_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" by fact
```
```   207   have xb: "R\<^sup>*\<^sup>* x b" by fact
```
```   208   thus ?case
```
```   209   proof (rule converse_rtranclpE)
```
```   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_rtranclpE)
```
```   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: rtranclp.rtrancl_refl
```
```   230             intro: rtranclp_trans
```
```   231             dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
```
```   232     qed
```
```   233   qed
```
```   234 qed
```
```   235
```
```   236 end
```