*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Getting cong to work with carriers*From*: Holden Lee <hl422 at cam.ac.uk>*Date*: Sat, 9 Aug 2014 10:20:37 +0100*Sender*: oldheneel at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Getting cong to work with carriers***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Changing axiom names in a locale
- Next by Date: Re: [isabelle] Getting cong to work with carriers
- Previous by Thread: [isabelle] Discussing RC issues in separate threads
- Next by Thread: Re: [isabelle] Getting cong to work with carriers
- Cl-isabelle-users August 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list