src/HOL/Proofs/Lambda/Commutation.thy
author haftmann
Sat, 05 Jul 2014 11:01:53 +0200
changeset 57514 bdc2c6b40bf2
parent 46512 4f9f61f9b535
child 58372 bfd497f2f4c2
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39126
diff changeset
     1
(*  Title:      HOL/Proofs/Lambda/Commutation.thy
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1302
diff changeset
     2
    Author:     Tobias Nipkow
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     3
    Copyright   1995  TU Muenchen
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     4
*)
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
     5
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
     6
header {* Abstract commutation and confluence notions *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13550
diff changeset
     8
theory Commutation imports Main begin
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
     9
46512
4f9f61f9b535 simplified configuration options for syntax ambiguity;
wenzelm
parents: 46506
diff changeset
    10
declare [[syntax_ambiguity_warning = false]]
39126
ee117c5b3b75 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents: 36862
diff changeset
    11
ee117c5b3b75 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents: 36862
diff changeset
    12
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    13
subsection {* Basic definitions *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    14
19086
1b3780be6cc2 new-style definitions/abbreviations;
wenzelm
parents: 18513
diff changeset
    15
definition
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    16
  square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
19086
1b3780be6cc2 new-style definitions/abbreviations;
wenzelm
parents: 18513
diff changeset
    17
  "square R S T U =
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    18
    (\<forall>x y. R x y --> (\<forall>z. S x z --> (\<exists>u. T y u \<and> U z u)))"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    19
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19363
diff changeset
    20
definition
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    21
  commute :: "['a => 'a => bool, 'a => 'a => bool] => bool" where
19086
1b3780be6cc2 new-style definitions/abbreviations;
wenzelm
parents: 18513
diff changeset
    22
  "commute R S = square R S S R"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    23
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19363
diff changeset
    24
definition
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    25
  diamond :: "('a => 'a => bool) => bool" where
19086
1b3780be6cc2 new-style definitions/abbreviations;
wenzelm
parents: 18513
diff changeset
    26
  "diamond R = commute R R"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    27
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19363
diff changeset
    28
definition
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    29
  Church_Rosser :: "('a => 'a => bool) => bool" where
19086
1b3780be6cc2 new-style definitions/abbreviations;
wenzelm
parents: 18513
diff changeset
    30
  "Church_Rosser R =
22422
ee19cdb07528 stepping towards uniform lattice theory development in HOL
haftmann
parents: 22270
diff changeset
    31
    (\<forall>x y. (sup R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    32
19363
667b5ea637dd refined 'abbreviation';
wenzelm
parents: 19086
diff changeset
    33
abbreviation
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    34
  confluent :: "('a => 'a => bool) => bool" where
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    35
  "confluent R == diamond (R^**)"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    36
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    37
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    38
subsection {* Basic lemmas *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    39
25972
94b15338da8d tuned document;
wenzelm
parents: 23815
diff changeset
    40
subsubsection {* @{text "square"} *}
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    41
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    42
lemma square_sym: "square R S T U ==> square S R U T"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    43
  apply (unfold square_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    44
  apply blast
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    45
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    46
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    47
lemma square_subset:
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    48
    "[| square R S T U; T \<le> T' |] ==> square R S T' U"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    49
  apply (unfold square_def)
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    50
  apply (blast dest: predicate2D)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    51
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    52
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    53
lemma square_reflcl:
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    54
    "[| square R S T (R^==); S \<le> T |] ==> square (R^==) S T (R^==)"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    55
  apply (unfold square_def)
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    56
  apply (blast dest: predicate2D)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    57
  done
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    58
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    59
lemma square_rtrancl:
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    60
    "square R S S T ==> square (R^**) S S (T^**)"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    61
  apply (unfold square_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    62
  apply (intro strip)
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
    63
  apply (erule rtranclp_induct)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    64
   apply blast
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
    65
  apply (blast intro: rtranclp.rtrancl_into_rtrancl)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    66
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    67
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    68
lemma square_rtrancl_reflcl_commute:
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    69
    "square R S (S^**) (R^==) ==> commute (R^**) (S^**)"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    70
  apply (unfold commute_def)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 42793
diff changeset
    71
  apply (fastforce dest: square_reflcl square_sym [THEN square_rtrancl])
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    72
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    73
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
    74
25972
94b15338da8d tuned document;
wenzelm
parents: 23815
diff changeset
    75
subsubsection {* @{text "commute"} *}
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    76
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    77
lemma commute_sym: "commute R S ==> commute S R"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    78
  apply (unfold commute_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    79
  apply (blast intro: square_sym)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    80
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    81
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
    82
lemma commute_rtrancl: "commute R S ==> commute (R^**) (S^**)"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    83
  apply (unfold commute_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    84
  apply (blast intro: square_rtrancl square_sym)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    85
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    86
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    87
lemma commute_Un:
22422
ee19cdb07528 stepping towards uniform lattice theory development in HOL
haftmann
parents: 22270
diff changeset
    88
    "[| commute R T; commute S T |] ==> commute (sup R S) T"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    89
  apply (unfold commute_def square_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    90
  apply blast
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    91
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    92
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    93
25972
94b15338da8d tuned document;
wenzelm
parents: 23815
diff changeset
    94
subsubsection {* @{text "diamond"}, @{text "confluence"}, and @{text "union"} *}
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    95
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    96
lemma diamond_Un:
22422
ee19cdb07528 stepping towards uniform lattice theory development in HOL
haftmann
parents: 22270
diff changeset
    97
    "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
    98
  apply (unfold diamond_def)
23815
paulson
parents: 23750
diff changeset
    99
  apply (blast intro: commute_Un commute_sym) 
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   100
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   101
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   102
lemma diamond_confluent: "diamond R ==> confluent R"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   103
  apply (unfold diamond_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   104
  apply (erule commute_rtrancl)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   105
  done
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
   106
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   107
lemma square_reflcl_confluent:
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   108
    "square R R (R^==) (R^==) ==> confluent R"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   109
  apply (unfold diamond_def)
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   110
  apply (fast intro: square_rtrancl_reflcl_commute elim: square_subset)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   111
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   112
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   113
lemma confluent_Un:
22422
ee19cdb07528 stepping towards uniform lattice theory development in HOL
haftmann
parents: 22270
diff changeset
   114
    "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (sup R S)"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   115
  apply (rule rtranclp_sup_rtranclp [THEN subst])
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   116
  apply (blast dest: diamond_Un intro: diamond_confluent)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   117
  done
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
   118
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   119
lemma diamond_to_confluence:
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   120
    "[| diamond R; T \<le> R; R \<le> T^** |] ==> confluent T"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   121
  apply (force intro: diamond_confluent
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   122
    dest: rtranclp_subset [symmetric])
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   123
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   124
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   125
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   126
subsection {* Church-Rosser *}
1278
7e6189fc833c Commutation replaces Confluence
nipkow
parents:
diff changeset
   127
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   128
lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   129
  apply (unfold square_def commute_def diamond_def Church_Rosser_def)
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 39159
diff changeset
   130
  apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   131
   apply (tactic {*
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 39159
diff changeset
   132
     blast_tac (put_claset HOL_cs @{context} addIs
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 39157
diff changeset
   133
       [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
0dec18004e75 more antiquotations;
wenzelm
parents: 39157
diff changeset
   134
        @{thm rtranclp_converseI}, @{thm conversepI},
0dec18004e75 more antiquotations;
wenzelm
parents: 39157
diff changeset
   135
        @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *})
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   136
  apply (erule rtranclp_induct)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   137
   apply blast
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   138
  apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   139
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 8624
diff changeset
   140
13089
c8c28a1dc787 Added proof of Newman's lemma.
berghofe
parents: 10212
diff changeset
   141
c8c28a1dc787 Added proof of Newman's lemma.
berghofe
parents: 10212
diff changeset
   142
subsection {* Newman's lemma *}
c8c28a1dc787 Added proof of Newman's lemma.
berghofe
parents: 10212
diff changeset
   143
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   144
text {* Proof by Stefan Berghofer *}
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   145
13343
3b2b18c58d80 *** empty log message ***
nipkow
parents: 13331
diff changeset
   146
theorem newman:
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   147
  assumes wf: "wfP (R\<inverse>\<inverse>)"
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   148
  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   149
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   150
  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   151
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   152
  using wf
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   153
proof induct
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   154
  case (less x b c)
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22422
diff changeset
   155
  have xc: "R\<^sup>*\<^sup>* x c" by fact
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22422
diff changeset
   156
  have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   157
  proof (rule converse_rtranclpE)
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   158
    assume "x = b"
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   159
    with xc have "R\<^sup>*\<^sup>* b c" by simp
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   160
    thus ?thesis by iprover
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   161
  next
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   162
    fix y
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   163
    assume xy: "R x y"
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   164
    assume yb: "R\<^sup>*\<^sup>* y b"
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   165
    from xc show ?thesis
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   166
    proof (rule converse_rtranclpE)
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   167
      assume "x = c"
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   168
      with xb have "R\<^sup>*\<^sup>* c b" by simp
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   169
      thus ?thesis by iprover
13089
c8c28a1dc787 Added proof of Newman's lemma.
berghofe
parents: 10212
diff changeset
   170
    next
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   171
      fix y'
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   172
      assume y'c: "R\<^sup>*\<^sup>* y' c"
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   173
      assume xy': "R x y'"
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   174
      with xy have "\<exists>u. R\<^sup>*\<^sup>* y u \<and> R\<^sup>*\<^sup>* y' u" by (rule lc)
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   175
      then obtain u where yu: "R\<^sup>*\<^sup>* y u" and y'u: "R\<^sup>*\<^sup>* y' u" by iprover
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   176
      from xy have "R\<inverse>\<inverse> y x" ..
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   177
      from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   178
      then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   179
      from xy' have "R\<inverse>\<inverse> y' x" ..
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   180
      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtranclp_trans)
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   181
      moreover note y'c
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   182
      ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   183
      then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   184
      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtranclp_trans)
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   185
      with cw show ?thesis by iprover
13089
c8c28a1dc787 Added proof of Newman's lemma.
berghofe
parents: 10212
diff changeset
   186
    qed
c8c28a1dc787 Added proof of Newman's lemma.
berghofe
parents: 10212
diff changeset
   187
  qed
c8c28a1dc787 Added proof of Newman's lemma.
berghofe
parents: 10212
diff changeset
   188
qed
c8c28a1dc787 Added proof of Newman's lemma.
berghofe
parents: 10212
diff changeset
   189
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   190
text {*
28455
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   191
  Alternative version.  Partly automated by Tobias
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   192
  Nipkow. Takes 2 minutes (2002).
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   193
28455
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   194
  This is the maximal amount of automation possible using @{text blast}.
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   195
*}
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   196
13349
7d4441c8c46a Added "using" to the beginning of original newman proof again, because
berghofe
parents: 13346
diff changeset
   197
theorem newman':
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   198
  assumes wf: "wfP (R\<inverse>\<inverse>)"
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   199
  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   200
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   201
  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   202
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
   203
  using wf
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   204
proof induct
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   205
  case (less x b c)
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   206
  note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   207
                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
23464
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22422
diff changeset
   208
  have xc: "R\<^sup>*\<^sup>* x c" by fact
bc2563c37b1a tuned proofs -- avoid implicit prems;
wenzelm
parents: 22422
diff changeset
   209
  have xb: "R\<^sup>*\<^sup>* x b" by fact
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   210
  thus ?case
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   211
  proof (rule converse_rtranclpE)
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   212
    assume "x = b"
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   213
    with xc have "R\<^sup>*\<^sup>* b c" by simp
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   214
    thus ?thesis by iprover
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   215
  next
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   216
    fix y
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   217
    assume xy: "R x y"
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   218
    assume yb: "R\<^sup>*\<^sup>* y b"
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   219
    from xc show ?thesis
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   220
    proof (rule converse_rtranclpE)
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   221
      assume "x = c"
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   222
      with xb have "R\<^sup>*\<^sup>* c b" by simp
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   223
      thus ?thesis by iprover
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   224
    next
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   225
      fix y'
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   226
      assume y'c: "R\<^sup>*\<^sup>* y' c"
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   227
      assume xy': "R x y'"
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   228
      with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
   229
        by (blast dest: lc)
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   230
      from yb u y'c show ?thesis
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   231
        by (blast del: rtranclp.rtrancl_refl
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 23464
diff changeset
   232
            intro: rtranclp_trans
22270
4ccb7e6be929 Converted to predicate notation.
berghofe
parents: 21669
diff changeset
   233
            dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
13346
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   234
    qed
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   235
  qed
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   236
qed
6918b6d5192b Added partly automated version of Newman.
nipkow
parents: 13343
diff changeset
   237
28455
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   238
text {*
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   239
  Using the coherent logic prover, the proof of the induction step
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   240
  is completely automatic.
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   241
*}
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   242
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   243
lemma eq_imp_rtranclp: "x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y"
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   244
  by simp
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   245
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   246
theorem newman'':
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   247
  assumes wf: "wfP (R\<inverse>\<inverse>)"
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   248
  and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   249
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   250
  shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   251
    \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   252
  using wf
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   253
proof induct
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   254
  case (less x b c)
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   255
  note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   256
                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   257
  show ?case
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   258
    by (coherent
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   259
      `R\<^sup>*\<^sup>* x c` `R\<^sup>*\<^sup>* x b`
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   260
      refl [where 'a='a] sym
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   261
      eq_imp_rtranclp
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   262
      r_into_rtranclp [of R]
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   263
      rtranclp_trans
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   264
      lc IH [OF conversepI]
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   265
      converse_rtranclpE)
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   266
qed
a79701b14a30 Yet another proof of Newman's lemma, this time using the coherent logic prover.
berghofe
parents: 25972
diff changeset
   267
10179
9d5678e6bf34 added rtranclIs
nipkow
parents: 9811
diff changeset
   268
end