src/HOL/Proofs/Lambda/Commutation.thy
 author wenzelm Mon Sep 06 19:13:10 2010 +0200 (2010-09-06) changeset 39159 0dec18004e75 parent 39157 b98909faaea8 child 42793 88bee9f6eec7 permissions -rw-r--r--
more antiquotations;
```     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_level = 100]]
```
```    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 (fastsimp 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 HOL_cs *})
```
```   131    apply (tactic {*
```
```   132      blast_tac (HOL_cs 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
```