[isabelle] specific rewriting?

[Kawin Worrasangasilpa]

Hi,

Lately, I have been working with big summation terms and what I do mostly
is to simplify or unfold it line by line. But then yesterday I found some
weird problem that is when I want to fold a specific term in the expression
below I couldn't get it done by simp, auto or blast as I used to do.
...
also have "... = (∑a∈{f. ∀x. x ∉ {..<n} ⟶ f x = False}. pmf (w_i_pmf n) a
*⇩R
(*Φ_n i (map a [0..<n])* - Φ_n (i-1) (map a [0..<n])))"
using expectation_return_pmf
by (simp add: Δ_n_def)
...
so I want it to be unfolded to:

also have "... = (∑a∈{f. ∀x. x ∉ {..<n} ⟶ f x = False}. pmf (w_i_pmf n) a
*⇩R
(*real_of_int (fst (rev_m (drop (length (map a [0..<n]) - i) (map a
[0..<n]))))*
* + α * real_of_int (min 0 (snd (rev_m (drop (length (map a [0..<n]) - i)
(map a [0..<n])))))*)
- Φ_n (i-1) (map a [0..<n]))"

since I have
definition Φ_n :: "nat ⇒ bool list ⇒ real" where
"Φ_n n l= (λp. real_of_int (fst p) + α * (real_of_int (min 0 (snd p))))
(rev_m (drop (size l - n) l))".
usually, it should be trivial and done by (simp add: Φ_n_def), but this
time it doesn't work. So I would like to ask if there is any tactic that we
can use to replace the exact term at the exact place in an expression with
some term either simpler or more complicated if we know they are equal. I
have never had this problem before and had no idea how trivial it was but I
couldn't find a way to solve it.

Thanks,
Kawin

[Simon Wimmer]

Hi Kawin,

there is the rewrite method in "HOL-Library.Rewrite".
You can have a look at src/HOL/ex/Rewrite_Examples.thy for usage examples.

Simon

Post by Kawin Worrasangasilpa
Hi,
Lately, I have been working with big summation terms and what I do mostly
is to simplify or unfold it line by line. But then yesterday I found some
weird problem that is when I want to fold a specific term in the expression
below I couldn't get it done by simp, auto or blast as I used to do.
...
also have "... = (∑a∈{f. ∀x. x ∉ {..<n} ⟶ f x = False}. pmf (w_i_pmf n) a
*⇩R
(*Φ_n i (map a [0..<n])* - Φ_n (i-1) (map a [0..<n])))"
using expectation_return_pmf
by (simp add: Δ_n_def)
...
also have "... = (∑a∈{f. ∀x. x ∉ {..<n} ⟶ f x = False}. pmf (w_i_pmf n) a
*⇩R
(*real_of_int (fst (rev_m (drop (length (map a [0..<n]) - i) (map a
[0..<n]))))*
* + α * real_of_int (min 0 (snd (rev_m (drop (length (map a [0..<n]) - i)
(map a [0..<n])))))*)
- Φ_n (i-1) (map a [0..<n]))"
since I have
definition Φ_n :: "nat ⇒ bool list ⇒ real" where
"Φ_n n l= (λp. real_of_int (fst p) + α * (real_of_int (min 0 (snd p))))
(rev_m (drop (size l - n) l))".
usually, it should be trivial and done by (simp add: Φ_n_def), but this
time it doesn't work. So I would like to ask if there is any tactic that we
can use to replace the exact term at the exact place in an expression with
some term either simpler or more complicated if we know they are equal. I
have never had this problem before and had no idea how trivial it was but I
couldn't find a way to solve it.
Thanks,
Kawin

[Manuel Eberl]

There is also the less fancy "subst", which performs a single rewrite
step in the goal. If there is more than one possible place for the
rewrite, the positions can be chosen with a number, e.g. "apply (subst
(2 4 5) my_equation)". Assumptions can be rewritten with an additional
"(asm)" option.

Manuel

Post by Simon Wimmer
Hi Kawin,
there is the rewrite method in "HOL-Library.Rewrite".
You can have a look at src/HOL/ex/Rewrite_Examples.thy for usage examples.
Simon

Post by Kawin Worrasangasilpa
Hi,
Lately, I have been working with big summation terms and what I do mostly
is to simplify or unfold it line by line. But then yesterday I found some
weird problem that is when I want to fold a specific term in the expression
below I couldn't get it done by simp, auto or blast as I used to do.
...
also have "... = (∑a∈{f. ∀x. x ∉ {..<n} ⟶ f x = False}. pmf (w_i_pmf n) a
*⇩R
(*Φ_n i (map a [0..<n])* - Φ_n (i-1) (map a [0..<n])))"
using expectation_return_pmf
by (simp add: Δ_n_def)
...
also have "... = (∑a∈{f. ∀x. x ∉ {..<n} ⟶ f x = False}. pmf (w_i_pmf n) a
*⇩R
(*real_of_int (fst (rev_m (drop (length (map a [0..<n]) - i) (map a
[0..<n]))))*
* + α * real_of_int (min 0 (snd (rev_m (drop (length (map a [0..<n]) - i)
(map a [0..<n])))))*)
- Φ_n (i-1) (map a [0..<n]))"
since I have
definition Φ_n :: "nat ⇒ bool list ⇒ real" where
"Φ_n n l= (λp. real_of_int (fst p) + α * (real_of_int (min 0 (snd p))))
(rev_m (drop (size l - n) l))".
usually, it should be trivial and done by (simp add: Φ_n_def), but this
time it doesn't work. So I would like to ask if there is any tactic that we
can use to replace the exact term at the exact place in an expression with
some term either simpler or more complicated if we know they are equal. I
have never had this problem before and had no idea how trivial it was but I
couldn't find a way to solve it.
Thanks,
Kawin