Email Gateway (Aug 19 2022 at 15:49): Email Gateway (Aug 19 2022 at 15:49):From: Holden Lee <hl422@cam.ac.uk>
Working with abstract algebra (with locales) requires always showing
elements are in the carrier before concluding anything with them. Using
type classes, this would be automatic from type-checking. I feel like there
should be a way to make it as automatic with carriers by declaring the
right simp rules, but so far I've had no success, and have to continually
pipe in facts about elements being in the carrier every time I want to
prove something. Does anyone know a way to get around this?
I can get it to do basic things like: if a, b are in the carrier then a*b+c
is in the carrier. But I am working with finite sums, where congruence
rules and not just simp rules are required.
I've set up a baby example to see where the problem is.
Suppose I have a simp rule and congruence rules (think of F being like sum
or finsum, for instance)
lemma simp_rule:
fixes x
assumes "x∈S"
shows "a x = b x"
sorry
lemma rule_cong':
"[|A=B; !! x. x∈A ==> f x = g x|] ==> F A f = F B g"
sorry
(cong)
lemma rule_cong:
"[|A=B; !!x. x∈A =simp=> f x = g x|] ==> F A f = F B g"
sorry
Then Isabelle successfully solves the following, as expected (by
simplifying the LHS to F S b, then the RHS also to F S b).
lemma test_cong':
"F S (λx. if (x∈S) then b x else 0) = F S a"
by (auto cong: rule_cong simp add: simp_rule)
But Isabelle stumbles on the following:
lemma* test_congT'*:
"F T (λx. if (x∈S) then b x else 0) = F T a"
proof -
have 1:"T⊆S" by (unfold T_def S_def, auto)
from 1 show ?thesis
apply (auto cong: rule_cong simp add: simp_rule elim!: subsetD)
(fails* - also with cong/cong' elim!/intro*)
(subsetD: ?A ⊆ ?B ==> ?c ∈ ?A ==> ?c ∈ ?B)
The problem is that applying the congruence rule it fails to show x\in S.
With the assumption T⊆S and x∈T and subsetD declared as an elim rule
explicitly, it should conclude x∈S. Why doesn't it, and how can I get it to
do this?
The application is that F is finsum/finprod and the expression inside
simplifies on the condition that x∈carrier G, while the set T is a
subset of carrier G
For easy experimentation, here is the file:
https://dl.dropboxusercontent.com/u/27883775/work/Isabelle/TestTactics.thy
-Holden
Email Gateway (Aug 19 2022 at 15:49):From: Lawrence Paulson <lp15@cam.ac.uk>
You may have luck with
apply (auto cong: rule_cong simp add: simp_rule subsetD [OF 1])
Auto doesn’t use “elim!” inside the simplifier, but outside it, so it cannot help.
The point of my suggestion is to instantiate the variables in subsetD.
Larry
Last updated: Nov 21 2024 at 12:39 UTC