*To*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Subject*: Re: [isabelle] Evaluation of List.coset*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 31 Jan 2013 13:54:21 +0100*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAL0S8BfSAy1SSUcG0O5E5H2Hc9PqmJQ3k6SVkJx43NPJopzU+Q@mail.gmail.com>*References*: <CAL0S8BcgWBZ4fJApxHYECNPx-TL+yWofkFAawq73N1AEP_D=sg@mail.gmail.com> <5108C956.5020205@inf.ethz.ch> <CAL0S8BdBNq6AL72fjQYNQSBFW=eipdP72YTEuoAvZm1M1o9mAg@mail.gmail.com> <alpine.LNX.2.00.1301301334000.30318@macbroy21.informatik.tu-muenchen.de> <CAL0S8Bf-HGcDqzH5F9XLgjn6VF604JT7MNOrpkQHGUmuD43Efg@mail.gmail.com> <510A2235.7080900@inf.ethz.ch> <CAL0S8BfSAy1SSUcG0O5E5H2Hc9PqmJQ3k6SVkJx43NPJopzU+Q@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130106 Thunderbird/17.0.2

Dear Jesus,

1. You instantiate the type class equal by definition "equal_bit0 x y = (x = y)"

lemma equal_bit0_code [code]: "equal_class.equal x y = (Rep_bit0 x = Rep_bit0 y)" by(simp add: equal_eq Rep_bit0_inject) lemma equal_bit1_code [code]: "equal_class.equal x y = (Rep_bit1 x = Rep_bit1 y)" by(simp add: equal_eq Rep_bit1_inject)

lemma [code abstract]: "Rep_bit0 (Abs_bit0' x :: 'a :: {finite, card_UNIV} bit0) = x mod int (CARD('a bit0))" apply(simp add: Abs_bit0'_def) apply(rule Abs_bit0_inverse) apply simp

lemma [code abstract]:

apply(simp add: Abs_bit1'_def) apply(rule Abs_bit1_inverse) apply simp

instantiation bit1 :: (type) finite_UNIV begin definition "finite_UNIV = Phantom('a bit1) True" instance sorry end instantiation bit1 :: (card_UNIV) card_UNIV begin

instance sorry end instantiation bit0 :: (type) finite_UNIV begin definition "finite_UNIV = Phantom('a bit0) True" instance sorry end instantiation bit0 :: (card_UNIV) card_UNIV begin

instance sorry end instantiation num0 :: card_UNIV begin definition "finite_UNIV = Phantom(num0) False" definition "card_UNIV = Phantom(num0) 0" instance sorry end instantiation num1 :: card_UNIV begin definition "finite_UNIV = Phantom(num1) True" definition "card_UNIV = Phantom(num1) 1" instance sorry end

I send attached a file where some examples of evaluations over "finite_n" types succeed, whereas the same evaluations over Numeral_Types (bit0 and bit1) do not terminate; in the file can be also found some instantiations that I missed in the Library (some of them were required for the bit0 and bit1 types to be evaluated): - bit0 and bit1 are intances of "equal" - bit0 and bit1 are instances of "linorder" - bit0 and bit1 are instances of "enum"

Best, Andreas

**References**:**[isabelle] Evaluation of List.coset***From:*Jesus Aransay

**Re: [isabelle] Evaluation of List.coset***From:*Andreas Lochbihler

**Re: [isabelle] Evaluation of List.coset***From:*Jesus Aransay

**Re: [isabelle] Evaluation of List.coset***From:*Makarius

**Re: [isabelle] Evaluation of List.coset***From:*Jesus Aransay

**Re: [isabelle] Evaluation of List.coset***From:*Andreas Lochbihler

**Re: [isabelle] Evaluation of List.coset***From:*Jesus Aransay

- Previous by Date: Re: [isabelle] Evaluation of List.coset
- Next by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Previous by Thread: Re: [isabelle] Evaluation of List.coset
- Next by Thread: [isabelle] LaTeXsugar
- Cl-isabelle-users January 2013 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