src/HOL/ex/Rewrite_Examples.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 60117 2712f40d6309
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
bundle lifting_syntax;
noschinl@59739
     1
theory Rewrite_Examples
noschinl@59739
     2
imports Main "~~/src/HOL/Library/Rewrite"
noschinl@59739
     3
begin
noschinl@59739
     4
noschinl@59739
     5
section \<open>The rewrite Proof Method by Example\<close>
noschinl@59739
     6
noschinl@59739
     7
(* This file is intended to give an overview over
noschinl@59739
     8
   the features of the pattern-based rewrite proof method.
noschinl@59739
     9
noschinl@59739
    10
   See also https://www21.in.tum.de/~noschinl/Pattern-2014/
noschinl@59739
    11
*)
noschinl@59739
    12
lemma
noschinl@59739
    13
  fixes a::int and b::int and c::int
noschinl@59739
    14
  assumes "P (b + a)"
noschinl@59739
    15
  shows "P (a + b)"
noschinl@59739
    16
by (rewrite at "a + b" add.commute)
noschinl@59739
    17
   (rule assms)
noschinl@59739
    18
noschinl@59739
    19
(* Selecting a specific subterm in a large, ambiguous term. *)
noschinl@59739
    20
lemma
noschinl@59739
    21
  fixes a b c :: int
noschinl@59739
    22
  assumes "f (a - a + (a - a)) + f (   0    + c) = f 0 + f c"
noschinl@59739
    23
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047
    24
  by (rewrite in "f _ + f \<hole> = _" diff_self) fact
noschinl@59739
    25
noschinl@59739
    26
lemma
noschinl@59739
    27
  fixes a b c :: int
noschinl@59739
    28
  assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
noschinl@59739
    29
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047
    30
  by (rewrite at "f (_ + \<hole>) + f _ = _" diff_self) fact
noschinl@59739
    31
noschinl@59739
    32
lemma
noschinl@59739
    33
  fixes a b c :: int
noschinl@59739
    34
  assumes "f (  0   + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@59739
    35
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047
    36
  by (rewrite in "f (\<hole> + _) + _ = _" diff_self) fact
noschinl@59739
    37
noschinl@59739
    38
lemma
noschinl@59739
    39
  fixes a b c :: int
noschinl@59739
    40
  assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
noschinl@59739
    41
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047
    42
  by (rewrite in "f (_ + \<hole>) + _ = _" diff_self) fact
noschinl@59739
    43
noschinl@59739
    44
lemma
noschinl@59739
    45
  fixes x y :: nat
noschinl@59739
    46
  shows"x + y > c \<Longrightarrow> y + x > c"
noschinl@60047
    47
  by (rewrite at "\<hole> > c" add.commute) assumption
noschinl@59739
    48
noschinl@59739
    49
(* We can also rewrite in the assumptions.  *)
noschinl@59739
    50
lemma
noschinl@59739
    51
  fixes x y :: nat
noschinl@59739
    52
  assumes "y + x > c \<Longrightarrow> y + x > c"
noschinl@59739
    53
  shows   "x + y > c \<Longrightarrow> y + x > c"
noschinl@59739
    54
  by (rewrite in asm add.commute) fact
noschinl@59739
    55
noschinl@59739
    56
lemma
noschinl@59739
    57
  fixes x y :: nat
noschinl@59739
    58
  assumes "y + x > c \<Longrightarrow> y + x > c"
noschinl@59739
    59
  shows   "x + y > c \<Longrightarrow> y + x > c"
noschinl@59739
    60
  by (rewrite in "x + y > c" at asm add.commute) fact
noschinl@59739
    61
noschinl@59739
    62
lemma
noschinl@59739
    63
  fixes x y :: nat
noschinl@59739
    64
  assumes "y + x > c \<Longrightarrow> y + x > c"
noschinl@59739
    65
  shows   "x + y > c \<Longrightarrow> y + x > c"
noschinl@60047
    66
  by (rewrite at "\<hole> > c" at asm  add.commute) fact
noschinl@59739
    67
noschinl@59739
    68
lemma
noschinl@59739
    69
  assumes "P {x::int. y + 1 = 1 + x}"
noschinl@59739
    70
  shows   "P {x::int. y + 1 = x + 1}"
noschinl@60047
    71
  by (rewrite at "x+1" in "{x::int. \<hole> }" add.commute) fact
noschinl@59739
    72
noschinl@59739
    73
lemma
noschinl@59739
    74
  assumes "P {x::int. y + 1 = 1 + x}"
noschinl@59739
    75
  shows   "P {x::int. y + 1 = x + 1}"
noschinl@60047
    76
  by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<hole> }" add.commute)
noschinl@59739
    77
   fact
noschinl@59739
    78
noschinl@59739
    79
lemma
noschinl@59739
    80
  assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. s * t + y - 3)}"
noschinl@59739
    81
  shows   "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}"
noschinl@60047
    82
  by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact
noschinl@59739
    83
noschinl@60052
    84
(* This is not limited to the first assumption *)
noschinl@60052
    85
lemma
noschinl@60052
    86
  assumes "PROP P \<equiv> PROP Q"
noschinl@60052
    87
  shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
noschinl@60052
    88
    by (rewrite at asm assms)
noschinl@60052
    89
noschinl@60117
    90
lemma
noschinl@60117
    91
  assumes "PROP P \<equiv> PROP Q"
noschinl@60117
    92
  shows "PROP R \<Longrightarrow> PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
noschinl@60117
    93
    by (rewrite at asm assms)
noschinl@60117
    94
noschinl@60053
    95
(* Rewriting "at asm" selects each full assumption, not any parts *)
noschinl@60053
    96
lemma
noschinl@60053
    97
  assumes "(PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP S \<Longrightarrow> PROP R)"
noschinl@60053
    98
  shows "PROP S \<Longrightarrow> (PROP P \<Longrightarrow> PROP Q) \<Longrightarrow> PROP R"
noschinl@60053
    99
  apply (rewrite at asm assms)
noschinl@60053
   100
  apply assumption
noschinl@60053
   101
  done
noschinl@60053
   102
noschinl@60052
   103
noschinl@59739
   104
noschinl@59739
   105
(* Rewriting with conditional rewriting rules works just as well. *)
noschinl@59739
   106
lemma test_theorem:
noschinl@59739
   107
  fixes x :: nat
noschinl@59739
   108
  shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y"
noschinl@59739
   109
  by (rule Orderings.order_antisym)
noschinl@59739
   110
noschinl@60050
   111
(* Premises of the conditional rule yield new subgoals. The
noschinl@60050
   112
   assumptions of the goal are propagated into these subgoals
noschinl@60050
   113
*)
noschinl@59739
   114
lemma
noschinl@60050
   115
  fixes f :: "nat \<Rightarrow> nat"
noschinl@60050
   116
  shows "f x \<le> 0 \<Longrightarrow> f x \<ge> 0 \<Longrightarrow> f x = 0"
noschinl@59739
   117
  apply (rewrite at "f x" to "0" test_theorem)
noschinl@60050
   118
  apply assumption
noschinl@60050
   119
  apply assumption
noschinl@59739
   120
  apply (rule refl)
noschinl@60050
   121
  done
noschinl@59739
   122
noschinl@60054
   123
(* This holds also for rewriting in assumptions. The order of assumptions is preserved *)
noschinl@60054
   124
lemma
noschinl@60054
   125
  assumes rewr: "PROP P \<Longrightarrow> PROP Q \<Longrightarrow> PROP R \<equiv> PROP R'"
noschinl@60054
   126
  assumes A1: "PROP S \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP P"
noschinl@60054
   127
  assumes A2: "PROP S \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP Q"
noschinl@60054
   128
  assumes C: "PROP S \<Longrightarrow> PROP R' \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP V"
noschinl@60054
   129
  shows "PROP S \<Longrightarrow> PROP R \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP V"
noschinl@60054
   130
  apply (rewrite at asm rewr)
noschinl@60054
   131
  apply (fact A1)
noschinl@60054
   132
  apply (fact A2)
noschinl@60054
   133
  apply (fact C)
noschinl@60054
   134
  done
noschinl@60054
   135
noschinl@60054
   136
noschinl@59739
   137
(*
noschinl@59739
   138
   Instantiation.
noschinl@59739
   139
noschinl@59739
   140
   Since all rewriting is now done via conversions,
noschinl@59739
   141
   instantiation becomes fairly easy to do.
noschinl@59739
   142
*)
noschinl@59739
   143
noschinl@59739
   144
(* We first introduce a function f and an extended
noschinl@59739
   145
   version of f that is annotated with an invariant. *)
noschinl@59739
   146
fun f :: "nat \<Rightarrow> nat" where "f n = n"
noschinl@59739
   147
definition "f_inv (I :: nat \<Rightarrow> bool) n \<equiv> f n"
noschinl@59739
   148
noschinl@59739
   149
lemma annotate_f: "f = f_inv I"
noschinl@59739
   150
  by (simp add: f_inv_def fun_eq_iff)
noschinl@59739
   151
noschinl@59739
   152
(* We have a lemma with a bound variable n, and
noschinl@59739
   153
   want to add an invariant to f. *)
noschinl@59739
   154
lemma
noschinl@59739
   155
  assumes "P (\<lambda>n. f_inv (\<lambda>_. True) n + 1) = x"
noschinl@59739
   156
  shows "P (\<lambda>n. f n + 1) = x"
noschinl@59739
   157
  by (rewrite to "f_inv (\<lambda>_. True)" annotate_f) fact
noschinl@59739
   158
noschinl@59739
   159
(* We can also add an invariant that contains the variable n bound in the outer context.
noschinl@59739
   160
   For this, we need to bind this variable to an identifier. *)
noschinl@59739
   161
lemma
noschinl@59739
   162
  assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
noschinl@59739
   163
  shows "P (\<lambda>n. f n + 1) = x"
noschinl@60047
   164
  by (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact
noschinl@59739
   165
noschinl@59739
   166
(* Any identifier will work *)
noschinl@59739
   167
lemma
noschinl@59739
   168
  assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
noschinl@59739
   169
  shows "P (\<lambda>n. f n + 1) = x"
noschinl@60047
   170
  by (rewrite in "\<lambda>abc. \<hole>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact
noschinl@59739
   171
noschinl@59739
   172
(* The "for" keyword. *)
noschinl@59739
   173
lemma
noschinl@59739
   174
  assumes "P (2 + 1)"
noschinl@59739
   175
  shows "\<And>x y. P (1 + 2 :: nat)"
noschinl@59739
   176
by (rewrite in "P (1 + 2)" at for (x) add.commute) fact
noschinl@59739
   177
noschinl@59739
   178
lemma
noschinl@59739
   179
  assumes "\<And>x y. P (y + x)"
noschinl@59739
   180
  shows "\<And>x y. P (x + y :: nat)"
noschinl@59739
   181
by (rewrite in "P (x + _)" at for (x y) add.commute) fact
noschinl@59739
   182
noschinl@59739
   183
lemma
noschinl@59739
   184
  assumes "\<And>x y z. y + x + z = z + y + (x::int)"
noschinl@59739
   185
  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
noschinl@60108
   186
by (rewrite at "x + y" in "x + y + z" in for (x y z) add.commute) fact
noschinl@59739
   187
noschinl@59739
   188
lemma
noschinl@59739
   189
  assumes "\<And>x y z. z + (x + y) = z + y + (x::int)"
noschinl@59739
   190
  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
noschinl@60108
   191
by (rewrite at "(_ + y) + z" in for (y z) add.commute) fact
noschinl@59739
   192
noschinl@59739
   193
lemma
noschinl@59739
   194
  assumes "\<And>x y z. x + y + z = y + z + (x::int)"
noschinl@59739
   195
  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
noschinl@60108
   196
by (rewrite at "\<hole> + _" at "_ = \<hole>" in for () add.commute) fact
noschinl@59739
   197
noschinl@60108
   198
lemma
noschinl@60108
   199
  assumes eq: "\<And>x. P x \<Longrightarrow> g x = x"
noschinl@60108
   200
  assumes f1: "\<And>x. Q x \<Longrightarrow> P x"
noschinl@60108
   201
  assumes f2: "\<And>x. Q x \<Longrightarrow> x"
noschinl@60108
   202
  shows "\<And>x. Q x \<Longrightarrow> g x"
noschinl@60108
   203
  apply (rewrite at "g x" in for (x) eq)
noschinl@60108
   204
  apply (fact f1)
noschinl@60108
   205
  apply (fact f2)
noschinl@60108
   206
  done
noschinl@60108
   207
noschinl@60108
   208
(* The for keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
noschinl@59739
   209
lemma
noschinl@59739
   210
  assumes "(\<And>(x::int). x < 1 + x)"
noschinl@59739
   211
  and     "(x::int) + 1 > x"
noschinl@59739
   212
  shows   "(\<And>(x::int). x + 1 > x) \<Longrightarrow> (x::int) + 1 > x"
noschinl@59739
   213
by (rewrite at "x + 1" in for (x) at asm add.commute)
noschinl@59739
   214
   (rule assms)
noschinl@59739
   215
noschinl@60079
   216
(* The rewrite method also has an ML interface *)
noschinl@60079
   217
lemma
noschinl@60079
   218
  assumes "\<And>a b. P ((a + 1) * (1 + b)) "
noschinl@60079
   219
  shows "\<And>a b :: nat. P ((a + 1) * (b + 1))"
noschinl@60079
   220
  apply (tactic \<open>
noschinl@60079
   221
    let
noschinl@60079
   222
      val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context}
noschinl@60079
   223
      (* Note that the pattern order is reversed *)
noschinl@60079
   224
      val pat = [
noschinl@60079
   225
        Rewrite.For [(x, SOME @{typ nat})],
noschinl@60079
   226
        Rewrite.In,
noschinl@60079
   227
        Rewrite.Term (@{const plus(nat)} $ Free (x, @{typ nat}) $ @{term "1 :: nat"}, [])]
noschinl@60079
   228
      val to = NONE
noschinl@60117
   229
    in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
noschinl@60079
   230
  \<close>)
noschinl@60079
   231
  apply (fact assms)
noschinl@60079
   232
  done
noschinl@60079
   233
noschinl@60079
   234
lemma
noschinl@60079
   235
  assumes "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. a + b))"
noschinl@60079
   236
  shows "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. b + a))"
noschinl@60079
   237
  apply (tactic \<open>
noschinl@60079
   238
    let
noschinl@60079
   239
      val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context}
noschinl@60079
   240
      val pat = [
noschinl@60079
   241
        Rewrite.Concl,
noschinl@60079
   242
        Rewrite.In,
noschinl@60079
   243
        Rewrite.Term (Free ("Q", (@{typ "int"} --> TVar (("'b",0), [])) --> @{typ bool})
noschinl@60079
   244
          $ Abs ("x", @{typ int}, Rewrite.mk_hole 1 (@{typ int} --> TVar (("'b",0), [])) $ Bound 0), [(x, @{typ int})]),
noschinl@60079
   245
        Rewrite.In,
noschinl@60079
   246
        Rewrite.Term (@{const plus(int)} $ Free (x, @{typ int}) $ Var (("c", 0), @{typ int}), [])
noschinl@60079
   247
        ]
noschinl@60079
   248
      val to = NONE
noschinl@60117
   249
    in CCONVERSION (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) 1 end
noschinl@60079
   250
  \<close>)
noschinl@60079
   251
  apply (fact assms)
noschinl@60079
   252
  done
noschinl@60079
   253
noschinl@60079
   254
(* There is also conversion-like rewrite function: *)
noschinl@60079
   255
ML \<open>
noschinl@60079
   256
  val ct = @{cprop "Q (\<lambda>b :: int. P (\<lambda>a. a + b) (\<lambda>a. b + a))"}
noschinl@60079
   257
  val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context}
noschinl@60079
   258
  val pat = [
noschinl@60079
   259
    Rewrite.Concl,
noschinl@60079
   260
    Rewrite.In,
noschinl@60079
   261
    Rewrite.Term (Free ("Q", (@{typ "int"} --> TVar (("'b",0), [])) --> @{typ bool})
noschinl@60079
   262
      $ Abs ("x", @{typ int}, Rewrite.mk_hole 1 (@{typ int} --> TVar (("'b",0), [])) $ Bound 0), [(x, @{typ int})]),
noschinl@60079
   263
    Rewrite.In,
noschinl@60079
   264
    Rewrite.Term (@{const plus(int)} $ Free (x, @{typ int}) $ Var (("c", 0), @{typ int}), [])
noschinl@60079
   265
    ]
noschinl@60079
   266
  val to = NONE
noschinl@60117
   267
  val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct
noschinl@60079
   268
\<close>
noschinl@60079
   269
noschinl@60088
   270
section \<open>Regression tests\<close>
noschinl@60088
   271
noschinl@60088
   272
ML \<open>
noschinl@60088
   273
  val ct = @{cterm "(\<lambda>b :: int. (\<lambda>a. b + a))"}
noschinl@60088
   274
  val (x, ctxt) = yield_singleton Variable.add_fixes "x" @{context}
noschinl@60088
   275
  val pat = [
noschinl@60088
   276
    Rewrite.In,
noschinl@60088
   277
    Rewrite.Term (@{const plus(int)} $ Var (("c", 0), @{typ int}) $ Var (("c", 0), @{typ int}), [])
noschinl@60088
   278
    ]
noschinl@60088
   279
  val to = NONE
noschinl@60117
   280
  val _ =
noschinl@60117
   281
    case try (Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute}) ct of
noschinl@60117
   282
      NONE => ()
noschinl@60088
   283
    | _ => error "should not have matched anything"
noschinl@60088
   284
\<close>
noschinl@60088
   285
noschinl@60117
   286
ML \<open>
noschinl@60117
   287
  Rewrite.params_pconv (Conv.all_conv |> K |> K) @{context} (Vartab.empty, []) @{cterm "\<And>x. PROP A"}
noschinl@60117
   288
\<close>
noschinl@60088
   289
noschinl@60117
   290
lemma
noschinl@60117
   291
  assumes eq: "PROP A \<Longrightarrow> PROP B \<equiv> PROP C"
noschinl@60117
   292
  assumes f1: "PROP D \<Longrightarrow> PROP A"
noschinl@60117
   293
  assumes f2: "PROP D \<Longrightarrow> PROP C"
noschinl@60117
   294
  shows "\<And>x. PROP D \<Longrightarrow> PROP B"
noschinl@60117
   295
  apply (rewrite eq)
noschinl@60117
   296
  apply (fact f1)
noschinl@60117
   297
  apply (fact f2)
noschinl@60117
   298
  done
noschinl@60088
   299
noschinl@59739
   300
end