isabelle - How to get a typedef type to inherit operators from its mother type for type classes -

post answer follow question

brian provided answer suggested solution being use lifting , transfer. however, can't find enough tutorial information on lifting , transfer know how tweak answer finish off need do.

here, work in dark, , use answer given plug'n'play template ask follow question.

the command in initial code, typedef trivalg = "{x::st. x = ems}" gives me new type subset of mother type st.

i have membership operator consts inp :: "st => st => bool", , in naive view of lifting , transfer, since monoid_add 0 has been defined being constant ems::st, , can make statement, (ems::st) inp ems, want this:

theorem "~((0::trivalg) inp 0)" 

so, try use lifting operator inp work type trivalg this:

lift_definition inp_trivalg :: "trivalg => trivalg => bool"   "% x y. (x inp y)"    simp  theorem "~((0::trivalg) inp 0)"  theorem "(ems::trivalg) = ems" 

however, type clashes use of theorem because use of type st , trivalg aren't compatible.

if answer can added to show me how inp work type trivalg appreciate it. or, maybe i'm way off mark.

preliminaries (original) question

i have type st, represents "everything set". far, constants , operators have been defined single type st. example, empty set, membership operator, , union operator defined this:

consts ems :: "st" consts inp :: "st => st => bool" consts geu :: "st => st" 

i'm doing investigating whether can tie st generalized groups in groups.thy.

from hol document, i'm trying examples sections 4.2, 4.3, , 4.4 of groups, , 15.2 , 15.3 of nat.

here, i'm question, don't know enough know whether i'm asking intelligent question. think know solution may locales, sublocales, , interpretations rather type classes.

i've been looking little @ locales.pdf , classes.pdf, , know locales , classes intertwined. i've been looking @ isarmathlib see how locales, sublocales, , interpretations being used there.

the question

my question is, trivial algebraic structure below, trivalg, new type defined typedef, how can set things type classes can use constants, such ems, inp, , geu listed above, elements of type trivalg?

after list code below, ask questions specific lines of code in groups.thy.

the code

typedef trivalg = "{x::st. x = ems}"   auto  instantiation trivalg :: 0 begin definition trivalg_zero:   "0 = abs_trivalg ems" instance .. end  instantiation trivalg :: monoid_add begin definition plus_trivalg:   "m + n = (abs_trivalg ems)"  instance proof   fix n m q :: trivalg   show "(n + m) + q = n + (m + q)"     by(metis plus_trivalg)   show "0 + n = n"     apply(induct n) apply(auto)     by(metis plus_trivalg)   show "n + 0  = n"     apply(induct n) apply(auto)     by(metis plus_trivalg) qed end  theorem   "((n::trivalg) + m) + q = n + (m + q)"   by(metis plus_trivalg)  theorem   "((0::trivalg) + 0) = 0"   by(metis monoid_add_class.add.left_neutral) 

a subsequent question groups.thy

on lines 151 155 in groups.thy, there following code:

class semigroup_add = plus +   assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = + (b + c)"  sublocale semigroup_add < add!: semigroup plus proof qed (fact add_assoc)  

there's no 1 document teach me how use classes, locales, sublocales, , interpretations, don't know tells me.

if want use semigroup_add that's in groups.thy, have choice of using either type class or locale?

to corresponding operations on type trivalg, easiest way use isabelle's lifting package; can use transfer package prove class instances. here example:

typedef trivalg = "{x::st. x = ems}"   auto  setup_lifting type_definition_trivalg  instantiation trivalg :: 0 begin lift_definition zero_trivalg :: "trivalg" "ems" . instance .. end  instantiation trivalg :: monoid_add begin lift_definition plus_trivalg :: "trivalg => trivalg => trivalg"   "% x y. ems" simp  instance proof   fix n m q :: trivalg   show "(n + m) + q = n + (m + q)"     transfer simp   show "0 + n = n"     transfer simp   show "n + 0  = n"     transfer simp qed end