[isabelle] Getting cong to work with carriers



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.