*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Simp, cong, and intro*From*: Holden Lee <hl422 at cam.ac.uk>*Date*: Thu, 24 Jul 2014 19:24:20 +0100*Sender*: oldheneel at gmail.com

In general I can't seem to get auto/simp to check conditions thoroughly. Here is an example. lemma (in module) mult1: assumes h1: "finite S" and h2: "S⊆ carrier M" shows "(⨁⇘M⇙x∈S. 𝟭⇘R⇙⊙⇘M⇙ x) = (⨁⇘M⇙x∈S. x) " proof - from assms show ?thesis ........................ done qed I tried *apply (auto cong: finsum_cong')* but this doesn't work. Here, the following does work:* apply (intro finsum_cong', auto)*. (But in more complicated things*, if I can't use auto/simp then I'm forced to break the problem into pieces by subgoal_tac.) I'm confused as to why intro would be stronger than cong here (especially since the name finsum_cong' suggests that it be used as a congruence rule). In general what does "intro" do that auto/simp cong does not? To my understanding, when simp wants to prove P and P appears in the conclusion of a simp rule, it should try to prove the premises of the rule; wouldn't this be the same as intro? What I would imagine the simplifier does above is (1) look at finsum_cong' "[| A = B; g ∈ B -> carrier G; !!i. i ∈ B ==> f i = g i |] ==> finsum G f A = finsum G g B" and from this, try to show (1) S=S (2) g∈ S -> carrier M (3) !!x∈ B ==>𝟭⇘R⇙⊙⇘M⇙ x = x (2) should be discharged by the simp rule Pi_I'[simp]: "(!!x. x : A --> f x : B x) ==> f : Pi A B", the fact that S⊆ carrier M, and hence that %x. x is in S->carrier M (in fact this is another simp rule in FuncSet) (3) should be simplified by the module axioms (declared simp). Thanks, Holden *Another example ... ==> (⨁⇘V⇙v∈S. (λv∈S. m1 v ⊕⇘K⇙ m2 v) v ⊙⇘V⇙ v) = (⨁⇘V⇙v∈S. m1 v ⊙⇘V⇙ v) ⊕⇘V⇙ (⨁⇘V⇙v∈S. m2 v ⊙⇘V⇙ v) I pass to auto/simp a rule that combines sums over the same set provided that the terms are in the carrier, so I would expect the RHS to be rewritten (but it's not). There are of course also simp/intro rules for showing that a sum of terms in carrier V is also in carrier V, and that scalar multiplication of terms in carrier V is also in carrier V. Here is part of the simp_trace, if it helps. (I don't know how to read it.) [4]SIMPLIFIER INVOKED ON THE FOLLOWING TERM: x ∈ S ⟹ ?g x ∈ carrier M ≡ ?Q'1 [4]Adding rewrite rule "??.unknown": x ∈ S ≡ True [3]SUCCEEDED x ∈ S ⟶ ?g x ∈ carrier M ≡ x ∈ S ⟶ ?g x ∈ carrier M [2]FAILED (⋀x. x ∈ S ⟶ ?g x ∈ carrier M) ⟹ ?g ∈ S → carrier M ≡ True [1]Congruence proof failed. Could not prove S ≡ ?B ⟹ ?g ∈ ?B → carrier M ⟹ (⋀i. i ∈ ?B ⟹ 𝟭 ⊙⇘M⇙ i ≡ ?g i) ⟹ finsum M (op ⊙⇘M⇙ 𝟭) S ≡ finsum M ?g ?B

- Previous by Date: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Next by Date: Re: [isabelle] Isabelle2014-RC0: lift_definition ignores no_code
- Previous by Thread: Re: [isabelle] returning to the original document in Isabelle/jedit
- Next by Thread: Re: [isabelle] print_statement and sorts
- Cl-isabelle-users July 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