Mete Polat (Jun 25 2024 at 11:09): Mete Polat (Jun 25 2024 at 11:09):What is the difference between adding facts to the goal premise with keywords like using in comparison to adding them to the simplifier with simp add: fact and the no_asm_simp attribute?
Specifically this fails:
theorem "card a = 2 ⟹ card b = 3 ⟹ card (a × b) = 6"
using card_cartesian_product by (simp (no_asm_simp))
This works:
theorem "card a = 2 ⟹ card b = 3 ⟹ card (a × b) = 6"
by (simp add: card_cartesian_product)
From the documentation:
Note that the original goal premises and chained facts are subject to simplification themselves, while declarations via add/del merely follow the policies of the object-logic to extract rewrite rules from theorems, without further simplification. This may lead to slightly different behavior in either case, which might be required precisely like that in some boundary situations to perform the intended simplification step!
I thought adding no_asm_simp would equalize their behavior:
assumptions are used in the simplification of the conclusion but are not themselves simplified
Am I missing something here?
Mathias Fleury (Jun 29 2024 at 07:44):declare [[simp_trace]] is your friend:
[1]Cannot add premise as rewrite rule because it contains (type) unknowns:
⋀A B. card (A × B) = card A * card B
Last updated: Dec 21 2024 at 16:20 UTC