src/HOL/ex/Rewrite_Examples.thy
author noschinl
Mon Apr 13 12:18:47 2015 +0200 (2015-04-13)
changeset 60050 dc6ac152d864
parent 60047 58e5b16cbd94
child 60052 616a17640229
permissions -rw-r--r--
rewrite: propagate premises to new subgoals
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
noschinl@59739
    13
lemma
noschinl@59739
    14
  fixes a::int and b::int and c::int
noschinl@59739
    15
  assumes "P (b + a)"
noschinl@59739
    16
  shows "P (a + b)"
noschinl@59739
    17
by (rewrite at "a + b" add.commute)
noschinl@59739
    18
   (rule assms)
noschinl@59739
    19
noschinl@59739
    20
(* Selecting a specific subterm in a large, ambiguous term. *)
noschinl@59739
    21
lemma
noschinl@59739
    22
  fixes a b c :: int
noschinl@59739
    23
  assumes "f (a - a + (a - a)) + f (   0    + c) = f 0 + f c"
noschinl@59739
    24
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047
    25
  by (rewrite in "f _ + f \<hole> = _" diff_self) fact
noschinl@59739
    26
noschinl@59739
    27
lemma
noschinl@59739
    28
  fixes a b c :: int
noschinl@59739
    29
  assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
noschinl@59739
    30
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047
    31
  by (rewrite at "f (_ + \<hole>) + f _ = _" diff_self) fact
noschinl@59739
    32
noschinl@59739
    33
lemma
noschinl@59739
    34
  fixes a b c :: int
noschinl@59739
    35
  assumes "f (  0   + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@59739
    36
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047
    37
  by (rewrite in "f (\<hole> + _) + _ = _" diff_self) fact
noschinl@59739
    38
noschinl@59739
    39
lemma
noschinl@59739
    40
  fixes a b c :: int
noschinl@59739
    41
  assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
noschinl@59739
    42
  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
noschinl@60047
    43
  by (rewrite in "f (_ + \<hole>) + _ = _" diff_self) fact
noschinl@59739
    44
noschinl@59739
    45
lemma
noschinl@59739
    46
  fixes x y :: nat
noschinl@59739
    47
  shows"x + y > c \<Longrightarrow> y + x > c"
noschinl@60047
    48
  by (rewrite at "\<hole> > c" add.commute) assumption
noschinl@59739
    49
noschinl@59739
    50
(* We can also rewrite in the assumptions.  *)
noschinl@59739
    51
lemma
noschinl@59739
    52
  fixes x y :: nat
noschinl@59739
    53
  assumes "y + x > c \<Longrightarrow> y + x > c"
noschinl@59739
    54
  shows   "x + y > c \<Longrightarrow> y + x > c"
noschinl@59739
    55
  by (rewrite in asm add.commute) fact
noschinl@59739
    56
noschinl@59739
    57
lemma
noschinl@59739
    58
  fixes x y :: nat
noschinl@59739
    59
  assumes "y + x > c \<Longrightarrow> y + x > c"
noschinl@59739
    60
  shows   "x + y > c \<Longrightarrow> y + x > c"
noschinl@59739
    61
  by (rewrite in "x + y > c" at asm add.commute) fact
noschinl@59739
    62
noschinl@59739
    63
lemma
noschinl@59739
    64
  fixes x y :: nat
noschinl@59739
    65
  assumes "y + x > c \<Longrightarrow> y + x > c"
noschinl@59739
    66
  shows   "x + y > c \<Longrightarrow> y + x > c"
noschinl@60047
    67
  by (rewrite at "\<hole> > c" at asm  add.commute) fact
noschinl@59739
    68
noschinl@59739
    69
lemma
noschinl@59739
    70
  assumes "P {x::int. y + 1 = 1 + x}"
noschinl@59739
    71
  shows   "P {x::int. y + 1 = x + 1}"
noschinl@60047
    72
  by (rewrite at "x+1" in "{x::int. \<hole> }" add.commute) fact
noschinl@59739
    73
noschinl@59739
    74
lemma
noschinl@59739
    75
  assumes "P {x::int. y + 1 = 1 + x}"
noschinl@59739
    76
  shows   "P {x::int. y + 1 = x + 1}"
noschinl@60047
    77
  by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<hole> }" add.commute)
noschinl@59739
    78
   fact
noschinl@59739
    79
noschinl@59739
    80
lemma
noschinl@59739
    81
  assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. s * t + y - 3)}"
noschinl@59739
    82
  shows   "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}"
noschinl@60047
    83
  by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact
noschinl@59739
    84
noschinl@59739
    85
noschinl@59739
    86
(* Rewriting with conditional rewriting rules works just as well. *)
noschinl@59739
    87
lemma test_theorem:
noschinl@59739
    88
  fixes x :: nat
noschinl@59739
    89
  shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y"
noschinl@59739
    90
  by (rule Orderings.order_antisym)
noschinl@59739
    91
noschinl@60050
    92
(* Premises of the conditional rule yield new subgoals. The
noschinl@60050
    93
   assumptions of the goal are propagated into these subgoals
noschinl@60050
    94
*)
noschinl@59739
    95
lemma
noschinl@60050
    96
  fixes f :: "nat \<Rightarrow> nat"
noschinl@60050
    97
  shows "f x \<le> 0 \<Longrightarrow> f x \<ge> 0 \<Longrightarrow> f x = 0"
noschinl@59739
    98
  apply (rewrite at "f x" to "0" test_theorem)
noschinl@60050
    99
  apply assumption
noschinl@60050
   100
  apply assumption
noschinl@59739
   101
  apply (rule refl)
noschinl@60050
   102
  done
noschinl@59739
   103
noschinl@59739
   104
(*
noschinl@59739
   105
   Instantiation.
noschinl@59739
   106
noschinl@59739
   107
   Since all rewriting is now done via conversions,
noschinl@59739
   108
   instantiation becomes fairly easy to do.
noschinl@59739
   109
*)
noschinl@59739
   110
noschinl@59739
   111
(* We first introduce a function f and an extended
noschinl@59739
   112
   version of f that is annotated with an invariant. *)
noschinl@59739
   113
fun f :: "nat \<Rightarrow> nat" where "f n = n"
noschinl@59739
   114
definition "f_inv (I :: nat \<Rightarrow> bool) n \<equiv> f n"
noschinl@59739
   115
noschinl@59739
   116
lemma annotate_f: "f = f_inv I"
noschinl@59739
   117
  by (simp add: f_inv_def fun_eq_iff)
noschinl@59739
   118
noschinl@59739
   119
(* We have a lemma with a bound variable n, and
noschinl@59739
   120
   want to add an invariant to f. *)
noschinl@59739
   121
lemma
noschinl@59739
   122
  assumes "P (\<lambda>n. f_inv (\<lambda>_. True) n + 1) = x"
noschinl@59739
   123
  shows "P (\<lambda>n. f n + 1) = x"
noschinl@59739
   124
  by (rewrite to "f_inv (\<lambda>_. True)" annotate_f) fact
noschinl@59739
   125
noschinl@59739
   126
(* We can also add an invariant that contains the variable n bound in the outer context.
noschinl@59739
   127
   For this, we need to bind this variable to an identifier. *)
noschinl@59739
   128
lemma
noschinl@59739
   129
  assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
noschinl@59739
   130
  shows "P (\<lambda>n. f n + 1) = x"
noschinl@60047
   131
  by (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact
noschinl@59739
   132
noschinl@59739
   133
(* Any identifier will work *)
noschinl@59739
   134
lemma
noschinl@59739
   135
  assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
noschinl@59739
   136
  shows "P (\<lambda>n. f n + 1) = x"
noschinl@60047
   137
  by (rewrite in "\<lambda>abc. \<hole>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact
noschinl@59739
   138
noschinl@59739
   139
(* The "for" keyword. *)
noschinl@59739
   140
lemma
noschinl@59739
   141
  assumes "P (2 + 1)"
noschinl@59739
   142
  shows "\<And>x y. P (1 + 2 :: nat)"
noschinl@59739
   143
by (rewrite in "P (1 + 2)" at for (x) add.commute) fact
noschinl@59739
   144
noschinl@59739
   145
lemma
noschinl@59739
   146
  assumes "\<And>x y. P (y + x)"
noschinl@59739
   147
  shows "\<And>x y. P (x + y :: nat)"
noschinl@59739
   148
by (rewrite in "P (x + _)" at for (x y) add.commute) fact
noschinl@59739
   149
noschinl@59739
   150
lemma
noschinl@59739
   151
  assumes "\<And>x y z. y + x + z = z + y + (x::int)"
noschinl@59739
   152
  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
noschinl@59739
   153
by (rewrite at "x + y" in "x + y + z" in concl at for (x y z) add.commute) fact
noschinl@59739
   154
noschinl@59739
   155
lemma
noschinl@59739
   156
  assumes "\<And>x y z. z + (x + y) = z + y + (x::int)"
noschinl@59739
   157
  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
noschinl@59739
   158
by (rewrite at "(_ + y) + z" in concl at for (y z) add.commute) fact
noschinl@59739
   159
noschinl@59739
   160
lemma
noschinl@59739
   161
  assumes "\<And>x y z. x + y + z = y + z + (x::int)"
noschinl@59739
   162
  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
noschinl@60047
   163
by (rewrite at "\<hole> + _" at "_ = \<hole>" in concl at for () add.commute) fact
noschinl@59739
   164
noschinl@59739
   165
(* The all-keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
noschinl@59739
   166
lemma
noschinl@59739
   167
  assumes "(\<And>(x::int). x < 1 + x)"
noschinl@59739
   168
  and     "(x::int) + 1 > x"
noschinl@59739
   169
  shows   "(\<And>(x::int). x + 1 > x) \<Longrightarrow> (x::int) + 1 > x"
noschinl@59739
   170
by (rewrite at "x + 1" in for (x) at asm add.commute)
noschinl@59739
   171
   (rule assms)
noschinl@59739
   172
noschinl@59739
   173
end
noschinl@59739
   174